From 6c00182d5f729c4e58e4137605bf1d530045f97a Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Thu, 25 Jun 2026 14:54:02 +0100
Subject: [PATCH 01/10] addbit proof

---
 DatapathVerification/BitHeap/BitHeap.lean | 109 ++++++++++++++++------
 DatapathVerification/BitHeap/Column.lean  |  21 ++++-
 2 files changed, 96 insertions(+), 34 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index b69c6f4..bee83e9 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -1,10 +1,8 @@
-import Std.Data.HashMap
 import Std.Data.HashSet
 import DatapathVerification.BitHeap.Circuit
 import DatapathVerification.BitHeap.Column
 import Mathlib.Tactic.SplitIfs
-import Std.Data.HashMap.Lemmas
-import Std.Tactic.Do
+import Mathlib.Algebra.Divisibility.Basic
 
 structure BitHeap (width : Nat) where
   columns : Vector BitHeap.Column width
@@ -22,11 +20,19 @@ instance : ToString (BitHeap w) where
 
 def empty (w : Nat) : BitHeap w := ⟨Vector.replicate w Column.empty⟩
 
+/--
+Horner's method to compute the weighted sum
+-/
+def HornersMethod (env : BitEnv) : List Column → Nat
+  | [] => 0
+  | c :: rest => (c.eval env) + 2 * HornersMethod env rest
+
 /--
 Evaluate a bit-heap, to compute the final sum of all the bits in the heap.
 -/
-def eval (h : BitHeap w) (env : BitEnv) : Int :=
-  h.columns.toList.zipIdx.foldl (fun acc (col, idx) => acc + 2^idx * col.eval env) 0
+def eval (h : BitHeap w) (env : BitEnv) : Nat :=
+  HornersMethod env h.columns.toList
+  -- h.columns.toList.zipIdx.foldl (fun acc (col, idx) => acc + 2^idx * col.eval env) 0
 
 /--
 Evaluate a bit-heap modulo 2^width, to compute the final sum of all the bits in the heap.
@@ -109,15 +115,54 @@ theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env
   -- have : (h.columns.modify column fun col => col.erase c)  = h.columns - 2 ^ column * (c.eval env).toInt := by sorry
   sorry
 
-theorem by_pow2_of_zero_eval (h : BitHeap w) (h1 : col ≥ w) :
-  (2 : Int) ^ w ∣ (2 : Int) ^ col := by
-  sorry
-  -- exact Nat.pow_dvd_pow_iff_le_right'.mpr h1 -> this works for Nat.
+-- 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
 
-theorem eval_insertColumn (h : BitHeap w) (k : Nat) (col : Column) (env : BitEnv) (h1 : column < w) :
-    ({ columns := h.columns.set column col h1 } : BitHeap w).eval env
-      = ({ columns := h.columns.set column (Column.empty) h1} : BitHeap w).eval env + 2 ^ column * (col.eval env : Int) := by
-  sorry
+@[grind => ]
+theorem eval_insertColumn_eq_eval_add (h : BitHeap w) (k : Nat) (v : Column) (env : BitEnv) (h1 : k < w) :
+    ({ columns := h.columns.set k v h1 } : BitHeap w).eval env
+      = h.eval env + 2 ^ k * (v.eval env : Int) - 2 ^ k * ((h.get k).eval env : Int) := by
+  simp only [BitHeap.eval, Vector.toList_set]
+  rw [hornersMethod_set env h.columns.toList k v (by simpa using h1)]
+  simp only [Vector.getElem_toList, Int.sub_right_inj]
+  rw [getD_in_bounds h k h1]
+
+@[grind => ]
+theorem eval_eraseColumn_eq_eval_sub (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
+    ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env
+      = h.eval env - 2 ^ k * ((h.get k).eval env : Int) := by
+  simp only [BitHeap.eval, Vector.toList_set]
+  rw [hornersMethod_set env h.columns.toList k (Column.empty) (by simpa using h1)]
+  simp only [empty_eval_zero, Int.cast_ofNat_Int, Int.mul_zero, Int.add_zero, Vector.getElem_toList,
+    Int.sub_right_inj]
+  rw [getD_in_bounds h k h1]
+
+theorem eval_insertColumn (h : BitHeap w) (k : Nat) (col : Column) (env : BitEnv) (h1 : k < w) :
+    ({ columns := h.columns.set k col h1 } : BitHeap w).eval env
+      = ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env + 2 ^ k * (col.eval env : Nat) := by
+  have := eval_insertColumn_eq_eval_add h k col env h1
+  have := eval_eraseColumn_eq_eval_sub h k env h1
+  grind only
+
+theorem eval_eraseColumn (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
+    h.eval env
+      = ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env + 2 ^ k * ((h.get k).eval env : Nat) := by
+  have := eval_eraseColumn_eq_eval_sub h k env h1
+  grind
 
 @[simp]
 theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env : BitEnv) :
@@ -132,21 +177,18 @@ theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env :
       · simp only [Bool.toInt_true]
         rw [Int.mul_one]
         apply Int.emod_eq_zero_of_dvd
-        exact_mod_cast by_pow2_of_zero_eval h h1
+        have : (2:Nat)^w ∣ (2:Nat)^col := Nat.pow_dvd_pow 2 h1
+        exact Int.natAbs_dvd_natAbs.mp this
     simp [Int.add_emod, h3]
   | case2 column h h4 h3 col h1 =>
     simp only [evalMod, Int.emod_add_emod]
     have : ({ columns := h.columns.set column (col.insert c) h3 } : BitHeap w).eval env = (h.eval env + 2 ^ column * (c.eval env).toInt) := by
-      simp_all
       rw [eval_insertColumn]
-      · rw [Column.eval_insert]
-        · simp
-          rw [Int.mul_add]
-          simp [eval]
-          sorry
-        · simp
-          exact h1
-      · exact h.maxHeight
+      rw [eval_eraseColumn h column env h3]
+      rw [Column.eval_insert]
+      · push_cast
+        cases c.eval env <;> simp <;> grind
+      · simp_all
     rw [this]
   | case3 col h h4 h3 h2 h1 ih =>
     rw [ih]
@@ -176,30 +218,39 @@ theorem get_removeBit_of_ne (column : Nat) (h : BitHeap w) (i j : Circuit)
     rw [hr]
     exact h1
 
+@[grind => ]
 theorem removeBit_decreases_size (col : Nat) (c : Circuit) (h : BitHeap w) (h1: c ∈ h.get col) :
-    ((removeBit col c h).get col).height < (h.get col).height := by
+    ((removeBit col c h).get col).height ≤ (h.get col).height := by
   simp only [removeBit, height_eq_size]
   simp [erase]
-  sorry
+  by_cases h2 : col < w
+  · rw [getD_in_bounds _ _ h2]
+    rw [Vector.getElem_setIfInBounds]
+    grind
+  · rw [Vector.setIfInBounds_eq_of_size_le]
+    · simp
+    · grind
 
+@[grind => ]
 theorem double_removeBit_decreases (col : Nat) (c₁ c₂ : Circuit) (h : BitHeap w)
     (h1 : c₁ ∈ h.get col) (h2 : c₂ ∈ h.get col) (hne : c₁ ≠ c₂) :
-  ((removeBit col c₁ (removeBit col c₂ h)).get col).height < (h.get col).height := by
+  ((removeBit col c₁ (removeBit col c₂ h)).get col).height ≤ (h.get col).height := by
     have h1' : c₁ ∈ (removeBit col c₂ h).get col :=
       get_removeBit_of_ne col h c₁ c₂ h1 hne
-    exact Nat.lt_trans
+    exact Nat.le_trans
       (removeBit_decreases_size col c₁ (removeBit col c₂ h) h1')
       (removeBit_decreases_size col c₂ h h2)
 
+@[grind => ]
 theorem triple_removeBit_decreases (col : Nat) (c₁ c₂ c₃ : Circuit) (h : BitHeap w)
     (h1 : c₁ ∈ h.get col) (h2 : c₂ ∈ h.get col) (h3 : c₃ ∈ h.get col)
     (hne12 : c₁ ≠ c₂) (hne13 : c₁ ≠ c₃) (hne23 : c₂ ≠ c₃) :
-  ((removeBit col c₁ (removeBit col c₂ (removeBit col c₃ h))).get col).height < (h.get col).height := by
+  ((removeBit col c₁ (removeBit col c₂ (removeBit col c₃ h))).get col).height ≤ (h.get col).height := by
     have h1' : c₁ ∈ (removeBit col c₃ h).get col :=
       get_removeBit_of_ne col h c₁ c₃ h1 hne13
     have h2' : c₂ ∈ (removeBit col c₃ h).get col :=
       get_removeBit_of_ne col h c₂ c₃ h2 hne23
-    exact Nat.lt_trans
+    exact Nat.le_trans
       (double_removeBit_decreases col c₁ c₂ (removeBit col c₃ h) h1' h2' hne12)
       (removeBit_decreases_size col c₃ h h3)
 
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index 2acc1a4..579dbb7 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -46,6 +46,12 @@ def height (col : Column) : Nat :=
 @[simp]
 theorem height_eq_size (col : Column) : col.height = col.elems.size := rfl
 
+@[simp]
+theorem empty_eval_zero (col : Column) (env : BitEnv) (h : col = Column.empty) : col.eval env = 0 := by
+  simp_all [eval, empty]
+  rw [Std.HashSet.fold_eq_foldl_toList]
+  simp
+
 def toList (col : Column) : List Circuit :=
   col.elems.toList
 
@@ -60,17 +66,21 @@ theorem foldl_sum (l : List Circuit) (env : BitEnv) (a : Nat) :
   | cons p ps ih =>
     grind
 
+@[grind =>]
+theorem Std.HashSet.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+  (m : Std.HashSet α) :
+    (m.erase d).toList.Perm (m.toList.filter (fun x => (x == d) = false)) := by
+  sorry
+
 @[simp]
 theorem eval_erase (col : Column) (c : Circuit) (env : BitEnv) (h : c ∈ col) :
-    (col.erase c).eval env = col.eval env - (c.eval env).toInt := by
+    (col.erase c).eval env = col.eval env - (c.eval env).toNat := by
   simp [eval, erase]
-  repeat rw [Std.HashSet.fold_eq_foldl_toList]
-  rw [eq_comm, Int.sub_eq_iff_eq_add']
-  repeat rw [foldl_sum]
+  repeat rw [Std.HashSet.fold_eq_foldl_toList, foldl_sum]
   simp only [Nat.zero_add]
   have : col.elems.toList.Perm (c :: (col.elems.erase c).toList) := by
     sorry
-  sorry
+  grind
 
 @[simp]
 theorem eval_insert (col : Column) (c : Circuit) (env : BitEnv) (h : c ∉ col) :
@@ -85,6 +95,7 @@ theorem eval_insert (col : Column) (c : Circuit) (env : BitEnv) (h : c ∉ col)
     exact key
   grind
 
+
 end Column
 
 end BitHeap

From c5c7771702324200166ce9ed5cb1ed9b537ca3a7 Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Thu, 25 Jun 2026 15:03:54 +0100
Subject: [PATCH 02/10] nit

---
 DatapathVerification/BitHeap/BitHeap.lean | 21 ++++++---------------
 DatapathVerification/BitHeap/Column.lean  |  7 -------
 2 files changed, 6 insertions(+), 22 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index bee83e9..399ad04 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -218,39 +218,30 @@ theorem get_removeBit_of_ne (column : Nat) (h : BitHeap w) (i j : Circuit)
     rw [hr]
     exact h1
 
-@[grind => ]
 theorem removeBit_decreases_size (col : Nat) (c : Circuit) (h : BitHeap w) (h1: c ∈ h.get col) :
-    ((removeBit col c h).get col).height ≤ (h.get col).height := by
+    ((removeBit col c h).get col).height < (h.get col).height := by
   simp only [removeBit, height_eq_size]
   simp [erase]
-  by_cases h2 : col < w
-  · rw [getD_in_bounds _ _ h2]
-    rw [Vector.getElem_setIfInBounds]
-    grind
-  · rw [Vector.setIfInBounds_eq_of_size_le]
-    · simp
-    · grind
+  sorry
 
-@[grind => ]
 theorem double_removeBit_decreases (col : Nat) (c₁ c₂ : Circuit) (h : BitHeap w)
     (h1 : c₁ ∈ h.get col) (h2 : c₂ ∈ h.get col) (hne : c₁ ≠ c₂) :
-  ((removeBit col c₁ (removeBit col c₂ h)).get col).height ≤ (h.get col).height := by
+  ((removeBit col c₁ (removeBit col c₂ h)).get col).height < (h.get col).height := by
     have h1' : c₁ ∈ (removeBit col c₂ h).get col :=
       get_removeBit_of_ne col h c₁ c₂ h1 hne
-    exact Nat.le_trans
+    exact Nat.lt_trans
       (removeBit_decreases_size col c₁ (removeBit col c₂ h) h1')
       (removeBit_decreases_size col c₂ h h2)
 
-@[grind => ]
 theorem triple_removeBit_decreases (col : Nat) (c₁ c₂ c₃ : Circuit) (h : BitHeap w)
     (h1 : c₁ ∈ h.get col) (h2 : c₂ ∈ h.get col) (h3 : c₃ ∈ h.get col)
     (hne12 : c₁ ≠ c₂) (hne13 : c₁ ≠ c₃) (hne23 : c₂ ≠ c₃) :
-  ((removeBit col c₁ (removeBit col c₂ (removeBit col c₃ h))).get col).height ≤ (h.get col).height := by
+  ((removeBit col c₁ (removeBit col c₂ (removeBit col c₃ h))).get col).height < (h.get col).height := by
     have h1' : c₁ ∈ (removeBit col c₃ h).get col :=
       get_removeBit_of_ne col h c₁ c₃ h1 hne13
     have h2' : c₂ ∈ (removeBit col c₃ h).get col :=
       get_removeBit_of_ne col h c₂ c₃ h2 hne23
-    exact Nat.le_trans
+    exact Nat.lt_trans
       (double_removeBit_decreases col c₁ c₂ (removeBit col c₃ h) h1' h2' hne12)
       (removeBit_decreases_size col c₃ h h3)
 
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index 579dbb7..8806a6c 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -66,12 +66,6 @@ theorem foldl_sum (l : List Circuit) (env : BitEnv) (a : Nat) :
   | cons p ps ih =>
     grind
 
-@[grind =>]
-theorem Std.HashSet.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
-  (m : Std.HashSet α) :
-    (m.erase d).toList.Perm (m.toList.filter (fun x => (x == d) = false)) := by
-  sorry
-
 @[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
@@ -95,7 +89,6 @@ theorem eval_insert (col : Column) (c : Circuit) (env : BitEnv) (h : c ∉ col)
     exact key
   grind
 
-
 end Column
 
 end BitHeap

From db77f81fc518f93d81a0d400870e32060c12d58e Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Thu, 25 Jun 2026 21:40:03 +0100
Subject: [PATCH 03/10] wip for removeBit

---
 DatapathVerification/BitHeap/BitHeap.lean | 41 +++++++++++++++++------
 DatapathVerification/BitHeap/Column.lean  |  6 +++-
 2 files changed, 36 insertions(+), 11 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 399ad04..5722053 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -105,16 +105,6 @@ def fullAdder (column : Nat) (i j k : Circuit) (h : BitHeap w) : AdderResult w :
   let h := h.addBit (column + 1) carry
   ⟨h, sum, carry⟩
 
-@[simp]
-theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env : BitEnv) (h1 : c ∈ h.get column) :
-  (h.removeBit column c).evalMod env = (h.evalMod env - 2^(column) * (c.eval env).toInt) % 2^(w) := by
-  unfold evalMod
-  simp [eval, removeBit]
-  have : (h.get column |>.erase c).eval env = (h.get column).eval env - 2 ^ column * (c.eval env).toInt := by
-    sorry
-  -- have : (h.columns.modify column fun col => col.erase c)  = h.columns - 2 ^ column * (c.eval env).toInt := by sorry
-  sorry
-
 -- 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) :
@@ -164,6 +154,37 @@ theorem eval_eraseColumn (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
   have := eval_eraseColumn_eq_eval_sub h k env h1
   grind
 
+
+theorem if_elem_not_empty (col : Nat) (c : Circuit) (h : BitHeap w) :
+   (c ∈ h.get col) → (col < w) := by
+  intro h1
+  by_contra hge
+  simp at hge
+  have hempty : h.get col = Column.empty := by
+    simp [get, Vector.getD, hge]
+  rw [hempty, mem_iff_contains, Column.empty, Column.contains] at h1
+  grind
+
+@[simp]
+theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env : BitEnv) (h1 : c ∈ h.get column) :
+  (h.removeBit column c).evalMod env = (h.evalMod env - 2^(column) * (c.eval env).toInt) % 2^(w) := by
+  simp [evalMod, removeBit]
+  have : ({ columns := h.columns.setIfInBounds column ((h.get column).erase c) : BitHeap w}.eval env) = (↑(h.eval env) - 2 ^ column * (c.eval env).toInt) := by
+    simp only [eval, Vector.toList_setIfInBounds]
+    rw [hornersMethod_set]
+    · rw [eval_erase]
+      ·
+        rw [getD_in_bounds h column]
+        ·
+          push_cast
+          sorry
+        · exact if_elem_not_empty column c h h1
+      · exact h1
+    · simp
+      exact if_elem_not_empty column c h h1
+
+  rw [this]
+
 @[simp]
 theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env : BitEnv) :
     (h.addBit column c).evalMod env = (h.evalMod env +  2^column  * (c.eval env).toInt) % 2^(w) := by
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index 8806a6c..b6fee4b 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -66,7 +66,11 @@ theorem foldl_sum (l : List Circuit) (env : BitEnv) (a : Nat) :
   | cons p ps ih =>
     grind
 
-@[simp]
+theorem Std.HashSet.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+  (m : Std.HashSet α) :
+    (m.erase d).toList.Perm (m.toList.filter (fun x => (x == d) = false)) := by
+  sorry
+
 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
   simp [eval, erase]

From deeb66e047baa91e3397782e701be4ee307fb94c Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 02:39:16 +0100
Subject: [PATCH 04/10] work on removebit

---
 DatapathVerification/BitHeap/BitHeap.lean | 21 ++++++++++++---------
 DatapathVerification/BitHeap/Column.lean  |  4 ++++
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 5722053..bf39a97 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -154,7 +154,6 @@ theorem eval_eraseColumn (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
   have := eval_eraseColumn_eq_eval_sub h k env h1
   grind
 
-
 theorem if_elem_not_empty (col : Nat) (c : Circuit) (h : BitHeap w) :
    (c ∈ h.get col) → (col < w) := by
   intro h1
@@ -162,8 +161,8 @@ theorem if_elem_not_empty (col : Nat) (c : Circuit) (h : BitHeap w) :
   simp at hge
   have hempty : h.get col = Column.empty := by
     simp [get, Vector.getD, hge]
-  rw [hempty, mem_iff_contains, Column.empty, Column.contains] at h1
-  grind
+  rw [hempty, mem_iff_contains, Column.empty, Column.contains, Std.HashSet.contains_emptyWithCapacity] at h1
+  contradiction
 
 @[simp]
 theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env : BitEnv) (h1 : c ∈ h.get column) :
@@ -173,16 +172,20 @@ theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env
     simp only [eval, Vector.toList_setIfInBounds]
     rw [hornersMethod_set]
     · rw [eval_erase]
-      ·
-        rw [getD_in_bounds h column]
-        ·
-          push_cast
-          sorry
+      · rw [getD_in_bounds h column]
+        · rw [Int.add_sub_assoc]
+          have hidx : ∀ (hb : column < w), h.columns[column] = h.columns.toList[column]'(by grind) := by
+            simp [Vector.getElem_toList]
+          rw [hidx]
+          rw [Int.natCast_sub]
+          · cases c.eval env <;> simp_all <;> grind
+          · simp [Column.eval]
+            cases c.eval env <;> simp
+            sorry
         · exact if_elem_not_empty column c h h1
       · exact h1
     · simp
       exact if_elem_not_empty column c h h1
-
   rw [this]
 
 @[simp]
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index b6fee4b..41f2ee1 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -17,6 +17,10 @@ instance : ToString Column where
 
 namespace Column
 
+#check @Std.HashSet.contains_emptyWithCapacity   -- (emptyWithCapacity n).contains a = false
+#check @Std.HashSet.not_mem_emptyWithCapacity    -- ¬ a ∈ emptyWithCapacity n
+-- or possibly mem_emptyWithCapacity : a ∈ emptyWithCapacity n ↔ False
+
 def contains (col : Column) (c : Circuit) : Bool :=
   col.elems.contains c
 

From 99b323c08ba931dca1875d47a30fba19fcc9ec63 Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 14:40:28 +0100
Subject: [PATCH 05/10] add lemmas

---
 DatapathVerification/BitHeap/BitHeap.lean     |  2 +
 DatapathVerification/BitHeap/Column.lean      |  5 +-
 .../BitHeap/HashSetLemmas.lean                | 71 +++++++++++++++++++
 3 files changed, 74 insertions(+), 4 deletions(-)
 create mode 100644 DatapathVerification/BitHeap/HashSetLemmas.lean

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index bf39a97..45231dd 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -181,6 +181,8 @@ theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env
           · cases c.eval env <;> simp_all <;> grind
           · simp [Column.eval]
             cases c.eval env <;> simp
+            rw [Std.HashSet.fold_eq_foldl_toList]
+            simp [Column.foldl_sum]
             sorry
         · exact if_elem_not_empty column c h h1
       · exact h1
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index 41f2ee1..0e54c03 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -1,5 +1,6 @@
 import Std.Data.HashSet
 import DatapathVerification.BitHeap.Circuit
+import DatapathVerification.BitHeap.HashSetLemmas
 
 namespace BitHeap
 
@@ -17,10 +18,6 @@ instance : ToString Column where
 
 namespace Column
 
-#check @Std.HashSet.contains_emptyWithCapacity   -- (emptyWithCapacity n).contains a = false
-#check @Std.HashSet.not_mem_emptyWithCapacity    -- ¬ a ∈ emptyWithCapacity n
--- or possibly mem_emptyWithCapacity : a ∈ emptyWithCapacity n ↔ False
-
 def contains (col : Column) (c : Circuit) : Bool :=
   col.elems.contains c
 
diff --git a/DatapathVerification/BitHeap/HashSetLemmas.lean b/DatapathVerification/BitHeap/HashSetLemmas.lean
new file mode 100644
index 0000000..8d53857
--- /dev/null
+++ b/DatapathVerification/BitHeap/HashSetLemmas.lean
@@ -0,0 +1,71 @@
+import Std.Data.HashMap.Lemmas
+import Std.Data.HashSet.Lemmas
+
+open Std
+
+theorem List.Perm.of_nodup_of_nodup_of_forall_mem_iff_mem {α : Type u} (l₁ l₂ : List α)
+  (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) (h₃ : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) :
+    l₁.Perm l₂ := by
+  induction l₁ generalizing l₂ with
+  | nil => simp_all [List.eq_nil_iff_forall_not_mem]
+  | cons hd tl ih =>
+    classical
+    simp only [mem_cons] at h₃
+    refine (Perm.trans ((perm_cons _).2 ?_) (perm_cons_erase ((h₃ hd).1 (Or.inl rfl))).symm)
+    exact ih _ h₁.tail (h₂.erase _) (by simpa [h₂.mem_erase_iff, ← h₃, and_or_left] using
+      fun _ => (ne_of_mem_of_not_mem · (List.nodup_cons.1 h₁).1))
+
+theorem List.filter_nodup {l : List α} {p : α → Bool} (hl : l.Nodup) :
+    (l.filter p).Nodup := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp [filter_cons]
+    split
+    · grind
+    · grind
+
+theorem Std.HashMap.nodup_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+  (m : HashMap α β) :
+    m.toList.Nodup := by
+  have := HashMap.nodup_keys (m := m)
+  simp [← HashMap.map_fst_toList_eq_keys] at this
+  rw [List.nodup_iff_pairwise_ne] at this ⊢
+  apply List.Pairwise.of_map _ _ this
+  simp
+
+theorem Std.HashMap.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+  (m : HashMap α β) :
+    (m.erase d).toList.Perm (m.toList.filter (fun x => (x.1 == d) = false)) := by
+  apply List.Perm.of_nodup_of_nodup_of_forall_mem_iff_mem
+  · apply HashMap.nodup_toList
+  · apply List.filter_nodup
+    apply HashMap.nodup_toList
+  · simp [HashMap.getKey?_erase, HashMap.getElem?_erase]
+    intro a b
+    by_cases h : d == a
+    · simp [h, BEq.symm h]
+    · simp at h
+      simp [h, BEq.symm_false h]
+
+theorem Std.HashSet.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+  (m : Std.HashSet α) :
+    (m.erase d).toList.Perm (m.toList.filter (fun x => (x == d) = false)) := by
+  simp [toList, ← HashMap.map_fst_toList_eq_keys, erase]
+  apply List.Perm.of_nodup_of_nodup_of_forall_mem_iff_mem
+  · rw [List.nodup_iff_pairwise_ne]
+    apply List.Pairwise.map (fun (x : α × Unit) => x.1) (R := fun a b => a ≠ b)
+    · grind
+    · apply HashMap.nodup_toList
+  · apply List.filter_nodup
+    apply List.Pairwise.map (fun (x : α × Unit) => x.1) (R := fun a b => a ≠ b)
+    · grind
+    · apply HashMap.nodup_toList
+  · intro a
+    simp only [List.mem_filter, Bool.not_eq_eq_eq_not,
+      Bool.not_true, List.mem_map]
+    simp [HashMap.getKey?_erase, HashMap.getElem?_erase]
+    by_cases h : d == a
+    · simp [h, BEq.symm h]
+    · simp at h
+      simp [h, BEq.symm_false h]

From 2cda2a902a33b4727b2b49d25da0c5a7fe8184ef Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 15:52:09 +0100
Subject: [PATCH 06/10] evalMod_heap_removeBit proof

---
 DatapathVerification/BitHeap/BitHeap.lean     | 16 +++++++++++---
 DatapathVerification/BitHeap/Column.lean      | 21 ++++++++++++-------
 .../BitHeap/HashSetLemmas.lean                |  9 ++++++++
 3 files changed, 36 insertions(+), 10 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 45231dd..bc82d31 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -3,6 +3,8 @@ import DatapathVerification.BitHeap.Circuit
 import DatapathVerification.BitHeap.Column
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Algebra.Divisibility.Basic
+import Mathlib.Algebra.Order.BigOperators.Group.List
+import Mathlib.Algebra.Order.Group.Nat
 
 structure BitHeap (width : Nat) where
   columns : Vector BitHeap.Column width
@@ -152,7 +154,7 @@ theorem eval_eraseColumn (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
     h.eval env
       = ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env + 2 ^ k * ((h.get k).eval env : Nat) := by
   have := eval_eraseColumn_eq_eval_sub h k env h1
-  grind
+  grind only
 
 theorem if_elem_not_empty (col : Nat) (c : Circuit) (h : BitHeap w) :
    (c ∈ h.get col) → (col < w) := by
@@ -180,10 +182,18 @@ theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env
           rw [Int.natCast_sub]
           · cases c.eval env <;> simp_all <;> grind
           · simp [Column.eval]
-            cases c.eval env <;> simp
             rw [Std.HashSet.fold_eq_foldl_toList]
             simp [Column.foldl_sum]
-            sorry
+            apply List.single_le_sum
+            · intro hx hy
+              exact Nat.zero_le hx
+            · simp
+              use c
+              constructor
+              · rw [getD_in_bounds h column (by exact if_elem_not_empty column c h h1)] at h1
+                simp [Column.mem_iff_contains, Column.contains] at h1
+                exact h1
+              · rfl
         · exact if_elem_not_empty column c h h1
       · exact h1
     · simp
diff --git a/DatapathVerification/BitHeap/Column.lean b/DatapathVerification/BitHeap/Column.lean
index 0e54c03..b7dfad7 100644
--- a/DatapathVerification/BitHeap/Column.lean
+++ b/DatapathVerification/BitHeap/Column.lean
@@ -67,18 +67,25 @@ theorem foldl_sum (l : List Circuit) (env : BitEnv) (a : Nat) :
   | cons p ps ih =>
     grind
 
-theorem Std.HashSet.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
-  (m : Std.HashSet α) :
-    (m.erase d).toList.Perm (m.toList.filter (fun x => (x == d) = false)) := by
-  sorry
-
+@[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
   simp [eval, erase]
   repeat rw [Std.HashSet.fold_eq_foldl_toList, foldl_sum]
   simp only [Nat.zero_add]
-  have : col.elems.toList.Perm (c :: (col.elems.erase c).toList) := by
-    sorry
+  have hP1 : col.elems.toList.Perm (c :: (col.elems.erase c).toList) := by
+    have hP2: col.elems.toList.Perm (c :: col.elems.toList.filter (fun x => (x == c) = false)) := by
+      simp
+      have helem : c ∈ col.elems.toList := by
+        simpa
+      have hNp : col.elems.toList.Nodup := by
+        exact Std.HashSet.nodup_toList col.elems
+      have hFnp : (col.elems.toList.filter (fun x => (x == c) = false)).Nodup := by
+        exact List.filter_nodup hNp
+      grind
+    have : (col.elems.erase c).toList.Perm (col.elems.toList.filter (fun x => (x == c) = false)) := by
+      apply Std.HashSet.erase_toList_perm_filter_toList
+    grind
   grind
 
 @[simp]
diff --git a/DatapathVerification/BitHeap/HashSetLemmas.lean b/DatapathVerification/BitHeap/HashSetLemmas.lean
index 8d53857..79304fc 100644
--- a/DatapathVerification/BitHeap/HashSetLemmas.lean
+++ b/DatapathVerification/BitHeap/HashSetLemmas.lean
@@ -34,6 +34,15 @@ theorem Std.HashMap.nodup_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHas
   apply List.Pairwise.of_map _ _ this
   simp
 
+theorem Std.HashSet.nodup_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+  (m : Std.HashSet α) :
+    m.toList.Nodup := by
+  simp [toList, ← HashMap.map_fst_toList_eq_keys]
+  rw [List.nodup_iff_pairwise_ne]
+  apply List.Pairwise.map (fun (x : α × Unit) => x.1) (R := fun a b => a ≠ b)
+  · grind
+  · apply HashMap.nodup_toList
+
 theorem Std.HashMap.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
   (m : HashMap α β) :
     (m.erase d).toList.Perm (m.toList.filter (fun x => (x.1 == d) = false)) := by

From c9f48b3ef7154bb1d5494000bc6609caa163f309 Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 15:54:01 +0100
Subject: [PATCH 07/10] nit

---
 DatapathVerification/BitHeap/BitHeap.lean       |  1 -
 DatapathVerification/BitHeap/HashSetLemmas.lean | 14 --------------
 2 files changed, 15 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index bc82d31..90dc125 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -34,7 +34,6 @@ 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
-  -- h.columns.toList.zipIdx.foldl (fun acc (col, idx) => acc + 2^idx * col.eval env) 0
 
 /--
 Evaluate a bit-heap modulo 2^width, to compute the final sum of all the bits in the heap.
diff --git a/DatapathVerification/BitHeap/HashSetLemmas.lean b/DatapathVerification/BitHeap/HashSetLemmas.lean
index 79304fc..b8f90c9 100644
--- a/DatapathVerification/BitHeap/HashSetLemmas.lean
+++ b/DatapathVerification/BitHeap/HashSetLemmas.lean
@@ -43,20 +43,6 @@ theorem Std.HashSet.nodup_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHas
   · grind
   · apply HashMap.nodup_toList
 
-theorem Std.HashMap.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
-  (m : HashMap α β) :
-    (m.erase d).toList.Perm (m.toList.filter (fun x => (x.1 == d) = false)) := by
-  apply List.Perm.of_nodup_of_nodup_of_forall_mem_iff_mem
-  · apply HashMap.nodup_toList
-  · apply List.filter_nodup
-    apply HashMap.nodup_toList
-  · simp [HashMap.getKey?_erase, HashMap.getElem?_erase]
-    intro a b
-    by_cases h : d == a
-    · simp [h, BEq.symm h]
-    · simp at h
-      simp [h, BEq.symm_false h]
-
 theorem Std.HashSet.erase_toList_perm_filter_toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
   (m : Std.HashSet α) :
     (m.erase d).toList.Perm (m.toList.filter (fun x => (x == d) = false)) := by

From c9dae177dade9a6b42a970b0a4d4f1f4e05f5cbe Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 18:10:40 +0100
Subject: [PATCH 08/10] refactor

---
 DatapathVerification/BitHeap/BitHeap.lean | 44 +++++++++++++----------
 1 file changed, 25 insertions(+), 19 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 90dc125..b1d731d 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -55,9 +55,6 @@ instance : Membership Circuit (BitHeap w) where
   mem h c :=
     ∃ (col : Nat), c ∈ h.get col
 
-def removeBit (column : Nat) (c : Circuit) (h : BitHeap w) : BitHeap w :=
-  ⟨h.columns.setIfInBounds column ((h.get column).erase c)⟩
-
 -- Maximum height across all columns
 def maxHeight (h : BitHeap w) : Nat :=
   h.columns.foldl (fun acc col => max acc col.height) 0
@@ -69,6 +66,18 @@ def highestColumn (h : BitHeap w) : Option Nat :=
   h.columns.toList.zipIdx.findSome?
     (fun (col, idx) => if col.height == target then some idx else none)
 
+def setColumn (h : BitHeap w) (k : Nat) (v : Column) (hk :  k < w) : BitHeap w :=
+  { h with columns := h.columns.set k v}
+
+def setIfInBounds (h : BitHeap w) (k : Nat) (v : Column) : BitHeap w :=
+  { h with columns := h.columns.setIfInBounds k v}
+
+/-
+Remove a bit from the BitHeap if the index is in bounds, otherwise return the original BitHeap.
+-/
+def removeBit (column : Nat) (c : Circuit) (h : BitHeap w) : BitHeap w :=
+  h.setIfInBounds column ((h.get column).erase c)
+
 /--
 Add a bit into the bit heap, returning a new bit heap.
 If the bit already exists in the column, remove it and add it to the next column.
@@ -79,7 +88,7 @@ def addBit (column : Nat) (c : Circuit) (h : BitHeap w) : BitHeap w :=
   have h1 : column < w := by omega
   let col := h.get column
     if !col.contains c then
-      ⟨h.columns.set column (col.insert c) h1⟩
+      h.setColumn column (col.insert c) h1
       else addBit (column + 1) c (h.removeBit column c)
 
 structure AdderResult (w : Nat) where
@@ -125,33 +134,30 @@ theorem hornersMethod_set (env : BitEnv) (l : List Column) (k : Nat) (v : Column
 
 @[grind => ]
 theorem eval_insertColumn_eq_eval_add (h : BitHeap w) (k : Nat) (v : Column) (env : BitEnv) (h1 : k < w) :
-    ({ columns := h.columns.set k v h1 } : BitHeap w).eval env
+    (h.setColumn k v h1).eval env
       = h.eval env + 2 ^ k * (v.eval env : Int) - 2 ^ k * ((h.get k).eval env : Int) := by
-  simp only [BitHeap.eval, Vector.toList_set]
-  rw [hornersMethod_set env h.columns.toList k v (by simpa using h1)]
-  simp only [Vector.getElem_toList, Int.sub_right_inj]
-  rw [getD_in_bounds h k h1]
+  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn, hornersMethod_set env h.columns.toList k v (by simpa using h1), Vector.getElem_toList, getD_in_bounds h k h1]
 
 @[grind => ]
 theorem eval_eraseColumn_eq_eval_sub (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
-    ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env
+    (h.setColumn k (Column.empty) h1).eval env
       = h.eval env - 2 ^ k * ((h.get k).eval env : Int) := by
-  simp only [BitHeap.eval, Vector.toList_set]
+  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn]
   rw [hornersMethod_set env h.columns.toList k (Column.empty) (by simpa using h1)]
   simp only [empty_eval_zero, Int.cast_ofNat_Int, Int.mul_zero, Int.add_zero, Vector.getElem_toList,
     Int.sub_right_inj]
   rw [getD_in_bounds h k h1]
 
 theorem eval_insertColumn (h : BitHeap w) (k : Nat) (col : Column) (env : BitEnv) (h1 : k < w) :
-    ({ columns := h.columns.set k col h1 } : BitHeap w).eval env
-      = ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env + 2 ^ k * (col.eval env : Nat) := by
+    (h.setColumn k col h1).eval env
+      = (h.setColumn k (Column.empty) h1).eval env + 2 ^ k * (col.eval env : Nat) := by
   have := eval_insertColumn_eq_eval_add h k col env h1
   have := eval_eraseColumn_eq_eval_sub h k env h1
   grind only
 
 theorem eval_eraseColumn (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
     h.eval env
-      = ({ columns := h.columns.set k (Column.empty) h1} : BitHeap w).eval env + 2 ^ k * ((h.get k).eval env : Nat) := by
+      = (h.setColumn k (Column.empty) h1).eval env + 2 ^ k * ((h.get k).eval env : Nat) := by
   have := eval_eraseColumn_eq_eval_sub h k env h1
   grind only
 
@@ -169,8 +175,8 @@ theorem if_elem_not_empty (col : Nat) (c : Circuit) (h : BitHeap w) :
 theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env : BitEnv) (h1 : c ∈ h.get column) :
   (h.removeBit column c).evalMod env = (h.evalMod env - 2^(column) * (c.eval env).toInt) % 2^(w) := by
   simp [evalMod, removeBit]
-  have : ({ columns := h.columns.setIfInBounds column ((h.get column).erase c) : BitHeap w}.eval env) = (↑(h.eval env) - 2 ^ column * (c.eval env).toInt) := by
-    simp only [eval, Vector.toList_setIfInBounds]
+  have : ((h.setIfInBounds column ((h.get column).erase c))).eval env = (↑(h.eval env) - 2 ^ column * (c.eval env).toInt) := by
+    simp only [eval, Vector.toList_setIfInBounds, BitHeap.setIfInBounds]
     rw [hornersMethod_set]
     · rw [eval_erase]
       · rw [getD_in_bounds h column]
@@ -217,7 +223,7 @@ theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env :
     simp [Int.add_emod, h3]
   | case2 column h h4 h3 col h1 =>
     simp only [evalMod, Int.emod_add_emod]
-    have : ({ columns := h.columns.set column (col.insert c) h3 } : BitHeap w).eval env = (h.eval env + 2 ^ column * (c.eval env).toInt) := by
+    have : (h.setColumn column (col.insert c) h3).eval env = (h.eval env + 2 ^ column * (c.eval env).toInt) := by
       rw [eval_insertColumn]
       rw [eval_eraseColumn h column env h3]
       rw [Column.eval_insert]
@@ -237,7 +243,7 @@ theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env :
 
 theorem get_removeBit_self (column : Nat) (c : Circuit) (h : BitHeap w) (hb : column < w) :
     (removeBit column c h).get column = (h.get column).erase c := by
-  simp only [removeBit]
+  simp only [removeBit, BitHeap.setIfInBounds]
   rw [getD_in_bounds] <;> grind
 
 @[simp]
@@ -247,7 +253,7 @@ theorem get_removeBit_of_ne (column : Nat) (h : BitHeap w) (i j : Circuit)
   · rw [get_removeBit_self _ _ _ hb]
     exact (erase_eq_erase (h.get column) h1 (id (Ne.symm hne))).mpr h1
   · have hr : removeBit column j h = h := by
-      simp only [removeBit]
+      simp only [removeBit, BitHeap.setIfInBounds]
       rw [Vector.setIfInBounds_eq_of_size_le]
       grind
     rw [hr]

From 1d00fdf31386b1796e281ae0be16e5303f535018 Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 18:10:55 +0100
Subject: [PATCH 09/10] nit

---
 DatapathVerification/BitHeap/BitHeap.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index b1d731d..5524106 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -136,7 +136,10 @@ theorem hornersMethod_set (env : BitEnv) (l : List Column) (k : Nat) (v : Column
 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
       = h.eval env + 2 ^ k * (v.eval env : Int) - 2 ^ k * ((h.get k).eval env : Int) := by
-  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn, hornersMethod_set env h.columns.toList k v (by simpa using h1), Vector.getElem_toList, getD_in_bounds h k h1]
+  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn]
+  rw [hornersMethod_set env h.columns.toList k v (by simpa using h1)]
+  simp only [Vector.getElem_toList, Int.sub_right_inj]
+  rw [getD_in_bounds h k h1]
 
 @[grind => ]
 theorem eval_eraseColumn_eq_eval_sub (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :

From dff26c18518e20a0b931a932b32dee6b6434bf5d Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Fri, 26 Jun 2026 18:18:04 +0100
Subject: [PATCH 10/10] simplify proofs

---
 DatapathVerification/BitHeap/BitHeap.lean | 48 +++++++++--------------
 1 file changed, 18 insertions(+), 30 deletions(-)

diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 5524106..251ba5f 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -136,20 +136,18 @@ theorem hornersMethod_set (env : BitEnv) (l : List Column) (k : Nat) (v : Column
 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
       = h.eval env + 2 ^ k * (v.eval env : Int) - 2 ^ k * ((h.get k).eval env : Int) := by
-  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn]
-  rw [hornersMethod_set env h.columns.toList k v (by simpa using h1)]
-  simp only [Vector.getElem_toList, Int.sub_right_inj]
-  rw [getD_in_bounds h k h1]
+  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn,
+    hornersMethod_set env h.columns.toList k v (by simpa using h1),
+    Vector.getElem_toList, getD_in_bounds h k h1]
 
 @[grind => ]
 theorem eval_eraseColumn_eq_eval_sub (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
     (h.setColumn k (Column.empty) h1).eval env
       = h.eval env - 2 ^ k * ((h.get k).eval env : Int) := by
-  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn]
-  rw [hornersMethod_set env h.columns.toList k (Column.empty) (by simpa using h1)]
-  simp only [empty_eval_zero, Int.cast_ofNat_Int, Int.mul_zero, Int.add_zero, Vector.getElem_toList,
-    Int.sub_right_inj]
-  rw [getD_in_bounds h k h1]
+  simp only [BitHeap.eval, Vector.toList_set, BitHeap.setColumn,
+    hornersMethod_set env h.columns.toList k (Column.empty) (by simpa using h1),
+    empty_eval_zero, Int.cast_ofNat_Int, Int.mul_zero, Int.add_zero, Vector.getElem_toList,
+    getD_in_bounds h k h1]
 
 theorem eval_insertColumn (h : BitHeap w) (k : Nat) (col : Column) (env : BitEnv) (h1 : k < w) :
     (h.setColumn k col h1).eval env
@@ -164,7 +162,7 @@ theorem eval_eraseColumn (h : BitHeap w) (k : Nat) (env : BitEnv) (h1 : k < w) :
   have := eval_eraseColumn_eq_eval_sub h k env h1
   grind only
 
-theorem if_elem_not_empty (col : Nat) (c : Circuit) (h : BitHeap w) :
+theorem is_elem_in_bounds (col : Nat) (c : Circuit) (h : BitHeap w) :
    (c ∈ h.get col) → (col < w) := by
   intro h1
   by_contra hge
@@ -186,26 +184,23 @@ theorem evalMod_heap_removeBit (column : Nat) (c : Circuit) (h : BitHeap w) (env
         · rw [Int.add_sub_assoc]
           have hidx : ∀ (hb : column < w), h.columns[column] = h.columns.toList[column]'(by grind) := by
             simp [Vector.getElem_toList]
-          rw [hidx]
-          rw [Int.natCast_sub]
+          rw [hidx, Int.natCast_sub]
           · cases c.eval env <;> simp_all <;> grind
-          · simp [Column.eval]
-            rw [Std.HashSet.fold_eq_foldl_toList]
-            simp [Column.foldl_sum]
+          · simp [Column.eval, Std.HashSet.fold_eq_foldl_toList, Column.foldl_sum]
             apply List.single_le_sum
             · intro hx hy
               exact Nat.zero_le hx
             · simp
               use c
               constructor
-              · rw [getD_in_bounds h column (by exact if_elem_not_empty column c h h1)] at h1
-                simp [Column.mem_iff_contains, Column.contains] at h1
+              · rw [getD_in_bounds h column (by exact is_elem_in_bounds column c h h1),
+                    Column.mem_iff_contains, Column.contains] at h1
                 exact h1
               · rfl
-        · exact if_elem_not_empty column c h h1
+        · exact is_elem_in_bounds column c h h1
       · exact h1
     · simp
-      exact if_elem_not_empty column c h h1
+      exact is_elem_in_bounds column c h h1
   rw [this]
 
 @[simp]
@@ -218,8 +213,7 @@ theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env :
       generalize hvi : c.eval env = vi
       rcases vi
       · simp
-      · simp only [Bool.toInt_true]
-        rw [Int.mul_one]
+      · simp only [Bool.toInt_true, Int.mul_one]
         apply Int.emod_eq_zero_of_dvd
         have : (2:Nat)^w ∣ (2:Nat)^col := Nat.pow_dvd_pow 2 h1
         exact Int.natAbs_dvd_natAbs.mp this
@@ -227,22 +221,16 @@ theorem evalMod_heap_addBit (column : Nat) (c : Circuit) (h : BitHeap w) (env :
   | case2 column h h4 h3 col h1 =>
     simp only [evalMod, Int.emod_add_emod]
     have : (h.setColumn column (col.insert c) h3).eval env = (h.eval env + 2 ^ column * (c.eval env).toInt) := by
-      rw [eval_insertColumn]
-      rw [eval_eraseColumn h column env h3]
-      rw [Column.eval_insert]
+      rw [eval_insertColumn, eval_eraseColumn h column env h3, Column.eval_insert]
       · push_cast
         cases c.eval env <;> simp <;> grind
       · simp_all
     rw [this]
   | case3 col h h4 h3 h2 h1 ih =>
-    rw [ih]
-    rw [evalMod_heap_removeBit]
+    rw [ih, evalMod_heap_removeBit]
     have : (- 2 ^ col * (c.eval env).toInt + 2 ^ (col + 1) * (c.eval env).toInt) = 2 ^ col * (c.eval env).toInt := by grind
     rw [← this]
-    simp_all -- this looks very ugly
-    grind
-    simp_all
-    grind
+    all_goals (simp_all; grind)
 
 theorem get_removeBit_self (column : Nat) (c : Circuit) (h : BitHeap w) (hb : column < w) :
     (removeBit column c h).get column = (h.get column).erase c := by