diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-05-23 09:38:17 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-05-23 09:38:17 +0100 |
commit | 69a61d57f53b56f4efa0c78054aad9fce56f0422 (patch) | |
tree | d2e820832b3b39387014027542318884ee438f43 | |
parent | 8a944ab3c58854f19197745f1b3c1f9ea6c3093f (diff) | |
download | vericert-69a61d57f53b56f4efa0c78054aad9fce56f0422.tar.gz vericert-69a61d57f53b56f4efa0c78054aad9fce56f0422.zip |
Add very top-level proof
-rw-r--r-- | src/hls/RTLPargenproof.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index e0c20c1..c610ff0 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -343,4 +343,37 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. } Qed. + Lemma transl_initial_states: + forall S, + RTLBlock.initial_state prog S -> + exists R, RTLPar.initial_state tprog R /\ match_states S R. + Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + econstructor; split. + econstructor. apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply match_program_main; eauto. + eexact A. + rewrite <- H2. apply sig_transl_function; auto. + constructor. auto. constructor. + Qed. + + Lemma transl_final_states: + forall S R r, + match_states S R -> RTLBlock.final_state S r -> RTLPar.final_state R r. + Proof. + intros. inv H0. inv H. inv STACKS. constructor. + Qed. + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTLBlock.semantics prog) (RTLPar.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus. + apply senv_preserved. + eexact transl_initial_states. + eexact transl_final_states. + exact transl_step_correct. + Qed. + End CORRECTNESS. |