From 3348c88e1d61d109a8c0388ec421ac6bf17a5c6b Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 4 Jun 2021 09:07:45 +0200 Subject: progress in BTL_SEsimuref --- scheduling/BTL_SEtheory.v | 34 +++++++++++----------------------- 1 file changed, 11 insertions(+), 23 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 557541ce..9ab64d7d 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1064,32 +1064,10 @@ Qed. (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) -(* -Definition equiv_input_regs (f1 f2: BTL.function): Prop := - (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) - /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). - -Lemma equiv_input_regs_union f1 f2: - equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. -Proof. - intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. - generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. - do 2 autodestruct; intuition; try_simplify_someHyps. - intros; exploit EQS; eauto; clear EQS. congruence. -Qed. - -Lemma equiv_input_regs_pre f1 f2 tbl or: - equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. -Proof. - intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. -Qed. -*) - Record simu_proof_context {f1 f2: BTL.function} := Sctx { sge1: BTL.genv; sge2: BTL.genv; sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; - (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *) ssp: val; srs0: regset; sm0: mem @@ -1156,7 +1134,7 @@ Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): 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) /\ sistate_simu ctx sis1 sis2 - /\ sfv_simu ctx sfv1 sfv2 + /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> 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). @@ -1261,6 +1239,16 @@ Proof. rewrite smem_eval_preserved; auto. Qed. +(* TODO: useless ? +Lemma run_sem_isstate_preserved sis: + run_sem_isstate (bctx1 ctx) sis = run_sem_isstate (bctx2 ctx) sis. +Proof. + induction sis; simpl; eauto. + erewrite seval_condition_preserved. + repeat (autodestruct; auto). +Qed. +*) + (* additional preservation properties under this additional hypothesis *) Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). -- cgit