diff --git a/DatapathVerification/BitHeap/BVComb.lean b/DatapathVerification/BitHeap/BVComb.lean
new file mode 100644
index 0000000..498fd6a
--- /dev/null
+++ b/DatapathVerification/BitHeap/BVComb.lean
@@ -0,0 +1,217 @@
+import DatapathVerification.BitHeap.BitHeap
+import DatapathVerification.BitHeap.Circuit
+import DatapathVerification.BitHeap.Compressors.DaddaTree
+import DatapathVerification.BitHeap.Compressors.NaiveCompression
+
+
+open BitHeap
+namespace Comb
+
+inductive ArithBinopKind
+| add
+| mul
+
+-- inductive ArithUnopKind
+-- | neg
+
+-- inductive BooleanBinopKind
+-- | and | or | xor
+
+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)
+
+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.
+-/
+def BitHeap.toSingleRow (bh : BitHeap w) : CircuitVector :=
+    let (pp1, _) := NaiveCompression.naiveCompression bh
+    pp1.columns.toArray.map fun col => col.elems.toList.headD (.const false)
+
+namespace ArithCircuit
+
+/--
+Given a bitvector (x : BV 3), build a bitheap
+```
+*   *  *
+x2 x1 x0
+```
+-/
+def bitheapOfVar (varIndex : Nat) : BitHeap w :=
+  -- | 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)
+
+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 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
+  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 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
+  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 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
+
+end Comb
diff --git a/DatapathVerification/BitHeap/BitHeap.lean b/DatapathVerification/BitHeap/BitHeap.lean
index 251ba5f..2f079bb 100644
--- a/DatapathVerification/BitHeap/BitHeap.lean
+++ b/DatapathVerification/BitHeap/BitHeap.lean
@@ -29,18 +29,49 @@ 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.
 -/
 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.
 -/
 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)
 
@@ -91,6 +122,30 @@ 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)
 
+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 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)
+  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
+
 structure AdderResult (w : Nat) where
   heap : BitHeap w
   sum : Circuit
@@ -115,23 +170,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/Circuit.lean b/DatapathVerification/BitHeap/Circuit.lean
index c34c06d..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 :=
@@ -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/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
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/Examples.lean b/DatapathVerification/BitHeap/Examples/Examples.lean
index 4702bae..f5146e6 100644
--- a/DatapathVerification/BitHeap/Examples/Examples.lean
+++ b/DatapathVerification/BitHeap/Examples/Examples.lean
@@ -99,6 +99,49 @@ info: 6
 #eval (applyChain compressionChain fourBitsInCol1).eval
         (show BitEnv from fun n => n = 1 || n = 2 || n = 3)
 
+----------------------------
+
+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 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 ↦ [b4, b8, b0], 1 ↦ [b1, b5, b9], 2 ↦ [b2, b10, b6], 3 ↦ [b3, b11, b7]}
+-/
+#guard_msgs in
+#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)]}
+-/
+#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
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