cleaning BTL_SEtheory

1 files changed, 114 insertions, 190 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index d6b4e741..79db99c8 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1,20 +1,19 @@
-(* 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.
+
 
-(* TODO: A REVOIR - remplacer les [tid] par [tr_inputs] pour montrer la bisimulation avec [fsem] plutôt. *)
+*)
 
 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 *)
-
 Record iblock_exec_context := Bctx {
   cge: BTL.genv;
   cstk: list stackframe;
@@ -113,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 *)
 
@@ -170,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)
@@ -436,105 +435,6 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
         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 }.
@@ -909,80 +809,8 @@ Proof.
   rewrite <- REG2, X. auto.
 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.
-Proof.
-  Local Hint Resolve equiv_stack_trans: core.
-  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.
-
-(* Local Hint Resolve tr_inputs_ext: core. *)
-Local Hint Resolve regmap_setres_eq: core.
+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 ->
@@ -991,11 +819,8 @@ Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
 Proof.
   unfold str_regs.
   destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence.
-  constructor; eauto.
 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
@@ -1125,7 +950,7 @@ 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 (cf ctx) ib sis k))
@@ -1195,7 +1020,7 @@ Proof.
     inversion SEXEC.
 Qed.
 
-(** * High-Level specification of the symbolic simulation test as predicate [sstate_simu] *)
+(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
 
 Record simu_proof_context := Sctx {
    sge1: BTL.genv;
@@ -1218,12 +1043,14 @@ 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.
 
-Theorem sstate_simu_correct ctx ib1 ib2:
-  sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2) ->
+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 sstate_simu.
+  unfold symbolic_simu, sstate_simu.
   intros SIMU t s1 STEP1.
   exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
   intros; exploit SIMU; eauto.
@@ -1234,3 +1061,100 @@ Proof.
   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.