diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:06:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:06:43 +0200 |
| commit | 42f89ff7198a9f088b428944ffdcc3b488571de5 (patch) | |
| tree | 1d8122359528e2e49fbd0e1cffa7137d3e695bef /backend/Profilingproof.v | |
| parent | 3b8f4d59dd831c9e58d3c02faab1a863c2fcbad6 (diff) | |
| download | compcert-kvx-42f89ff7198a9f088b428944ffdcc3b488571de5.tar.gz compcert-kvx-42f89ff7198a9f088b428944ffdcc3b488571de5.zip | |
progress in proofs
Diffstat (limited to 'backend/Profilingproof.v')
| -rw-r--r-- | backend/Profilingproof.v | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index 057be888..630fecbc 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -205,6 +205,27 @@ Proof. * rewrite eval_operation_preserved with (ge1:=ge); eauto with profiling. + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iload with (trap:=trap) (chunk:=chunk) + (addr:=addr) (args:=args) (a:=a). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iload_notrap1 with (chunk:=chunk) + (addr:=addr) (args:=args). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iload_notrap2 with (chunk:=chunk) + (addr:=addr) (args:=args) (a:=a). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. - admit. - admit. - admit. @@ -214,9 +235,10 @@ Proof. - admit. - admit. - admit. - - admit. - - admit. - - admit. + - inv STACKS. inv H1. + econstructor; split. + + apply plus_one. apply exec_return. + + constructor; auto. Admitted. (* |