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 1/3] 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 2/3] 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 3/3] 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