refactorisation + 1ere version de sstate

1 files changed, 169 insertions, 1461 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 53c00c8b..7025b90c 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -13,6 +13,16 @@ Require Import RTL BTL OptionMonad.
 Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
 Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)
 
+
+Record iblock_exec_context := {
+  cge: BTL.genv;
+  csp: val;
+  cstk: list stackframe;
+  cf: function;
+  crs0: regset;
+  cm0: mem
+}.
+
 (** * Syntax and semantics of symbolic values *)
 
 (* symbolic value *)
@@ -40,26 +50,26 @@ Fixpoint list_sval_inj (l: list sval): list_sval :=
 
 Local Open Scope option_monad_scope.
 
-Fixpoint eval_sval (ge: BTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val :=
+Fixpoint eval_sval ctx (sv: sval): option val :=
   match sv with
-  | Sinput r => Some (rs0#r)
+  | Sinput r => Some ((crs0 ctx)#r)
   | Sop op l sm =>
-     SOME args <- eval_list_sval ge sp l rs0 m0 IN
-     SOME m <- eval_smem ge sp sm rs0 m0 IN
-     eval_operation ge sp op args m
+     SOME args <- eval_list_sval ctx l IN
+     SOME m <- eval_smem ctx sm IN
+     eval_operation (cge ctx) (csp ctx) op args m
   | Sload sm trap chunk addr lsv =>
       match trap with
       | TRAP =>
-          SOME args <- eval_list_sval ge sp lsv rs0 m0 IN
-          SOME a <- eval_addressing ge sp addr args IN
-          SOME m <- eval_smem ge sp sm rs0 m0 IN
+          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
           Mem.loadv chunk m a
       | NOTRAP =>
-          SOME args <- eval_list_sval ge sp lsv rs0 m0 IN
-          match (eval_addressing ge sp addr args) with
+          SOME args <- eval_list_sval ctx lsv IN
+          match (eval_addressing (cge ctx) (csp ctx) addr args) with
           | None => Some (default_notrap_load_value chunk)
           | Some a =>
-              SOME m <- eval_smem ge sp sm rs0 m0 IN
+              SOME m <- eval_smem ctx sm IN
               match (Mem.loadv chunk m a) with
               | None => Some (default_notrap_load_value chunk)
               | Some val => Some val
@@ -67,52 +77,49 @@ Fixpoint eval_sval (ge: BTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): o
           end
       end
   end
-with eval_list_sval (ge: BTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) :=
+with eval_list_sval ctx (lsv: list_sval): option (list val) :=
   match lsv with
   | Snil => Some nil
   | Scons sv lsv' => 
-    SOME v <- eval_sval ge sp sv rs0 m0 IN
-    SOME lv <- eval_list_sval ge sp lsv' rs0 m0 IN
+    SOME v <- eval_sval ctx sv IN
+    SOME lv <- eval_list_sval ctx lsv' IN
     Some (v::lv)
   end
-with eval_smem (ge: BTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem :=
+with eval_smem ctx (sm: smem): option mem :=
   match sm with
-  | Sinit => Some m0
+  | Sinit => Some (cm0 ctx)
   | Sstore sm chunk addr lsv srce =>
-     SOME args <- eval_list_sval ge sp lsv rs0 m0 IN
-     SOME a <- eval_addressing ge sp addr args IN
-     SOME m <- eval_smem ge sp sm rs0 m0 IN
-     SOME sv <- eval_sval ge sp srce rs0 m0 IN
+     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
+     SOME sv <- eval_sval ctx srce IN
      Mem.storev chunk m a sv
   end.
 
-Lemma eval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
-   (forall r : reg, eval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
-   eval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l).
+Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: 
+  (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) ->
+  eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l).
 Proof.
   intros H; induction l as [|r l]; simpl; repeat autodestruct; auto.
 Qed.
 
-Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool :=
-  SOME args <- eval_list_sval ge sp lsv rs0 m0 IN
-  SOME m <- eval_smem ge sp sm rs0 m0 IN
+Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool :=
+  SOME args <- eval_list_sval ctx lsv IN
+  SOME m <- eval_smem ctx sm IN
   eval_condition cond args m.
 
 
 (** * Auxiliary definitions on Builtins *)
-(* TODO: clean this. Some generic stuffs could be put in [AST.v] *)
+(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *)
 
 Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)
 
-Variable ge: BTL.genv.
-Variable sp: val.
+Variable ctx: iblock_exec_context.
 Variable m: mem.
-Variable rs0: regset.
-Variable m0: mem.
 
 Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop :=
   | seval_BA: forall x v,
-      eval_sval ge sp x rs0 m0 = Some v ->
+      eval_sval ctx x = Some v ->
       seval_builtin_arg (BA x) v
   | seval_BA_int: forall n,
       seval_builtin_arg (BA_int n) (Vint n)
@@ -123,22 +130,23 @@ Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop :=
   | seval_BA_single: forall n,
       seval_builtin_arg (BA_single n) (Vsingle n)
   | seval_BA_loadstack: forall chunk ofs v,
-      Mem.loadv chunk m (Val.offset_ptr sp ofs) = Some v ->
+      Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v ->
       seval_builtin_arg (BA_loadstack chunk ofs) v
   | seval_BA_addrstack: forall ofs,
-      seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr sp ofs)
+      seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs)
   | seval_BA_loadglobal: forall chunk id ofs v,
-      Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v ->
+      Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v ->
       seval_builtin_arg (BA_loadglobal chunk id ofs) v
   | seval_BA_addrglobal: forall id ofs,
-      seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs)
+      seval_builtin_arg (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)
   | 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)
-                       (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
+                       (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.
@@ -159,7 +167,7 @@ Qed.
 
 End SEVAL_BUILTIN_ARG.
 
-(* NB: generic function that could be put into [AST] file *)
+(* NB: (cge ctx)neric function that could be put into [AST] file *)
 Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
   match arg with
   | BA x => BA (f x)
@@ -175,10 +183,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 ge sp rs m rs0 m0 sreg: forall arg varg,
-  (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
-  eval_builtin_arg ge (fun r => rs # r) sp m arg varg ->
-  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg.
+Lemma seval_builtin_arg_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.
 Proof.
   induction arg.
   all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
@@ -188,10 +196,10 @@ Proof.
     eapply IHarg1; eauto. eapply IHarg2; eauto.
 Qed.
 
-Lemma seval_builtin_args_correct ge sp rs m rs0 m0 sreg args vargs:
-  (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
-  eval_builtin_args ge (fun r => rs # r) sp m args vargs ->
-  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs.
+Lemma seval_builtin_args_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.
 Proof.
   induction 2.
   - constructor.
@@ -199,10 +207,10 @@ Proof.
     eapply seval_builtin_arg_correct; eauto.
 Qed.
 
-Lemma seval_builtin_arg_complete ge sp rs m rs0 m0 sreg: forall arg varg,
-  (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
-  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg ->
-  eval_builtin_arg ge (fun r => rs # r) sp m arg varg.
+Lemma seval_builtin_arg_complete 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_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.
 Proof.
   induction arg.
   all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence).
@@ -213,10 +221,10 @@ Proof.
     eapply IHarg1; eauto. eapply IHarg2; eauto.
 Qed.
 
-Lemma seval_builtin_args_complete ge sp rs m rs0 m0 sreg: forall args vargs,
-  (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
-  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs ->
-  eval_builtin_args ge (fun r => rs # r) sp m args vargs.
+Lemma seval_builtin_args_complete 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_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
 Proof.
   induction args.
   - simpl. intros. inv H0. constructor.
@@ -225,16 +233,16 @@ Proof.
     eapply seval_builtin_arg_complete; eauto.
 Qed.
 
-Fixpoint seval_builtin_sval ge sp bsv rs0 m0 :=
+Fixpoint seval_builtin_sval ctx bsv :=
   match bsv with
-  | BA sv => SOME v <- eval_sval ge sp sv rs0 m0 IN Some (BA v)
+  | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v)
   | BA_splitlong sv1 sv2 =>
-      SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
-      SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN
+      SOME v1 <- seval_builtin_sval ctx sv1 IN
+      SOME v2 <- seval_builtin_sval ctx sv2 IN
       Some (BA_splitlong v1 v2)
   | BA_addptr sv1 sv2 =>
-      SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
-      SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN
+      SOME v1 <- seval_builtin_sval ctx sv1 IN
+      SOME v2 <- seval_builtin_sval ctx sv2 IN
       Some (BA_addptr v1 v2)
   | BA_int i => Some (BA_int i)
   | BA_long l => Some (BA_long l)
@@ -246,56 +254,54 @@ Fixpoint seval_builtin_sval ge sp bsv rs0 m0 :=
   | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
   end.
 
-Fixpoint eval_list_builtin_sval ge sp lbsv rs0 m0 :=
+Fixpoint eval_list_builtin_sval ctx lbsv :=
   match lbsv with
   | nil => Some nil
-  | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN
-                 SOME lv <- eval_list_builtin_sval ge sp lbsv rs0 m0 IN
+  | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN
+                 SOME lv <- eval_list_builtin_sval ctx lbsv IN
                  Some (v::lv)
   end.
 
-Lemma eval_list_builtin_sval_nil ge sp rs0 m0 lbs2:
-  eval_list_builtin_sval ge sp lbs2 rs0 m0 = Some nil ->
+Lemma eval_list_builtin_sval_nil ctx lbs2:
+  eval_list_builtin_sval ctx lbs2 = Some nil ->
   lbs2 = nil.
 Proof.
-  destruct lbs2; simpl; auto.
-  intros. destruct (seval_builtin_sval _ _ _ _ _);
-    try destruct (eval_list_builtin_sval _ _ _ _ _); discriminate.
+  destruct lbs2; simpl; repeat autodestruct; congruence.
 Qed.
 
-Lemma seval_builtin_sval_arg ge sp rs0 m0 bs:
+Lemma seval_builtin_sval_arg ctx bs:
    forall ba m v, 
-   seval_builtin_sval ge sp bs rs0 m0 = Some ba ->
-   eval_builtin_arg ge (fun id => id) sp m ba v ->
-   seval_builtin_arg ge sp m rs0 m0 bs v.
+   seval_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.
 Proof.
    induction bs; simpl; 
    try (intros ba m v H; inversion H; subst; clear H;
         intros H; inversion H; subst;
         econstructor; auto; fail).
-   - intros ba m v; destruct (eval_sval _ _ _ _ _) eqn: SV;
+   - intros ba m v; destruct (eval_sval _ _) eqn: SV;
      intros H; inversion H; subst; clear H.
      intros H; inversion H; subst.
      econstructor; auto.
    - intros ba m v. 
-     destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence.
-     destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence.
+     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
+     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
      intros H; inversion H; subst; clear H.
      intros H; inversion H; subst.
      econstructor; eauto.
    - intros ba m v. 
-     destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence.
-     destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence.
+     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
+     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
      intros H; inversion H; subst; clear H.
      intros H; inversion H; subst.
      econstructor; eauto.
 Qed.
 
-Lemma seval_builtin_arg_sval ge sp m rs0 m0 v: forall bs,
-  seval_builtin_arg ge sp m rs0 m0 bs v ->
+Lemma seval_builtin_arg_sval ctx m v: forall bs,
+  seval_builtin_arg ctx m bs v ->
   exists ba,
-    seval_builtin_sval ge sp bs rs0 m0 = Some ba
-    /\ eval_builtin_arg ge (fun id => id) sp m ba v.
+    seval_builtin_sval ctx bs = Some ba
+    /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.
 Proof.
   induction 1.
   all: try (eexists; constructor; [simpl; reflexivity | constructor]).
@@ -315,28 +321,28 @@ Proof.
     + constructor; assumption.
 Qed.
 
-Lemma seval_builtin_sval_args ge sp rs0 m0 lbs:
+Lemma seval_builtin_sval_args ctx lbs:
    forall lba m v, 
-   eval_list_builtin_sval ge sp lbs rs0 m0 = Some lba ->
-   list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba v ->
-   seval_builtin_args ge sp m rs0 m0 lbs 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.
 Proof.
   unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
   - intros H; inversion H; subst; clear H.
     intros H; inversion H. econstructor.
-  - destruct (seval_builtin_sval _ _ _ _ _) eqn:SV; try congruence.
-    destruct (eval_list_builtin_sval _ _ _ _ _) eqn: SVL; try congruence.
+  - destruct (seval_builtin_sval _ _) eqn:SV; try congruence.
+    destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence.
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst; clear H. 
     econstructor; eauto.
     eapply seval_builtin_sval_arg; eauto.
 Qed.
 
-Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs,
-  seval_builtin_args ge sp m rs0 m0 lbs lv ->
+Lemma seval_builtin_args_sval ctx m lv: forall lbs,
+  seval_builtin_args ctx m lbs lv ->
   exists lba,
-    eval_list_builtin_sval ge sp lbs rs0 m0 = Some lba
-    /\ list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba lv.
+    eval_list_builtin_sval ctx lbs = Some lba
+    /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv.
 Proof.
   induction 1.
   - eexists. constructor.
@@ -349,10 +355,10 @@ Proof.
     + constructor; assumption.
 Qed.
 
-Lemma seval_builtin_sval_correct ge sp m rs0 m0: forall bs1 v bs2,
-  seval_builtin_arg ge sp m rs0 m0 bs1 v ->
-  (seval_builtin_sval ge sp bs1 rs0 m0) = (seval_builtin_sval ge sp bs2 rs0 m0) ->
-  seval_builtin_arg ge sp m rs0 m0 bs2 v.
+Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2,
+  seval_builtin_arg ctx m bs1 v ->
+  (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) ->
+  seval_builtin_arg ctx m bs2 v.
 Proof.
   intros. exploit seval_builtin_arg_sval; eauto.
   intros (ba & X1 & X2).
@@ -360,10 +366,10 @@ Proof.
   congruence.
 Qed.
 
-Lemma eval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1,
-  seval_builtin_args ge sp m rs0 m0 lbs1 vargs ->
-  forall lbs2, (eval_list_builtin_sval ge sp lbs1 rs0 m0) = (eval_list_builtin_sval ge sp lbs2 rs0 m0) ->
-  seval_builtin_args ge sp m rs0 m0 lbs2 vargs.
+Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
+  seval_builtin_args 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.
 Proof.
   intros. exploit seval_builtin_args_sval; eauto.
   intros (ba & X1 & X2).
@@ -383,164 +389,64 @@ Inductive sfval :=
   | Sreturn: option sval -> sfval
 .
 
-Definition sfind_function (ge: BTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef :=
+Definition sfind_function ctx (svos : sval + ident): option fundef :=
   match svos with
-  | inl sv => SOME v <- eval_sval ge sp sv rs0 m0 IN Genv.find_funct ge v
-  | inr symb => SOME b <- Genv.find_symbol ge symb IN Genv.find_funct_ptr ge b
+  | inl sv => SOME v <- eval_sval ctx sv IN Genv.find_funct (cge ctx) v
+  | inr symb => SOME b <- Genv.find_symbol (cge ctx) symb IN Genv.find_funct_ptr (cge ctx) b
   end
 .
 
-Inductive sem_sfval (ge: BTL.genv) (sp:val) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop :=
+Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
   | exec_Sgoto pc rs m:
-      sem_sfval ge sp stack f rs0 m0 (Sgoto pc) rs m E0 (State stack f sp pc rs m)
+      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m)
   | exec_Sreturn stk osv rs m m' v:
-      sp = (Vptr stk Ptrofs.zero) ->
-      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      match osv with Some sv => eval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
-      sem_sfval ge sp stack f rs0 m0 (Sreturn osv) rs m 
-         E0 (Returnstate stack v m')
+      (csp ctx) = (Vptr stk Ptrofs.zero) ->
+      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
+      match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
+      sem_sfval ctx (Sreturn osv) rs m 
+         E0 (Returnstate (cstk ctx) v m')
   | exec_Scall rs m sig svos lsv args res pc fd:
-      sfind_function ge sp svos rs0 m0 = Some fd ->
+      sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
-      eval_list_sval ge sp lsv rs0 m0 = Some args ->
-      sem_sfval ge sp stack f rs0 m0 (Scall sig svos lsv res pc) rs m
-        E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m)
+      eval_list_sval ctx lsv = Some args ->
+      sem_sfval ctx (Scall sig svos lsv res pc) rs m
+        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m)
   | exec_Stailcall stk rs m sig svos args fd m' lsv:
-      sfind_function ge sp svos rs0 m0 = Some fd ->
+      sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
-      sp = Vptr stk Ptrofs.zero ->
-      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      eval_list_sval ge sp lsv rs0 m0 = Some args ->
-      sem_sfval ge sp stack f rs0 m0 (Stailcall sig svos lsv) rs m
-        E0 (Callstate stack fd args m')
+      (csp ctx) = Vptr stk Ptrofs.zero ->
+      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
+      eval_list_sval ctx lsv = Some args ->
+      sem_sfval ctx (Stailcall sig svos lsv) rs m
+        E0 (Callstate (cstk ctx) fd args m')
   | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
-      seval_builtin_args ge sp m rs0 m0 sargs vargs ->
-      external_call ef ge vargs m t vres m' ->
-      sem_sfval ge sp stack f rs0 m0 (Sbuiltin ef sargs res pc) rs m
-        t (State stack f sp pc (regmap_setres res vres rs) m')
+      seval_builtin_args ctx m sargs vargs ->
+      external_call ef (cge ctx) vargs m t vres m' ->
+      sem_sfval ctx (Sbuiltin ef sargs res pc) rs m
+        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m')
   | exec_Sjumptable sv tbl pc' n rs m:
-      eval_sval ge sp sv rs0 m0 = Some (Vint n) ->
+      eval_sval ctx sv = Some (Vint n) ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      sem_sfval ge sp stack f rs0 m0 (Sjumptable sv tbl) rs m
-        E0 (State stack f sp pc' rs m)
+      sem_sfval ctx (Sjumptable sv tbl) rs m
+        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
 .
 
 
-(** * Preservation properties *)
-
-Section SymbValPreserved.
-
-Variable ge ge': BTL.genv.
-
-Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
-
-Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
-
-Lemma senv_find_symbol_preserved id:
-  Senv.find_symbol ge id = Senv.find_symbol ge' id.
-Proof.
-  destruct senv_preserved_BTL as (A & B & C). congruence.
-Qed.
-
-Lemma senv_symbol_address_preserved id ofs:
-  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
-Proof.
-  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
-  reflexivity.
-Qed.
-
-Lemma eval_sval_preserved sp sv rs0 m0:
-  eval_sval ge sp sv rs0 m0 = eval_sval ge' sp sv rs0 m0.
-Proof.
-  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval ge sp lsv rs0 m0 = eval_list_sval ge' sp lsv rs0 m0)
-                                   (P1 := fun sm => eval_smem ge sp sm rs0 m0 = eval_smem ge' sp sm rs0 m0); simpl; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _ _ _); auto.
-    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _ _ _); auto.
-    erewrite eval_operation_preserved; eauto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _ _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _ _ _); auto.
-    rewrite IHsv0; auto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _ _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; clear IHsv. destruct (eval_smem _ _ _ _); auto.
-    rewrite IHsv1; auto.
-Qed.
-
-Lemma seval_builtin_arg_preserved sp m rs0 m0:
-  forall bs varg,
-  seval_builtin_arg ge sp m rs0 m0 bs varg ->
-  seval_builtin_arg ge' sp m rs0 m0 bs varg.
-Proof.
-  induction 1.
-  all: try (constructor; auto).
-  - rewrite <- eval_sval_preserved. assumption.
-  - rewrite <- senv_symbol_address_preserved. assumption.
-  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
-Qed.
-
-Lemma seval_builtin_args_preserved sp m rs0 m0 lbs vargs:
-  seval_builtin_args ge sp m rs0 m0 lbs vargs ->
-  seval_builtin_args ge' sp m rs0 m0 lbs vargs.
-Proof.
-  induction 1; constructor; eauto.
-  eapply seval_builtin_arg_preserved; auto.
-Qed.
-
-Lemma list_sval_eval_preserved sp lsv rs0 m0: 
-  eval_list_sval ge sp lsv rs0 m0 = eval_list_sval ge' sp lsv rs0 m0.
-Proof.
-  induction lsv; simpl; auto.
-  rewrite eval_sval_preserved. destruct (eval_sval _ _ _ _); auto.
-  rewrite IHlsv; auto.
-Qed.
-
-Lemma smem_eval_preserved sp sm rs0 m0: 
-  eval_smem ge sp sm rs0 m0 = eval_smem ge' sp sm rs0 m0.
-Proof.
-  induction sm; simpl; auto.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _ _ _); auto.
-  erewrite <- eval_addressing_preserved; eauto.
-  destruct (eval_addressing _ sp _ _); auto.
-  rewrite IHsm; clear IHsm. destruct (eval_smem _ _ _ _); auto.
-  rewrite eval_sval_preserved; auto.
-Qed.
-
-Lemma seval_condition_preserved sp cond lsv sm rs0 m0:
- seval_condition ge sp cond lsv sm rs0 m0 = seval_condition ge' sp cond lsv sm rs0 m0.
-Proof.
-  unfold seval_condition.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _ _ _); auto.
-  rewrite smem_eval_preserved; auto.
-Qed.
-
-End SymbValPreserved.
-
 
 (* Syntax and Semantics of symbolic internal states *)
-(* [si_pre] is a precondition on initial ge, sp, rs0, m0 *)
-Record sistate := { si_pre: BTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }.
+(* [si_pre] is a precondition on initial context *)
+Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }.
 
-(* Predicate on which (rs, m) is a possible final state after evaluating [st] on (rs0, m0) *)
-Definition sem_sistate (ge: BTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop :=
-  st.(si_pre) ge sp rs0 m0
-  /\ eval_smem ge sp st.(si_smem) rs0 m0 = Some m
-  /\ forall (r:reg), eval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r).
+(* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *)
+Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop :=
+  st.(si_pre) ctx
+  /\ eval_smem ctx st.(si_smem) = Some m
+  /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).
 
-Definition abort_sistate (ge: BTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem): Prop :=
-  ~(st.(si_pre) ge sp rs0 m0)
-  \/ eval_smem ge sp st.(si_smem) rs0 m0 = None
-  \/ exists (r: reg), eval_sval ge sp (st.(si_sreg) r) rs0 m0 = None.
-
-Record sstate_exit := { se_sis:> sistate; se_sfv: sfval }.
-
-Definition sem_sexit ge (sp:val) (st: sstate_exit) stack f (rs0: regset) (m0: mem) rs m (t: trace) (s:BTL.state) :=
-     sem_sistate ge sp st rs0 m0 rs m /\
-     sem_sfval ge sp stack f rs0 m0 st.(se_sfv) rs m t s
-  .
+Definition abort_sistate ctx (st: sistate): Prop :=
+  ~(st.(si_pre) ctx)
+  \/ eval_smem ctx st.(si_smem) = None
+  \/ exists (r: reg), eval_sval ctx (st.(si_sreg) r) = None.
 
 (** * Symbolic execution of final step *)
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
@@ -567,10 +473,10 @@ Definition sexec_final_sfv (i: final) (sis: sistate): sfval :=
 
 Local Hint Constructors sem_sfval: core.
 
-Lemma sexec_final_svf_correct ge sp i f sis stack rs0 m0 t rs m s:
-  sem_sistate ge sp sis rs0 m0 rs m ->
-  final_step ge stack f sp rs m i t s -> 
-  sem_sfval ge sp stack f rs0 m0 (sexec_final_sfv i sis) rs m t s.
+Lemma sexec_final_svf_correct ctx i sis t rs m s:
+  sem_sistate ctx sis rs m ->
+  final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
+  sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
 Proof.
   intros (PRE&MEM&REG). 
   destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto.
@@ -578,9 +484,9 @@ Proof.
     - destruct ros; simpl in * |- *; auto.
       rewrite REG; auto.
     - erewrite eval_list_sval_inj; simpl; auto.
-  + (* Btailcall *) intros. eapply exec_Stailcall; auto.
-    - destruct ros; simpl in * |- *; auto.
-      rewrite REG; auto.
+  + (* Btailcall *) intros. eapply exec_Stailcall; eauto.
+    - destruct ros; simpl in * |- *; eauto.
+      rewrite REG; eauto.
     - erewrite eval_list_sval_inj; simpl; auto.
   + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
     eapply seval_builtin_args_correct; eauto.
@@ -590,10 +496,10 @@ Qed.
 Local Hint Constructors final_step: core.
 Local Hint Resolve seval_builtin_args_complete: core.
 
-Lemma sexec_final_svf_complete ge sp i f sis stack rs0 m0 t rs m s:
-  sem_sistate ge sp sis rs0 m0 rs m ->
-  sem_sfval ge sp stack f rs0 m0 (sexec_final_sfv i sis) rs m t s
-  -> final_step ge stack f sp rs m i t s.
+Lemma sexec_final_svf_complete ctx i sis t rs m s:
+  sem_sistate ctx sis rs m ->
+  sem_sfval ctx (sexec_final_sfv i sis) rs m t s
+  -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
 Proof.
   intros (PRE&MEM&REG).
   destruct i; simpl; intros LAST; inv LAST; eauto.
@@ -615,1217 +521,19 @@ Proof.
     congruence.
 Qed.
 
-
-(* TODO: clean/recover this COPY-PASTE OF RTLpathSE_theory.v 
-
-
-(* Syntax and semantics of symbolic exit states *)
-
-Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop :=
-  forall ext, List.In ext lx ->
-  seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some false.
-
-Lemma all_fallthrough_revcons ge sp ext rs m lx:
-  all_fallthrough ge sp (ext::lx) rs m ->
-  seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false
-  /\ all_fallthrough ge sp lx rs m.
-Proof.
-  intros ALLFU. constructor.
-  - assert (In ext (ext::lx)) by (constructor; auto). apply ALLFU in H. assumption.
-  - intros ext' INEXT. assert (In ext' (ext::lx)) by (apply in_cons; auto).
-    apply ALLFU in H. assumption.
-Qed.
-
-(** Semantic of an exit in pseudo code:
-     if si_cond (si_condargs)
-       si_elocal; goto if_so
-     else ()
-*)
-
-Definition ssem_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop :=
-    seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true
- /\ ssem_local ge sp (si_elocal ext) rs m rs' m'
- /\ (si_ifso ext) = pc'.
-
-(* Either an abort on the condition evaluation OR an abort on the sistate_local IF the condition was true *)
-Definition sabort_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) : Prop :=
-  let sev_cond := seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m in
-  sev_cond = None
-  \/ (sev_cond = Some true /\ sabort_local ge sp ext.(si_elocal) rs m).
-
-(** * Syntax and Semantics of symbolic internal state *)
-Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 
-
-Definition all_fallthrough_upto_exit ge sp ext lx' lx rs m : Prop :=
-  is_tail (ext::lx') lx /\ all_fallthrough ge sp lx' rs m.
-
-(** Semantic of a sistate in pseudo code:
-     si_exit1; si_exit2; ...; si_exitn;
-     si_local; goto si_pc *)
-
-(* Note: in RTLpath, is.(icontinue) = false iff we took an early exit *)
-
-Definition ssem_internal (ge: RTL.genv) (sp:val) (st: sistate) (rs: regset) (m: mem) (is: istate): Prop :=
-  if (is.(icontinue)) 
-  then 
-    ssem_local ge sp st.(si_local) rs m is.(irs) is.(imem) 
-    /\ st.(si_pc) = is.(ipc)
-    /\ all_fallthrough ge sp st.(si_exits) rs m
-  else exists ext lx,
-    ssem_exit ge sp ext rs m is.(irs) is.(imem) is.(ipc)
-    /\ all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m.
-
-Definition sabort (ge: RTL.genv) (sp: val) (st: sistate) (rs: regset) (m: mem): Prop :=
-  (* No early exit was met but we aborted on the si_local *)
-  (all_fallthrough ge sp st.(si_exits) rs m /\ sabort_local ge sp st.(si_local) rs m)
-  (* OR we aborted on an evaluation of one of the early exits *)
-  \/ (exists ext lx, all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m /\ sabort_exit ge sp ext rs m).
-
-Definition ssem_internal_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop :=
-  match ois with
-  | Some is => ssem_internal ge sp st rs0 m0 is
-  | None => sabort ge sp st rs0 m0
-  end.
-
-Definition ssem_internal_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop :=
-  match ost with
-  | Some st => ssem_internal_opt ge sp st rs0 m0 ois
-  | None => ois=None
-  end.
-
-(** * An internal state represents a parallel program !
-
-     We prove below that the semantics [ssem_internal_opt] is deterministic.
-
- *)
-
-Definition istate_eq ist1 ist2 :=
-  ist1.(icontinue) = ist2.(icontinue) /\
-  ist1.(ipc) = ist2.(ipc) /\
-  (forall r, (ist1.(irs)#r) = ist2.(irs)#r) /\ 
-  ist1.(imem) = ist2.(imem).
-
-Lemma all_fallthrough_noexit ge sp ext lx rs0 m0 rs m pc:
-  ssem_exit ge sp ext rs0 m0 rs m pc ->
-  In ext lx ->
-  all_fallthrough ge sp lx rs0 m0 ->
-  False.
-Proof.
-  Local Hint Resolve is_tail_in: core.
-  intros SSEM INE ALLF.
-  destruct SSEM as (SSEM & SSEM').
-  unfold all_fallthrough in ALLF. rewrite ALLF in SSEM; eauto.
-  discriminate.
-Qed.
-
-Lemma ssem_internal_exclude_incompatible_continue ge sp st rs m is1 is2:
-  is1.(icontinue) = true ->
-  is2.(icontinue) = false ->
-  ssem_internal ge sp st rs m is1 ->
-  ssem_internal ge sp st rs m is2 ->
-  False.
-Proof.
-  Local Hint Resolve all_fallthrough_noexit: core.
-  unfold ssem_internal.
-  intros CONT1 CONT2.
-  rewrite CONT1, CONT2; simpl.
-  intuition eauto.
-  destruct H0 as (ext & lx & SSEME & ALLFU).
-  destruct ALLFU as (ALLFU & ALLFU').
-  eapply all_fallthrough_noexit; eauto.
-Qed.
-
-Lemma ssem_internal_determ_continue ge sp st rs m is1 is2:
-   ssem_internal ge sp st rs m is1 ->
-   ssem_internal ge sp st rs m is2 ->
-   is1.(icontinue) = is2.(icontinue).
-Proof.
-   Local Hint Resolve ssem_internal_exclude_incompatible_continue: core.
-   destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto.
-   intros H1 H2. assert (absurd: False); intuition.
-   destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto.
-Qed.
-
-Lemma ssem_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2:
-  ssem_local ge sp st rs0 m0 rs1 m1 ->
-  ssem_local ge sp st rs0 m0 rs2 m2 ->
-  (forall r, rs1#r = rs2#r) /\ m1 = m2.
-Proof.
-  unfold ssem_local. intuition try congruence.
-  generalize (H5 r); rewrite H4; congruence.
-Qed.
-
-(* TODO: lemma to move in Coqlib *)
-Lemma is_tail_bounded_total {A} (l1 l2 l3: list A): is_tail l1 l3 -> is_tail l2 l3
-  -> is_tail l1 l2 \/ is_tail l2 l1.
-Proof.
-  Local Hint Resolve is_tail_cons: core.
-  induction 1 as [|i l1 l3 T1 IND]; simpl; auto.
-  intros T2; inversion T2; subst; auto.
-Qed.
-
-Lemma exit_cond_determ ge sp rs0 m0 l1 l2: 
-  is_tail l1 l2 -> forall ext1 lx1 ext2 lx2, 
-  l1=(ext1 :: lx1) -> 
-  l2=(ext2 :: lx2) ->
-  all_fallthrough ge sp lx1 rs0 m0 ->
-  seval_condition ge sp (si_cond ext1) (si_scondargs ext1) (si_smem (si_elocal ext1)) rs0 m0 = Some true ->
-  all_fallthrough ge sp lx2 rs0 m0 ->
-  ext1=ext2.
-Proof.
-  destruct 1 as [l1|i l1 l3 T1]; intros ext1 lx1 ext2 lx2 EQ1 EQ2; subst; 
-  inversion EQ2; subst; auto.
-  intros D1 EVAL NYE.
-  Local Hint Resolve is_tail_in: core.
-  unfold all_fallthrough in NYE.
-  rewrite NYE in EVAL; eauto.
-  try congruence.
-Qed.
-
-Lemma ssem_exit_determ ge sp ext rs0 m0 rs1 m1 pc1 rs2 m2 pc2:
-  ssem_exit ge sp ext rs0 m0 rs1 m1 pc1 ->
-  ssem_exit ge sp ext rs0 m0 rs2 m2 pc2 ->
-  pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2.
-Proof.
-  Local Hint Resolve exit_cond_determ eq_sym: core.
-  intros SSEM1 SSEM2. destruct SSEM1 as (SEVAL1 & SLOC1 & PCEQ1). destruct SSEM2 as (SEVAL2 & SLOC2 & PCEQ2). subst.
-  destruct (ssem_local_determ ge sp (si_elocal ext) rs0 m0 rs1 m1 rs2 m2); auto.
-Qed.
-
-Remark is_tail_inv_left {A: Type} (a a': A) l l':
-  is_tail (a::l) (a'::l') ->
-  (a = a' /\ l = l') \/ (In a l' /\ is_tail l (a'::l')).
-Proof.
-  intros. inv H.
-  - left. eauto.
-  - right. econstructor.
-    + eapply is_tail_in; eauto.
-    + eapply is_tail_cons_left; eauto.
-Qed.
-
-Lemma ssem_internal_determ ge sp st rs m is1 is2:
-  ssem_internal ge sp st rs m is1 ->
-  ssem_internal ge sp st rs m is2 ->
-  istate_eq is1 is2.
-Proof.
-  unfold istate_eq.
-  intros SEM1 SEM2. 
-  exploit (ssem_internal_determ_continue ge sp st rs m is1 is2); eauto.
-  intros CONTEQ. unfold ssem_internal in * |-. rewrite CONTEQ in * |- *.
-  destruct (icontinue is2).
-  - destruct (ssem_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); 
-    intuition (try congruence).
-  - destruct SEM1 as (ext1 & lx1 & SSEME1 & ALLFU1). destruct SEM2 as (ext2 & lx2 & SSEME2 & ALLFU2).
-    destruct ALLFU1 as (ALLFU1 & ALLFU1'). destruct ALLFU2 as (ALLFU2 & ALLFU2').
-    destruct SSEME1 as (SSEME1 & SSEME1' & SSEME1''). destruct SSEME2 as (SSEME2 & SSEME2' & SSEME2'').
-    assert (X:ext1=ext2).
-    { destruct (is_tail_bounded_total (ext1 :: lx1) (ext2 :: lx2) (si_exits st)) as [TAIL|TAIL]; eauto. }
-    subst. destruct (ssem_local_determ ge sp (si_elocal ext2) rs m (irs is1) (imem is1) (irs is2) (imem is2)); auto.
-    intuition. congruence.
-Qed.
-
-Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m':
-  ssem_local ge sp loc rs m rs' m' ->
-  sabort_local ge sp loc rs m ->
-  False.
-Proof.
-  intros SIML ABORT. inv SIML. destruct H0 as (H0 & H0').
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
-Qed.
-
-Lemma ssem_local_exclude_sabort ge sp st rs m rs' m':
-  ssem_local ge sp (si_local st) rs m rs' m' ->
-  all_fallthrough ge sp (si_exits st) rs m ->
-  sabort ge sp st rs m ->
-  False.
-Proof.
-  intros SIML ALLF ABORT.
-  inv ABORT.
-  - intuition; eapply ssem_local_exclude_sabort_local; eauto.
-  - destruct H as (ext & lx & ALLFU & SABORT).
-    destruct ALLFU as (TAIL & _). eapply is_tail_in in TAIL.
-    eapply ALLF in TAIL.
-    destruct SABORT as [CONDFAIL | (CONDTRUE & ABORTL)]; congruence.
-Qed.
-
-Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc':
-  ssem_exit ge sp ext rs m rs' m' pc' ->
-  all_fallthrough_upto_exit ge sp ext lx exits rs m ->
-  all_fallthrough_upto_exit ge sp ext' lx' exits rs m ->
-  is_tail (ext'::lx') (ext::lx).
-Proof.
-  intros SSEME ALLFU ALLFU'.
-  destruct ALLFU as (ISTAIL & ALLFU). destruct ALLFU' as (ISTAIL' & ALLFU').
-  destruct (is_tail_bounded_total (ext::lx) (ext'::lx') exits); eauto.
-  inv H.
-  - econstructor; eauto.
-  - eapply is_tail_in in H2. eapply ALLFU' in H2.
-    destruct SSEME as (SEVAL & _). congruence.
-Qed.
-
-Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc':
-  ssem_exit ge sp ext rs m rs' m' pc' ->
-  sabort_exit ge sp ext rs m ->
-  False.
-Proof.
-  intros A B. destruct A as (A & A' & A''). inv B.
-  - congruence.
-  - destruct H as (_ & H). eapply ssem_local_exclude_sabort_local; eauto.
-Qed.
-
-Lemma ssem_exit_exclude_sabort ge sp ext st lx rs m rs' m' pc':
-  ssem_exit ge sp ext rs m rs' m' pc' ->
-  all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m ->
-  sabort ge sp st rs m ->
-  False.
-Proof.
-  intros SSEM ALLFU ABORT.
-  inv ABORT.
-  - destruct H as (ALLF & _). destruct ALLFU as (TAIL & _).
-    eapply is_tail_in in TAIL.
-    destruct SSEM as (SEVAL & _ & _).
-    eapply ALLF in TAIL. congruence.
-  - destruct H as (ext' & lx' & ALLFU' & ABORT).
-    exploit ssem_exit_fallthrough_upto_exit; eauto. intros ITAIL.
-    destruct ALLFU as (ALLFU1 & ALLFU2). destruct ALLFU' as (ALLFU1' & ALLFU2').
-    exploit (is_tail_inv_left ext' ext lx' lx); eauto. intro. inv H.
-    + inv H0. eapply ssem_exit_exclude_sabort_exit; eauto.
-    + destruct H0 as (INE & TAIL). eapply ALLFU2 in INE. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence.
-Qed.
-
-Lemma ssem_internal_exclude_sabort ge sp st rs m is:
-  sabort ge sp st rs m ->
-  ssem_internal ge sp st rs m is -> False.
-Proof.
-  intros ABORT SEM.
-  unfold ssem_internal in SEM. destruct icontinue.
-  - destruct SEM as (SEM1 & SEM2 & SEM3).
-    eapply ssem_local_exclude_sabort; eauto.
-  - destruct SEM as (ext & lx & SEM1 & SEM2). eapply ssem_exit_exclude_sabort; eauto.
-Qed.
-
-Definition istate_eq_opt ist1 oist :=
-  exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2.
-
-Lemma ssem_internal_opt_determ ge sp st rs m ois is:
-  ssem_internal_opt ge sp st rs m ois ->
-  ssem_internal ge sp st rs m is ->
-  istate_eq_opt is ois.
-Proof.
-  destruct ois as [is1|]; simpl; eauto.
-  - intros; eexists; intuition; eapply ssem_internal_determ; eauto.
-  - intros; exploit ssem_internal_exclude_sabort; eauto. destruct 1.
-Qed.
-
-(** * Symbolic execution of one internal step *)
-
-Definition slocal_set_sreg (st:sistate_local) (r:reg) (sv:sval) :=
-  {| si_pre:=(fun ge sp rs m => eval_sval ge sp (st.(si_sreg) r) rs m <> None /\ (st.(si_pre) ge sp rs m));
-     si_sreg:=fun y => if Pos.eq_dec r y then sv else st.(si_sreg) y;
-     si_smem:= st.(si_smem)|}.
-
-Definition slocal_set_smem (st:sistate_local) (sm:smem) :=
-  {| si_pre:=(fun ge sp rs m => eval_smem ge sp st.(si_smem) rs m <> None /\ (st.(si_pre) ge sp rs m));
-     si_sreg:= st.(si_sreg);
-     si_smem:= sm |}.
-
-Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): sistate :=
-   {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.
-
-Definition slocal_store st chunk addr args src : sistate_local :=
-   let args := list_sval_inj (List.map (si_sreg st) args) in
-   let src := si_sreg st src in
-   let sm := Sstore (si_smem st) chunk addr args src
-   in slocal_set_smem st sm.
-
-Definition siexec_inst (i: instruction) (st: sistate): option sistate := 
-  match i with
-  | Inop pc' => 
-      Some (sist_set_local st pc' st.(si_local))
-  | Iop op args dst pc' =>
-      let prev := st.(si_local) in
-      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
-      let next := slocal_set_sreg prev dst (Sop op vargs prev.(si_smem)) in
-      Some (sist_set_local st pc' next)
-  | Iload trap chunk addr args dst pc' =>
-      let prev := st.(si_local) in
-      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
-      let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in
-      Some (sist_set_local st pc' next)
-  | Istore chunk addr args src pc' =>
-      let next := slocal_store st.(si_local) chunk addr args src in
-      Some (sist_set_local st pc' next)
-   | Icond cond args ifso ifnot _ =>
-      let prev := st.(si_local) in
-      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
-      let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in
-      Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |}
-  | _ => None
-  end.
-
-Lemma slocal_set_sreg_preserves_sabort_local ge sp st rs0 m0 r sv:
-  sabort_local ge sp st rs0 m0 ->
-  sabort_local ge sp (slocal_set_sreg st r sv) rs0 m0.
-Proof.
-  unfold sabort_local. simpl; intuition.
-  destruct H as [r1 H]. destruct (Pos.eq_dec r r1) as [TEST|TEST] eqn: HTEST.
-  - subst; rewrite H; intuition.
-  - right. right. exists r1. rewrite HTEST. auto.
-Qed.
-
-Lemma slocal_set_smem_preserves_sabort_local ge sp st rs0 m0 m:
-  sabort_local ge sp st rs0 m0 ->
-  sabort_local ge sp (slocal_set_smem st m) rs0 m0.
-Proof.
-  unfold sabort_local. simpl; intuition.
-Qed.
-
-Lemma all_fallthrough_upto_exit_cons ge sp ext lx ext' exits rs m:
-  all_fallthrough_upto_exit ge sp ext lx exits rs m ->
-  all_fallthrough_upto_exit ge sp ext lx (ext'::exits) rs m.
-Proof.
-  intros. inv H. econstructor; eauto.
-Qed.
-
-Lemma all_fallthrough_cons ge sp exits rs m ext:
-  all_fallthrough ge sp exits rs m ->
-  seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false ->
-  all_fallthrough ge sp (ext::exits) rs m.
-Proof.
-  intros. unfold all_fallthrough in *. intros.
-  inv H1; eauto.
-Qed.
-
-Lemma siexec_inst_preserves_sabort i ge sp rs m st st': 
-  siexec_inst i st = Some st' ->
-  sabort ge sp st rs m -> sabort ge sp st' rs m.
-Proof.
-  intros SISTEP ABORT.
-  destruct i; simpl in SISTEP; try discriminate; inv SISTEP; unfold sabort; simpl.
-  (* NOP *)
-  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
-    - left. constructor; eauto.
-    - right. exists ext0, lx0. constructor; eauto.
-  (* OP *)
-  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
-    - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto.
-    - right. exists ext0, lx0. constructor; eauto.
-  (* LOAD *)
-  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
-    - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto.
-    - right. exists ext0, lx0. constructor; eauto.
-  (* STORE *)
-  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
-    - left. constructor; eauto. eapply slocal_set_smem_preserves_sabort_local; eauto.
-    - right. exists ext0, lx0. constructor; eauto.
-  (* COND *)
-  * remember ({| si_cond := _; si_scondargs := _; si_elocal := _; si_ifso := _ |}) as ext.
-    destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
-    - destruct (seval_condition ge sp (si_cond ext) (si_scondargs ext)
-        (si_smem (si_elocal ext)) rs m) eqn:SEVAL; [destruct b|].
-      (* case true *)
-      + right. exists ext, (si_exits st).
-        constructor.
-        ++ constructor. econstructor; eauto. eauto.
-        ++ unfold sabort_exit. right. constructor; eauto.
-           subst. simpl. eauto.
-      (* case false *)
-      + left. constructor; eauto. eapply all_fallthrough_cons; eauto.
-      (* case None *)
-      + right. exists ext, (si_exits st). constructor.
-        ++ constructor. econstructor; eauto. eauto.
-        ++ unfold sabort_exit. left. eauto.
-    - right. exists ext0, lx0. constructor; eauto. eapply all_fallthrough_upto_exit_cons; eauto.
-Qed.
-
-Lemma siexec_inst_WF i st:
-  siexec_inst i st = None -> default_succ i = None.
-Proof.
-  destruct i; simpl; unfold sist_set_local; simpl; congruence.
-Qed.
-
-Lemma siexec_inst_default_succ i st st':
-  siexec_inst i st = Some st' -> default_succ i = Some (st'.(si_pc)).
-Proof.
-  destruct i; simpl; unfold sist_set_local; simpl; try congruence;
-  intro H; inversion_clear H; simpl; auto.
-Qed.
-
-
-Lemma eval_list_sval_inj_not_none ge sp st rs0 m0: forall l,
-  (forall r, List.In r l -> eval_sval ge sp (si_sreg st r) rs0 m0 = None -> False) ->
-  eval_list_sval ge sp (list_sval_inj (map (si_sreg st) l)) rs0 m0 = None -> False.
-Proof.
-  induction l.
-  - intuition discriminate.
-  - intros ALLR. simpl.
-    inversion_SOME v.
-    + intro SVAL. inversion_SOME lv; [discriminate|].
-      assert (forall r : reg, In r l -> eval_sval ge sp (si_sreg st r) rs0 m0 = None -> False).
-      { intros r INR. eapply ALLR. right. assumption. }
-      intro SVALLIST. intro. eapply IHl; eauto.
-    + intros. exploit (ALLR a); simpl; eauto.
-Qed.
-
-Lemma siexec_inst_correct ge sp i st rs0 m0 rs m:
-  ssem_local ge sp st.(si_local) rs0 m0 rs m ->
-  all_fallthrough ge sp st.(si_exits) rs0 m0 ->
-  ssem_internal_opt2 ge sp (siexec_inst i st) rs0 m0 (istep ge i sp rs m).
-Proof.
-  intros (PRE & MEM & REG) NYE.
-  destruct i; simpl; auto.
-  + (* Nop *)
-    constructor; [|constructor]; simpl; auto.
-    constructor; auto.
-  + (* Op *)
-    inversion_SOME v; intros OP; simpl.
-    - constructor; [|constructor]; simpl; auto.
-      constructor; simpl; auto.
-      * constructor; auto. congruence.
-      * constructor; auto.
-        intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
-        subst. rewrite Regmap.gss; simpl; auto.
-        erewrite eval_list_sval_inj; simpl; auto.
-        try_simplify_someHyps.
-    - left. constructor; simpl; auto.
-      unfold sabort_local. right. right.
-      simpl. exists r. destruct (Pos.eq_dec r r); try congruence.
-      simpl. erewrite eval_list_sval_inj; simpl; auto.
-      try_simplify_someHyps.
-  + (* LOAD *) 
-    inversion_SOME a0; intro ADD.
-    { inversion_SOME v; intros LOAD; simpl. 
-      - explore_destruct; unfold ssem_internal, ssem_local; simpl; intuition.
-        * unfold ssem_internal. simpl. constructor; [|constructor]; auto.
-          constructor; constructor; simpl; auto. congruence. intro r0.
-          destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
-          subst; rewrite Regmap.gss; simpl.
-          erewrite eval_list_sval_inj; simpl; auto.
-          try_simplify_someHyps.
-        * unfold ssem_internal. simpl. constructor; [|constructor]; auto.
-          constructor; constructor; simpl; auto. congruence. intro r0.
-          destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
-          subst; rewrite Regmap.gss; simpl.
-          inversion_SOME args; intros ARGS.
-          2: { exploit eval_list_sval_inj_not_none; eauto; intuition congruence. }
-          exploit eval_list_sval_inj; eauto. intro ARGS'. erewrite ARGS in ARGS'. inv ARGS'. rewrite ADD.
-          inversion_SOME m2. intro SMEM.
-          assert (m = m2) by congruence. subst. rewrite LOAD. reflexivity.
-      - explore_destruct; unfold sabort, sabort_local; simpl.
-        * unfold sabort. simpl. left. constructor; auto.
-          right. right. exists r. simpl. destruct (Pos.eq_dec r r); try congruence.
-          simpl. erewrite eval_list_sval_inj; simpl; auto.
-          rewrite ADD; simpl; auto. try_simplify_eval_svalsomeHyps.
-        * unfold ssem_internal. simpl. constructor; [|constructor]; auto.
-          constructor; constructor; simpl; auto. congruence. intro r0.
-          destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
-          subst; rewrite Regmap.gss; simpl.
-          erewrite eval_list_sval_inj; simpl; auto.
-          try_simplify_someHyps.
-     } { rewrite ADD. destruct t.
-          - simpl. left; eauto. simpl. econstructor; eauto.
-            right. right. simpl. exists r. destruct (Pos.eq_dec r r); [|contradiction].
-            simpl. inversion_SOME args. intro SLS.
-            eapply eval_list_sval_inj in REG. rewrite REG in SLS. inv SLS.
-            rewrite ADD. reflexivity.
-          - simpl. constructor; [|constructor]; simpl; auto.
-            constructor; simpl; constructor; auto; [congruence|].
-            intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
-            subst. simpl. rewrite Regmap.gss.
-            erewrite eval_list_sval_inj; simpl; auto.
-            try_simplify_someHyps.
-     }
-  + (* STORE *)
-    inversion_SOME a0; intros ADD.
-    { inversion_SOME m'; intros STORE; simpl.
-      - unfold ssem_internal, ssem_local; simpl; intuition.
-        * congruence.
-        * erewrite eval_list_sval_inj; simpl; auto.
-          erewrite REG.
-          try_simplify_someHyps.
-      - unfold sabort, sabort_local; simpl.
-        left. constructor; auto. right. left.
-        erewrite eval_list_sval_inj; simpl; auto.
-        erewrite REG.
-        try_simplify_someHyps. }
-    { unfold sabort, sabort_local; simpl.
-      left. constructor; auto. right. left.eval_sval
-      erewrite eval_list_sval_inj; simpl; auto.
-      erewrite ADD; simpl; auto. }
-  + (* COND *)
-    Local Hint Resolve is_tail_refl: core.
-    Local Hint Unfold ssem_local: core.
-    inversion_SOME b; intros COND.
-    { destruct b; simpl; unfold ssem_internal, ssem_local; simpl.
-      - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st).
-        constructor; constructor; subst; simpl; auto.
-        unfold seval_condition. subst; simpl.
-        erewrite eval_list_sval_inj; simpl; auto.
-        try_simplify_someHyps.
-      - intuition. unfold all_fallthrough in * |- *. simpl.
-        intuition. subst. simpl.
-        unfold seval_condition.
-        erewrite eval_list_sval_inj; simpl; auto.
-        try_simplify_someHyps. }
-    { unfold sabort. simpl. right.
-      remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st).
-      constructor; [constructor; subst; simpl; auto|].
-      left. subst; simpl; auto.
-      unfold seval_condition.
-      erewrite eval_list_sval_inj; simpl; auto.
-      try_simplify_someHyps. }
-Qed.
-
-
-Lemma siexec_inst_correct_None ge sp i st rs0 m0 rs m:
-  ssem_local ge sp (st.(si_local)) rs0 m0 rs m ->
-  siexec_inst i st = None -> 
-  istep ge i sp rs m = None.
-Proof.
-  intros (PRE & MEM & REG).
-  destruct i; simpl; unfold sist_set_local, ssem_internal, ssem_local; simpl; try_simplify_someHyps.
-Qed.
-
-(** * Symbolic execution of the internal steps of a path *)
-Fixpoint siexec_path (path:nat) (f: function) (st: sistate): option sistate :=
-  match path with
-  | O => Some st
-  | S p =>
-    SOME i <- (fn_code f)!(st.(si_pc)) IN
-    SOME st1 <- siexec_inst i st IN
-    siexec_path p f st1
-  end.
-
-Lemma siexec_inst_add_exits i st st':
-  siexec_inst i st = Some st' ->
-  ( si_exits st' = si_exits st \/ exists ext, si_exits st' = ext :: si_exits st ).
-Proof.
-  destruct i; simpl; intro SISTEP; inversion_clear SISTEP; unfold siexec_inst; simpl; (discriminate || eauto).
-Qed.
-
-Lemma siexec_inst_preserves_allfu ge sp ext lx rs0 m0 st st' i:
-  all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs0 m0 ->
-  siexec_inst i st = Some st' ->
-  all_fallthrough_upto_exit ge sp ext lx (si_exits st') rs0 m0.
-Proof.
-  intros ALLFU SISTEP. destruct ALLFU as (ISTAIL & ALLF).
-  constructor; eauto.
-  destruct i; simpl in SISTEP; inversion_clear SISTEP; simpl; (discriminate || eauto).
-Qed.
-
-Lemma siexec_path_correct_false ge sp f rs0 m0 st' is:
-  forall path,
-  is.(icontinue)=false ->
-  forall st, ssem_internal ge sp st rs0 m0 is ->
-  siexec_path path f st = Some st' ->
-  ssem_internal ge sp st' rs0 m0 is.
-Proof.
-  induction path; simpl.
-  - intros. congruence.
-  - intros ICF st SSEM STEQ'.
-    destruct ((fn_code f) ! (si_pc st)) eqn:FIC; [|discriminate].
-    destruct (siexec_inst _ _) eqn:SISTEP; [|discriminate].
-    eapply IHpath. 3: eapply STEQ'. eauto.
-    unfold ssem_internal in SSEM. rewrite ICF in SSEM.
-    destruct SSEM as (ext & lx & SEXIT & ALLFU).
-    unfold ssem_internal. rewrite ICF. exists ext, lx.
-    constructor; auto. eapply siexec_inst_preserves_allfu; eauto.
-Qed.
-
-Lemma siexec_path_preserves_sabort ge sp path f rs0 m0 st': forall st, 
-  siexec_path path f st = Some st' ->
-  sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0.
-Proof.
-  Local Hint Resolve siexec_inst_preserves_sabort: core.
-  induction path; simpl.
-  + unfold sist_set_local; try_simplify_someHyps.
-  + intros st; inversion_SOME i.
-    inversion_SOME st1; eauto.
-Qed.
-
-Lemma siexec_path_WF path f: forall st,
-  siexec_path path f st = None -> nth_default_succ (fn_code f) path st.(si_pc) = None.
-Proof.
-  induction path; simpl.
-  + unfold sist_set_local. intuition congruence.
-  + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try tauto.
-    destruct (siexec_inst i st) as [st1|] eqn: Hst1; simpl.
-    - intros; erewrite siexec_inst_default_succ; eauto.
-    - intros; erewrite siexec_inst_WF; eauto.
-Qed.
-
-Lemma siexec_path_default_succ path f st': forall st,
-  siexec_path path f st = Some st' -> nth_default_succ (fn_code f) path st.(si_pc) = Some st'.(si_pc).
-Proof.
-  induction path; simpl.
-  + unfold sist_set_local. intros st H. inversion_clear H; simpl; try congruence.
-  + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try congruence.
-    destruct (siexec_inst i st) as [st1|] eqn: Hst1; simpl; try congruence.
-    intros; erewrite siexec_inst_default_succ; eauto.
-Qed.
-
-Lemma siexec_path_correct_true ge sp path (f:function) rs0 m0: forall st is,
-  is.(icontinue)=true ->
-  ssem_internal ge sp st rs0 m0 is -> 
-  nth_default_succ (fn_code f) path st.(si_pc) <> None ->
-  ssem_internal_opt2 ge sp (siexec_path path f st) rs0 m0
-                         (isteps ge path f sp is.(irs) is.(imem) is.(ipc))
-  .
-Proof.
-  Local Hint Resolve siexec_path_correct_false siexec_path_preserves_sabort siexec_path_WF: core.
-  induction path; simpl.
-  + intros st is CONT INV WF;
-    unfold ssem_internal, sist_set_local in * |- *;
-    try_simplify_someHyps. simpl.
-    destruct is; simpl in * |- *; subst; intuition auto.
-  + intros st is CONT; unfold ssem_internal at 1; rewrite CONT.
-    intros (LOCAL & PC & NYE) WF.
-    rewrite <- PC.
-    inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto.
-    exploit siexec_inst_correct; eauto. 
-    inversion_SOME st1; intros Hst1; erewrite Hst1; simpl.
-    - inversion_SOME is1; intros His1;rewrite His1; simpl. 
-      * destruct (icontinue is1) eqn:CONT1.
-        (* icontinue is0 = true *)
-        intros; eapply IHpath; eauto.
-        destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps.
-        (* icontinue is0 = false -> EARLY EXIT *)
-        destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto.
-        destruct WF. erewrite siexec_inst_default_succ; eauto.
-        (* try_simplify_someHyps; eauto. *)
-      * destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto.
-    - intros His1;rewrite His1; simpl; auto.
-Qed.
-
-(** REM: in the following two unused lemmas *)
-
-Lemma siexec_path_right_assoc_decompose f path: forall st st',
-  siexec_path (S path) f st = Some st' ->
-  exists st0, siexec_path path f st = Some st0 /\ siexec_path 1%nat f st0 = Some st'.
-Proof.
-  induction path; simpl; eauto.
-  intros st st'.
-  inversion_SOME i1.
-  inversion_SOME st1.
-  try_simplify_someHyps; eauto.
-Qed.
-
-Lemma siexec_path_right_assoc_compose f path: forall st st0 st',
-  siexec_path path f st = Some st0 ->
-  siexec_path 1%nat f st0 = Some st' ->
-  siexec_path (S path) f st = Some st'.
-Proof.
-  induction path.
-  + intros st st0 st' H. simpl in H.
-    try_simplify_someHyps; auto.
-  + intros st st0 st'.
-    assert (X:exists x, x=(S path)); eauto.
-    destruct X as [x X]. 
-    intros H1 H2. rewrite <- X.
-    generalize H1; clear H1. simpl.
-    inversion_SOME i1. intros Hi1; rewrite Hi1.
-    inversion_SOME st1. intros Hst1; rewrite Hst1.
-    subst; eauto.
-Qed.
-
-
-(** * Main function of the symbolic execution *)
-
-Definition init_sistate_local := {| si_pre:= fun _ _ _ _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.
-
-Definition init_sistate pc := {| si_pc:= pc; si_exits:=nil; si_local:= init_sistate_local |}.
-
-Lemma init_ssem_internal ge sp pc rs m: ssem_internal ge sp (init_sistate pc) rs m (mk_istate true pc rs m).
-Proof.
-  unfold ssem_internal, ssem_local, all_fallthrough; simpl. intuition.
-Qed.
-
-Definition sexec (f: function) (pc:node): option sstate :=
-  SOME path <- (fn_path f)!pc IN
-  SOME st <- siexec_path path.(psize) f (init_sistate pc) IN
-  SOME i <- (fn_code f)!(st.(si_pc)) IN
-  Some (match siexec_inst i st with
-       | Some st' => {| internal := st'; final := Snone |}
-       | None => {| internal := st; final := sexec_final i st.(si_local) |}
-       end).
-
-Lemma final_node_path_simpl f path pc:
-   (fn_path f)!pc = Some path -> nth_default_succ_inst (fn_code f) path.(psize) pc <> None. 
-Proof.
-  intros; exploit final_node_path; eauto.
-  intros (i & NTH & DUM).
-  congruence.
-Qed.
-
-Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: 
-  (fn_code f) ! pc = Some i ->
-  pc = st.(si_pc) ->
-  siexec_inst i st = Some st' ->
-  path_last_step ge pge stack f sp pc rs m t s ->
-  exists mk_istate, 
-     istep ge i sp rs m = Some mk_istate 
-  /\ t = E0 
-  /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)).
-Proof.
-  intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl.
-Qed.
-
-(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
-(sexec is a correct over-approximation)
-*)
-Theorem sexec_correct f pc pge ge sp path stack rs m t s: 
-  (fn_path f)!pc = Some path ->
-  path_step ge pge path.(psize) stack f sp rs m pc t s ->
-  exists st, sexec f pc = Some st /\ ssem pge ge sp st stack f rs m t s.
-Proof.
-  Local Hint Resolve init_ssem_internal: core.
-  intros PATH STEP; unfold sexec; rewrite PATH; simpl.
-  lapply (final_node_path_simpl f path pc); eauto. intro WF.
-  exploit (siexec_path_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto.
-  { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. }
-  (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]).
-  destruct STEP as [sti STEPS CONT|sti t s STEPS CONT LAST];
-  (* intro Hst *)
-  (rewrite STEPS; unfold ssem_internal_opt2; destruct (siexec_path _ _ _) as [st|] eqn: Hst; try congruence);
-  (* intro SEM *)
-  (simpl; unfold ssem_internal; simpl; rewrite CONT; intro SEM);
-  (* intro Hi' *)
-  ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); 
-    [ unfold nth_default_succ_inst in Hi; 
-      exploit siexec_path_default_succ; eauto; simpl;
-      intros DEF; rewrite DEF in Hi; auto 
-      | clear Hi; rewrite Hi' ]);
-  (* eexists *)
-  (eexists; constructor; eauto).
-  - (* early *)
-    eapply ssem_early; eauto.
-    unfold ssem_internal; simpl; rewrite CONT.
-    destruct (siexec_inst i st) as [st'|] eqn: Hst'; simpl; eauto.
-    destruct SEM as (ext & lx & SEM & ALLFU). exists ext, lx.
-    constructor; auto. eapply siexec_inst_preserves_allfu; eauto.
-  - destruct SEM as (SEM & PC & HNYE).
-    destruct (siexec_inst i st) as [st'|] eqn: Hst'; simpl.
-    + (* normal on Snone *)
-      rewrite <- PC in LAST.
-      exploit symb_path_last_step; eauto; simpl.
-      intros (mk_istate & ISTEP & Ht & Hs); subst.
-      exploit siexec_inst_correct; eauto. simpl.
-      erewrite Hst', ISTEP; simpl.
-      clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i.
-      intro SEM; destruct (mk_istate.(icontinue)) eqn: CONT.
-      { (* icontinue mk_istate = true *)
-        eapply ssem_normal; simpl; eauto.
-        unfold ssem_internal in SEM.
-        rewrite CONT in SEM.eval_sval
-        destruct SEM as (SEM & PC & HNYE).
-        rewrite <- PC.
-        eapply exec_Snone. }
-      { eapply ssem_early; eauto. }
-    + (* normal non-Snone instruction *) 
-      eapply ssem_normal; eauto.
-      * unfold ssem_internal; simpl; rewrite CONT; intuition.
-      * simpl. eapply sexec_final_correct; eauto.
-        rewrite PC; auto.
-Qed.
-
-(* TODO: déplacer les trucs sur equiv_stackframe dans RTLpath ? *)
-Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
-  | equiv_stackframe_intro res f sp pc rs1 rs2
-      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
-      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2).
-
-Inductive equiv_state: state -> state -> Prop :=
-  | State_equiv stack f sp pc rs1 m rs2
-     (EQUIV: forall r, rs1#r = rs2#r): 
-     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
-  | Call_equiv stk stk' f args m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
-  | Return_equiv stk stk' v m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Returnstate stk v m) (Returnstate stk' v m).
-
-Lemma equiv_stackframe_refl stf: equiv_stackframeeval_sval stf stf.
-Proof.
-  destruct stf. constructor; auto.
-Qed.
-
-Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
-Proof.
-  Local Hint Resolve equiv_stackframe_refl: core.
-  induction stk; simpl; constructor; auto.
-Qed.eval_sval
-
-Lemma equiv_state_refl s: equiv_state s s.
-Proof.
-  Local Hint Resolve equiv_stack_refl: core.
-  induction s; simpl; constructor; auto.
-Qed.
-
-(*
-Lemma equiv_stackframe_trans stf1 stf2 stf3:
-  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
-Proof.
-  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
-  intros; eapply eq_trans; eauto.
-Qed.
-
-Lemma equiv_stack_trans stk1 stk2:
-  list_forall2 equiv_stackframe stk1 stk2 -> 
-  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
-  list_forall2 equiv_stackframe stk1 stk3.
-Proof.
-  Local Hint Resolve equiv_stackframe_trans.
-  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
-Qed.
-
-Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
-Proof.
-  Local Hint Resolve equiv_stack_trans.
-  destruct 1; intros EQ; inv EQ; econstructor; eauto.
-  intros; eapply eq_trans; eauto.
-Qed.
-*)
-
-Lemma regmap_setres_eq (rs rs': regset) res vres:
-  (forall r, rs # r = rs' # r) ->
-  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
-Proof.
-  intros RSEQ r. destruct res; simpl; try congruence.
-  destruct (peq x r).
-  - subst. repeat (rewrite Regmap.gss). reflexivity.
-  - repeat (rewrite Regmap.gso); auto.
-Qed.
-
-Lemma sem_sfval_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s:
-  sem_sfval pge ge sp st stack f rs0 m0 sv rs1 m t s ->
-  (forall r, rs1#r = rs2#r) -> 
-  exists s', equiv_state s s' /\ sem_sfval pge ge sp st stack f rs0 m0 sv rs2 m t s'.
-Proof. eval_sval
-  Local Hint Resolve equiv_stack_refl: core.
-  destruct 1.
-  - (* Snone *) intros; eexists; econstructor.
-    + eapply State_equiv; eauto.
-    + eapply exec_Snone.
-  - (* Scall *)
-    intros; eexists; econstructor.
-    2: { eapply exec_Scall; eauto. }
-    apply Call_equiv; auto.
-    repeat (constructor; auto).
-  - (* Stailcall *)
-    intros; eexists; econstructor; [| eapply exec_Stailcall; eauto].
-    apply Call_equiv; auto.
-  - (* Sbuiltin *)
-    intros; eexists; econstructor; [| eapply exec_Sbuiltin; eauto].
-    constructor. eapply regmap_setres_eq; eauto.
-  - (* Sjumptable *)
-    intros; eexists; econstructor; [| eapply exec_Sjumptable; eauto].
-    constructor. assumption.
-  - (* Sreturn *)
-    intros; eexists; econstructor; [| eapply exec_Sreturn; eauto].
-    eapply equiv_state_refl; eauto.
-Qed.
-
-Lemma siexec_inst_early_exit_absurd i st st' ge sp rs m rs' m' pc':
-  siexec_inst i st = Some st' ->
-  (exists ext lx, ssem_exit ge sp ext rs m rs' m' pc' /\
-     all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m) ->
-  all_fallthrough ge sp (si_exits st') rs m ->
-  False.
-Proof.
-  intros SIEXEC (ext & lx & SSEME & ALLFU) ALLF. destruct ALLFU as (TAIL & _).
-  exploit siexec_inst_add_exits; eauto. destruct 1 as [SIEQ | (ext0 & SIEQ)].
-  - rewrite SIEQ in *. eapply all_fallthrough_noexit. eauto. 2: eapply ALLF. eapply is_tail_in. eassumption.
-  - rewrite SIEQ in *. eapply all_fallthrough_noexit. eauto. 2: eapply ALLF. eapply is_tail_in.
-    constructor. eassumption.
-Qed.
-eval_sval
-Lemma is_tail_false {A: Type}: forall (l: list A) a, is_tail (a::l) nil -> False.
-Proof.
-  intros. eapply is_tail_incl in H. unfold incl in H. pose (H a).
-  assert (In a (a::l)) by (constructor; auto). assert (In a nil) by auto. apply in_nil in H1.
-  contradiction.
-Qed.
-
-Lemma cons_eq_false {A: Type}: forall (l: list A) a,
-  a :: l = l -> False.
-Proof.
-  induction l; intros.
-  - discriminate.
-  - inv H. apply IHl in H2. contradiction.
-Qed.
-
-Lemma app_cons_nil_eq {A: Type}: forall l' l (a:A),
-  (l' ++ a :: nil) ++ l = l' ++ a::l.
-Proof.
-  induction l'; intros.
-  - simpl. reflexivity.
-  - simpl. rewrite IHl'. reflexivity. 
-Qed.
-
-Lemma app_eq_false {A: Type}: forall l (l': list A) a,
-  l' ++ a :: l = l -> False.
-Proof.
-  induction l; intros.
-  - apply app_eq_nil in H. destruct H as (_ & H). apply cons_eq_false in H. contradiction.
-  - destruct l' as [|a' l'].
-    + simpl in H. apply cons_eq_false in H. contradiction.
-    + rewrite <- app_comm_cons in H. inv H.
-      apply (IHl (l' ++ (a0 :: nil)) a). rewrite app_cons_nil_eq. assumption.
-Qed.
-
-Lemma is_tail_false_gen {A: Type}: forall (l: list A) l' a, is_tail (l'++(a::l)) l -> False.
-Proof.
-  induction l.
-  - intros. destruct l' as [|a' l'].
-    + simpl in H. apply is_tail_false in H. contradiction.
-    + rewrite <- app_comm_cons in H. apply is_tail_false in H. contradiction.
-  - intros. inv H.
-    + apply app_eq_false in H2. contradiction.
-    + apply (IHl (l' ++ (a0 :: nil)) a). rewrite app_cons_nil_eq. assumption.
-Qed.
-
-Lemma is_tail_eq {A: Type}: forall (l l': list A),
-  is_tail l' l ->
-  is_tail l l' ->
-  l = l'.
-Proof.
-  destruct l as [|a l]; intros l' ITAIL ITAIL'.
-  - destruct l' as [|i' l']; auto. apply is_tail_false in ITAIL. contradiction.
-  - inv ITAIL; auto.
-    destruct l' as [|i' l']. { apply is_tail_false in ITAIL'. contradiction. }
-    exploit is_tail_trans. eapply ITAIL'. eauto. intro ABSURD.
-    apply (is_tail_false_gen l nil a) in ABSURD. contradiction.
-Qed.
-
-(* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution
-  (sexec is exact).
-*)
-Theorem sexec_exact f pc pge ge sp path stack st rs m t s1: 
-  (fn_path f)!pc = Some path ->
-  sexec f pc = Some st -> 
-  ssem pge ge sp st stack f rs m t s1 ->
-  exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ 
-             equiv_state s1 s2.
-Proof.
-  Local Hint Resolve init_ssem_internal: core.
-  unfold sexec; intros PATH SSTEP SEM; rewrite PATH in SSTEP.
-  lapply (final_node_path_simpl f path pc); eauto. intro WF.
-  exploit (siexec_path_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto.
-  { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. }
-  (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]).
-  unfold nth_default_succ_inst in Hi.
-  destruct (siexec_path path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl.
-  2:{ (* absurd case *)
-      exploit siexec_path_WF; eauto.
-      simpl; intros NDS; rewrite NDS in Hi; congruence. }
-  exploit siexec_path_default_succ;eval_sval eauto; simpl.
-  intros NDS; rewrite NDS in Hi.
-  rewrite Hi in SSTEP.
-  intros ISTEPS. try_simplify_someHyps.
-  destruct (siexec_inst i st0) as [st'|] eqn:Hst'; simpl.
-  + (* exit on Snone instruction *)
-    assert (SEM': t = E0 /\ exists is, ssem_internal ge sp st' rs m is
-           /\ s1 = (State stack f sp (if (icontinue is) then (si_pc st') else (ipc is)) (irs is) (imem is))).
-    {  destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *.
-       - repeat (econstructor; eauto).
-         rewrite CONT; eauto.
-       - inversion SEM2. repeat (econstructor; eauto).
-         rewrite CONT; eauto. }
-    clear SEM; subst. destruct SEM' as [X (is & SEM & X')]; subst.
-    intros.
-    destruct (isteps ge (psize path) f sp rs m pc) as [is0|] eqn:RISTEPS; simpl in *.
-    * unfold ssem_internal in ISTEPS. destruct (icontinue is0) eqn: ICONT0. 
-      ** (* icontinue is0=true: path_step by normal_exit *)
-         destruct ISTEPS as (SEMis0&H1&H2).
-         rewrite H1 in * |-.
-         exploit siexec_inst_correct; eauto.
-         rewrite Hst'; simpl.
-         intros; exploit ssem_internal_opt_determ; eauto.
-         destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
-         eexists. econstructor 1.
-         *** eapply exec_normal_exit; eauto.
-             eapply exec_istate; eauto.
-         *** rewrite EQ1.
-             enough ((ipc st) = (if icontinue st then si_pc st' else ipc is)) as ->.
-             { rewrite EQ2, EQ4. eapply State_equiv; auto. }
-             destruct (icontinue st) eqn:ICONT; auto.
-             exploit siexec_inst_default_succ; eauto.
-             erewrite istep_normal_exit; eauto.
-             try_simplify_someHyps.
-      ** (* The concrete execution has not reached "i" => early exit *) 
-         unfold ssem_internal in SEM.
-         destruct (icontinue is) eqn:ICONT.
-         { destruct SEM as (SEML & SIPC & ALLF).
-           exploit siexec_inst_early_exit_absurd; eauto. contradiction. }
-         
-         eexists. econstructor 1.
-         *** eapply exec_early_exit; eauto.
-         *** destruct ISTEPS as (ext & lx & SSEME & ALLFU). destruct SEM as (ext' & lx' & SSEME' & ALLFU').
-             eapply siexec_inst_preserves_allfu in ALLFU; eauto.
-             exploit ssem_exit_fallthrough_upto_exit; eauto.
-             exploit ssem_exit_fallthrough_upto_exit. eapply SSEME. eapply ALLFU. eapply ALLFU'.
-             intros ITAIL ITAIL'. apply is_tail_eq in ITAIL; auto. clear ITAIL'.
-             inv ITAIL. exploit ssem_exit_determ. eapply SSEME. eapply SSEME'. intros (IPCEQ & IRSEQ & IMEMEQ).
-             rewrite <- IPCEQ. rewrite <- IMEMEQ. constructor. congruence. 
-    * (* The concrete execution has not reached "i" => abort case *)
-      eapply siexec_inst_preserves_sabort in ISTEPS; eauto.
-      exploit ssem_internal_exclude_sabort; eauto. contradiction.
-  + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *.
-    - (* early exit *)
-      intros.
-      exploit ssem_internal_opt_determ; eauto.
-      destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
-      eexists. econstructor 1.
-      * eapply exec_early_exit; eauto.
-      * rewrite EQ2, EQ4; eapply State_equiv. auto.
-    - (* normal exit non-Snone instruction *)
-      intros.
-      exploit ssem_internal_opt_determ; eauto.
-      destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
-      unfold ssem_internal in SEM1.
-      rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0).
-      exploit sem_sfval_equiv; eauto.
-      clear SEM2; destruct 1 as (s' & Ms' & SEM2).
-      rewrite ! EQ4 in * |-; clear EQ4.
-      rewrite ! EQ2 in * |-; clear EQ2.
-      exists s'; intuition.
-      eapply exec_normal_exit; eauto.
-      eapply sexec_final_complete; eauto.
-      * congruence.
-      * unfold ssem_local in * |- *. 
-        destruct SEM1 as (A & B & C). constructor; [|constructor]; eauto.
-        intro r. congruence.
-      * congruence.
-Qed.
-
-Require Import RTLpathLivegen RTLpathLivegenproof.
-
-(** * DEFINITION OF SIMULATION BETWEEN (ABSTRACT) SYMBOLIC EXECUTIONS
-*)
-
-Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop :=
-     is1.(icontinue) = is2.(icontinue)
-     /\ eqlive_reg alive is1.(irs) is2.(irs)
-     /\ is1.(imem) = is2.(imem).
-
-Definition istate_simu f (srce: PTree.t node) outframe is1 is2: Prop :=
-  if is1.(icontinue) then
-     istate_simulive (fun r => Regset.In r outframe) srce is1 is2
-  else
-     exists path, f.(fn_path)!(is1.(ipc)) = Some path 
-     /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
-     /\ srce!(is2.(ipc)) = Some is1.(ipc).
-
-Record simu_proof_context {f1: RTLpath.function} := {
-   liveness_hyps: liveness_ok_function f1;
-   the_ge1: RTL.genv;
-   the_ge2: RTL.genv;
-   genv_match: forall s, Genv.find_symbol the_ge1 s = Genv.find_symbol the_ge2 s;
-   the_sp: val;
-   the_rs0: regset; 
-   the_m0: mem
-}.
-Arguments simu_proof_context: clear implicits.
-
-(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *)
-Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
-  forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 ->
-  exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2
-              /\ istate_simu f dm outframe is1 is2.
-
-Inductive svident_simu (f: RTLpath.function) (ctx: simu_proof_context f): (sval + ident) -> (sval + ident) -> Prop :=
-  | Sleft_simu sv1 sv2:
-     (eval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) = (eval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx))
-     -> svident_simu f ctx (inl sv1) (inl sv2)
-  | Sright_simu id1 id2:
-     id1 = id2
-     -> svident_simu f ctx (inr id1) (inr id2)
+(* symbolic state *)
+Inductive sstate :=
+  | Sfinal (sis: sistate) (sfv: sfval)
+  | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
+ .
+
+Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop :=
+  | sem_Sfinal sis sfv
+     (SIS: sem_sistate ctx sis rs m)
+     (SFV: sem_sfval ctx sfv rs m t s)
+     : sem_internal_sstate ctx rs m t s (Sfinal sis sfv)
+  | sem_Scond b cond args sm ifso ifnot
+     (SEVAL: seval_condition ctx cond args sm = Some b)
+     (SELECT: sem_internal_sstate ctx rs m t s (if b then ifso else ifnot))
+     : sem_internal_sstate ctx rs m t s (Scond cond args sm ifso ifnot)
   .
-
-
-Fixpoint ptree_get_list (pt: PTree.t node) (lp: list positive) : option (list positive) :=
-  match lp with
-  | nil => Some nil
-  | p1::lp => SOME p2 <- pt!p1 IN
-              SOME lp2 <- (ptree_get_list pt lp) IN
-              Some (p2 :: lp2)
-  end.
-
-Lemma ptree_get_list_nth dm p2: forall lp2 lp1,
-  ptree_get_list dm lp2 = Some lp1 ->
-  forall n, list_nth_z lp2 n = Some p2 ->
-  exists p1,
-    list_nth_z lp1 n = Some p1 /\ dm ! p2 = Some p1.
-Proof.
-  induction lp2.
-  - simpl. intros. inv H. simpl in *. discriminate.
-  - intros lp1 PGL n LNZ. simpl in PGL. explore.
-    inv LNZ. destruct (zeq n 0) eqn:ZEQ.
-    + subst. inv H0. exists n0. simpl; constructor; auto.
-    + exploit IHlp2; eauto. intros (p1 & LNZ & DMEQ).
-      eexists. simpl. rewrite ZEQ.
-      constructor; eauto.
-Qed.
-
-Lemma ptree_get_list_nth_rev dm p1: forall lp2 lp1,
-  ptree_get_list dm lp2 = Some lp1 ->
-  forall n, list_nth_z lp1 n = Some p1 ->
-  exists p2,
-    list_nth_z lp2 n = Some p2 /\ dm ! p2 = Some p1.
-Proof.
-  induction lp2.
-  - simpl. intros. inv H. simpl in *. discriminate.
-  - intros lp1 PGL n LNZ. simpl in PGL. explore.
-    inv LNZ. destruct (zeq n 0) eqn:ZEQ.
-    + subst. inv H0. exists a. simpl; constructor; auto.
-    + exploit IHlp2; eauto. intros (p2 & LNZ & DMEQ).
-      eexists. simpl. rewrite ZEQ.
-      constructor; eauto. congruence.
-Qed.
-
-(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *)
-Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop :=
-  | Snone_simu: 
-      dm!opc2 = Some opc1 -> 
-      sfval_simu dm f opc1 opc2 ctx Snone Snone
-  | Scall_simu sig svos1 svos2 lsv1 lsv2 res pc1 pc2:
-      dm!pc2 = Some pc1 ->
-      svident_simu f ctx svos1 svos2 ->
-      (eval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx))
-      = (eval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) ->
-      sfval_simu dm f opc1 opc2 ctx (Scall sig svos1 lsv1 res pc1) (Scall sig svos2 lsv2 res pc2)
-  | Stailcall_simu sig svos1 svos2 lsv1 lsv2:
-      svident_simu f ctx svos1 svos2 ->
-      (eval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx))
-      = (eval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) ->
-      sfval_simu dm f opc1 opc2 ctx (Stailcall sig svos1 lsv1) (Stailcall sig svos2 lsv2)
-  | Sbuiltin_simu ef lbs1 lbs2 br pc1 pc2:
-      dm!pc2 = Some pc1 ->
-      (eval_list_builtin_sval (the_ge1 ctx) (the_sp ctx) lbs1 (the_rs0 ctx) (the_m0 ctx))
-      = (eval_list_builtin_sval (the_ge2 ctx) (the_sp ctx) lbs2 (the_rs0 ctx) (the_m0 ctx)) ->
-      sfval_simu dm f opc1 opc2 ctx (Sbuiltin ef lbs1 br pc1) (Sbuiltin ef lbs2 br pc2)
-  | Sjumptable_simu sv1 sv2 lpc1 lpc2:
-      ptree_get_list dm lpc2 = Some lpc1 ->
-      (eval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx))
-      = (eval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
-      sfval_simu dm f opc1 opc2 ctx (Sjumptable sv1 lpc1) (Sjumptable sv2 lpc2)
-  | Sreturn_simu_none: sfval_simu dm f opc1 opc2 ctx (Sreturn None) (Sreturn None)
-  | Sreturn_simu_some sv1 sv2:
-      (eval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx))
-      = (eval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
-      sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)).
-
-Definition sstate_simu dm f outframe (s1 s2: sstate) (ctx: simu_proof_context f): Prop :=
-       sistate_simu dm f outframe s1.(internal) s2.(internal) ctx
-    /\ forall is1,
-           ssem_internal (the_ge1 ctx) (the_sp ctx) s1 (the_rs0 ctx) (the_m0 ctx) is1 -> 
-           is1.(icontinue) = true ->
-           sfval_simu dm f s1.(si_pc) s2.(si_pc) ctx s1.(final) s2.(final).
-
-Definition sexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop :=
-    forall st1, sexec f1 pc1 = Some st1 -> 
-    exists path st2, (fn_path f1)!pc1 = Some path /\ sexec f2 pc2 = Some st2 
-     /\ forall ctx, sstate_simu dm f1 path.(pre_output_regs) st1 st2 ctx.
-
-*)
\ No newline at end of file