From 0d856574d11ccccab397e007d43437980e07aeac Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 3 Jun 2021 08:31:20 +0200 Subject: progress in BTL_SEsimuref --- scheduling/BTL_SEsimuref.v | 136 +++++++++++++++++++-------------------------- scheduling/BTL_SEtheory.v | 85 +++++++++++++++++----------- 2 files changed, 112 insertions(+), 109 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index e9ae11e0..c322a9a5 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -89,14 +89,13 @@ Proof. - 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: +Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: ris_simu ris1 ris2 -> ris_refines (bctx1 ctx) ris1 sis1 -> ris_refines (bctx2 ctx) ris2 sis2 -> - sem_sistate (bctx1 ctx) sis1 rs m -> - sem_sistate (bctx2 ctx) sis2 rs m. + sistate_simu ctx sis1 sis2. Proof. - intros RIS REF1 REF2 SEM. + intros RIS REF1 REF2 rs m SEM. exploit sem_sok; eauto. erewrite OK_EQUIV; eauto. intros ROK1. @@ -113,62 +112,76 @@ Proof. 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 - | None, None => True - | _, _ => False - end. +Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop := + | RefSome rsv sv + (REF:eval_sval ctx rsv = eval_sval ctx sv) + :optrsv_refines ctx (Some rsv) (Some sv) + | RefNone: optrsv_refines ctx None None + . -Definition sum_refines ctx (rsi: sval + ident) (si: sval + ident) := - match rsi, si with - | inl rsv, inl sv => eval_sval ctx rsv = eval_sval ctx sv - | inr id, inr id' => id = id' - | _, _ => False - end. +Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop := + | RefLeft rsv sv + (REF:eval_sval ctx rsv = eval_sval ctx sv) + :rsvident_refines ctx (inl rsv) (inl sv) + | RefRight id1 id2 + (IDSIMU: id1 = id2) + :rsvident_refines ctx (inr id1) (inr id2) + . Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop := eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args. Inductive rfv_refines ctx: sfval -> sfval -> Prop := - | refines_Sgoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc) - | refines_Scall: forall sig rvos ros rargs args r pc - (SUM:sum_refines ctx rvos ros) + | RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc) + | RefCall sig rvos ros rargs args r pc + (SV:rsvident_refines ctx rvos ros) (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) - ,rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc) - | refines_Stailcall: forall sig rvos ros rargs args - (SUM:sum_refines ctx rvos ros) + :rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc) + | RefTailcall sig rvos ros rargs args + (SV:rsvident_refines ctx rvos ros) (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) - ,rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args) - | refines_Sbuiltin: forall ef lbra lba br pc + :rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args) + | RefBuiltin ef lbra lba br pc (BARGS: bargs_refines ctx lbra lba) - ,rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc) - | refines_Sjumptable: forall rsv sv lpc + :rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc) + | RefJumptable rsv sv lpc (VAL: eval_sval ctx rsv = eval_sval ctx sv) - ,rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc) - | refines_Sreturn: forall orsv osv - (OPT:option_refines ctx orsv osv) - ,rfv_refines ctx (Sreturn orsv) (Sreturn osv) + :rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc) + | RefReturn orsv osv + (OPT:optrsv_refines ctx orsv osv) + :rfv_refines ctx (Sreturn orsv) (Sreturn osv) . Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2. -Local Hint Constructors sem_sfval equiv_state: core. +Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core. -Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s: +Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2: rfv_simu rfv1 rfv2 -> rfv_refines (bctx1 ctx) rfv1 sfv1 -> rfv_refines (bctx2 ctx) rfv2 sfv2 -> - sem_sfval (bctx1 ctx) sfv1 rs m t s -> - exists s', sem_sfval (bctx2 ctx) sfv2 rs m t s' /\ equiv_state s s'. + sfv_simu ctx sfv1 sfv2. Proof. - unfold rfv_simu; intros X REF1 REF2 SEM. subst. - unfold bctx2; destruct REF1; inv REF2; inv SEM; simpl. - - eexists; split; eauto; simpl. - (* eapply State_equiv; eauto. NE MARCHE PAS ! *) -Admitted. + unfold rfv_simu; intros X REF1 REF2. subst. + unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto. + - (* call svid *) + inv SV; inv SV0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. + - (* call args *) + rewrite <- LIST, <- LIST0; eauto. + - (* taillcall svid *) + inv SV; inv SV0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. + - (* tailcall args *) + rewrite <- LIST, <- LIST0; eauto. + - (* builtin args *) + unfold bargs_refines, bargs_simu in *. + rewrite <- BARGS, <- BARGS0; eauto. + - rewrite <- VAL, <- VAL0; eauto. + - (* return *) + inv OPT; inv OPT0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. +Qed. (* refinement of (symbolic) state *) Inductive rstate := @@ -197,18 +210,18 @@ Inductive rst_simu: rstate -> rstate -> Prop := (* Comment prend on en compte le ris en cours d'execution ??? *) Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop := - | refines_Sfinal ris sis rfv sfv (*ok: Prop*) + | Reffinal ris sis rfv sfv (*ok: Prop*) (*OK: ris_ok ctx ris -> ok*) (RIS: ris_refines ctx ris sis) (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) : rst_refines ctx (*ok*) (Rfinal ris rfv) (Sfinal sis sfv) - | refines_Scond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*) + | Refcond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*) (*OK1: ok2 -> ok1*) (RCOND: (* ok2 -> *) seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm) (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx (*ok2*) rifso ifso) (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx (*ok2*) rifnot ifnot) : rst_refines ctx (*ok1*) (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot) - | refines_Sabort + | Refabort : rst_refines ctx Rabort Sabort . @@ -223,37 +236,4 @@ Proof. induction 1; simpl; auto. - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. inv REF1. inv REF2. inv SEM1. - exploit sem_sok; eauto. - rewrite OK_EQUIV; eauto. - intros RIS_OK1. - exploit (ris_simu_ok_preserv f1 f2); eauto. - intros RIS_OK2. intuition. - exploit ris_simu_correct; eauto. - exploit rvf_simu_correct; eauto. - simpl. (* - eexists; split. - + econstructor; eauto. - simpl. - clear SIS. - admit. (* TODO: condition sur les tr_inputs du simu_proof_context ! *) - (* TODO: le rfv_refines est trop sémantique ! *) - + admit. - - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. - inv REF1. inv REF2. inv SEM1. - destruct b; simpl. - + assert (TODO1: rst_refines (bctx1 ctx) rifso1 ifso). admit. - assert (TODO2: rst_refines (bctx2 ctx) rifso2 ifso0). admit. - exploit IHrst_simu1; eauto. - intros (s2 & X1 & X2). - exists s2; split; eauto. - econstructor; eauto. - * assert (TODO3: seval_condition (bctx2 ctx) cond args0 sm0 = Some true). admit. - eauto. - * simpl; eauto. - + admit. - - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. - inv REF1. inv SEM1. -*) - -Admitted. -*) \ No newline at end of file +Admitted. \ No newline at end of file diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 7f00e46f..557541ce 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -235,16 +235,16 @@ Proof. eapply seval_builtin_arg_exact; eauto. Qed. -Fixpoint seval_builtin_sval ctx bsv := +Fixpoint eval_builtin_sval ctx bsv := match bsv with | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v) | BA_splitlong sv1 sv2 => - SOME v1 <- seval_builtin_sval ctx sv1 IN - SOME v2 <- seval_builtin_sval ctx sv2 IN + SOME v1 <- eval_builtin_sval ctx sv1 IN + SOME v2 <- eval_builtin_sval ctx sv2 IN Some (BA_splitlong v1 v2) | BA_addptr sv1 sv2 => - SOME v1 <- seval_builtin_sval ctx sv1 IN - SOME v2 <- seval_builtin_sval ctx sv2 IN + SOME v1 <- eval_builtin_sval ctx sv1 IN + SOME v2 <- eval_builtin_sval ctx sv2 IN Some (BA_addptr v1 v2) | BA_int i => Some (BA_int i) | BA_long l => Some (BA_long l) @@ -259,7 +259,7 @@ Fixpoint seval_builtin_sval ctx bsv := Fixpoint eval_list_builtin_sval ctx lbsv := match lbsv with | nil => Some nil - | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN + | bsv::lbsv => SOME v <- eval_builtin_sval ctx bsv IN SOME lv <- eval_list_builtin_sval ctx lbsv IN Some (v::lv) end. @@ -271,9 +271,9 @@ Proof. destruct lbs2; simpl; repeat autodestruct; congruence. Qed. -Lemma seval_builtin_sval_arg ctx bs: +Lemma eval_builtin_sval_arg ctx bs: forall ba m v, - seval_builtin_sval ctx bs = Some ba -> + eval_builtin_sval ctx bs = Some ba -> eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> seval_builtin_arg ctx m bs v. Proof. @@ -286,14 +286,14 @@ Proof. intros H; inversion H; subst. econstructor; auto. - intros ba m v. - destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. intros H; inversion H; subst; clear H. intros H; inversion H; subst. econstructor; eauto. - intros ba m v. - destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. intros H; inversion H; subst; clear H. intros H; inversion H; subst. econstructor; eauto. @@ -302,7 +302,7 @@ Qed. Lemma seval_builtin_arg_sval ctx m v: forall bs, seval_builtin_arg ctx m bs v -> exists ba, - seval_builtin_sval ctx bs = Some ba + eval_builtin_sval ctx bs = Some ba /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v. Proof. induction 1. @@ -323,7 +323,7 @@ Proof. + constructor; assumption. Qed. -Lemma seval_builtin_sval_args ctx lbs: +Lemma eval_builtin_sval_args ctx lbs: forall lba m v, eval_list_builtin_sval ctx lbs = Some lba -> list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v -> @@ -332,12 +332,12 @@ Proof. unfold seval_builtin_args; induction lbs; simpl; intros lba m v. - intros H; inversion H; subst; clear H. intros H; inversion H. econstructor. - - destruct (seval_builtin_sval _ _) eqn:SV; try congruence. + - destruct (eval_builtin_sval _ _) eqn:SV; try congruence. destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence. intros H; inversion H; subst; clear H. intros H; inversion H; subst; clear H. econstructor; eauto. - eapply seval_builtin_sval_arg; eauto. + eapply eval_builtin_sval_arg; eauto. Qed. Lemma seval_builtin_args_sval ctx m lv: forall lbs, @@ -357,14 +357,14 @@ Proof. + constructor; assumption. Qed. -Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2, +Lemma eval_builtin_sval_correct ctx m: forall bs1 v bs2, seval_builtin_arg ctx m bs1 v -> - (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) -> + (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) -> seval_builtin_arg ctx m bs2 v. Proof. intros. exploit seval_builtin_arg_sval; eauto. intros (ba & X1 & X2). - eapply seval_builtin_sval_arg; eauto. + eapply eval_builtin_sval_arg; eauto. congruence. Qed. @@ -375,7 +375,7 @@ Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1, Proof. intros. exploit seval_builtin_args_sval; eauto. intros (ba & X1 & X2). - eapply seval_builtin_sval_args; eauto. + eapply eval_builtin_sval_args; eauto. congruence. Qed. @@ -1110,19 +1110,19 @@ Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) f2 ct *) 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) + | Ssome_simu sv1 sv2 + (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :optsv_simu ctx (Some sv1) (Some sv2) | Snone_simu: optsv_simu ctx None None . 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) + | Sleft_simu sv1 sv2 + (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :svident_simu ctx (inl sv1) (inl sv2) + | Sright_simu id1 id2 + (IDSIMU: id1 = id2) + :svident_simu ctx (inr id1) (inr id2) . Definition bargs_simu {f1 f2: function} (ctx: simu_proof_context f1 f2) (args1 args2: list (builtin_arg sval)): Prop := @@ -1149,9 +1149,14 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr :sfv_simu ctx (Sreturn osv1) (Sreturn osv2) . +Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop := + forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m. + 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 + exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) + /\ sistate_simu ctx sis1 sis2 + /\ 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). @@ -1182,7 +1187,7 @@ Proof. Qed. *) -(** * Preservation properties *) +(** * Preservation properties under a [simu_proof_context] *) Section SymbValPreserved. @@ -1231,6 +1236,23 @@ Proof. rewrite eval_sval_preserved; auto. Qed. +Lemma eval_builtin_sval_preserved sv: + eval_builtin_sval (bctx1 ctx) sv = eval_builtin_sval (bctx2 ctx) sv. +Proof. + induction sv; simpl; auto. + all: try (erewrite eval_sval_preserved by eauto); trivial. + all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity. +Qed. + +Lemma eval_list_builtin_sval_preserved lsv: + eval_list_builtin_sval (bctx1 ctx) lsv = eval_list_builtin_sval (bctx2 ctx) lsv. +Proof. + induction lsv; simpl; auto. + erewrite eval_builtin_sval_preserved by eauto. + erewrite IHlsv by eauto. + reflexivity. +Qed. + Lemma seval_condition_preserved cond lsv sm: seval_condition (bctx1 ctx) cond lsv sm = seval_condition (bctx2 ctx) cond lsv sm. Proof. @@ -1239,6 +1261,7 @@ Proof. rewrite smem_eval_preserved; auto. Qed. +(* additional preservation properties under this additional hypothesis *) Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). Lemma senv_find_symbol_preserved id: -- cgit