diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 18:43:08 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 18:43:08 +0200 |
| commit | 3b8f4d59dd831c9e58d3c02faab1a863c2fcbad6 (patch) | |
| tree | c885a8c70421cd12abf38c0e496094e5e4886c01 /backend/Profilingproof.v | |
| parent | 0ef40fc8a82aa7bd92f612b96324ffa58e839151 (diff) | |
| download | compcert-kvx-3b8f4d59dd831c9e58d3c02faab1a863c2fcbad6.tar.gz compcert-kvx-3b8f4d59dd831c9e58d3c02faab1a863c2fcbad6.zip | |
progress in proofs
Diffstat (limited to 'backend/Profilingproof.v')
| -rw-r--r-- | backend/Profilingproof.v | 24 |
1 files changed, 24 insertions, 0 deletions
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. (* |