Basically done with proof

6 files changed, 62 insertions, 18 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index e614246..61ea541 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -92,6 +92,7 @@ Record module: Type :=
     mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath;
     mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk;
     mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r';
+    mod_params_wf : Forall (Pos.gt mod_st) mod_params;
   }.
 
 Definition fundef := AST.fundef module.
@@ -338,3 +339,16 @@ Proof.
   inversion 1 as [ Hv | Hv ]; unfold max_reg_module;
   apply max_reg_stmnt_le_stmnt_tree in Hv; lia.
 Qed.
+
+Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l.
+Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed.
+
+Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True}.
+  refine (
+      match bool_dec (max_list l <? st) true with
+      | left _ => left _
+      | _ => _
+      end
+    ); auto.
+  apply max_list_correct. apply Pos.ltb_lt in e. lia.
+Qed.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 50defee..7ce6c7a 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -817,9 +817,10 @@ Definition transf_module (f: function) : mon HTL.module.
               Integers.Int.max_unsigned,
           zle (Z.pos (max_pc_map current_state.(st_controllogic)))
               Integers.Int.max_unsigned,
-          decide_order (st_st current_state) fin rtrn stack start rst clk
+          decide_order (st_st current_state) fin rtrn stack start rst clk,
+          max_list_dec (fn_params f) (st_st current_state)
     with
-    | left LEDATA, left LECTRL, left MORD =>
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
         ret (HTL.mkmodule
            f.(fn_params)
            current_state.(st_datapath)
@@ -838,8 +839,9 @@ Definition transf_module (f: function) : mon HTL.module.
            None
            (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
            MORD
-           _)
-    | _, _, _ => error (Errors.msg "More than 2^32 states.")
+           _
+           WFPARAMS)
+    | _, _, _, _ => error (Errors.msg "More than 2^32 states.")
     end
   else error (Errors.msg "Stack size misalignment.")); discriminate.
 Defined.
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index b55d7a3..4d60a24 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -608,9 +608,10 @@ Definition transf_module (f: function) : mon HTL.module.
     do current_state <- get;
     match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
           zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned,
-          decide_order (st_st current_state) fin rtrn stack start rst clk
+          decide_order (st_st current_state) fin rtrn stack start rst clk,
+          max_list_dec (RTL.fn_params f) (st_st current_state)
     with
-    | left LEDATA, left LECTRL, left MORD =>
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
         ret (HTL.mkmodule
            f.(RTL.fn_params)
            current_state.(st_datapath)
@@ -629,8 +630,9 @@ Definition transf_module (f: function) : mon HTL.module.
            None
            (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
            MORD
-           _)
-    | _, _, _ => error (Errors.msg "More than 2^32 states.")
+           _
+           WFPARAMS)
+    | _, _, _, _ => error (Errors.msg "More than 2^32 states.")
     end
   else error (Errors.msg "Stack size misalignment.")); discriminate.
 Defined.
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 3b5496f..1aac3b7 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -2602,7 +2602,7 @@ Section CORRECTNESS.
       constructor. constructor. constructor.
 
       unfold state_st_wf in WF; big_tac; eauto.
-      destruct wf as [HCTRL HDATA]. apply HCTRL.
+      destruct wf1 as [HCTRL HDATA]. apply HCTRL.
       apply AssocMapExt.elements_iff. eexists.
       match goal with H: control ! pc = Some _ |- _ => apply H end.
 
@@ -2632,7 +2632,7 @@ Section CORRECTNESS.
 
       unfold state_st_wf in WF; big_tac; eauto.
 
-      destruct wf as [HCTRL HDATA]. apply HCTRL.
+      destruct wf1 as [HCTRL HDATA]. apply HCTRL.
       apply AssocMapExt.elements_iff. eexists.
       match goal with H: control ! pc = Some _ |- _ => apply H end.
 
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 6a10fa2..16bdcaf 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -178,12 +178,12 @@ Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3,
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3 wf4,
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                        st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3) ->
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3 wf4) ->
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index 8453263..06e0aec 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -207,9 +207,9 @@ Definition transf_module (m: module): module.
                        (AssocMap.set m.(mod_stk)
                                  (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls))
                  (Some ram)
-                 _ _ _
+                 _ (mod_ordering_wf m) _ (mod_params_wf m)
   | _, _ => m
-  end). apply is_wf. exact (mod_ordering_wf m).
+  end). apply is_wf.
   inversion 1; subst. auto using module_ram_wf'.
 Defined.
 
@@ -3139,10 +3139,18 @@ Proof.
 Qed.
 Hint Resolve disable_ram_set_gso : mgen.
 
-Lemma disable_ram_None : forall rs, disable_ram None rs.
+Lemma disable_ram_None rs : disable_ram None rs.
 Proof. unfold disable_ram; auto. Qed.
 Hint Resolve disable_ram_None : mgen.
 
+Lemma init_regs_equal_empty l st :
+  Forall (Pos.gt st) l -> (init_regs nil l) ! st = None.
+Proof. induction l; simplify; apply AssocMap.gempty. Qed.
+
+Lemma forall_lt_num :
+  forall l p p', Forall (Pos.gt p) l -> p < p' -> Forall (Pos.gt p') l.
+Proof. induction l; crush; inv H; constructor; [lia | eauto]. Qed.
+
 Section CORRECTNESS.
 
   Context (prog tprog: program).
@@ -3259,7 +3267,17 @@ 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.
-      admit.
+      pose proof (mod_ordering_wf m); unfold module_ordering in *.
+      pose proof (mod_params_wf m).
+      pose proof (mod_ram_wf m r Heqo0).
+      pose proof (ram_ordering r).
+      simplify.
+      repeat rewrite find_assocmap_gso by lia.
+      assert ((init_regs nil (mod_params m)) ! (ram_en r) = None).
+      { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. }
+      assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None).
+      { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. }
+      unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto.
     - 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).
@@ -3270,7 +3288,15 @@ Section CORRECTNESS.
       all: try solve [unfold transf_module; repeat destruct_match; mgen_crush].
       repeat econstructor; mgen_crush.
       unfold disable_ram. unfold transf_module; repeat destruct_match; crush.
-      admit.
+      unfold max_reg_module.
+      repeat rewrite find_assocmap_gso by lia.
+      assert (max_reg_module m + 1 > max_list (mod_params m)).
+      { unfold max_reg_module. lia. }
+      apply max_list_correct in H0.
+      unfold find_assocmap, AssocMapExt.get_default.
+      rewrite init_regs_equal_empty. rewrite init_regs_equal_empty. auto.
+      eapply forall_lt_num. eassumption. unfold max_reg_module. lia.
+      eapply forall_lt_num. eassumption. unfold max_reg_module. lia.
     - inv STACKS. destruct b1; subst.
       econstructor. econstructor. apply Smallstep.plus_one.
       econstructor. eauto.
@@ -3329,7 +3355,7 @@ Section CORRECTNESS.
       simplify. unfold max_reg_module. lia.
       simplify. unfold max_reg_module. lia.
       simplify. unfold max_reg_module. lia.
-  Admitted.
+  Qed.
   Hint Resolve transf_step_correct : mgen.
 
   Lemma transf_initial_states :