diff options
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 116 |
1 files changed, 8 insertions, 108 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 65052310..e9ae11e0 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -1,9 +1,7 @@ (** Refinement of BTL_SEtheory data-structures in order to introduce (and prove correct) a lower-level specification of the simulation test. - TODO: not yet with hash-consing ? Or "fake" hash-consing only ? - - Ceci est un "bac à sable". + Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate]. - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques, @@ -17,106 +15,6 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import Op Registers. Require Import RTL BTL OptionMonad BTL_SEtheory. -(** * Preservation properties *) - -(* TODO: inherited from RTLpath. Use simu_proof_context + bctx2 + bctx1 instead of all the hypotheses/variables below ? *) - -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. - (** * ... *) Record sis_ok ctx (sis: sistate): Prop := { @@ -187,8 +85,8 @@ Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2): Proof. intros SIMU OK; econstructor; eauto. - erewrite <- SIMU_MEM; eauto. - unfold bctx2; erewrite smem_eval_preserved; eauto. - - unfold bctx2; intros; erewrite eval_sval_preserved; eauto. + erewrite <- smem_eval_preserved; eauto. + - intros; erewrite <- eval_sval_preserved; eauto. Qed. Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: @@ -199,7 +97,6 @@ Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 sem_sistate (bctx2 ctx) sis2 rs m. Proof. intros RIS REF1 REF2 SEM. - (* destruct REF1. destruct REF2. *) exploit sem_sok; eauto. erewrite OK_EQUIV; eauto. intros ROK1. @@ -209,13 +106,15 @@ Proof. destruct SEM as (PRE & SMEM & SREG). unfold sem_sistate; intuition eauto. + erewrite <- MEM_EQ, <- SIMU_MEM; eauto. - unfold bctx2; erewrite smem_eval_preserved; eauto. + erewrite <- smem_eval_preserved; eauto. erewrite MEM_EQ; eauto. + erewrite <- REG_EQ, <- SIMU_REG; eauto. - unfold bctx2; erewrite eval_sval_preserved; eauto. + erewrite <- eval_sval_preserved; eauto. erewrite REG_EQ; eauto. Qed. +(* TODO: + Definition option_refines ctx (orsv: option sval) (osv: option sval) := match orsv, osv with | Some rsv, Some sv => eval_sval ctx rsv = eval_sval ctx sv @@ -357,3 +256,4 @@ Proof. *) Admitted. +*)
\ No newline at end of file |