[wp] removed semantics dir

0cba9655 · Loïc Correnson · François Bobot · 445a43f3 · 445a43f3 · 445a43f3
Commit 0cba9655 authored 5 years ago by Loïc Correnson Committed by François Bobot 5 years ago
--- a/src/plugins/wp/semantics/Cil.v
+++ b/src/plugins/wp/semantics/Cil.v
-Require Import Datatype.
-Require Import Primitive.
-Parameter cvar : Data.
-Parameter cfield : Data.
-Parameter ctypedef : Data.
-Parameter label : Data.
-Inductive cref : Set :=
-  | Rvoid : cref
-  | Rint : cint -> cref
-  | Rflt : cflt -> cref
-  | Rdef : ctypedef -> cref.
-Inductive ctype : Set := 
-  | Cptr : cref -> ctype
-  | Cint : cint -> ctype
-  | Cflt : cflt -> ctype
-  | Carray  : ctype -> Z -> ctype
-  | Cstruct : [ cfield => ctype ] -> ctype
-  | Cunion  : [ cfield => ctype ] -> ctype.
-Record cenv : Type := {
-  g_var : cvar -> ctype ;
-  g_typedef : ctypedef -> ctype
-}.
-Inductive lval : Set :=
-  | Lvar : cvar -> lval
-  | Lshift : lval -> exp -> lval
-  | Lfield : lval -> cfield -> lval
-  | Lderef : exp -> lval
-with exp : Set :=
-  | Lval   : lval -> exp
-  | AddrOf : lval -> exp
-  | Shift  : exp -> exp -> exp
-  | Op     : op -> exp -> exp -> exp.
-Inductive instr : Set :=
-  | Instr : lval -> exp -> instr
-  | Guard : exp -> instr.
-Definition stmt := ( label * instr * label )%type.
-Definition program := List.list stmt.
--- a/src/plugins/wp/semantics/Datatype.v
+++ b/src/plugins/wp/semantics/Datatype.v
-(** Basic Datatypes *)
-Set Implicit Arguments.
-Require Export Bool.
-Require Export Reals.
-Require Export ZArith.
-Require Export Program.
-Open Scope Z_scope. 
-(** ** Tactics for finishing proof trees. *)
-Ltac forward := 
-  repeat (first [ split | intros ]) ; 
-  try discriminate ; 
-  try contradiction ; 
-  try tauto ; 
-  try constructor ; 
-  try (apply False_ind ; omega ; fail) ;
-  try (apply False_ind ; auto with zarith ; fail) ;
-  auto with zarith.
-Ltac finish := forward ; fail.
-Tactic Notation "by" tactic(A) := A ; finish.
-(** ** Empty Set. *)
-Inductive Void : Set := .
-(** ** Unit Set. *)
-Inductive Unit : Set := unit.
-(** ** Decidability. *)
-Definition decide P := {P}+{~P}.
-Definition isTrue p := (p = true).
-Definition isFalse p := (p = false).
-(*
-Lemma not_is_true  : forall p, ~(isTrue p) -> isFalse p.
-Lemma not_is_false : forall p, ~(isFalse p) -> isTrue p.
-*)
-Coercion bool2p := isTrue.
-Lemma split_andb : forall p q, p && q <-> p /\ q. 
-Proof. intros p q. induction p ; induction q ; intuition. Qed.
-Lemma split_orb  : forall p q, p || q <-> p \/ q. 
-Proof. intros p q. induction p ; induction q ; intuition. Qed.
-(** ** Types with decidable equality. *)
-Record Data := {
-  type :> Set ;
-  eqdec : forall (a b : type), decide (a=b)
-}.
-Definition eqb {D : Data} (a b : D) :=
-  match eqdec _ a b with
-  | left _ => true
-  | right _ => false
-  end.
-Notation "a == b" := (@eqb _ a b) (at level 70).
-(** ** Tactics for proof by case on Data equality. *)
-Lemma eqb_true : forall (D : Data) (x y : D), x=y -> (x==y) = true.
-Proof. intros. rewrite H. unfold eqb. induction (eqdec _ y y). trivial. auto. Qed.
-Lemma eqb_false : forall (D : Data) (x y : D), x<>y -> (x==y) = false.
-Proof. intros. unfold eqb. induction (eqdec _ x y). rewrite a in H. intuition. trivial. Qed.
-Ltac equality a b :=
-  let Eq := fresh "Eq_" a "_" b in
-  let Neq := fresh "Neq_" a "_" b in
-  induction (eqdec _ a b) as [ Eq | Neq ] ; 
-  [ try (rewrite Eq in *) ; try (rewrite eqb_true in *) 
-  | try (rewrite Neq in *) ; try (rewrite eqb_false in *)
-  ] ; auto.
-(** ** Dependent Equalities. *)
-(** Lift an equality [x = y] into an equality over [u : B x] and [v : B y]. *)
-Definition lift_eq {A : Set} (B : A -> Set) {x y : A} (p : x = y) : B x -> B y -> Prop :=
-  let P := fun z => B x -> B z -> Prop in
-  let E := (@eq (B x)) in
-  eq_rect x P E y p.
-(** List is the expected equality. *)
-Lemma lift_eq_is_eq : 
-  forall (A : Set) (B : A -> Set) x, 
-  lift_eq B (eq_refl x) = (fun (y z : B x) => y = z).
-Proof. intros. simpl. trivial. Qed.
-(** ** Typical Data *)
-Program Definition Int : Data := {| type := Z |}.
-Next Obligation. apply Z.eq_dec. Qed.
-Lemma fst_neq : forall A B, forall (p q : A*B), fst p <> fst q -> p <> q.
-  Proof. intros. unfold not. intro E. rewrite E in H. auto. Qed.
-Lemma snd_neq : forall A B, forall (p q : A*B), snd p <> snd q -> p <> q.
-  Proof. intros. unfold not. intro E. rewrite E in H. auto. Qed.
-Program Definition Pair (A B : Data) : Data := {| type := A * B |}.
-Next Obligation.
-  elim (eqdec A t1 t) ; elim (eqdec B t2 t0) ; intros.
-  * left. rewrite a,a0. trivial.
-  * right. apply snd_neq. auto.
-  * right. apply fst_neq. auto.
-  * right. apply fst_neq. auto.
-Qed.
-(** ** Functional Updates *)
-Definition select {A B : Type} {P : A -> Prop} (s : forall a, decide(P a)) (a b : A -> B) 
-  := fun k => if s k then a k else b k.
-(** ** Finite Environments *)
-Inductive env {A B : Type} : Type :=
-  | empty : env
-  | add : A -> B -> env -> env.
-Notation "[ A => B ]" := (@env A B).
-Fixpoint map {A B C : Type} (f : A -> B -> C) (e : [A => B]) : [A => C] :=
-  match e with
-  | empty => empty
-  | add x v e => add x (f x v) (map f e)
-  end.
-Fixpoint find {A : Data} {B : Type} (x : A) e (d : B) :=
-  match e with	
-  | empty => d
-  | add x' v e => if x == x' then v else find x e d
-  end.
-Fixpoint bind {A : Data} {B : Type} (x : A) (v : B) e : Prop :=
-  match e with
-  | empty => False
-  | add x' v' e => if x == x' then v = v' else bind x v e
-  end.
-Lemma bind_map_exists :
-  forall (A : Data) (B C : Type) (f : A -> B -> C),
-    forall x w e, bind x w (map f e) -> exists v, bind x v e /\ w = f x v.
-Proof.
-  intros.
-  induction e.
-  * by (simpl in H).
-  * simpl in H. equality x a. 
-    - exists b. simpl. rewrite eqb_true ; auto.
-    - simpl. rewrite eqb_false ; auto.
-Qed.
-Lemma bind_map :
-  forall (A : Data) (B C : Type) (f : A -> B -> C),
-    forall x v e, bind x v e -> bind x (f x v) (map f e).
-Proof.
-  intros.
-  induction e ; simpl in * ; auto.
-  equality x a ; rewrite H ; auto.
-Qed.
-Inductive subset {A B : Type} : [ A => B ] -> [ A => B ] -> Prop :=
-  | Sub_empty : subset empty empty
-  | Sub_skip  : forall a b w1 w2, subset w1 w2 -> subset w1 (add a b w2)
-  | Sub_same  : forall a b w1 w2, subset w1 w2 -> subset (add a b w1) (add a b w2).
-(** ** Records (dependent maps) *)
-Inductive record {A : Type} : [ A => Type ] -> Type :=
-  | Rempty : record empty
-  | Rfield : forall (a:A) {t:Type} (v:t) 
-                          {r:[A => Type]} (R:record r),
-                          record (add a t r).
-Notation "{[ m ]}" := (record m).
-Inductive union {A : Type} :  [ A => Type ] -> Type :=
-  | Uempty : union empty
-  | Uskip  : forall (a:A) { t: Type } (* no value *)
-                          { u: [A => Type] } (U:union u),
-                          union (add a t u)
-  | Ufield : forall (a:A) { t: Type } (v:t) (* some value *)
-                          { u: [A => Type] } (U:union u),
-                          union (add a t u).
-Notation "{[ m ?]}" := (union m).
-(** ** Positive integers *)
-Coercion Z.pos : positive >-> Z.
-(** ** Finite integers *)
-Record range (n : Z) : Type :=
-  { index :> Z ; in_range : 0 <= index < n }.
-Definition range_dec (n k : Z) : decide (0 <= k < n).
-Proof.
-  induction (Z_le_dec 0 k) ; induction (Z_lt_dec k n) ; try (by left) ; try (by right).
-Qed.
-Fixpoint iter (P : nat -> bool) n := 
-  match n with
-  | O => true
-  | S n => P n && iter P n
-  end.
-Lemma iter_forall : 
-  forall P n, iter P n -> (forall k, (k < n)%nat -> P k).
-Proof.
-  intros P n.
-  induction n.
-  * simpl. intros. omega.
-  * simpl. intros Step k Rk.
-    rewrite split_andb in Step.
-    assert (Rn : (k <= n)%nat) by omega.
-    induction (le_lt_eq_dec k n) as [Lt | Eq] ; auto with arith.
-    + by (apply IHn).
-    + by (rewrite Eq).
-Qed.
-(** ** Arrays of known size *)
-Definition array (A : Type) (n : Z) : Type := range n -> A.
-Notation "a [ n ]" := (array a n) (at level 10).
-Definition slice {A} p n (w : Z -> A) : A[n] := fun k : range n => w (p+k).
-Definition get {A n} (a : A[n]) k rk := a {| index := k ; in_range := rk |}.
-Implicit Arguments get [A n].
-Definition split {n m} (k : range (n+m)) : {0 <= k < n}+{0<= k-n < m}.
-Proof. 
-  generalize (in_range k). intro Rk.
-  induction (range_dec n k) ; [ left | right] ; forward.
-Qed.
-Definition concat {A n m} (a : A[n]) (b : A[m]) : A[n+m] :=
-  fun k : range (n+m) =>
-    match split k with
-    | left p => get a k p
-    | right q => get b (k-n) q
-    end.
-Lemma concat_l {A n m} (a : A[n]) (b : A[m]) :
-  forall (k : range (n+m)) (r : 0 <= k < n), (concat a b) k = get a k r.
-Proof.
-  intros.
-  unfold concat.
-  destruct (split k).
-  + apply f_equal. apply proof_irrelevance.
-  + generalize (in_range k). intros. omega.
-Qed.
-Lemma concat_r {A n m} (a : A[n]) (b : A[m]) :
-  forall (k : range (n+m)) (r : 0 <= k-n < m), (concat a b) k = get b (k-n) r.
-Proof.
-  intros.
-  unfold concat.
-  destruct (split k).
-  + generalize (in_range k). intros. omega.
-  + apply f_equal. apply proof_irrelevance.
-Qed.
-Lemma array_inj {A n} : forall (a b : A[n]),
-  (forall k : range n, a k = b k) -> a = b.
-Proof.
-  intros a b Elt.
-  extensionality k.
-  apply Elt.
-Qed.
-Record vector (A : Type) : Type := { size ; elt :> A[size] }.
-Notation "a []" := (vector a) (at level 10).
-Definition compatible {A n m} (a : A[n]) (b : A[m]) :=
-  forall k (ka : 0 <= k < n) (kb : 0 <= k < m), 
-    get a k ka = get b k kb.
--- a/src/plugins/wp/semantics/Layout.v
+++ b/src/plugins/wp/semantics/Layout.v
-Require Import Datatype.
-Require Import Pointer.
-Require Import Machine.
-Open Scope Z_scope.
-Program Definition empty_layout (A : Type) : layout A := {|
-  sizeof := 0 ;
-  encoding := fun p w => True
-|}.
-Next Obligation. intuition. Qed.
-Program Definition interpret {A B} (phi : B -> A) : layout A -> layout B := 
-  fun enc => {| encoding := fun v w => enc (phi v) w ; sizeof := sizeof enc |}.
-Next Obligation.
-  by (apply (positive enc)).
-Qed.
-Next Obligation.
-  apply (footprint enc H).
-Qed. 
-Program Definition concat {A B} : layout A -> layout B -> layout (A*B) :=
-  fun a b => {| 
-    sizeof := sizeof a + sizeof b ;
-    encoding := fun p w => (a (fst p) w /\ b (snd p) (w <+> sizeof a)) 
-  |}.
-Next Obligation.
-  generalize (positive a).
-  generalize (positive b).
-  auto with zarith.
-Qed.
-Next Obligation.
-  simpl.
-  cut (b b0 (wa <+> sizeof a) <-> b b0 (wb <+> sizeof a)).
-  cut (a a0 wa <-> a a0 wb).
-  intuition.
-  * apply (footprint a).
-      unfold eq_range. 
-      intros k R. apply H.
-      generalize (positive a).
-      generalize (positive b).
-      auto with zarith.
-  * apply (footprint b).
-      unfold eq_range.
-      intros k R. unfold offset. apply H.
-      generalize (positive a).
-      generalize (positive b).
-      auto with zarith.
-Defined.
-Program Definition superpose {A B} : layout A -> layout B -> layout (A * B) :=
-  fun a b => {|
-    sizeof := Z.max (sizeof a) (sizeof b) ;
-    encoding := fun p w => (a (fst p) w /\ b (snd p) w)
-  |}.
-Next Obligation.
-  apply Z.max_case. apply (positive a). apply (positive b).
-Qed.
-Next Obligation.
-  simpl.
-  cut (b b0 wa <-> b b0 wb).
-  cut (a a0 wa <-> a a0 wb).
-  intuition.
-  * apply (footprint a).
-      unfold eq_range. 
-      intros k R. apply H. 
-      generalize (Z.le_max_l (sizeof a) (sizeof b)).
-      omega.
-  * apply (footprint b).
-      unfold eq_range.
-      intros k R. apply H.
-      generalize (Z.le_max_r (sizeof a) (sizeof b)).
-      omega.
-Defined.
-Program Definition concat_n {A} : layout A -> forall n, layout (A[n]) :=
-  fun a n => {|
-    sizeof := Z.max 0 (n * sizeof a) ;
-    encoding := fun v w => forall (k : range n), a (v k) (w <+> k * sizeof a)
-  |}.
-Next Obligation.
-  by (apply Z.le_max_l). 
-Qed.
-Next Obligation.
-  cut (forall k : range n, a (v k) (wa <+> k * sizeof a) 
-                       <-> a (v k) (wb <+> k * sizeof a)).
-  intuition ; apply H0 ; apply H1.
-  intro k.
-  apply (footprint a).
-    unfold eq_range, forall_range, offset. intros i Ri. simpl. apply H.
-    generalize (in_range k). intro Rk.
-    generalize (positive a). intro Pa.
-    rewrite Z.max_r ; auto with zarith.
-    assert (R1 : k <= n-1) by auto with zarith.
-    assert (R2 : k * sizeof a <= (n-1) * sizeof a) 
-       by (apply Zmult_le_compat_r ; forward).
-    assert (R3 : (n-1) * sizeof a = n * sizeof a - sizeof a) by ring.
-    rewrite R3 in R2.
-    auto with zarith.
-Defined.
-Program Definition option_layout {A} : layout A -> layout (option A) :=
-  fun a => {|
-    sizeof := sizeof a ;
-    encoding := fun v w => 
-      match v with
-      | None => forall x, not (a x w)
-      | Some x => a x w
-      end
-  |}.
-Next Obligation. exact (positive a). Qed.
-Next Obligation.
-  induction v.
-  + apply (footprint a H).
-  + generalize (footprint a H).
-    intuition.
-    apply (H1 x). by (rewrite H0).
-    apply (H1 x). by (rewrite <- H0).
-Qed.
--- a/src/plugins/wp/semantics/Machine.v
+++ b/src/plugins/wp/semantics/Machine.v
-Require Import Datatype.
-Require Import Primitive.
-Require Import Pointer.
-Set Implicit Arguments.
-Inductive byte : Type :=
-  | Byte  : forall b, 0 <= b < 255 -> byte
-  | Ptr   : Addr -> nat -> byte
-  | Undef : byte.
-Inductive perm := Read | Write.
-Definition grants p q := p = Write \/ q = Read.
-Definition granted q p := p = Write \/ q = Read. 
-Definition bytes := Z -> byte.
-Definition perms := Z -> perm.
-Record layout (A : Type) := {
-  encoding :> A -> bytes -> Prop ;
-  sizeof : Z ;
-  positive : 0 <= sizeof ;
-  footprint : forall {wa wb},
-      	      wa =/ sizeof wb ->
-      	      forall v, encoding v wa <-> encoding v wb
-}.
-Record architecture := {
-  int_layout : cint -> layout Z ;
-  flt_layout : cflt -> layout R ;
-  ptr_layout : layout Addr ;
-  char_size  : sizeof (int_layout char) = 1
-}.
-Record mem := { 
-  byte_at : Addr -> byte ;
-  perm_at : Addr -> perm ;
-  arch :> architecture
-}.
-Definition undef {A} : A -> byte := fun _ => Undef.
-Definition mload (m : mem) (p : Addr) (n : Z) : bytes :=
-  select (range_dec n) (byte_at m @ p) undef.
-Definition store (m : mem) (p : Addr) n (v : bytes) : mem := 
-{|
-  arch := m ;
-  perm_at := perm_at m ;
-  byte_at := select (ptr_range p n) (v & p) (byte_at m)
-|}.
-Definition valid (pi : perm) (m : mem) (p : Addr) n : Prop :=
-  (fun k => grants (perm_at m (shift p k)) pi) /: n.
-Record read {A} (T : layout A) 
-  (m : mem) (p : Addr) (a : A) : Prop 
-:= {
-  valid_read :> valid Read m p (sizeof T) ;
-  value_read :> T a (mload m p (sizeof T))
-}.
-Record written {A} (T : layout A)
-  (m : mem) (p : Addr) (a : A) (v : bytes) (m' : mem) : Prop
-:= {
-  valid_write :> valid Write m p (sizeof T) ;
-  value_write :> T a v ;
-  mem_write : m' = store m p (sizeof T) v
-}.
-Definition write {A} (T : layout A)
-  (m : mem) (p : Addr) (a : A) (m' : mem) : Prop 
-  := exists v, written T m p a v m'.
--- a/src/plugins/wp/semantics/Makefile
+++ b/src/plugins/wp/semantics/Makefile
-.PHONY: all depend
-MODULES= Datatype Primitive Cil Pointer Machine Layout Values Typing Semantics
-INCLUDES= -I .
-SOURCES=$(addsuffix .v, $(MODULES))
-OBJECTS=$(addsuffix .vo, $(MODULES))
-all: $(OBJECTS)
-.SUFFIXES: .v .vo
-.v.vo:
-	coqc $(INCLUDES) $<
-depend:
-	coqdep $(INCLUDES) $(SOURCES) > .depend
-clean:
-	rm -f *~ *.vo *.glob
-sinclude .depend
--- a/src/plugins/wp/semantics/Pointer.v
+++ b/src/plugins/wp/semantics/Pointer.v
-Require Import Datatype.
-Open Scope Z_scope.
-Parameter base : Data. 
-Definition Addr := Pair base Int.
-Definition shift (p : Addr) (k : Z) : Addr := ( fst p , snd p + k ).
-Definition separated p n q m :=
-  forall i j, 0 <= i <= n -> 0 <= j <= m -> shift p i <> shift q j.
-Definition in_ptr_range (p : Addr) n q :=
-  fst p = fst q /\ snd p <= snd q < snd p + n.
-Definition ptr_range (p:Addr) n q : decide ( in_ptr_range p n q ).
-Proof.
-  unfold in_ptr_range.
-  induction (eqdec base (fst p) (fst q)) as [Eq | Neq] ;
-  induction (range_dec n (snd q - snd p)) ;
-  try (by left) ;
-  try (by right).
-Qed.
-Definition read_at_ptr {A} (phi : Addr -> A) (p : Addr) : Z -> A 
-  := fun k => phi (shift p k).
-Infix "@" := read_at_ptr (at level 70).
-Definition copy_to_ptr {A} (phi : Z -> A) (p : Addr) : Addr -> A
-  := fun (q : Addr) => phi (snd q - snd p).
-Infix "&" := copy_to_ptr (at level 70).
-Definition offset {A:Type} (m : Z -> A) (p:Z) := fun k => m (p+k).
-Infix "<+>" := offset (at level 70).
-Definition forall_range (phi : Z -> Prop) n : Prop := forall k, 0 <= k < n -> phi k.
-Infix "/:" := forall_range (at level 70).
-Definition eq_range {A : Type} n (a b : Z -> A) := (fun k => a k = b k) /: n.
-Notation "a =/ n b" := (eq_range n a b) (at level 70, n at level 0).
--- a/src/plugins/wp/semantics/Primitive.v
+++ b/src/plugins/wp/semantics/Primitive.v
-Require Import Datatype.
-Parameter cint : Data.
-Parameter cflt : Data.
-Parameter char : cint.
-Parameter irange : cint -> Z -> Prop.
-Parameter frange : cflt -> R -> Prop.
-Definition ptype := (cint + cflt)%type.
-Definition prim  := (Z + R)%type.
-Inductive prange : ptype -> prim -> Prop :=
-  | PRIM_int : forall i x, irange i x -> prange (inl i) (inl x)
-  | PRIM_flt : forall f u, frange f u -> prange (inr f) (inr u).
-Parameter op : Data.
-Parameter typeof_op : op -> ptype -> ptype -> ptype -> Prop.
-Parameter sem_op    : op -> prim ->  prim ->  prim ->  Prop.
-Inductive prim_domain : prim -> forall {t : Type}, t -> Prop :=
-  | DOMAIN_int : forall x, prim_domain (inl x) x
-  | DOMAIN_flt : forall u, prim_domain (inr u) u.
--- a/src/plugins/wp/semantics/Semantics.v
+++ b/src/plugins/wp/semantics/Semantics.v
-Require Import Datatype.
-Require Import Primitive.
-Require Import Cil.
-Require Import Pointer.
-Require Import Machine.
-Require Import Values.
-Require Import Typing.
-Record Compiler := { cc_env :> Gamma ; cc_link : cvar -> base }.
-Inductive sem_lval (G : Compiler) (m : mem) : lval -> Addr -> Prop :=
-  | Svar : forall x,
-      (* ----------------------------------------------- *)
-      sem_lval G m (Lvar x) ( G.(cc_link) x , 0 )
-  | Sshift_l : forall l t {d} (enc : layout d) p a (k:Z),
-      typeof_lval G l t ->
-      overlay m t enc ->
-      sem_lval G m l p ->
-      sem_exp G m a k ->
-      (* ----------------------------------------------- *)
-      sem_lval G m (Lshift l a) (shift p (sizeof enc * k))
-  | Sfield_s : forall l s p f k,
-      typeof_lval G l (Cstruct s) ->
-      field_offset m f k s ->
-      sem_lval G m l p ->
-      (* ----------------------------------------------- *)
-      sem_lval G m (Lfield l f) (shift p k)
-  | Sfield_u : forall l s p f,
-      typeof_lval G l (Cunion s) ->
-      sem_lval G m l p ->
-      (* ----------------------------------------------- *)
-      sem_lval G m (Lfield l f) p
-with sem_exp (G : Compiler) (m : mem) : exp -> forall {T : Type}, T -> Prop :=
-  | Sem_lval : forall l t p d (enc : layout d) (v : d),
-      typeof_lval G l t ->
-      overlay m t enc ->
-      sem_lval G m l p ->
-      read enc m p v ->
-      (* ----------------------------------------------- *)
-      sem_exp G m (Lval l) v
-  | Sem_addrof : forall l p,
-      sem_lval G m l p ->
-      (* ----------------------------------------------- *)
-      sem_exp G m (AddrOf l) p
-  | Sem_shift : forall a p r {d} (enc : layout d) b k,
-      typeof_exp G a (Cptr r) ->
-      overlay m (typeof_ref G r) enc ->
-      sem_exp G m a p ->
-      sem_exp G m b k ->
-      (* ----------------------------------------------- *)
-      sem_exp G m (Shift a b) (shift p (sizeof enc * k))
-  | Sem_op : forall op a b (ta tb tc : Type)
-             pa (va : ta) pb (vb : tb) pc (vc : tc),	
-      prim_domain pa va -> sem_exp G m a va ->
-      prim_domain pb vb -> sem_exp G m b vb ->
-      prim_domain pc vc -> sem_op op pa pb pc ->
-      (* ----------------------------------------------- *)
-      sem_exp G m (Op op a b) vc
-.
-Theorem sem_welltyped (G : Compiler) (m : mem) :
-  forall e t d (v : d),
-    typeof_exp G e t ->
-    sem_exp G m e v ->
-    domain t d.
-Admitted.
--- a/src/plugins/wp/semantics/Typing.v
+++ b/src/plugins/wp/semantics/Typing.v
-Require Import Datatype.
-Require Import Primitive.
-Require Import Cil.
-Record Gamma : Type := {
-  g_var : cvar -> ctype ;
-  g_type : ctypedef -> ctype
-}.
-Definition typeof_ref (G : Gamma) (r : cref) : ctype :=
-  match r with
-  | Rvoid  => Cint char
-  | Rint i => Cint i
-  | Rflt f => Cflt f
-  | Rdef d => G.(g_type) d
-  end.
-Definition ptype (p : ptype) : ctype := 
-  match p with 
-  | inl i => Cint i 
-  | inr f => Cflt f 
-  end.
-Inductive typeof_exp (G : Gamma) : exp -> ctype -> Prop := 
-  | Tlval : forall l t,
-      typeof_lval G l t ->  
-      (* -------------------------------------- *)
-      typeof_exp G (Lval l) t
-  | Taddrof : forall l r,
-      typeof_lval G l (typeof_ref G r) -> 
-      (* -------------------------------------- *)
-      typeof_exp G (AddrOf l) (Cptr r)
-  | Tshift : forall p k r i,
-      typeof_exp G p (Cptr r) ->
-      typeof_exp G k (Cint i) ->
-      (* -------------------------------------- *)
-      typeof_exp G (Shift p k) (Cptr r)
-  | Top : forall op a pa b pb pr,
-     typeof_op op pa pb pr ->
-     typeof_exp G a (ptype pa) ->
-     typeof_exp G b (ptype pb) ->
-     (* --------------------------------------- *)
-     typeof_exp G (Op op a b) (ptype pr)
-with typeof_lval (G : Gamma) : lval -> ctype -> Prop :=
-  | Tvar : forall x, 
-      (* -------------------------------------- *)
-      typeof_lval G (Lvar x) (G.(g_var) x)
-  | Tshift_l : forall l t n e i, 
-      typeof_lval G l (Carray t n) ->
-      typeof_exp  G e (Cint i) ->
-      (* -------------------------------------- *)
-      typeof_lval G (Lshift l e) t                     
-  | Tfield_s : forall l s f t,
-      typeof_lval G l (Cstruct s) ->
-      bind f t s ->
-      (* -------------------------------------- *)
-      typeof_lval G (Lfield l f) t
-  | Tfield_u : forall l s f t,
-      typeof_lval G l (Cunion s) ->
-      bind f t s ->
-      (* -------------------------------------- *)
-      typeof_lval G (Lfield l f) t
-  | Tderef : forall p r,
-      typeof_exp G p (Cptr r) ->
-      (* -------------------------------------- *)
-      typeof_lval G (Lderef p) (typeof_ref G r)
-.
--- a/src/plugins/wp/semantics/Values.v
+++ b/src/plugins/wp/semantics/Values.v
-Require Import Datatype.
-Require Import Cil.
-Require Import Pointer.
-Require Import Machine.
-Require Import Layout.
-(** * Type Interpretation *)
-Definition Ccomp := [ cfield => ctype ].
-Definition Dcomp := [ cfield => Type ].
-Inductive domain : ctype -> Type -> Prop :=
-  | Dptr : forall p, domain (Cptr p) Addr
-  | Dint : forall i, domain (Cint i) Z
-  | Dflt : forall f, domain (Cflt f) R
-  | Darr : forall t n d, domain t d -> domain (Carray t n) (d[n])
-  | Dstruct : forall s r, compound s r -> domain (Cstruct s) {[ r ]}
-  | Dunion  : forall s r, compound s r -> domain (Cunion s) {[ r ?]} 
-with compound : Ccomp -> Dcomp -> Prop :=
-  | Dempty : compound empty empty
-  | Dfield : forall f t d T D, 
-             domain t d -> 
-             compound T D ->
-	     compound (add f t T) (add f d D).
-(** * Type Layout *)
-Definition head_record (f : cfield) T R (r : record (add f T R)) : T * record R :=
-  match r with
-  | Rempty => False
-  | Rfield _ _ v _ r => (v,r)
-  end.
-Definition struct_field (f : cfield) {T R} : 
-  layout T -> layout (record R) -> layout (record (add f T R))
-  := fun a r => interpret (head_record f T R) (concat a r).
-Definition head_union (f : cfield) T U (u : union (add f T U)) : (option T) * union U :=
-  match u with
-  | Uempty => False
-  | Uskip _ _ _ u => (None,u)
-  | Ufield _ _ v _ u => (Some v,u)
-  end.
-Definition union_field (f : cfield) {T R} :
-  layout T -> layout (union R) -> layout (union (add f T R))
-  := fun a r => interpret (head_union f T R) (superpose (option_layout a) r).
-Inductive overlay arch : ctype -> forall {t}, layout t -> Prop :=
-  | Lptr : forall p, overlay arch (Cptr p) (ptr_layout arch)
-  | Lint : forall i, overlay arch (Cint i) (int_layout arch i)
-  | Lflt : forall f, overlay arch (Cflt f) (flt_layout arch f)
-  | Lstruct : forall s r (e : layout {[ r ]}), struct_overlay arch s e -> overlay arch (Cstruct s) e
-  | Lunion  : forall s r (e : layout {[ r ?]}), union_overlay arch s e -> overlay arch (Cunion s) e
-with struct_overlay arch : Ccomp -> forall {r:Dcomp}, layout {[ r ]} -> Prop :=
-  | Sempty : struct_overlay arch empty (empty_layout {[ empty ]})
-  | Sfield : forall (f : cfield) t {d} (e : layout d) 
-                                 T {D} (R : layout {[ D ]}),
-               overlay arch t e ->
-	       struct_overlay arch T R ->
-	       struct_overlay arch (add f t T) (struct_field f e R)
-with union_overlay arch : Ccomp -> forall {r:Dcomp}, layout {[ r ?]} -> Prop :=
-  | Uempty : union_overlay arch empty (empty_layout {[ empty ?]})
-  | Ufield : forall (f : cfield) t {d} (e : layout d) 
-                                   T {D} (R : layout {[ D ?]}),
-               overlay arch t e ->
-	       union_overlay arch T R ->
-	       union_overlay arch (add f t T) (union_field f e R).
-Inductive field_offset arch : cfield -> Z -> Ccomp -> Prop :=
-  | Ofs_field : forall f t T, field_offset arch f 0 (add f t T)
-  | Ofs_next  : forall f k g (t : ctype) {d} (enc : layout d) T, 
-       overlay arch t enc ->
-       field_offset arch f k T ->
-       field_offset arch f (sizeof enc + k) (add g t T).
-(** * Type and Domain Consistency *)
-Theorem overlay_domain : forall arch t d (e : layout d), overlay arch t e -> domain t d
-   with struct_overlay_domain : forall arch T D (R : layout {[ D ]}), struct_overlay arch T R -> compound T D
-   with union_overlay_domain : forall arch T D (R : layout {[ D ?]}), union_overlay arch T R -> compound T D.
-Proof.
-* intros.
-  induction H.
-  + apply Dptr.
-  + apply Dint.
-  + apply Dflt.
-  + apply Dstruct.
-    apply (struct_overlay_domain arch s r e). assumption.
-  + apply Dunion.
-    apply (union_overlay_domain arch s r e). assumption.
-* intros.
-  induction H. 
-  - apply Dempty. 
-  - apply Dfield. 
-      + by (apply (overlay_domain arch t d e)).
-      + by (apply (struct_overlay_domain arch T D R)).
-* intros. 
-  induction H.
-  - apply Dempty.
-  - apply Dfield.
-      + by (apply (overlay_domain arch t d e)).
-      + by (apply (union_overlay_domain arch T D R)).
-Qed.
--- a/src/plugins/wp/semantics/coqide.sh
+++ b/src/plugins/wp/semantics/coqide.sh
-coqide -I . $*