Reversing sorting circuits with saved comparison decisions

The forward circuits in Sorting sort records once and retain the comparison controls. This module reverses those decisions on new payloads using the same CSLib circuit representation. Reversal inspects only the controls, so answer payloads may have a different width and need not contain keys or unique identifiers.

A trace has BitonicSort.sortTraceSize d decisions stored as twice that many control wires, followed by BitonicSort.arity d consecutive records. The reverse circuit expects complementary control pairs; arbitrary pairs are not asserted to describe a permutation.

Reversal costs six gates per answer bit and comparison. These are circuit gate costs with free wiring, not bounds on retained storage or the circuit constructor's runtime.

Main definitions

• Cslib.Circuits.Boolean.bitonicUnsortCircuit: reverse saved decisions on new payloads.

Main results

• Cslib.Circuits.Boolean.eval_bitonicUnsortCircuit: reverse arbitrary paired decisions.
• Cslib.Circuits.Boolean.eval_bitonicUnsortCircuit_sort: restore transformed sorted records. The transformation is a semantic parameter; its implementation cost is not included.
• Cslib.Circuits.Boolean.size_bitonicUnsortCircuit: exact reversal gate count.

References

• K. E. Batcher, Sorting Networks and Their Applications.
• Extends the sorting backend adapted from S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.select {a t n m r : ℕ} (cs : Fin a → Fin t) (rs : Fin n → Fin m) : Circuit signature (t * 2 + m * r) (a * 2 + n * r)

Select controls and records independently by free wiring.

def Cslib.Circuits.Boolean.bitonicSortTraceCircuit.unlayer (n r : ℕ) : Circuit signature (n * 2 + (n + n) * r) ((n + n) * r)

Reverse a comparison layer, reading the saved decision and its complement.

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

Reverse two independent circuits using the matching halves of their controls and records.

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

Preserve the first controls while undoing the second stage, then undo the first stage.

theorem Cslib.Circuits.Boolean.bitonicSortTraceCircuit.pairs_comp {a b : ℕ} (flags : BitString a) (f : Fin b → Fin a) : pairs (flags ∘ f) = pairs flags ∘ f

def Cslib.Circuits.Boolean.bitonicUnmergeCircuit (r d : ℕ) : Circuit signature (BitonicSort.mergeTraceSize d * 2 + BitonicSort.arity d * r) (BitonicSort.arity d * r)

Undo the child merges before reversing the first comparison layer.

def Cslib.Circuits.Boolean.bitonicUnsortCircuit (r d : ℕ) : Circuit signature (BitonicSort.sortTraceSize d * 2 + BitonicSort.arity d * r) (BitonicSort.arity d * r)

Undo the final merge before reversing the two child sorts.

theorem Cslib.Circuits.Boolean.eval_bitonicUnmergeCircuit (r d : ℕ) (flags : BitString (BitonicSort.mergeTraceSize d)) (x : Fin (BitonicSort.arity d) → BitString r) : directProductInput ((bitonicUnmergeCircuit r d).eval interpretation (bitonicSortTraceCircuit.pack (bitonicSortTraceCircuit.pairs flags) x)) = BitonicSort.unrouteMerge d flags x

The reverse merge implements reversal for every paired trace and payload.

theorem Cslib.Circuits.Boolean.eval_bitonicUnsortCircuit (r d : ℕ) (flags : BitString (BitonicSort.sortTraceSize d)) (x : Fin (BitonicSort.arity d) → BitString r) : directProductInput ((bitonicUnsortCircuit r d).eval interpretation (bitonicSortTraceCircuit.pack (bitonicSortTraceCircuit.pairs flags) x)) = BitonicSort.unrouteSort d flags x

The reverse sorter implements reversal for every paired trace and payload.

theorem Cslib.Circuits.Boolean.cost_program_bitonicUnmergeCircuit (r d : ℕ) (cost : signature.Op → ℕ) : (bitonicUnmergeCircuit r d).program.cost cost = BitonicSort.mergeTraceSize d * (2 * r * (2 * cost Op.and + cost Op.or))

A reverse merge charges only switching; saved controls require no new negations.

theorem Cslib.Circuits.Boolean.cost_program_bitonicUnsortCircuit (r d : ℕ) (cost : signature.Op → ℕ) : (bitonicUnsortCircuit r d).program.cost cost = BitonicSort.sortTraceSize d * (2 * r * (2 * cost Op.and + cost Op.or))

A reverse sort charges only switching; saved controls require no new negations.

theorem Cslib.Circuits.Boolean.size_bitonicUnsortCircuit (r d : ℕ) : (bitonicUnsortCircuit r d).size = BitonicSort.sortTraceSize d * (6 * r)

Reversing a sort uses six gates per payload bit and comparison.

theorem Cslib.Circuits.Boolean.eval_bitonicUnsortCircuit_sort {k r v : ℕ} (key : Fin k → Fin r) (d : ℕ) (ascending : Bool) (f : BitString r → BitString v) (x : BitString (BitonicSort.arity d * r)) : have output := (bitonicSortTraceCircuit key d ascending).eval interpretation x; directProductInput ((bitonicUnsortCircuit v d).eval interpretation (bitonicSortTraceCircuit.pack (bitonicSortTraceCircuit.controls output) (f ∘ bitonicSortTraceCircuit.records output))) = f ∘ directProductInput x

Saved controls restore transformed records, even when the answer has a different width.