From 89aececb825a04dbc1982ec9e61331ef3272c228 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 7 May 2021 13:35:35 +0200 Subject: intermediate lemma for opt_simu intro case --- scheduling/RTLtoBTLproof.v | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 7d58de5a..f5ea9fdc 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -243,6 +243,24 @@ Definition omeasure (oib: option iblock): nat := | Some ib => measure ib end. +Lemma opt_simu_intro + sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1' + (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1') + (STACKS : list_forall2 match_stackframes st st') + (TRANSF : match_function dupmap f f') + (ATpc0 : (fn_code f') ! pcB0 = Some ib0) + (DUPLIC : dupmap ! pcB0 = Some pcR0) + (MIB : match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) + (RIGHTA : is_right_assoc ib) + (RTL_RUN : star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 + (RTL.State st f sp pcR1 rs m)) + (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 = + iblock_istep_run tge sp ib rs m) + : exists (oib : option iblock), + omeasure oib < omeasure (Some ib) /\ + t = E0 /\ match_states oib s1' (State st' f' sp pcB0 rs0 m0). +Admitted. + Theorem opt_simu s1 t s1' oib s2: RTL.step ge s1 t s1' -> match_states oib s1 s2 -> @@ -253,15 +271,8 @@ Theorem opt_simu s1 t s1' oib s2: Proof. inversion 2; subst; clear H0. - (* State *) - inv H. - - 1: { (* Inop *) - eexists; right; split. - 2: split; trivial. - 2: { - econstructor; eauto. - all: admit. } admit. } - all: admit. + exploit opt_simu_intro; eauto. + intros (oib' & SIMU); exists oib'; right; assumption. - (* Callstate *) inv H. + (* Internal function *) @@ -295,7 +306,7 @@ Proof. + econstructor; eauto. eapply code_right_assoc; eauto. constructor. -Admitted. +Qed. Local Hint Resolve plus_one star_refl: core. -- cgit