chaining of adders

Author: osmanyasar05

DatapathVerification/BitHeap/BitHeap.lean

@@ -112,4 +112,43 @@ theorem fullAdder_correct (column : Nat) (i j k : Circuit) (h : BitHeap)
   generalize hvk : k.eval env = vk
   rcases vi <;> rcases vj <;> rcases vk <;> grind
 
+inductive Adder where
+| halfAdder (column : Nat) (a b : Circuit)
+| fullAdder (column : Nat) (a b c : Circuit)
+
+def applyAdder (adder : Adder) (h : BitHeap) : BitHeap :=
+  match adder with
+  | .halfAdder column i j => (h.halfAdder column i j).heap
+  | .fullAdder column i j k => (h.fullAdder column i j k).heap
+
+theorem applyAdder_halfAdder_correct (column : Nat) (i j : Circuit) (h : BitHeap)
+    (h1 : i ∈ h.get column) (h2 : j ∈ h.get column) (hne : i ≠ j) :
+    ∀ (env : BitEnv), (applyAdder (.halfAdder column i j) h).eval env = h.eval env := by
+    intros env
+    simp [applyAdder]
+    exact halfAdder_correct column i j h h1 h2 hne env
+
+theorem applyAdder_fullAdder_correct (column : Nat) (i j k : Circuit) (h : BitHeap)
+    (h1 : i ∈ h.get column) (h2 : j ∈ h.get column) (h3 : k ∈ h.get column) (hne : i ≠ j) (hne2 : i ≠ k) (hne3 : j ≠ k) :
+    ∀ (env : BitEnv), (applyAdder (.fullAdder column i j k) h).eval env = h.eval env := by
+    intros env
+    simp [applyAdder]
+    exact fullAdder_correct column i j k h h1 h2 h3 hne hne2 hne3 env
+
+def applyChain (adders : List Adder) (h : BitHeap) : BitHeap :=
+  match adders with
+  | [] => h
+  | s :: rest => applyChain rest (applyAdder s h)
+
+theorem applyChain_correct (steps : List Adder) (h : BitHeap) (env : BitEnv) :
+    (applyChain steps h).eval env = h.eval env := by
+  induction steps generalizing h with
+  | nil => rfl
+  | cons s rest ih =>
+    simp [applyChain]
+    rw [ih]
+    cases s with
+    | halfAdder => sorry
+    | fullAdder => sorry
+
 end BitHeap