From 764b167efe9edb3d0d20e8ea37263320c42f3036 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 11:22:56 +0200 Subject: transf_function_inj_plusstep --- backend/Injectproof.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'backend/Injectproof.v') diff --git a/backend/Injectproof.v b/backend/Injectproof.v index c3382d72..51d049b1 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -953,5 +953,30 @@ Section INJECTOR. lia. Qed. + Lemma transf_function_inj_plusstep : + forall ts f tf sp m inj_n src_pc inj_pc inj_code i + (FUN : transf_function gen_injections f = OK tf) + (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + Some (src_pc, inj_code)) + (SRC: (fn_code f) ! src_pc = Some i) + (POSITION : inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) inj_n = inj_pc) + (trs : regset), + exists trs', + match_regs (f : function) trs trs' /\ + Smallstep.plus RTL.step ge + (State ts tf sp inj_pc trs m) E0 + (State ts tf sp (successor i) trs' m). + Proof. + intros. + destruct (transf_function_inj_starstep ts f tf sp m inj_n src_pc inj_pc inj_code FUN INJ POSITION trs) as [trs' [MATCH PLUS]]. + exists trs'. + split. assumption. + eapply Smallstep.plus_right. + exact PLUS. + eapply transf_function_inj_end; eassumption. + reflexivity. + Qed. + End PRESERVATION. End INJECTOR. -- cgit