init BTL_SEtheory (by copy/paste from RTLpathSE_theory)

1 files changed, 1831 insertions, 0 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
new file mode 100644
index 00000000..53c00c8b
--- /dev/null
+++ b/scheduling/BTL_SEtheory.v
@@ -0,0 +1,1831 @@
+(* A theory of symbolic execution on BTL
+
+NB: an efficient implementation with hash-consing will be defined in another file (some day)
+
+*)
+
+Require Import Coqlib Maps Floats.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import Op Registers.
+Require Import RTL BTL OptionMonad.
+
+(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *)
+Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
+Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)
+
+(** * Syntax and semantics of symbolic values *)
+
+(* symbolic value *)
+Inductive sval :=
+  | Sinput (r: reg)
+  | Sop (op:operation) (lsv: list_sval)  (sm: smem)
+  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
+with list_sval := 
+  | Snil
+  | Scons (sv: sval) (lsv: list_sval)
+(* symbolic memory *)
+with smem :=
+  | Sinit 
+  | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval).
+
+Scheme sval_mut := Induction for sval Sort Prop
+with list_sval_mut := Induction for list_sval Sort Prop
+with smem_mut := Induction for smem Sort Prop.
+
+Fixpoint list_sval_inj (l: list sval): list_sval :=
+  match l with
+  | nil => Snil
+  | v::l => Scons v (list_sval_inj l)
+  end.
+
+Local Open Scope option_monad_scope.
+
+Fixpoint eval_sval (ge: BTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val :=
+  match sv with
+  | Sinput r => Some (rs0#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
+  | 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
+          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
+          | None => Some (default_notrap_load_value chunk)
+          | Some a =>
+              SOME m <- eval_smem ge sp sm rs0 m0 IN
+              match (Mem.loadv chunk m a) with
+              | None => Some (default_notrap_load_value chunk)
+              | Some val => Some val
+              end
+          end
+      end
+  end
+with eval_list_sval (ge: BTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): 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::lv)
+  end
+with eval_smem (ge: BTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem :=
+  match sm with
+  | Sinit => Some m0
+  | 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
+     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).
+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
+  eval_condition cond args m.
+
+
+(** * Auxiliary definitions on Builtins *)
+(* TODO: clean this. Some generic stuffs could be put in [AST.v] *)
+
+Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)
+
+Variable ge: BTL.genv.
+Variable sp: val.
+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 ->
+      seval_builtin_arg (BA x) v
+  | seval_BA_int: forall n,
+      seval_builtin_arg (BA_int n) (Vint n)
+  | seval_BA_long: forall n,
+      seval_builtin_arg (BA_long n) (Vlong n)
+  | seval_BA_float: forall n,
+      seval_builtin_arg (BA_float n) (Vfloat n)
+  | 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 ->
+      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_BA_loadglobal: forall chunk id ofs v,
+      Mem.loadv chunk m (Senv.symbol_address ge 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_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).
+
+Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop :=
+  list_forall2 seval_builtin_arg al vl.
+
+Lemma seval_builtin_arg_determ:
+  forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v.
+Proof.
+  induction 1; intros v' EV; inv EV; try congruence.
+  f_equal; eauto.
+  apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. 
+Qed.
+
+Lemma eval_builtin_args_determ:
+  forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl.
+Proof.
+  induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ.
+Qed.
+
+End SEVAL_BUILTIN_ARG.
+
+(* NB: generic function that could be put into [AST] file *)
+Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
+  match arg with
+  | BA x => BA (f x)
+  | BA_int n => BA_int n
+  | BA_long n => BA_long n
+  | BA_float f => BA_float f
+  | BA_single s => BA_single s
+  | BA_loadstack chunk ptr => BA_loadstack chunk ptr
+  | BA_addrstack ptr => BA_addrstack ptr
+  | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr
+  | BA_addrglobal id ptr => BA_addrglobal id ptr
+  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2)
+  | 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.
+Proof.
+  induction arg.
+  all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
+  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
+    eapply IHarg1; eauto. eapply IHarg2; eauto.
+  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
+    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.
+Proof.
+  induction 2.
+  - constructor.
+  - simpl. constructor; [| assumption].
+    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.
+Proof.
+  induction arg.
+  all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence).
+  - inv BARG. rewrite SEVAL in H0. inv H0. constructor.
+  - inv BARG. simpl. constructor.
+    eapply IHarg1; eauto. eapply IHarg2; eauto.
+  - inv BARG. simpl. constructor.
+    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.
+Proof.
+  induction args.
+  - simpl. intros. inv H0. constructor.
+  - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
+    constructor; [| eapply IHargs; eauto].
+    eapply seval_builtin_arg_complete; eauto.
+Qed.
+
+Fixpoint seval_builtin_sval ge sp bsv rs0 m0 :=
+  match bsv with
+  | BA sv => SOME v <- eval_sval ge sp sv rs0 m0 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 (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 (BA_addptr v1 v2)
+  | BA_int i => Some (BA_int i)
+  | BA_long l => Some (BA_long l)
+  | BA_float f => Some (BA_float f)
+  | BA_single s => Some (BA_single s)
+  | BA_loadstack chk ptr => Some (BA_loadstack chk ptr)
+  | BA_addrstack ptr => Some (BA_addrstack ptr)
+  | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr)
+  | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
+  end.
+
+Fixpoint eval_list_builtin_sval ge sp lbsv rs0 m0 :=
+  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
+                 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 ->
+  lbs2 = nil.
+Proof.
+  destruct lbs2; simpl; auto.
+  intros. destruct (seval_builtin_sval _ _ _ _ _);
+    try destruct (eval_list_builtin_sval _ _ _ _ _); discriminate.
+Qed.
+
+Lemma seval_builtin_sval_arg ge sp rs0 m0 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.
+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 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.
+     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.
+     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 ->
+  exists ba,
+    seval_builtin_sval ge sp bs rs0 m0 = Some ba
+    /\ eval_builtin_arg ge (fun id => id) sp m ba v.
+Proof.
+  induction 1.
+  all: try (eexists; constructor; [simpl; reflexivity | constructor]).
+  2-3: try assumption.
+  - eexists. constructor.
+    + simpl. rewrite H. reflexivity.
+    + constructor.
+  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
+    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+    eexists. constructor.
+    + simpl. rewrite A1. rewrite A2. reflexivity.
+    + constructor; assumption. 
+  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
+    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+    eexists. constructor.
+    + simpl. rewrite A1. rewrite A2. reflexivity.
+    + constructor; assumption.
+Qed.
+
+Lemma seval_builtin_sval_args ge sp rs0 m0 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.
+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.
+    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 ->
+  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.
+Proof.
+  induction 1.
+  - eexists. constructor.
+    + simpl. reflexivity.
+    + constructor.
+  - destruct IHlist_forall2 as (lba & A & B).
+    apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
+    eexists. constructor.
+    + simpl. rewrite A'. rewrite A. reflexivity.
+    + 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.
+Proof.
+  intros. exploit seval_builtin_arg_sval; eauto.
+  intros (ba & X1 & X2).
+  eapply seval_builtin_sval_arg; eauto.
+  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.
+Proof.
+  intros. exploit seval_builtin_args_sval; eauto.
+  intros (ba & X1 & X2).
+  eapply seval_builtin_sval_args; eauto.
+  congruence.
+Qed.
+
+(** * Symbolic (final) value of a block *)
+
+Inductive sfval :=
+  | Sgoto (pc: exit)
+  | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
+    (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
+  | Stailcall: signature -> sval + ident -> list_sval -> sfval
+  | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
+  | Sjumptable (sv: sval) (tbl: list exit)
+  | Sreturn: option sval -> sfval
+.
+
+Definition sfind_function (ge: BTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): 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
+  end
+.
+
+Inductive sem_sfval (ge: BTL.genv) (sp:val) stack (f: function) (rs0: regset) (m0: mem): 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)
+  | 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')
+  | exec_Scall rs m sig svos lsv args res pc fd:
+      sfind_function ge sp svos rs0 m0 = 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)
+  | exec_Stailcall stk rs m sig svos args fd m' lsv:
+      sfind_function ge sp svos rs0 m0 = 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')
+  | 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')
+  | exec_Sjumptable sv tbl pc' n rs m:
+      eval_sval ge sp sv rs0 m0 = 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)
+.
+
+
+(** * 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 }.
+
+(* 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).
+
+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
+  .
+
+(** * Symbolic execution of final step *)
+Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
+  match i with
+  | Bgoto pc => Sgoto pc
+  | Bcall sig ros args res pc => 
+    let svos := sum_left_map sis.(si_sreg) ros in
+    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
+    Scall sig svos sargs res pc
+  | Btailcall sig ros args =>
+    let svos := sum_left_map sis.(si_sreg) ros in
+    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
+    Stailcall sig svos sargs
+  | Bbuiltin ef args res pc =>
+    let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
+    Sbuiltin ef sargs res pc
+  | Breturn or => 
+    let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
+    Sreturn sor
+  | Bjumptable reg tbl =>
+    let sv := sis.(si_sreg) reg in
+    Sjumptable sv tbl
+  end.
+
+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.
+Proof.
+  intros (PRE&MEM&REG). 
+  destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto.
+  + (* Bcall *) intros; eapply exec_Scall; auto.
+    - 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.
+    - erewrite eval_list_sval_inj; simpl; auto.
+  + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
+    eapply seval_builtin_args_correct; eauto.
+  + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
+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.
+Proof.
+  intros (PRE&MEM&REG).
+  destruct i; simpl; intros LAST; inv LAST; eauto.
+  + (* Breturn *)
+    enough (v=regmap_optget res Vundef rs) as ->; eauto.
+    destruct res; simpl in *; congruence.
+  + (* Bcall *)
+    erewrite eval_list_sval_inj in *; try_simplify_someHyps.
+    intros; eapply exec_Bcall; eauto.
+    destruct fn; simpl in * |- *; auto.
+    rewrite REG in * |- ; auto.
+  + (* Btailcall *)
+    erewrite eval_list_sval_inj in *; try_simplify_someHyps.
+    intros; eapply exec_Btailcall; eauto.
+    destruct fn; simpl in * |- *; auto.
+    rewrite REG in * |- ; auto.
+  + (* Bjumptable *)
+    eapply exec_Bjumptable; eauto.
+    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)
+  .
+
+
+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