Some renaming

1 files changed, 230 insertions, 129 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index bd6fafa4..3963326a 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -20,8 +20,8 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
-Ltac wlp_intros varname hname := apply wlp_unfold; intros varname hname.
-Ltac wlp_step_bind varname hname := apply wlp_bind; wlp_intros varname hname.
+Ltac wlp_intro varname hname := apply wlp_unfold; intros varname hname.
+Ltac wlp_bind varname hname := apply wlp_bind; wlp_intro varname hname.
 
 Ltac wlp_absurd := match goal with
   | [ H : FAILWITH ?msg |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
@@ -33,19 +33,18 @@ end.
 (** ** Implementation of symbolic values/symbolic memories with hash-consing data *)
 
 Inductive hsval :=
-  | HSinput (r: reg) (hid:hashcode)
-  | HSop (op:operation) (hlsv: hlist_sval)  (hsm: hsmem) (hid:hashcode)
-  | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (hid:hashcode)
-with hlist_sval := 
-  | HSnil (hid:hashcode)
-  | HScons (hsv: hsval) (hlsv: hlist_sval) (hid:hashcode)
-(* symbolic memory *)
+  | HSinput (r: reg) (hid: hashcode)
+  | HSop (op: operation) (lhsv: list_hsval)  (hsm: hsmem) (hid: hashcode)
+  | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode)
+with list_hsval :=
+  | HSnil (hid: hashcode)
+  | HScons (hsv: hsval) (lhsv: list_hsval) (hid: hashcode)
 with hsmem :=
-  | HSinit (hid:hashcode)
-  | HSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval) (hid:hashcode).
+  | HSinit (hid: hashcode)
+  | HSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval) (hid:hashcode).
 
 Scheme hsval_mut := Induction for hsval Sort Prop
-with hlist_sval_mut := Induction for hlist_sval Sort Prop
+with list_hsval_mut := Induction for list_hsval Sort Prop
 with hsmem_mut := Induction for hsmem Sort Prop.
 
 Definition hsval_get_hid (hsv: hsval): hashcode :=
@@ -55,13 +54,13 @@ Definition hsval_get_hid (hsv: hsval): hashcode :=
   | HSload _ _ _ _ _ hid => hid
   end.
 
-Definition hlist_sval_get_hid (hlsv: hlist_sval): hashcode :=
-  match hlsv with
+Definition list_hsval_get_hid (lhsv: list_hsval): hashcode :=
+  match lhsv with
   | HSnil hid => hid
   | HScons _ _ hid => hid
   end.
 
-Definition hsmem_get_hid (hsm: hsmem ): hashcode :=
+Definition hsmem_get_hid (hsm: hsmem): hashcode :=
   match hsm with
   | HSinit hid => hid
   | HSstore _ _ _ _ _ hid => hid
@@ -70,30 +69,29 @@ Definition hsmem_get_hid (hsm: hsmem ): hashcode :=
 Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval :=
   match hsv with
   | HSinput r _ => HSinput r hid
-  | HSop o hlsv hsm _ => HSop o hlsv hsm hid
-  | HSload hsm trap chunk addr hlsv _ => HSload hsm trap chunk addr hlsv hid
+  | HSop o lhsv hsm _ => HSop o lhsv hsm hid
+  | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid
   end.
 
-Definition hlist_sval_set_hid (hlsv: hlist_sval) (hid: hashcode): hlist_sval :=
-  match hlsv with
+Definition list_hsval_set_hid (lhsv: list_hsval) (hid: hashcode): list_hsval :=
+  match lhsv with
   | HSnil _ => HSnil hid
-  | HScons hsv hlsv _ => HScons hsv hlsv hid
+  | HScons hsv lhsv _ => HScons hsv lhsv hid
   end.
 
-Definition hsmem_set_hid (hsm: hsmem ) (hid: hashcode): hsmem :=
+Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem :=
   match hsm with
   | HSinit _ => HSinit hid
-  | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid
+  | HSstore hsm chunk addr lhsv srce _ => HSstore hsm chunk addr lhsv srce hid
   end.
 
-(* Now, we build the hash-Cons value from a "hash_eq".
+(** Now, we build the hash-Cons value from a "hash_eq".
 
-Informal specification: 
-  [hash_eq] must be consistent with the "hashed" constructors defined above.
+  Informal specification: 
+    [hash_eq] must be consistent with the "hashed" constructors defined above.
 
-We expect that hashinfo values in the code of these "hashed" constructors verify:
-
-  (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
+  We expect that hashinfo values in the code of these "hashed" constructors verify:
+    (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
 *)
 
 Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
@@ -116,7 +114,7 @@ Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
   | _,_ => RET false
   end.
 
-Definition hlist_sval_hash_eq (lsv1 lsv2: hlist_sval): ?? bool :=
+Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool :=
   match lsv1, lsv2 with
   | HSnil _, HSnil _ => RET true
   | HScons sv1 lsv1' _, HScons sv2 lsv2' _  =>
@@ -142,7 +140,7 @@ Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
   end.
 
 Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. 
-Definition hLSVAL: hashP hlist_sval := {| hash_eq := hlist_sval_hash_eq; get_hid:= hlist_sval_get_hid; set_hid:= hlist_sval_set_hid |}.
+Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}.
 Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}.
 
 Program Definition mk_hash_params: Dict.hash_params hsval :=
@@ -155,16 +153,16 @@ Obligation 1.
 Qed.
 
 
-(* Symbolic final value -- from hash-consed values
-It does not seem useful to hash-consed these final values (because they are final).
+(** Symbolic final value -- from hash-consed values
+  It does not seem useful to hash-consed these final values (because they are final).
 *)
 Inductive hsfval :=
   | HSnone
-  | HScall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) (res:reg) (pc:node)
-  | HStailcall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval)
-  | HSbuiltin (ef:external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc:node)
+  | HScall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) (res: reg) (pc: node)
+  | HStailcall (sig: signature) (svos: hsval + ident) (lsv: list_hsval)
+  | HSbuiltin (ef: external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc: node)
   | HSjumptable (sv: hsval) (tbl: list node)
-  | HSreturn (res:option hsval)
+  | HSreturn (res: option hsval)
 .
 
 (** ** Implementation of symbolic states 
@@ -185,7 +183,7 @@ Record hsistate_local :=
 
 (* Syntax and semantics of symbolic exit states *)
 Record hsistate_exit := mk_hsistate_exit
-  { hsi_cond: condition; hsi_scondargs: hlist_sval; hsi_elocal: hsistate_local; hsi_ifso: node }.
+  { hsi_cond: condition; hsi_scondargs: list_hsval; hsi_elocal: hsistate_local; hsi_ifso: node }.
 
 
 (** ** Syntax and Semantics of symbolic internal state *)
@@ -222,12 +220,12 @@ Hypothesis hC_hsval_correct: forall hs rhsv,
   (hsval_proj (hdata hs)) = (hsval_proj rhsv).
 Local Hint Resolve hC_hsval_correct: wlp.
 
-Variable hC_hlist_sval: hashinfo hlist_sval -> ?? hlist_sval.
+Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval.
 
-Hypothesis hC_hlist_sval_correct: forall hs rhsv,
-  hC_hlist_sval hs ~~> rhsv ->
+Hypothesis hC_list_hsval_correct: forall hs rhsv,
+  hC_list_hsval hs ~~> rhsv ->
   (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv).
-Local Hint Resolve hC_hlist_sval_correct: wlp.
+Local Hint Resolve hC_list_hsval_correct: wlp.
 
 Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
 
@@ -252,48 +250,46 @@ Definition hSinput (r:reg): ?? hsval :=
    DO hv <~ hSinput_hcodes r;;
    hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}.
 
-
-Definition hSop_hcodes (op:operation) (hlsv: hlist_sval)  (hsm: hsmem) :=
+Definition hSop_hcodes (op:operation) (lhsv: list_hsval)  (hsm: hsmem) :=
    DO hc <~ hash op_hcode;;
    DO hv <~ hash op;;
-   RET [hc;hv;hlist_sval_get_hid hlsv; hsmem_get_hid hsm].
+   RET [hc;hv;list_hsval_get_hid lhsv; hsmem_get_hid hsm].
 Extraction Inline hSop_hcodes.
 
-Definition hSop (op:operation) (hlsv: hlist_sval)  (hsm: hsmem): ?? hsval :=
-   DO hv <~ hSop_hcodes op hlsv hsm;;
-   hC_hsval {| hdata:=HSop op hlsv hsm unknown_hid; hcodes :=hv |}.
-
+Definition hSop (op:operation) (lhsv: list_hsval)  (hsm: hsmem): ?? hsval :=
+   DO hv <~ hSop_hcodes op lhsv hsm;;
+   hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}.
 
-Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval):=
+Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):=
    DO hc <~ hash load_hcode;;
    DO hv1 <~ hash trap;;
    DO hv2 <~ hash chunk;;
    DO hv3 <~ hash addr;;
-   RET [hc;hsmem_get_hid hsm;hv1;hv2;hv3;hlist_sval_get_hid hlsv].
+   RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv].
 Extraction Inline hSload_hcodes.
 
-Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval): ?? hsval :=
-   DO hv <~ hSload_hcodes hsm trap chunk addr hlsv;;
-   hC_hsval {| hdata:=HSload hsm trap chunk addr hlsv unknown_hid; hcodes :=hv |}.
+Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval :=
+   DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;;
+   hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}.
 
-Definition hSnil (_: unit): ?? hlist_sval :=
-   hC_hlist_sval {| hdata:=HSnil unknown_hid; hcodes := nil |}.
+Definition hSnil (_: unit): ?? list_hsval :=
+   hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}.
 
-Definition hScons (hsv: hsval) (hlsv: hlist_sval): ?? hlist_sval :=
-   hC_hlist_sval {| hdata:=HScons hsv hlsv unknown_hid; hcodes := [hsval_get_hid hsv; hlist_sval_get_hid hlsv] |}.
+Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval :=
+   hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}.
 
 Definition hSinit (_: unit): ?? hsmem :=
-   hC_hsmem {| hdata:=HSinit unknown_hid; hcodes := nil |}.
+   hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}.
 
-Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval):=
+Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):=
    DO hv1 <~ hash chunk;;
    DO hv2 <~ hash addr;;
-   RET [hsmem_get_hid hsm;hv1;hv2;hlist_sval_get_hid hlsv;hsval_get_hid srce].
+   RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce].
 Extraction Inline hSstore_hcodes.
 
-Definition hSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval): ?? hsmem :=
-   DO hv <~ hSstore_hcodes hsm chunk addr hlsv srce;;
-   hC_hsmem {| hdata:=HSstore hsm chunk addr hlsv srce unknown_hid; hcodes := hv |}.
+Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem :=
+   DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;;
+   hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}.
 
 
 Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
@@ -302,17 +298,17 @@ Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
    | Some sv => RET sv
    end.
 
-Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? hlist_sval :=
+Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval :=
   match l with
   | nil => hSnil()
   | r::l =>
     DO v <~ hsi_sreg_get hst r;;
-    DO hlsv <~ hlist_args hst l;;
-    hScons v hlsv
+    DO lhsv <~ hlist_args hst l;;
+    hScons v lhsv
   end.
 
 (** ** Assignment of memory *)
-Definition hslocal_store (hst:hsistate_local) chunk addr args src: ?? hsistate_local :=
+Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local :=
    let pt := hst.(hsi_sreg) in
    DO hargs <~ hlist_args pt args;;
    DO hsrc <~ hsi_sreg_get pt src;;
@@ -329,56 +325,56 @@ Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hs
 
 (** ** Assignment of registers *)
 
-(* locally new symbolic values during symbolic execution *)
+(** locally new symbolic values during symbolic execution *)
 Inductive root_sval: Type :=
-| Rop (op:operation)
-| Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing)
+| Rop (op: operation)
+| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
 .
 
-Definition root_apply (rsv: root_sval) (lsv: list reg) (hst: hsistate_local) : ?? hsval :=
-  DO hlsv <~ hlist_args hst lsv;;
+Definition root_apply (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval :=
+  DO lhsv <~ hlist_args hst lr;;
   match rsv with
-  | Rop op => hSop op hlsv hst
-  | Rload trap chunk addr => hSload hst trap chunk addr hlsv
+  | Rop op => hSop op lhsv hst
+  | Rload trap chunk addr => hSload hst trap chunk addr lhsv
   end.
 
 Local Open Scope lazy_bool_scope.
 
 (* NB: return [false] if the rsv cannot fail *)
-Definition may_trap (rsv: root_sval) (lsv: list reg): bool :=
+Definition may_trap (rsv: root_sval) (lr: list reg): bool :=
   match rsv with 
-  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lsv) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
+  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
   | Rload TRAP _ _  => true
   | _ => false
   end.
 
-(* simplify a symbolic value before assignment to a register *)
-Definition simplify (rsv: root_sval) (lsv: list reg) (hst: hsistate_local): ?? hsval :=
+(** simplify a symbolic value before assignment to a register *)
+Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
   match rsv with
   | Rop op =>
-     match is_move_operation op lsv with
-     | Some arg => hsi_sreg_get hst arg (* optimization of Omove *)
+     match is_move_operation op lr with
+     | Some arg => hsi_sreg_get hst arg (** optimization of Omove *)
      | None =>
        DO hsi <~ hSinit ();;
-       DO hlsv <~ hlist_args hst lsv;;
-       hSop op hlsv hsi (* magically remove the dependency on sm ! *)
+       DO lhsv <~ hlist_args hst lr;;
+       hSop op lhsv hsi (** magically remove the dependency on sm ! *)
      end
   | Rload _ chunk addr => 
-       DO hlsv <~ hlist_args hst lsv;;
-       hSload hst NOTRAP chunk addr hlsv
+       DO lhsv <~ hlist_args hst lr;;
+       hSload hst NOTRAP chunk addr lhsv
   end.
 
-Definition red_PTree_set (r:reg) (sv: hsval) (hst: PTree.t hsval): PTree.t hsval :=
-  match sv with
+Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsval :=
+  match hsv with
   | HSinput r' _ =>
      if Pos.eq_dec r r' 
      then PTree.remove r' hst
-     else PTree.set r sv hst
-  | _ => PTree.set r sv hst
+     else PTree.set r hsv hst
+  | _ => PTree.set r hsv hst
   end.
 
-Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv: ?? hsistate_local :=
-  DO hsiok <~ 
+Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) lsv: ?? hsistate_local :=
+  DO hsiok <~
    (if may_trap rsv lsv
     then DO hv <~ root_apply rsv lsv hst;; RET (hv::(hsi_ok_lsval hst))
     else RET (hsi_ok_lsval hst));;
@@ -465,7 +461,6 @@ Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident)
   end.
 
 
-
 (** * The simulation test of concrete hash-consed symbolic execution *)
 
 Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
@@ -482,7 +477,7 @@ Qed.
 Global Opaque phys_check.
 Hint Resolve phys_check_correct: wlp.
 
-Definition struct_check {A} (x y:A) (msg: pstring): ?? unit :=
+Definition struct_check {A} (x y: A) (msg: pstring): ?? unit :=
   DO b <~ struct_eq x y;;
   assert_b b msg;;
   RET tt.
@@ -1052,7 +1047,7 @@ Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
   WHEN init_hsistate pc ~> hst THEN
   hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc).
 Proof.
-  unfold init_hsistate. wlp_step_bind hst HST.
+  unfold init_hsistate. wlp_bind hst HST.
   wlp_simplify.
   constructor; simpl; auto; [|constructor].
   - apply list_forall2_nil.
@@ -1266,7 +1261,7 @@ Definition sum_refines (hsi: hsval + ident) (si: sval + ident) :=
   | _, _ => False
   end.
 
-Inductive list_refines: hlist_sval -> list_sval -> Prop :=
+Inductive list_refines: list_hsval -> list_sval -> Prop :=
   | hsnil_ref: forall h, list_refines (HSnil h) Snil
   | hscons_ref: forall lhv lsv hv sv h,
       list_refines lhv lsv ->
@@ -1320,18 +1315,18 @@ Proof. constructor. Qed.
 
 End HFINAL_REFINES.
 
-Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv hlsv,
+Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
   (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
-  list_refines ge sp rs0 m0 hlsv lsv ->
-  forall hlsv' lsv',
-  list_refines ge' sp rs0 m0 hlsv' lsv' ->
-  hsval_list_proj hlsv = hsval_list_proj hlsv' ->
+  list_refines ge sp rs0 m0 lhsv lsv ->
+  forall lhsv' lsv',
+  list_refines ge' sp rs0 m0 lhsv' lsv' ->
+  hsval_list_proj lhsv = hsval_list_proj lhsv' ->
   seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0.
 Proof.
   induction 2; rename H into GFS.
-  - simpl. intros. destruct hlsv'; try discriminate. clear H0.
+  - simpl. intros. destruct lhsv'; try discriminate. clear H0.
     inv H. simpl. reflexivity.
-  - simpl. intros. destruct hlsv'; try discriminate.
+  - simpl. intros. destruct lhsv'; try discriminate.
     simpl in H2. inv H2. destruct lsv'; [inv H|].
     inv H. simpl.
     assert (SVALEQ: seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv0 rs0 m0). {
@@ -1534,7 +1529,7 @@ Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r:
   WHEN hsi_sreg_get hsl r ~> hsv THEN
   sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
 Proof.
-  intros HOK HREF. wlp_intros hsv HSV. unfold sval_refines.
+  intros HOK HREF. wlp_intro hsv HSV. unfold sval_refines.
   erewrite <- hsi_sreg_eval_correct; eauto.
   destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption].
   reflexivity.
@@ -1547,14 +1542,14 @@ Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros:
   sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros).
 Proof.
   intros HOK HREF. destruct ros; [| wlp_simplify].
-  wlp_step_bind hr HGET. wlp_simplify. unfold sval_refines.
+  wlp_bind hr HGET. wlp_simplify. unfold sval_refines.
   rewrite sval_refines_local_get; eauto.
 Qed.
 
 Lemma hSnil_correct:
   WHEN hSnil () ~> shv THEN hsval_list_proj shv = Snil.
 Proof.
-  wlp_simplify. unfold hSnil in Hexta. apply hC_hlist_sval_correct in Hexta.
+  wlp_simplify. unfold hSnil in Hexta. apply hC_list_hsval_correct in Hexta.
   simpl in *. symmetry. assumption.
 Qed.
 Global Opaque hSnil.
@@ -1565,9 +1560,9 @@ Lemma hScons_correct: forall lhsv hsv,
   hsval_list_proj lhsv' = Scons (hsval_proj hsv) (hsval_list_proj lhsv).
 Proof.
   destruct lhsv; wlp_simplify.
-  - unfold hScons in Hexta. apply hC_hlist_sval_correct in Hexta.
+  - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta.
     simpl in *. congruence.
-  - unfold hScons in Hexta. apply hC_hlist_sval_correct in Hexta. simpl in *. congruence.
+  - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence.
 Qed.
 Global Opaque hScons.
 Hint Resolve hScons_correct: wlp.
@@ -1578,7 +1573,7 @@ Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r:
   WHEN hsi_sreg_get hsl r ~> hsv THEN
   sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
 Proof.
-  intros HOK HREF. wlp_intros hsv HGET. destruct HREF as (_ & _ & A & _).
+  intros HOK HREF. wlp_intro hsv HGET. destruct HREF as (_ & _ & A & _).
   unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption.
   rewrite A by assumption. reflexivity.
 Qed.
@@ -1604,7 +1599,7 @@ Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r:
   hsval_proj hsv = hsval_proj hsv' ->
   sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
 Proof.
-  intros HOK HREF. wlp_intros hsv' HGET. intros PROJ.
+  intros HOK HREF. wlp_intro hsv' HGET. intros PROJ.
   unfold sval_refines. unfold seval_hsval.
   rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity].
   erewrite hsi_sreg_get_refines; eauto.
@@ -1620,7 +1615,7 @@ Lemma hlist_args_correct ge sp rs0 m0 hsl sl:
 Proof.
   intros HOK HREF. induction lr.
   - simpl. wlp_simplify. destruct exta; try discriminate. constructor.
-  - simpl. wlp_step_bind v V. wlp_step_bind hlsv HLSV. wlp_simplify.
+  - simpl. wlp_bind v V. wlp_bind lhsv HLSV. wlp_simplify.
     apply IHlr in HLSV. clear IHlr.
     destruct exta; try discriminate. simpl in H. inv H. constructor.
     + eapply hsval_list_proj_correct; eauto.
@@ -1641,7 +1636,7 @@ Proof.
   induction br.
   all: try (wlp_simplify; constructor; auto; fail).
   (* BA *)
-  - simpl. wlp_step_bind hsv HGET. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
+  - simpl. wlp_bind hsv HGET. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
 Qed.
 
 Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
@@ -1653,7 +1648,7 @@ Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
 Proof.
   intros HOK HREF.
   induction lbr; [wlp_simplify; constructor|].
-  simpl. wlp_step_bind ha HA. wlp_step_bind hl HL. wlp_simplify.
+  simpl. wlp_bind ha HA. wlp_bind hl HL. wlp_simplify.
   constructor; [|auto]. eapply hbuiltin_arg_correct; eauto.
 Qed.
 
@@ -1666,20 +1661,20 @@ Proof.
   intro HOK.
   destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
   (* Scall *)
-  - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_simplify. constructor.
+  - wlp_bind svos SVOS. wlp_bind sargs SARGS. wlp_simplify. constructor.
     + eapply hsum_left_correct; eauto.
     + eapply hlist_args_correct; eauto.
   (* Stailcall *)
-  - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_simplify. constructor.
+  - wlp_bind svos SVOS. wlp_bind sargs SARGS. wlp_simplify. constructor.
     + eapply hsum_left_correct; eauto.
     + eapply hlist_args_correct; eauto.
   (* Sbuiltin *)
   - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto.
   (* Sjumptable *)
-  - wlp_step_bind sv SV. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
+  - wlp_bind sv SV. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
   (* Sreturn *)
   - destruct o.
-    -- wlp_step_bind sv HGET. wlp_simplify. constructor. simpl.
+    -- wlp_bind sv HGET. wlp_simplify. constructor. simpl.
        eapply hsi_sreg_get_refines; eauto.
     -- wlp_simplify. repeat constructor.
 Qed.
@@ -1755,12 +1750,12 @@ Proof.
   - destruct bs2; wlp_simplify; try wlp_absurd. congruence.
   (* BA_splitlong *)
   - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
-    wlp_step_bind b1 B1. wlp_intros b2 B2.
+    wlp_bind b1 B1. wlp_intro b2 B2.
     rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
     reflexivity.
   (* BA_addptr *)
   - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
-    wlp_step_bind b1 B1. wlp_intros b2 B2.
+    wlp_bind b1 B1. wlp_intro b2 B2.
     rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
     reflexivity.
 Qed.
@@ -1822,18 +1817,18 @@ Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2:
 Proof.
   destruct fv1; destruct fv2; try (wlp_simplify; simpl in Hexta; wlp_absurd).
   (* HScall *)
-  - simpl. wlp_step_bind u1 REVMAP. wlp_step_bind u2 SIG. wlp_step_bind u3 RES.
-    wlp_step_bind u4 SVOS. wlp_intros u5 LSV.
+  - simpl. wlp_bind u1 REVMAP. wlp_bind u2 SIG. wlp_bind u3 RES.
+    wlp_bind u4 SVOS. wlp_intro u5 LSV.
     apply phys_check_correct in SIG. apply phys_check_correct in RES.
     apply revmap_check_single_correct in REVMAP. apply phys_check_correct in LSV.
     apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto).
   (* HStailcall *)
-  - simpl. wlp_step_bind u1 SIG. wlp_step_bind u2 SVOS. wlp_intros u3 LSV.
+  - simpl. wlp_bind u1 SIG. wlp_bind u2 SVOS. wlp_intro u3 LSV.
     apply phys_check_correct in SIG. apply phys_check_correct in LSV.
     apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto).
   (* HSbuiltin *)
-  - simpl. wlp_step_bind u1 RMAP. wlp_step_bind u2 EF. wlp_step_bind u3 RES.
-    wlp_intros u4 SARGS.
+  - simpl. wlp_bind u1 RMAP. wlp_bind u2 EF. wlp_bind u3 RES.
+    wlp_intro u4 SARGS.
     apply phys_check_correct in EF. apply phys_check_correct in RES.
     apply list_builtin_arg_simu_check_correct in SARGS. apply revmap_check_single_correct in RMAP.
     subst. repeat (constructor; auto).
@@ -1885,7 +1880,104 @@ Proof.
   wlp_simplify. constructor. 1-2: assumption.
 Qed.
 Hint Resolve hsstate_simu_check_correct: wlp.
-Global Opaque hsstate_simu_core.
+Global Opaque hsstate_simu_core. 
+
+Definition seval_list_hsval ge sp lhsv rs m := seval_list_sval ge sp (hsval_list_proj lhsv) rs m.
+
+Definition hok_args ge sp rs0 m0 hst lhsv :=
+  hsok_local ge sp rs0 m0 hst -> 
+  (seval_list_hsval ge sp lhsv rs0 m0 <> None).
+
+(* Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lhsv sv':
+  hsilocal_refines ge sp rs0 m0 hst st ->
+  hok_args ge sp rs0 m0 hst lhsv -> 
+  (hsok_local ge sp rs0 m0 hst -> seval_hsval ge sp hsv' rs0 m0 = seval_hsval ge sp (rsv lhsv (hsi_smem hst)) rs0 m0) ->
+  hsilocal_refines ge sp rs0 m0 (hslocal_set_sreg hst r rsv lsv) (slocal_set_sreg st r sv').
+Proof.
+  intros (ROK & RMEM & RVAL) OKA RSV.
+  unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split.
+  + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto.
+    intuition congruence.
+  + split; try tauto.
+    intros (HOKL & RSV2) r0.
+    rewrite red_PTree_set_correct.
+    rewrite hsi_sreg_eval_correct. unfold hsi_sreg_get.
+    destruct (Pos.eq_dec r r0).
+    * subst. rewrite PTree.gss, RSV; auto.
+      destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence.
+      eapply simplify_correct; eauto.
+    * intros; rewrite PTree.gso; auto.
+      rewrite <- RVAL, hsi_sreg_eval_correct; auto.
+Qed. *)
+
+(* Lemma refines_hokargs ge sp rs0 m0 hst st l:
+  hsistate_refines_dyn ge sp rs0 m0 hst st ->
+  WHEN hlist_args (hsi_local hst) l ~> lhsv THEN
+  hok_args ge sp rs0 m0 (hsi_local hst) lhsv.
+Proof.
+  unfold hok_args. intros (_ & HLREF & _).
+  wlp_intro lhsv LHSV. intros HOK.
+  eapply hlist_args_correct in LHSV; eauto.
+
+
+  intros (_ & HLREF & _) OK.
+  erewrite seval_list_sval_refines; eauto.
+  destruct HLREF as (OKEQ & _ & _).
+  rewrite <- OKEQ in OK.
+  destruct OK as (_ & _ & OK).
+  clear OKEQ; induction l as [|r l]; simpl; try congruence.
+  simplify_SOME x. congruence.
+Qed. *)
+
+(* Local Hint Resolve refines_okargs: core.
+Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
+  hsiexec_inst i hst = Some hst' ->
+  siexec_inst i st = Some st' ->
+  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'.
+Proof.
+  destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1;
+    inversion_clear STEP2; discriminate || (intro REF; eauto).
+  - (* Iop *)
+    eapply hsist_set_local_correct_dyn; eauto.
+    + eapply hslocal_set_sreg_correct; eauto.
+      simpl; intros.
+      erewrite seval_list_sval_refines; eauto.
+      erewrite seval_smem_refines; eauto.
+    + unfold sok_local; simpl; intros (PRE & MEM & REG).
+      intuition.
+      generalize (REG r0); clear REG.
+      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
+  - (* Iload *)
+    eapply hsist_set_local_correct_dyn; eauto.
+    + eapply hslocal_set_sreg_correct; eauto.
+      simpl; intros.
+      erewrite seval_list_sval_refines; eauto.
+      erewrite seval_smem_refines; eauto.
+    + unfold sok_local; simpl; intros (PRE & MEM & REG).
+      intuition.
+      generalize (REG r0); clear REG.
+      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
+  - (* Istore *)
+    eapply hsist_set_local_correct_dyn; eauto.
+    + eapply hslocal_set_mem_correct; eauto.
+      * simpl. simplify_SOME x.
+      * intros. simpl.
+        erewrite seval_list_sval_refines; eauto.
+        erewrite seval_smem_refines; eauto.
+        erewrite seval_sval_refines; eauto.
+    + unfold sok_local; simpl; intuition.
+  - (* Icond *)
+    destruct REF as (EXREF & LREF & NEST).
+    split.
+    + constructor; simpl; auto.
+      constructor; simpl; auto.
+      intros; erewrite seval_condition_refines; eauto.
+      unfold seval_condition.
+      erewrite seval_list_sval_refines; eauto.
+    + split; simpl; auto.
+      destruct NEST as [|st0 se lse TOP NEST];
+      econstructor; simpl; auto; constructor; auto.
+Qed. *)
 
 Definition hsexec (f: function) (pc:node): ?? hsstate :=
   DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";;
@@ -1899,6 +1991,15 @@ Definition hsexec (f: function) (pc:node): ?? hsstate :=
             RET {| hinternal := hst; hfinal := hsvf |}
   end.
 
+(**
+ * init_hsistate_correct_stat : OK
+ * init_hsistate_correct_dyn : OK
+ * hsexec_final_correct : OK
+ * hsiexec_inst_correct_dyn : TODO
+ * hsiexec_path_correct_dyn : TODO
+ * hfinal_refines_snone : OK
+ *)
+
 (* Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct
   hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core. *)
 
@@ -1930,9 +2031,9 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   let (pc2, pc1) := m in
   (* creating the hash-consing tables *)
   DO hC_sval <~ hCons hSVAL;;
-  DO hC_hlist_sval <~ hCons hLSVAL;;
+  DO hC_list_hsval <~ hCons hLSVAL;;
   DO hC_hsmem <~ hCons hSMEM;;
-  let hsexec := hsexec hC_sval.(hC) hC_hlist_sval.(hC) hC_hsmem.(hC) in
+  let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
   (* performing the hash-consed executions *)
   DO hst1 <~ hsexec f pc1;;
   DO hst2 <~ hsexec tf pc2;;
@@ -1944,13 +2045,13 @@ Lemma simu_check_single_correct dm tf f pc1 pc2:
   sexec_simu dm f tf pc1 pc2.
 Proof.
   unfold simu_check_single.
-  wlp_step_bind hC_sval HSVAL. wlp_step_bind hC_hlist_sval HLSVAL.
-  wlp_step_bind hC_hsmem HSMEM. wlp_step_bind hst1 HSEXEC1. wlp_step_bind hst2 HSEXEC2.
-  wlp_intros u HSIMU.
+  wlp_bind hC_sval HSVAL. wlp_bind hC_list_hsval HLSVAL.
+  wlp_bind hC_hsmem HSMEM. wlp_bind hst1 HSEXEC1. wlp_bind hst2 HSEXEC2.
+  wlp_intro u HSIMU.
   unfold sexec_simu. intros st1 SEXEC. explore.
   assert (TODO1: forall hs rhsv, hC hC_sval hs ~~> rhsv -> hsval_proj (hdata hs) = hsval_proj rhsv)
     by admit.
-  assert (TODO2: forall hs rhsv, hC hC_hlist_sval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv)
+  assert (TODO2: forall hs rhsv, hC hC_list_hsval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv)
     by admit.
   assert (TODO3: forall hs rhsv, hC hC_hsmem hs ~~> rhsv -> hsmem_proj (hdata hs) = hsmem_proj rhsv)
     by admit.