Gate counts for sorting and detecting records

A family of records is available when every bit of every encoded record is (Record.wireSet). Sorting an available array inserts one Batcher circuit (Record.synthesis_sorted); its native gate count is at most 18 * d ^ 2 * 2 ^ d per record bit and comparison layer. Testing every adjacent pair for a collision and selecting one costs linearly in the array (Record.synthesis_detect).

Main definitions

• Cslib.Circuits.Boolean.Iteration.wires: the coordinate functions of a family of bit strings.
• Cslib.Circuits.Boolean.Iteration.Record.wireSet, Cslib.Circuits.Boolean.Iteration.Record.pairEncode, Cslib.Circuits.Boolean.Iteration.Record.pairWires, Cslib.Circuits.Boolean.Iteration.Record.recordsWires: available records, record pairs, and record arrays.

Main results

• Cslib.Circuits.Boolean.Iteration.Record.size_sortCircuit_le: the native sorter's size.
• Cslib.Circuits.Boolean.Iteration.Record.synthesis_sorted: sorting an available array.
• Cslib.Circuits.Boolean.Iteration.Record.synthesis_detect: detecting a colliding pair.

References

• Adapted from lean/Proofs/{RecordCircuits,Construction}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Boolean.Iteration.wires {n m : ℕ} (a : BitString n → BitString m) : Set (BooleanFunction n)

The coordinate functions of a family of bit strings.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_bits_eq {n m : ℕ} (s : Set (BooleanFunction n)) (a b : BitString n → BitString m) (ha : wires a ⊆ s) (hb : wires b ⊆ s) : Synthesis interpretation s {fun (x : BitString n) => decide (a x = b x)} (6 * m + 1)

Equality of two available bit strings, by the native equality formula.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_bits_mux {n m : ℕ} (s : Set (BooleanFunction n)) (a b : BitString n → BitString m) (flag : BooleanFunction n) (ha : wires a ⊆ s) (hb : wires b ⊆ s) (hf : flag ∈ s) : Synthesis interpretation s (wires fun (x : BitString n) => if flag x = true then a x else b x) (4 * m)

Multiplexing two m-bit strings by an available Boolean flag costs 4 * m gates.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_ite {n m A B F : ℕ} {s : Set (BooleanFunction n)} {a b : BitString n → BitString m} {flag : BooleanFunction n} (ha : Synthesis interpretation s (wires a) A) (hb : Synthesis interpretation s (wires b) B) (hf : Synthesis interpretation s {flag} F) : Synthesis interpretation s (wires fun (x : BitString n) => if flag x = true then a x else b x) (A + B + F + 4 * m)

Choosing between two constructions by a third adds four gates per output bit.

def Cslib.Circuits.Boolean.Iteration.Record.wireSet {n w : ℕ} (a : BitString n → Record n w) : Set (BooleanFunction n)

The bits of an available family of records.

theorem Cslib.Circuits.Boolean.Iteration.Record.padding_mem {n w : ℕ} {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) : (fun (x : BitString n) => (a x).padding) ∈ s

The padding bit of an available record belongs to s.

theorem Cslib.Circuits.Boolean.Iteration.Record.state_mem {n w : ℕ} {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) (i : Fin n) : (fun (x : BitString n) => (a x).state i) ∈ s

Each state bit of an available record belongs to s.

theorem Cslib.Circuits.Boolean.Iteration.Record.checkpoint_mem {n w : ℕ} {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) : (fun (x : BitString n) => (a x).checkpoint) ∈ s

The checkpoint bit of an available record belongs to s.

theorem Cslib.Circuits.Boolean.Iteration.Record.index_mem {n w : ℕ} {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) (i : Fin w) : (fun (x : BitString n) => (a x).index.getLsbD ↑i) ∈ s

Each index bit of an available record belongs to s.

theorem Cslib.Circuits.Boolean.Iteration.Record.payload_mem {n w : ℕ} {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) (i : Fin n) : (fun (x : BitString n) => (a x).payload i) ∈ s

Each payload bit of an available record belongs to s.

def Cslib.Circuits.Boolean.Iteration.Record.pairEncode {n w : ℕ} (pair : Record n w × Record n w) : BitString (width n w + width n w)

The bits of a pair of records, the first record first.

def Cslib.Circuits.Boolean.Iteration.Record.pairWires {n w : ℕ} (p : BitString n → Record n w × Record n w) : Set (BooleanFunction n)

The bits of an available family of pairs of records.

theorem Cslib.Circuits.Boolean.Iteration.Record.wireSet_fst_subset {n w : ℕ} (p : BitString n → Record n w × Record n w) : (wireSet fun (x : BitString n) => (p x).1) ⊆ pairWires p

The wire set of the first record of a pair is contained in pairWires p.

theorem Cslib.Circuits.Boolean.Iteration.Record.wireSet_snd_subset {n w : ℕ} (p : BitString n → Record n w × Record n w) : (wireSet fun (x : BitString n) => (p x).2) ⊆ pairWires p

The wire set of the second record of a pair is contained in pairWires p.

theorem Cslib.Circuits.Boolean.Iteration.Record.synthesis_detect {n w R : ℕ} (s : Set (BooleanFunction n)) (records : BitString n → Fin R → Record n w) (hr : ∀ (j : Fin R), (wireSet fun (x : BitString n) => records x j) ⊆ s) (hconst : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : Synthesis interpretation s (pairWires fun (x : BitString n) => detect (records x)) (30 * R * (width n w + 1))

Testing all adjacent pairs and selecting a colliding one.

def Cslib.Circuits.Boolean.Iteration.Record.recordsWires {n w R : ℕ} (records : BitString n → Fin R → Record n w) : Set (BooleanFunction n)

The bits of every record of an available array.

theorem Cslib.Circuits.Boolean.Iteration.Record.wireSet_subset_recordsWires {n w R : ℕ} (records : BitString n → Fin R → Record n w) (j : Fin R) : (wireSet fun (x : BitString n) => records x j) ⊆ recordsWires records

The wire set of the j-th record in an array is contained in recordsWires records.

theorem Cslib.Circuits.Boolean.Iteration.Record.size_sortCircuit_le {n w : ℕ} (d : ℕ) : (bitonicSortCircuit keyBits d true).size ≤ 18 * d ^ 2 * 2 ^ d * (width n w + 1)

The native sorter has at most 18 * d ^ 2 * 2 ^ d * (width + 1) gates.

theorem Cslib.Circuits.Boolean.Iteration.Record.synthesis_sorted {n w : ℕ} (s : Set (BooleanFunction n)) (d : ℕ) (records : BitString n → Fin (BitonicSort.arity d) → Record n w) (hr : recordsWires records ⊆ s) : Synthesis interpretation s (recordsWires fun (x : BitString n) => sorted d (records x)) (18 * d ^ 2 * 2 ^ d * (width n w + 1))

Sorting an available array inserts one native sorting circuit.