Compiler Proof

Table of Contents

Imports
Declarations
- Top-level Translation
Correctness Proof
- Backward Simulation

This is the top-level module of the correctness proof and proves the final backwards simulation correct.

Imports

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.

Declarations

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.

Lemma print_identity:
  forall (A: Type) (printer: A -> unit) (prog: A),
  print printer prog = prog.forall (A : Type) (printer : A -> unit) (prog : A),
print printer prog = prog
Proof.forall (A : Type) (printer : A -> unit) (prog : A),
print printer prog = prog
  intros; unfold print.A:Type
printer:A -> unit
prog:A
prog = prog destruct (printer prog); auto.
Qed.

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.

Lemma compose_print_identity:
  forall (A: Type) (x: res A) (f: A -> unit),
  x @@ print f = x.forall (A : Type) (x : res A) (f : A -> unit),
x @@ print f = x
Proof.forall (A : Type) (x : res A) (f : A -> unit),
x @@ print f = x
  intros.A:Type
x:res A
f:A -> unit
x @@ print f = x destruct x; simpl.A:Type
a:A
f:A -> unit
OK (print f a) = OK a
A:Type
e:errmsg
f:A -> unit
Error e = Error e rewrite print_identity.A:Type
a:A
f:A -> unit
OK a = OK a
A:Type
e:errmsg
f:A -> unit
Error e = Error e auto.A:Type
e:errmsg
f:A -> unit
Error e = Error e auto.
Qed.

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.

Top-level Translation

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.

Correctness Proof

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.

Theorem transf_hls_match:
  forall p tp,
    transf_hls p = OK tp ->
    match_prog p tp.forall (p : Csyntax.program) (tp : Verilog.program),
transf_hls p = OK tp -> match_prog p tp
Proof.forall (p : Csyntax.program) (tp : Verilog.program),
transf_hls p = OK tp -> match_prog p tp
  intros p tp T.p:Csyntax.program
tp:Verilog.program
T:transf_hls p = OK tp
match_prog p tp
  unfold transf_hls in T.p:Csyntax.program
tp:Verilog.program
T: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 tp
match_prog p tp simpl in T.p:Csyntax.program
tp:Verilog.program
T: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 tp
match_prog p tp
  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
T:SimplLocals.transf_program p1 @@@
Cshmgen.transl_program @@@
Cminorgen.transl_program @@@ Selection.sel_program @@@
RTLgen.transl_program @@ print (print_RTL 0) @@@
transf_backend = OK tp
match_prog p tp
  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
T:Cshmgen.transl_program p2 @@@
Cminorgen.transl_program @@@ Selection.sel_program @@@
RTLgen.transl_program @@ print (print_RTL 0) @@@
transf_backend = OK tp
match_prog p tp
  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
T:Cminorgen.transl_program p3 @@@
Selection.sel_program @@@ RTLgen.transl_program @@
print (print_RTL 0) @@@ transf_backend = OK tp
match_prog p tp
  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
T:Selection.sel_program p4 @@@ RTLgen.transl_program @@
print (print_RTL 0) @@@ transf_backend = OK tp
match_prog p tp
  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
T:RTLgen.transl_program p5 @@ print (print_RTL 0) @@@
transf_backend = OK tp
match_prog p tp
  rewrite ! compose_print_identity in T.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
T:RTLgen.transl_program p5 @@@ transf_backend =
OK tp
match_prog p tp
  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
T:transf_backend p6 = OK tp
match_prog p tp
  unfold transf_backend in T.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
T: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 tp
match_prog p tp simpl in T.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
T: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 tp
match_prog p tp rewrite ! compose_print_identity in T.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
T:Inlining.transf_program p6 @@
Renumber.transf_program @@@ HTLgen.transl_program @@
Veriloggen.transl_program = OK tp
match_prog p tp
  destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
T:HTLgen.transl_program (Renumber.transf_program p7) @@
Veriloggen.transl_program = OK tp
match_prog p tp
  set (p8 := Renumber.transf_program p7) in *.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
T:HTLgen.transl_program p8 @@
Veriloggen.transl_program = OK tp
match_prog p tp
  destruct (HTLgen.transl_program p8) as [p9|e] eqn:P9; simpl in T; try discriminate.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
T:OK (Veriloggen.transl_program p9) = OK tp
match_prog p tp
  set (p10 := Veriloggen.transl_program p9) in *.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
match_prog p tp
  unfold match_prog; simpl.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
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 /\ (...)))))))))
  exists p1; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
SimplExprproof.match_prog p p1
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)))))))) apply SimplExprproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))))))))
  exists p2; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
SimplLocalsproof.match_prog p1 p2
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))))))) apply SimplLocalsproof.match_transf_program; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)))))))
  exists p3; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
Cshmgenproof.match_prog p2 p3
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)))))) apply Cshmgenproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))))))
  exists p4; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
Cminorgenproof.match_prog p3 p4
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))))) apply Cminorgenproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)))))
  exists p5; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
Selectionproof.match_prog p4 p5
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)))) apply Selectionproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))))
  exists p6; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
RTLgenproof.match_prog p5 p6
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))) apply RTLgenproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)))
  exists p7; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
Inliningproof.match_prog p6 p7
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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)) apply Inliningproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists 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))
  exists p8; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
Renumberproof.match_prog p7 p8
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists p2 : HTL.program,
  HTLgenproof.match_prog p8 p2 /\
  (exists p3 : Verilog.program,
     Veriloggenproof.match_prog p2 p3 /\ p3 = tp) apply Renumberproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists p2 : HTL.program,
  HTLgenproof.match_prog p8 p2 /\
  (exists p3 : Verilog.program,
     Veriloggenproof.match_prog p2 p3 /\ p3 = tp)
  exists p9; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
HTLgenproof.match_prog p8 p9
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists p2 : Verilog.program,
  Veriloggenproof.match_prog p9 p2 /\ p2 = tp apply HTLgenproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
exists p2 : Verilog.program,
  Veriloggenproof.match_prog p9 p2 /\ p2 = tp
  exists p10; split.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
Veriloggenproof.match_prog p9 p10
p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
p10 = tp apply Veriloggenproof.transf_program_match; auto.p:Csyntax.program
tp:Verilog.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
T:OK p10 = OK tp
p10 = tp
  inv T.p:Csyntax.program
p1:Clight.program
P1:SimplExpr.transl_program p = OK p1
p2:Clight.program
P2:SimplLocals.transf_program p1 = OK p2
p3:Csharpminor.program
P3:Cshmgen.transl_program p2 = OK p3
p4:Cminor.program
P4:Cminorgen.transl_program p3 = OK p4
p5:CminorSel.program
P5:Selection.sel_program p4 = OK p5
p6:RTL.program
P6:RTLgen.transl_program p5 = OK p6
p7:RTL.program
P7:Inlining.transf_program p6 = OK p7
p8:=Renumber.transf_program p7:RTL.program
p9:HTL.program
P9:HTLgen.transl_program p8 = OK p9
p10:=Veriloggen.transl_program p9:Verilog.program
p10 = p10 reflexivity.
Qed.

Remark forward_simulation_identity:
  forall sem, forward_simulation sem sem.forall sem : semantics, forward_simulation sem sem
Proof.forall sem : semantics, forward_simulation sem sem
  intros.sem:semantics
forward_simulation sem sem apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros.sem:semantics
id:AST.ident
Globalenvs.Senv.public_symbol (symbolenv sem) id =
Globalenvs.Senv.public_symbol (symbolenv sem) id
sem:semantics
s1:state sem
H:initial_state sem s1
exists s2 : state sem, initial_state sem s2 /\ s2 = s1
sem:semantics
s1, s2:state sem
r:Integers.Int.int
H:s2 = s1
H0:final_state sem s1 r
final_state sem s2 r
sem:semantics
s1:state sem
t:Events.trace
s1':state sem
H:Step sem s1 t s1'
s2:state sem
H0:s2 = s1
exists s2' : state sem, Step sem s2 t s2' /\ s2' = s1'
-sem:semantics
id:AST.ident
Globalenvs.Senv.public_symbol (symbolenv sem) id =
Globalenvs.Senv.public_symbol (symbolenv sem) id auto.
-sem:semantics
s1:state sem
H:initial_state sem s1
exists s2 : state sem, initial_state sem s2 /\ s2 = s1 exists s1; auto.
-sem:semantics
s1, s2:state sem
r:Integers.Int.int
H:s2 = s1
H0:final_state sem s1 r
final_state sem s2 r subst s2; auto.
-sem:semantics
s1:state sem
t:Events.trace
s1':state sem
H:Step sem s1 t s1'
s2:state sem
H0:s2 = s1
exists s2' : state sem, Step sem s2 t s2' /\ s2' = s1' subst s2.sem:semantics
s1:state sem
t:Events.trace
s1':state sem
H:Step sem s1 t s1'
exists s2' : state sem, Step sem s1 t s2' /\ s2' = s1' exists s1'; auto.
Qed.

Theorem cstrategy_semantic_preservation:
  forall p tp,
  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)
Proof.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)
  intros p tp M.p:Csyntax.program
tp:Verilog.program
M:match_prog p tp
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics tp) /\
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp) unfold match_prog, pass_match in M; simpl in M.p:Csyntax.program
tp:Verilog.program
M: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)
Ltac DestructM :=
  match goal with
    [ H: exists p, _ /\ _ |- _ ] =>
      let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in
      destruct H as (p & M & MM); clear H
  end.p:Csyntax.program
tp:Verilog.program
M: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)
  repeat DestructM.p:Csyntax.program
tp:Verilog.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
MM0:p10 = tp
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics tp) /\
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp) subst tp.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10) /\
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics p10)
  assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)).p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F: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.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply SimplExprproof.transl_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Clight.semantics1 p0)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply SimplLocalsproof.transf_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Clight.semantics2 p1)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply Cshmgenproof.transl_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Csharpminor.semantics p3)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply Cminorgenproof.transl_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (Cminor.semantics p4)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply Selectionproof.transf_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (CminorSel.semantics p5)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply RTLgenproof.transf_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (RTL.semantics p6)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply Inliningproof.transf_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (RTL.semantics p7)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (RTL.semantics p8)
  (Verilog.semantics p10)
  eapply compose_forward_simulations.
    eapply HTLgenproof.transf_program_correct. eassumption.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
forward_simulation (HTL.semantics p9)
  (Verilog.semantics p10)
  eapply Veriloggenproof.transf_program_correct; eassumption.
  }p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F: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)
  split.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics p10) auto.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics p10)
  apply forward_to_backward_simulation.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
forward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
receptive (atomic (Cstrategy.semantics p))
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10)
  apply factor_forward_simulation.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
single_events (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
receptive (atomic (Cstrategy.semantics p))
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10) auto.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
single_events (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
receptive (atomic (Cstrategy.semantics p))
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10) eapply sd_traces.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
receptive (atomic (Cstrategy.semantics p))
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10) eapply Verilog.semantics_determinate.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
receptive (atomic (Cstrategy.semantics p))
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10)
  apply atomic_receptive.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
strongly_receptive (Cstrategy.semantics p)
p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10) apply Cstrategy.semantics_strongly_receptive.p:Csyntax.program
p0:Clight.program
M0:SimplExprproof.match_prog p p0
p1:Clight.program
M:SimplLocalsproof.match_prog p0 p1
p3:Csharpminor.program
M1:Cshmgenproof.match_prog p1 p3
p4:Cminor.program
M2:Cminorgenproof.match_prog p3 p4
p5:CminorSel.program
M3:Selectionproof.match_prog p4 p5
p6:RTL.program
M4:RTLgenproof.match_prog p5 p6
p7:RTL.program
M5:Inliningproof.match_prog p6 p7
p8:RTL.program
M6:Renumberproof.match_prog p7 p8
p9:HTL.program
M7:HTLgenproof.match_prog p8 p9
p10:Verilog.program
M8:Veriloggenproof.match_prog p9 p10
F:forward_simulation (Cstrategy.semantics p)
  (Verilog.semantics p10)
determinate (Verilog.semantics p10)
  apply Verilog.semantics_determinate.
Qed.

Backward Simulation

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.

Theorem c_semantic_preservation:
  forall p tp,
  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)
Proof.forall (p : Csyntax.program) (tp : Verilog.program),
match_prog p tp ->
backward_simulation (Csem.semantics p)
  (Verilog.semantics tp)
  intros.p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (Csem.semantics p)
  (Verilog.semantics tp)
  apply compose_backward_simulation with (atomic (Cstrategy.semantics p)).p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
single_events (Verilog.semantics tp)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (Csem.semantics p)
  (atomic (Cstrategy.semantics p))
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp)
  eapply sd_traces; eapply Verilog.semantics_determinate.p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (Csem.semantics p)
  (atomic (Cstrategy.semantics p))
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp)
  apply factor_backward_simulation.p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (Csem.semantics p)
  (Cstrategy.semantics p)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
single_events (Csem.semantics p)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
well_behaved_traces (Cstrategy.semantics p)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp)
  apply Cstrategy.strategy_simulation.p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
single_events (Csem.semantics p)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
well_behaved_traces (Cstrategy.semantics p)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp)
  apply Csem.semantics_single_events.p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
well_behaved_traces (Cstrategy.semantics p)
p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp)
  eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive.p:Csyntax.program
tp:Verilog.program
H:match_prog p tp
backward_simulation (atomic (Cstrategy.semantics p))
  (Verilog.semantics tp)
  exact (proj2 (cstrategy_semantic_preservation _ _ H)).
Qed.

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.

Theorem transf_c_program_correct:
  forall p tp,
  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)
Proof.forall (p : Csyntax.program) (tp : Verilog.program),
transf_hls p = OK tp ->
backward_simulation (Csem.semantics p)
  (Verilog.semantics tp)
  intros.p:Csyntax.program
tp:Verilog.program
H:transf_hls p = OK tp
backward_simulation (Csem.semantics p)
  (Verilog.semantics tp) apply c_semantic_preservation.p:Csyntax.program
tp:Verilog.program
H:transf_hls p = OK tp
match_prog p tp apply transf_hls_match; auto.
Qed.

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.

Theorem separate_transf_c_program_correct:
  forall c_units verilog_units c_program,
  nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units verilog_units ->
  link_list c_units = Some c_program ->
  exists 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)
Proof.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)
  intros.c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0: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)
  assert (nlist_forall2 match_prog c_units verilog_units).c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
nlist_forall2 match_prog c_units verilog_units
c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
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.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
nlist_forall2 match_prog c_units verilog_units eapply nlist_forall2_imply. eauto.c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
forall (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 v2 simpl; intros.c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
v1:Csyntax.program
v2:Verilog.program
H1:nIn v1 c_units
H2:nIn v2 verilog_units
H3:transf_hls v1 = OK v2
match_prog v1 v2 apply transf_hls_match; auto. }c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  backward_simulation (Csem.semantics c_program)
    (Verilog.semantics verilog_program)
  assert (exists verilog_program, link_list verilog_units = Some verilog_program
                                  /\ match_prog c_program verilog_program).c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  match_prog c_program verilog_program
c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
H2:exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  match_prog c_program verilog_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.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  match_prog c_program verilog_program eapply link_list_compose_passes; eauto. }c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
H2:exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  match_prog c_program verilog_program
exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  backward_simulation (Csem.semantics c_program)
    (Verilog.semantics verilog_program)
  destruct H2 as (verilog_program & P & Q).c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
verilog_program:Verilog.program
P:link_list verilog_units = Some verilog_program
Q:match_prog c_program verilog_program
exists verilog_program : Verilog.program,
  link_list verilog_units = Some verilog_program /\
  backward_simulation (Csem.semantics c_program)
    (Verilog.semantics verilog_program)
  exists verilog_program; split; auto.c_units:nlist Csyntax.program
verilog_units:nlist Verilog.program
c_program:Csyntax.program
H:nlist_forall2
  (fun (cu : Csyntax.program)
     (tcu : Verilog.program) =>
   transf_hls cu = OK tcu) c_units verilog_units
H0:link_list c_units = Some c_program
H1:nlist_forall2 match_prog c_units verilog_units
verilog_program:Verilog.program
P:link_list verilog_units = Some verilog_program
Q:match_prog c_program verilog_program
backward_simulation (Csem.semantics c_program)
  (Verilog.semantics verilog_program) apply c_semantic_preservation; auto.
Qed.