From 8ff5b3e6425ebd818ba593848f5c21e687969d2b Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Wed, 17 Jun 2026 17:20:23 +0100
Subject: [PATCH 01/13] first commit

---
 DatapathVerification/BitHeap/BVComb.lean      | 71 +++++++++++++++++++
 DatapathVerification/BitHeap/BitHeap.lean     | 20 ++++++
 DatapathVerification/BitHeap/Circuit.lean     | 12 ++++
 .../BitHeap/Examples/Examples.lean            | 29 ++++++++
 4 files changed, 132 insertions(+)
 create mode 100644 DatapathVerification/BitHeap/BVComb.lean

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
new file mode 100644
index 0000000..2354a4b
--- /dev/null
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -0,0 +1,71 @@
+import DatapathVerification.BitHeap.BitHeap
+import DatapathVerification.BitHeap.Circuit
+import DatapathVerification.BitHeap.DaddaTree
+
+open BitHeap
+namespace Comb
+
+inductive ArithBinopKind
+| add
+| mul
+
+-- inductive ArithUnopKind
+-- | neg
+
+-- inductive BooleanBinopKind
+-- | and | or | xor
+
+inductive ArithCircuit
+  | var (width : Nat) (varIndex : Nat)
+  | arithbinop (kind : ArithBinopKind) (width : Nat) (l r : ArithCircuit)
+  -- | arithunop (kind : ArithUnopKind) (width : Nat) (arg : ArithCircuit)
+  -- | bvbinop (kind : BooleanBinopKind) (width : Nat) (l r : ArithCircuit)
+
+/--
+Convert a bitheap into a new bitheap that has a single row,
+by building a Dadda tree of adders to reduce the bitheap to a single row.
+-/
+def BitHeap.toSingleRow : BitHeap → CircuitVector
+  | bh =>
+    let (pp1, pp2) := DaddaTree.DaddaTree bh
+    -- add pp1 and pp2 to get the final row
+    sorry
+
+namespace ArithCircuit
+/--
+Given a bitvector (x : BV 3), but a bitheap
+```
+*   *  *
+x2 x1 x0
+```
+-/
+def bitheapOfVar (width : Nat) (varIndex : Nat) : BitHeap :=
+  --  I want to create a bitheap that has one bit-variable per bit in the bitvector variable.
+  -- | We need to know that this index is unique which is a gigantic pain.
+  List.range width |>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * width + i))) BitHeap.empty
+
+def toBitHeap (c : ArithCircuit) : BitHeap :=
+  match c with
+  | .var width varIndex => bitheapOfVar width varIndex
+  | .arithbinop kind width l r =>
+    match kind with
+    | .add => (toBitHeap l).addBitHeap (toBitHeap r)
+    | .mul => (toBitHeap l).mulBitHeap (toBitHeap r)
+  -- | .arithunop kind width arg =>
+  --   match kind with
+  --   | .neg => (toBitHeap arg).negBitHeap
+  -- | .bvbinop kind width l r =>
+  --   match kind with
+  --   | .and =>
+  --     let lRow := (l.toBitHeap).toSingleRow
+  --     let rRow := (r.toBitHeap).toSingleRow
+  --     let newRow := Array.zipWith (fun lBit rBit => Circuit.and lBit rBit) lRow rRow
+  --     BitHeap.fromRow newRow
+
+def toCircuitVector (c : ArithCircuit) : CircuitVector :=
+  let bh := c.toBitHeap
+  bh.toSingleRow
+
+end ArithCircuit
+
+end Comb
diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 789f2c6..2075323 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -2,6 +2,7 @@ import Std.Data.HashMap
 import Std.Data.HashSet
 import DatapathVerification.BitHeap.Circuit
 import DatapathVerification.BitHeap.Column
+import Std.Tactic.BVDecide
 
 structure BitHeap where
   width : Nat
@@ -67,6 +68,25 @@ partial def addBit (column : Nat) (c : Circuit) (h : BitHeap) : BitHeap :=
   else
     ⟨h.width, h.columns.insert column (col.insert c)⟩
 
+-- TODO: make this variable size add
+def addBitHeap (h1 h2 : BitHeap) : BitHeap :=
+  let h : BitHeap := ⟨h1.width, Std.HashMap.emptyWithCapacity 0⟩
+  let h := h1.columns.fold (fun acc col column =>
+             column.elems.toList.foldl (fun acc' c => acc'.addBit col c) acc) h
+  let h := h2.columns.fold (fun acc col column =>
+             column.elems.toList.foldl (fun acc' c => acc'.addBit col c) acc) h
+  h
+
+def mulBitHeap (h1 h2 : BitHeap) : BitHeap :=
+  let newWidth := max h1.width h2.width
+  let h : BitHeap := ⟨newWidth, Std.HashMap.emptyWithCapacity 0⟩
+  let h := h1.columns.fold (fun acc col1 column1 =>
+             h2.columns.fold (fun acc' col2 column2 =>
+               column1.elems.toList.foldl (fun acc'' c1 =>
+                 column2.elems.toList.foldl (fun acc''' c2 =>
+                   acc'''.addBit (col1 + col2) (Circuit.binop .and c1 c2)) acc'') acc') acc) h
+  h
+
 def halfAdder (column : Nat) (i j : Circuit) (h : BitHeap) : AdderResult :=
   let h := h.removeBit column i
   let h := h.removeBit column j
diff --git a/DatapathVerification/BitHeap/Circuit.lean b/DatapathVerification/BitHeap/Circuit.lean
index c34c06d..62cee0c 100644
--- a/DatapathVerification/BitHeap/Circuit.lean
+++ b/DatapathVerification/BitHeap/Circuit.lean
@@ -76,4 +76,16 @@ theorem eval_atLeastTwo (a b c : Circuit) (env : BitEnv) :
 
 end Circuit
 
+
+/-- A vector of circuits, used to represent symbolic BitVectors. -/
+def CircuitVector := Array Circuit
+
+namespace CircuitVector
+
+def eval (vec : CircuitVector) (env : Circuit.BitEnv) : Int :=
+  (vec.mapIdx (fun i c => 2^i * (if c.eval env then 1 else 0))).sum
+
+end CircuitVector
+
+
 end BitHeap
diff --git a/DatapathVerification/BitHeap/Examples/Examples.lean b/DatapathVerification/BitHeap/Examples/Examples.lean
index 9ea6e98..8f6d374 100644
--- a/DatapathVerification/BitHeap/Examples/Examples.lean
+++ b/DatapathVerification/BitHeap/Examples/Examples.lean
@@ -99,6 +99,35 @@ info: 6
 #eval (applyChain compressionChain fourBitsInCol1).eval
         (show BitEnv from fun n => n = 1 || n = 2 || n = 3)
 
+----------------------------
+
+def exampleHeap1 : BitHeap :=
+  let h := BitHeap.empty
+  let h := h.addBit 0 (Circuit.bit 0)
+  let h := h.addBit 1 (Circuit.bit 1)
+  let h := h.addBit 2 (Circuit.bit 2)
+  let h := h.addBit 3 (Circuit.bit 3)
+  h
+
+def exampleHeap2 : BitHeap :=
+  let h := BitHeap.empty
+  let h := h.addBit 0 (Circuit.bit 4)
+  let h := h.addBit 1 (Circuit.bit 5)
+  let h := h.addBit 2 (Circuit.bit 6)
+  let h := h.addBit 3 (Circuit.bit 7)
+  h
+
+/--
+info: {0 ↦ [b0, b4], 1 ↦ [b1, b5], 2 ↦ [b2, b6], 3 ↦ [b3, b7]}-/
+#guard_msgs in
+#eval addBitHeap exampleHeap1 exampleHeap2
+
+/--
+info: {0 ↦ [(b0 ∧ b4)], 1 ↦ [(b0 ∧ b5), (b1 ∧ b4)], 2 ↦ [(b1 ∧ b5), (b2 ∧ b4), (b0 ∧ b6)], 3 ↦ [(b3 ∧ b4), (b0 ∧ b7), (b2 ∧ b5), (b1 ∧ b6)], 4 ↦ [(b2 ∧ b6), (b3 ∧ b5), (b1 ∧ b7)], 5 ↦ [(b3 ∧ b6), (b2 ∧ b7)], 6 ↦ [(b3 ∧ b7)]}
+-/
+#guard_msgs in
+#eval mulBitHeap exampleHeap1 exampleHeap2
+
 end Examples
 
 end BitHeap

From 60ab119fd09cf4a2616d882f1249cdc0cbf0259e Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 20:20:42 +0100
Subject: [PATCH 02/13] fix add/mul

---
 DatapathVerification/BitHeap/BitHeap.lean     | 34 +++++++++++--------
 .../BitHeap/Examples/Examples.lean            | 20 +++++++----
 2 files changed, 33 insertions(+), 21 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 6f1a177..ee9cb84 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -92,25 +92,29 @@ def addBit (column : Nat) (c : Circuit) (h : BitHeap w) : BitHeap w :=
       else addBit (column + 1) c (h.removeBit column c)
 
 -- TODO: make this variable size add
-def addBitHeap (h1 h2 : BitHeap) : BitHeap :=
-  let h : BitHeap := ⟨h1.width, Std.HashMap.emptyWithCapacity 0⟩
-  let h := h1.columns.fold (fun acc col column =>
-             column.elems.toList.foldl (fun acc' c => acc'.addBit col c) acc) h
-  let h := h2.columns.fold (fun acc col column =>
-             column.elems.toList.foldl (fun acc' c => acc'.addBit col c) acc) h
+def addBitHeap' (h1 h2 : BitHeap w) : BitHeap w:=
+  let h := BitHeap.empty w
+  let h := h1.columns.zipIdx.foldl (fun acc (column, index) =>
+             column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc) h
+  let h := h2.columns.zipIdx.foldl (fun acc (column, index) =>
+             column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc) h
   h
 
-def mulBitHeap (h1 h2 : BitHeap) : BitHeap :=
-  let newWidth := max h1.width h2.width
-  let h : BitHeap := ⟨newWidth, Std.HashMap.emptyWithCapacity 0⟩
-  let h := h1.columns.fold (fun acc col1 column1 =>
-             h2.columns.fold (fun acc' col2 column2 =>
-               column1.elems.toList.foldl (fun acc'' c1 =>
-                 column2.elems.toList.foldl (fun acc''' c2 =>
-                   acc'''.addBit (col1 + col2) (Circuit.binop .and c1 c2)) acc'') acc') acc) h
+def addBitHeap (bhs : List (BitHeap w)) : BitHeap w:=
+  let h := BitHeap.empty w
+  let h := bhs.foldl (fun acc heap => heap.columns.zipIdx.foldl (fun acc' (column, index) =>
+             column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc') acc) h
+  h
+
+def mulBitHeap (h0 h1 : BitHeap w) : BitHeap (2 * w - 1) :=
+  let h := BitHeap.empty (2 * w - 1)
+  let h := h0.columns.zipIdx.foldl (fun acc (column0, i0) =>
+             h1.columns.zipIdx.foldl (fun acc' (column1, i2) =>
+               column0.elems.toList.foldl (fun acc'' c1 =>
+                 column1.elems.toList.foldl (fun acc''' c2 =>
+                   acc'''.addBit (i0 + i2) (Circuit.binop .and c1 c2)) acc'') acc') acc) h
   h
 
-def halfAdder (column : Nat) (i j : Circuit) (h : BitHeap) : AdderResult :=
 structure AdderResult (w : Nat) where
   heap : BitHeap w
   sum : Circuit
diff --git a/DatapathVerification/BitHeap/Examples/Examples.lean b/DatapathVerification/BitHeap/Examples/Examples.lean
index e6e9e3a..186a5b8 100644
--- a/DatapathVerification/BitHeap/Examples/Examples.lean
+++ b/DatapathVerification/BitHeap/Examples/Examples.lean
@@ -101,26 +101,34 @@ info: 6
 
 ----------------------------
 
-def exampleHeap1 : BitHeap :=
-  let h := BitHeap.empty
+def exampleHeap1 : BitHeap 4 :=
+  let h := BitHeap.empty 4
   let h := h.addBit 0 (Circuit.bit 0)
   let h := h.addBit 1 (Circuit.bit 1)
   let h := h.addBit 2 (Circuit.bit 2)
   let h := h.addBit 3 (Circuit.bit 3)
   h
 
-def exampleHeap2 : BitHeap :=
-  let h := BitHeap.empty
+def exampleHeap2 : BitHeap 4 :=
+  let h := BitHeap.empty 4
   let h := h.addBit 0 (Circuit.bit 4)
   let h := h.addBit 1 (Circuit.bit 5)
   let h := h.addBit 2 (Circuit.bit 6)
   let h := h.addBit 3 (Circuit.bit 7)
   h
 
+def exampleHeap3 : BitHeap 4 :=
+  let h := BitHeap.empty 4
+  let h := h.addBit 0 (Circuit.bit 8)
+  let h := h.addBit 1 (Circuit.bit 9)
+  let h := h.addBit 2 (Circuit.bit 10)
+  let h := h.addBit 3 (Circuit.bit 11)
+  h
 /--
-info: {0 ↦ [b0, b4], 1 ↦ [b1, b5], 2 ↦ [b2, b6], 3 ↦ [b3, b7]}-/
+info: {0 ↦ [b4, b8, b0], 1 ↦ [b1, b5, b9], 2 ↦ [b2, b10, b6], 3 ↦ [b3, b11, b7]}
+-/
 #guard_msgs in
-#eval addBitHeap exampleHeap1 exampleHeap2
+#eval addBitHeap [exampleHeap1, exampleHeap2, exampleHeap3]
 
 /--
 info: {0 ↦ [(b0 ∧ b4)], 1 ↦ [(b0 ∧ b5), (b1 ∧ b4)], 2 ↦ [(b1 ∧ b5), (b2 ∧ b4), (b0 ∧ b6)], 3 ↦ [(b3 ∧ b4), (b0 ∧ b7), (b2 ∧ b5), (b1 ∧ b6)], 4 ↦ [(b2 ∧ b6), (b3 ∧ b5), (b1 ∧ b7)], 5 ↦ [(b3 ∧ b6), (b2 ∧ b7)], 6 ↦ [(b3 ∧ b7)]}

From 8346a4da2810434453f1483140b21c38cc498873 Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Mon, 6 Jul 2026 16:59:47 +0100
Subject: [PATCH 03/13] wip

---
 DatapathVerification/BitHeap/BVComb.lean      | 44 +++++++++--------
 DatapathVerification/BitHeap/BitHeap.lean     | 49 +++++++++----------
 .../BitHeap/Examples/Examples.lean            |  6 +++
 3 files changed, 54 insertions(+), 45 deletions(-)

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index 2354a4b..2f133ac 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -1,6 +1,8 @@
 import DatapathVerification.BitHeap.BitHeap
 import DatapathVerification.BitHeap.Circuit
-import DatapathVerification.BitHeap.DaddaTree
+import DatapathVerification.BitHeap.Compressors.DaddaTree
+import DatapathVerification.BitHeap.Compressors.NaiveCompression
+
 
 open BitHeap
 namespace Comb
@@ -15,20 +17,19 @@ inductive ArithBinopKind
 -- inductive BooleanBinopKind
 -- | and | or | xor
 
-inductive ArithCircuit
-  | var (width : Nat) (varIndex : Nat)
-  | arithbinop (kind : ArithBinopKind) (width : Nat) (l r : ArithCircuit)
+inductive ArithCircuit : Nat → Type
+  | var (varIndex : Nat) : ArithCircuit w
+  | add (args : List (ArithCircuit w)) : ArithCircuit w
+  | mul (l r : ArithCircuit w) : ArithCircuit w
   -- | arithunop (kind : ArithUnopKind) (width : Nat) (arg : ArithCircuit)
   -- | bvbinop (kind : BooleanBinopKind) (width : Nat) (l r : ArithCircuit)
 
 /--
 Convert a bitheap into a new bitheap that has a single row,
-by building a Dadda tree of adders to reduce the bitheap to a single row.
+by using the naive compression algorithm.
 -/
-def BitHeap.toSingleRow : BitHeap → CircuitVector
-  | bh =>
-    let (pp1, pp2) := DaddaTree.DaddaTree bh
-    -- add pp1 and pp2 to get the final row
+def BitHeap.toSingleRow (bh : BitHeap w) : CircuitVector :=
+    let (pp1, pp2) := NaiveCompression.naiveCompression bh
     sorry
 
 namespace ArithCircuit
@@ -39,19 +40,22 @@ Given a bitvector (x : BV 3), but a bitheap
 x2 x1 x0
 ```
 -/
-def bitheapOfVar (width : Nat) (varIndex : Nat) : BitHeap :=
+def bitheapOfVar (varIndex : Nat) : BitHeap w :=
   --  I want to create a bitheap that has one bit-variable per bit in the bitvector variable.
   -- | We need to know that this index is unique which is a gigantic pain.
-  List.range width |>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * width + i))) BitHeap.empty
+  List.range w |>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * w + i))) (BitHeap.empty w)
+
+def toBitHeap : ArithCircuit w → BitHeap w
+  | .var varIndex => bitheapOfVar varIndex
+  | .add args => BitHeap.addBitHeap (args.map toBitHeap)
+  | .mul l r => BitHeap.truncate ((toBitHeap l).mulBitHeap (toBitHeap r)) w (by omega)
 
-def toBitHeap (c : ArithCircuit) : BitHeap :=
-  match c with
-  | .var width varIndex => bitheapOfVar width varIndex
-  | .arithbinop kind width l r =>
-    match kind with
-    | .add => (toBitHeap l).addBitHeap (toBitHeap r)
-    | .mul => (toBitHeap l).mulBitHeap (toBitHeap r)
-  -- | .arithunop kind width arg =>
+-- def toBitHeap' (c : ArithCircuit) : BitHeap w :=
+--   match c with
+--   | .var width varIndex => bitheapOfVar width varIndex
+--   | .add width args => BitHeap.addBitHeap (args.map toBitHeap)
+--   | .mul width l r => BitHeap.truncate ((toBitHeap l).mulBitHeap (toBitHeap r)) width (by omega)
+  -- | .arithunop kind width arg =>`
   --   match kind with
   --   | .neg => (toBitHeap arg).negBitHeap
   -- | .bvbinop kind width l r =>
@@ -62,7 +66,7 @@ def toBitHeap (c : ArithCircuit) : BitHeap :=
   --     let newRow := Array.zipWith (fun lBit rBit => Circuit.and lBit rBit) lRow rRow
   --     BitHeap.fromRow newRow
 
-def toCircuitVector (c : ArithCircuit) : CircuitVector :=
+def toCircuitVector (c : ArithCircuit w) : CircuitVector :=
   let bh := c.toBitHeap
   bh.toSingleRow
 
diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index ee9cb84..c31dc91 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -29,6 +29,23 @@ def HornersMethod (env : BitEnv) : List Column → Nat
   | [] => 0
   | c :: rest => (c.eval env) + 2 * HornersMethod env rest
 
+-- Basically eval_insertColumn_eq_eval_add, but for HornersMethod. Adding a new column to a list is equivalent
+-- to adding the new column's evaluation to the old evaluation, and subtracting the old column's evaluation.
+theorem hornersMethod_set (env : BitEnv) (l : List Column) (k : Nat) (v : Column) (hk : k < l.length) :
+    (HornersMethod env (l.set k v) : Int)
+      = HornersMethod env l + 2^k * (v.eval env : Int) - 2^k * ((l[k]'hk).eval env : Int) := by
+  induction l generalizing k with
+  | nil =>
+    simp at hk
+  | cons c cs ih =>
+    cases k with
+    | zero =>
+      simp [HornersMethod, List.set]
+      grind
+    | succ j =>
+      simp [HornersMethod]
+      grind
+
 /--
 Evaluate a bit-heap, to compute the final sum of all the bits in the heap.
 -/
@@ -91,14 +108,13 @@ def addBit (column : Nat) (c : Circuit) (h : BitHeap w) : BitHeap w :=
       h.setColumn column (col.insert c) h1
       else addBit (column + 1) c (h.removeBit column c)
 
--- TODO: make this variable size add
-def addBitHeap' (h1 h2 : BitHeap w) : BitHeap w:=
-  let h := BitHeap.empty w
-  let h := h1.columns.zipIdx.foldl (fun acc (column, index) =>
-             column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc) h
-  let h := h2.columns.zipIdx.foldl (fun acc (column, index) =>
-             column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc) h
-  h
+def truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) : BitHeap n :=
+  ⟨Vector.ofFn (fun i => h.columns[i]'(by omega))⟩
+
+theorem evalMod_truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) (env : BitEnv) :
+    (h.truncate n hn).evalMod env = (h.eval env) % 2^n := by
+  simp [evalMod, eval, truncate]
+  sorry
 
 def addBitHeap (bhs : List (BitHeap w)) : BitHeap w:=
   let h := BitHeap.empty w
@@ -139,23 +155,6 @@ def fullAdder (column : Nat) (i j k : Circuit) (h : BitHeap w) : AdderResult w :
   let h := h.addBit (column + 1) carry
   ⟨h, sum, carry⟩
 
--- Basically eval_insertColumn_eq_eval_add, but for HornersMethod. Adding a new column to a list is equivalent
--- to adding the new column's evaluation to the old evaluation, and subtracting the old column's evaluation.
-theorem hornersMethod_set (env : BitEnv) (l : List Column) (k : Nat) (v : Column) (hk : k < l.length) :
-    (HornersMethod env (l.set k v) : Int)
-      = HornersMethod env l + 2^k * (v.eval env : Int) - 2^k * ((l[k]'hk).eval env : Int) := by
-  induction l generalizing k with
-  | nil =>
-    simp at hk
-  | cons c cs ih =>
-    cases k with
-    | zero =>
-      simp [HornersMethod, List.set]
-      grind
-    | succ j =>
-      simp [HornersMethod]
-      grind
-
 @[grind => ]
 theorem eval_insertColumn_eq_eval_add (h : BitHeap w) (k : Nat) (v : Column) (env : BitEnv) (h1 : k < w) :
     (h.setColumn k v h1).eval env
diff --git a/DatapathVerification/BitHeap/Examples/Examples.lean b/DatapathVerification/BitHeap/Examples/Examples.lean
index 186a5b8..f5146e6 100644
--- a/DatapathVerification/BitHeap/Examples/Examples.lean
+++ b/DatapathVerification/BitHeap/Examples/Examples.lean
@@ -136,6 +136,12 @@ info: {0 ↦ [(b0 ∧ b4)], 1 ↦ [(b0 ∧ b5), (b1 ∧ b4)], 2 ↦ [(b1 ∧ b5)
 #guard_msgs in
 #eval mulBitHeap exampleHeap1 exampleHeap2
 
+/--
+info: {0 ↦ [b8], 1 ↦ [b9]}
+-/
+#guard_msgs in
+#eval truncate exampleHeap3 2 (by omega)
+
 end Examples
 
 end BitHeap

From d1bc3db4d817ae7b056ed4ec57f2e0f697263012 Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Tue, 14 Jul 2026 14:26:54 +0100
Subject: [PATCH 04/13] wip

---
 DatapathVerification/BitHeap/BVComb.lean | 27 ++++++++----------------
 1 file changed, 9 insertions(+), 18 deletions(-)

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index 2f133ac..3d30650 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -24,13 +24,15 @@ inductive ArithCircuit : Nat → Type
   -- | arithunop (kind : ArithUnopKind) (width : Nat) (arg : ArithCircuit)
   -- | bvbinop (kind : BooleanBinopKind) (width : Nat) (l r : ArithCircuit)
 
+def BitVecEnv (w : Nat) := Nat → BitVec w
+
 /--
 Convert a bitheap into a new bitheap that has a single row,
 by using the naive compression algorithm.
 -/
 def BitHeap.toSingleRow (bh : BitHeap w) : CircuitVector :=
-    let (pp1, pp2) := NaiveCompression.naiveCompression bh
-    sorry
+    let (pp1, _) := NaiveCompression.naiveCompression bh
+    pp1.columns.toArray.map fun col => col.elems.toList.headD (.const false)
 
 namespace ArithCircuit
 /--
@@ -50,25 +52,14 @@ def toBitHeap : ArithCircuit w → BitHeap w
   | .add args => BitHeap.addBitHeap (args.map toBitHeap)
   | .mul l r => BitHeap.truncate ((toBitHeap l).mulBitHeap (toBitHeap r)) w (by omega)
 
--- def toBitHeap' (c : ArithCircuit) : BitHeap w :=
---   match c with
---   | .var width varIndex => bitheapOfVar width varIndex
---   | .add width args => BitHeap.addBitHeap (args.map toBitHeap)
---   | .mul width l r => BitHeap.truncate ((toBitHeap l).mulBitHeap (toBitHeap r)) width (by omega)
-  -- | .arithunop kind width arg =>`
-  --   match kind with
-  --   | .neg => (toBitHeap arg).negBitHeap
-  -- | .bvbinop kind width l r =>
-  --   match kind with
-  --   | .and =>
-  --     let lRow := (l.toBitHeap).toSingleRow
-  --     let rRow := (r.toBitHeap).toSingleRow
-  --     let newRow := Array.zipWith (fun lBit rBit => Circuit.and lBit rBit) lRow rRow
-  --     BitHeap.fromRow newRow
+def denote (ρ : BitVecEnv w) : ArithCircuit w → BitVec w
+  | .var i => ρ i
+  | .add args => (args.map (denote ρ)).foldl (· + ·) 0
+  | .mul l r => denote ρ l * denote ρ r
 
 def toCircuitVector (c : ArithCircuit w) : CircuitVector :=
   let bh := c.toBitHeap
-  bh.toSingleRow
+  BitHeap.toSingleRow bh
 
 end ArithCircuit
 

From 8eff281daf5f2135189d48a4cc66dc4b0420d190 Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Wed, 15 Jul 2026 16:48:56 +0100
Subject: [PATCH 05/13] wip

---
 DatapathVerification/BitHeap/BVComb.lean      | 45 ++++++++++++++++++-
 DatapathVerification/BitHeap/BitHeap.lean     | 10 +++++
 DatapathVerification/BitHeap/Circuit.lean     |  2 +-
 .../BitHeap/Compressors/NaiveCompression.lean |  4 +-
 .../BitHeap/Examples/BVCombExamples.lean      | 20 +++++++++
 .../Examples/NaiveCompressionExamples.lean    | 22 ++++-----
 6 files changed, 87 insertions(+), 16 deletions(-)
 create mode 100644 DatapathVerification/BitHeap/Examples/BVCombExamples.lean

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index 3d30650..5053187 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -26,6 +26,9 @@ inductive ArithCircuit : Nat → Type
 
 def BitVecEnv (w : Nat) := Nat → BitVec w
 
+def BitVecEnv.toBitEnv (bv : BitVecEnv w) : Circuit.BitEnv :=
+  fun n => (bv (n / w)).getLsbD (n % w)
+
 /--
 Convert a bitheap into a new bitheap that has a single row,
 by using the naive compression algorithm.
@@ -35,15 +38,15 @@ def BitHeap.toSingleRow (bh : BitHeap w) : CircuitVector :=
     pp1.columns.toArray.map fun col => col.elems.toList.headD (.const false)
 
 namespace ArithCircuit
+
 /--
-Given a bitvector (x : BV 3), but a bitheap
+Given a bitvector (x : BV 3), build a bitheap
 ```
 *   *  *
 x2 x1 x0
 ```
 -/
 def bitheapOfVar (varIndex : Nat) : BitHeap w :=
-  --  I want to create a bitheap that has one bit-variable per bit in the bitvector variable.
   -- | We need to know that this index is unique which is a gigantic pain.
   List.range w |>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * w + i))) (BitHeap.empty w)
 
@@ -61,6 +64,44 @@ def toCircuitVector (c : ArithCircuit w) : CircuitVector :=
   let bh := c.toBitHeap
   BitHeap.toSingleRow bh
 
+theorem BitVecEnv.toBitEnv_apply (bv : BitVecEnv w) (i k : Nat) (hk : k < w) :
+    bv.toBitEnv (i * w + k) = (bv i).getLsbD k := by
+  simp [BitVecEnv.toBitEnv]
+  have h1 : (i * w + k) / w = i := by
+    have hw : 0 < w := by grind
+    rw [Nat.mul_comm, Nat.mul_add_div hw, Nat.add_eq_left, Nat.div_eq_of_lt hk]
+  have h2 : k % w = k := by
+    exact Nat.mod_eq_of_lt hk
+  simp [h1, h2]
+
+theorem bitheapOfVar_go (i : Nat) (bv : BitVecEnv w) (k : Nat) (hk : k ≤ w) :
+    ((List.range k).foldl
+        (fun bh j => bh.addBit j (.bit (i * w + j)))
+        (BitHeap.empty w)).eval bv.toBitEnv
+      = (bv i).toNat % 2 ^ k := by
+  induction k with
+  | zero =>
+    simp only [List.range_zero, List.foldl_nil, empty_eval, pow_zero]
+    grind
+  | succ m ih =>
+    rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil]
+    sorry
+
+
+theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
+    c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int):= by
+  fun_induction toBitHeap with
+  | case1 varIndex =>
+    simp only [BitHeap.evalMod, bitheapOfVar]
+    rw [bitheapOfVar_go varIndex bv w (le_refl w)]
+    simp [denote]
+    norm_cast
+    rw [BitVec.toNat_mod_cancel]
+  | case2 =>
+    sorry
+  | case3 =>
+    sorry
+
 end ArithCircuit
 
 end Comb
diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index c31dc91..4a07162 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -52,6 +52,16 @@ Evaluate a bit-heap, to compute the final sum of all the bits in the heap.
 def eval (h : BitHeap w) (env : BitEnv) : Nat :=
   HornersMethod env h.columns.toList
 
+@[simp]
+theorem empty_eval (env : BitEnv) : (empty w).eval env = 0 := by
+  simp [eval, empty]
+  induction w with
+  | zero =>
+    simp [HornersMethod]
+  | succ w ih =>
+    simp [List.replicate_succ, HornersMethod]
+    grind
+
 /--
 Evaluate a bit-heap modulo 2^width, to compute the final sum of all the bits in the heap.
 -/
diff --git a/DatapathVerification/BitHeap/Circuit.lean b/DatapathVerification/BitHeap/Circuit.lean
index 62cee0c..9206898 100644
--- a/DatapathVerification/BitHeap/Circuit.lean
+++ b/DatapathVerification/BitHeap/Circuit.lean
@@ -36,7 +36,7 @@ def numVars (c : Circuit) : Nat :=
   | .const _ => 0
 
 /-- An environment assigns a value to each bit, where bits are given by natural number indexes. -/
-def BitEnv := Nat → Bool
+abbrev BitEnv := Nat → Bool
 
 /-- Evaluate a circuit under a given environment. -/
 def eval (c : Circuit) (env : BitEnv) : Bool :=
diff --git a/DatapathVerification/BitHeap/Compressors/NaiveCompression.lean b/DatapathVerification/BitHeap/Compressors/NaiveCompression.lean
index ad798a2..9bc7c4f 100644
--- a/DatapathVerification/BitHeap/Compressors/NaiveCompression.lean
+++ b/DatapathVerification/BitHeap/Compressors/NaiveCompression.lean
@@ -13,10 +13,10 @@ Another difference with the Wallace tree is that this naive approach consumes ca
 -- if height >= 4, apply FA. if height = 3, apply HA.
 def reduceColumnStep (col : Nat) (h : BitHeap w) : Option (BitHeap w × Adder) :=
     match (h.get col).toList with
-  | a :: b :: c :: _ :: _ =>
+  | a :: b :: c :: _ =>
       let FA := Adder.fullAdder col a b c
       some (Chain.applyAdder FA h, FA)
-  | a :: b :: _ :: [] =>
+  | a :: b :: [] =>
       let HA := Adder.halfAdder col a b
       some (Chain.applyAdder HA h, HA)
   | _ => none
diff --git a/DatapathVerification/BitHeap/Examples/BVCombExamples.lean b/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
new file mode 100644
index 0000000..7e2b555
--- /dev/null
+++ b/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
@@ -0,0 +1,20 @@
+import DatapathVerification.BitHeap.BVComb
+
+open BitHeap
+open Comb
+
+def testEnv : BitVecEnv 4 := fun i => if i = 0 then 6#4 else 3#4
+
+-- 6x3 = 18
+/--
+info: 18
+-/
+#guard_msgs in
+#eval (ArithCircuit.mul (.var 0) (.var 1) : ArithCircuit 4).toBitHeap.eval (BitVecEnv.toBitEnv testEnv)
+
+-- 6 + 3 + 3 = 12
+/--
+info: 12
+-/
+#guard_msgs in
+#eval ((ArithCircuit.add [(.var 0), (.var 1), (.var 2)] : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
diff --git a/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean b/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean
index 43cba34..37b74c3 100644
--- a/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean
+++ b/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean
@@ -44,10 +44,10 @@ def env2 : BitEnv := fun n => n = 0 || n = 2 || n = 5 || n = 6
 -------------
 
 /--
-info: 4
+info: 0
 -/
 #guard_msgs in
-#eval threeBitsInCol1.eval (show BitEnv from env1)
+#eval threeBitsInCol1.evalMod (show BitEnv from env1)
 
 -- Chain length 1 (single FA)
 /--
@@ -58,10 +58,10 @@ info: 1
 
 -- Reduced heap evaluates the same
 /--
-info: 4
+info: 0
 -/
 #guard_msgs in
-#eval (NaiveCompression.reduceColumn 1 threeBitsInCol1).1.eval (show BitEnv from env1)
+#eval (NaiveCompression.reduceColumn 1 threeBitsInCol1).1.evalMod (show BitEnv from env1)
 
 -------------
 
@@ -69,7 +69,7 @@ info: 4
 info: 6
 -/
 #guard_msgs in
-#eval fiveBitsInCol1.eval (show BitEnv from env1)
+#eval fiveBitsInCol1.evalMod (show BitEnv from env1)
 
 -- Chain length 2 (FA + FA)
 /--
@@ -87,32 +87,32 @@ info: 6
 
 -------------
 /--
-info: 9
+info: 1
 -/
 #guard_msgs in
-#eval multiColSmall.eval (show BitEnv from env2)
+#eval multiColSmall.evalMod (show BitEnv from env2)
 
 /--
-info: 2
+info: 5
 -/
 #guard_msgs in
 #eval (NaiveCompression.naiveCompression multiColSmall).2.length
 
 -- Value preserved
 /--
-info: 9
+info: 1
 -/
 #guard_msgs in
 #eval (NaiveCompression.naiveCompression multiColSmall).1.eval (show BitEnv from env2)
 
 /--
-info: 2
+info: 1
 -/
 #guard_msgs in
 #eval (NaiveCompression.naiveCompression multiColSmall).1.maxHeight
 
 /--
-info: [FA(1: b2, b4, b3), HA(2: (((b2 ∧ b4) ∨ (b2 ∧ b3)) ∨ (b4 ∧ b3)), b7)]
+info: [HA(0: b1, b0), FA(1: b2, b4, b3), FA(1: ((b2 ⊕ b4) ⊕ b3), b5, (b1 ∧ b0)), FA(2: (((b2 ∧ b4) ∨ (b2 ∧ b3)) ∨ (b4 ∧ b3)), b6, b7), HA(2: (((((b2 ⊕ b4) ⊕ b3) ∧ b5) ∨ (((b2 ⊕ b4) ⊕ b3) ∧ (b1 ∧ b0))) ∨ (b5 ∧ (b1 ∧ b0))), (((((b2 ∧ b4) ∨ (b2 ∧ b3)) ∨ (b4 ∧ b3)) ⊕ b6) ⊕ b7))]
 -/
 #guard_msgs in
 #eval (NaiveCompression.naiveCompression multiColSmall).2

From ad9d7d41814df275da08c03ad39fd66d4998a77b Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Mon, 20 Jul 2026 17:56:51 +0100
Subject: [PATCH 06/13] add proof

---
 DatapathVerification/BitHeap/BVComb.lean  | 116 +++++++++++++++++++++-
 DatapathVerification/BitHeap/BitHeap.lean |  15 ++-
 DatapathVerification/BitHeap/Column.lean  |  13 +++
 3 files changed, 136 insertions(+), 8 deletions(-)

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index 5053187..498fd6a 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -87,6 +87,108 @@ theorem bitheapOfVar_go (i : Nat) (bv : BitVecEnv w) (k : Nat) (hk : k ≤ w) :
     rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil]
     sorry
 
+theorem foldl_addBit_evalMod  (idx : Nat) (h : BitHeap w) (cs : List Circuit) :
+  (List.foldl (fun a c => addBit idx c a) h cs).evalMod env
+    = (h.evalMod env + (cs.map (fun c => 2^idx * (c.eval env).toInt)).sum) % 2^w := by
+    induction cs generalizing h with
+    | nil =>
+      simp [evalMod]
+    | cons c tl ih =>
+      simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, BitHeap.evalMod_heap_addBit, Int.emod_add_emod]
+      grind
+
+theorem foldl_columns_evalMod (acc : BitHeap w) (ps : List (Column × Nat)) :
+    (ps.foldl (fun a p => List.foldl (fun a' c => addBit p.2 c a') a p.1.elems.toList)
+        acc).evalMod env
+      = (acc.evalMod env
+          + (ps.map (fun p =>
+              (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum) % 2^w := by
+    induction ps generalizing acc with
+    | nil =>
+      simp [evalMod]
+    | cons p tl ih =>
+      simp only [List.foldl_cons, List.map_cons, List.sum_cons]
+      rw [ih, foldl_addBit_evalMod, Int.emod_add_emod]
+      grind
+
+theorem hornersMethod_eq_sum_zipIdx (env : Circuit.BitEnv) (l : List Column) (s : Nat) :
+    (2^s : Int) * (HornersMethod env l : Int)
+      = ((l.zipIdx s).map (fun p =>
+          (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
+  induction l generalizing s with
+  | nil =>
+    simp [HornersMethod]
+  | cons p ps ih =>
+    simp [HornersMethod, List.zipIdx_cons, List.map_cons, List.sum_cons]
+    rw [← ih]
+    rw [Int.mul_add]
+    have : 2 ^ s * (2 * ↑(HornersMethod env ps)) = 2 ^ (s + 1) * (HornersMethod env ps) := by
+      grind
+    norm_cast
+    simp [this, Column.eval_eq_sum]
+    induction p.elems.toList with
+    | nil =>
+      simp
+    | cons c tl ih' =>
+      simp only [List.map_cons, List.sum_cons]
+      grind
+
+theorem eval_eq_sum_columns (h : BitHeap w) (env : Circuit.BitEnv) :
+    ((h.eval env : Int))
+      = (h.columns.toList.zipIdx.map (fun p =>
+          (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
+  simp [eval]
+  have h0 := hornersMethod_eq_sum_zipIdx env h.columns.toList 0
+  simp only [pow_zero, one_mul] at h0
+  exact h0
+
+theorem mergeInto_evalMod(acc h : BitHeap w) :
+    (mergeInto acc h).evalMod env = (acc.evalMod env + h.evalMod env) % 2^w := by
+  simp [mergeInto]
+  rw [Vector.foldl, ←Array.foldl_toList]
+  rw [foldl_columns_evalMod]
+  simp only [evalMod, Vector.toArray_zipIdx, Array.toList_zipIdx, Int.emod_add_emod,
+    Int.add_emod_emod]
+  rw [eval_eq_sum_columns, eval_eq_sum_columns]
+  grind
+
+theorem foldl_mergeInto_evalMod (hs : List (BitHeap w)) (acc : BitHeap w) :
+    (hs.foldl mergeInto acc).evalMod env
+      = (acc.evalMod env + (hs.map (·.evalMod env)).sum) % 2^w := by
+    induction hs generalizing acc with
+    | nil =>
+      simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, add_zero, dvd_refl,
+        Int.emod_emod_of_dvd]
+    | cons h tl ih =>
+      simp only [List.foldl_cons, List.map_cons, List.sum_cons]
+      rw [ih]
+      rw [mergeInto_evalMod]
+      simp
+      grind
+
+theorem foldl_add_init {w : ℕ} (acc hd : BitVec w) (tl : List (BitVec w)) :
+    List.foldl (· + ·) (acc + hd) tl = List.foldl (· + ·) acc tl + hd := by
+  induction tl generalizing acc with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [List.foldl_cons]
+    rw [← ih]
+    grind
+
+theorem foldl_add_toNat_go (acc : BitVec w) (l : List (BitVec w)) :
+    ((l.foldl (· + ·) acc).toNat : Int)
+      = ((acc.toNat : Int) + (l.map (fun x => (x.toNat : Int))).sum) % 2^w := by
+  induction l with
+  | nil =>
+    simp only [List.foldl_nil, List.map_nil, List.sum_nil, add_zero]
+    norm_cast
+    simp only [BitVec.toNat_mod_cancel]
+  | cons hd tl ih =>
+    simp only [List.foldl_cons, List.map_cons, List.sum_cons]
+    rw [foldl_add_init]
+    rw [BitVec.toNat_add]
+    simp [ih]
+    grind
 
 theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
     c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int):= by
@@ -97,9 +199,17 @@ theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
     simp [denote]
     norm_cast
     rw [BitVec.toNat_mod_cancel]
-  | case2 =>
-    sorry
-  | case3 =>
+  | case2 args ih =>
+    simp only [denote, BitHeap.addBitHeap]
+    rw [foldl_mergeInto_evalMod]
+    rw [foldl_add_toNat_go]
+    simp only [empty_evalMod, List.map_map, zero_add, BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat,
+      Nat.zero_mod, Int.cast_ofNat_Int]
+    congr 1
+    congr 1
+    simp only [List.map_inj_left, Function.comp_apply]
+    assumption
+  | case3 l r ih1 ih2=>
     sorry
 
 end ArithCircuit
diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 4a07162..2f079bb 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -68,6 +68,10 @@ Evaluate a bit-heap modulo 2^width, to compute the final sum of all the bits in
 def evalMod (h : BitHeap w) (env : BitEnv) : Int :=
   h.eval env % 2^(w)
 
+@[simp]
+theorem empty_evalMod (env : BitEnv) : (empty w).evalMod env = 0 := by
+  simp [evalMod, empty_eval]
+
 def get (h : BitHeap w) (column : Nat) : Column :=
   h.columns.getD column (Column.empty)
 
@@ -126,11 +130,12 @@ theorem evalMod_truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) (env : BitEnv)
   simp [evalMod, eval, truncate]
   sorry
 
-def addBitHeap (bhs : List (BitHeap w)) : BitHeap w:=
-  let h := BitHeap.empty w
-  let h := bhs.foldl (fun acc heap => heap.columns.zipIdx.foldl (fun acc' (column, index) =>
-             column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc') acc) h
-  h
+def mergeInto (acc h : BitHeap w) : BitHeap w :=
+  h.columns.zipIdx.foldl (fun acc' (col, idx) =>
+    col.elems.toList.foldl (fun a c => a.addBit idx c) acc') acc
+
+def addBitHeap (bhs : List (BitHeap w)) : BitHeap w :=
+  bhs.foldl mergeInto (BitHeap.empty w)
 
 def mulBitHeap (h0 h1 : BitHeap w) : BitHeap (2 * w - 1) :=
   let h := BitHeap.empty (2 * w - 1)
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index b7dfad7..fca836f 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -67,6 +67,19 @@ theorem foldl_sum (l : List Circuit) (env : BitEnv) (a : Nat) :
   | cons p ps ih =>
     grind
 
+theorem eval_eq_sum (col : Column) (env : Circuit.BitEnv) :
+    ((col.eval env : Int)) = (col.elems.toList.map (fun c => (c.eval env).toInt)).sum := by
+  simp [eval]
+  rw [Std.HashSet.fold_eq_foldl_toList, foldl_sum, Nat.zero_add]
+  have hpt : ∀ b : Bool, ((b.toNat : Int)) = b.toInt := by
+    intro b; cases b <;> rfl
+  induction col.elems.toList with
+  | nil => simp
+  | cons p ps ih =>
+    simp only [List.map_cons, List.sum_cons]
+    push_cast
+    rw [ih, hpt]
+
 @[simp]
 theorem eval_erase (col : Column) (c : Circuit) (env : BitEnv) (h : c ∈ col) :
     (col.erase c).eval env = col.eval env - (c.eval env).toNat := by

From 89398a8796bb7aaafcf0f1cdc797d914570f6067 Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Wed, 22 Jul 2026 01:11:22 +0100
Subject: [PATCH 07/13] trunc proof

---
 DatapathVerification/BitHeap/BitHeap.lean | 50 +++++++++++++++++++----
 1 file changed, 41 insertions(+), 9 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 2f079bb..e1bb828 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -3,6 +3,7 @@ import DatapathVerification.BitHeap.Circuit
 import DatapathVerification.BitHeap.Column
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Algebra.Divisibility.Basic
+import Mathlib.Data.Int.ModEq
 import Mathlib.Algebra.Order.BigOperators.Group.List
 import Mathlib.Algebra.Order.Group.Nat
 
@@ -125,10 +126,39 @@ def addBit (column : Nat) (c : Circuit) (h : BitHeap w) : BitHeap w :=
 def truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) : BitHeap n :=
   ⟨Vector.ofFn (fun i => h.columns[i]'(by omega))⟩
 
+theorem hornersMethod_take (env : BitEnv) (n : Nat) (l : List Column) :
+    ((HornersMethod env (l.take n) : Int)) % 2^n
+      = ((HornersMethod env l : Int)) % 2^n := by
+  induction n generalizing l with
+  | zero => simp
+  | succ m ih =>
+    cases l with
+    | nil => simp
+    | cons c cs =>
+      simp only [List.take_succ_cons, HornersMethod, Nat.cast_add, Nat.cast_mul,
+        Nat.cast_ofNat]
+      have h2 : (2 : Int) * (HornersMethod env (cs.take m))
+          ≡ 2 * (HornersMethod env cs) [ZMOD 2^(m+1)] := by
+        have hme : ((HornersMethod env (cs.take m) : Int))
+            ≡ (HornersMethod env cs : Int) [ZMOD 2^m] := ih cs
+        have hm2 := hme.mul_left' (c := 2)
+        rw [pow_succ, mul_comm ((2:Int)^m) 2]
+        exact hm2
+      exact (Int.ModEq.refl _).add h2
+
+theorem truncate_columns_toList (h : BitHeap w) (n : Nat) (hn : n ≤ w) :
+    (h.truncate n hn).columns.toList = h.columns.toList.take n := by
+  apply List.ext_getElem
+  · simp [truncate]
+    omega
+  · intro i h1 h2
+    simp only [truncate, Fin.getElem_fin, Vector.getElem_toList, Vector.getElem_ofFn,
+      List.getElem_take]
+
 theorem evalMod_truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) (env : BitEnv) :
     (h.truncate n hn).evalMod env = (h.eval env) % 2^n := by
-  simp [evalMod, eval, truncate]
-  sorry
+  simp only [evalMod, eval]
+  simp [hornersMethod_take, truncate_columns_toList]
 
 def mergeInto (acc h : BitHeap w) : BitHeap w :=
   h.columns.zipIdx.foldl (fun acc' (col, idx) =>
@@ -137,14 +167,16 @@ def mergeInto (acc h : BitHeap w) : BitHeap w :=
 def addBitHeap (bhs : List (BitHeap w)) : BitHeap w :=
   bhs.foldl mergeInto (BitHeap.empty w)
 
+def mulColumns (acc : BitHeap v) (col0 col1 : Column) (idx : Nat) : BitHeap v :=
+  col0.elems.toList.foldl (fun a c1 =>
+    col1.elems.toList.foldl (fun a' c2 =>
+      a'.addBit idx (.binop .and c1 c2)) a) acc
+
 def mulBitHeap (h0 h1 : BitHeap w) : BitHeap (2 * w - 1) :=
-  let h := BitHeap.empty (2 * w - 1)
-  let h := h0.columns.zipIdx.foldl (fun acc (column0, i0) =>
-             h1.columns.zipIdx.foldl (fun acc' (column1, i2) =>
-               column0.elems.toList.foldl (fun acc'' c1 =>
-                 column1.elems.toList.foldl (fun acc''' c2 =>
-                   acc'''.addBit (i0 + i2) (Circuit.binop .and c1 c2)) acc'') acc') acc) h
-  h
+  h0.columns.zipIdx.foldl (fun acc (col0, i0) =>
+    h1.columns.zipIdx.foldl (fun acc' (col1, i1) =>
+      mulColumns acc' col0 col1 (i0 + i1)) acc)
+    (BitHeap.empty (2 * w - 1))
 
 structure AdderResult (w : Nat) where
   heap : BitHeap w

From c01a0d0e3e03ee0d34036d939c66f4b98a0a5bfe Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Wed, 22 Jul 2026 01:16:07 +0100
Subject: [PATCH 08/13] nit

---
 DatapathVerification/BitHeap/BitHeap.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index e1bb828..906630f 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -137,13 +137,13 @@ theorem hornersMethod_take (env : BitEnv) (n : Nat) (l : List Column) :
     | cons c cs =>
       simp only [List.take_succ_cons, HornersMethod, Nat.cast_add, Nat.cast_mul,
         Nat.cast_ofNat]
-      have h2 : (2 : Int) * (HornersMethod env (cs.take m))
-          ≡ 2 * (HornersMethod env cs) [ZMOD 2^(m+1)] := by
-        have hme : ((HornersMethod env (cs.take m) : Int))
-            ≡ (HornersMethod env cs : Int) [ZMOD 2^m] := ih cs
-        have hm2 := hme.mul_left' (c := 2)
-        rw [pow_succ, mul_comm ((2:Int)^m) 2]
-        exact hm2
+      have h2 : (2 : Int) * (HornersMethod env (cs.take m)) % 2^(m+1)
+          = 2 * (HornersMethod env cs) % 2^(m+1) := by
+        have hme : ((HornersMethod env (cs.take m) : Int)) % 2^(m)
+            = (HornersMethod env cs : Int) % 2^(m) := ih cs
+        simp only [pow_succ, mul_comm ((2 : Int) ^ m) 2, Int.reduceLT, Int.mul_emod_mul_of_pos,
+          mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false]
+        exact Int.ModEq.eq (ih cs)
       exact (Int.ModEq.refl _).add h2
 
 theorem truncate_columns_toList (h : BitHeap w) (n : Nat) (hn : n ≤ w) :

From a53de1f466b075a211b42543fe219bacde73a698 Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Wed, 22 Jul 2026 01:16:41 +0100
Subject: [PATCH 09/13] nit

---
 DatapathVerification/BitHeap/BitHeap.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 906630f..ded55d7 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -139,8 +139,6 @@ theorem hornersMethod_take (env : BitEnv) (n : Nat) (l : List Column) :
         Nat.cast_ofNat]
       have h2 : (2 : Int) * (HornersMethod env (cs.take m)) % 2^(m+1)
           = 2 * (HornersMethod env cs) % 2^(m+1) := by
-        have hme : ((HornersMethod env (cs.take m) : Int)) % 2^(m)
-            = (HornersMethod env cs : Int) % 2^(m) := ih cs
         simp only [pow_succ, mul_comm ((2 : Int) ^ m) 2, Int.reduceLT, Int.mul_emod_mul_of_pos,
           mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false]
         exact Int.ModEq.eq (ih cs)

From e5070f65573c0f23ac82fd47a2b6129a3966d4aa Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Thu, 23 Jul 2026 22:35:30 +0100
Subject: [PATCH 10/13] mul proof

---
 DatapathVerification/BitHeap/BVComb.lean      | 184 ++++++++++++------
 DatapathVerification/BitHeap/BitHeap.lean     |  41 ++++
 DatapathVerification/BitHeap/Column.lean      |   3 +
 .../BitHeap/Examples/BVCombExamples.lean      |  72 +++++--
 4 files changed, 234 insertions(+), 66 deletions(-)

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index 498fd6a..dbcd607 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -2,6 +2,7 @@ import DatapathVerification.BitHeap.BitHeap
 import DatapathVerification.BitHeap.Circuit
 import DatapathVerification.BitHeap.Compressors.DaddaTree
 import DatapathVerification.BitHeap.Compressors.NaiveCompression
+import Mathlib.Algebra.BigOperators.Ring.List
 
 
 open BitHeap
@@ -64,7 +65,7 @@ def toCircuitVector (c : ArithCircuit w) : CircuitVector :=
   let bh := c.toBitHeap
   BitHeap.toSingleRow bh
 
-theorem BitVecEnv.toBitEnv_apply (bv : BitVecEnv w) (i k : Nat) (hk : k < w) :
+theorem toBitEnv_apply (bv : BitVecEnv w) (i k : Nat) (hk : k < w) :
     bv.toBitEnv (i * w + k) = (bv i).getLsbD k := by
   simp [BitVecEnv.toBitEnv]
   have h1 : (i * w + k) / w = i := by
@@ -74,18 +75,33 @@ theorem BitVecEnv.toBitEnv_apply (bv : BitVecEnv w) (i k : Nat) (hk : k < w) :
     exact Nat.mod_eq_of_lt hk
   simp [h1, h2]
 
+theorem toNat_mod_two_pow_succ (x : BitVec n) (m : Nat) :
+    x.toNat % 2 ^ (m + 1) = x.toNat % 2 ^ m + 2 ^ m * (x.getLsbD m).toNat := by
+  rw [Nat.mod_pow_succ, ← BitVec.testBit_toNat, Nat.toNat_testBit]
+
+theorem natCast_emod_two_pow_of_lt {a w : Nat} (ha : a < 2 ^ w) :
+    ((a : Int)) % 2 ^ w = (a : Int) := by
+  have e : ((2 : Int) ^ w) = ((2 ^ w : Nat) : Int) := by grind
+  rw [e, ← Int.natCast_emod, Nat.mod_eq_of_lt ha]
+
 theorem bitheapOfVar_go (i : Nat) (bv : BitVecEnv w) (k : Nat) (hk : k ≤ w) :
     ((List.range k).foldl
         (fun bh j => bh.addBit j (.bit (i * w + j)))
-        (BitHeap.empty w)).eval bv.toBitEnv
+        (BitHeap.empty w)).evalMod bv.toBitEnv
       = (bv i).toNat % 2 ^ k := by
   induction k with
   | zero =>
-    simp only [List.range_zero, List.foldl_nil, empty_eval, pow_zero]
+    simp only [List.range_zero, List.foldl_nil, empty_evalMod, pow_zero]
     grind
   | succ m ih =>
-    rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil]
-    sorry
+    simp only [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil,
+      evalMod_heap_addBit, ih (by omega), Circuit.eval, toBitEnv_apply bv i m (by omega)]
+    have key : ((bv i).toNat % 2 ^ m : Int) + 2 ^ m * ((bv i).getLsbD m).toInt
+        = (((bv i).toNat % 2 ^ (m + 1) : Nat) : Int) := by
+      rw [toNat_mod_two_pow_succ]; cases (bv i).getLsbD m <;> grind
+    have hlt : (bv i).toNat % 2 ^ (m + 1) < 2 ^ w :=
+      ((bv i).toNat.mod_lt (Nat.two_pow_pos _)).trans_le (Nat.pow_le_pow_right (by omega) (by omega))
+    grind [natCast_emod_two_pow_of_lt hlt]
 
 theorem foldl_addBit_evalMod  (idx : Nat) (h : BitHeap w) (cs : List Circuit) :
   (List.foldl (fun a c => addBit idx c a) h cs).evalMod env
@@ -107,30 +123,7 @@ theorem foldl_columns_evalMod (acc : BitHeap w) (ps : List (Column × Nat)) :
     | nil =>
       simp [evalMod]
     | cons p tl ih =>
-      simp only [List.foldl_cons, List.map_cons, List.sum_cons]
-      rw [ih, foldl_addBit_evalMod, Int.emod_add_emod]
-      grind
-
-theorem hornersMethod_eq_sum_zipIdx (env : Circuit.BitEnv) (l : List Column) (s : Nat) :
-    (2^s : Int) * (HornersMethod env l : Int)
-      = ((l.zipIdx s).map (fun p =>
-          (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
-  induction l generalizing s with
-  | nil =>
-    simp [HornersMethod]
-  | cons p ps ih =>
-    simp [HornersMethod, List.zipIdx_cons, List.map_cons, List.sum_cons]
-    rw [← ih]
-    rw [Int.mul_add]
-    have : 2 ^ s * (2 * ↑(HornersMethod env ps)) = 2 ^ (s + 1) * (HornersMethod env ps) := by
-      grind
-    norm_cast
-    simp [this, Column.eval_eq_sum]
-    induction p.elems.toList with
-    | nil =>
-      simp
-    | cons c tl ih' =>
-      simp only [List.map_cons, List.sum_cons]
+      simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, foldl_addBit_evalMod, Int.emod_add_emod]
       grind
 
 theorem eval_eq_sum_columns (h : BitHeap w) (env : Circuit.BitEnv) :
@@ -145,11 +138,9 @@ theorem eval_eq_sum_columns (h : BitHeap w) (env : Circuit.BitEnv) :
 theorem mergeInto_evalMod(acc h : BitHeap w) :
     (mergeInto acc h).evalMod env = (acc.evalMod env + h.evalMod env) % 2^w := by
   simp [mergeInto]
-  rw [Vector.foldl, ←Array.foldl_toList]
-  rw [foldl_columns_evalMod]
+  rw [Vector.foldl, ←Array.foldl_toList, foldl_columns_evalMod]
   simp only [evalMod, Vector.toArray_zipIdx, Array.toList_zipIdx, Int.emod_add_emod,
-    Int.add_emod_emod]
-  rw [eval_eq_sum_columns, eval_eq_sum_columns]
+    Int.add_emod_emod,eval_eq_sum_columns, eval_eq_sum_columns]
   grind
 
 theorem foldl_mergeInto_evalMod (hs : List (BitHeap w)) (acc : BitHeap w) :
@@ -160,10 +151,7 @@ theorem foldl_mergeInto_evalMod (hs : List (BitHeap w)) (acc : BitHeap w) :
       simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, add_zero, dvd_refl,
         Int.emod_emod_of_dvd]
     | cons h tl ih =>
-      simp only [List.foldl_cons, List.map_cons, List.sum_cons]
-      rw [ih]
-      rw [mergeInto_evalMod]
-      simp
+      simp [List.foldl_cons, List.map_cons, List.sum_cons, ih, mergeInto_evalMod]
       grind
 
 theorem foldl_add_init {w : ℕ} (acc hd : BitVec w) (tl : List (BitVec w)) :
@@ -171,8 +159,7 @@ theorem foldl_add_init {w : ℕ} (acc hd : BitVec w) (tl : List (BitVec w)) :
   induction tl generalizing acc with
   | nil => rfl
   | cons x xs ih =>
-    simp only [List.foldl_cons]
-    rw [← ih]
+    simp only [List.foldl_cons, ← ih]
     grind
 
 theorem foldl_add_toNat_go (acc : BitVec w) (l : List (BitVec w)) :
@@ -184,33 +171,120 @@ theorem foldl_add_toNat_go (acc : BitVec w) (l : List (BitVec w)) :
     norm_cast
     simp only [BitVec.toNat_mod_cancel]
   | cons hd tl ih =>
-    simp only [List.foldl_cons, List.map_cons, List.sum_cons]
-    rw [foldl_add_init]
-    rw [BitVec.toNat_add]
-    simp [ih]
+    simp [List.foldl_cons, List.map_cons, List.sum_cons, foldl_add_init, BitVec.toNat_add, ih]
+    grind
+
+theorem foldl_andBit_evalMod (env : Circuit.BitEnv) (idx : Nat) (c1 : Circuit)
+    (cs : List Circuit) (h : BitHeap v) :
+    (cs.foldl (fun a c2 => a.addBit idx (.binop .and c1 c2)) h).evalMod env
+      = (h.evalMod env + 2^idx * (c1.eval env).toInt
+          * (cs.map (fun c => (c.eval env).toInt)).sum) % 2^v := by
+  induction cs generalizing h with
+  | nil =>
+    simp only [List.foldl_nil, List.map_nil, List.sum_nil, mul_zero, add_zero,
+      BitHeap.evalMod, dvd_refl, Int.emod_emod_of_dvd]
+  | cons c tl ih =>
+    simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih,
+      BitHeap.evalMod_heap_addBit, Circuit.eval_and, Column.toInt_and_eq_mul, Int.emod_add_emod]
+    grind
+
+theorem mulColumns_evalMod (env : Circuit.BitEnv) (acc : BitHeap v)
+    (col0 col1 : Column) (idx : Nat) :
+    (mulColumns acc col0 col1 idx).evalMod env
+      = (acc.evalMod env
+          + 2^idx * (col0.eval env : Int) * (col1.eval env : Int)) % 2^v := by
+  simp only [mulColumns]
+  rw [Column.eval_eq_sum col0, Column.eval_eq_sum col1]
+  generalize col0.elems.toList = l0
+  induction l0 generalizing acc with
+  | nil =>
+    simp only [List.foldl_nil, List.map_nil, List.sum_nil, mul_zero, zero_mul, add_zero,
+      BitHeap.evalMod, dvd_refl, Int.emod_emod_of_dvd]
+  | cons c1 tl ih =>
+    simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, foldl_andBit_evalMod,
+      Int.emod_add_emod]
+    grind
+
+theorem foldl_mulColumns_evalMod (env : Circuit.BitEnv) (col0 : Column) (i0 : Nat)
+    (qs : List (Column × Nat)) (acc : BitHeap v) :
+    (qs.foldl (fun a q => mulColumns a col0 q.1 (i0 + q.2)) acc).evalMod env
+      = (acc.evalMod env + (col0.eval env : Int)
+          * (qs.map (fun q => 2^(i0 + q.2) * (q.1.eval env : Int))).sum) % 2^v := by
+  induction qs generalizing acc with
+  | nil =>
+    simp [evalMod]
+  | cons q tl ih =>
+    simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, mulColumns_evalMod,
+      Int.emod_add_emod]
     grind
 
+theorem mulRow_evalMod (env : Circuit.BitEnv) (col0 : Column) (i0 : Nat)
+    (h1 : BitHeap w) (acc : BitHeap v) :
+    (h1.columns.zipIdx.foldl
+        (fun acc' q => mulColumns acc' col0 q.1 (i0 + q.2)) acc).evalMod env
+      = (acc.evalMod env
+          + 2^i0 * (col0.eval env : Int) * (h1.eval env : Int)) % 2^v := by
+  rw [Vector.foldl, ← Array.foldl_toList, foldl_mulColumns_evalMod]
+  simp only [Vector.toArray_zipIdx, Array.toList_zipIdx]
+  have hsum : (col0.eval env : Int)
+        * ((h1.columns.toList.zipIdx.map
+            (fun q => 2^(i0 + q.2) * (q.1.eval env : Int))).sum)
+      = 2^i0 * (col0.eval env : Int) * (h1.eval env : Int) := by
+    have hz := BitHeap.hornersMethod_mul_eq_sum_zipIdx env h1.columns.toList i0 0
+    have heval : (h1.eval env : Int) = HornersMethod env h1.columns.toList := by
+      simp [eval]
+    rw [heval, ← hz]
+    simp only [Nat.add_zero]
+    grind
+  simp only [Vector.toList] at hsum ⊢
+  rw [hsum]
+
+theorem foldl_mulRow_evalMod (env : Circuit.BitEnv) (h1 : BitHeap w)
+    (ps : List (Column × Nat)) (acc : BitHeap v) :
+    (ps.foldl (fun a p =>
+        h1.columns.zipIdx.foldl
+          (fun a' q => mulColumns a' p.1 q.1 (p.2 + q.2)) a) acc).evalMod env
+      = (acc.evalMod env
+          + (ps.map (fun p => 2^p.2 * (p.1.eval env : Int))).sum
+              * (h1.eval env : Int)) % 2^v := by
+  induction ps generalizing acc with
+  | nil =>
+    simp [evalMod]
+  | cons p tl ih =>
+    simp [ih, mulRow_evalMod]
+    grind
+
+theorem mulBitHeap_evalMod (h0 h1 : BitHeap w) (env : Circuit.BitEnv) :
+    (h0.mulBitHeap h1).evalMod env
+      = ((h0.eval env : Int) * (h1.eval env : Int)) % 2^(2*w - 1) := by
+  simp [mulBitHeap]
+  rw [←Vector.foldl_toList, foldl_mulRow_evalMod]
+  congr 1
+  simp only [empty_evalMod, Vector.toList_zipIdx, zero_add, mul_eq_mul_right_iff,
+    Int.natCast_eq_zero, eval]
+  left
+  have h0 := hornersMethod_eq_sum_zipIdx env h0.columns.toList 0
+  simp_all only [pow_zero, one_mul]
+  simp only [Column.eval_eq_sum, List.sum_map_mul_left]
+
 theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
     c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int):= by
   fun_induction toBitHeap with
   | case1 varIndex =>
-    simp only [BitHeap.evalMod, bitheapOfVar]
-    rw [bitheapOfVar_go varIndex bv w (le_refl w)]
-    simp [denote]
+    simp only [bitheapOfVar, bitheapOfVar_go varIndex bv w (le_refl w), denote]
     norm_cast
     rw [BitVec.toNat_mod_cancel]
   | case2 args ih =>
-    simp only [denote, BitHeap.addBitHeap]
-    rw [foldl_mergeInto_evalMod]
-    rw [foldl_add_toNat_go]
-    simp only [empty_evalMod, List.map_map, zero_add, BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat,
-      Nat.zero_mod, Int.cast_ofNat_Int]
-    congr 1
-    congr 1
-    simp only [List.map_inj_left, Function.comp_apply]
+    simp [denote, BitHeap.addBitHeap, foldl_mergeInto_evalMod, foldl_add_toNat_go]
+    congr 2
+    simp
     assumption
   | case3 l r ih1 ih2=>
-    sorry
+    simp only [denote]
+    simp only [BitHeap.evalMod] at ih1 ih2
+    have hdvd : ((2:Int)^w) ∣ ((2:Int)^(2*w - 1)) := pow_dvd_pow 2 (by omega)
+    rw [evalMod_truncateMod, BitVec.toNat_mul, mulBitHeap_evalMod, Int.emod_emod_of_dvd _ hdvd, Int.mul_emod, ih1, ih2]
+    congr 1
 
 end ArithCircuit
 
diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index ded55d7..91182ec 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -47,6 +47,43 @@ theorem hornersMethod_set (env : BitEnv) (l : List Column) (k : Nat) (v : Column
       simp [HornersMethod]
       grind
 
+theorem hornersMethod_eq_sum_zipIdx (env : Circuit.BitEnv) (l : List Column) (s : Nat) :
+    (2^s : Int) * (HornersMethod env l : Int)
+      = ((l.zipIdx s).map (fun p =>
+          (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
+  induction l generalizing s with
+  | nil =>
+    simp [HornersMethod]
+  | cons p ps ih =>
+    simp [HornersMethod, List.zipIdx_cons, List.map_cons, List.sum_cons]
+    rw [← ih]
+    rw [Int.mul_add]
+    have : 2 ^ s * (2 * ↑(HornersMethod env ps)) = 2 ^ (s + 1) * (HornersMethod env ps) := by
+      grind
+    norm_cast
+    simp [this, Column.eval_eq_sum]
+    induction p.elems.toList with
+    | nil =>
+      simp
+    | cons c tl ih' =>
+      simp only [List.map_cons, List.sum_cons]
+      grind
+
+theorem hornersMethod_mul_eq_sum_zipIdx (env : Circuit.BitEnv) (l : List Column) (i0 s : Nat) :
+    (2^(i0 + s) : Int) * (HornersMethod env l : Int)
+      = ((l.zipIdx s).map (fun q => 2^(i0 + q.2) * (q.1.eval env : Int))).sum := by
+  induction l generalizing s with
+  | nil =>
+    simp [HornersMethod]
+  | cons p ps ih =>
+    simp only [HornersMethod, List.zipIdx_cons, List.map_cons, List.sum_cons]
+    rw [← ih]
+    push_cast
+    have hpow : (2 : Int) ^ (i0 + (s + 1)) = 2 ^ (i0 + s) * 2 := by
+      rw [← Nat.add_assoc, pow_succ]
+    rw [hpow]
+    grind
+
 /--
 Evaluate a bit-heap, to compute the final sum of all the bits in the heap.
 -/
@@ -158,6 +195,10 @@ theorem evalMod_truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) (env : BitEnv)
   simp only [evalMod, eval]
   simp [hornersMethod_take, truncate_columns_toList]
 
+theorem evalMod_truncateMod (h : BitHeap w) (n : Nat) (hn : n ≤ w) (env : BitEnv) :
+    (h.truncate n hn).evalMod env = (h.evalMod env) % 2^n := by
+  rw [evalMod_truncate, evalMod, (Int.emod_emod_of_dvd _ (pow_dvd_pow 2 hn)).symm]
+
 def mergeInto (acc h : BitHeap w) : BitHeap w :=
   h.columns.zipIdx.foldl (fun acc' (col, idx) =>
     col.elems.toList.foldl (fun a c => a.addBit idx c) acc') acc
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index fca836f..2dda7b0 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -44,6 +44,9 @@ def erase (col : Column) (c : Circuit) : Column :=
 def height (col : Column) : Nat :=
   col.elems.size
 
+theorem toInt_and_eq_mul (a b : Bool) : (a && b).toInt = a.toInt * b.toInt := by
+  cases a <;> cases b <;> rfl
+
 @[simp]
 theorem height_eq_size (col : Column) : col.height = col.elems.size := rfl
 
diff --git a/DatapathVerification/BitHeap/Examples/BVCombExamples.lean b/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
index 7e2b555..06ceeeb 100644
--- a/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
+++ b/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
@@ -3,18 +3,68 @@ import DatapathVerification.BitHeap.BVComb
 open BitHeap
 open Comb
 
-def testEnv : BitVecEnv 4 := fun i => if i = 0 then 6#4 else 3#4
+def testEnv : BitVecEnv 4 := fun i =>
+  match i with
+  | 0 => 6#4
+  | 1 => 3#4
+  | 2 => 5#4
+  | 3 => 15#4
+  | _ => 0#4
 
--- 6x3 = 18
-/--
-info: 18
--/
+----------
+
+/-- info: 6 -/
+#guard_msgs in
+#eval (ArithCircuit.var 0 : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
+
+-- add, no overflow: (6+3) % 16 = 9
+/-- info: 9 -/
+#guard_msgs in
+#eval (ArithCircuit.add [.var 0, .var 1] : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
+
+-- add, WITH overflow: (6+3+5+15) % 16 = 29 % 16 = 13
+/-- info: 13 -/
+#guard_msgs in
+#eval (ArithCircuit.add [.var 0, .var 1, .var 2, .var 3] : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
+
+-- mul, no overflow: (3*5) % 16 = 15 % 16 = 15
+/-- info: 15 -/
+#guard_msgs in
+#eval (ArithCircuit.mul (.var 1) (.var 2) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
+
+-- mul, WITH overflow: (5*15) % 16 = 75 % 16 = 11
+/-- info: 11 -/
+#guard_msgs in
+#eval (ArithCircuit.mul (.var 2) (.var 3) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
+
+-- (5*5) % 16 = 25 % 16 = 9
+/-- info: 9 -/
 #guard_msgs in
-#eval (ArithCircuit.mul (.var 0) (.var 1) : ArithCircuit 4).toBitHeap.eval (BitVecEnv.toBitEnv testEnv)
+#eval (ArithCircuit.mul (.var 2) (.var 2) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
 
--- 6 + 3 + 3 = 12
-/--
-info: 12
--/
+-- nesting: (6+3)*5 % 16 = 45 % 16 = 13
+/-- info: 13 -/
 #guard_msgs in
-#eval ((ArithCircuit.add [(.var 0), (.var 1), (.var 2)] : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
+#eval (ArithCircuit.mul (.add [.var 0, .var 1]) (.var 2) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
+
+----------
+
+/-- info: 13 -/
+#guard_msgs in
+#eval ((ArithCircuit.add [.var 0, .var 1, .var 2, .var 3] : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
+
+/-- info: 11 -/
+#guard_msgs in
+#eval ((ArithCircuit.mul (.var 2) (.var 3) : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
+
+/-- info: 9 -/
+#guard_msgs in
+#eval ((ArithCircuit.mul (.var 2) (.var 2) : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
+
+/-- info: 225 -/
+#guard_msgs in
+#eval ((ArithCircuit.var 3 : ArithCircuit 4).toBitHeap.mulBitHeap
+        (ArithCircuit.var 3 : ArithCircuit 4).toBitHeap).eval (BitVecEnv.toBitEnv testEnv)
+
+#eval toString ((ArithCircuit.var 3 : ArithCircuit 4).toBitHeap.mulBitHeap
+        (ArithCircuit.var 3 : ArithCircuit 4).toBitHeap)

From efc26dcaeaffa99e78479a93d61747d356805f49 Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Thu, 23 Jul 2026 23:11:12 +0100
Subject: [PATCH 11/13] compression proof

---
 DatapathVerification/BitHeap/BVComb.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index dbcd607..aa298a0 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -286,6 +286,12 @@ theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
     rw [evalMod_truncateMod, BitVec.toNat_mul, mulBitHeap_evalMod, Int.emod_emod_of_dvd _ hdvd, Int.mul_emod, ih1, ih2]
     congr 1
 
+theorem compressed_toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w)
+    (adders : List Chain.Adder) (h' : BitHeap w)
+    (heq : Chain.applyChainSafe adders c.toBitHeap = some h') :
+    h'.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int) := by
+  rw [Chain.applyChainSafe_correct_mod adders c.toBitHeap h' heq, toBitHeap_correct]
+
 end ArithCircuit
 
 end Comb

From 2718542365deb99e875d62a9dd518a3f11f484a8 Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Fri, 24 Jul 2026 00:24:29 +0100
Subject: [PATCH 12/13] examples

---
 .../BitHeap/Examples/BVCombExamples.lean      | 26 +++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/DatapathVerification/BitHeap/Examples/BVCombExamples.lean b/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
index 06ceeeb..73fdae1 100644
--- a/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
+++ b/DatapathVerification/BitHeap/Examples/BVCombExamples.lean
@@ -68,3 +68,29 @@ def testEnv : BitVecEnv 4 := fun i =>
 
 #eval toString ((ArithCircuit.var 3 : ArithCircuit 4).toBitHeap.mulBitHeap
         (ArithCircuit.var 3 : ArithCircuit 4).toBitHeap)
+
+------
+
+def compressed (c : ArithCircuit w) : BitHeap w := (DaddaTree.DaddaTree c.toBitHeap).1
+
+def addThree : ArithCircuit 4 := .add [.var 0, .var 1, .var 2]
+
+/-- info: "{0 ↦ [b4, b8, b0], 1 ↦ [b1, b5, b9], 2 ↦ [b2, b10, b6], 3 ↦ [b3, b11, b7]}" -/
+#guard_msgs in
+#eval toString addThree.toBitHeap
+
+/-- info: "{0 ↦ [(b4 ⊕ b8), b0], 1 ↦ [(b4 ∧ b8), ((b1 ⊕ b5) ⊕ b9)], 2 ↦ [(((b1 ∧ b5) ∨ (b1 ∧ b9)) ∨ (b5 ∧ b9)), ((b2 ⊕ b10) ⊕ b6)], 3 ↦ [(((b2 ∧ b10) ∨ (b2 ∧ b6)) ∨ (b10 ∧ b6)), ((b3 ⊕ b11) ⊕ b7)]}" -/
+#guard_msgs in
+#eval toString (compressed addThree)
+
+/-- info: "[HA(0: b4, b8), FA(1: b1, b5, b9), FA(2: b2, b10, b6), FA(3: b3, b11, b7)]" -/
+#guard_msgs in
+#eval toString (DaddaTree.DaddaTree addThree.toBitHeap).2
+
+/-- info: 13 -/
+#guard_msgs in
+#eval (compressed (.add [.var 0, .var 1, .var 2, .var 3] : ArithCircuit 4)).eval (BitVecEnv.toBitEnv testEnv)
+
+/-- info: 11 -/
+#guard_msgs in
+#eval (compressed (.mul (.var 2) (.var 3) : ArithCircuit 4)).eval (BitVecEnv.toBitEnv testEnv)

From f06b63604ae3437c3476ecdbc579c1d40678287b Mon Sep 17 00:00:00 2001
From: Osman Yasar <osmanyas05@gmail.com>
Date: Fri, 24 Jul 2026 12:03:06 +0100
Subject: [PATCH 13/13] no non-terminal simp

---
 DatapathVerification/BitHeap/BVComb.lean | 40 ++++++++++++++----------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
index aa298a0..d7c3cd6 100644
--- a/DatapathVerification/BitHeap/BVComb.lean
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -67,7 +67,7 @@ def toCircuitVector (c : ArithCircuit w) : CircuitVector :=
 
 theorem toBitEnv_apply (bv : BitVecEnv w) (i k : Nat) (hk : k < w) :
     bv.toBitEnv (i * w + k) = (bv i).getLsbD k := by
-  simp [BitVecEnv.toBitEnv]
+  simp only [BitVecEnv.toBitEnv, Nat.mul_add_mod_self_right]
   have h1 : (i * w + k) / w = i := by
     have hw : 0 < w := by grind
     rw [Nat.mul_comm, Nat.mul_add_div hw, Nat.add_eq_left, Nat.div_eq_of_lt hk]
@@ -108,7 +108,8 @@ theorem foldl_addBit_evalMod  (idx : Nat) (h : BitHeap w) (cs : List Circuit) :
     = (h.evalMod env + (cs.map (fun c => 2^idx * (c.eval env).toInt)).sum) % 2^w := by
     induction cs generalizing h with
     | nil =>
-      simp [evalMod]
+      simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, add_zero, dvd_refl,
+        Int.emod_emod_of_dvd]
     | cons c tl ih =>
       simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, BitHeap.evalMod_heap_addBit, Int.emod_add_emod]
       grind
@@ -121,7 +122,8 @@ theorem foldl_columns_evalMod (acc : BitHeap w) (ps : List (Column × Nat)) :
               (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum) % 2^w := by
     induction ps generalizing acc with
     | nil =>
-      simp [evalMod]
+      simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, add_zero, dvd_refl,
+        Int.emod_emod_of_dvd]
     | cons p tl ih =>
       simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, foldl_addBit_evalMod, Int.emod_add_emod]
       grind
@@ -130,7 +132,7 @@ theorem eval_eq_sum_columns (h : BitHeap w) (env : Circuit.BitEnv) :
     ((h.eval env : Int))
       = (h.columns.toList.zipIdx.map (fun p =>
           (p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
-  simp [eval]
+  simp only [eval]
   have h0 := hornersMethod_eq_sum_zipIdx env h.columns.toList 0
   simp only [pow_zero, one_mul] at h0
   exact h0
@@ -151,7 +153,8 @@ theorem foldl_mergeInto_evalMod (hs : List (BitHeap w)) (acc : BitHeap w) :
       simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, add_zero, dvd_refl,
         Int.emod_emod_of_dvd]
     | cons h tl ih =>
-      simp [List.foldl_cons, List.map_cons, List.sum_cons, ih, mergeInto_evalMod]
+      simp only [List.foldl_cons, ih, mergeInto_evalMod, Int.emod_add_emod, List.map_cons,
+        List.sum_cons]
       grind
 
 theorem foldl_add_init {w : ℕ} (acc hd : BitVec w) (tl : List (BitVec w)) :
@@ -171,7 +174,8 @@ theorem foldl_add_toNat_go (acc : BitVec w) (l : List (BitVec w)) :
     norm_cast
     simp only [BitVec.toNat_mod_cancel]
   | cons hd tl ih =>
-    simp [List.foldl_cons, List.map_cons, List.sum_cons, foldl_add_init, BitVec.toNat_add, ih]
+    simp only [List.foldl_cons, foldl_add_init, BitVec.toNat_add, Int.natCast_emod, Nat.cast_add,
+      ih, Nat.cast_pow, Nat.cast_ofNat, Int.emod_add_emod, List.map_cons, List.sum_cons]
     grind
 
 theorem foldl_andBit_evalMod (env : Circuit.BitEnv) (idx : Nat) (c1 : Circuit)
@@ -212,7 +216,8 @@ theorem foldl_mulColumns_evalMod (env : Circuit.BitEnv) (col0 : Column) (i0 : Na
           * (qs.map (fun q => 2^(i0 + q.2) * (q.1.eval env : Int))).sum) % 2^v := by
   induction qs generalizing acc with
   | nil =>
-    simp [evalMod]
+    simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, mul_zero, add_zero, dvd_refl,
+      Int.emod_emod_of_dvd]
   | cons q tl ih =>
     simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, mulColumns_evalMod,
       Int.emod_add_emod]
@@ -232,7 +237,7 @@ theorem mulRow_evalMod (env : Circuit.BitEnv) (col0 : Column) (i0 : Nat)
       = 2^i0 * (col0.eval env : Int) * (h1.eval env : Int) := by
     have hz := BitHeap.hornersMethod_mul_eq_sum_zipIdx env h1.columns.toList i0 0
     have heval : (h1.eval env : Int) = HornersMethod env h1.columns.toList := by
-      simp [eval]
+      simp only [eval]
     rw [heval, ← hz]
     simp only [Nat.add_zero]
     grind
@@ -249,23 +254,23 @@ theorem foldl_mulRow_evalMod (env : Circuit.BitEnv) (h1 : BitHeap w)
               * (h1.eval env : Int)) % 2^v := by
   induction ps generalizing acc with
   | nil =>
-    simp [evalMod]
+    simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, zero_mul, add_zero, dvd_refl,
+      Int.emod_emod_of_dvd]
   | cons p tl ih =>
-    simp [ih, mulRow_evalMod]
+    simp only [List.foldl_cons, ih, mulRow_evalMod, Int.emod_add_emod, List.map_cons, List.sum_cons]
     grind
 
 theorem mulBitHeap_evalMod (h0 h1 : BitHeap w) (env : Circuit.BitEnv) :
     (h0.mulBitHeap h1).evalMod env
       = ((h0.eval env : Int) * (h1.eval env : Int)) % 2^(2*w - 1) := by
-  simp [mulBitHeap]
+  simp only [mulBitHeap]
   rw [←Vector.foldl_toList, foldl_mulRow_evalMod]
   congr 1
   simp only [empty_evalMod, Vector.toList_zipIdx, zero_add, mul_eq_mul_right_iff,
     Int.natCast_eq_zero, eval]
   left
   have h0 := hornersMethod_eq_sum_zipIdx env h0.columns.toList 0
-  simp_all only [pow_zero, one_mul]
-  simp only [Column.eval_eq_sum, List.sum_map_mul_left]
+  simp_all [pow_zero, one_mul, Column.eval_eq_sum, List.sum_map_mul_left]
 
 theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
     c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int):= by
@@ -275,11 +280,12 @@ theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
     norm_cast
     rw [BitVec.toNat_mod_cancel]
   | case2 args ih =>
-    simp [denote, BitHeap.addBitHeap, foldl_mergeInto_evalMod, foldl_add_toNat_go]
+    simp only [addBitHeap, foldl_mergeInto_evalMod, empty_evalMod, List.map_map, zero_add, denote,
+      BitVec.ofNat_eq_ofNat, foldl_add_toNat_go, BitVec.toNat_ofNat, Nat.zero_mod, Nat.cast_zero]
     congr 2
-    simp
-    assumption
-  | case3 l r ih1 ih2=>
+    simp only [List.map_inj_left, Function.comp_apply]
+    exact ih
+  | case3 l r ih1 ih2 =>
     simp only [denote]
     simp only [BitHeap.evalMod] at ih1 ih2
     have hdvd : ((2:Int)^w) ∣ ((2:Int)^(2*w - 1)) := pow_dvd_pow 2 (by omega)