Remove all Admitted from top-level Compiler.v

7 files changed, 618 insertions, 425 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index a4accfc..170acb4 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -254,24 +254,6 @@ Finally, the top-level definition for all the passes is defined, which combines
 
 Local Open Scope linking_scope.
 
-Definition verilog_transflink : TransfLink Veriloggenproof.match_prog.
-Admitted.
-
-Definition Renaming_match_prog : HTL.program -> HTL.program -> Prop.
-Admitted.
-Instance TransfLink_Renaming : TransfLink Renaming_match_prog.
-Admitted.
-Lemma Renaming_transf_program_match : forall p tp, Renaming.transf_program p = OK tp -> Renaming_match_prog p tp.
-Admitted.
-
-Definition ApplyExternctrl_match_prog : HTL.program -> HTL.program -> Prop :=
-  match_program (fun ctx f tf => ApplyExternctrl.transf_fundef ctx f = OK tf) eq.
-Instance TransfLink_ApplyExternctrl : TransfLink ApplyExternctrl_match_prog.
-Admitted.
-Lemma ApplyExternctrl_transf_program_match : forall p tp,
-  ApplyExternctrl.transf_program p = OK tp -> ApplyExternctrl_match_prog p tp.
-Admitted.
-
 Definition CompCert's_passes :=
       mkpass SimplExprproof.match_prog
   ::: mkpass SimplLocalsproof.match_prog
@@ -287,9 +269,9 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
   ::: mkpass Unusedglobproof.match_prog
   ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program))
-  ::: mkpass Renaming_match_prog
-  ::: mkpass ApplyExternctrl_match_prog
-  ::: (@mkpass _ _ Veriloggenproof.match_prog verilog_transflink)
+  ::: mkpass Renaming.match_prog
+  ::: mkpass ApplyExternctrl.match_prog
+  ::: mkpass Veriloggenproof.match_prog
   ::: pass_nil _.
 
 (*|
@@ -317,7 +299,7 @@ Proof.
   destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
   rewrite ! compose_print_identity in T.
   destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
-  unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T.
+  unfold transf_backend, time in T. rewrite ! compose_print_identity in T. simpl in T.
   destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate.
   set (p8 := Renumber.transf_program p7) in *.
   set (p9 := total_if Compopts.optim_constprop Constprop.transf_program p8) in *.
@@ -345,13 +327,11 @@ Proof.
   exists p12; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
   exists p13; split. apply Unusedglobproof.transf_program_match; auto.
   exists p14; split. apply HTLgenproof.transf_program_match; auto.
-  exists p15; split. apply Renaming_transf_program_match; auto.
-  exists p16; split. apply ApplyExternctrl_transf_program_match; auto.
+  exists p15; split. apply Renaming.transf_program_match; auto.
+  exists p16; split. apply ApplyExternctrl.transf_program_match; auto.
   exists p17; split. apply Veriloggenproof.transf_program_match; auto.
   inv T. reflexivity.
-(*apply Veriloggenproof.transf_program_match; auto.
-  inv T. reflexivity.*)
-Admitted.
+Qed.
 
 Theorem cstrategy_semantic_preservation:
   forall p tp,
@@ -361,14 +341,14 @@ Theorem cstrategy_semantic_preservation:
 Proof.
   intros p tp M. unfold match_prog, pass_match in M; simpl in M.
 
-Ltac DestructM :=
-  match goal with
+  repeat 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.
-  repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p15)).
+  subst tp.
+
+  assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p17)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -397,16 +377,21 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply Unusedglobproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
-    eapply HTLgenproof.transf_program_correct. eassumption.
-  (* eapply Veriloggenproof.transf_program_correct; eassumption. *)
-  admit.
+    eapply HTLgenproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Renaming.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply ApplyExternctrl.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Veriloggenproof.transf_program_correct; eassumption.
+  eapply forward_simulation_identity.
   }
   split. auto.
   apply forward_to_backward_simulation.
   apply factor_forward_simulation. auto. eapply sd_traces. eapply Verilog.semantics_determinate.
   apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive.
   apply Verilog.semantics_determinate.
-Admitted.
+Qed.
 
 (*|
 Backward Simulation
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 33ddb71..0fae032 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -85,14 +85,17 @@ Ltac solve_by_invert := solve_by_inverts 1.
 Ltac invert x := inversion x; subst; clear x.
 
 (** For a hypothesis of a forall-type, instantiate every variable to a fresh existential *)
+Ltac insterU1 H :=
+  match type of H with
+  | forall x : ?T, _ =>
+    let x := fresh "x" in
+    evar (x : T);
+    let x' := eval unfold x in x in
+        clear x; specialize (H x')
+  end.
+
 Ltac insterU H :=
-  repeat match type of H with
-         | forall x : ?T, _ =>
-           let x := fresh "x" in
-           evar (x : T);
-           let x' := eval unfold x in x in
-               clear x; specialize (H x')
-         end.
+  repeat (insterU1 H).
 
 Ltac destruct_match :=
   match goal with
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
index 44c6b83..5ddbd4a 100644
--- a/src/hls/ApplyExternctrl.v
+++ b/src/hls/ApplyExternctrl.v
@@ -178,3 +178,19 @@ End APPLY_EXTERNCTRL.
 
 Definition transf_fundef (prog : HTL.program) := transf_partial_fundef (module_apply_externctrl prog).
 Definition transf_program (prog : HTL.program) := transform_partial_program (transf_fundef prog) prog.
+
+(* Semantics *)
+
+Definition match_prog : HTL.program -> HTL.program -> Prop :=
+  Linking.match_program (fun ctx f tf => ApplyExternctrl.transf_fundef ctx f = OK tf) eq.
+
+Lemma transf_program_match : forall p tp,
+  ApplyExternctrl.transf_program p = OK tp -> match_prog p tp.
+Admitted.
+
+Lemma transf_program_correct : forall p tp,
+  match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp).
+Admitted.
+
+Instance TransfLink : Linking.TransfLink match_prog.
+Admitted.
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 0513066..cba21b0 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -171,6 +171,7 @@ Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop :=
     forall f m rtl_args htl_args mid mem rtl_stk htl_stk
     (TF : tr_module ge f m)
     (MF : match_frames ge mid mem rtl_stk htl_stk)
+    (NP : Forall not_pointer rtl_args)
     (MARGS : list_forall2 val_value_lessdef rtl_args htl_args),
       match_states ge
                    (RTL.Callstate rtl_stk (AST.Internal f) rtl_args mem)
@@ -1256,6 +1257,39 @@ Section CORRECTNESS.
     - destruct params; eauto using regs_lessdef_add_match with htlproof.
   Qed.
 
+  Lemma stack_based_set : forall sp r v rs,
+      stack_based v sp ->
+      reg_stack_based_pointers sp rs ->
+      reg_stack_based_pointers sp (Registers.Regmap.set r v rs).
+  Proof.
+    unfold reg_stack_based_pointers, Registers.Regmap.set, "_ !! _".
+    intros * ? ? r0.
+    simpl.
+    destruct (peq r r0); subst.
+    - rewrite AssocMap.gss; auto.
+    - rewrite AssocMap.gso; auto.
+  Qed.
+
+  Lemma stack_based_non_pointers : forall args params stk,
+      Forall not_pointer args ->
+      reg_stack_based_pointers stk (RTL.init_regs args params).
+  Proof.
+    unfold reg_stack_based_pointers.
+    induction args; intros * NP *.
+    + destruct params;
+      simpl;
+      unfold "_ !! _";
+      rewrite PTree.gempty;
+      crush.
+    + destruct params; simpl.
+      * unfold "_ !! _". rewrite PTree.gempty. crush.
+      * inv NP.
+        apply stack_based_set;
+        [ destruct a; crush
+        | unfold reg_stack_based_pointers; auto
+        ].
+  Qed.
+
   Lemma transl_callstate_correct:
     forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val)
       (m : mem) (m' : Mem.mem') (stk : Values.block),
@@ -1280,17 +1314,15 @@ Section CORRECTNESS.
     - repeat apply regs_lessdef_add_greater; try not_control_reg.
       eauto using match_args.
     - edestruct no_stack_calls; eauto.
-      + replace (RTL.fn_stacksize f) in *.
-        replace m' with m by
-            (destruct (mem_alloc_zero m); crush).
-        subst.
+      + replace (RTL.fn_stacksize f) with 0 in *
+          by assumption.
+        replace m' with m
+          by (destruct (mem_alloc_zero m); crush).
         assumption.
       + subst. inv MF. constructor.
-    - (* Stack pointer *)
-      admit.
-    - (* Stack based args *)
-      unfold reg_stack_based_pointers; intros.
+    - big_tac.
       admit.
+    - eauto using stack_based_non_pointers.
     - (* Stack based stack pointer *)
       unfold arr_stack_based_pointers; intros.
       admit.
@@ -1315,7 +1347,76 @@ Section CORRECTNESS.
     exists x. crush.
   Qed.
 
-  Require Import Registers.
+  Fixpoint assign_all acc (rs : list reg) (vals : list value) :=
+    match rs, vals with
+    | r::rs', val::vals' => assign_all (acc # r <- val) rs' vals'
+    | _, _ => acc
+    end.
+
+  Notation "a ## b '<-' c" := (assign_all a b c) (at level 1, b at next level) : assocmap.
+
+  Lemma assign_all_nil : forall a rs, a ## rs <- nil = a.
+  Proof. destruct rs; crush. Qed.
+
+  Lemma assign_all_out : forall rs vs a r, (forall v, ~ In (r, v) (List.combine rs vs)) -> (a ## rs <- vs) ! r = a ! r.
+  Proof.
+    induction rs; intros * H.
+    - trivial.
+    - destruct vs.
+      + rewrite assign_all_nil.
+        trivial.
+      + simpl.
+        rewrite IHrs.
+        rewrite AssocMap.gso.
+        crush.
+        * simpl (List.combine _ _) in *.
+          specialize (H v).
+          rewrite not_in_cons in H.
+          inv H.
+          crush.
+        * intros v0.
+          specialize (H v0).
+          simpl (List.combine _ _) in *.
+          rewrite not_in_cons in H.
+          crush.
+  Qed.
+
+  Lemma nonblock_all_exec : forall from_regs to_regs f basr nasr basa nasa,
+      Verilog.stmnt_runp
+        f
+        {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr |}
+        {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}
+        (nonblock_all (List.combine to_regs from_regs))
+        {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr ## to_regs <- (basr##from_regs) |}
+        {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}.
+  Proof.
+    induction from_regs; intros.
+    - rewrite combine_nil, assign_all_nil.
+      constructor.
+    - destruct to_regs; try solve [ constructor ].
+      simpl.
+      econstructor.
+      + repeat econstructor.
+      + eapply IHfrom_regs.
+  Qed.
+
+  Lemma fork_exec : forall f basr nasr basa nasa rst to_regs from_regs,
+      Verilog.stmnt_runp
+        f
+        {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr |}
+        {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}
+        (fork rst (List.combine to_regs from_regs))
+        {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := (nasr # rst <- (ZToValue 1)) ## to_regs <- (basr##from_regs) |}
+        {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}.
+  Proof.
+    intros.
+    unfold fork.
+    econstructor.
+    - repeat econstructor.
+    - unfold Verilog.nonblock_reg; simpl.
+      eapply nonblock_all_exec.
+  Qed.
+
   Lemma transl_icall_correct:
     forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val)
       (pc : positive) (rs : RTL.regset) (m : mem) sig fn fd args dst pc',
@@ -1325,8 +1426,96 @@ Section CORRECTNESS.
         match_states ge (RTL.State s f sp pc rs m) R1 ->
         exists R2 : HTL.state,
           Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
-          match_states ge (RTL.Callstate (RTL.Stackframe dst f sp pc' rs :: s) fd rs##args m) R2.
+          match_states ge (RTL.Callstate (RTL.Stackframe dst f sp pc' rs :: s) fd
+                                         (List.map (fun r => Registers.Regmap.get r rs) args) m)
+                       R2.
   Proof.
+    intros * H Hfunc * MSTATE.
+    inv_state.
+    edestruct (only_internal_calls fd); eauto; subst fd.
+    simpl in *.
+    eexists. split.
+    - inv CONST.
+      simplify.
+      eapply Smallstep.plus_three; simpl in *.
+      + eapply HTL.step_module; simpl.
+        * repeat econstructor; auto.
+        * repeat econstructor; auto.
+        * repeat econstructor; eauto.
+        * repeat econstructor; eauto.
+        * repeat econstructor; eauto.
+        * repeat econstructor; auto.
+        * repeat econstructor; eauto.
+        * eapply fork_exec.
+        * trivial.
+        * trivial.
+        * eapply AssocMapExt.merge_correct_1.
+          rewrite assign_all_out.
+          big_tac.
+          -- not_control_reg.
+          -- simpl.
+             insterU H6.
+             simplify.
+             admit.
+        * admit.
+      + eapply HTL.step_module; trivial.
+        * simpl.
+          apply AssocMapExt.merge_correct_2; auto.
+          rewrite assign_all_out by admit.
+          rewrite AssocMap.gso by not_control_reg.
+          rewrite AssocMap.gso by lia.
+          apply AssocMap.gempty.
+        * simpl.
+          apply AssocMapExt.merge_correct_2; auto.
+          rewrite assign_all_out by admit.
+          rewrite AssocMap.gso by not_control_reg.
+          rewrite AssocMap.gso by lia.
+          apply AssocMap.gempty.
+        * simpl.
+          apply AssocMapExt.merge_correct_1; auto.
+          rewrite assign_all_out by admit.
+          rewrite AssocMap.gso by not_control_reg.
+          apply AssocMap.gss.
+        * eauto.
+        * eauto.
+        * unfold state_wait.
+          eapply Verilog.stmnt_runp_Vcond_false.
+          -- simpl. econstructor; econstructor; simpl.
+             replace (Verilog.merge_regs ((empty_assocmap # st1 <- (posToValue x0)) # x1 <- (ZToValue 1)) ## x4 <- (asr ## args) asr) # x3
+               with (ZToValue 0) by admit.
+             trivial.
+          -- auto.
+          -- econstructor.
+        * simpl.
+          apply AssocMapExt.merge_correct_1; auto.
+          rewrite assign_all_out by admit.
+          rewrite AssocMap.gso by not_control_reg.
+          apply AssocMap.gss.
+        * repeat econstructor.
+        * simpl.
+          apply AssocMapExt.merge_correct_2.
+          big_tac.
+          apply AssocMap.gempty.
+          not_control_reg.
+          assert (Ple dst (RTL.max_reg_function f))
+                 by eauto using RTL.max_reg_function_def.
+          xomega.
+          apply AssocMapExt.merge_correct_1.
+          rewrite assign_all_out by admit.
+          rewrite AssocMap.gso by not_control_reg.
+          apply AssocMap.gss.
+        * admit.
+      + eapply HTL.step_initcall.
+        * (* find called module *) admit.
+        * (* callee reset mapped *) admit.
+        * (* params mapped *) admit.
+        * (* callee reset unset *) admit.
+        * (* params set *) admit.
+      + eauto with htlproof.
+    - econstructor; try solve [repeat econstructor; eauto with htlproof ].
+      + (* Called module is translated *) admit.
+      + (* Match stackframes *) admit.
+      + (* Argument values match *) admit.
   Admitted.
   Hint Resolve transl_icall_correct : htlproof.
   Close Scope rtl.
@@ -1392,19 +1581,6 @@ Section CORRECTNESS.
   Qed.
   Hint Resolve transl_ireturn_correct : htlproof.
 
-  Lemma stack_based_set : forall sp r v rs,
-      stack_based v sp ->
-      reg_stack_based_pointers sp rs ->
-      reg_stack_based_pointers sp (Registers.Regmap.set r v rs).
-  Proof.
-    unfold reg_stack_based_pointers, Registers.Regmap.set, "_ !! _".
-    intros * ? ? r0.
-    simpl.
-    destruct (Pos.eq_dec r r0); subst.
-    - rewrite AssocMap.gss; auto.
-    - rewrite AssocMap.gso; auto.
-  Qed.
-
   Lemma transl_returnstate_correct:
     forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node)
       (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem)
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v
index 3efc20f..b9fbcaa 100644
--- a/src/hls/Renaming.v
+++ b/src/hls/Renaming.v
@@ -216,3 +216,16 @@ Definition transf_program (p : HTL.program) : Errors.res HTL.program :=
                               (fun _ f => renumber_fundef f)
                               (mk_renumber_state 1%positive (PTree.empty reg))
                               p.
+
+Definition match_prog : HTL.program -> HTL.program -> Prop := fun _ _ => True.
+
+Instance TransfRenamingLink : Linking.TransfLink match_prog.
+Admitted.
+
+Lemma transf_program_match : forall p tp,
+  Renaming.transf_program p = Errors.OK tp -> match_prog p tp.
+Admitted.
+
+Lemma transf_program_correct : forall p tp,
+  match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp).
+Admitted.
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index 1f0938b..7ace6be 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -63,9 +63,9 @@ Section TRANSLATE.
     end.
 
   (* FIXME Remove the fuel parameter (recursion limit)*)
-  Fixpoint transf_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module :=
+  Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module :=
     match fuel with
-    | O => Error (msg "Veriloggen: transf_module recursion too deep")
+    | O => Error (msg "Veriloggen: transl_module recursion too deep")
     | S fuel' =>
       let clk := match externclk with
                  | None => HTL.mod_clk m
@@ -77,7 +77,7 @@ Section TRANSLATE.
       let htl_modules := PTree.filter
                        (fun m _ => List.existsb (Pos.eqb m) inline_names)
                        modmap in
-      do translated_modules <- PTree.traverse (fun _ => transf_module fuel' prog (Some clk)) htl_modules;
+      do translated_modules <- PTree.traverse (fun _ => transl_module fuel' prog (Some clk)) htl_modules;
       let cleaned_modules := PTree.map1 (map_body (Option.map_option (clean_up_decl clk)))
                                         translated_modules in
 
@@ -125,7 +125,7 @@ Section TRANSLATE.
                (HTL.mod_entrypoint m))
     end.
 
-  Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transf_module 10 prog None).
+  Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transl_module 10 prog None).
   Definition transl_program (prog : HTL.program) := transform_partial_program (transl_fundef prog) prog.
 
 End TRANSLATE.
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index 59267f7..ccb315e 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -22,247 +22,247 @@ From vericert Require HTL.
 From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
 Require Import Lia.
 
-
 Local Open Scope assocmap.
 
 Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
   match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog.
 
-(*
-
 Lemma transf_program_match:
-  forall prog, match_prog prog (transl_program prog).
-Proof.
-  intros. eapply match_transform_program_contextual. auto.
-Qed.
-
-Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
-| match_stack :
-    forall res m pc reg_assoc arr_assoc hstk vstk,
-      match_stacks hstk vstk ->
-      match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
-                   (Stackframe res (transl_module m) pc
-                                       reg_assoc arr_assoc :: vstk)
-| match_stack_nil : match_stacks nil nil.
-
-Inductive match_states : HTL.state -> state -> Prop :=
-| match_state :
-    forall m st reg_assoc arr_assoc hstk vstk,
-      match_stacks hstk vstk ->
-      match_states (HTL.State hstk m st reg_assoc arr_assoc)
-                   (State vstk (transl_module m) st reg_assoc arr_assoc)
-| match_returnstate :
-    forall v hstk vstk,
-      match_stacks hstk vstk ->
-      match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
-| match_initial_call :
-    forall m,
-      match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
-
-Lemma Vlit_inj :
-  forall a b, Vlit a = Vlit b -> a = b.
-Proof. inversion 1. trivial. Qed.
-
-Lemma posToValue_inj :
-  forall a b,
-    0 <= Z.pos a <= Int.max_unsigned ->
-    0 <= Z.pos b <= Int.max_unsigned ->
-    posToValue a = posToValue b ->
-    a = b.
-Proof.
-  intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id.
-  rewrite <- Int.unsigned_repr at 1; try assumption.
-  symmetry.
-  rewrite <- Int.unsigned_repr at 1; try assumption.
-  unfold posToValue in *. rewrite H1; auto.
-Qed.
-
-Lemma valueToPos_inj :
-  forall a b,
-    0 < Int.unsigned a ->
-    0 < Int.unsigned b ->
-    valueToPos a = valueToPos b ->
-    a = b.
-Proof.
-  intros. unfold valueToPos in *.
-  rewrite <- Int.repr_unsigned at 1.
-  rewrite <- Int.repr_unsigned.
-  apply Pos2Z.inj_iff in H1.
-  rewrite Z2Pos.id in H1; auto.
-  rewrite Z2Pos.id in H1; auto.
-  rewrite H1. auto.
-Qed.
-
-Lemma unsigned_posToValue_le :
-  forall p,
-    Z.pos p <= Int.max_unsigned ->
-    0 < Int.unsigned (posToValue p).
-Proof.
-  intros. unfold posToValue. rewrite Int.unsigned_repr; lia.
-Qed.
-
-Lemma transl_ctrl_fun_fst :
-  forall p1 p2 a b,
-    0 <= Z.pos p1 <= Int.max_unsigned ->
-    0 <= Z.pos p2 <= Int.max_unsigned ->
-    transl_ctrl_fun (p1, a) = transl_ctrl_fun (p2, b) ->
-    (p1, a) = (p2, b).
-Proof.
-  intros. unfold transl_ctrl_fun in H1. apply pair_equal_spec in H1.
-  destruct H1. rewrite H2. apply Vlit_inj in H1.
-  apply posToValue_inj in H1; try assumption.
-  rewrite H1; auto.
-Qed.
-
-Lemma transl_data_fun_fst :
-  forall p1 p2 a b,
-    0 <= Z.pos p1 <= Int.max_unsigned ->
-    0 <= Z.pos p2 <= Int.max_unsigned ->
-    transl_datapath_fun (p1, a) = transl_datapath_fun (p2, b) ->
-    p1 = p2.
-Proof.
-  intros.
-  unfold transl_datapath_fun in H1. apply pair_equal_spec in H1. destruct H1.
-  apply Vlit_inj in H1. apply posToValue_inj in H1; assumption.
-Qed.
-
-Lemma Zle_relax :
-  forall p q r,
-  p < q <= r ->
-  p <= q <= r.
-Proof. lia. Qed.
-Hint Resolve Zle_relax : verilogproof.
-
-Lemma transl_in :
-  forall l p,
-  0 <= Z.pos p <= Int.max_unsigned ->
-  (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-  In (Vlit (posToValue p)) (map fst (map transl_ctrl_fun l)) ->
-  In p (map fst l).
-Proof.
-  induction l.
-  - simplify. auto.
-  - intros. destruct a. simplify. destruct (peq p0 p); auto.
-    right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction.
-    auto with verilogproof.
-    apply IHl; auto.
-Qed.
-
-Lemma transl_notin :
-  forall l p,
-    0 <= Z.pos p <= Int.max_unsigned ->
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_ctrl l)).
-Proof.
-  induction l; auto. intros. destruct a. unfold not in *. intros.
-  simplify.
-  destruct (peq p0 p). apply H1. auto. apply H1.
-  unfold transl_ctrl in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H.
-  contradiction.
-  auto with verilogproof. auto.
-  right. apply transl_in; auto.
-Qed.
-
-Lemma transl_norepet :
-  forall l,
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_ctrl l)).
+  forall prog tprog, transl_program prog = Errors.OK tprog -> match_prog prog tprog.
 Proof.
-  induction l.
-  - intros. simpl. apply list_norepet_nil.
-  - destruct a. intros. simpl. apply list_norepet_cons.
-    inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto.
-    intros. apply H. destruct (peq p0 p); subst; simplify; auto.
-    assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto.
-    simplify. inv H0. assumption.
+  intros. unfold transl_program in *. eapply match_transform_partial_program_contextual; eauto.
 Qed.
 
-Lemma transl_ctrl_correct :
-  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    list_norepet (List.map fst l) ->
-    asr!ev = Some v ->
-    (forall p s,
-        In (p, s) l ->
-        v = posToValue p ->
-        stmnt_runp f
-                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                   s
-                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
-        stmnt_runp f
-                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                   (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip))
-                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
-Proof.
-  induction l as [| a l IHl].
-  - contradiction.
-  - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.
-    destruct a as [p' s']. simplify.
-    destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match.
-    constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
-    rewrite ASSOC. trivial. constructor. auto.
-    inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption.
-    inv NOREP. eapply in_map with (f := fst) in INV. contradiction.
-
-    eapply stmnt_runp_Vcase_nomatch. constructor. simplify.
-    unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
-    trivial. constructor. unfold not. intros. apply n. apply posToValue_inj.
-    apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction.
-    eapply in_map with (f := fst) in H0. auto.
-    apply Zle_relax. apply BOUND; auto. auto.
-
-    eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
-    trivial. assumption.
-Qed.
-Hint Resolve transl_ctrl_correct : verilogproof.
-
-(* FIXME Probably wrong we probably need some statemnt about datapath_statement_runp *)
-Lemma transl_datapath_correct :
-  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    list_norepet (List.map fst l) ->
-    asr!ev = Some v ->
-    (forall p s,
-        In (p, s) l ->
-        v = posToValue p ->
-        stmnt_runp f
-                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                   s
-                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
-        stmnt_runp f
-                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                   (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip))
-                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
-Proof. Admitted.
-
-Lemma pc_wf :
-  forall A m p v,
-  (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-  m!p = Some v ->
-  0 <= Z.pos p <= Int.max_unsigned.
-Proof.
-  intros A m p v LT S. apply Zle_relax. apply LT.
-  apply AssocMap.elements_correct in S. remember (p, v) as x.
-  exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto.
-Qed.
-
-Lemma mis_stepp_decl :
-  forall l asr asa f,
-    mis_stepp f asr asa (map Vdeclaration l) asr asa.
-Proof.
-  induction l.
-  - intros. constructor.
-  - intros. simplify. econstructor. constructor. auto.
-Qed.
-Hint Resolve mis_stepp_decl : verilogproof.
+Instance TransfVerilogLink : TransfLink Veriloggenproof.match_prog.
+Admitted.
+
+(* Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := *)
+(* | match_stack : *)
+(*     forall res m pc reg_assoc arr_assoc hstk vstk, *)
+(*       match_stacks hstk vstk -> *)
+(*       match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) *)
+(*                    (Stackframe res (transl_module m) pc *)
+(*                                        reg_assoc arr_assoc :: vstk) *)
+(* | match_stack_nil : match_stacks nil nil. *)
+
+(* Inductive match_states : HTL.state -> state -> Prop := *)
+(* | match_state : *)
+(*     forall m st reg_assoc arr_assoc hstk vstk, *)
+(*       match_stacks hstk vstk -> *)
+(*       match_states (HTL.State hstk m st reg_assoc arr_assoc) *)
+(*                    (State vstk (transl_module m) st reg_assoc arr_assoc) *)
+(* | match_returnstate : *)
+(*     forall v hstk vstk, *)
+(*       match_stacks hstk vstk -> *)
+(*       match_states (HTL.Returnstate hstk v) (Returnstate vstk v) *)
+(* | match_initial_call : *)
+(*     forall m, *)
+(*       match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). *)
+
+(* Lemma Vlit_inj : *)
+(*   forall a b, Vlit a = Vlit b -> a = b. *)
+(* Proof. inversion 1. trivial. Qed. *)
+
+(* Lemma posToValue_inj : *)
+(*   forall a b, *)
+(*     0 <= Z.pos a <= Int.max_unsigned -> *)
+(*     0 <= Z.pos b <= Int.max_unsigned -> *)
+(*     posToValue a = posToValue b -> *)
+(*     a = b. *)
+(* Proof. *)
+(*   intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. *)
+(*   rewrite <- Int.unsigned_repr at 1; try assumption. *)
+(*   symmetry. *)
+(*   rewrite <- Int.unsigned_repr at 1; try assumption. *)
+(*   unfold posToValue in *. rewrite H1; auto. *)
+(* Qed. *)
+
+(* Lemma valueToPos_inj : *)
+(*   forall a b, *)
+(*     0 < Int.unsigned a -> *)
+(*     0 < Int.unsigned b -> *)
+(*     valueToPos a = valueToPos b -> *)
+(*     a = b. *)
+(* Proof. *)
+(*   intros. unfold valueToPos in *. *)
+(*   rewrite <- Int.repr_unsigned at 1. *)
+(*   rewrite <- Int.repr_unsigned. *)
+(*   apply Pos2Z.inj_iff in H1. *)
+(*   rewrite Z2Pos.id in H1; auto. *)
+(*   rewrite Z2Pos.id in H1; auto. *)
+(*   rewrite H1. auto. *)
+(* Qed. *)
+
+(* Lemma unsigned_posToValue_le : *)
+(*   forall p, *)
+(*     Z.pos p <= Int.max_unsigned -> *)
+(*     0 < Int.unsigned (posToValue p). *)
+(* Proof. *)
+(*   intros. unfold posToValue. rewrite Int.unsigned_repr; lia. *)
+(* Qed. *)
+
+(* Lemma transl_ctrl_fun_fst : *)
+(*   forall p1 p2 a b, *)
+(*     0 <= Z.pos p1 <= Int.max_unsigned -> *)
+(*     0 <= Z.pos p2 <= Int.max_unsigned -> *)
+(*     transl_ctrl_fun (p1, a) = transl_ctrl_fun (p2, b) -> *)
+(*     (p1, a) = (p2, b). *)
+(* Proof. *)
+(*   intros. unfold transl_ctrl_fun in H1. apply pair_equal_spec in H1. *)
+(*   destruct H1. rewrite H2. apply Vlit_inj in H1. *)
+(*   apply posToValue_inj in H1; try assumption. *)
+(*   rewrite H1; auto. *)
+(* Qed. *)
+
+(* Lemma transl_data_fun_fst : *)
+(*   forall p1 p2 a b, *)
+(*     0 <= Z.pos p1 <= Int.max_unsigned -> *)
+(*     0 <= Z.pos p2 <= Int.max_unsigned -> *)
+(*     transl_datapath_fun (p1, a) = transl_datapath_fun (p2, b) -> *)
+(*     p1 = p2. *)
+(* Proof. *)
+(*   intros. *)
+(*   unfold transl_datapath_fun in H1. apply pair_equal_spec in H1. destruct H1. *)
+(*   apply Vlit_inj in H1. apply posToValue_inj in H1; assumption. *)
+(* Qed. *)
+
+(* Lemma Zle_relax : *)
+(*   forall p q r, *)
+(*   p < q <= r -> *)
+(*   p <= q <= r. *)
+(* Proof. lia. Qed. *)
+(* Hint Resolve Zle_relax : verilogproof. *)
+
+(* Lemma transl_in : *)
+(*   forall l p, *)
+(*   0 <= Z.pos p <= Int.max_unsigned -> *)
+(*   (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *)
+(*   In (Vlit (posToValue p)) (map fst (map transl_ctrl_fun l)) -> *)
+(*   In p (map fst l). *)
+(* Proof. *)
+(*   induction l. *)
+(*   - simplify. auto. *)
+(*   - intros. destruct a. simplify. destruct (peq p0 p); auto. *)
+(*     right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. *)
+(*     auto with verilogproof. *)
+(*     apply IHl; auto. *)
+(* Qed. *)
+
+(* Lemma transl_notin : *)
+(*   forall l p, *)
+(*     0 <= Z.pos p <= Int.max_unsigned -> *)
+(*     (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *)
+(*     ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_ctrl l)). *)
+(* Proof. *)
+(*   induction l; auto. intros. destruct a. unfold not in *. intros. *)
+(*   simplify. *)
+(*   destruct (peq p0 p). apply H1. auto. apply H1. *)
+(*   unfold transl_ctrl in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. *)
+(*   contradiction. *)
+(*   auto with verilogproof. auto. *)
+(*   right. apply transl_in; auto. *)
+(* Qed. *)
+
+(* Lemma transl_norepet : *)
+(*   forall l, *)
+(*     (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *)
+(*     list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_ctrl l)). *)
+(* Proof. *)
+(*   induction l. *)
+(*   - intros. simpl. apply list_norepet_nil. *)
+(*   - destruct a. intros. simpl. apply list_norepet_cons. *)
+(*     inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. *)
+(*     intros. apply H. destruct (peq p0 p); subst; simplify; auto. *)
+(*     assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. *)
+(*     simplify. inv H0. assumption. *)
+(* Qed. *)
+
+(* Lemma transl_ctrl_correct : *)
+(*   forall l v ev f asr asa asrn asan asr' asa' asrn' asan', *)
+(*     (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *)
+(*     list_norepet (List.map fst l) -> *)
+(*     asr!ev = Some v -> *)
+(*     (forall p s, *)
+(*         In (p, s) l -> *)
+(*         v = posToValue p -> *)
+(*         stmnt_runp f *)
+(*                    {| assoc_blocking := asr; assoc_nonblocking := asrn |} *)
+(*                    {| assoc_blocking := asa; assoc_nonblocking := asan |} *)
+(*                    s *)
+(*                    {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *)
+(*                    {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> *)
+(*         stmnt_runp f *)
+(*                    {| assoc_blocking := asr; assoc_nonblocking := asrn |} *)
+(*                    {| assoc_blocking := asa; assoc_nonblocking := asan |} *)
+(*                    (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) *)
+(*                    {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *)
+(*                    {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). *)
+(* Proof. *)
+(*   induction l as [| a l IHl]. *)
+(*   - contradiction. *)
+(*   - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. *)
+(*     destruct a as [p' s']. simplify. *)
+(*     destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. *)
+(*     constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. *)
+(*     rewrite ASSOC. trivial. constructor. auto. *)
+(*     inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. *)
+(*     inv NOREP. eapply in_map with (f := fst) in INV. contradiction. *)
+
+(*     eapply stmnt_runp_Vcase_nomatch. constructor. simplify. *)
+(*     unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. *)
+(*     trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. *)
+(*     apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. *)
+(*     eapply in_map with (f := fst) in H0. auto. *)
+(*     apply Zle_relax. apply BOUND; auto. auto. *)
+
+(*     eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. *)
+(*     trivial. assumption. *)
+(* Qed. *)
+(* Hint Resolve transl_ctrl_correct : verilogproof. *)
+
+(* (* FIXME Probably wrong we probably need some statemnt about datapath_statement_runp *) *)
+(* Lemma transl_datapath_correct : *)
+(*   forall l v ev f asr asa asrn asan asr' asa' asrn' asan', *)
+(*     (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *)
+(*     list_norepet (List.map fst l) -> *)
+(*     asr!ev = Some v -> *)
+(*     (forall p s, *)
+(*         In (p, s) l -> *)
+(*         v = posToValue p -> *)
+(*         stmnt_runp f *)
+(*                    {| assoc_blocking := asr; assoc_nonblocking := asrn |} *)
+(*                    {| assoc_blocking := asa; assoc_nonblocking := asan |} *)
+(*                    s *)
+(*                    {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *)
+(*                    {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> *)
+(*         stmnt_runp f *)
+(*                    {| assoc_blocking := asr; assoc_nonblocking := asrn |} *)
+(*                    {| assoc_blocking := asa; assoc_nonblocking := asan |} *)
+(*                    (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) *)
+(*                    {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *)
+(*                    {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). *)
+(* Proof. Admitted. *)
+
+(* Lemma pc_wf : *)
+(*   forall A m p v, *)
+(*   (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *)
+(*   m!p = Some v -> *)
+(*   0 <= Z.pos p <= Int.max_unsigned. *)
+(* Proof. *)
+(*   intros A m p v LT S. apply Zle_relax. apply LT. *)
+(*   apply AssocMap.elements_correct in S. remember (p, v) as x. *)
+(*   exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. *)
+(* Qed. *)
+
+(* Lemma mis_stepp_decl : *)
+(*   forall l asr asa f, *)
+(*     mis_stepp f asr asa (map Vdeclaration l) asr asa. *)
+(* Proof. *)
+(*   induction l. *)
+(*   - intros. constructor. *)
+(*   - intros. simplify. econstructor. constructor. auto. *)
+(* Qed. *)
+(* Hint Resolve mis_stepp_decl : verilogproof. *)
 
 Section CORRECTNESS.
 
@@ -279,133 +279,133 @@ Section CORRECTNESS.
   Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
   Hint Resolve symbols_preserved : verilogproof.
 
-  Lemma function_ptr_translated:
-    forall (b: Values.block) (f: HTL.fundef),
-      Genv.find_funct_ptr ge b = Some f ->
-      exists tf,
-        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf.
-  Proof.
-    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
-    intros (cu & tf & P & Q & R); exists tf; auto.
-  Qed.
-  Hint Resolve function_ptr_translated : verilogproof.
-
-  Lemma functions_translated:
-    forall (v: Values.val) (f: HTL.fundef),
-      Genv.find_funct ge v = Some f ->
-      exists tf,
-        Genv.find_funct tge v = Some tf /\ transl_fundef f = tf.
-  Proof.
-    intros. exploit (Genv.find_funct_match TRANSL); eauto.
-    intros (cu & tf & P & Q & R); exists tf; auto.
-  Qed.
-  Hint Resolve functions_translated : verilogproof.
-
-  Lemma senv_preserved:
-    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
-  Proof.
-    intros. eapply (Genv.senv_match TRANSL).
-  Qed.
-  Hint Resolve senv_preserved : verilogproof.
-
-  Theorem transl_step_correct :
-    forall (S1 : HTL.state) t S2,
-      HTL.step ge S1 t S2 ->
-      forall (R1 : state),
-        match_states S1 R1 ->
-        exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
-  Proof.
-    induction 1; intros R1 MSTATE; inv MSTATE.
-    - econstructor; split. apply Smallstep.plus_one. econstructor.
-      assumption. assumption. eassumption. apply valueToPos_posToValue.
-      split. lia.
-      eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
-      split. lia. apply HP. eassumption. eassumption.
-      econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
-      simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
-      rewrite H. trivial.
-
-      econstructor. simpl. auto. auto.
-
-      eapply transl_ctrl_correct.
-      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto.
-      apply Maps.PTree.elements_keys_norepet. eassumption.
-      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
-           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption.
-           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
-           destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption. trivial.
-      }
-      apply Maps.PTree.elements_correct. eassumption. eassumption.
-
-      econstructor. econstructor.
-
-      { admit.
-      (*
-      eapply transl_list_correct.
-      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto.
-      apply Maps.PTree.elements_keys_norepet. eassumption.
-      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
-           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption.
-           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
-           destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption. trivial.
-      }
-      apply Maps.PTree.elements_correct. eassumption. eassumption.
-      *)
-      }
-
-      apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto.
-      rewrite valueToPos_posToValue. constructor; assumption. lia.
-    - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
-      constructor; assumption.
-    - econstructor; split. apply Smallstep.plus_one. constructor.
-
-      constructor. constructor.
-    - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
-
-      apply match_state. assumption.
-  Admitted.
-  Hint Resolve transl_step_correct : verilogproof.
-
-  Lemma transl_initial_states :
-    forall s1 : Smallstep.state (HTL.semantics prog),
-      Smallstep.initial_state (HTL.semantics prog) s1 ->
-      exists s2 : Smallstep.state (Verilog.semantics tprog),
-        Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2.
-  Proof.
-    induction 1.
-    econstructor; split. econstructor.
-    apply (Genv.init_mem_transf TRANSL); eauto.
-    rewrite symbols_preserved.
-    replace (AST.prog_main tprog) with (AST.prog_main prog); eauto.
-    symmetry; eapply Linking.match_program_main; eauto.
-    exploit function_ptr_translated; eauto. intros [tf [A B]].
-    inv B. eauto.
-    constructor.
-  Qed.
-  Hint Resolve transl_initial_states : verilogproof.
-
-  Lemma transl_final_states :
-    forall (s1 : Smallstep.state (HTL.semantics prog))
-           (s2 : Smallstep.state (Verilog.semantics tprog))
-           (r : Integers.Int.int),
-      match_states s1 s2 ->
-      Smallstep.final_state (HTL.semantics prog) s1 r ->
-      Smallstep.final_state (Verilog.semantics tprog) s2 r.
-  Proof.
-    intros. inv H0. inv H. inv H3. constructor. reflexivity.
-  Qed.
-  Hint Resolve transl_final_states : verilogproof.
+(*   Lemma function_ptr_translated: *)
+(*     forall (b: Values.block) (f: HTL.fundef), *)
+(*       Genv.find_funct_ptr ge b = Some f -> *)
+(*       exists tf, *)
+(*         Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. *)
+(*   Proof. *)
+(*     intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. *)
+(*     intros (cu & tf & P & Q & R); exists tf; auto. *)
+(*   Qed. *)
+(*   Hint Resolve function_ptr_translated : verilogproof. *)
+
+(*   Lemma functions_translated: *)
+(*     forall (v: Values.val) (f: HTL.fundef), *)
+(*       Genv.find_funct ge v = Some f -> *)
+(*       exists tf, *)
+(*         Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. *)
+(*   Proof. *)
+(*     intros. exploit (Genv.find_funct_match TRANSL); eauto. *)
+(*     intros (cu & tf & P & Q & R); exists tf; auto. *)
+(*   Qed. *)
+(*   Hint Resolve functions_translated : verilogproof. *)
+
+(*   Lemma senv_preserved: *)
+(*     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). *)
+(*   Proof. *)
+(*     intros. eapply (Genv.senv_match TRANSL). *)
+(*   Qed. *)
+(*   Hint Resolve senv_preserved : verilogproof. *)
+
+(*   Theorem transl_step_correct : *)
+(*     forall (S1 : HTL.state) t S2, *)
+(*       HTL.step ge S1 t S2 -> *)
+(*       forall (R1 : state), *)
+(*         match_states S1 R1 -> *)
+(*         exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. *)
+(*   Proof. *)
+(*     induction 1; intros R1 MSTATE; inv MSTATE. *)
+(*     - econstructor; split. apply Smallstep.plus_one. econstructor. *)
+(*       assumption. assumption. eassumption. apply valueToPos_posToValue. *)
+(*       split. lia. *)
+(*       eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *)
+(*       split. lia. apply HP. eassumption. eassumption. *)
+(*       econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. *)
+(*       simpl. unfold find_assocmap. unfold AssocMapExt.get_default. *)
+(*       rewrite H. trivial. *)
+
+(*       econstructor. simpl. auto. auto. *)
+
+(*       eapply transl_ctrl_correct. *)
+(*       intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. *)
+(*       apply Maps.PTree.elements_keys_norepet. eassumption. *)
+(*       2: { apply valueToPos_inj. apply unsigned_posToValue_le. *)
+(*            eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *)
+(*            split. lia. apply HP. eassumption. eassumption. *)
+(*            apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. *)
+(*            destruct HP as [HP _]. *)
+(*            split. lia. apply HP. eassumption. eassumption. trivial. *)
+(*       } *)
+(*       apply Maps.PTree.elements_correct. eassumption. eassumption. *)
+
+(*       econstructor. econstructor. *)
+
+(*       { admit. *)
+(*       (* *) *)
+(* (*       eapply transl_list_correct. *) *)
+(* (*       intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. *) *)
+(* (*       apply Maps.PTree.elements_keys_norepet. eassumption. *) *)
+(* (*       2: { apply valueToPos_inj. apply unsigned_posToValue_le. *) *)
+(* (*            eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) *)
+(* (*            split. lia. apply HP. eassumption. eassumption. *) *)
+(* (*            apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. *) *)
+(* (*            destruct HP as [HP _]. *) *)
+(* (*            split. lia. apply HP. eassumption. eassumption. trivial. *) *)
+(* (*       } *) *)
+(* (*       apply Maps.PTree.elements_correct. eassumption. eassumption. *) *)
+(* (*       *) *)
+(*       } *)
+
+(*       apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. *)
+(*       rewrite valueToPos_posToValue. constructor; assumption. lia. *)
+(*     - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. *)
+(*       constructor; assumption. *)
+(*     - econstructor; split. apply Smallstep.plus_one. constructor. *)
+
+(*       constructor. constructor. *)
+(*     - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. *)
+
+(*       apply match_state. assumption. *)
+(*   Admitted. *)
+(*   Hint Resolve transl_step_correct : verilogproof. *)
+
+(*   Lemma transl_initial_states : *)
+(*     forall s1 : Smallstep.state (HTL.semantics prog), *)
+(*       Smallstep.initial_state (HTL.semantics prog) s1 -> *)
+(*       exists s2 : Smallstep.state (Verilog.semantics tprog), *)
+(*         Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. *)
+(*   Proof. *)
+(*     induction 1. *)
+(*     econstructor; split. econstructor. *)
+(*     apply (Genv.init_mem_transf TRANSL); eauto. *)
+(*     rewrite symbols_preserved. *)
+(*     replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. *)
+(*     symmetry; eapply Linking.match_program_main; eauto. *)
+(*     exploit function_ptr_translated; eauto. intros [tf [A B]]. *)
+(*     inv B. eauto. *)
+(*     constructor. *)
+(*   Qed. *)
+(*   Hint Resolve transl_initial_states : verilogproof. *)
+
+(*   Lemma transl_final_states : *)
+(*     forall (s1 : Smallstep.state (HTL.semantics prog)) *)
+(*            (s2 : Smallstep.state (Verilog.semantics tprog)) *)
+(*            (r : Integers.Int.int), *)
+(*       match_states s1 s2 -> *)
+(*       Smallstep.final_state (HTL.semantics prog) s1 r -> *)
+(*       Smallstep.final_state (Verilog.semantics tprog) s2 r. *)
+(*   Proof. *)
+(*     intros. inv H0. inv H. inv H3. constructor. reflexivity. *)
+(*   Qed. *)
+(*   Hint Resolve transl_final_states : verilogproof. *)
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
   Proof.
-    eapply Smallstep.forward_simulation_plus; eauto with verilogproof.
-    apply senv_preserved.
-  Qed.
+    (* eapply Smallstep.forward_simulation_plus; eauto with verilogproof. *)
+    (* apply senv_preserved. *)
+    admit.
+  Admitted.
 
 End CORRECTNESS.
-*)