Correctness of the packed Boolean sorting circuit

This module bridges the explicit flat-bit Batcher circuit to the generic record-level correctness theorem. Keys are the initial keyWidth bits of each record, ordered lexicographically; all remaining bits are payload and must move with their record.

def Algebraic.MassProduction.Sorting.flatRecords {depth recordWidth : ℕ} (input : Fin (networkBits depth recordWidth) → Bool) : Fin (networkRecords depth) → Fin recordWidth → Bool

View a flat row-major bit vector as a sequence of complete records.

Equations

• Algebraic.MassProduction.Sorting.flatRecords input record = Algebraic.MassProduction.Sorting.networkRecord input record

def Algebraic.MassProduction.Sorting.firstRecordIndex (depth : ℕ) (pair : Fin (networkRecords depth)) : Fin (networkRecords (depth + 1))

First-half record index with the successor-depth type made explicit.

Equations

• Algebraic.MassProduction.Sorting.firstRecordIndex depth pair = ⟨↑pair, ⋯⟩

def Algebraic.MassProduction.Sorting.secondRecordIndex (depth : ℕ) (pair : Fin (networkRecords depth)) : Fin (networkRecords (depth + 1))

Second-half record index with the successor-depth type made explicit.

Equations

• Algebraic.MassProduction.Sorting.secondRecordIndex depth pair = ⟨Algebraic.MassProduction.Sorting.networkRecords depth + ↑pair, ⋯⟩

def Algebraic.MassProduction.Sorting.flatRecordKey {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (record : Fin recordWidth → Bool) : Lex (Fin keyWidth → Bool)

Lexicographic key carried by the initial bits of one record.

Equations

• Algebraic.MassProduction.Sorting.flatRecordKey keyFits record = toLex fun (bit : Fin keyWidth) => record (Fin.castLE keyFits bit)

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

Key-sortedness of a packed record array in the selected direction.

Equations

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

def Algebraic.MassProduction.Sorting.FlatRecordsPermute {depth recordWidth : ℕ} (output input : Fin (networkBits depth recordWidth) → Bool) : Prop

Preservation of all complete records, including payload bits.

Equations

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

theorem Algebraic.MassProduction.Sorting.FlatRecordsPermute.rangeContained {depth recordWidth : ℕ} {output input : Fin (networkBits depth recordWidth) → Bool} (permuted : FlatRecordsPermute output input) : Semantics.SequenceRangeContained (flatRecords output) (flatRecords input)

Every output record of a complete-record permutation occurs in the input record array.

theorem Algebraic.MassProduction.Sorting.FlatRecordsPermute.uniqueIndexWhere {depth recordWidth : ℕ} {output input : Fin (networkBits depth recordWidth) → Bool} {predicate : (Fin recordWidth → Bool) → Prop} (permuted : FlatRecordsPermute output input) (uniqueInput : Semantics.UniqueIndexWhere (flatRecords input) predicate) : Semantics.UniqueIndexWhere (flatRecords output) predicate

A complete-record permutation preserves unique satisfaction of every record predicate.

theorem Algebraic.MassProduction.Sorting.flatRecords_bitonicMergeBits {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : flatRecords (bitonicMergeBits keyFits depth ascending input) = Semantics.keyedBitonicMerge (flatRecordKey keyFits) depth ascending (flatRecords input)

The packed merge refines the generic keyed record merge.

theorem Algebraic.MassProduction.Sorting.flatRecords_bitonicSortBits {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : flatRecords (bitonicSortBits keyFits depth ascending input) = Semantics.keyedBitonicSort (flatRecordKey keyFits) depth ascending (flatRecords input)

The packed sorter refines the generic keyed Batcher sorter.

theorem Algebraic.MassProduction.Sorting.bitonicSortBits_keysSorted {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatKeysSorted keyFits ascending (bitonicSortBits keyFits depth ascending input)

The explicit packed semantics sorts all record keys.

theorem Algebraic.MassProduction.Sorting.bitonicSortBits_recordsPermute {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatRecordsPermute (bitonicSortBits keyFits depth ascending input) input

The explicit packed semantics preserves complete records up to permutation.

theorem Algebraic.MassProduction.Sorting.bitonicSortCircuit_keysSorted {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatKeysSorted keyFits ascending ((bitonicSortCircuit keyFits depth ascending).eval DeMorgan.interpretation input)

The evaluated Boolean circuit sorts every key in the chosen direction.

theorem Algebraic.MassProduction.Sorting.bitonicSortCircuit_recordsPermute {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : FlatRecordsPermute ((bitonicSortCircuit keyFits depth ascending).eval DeMorgan.interpretation input) input

The evaluated Boolean circuit permutes complete records and therefore cannot separate a payload from its key.