Prove idempotency of array merge

2 files changed, 86 insertions, 20 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 2e4987d..6dc1856 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -52,6 +52,7 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
     Z.pos p0 <= Integers.Int.max_unsigned.
 
 Record ram := mk_ram {
+  ram_size: nat;
   ram_mem: reg;
   ram_en: reg;
   ram_addr: reg;
@@ -128,8 +129,8 @@ Inductive exec_ram:
   Prop :=
 | exec_ram_Some_idle:
     forall ra ar ram,
-    (Verilog.assoc_blocking ra)!(ram_en ram) = Some (ZToValue 0) ->
-    exec_ram ra ar (Some ram) ra ar
+      (Verilog.assoc_blocking ra)#(ram_en ram, 32) = ZToValue 0 ->
+      exec_ram ra ar (Some ram) ra ar
 | exec_ram_Some_write:
     forall ra ar ram d_in addr en wr_en,
       en <> ZToValue 0 ->
@@ -141,10 +142,13 @@ Inductive exec_ram:
       exec_ram ra ar (Some ram) ra
                (Verilog.nonblock_arr (ram_mem ram) (valueToNat addr) ar d_in)
 | exec_ram_Some_load:
-    forall ra ar ram addr v_d_out,
+    forall ra ar ram addr v_d_out en,
+      en <> ZToValue 0 ->
+      (Verilog.assoc_blocking ra)!(ram_en ram) = Some en ->
       (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 0) ->
       (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr ->
-      Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem ram) (valueToNat addr) = Some v_d_out ->
+      Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar)
+                                  (ram_mem ram) (valueToNat addr) = Some v_d_out ->
       exec_ram ra ar (Some ram) (Verilog.nonblock_reg (ram_d_out ram) ra v_d_out) ar
 | exec_ram_None:
     forall r a,
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index fa4946f..7ce61b3 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -177,7 +177,8 @@ Definition transf_module (m: module): module :=
   let d_in := max_reg+3 in
   let d_out := max_reg+4 in
   let wr_en := max_reg+5 in
-  let ram := mk_ram (mod_stk m) en addr d_in d_out wr_en in
+  let new_size := (2 ^ Nat.log2_up m.(mod_stk_len))%nat in
+  let ram := mk_ram new_size (mod_stk m) en addr d_in d_out wr_en in
   match transf_code ram (mod_datapath m) (mod_controllogic m) with
   | (nd, nc) =>
     mkmodule m.(mod_params)
@@ -186,7 +187,7 @@ Definition transf_module (m: module): module :=
              m.(mod_entrypoint)
              m.(mod_st)
              m.(mod_stk)
-             (2 ^ Nat.log2_up m.(mod_stk_len))%nat
+             new_size
              m.(mod_finish)
              m.(mod_return)
              m.(mod_start)
@@ -236,6 +237,18 @@ Inductive match_states : HTL.state -> HTL.state -> Prop :=
       (HTL.Callstate nil (transf_module m) nil).
 Hint Constructors match_states : htlproof.
 
+Definition empty_stack_ram r :=
+  AssocMap.set (ram_mem r) (Array.arr_repeat None (ram_size r)) (AssocMap.empty arr).
+
+Definition empty_stack' len st :=
+  AssocMap.set st (Array.arr_repeat None len) (AssocMap.empty arr).
+
+Definition merge_reg_assocs r :=
+  Verilog.mkassociations (Verilog.merge_regs (assoc_nonblocking r) (assoc_blocking r)) empty_assocmap.
+
+Definition merge_arr_assocs st len r :=
+  Verilog.mkassociations (Verilog.merge_arrs (assoc_nonblocking r) (assoc_blocking r)) (empty_stack' len st).
+
 Inductive match_reg_assocs : reg_associations -> reg_associations -> Prop :=
   match_reg_association:
     forall rab rab' ran ran',
@@ -276,30 +289,79 @@ Definition forall_ram (P: reg -> Prop) ram :=
   /\ P (ram_d_in ram)
   /\ P (ram_d_out ram).
 
-Definition exec_all d_s c_s r rs1 ar1 rs4 ar4 :=
+Definition exec_all d_s c_s rs1 ar1 rs3 ar3 :=
+  exists f rs2 ar2,
+    stmnt_runp f rs1 ar1 d_s rs2 ar2
+    /\ stmnt_runp f rs2 ar2 c_s rs3 ar3.
+
+Definition exec_all_ram r d_s c_s rs1 ar1 rs4 ar4 :=
   exists f rs2 ar2 rs3 ar3,
     stmnt_runp f rs1 ar1 d_s rs2 ar2
     /\ stmnt_runp f rs2 ar2 c_s rs3 ar3
-    /\ exec_ram
-         (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap)
-         (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m))
-         r rs4 ar4.
+    /\ exec_ram (merge_reg_assocs rs3) (merge_arr_assocs (ram_mem r) (ram_size r) ar3) (Some r) rs4 ar4.
+
+Lemma merge_reg_idempotent :
+  forall rs, merge_reg_assocs (merge_reg_assocs rs) = merge_reg_assocs rs.
+Proof. auto. Qed.
+Hint Rewrite merge_reg_idempotent : mgen.
+
+Lemma merge_arr_idempotent :
+  forall ar st len v v',
+    (assoc_nonblocking ar)!st = Some v ->
+    (assoc_blocking ar)!st = Some v' ->
+    arr_length v' = len ->
+    arr_length v = len ->
+    (assoc_blocking (merge_arr_assocs st len (merge_arr_assocs st len ar)))!st
+    = (assoc_blocking (merge_arr_assocs st len ar))!st
+    /\ (assoc_nonblocking (merge_arr_assocs st len (merge_arr_assocs st len ar)))!st
+    = (assoc_nonblocking (merge_arr_assocs st len ar))!st.
+Proof.
+  split; simplify; eauto.
+  unfold merge_arrs.
+  rewrite AssocMap.gcombine by reflexivity.
+  unfold empty_stack'.
+  rewrite AssocMap.gss.
+  setoid_rewrite merge_arr_empty2; auto.
+  rewrite AssocMap.gcombine by reflexivity.
+  unfold merge_arr, arr.
+  rewrite H. rewrite H0. auto.
+  unfold combine.
+  simplify.
+  rewrite list_combine_length.
+  rewrite (arr_wf v). rewrite (arr_wf v').
+  lia.
+Qed.
 
-Definition behaviour_correct d c r d' c' r' :=
-  forall rs1 ar1 rs4 ar4 d_s c_s i,
+Definition behaviour_correct d c d' c' r' :=
+  forall rs1 ar1 rs2 ar2 d_s c_s i,
     PTree.get i d = Some d_s ->
     PTree.get i c = Some c_s ->
-    exec_all d_s c_s r rs1 ar1 rs4 ar4 ->
-    exists d_s' c_s' trs4 tar4,
+    exec_all d_s c_s rs1 ar1 rs2 ar2 ->
+    exists d_s' c_s' trs2 tar2,
       PTree.get i d' = Some d_s'
       /\ PTree.get i c' = Some c_s'
-      /\ exec_all d_s' c_s' r' rs1 ar1 trs4 tar4
-      /\ match_reg_assocs rs4 trs4
-      /\ match_arr_assocs ar4 tar4.
+      /\ exec_all_ram r' d_s' c_s' rs1 ar1 trs2 tar2
+      /\ match_reg_assocs (merge_reg_assocs rs2) (merge_reg_assocs trs2)
+      /\ match_arr_assocs (merge_arr_assocs ar2 r') (merge_arr_assocs tar2 r').
 
 Lemma behaviour_correct_equiv :
-  forall d c r, behaviour_correct d c r d c r.
-Proof. intros; unfold behaviour_correct; repeat (eexists; mgen_crush). Qed.
+  forall d c r,
+    forall_ram (fun x => max_stmnt_tree d < x /\ max_stmnt_tree c < x) r ->
+    behaviour_correct d c d c r.
+Proof.
+  intros; unfold behaviour_correct.
+  intros. exists d_s. exists c_s.
+  unfold exec_all in *. inv H2. inv H3. inv H2. inv H3.
+  econstructor. econstructor.
+  simplify; auto.
+  unfold exec_all_ram.
+  exists x. exists x0. exists x1. econstructor. econstructor.
+  simplify; eauto.
+  econstructor.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  assert ((assoc_blocking (merge_reg_assocs rs2)) ! (ram_en r) = None) by admit.
+  destruct_match; try discriminate; auto.
+Qed.
 Hint Resolve behaviour_correct_equiv : mgen.
 
 Lemma stmnt_runp_gtassoc :