From 3b8f4d59dd831c9e58d3c02faab1a863c2fcbad6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 18:43:08 +0200 Subject: progress in proofs --- backend/Profilingproof.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'backend/Profilingproof.v') diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index 6c85f6a1..057be888 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -187,12 +187,36 @@ Inductive match_states: RTL.state -> RTL.state -> Prop := match_states (Returnstate stk v m) (Returnstate stk' v m). +Hint Resolve symbols_preserved : profiling. + Lemma step_simulation: forall s1 t s2 (STEP : step ge s1 t s2) s1' (MS: match_states s1 s1'), exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. Proof. induction 1; intros; inv MS. + - econstructor; split. + + apply plus_one. apply exec_Inop. + erewrite transf_function_at; eauto. apply I. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iop with (op:=op) (args:=args). + * erewrite transf_function_at; eauto. apply I. + * rewrite eval_operation_preserved with (ge1:=ge); + eauto with profiling. + + constructor; auto. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. Admitted. (* -- cgit