Two-sort batched routing

The first sort groups matching keys and places false-tagged sources before true-tagged requests. Shared broadcast replaces values while retaining every header bit. The second sort computes an arbitrary restoration key from each retained header. It does not rewrite headers or depend on the broadcast values.

Correctness is stated directly against the original unsorted input. Destination keys may repeat. Without source uniqueness, each destination receives the bitwise OR of all matching sources. A unique source is copied exactly. To recover a fixed output position, the client identifies a unique restoration key and counts the smaller keys in the original input.

Both sorts have 2 ^ depth records; padding is supplied by the caller. Keys and values may be empty, selectors may repeat, and computed restoration keys are charged once per record. Constants, negations and unused gates are included. The circuit constructor is executable; these gate bounds do not certify its running time. Concrete table layout and padding bounds for batched lookup are separate clients.

Main definitions

• Cslib.Circuits.Boolean.routeCircuit: the complete two-sort router.
• Cslib.Circuits.Boolean.routeCircuit.broadcast: matching sort and shared broadcast.

Main results

• Cslib.Circuits.Boolean.routeCircuit_headers_perm: all headers are retained.
• Cslib.Circuits.Boolean.eval_routeCircuit_value_eq_true_iff: destination OR semantics.
• Cslib.Circuits.Boolean.eval_routeCircuit_value_of_unique_source: fixed-position copying.
• Cslib.Circuits.Boolean.four_mul_cost_program_routeCircuit: exact weighted gate cost.
• Cslib.Circuits.Boolean.four_mul_size_routeCircuit: exact gate count.

References

Adapts MassProduction/Nonuniform/BatchRouting.lean from S. Schlesinger, Boolean circuit mass production formalization. The computed-key sorting API preserves the original headers without a separate complementing pass.

def Cslib.Circuits.Boolean.routeCircuit.matchKey {h k : ℕ} (key : Fin k → Fin h) (tag : Fin h) (width : ℕ) : Circuit signature (h + width) (k + 1)

Select the matching key followed by its source/destination tag.

def Cslib.Circuits.Boolean.routeCircuit.broadcast {h k : ℕ} (key : Fin k → Fin h) (tag : Fin h) (depth width : ℕ) : Circuit signature (BitonicSort.arity depth * (h + width)) (BitonicSort.arity depth * (h + width))

Sort by matching key and tag, then broadcast values while retaining every header.

theorem Cslib.Circuits.Boolean.routeCircuit.headers_perm {h k depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (x : BitString (BitonicSort.arity depth * (h + width))) : (List.ofFn (broadcastCircuit.header ((broadcast key tag depth width).eval interpretation x))).Perm (List.ofFn (broadcastCircuit.header x))

Matching and broadcast preserve the multiset of complete headers.

theorem Cslib.Circuits.Boolean.routeCircuit.value_eq_true_iff {h k depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (x : BitString (BitonicSort.arity depth * (h + width))) (destination : Fin (BitonicSort.arity depth)) (htag : broadcastCircuit.header ((broadcast key tag depth width).eval interpretation x) destination tag = true) (bit : Fin width) : broadcastCircuit.value ((broadcast key tag depth width).eval interpretation x) destination bit = true ↔ ∃ (source : Fin (BitonicSort.arity depth)), broadcastCircuit.header x source ∘ key = broadcastCircuit.header ((broadcast key tag depth width).eval interpretation x) destination ∘ key ∧ broadcastCircuit.header x source tag = false ∧ broadcastCircuit.value x source bit = true

Each destination after matching receives the OR of its original matching sources.

def Cslib.Circuits.Boolean.routeCircuit {h k o : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (depth width : ℕ) : Circuit signature (BitonicSort.arity depth * (h + width)) (BitonicSort.arity depth * (h + width))

Sort, broadcast, then sort by a computed header key. Both sorts retain the original header.

theorem Cslib.Circuits.Boolean.routeCircuit_headers_perm {h k o depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (x : BitString (BitonicSort.arity depth * (h + width))) : (List.ofFn (broadcastCircuit.header ((routeCircuit key tag order depth width).eval interpretation x))).Perm (List.ofFn (broadcastCircuit.header x))

The complete router preserves the multiset of headers, including all routing metadata.

theorem Cslib.Circuits.Boolean.monotone_routeCircuit {h k o depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (x : BitString (BitonicSort.arity depth * (h + width))) : Monotone fun (record : Fin (BitonicSort.arity depth)) => toLex (order.eval interpretation (broadcastCircuit.header ((routeCircuit key tag order depth width).eval interpretation x) record))

The final headers are ordered by the computed restoration key.

theorem Cslib.Circuits.Boolean.eval_routeCircuit_value_eq_true_iff {h k o depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (x : BitString (BitonicSort.arity depth * (h + width))) (destination : Fin (BitonicSort.arity depth)) (htag : broadcastCircuit.header ((routeCircuit key tag order depth width).eval interpretation x) destination tag = true) (bit : Fin width) : broadcastCircuit.value ((routeCircuit key tag order depth width).eval interpretation x) destination bit = true ↔ ∃ (source : Fin (BitonicSort.arity depth)), broadcastCircuit.header x source ∘ key = broadcastCircuit.header ((routeCircuit key tag order depth width).eval interpretation x) destination ∘ key ∧ broadcastCircuit.header x source tag = false ∧ broadcastCircuit.value x source bit = true

A destination receives the OR of matching original sources, even with repeated source keys.

theorem Cslib.Circuits.Boolean.eval_routeCircuit_header_of_rank {h k o depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (x : BitString (BitonicSort.arity depth * (h + width))) (destination target : Fin (BitonicSort.arity depth)) (unique : ∀ (i : Fin (BitonicSort.arity depth)), order.eval interpretation (broadcastCircuit.header x i) = order.eval interpretation (broadcastCircuit.header x destination) → i = destination) (rank : {i : Fin (BitonicSort.arity depth) | toLex (order.eval interpretation (broadcastCircuit.header x i)) < toLex (order.eval interpretation (broadcastCircuit.header x destination))}.card = ↑target) : broadcastCircuit.header ((routeCircuit key tag order depth width).eval interpretation x) target = broadcastCircuit.header x destination

A uniquely keyed destination header is restored to its rank in the original input.

theorem Cslib.Circuits.Boolean.eval_routeCircuit_value_eq_true_iff_of_rank {h k o depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (x : BitString (BitonicSort.arity depth * (h + width))) (destination target : Fin (BitonicSort.arity depth)) (unique : ∀ (i : Fin (BitonicSort.arity depth)), order.eval interpretation (broadcastCircuit.header x i) = order.eval interpretation (broadcastCircuit.header x destination) → i = destination) (rank : {i : Fin (BitonicSort.arity depth) | toLex (order.eval interpretation (broadcastCircuit.header x i)) < toLex (order.eval interpretation (broadcastCircuit.header x destination))}.card = ↑target) (htag : broadcastCircuit.header x destination tag = true) (bit : Fin width) : broadcastCircuit.value ((routeCircuit key tag order depth width).eval interpretation x) target bit = true ↔ ∃ (source : Fin (BitonicSort.arity depth)), broadcastCircuit.header x source ∘ key = broadcastCircuit.header x destination ∘ key ∧ broadcastCircuit.header x source tag = false ∧ broadcastCircuit.value x source bit = true

At a fixed restored position, destination values are the OR of matching original sources.

theorem Cslib.Circuits.Boolean.eval_routeCircuit_value_of_unique_source {h k o depth width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (x : BitString (BitonicSort.arity depth * (h + width))) (source destination target : Fin (BitonicSort.arity depth)) (uniqueDestination : ∀ (i : Fin (BitonicSort.arity depth)), order.eval interpretation (broadcastCircuit.header x i) = order.eval interpretation (broadcastCircuit.header x destination) → i = destination) (rank : {i : Fin (BitonicSort.arity depth) | toLex (order.eval interpretation (broadcastCircuit.header x i)) < toLex (order.eval interpretation (broadcastCircuit.header x destination))}.card = ↑target) (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) (uniqueSource : ∀ (i : Fin (BitonicSort.arity depth)), broadcastCircuit.header x i ∘ key = broadcastCircuit.header x source ∘ key → broadcastCircuit.header x i tag = false → i = source) : broadcastCircuit.value ((routeCircuit key tag order depth width).eval interpretation x) target = broadcastCircuit.value x source

A uniquely keyed destination copies its unique matching source to a fixed position.

theorem Cslib.Circuits.Boolean.cost_program_routeCircuit {h k o : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (depth width : ℕ) (cost : signature.Op → ℕ) : (routeCircuit key tag order depth width).program.cost cost = (keyedSortCircuit (routeCircuit.matchKey key tag width) depth true).program.cost cost + (broadcastCircuit key tag (BitonicSort.arity depth) width).program.cost cost + (keyedSortCircuit (order.comp (Circuit.wiring signature (Fin.castAdd width))) depth true).program.cost cost

Exact additive weighted cost of the two sorting circuits and shared broadcast.

theorem Cslib.Circuits.Boolean.four_mul_cost_program_routeCircuit {h k o : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (depth width : ℕ) (cost : signature.Op → ℕ) : 4 * (routeCircuit key tag order depth width).program.cost cost = 4 * 2 ^ depth * order.program.cost cost + depth * (depth + 1) * 2 ^ depth * ((compareSwapCircuit (Fin.castAdd (h + width))).program.cost cost + (compareSwapCircuit (Fin.castAdd (h + width))).program.cost cost) + 4 * (cost (Op.const false) + (2 ^ depth - 1) * (cost (Op.const true) + k * (3 * cost Op.and + 2 * cost Op.not + cost Op.or)) + width * (cost (Op.const false) + 2 ^ depth * (cost Op.not + 2 * cost Op.and + cost Op.or)))

Exact weighted cost, charging restoration keys once per record and all broadcast gates.

theorem Cslib.Circuits.Boolean.four_mul_size_routeCircuit {h k o : ℕ} (key : Fin k → Fin h) (tag : Fin h) (order : Circuit signature h o) (depth width : ℕ) : 4 * (routeCircuit key tag order depth width).size = 4 * 2 ^ depth * order.size + depth * (depth + 1) * 2 ^ depth * (12 * (k + 1 + o + h + width) + 4) + 4 * (1 + (2 ^ depth - 1) * (6 * k + 1) + width * (1 + 4 * 2 ^ depth))

Exact gate count; the factor four avoids natural division, including at depth zero.