From cc5f8c4e4d71d824a4d1818745d6bf1015b98f98 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 3 May 2021 13:55:15 +0200 Subject: une autre suggestion --- scheduling/BTLtoRTLproof.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 7f6f21c7..ab3cab69 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -106,6 +106,20 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. +(* suggestion *) +Lemma iblock_stepi_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin + (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin): + forall cfg' pc0 opc isfst + (MIB: match_iblock dupmap cfg' isfst pc0 ib opc) + , + match ofin with + | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) + | Some fin => True (* TODO: A CHANGER *) + end. +Proof. + induction IBIS; simpl; auto. +Admitted. + Inductive iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg: state -> trace -> bool -> option final -> option node -> Prop := | ibis_synced ib rs1 m1 opc pc1 (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 None) -- cgit