From 9d2de6922431ca768e7c1b7c9f7ffbd4fa2dfd3e Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Thu, 23 Apr 2026 18:02:01 +0100
Subject: [PATCH 1/3] add implementation

---
 DatapathVerification/CSA.lean | 77 +++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

diff --git a/DatapathVerification/CSA.lean b/DatapathVerification/CSA.lean
index fa3bf55..a46c629 100644
--- a/DatapathVerification/CSA.lean
+++ b/DatapathVerification/CSA.lean
@@ -14,6 +14,7 @@ structure CSAResult (w : ℕ) where
 -- The carry-save adder splits the sum into a partial sum `s` and
 -- carry bits `t`, such that the original sum is recovered by
 -- adding `s` to the carries shifted left by 1 (i.e., t * 2).
+@[bv_normalize]
 def carrySave (w : ℕ) (a b c : BitVec w) : CSAResult w :=
   let s := a ^^^ b ^^^ c
   let t := (a &&& b ||| a &&& c ||| b &&& c)
@@ -26,6 +27,7 @@ info: { s := 0x5#4, t := 0x5#4 }
 #eval carrySave 4 5 5 5
 
 -- a + b + c = CSA(a, b, c)
+@[bv_normalize]
 theorem carrySaveAdder (w : ℕ) (a b c : BitVec w) :
     let ⟨s, t⟩ := carrySave w a b c
     a + b + c = s + t <<< 1 := by
@@ -76,6 +78,7 @@ theorem mul4_correct (a b : BitVec 4) : a * b = mul4 a b := by
 
 -- N:2 compressor implementation.
 -- Takes a list of n Bitvectors and reduces them to 2 Bitvectors (sum and carry) using a tree of carry-save adders.
+@[bv_normalize]
 def chain {w : Nat} (v : List (BitVec w)) : CSAResult w :=
   match v with
   | [] => ⟨0, 0⟩
@@ -133,4 +136,78 @@ theorem chain_correct {w : Nat} (v : List (BitVec w)) :
       clear ih hrest
       bv_automata_classic
 
+@[bv_normalize]
+def chain_reverse {w : Nat} (v : List (BitVec w)) : CSAResult w :=
+  match v with
+  | [] => ⟨0, 0⟩
+  | [a] => ⟨a, 0⟩
+  | [a,b] => carrySave w a b 0
+  | [a,b,c] => carrySave w a b c
+  | a :: b :: c :: rest =>
+    let ⟨sum, carry⟩ := carrySave w a b c
+    let new_list := sum :: (carry <<< 1) :: rest
+    let back := new_list.reverse
+    let ⟨sum, carry⟩ := chain_reverse back
+    ⟨sum, carry⟩
+  termination_by v.length
+  decreasing_by
+    simp
+
+#eval chain_reverse (v := [5#10, 2#10, 3#10, 7#10, 3#10])
+
+theorem chain_reverse_correct {w : Nat} (v : List (BitVec w)) :
+    let ⟨s, t⟩ := chain_reverse v
+    list_sum v = s + t <<< 1 := by
+  induction v with
+  | nil =>
+    simp [chain_reverse, list_sum]
+  | cons hd rest ih =>
+    match hrest : rest with
+    | [] =>
+      simp [chain_reverse, list_sum]
+    | [a] =>
+      simp only [chain_reverse, list_sum, carrySave]
+      clear ih hrest rest
+      bv_automata_classic
+    | [a, b] =>
+      simp only [chain_reverse, list_sum, carrySave]
+      clear ih hrest rest
+      bv_automata_classic
+    | a :: b :: c :: rest' =>
+      simp only [chain_reverse, list_sum, carrySave] at ih ⊢
+      simp
+      unfold chain_reverse at ih ⊢
+      clear ih hrest
+      sorry
+      -- bv_automata_classic
+
+-- Recursive partial-products: produces `[p_{n-1}, p_{n-2}, ..., p_0]`
+-- where `p_i = (y[i] ? x : 0) <<< i`. Order is reversed vs. index.
+@[bv_normalize]
+def partialProducts' {w : Nat} (x y : BitVec w) : Nat → List (BitVec w)
+  | 0 => []
+  | n + 1 =>
+    let cur := if y.getLsbD n then (x <<< n) else 0
+    cur :: partialProducts' x y n
+
+@[bv_normalize]
+def partialProducts {w : Nat} (x y : BitVec w) : List (BitVec w) :=
+  partialProducts' x y w
+
+#eval partialProducts (5#4) (3#4)
+
+-- Multiplication circuit: build partial products, then sum them via the CSA chain.
+@[bv_normalize]
+def mulChain {w : Nat} (a b : BitVec w) : BitVec w :=
+  let ⟨s, t⟩ := chain_reverse (partialProducts a b)
+  s + t <<< 1
+
+#eval mulChain (5#4) (3#4)
+
+set_option trace.profiler true in
+theorem mul_comm' (x y : BitVec 8) : mulChain x y = mulChain y x  := by
+  simp [mulChain, partialProducts, partialProducts']
+  repeat (unfold chain_reverse; simp [List.reverse, List.reverseAux])
+  bv_decide
+
 end CSA

From b6be476f77d36856e39882dbb829b0400b0d065c Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Thu, 23 Apr 2026 22:39:27 +0100
Subject: [PATCH 2/3] implementation

---
 DatapathVerification/CSA.lean | 56 ++++++++++-------------------------
 1 file changed, 16 insertions(+), 40 deletions(-)

diff --git a/DatapathVerification/CSA.lean b/DatapathVerification/CSA.lean
index a46c629..9dc323b 100644
--- a/DatapathVerification/CSA.lean
+++ b/DatapathVerification/CSA.lean
@@ -136,8 +136,13 @@ theorem chain_correct {w : Nat} (v : List (BitVec w)) :
       clear ih hrest
       bv_automata_classic
 
+/-!
+  N:2 compressor implementation with a more optimized structure. Instead of chaining the carry-save adders in a linear fashion,
+  we compress the input list in a more balanced way. First we compress the first three elements, then we create a new list with the sum and carry from the first compression, and the remaining elements.
+  We then reverse this new list and apply the chain_opt function recursively. This enables applying the carry chain adders to the front and back of the list in parallel.
+-/
 @[bv_normalize]
-def chain_reverse {w : Nat} (v : List (BitVec w)) : CSAResult w :=
+def chain_opt {w : Nat} (v : List (BitVec w)) : CSAResult w :=
   match v with
   | [] => ⟨0, 0⟩
   | [a] => ⟨a, 0⟩
@@ -147,67 +152,38 @@ def chain_reverse {w : Nat} (v : List (BitVec w)) : CSAResult w :=
     let ⟨sum, carry⟩ := carrySave w a b c
     let new_list := sum :: (carry <<< 1) :: rest
     let back := new_list.reverse
-    let ⟨sum, carry⟩ := chain_reverse back
+    let ⟨sum, carry⟩ := chain_opt back
     ⟨sum, carry⟩
   termination_by v.length
   decreasing_by
     simp
 
-#eval chain_reverse (v := [5#10, 2#10, 3#10, 7#10, 3#10])
+#eval chain_opt (v := [5#10, 2#10, 3#10, 7#10, 3#10])
 
-theorem chain_reverse_correct {w : Nat} (v : List (BitVec w)) :
-    let ⟨s, t⟩ := chain_reverse v
+theorem chain_opt_correct {w : Nat} (v : List (BitVec w)) :
+    let ⟨s, t⟩ := chain_opt v
     list_sum v = s + t <<< 1 := by
   induction v with
   | nil =>
-    simp [chain_reverse, list_sum]
+    simp [chain_opt, list_sum]
   | cons hd rest ih =>
     match hrest : rest with
     | [] =>
-      simp [chain_reverse, list_sum]
+      simp [chain_opt, list_sum]
     | [a] =>
-      simp only [chain_reverse, list_sum, carrySave]
+      simp only [chain_opt, list_sum, carrySave]
       clear ih hrest rest
       bv_automata_classic
     | [a, b] =>
-      simp only [chain_reverse, list_sum, carrySave]
+      simp only [chain_opt, list_sum, carrySave]
       clear ih hrest rest
       bv_automata_classic
     | a :: b :: c :: rest' =>
-      simp only [chain_reverse, list_sum, carrySave] at ih ⊢
+      simp only [chain_opt, list_sum, carrySave] at ih ⊢
       simp
-      unfold chain_reverse at ih ⊢
+      unfold chain_opt at ih ⊢
       clear ih hrest
       sorry
       -- bv_automata_classic
 
--- Recursive partial-products: produces `[p_{n-1}, p_{n-2}, ..., p_0]`
--- where `p_i = (y[i] ? x : 0) <<< i`. Order is reversed vs. index.
-@[bv_normalize]
-def partialProducts' {w : Nat} (x y : BitVec w) : Nat → List (BitVec w)
-  | 0 => []
-  | n + 1 =>
-    let cur := if y.getLsbD n then (x <<< n) else 0
-    cur :: partialProducts' x y n
-
-@[bv_normalize]
-def partialProducts {w : Nat} (x y : BitVec w) : List (BitVec w) :=
-  partialProducts' x y w
-
-#eval partialProducts (5#4) (3#4)
-
--- Multiplication circuit: build partial products, then sum them via the CSA chain.
-@[bv_normalize]
-def mulChain {w : Nat} (a b : BitVec w) : BitVec w :=
-  let ⟨s, t⟩ := chain_reverse (partialProducts a b)
-  s + t <<< 1
-
-#eval mulChain (5#4) (3#4)
-
-set_option trace.profiler true in
-theorem mul_comm' (x y : BitVec 8) : mulChain x y = mulChain y x  := by
-  simp [mulChain, partialProducts, partialProducts']
-  repeat (unfold chain_reverse; simp [List.reverse, List.reverseAux])
-  bv_decide
-
 end CSA

From 60c21f19a7604b929111f90f2094c1aa2a571a7e Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Wed, 6 May 2026 16:06:37 +0100
Subject: [PATCH 3/3] compare

---
 DatapathVerification/compare.lean | 78 ++++++++++++++++++++++++++++---
 1 file changed, 72 insertions(+), 6 deletions(-)

diff --git a/DatapathVerification/compare.lean b/DatapathVerification/compare.lean
index 3ed7647..f67e0e7 100644
--- a/DatapathVerification/compare.lean
+++ b/DatapathVerification/compare.lean
@@ -1,6 +1,8 @@
 import Blase
 import DatapathVerification.CSA
 
+set_option maxHeartbeats 50000000
+set_option Elab.async false
 /-!
   This file compares the performance of bv_decide in different multiplication circuits.
 -/
@@ -10,29 +12,85 @@ namespace CSA
 
 -- Multiplication implementation based on compression of partial products.
 set_option trace.profiler true in
-theorem mul_comm_4bit (x y : BitVec 4) : mulChain x y = mulChain y x  := by
+theorem mulChain_4bit (x y : BitVec 4) : mulChain x y = mulChain y x  := by
   bv_decide
 
 set_option trace.profiler true in
-theorem mul_comm_5bit (x y : BitVec 5) : mulChain x y = mulChain y x  := by
+theorem mulChain_5bit (x y : BitVec 5) : mulChain x y = mulChain y x  := by
   bv_decide
 
 set_option trace.profiler true in
-theorem mul_comm_6bit (x y : BitVec 6) : mulChain x y = mulChain y x  := by
+theorem mulChain_6bit (x y : BitVec 6) : mulChain x y = mulChain y x  := by
   bv_decide
 
 set_option trace.profiler true in
-theorem mul_comm_7bit (x y : BitVec 7) : mulChain x y = mulChain y x  := by
+theorem mulChain_7bit (x y : BitVec 7) : mulChain x y = mulChain y x  := by
   bv_decide
 
 set_option trace.profiler true in
-theorem mul_comm_8bit (x y : BitVec 8) : mulChain x y = mulChain y x  := by
+theorem mulChain_8bit (x y : BitVec 8) : mulChain x y = mulChain y x  := by
   bv_decide
 
 set_option trace.profiler true in
-theorem mul_comm_9bit (x y : BitVec 9) : mulChain x y = mulChain y x  := by
+theorem mulChain_9bit (x y : BitVec 9) : mulChain x y = mulChain y x  := by
   bv_decide
 
+set_option trace.profiler true in
+theorem mulChain_10bit (x y : BitVec 10) : mulChain x y = mulChain y x  := by
+  bv_decide (config := { timeout := 200})
+
+set_option trace.profiler true in
+theorem mulChain_11bit (x y : BitVec 11) : mulChain x y = mulChain y x  := by
+  bv_decide (config := { timeout := 200})
+
+set_option trace.profiler true in
+theorem mulChain_opt_4bit (x y : BitVec 4) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide
+
+set_option trace.profiler true in
+theorem mulChain_opt_5bit (x y : BitVec 5) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide
+
+set_option trace.profiler true in
+theorem mulChain_opt_6bit (x y : BitVec 6) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide
+
+set_option trace.profiler true in
+theorem mulChain_opt_7bit (x y : BitVec 7) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide
+
+set_option trace.profiler true in
+theorem mulChain_opt_8bit (x y : BitVec 8) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide
+
+set_option trace.profiler true in
+theorem mulChain_opt_9bit (x y : BitVec 9) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide
+
+set_option trace.profiler true in
+theorem mulChain_opt_10bit (x y : BitVec 10) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide (config := { timeout := 200})
+
+set_option trace.profiler true in
+theorem mulChain_opt_11bit (x y : BitVec 11) : mulChain_opt x y = mulChain_opt y x  := by
+  simp [mulChain_opt, partialProducts, partialProducts']
+  repeat (unfold chain_opt; simp [List.reverse, List.reverseAux])
+  bv_decide (config := { timeout := 400})
+
 end CSA
 
 -- Multiplication implementation used in the Bit Blaster of Lean 4.
@@ -73,4 +131,12 @@ set_option trace.profiler true in
 theorem mul_comm_9bit (x y : BitVec 9) : mulRef x y = mulRef y x  := by
     bv_decide
 
+set_option trace.profiler true in
+theorem mul_comm_10bit (x y : BitVec 10) : mulRef x y = mulRef y x  := by
+  bv_decide (config := { timeout := 200})
+
+set_option trace.profiler true in
+theorem mul_comm_11bit (x y : BitVec 11) : mulRef x y = mulRef y x  := by
+  bv_decide (config := { timeout := 200})
+
 end CSABlastMul