add hid in BTL_SEtheory: this avoids duplication of types (and should not be harmful)

1 files changed, 142 insertions, 127 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 5a94b235..2a335790 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -13,54 +13,77 @@ Require Import Coqlib Maps Floats.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL BTL OptionMonad.
+Require Export Impure.ImpHCons.
+Import HConsing.
 
+(** * Syntax and semantics of symbolic values *)
+
+(** The semantics of symbolic execution is parametrized by the context of the execution of a block *)
 Record iblock_exec_context := Bctx {
-  cge: BTL.genv;
-  (* cstk: list stackframe; *) (* having the stack here does seem not a good idea *)
-  cf: function;
-  csp: val;
-  crs0: regset;
-  cm0: mem
+  cge: BTL.genv; (** usual environment for identifiers *)
+  cf: function;  (** ambient function of the block *)
+  csp: val;      (** stack pointer *)
+  crs0: regset;  (** initial state of registers (at the block entry) *)
+  cm0: mem       (** initial memory state *)
 }.
 
-(** * Syntax and semantics of symbolic values *)
 
-(* TODO: introduire les hash-code directement ici - avec les "fake" smart constructors qui mettent un unknown_hid ? *)
-
-(* symbolic value *)
+(** symbolic value *)
 Inductive sval :=
-  | Sundef
-  | Sinput (r: reg)
-  | Sop (op:operation) (lsv: list_sval)
-  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
-with list_sval := 
-  | Snil
-  | Scons (sv: sval) (lsv: list_sval)
-(* symbolic memory *)
+  | Sundef (hid: hashcode)
+  | Sinput (r: reg) (hid: hashcode)
+  | Sop (op:operation) (lsv: list_sval) (hid: hashcode)
+  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (hid: hashcode)
+(** list of symbolic values *)
+with list_sval :=
+  | Snil (hid: hashcode)
+  | Scons (sv: sval) (lsv: list_sval) (hid: hashcode)
+(** symbolic memory *)
 with smem :=
-  | Sinit 
-  | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval).
+  | Sinit (hid: hashcode)
+  | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval) (hid: hashcode)
+.
 
 Scheme sval_mut := Induction for sval Sort Prop
 with list_sval_mut := Induction for list_sval Sort Prop
 with smem_mut := Induction for smem Sort Prop.
 
+(** "fake" smart-constructors using an [unknown_hid] instead of the one provided by hash-consing.
+These smart-constructors are those used in the abstract model of symbolic execution.
+They will also appear in the implementation of rewriting rules (in order to avoid hash-consing handling 
+in proofs of rewriting rules).
+*)
+
+Definition fSundef := Sundef unknown_hid.
+Definition fSinput (r: reg) := Sinput r unknown_hid.
+Definition fSop (op:operation) (lsv: list_sval) := Sop op lsv unknown_hid.
+Definition fSload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval)
+ := Sload sm trap chunk addr lsv unknown_hid.
+
+Definition fSnil := Snil unknown_hid.
+Definition fScons (sv: sval) (lsv: list_sval) := Scons sv lsv unknown_hid.
+
+Definition fSinit := Sinit unknown_hid.
+Definition fSstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval) 
+  := Sstore sm chunk addr lsv srce unknown_hid.
+
 Fixpoint list_sval_inj (l: list sval): list_sval :=
   match l with
-  | nil => Snil
-  | v::l => Scons v (list_sval_inj l)
+  | nil => fSnil
+  | v::l => fScons v (list_sval_inj l)
   end.
 
 Local Open Scope option_monad_scope.
 
+(** Semantics *)
 Fixpoint eval_sval ctx (sv: sval): option val :=
   match sv with
-  | Sundef => Some Vundef
-  | Sinput r => Some ((crs0 ctx)#r)
-  | Sop op l =>
+  | Sundef _ => Some Vundef
+  | Sinput r _ => Some ((crs0 ctx)#r)
+  | Sop op l _ =>
      SOME args <- eval_list_sval ctx l IN
      eval_operation (cge ctx) (csp ctx) op args (cm0 ctx)
-  | Sload sm trap chunk addr lsv =>
+  | Sload sm trap chunk addr lsv _ =>
       match trap with
       | TRAP =>
           SOME args <- eval_list_sval ctx lsv IN
@@ -82,16 +105,16 @@ Fixpoint eval_sval ctx (sv: sval): option val :=
   end
 with eval_list_sval ctx (lsv: list_sval): option (list val) :=
   match lsv with
-  | Snil => Some nil
-  | Scons sv lsv' => 
+  | Snil _ => Some nil
+  | Scons sv lsv' _ => 
     SOME v <- eval_sval ctx sv IN
     SOME lv <- eval_list_sval ctx lsv' IN
     Some (v::lv)
   end
 with eval_smem ctx (sm: smem): option mem :=
   match sm with
-  | Sinit => Some (cm0 ctx)
-  | Sstore sm chunk addr lsv srce =>
+  | Sinit _ => Some (cm0 ctx)
+  | Sstore sm chunk addr lsv srce _ =>
      SOME args <- eval_list_sval ctx lsv IN
      SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
      SOME m <- eval_smem ctx sm IN
@@ -99,7 +122,12 @@ with eval_smem ctx (sm: smem): option mem :=
      Mem.storev chunk m a sv
   end.
 
+(** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. 
+    Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block
+   (their semantics only depends on the initial memory of the block).
 
+   The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq].
+*)
 Lemma valid_pointer_preserv ctx sm:
   forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs.
 Proof.
@@ -116,7 +144,7 @@ Proof.
   intros H; induction l as [|r l]; simpl; repeat autodestruct; auto.
 Qed.
 
-Definition seval_condition ctx (cond: condition) (lsv: list_sval): option bool :=
+Definition eval_scondition ctx (cond: condition) (lsv: list_sval): option bool :=
   SOME args <- eval_list_sval ctx lsv IN
   eval_condition cond args (cm0 ctx).
 
@@ -124,60 +152,60 @@ Definition seval_condition ctx (cond: condition) (lsv: list_sval): option bool :
 (** * Auxiliary definitions on Builtins *)
 (* TODO: clean this. Some generic stuffs could be put in [AST.v] *)
 
-Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)
+Section EVAL_BUILTIN_SARG. (* adapted from Events.v *)
 
 Variable ctx: iblock_exec_context.
 Variable m: mem.
 
-Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop :=
+Inductive eval_builtin_sarg: builtin_arg sval -> val -> Prop :=
   | seval_BA: forall x v,
       eval_sval ctx x = Some v ->
-      seval_builtin_arg (BA x) v
+      eval_builtin_sarg (BA x) v
   | seval_BA_int: forall n,
-      seval_builtin_arg (BA_int n) (Vint n)
+      eval_builtin_sarg (BA_int n) (Vint n)
   | seval_BA_long: forall n,
-      seval_builtin_arg (BA_long n) (Vlong n)
+      eval_builtin_sarg (BA_long n) (Vlong n)
   | seval_BA_float: forall n,
-      seval_builtin_arg (BA_float n) (Vfloat n)
+      eval_builtin_sarg (BA_float n) (Vfloat n)
   | seval_BA_single: forall n,
-      seval_builtin_arg (BA_single n) (Vsingle n)
+      eval_builtin_sarg (BA_single n) (Vsingle n)
   | seval_BA_loadstack: forall chunk ofs v,
       Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v ->
-      seval_builtin_arg (BA_loadstack chunk ofs) v
+      eval_builtin_sarg (BA_loadstack chunk ofs) v
   | seval_BA_addrstack: forall ofs,
-      seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs)
+      eval_builtin_sarg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs)
   | seval_BA_loadglobal: forall chunk id ofs v,
       Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v ->
-      seval_builtin_arg (BA_loadglobal chunk id ofs) v
+      eval_builtin_sarg (BA_loadglobal chunk id ofs) v
   | seval_BA_addrglobal: forall id ofs,
-      seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs)
+      eval_builtin_sarg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs)
   | seval_BA_splitlong: forall hi lo vhi vlo,
-      seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo ->
-      seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
+      eval_builtin_sarg hi vhi -> eval_builtin_sarg lo vlo ->
+      eval_builtin_sarg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
   | seval_BA_addptr: forall a1 a2 v1 v2,
-      seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 ->
-      seval_builtin_arg (BA_addptr a1 a2)
+      eval_builtin_sarg a1 v1 -> eval_builtin_sarg a2 v2 ->
+      eval_builtin_sarg (BA_addptr a1 a2)
                        (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2)
 .
 
-Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop :=
-  list_forall2 seval_builtin_arg al vl.
+Definition eval_builtin_sargs (al: list (builtin_arg sval)) (vl: list val) : Prop :=
+  list_forall2 eval_builtin_sarg al vl.
 
-Lemma seval_builtin_arg_determ:
-  forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v.
+Lemma eval_builtin_sarg_determ:
+  forall a v, eval_builtin_sarg a v -> forall v', eval_builtin_sarg a v' -> v' = v.
 Proof.
   induction 1; intros v' EV; inv EV; try congruence.
   f_equal; eauto.
-  apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. 
+  apply IHeval_builtin_sarg1 in H3. apply IHeval_builtin_sarg2 in H5. subst; auto. 
 Qed.
 
-Lemma eval_builtin_args_determ:
-  forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl.
+Lemma eval_builtin_sargs_determ:
+  forall al vl, eval_builtin_sargs al vl -> forall vl', eval_builtin_sargs al vl' -> vl' = vl.
 Proof.
-  induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ.
+  induction 1; intros v' EV; inv EV; f_equal; eauto using eval_builtin_sarg_determ.
 Qed.
 
-End SEVAL_BUILTIN_ARG.
+End EVAL_BUILTIN_SARG.
 
 (* NB: generic function that could be put into [AST] file *)
 Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
@@ -195,10 +223,10 @@ Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B
   | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2)
   end.
 
-Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg,
+Lemma eval_builtin_sarg_correct ctx rs m sreg: forall arg varg,
   (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
   eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg ->
-  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg.
+  eval_builtin_sarg ctx m (builtin_arg_map sreg arg) varg.
 Proof.
   induction arg.
   all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
@@ -208,20 +236,20 @@ Proof.
     eapply IHarg1; eauto. eapply IHarg2; eauto.
 Qed.
 
-Lemma seval_builtin_args_correct ctx rs m sreg args vargs:
+Lemma eval_builtin_sargs_correct ctx rs m sreg args vargs:
   (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
   eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs ->
-  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs.
+  eval_builtin_sargs ctx m (map (builtin_arg_map sreg) args) vargs.
 Proof.
   induction 2.
   - constructor.
   - simpl. constructor; [| assumption].
-    eapply seval_builtin_arg_correct; eauto.
+    eapply eval_builtin_sarg_correct; eauto.
 Qed.
 
-Lemma seval_builtin_arg_exact ctx rs m sreg: forall arg varg,
+Lemma eval_builtin_sarg_exact ctx rs m sreg: forall arg varg,
   (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
-  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg ->
+  eval_builtin_sarg ctx m (builtin_arg_map sreg arg) varg ->
   eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.
 Proof.
   induction arg.
@@ -233,16 +261,16 @@ Proof.
     eapply IHarg1; eauto. eapply IHarg2; eauto.
 Qed.
 
-Lemma seval_builtin_args_exact ctx rs m sreg: forall args vargs,
+Lemma eval_builtin_sargs_exact ctx rs m sreg: forall args vargs,
   (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
-  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs ->
+  eval_builtin_sargs ctx m (map (builtin_arg_map sreg) args) vargs ->
   eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
 Proof.
   induction args.
   - simpl. intros. inv H0. constructor.
   - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
     constructor; [| eapply IHargs; eauto].
-    eapply seval_builtin_arg_exact; eauto.
+    eapply eval_builtin_sarg_exact; eauto.
 Qed.
 
 Fixpoint eval_builtin_sval ctx bsv :=
@@ -285,7 +313,7 @@ Lemma eval_builtin_sval_arg ctx bs:
    forall ba m v, 
    eval_builtin_sval ctx bs = Some ba ->
    eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
-   seval_builtin_arg ctx m bs v.
+   eval_builtin_sarg ctx m bs v.
 Proof.
    induction bs; simpl; 
    try (intros ba m v H; inversion H; subst; clear H;
@@ -309,8 +337,8 @@ Proof.
      econstructor; eauto.
 Qed.
 
-Lemma seval_builtin_arg_sval ctx m v: forall bs,
-  seval_builtin_arg ctx m bs v ->
+Lemma eval_builtin_sarg_sval ctx m v: forall bs,
+  eval_builtin_sarg ctx m bs v ->
   exists ba,
     eval_builtin_sval ctx bs = Some ba
     /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.
@@ -321,13 +349,13 @@ Proof.
   - eexists. constructor.
     + simpl. rewrite H. reflexivity.
     + constructor.
-  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
-    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+  - destruct IHeval_builtin_sarg1 as (ba1 & A1 & B1).
+    destruct IHeval_builtin_sarg2 as (ba2 & A2 & B2).
     eexists. constructor.
     + simpl. rewrite A1. rewrite A2. reflexivity.
     + constructor; assumption. 
-  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
-    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+  - destruct IHeval_builtin_sarg1 as (ba1 & A1 & B1).
+    destruct IHeval_builtin_sarg2 as (ba2 & A2 & B2).
     eexists. constructor.
     + simpl. rewrite A1. rewrite A2. reflexivity.
     + constructor; assumption.
@@ -337,9 +365,9 @@ Lemma eval_builtin_sval_args ctx lbs:
    forall lba m v, 
    eval_list_builtin_sval ctx lbs = Some lba ->
    list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v ->
-   seval_builtin_args ctx m lbs v.
+   eval_builtin_sargs ctx m lbs v.
 Proof.
-  unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
+  unfold eval_builtin_sargs; induction lbs; simpl; intros lba m v.
   - intros H; inversion H; subst; clear H.
     intros H; inversion H. econstructor.
   - destruct (eval_builtin_sval _ _) eqn:SV; try congruence.
@@ -350,8 +378,8 @@ Proof.
     eapply eval_builtin_sval_arg; eauto.
 Qed.
 
-Lemma seval_builtin_args_sval ctx m lv: forall lbs,
-  seval_builtin_args ctx m lbs lv ->
+Lemma eval_builtin_sargs_sval ctx m lv: forall lbs,
+  eval_builtin_sargs ctx m lbs lv ->
   exists lba,
     eval_list_builtin_sval ctx lbs = Some lba
     /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv.
@@ -361,29 +389,29 @@ Proof.
     + simpl. reflexivity.
     + constructor.
   - destruct IHlist_forall2 as (lba & A & B).
-    apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
+    apply eval_builtin_sarg_sval in H. destruct H as (ba & A' & B').
     eexists. constructor.
     + simpl. rewrite A'. rewrite A. reflexivity.
     + constructor; assumption.
 Qed.
 
 Lemma eval_builtin_sval_correct ctx m: forall bs1 v bs2,
-  seval_builtin_arg ctx m bs1 v ->
+  eval_builtin_sarg ctx m bs1 v ->
   (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) ->
-  seval_builtin_arg ctx m bs2 v.
+  eval_builtin_sarg ctx m bs2 v.
 Proof.
-  intros. exploit seval_builtin_arg_sval; eauto.
+  intros. exploit eval_builtin_sarg_sval; eauto.
   intros (ba & X1 & X2).
   eapply eval_builtin_sval_arg; eauto.
   congruence.
 Qed.
 
 Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
-  seval_builtin_args ctx m lbs1 vargs ->
+  eval_builtin_sargs ctx m lbs1 vargs ->
   forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) ->
-  seval_builtin_args ctx m lbs2 vargs.
+  eval_builtin_sargs ctx m lbs2 vargs.
 Proof.
-  intros. exploit seval_builtin_args_sval; eauto.
+  intros. exploit eval_builtin_sargs_sval; eauto.
   intros (ba & X1 & X2).
   eapply eval_builtin_sval_args; eauto.
   congruence.
@@ -391,6 +419,9 @@ Qed.
 
 (** * Symbolic (final) value of a block *)
 
+(** TODO: faut-il hash-conser les valeurs symboliques finales. Pas très utile si pas de join interne. 
+Mais peut être utile dans le cas contraire. *)
+
 Inductive sfval :=
   | Sgoto (pc: exit)
   | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
@@ -434,7 +465,7 @@ Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop :=
       sem_sfval ctx stk (Stailcall sig svos lsv) rs m
         E0 (Callstate stk fd args m')
   | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
-      seval_builtin_args ctx m sargs vargs ->
+      eval_builtin_sargs ctx m sargs vargs ->
       external_call ef (cge ctx) vargs m t vres m' ->
       sem_sfval ctx stk (Sbuiltin ef sargs res pc) rs m
         t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m')
@@ -496,12 +527,12 @@ Proof.
       rewrite REG; eauto.
     - erewrite eval_list_sval_inj; simpl; auto.
   + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
-    eapply seval_builtin_args_correct; eauto.
+    eapply eval_builtin_sargs_correct; eauto.
   + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
 Qed.
 
 Local Hint Constructors final_step: core.
-Local Hint Resolve seval_builtin_args_exact: core.
+Local Hint Resolve eval_builtin_sargs_exact: core.
 
 Lemma sexec_final_sfv_exact ctx stk i sis t rs m s:
   sem_sistate ctx sis rs m ->
@@ -530,7 +561,7 @@ Qed.
 
 (** * symbolic execution of basic instructions *)
 
-Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.
+Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => fSinput r; si_smem:= fSinit |}.
 
 Lemma sis_init_correct ctx:
   sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx).
@@ -575,7 +606,7 @@ Qed.
 
 Definition sexec_op op args dst sis: sistate :=
    let args := list_sval_inj (List.map sis.(si_sreg) args) in
-   set_sreg dst (Sop op args) sis.
+   set_sreg dst (fSop op args) sis.
 
 Lemma sexec_op_correct ctx op args dst sis rs m v
  (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v)
@@ -593,7 +624,7 @@ Qed.
 
 Definition sexec_load trap chunk addr args dst sis: sistate :=
    let args := list_sval_inj (List.map sis.(si_sreg) args) in
-   set_sreg dst (Sload sis.(si_smem) trap chunk addr args) sis.
+   set_sreg dst (fSload sis.(si_smem) trap chunk addr args) sis.
 
 Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v
  (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a)
@@ -612,7 +643,7 @@ Qed.
 Definition sexec_store chunk addr args src sis: sistate :=
    let args := list_sval_inj (List.map sis.(si_sreg) args) in
    let src := sis.(si_sreg) src in
-   let sm := Sstore sis.(si_smem) chunk addr args src in
+   let sm := fSstore sis.(si_smem) chunk addr args src in
    set_smem sm sis.
 
 Lemma sexec_store_correct ctx chunk addr args src sis rs m m' a
@@ -628,11 +659,11 @@ Proof.
   rewrite REG; auto.
 Qed.
 
-Lemma seval_condition_eq ctx cond args sis rs m
+Lemma eval_scondition_eq ctx cond args sis rs m
   (SIS : sem_sistate ctx sis rs m)
-  :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) = eval_condition cond rs ## args m.
+  :eval_scondition ctx cond (list_sval_inj (map (si_sreg sis) args)) = eval_condition cond rs ## args m.
 Proof.
-  destruct SIS as (PRE&MEM&REG); unfold seval_condition; simpl.
+  destruct SIS as (PRE&MEM&REG); unfold eval_scondition; simpl.
   erewrite eval_list_sval_inj; simpl; auto.
   eapply cond_valid_pointer_eq; eauto.
 Qed.
@@ -640,7 +671,7 @@ Qed.
 (** * Compute sistate associated to final values *)
 Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
   match inputs with
-  | nil => fun r => Sundef 
+  | nil => fun r => fSundef 
   | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r
   end.
 
@@ -723,7 +754,7 @@ Fixpoint get_soutcome ctx (st:sstate): option soutcome :=
   match st with
   | Sfinal sis sfv => Some (sout sis sfv)
   | Scond cond args ifso ifnot =>
-     SOME b <- seval_condition ctx cond args IN
+     SOME b <- eval_scondition ctx cond args IN
      get_soutcome ctx (if b then ifso else ifnot)
   | Sabort => None
   end.
@@ -735,7 +766,7 @@ Inductive sem_sstate ctx stk t s: sstate -> Prop :=
      (SFV: sem_sfval ctx stk sfv rs m t s)
      : sem_sstate ctx stk t s (Sfinal sis sfv)
   | sem_Scond b cond args ifso ifnot
-     (SEVAL: seval_condition ctx cond args = Some b)
+     (SEVAL: eval_scondition ctx cond args = Some b)
      (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot))
      : sem_sstate ctx stk t s (Scond cond args ifso ifnot)
   (* NB: Sabort: fails to produce a transition *) 
@@ -768,14 +799,10 @@ Proof.
 Qed.
 
 
-(** * Idée de l'execution symbolique en Continuation Passing Style 
-
-[k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche)
+(** * Model of Symbolic Execution with Continuation Passing Style 
 
-Rem: si manipuler une telle continuation s'avère compliqué dans les preuves,
-il faudra faire autrement dans le modèle -- par exemple avec une structure de donnée 
-pour représenter l'ensemble des chemins.
-(même si on peut conserver le CPS dans l'implem finale, pour l'efficacité).
+Parameter [k] is the continuation, i.e. the [sstate] construction that will be applied in each execution branch.
+Its input parameter is the symbolic internal state of the branch.
 
 *)
 
@@ -821,7 +848,7 @@ Proof.
   (* condition *)
   all: intros;
     eapply sem_Scond; eauto; [
-      erewrite seval_condition_eq; eauto |
+      erewrite eval_scondition_eq; eauto |
       replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (if b then ifso else ifnot) sis k); 
       try autodestruct; eauto ].
 Qed.
@@ -1044,7 +1071,7 @@ Proof.
     exploit IHib2; eauto.
   - (* Bcond *)
     inv SEXEC.
-    erewrite seval_condition_eq in SEVAL; eauto.
+    erewrite eval_scondition_eq in SEVAL; eauto.
     rewrite SEVAL.
     destruct b.
     + exploit IHib1; eauto.
@@ -1139,7 +1166,6 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr
 Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop :=
   forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m.
 
-
 Record si_ok ctx (sis: sistate): Prop := {
   OK_PRE: (sis.(si_pre) ctx);
   OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
@@ -1154,7 +1180,6 @@ Proof.
   intuition congruence.
 Qed.
 
-
 Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop :=
   forall sis1 sfv1, get_soutcome (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 ->
   exists sis2 sfv2, get_soutcome (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
@@ -1255,23 +1280,13 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma seval_condition_preserved cond lsv:
-  seval_condition (bctx1 ctx) cond lsv = seval_condition (bctx2 ctx) cond lsv.
+Lemma eval_scondition_preserved cond lsv:
+  eval_scondition (bctx1 ctx) cond lsv = eval_scondition (bctx2 ctx) cond lsv.
 Proof.
-  unfold seval_condition.
+  unfold eval_scondition.
   rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
 Qed.
 
-(* TODO: useless ?
-Lemma get_soutcome_preserved sis:
-  get_soutcome (bctx1 ctx) sis = get_soutcome (bctx2 ctx) sis.
-Proof.
-  induction sis; simpl; eauto.
-  erewrite seval_condition_preserved.
-  repeat (autodestruct; auto).
-Qed.
-*)
-
 (* additional preservation properties under this additional hypothesis *)
 Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx).
 
@@ -1288,9 +1303,9 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma seval_builtin_arg_preserved m: forall bs varg,
-  seval_builtin_arg (bctx1 ctx) m bs varg ->
-  seval_builtin_arg (bctx2 ctx) m bs varg.
+Lemma eval_builtin_sarg_preserved m: forall bs varg,
+  eval_builtin_sarg (bctx1 ctx) m bs varg ->
+  eval_builtin_sarg (bctx2 ctx) m bs varg.
 Proof.
   induction 1; simpl.
   all: try (constructor; auto).
@@ -1299,12 +1314,12 @@ Proof.
   - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
 Qed.
 
-Lemma seval_builtin_args_preserved m lbs vargs:
-  seval_builtin_args (bctx1 ctx) m lbs vargs ->
-  seval_builtin_args (bctx2 ctx) m lbs vargs.
+Lemma eval_builtin_sargs_preserved m lbs vargs:
+  eval_builtin_sargs (bctx1 ctx) m lbs vargs ->
+  eval_builtin_sargs (bctx2 ctx) m lbs vargs.
 Proof.
   induction 1; constructor; eauto.
-  eapply seval_builtin_arg_preserved; auto.
+  eapply eval_builtin_sarg_preserved; auto.
 Qed.
 
 End SymbValPreserved.