Batcher sorting circuits

Records occupy consecutive blocks of input wires. The key selects coordinates in lexicographic order, with coordinate zero most significant. Each comparison moves whole records and shares its comparison flag across the record bits. Descending layers reverse ascending pairs, including ties; the complete sorter is not stable. Traced outputs prepend each comparison decision and its complement to the record blocks, sharing the original negation. Ordinary sorting selects the record outputs by free wiring. Empty records bypass the traced construction and use identity wiring; traced sorting still computes its control pairs. At depth d there are 2^d records and d * (d + 1) * 2^d / 4 comparisons. The circuit constructor is executable; the gate-count theorems do not certify its running time.

Main definitions

• Cslib.Circuits.Boolean.bitonicLayerCircuit: compare corresponding records in two halves.
• Cslib.Circuits.Boolean.bitonicMergeCircuit: merge a bitonic record array.
• Cslib.Circuits.Boolean.bitonicSortCircuit: sort a power-of-two record array.
• Cslib.Circuits.Boolean.bitonicSortTraceCircuit: sort and retain the comparison controls.
• Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pack: controls followed by records.

Main results

• Cslib.Circuits.Boolean.eval_bitonicSortCircuit: agreement with the generic algorithm.
• Cslib.Circuits.Boolean.eval_bitonicSortTraceCircuit: exact trace and record semantics.
• Cslib.Circuits.Boolean.monotone_bitonicSortCircuit and Cslib.Circuits.Boolean.antitone_bitonicSortCircuit: key sortedness in both directions.
• Cslib.Circuits.Boolean.bitonicSortCircuit_perm: preservation of complete records.
• Cslib.Circuits.Boolean.four_mul_cost_program_bitonicSortCircuit: exact weighted gate cost.
• Cslib.Circuits.Boolean.cost_program_bitonicSortTraceCircuit_eq: retaining controls adds no gates at nonzero record width, under arbitrary gate weights.

References

• K. E. Batcher, Sorting Networks and Their Applications.
• Adapted from MassProduction/SortingNetwork.lean and MassProduction/SortingCorrectness.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.bitonicLayerCircuit.pairInput {n r : ℕ} (j : Fin n) : Fin (r + r) → Fin ((n + n) * r)

Read a comparison's two records from the two halves.

def Cslib.Circuits.Boolean.bitonicLayerCircuit.gather (n r : ℕ) : Fin (n * (r + r)) → Fin ((n + n) * r)

Gather corresponding records into adjacent pairs.

def Cslib.Circuits.Boolean.bitonicLayerCircuit.scatter (n r : ℕ) : Fin ((n + n) * r) → Fin (n * (r + r))

Scatter the compared pairs back into the two record halves.

theorem Cslib.Circuits.Boolean.bitonicLayerCircuit.gather_pair {n r : ℕ} (x : BitString ((n + n) * r)) (j : Fin n) : directProductInput (x ∘ gather n r) j = Fin.append (directProductInput x (Fin.castAdd n j)) (directProductInput x (Fin.natAdd n j))

Gather reads corresponding records from the two halves without changing their bits.

def Cslib.Circuits.Boolean.bitonicMergeCircuit.firstHalf (n r : ℕ) : Fin (n * r) → Fin ((n + n) * r)

Select the first half of a flat record array.

def Cslib.Circuits.Boolean.bitonicMergeCircuit.secondHalf (n r : ℕ) : Fin (n * r) → Fin ((n + n) * r)

Select the second half of a flat record array.

theorem Cslib.Circuits.Boolean.bitonicMergeCircuit.records_firstHalf {n r : ℕ} (x : BitString ((n + n) * r)) : directProductInput (x ∘ firstHalf n r) = directProductInput x ∘ Fin.castAdd n

The first flat input block is the first half of the record array.

theorem Cslib.Circuits.Boolean.bitonicMergeCircuit.records_secondHalf {n r : ℕ} (x : BitString ((n + n) * r)) : directProductInput (x ∘ secondHalf n r) = directProductInput x ∘ Fin.natAdd n

The second flat input block is the second half of the record array.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.flatten {n r : ℕ} (x : Fin n → BitString r) : BitString (n * r)

Flatten a finite array of equal-width records.

@[simp]

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.directProductInput_flatten {n r : ℕ} (x : Fin n → BitString r) : directProductInput (flatten x) = x

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.controls {t n r : ℕ} (x : BitString (t * 2 + n * r)) : Fin t → BitString 2

The controls retain both a decision and its complement.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.records {t n r : ℕ} (x : BitString (t * 2 + n * r)) : Fin n → BitString r

The payload records following the controls.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pack {t n r : ℕ} (c : Fin t → BitString 2) (x : Fin n → BitString r) : BitString (t * 2 + n * r)

Encode control pairs followed by records.

@[simp]

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.controls_pack {t n r : ℕ} (c : Fin t → BitString 2) (x : Fin n → BitString r) : controls (pack c x) = c

@[simp]

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.records_pack {t n r : ℕ} (c : Fin t → BitString 2) (x : Fin n → BitString r) : records (pack c x) = x

@[simp]

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pack_comp_natAdd {t n r : ℕ} (c : Fin t → BitString 2) (x : Fin n → BitString r) : pack c x ∘ Fin.natAdd (t * 2) = flatten x

@[simp]

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.flatten_directProductInput {n r : ℕ} (x : BitString (n * r)) : flatten (directProductInput x) = x

Flattening the record view recovers the original wire assignment.

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.eval_parallel_pack {t n m r v : ℕ} (f : Circuit signature (n * r) (m * v)) (c : Fin t → BitString 2) (x : Fin n → BitString r) : ((Circuit.id signature (t * 2)).parallel f).eval interpretation (pack c x) = pack c (directProductInput (f.eval interpretation (flatten x)))

Apply a circuit to the payload while retaining every control pair by free wiring.

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.ext {t n r : ℕ} {x y : BitString (t * 2 + n * r)} (hc : controls x = controls y) (hd : records x = records y) : x = y

Control pairs and payload records determine the complete wire assignment.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.layout (t n r : ℕ) : Fin t × Fin 2 ⊕ Fin n × Fin r ≃ Fin (t * 2 + n * r)

The explicit numbering of control-pair and record coordinates.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.collect {input a b n m r : ℕ} (left : Circuit signature input (a * 2 + n * r)) (right : Circuit signature input (b * 2 + m * r)) : Circuit signature input ((a + b) * 2 + (n + m) * r)

Collect two circuits' controls before their concatenated record outputs.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.chain {input a b n m r : ℕ} (first : Circuit signature input (a * 2 + n * r)) (second : Circuit signature (n * r) (b * 2 + m * r)) : Circuit signature input ((a + b) * 2 + m * r)

Preserve the first controls while executing the second circuit on its payload.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pairs {n : ℕ} (flags : BitString n) : Fin n → BitString 2

Pair each decision with its complement.

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pairs_append {n m : ℕ} (x : BitString n) (y : BitString m) : pairs (Fin.append x y) = Fin.append (pairs x) (pairs y)

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pair {r : ℕ} (flag : Circuit signature (r + r) 1) (ascending : Bool) : Circuit signature (r + r) (2 + (r + r))

Descending compare-exchange reverses both the payload and the two control wires.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.layer {k r : ℕ} (key : Fin k → Fin r) (n : ℕ) (ascending : Bool) : Circuit signature ((n + n) * r) (n * 2 + (n + n) * r)

Compare a layer and retain all of its controls before the payload.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.halves {a b n r : ℕ} (left : Circuit signature (n * r) (a * 2 + n * r)) (right : Circuit signature (n * r) (b * 2 + n * r)) : Circuit signature ((n + n) * r) ((a + b) * 2 + (n + n) * r)

Run one traced circuit on each half of a record array.

def Cslib.Circuits.Boolean.bitonicMergeTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) : Bool → Circuit signature (BitonicSort.arity d * r) (BitonicSort.mergeTraceSize d * 2 + BitonicSort.arity d * r)

Bitonic merge, retaining comparison decisions before the merged records.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) : Bool → Circuit signature (BitonicSort.arity d * r) (BitonicSort.sortTraceSize d * 2 + BitonicSort.arity d * r)

Bitonic sorting, retaining comparison decisions before the sorted records.

theorem Cslib.Circuits.Boolean.eval_bitonicMergeTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity d * r)) : (bitonicMergeTraceCircuit key d ascending).eval interpretation x = bitonicSortTraceCircuit.pack (bitonicSortTraceCircuit.pairs (BitonicSort.mergeTrace (fun (row : BitString r) => toLex (row ∘ key)) d ascending (directProductInput x))) (BitonicSort.merge (fun (row : BitString r) => toLex (row ∘ key)) d ascending (directProductInput x))

The forward merge exposes exactly the semantic trace and merged records.

theorem Cslib.Circuits.Boolean.eval_bitonicSortTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity d * r)) : (bitonicSortTraceCircuit key d ascending).eval interpretation x = bitonicSortTraceCircuit.pack (bitonicSortTraceCircuit.pairs (BitonicSort.sortTrace (fun (row : BitString r) => toLex (row ∘ key)) d ascending (directProductInput x))) (BitonicSort.sort (fun (row : BitString r) => toLex (row ∘ key)) d ascending (directProductInput x))

The forward sorter exposes exactly the semantic trace and sorted records.

theorem Cslib.Circuits.Boolean.cost_program_bitonicMergeTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) (cost : signature.Op → ℕ) : (bitonicMergeTraceCircuit key d ascending).program.cost cost = BitonicSort.mergeTraceSize d * (compareSwapCircuit.record (Formula.lexLt (Fin.natAdd r ∘ key) (Fin.castAdd r ∘ key)).toCircuit).program.cost cost

A traced merge computes each comparator once, retaining its existing control pair.

theorem Cslib.Circuits.Boolean.cost_program_bitonicSortTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) (cost : signature.Op → ℕ) : (bitonicSortTraceCircuit key d ascending).program.cost cost = BitonicSort.sortTraceSize d * (compareSwapCircuit.record (Formula.lexLt (Fin.natAdd r ∘ key) (Fin.castAdd r ∘ key)).toCircuit).program.cost cost

A traced sort computes each comparator once, retaining its existing control pair.

def Cslib.Circuits.Boolean.bitonicLayerCircuit {k r : ℕ} (key : Fin k → Fin r) (n : ℕ) (ascending : Bool) : Circuit signature ((n + n) * r) ((n + n) * r)

Compare corresponding records, discarding the saved controls. Empty records use no gates.

def Cslib.Circuits.Boolean.bitonicMergeCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) : Circuit signature (BitonicSort.arity depth * r) (BitonicSort.arity depth * r)

Merge a bitonic array by selecting its traced merge's record outputs.

def Cslib.Circuits.Boolean.bitonicSortCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) : Circuit signature (BitonicSort.arity depth * r) (BitonicSort.arity depth * r)

Sort complete records, retaining the traced construction's sharing internally.

theorem Cslib.Circuits.Boolean.eval_bitonicLayerCircuit {k r : ℕ} (key : Fin k → Fin r) (n : ℕ) (ascending : Bool) (x : BitString ((n + n) * r)) : directProductInput ((bitonicLayerCircuit key n ascending).eval interpretation x) = BitonicSort.compareLayer (fun (record : BitString r) => toLex (record ∘ key)) ascending (directProductInput x)

Reading complete output records agrees with the generic bitonic comparison layer.

theorem Cslib.Circuits.Boolean.eval_bitonicMergeCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity depth * r)) : directProductInput ((bitonicMergeCircuit key depth ascending).eval interpretation x) = BitonicSort.merge (fun (record : BitString r) => toLex (record ∘ key)) depth ascending (directProductInput x)

The native circuit realizes bitonic merge on complete records.

theorem Cslib.Circuits.Boolean.eval_bitonicSortCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity depth * r)) : directProductInput ((bitonicSortCircuit key depth ascending).eval interpretation x) = BitonicSort.sort (fun (record : BitString r) => toLex (record ∘ key)) depth ascending (directProductInput x)

The native circuit realizes Batcher sorting on complete records.

theorem Cslib.Circuits.Boolean.monotone_bitonicSortCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (x : BitString (BitonicSort.arity depth * r)) : Monotone fun (j : Fin (BitonicSort.arity depth)) => toLex (directProductInput ((bitonicSortCircuit key depth true).eval interpretation x) j ∘ key)

The output keys of ascending sorting are nondecreasing.

theorem Cslib.Circuits.Boolean.antitone_bitonicSortCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (x : BitString (BitonicSort.arity depth * r)) : Antitone fun (j : Fin (BitonicSort.arity depth)) => toLex (directProductInput ((bitonicSortCircuit key depth false).eval interpretation x) j ∘ key)

The output keys of descending sorting are nonincreasing.

theorem Cslib.Circuits.Boolean.bitonicSortCircuit_perm {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity depth * r)) : (List.ofFn (directProductInput ((bitonicSortCircuit key depth ascending).eval interpretation x))).Perm (List.ofFn (directProductInput x))

Sorting preserves the multiset of complete input records, including payload and duplicates.

theorem Cslib.Circuits.Boolean.cost_program_bitonicLayerCircuit {k r : ℕ} (key : Fin k → Fin r) (n : ℕ) (ascending : Bool) (cost : signature.Op → ℕ) : (bitonicLayerCircuit key n ascending).program.cost cost = n * (compareSwapCircuit key).program.cost cost

A layer uses n copies of the comparator under any assignment of gate costs.

theorem Cslib.Circuits.Boolean.two_mul_cost_program_bitonicMergeCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) (cost : signature.Op → ℕ) : 2 * (bitonicMergeCircuit key depth ascending).program.cost cost = depth * 2 ^ depth * (compareSwapCircuit key).program.cost cost

Exact merge cost: depth * 2^depth / 2 comparisons, stated without natural division.

theorem Cslib.Circuits.Boolean.four_mul_cost_program_bitonicSortCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) (cost : signature.Op → ℕ) : 4 * (bitonicSortCircuit key depth ascending).program.cost cost = depth * (depth + 1) * 2 ^ depth * (compareSwapCircuit key).program.cost cost

Exact sorting cost: depth * (depth + 1) * 2^depth / 4 comparisons. The identity includes depth zero, empty keys, empty records, and arbitrary gate costs.

@[simp]

theorem Cslib.Circuits.Boolean.size_bitonicLayerCircuit {k r : ℕ} (key : Fin k → Fin r) (n : ℕ) (ascending : Bool) : (bitonicLayerCircuit key n ascending).size = n * (compareSwapCircuit key).size

Each of the n comparisons is charged once, including constants and negations.

theorem Cslib.Circuits.Boolean.four_mul_size_bitonicSortCircuit {k r : ℕ} (key : Fin k → Fin r) (depth : ℕ) (ascending : Bool) : 4 * (bitonicSortCircuit key depth ascending).size = depth * (depth + 1) * 2 ^ depth * if r = 0 then 0 else 6 * k + 6 * r + 2

Exact total gate count, including constants and negations.

theorem Cslib.Circuits.Boolean.cost_program_bitonicSortTraceCircuit_eq {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) (hr : r ≠ 0) (cost : signature.Op → ℕ) : (bitonicSortTraceCircuit key d ascending).program.cost cost = (bitonicSortCircuit key d ascending).program.cost cost

Retaining the trace adds no gates to ordinary sorting when records are nonempty.

theorem Cslib.Circuits.Boolean.size_bitonicSortTraceCircuit {k r : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) : (bitonicSortTraceCircuit key d ascending).size = BitonicSort.sortTraceSize d * (6 * k + 6 * r + 2)

Exact gate count, including the comparison constant and shared negation at empty width.