Oblivious sorting-network layers

This module lifts the verified two-record comparator to a full butterfly layer on 2^(depth+1) records. The construction is explicit at the circuit level and its cost is linear in the number of records times the local comparator cost. Recursive Batcher merge and sort networks build on this layer.

def Algebraic.MassProduction.Sorting.networkRecords : ℕ → ℕ

Recursive power-of-two record count.

Equations

• Algebraic.MassProduction.Sorting.networkRecords 0 = 1
• Algebraic.MassProduction.Sorting.networkRecords depth.succ = Algebraic.MassProduction.Sorting.networkRecords depth + Algebraic.MassProduction.Sorting.networkRecords depth

@[simp]

theorem Algebraic.MassProduction.Sorting.networkRecords_eq_two_pow (depth : ℕ) : networkRecords depth = 2 ^ depth

theorem Algebraic.MassProduction.Sorting.networkRecords_succ (depth : ℕ) : networkRecords (depth + 1) = networkRecords depth + networkRecords depth

The record count doubles at successor depth.

def Algebraic.MassProduction.Sorting.networkBits (depth recordWidth : ℕ) : ℕ

Flat bit count of a power-of-two record array.

Equations

• Algebraic.MassProduction.Sorting.networkBits depth recordWidth = Algebraic.MassProduction.Sorting.networkRecords depth * recordWidth

theorem Algebraic.MassProduction.Sorting.networkBits_succ (depth recordWidth : ℕ) : networkBits (depth + 1) recordWidth = networkBits depth recordWidth + networkBits depth recordWidth

def Algebraic.MassProduction.Sorting.firstHalfWire (depth recordWidth : ℕ) : Fin (networkBits depth recordWidth) → Fin (networkBits (depth + 1) recordWidth)

Embed a bit from the first half into the doubled record array.

Equations

• Algebraic.MassProduction.Sorting.firstHalfWire depth recordWidth input = Fin.cast ⋯ (Fin.castAdd (Algebraic.MassProduction.Sorting.networkBits depth recordWidth) input)

def Algebraic.MassProduction.Sorting.secondHalfWire (depth recordWidth : ℕ) : Fin (networkBits depth recordWidth) → Fin (networkBits (depth + 1) recordWidth)

Embed a bit from the second half into the doubled record array.

Equations

• Algebraic.MassProduction.Sorting.secondHalfWire depth recordWidth input = Fin.cast ⋯ (Fin.natAdd (Algebraic.MassProduction.Sorting.networkBits depth recordWidth) input)

def Algebraic.MassProduction.Sorting.firstHalfBits {depth recordWidth : ℕ} (input : Fin (networkBits (depth + 1) recordWidth) → Bool) : Fin (networkBits depth recordWidth) → Bool

Restrict a flat record array to its first half.

Equations

• Algebraic.MassProduction.Sorting.firstHalfBits input = input ∘ Algebraic.MassProduction.Sorting.firstHalfWire depth recordWidth

def Algebraic.MassProduction.Sorting.secondHalfBits {depth recordWidth : ℕ} (input : Fin (networkBits (depth + 1) recordWidth) → Bool) : Fin (networkBits depth recordWidth) → Bool

Restrict a flat record array to its second half.

Equations

• Algebraic.MassProduction.Sorting.secondHalfBits input = input ∘ Algebraic.MassProduction.Sorting.secondHalfWire depth recordWidth

def Algebraic.MassProduction.Sorting.joinHalfBits {depth recordWidth : ℕ} (left right : Fin (networkBits depth recordWidth) → Bool) : Fin (networkBits (depth + 1) recordWidth) → Bool

Concatenate two equal-depth flat record arrays.

Equations

• Algebraic.MassProduction.Sorting.joinHalfBits left right output = Fin.append left right (Fin.cast ⋯ output)

@[simp]

theorem Algebraic.MassProduction.Sorting.firstHalfBits_joinHalfBits {depth recordWidth : ℕ} (left right : Fin (networkBits depth recordWidth) → Bool) : firstHalfBits (joinHalfBits left right) = left

@[simp]

theorem Algebraic.MassProduction.Sorting.secondHalfBits_joinHalfBits {depth recordWidth : ℕ} (left right : Fin (networkBits depth recordWidth) → Bool) : secondHalfBits (joinHalfBits left right) = right

def Algebraic.MassProduction.Sorting.Circuit.parallelHalves {σ : Signature} {depth recordWidth : ℕ} (left right : Circuit σ (networkBits depth recordWidth) (networkBits depth recordWidth)) : Circuit σ (networkBits (depth + 1) recordWidth) (networkBits (depth + 1) recordWidth)

Run one circuit on each half of a doubled flat record array.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.Circuit.eval_parallelHalves {σ : Signature} {depth recordWidth : ℕ} {U : Type u_2} (left right : Circuit σ (networkBits depth recordWidth) (networkBits depth recordWidth)) (interpretation : Interpretation σ U) (input : Fin (networkBits (depth + 1) recordWidth) → U) : (parallelHalves left right).eval interpretation input = fun (output : Fin (networkBits (depth + 1) recordWidth)) => Fin.append (left.eval interpretation (input ∘ firstHalfWire depth recordWidth)) (right.eval interpretation (input ∘ secondHalfWire depth recordWidth)) (Fin.cast ⋯ output)

@[simp]

theorem Algebraic.MassProduction.Sorting.Circuit.cost_parallelHalves {σ : Signature} {depth recordWidth : ℕ} (left right : Circuit σ (networkBits depth recordWidth) (networkBits depth recordWidth)) (operationCost : OperationCost σ) : (parallelHalves left right).cost operationCost = left.cost operationCost + right.cost operationCost

@[simp]

theorem Algebraic.MassProduction.Sorting.Circuit.size_parallelHalves {σ : Signature} {depth recordWidth : ℕ} (left right : Circuit σ (networkBits depth recordWidth) (networkBits depth recordWidth)) : (parallelHalves left right).size = left.size + right.size

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

Read one record from a flat row-major network array.

Equations

• Algebraic.MassProduction.Sorting.networkRecord input record bit = input (finProdFinEquiv (record, bit))

def Algebraic.MassProduction.Sorting.gatherLayerPairInput (depth recordWidth : ℕ) (pair : Fin (networkRecords depth)) : Fin (2 * recordWidth) → Fin (networkBits (depth + 1) recordWidth)

Input wiring which gathers corresponding records from the two halves.

Equations

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

def Algebraic.MassProduction.Sorting.reverseRecordPairOutput {recordWidth : ℕ} (output : Fin (2 * recordWidth)) : Fin (2 * recordWidth)

Swap the two record-sized halves of a local pair output.

Equations

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

def Algebraic.MassProduction.Sorting.comparePairBits {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) (input : Fin (2 * recordWidth) → Bool) : Fin (2 * recordWidth) → Bool

Ascending or descending local compare--exchange semantics.

Equations

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

def Algebraic.MassProduction.Sorting.comparePairCircuit {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : Circuit DeMorgan.signature (2 * recordWidth) (2 * recordWidth)

Ascending or descending local compare--exchange circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.comparePairCircuit_eval {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) (input : Fin (2 * recordWidth) → Bool) : (comparePairCircuit keyFits ascending).eval DeMorgan.interpretation input = comparePairBits keyFits ascending input

@[simp]

theorem Algebraic.MassProduction.Sorting.comparePairCircuit_cost {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : (comparePairCircuit keyFits ascending).cost DeMorgan.standardCost = (compareSwapCircuit keyFits).cost DeMorgan.standardCost

@[simp]

theorem Algebraic.MassProduction.Sorting.comparePairCircuit_size {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : (comparePairCircuit keyFits ascending).size = compareSwapGateCount keyFits

def Algebraic.MassProduction.Sorting.compareLayerPairCircuit {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) (pair : Fin (networkRecords depth)) : Circuit DeMorgan.signature (networkBits (depth + 1) recordWidth) (2 * recordWidth)

One gathered pair comparator inside a butterfly layer.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.compareLayerPairCircuit_size {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) (pair : Fin (networkRecords depth)) : (compareLayerPairCircuit depth keyFits ascending pair).size = compareSwapGateCount keyFits

def Algebraic.MassProduction.Sorting.compareLayerOutputMap (depth recordWidth : ℕ) : Fin (networkBits (depth + 1) recordWidth) → Fin (networkRecords depth * (2 * recordWidth))

Convert the desired half-major output layout to the pair-major layout emitted by parallelFinVector.

Equations

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

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

Semantic butterfly layer comparing corresponding records in the two halves.

Equations

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

@[reducible]

def Algebraic.MassProduction.Sorting.compareLayerGateCount {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) : ℕ

Total emitted gate count of one butterfly layer.

Equations

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

def Algebraic.MassProduction.Sorting.compareLayerCircuit {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : Circuit DeMorgan.signature (networkBits (depth + 1) recordWidth) (networkBits (depth + 1) recordWidth)

Explicit circuit for one full butterfly compare layer.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.compareLayerCircuit_size {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : (compareLayerCircuit depth keyFits ascending).size = compareLayerGateCount depth keyFits

@[simp]

theorem Algebraic.MassProduction.Sorting.compareLayerCircuit_eval {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) (input : Fin (networkBits (depth + 1) recordWidth) → Bool) : (compareLayerCircuit depth keyFits ascending).eval DeMorgan.interpretation input = compareLayerBits depth keyFits ascending input

@[simp]

theorem Algebraic.MassProduction.Sorting.compareLayerCircuit_cost {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : (compareLayerCircuit depth keyFits ascending).cost DeMorgan.standardCost = networkRecords depth * (compareSwapCircuit keyFits).cost DeMorgan.standardCost

theorem Algebraic.MassProduction.Sorting.compareLayerCircuit_cost_le {keyWidth recordWidth : ℕ} (depth : ℕ) (keyFits : keyWidth ≤ recordWidth) (ascending : Bool) : (compareLayerCircuit depth keyFits ascending).cost DeMorgan.standardCost ≤ networkRecords depth * (2 * recordWidth * (2 * (keyWidth * (6 * keyWidth + 4)) + 4))

One layer is linear in its number of comparators.

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

Semantic bitonic merge on a power-of-two flat record array.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicMergeBits keyFits 0 x✝ input = input

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

Semantic Batcher sorting network on a power-of-two record array.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicSortBits keyFits 0 x✝ input = input

@[reducible]

def Algebraic.MassProduction.Sorting.bitonicMergeGateCount {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) : ℕ → ℕ

Gate count emitted by the recursive merge circuit.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicMergeGateCount keyFits 0 = 0

@[reducible]

def Algebraic.MassProduction.Sorting.bitonicSortGateCount {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) : ℕ → ℕ

Gate count emitted by the complete recursive sorter.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicSortGateCount keyFits 0 = 0

def Algebraic.MassProduction.Sorting.bitonicMergeCircuit {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : Circuit DeMorgan.signature (networkBits depth recordWidth) (networkBits depth recordWidth)

Explicit recursive bitonic merge circuit.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicMergeCircuit keyFits 0 x✝ = Cslib.Circuits.Circuit.castCounts ⋯ ⋯ (Cslib.Circuits.Circuit.id Algebraic.DeMorgan.signature recordWidth)

def Algebraic.MassProduction.Sorting.bitonicSortCircuit {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : Circuit DeMorgan.signature (networkBits depth recordWidth) (networkBits depth recordWidth)

Explicit recursive Batcher sorting circuit.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicSortCircuit keyFits 0 x✝ = Cslib.Circuits.Circuit.castCounts ⋯ ⋯ (Cslib.Circuits.Circuit.id Algebraic.DeMorgan.signature recordWidth)

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicMergeCircuit_eval {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) (input : Fin (networkBits depth recordWidth) → Bool) : (bitonicMergeCircuit keyFits depth ascending).eval DeMorgan.interpretation input = bitonicMergeBits keyFits depth ascending input

@[simp]

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

def Algebraic.MassProduction.Sorting.bitonicMergeStandardCost {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) : ℕ → ℕ

Exact standard-cost recurrence for the recursive merge.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicMergeStandardCost keyFits 0 = 0

def Algebraic.MassProduction.Sorting.bitonicSortStandardCost {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) : ℕ → ℕ

Exact standard-cost recurrence for the complete sorter.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.bitonicSortStandardCost keyFits 0 = 0

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicMergeCircuit_cost {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicMergeCircuit keyFits depth ascending).cost DeMorgan.standardCost = bitonicMergeStandardCost keyFits depth

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicSortCircuit_cost {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicSortCircuit keyFits depth ascending).cost DeMorgan.standardCost = bitonicSortStandardCost keyFits depth

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicMergeCircuit_size {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicMergeCircuit keyFits depth ascending).size = bitonicMergeGateCount keyFits depth

The recursive merge emits exactly bitonicMergeGateCount gates.

@[simp]

theorem Algebraic.MassProduction.Sorting.bitonicSortCircuit_size {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicSortCircuit keyFits depth ascending).size = bitonicSortGateCount keyFits depth

The recursive sorter emits exactly bitonicSortGateCount gates.

theorem Algebraic.MassProduction.Sorting.bitonicMergeStandardCost_succ {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) : bitonicMergeStandardCost keyFits (depth + 1) = (depth + 1) * networkRecords depth * (compareSwapCircuit keyFits).cost DeMorgan.standardCost

At successor depth, the merge has one half-array of comparators at each recursive level.

theorem Algebraic.MassProduction.Sorting.two_mul_bitonicSortStandardCost_succ {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) : 2 * bitonicSortStandardCost keyFits (depth + 1) = (depth + 1) * (depth + 2) * networkRecords depth * (compareSwapCircuit keyFits).cost DeMorgan.standardCost

Twice the exact sorter cost has a division-free closed form.

theorem Algebraic.MassProduction.Sorting.bitonicSortStandardCost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) : bitonicSortStandardCost keyFits depth ≤ depth * depth * networkRecords depth * (compareSwapCircuit keyFits).cost DeMorgan.standardCost

Standard-cost bound for Batcher sorting: number of records times the square of the recursion depth times one comparator cost.

theorem Algebraic.MassProduction.Sorting.bitonicSortCircuit_cost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (depth : ℕ) (ascending : Bool) : (bitonicSortCircuit keyFits depth ascending).cost DeMorgan.standardCost ≤ depth * depth * networkRecords depth * (2 * recordWidth * (2 * (keyWidth * (6 * keyWidth + 4)) + 4))

Fully explicit polynomial gate-cost bound for the Boolean sorter.