diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:21:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:21:30 +0200 |
| commit | 44e48a67a58a171ca29f22e15429b1baaf64ae81 (patch) | |
| tree | 2f4b3c571e98fac79ef0e6ae74f088216c0c582f /backend/Profilingproof.v | |
| parent | 2e7e3340e9739e6317f2fb6049a659d7258aa45b (diff) | |
| download | compcert-kvx-44e48a67a58a171ca29f22e15429b1baaf64ae81.tar.gz compcert-kvx-44e48a67a58a171ca29f22e15429b1baaf64ae81.zip | |
progress in proofs
Diffstat (limited to 'backend/Profilingproof.v')
| -rw-r--r-- | backend/Profilingproof.v | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index 1372c9d9..ed07443c 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -194,7 +194,14 @@ Proof. destruct fd; simpl; trivial. Qed. -Hint Resolve symbols_preserved funsig_preserved external_call_symbols_preserved senv_preserved : profiling. +Lemma stacksize_preserved: + forall f, + fn_stacksize (transf_function f) = fn_stacksize f. +Proof. + destruct f; simpl; trivial. +Qed. + +Hint Resolve symbols_preserved funsig_preserved external_call_symbols_preserved senv_preserved stacksize_preserved : profiling. Lemma step_simulation: forall s1 t s2 (STEP : step ge s1 t s2) @@ -262,8 +269,19 @@ Proof. all: eauto with profiling. + constructor; auto. - admit. - - admit. - - admit. + - econstructor; split. + + apply plus_one. + apply exec_Ijumptable with (arg:=arg) (tbl:=tbl) (n:=n). + erewrite transf_function_at; eauto. apply I. + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. + apply exec_Ireturn. + erewrite transf_function_at; eauto. apply I. + rewrite stacksize_preserved. + eassumption. + + constructor; auto. - admit. - admit. - inv STACKS. inv H1. |