diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-02 01:57:46 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-02 01:57:46 +0100 |
| commit | 89bc64204b4d99cb7dc9eacb1ecdf26b30dc26a0 (patch) | |
| tree | f5403d3853c8d0863b9f7f29e8efcf8f7d598e87 /src/translation/HTLgenproof.v | |
| parent | aa28022035b16417aaafa36a450461c5133a44b4 (diff) | |
| download | vericert-kvx-89bc64204b4d99cb7dc9eacb1ecdf26b30dc26a0.tar.gz vericert-kvx-89bc64204b4d99cb7dc9eacb1ecdf26b30dc26a0.zip | |
Fix spec by adding details about reg vals
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 6e470d5..5b393a0 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -86,18 +86,6 @@ Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_frames_nil : match_frames nil nil. -(* | match_frames_cons : *) -(* forall cs lr r f sp sp' pc rs m asr asa *) -(* (TF : tr_module f m) *) -(* (ST: match_frames mem cs lr) *) -(* (MA: match_assocmaps f rs asr) *) -(* (MARR : match_arrs m f sp mem asa) *) -(* (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) *) -(* (RSBP: reg_stack_based_pointers sp' rs) *) -(* (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) *) -(* (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), *) -(* match_frames mem (RTL.Stackframe r f sp pc rs :: cs) *) -(* (HTL.Stackframe r m pc asr asa :: lr). *) Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem m st res @@ -2098,7 +2086,6 @@ Section CORRECTNESS. trivial. symmetry; eapply Linking.match_program_main; eauto. Qed. - (* Had to admit proof because currently there is no way to force main to be Internal. *) Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), Smallstep.initial_state (RTL.semantics prog) s1 -> @@ -2119,7 +2106,7 @@ Section CORRECTNESS. repeat (unfold_match B). inversion B. subst. exploit main_tprog_internal; eauto; intros. rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). - apply Heqo. symmetry; eapply Linking.match_program_main; eauto. + Apply Heqo. symmetry; eapply Linking.match_program_main; eauto. inversion H5. econstructor; split. econstructor. apply (Genv.init_mem_transf_partial TRANSL'); eauto. |