Sorting records by a computed key

Compute each record's key once, sort the enriched records, and discard the temporary keys. The same record layout can therefore support successive sorts with different keys. Keys are ordered lexicographically, with coordinate zero most significant. Complete records, including duplicates and payload, are preserved; sorting need not be stable.

Main definitions

• Cslib.Circuits.Boolean.keyedSortCircuit: Batcher sorting by a supplied key circuit.

Main results

• Cslib.Circuits.Boolean.keyedSortCircuit_perm: preservation of complete records.
• Cslib.Circuits.Boolean.monotone_keyedSortCircuit and Cslib.Circuits.Boolean.antitone_keyedSortCircuit: recomputed output keys are sorted.
• Cslib.Circuits.Boolean.four_mul_cost_program_keyedSortCircuit: exact weighted cost, charging key computation once per record. This does not certify constructor runtime.

References

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

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

Compute keys, sort the enriched records, and retain the original record bodies.

def Cslib.Circuits.Boolean.keyedSortCircuit.pack {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) : Circuit signature (BitonicSort.arity depth * r) (BitonicSort.arity depth * (k + r))

Prepend the computed key to each complete record.

theorem Cslib.Circuits.Boolean.eval_keyedSortCircuit_pack {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (x : BitString (BitonicSort.arity depth * r)) (j : Fin (BitonicSort.arity depth)) : directProductInput ((keyedSortCircuit.pack key depth).eval interpretation x) j = Fin.append (key.eval interpretation (directProductInput x j)) (directProductInput x j)

Packing retains each record after its computed key.

theorem Cslib.Circuits.Boolean.eval_keyedSortCircuit {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity depth * r)) (j : Fin (BitonicSort.arity depth)) : directProductInput ((keyedSortCircuit key depth ascending).eval interpretation x) j = directProductInput ((bitonicSortCircuit (Fin.castAdd r) depth ascending).eval interpretation ((keyedSortCircuit.pack key depth).eval interpretation x)) j ∘ Fin.natAdd k

Each output record is the body of the corresponding sorted enriched record.

theorem Cslib.Circuits.Boolean.keyedSortCircuit_perm {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (ascending : Bool) (x : BitString (BitonicSort.arity depth * r)) : (List.ofFn (directProductInput ((keyedSortCircuit key depth ascending).eval interpretation x))).Perm (List.ofFn (directProductInput x))

Sorting by computed keys preserves the multiset of complete records.

theorem Cslib.Circuits.Boolean.monotone_keyedSortCircuit {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (x : BitString (BitonicSort.arity depth * r)) : Monotone fun (j : Fin (BitonicSort.arity depth)) => toLex (key.eval interpretation (directProductInput ((keyedSortCircuit key depth true).eval interpretation x) j))

Recomputing the keys of ascending output records gives a nondecreasing sequence.

theorem Cslib.Circuits.Boolean.antitone_keyedSortCircuit {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (x : BitString (BitonicSort.arity depth * r)) : Antitone fun (j : Fin (BitonicSort.arity depth)) => toLex (key.eval interpretation (directProductInput ((keyedSortCircuit key depth false).eval interpretation x) j))

Recomputing the keys of descending output records gives a nonincreasing sequence.

theorem Cslib.Circuits.Boolean.cost_program_keyedSortCircuit {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (ascending : Bool) (cost : signature.Op → ℕ) : (keyedSortCircuit key depth ascending).program.cost cost = BitonicSort.arity depth * key.program.cost cost + (bitonicSortCircuit (Fin.castAdd r) depth ascending).program.cost cost

Key computation is charged once per record; packing and dropping keys are free wirings.

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

Exact weighted cost, including all temporary key gates and comparisons. The factor four avoids natural division and includes depth zero, empty keys, and empty records.

theorem Cslib.Circuits.Boolean.four_mul_size_keyedSortCircuit {k r : ℕ} (key : Circuit signature r k) (depth : ℕ) (ascending : Bool) : 4 * (keyedSortCircuit key depth ascending).size = 4 * 2 ^ depth * key.size + depth * (depth + 1) * 2 ^ depth * if k + r = 0 then 0 else 6 * k + 6 * (k + r) + 2

Exact total gate count, including constants and negations.