diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-29 10:04:11 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-29 10:04:11 +0100 |
commit | af0f6f7689fa3520290a4e2ee8d8ea72786f8150 (patch) | |
tree | d6cde08cc303623edad2a7033a78c44c46e806b6 /src/translation/Veriloggenproof.v | |
parent | 4c475a386caeaee3e3ef7682840c738cecdee941 (diff) | |
parent | 0c360ec297c42d73c1090958d061447c2bfbe31b (diff) | |
download | vericert-kvx-af0f6f7689fa3520290a4e2ee8d8ea72786f8150.tar.gz vericert-kvx-af0f6f7689fa3520290a4e2ee8d8ea72786f8150.zip |
Merge branch 'develop' into dev-nadesh
Diffstat (limited to 'src/translation/Veriloggenproof.v')
-rw-r--r-- | src/translation/Veriloggenproof.v | 58 |
1 files changed, 54 insertions, 4 deletions
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 6c58c56..db96949 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -16,16 +16,66 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import Smallstep. -From coqup Require HTL Verilog. +From compcert Require Import Smallstep Linking. +From coqup Require HTL. +From coqup Require Import Coquplib Veriloggen Verilog. + +Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := + match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + +Lemma transf_program_match: + forall prog, match_prog prog (transl_program prog). +Proof. + intros. eapply match_transform_program_contextual. auto. +Qed. + +Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := +| match_stack : + forall res m pc reg_assoc arr_assoc hstk vstk, + match_stacks hstk vstk -> + match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) + (Stackframe res (transl_module m) pc + reg_assoc arr_assoc :: vstk) +| match_stack_nil : match_stacks nil nil. + +Inductive match_states : HTL.state -> state -> Prop := +| match_state : + forall m st reg_assoc arr_assoc hstk vstk, + match_stacks hstk vstk -> + match_states (HTL.State hstk m st reg_assoc arr_assoc) + (State vstk (transl_module m) st reg_assoc arr_assoc) +| match_returnstate : + forall v hstk vstk, + match_stacks hstk vstk -> + match_states (HTL.Returnstate hstk v) (Returnstate vstk v) +| match_initial_call : + forall m, + match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). Section CORRECTNESS. Variable prog: HTL.program. - Variable tprog: Verilog.program. + Variable tprog: program. + + Hypothesis TRANSL : match_prog prog tprog. + + Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + + Theorem transl_step_correct : + forall (S1 : HTL.state) t S2, + HTL.step ge S1 t S2 -> + forall (R1 : state), + match_states S1 R1 -> + exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. + - apply Smallstep.plus_one. econstructor. eassumption. trivial. + * econstructor. econstructor. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). - Admitted. + End CORRECTNESS. + |