example

Author: osmanyasar05

DatapathVerification/BitHeap/BitHeap.lean

@@ -15,6 +15,8 @@ namespace BitHeap
 open Circuit
 open Column
 
+def empty : BitHeap := ⟨Std.HashMap.emptyWithCapacity 0⟩
+
 /--
 Evaluate a bit-heap, to compute the final sum of all the bits in the heap.
 -/
@@ -34,8 +36,6 @@ def get (h : BitHeap) (i : Index) : Circuit :=
   | none => Circuit.const false
   | some col => (col.getD i.index (Circuit.const false))
 
-def empty : BitHeap := ⟨Std.HashMap.emptyWithCapacity 0⟩
-
 /--
 Add a bit into the bit heap, returning a new bit heap, and an index to the added bit.
 -/
@@ -47,14 +47,6 @@ def addBit (h : BitHeap) (c : Circuit) (w : Nat) : BitHeap × Index :=
 def removeBit (h : BitHeap) (i : Index) : BitHeap :=
   ⟨h.columns.modify i.column (fun col => ⟨col.elems.eraseIdx i.index⟩)⟩
 
-def addBitsExample : BitHeap :=
-  let h := BitHeap.empty
-  let (h, _) := h.addBit (Circuit.bit 0) 0 -- add a bit in column 0
-  let (h, _) := h.addBit (Circuit.bit 1) 1 -- add a bit in column 1
-  let (h, _) := h.addBit (Circuit.bit 1) 1 -- add another bit in column 1
-  let h := h.removeBit (Index.mk 0 0) -- remove the bit in column 0
-  h
-
 structure AdderResult where
   heap : BitHeap
   sumIndex : Index

DatapathVerification/BitHeap/Column.lean

@@ -17,7 +17,7 @@ def empty : Column := ⟨[]⟩
 
 def insert (col : Column) (c : Circuit): Column × Nat :=
   let newIndex := col.elems.length
-  let col := ⟨c :: col.elems⟩
+  let col := ⟨col.elems ++ [c]⟩
   (col, newIndex)
 
 def eval (col : Column) (env : BitEnv) : Nat :=