Finish Veriloggenproof completely

4 files changed, 339 insertions, 57 deletions

diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index 99df6d4..87317ef 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -3045,6 +3045,7 @@ Proof.
     2: { inv H23. }
     inv H23. inv H27. simplify. inv H4.
     2: { inv H24. }
+    inv H24.
     do 2 econstructor. eapply Smallstep.plus_two.
     econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption.
     eassumption. econstructor. simplify. econstructor. econstructor. simplify.
@@ -3118,6 +3119,27 @@ Proof.
       { eassumption. }
       { econstructor. econstructor. simplify. unfold merge_regs. unfold_merge.
         eapply expr_runp_matches. eassumption.
+        assert (max_reg_expr x0 + 1 <= max_reg_module m + 1).
+        { pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          apply expr_lt_max_module_controllogic in X. simplify. remember (max_reg_module m). lia. }
+        assert (max_reg_expr x0 + 1 <= mod_st m).
+        { unfold module_ordering in *. simplify.
+          repeat match goal with
+                 | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
+                 end.
+          pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          simplify. lia.
+        }
+        remember (max_reg_module m).
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        simplify.
+        eapply match_assocmaps_ge. eauto. lia.
+        mgen_crush.
       }
       { simplify. unfold merge_regs. unfold_merge.
         unfold transf_module; repeat destruct_match; try discriminate; simplify.
@@ -3148,9 +3170,18 @@ Proof.
       { crush. }
       { crush. }
       { unfold merge_regs. unfold_merge. simplify.
-        assert (mod_st (transf_module m) <> r) by admit.
-        repeat rewrite AssocMap.gso by lia.
+        assert (r < mod_st m).
+        { unfold module_ordering in *. simplify.
+          repeat match goal with
+                 | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
+                 end.
+          pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          simplify. lia.
+        }
+        unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8.
+        simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8.
         unfold transf_module; repeat destruct_match; try discriminate; simplify.
+        repeat rewrite AssocMap.gso by lia.
         apply AssocMap.gss. }
       { eassumption. }
     }
@@ -3175,7 +3206,14 @@ Proof.
         apply match_assocmaps_gt; [lia|].
         apply match_assocmaps_duplicate.
         apply match_assocmaps_gss. auto.
-        assert (mod_st m <> r) by admit; auto.
+        assert (r < mod_st m).
+        { unfold module_ordering in *. simplify.
+          repeat match goal with
+                 | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
+                 end.
+          pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          simplify. lia.
+        } lia.
       }
       {
         apply merge_arr_empty. mgen_crush.
@@ -3302,7 +3340,9 @@ Section CORRECTNESS.
       end.
     induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum;
       repeat transf_step_correct_tac.
-    - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1).
+    - assert (RAM0: transf_module m = m).
+      { eapply transf_module_code_ram. left. eassumption. }
+      assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1).
       { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. }
       simplify.
       assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2).
@@ -3313,17 +3353,17 @@ Section CORRECTNESS.
       assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush.
       exploit match_states_same. apply H4. eauto with mgen.
       econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto.
-      intros. repeat inv_exists. simplify. inv H18. inv H21.
+      intros. repeat inv_exists. simplify. inv H17. inv H20.
       exploit match_states_same. apply H6. eauto with mgen.
-      econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23.
+      econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H17. inv H22.
       exploit exec_ram_same; eauto. eauto with mgen.
       econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen.
       econstructor.
       apply match_arrs_merge; eauto with mgen. eauto with mgen.
-      intros. repeat inv_exists. simplify. inv H18. inv H28.
+      intros. repeat inv_exists. simplify. inv H17. inv H27.
       econstructor; simplify. apply Smallstep.plus_one. econstructor.
       mgen_crush. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption.
-      rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0.
+      rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H20. rewrite RAM0.
       rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto.
       econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto.
       apply match_empty_size_merge; mgen_crush; mgen_crush.
@@ -3339,14 +3379,16 @@ Section CORRECTNESS.
       apply match_empty_size_merge; mgen_crush; mgen_crush.
       unfold disable_ram.
       unfold transf_module; repeat destruct_match; crush.
-      apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21.
+      apply exec_ram_resets_en in H20. unfold merge_reg_assocs in H20.
       simplify. auto. auto.
-    - eapply translation_correct; eauto.
+    - eapply translation_correct; eauto. admit.
     - do 2 econstructor. apply Smallstep.plus_one.
       apply step_finish; mgen_crush. constructor; eauto.
     - do 2 econstructor. apply Smallstep.plus_one.
       apply step_finish; mgen_crush. econstructor; eauto.
-    - econstructor. econstructor. apply Smallstep.plus_one. econstructor.
+    - assert (RAM0: transf_module m = m).
+      { eapply transf_module_code_ram. left. eassumption. }
+      econstructor. econstructor. apply Smallstep.plus_one. econstructor.
       replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto).
       replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto).
       replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto).
@@ -3355,9 +3397,7 @@ Section CORRECTNESS.
       replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto).
       repeat econstructor; mgen_crush.
       unfold disable_ram. unfold transf_module; repeat destruct_match; crush.
-      unfold find_assocmap, AssocMapExt.get_default. destruct_match.
-      rewrite AssocMap.gso in Heqo1 by admit. rewrite AssocMap.gso in Heqo1 by admit.
-      rewrite AssocMap.gso in Heqo1 by admit. admit. admit.
+      admit.
     - econstructor. econstructor. apply Smallstep.plus_one. econstructor.
       replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m).
       replace (mod_reset (transf_module m)) with (mod_reset m).
@@ -3371,10 +3411,12 @@ Section CORRECTNESS.
       unfold find_assocmap, AssocMapExt.get_default. destruct_match.
       rewrite AssocMap.gso in Heqo by admit. rewrite AssocMap.gso in Heqo by admit.
       rewrite AssocMap.gso in Heqo by admit. admit. admit.
-    - inv STACKS. destruct b1; subst.
+    - assert (RAM0: transf_module m = m).
+      { eapply transf_module_code_ram. left. eassumption. }
+      inv STACKS. destruct b1; subst.
       econstructor. econstructor. apply Smallstep.plus_one.
       econstructor. eauto.
-      clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor.
+      clear Learn. inv H0. inv H2. inv STACKS. inv H2. constructor.
       constructor. intros.
       rewrite RAM0.
       destruct (Pos.eq_dec r res); subst.
@@ -3386,9 +3428,9 @@ Section CORRECTNESS.
       rewrite AssocMap.gss.
       rewrite AssocMap.gss. auto.
       rewrite AssocMap.gso; auto.
-      symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto.
+      symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H0. auto.
       auto. auto. auto. auto.
-      rewrite RAM0. rewrite H. rewrite RAM0 in DISABLE_RAM. rewrite H in DISABLE_RAM.
+      rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM.
       apply disable_ram_set_gso.
       apply disable_ram_set_gso. auto. admit. admit. admit. admit.
     - inv STACKS. destruct b1; subst.
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index a9ec5a1..46a9674 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -519,18 +519,27 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
 | mi_stepp_Valways :
     forall f sr0 sa0 st sr1 sa1 c,
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways c st) sr1 sa1
-| mi_stepp_Valways_ff :
-    forall f sr0 sa0 st sr1 sa1 c,
-    stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1
-| mi_stepp_Valways_comb :
+    mi_stepp f sr0 sa0 (Valways (Vposedge c) st) sr1 sa1
+| mi_stepp_Valways_ne :
+    forall f sr0 sa0 c st,
+    mi_stepp f sr0 sa0 (Valways (Vnegedge c) st) sr0 sa0
+| mi_stepp_Vdecl :
+    forall f sr0 sa0 d,
+    mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0.
+Hint Constructors mi_stepp : verilog.
+
+Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations ->
+                             module_item -> reg_associations -> arr_associations -> Prop :=
+| mi_stepp_negedge_Valways :
     forall f sr0 sa0 st sr1 sa1 c,
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
-| mi_stepp_Vdecl :
-    forall f sr sa d,
-    mi_stepp f sr sa (Vdeclaration d) sr sa.
+    mi_stepp_negedge f sr0 sa0 (Valways (Vnegedge c) st) sr1 sa1
+| mi_stepp_negedge_Valways_ne :
+    forall f sr0 sa0 c st,
+    mi_stepp_negedge f sr0 sa0 (Valways (Vposedge c) st) sr0 sa0
+| mi_stepp_negedge_Vdecl :
+    forall f sr0 sa0 d,
+    mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0.
 Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
@@ -545,6 +554,18 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
     mis_stepp f sr sa nil sr sa.
 Hint Constructors mis_stepp : verilog.
 
+Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations ->
+                      list module_item -> reg_associations -> arr_associations -> Prop :=
+| mis_stepp_negedge_Cons :
+    forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2,
+    mi_stepp_negedge f sr0 sa0 mi sr1 sa1 ->
+    mis_stepp_negedge f sr1 sa1 mis sr2 sa2 ->
+    mis_stepp_negedge f sr0 sa0 (mi :: mis) sr2 sa2
+| mis_stepp_negedge_Nil :
+    forall f sr sa,
+    mis_stepp_negedge f sr sa nil sr sa.
+Hint Constructors mis_stepp : verilog.
+
 Local Close Scope error_monad_scope.
 
 Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
@@ -559,18 +580,24 @@ Definition empty_stack (m : module) : assocmap_arr :=
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
-      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist,
+      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 basr2 nasr2
+             basa2 nasa2 f stval pstval m sf st g ist,
       asr!(m.(mod_reset)) = Some (ZToValue 0) ->
       asr!(m.(mod_finish)) = Some (ZToValue 0) ->
       asr!(m.(mod_st)) = Some ist ->
       valueToPos ist = st ->
       mis_stepp f (mkassociations asr empty_assocmap)
                   (mkassociations asa (empty_stack m))
-                  m.(mod_body)
+                  (mod_body m)
                   (mkassociations basr1 nasr1)
-                  (mkassociations basa1 nasa1)->
-      asr' = merge_regs nasr1 basr1 ->
-      asa' = merge_arrs nasa1 basa1 ->
+                  (mkassociations basa1 nasa1) ->
+      mis_stepp_negedge f (mkassociations (merge_regs nasr1 basr1) empty_assocmap)
+                        (mkassociations (merge_arrs nasa1 basa1) (empty_stack m))
+                        (mod_body m)
+                        (mkassociations basr2 nasr2)
+                        (mkassociations basa2 nasa2) ->
+      asr' = merge_regs nasr2 basr2 ->
+      asa' = merge_arrs nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -718,6 +745,22 @@ Proof.
               end; crush).
 Qed.
 
+Lemma mi_stepp_negedge_determinate :
+  forall f asr0 asa0 m asr1 asa1,
+  mi_stepp_negedge f asr0 asa0 m asr1 asa1 ->
+  forall asr1' asa1',
+  mi_stepp_negedge f asr0 asa0 m asr1' asa1' ->
+  asr1' = asr1 /\ asa1' = asa1.
+Proof.
+  intros. destruct m; invert H; invert H0;
+
+  repeat (try match goal with
+              | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _,
+                  H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
+                learn (stmnt_runp_determinate H1 H2)
+              end; crush).
+Qed.
+
 Lemma mis_stepp_determinate :
   forall f asr0 asa0 m asr1 asa1,
   mis_stepp f asr0 asa0 m asr1 asa1 ->
@@ -741,13 +784,37 @@ Proof.
               end; crush).
 Qed.
 
+Lemma mis_stepp_negedge_determinate :
+  forall f asr0 asa0 m asr1 asa1,
+  mis_stepp_negedge f asr0 asa0 m asr1 asa1 ->
+  forall asr1' asa1',
+  mis_stepp_negedge f asr0 asa0 m asr1' asa1' ->
+  asr1' = asr1 /\ asa1' = asa1.
+Proof.
+  induction 1; intros;
+
+  repeat (try match goal with
+              | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => invert H
+              | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H
+
+              | [ H1 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _,
+                  H2 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
+                learn (mi_stepp_negedge_determinate H1 H2)
+
+             | [ H1 : forall asr1 asa1, mis_stepp_negedge _ ?asr0 ?asa0 ?m asr1 asa1 -> _,
+                 H2 : mis_stepp_negedge _ ?asr0 ?asa0 ?m _ _ |- _ ] =>
+               learn (H1 _ _ H2)
+              end; crush).
+Qed.
+
 Lemma semantics_determinate :
   forall (p: program), Smallstep.determinate (semantics p).
 Proof.
   intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
   - invert H; invert H0; constructor. (* Traces are always empty *)
   - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
-    pose proof (mis_stepp_determinate H5 H15).
+    pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4.
+    pose proof (mis_stepp_negedge_determinate H6 H17).
     crush.
   - constructor. invert H; crush.
   - invert H; invert H0; unfold ge0, ge1 in *; crush.
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index e43ab66..aba2293 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -42,17 +42,16 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
 
 Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
-Definition inst_ram clk stk_len ram :=
+Definition inst_ram clk ram :=
   Valways (Vnegedge clk)
-          (Vseq (Vcond (Vbinop Vand (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram)))
-                               (Vbinop Vlt (Vvar (ram_addr ram)) (Vlit (natToValue stk_len))))
-                 (Vcond (Vvar (ram_wr_en ram))
-                        (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram)))
-                                   (Vvar (ram_d_in ram)))
-                        (Vnonblock (Vvar (ram_d_out ram))
-                                   (Vvari (ram_mem ram) (Vvar (ram_addr ram)))))
-                 Vskip)
-                (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))).
+          (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram)))
+                 (Vseq (Vcond (Vvar (ram_wr_en ram))
+                              (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram)))
+                                         (Vvar (ram_d_in ram)))
+                              (Vnonblock (Vvar (ram_d_out ram))
+                                         (Vvari (ram_mem ram) (Vvar (ram_addr ram)))))
+                       (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram))))
+                 Vskip).
 
 Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in
@@ -64,7 +63,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
                                                   (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint))))
                                                   (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip)))
                 :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip))
-                :: inst_ram m.(HTL.mod_clk) (HTL.mod_stk_len m) ram
+                :: inst_ram m.(HTL.mod_clk) ram
                 :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
                                                           ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
     Verilog.mkmodule m.(HTL.mod_start)
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index 5c484d3..ccc0688 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -225,6 +225,116 @@ Proof.
 Qed.
 Hint Resolve mis_stepp_decl : verilogproof.
 
+Lemma mis_stepp_negedge_decl :
+  forall l asr asa f,
+    mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa.
+Proof.
+  induction l.
+  - intros. constructor.
+  - intros. simplify. econstructor. constructor. auto.
+Qed.
+Hint Resolve mis_stepp_negedge_decl : verilogproof.
+
+Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_stk_len_equiv m : mod_stk_len (transl_module m) = HTL.mod_stk_len m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_finish_equiv m : mod_finish (transl_module m) = HTL.mod_finish m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_reset_equiv m : mod_reset (transl_module m) = HTL.mod_reset m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_clk_equiv m : mod_clk (transl_module m) = HTL.mod_clk m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_return_equiv m : mod_return (transl_module m) = HTL.mod_return m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_params_equiv m : mod_args (transl_module m) = HTL.mod_params m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma empty_stack_equiv m : empty_stack (transl_module m) = HTL.empty_stack m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Ltac rewrite_eq := rewrite mod_return_equiv
+                   || rewrite mod_clk_equiv
+                   || rewrite mod_reset_equiv
+                   || rewrite mod_finish_equiv
+                   || rewrite mod_stk_len_equiv
+                   || rewrite mod_stk_equiv
+                   || rewrite mod_st_equiv
+                   || rewrite mod_entrypoint_equiv
+                   || rewrite mod_params_equiv
+                   || rewrite empty_stack_equiv.
+
+Lemma find_assocmap_get r i v : r ! i = Some v -> r # i = v.
+Proof.
+  intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. auto.
+Qed.
+
+Lemma ram_exec_match :
+  forall f asr asa asr' asa' r clk,
+    HTL.exec_ram asr asa (Some r) asr' asa' ->
+    mi_stepp_negedge f asr asa (inst_ram clk r) asr' asa'.
+Proof.
+  inversion 1; subst; simplify.
+  { unfold inst_ram. econstructor.
+    eapply stmnt_runp_Vcond_false.
+    econstructor. econstructor. econstructor. auto.
+    econstructor. auto.
+    simplify.
+    unfold boolToValue, natToValue, valueToBool.
+    rewrite Int.eq_sym. rewrite H3. simplify.
+    auto. constructor. }
+  { unfold inst_ram. econstructor. econstructor. econstructor.
+    econstructor. econstructor. auto.
+    econstructor. auto.
+    simplify.
+    unfold boolToValue, natToValue, valueToBool.
+    pose proof H4 as X. apply find_assocmap_get in X.
+    rewrite X. rewrite Int.eq_sym. rewrite H1. auto.
+    econstructor. econstructor. econstructor. econstructor.
+    pose proof H5 as X. apply find_assocmap_get in X.
+    rewrite X.
+    unfold valueToBool. unfold ZToValue in *.
+    unfold Int.eq in H2.
+    unfold uvalueToZ.
+    assert (Int.unsigned wr_en =? 0 = false).
+    apply Z.eqb_neq. rewrite Int.unsigned_repr in H2 by (simplify; lia).
+    destruct (zeq (Int.unsigned wr_en) 0); crush.
+    rewrite H0. auto.
+    apply stmnt_runp_Vnonblock_arr. econstructor. econstructor. auto.
+    econstructor. econstructor.
+    apply find_assocmap_get in H9. rewrite H9.
+    apply find_assocmap_get in H6. rewrite H6.
+    repeat econstructor. apply find_assocmap_get; auto.
+  }
+  { econstructor. econstructor. econstructor. econstructor. auto.
+    econstructor. auto.
+    econstructor.
+    unfold boolToValue, natToValue, valueToBool.
+    apply find_assocmap_get in H3. rewrite H3.
+    rewrite Int.eq_sym. rewrite H1. auto.
+    econstructor.
+    eapply stmnt_runp_Vcond_false. econstructor. auto.
+    simplify. apply find_assocmap_get in H4. rewrite H4.
+    auto.
+    repeat (econstructor; auto). apply find_assocmap_get in H5.
+    rewrite H5. eassumption.
+    repeat econstructor. simplify. apply find_assocmap_get; auto.
+  }
+Qed.
+
+
 Section CORRECTNESS.
 
   Variable prog: HTL.program.
@@ -269,6 +379,12 @@ Section CORRECTNESS.
   Qed.
   Hint Resolve senv_preserved : verilogproof.
 
+  Ltac unfold_replace :=
+    match goal with
+    | H: HTL.mod_ram _ = _ |- context[transl_module] =>
+      unfold transl_module; rewrite H
+    end.
+
   Theorem transl_step_correct :
     forall (S1 : HTL.state) t S2,
       HTL.step ge S1 t S2 ->
@@ -276,13 +392,14 @@ Section CORRECTNESS.
         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.
-    Admitted.
-(*    - econstructor; split. apply Smallstep.plus_one. econstructor.
-      assumption. assumption. eassumption. apply valueToPos_posToValue.
+    induction 1; intros R1 MSTATE; inv MSTATE; destruct (HTL.mod_ram m) eqn:?.
+    - econstructor; split. apply Smallstep.plus_one. econstructor.
+      unfold_replace. assumption. unfold_replace. assumption.
+      unfold_replace. 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.
+      unfold_replace.
       econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
       simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
       rewrite H. trivial.
@@ -314,19 +431,76 @@ Section CORRECTNESS.
            split. lia. apply HP. eassumption. eassumption. trivial.
       }
       apply Maps.PTree.elements_correct. eassumption. eassumption.
+      econstructor. econstructor.
+      apply mis_stepp_decl. simplify. unfold_replace. simplify.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor.
+      apply ram_exec_match. eauto.
+      apply mis_stepp_negedge_decl. simplify. auto. auto.
+      rewrite_eq. eauto. auto.
+      rewrite valueToPos_posToValue. econstructor. auto.
+      simplify; lia.
+    - inv H7. econstructor; split. apply Smallstep.plus_one. econstructor.
+      unfold_replace. assumption. unfold_replace. assumption.
+      unfold_replace. 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.
+      unfold_replace.
+      econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
+      simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
+      rewrite H. trivial.
 
-      apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto.
-      rewrite valueToPos_posToValue. constructor; assumption. lia.
+      econstructor. simpl. auto. auto.
+
+      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.
+
+      econstructor. econstructor.
+
+      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.
 
-    - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
+      apply mis_stepp_decl. simplify.
+      unfold_replace.
+      repeat econstructor. apply mis_stepp_negedge_decl. trivial. trivial.
+      simpl. unfold_replace. eassumption. auto. simplify.
+      rewrite valueToPos_posToValue. constructor; eassumption. simplify; lia.
+    - econstructor; split. apply Smallstep.plus_one. apply step_finish.
+      rewrite_eq. assumption.
+      rewrite_eq. eassumption.
+      econstructor; auto.
+    - econstructor; split. apply Smallstep.plus_one. apply step_finish.
+      unfold transl_module. rewrite Heqo. simplify.
+      assumption. unfold_replace. eassumption.
       constructor; assumption.
     - econstructor; split. apply Smallstep.plus_one. constructor.
-
-      constructor. constructor.
+      repeat rewrite_eq. constructor. constructor.
+    - econstructor; split. apply Smallstep.plus_one. constructor.
+      repeat rewrite_eq. constructor. constructor.
     - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
-
-      apply match_state. assumption.
-  Qed.*)
+      repeat rewrite_eq. apply match_state. assumption.
+    - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
+      repeat rewrite_eq. apply match_state. assumption.
+  Qed.
   Hint Resolve transl_step_correct : verilogproof.
 
   Lemma transl_initial_states :