Explicit Boolean record comparators

The scheduler and router need oblivious sorting on fixed-width records. This module supplies the local building block: a lexicographic compare--exchange over the first keyWidth bits of two records. Its De Morgan circuit is explicit, its semantics are tied to Mathlib's lexicographic linear order, and its cost is polynomial. Network topology is developed separately.

def Algebraic.MassProduction.Sorting.recordPairIndex {recordWidth : ℕ} (side : Fin 2) (bit : Fin recordWidth) : Fin (2 * recordWidth)

Row-major index of one bit in a pair of equal-width records.

Equations

• Algebraic.MassProduction.Sorting.recordPairIndex side bit = finProdFinEquiv (side, bit)

def Algebraic.MassProduction.Sorting.recordPairSide {recordWidth : ℕ} (input : Fin (2 * recordWidth) → Bool) (side : Fin 2) : Fin recordWidth → Bool

Select one of the two records from a paired input.

Equations

• Algebraic.MassProduction.Sorting.recordPairSide input side bit = input (Algebraic.MassProduction.Sorting.recordPairIndex side bit)

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

Select the first keyWidth bits of one record.

Equations

• Algebraic.MassProduction.Sorting.recordKey keyFits input side bit = input (Algebraic.MassProduction.Sorting.recordPairIndex side (Fin.castLE keyFits bit))

def Algebraic.MassProduction.Sorting.bitEqualityExpression {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (bit : Fin keyWidth) : DeMorgan.Expression (2 * recordWidth)

XNOR expression for one pair of key bits.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.bitEqualityExpression_eval_eq_true_iff {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (bit : Fin keyWidth) (input : Fin (2 * recordWidth) → Bool) : DeMorgan.Expression.eval input (bitEqualityExpression keyFits leftSide rightSide bit) = true ↔ recordKey keyFits input leftSide bit = recordKey keyFits input rightSide bit

@[simp]

theorem Algebraic.MassProduction.Sorting.bitEqualityExpression_standardCost {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (bit : Fin keyWidth) : (bitEqualityExpression keyFits leftSide rightSide bit).standardCost = 5

def Algebraic.MassProduction.Sorting.priorKeyEqualityExpression {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (pivot : Fin keyWidth) : DeMorgan.Expression (2 * recordWidth)

All key coordinates before pivot are equal.

Equations

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

theorem Algebraic.MassProduction.Sorting.priorKeyEqualityExpression_eval_eq_true_iff {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (pivot : Fin keyWidth) (input : Fin (2 * recordWidth) → Bool) : DeMorgan.Expression.eval input (priorKeyEqualityExpression keyFits leftSide rightSide pivot) = true ↔ ∀ previous < pivot, recordKey keyFits input leftSide previous = recordKey keyFits input rightSide previous

def Algebraic.MassProduction.Sorting.keyLessAtExpression {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (pivot : Fin keyWidth) : DeMorgan.Expression (2 * recordWidth)

One possible first differing coordinate witnessing lexicographic strict inequality.

Equations

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

theorem Algebraic.MassProduction.Sorting.keyLessAtExpression_eval_eq_true_iff {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (pivot : Fin keyWidth) (input : Fin (2 * recordWidth) → Bool) : DeMorgan.Expression.eval input (keyLessAtExpression keyFits leftSide rightSide pivot) = true ↔ (∀ previous < pivot, recordKey keyFits input leftSide previous = recordKey keyFits input rightSide previous) ∧ recordKey keyFits input leftSide pivot < recordKey keyFits input rightSide pivot

def Algebraic.MassProduction.Sorting.keyLessExpression {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) : DeMorgan.Expression (2 * recordWidth)

Lexicographic strict-comparison expression for two record keys.

Equations

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

theorem Algebraic.MassProduction.Sorting.keyLessExpression_eval_eq_true_iff {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (input : Fin (2 * recordWidth) → Bool) : DeMorgan.Expression.eval input (keyLessExpression keyFits leftSide rightSide) = true ↔ Pi.Lex (fun (left right : Fin keyWidth) => left < right) (fun {i : Fin keyWidth} (left right : Bool) => left < right) (recordKey keyFits input leftSide) (recordKey keyFits input rightSide)

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

The Boolean swap flag is true exactly when the right key is lexicographically smaller than the left key.

Equations

• Algebraic.MassProduction.Sorting.compareSwapFlag keyFits input = Algebraic.DeMorgan.Expression.eval input (Algebraic.MassProduction.Sorting.keyLessExpression keyFits 1 0)

theorem Algebraic.MassProduction.Sorting.compareSwapFlag_eq_true_iff {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : compareSwapFlag keyFits input = true ↔ toLex (recordKey keyFits input 1) < toLex (recordKey keyFits input 0)

def Algebraic.MassProduction.Sorting.muxExpression {n : ℕ} (flag whenTrue whenFalse : DeMorgan.Expression n) : DeMorgan.Expression n

A Boolean multiplexer expression.

Equations

• Algebraic.MassProduction.Sorting.muxExpression flag whenTrue whenFalse = (flag.and whenTrue).or (flag.not.and whenFalse)

@[simp]

theorem Algebraic.MassProduction.Sorting.muxExpression_eval {n : ℕ} (flag whenTrue whenFalse : DeMorgan.Expression n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (muxExpression flag whenTrue whenFalse) = if DeMorgan.Expression.eval input flag = true then DeMorgan.Expression.eval input whenTrue else DeMorgan.Expression.eval input whenFalse

def Algebraic.MassProduction.Sorting.compareSwapBitExpression {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (output : Fin (2 * recordWidth)) : DeMorgan.Expression (2 * recordWidth)

One output bit of ascending compare--exchange.

Equations

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

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

Semantic ascending compare--exchange on a pair of records.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.compareSwapBitExpression_eval {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) (output : Fin (2 * recordWidth)) : DeMorgan.Expression.eval input (compareSwapBitExpression keyFits output) = compareSwapBits keyFits input output

@[reducible]

def Algebraic.MassProduction.Sorting.compareSwapBitGateCount {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (output : Fin (2 * recordWidth)) : ℕ

Gate count of one compiled compare--exchange output bit.

Equations

• Algebraic.MassProduction.Sorting.compareSwapBitGateCount keyFits output = (Algebraic.MassProduction.Sorting.compareSwapBitExpression keyFits output).gateCount

@[reducible]

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

Total emitted gate count of one compiled compare--exchange.

Equations

• Algebraic.MassProduction.Sorting.compareSwapGateCount keyFits = ∑ output : Fin (2 * recordWidth), Algebraic.MassProduction.Sorting.compareSwapBitGateCount keyFits output

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

Explicit ascending compare--exchange circuit on two packed records.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Sorting.compareSwapCircuit_size {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) : (compareSwapCircuit keyFits).size = compareSwapGateCount keyFits

The compiled compare--exchange emits exactly compareSwapGateCount gates.

@[simp]

theorem Algebraic.MassProduction.Sorting.compareSwapCircuit_eval {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : (compareSwapCircuit keyFits).eval DeMorgan.interpretation input = compareSwapBits keyFits input

@[simp]

theorem Algebraic.MassProduction.Sorting.muxExpression_standardCost {n : ℕ} (flag whenTrue whenFalse : DeMorgan.Expression n) : (muxExpression flag whenTrue whenFalse).standardCost = 2 * flag.standardCost + whenTrue.standardCost + whenFalse.standardCost + 4

Direct cost formula for a tree-shaped Boolean multiplexer.

theorem Algebraic.MassProduction.Sorting.priorKeyEqualityExpression_standardCost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (pivot : Fin keyWidth) : (priorKeyEqualityExpression keyFits leftSide rightSide pivot).standardCost ≤ 6 * keyWidth

theorem Algebraic.MassProduction.Sorting.keyLessAtExpression_standardCost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) (pivot : Fin keyWidth) : (keyLessAtExpression keyFits leftSide rightSide pivot).standardCost ≤ 6 * keyWidth + 3

theorem Algebraic.MassProduction.Sorting.keyLessExpression_standardCost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (leftSide rightSide : Fin 2) : (keyLessExpression keyFits leftSide rightSide).standardCost ≤ keyWidth * (6 * keyWidth + 4)

theorem Algebraic.MassProduction.Sorting.compareSwapBitExpression_standardCost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (output : Fin (2 * recordWidth)) : (compareSwapBitExpression keyFits output).standardCost ≤ 2 * (keyWidth * (6 * keyWidth + 4)) + 4

theorem Algebraic.MassProduction.Sorting.compareSwapCircuit_cost_le {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) : (compareSwapCircuit keyFits).cost DeMorgan.standardCost ≤ 2 * recordWidth * (2 * (keyWidth * (6 * keyWidth + 4)) + 4)

Explicit polynomial bound for one compare--exchange circuit.

@[simp]

theorem Algebraic.MassProduction.Sorting.compareSwapBits_side_zero {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : recordPairSide (compareSwapBits keyFits input) 0 = if compareSwapFlag keyFits input = true then recordPairSide input 1 else recordPairSide input 0

@[simp]

theorem Algebraic.MassProduction.Sorting.compareSwapBits_side_one {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : recordPairSide (compareSwapBits keyFits input) 1 = if compareSwapFlag keyFits input = true then recordPairSide input 0 else recordPairSide input 1

theorem Algebraic.MassProduction.Sorting.recordKey_compareSwapBits_zero {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : recordKey keyFits (compareSwapBits keyFits input) 0 = if compareSwapFlag keyFits input = true then recordKey keyFits input 1 else recordKey keyFits input 0

theorem Algebraic.MassProduction.Sorting.recordKey_compareSwapBits_one {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : recordKey keyFits (compareSwapBits keyFits input) 1 = if compareSwapFlag keyFits input = true then recordKey keyFits input 0 else recordKey keyFits input 1

theorem Algebraic.MassProduction.Sorting.compareSwapBits_keys_ordered {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : toLex (recordKey keyFits (compareSwapBits keyFits input) 0) ≤ toLex (recordKey keyFits (compareSwapBits keyFits input) 1)

Ascending compare--exchange orders its two output keys.

theorem Algebraic.MassProduction.Sorting.compareSwapBits_eq_pair {keyWidth recordWidth : ℕ} (keyFits : keyWidth ≤ recordWidth) (input : Fin (2 * recordWidth) → Bool) : compareSwapBits keyFits input = if compareSwapFlag keyFits input = true then fun (output : Fin (2 * recordWidth)) => have sideAndBit := finProdFinEquiv.symm output; Fin.cases (recordPairSide input 1 sideAndBit.2) (fun (x : Fin 1) => recordPairSide input 0 sideAndBit.2) sideAndBit.1 else input

Compare--exchange either preserves the record pair or swaps its two members, according to the comparison flag.