Batched routing with one sort and saved swaps

Sort by matching key and source/destination tag, broadcast source values along equal-key runs, then reverse the saved swaps on the values alone. Every destination receives its answer at its original input position. Neither request identifiers nor unique restoration keys are needed. False tags designate sources; true tags designate destinations. Multiple matching sources contribute their bitwise OR. A unique matching source is copied exactly.

The circuit returns value fields only. Header bits can be retained directly from the input by free wiring; they need not travel through the reverse circuit. Source-position outputs retain the broadcast's prefix accumulations, so destination correctness is a relational invariant, not a pointwise description of the entire broadcast.

All gate costs are charged, including constants and negations. Saved controls include their complements. Gate counts do not certify construction runtime or retained storage.

Main definitions

• Cslib.Circuits.Boolean.routeValuesCircuit: one sort, shared broadcast, and reverse routing.

Main results

• Cslib.Circuits.Boolean.eval_routeValuesCircuit_value_eq_true_iff: destination OR semantics at the original input position.
• Cslib.Circuits.Boolean.eval_routeValuesCircuit_of_unique_source: exact source copying.
• Cslib.Circuits.Boolean.cost_program_routeValuesCircuit: exact arbitrary weighted gate cost.
• Cslib.Circuits.Boolean.size_routeValuesCircuit: exact total gate count.

References

Simplifies the batched routing construction in S. Schlesinger, Boolean circuit mass production formalization, using the saved decisions of K. E. Batcher, Sorting Networks and Their Applications.

def Cslib.Circuits.Boolean.routeValuesCircuit.answerWiring (n h width : ℕ) : Circuit signature (n * (h + width)) (n * width)

Select the value field of each record, retaining row-major order.

def Cslib.Circuits.Boolean.routeValuesCircuit.matchingSelector {h k : ℕ} (key : Fin k → Fin h) (tag : Fin h) (width : ℕ) : Fin (k + 1) → Fin (h + width)

Select matching keys followed by their source/destination tag.

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

Sort once, broadcast matching source values, and undo saved swaps on the value fields.

theorem Cslib.Circuits.Boolean.cost_program_routeValuesCircuit {h k : ℕ} (key : Fin k → Fin h) (tag : Fin h) (d width : ℕ) (cost : signature.Op → ℕ) : (routeValuesCircuit key tag d width).program.cost cost = (bitonicSortTraceCircuit (routeValuesCircuit.matchingSelector key tag width) d true).program.cost cost + (broadcastCircuit key tag (BitonicSort.arity d) width).program.cost cost + BitonicSort.sortTraceSize d * (2 * width * (2 * cost Op.and + cost Op.or))

Exact weighted cost: one traced sort, shared broadcast, and reversal of the values only.

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

Each original destination receives the OR of matching original sources. Requests may repeat; no restoration keys, identifiers, rank calculations or source uniqueness are needed.

theorem Cslib.Circuits.Boolean.size_routeValuesCircuit {h k : ℕ} (key : Fin k → Fin h) (tag : Fin h) (d width : ℕ) : (routeValuesCircuit key tag d width).size = BitonicSort.sortTraceSize d * (6 * (k + 1) + 6 * h + 12 * width + 2) + (broadcastCircuit key tag (BitonicSort.arity d) width).size

Exact gate count for routing values back to the original record positions.

theorem Cslib.Circuits.Boolean.eval_routeValuesCircuit_of_unique_source {h k d width : ℕ} (key : Fin k → Fin h) (tag : Fin h) (x : BitString (BitonicSort.arity d * (h + width))) (source destination : Fin (BitonicSort.arity d)) (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 : ∀ (i : Fin (BitonicSort.arity d)), broadcastCircuit.header x i ∘ key = broadcastCircuit.header x source ∘ key → broadcastCircuit.header x i tag = false → i = source) : directProductInput ((routeValuesCircuit key tag d width).eval interpretation x) destination = broadcastCircuit.value x source

A destination receives its unique matching source at its literal original input position.