diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:17:04 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:17:04 +0200 |
| commit | 2e7e3340e9739e6317f2fb6049a659d7258aa45b (patch) | |
| tree | abb778df882fa299fbf6d7107108055489d8f591 /backend/Profilingproof.v | |
| parent | e38366c52fc76edbca3e2842375fdab017356427 (diff) | |
| download | compcert-kvx-2e7e3340e9739e6317f2fb6049a659d7258aa45b.tar.gz compcert-kvx-2e7e3340e9739e6317f2fb6049a659d7258aa45b.zip | |
progress in proofs
Diffstat (limited to 'backend/Profilingproof.v')
| -rw-r--r-- | backend/Profilingproof.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index fd905a39..1372c9d9 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -194,7 +194,7 @@ Proof. destruct fd; simpl; trivial. Qed. -Hint Resolve symbols_preserved funsig_preserved : profiling. +Hint Resolve symbols_preserved funsig_preserved external_call_symbols_preserved senv_preserved : profiling. Lemma step_simulation: forall s1 t s2 (STEP : step ge s1 t s2) @@ -254,7 +254,13 @@ Proof. apply find_function_translated with (fd := fd). all: eauto with profiling. + constructor; auto. - - admit. + - econstructor; split. + + apply plus_one. + apply exec_Ibuiltin with (ef:=ef) (args:=args) (vargs:=vargs). + erewrite transf_function_at; eauto. apply I. + apply eval_builtin_args_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. - admit. - admit. - admit. |