Sorting packed records by selected fields

The routing construction uses one physical record layout but sorts the same records by several different tuples of fields. Since input and output wiring is free in the circuit model, a within-record bit permutation turns any such tuple into the prefix consumed by the verified Batcher sorter. This module builds that wrapper and proves that it sorts the selected key, preserves every complete physical record, and has exactly the cost of the underlying sorter.

theorem Algebraic.MassProduction.Sorting.networkBits_eq_product (depth recordWidth : ℕ) : networkBits depth recordWidth = networkRecords depth * recordWidth

def Algebraic.MassProduction.Sorting.recordBitEquiv (depth recordWidth : ℕ) (bitOrder : Equiv.Perm (Fin recordWidth)) : Fin (networkBits depth recordWidth) → Fin (networkBits depth recordWidth)

Apply the same within-record bit permutation to every record in a flat row-major array. The permutation maps a virtual bit position to its physical position in the record.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.recordBitEquiv_recordBit {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (record : Fin (networkRecords depth)) (bit : Fin recordWidth) : recordBitEquiv depth recordWidth bitOrder (finProdFinEquiv (record, bit)) = finProdFinEquiv (record, bitOrder bit)

def Algebraic.MassProduction.Sorting.reindexRecordBits {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (input : Fin (networkBits depth recordWidth) → Bool) : Fin (networkBits depth recordWidth) → Bool

Reinterpret each physical record according to bitOrder.

Equations

• Algebraic.MassProduction.Sorting.reindexRecordBits bitOrder input = input ∘ Algebraic.MassProduction.Sorting.recordBitEquiv depth recordWidth bitOrder

@[simp]

theorem Algebraic.MassProduction.Sorting.reindexRecordBits_apply_recordBit {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (input : Fin (networkBits depth recordWidth) → Bool) (record : Fin (networkRecords depth)) (bit : Fin recordWidth) : reindexRecordBits bitOrder input (finProdFinEquiv (record, bit)) = input (finProdFinEquiv (record, bitOrder bit))

@[simp]

theorem Algebraic.MassProduction.Sorting.reindexRecordBits_symm_left {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (input : Fin (networkBits depth recordWidth) → Bool) : reindexRecordBits (Equiv.symm bitOrder) (reindexRecordBits bitOrder input) = input

@[simp]

theorem Algebraic.MassProduction.Sorting.reindexRecordBits_symm_right {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (input : Fin (networkBits depth recordWidth) → Bool) : reindexRecordBits bitOrder (reindexRecordBits (Equiv.symm bitOrder) input) = input

theorem Algebraic.MassProduction.Sorting.flatRecords_reindexRecordBits {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (input : Fin (networkBits depth recordWidth) → Bool) : flatRecords (reindexRecordBits bitOrder input) = fun (record : Fin (networkRecords depth)) (bit : Fin recordWidth) => flatRecords input record (bitOrder bit)

theorem Algebraic.MassProduction.Sorting.FlatRecordsPermute.reindexRecordBits {recordWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) {output input : Fin (networkBits depth recordWidth) → Bool} (recordsPermute : FlatRecordsPermute output input) : FlatRecordsPermute (Sorting.reindexRecordBits bitOrder output) (Sorting.reindexRecordBits bitOrder input)

Reindexing every record by the same bit permutation preserves a record-level permutation relation.

def Algebraic.MassProduction.Sorting.bitonicSortByBits {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : Fin (networkBits depth recordWidth) → Bool

Semantic sort by the first keyWidth virtual bits selected by bitOrder, returning records in their original physical layout.

Equations

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

def Algebraic.MassProduction.Sorting.bitonicSortByCircuit {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : Circuit DeMorgan.signature (networkBits depth recordWidth) (networkBits depth recordWidth)

Explicit Batcher circuit sorting by an arbitrary fixed tuple of record bits. Both layout conversions are free wire permutations.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicSortByCircuit_size {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicSortByCircuit bitOrder keyFits depth ascending).size = bitonicSortGateCount keyFits depth

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicSortByCircuit_eval {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : (bitonicSortByCircuit bitOrder keyFits depth ascending).eval DeMorgan.interpretation input = bitonicSortByBits bitOrder keyFits depth ascending input

def Algebraic.MassProduction.Sorting.FlatKeysSortedBy {recordWidth keyWidth depth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : Prop

The selected virtual prefix is sorted in the requested direction.

Equations

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

theorem Algebraic.MassProduction.Sorting.bitonicSortByBits_keysSorted {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatKeysSortedBy bitOrder keyFits ascending (bitonicSortByBits bitOrder keyFits depth ascending input)

theorem Algebraic.MassProduction.Sorting.bitonicSortByBits_recordsPermute {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatRecordsPermute (bitonicSortByBits bitOrder keyFits depth ascending input) input

theorem Algebraic.MassProduction.Sorting.bitonicSortByCircuit_keysSorted {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatKeysSortedBy bitOrder keyFits ascending ((bitonicSortByCircuit bitOrder keyFits depth ascending).eval DeMorgan.interpretation input)

theorem Algebraic.MassProduction.Sorting.bitonicSortByCircuit_recordsPermute {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatRecordsPermute ((bitonicSortByCircuit bitOrder keyFits depth ascending).eval DeMorgan.interpretation input) input

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicSortByCircuit_cost {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicSortByCircuit bitOrder keyFits depth ascending).cost DeMorgan.standardCost = (bitonicSortCircuit keyFits depth ascending).cost DeMorgan.standardCost

theorem Algebraic.MassProduction.Sorting.bitonicSortByCircuit_cost_le {recordWidth keyWidth : ℕ} (bitOrder : Equiv.Perm (Fin recordWidth)) (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicSortByCircuit bitOrder keyFits depth ascending).cost DeMorgan.standardCost ≤ depth * depth * networkRecords depth * (2 * recordWidth * (2 * (keyWidth * (6 * keyWidth + 4)) + 4))