fix the definition of [symbolic_simu] in BTL_SEtheory

1 files changed, 243 insertions, 64 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 72789121..c437846e 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -16,7 +16,7 @@ Require Import RTL BTL OptionMonad.
 
 Record iblock_exec_context := Bctx {
   cge: BTL.genv;
-  cstk: list stackframe;
+  (* cstk: list stackframe; *) (* having the stack here does seem not a good idea *)
   cf: function;
   csp: val;
   crs0: regset;
@@ -400,39 +400,39 @@ Definition sfind_function ctx (svos : sval + ident): option fundef :=
 Import ListNotations.
 Local Open Scope list_scope.
 
-Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
+Inductive sem_sfval ctx stk: 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 (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' ->
+      sem_sfval ctx stk (Sgoto pc) rs m E0 (State stk (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m)
+  | exec_Sreturn pstk osv rs m m' v:
+      (csp ctx) = (Vptr pstk Ptrofs.zero) ->
+      Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' ->
       match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
-      sem_sfval ctx (Sreturn osv) rs m
-         E0 (Returnstate (cstk ctx) v m')
+      sem_sfval ctx stk (Sreturn osv) rs m
+         E0 (Returnstate stk 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 (tr_inputs ctx.(cf) [pc] (Some res) rs)::cstk ctx) fd args m)
-  | exec_Stailcall stk rs m sig svos args fd m' lsv:
+      sem_sfval ctx stk (Scall sig svos lsv res pc) rs m
+        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::stk) fd args m)
+  | exec_Stailcall pstk rs m sig svos args fd m' lsv:
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
-      (csp ctx) = Vptr stk Ptrofs.zero ->
-      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
+      (csp ctx) = Vptr pstk Ptrofs.zero ->
+      Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' ->
       eval_list_sval ctx lsv = Some args ->
-      sem_sfval ctx (Stailcall sig svos lsv) rs m
-        E0 (Callstate (cstk ctx) fd args m')
+      sem_sfval ctx stk (Stailcall sig svos lsv) rs m
+        E0 (Callstate stk fd args m')
   | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
       seval_builtin_args ctx m sargs vargs ->
       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 (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m')
+      sem_sfval ctx stk (Sbuiltin ef sargs res pc) rs m
+        t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m')
   | 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' (tr_inputs ctx.(cf) tbl None rs) m)
+      sem_sfval ctx stk (Sjumptable sv tbl) rs m
+        E0 (State stk (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m)
 .
 
 (* Syntax and Semantics of symbolic internal states *)
@@ -470,10 +470,10 @@ Definition sexec_final_sfv (i: final) (sis: sistate): sfval :=
 
 Local Hint Constructors sem_sfval: core.
 
-Lemma sexec_final_svf_correct ctx i sis t rs m s:
+Lemma sexec_final_svf_correct ctx stk i sis t rs m s:
   sem_sistate ctx sis rs m ->
-  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.
+  final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s -> 
+  sem_sfval ctx stk (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.
@@ -493,10 +493,10 @@ Qed.
 Local Hint Constructors final_step: core.
 Local Hint Resolve seval_builtin_args_exact: core.
 
-Lemma sexec_final_svf_exact ctx i sis t rs m s:
+Lemma sexec_final_svf_exact ctx stk 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 tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
+  sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s
+  -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s.
 Proof.
   intros (PRE&MEM&REG).
   destruct i; simpl; intros LAST; inv LAST; eauto.
@@ -705,19 +705,61 @@ Inductive sstate :=
   | Sabort
  .
 
+(* outcome of a symbolic execution path *)
+Record soutcome := sout {
+   so_sis: sistate;
+   so_svf: sfval;
+}.
+
+Fixpoint run_sem_isstate ctx (st:sstate): option soutcome :=
+  match st with
+  | Sfinal sis sfv => Some (sout sis sfv)
+  | Scond cond args sm ifso ifnot =>
+     SOME b <- seval_condition ctx cond args sm IN
+     run_sem_isstate ctx (if b then ifso else ifnot)
+  | _ => None
+  end.
+
 (* transition (t,s) produced by a sstate in initial context ctx *)
-Inductive sem_sstate ctx t s: sstate -> Prop :=
+Inductive sem_sstate ctx stk t s: sstate -> Prop :=
   | 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)
+     (SFV: sem_sfval ctx stk sfv rs m t s)
+     : sem_sstate ctx stk t s (Sfinal sis sfv)
   | sem_Scond b cond args sm ifso ifnot
      (SEVAL: seval_condition ctx cond args sm = Some b)
-     (SELECT: sem_sstate ctx t s (if b then ifso else ifnot))
-     : sem_sstate ctx t s (Scond cond args sm ifso ifnot)
+     (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot))
+     : sem_sstate ctx stk t s (Scond cond args sm ifso ifnot)
   (* NB: Sabort: fails to produce a transition *) 
   .
 
+Lemma sem_sstate_run ctx stk st t s:
+  sem_sstate ctx stk t s st -> 
+  exists sis sfv rs m, 
+      run_sem_isstate ctx st = Some (sout sis sfv)
+   /\ sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m
+   /\ sem_sfval ctx stk sfv rs m t s
+   .
+Proof.
+  induction 1; simpl; try_simplify_someHyps; do 4 eexists; intuition eauto.
+Qed.
+
+Local Hint Resolve sem_Sfinal: core.
+
+Lemma run_sem_sstate ctx st sis sfv:
+  run_sem_isstate ctx st = Some (sout sis sfv) ->
+  forall rs m stk s t, 
+  sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m ->
+  sem_sfval ctx stk sfv rs m t s ->
+  sem_sstate ctx stk t s st
+  .
+Proof.
+  induction st; simpl; try_simplify_someHyps.
+  autodestruct; intros; econstructor; eauto.
+  autodestruct; eauto.
+Qed.
+
+
 (** * Idée de l'execution symbolique en Continuation Passing Style 
 
 [k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche)
@@ -755,14 +797,14 @@ Local Hint Constructors sem_sstate: core.
 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
+Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin
   (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k
   (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 tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx stk t s (k sis')
+         | Some fin => final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs1 m1 fin t s
          end),
-  sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k).
+  sem_sstate ctx stk t s (sexec_rec (cf ctx) ib sis k).
 Proof.
   induction ISTEP; simpl; try autodestruct; eauto.
   (* final value *)
@@ -780,9 +822,9 @@ 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 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).
+Theorem sexec_correct ctx stk ib t s: 
+  iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+  sem_sstate ctx stk t s (sexec (cf ctx) ib).
 Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
   eapply sexec_rec_correct; simpl; eauto.
@@ -812,10 +854,10 @@ 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 ->
+Lemma sem_sfval_equiv rs1 rs2 ctx stk sfv m t s:
+  sem_sfval ctx stk sfv rs1 m t s ->
   (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'.
+  exists s', sem_sfval ctx stk 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.
@@ -877,9 +919,9 @@ Qed.
 Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
   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 (cf ctx) ib sis k))
-  (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
+Lemma sexec_exclude_abort ctx stk ib t s1: forall sis k
+  (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k))
+  (CONT: forall sis', sem_sstate ctx stk t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   (ABORT: abort_sistate ctx sis),
   False.
 Proof.
@@ -952,16 +994,16 @@ Qed.
 
 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 (cf ctx) ib sis k))
+Lemma sexec_rec_exact ctx stk ib t s1: forall sis k
+  (SEXEC: sem_sstate ctx stk 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)
+  (CONT: forall sis', sem_sstate ctx stk 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 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')
+        exists s2, final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+     | Some (out rs' m' None) => exists sis', (sem_sstate ctx stk t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
      | None => False
      end.
 Proof.
@@ -1004,9 +1046,9 @@ Qed.
 (* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution
   (sexec is exact).
 *)
-Theorem sexec_exact ctx ib t s1: 
-  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
+Theorem sexec_exact ctx stk ib t s1: 
+  sem_sstate ctx stk t s1 (sexec (cf ctx) ib) ->
+  exists s2, iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
              /\ equiv_state s1 s2.
 Proof.
   intros; exploit sexec_rec_exact; eauto.
@@ -1047,9 +1089,6 @@ Record simu_proof_context {f1 f2: BTL.function} := 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;
    (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *)
    ssp: val;
    srs0: regset; 
@@ -1057,24 +1096,69 @@ Record simu_proof_context {f1 f2: BTL.function} := Sctx {
 }.
 Arguments simu_proof_context: clear implicits.
 
-Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0).
-Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0).
+Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0).
+Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0).
+
+(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract 
+         the [match_states] of BTL_Schedulerproof.
 
+  Indeed, the [match_states] involves [match_function] in [match_stackframe].
+  And, here, we aim to define a notion of simulation for defining [match_function].
 
-(* TODO: A REVOIR. L'approche suivie ne marche pas !!! 
+  A syntactic definition of the simulation on [sfval] avoids the circularity issue.
 
-le [equiv_state] ci-dessous n'est pas assez général 
-  => il faut un [match_state] qui va dépendre de [BTL_Scheduler.match_function] (dans le [match_stackframe]).
+*)
 
-Or, le [sstate_simu] qu'on cherche à définir ici, c'était pour définir ce [match_function]: circularité !
+Inductive optsv_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (option sval) -> (option sval) -> Prop :=
+  | Ssome_simu sv1 sv2:
+     eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2
+     -> optsv_simu ctx (Some sv1) (Some sv2)
+  | Snone_simu: optsv_simu ctx None None
+  .
 
-Une solution: définir le match_function à l'aide d'un [iblock_step_simu] ?
+Inductive svident_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (sval + ident) -> (sval + ident) -> Prop :=
+  | Sleft_simu sv1 sv2:
+     eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2
+     -> svident_simu ctx (inl sv1) (inl sv2)
+  | Sright_simu id1 id2:
+     id1 = id2
+     -> svident_simu ctx (inr id1) (inr id2)
+  .
 
-Pas sûr que ça marche, on aura aussi la dépendance circulaire entre [simu_proof_context] et [match_function] !
+Definition bargs_simu {f1 f2: function} (ctx: simu_proof_context f1 f2) (args1 args2: list (builtin_arg sval)): Prop :=
+  eval_list_builtin_sval (bctx1 ctx) args1 = eval_list_builtin_sval (bctx2 ctx) args2.
+
+Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Prop :=
+  | Sgoto_simu pc: sfv_simu ctx (Sgoto pc) (Sgoto pc)
+  | Scall_simu sig ros1 ros2 args1 args2 r pc
+      (SVID: svident_simu ctx ros1 ros2)
+      (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2)
+      :sfv_simu ctx (Scall sig ros1 args1 r pc) (Scall sig ros2 args2 r pc)
+  | Stailcall_simu sig ros1 ros2 args1 args2
+      (SVID: svident_simu ctx ros1 ros2)
+      (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2)
+      :sfv_simu ctx (Stailcall sig ros1 args1) (Stailcall sig ros2 args2)
+  | Sbuiltin_simu ef lba1 lba2 br pc
+      (BARGS: bargs_simu ctx lba1 lba2)
+      :sfv_simu ctx (Sbuiltin ef lba1 br pc) (Sbuiltin ef lba2 br pc)
+  | Sjumptable_simu sv1 sv2 lpc
+      (VAL: eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2)
+      :sfv_simu ctx (Sjumptable sv1 lpc) (Sjumptable sv2 lpc)
+  | simu_Sreturn osv1 osv2
+      (OPT:optsv_simu ctx osv1 osv2)
+      :sfv_simu ctx (Sreturn osv1) (Sreturn osv2)
+.
 
-Autre solution: définir [sfval_simu] syntaxiquement comme dans [RTLpath_SEtheory] pour éviter le problème de circularité !
+Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop :=
+  forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) ->
+  exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) /\ sfv_simu ctx sfv1 sfv2
+  .
+
+Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2).
 
+(* REM. L'approche suivie initialement ne marche pas !!!
 *)
+(*
 Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (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.
@@ -1095,4 +1179,99 @@ Proof.
   intros (s3 & STEP2 & EQ2).
   clear STEP1; eexists; split; eauto.
   eapply equiv_state_trans; eauto.
-Qed.
\ No newline at end of file
+Qed.
+*)
+
+(** * Preservation properties *)
+
+Section SymbValPreserved.
+
+Variable f1 f2: function.
+
+Hypothesis ctx: simu_proof_context f1 f2.
+Local Hint Resolve sge_match: core.
+
+Lemma eval_sval_preserved sv:
+  eval_sval (bctx1 ctx) sv = eval_sval (bctx2 ctx) sv.
+Proof.
+  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) lsv)
+                                   (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) 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 _ _ _ _); 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 _ _ _ _); auto.
+    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
+    rewrite IHsv1; auto.
+Qed.
+
+Lemma list_sval_eval_preserved lsv: 
+  eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) 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 (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm.
+Proof.
+  induction sm; simpl; auto.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  erewrite eval_addressing_preserved; eauto.
+  destruct (eval_addressing _ _ _ _); auto.
+  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
+  rewrite eval_sval_preserved; auto.
+Qed.
+
+Lemma seval_condition_preserved cond lsv sm:
+  seval_condition (bctx1 ctx) cond lsv sm = seval_condition (bctx2 ctx) cond lsv sm.
+Proof.
+  unfold seval_condition.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  rewrite smem_eval_preserved; auto.
+Qed.
+
+Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx).
+
+Lemma senv_find_symbol_preserved id:
+  Senv.find_symbol (sge1 ctx) id = Senv.find_symbol (sge2 ctx) id.
+Proof.
+  destruct senv_preserved_BTL as (A & B & C). congruence.
+Qed.
+
+Lemma senv_symbol_address_preserved id ofs:
+  Senv.symbol_address (sge1 ctx) id ofs = Senv.symbol_address (sge2 ctx) id ofs.
+Proof.
+  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
+  reflexivity.
+Qed.
+
+Lemma seval_builtin_arg_preserved m: forall bs varg,
+  seval_builtin_arg (bctx1 ctx) m bs varg ->
+  seval_builtin_arg (bctx2 ctx) m bs varg.
+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 (bctx1 ctx) m lbs vargs ->
+  seval_builtin_args (bctx2 ctx) m lbs vargs.
+Proof.
+  induction 1; constructor; eauto.
+  eapply seval_builtin_arg_preserved; auto.
+Qed.
+
+End SymbValPreserved.
+