bitadd is equivalent to BitVector addition

Std.lean

@@ -25,6 +25,7 @@ import Std.Data.BinomialHeap.Basic
 import Std.Data.BinomialHeap.Lemmas
 import Std.Data.BitVec
 import Std.Data.BitVec.Basic
+import Std.Data.BitVec.Bitblast
 import Std.Data.Bool
 import Std.Data.Char
 import Std.Data.DList

Std/Data/BitVec/Bitblast.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Harun Khan, Abdalrhman M Mohamed
+-/
+import Std.Data.BitVec.Basic
+import Std.Data.Nat.Lemmas
+import Std.Data.Bool
+
+namespace Std
+open Nat Bool
+
+/-! ### Preliminaries -/
+
+theorem bodd_eq_bodd_iff {m n} : bodd n = bodd m ↔ n % 2 = m % 2 := by
+  cases hn : bodd n <;> cases hm : bodd m
+  <;> simp [mod_two_of_bodd, hn, hm]
+
+theorem testBit_two_pow_mul_add {n b w i} (h : i < w) :
+    Nat.testBit (2 ^ w * b + n) i = Nat.testBit n i := by
+  simp only [testBit, shiftRight_eq_div_pow, bodd_eq_bodd_iff]
+  rw [← Nat.add_sub_of_le (succ_le_of_lt h), Nat.succ_eq_add_one, Nat.add_assoc]
+  rw [Nat.pow_add, Nat.add_comm, Nat.mul_assoc, add_mul_div_left _ _ (two_pow_pos _), add_mod]
+  rw [Nat.pow_add, Nat.pow_one, Nat.mul_assoc]
+  simp
+
+theorem testBit_two_pow_mul_toNat_add {n w b} (h : n < 2 ^ w) :
+    testBit (2 ^ w * (bit b 0) + n) w = b := by
+  simp only [testBit, shiftRight_eq_div_pow]
+  rw [Nat.add_comm, add_mul_div_left _ _ (two_pow_pos _), Nat.div_eq_of_lt h, Nat.zero_add]
+  cases b <;> simp
+
+@[simp] theorem toNat_eq_bif {b: Bool} : cond b 1 0 = toNat b := by simp [cond, toNat]
+
+theorem shiftRight_eq_testBit (x i : Nat) : (x >>> i) % 2 = toNat (testBit x i) := by
+  simp [Nat.testBit, Nat.mod_two_of_bodd, toNat_eq_bif]
+
+theorem div_add_mod_two_pow (m n : Nat) : n = 2 ^ m * n >>> m + n % (2 ^ m):= by
+  simp [shiftRight_eq_div_pow, Nat.div_add_mod]
+
+theorem mod_two_pow_succ (x i : Nat) :
+  x % 2 ^ (i + 1) = 2 ^ i * toNat (Nat.testBit x i) + x % (2 ^ i):= by
+  have h1 := div_add_mod_two_pow i x
+  rw [←div_add_mod (x >>> i) 2, Nat.mul_add, ←Nat.mul_assoc, ←pow_succ, shiftRight_eq_testBit] at h1
+  have h2 := Eq.trans (div_add_mod_two_pow (i + 1) x).symm h1
+  rw [shiftRight_succ, succ_eq_add_one, Nat.add_assoc] at h2
+  exact Nat.add_left_cancel h2
+
+/-- Generic method to create a natural number by appending bits tail-recursively.
+It takes a boolean function `f` on each bit the number of bits `i`.  It is
+almost always specialized  `i = w`; the length of the binary representation.
+This is an alternative to using `List` and is used to define bitadd, bitneg, bitmul etc.-/
+def ofBits (f : Nat → Bool) (z : Nat) : Nat → Nat
+  | 0 => z
+  | i + 1 => ofBits f (z.bit (f i)) i
+
+theorem ofBits_succ {f : Nat → Bool} {i z : Nat} : ofBits f z i = 2 ^ i * z + ofBits f 0 i:= by
+  revert z
+  induction i with
+  | zero => simp [ofBits, bit_val]
+  | succ i ih =>  intro z; simp only [ofBits, @ih (bit (f i) 0), @ih (bit (f i) z)]
+                  rw [bit_val, Nat.mul_add, ← Nat.mul_assoc, ← pow_succ]
+                  simp [bit_val, Nat.add_assoc]
+
+theorem ofBits_lt {f : Nat → Bool} : ofBits f 0 i < 2^i := by
+  induction i with
+  | zero => simp [ofBits, bit_val, lt_succ]
+  | succ i ih =>  simp only [ofBits]
+                  rw [ofBits_succ, two_pow_succ]
+                  cases (f i)
+                  · exact add_lt_add (by simp [bit_val, two_pow_pos i]) ih
+                  · simp only [bit_val, Nat.mul_zero, cond_true, Nat.zero_add, Nat.mul_one]
+                    exact Nat.add_lt_add_left ih _
+
+theorem ofBits_testBit {f : Nat → Bool} (h1: i < j) : (ofBits f 0 j).testBit i = f i := by
+  cases j with
+  | zero => simp [not_lt_zero] at h1
+  | succ j =>
+    revert i
+    induction j with
+    | zero => simp [lt_succ, ofBits, bit_val]
+              cases (f 0) <;> trivial
+    | succ j ih =>
+      intro i hi
+      rw [lt_succ] at hi
+      cases Nat.lt_or_eq_of_le hi with
+      | inl h1 => rw [← ih h1, ofBits, ofBits_succ, testBit_two_pow_mul_add h1]
+      | inr h1 => rw [h1, ofBits, ofBits_succ, testBit_two_pow_mul_toNat_add (ofBits_lt)]
+
+/-! ### Addition -/
+
+/-- Carry function for bitwise addition. -/
+def bitwise_carry (x y : Nat) : Nat → Bool
+  | 0     => false
+  | i + 1 => (x.testBit i && y.testBit i) || ((x.testBit i ^^ y.testBit i) && bitwise_carry x y i)
+
+/-- Bitwise addition implemented via a ripple carry adder. -/
+@[simp] def bitwise_add (x y i : Nat) :=
+  ofBits (λ j => (x.testBit j ^^ y.testBit j) ^^ bitwise_carry x y j) 0 i
+
+theorem bitwise_add_eq_add_base (x y i : Nat) :
+  x % (2 ^ i) + y % (2 ^ i) = bitwise_add x y i + 2 ^ i * toNat (bitwise_carry x y i) := by
+  induction i with
+  | zero => simp [mod_one, ofBits, bitwise_carry]
+  | succ i hi => rw [mod_two_pow_succ x, mod_two_pow_succ y]
+                 rw [Nat.add_assoc, Nat.add_comm _ (y % 2 ^ i), ← Nat.add_assoc (x % 2 ^ i)]
+                 rw [hi, bitwise_carry, two_pow_succ i]
+                 cases hx : Nat.testBit x i <;> cases hy : Nat.testBit y i
+                 <;> cases hc : bitwise_carry x y i
+                 <;> simp [bit_val, toNat, @ofBits_succ _ i 1, two_pow_succ, hx, hy, hc,
+                           ofBits, Nat.add_comm, Nat.add_assoc]
+
+theorem bitwise_add_eq_add (x y : Nat) : bitwise_add x y i = (x + y) % 2 ^ i := by
+  rw [Nat.add_mod, bitwise_add_eq_add_base]
+  cases i
+  · simp [mod_one, ofBits]
+  · simp [bitwise_add, Nat.mod_eq_of_lt ofBits_lt]
+
+theorem BV_add {x y : BitVec w} : bitwise_add (x.toNat) y.toNat w = (x + y).toNat := by
+  rw [bitwise_add_eq_add]
+  rfl

Std/Data/Bool.lean

@@ -95,6 +95,9 @@ theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y
 
 /-! ### xor -/
 
+/-- Infix notation for xor -/
+infix:30 " ^^ " => xor
+
 @[simp] theorem false_xor : ∀ (x : Bool), xor false x = x := by decide
 
 @[simp] theorem xor_false : ∀ (x : Bool), xor x false = x := by decide
@@ -189,3 +192,7 @@ theorem and_or_inj_left : ∀ {m x y : Bool}, (m && x) = (m && y) → (m || x) =
 theorem and_or_inj_left_iff :
     ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y := by decide
 @[deprecated] alias and_or_inj_left' := and_or_inj_left_iff
+
+/-- convert a `bool` to a `ℕ`, `false -> 0`, `true -> 1` -/
+def toNat (b : Bool) : Nat :=
+  cond b 1 0

Std/Data/Nat/Basic.lean

@@ -126,3 +126,92 @@ where
     else
       guess
 termination_by iter guess => guess
+
+/-- `bodd n` returns `true` if `n` is odd-/
+def bodd (n : Nat) : Bool :=
+  (1 &&& n) != 0
+
+/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
+def div2 (n : Nat) : Nat :=
+  n >>> 1
+
+/-- `bit b` appends the digit `b` to the binary representation of
+  its natural number input. -/
+def bit (b : Bool) (n : Nat) : Nat :=
+  cond b (n + n + 1) (n + n)
+
+/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
+def testBit (m n : Nat) : Bool :=
+  bodd (m >>> n)
+
+theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
+  cases b <;> rw [Nat.mul_comm]
+  · exact congrArg (· + n) n.zero_add.symm
+  · exact congrArg (· + n + 1) n.zero_add.symm
+
+theorem div2_val (n) : div2 n = n / 2 := rfl
+
+theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
+  match n % 2, @Nat.mod_lt n 2 (by simp) with
+  | 0, _ => .inl rfl
+  | 1, _ => .inr rfl
+
+theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
+  dsimp [bodd, (· &&& ·), AndOp.and, land]
+  unfold bitwise
+  by_cases n0 : n = 0
+  · simp [n0]
+  · simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
+      show 1 / 2 = 0 by decide]
+    cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
+
+theorem bodd_add_div2 (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
+  rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
+
+theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
+  (bit_val _ _).trans (bodd_add_div2 _)
+
+theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
+  cases n <;> cases b <;> simp [bit, Nat.succ_add]
+
+/-- For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for any given natural number. -/
+@[inline]
+def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
+
+theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n :=
+  div_lt_self (n.zero_lt_of_ne_zero h) (by decide)
+
+/-- A recursion principle for `bit` representations of natural numbers.
+  For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[specialize]
+def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) (n : Nat) : C n :=
+  if n0 : n = 0 then by rw [n0]; exact z
+  else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)
+  decreasing_by exact binaryRec_decreasing n0
+
+/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`-/
+@[elab_as_elim, specialize]
+def binaryRec' {C : Nat → Sort u} (z : C 0)
+    (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec z fun b n ih =>
+    if h : n = 0 → b = true then f b n h ih
+    else by
+      have : bit b n = 0 := by
+        rw [bit_eq_zero_iff]
+        cases n <;> cases b <;> simp at h <;> simp [h]
+      exact this ▸ z
+
+/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
+@[elab_as_elim, specialize]
+def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
+    (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec' z₀ fun b n h ih =>
+    if h' : n = 0 then by
+      rw [h', h h']
+      exact z₁
+    else f b n h' ih