Word arithmetic over the De Morgan basis

Words are Lean's BitVecs, stored least significant bit first. A word-valued function of the inputs is available when each of its coordinate functions is (Boolean.wordWires). This module bounds the gates needed to make words available from available words: addition, subtraction, unsigned comparison, comparison with a constant, complementation, constants, multiplexing, and selection of one of several words by a binary index. Equality of available bit strings is Formula.equalBits inserted by Synthesis.circuit. Their semantics are the BitVec operations, through the bit-blasting identities of the core library; no decision procedure or native evaluation is used.

Addition is a ripple-carry adder: every carry is computed once and shared by the sum bits, for 12 * w + 1 gates on w-bit words including the initial carry constant. All bounds charge every gate, including constants and negations.

Main definitions

• Cslib.Circuits.Boolean.word: the word with given bits.
• Cslib.Circuits.Boolean.wordWires: the coordinate functions of a word-valued function.
• Cslib.Circuits.Boolean.selectBits: select one of several bit strings by a binary index.

Main results

• Cslib.Circuits.Synthesis.mux: a multiplexer in four gates.
• Cslib.Circuits.Synthesis.word_add, word_addCarry, word_sub: ripple-carry arithmetic.
• Cslib.Circuits.Synthesis.word_ult, word_eq_const: comparisons.
• Cslib.Circuits.Synthesis.word_not, word_const, word_mux: bitwise operations.
• Cslib.Circuits.Synthesis.selectBits: selection charging one comparison per record and bit.

References

• Adapted from lean/Proofs/{Synthesis,Arithmetic,Words}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions, where each sum bit recomputes its carry chain.

def Cslib.Circuits.Boolean.word {w : ℕ} (bits : BitString w) : BitVec w

The word with the given bits, least significant first.

theorem Cslib.Circuits.Boolean.getLsbD_word {w : ℕ} (bits : BitString w) (i : Fin w) : (word bits).getLsbD ↑i = bits i

@[simp]

theorem Cslib.Circuits.Boolean.getElem_word {w : ℕ} (bits : BitString w) (i : ℕ) (hi : i < w) : (word bits)[i] = bits ⟨i, hi⟩

theorem Cslib.Circuits.Boolean.word_getLsbD {w : ℕ} (a : BitVec w) : (word fun (i : Fin w) => a.getLsbD ↑i) = a

theorem Cslib.Circuits.Boolean.toNat_word_eq_equivFin {w : ℕ} (x : BitString w) : (word x).toNat = ↑((BitString.equivFin w) x)

The word representation and the bit-string numbering use the same unsigned value.

def Cslib.Circuits.Boolean.wordWires {n w : ℕ} (a : BitString n → BitVec w) : Set (BooleanFunction n)

The coordinate functions of a word-valued function.

theorem Cslib.Circuits.Boolean.wordWires_setWidth_subset {n w v : ℕ} {s : Set (BooleanFunction n)} {value : BitString n → BitVec w} (hv : wordWires value ⊆ s) (hz : (fun (x : BitString n) => false) ∈ s) : (wordWires fun (x : BitString n) => BitVec.setWidth v (value x)) ⊆ s

Zero extension and truncation only rewire available bits and the false constant.

def Cslib.Circuits.Boolean.selectBits {k w R : ℕ} (index : BitVec k) (values : Fin R → BitString w) : BitString w

The bit string at the position given by the value of a binary index, or all-false if the value is not a position. Positions beyond 2 ^ k are never selected.

theorem Cslib.Circuits.Boolean.selectBits_of_toNat_lt {k w R : ℕ} (index : BitVec k) (values : Fin R → BitString w) (hi : index.toNat < R) : selectBits index values = values ⟨index.toNat, hi⟩

An index whose value is a position selects exactly that bit string.

theorem Cslib.Circuits.Boolean.selectBits_of_le_toNat {k w R : ℕ} (index : BitVec k) (values : Fin R → BitString w) (hi : R ≤ index.toNat) : selectBits index values = fun (x : Fin w) => false

An index whose value is not a position selects all-false.

theorem Cslib.Circuits.Boolean.selectBits_ofNat {k w R : ℕ} (hR : R ≤ 2 ^ k) (values : Fin R → BitString w) (j : Fin R) : selectBits (BitVec.ofNat k ↑j) values = values j

An in-range position written as an index selects exactly its bit string.

theorem Cslib.Circuits.Synthesis.mux {n : ℕ} {s : Set (BooleanFunction n)} {f a b : BooleanFunction n} (hf : f ∈ s) (ha : a ∈ s) (hb : b ∈ s) : Synthesis Boolean.interpretation s {fun (x : BitString n) => if f x = true then a x else b x} 4

One available control bit selects between two available functions in four gates.

theorem Cslib.Circuits.Synthesis.word_carry {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) (c : Bool) {t : ℕ} (ht : t ≤ w) : Synthesis Boolean.interpretation s {fun (x : BitString n) => BitVec.carry t (a x) (b x) c} (4 * t + 1)

One carry chain uses four gates per bit and its initial constant.

theorem Cslib.Circuits.Synthesis.word_carries {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) (c : Bool) : Synthesis Boolean.interpretation s (stages (fun (t : ℕ) => {fun (x : BitString n) => BitVec.carry t (a x) (b x) c}) w) (4 * w + 1)

All carries of a sum, each computed once from the previous one.

theorem Cslib.Circuits.Synthesis.word_addCarry {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) (c : Bool) : Synthesis Boolean.interpretation s (Boolean.wordWires fun (x : BitString n) => a x + b x + BitVec.setWidth w (BitVec.ofBool c)) (12 * w + 1)

Ripple-carry addition with an initial carry: four gates per carry, eight per sum bit and the initial constant.

theorem Cslib.Circuits.Synthesis.word_add {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) : Synthesis Boolean.interpretation s (Boolean.wordWires fun (x : BitString n) => a x + b x) (12 * w + 1)

Ripple-carry addition modulo the word width.

theorem Cslib.Circuits.Synthesis.word_const {n w : ℕ} {s : Set (BooleanFunction n)} (v : BitVec w) : Synthesis Boolean.interpretation s (Boolean.wordWires fun (x : BitString n) => v) w

A hardwired word uses one constant gate per bit.

theorem Cslib.Circuits.Synthesis.word_not {n w : ℕ} {s : Set (BooleanFunction n)} (b : BitString n → BitVec w) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) : Synthesis Boolean.interpretation s (Boolean.wordWires fun (x : BitString n) => ~~~b x) w

Bitwise complementation uses one gate per bit.

theorem Cslib.Circuits.Synthesis.word_ult {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) : Synthesis Boolean.interpretation s {fun (x : BitString n) => (a x).ult (b x)} (5 * w + 2)

Unsigned comparison, by the carry of a + ~~~b + 1.

theorem Cslib.Circuits.Synthesis.word_sub {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) : Synthesis Boolean.interpretation s (Boolean.wordWires fun (x : BitString n) => a x - b x) (13 * w + 1)

Subtraction modulo the word width, as a + ~~~b + 1.

theorem Cslib.Circuits.Synthesis.word_mux {n w : ℕ} {s : Set (BooleanFunction n)} (a b : BitString n → BitVec w) (flag : BooleanFunction n) (hf : flag ∈ s) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) : Synthesis Boolean.interpretation s (Boolean.wordWires fun (x : BitString n) => if flag x = true then a x else b x) (4 * w)

A word multiplexer shares one available control bit, four gates per bit.

theorem Cslib.Circuits.Synthesis.word_eq_const {n k : ℕ} {s : Set (BooleanFunction n)} (a : BitString n → BitVec k) (ha : ∀ (i : Fin k), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (v : BitVec k) : Synthesis Boolean.interpretation s {fun (x : BitString n) => decide (a x = v)} (2 * k + 1)

Testing a word against a constant needs one literal per bit and a conjunction.

theorem Cslib.Circuits.Synthesis.selectBits {n k w R : ℕ} {s : Set (BooleanFunction n)} (index : BitString n → BitVec k) (values : Fin R → BitString n → BitString w) (hi : ∀ (i : Fin k), (fun (x : BitString n) => (index x).getLsbD ↑i) ∈ s) (hv : ∀ (j : Fin R) (bit : Fin w), (fun (x : BitString n) => values j x bit) ∈ s) : Synthesis Boolean.interpretation s (Set.range fun (bit : Fin w) (x : Fin n → Bool) => Boolean.selectBits (index x) (fun (j : Fin R) => values j x) bit) (w * (R * (2 * k + 3) + 1))

Selecting among available bit strings by an available index charges one comparison with each position for every output bit.