Broadcast circuits for sorted records

Each record has a retained header followed by a value. Keys and source/destination tags are selected from the header. False tags seed source values; equal-key links carry their bitwise OR forward. When records are sorted by key followed by tag, each destination receives the OR of all matching sources. A unique matching source is therefore copied exactly. All header bits, including routing metadata, are preserved even on unsorted inputs.

Adjacent-key tests are computed once and shared across the value-bit scans. The construction uses native circuit composition, replication and wiring. It allows any record count, repeated keys and selectors, and empty key or value fields. With zero records, each value scan still contains its initial false constant. With zero value width, the shared key-test gates remain. The constructor is executable; its gate bounds do not certify the constructor's running time.

Main definitions

• Cslib.Circuits.Boolean.broadcastCircuit: a full record scan preserving the header.
• Cslib.Circuits.Boolean.broadcastCircuit.values: scans with arbitrary input selectors.
• Cslib.Circuits.Boolean.broadcastCircuit.header, Cslib.Circuits.Boolean.broadcastCircuit.value: projections of row-major record fields.

Main results

• Cslib.Circuits.Boolean.eval_broadcastCircuit_header: every header is preserved.
• Cslib.Circuits.Boolean.eval_broadcastCircuit_value_eq_true_iff: sorted destination semantics.
• Cslib.Circuits.Boolean.eval_broadcastCircuit_value_of_unique_source: exact source copying.
• Cslib.Circuits.Boolean.cost_program_broadcastCircuit: exact arbitrary weighted cost.
• Cslib.Circuits.Boolean.size_broadcastCircuit: exact gate count.

References

• Adapts MassProduction/Nonuniform/{BroadcastCircuit,BroadcastCorrectness,BroadcastRecords}.lean from S. Schlesinger, Boolean circuit mass production formalization, sharing the adjacent-key tests across value bits.

def Cslib.Circuits.Boolean.broadcastCircuit.scans (count width : ℕ) : Circuit signature (width * count + count) (width * count)

Run one shared propagation scan per value bit, reusing a single block of links.

def Cslib.Circuits.Boolean.broadcastCircuit.sources {input count width : ℕ} (tag : Fin count → Fin input) (payload : Fin count → Fin width → Fin input) : Circuit signature input (width * count)

Only false-tagged source records seed a value bit.

def Cslib.Circuits.Boolean.broadcastCircuit.values {input count keyWidth width : ℕ} (key : Fin count → Fin keyWidth → Fin input) (tag : Fin count → Fin input) (payload : Fin count → Fin width → Fin input) : Circuit signature input (width * count)

Broadcast all selected value bits, sharing adjacent-key tests between the scans.

theorem Cslib.Circuits.Boolean.broadcastCircuit.eval_values_eq_true_iff {input count keyWidth width : ℕ} (key : Fin count → Fin keyWidth → Fin input) (tag : Fin count → Fin input) (payload : Fin count → Fin width → Fin input) (x : BitString input) (sorted : Monotone fun (record : Fin count) => toLex (Fin.snoc (x ∘ key record) (x (tag record)))) (bit : Fin width) (destination : Fin count) (htag : x (tag destination) = true) : (values key tag payload).eval interpretation x (finProdFinEquiv (bit, destination)) = true ↔ ∃ (source : Fin count), x ∘ key source = x ∘ key destination ∧ x (tag source) = false ∧ x (payload source bit) = true

At a destination in sorted key/tag order, each output bit is the OR of all matching source bits. The selectors may overlap or repeat; source keys need not be unique.

def Cslib.Circuits.Boolean.broadcastCircuit.header {count headerWidth width : ℕ} (x : BitString (count * (headerWidth + width))) (record : Fin count) : BitString headerWidth

Read the retained header of a row-major record array.

def Cslib.Circuits.Boolean.broadcastCircuit.value {count headerWidth width : ℕ} (x : BitString (count * (headerWidth + width))) (record : Fin count) : BitString width

Read the value field following the retained header.

def Cslib.Circuits.Boolean.broadcastCircuit.outputWire (count headerWidth width : ℕ) (index : Fin (count * (headerWidth + width))) : Fin (count * (headerWidth + width) + width * count)

Keep every header wire and replace value wires by the corresponding scan outputs.

def Cslib.Circuits.Boolean.broadcastCircuit {headerWidth keyWidth : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (count width : ℕ) : Circuit signature (count * (headerWidth + width)) (count * (headerWidth + width))

Broadcast values in a record array, preserving the entire retained header. Keys and tags are selected from that header; the value field follows it. Sorted destination semantics is proved separately. Gate counts include unused work at zero output width or zero records.

theorem Cslib.Circuits.Boolean.eval_broadcastCircuit_header {count headerWidth keyWidth width : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (x : BitString (count * (headerWidth + width))) (record : Fin count) : broadcastCircuit.header ((broadcastCircuit key tag count width).eval interpretation x) record = broadcastCircuit.header x record

Every header bit is preserved, including keys, tags and arbitrary routing metadata.

theorem Cslib.Circuits.Boolean.eval_broadcastCircuit_value {count headerWidth keyWidth width : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (x : BitString (count * (headerWidth + width))) (record : Fin count) (bit : Fin width) : broadcastCircuit.value ((broadcastCircuit key tag count width).eval interpretation x) record bit = (broadcastCircuit.values (fun (record : Fin count) (bit : Fin keyWidth) => finProdFinEquiv (record, Fin.castAdd width (key bit))) (fun (record : Fin count) => finProdFinEquiv (record, Fin.castAdd width tag)) fun (record : Fin count) (bit : Fin width) => finProdFinEquiv (record, Fin.natAdd headerWidth bit)).eval interpretation x (finProdFinEquiv (bit, record))

The value field is supplied by the shared scans.

theorem Cslib.Circuits.Boolean.eval_broadcastCircuit_value_eq_true_iff {count headerWidth keyWidth width : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (x : BitString (count * (headerWidth + width))) (sorted : Monotone fun (record : Fin count) => toLex (Fin.snoc (broadcastCircuit.header x record ∘ key) (broadcastCircuit.header x record tag))) (destination : Fin count) (htag : broadcastCircuit.header x destination tag = true) (bit : Fin width) : broadcastCircuit.value ((broadcastCircuit key tag count width).eval interpretation x) destination bit = true ↔ ∃ (source : Fin count), broadcastCircuit.header x source ∘ key = broadcastCircuit.header x destination ∘ key ∧ broadcastCircuit.header x source tag = false ∧ broadcastCircuit.value x source bit = true

Each sorted destination receives the OR of all sources with its selected key.

theorem Cslib.Circuits.Boolean.eval_broadcastCircuit_value_of_unique_source {count headerWidth keyWidth width : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (x : BitString (count * (headerWidth + width))) (sorted : Monotone fun (record : Fin count) => toLex (Fin.snoc (broadcastCircuit.header x record ∘ key) (broadcastCircuit.header x record tag))) (source destination : Fin count) (hkey : broadcastCircuit.header x source ∘ key = broadcastCircuit.header x destination ∘ key) (hsource : broadcastCircuit.header x source tag = false) (hdestination : broadcastCircuit.header x destination tag = true) (unique : ∀ (record : Fin count), broadcastCircuit.header x record ∘ key = broadcastCircuit.header x source ∘ key → broadcastCircuit.header x record tag = false → record = source) : broadcastCircuit.value ((broadcastCircuit key tag count width).eval interpretation x) destination = broadcastCircuit.value x source

A sorted destination copies its unique matching source value exactly.

theorem Cslib.Circuits.Boolean.cost_program_broadcastCircuit {headerWidth keyWidth : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (count width : ℕ) (cost : signature.Op → ℕ) : (broadcastCircuit key tag count width).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))) + width * (cost (Op.const false) + count * (cost Op.not + 2 * cost Op.and + cost Op.or))

Exact arbitrary weighted cost: shared adjacent-key tests plus one scan per value bit.

theorem Cslib.Circuits.Boolean.size_broadcastCircuit {headerWidth keyWidth : ℕ} (key : Fin keyWidth → Fin headerWidth) (tag : Fin headerWidth) (count width : ℕ) : (broadcastCircuit key tag count width).size = (if count = 0 then 0 else 1 + (count - 1) * (6 * keyWidth + 1)) + width * (1 + 4 * count)

Exact gate count, including constants and unused gates at empty dimensions.