From 445aabbcf63e29d68dd0c98dde7f259af0381591 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 25 Jun 2020 09:09:23 +0100 Subject: Work on Veriloggen proof --- src/translation/Veriloggenproof.v | 52 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 50 insertions(+), 2 deletions(-) (limited to 'src/translation/Veriloggenproof.v') diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 6c58c56..825cb7e 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -16,16 +16,64 @@ * along with this program. If not, see . *) -From compcert Require Import Smallstep. +From compcert Require Import Smallstep Linking. +From coqup Require Import Veriloggen. From coqup Require HTL 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 Verilog.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) + (Verilog.Stackframe res (transl_module m) pc + reg_assoc arr_assoc :: vstk) +| match_stack_nil : match_stacks nil nil. + +Inductive match_states : HTL.state -> Verilog.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) + (Verilog.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) (Verilog.Returnstate vstk v) +| match_initial_call : + forall m, + match_states (HTL.Callstate nil m nil) (Verilog.Callstate nil (transl_module m) nil). + Section CORRECTNESS. Variable prog: HTL.program. Variable tprog: Verilog.program. + Hypothesis TRANSL : match_prog prog tprog. + + Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : Verilog.genv := Globalenvs.Genv.globalenv tprog. + + Theorem transl_step_correct: + forall (S1 : HTL.state) t S2, + HTL.step ge S1 t S2 -> + forall (R1 : Verilog.state), + match_states S1 R1 -> + exists R2, Smallstep.plus Verilog.step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; intros R1 MSTATE. + Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). - Admitted. + End CORRECTNESS. + -- cgit From cf9949a5151aa9ed86554fb31c2a56fad0614a10 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 25 Jun 2020 18:04:49 +0100 Subject: Progress on proof of Veriloggen --- src/translation/Veriloggenproof.v | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) (limited to 'src/translation/Veriloggenproof.v') diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 825cb7e..e556c69 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -17,8 +17,8 @@ *) From compcert Require Import Smallstep Linking. -From coqup Require Import Veriloggen. -From coqup Require HTL Verilog. +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. @@ -29,47 +29,52 @@ Proof. intros. eapply match_transform_program_contextual. auto. Qed. -Inductive match_stacks : list HTL.stackframe -> list Verilog.stackframe -> Prop := +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) - (Verilog.Stackframe res (transl_module m) pc + (Stackframe res (transl_module m) pc reg_assoc arr_assoc :: vstk) | match_stack_nil : match_stacks nil nil. -Inductive match_states : HTL.state -> Verilog.state -> Prop := +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) - (Verilog.State vstk (transl_module 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) (Verilog.Returnstate vstk v) + match_states (HTL.Returnstate hstk v) (Returnstate vstk v) | match_initial_call : forall m, - match_states (HTL.Callstate nil m nil) (Verilog.Callstate nil (transl_module m) nil). + 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 : Verilog.genv := Globalenvs.Genv.globalenv tprog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. - Theorem transl_step_correct: + Lemma stmnt_in_case : + exists e st, + + Theorem transl_step_correct : forall (S1 : HTL.state) t S2, HTL.step ge S1 t S2 -> - forall (R1 : Verilog.state), + forall (R1 : state), match_states S1 R1 -> - exists R2, Smallstep.plus Verilog.step tge R1 t R2 /\ match_states S2 R2. + exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; intros R1 MSTATE. + induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. + - apply Smallstep.plus_one. econstructor. econstructor. + * econstructor. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). -- cgit From 50ec2fb12454c2bc1f902c955f0b81df71b58c39 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 26 Jun 2020 09:40:16 +0100 Subject: Fix Verilog semantics and fix order of always blocks --- src/translation/Veriloggenproof.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'src/translation/Veriloggenproof.v') diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index e556c69..db96949 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -62,9 +62,6 @@ Section CORRECTNESS. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : genv := Globalenvs.Genv.globalenv tprog. - Lemma stmnt_in_case : - exists e st, - Theorem transl_step_correct : forall (S1 : HTL.state) t S2, HTL.step ge S1 t S2 -> @@ -73,8 +70,8 @@ Section CORRECTNESS. 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. econstructor. - * econstructor. + - apply Smallstep.plus_one. econstructor. eassumption. trivial. + * econstructor. econstructor. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). -- cgit