Sorting records by a computed key

Compute a key for each record, sort the enriched records, and discard the temporary keys. Complete original records are preserved. This wrapper avoids changing physical record layouts when successive scheduler passes use different key fields.

def Algebraic.MassProduction.Nonuniform.KeyedSort.keyPart {keyWidth recordWidth : ℕ} (record : Fin (keyWidth + recordWidth) → Bool) : Fin keyWidth → Bool

Key prefix of an enriched record.

Equations

• Algebraic.MassProduction.Nonuniform.KeyedSort.keyPart record bit = record (Fin.castAdd recordWidth bit)

def Algebraic.MassProduction.Nonuniform.KeyedSort.bodyPart {keyWidth recordWidth : ℕ} (record : Fin (keyWidth + recordWidth) → Bool) : Fin recordWidth → Bool

Original record carried after the temporary key.

Equations

• Algebraic.MassProduction.Nonuniform.KeyedSort.bodyPart record bit = record (Fin.natAdd keyWidth bit)

def Algebraic.MassProduction.Nonuniform.KeyedSort.packCircuit {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : Circuit DeMorgan.signature (Sorting.networkRecords depth * recordWidth) (Sorting.networkRecords depth * (keyWidth + recordWidth))

Compute the sorting key and carry each complete original record.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.packCircuit_size {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (packCircuit depth keyCircuit).size = Sorting.networkRecords depth * keyCircuit.size

Packing costs exactly one key evaluation per record.

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.packCircuit_eval {recordWidth keyWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.flatRecords ((packCircuit depth keyCircuit).eval DeMorgan.interpretation input) record = Fin.append (keyCircuit.eval DeMorgan.interpretation (Sorting.flatRecords input record)) (Sorting.flatRecords input record)

Each packed record consists of its computed key and its original bits.

def Algebraic.MassProduction.Nonuniform.KeyedSort.circuit {recordWidth keyWidth : ℕ} (depth : ℕ) (ascending : Bool) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : Circuit DeMorgan.signature (Sorting.networkRecords depth * recordWidth) (Sorting.networkRecords depth * recordWidth)

The explicit computed-key sorting circuit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.circuit_size {recordWidth keyWidth : ℕ} (depth : ℕ) (ascending : Bool) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (circuit depth ascending keyCircuit).size = Sorting.networkRecords depth * keyCircuit.size + Sorting.bitonicSortGateCount ⋯ depth

One key evaluation per record, then the bitonic sort; discarding the keys is pure wiring.

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.circuit_eval_record {recordWidth keyWidth depth : ℕ} {ascending : Bool} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.flatRecords ((circuit depth ascending keyCircuit).eval DeMorgan.interpretation input) record = bodyPart (Sorting.flatRecords (Sorting.bitonicSortBits ⋯ depth ascending ((packCircuit depth keyCircuit).eval DeMorgan.interpretation input)) record)

Output records are bodies of the sorted enriched records.

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.circuit_recordsPermute {recordWidth keyWidth depth : ℕ} {ascending : Bool} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) : Sorting.FlatRecordsPermute ((circuit depth ascending keyCircuit).eval DeMorgan.interpretation input) input

Computing and dropping temporary keys preserves the original records as a complete-record permutation.

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.circuit_keysSorted {recordWidth keyWidth depth : ℕ} {ascending : Bool} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) : Sorting.Semantics.SequenceSorted ascending fun (record : Fin (Sorting.networkRecords depth)) => toLex (keyCircuit.eval DeMorgan.interpretation (Sorting.flatRecords ((circuit depth ascending keyCircuit).eval DeMorgan.interpretation input) record))

The keys recomputed from output records are sorted in the requested direction. Key correctness follows from complete-record preservation.

theorem Algebraic.MassProduction.Nonuniform.KeyedSort.circuit_cost_le {recordWidth keyWidth depth : ℕ} {ascending : Bool} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (circuit depth ascending keyCircuit).cost DeMorgan.standardCost ≤ Sorting.networkRecords depth * keyCircuit.cost DeMorgan.standardCost + depth * depth * Sorting.networkRecords depth * (2 * (keyWidth + recordWidth) * (2 * (keyWidth * (6 * keyWidth + 4)) + 4))

Key computation is charged once per record; temporary keys add only their width to the sorting payload.