From 9c6213a5265408426b94416cf3807e891e54569a Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 7 May 2021 07:26:22 +0200
Subject: fix SymbValPreserved section

---
 scheduling/BTL_SEtheory.v | 99 ++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 98 insertions(+), 1 deletion(-)

(limited to 'scheduling/BTL_SEtheory.v')

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 7025b90c..4d5314f2 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -14,7 +14,7 @@ Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestr
 Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)
 
 
-Record iblock_exec_context := {
+Record iblock_exec_context := Bctx {
   cge: BTL.genv;
   csp: val;
   cstk: list stackframe;
@@ -431,6 +431,103 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
         E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
 .
 
+(** * Preservation properties *)
+
+Section SymbValPreserved.
+
+Variable ge ge': BTL.genv.
+
+Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
+
+Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
+
+Lemma senv_find_symbol_preserved id:
+  Senv.find_symbol ge id = Senv.find_symbol ge' id.
+Proof.
+  destruct senv_preserved_BTL as (A & B & C). congruence.
+Qed.
+
+Lemma senv_symbol_address_preserved id ofs:
+  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
+Proof.
+  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
+  reflexivity.
+Qed.
+
+Variable sp: val.
+Variable stk stk': list stackframe.
+Variable f f': function.
+Variable rs0: regset.
+Variable m0: mem.
+
+Lemma eval_sval_preserved sv:
+  eval_sval (Bctx ge sp stk f rs0 m0) sv = eval_sval (Bctx ge' sp stk' f' rs0 m0) sv.
+Proof.
+  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge sp stk f rs0 m0) lsv = eval_list_sval (Bctx ge' sp stk' f' rs0 m0) lsv)
+                                   (P1 := fun sm => eval_smem (Bctx ge sp stk f rs0 m0) sm = eval_smem (Bctx ge' sp stk' f' 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 sp stk f rs0 m0) m bs varg ->
+  seval_builtin_arg (Bctx ge' sp stk' f' 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 sp stk f rs0 m0) m lbs vargs ->
+  seval_builtin_args (Bctx ge' sp stk' f' 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 sp stk f rs0 m0) lsv = eval_list_sval (Bctx ge' sp stk' f' 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 sp stk f rs0 m0) sm = eval_smem (Bctx ge' sp stk' f' 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 sp stk f rs0 m0) cond lsv sm = seval_condition (Bctx ge' sp stk' f' 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 *)
-- 
cgit