Boolean comparison and compare-exchange circuits

The comparator reads key coordinates in selector order, with coordinate zero most significant. Its formula has 6 * k + 1 gates for k selected input bits. Compare-exchange computes the comparison once, retains it and its negation, and selects whole records using three gates per output bit. Ties preserve the input order, including payload bits outside the key.

For two nonempty records of width r, the circuit uses exactly 6 * k + 6 * r + 2 gates, including constants and negations. Empty records use no gates. Key positions may be arbitrary; the usual prefix key is Fin.castLE h for h : k ≤ r.

Main definitions

• Cslib.Circuits.Formula.lexLt: compare two selected input sequences lexicographically.
• Cslib.Circuits.Boolean.compareSwapCircuit: order two records by selected key coordinates.
• Cslib.Circuits.Boolean.compareSwapCircuit.record: expose a shared swap flag and its complement.
• Cslib.Circuits.Boolean.compareSwapCircuit.switch: exchange payloads using saved controls.

Main results

• Cslib.Circuits.Formula.eval_lexLt_iff: agreement with Mathlib's lexicographic order.
• Cslib.Circuits.Boolean.eval_compareSwapCircuit: swap whole records exactly when out of order.
• Cslib.Circuits.Boolean.size_compareSwapCircuit: exact total gate count.
• Cslib.Circuits.Boolean.compareSwapCircuit_keys_ordered: the output keys are in ascending order.
• Cslib.Circuits.Boolean.compareSwapCircuit.cost_record_eq_exchange: exposing controls adds no gates to exchange, which computes its flag even at zero payload width.

References

• Adapts the comparator endpoint of MassProduction/Sorting.lean in S. Schlesinger, Boolean circuit mass production formalization, using a linear-size comparison and sharing its result between outputs.

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

Compare two selected input sequences, with coordinate zero most significant.

@[simp]

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

Lexicographic comparison of selected input leaves uses six gates per coordinate and one constant gate. Repeated or overlapping selections are allowed.

@[simp]

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

The comparison formula agrees with the lexicographic order, including empty keys.

def Cslib.Circuits.Boolean.compareSwapCircuit {k r : ℕ} (key : Fin k → Fin r) : Circuit signature (r + r) (r + r)

Compare two records by key, preserving their order when the keys agree. The comparison and its negation are shared across all output bits. Empty records use the identity wiring.

def Cslib.Circuits.Boolean.compareSwapCircuit.flagPair : Circuit signature 1 2

Retain a flag and compute its negation once.

def Cslib.Circuits.Boolean.compareSwapCircuit.selectBit {n : ℕ} (left right : Fin n) : Formula signature (2 + n)

Select one of two data wires using a stored flag and its stored negation.

def Cslib.Circuits.Boolean.compareSwapCircuit.swapInput (r : ℕ) : Fin (r + r) → Fin (r + r)

Swap the two blocks of record wires.

def Cslib.Circuits.Boolean.compareSwapCircuit.switch (r : ℕ) : Circuit signature (2 + (r + r)) (r + r)

Switch two payload blocks using a supplied flag and its supplied complement.

def Cslib.Circuits.Boolean.compareSwapCircuit.record {r : ℕ} (flag : Circuit signature (r + r) 1) : Circuit signature (r + r) (2 + (r + r))

Expose the shared flag and its complement before the exchanged records.

def Cslib.Circuits.Boolean.compareSwapCircuit.exchange {r : ℕ} (flag : Circuit signature (r + r) 1) : Circuit signature (r + r) (r + r)

Share a swap flag across every bit of the two records.

theorem Cslib.Circuits.Boolean.compareSwapCircuit.eval_switch (r : ℕ) (b : Bool) (x y : BitString r) : (switch r).eval interpretation (Fin.append ![b, !b] (Fin.append x y)) = if b = true then Fin.append y x else Fin.append x y

The control bits are supplied together: invalid pairs are not asserted to be swaps.

theorem Cslib.Circuits.Boolean.compareSwapCircuit.eval_record {r : ℕ} (flag : Circuit signature (r + r) 1) (x y : BitString r) : (record flag).eval interpretation (Fin.append x y) = have b := flag.eval interpretation (Fin.append x y) 0; Fin.append ![b, !b] (if b = true then Fin.append y x else Fin.append x y)

Recording returns both existing control wires without duplicating their computation.

theorem Cslib.Circuits.Boolean.compareSwapCircuit.switch_involutive (r : ℕ) (b : Bool) (x y : BitString r) : (switch r).eval interpretation (Fin.append ![b, !b] ((switch r).eval interpretation (Fin.append ![b, !b] (Fin.append x y)))) = Fin.append x y

Applying the same saved controls twice restores arbitrary payloads.

theorem Cslib.Circuits.Boolean.compareSwapCircuit.cost_switch (r : ℕ) (cost : signature.Op → ℕ) : (switch r).program.cost cost = 2 * r * (2 * cost Op.and + cost Op.or)

Switching charges two ANDs and one OR for each output bit.

theorem Cslib.Circuits.Boolean.compareSwapCircuit.cost_record {r : ℕ} (flag : Circuit signature (r + r) 1) (cost : signature.Op → ℕ) : (record flag).program.cost cost = flag.program.cost cost + cost Op.not + 2 * r * (2 * cost Op.and + cost Op.or)

The comparator and one shared negation are charged in addition to switching.

theorem Cslib.Circuits.Boolean.compareSwapCircuit.cost_record_eq_exchange {r : ℕ} (flag : Circuit signature (r + r) 1) (cost : signature.Op → ℕ) : (record flag).program.cost cost = (exchange flag).program.cost cost

Exposing the controls adds no gates to exchange. Unlike compareSwapCircuit, exchange and record compute the flag even when the payload width is zero.

theorem Cslib.Circuits.Boolean.eval_compareSwapCircuit {k r : ℕ} (key : Fin k → Fin r) (x y : BitString r) : (compareSwapCircuit key).eval interpretation (Fin.append x y) = if toLex (y ∘ key) < toLex (x ∘ key) then Fin.append y x else Fin.append x y

Compare-exchange swaps whole records precisely when the right key precedes the left key.

@[simp]

theorem Cslib.Circuits.Boolean.size_compareSwapCircuit {k r : ℕ} (key : Fin k → Fin r) : (compareSwapCircuit key).size = if r = 0 then 0 else 6 * k + 6 * r + 2

Exact gate count, including the constant and the shared negation.

theorem Cslib.Circuits.Boolean.compareSwapCircuit_keys_ordered {k r : ℕ} (key : Fin k → Fin r) (x y : BitString r) : have output := (compareSwapCircuit key).eval interpretation (Fin.append x y); (toLex fun (i : Fin k) => output (Fin.castAdd r (key i))) ≤ toLex fun (i : Fin k) => output (Fin.natAdd r (key i))

The selected keys of the two output records are in ascending order.

theorem Cslib.Circuits.Boolean.eval_compareSwapCircuit_of_key_eq {k r : ℕ} (key : Fin k → Fin r) (x y : BitString r) (h : x ∘ key = y ∘ key) : (compareSwapCircuit key).eval interpretation (Fin.append x y) = Fin.append x y

Equal keys preserve the entire pair, including payload coordinates outside the key.