From 492a71c60c0dbc810f50b75bdf820c2acfc88d7d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 9 Jun 2021 18:45:26 +0200 Subject: fix sstate_simu --- scheduling/BTL_SEtheory.v | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 97dc7fc8..9074b071 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1137,8 +1137,24 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr 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. + +Record si_ok ctx (sis: sistate): Prop := { + OK_PRE: (sis.(si_pre) ctx); + OK_SMEM: eval_smem ctx sis.(si_smem) <> None; + OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None +}. + +Lemma sem_si_ok ctx sis rs m: + sem_sistate ctx sis rs m -> si_ok ctx sis. +Proof. + unfold sem_sistate; + econstructor; + intuition congruence. +Qed. + + 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) -> + forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 -> exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) /\ sistate_simu ctx sis1 sis2 /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2) -- cgit