Equality of selected Boolean inputs

The formula compares two sequences of selected inputs. Selectors may overlap or repeat; empty sequences compare equal. An XNOR for each coordinate is conjoined with the remainder, using six gates per coordinate and a single true constant.

Main definitions

• Cslib.Circuits.Formula.equalBits: equality of two selected input sequences.
• Cslib.Circuits.Boolean.adjacentEqualityCircuit: shared tests for consecutive selected keys.

Main results

• Cslib.Circuits.Formula.eval_equalBits_iff: equality of the selected functions.
• Cslib.Circuits.Formula.cost_equalBits: exact arbitrary weighted cost.
• Cslib.Circuits.Formula.size_equalBits: exact gate count, including the constant.
• Cslib.Circuits.Boolean.eval_adjacentEqualityCircuit_iff: exact incoming-link semantics.
• Cslib.Circuits.Boolean.cost_program_adjacentEqualityCircuit: weighted adjacent-test cost.

References

• Adapts the equality formulas in MassProduction/Routing.lean from S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Formula.equalBits {n k : ℕ} : (Fin k → Fin n) → (Fin k → Fin n) → Formula Boolean.signature n

Test equality of two selected input sequences, including empty and repeated selections.

@[simp]

theorem Cslib.Circuits.Formula.eval_equalBits_iff {n k : ℕ} (left right : Fin k → Fin n) (x : BitString n) : (equalBits left right).eval Boolean.interpretation x = true ↔ x ∘ left = x ∘ right

Selected-bit equality is equality of the two selected functions.

theorem Cslib.Circuits.Formula.cost_equalBits {n k : ℕ} (left right : Fin k → Fin n) (cost : Boolean.signature.Op → ℕ) : Formula.cost cost (equalBits left right) = cost (Boolean.Op.const true) + k * (3 * cost Boolean.Op.and + 2 * cost Boolean.Op.not + cost Boolean.Op.or)

Each coordinate uses three AND gates, two negations and one OR, after one true constant.

@[simp]

theorem Cslib.Circuits.Formula.size_equalBits {n k : ℕ} (left right : Fin k → Fin n) : (equalBits left right).size = 6 * k + 1

The formula has six gates per selected coordinate and one constant gate.

def Cslib.Circuits.Boolean.adjacentEqualityCircuit {input count keyWidth : ℕ} (key : Fin count → Fin keyWidth → Fin input) : Circuit signature input count

Compare each selected key with its predecessor; the first key has no incoming link.

theorem Cslib.Circuits.Boolean.eval_adjacentEqualityCircuit_iff {input count keyWidth : ℕ} (key : Fin count → Fin keyWidth → Fin input) (x : BitString input) (record : Fin count) : (adjacentEqualityCircuit key).eval interpretation x record = true ↔ ∃ (positive : 0 < ↑record), x ∘ key ⟨↑record - 1, ⋯⟩ = x ∘ key record

An incoming link is true precisely when the predecessor exists and has the same key.

theorem Cslib.Circuits.Boolean.cost_program_adjacentEqualityCircuit {input count keyWidth : ℕ} (key : Fin count → Fin keyWidth → Fin input) (cost : signature.Op → ℕ) : (adjacentEqualityCircuit key).program.cost cost = if count = 0 then 0 else cost (Op.const false) + (count - 1) * (cost (Op.const true) + keyWidth * (3 * cost Op.and + 2 * cost Op.not + cost Op.or))

Adjacent comparisons are computed once, with one false constant for the missing first link.