Vericert is the first formally verified high-level synthesis tool.
Table of Contents
This is the top-level module of the correctness proof and proves the final backwards simulation correct.
We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end.
From vericert Require Import HTLgenproof. From compcert.common Require Import Errors Linking. From compcert.lib Require Import Coqlib. From compcert.backend Require Selection RTL RTLgen Tailcall Inlining Renumber Constprop CSE Deadcode Unusedglob. From compcert.cfrontend Require Csyntax SimplExpr SimplLocals Cshmgen Cminorgen. From compcert.driver Require Compiler. From vericert Require Verilog Veriloggen Veriloggenproof HTLgen RTLBlock RTLBlockgen HTLSchedulegen. From compcert Require Import Smallstep.
We then need to declare the external OCaml functions used to print out intermediate steps in the compilation, such as print_RTL, print_HTL and print_RTLBlock.
Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. Parameter print_RTLBlock: RTLBlock.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog.forall (A : Type) (printer : A -> unit) (prog : A), print printer prog = progforall (A : Type) (printer : A -> unit) (prog : A), print printer prog = progdestruct (printer prog); auto. Qed.A:Typeprinter:A -> unitprog:Aprog = prog
We also declare some new notation, which is also used in CompCert to combine the monadic results of each pass.
Notation "a @@@ b" := (Compiler.apply_partial _ _ a b) (at level 50, left associativity). Notation "a @@ b" := (Compiler.apply_total _ _ a b) (at level 50, left associativity).
As printing is used in the translation but does not change the output, we need to prove that it has no effect so that it can be removed during the proof.
forall (A : Type) (x : res A) (f : A -> unit), x @@ print f = xforall (A : Type) (x : res A) (f : A -> unit), x @@ print f = xA:Typex:res Af:A -> unitx @@ print f = xA:Typea:Af:A -> unitOK (print f a) = OK aA:Typee:errmsgf:A -> unitError e = Error eA:Typea:Af:A -> unitOK a = OK aA:Typee:errmsgf:A -> unitError e = Error eauto. Qed.A:Typee:errmsgf:A -> unitError e = Error e
Finally, some optimisation passes are only activated by a flag, which is handled by the following functions for partial and total passes.
Definition total_if {A: Type} (flag: unit -> bool) (f: A -> A) (prog: A) : A := if flag tt then f prog else prog. Definition partial_if {A: Type} (flag: unit -> bool) (f: A -> res A) (prog: A) : res A := if flag tt then f prog else OK prog. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
An optimised transformation function from RTL to Verilog can then be defined, which applies the front end compiler optimisations of CompCert to the RTL that is generated and then performs the two Vericert passes from RTL to HTL and then from HTL to Verilog.
Definition transf_backend_opt (r : RTL.program) : res Verilog.program := OK r @@@ Inlining.transf_program @@ print (print_RTL 1) @@ Renumber.transf_program @@ print (print_RTL 2) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 3) @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 4) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 5) @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 6) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r @@@ Inlining.transf_program @@ print (print_RTL 1) @@ Renumber.transf_program @@ print (print_RTL 2) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program.
The transformation functions from RTL to Verilog are then added to the backend of the CompCert transformations from Clight to RTL.
Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend. Definition transf_hls_opt (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend_opt.
Finally, the top-level definition for all the passes is defined, which combines the match_prog predicates of each translation pass from C until Verilog.
Local Open Scope linking_scope. Definition CompCert's_passes := mkpass SimplExprproof.match_prog ::: mkpass SimplLocalsproof.match_prog ::: mkpass Cshmgenproof.match_prog ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _.
These passes are then composed into a larger, top-level match_prog predicate which matches a C program directly with a Verilog program.
Definition match_prog: Csyntax.program -> Verilog.program -> Prop :=
pass_match (compose_passes CompCert's_passes).
We then need to prove that this predicate holds, assuming that the translation is performed using the transf_hls function declared above.
forall (p : Csyntax.program) (tp : Verilog.program), transf_hls p = OK tp -> match_prog p tpforall (p : Csyntax.program) (tp : Verilog.program), transf_hls p = OK tp -> match_prog p tpp:Csyntax.programtp:Verilog.programT:transf_hls p = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programT:OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programT:SimplExpr.transl_program p @@@ SimplLocals.transf_program @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1T:SimplLocals.transf_program p1 @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2T:Cshmgen.transl_program p2 @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3T:Cminorgen.transl_program p3 @@@ Selection.sel_program @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4T:Selection.sel_program p4 @@@ RTLgen.transl_program @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5T:RTLgen.transl_program p5 @@ print (print_RTL 0) @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5T:RTLgen.transl_program p5 @@@ transf_backend = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6T:transf_backend p6 = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6T:OK p6 @@@ Inlining.transf_program @@ print (print_RTL 1) @@ Renumber.transf_program @@ print (print_RTL 2) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6T:Inlining.transf_program p6 @@ print (print_RTL 1) @@ Renumber.transf_program @@ print (print_RTL 2) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6T:Inlining.transf_program p6 @@ Renumber.transf_program @@@ HTLgen.transl_program @@ Veriloggen.transl_program = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7T:HTLgen.transl_program (Renumber.transf_program p7) @@ Veriloggen.transl_program = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programT:HTLgen.transl_program p8 @@ Veriloggen.transl_program = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9T:OK (Veriloggen.transl_program p9) = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpmatch_prog p tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Clight.program, SimplExprproof.match_prog p p2 /\ (exists p3 : Clight.program, SimplLocalsproof.match_prog p2 p3 /\ (exists p4 : Csharpminor.program, Cshmgenproof.match_prog p3 p4 /\ (exists p5 : Cminor.program, Cminorgenproof.match_prog p4 p5 /\ (exists p6 : CminorSel.program, Selectionproof.match_prog p5 p6 /\ (exists p7 : RTL.program, RTLgenproof.match_prog p6 p7 /\ (exists p8 : RTL.program, Inliningproof.match_prog p7 p8 /\ (exists p9 : RTL.program, Renumberproof.match_prog p8 p9 /\ (exists p10 : HTL.program, HTLgenproof.match_prog p9 p10 /\ (...)))))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpSimplExprproof.match_prog p p1p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Clight.program, SimplLocalsproof.match_prog p1 p2 /\ (exists p3 : Csharpminor.program, Cshmgenproof.match_prog p2 p3 /\ (exists p4 : Cminor.program, Cminorgenproof.match_prog p3 p4 /\ (exists p5 : CminorSel.program, Selectionproof.match_prog p4 p5 /\ (exists p6 : RTL.program, RTLgenproof.match_prog p5 p6 /\ (exists p7 : RTL.program, Inliningproof.match_prog p6 p7 /\ (exists p8 : RTL.program, Renumberproof.match_prog p7 p8 /\ (exists p9 : HTL.program, HTLgenproof.match_prog p8 p9 /\ (exists p10 : Verilog.program, Veriloggenproof.match_prog p9 p10 /\ p10 = tp))))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Clight.program, SimplLocalsproof.match_prog p1 p2 /\ (exists p3 : Csharpminor.program, Cshmgenproof.match_prog p2 p3 /\ (exists p4 : Cminor.program, Cminorgenproof.match_prog p3 p4 /\ (exists p5 : CminorSel.program, Selectionproof.match_prog p4 p5 /\ (exists p6 : RTL.program, RTLgenproof.match_prog p5 p6 /\ (exists p7 : RTL.program, Inliningproof.match_prog p6 p7 /\ (exists p8 : RTL.program, Renumberproof.match_prog p7 p8 /\ (exists p9 : HTL.program, HTLgenproof.match_prog p8 p9 /\ (exists p10 : Verilog.program, Veriloggenproof.match_prog p9 p10 /\ p10 = tp))))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpSimplLocalsproof.match_prog p1 p2p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p3 : Csharpminor.program, Cshmgenproof.match_prog p2 p3 /\ (exists p2 : Cminor.program, Cminorgenproof.match_prog p3 p2 /\ (exists p4 : CminorSel.program, Selectionproof.match_prog p2 p4 /\ (exists p5 : RTL.program, RTLgenproof.match_prog p4 p5 /\ (exists p6 : RTL.program, Inliningproof.match_prog p5 p6 /\ (exists p7 : RTL.program, Renumberproof.match_prog p6 p7 /\ (exists p8 : HTL.program, HTLgenproof.match_prog p7 p8 /\ (exists p9 : Verilog.program, Veriloggenproof.match_prog p8 p9 /\ p9 = tp)))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p3 : Csharpminor.program, Cshmgenproof.match_prog p2 p3 /\ (exists p2 : Cminor.program, Cminorgenproof.match_prog p3 p2 /\ (exists p4 : CminorSel.program, Selectionproof.match_prog p2 p4 /\ (exists p5 : RTL.program, RTLgenproof.match_prog p4 p5 /\ (exists p6 : RTL.program, Inliningproof.match_prog p5 p6 /\ (exists p7 : RTL.program, Renumberproof.match_prog p6 p7 /\ (exists p8 : HTL.program, HTLgenproof.match_prog p7 p8 /\ (exists p9 : Verilog.program, Veriloggenproof.match_prog p8 p9 /\ p9 = tp)))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpCshmgenproof.match_prog p2 p3p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Cminor.program, Cminorgenproof.match_prog p3 p2 /\ (exists p3 : CminorSel.program, Selectionproof.match_prog p2 p3 /\ (exists p4 : RTL.program, RTLgenproof.match_prog p3 p4 /\ (exists p5 : RTL.program, Inliningproof.match_prog p4 p5 /\ (exists p6 : RTL.program, Renumberproof.match_prog p5 p6 /\ (exists p7 : HTL.program, HTLgenproof.match_prog p6 p7 /\ (exists p8 : Verilog.program, Veriloggenproof.match_prog p7 p8 /\ p8 = tp))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Cminor.program, Cminorgenproof.match_prog p3 p2 /\ (exists p3 : CminorSel.program, Selectionproof.match_prog p2 p3 /\ (exists p4 : RTL.program, RTLgenproof.match_prog p3 p4 /\ (exists p5 : RTL.program, Inliningproof.match_prog p4 p5 /\ (exists p6 : RTL.program, Renumberproof.match_prog p5 p6 /\ (exists p7 : HTL.program, HTLgenproof.match_prog p6 p7 /\ (exists p8 : Verilog.program, Veriloggenproof.match_prog p7 p8 /\ p8 = tp))))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpCminorgenproof.match_prog p3 p4p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : CminorSel.program, Selectionproof.match_prog p4 p2 /\ (exists p3 : RTL.program, RTLgenproof.match_prog p2 p3 /\ (exists p4 : RTL.program, Inliningproof.match_prog p3 p4 /\ (exists p5 : RTL.program, Renumberproof.match_prog p4 p5 /\ (exists p6 : HTL.program, HTLgenproof.match_prog p5 p6 /\ (exists p7 : Verilog.program, Veriloggenproof.match_prog p6 p7 /\ p7 = tp)))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : CminorSel.program, Selectionproof.match_prog p4 p2 /\ (exists p3 : RTL.program, RTLgenproof.match_prog p2 p3 /\ (exists p4 : RTL.program, Inliningproof.match_prog p3 p4 /\ (exists p5 : RTL.program, Renumberproof.match_prog p4 p5 /\ (exists p6 : HTL.program, HTLgenproof.match_prog p5 p6 /\ (exists p7 : Verilog.program, Veriloggenproof.match_prog p6 p7 /\ p7 = tp)))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpSelectionproof.match_prog p4 p5p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : RTL.program, RTLgenproof.match_prog p5 p2 /\ (exists p3 : RTL.program, Inliningproof.match_prog p2 p3 /\ (exists p4 : RTL.program, Renumberproof.match_prog p3 p4 /\ (exists p5 : HTL.program, HTLgenproof.match_prog p4 p5 /\ (exists p6 : Verilog.program, Veriloggenproof.match_prog p5 p6 /\ p6 = tp))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : RTL.program, RTLgenproof.match_prog p5 p2 /\ (exists p3 : RTL.program, Inliningproof.match_prog p2 p3 /\ (exists p4 : RTL.program, Renumberproof.match_prog p3 p4 /\ (exists p5 : HTL.program, HTLgenproof.match_prog p4 p5 /\ (exists p6 : Verilog.program, Veriloggenproof.match_prog p5 p6 /\ p6 = tp))))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpRTLgenproof.match_prog p5 p6p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : RTL.program, Inliningproof.match_prog p6 p2 /\ (exists p3 : RTL.program, Renumberproof.match_prog p2 p3 /\ (exists p4 : HTL.program, HTLgenproof.match_prog p3 p4 /\ (exists p5 : Verilog.program, Veriloggenproof.match_prog p4 p5 /\ p5 = tp)))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : RTL.program, Inliningproof.match_prog p6 p2 /\ (exists p3 : RTL.program, Renumberproof.match_prog p2 p3 /\ (exists p4 : HTL.program, HTLgenproof.match_prog p3 p4 /\ (exists p5 : Verilog.program, Veriloggenproof.match_prog p4 p5 /\ p5 = tp)))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpInliningproof.match_prog p6 p7p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : RTL.program, Renumberproof.match_prog p7 p2 /\ (exists p3 : HTL.program, HTLgenproof.match_prog p2 p3 /\ (exists p4 : Verilog.program, Veriloggenproof.match_prog p3 p4 /\ p4 = tp))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : RTL.program, Renumberproof.match_prog p7 p2 /\ (exists p3 : HTL.program, HTLgenproof.match_prog p2 p3 /\ (exists p4 : Verilog.program, Veriloggenproof.match_prog p3 p4 /\ p4 = tp))p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpRenumberproof.match_prog p7 p8p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : HTL.program, HTLgenproof.match_prog p8 p2 /\ (exists p3 : Verilog.program, Veriloggenproof.match_prog p2 p3 /\ p3 = tp)p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : HTL.program, HTLgenproof.match_prog p8 p2 /\ (exists p3 : Verilog.program, Veriloggenproof.match_prog p2 p3 /\ p3 = tp)p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpHTLgenproof.match_prog p8 p9p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Verilog.program, Veriloggenproof.match_prog p9 p2 /\ p2 = tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpexists p2 : Verilog.program, Veriloggenproof.match_prog p9 p2 /\ p2 = tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpVeriloggenproof.match_prog p9 p10p:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpp10 = tpp:Csyntax.programtp:Verilog.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programT:OK p10 = OK tpp10 = tpreflexivity. Qed.p:Csyntax.programp1:Clight.programP1:SimplExpr.transl_program p = OK p1p2:Clight.programP2:SimplLocals.transf_program p1 = OK p2p3:Csharpminor.programP3:Cshmgen.transl_program p2 = OK p3p4:Cminor.programP4:Cminorgen.transl_program p3 = OK p4p5:CminorSel.programP5:Selection.sel_program p4 = OK p5p6:RTL.programP6:RTLgen.transl_program p5 = OK p6p7:RTL.programP7:Inlining.transf_program p6 = OK p7p8:=Renumber.transf_program p7:RTL.programp9:HTL.programP9:HTLgen.transl_program p8 = OK p9p10:=Veriloggen.transl_program p9:Verilog.programp10 = p10forall sem : semantics, forward_simulation sem semforall sem : semantics, forward_simulation sem semsem:semanticsforward_simulation sem semsem:semanticsid:AST.identGlobalenvs.Senv.public_symbol (symbolenv sem) id = Globalenvs.Senv.public_symbol (symbolenv sem) idsem:semanticss1:state semH:initial_state sem s1exists s2 : state sem, initial_state sem s2 /\ s2 = s1sem:semanticss1, s2:state semr:Integers.Int.intH:s2 = s1H0:final_state sem s1 rfinal_state sem s2 rsem:semanticss1:state semt:Events.traces1':state semH:Step sem s1 t s1's2:state semH0:s2 = s1exists s2' : state sem, Step sem s2 t s2' /\ s2' = s1'auto.sem:semanticsid:AST.identGlobalenvs.Senv.public_symbol (symbolenv sem) id = Globalenvs.Senv.public_symbol (symbolenv sem) idexists s1; auto.sem:semanticss1:state semH:initial_state sem s1exists s2 : state sem, initial_state sem s2 /\ s2 = s1subst s2; auto.sem:semanticss1, s2:state semr:Integers.Int.intH:s2 = s1H0:final_state sem s1 rfinal_state sem s2 rsem:semanticss1:state semt:Events.traces1':state semH:Step sem s1 t s1's2:state semH0:s2 = s1exists s2' : state sem, Step sem s2 t s2' /\ s2' = s1'exists s1'; auto. Qed.sem:semanticss1:state semt:Events.traces1':state semH:Step sem s1 t s1'exists s2' : state sem, Step sem s1 t s2' /\ s2' = s1'forall (p : Csyntax.program) (tp : Verilog.program), match_prog p tp -> forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)forall (p : Csyntax.program) (tp : Verilog.program), match_prog p tp -> forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programM:match_prog p tpforward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programM:exists p2 : Clight.program, SimplExprproof.match_prog p p2 /\ (exists p3 : Clight.program, SimplLocalsproof.match_prog p2 p3 /\ (exists p4 : Csharpminor.program, Cshmgenproof.match_prog p3 p4 /\ (exists p5 : Cminor.program, Cminorgenproof.match_prog p4 p5 /\ (exists p6 : CminorSel.program, Selectionproof.match_prog p5 p6 /\ (exists p7 : RTL.program, RTLgenproof.match_prog p6 p7 /\ (exists p8 : RTL.program, Inliningproof.match_prog p7 p8 /\ (exists p9 : RTL.program, Renumberproof.match_prog p8 p9 /\ (exists p10 : HTL.program, HTLgenproof.match_prog p9 p10 /\ (...)))))))))forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programM:exists p2 : Clight.program, SimplExprproof.match_prog p p2 /\ (exists p3 : Clight.program, SimplLocalsproof.match_prog p2 p3 /\ (exists p4 : Csharpminor.program, Cshmgenproof.match_prog p3 p4 /\ (exists p5 : Cminor.program, Cminorgenproof.match_prog p4 p5 /\ (exists p6 : CminorSel.program, Selectionproof.match_prog p5 p6 /\ (exists p7 : RTL.program, RTLgenproof.match_prog p6 p7 /\ (exists p8 : RTL.program, Inliningproof.match_prog p7 p8 /\ (exists p9 : RTL.program, Renumberproof.match_prog p8 p9 /\ (exists p10 : HTL.program, HTLgenproof.match_prog p9 p10 /\ (...)))))))))forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10MM0:p10 = tpforward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Clight.semantics1 p0) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Clight.semantics2 p1) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Csharpminor.semantics p3) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (Cminor.semantics p4) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (CminorSel.semantics p5) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (RTL.semantics p6) (Verilog.semantics p10)eapply compose_forward_simulations.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (RTL.semantics p7) (Verilog.semantics p10)eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (RTL.semantics p8) (Verilog.semantics p10)eapply Veriloggenproof.transf_program_correct; eassumption.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10forward_simulation (HTL.semantics p9) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10) /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)forward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)receptive (atomic (Cstrategy.semantics p))p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)single_events (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)receptive (atomic (Cstrategy.semantics p))p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)single_events (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)receptive (atomic (Cstrategy.semantics p))p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)receptive (atomic (Cstrategy.semantics p))p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)receptive (atomic (Cstrategy.semantics p))p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)strongly_receptive (Cstrategy.semantics p)p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)apply Verilog.semantics_determinate. Qed.p:Csyntax.programp0:Clight.programM0:SimplExprproof.match_prog p p0p1:Clight.programM:SimplLocalsproof.match_prog p0 p1p3:Csharpminor.programM1:Cshmgenproof.match_prog p1 p3p4:Cminor.programM2:Cminorgenproof.match_prog p3 p4p5:CminorSel.programM3:Selectionproof.match_prog p4 p5p6:RTL.programM4:RTLgenproof.match_prog p5 p6p7:RTL.programM5:Inliningproof.match_prog p6 p7p8:RTL.programM6:Renumberproof.match_prog p7 p8p9:HTL.programM7:HTLgenproof.match_prog p8 p9p10:Verilog.programM8:Veriloggenproof.match_prog p9 p10F:forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)determinate (Verilog.semantics p10)
The following theorem is a backward simulation between the C and Verilog, which proves the semantics preservation of the translation. We can assume that the C and Verilog programs match, as we have proven previously in transf_hls_match that our translation implies that the match_prog predicate will hold.
forall (p : Csyntax.program) (tp : Verilog.program), match_prog p tp -> backward_simulation (Csem.semantics p) (Verilog.semantics tp)forall (p : Csyntax.program) (tp : Verilog.program), match_prog p tp -> backward_simulation (Csem.semantics p) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (Csem.semantics p) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpsingle_events (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (Csem.semantics p) (atomic (Cstrategy.semantics p))p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (Csem.semantics p) (atomic (Cstrategy.semantics p))p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (Csem.semantics p) (Cstrategy.semantics p)p:Csyntax.programtp:Verilog.programH:match_prog p tpsingle_events (Csem.semantics p)p:Csyntax.programtp:Verilog.programH:match_prog p tpwell_behaved_traces (Cstrategy.semantics p)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpsingle_events (Csem.semantics p)p:Csyntax.programtp:Verilog.programH:match_prog p tpwell_behaved_traces (Cstrategy.semantics p)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:match_prog p tpwell_behaved_traces (Cstrategy.semantics p)p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)exact (proj2 (cstrategy_semantic_preservation _ _ H)). Qed.p:Csyntax.programtp:Verilog.programH:match_prog p tpbackward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp)
We can then use transf_hls_match to prove the backward simulation where the assumption is that the translation is performed using the transf_hls function and that it succeeds.
forall (p : Csyntax.program) (tp : Verilog.program), transf_hls p = OK tp -> backward_simulation (Csem.semantics p) (Verilog.semantics tp)forall (p : Csyntax.program) (tp : Verilog.program), transf_hls p = OK tp -> backward_simulation (Csem.semantics p) (Verilog.semantics tp)p:Csyntax.programtp:Verilog.programH:transf_hls p = OK tpbackward_simulation (Csem.semantics p) (Verilog.semantics tp)apply transf_hls_match; auto. Qed.p:Csyntax.programtp:Verilog.programH:transf_hls p = OK tpmatch_prog p tp
The final theorem of the semantic preservation of the translation of separate translation units can also be proven correct, however, this is only because the translation fails if more than one translation unit is passed to Vericert at the moment.
forall (c_units : nlist Csyntax.program) (verilog_units : nlist Verilog.program) (c_program : Csyntax.program), nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_units -> link_list c_units = Some c_program -> exists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)forall (c_units : nlist Csyntax.program) (verilog_units : nlist Verilog.program) (c_program : Csyntax.program), nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_units -> link_list c_units = Some c_program -> exists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programnlist_forall2 match_prog c_units verilog_unitsc_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)eapply nlist_forall2_imply.c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programnlist_forall2 match_prog c_units verilog_unitsc_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programforall (v1 : Csyntax.program) (v2 : Verilog.program), nIn v1 c_units -> nIn v2 verilog_units -> (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) v1 v2 -> match_prog v1 v2apply transf_hls_match; auto.c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programv1:Csyntax.programv2:Verilog.programH1:nIn v1 c_unitsH2:nIn v2 verilog_unitsH3:transf_hls v1 = OK v2match_prog v1 v2c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ match_prog c_program verilog_programc_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsH2:exists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ match_prog c_program verilog_programexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)eapply link_list_compose_passes; eauto.c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ match_prog c_program verilog_programc_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsH2:exists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ match_prog c_program verilog_programexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsverilog_program:Verilog.programP:link_list verilog_units = Some verilog_programQ:match_prog c_program verilog_programexists verilog_program : Verilog.program, link_list verilog_units = Some verilog_program /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)apply c_semantic_preservation; auto. Qed.c_units:nlist Csyntax.programverilog_units:nlist Verilog.programc_program:Csyntax.programH:nlist_forall2 (fun (cu : Csyntax.program) (tcu : Verilog.program) => transf_hls cu = OK tcu) c_units verilog_unitsH0:link_list c_units = Some c_programH1:nlist_forall2 match_prog c_units verilog_unitsverilog_program:Verilog.programP:link_list verilog_units = Some verilog_programQ:match_prog c_program verilog_programbackward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program)