Merge branch 'BTL_fsem' into BTL

1 files changed, 295 insertions, 246 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index cd69cd37..cea69f55 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1,7 +1,12 @@
-(* A theory of symbolic execution on BTL
+(** A theory of symbolic simulation (i.e. simulation of symbolic executions) on BTL blocks.
 
 NB: an efficient implementation with hash-consing will be defined in another file (some day)
 
+The main theorem of this file is [symbolic_simu_correct] stating
+that the abstract definition of symbolic simulation of two BTL blocks
+implies the simulation for BTL.fsem block-steps.
+
+
 *)
 
 Require Import Coqlib Maps Floats.
@@ -9,10 +14,6 @@ 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 *)
-
 Record iblock_exec_context := Bctx {
   cge: BTL.genv;
   cstk: list stackframe;
@@ -26,6 +27,7 @@ Record iblock_exec_context := Bctx {
 
 (* symbolic value *)
 Inductive sval :=
+  | Sundef
   | 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) 
@@ -51,6 +53,7 @@ Local Open Scope option_monad_scope.
 
 Fixpoint eval_sval ctx (sv: sval): option val :=
   match sv with
+  | Sundef => Some Vundef
   | Sinput r => Some ((crs0 ctx)#r)
   | Sop op l sm =>
      SOME args <- eval_list_sval ctx l IN
@@ -109,7 +112,7 @@ Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : o
 
 
 (** * Auxiliary definitions on Builtins *)
-(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *)
+(* TODO: clean this. Some generic stuffs could be put in [AST.v] *)
 
 Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)
 
@@ -166,7 +169,7 @@ Qed.
 
 End SEVAL_BUILTIN_ARG.
 
-(* NB: (cge ctx)neric function that could be put into [AST] file *)
+(* 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)
@@ -381,7 +384,6 @@ Qed.
 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)
@@ -395,21 +397,24 @@ Definition sfind_function ctx (svos : sval + ident): option fundef :=
   end
 .
 
+Import ListNotations.
+Local Open Scope list_scope.
+
 Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
   | exec_Sgoto pc rs m:
-      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m)
+      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m)
   | exec_Sreturn stk osv rs m m' v:
       (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 
+      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 ctx svos = Some fd ->
       funsig fd = sig ->
       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)
+        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::cstk ctx) fd args m)
   | exec_Stailcall stk rs m sig svos args fd m' lsv:
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
@@ -422,136 +427,23 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
       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')
+        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m')
   | exec_Sjumptable sv tbl pc' n rs m:
       eval_sval ctx sv = Some (Vint n) ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
       sem_sfval ctx (Sjumptable sv tbl) rs m
-        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
+        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None 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.
-
-Variable stk stk': list stackframe.
-Variable f f': function.
-Variable sp: val.
-Variable rs0: regset.
-Variable m0: mem.
-
-Lemma eval_sval_preserved sv:
-  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
-Proof.
-  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
-                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); 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 m: forall bs varg,
-  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
-  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
-Proof.
-  induction 1; simpl.
-  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 m lbs vargs:
-  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
-  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
-Proof.
-  induction 1; constructor; eauto.
-  eapply seval_builtin_arg_preserved; auto.
-Qed.
-
-Lemma list_sval_eval_preserved lsv: 
-  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
-Proof.
-  induction lsv; simpl; auto.
-  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
-  rewrite IHlsv; auto.
-Qed.
-
-Lemma smem_eval_preserved sm: 
-  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
-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 cond lsv sm:
-  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
-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 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 ((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).
-
-(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets.
-   And, nothing in their representation as (val * PTree.t val) enforces that
-     (forall r, rs1#r = rs2#r) -> rs1 = rs2
-*)
-Lemma sem_sistate_determ ctx st rs1 m1 rs2 m2:
-  sem_sistate ctx st rs1 m1 ->
-  sem_sistate ctx st rs2 m2 ->
-  (forall r, rs1#r = rs2#r) /\ m1 = m2.
-Proof.
-  intros (_&MEM1&REG1) (_&MEM2&REG2).
-  intuition try congruence.
-  generalize (REG1 r); rewrite REG2; congruence.
-Qed.
+Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
+  sis.(si_pre) ctx
+  /\ eval_smem ctx sis.(si_smem) = Some m
+  /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r).
 
 (** * Symbolic execution of final step *)
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
@@ -580,10 +472,10 @@ Local Hint Constructors sem_sfval: core.
 
 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 -> 
+  final_step tr_inputs (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). 
+  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.
@@ -604,7 +496,7 @@ Local Hint Resolve seval_builtin_args_exact: core.
 Lemma sexec_final_svf_exact 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.
+  -> final_step tr_inputs (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.
@@ -626,7 +518,6 @@ Proof.
     congruence.
 Qed.
 
-
 (** * symbolic execution of basic instructions *)
 
 Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.
@@ -735,6 +626,76 @@ Proof.
   erewrite MEM; auto.
 Qed.
 
+(** * Compute sistate associated to final values *)
+Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
+  match inputs with
+  | nil => fun r => Sundef 
+  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
+  end.
+
+Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)).
+
+Lemma str_inputs_correct ctx sis rs tbl or r:
+  (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) ->
+  eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r.
+Proof.
+  intros H.
+  unfold str_inputs, tr_inputs, transfer_regs.
+  induction (Regset.elements _) as [|x l]; simpl.
+  + rewrite Regmap.gi; auto.
+  + autodestruct; intros; subst.
+    * rewrite Regmap.gss; auto.
+    * rewrite Regmap.gso; eauto.
+Qed.
+
+Local Hint Resolve str_inputs_correct: core.
+
+Definition tr_sis f (fi: final) (sis: sistate) :=
+  {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
+     si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
+     si_smem := sis.(si_smem) |}.
+
+Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
+  eval_sval ctx (sis.(si_sreg) r).
+
+Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
+  sem_sistate ctx sis rs m ->
+  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
+Proof.
+  Local Opaque str_inputs.
+  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
+  destruct fin; simpl; eauto.
+Qed.
+
+Lemma tr_sis_regs_correct ctx fin sis rs m:
+  sem_sistate ctx sis rs m ->
+  sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m.
+Proof.
+  intros H.
+  generalize (tr_sis_regs_correct_aux _ fin _ _ _ H).
+  destruct H as (PRE & MEM & REG).
+  econstructor; simpl; intuition eauto || congruence.
+Qed.
+
+Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (svf: sfval): A := 
+  match svf with
+  | Sgoto pc => tr f [pc] None
+  | Scall _ _ _ res pc => tr f [pc] (Some res)
+  | Stailcall _ _ args => tr f [] None
+  | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
+  | Sreturn _ => tr f [] None
+  | Sjumptable _ tbl => tr f tbl None
+  end.
+
+Definition str_regs: function -> sfval -> regset -> regset :=
+  poly_str tr_inputs.
+
+Lemma str_tr_regs_equiv f fin sis:
+  str_regs f (sexec_final_sfv fin sis) = tr_regs f fin.
+Proof.
+  destruct fin; simpl; auto.
+Qed.
+
 (** * symbolic execution of blocks *)
 
 (* symbolic state *)
@@ -746,8 +707,8 @@ Inductive sstate :=
 
 (* transition (t,s) produced by a sstate in initial context ctx *)
 Inductive sem_sstate ctx t s: sstate -> Prop :=
-  | sem_Sfinal sis sfv rs m
-     (SIS: sem_sistate ctx sis rs m)
+  | sem_Sfinal sis sfv rs m 
+     (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m)
      (SFV: sem_sfval ctx sfv rs m t s)
      : sem_sstate ctx t s (Sfinal sis sfv)
   | sem_Scond b cond args sm ifso ifnot
@@ -768,9 +729,9 @@ pour représenter l'ensemble des chemins.
 
 *)
 
-Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
+Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := 
   match ib with
-  | BF fin _ => Sfinal sis (sexec_final_sfv fin sis)
+  | BF fin => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis)
   (* basic instructions *)
   | Bnop _ => k sis
   | Bop op args res _ => k (sexec_op op args res sis)
@@ -779,19 +740,19 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
-      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
+      sexec_rec f ib1 sis (fun sis2 => sexec_rec f ib2 sis2 k) 
   | Bcond cond args ifso ifnot _ =>
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
-      let ifso := sexec_rec ifso sis k in
-      let ifnot := sexec_rec ifnot sis k in
+      let ifso := sexec_rec f ifso sis k in
+      let ifnot := sexec_rec f ifnot sis k in
       Scond cond args sis.(si_smem) ifso ifnot
   end
   .
 
-Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort).
+Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort).
 
 Local Hint Constructors sem_sstate: core.
-Local Hint Resolve sexec_op_correct sexec_final_svf_correct 
+Local Hint Resolve sexec_op_correct sexec_final_svf_correct tr_sis_regs_correct_aux tr_sis_regs_correct
                    sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core.
 
 Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
@@ -799,131 +760,72 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
   (SIS: sem_sistate ctx sis rs m)
   (CONT: match ofin with
          | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
-         | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         | Some fin => final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
          end),
-  sem_sstate ctx t s (sexec_rec ib sis k).
+  sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k).
 Proof.
   induction ISTEP; simpl; try autodestruct; eauto.
+  (* final value *)
+  intros; econstructor; eauto.
+  rewrite str_tr_regs_equiv; eauto.
   (* condition *)
   all: intros;
     eapply sem_Scond; eauto; [
       erewrite seval_condition_eq; eauto |
-      replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); 
+      replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (if b then ifso else ifnot) sis k); 
       try autodestruct; eauto ].
 Qed.
 
+
 (* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
   (sexec is a correct over-approximation)
 *)
 Theorem sexec_correct ctx ib t s: 
-  iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
-  sem_sstate ctx t s (sexec ib).
+  iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+  sem_sstate ctx t s (sexec (cf ctx) ib).
 Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
   eapply sexec_rec_correct; simpl; eauto.
 Qed.
 
-
-(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *)
-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)
-  .
-
-Local Hint Constructors equiv_stackframe equiv_state: core.
-
-Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
-Proof.
-  destruct stf; eauto.
-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.
-
-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: core.
-  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.
+(* Remark that we want to reason modulo "extensionality" wrt Regmap.get about regsets.
+   And, nothing in their representation as (val * PTree.t val) enforces that
+     (forall r, rs1#r = rs2#r) -> rs1 = rs2
+*)
+Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
+  sem_sistate ctx sis rs1 m1 ->
+  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 ->
+     (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) 
+  /\ m1 = m2.
 Proof.
-  Local Hint Resolve equiv_stack_trans: core.
-  destruct 1; intros EQ; inv EQ; econstructor; eauto.
-  intros; eapply eq_trans; eauto.
+  intros H1 H2.
+  lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
+  unfold sreg_eval; intros X.
+  destruct H1 as (_&MEM1&REG1).
+  destruct H2 as (_&MEM2&REG2); simpl in *.
+  intuition try congruence.
+  cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r).
+  { congruence. }
+  rewrite <- REG2, X. auto.
 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.
+Local Hint Constructors equiv_stackframe list_forall2: core.
+Local Hint Resolve regmap_setres_eq equiv_stack_refl equiv_stack_refl: core.
 
 Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
   sem_sfval ctx sfv rs1 m t s ->
-  (forall r, rs1#r = rs2#r) -> 
-  exists s', equiv_state s s' /\  sem_sfval ctx sfv rs2 m t s'.
-Proof. 
-  Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core.
-  Local Hint Constructors sem_sfval: core.
-  destruct 1; eexists; split; econstructor; eauto.
-  econstructor; eauto.
+  (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) ->
+  exists s', sem_sfval ctx sfv rs2 m t s' /\ equiv_state s s'.
+Proof.
+  unfold str_regs.
+  destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence.
 Qed.
 
-Local Hint Resolve sexec_final_svf_exact: core.
-
 Definition abort_sistate ctx (sis: sistate): Prop :=
   ~(sis.(si_pre) ctx)
   \/ eval_smem ctx sis.(si_smem) = None
   \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None.
 
-Lemma sem_sistate_exclude_abort ctx sis rs m:
-  sem_sistate ctx sis rs m ->
-  abort_sistate ctx sis ->
-  False.
-Proof.
-  intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0').
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
-Qed.
-
-Local Hint Resolve sem_sistate_exclude_abort: core.
-
 Lemma set_sreg_preserves_abort ctx sv dst sis:
   abort_sistate ctx sis ->
   abort_sistate ctx (set_sreg dst sv sis).
@@ -963,11 +865,20 @@ Proof.
   intros; eapply set_smem_preserves_abort; eauto.
 Qed.
 
+Lemma sem_sistate_tr_sis_exclude_abort ctx sis fi rs m:
+  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs m ->
+  abort_sistate ctx sis ->
+  False.
+Proof.
+  intros ((PRE1 & PRE2) & MEM & REG); simpl in *.
+  intros [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; try congruence.
+Qed.
+
 Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
-  sexec_store_preserves_abort: core.
+  sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core.
 
 Lemma sexec_exclude_abort ctx ib t s1: forall sis k
-  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   (ABORT: abort_sistate ctx sis),
   False.
@@ -1039,17 +950,17 @@ Proof.
   intros; rewrite REG; autodestruct; try_simplify_someHyps.
 Qed.
 
-Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core.
+Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_svf_exact: core.
 
 Lemma sexec_rec_exact ctx ib t s1: forall sis k
-  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   rs m
   (SIS: sem_sistate ctx sis rs m)
   (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   ,
      match iblock_istep_run (cge ctx) (csp ctx) ib rs m with
      | Some (out rs' m' (Some fin)) =>
-        exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+        exists s2, final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
      | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
      | None => False
      end.
@@ -1057,11 +968,11 @@ Proof.
   induction ib; simpl; intros; eauto.
   - (* final *)
     inv SEXEC.
-    exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto.
+    exploit (sem_sistate_tr_sis_determ ctx sis rs m fi); eauto.
     intros (REG&MEM); subst.
     exploit (sem_sfval_equiv rs0 rs); eauto.
-    intros (s2 & EQUIV & SFV').
-    eexists; split; eauto.
+    * intros; rewrite REG, str_tr_regs_equiv; auto.
+    * intros (s2 & EQUIV & SFV'); eauto.
   - (* Bop *) autodestruct; eauto.
   - destruct trap; [| inv SEXEC ].
     repeat autodestruct; eauto.
@@ -1094,8 +1005,8 @@ Qed.
   (sexec is exact).
 *)
 Theorem sexec_exact ctx ib t s1: 
-  sem_sstate ctx t s1 (sexec ib) ->
-  exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
+  sem_sstate ctx t s1 (sexec (cf ctx) ib) ->
+  exists s2, iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
              /\ equiv_state s1 s2.
 Proof.
   intros; exploit sexec_rec_exact; eauto.
@@ -1109,3 +1020,141 @@ Proof.
     inversion SEXEC.
 Qed.
 
+(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
+
+Record simu_proof_context := Sctx {
+   sge1: BTL.genv;
+   sge2: BTL.genv;
+   sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s;
+   sstk1: list BTL.stackframe;
+   sstk2: list BTL.stackframe;
+   sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2;
+   sf1: BTL.function;
+   sf2: BTL.function;
+   ssp: val;
+   srs0: regset; 
+   sm0: mem
+}.
+
+Definition bctx1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) ctx.(sf1) ctx.(ssp) ctx.(srs0) ctx.(sm0).
+Definition bctx2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) ctx.(sf2) ctx.(ssp) ctx.(srs0) ctx.(sm0).
+
+Definition sstate_simu (ctx: simu_proof_context) (st1 st2: sstate) :=
+  forall t s1, sem_sstate (bctx1 ctx) t s1 st1 ->
+  exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2.
+
+Definition symbolic_simu ctx ib1 ib2: Prop := sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2).
+
+Theorem symbolic_simu_correct ctx ib1 ib2:
+  symbolic_simu ctx ib1 ib2 ->
+  forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 ->
+  exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2.
+Proof.
+  unfold symbolic_simu, sstate_simu.
+  intros SIMU t s1 STEP1.
+  exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
+  intros; exploit SIMU; eauto.
+  intros (s2 & SEM1 & EQ1).
+  exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
+  intros (s3 & STEP2 & EQ2).
+  clear STEP1; eexists; split; eauto.
+  eapply equiv_state_trans; eauto.
+Qed.
+
+(** * 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.
+
+Variable stk stk': list stackframe.
+Variable f f': function.
+Variable sp: val.
+Variable rs0: regset.
+Variable m0: mem.
+
+Lemma eval_sval_preserved sv:
+  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
+Proof.
+  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
+                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); 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 m: forall bs varg,
+  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
+  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
+Proof.
+  induction 1; simpl.
+  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 m lbs vargs:
+  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
+  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
+Proof.
+  induction 1; constructor; eauto.
+  eapply seval_builtin_arg_preserved; auto.
+Qed.
+
+Lemma list_sval_eval_preserved lsv: 
+  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
+Proof.
+  induction lsv; simpl; auto.
+  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
+  rewrite IHlsv; auto.
+Qed.
+
+Lemma smem_eval_preserved sm: 
+  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
+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 cond lsv sm:
+  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
+Proof.
+  unfold seval_condition.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  rewrite smem_eval_preserved; auto.
+Qed.
+
+End SymbValPreserved.