Fixed-wire record routing primitives

After records are sorted by (key, type), both scatter and gather use the same local operation: a destination record copies the payload of its immediate predecessor exactly when the predecessor has the source tag and the keys agree. The first array position uses a fixed dummy payload. This module builds that operation as an explicit De Morgan circuit and proves its exact semantics and a polynomial cost bound.

def Algebraic.MassProduction.Routing.recordWidth (keyWidth payloadWidth : ℕ) : ℕ

Width of a record containing key bits, one type bit, and payload bits.

Equations

• Algebraic.MassProduction.Routing.recordWidth keyWidth payloadWidth = keyWidth + 1 + payloadWidth

def Algebraic.MassProduction.Routing.recordBitIndex (depth keyWidth payloadWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (recordWidth keyWidth payloadWidth)) : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

Flat row-major index of one bit in a routing record array.

Equations

• Algebraic.MassProduction.Routing.recordBitIndex depth keyWidth payloadWidth record bit = finProdFinEquiv (record, bit)

@[simp]

theorem Algebraic.MassProduction.Routing.finProdFinEquiv_symm_recordBitIndex {depth keyWidth payloadWidth : ℕ} (record : Fin (Sorting.networkRecords depth)) (bit : Fin (recordWidth keyWidth payloadWidth)) : finProdFinEquiv.symm (recordBitIndex depth keyWidth payloadWidth record bit) = (record, bit)

def Algebraic.MassProduction.Routing.keyBit (keyWidth payloadWidth : ℕ) (bit : Fin keyWidth) : Fin (recordWidth keyWidth payloadWidth)

Index of one key bit in a routing record.

Equations

• Algebraic.MassProduction.Routing.keyBit keyWidth payloadWidth bit = ⟨↑bit, ⋯⟩

def Algebraic.MassProduction.Routing.tagBit (keyWidth payloadWidth : ℕ) : Fin (recordWidth keyWidth payloadWidth)

Index of the source/destination type bit.

Equations

• Algebraic.MassProduction.Routing.tagBit keyWidth payloadWidth = ⟨keyWidth, ⋯⟩

def Algebraic.MassProduction.Routing.payloadBit (keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) : Fin (recordWidth keyWidth payloadWidth)

Index of one payload bit in a routing record.

Equations

• Algebraic.MassProduction.Routing.payloadBit keyWidth payloadWidth bit = ⟨keyWidth + 1 + ↑bit, ⋯⟩

def Algebraic.MassProduction.Routing.packedRecordKey {keyWidth payloadWidth : ℕ} (record : Fin (recordWidth keyWidth payloadWidth) → Bool) : Fin keyWidth → Bool

Key projection from one standalone packed record.

Equations

• Algebraic.MassProduction.Routing.packedRecordKey record bit = record (Algebraic.MassProduction.Routing.keyBit keyWidth payloadWidth bit)

def Algebraic.MassProduction.Routing.packedRecordTag {keyWidth payloadWidth : ℕ} (record : Fin (recordWidth keyWidth payloadWidth) → Bool) : Bool

Type tag from one standalone packed record.

Equations

• Algebraic.MassProduction.Routing.packedRecordTag record = record (Algebraic.MassProduction.Routing.tagBit keyWidth payloadWidth)

def Algebraic.MassProduction.Routing.packedRecordPayload {keyWidth payloadWidth : ℕ} (record : Fin (recordWidth keyWidth payloadWidth) → Bool) : Fin payloadWidth → Bool

Payload projection from one standalone packed record.

Equations

• Algebraic.MassProduction.Routing.packedRecordPayload record bit = record (Algebraic.MassProduction.Routing.payloadBit keyWidth payloadWidth bit)

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

Key projection from one record in a flat routing array.

Equations

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

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

Type tag of one record in a flat routing array.

Equations

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

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

Payload projection from one record in a flat routing array.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.packedRecordKey_flatRecords {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : packedRecordKey (Sorting.flatRecords input record) = recordKey input record

@[simp]

theorem Algebraic.MassProduction.Routing.packedRecordTag_flatRecords {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : packedRecordTag (Sorting.flatRecords input record) = recordTag input record

@[simp]

theorem Algebraic.MassProduction.Routing.packedRecordPayload_flatRecords {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : packedRecordPayload (Sorting.flatRecords input record) = recordPayload input record

def Algebraic.MassProduction.Routing.predecessor {depth : ℕ} (record : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑record) : Fin (Sorting.networkRecords depth)

The record immediately before a positive array position.

Equations

• Algebraic.MassProduction.Routing.predecessor record positive = ⟨↑record - 1, ⋯⟩

def Algebraic.MassProduction.Routing.bitEqualExpression {n : ℕ} (left right : Fin n) : DeMorgan.Expression n

XNOR of two selected array inputs.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.bitEqualExpression_eval_eq_true_iff {n : ℕ} (left right : Fin n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (bitEqualExpression left right) = true ↔ input left = input right

@[simp]

theorem Algebraic.MassProduction.Routing.bitEqualExpression_standardCost {n : ℕ} (left right : Fin n) : (bitEqualExpression left right).standardCost = 5

def Algebraic.MassProduction.Routing.bitEqualsConstantExpression {n : ℕ} (expected : Bool) (input : Fin n) : DeMorgan.Expression n

Test one selected input bit against a hardwired Boolean tag.

Equations

• Algebraic.MassProduction.Routing.bitEqualsConstantExpression expected input = if expected = true then Algebraic.DeMorgan.Expression.input input else (Algebraic.DeMorgan.Expression.input input).not

@[simp]

theorem Algebraic.MassProduction.Routing.bitEqualsConstantExpression_eval_eq_true_iff {n : ℕ} (expected : Bool) (index : Fin n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (bitEqualsConstantExpression expected index) = true ↔ input index = expected

theorem Algebraic.MassProduction.Routing.bitEqualsConstantExpression_standardCost_le {n : ℕ} (expected : Bool) (index : Fin n) : (bitEqualsConstantExpression expected index).standardCost ≤ 1

def Algebraic.MassProduction.Routing.recordKeysEqualExpression (depth keyWidth payloadWidth : ℕ) (left right : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

Equality test for the keys of two records.

Equations

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

theorem Algebraic.MassProduction.Routing.recordKeysEqualExpression_eval_eq_true_iff {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (left right : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression.eval input (recordKeysEqualExpression depth keyWidth payloadWidth left right) = true ↔ recordKey input left = recordKey input right

@[simp]

theorem Algebraic.MassProduction.Routing.recordKeysEqualExpression_standardCost {depth keyWidth payloadWidth : ℕ} (left right : Fin (Sorting.networkRecords depth)) : (recordKeysEqualExpression depth keyWidth payloadWidth left right).standardCost = 6 * keyWidth

def Algebraic.MassProduction.Routing.predecessorMatchExpression (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) : DeMorgan.Expression (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

Guard saying that current is a destination immediately preceded by a same-key source record.

Equations

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

theorem Algebraic.MassProduction.Routing.predecessorMatchExpression_eval_eq_true_iff {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) : DeMorgan.Expression.eval input (predecessorMatchExpression depth keyWidth payloadWidth sourceTag destinationTag current positive) = true ↔ recordKey input (predecessor current positive) = recordKey input current ∧ recordTag input (predecessor current positive) = sourceTag ∧ recordTag input current = destinationTag

theorem Algebraic.MassProduction.Routing.predecessorMatchExpression_standardCost_le {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) : (predecessorMatchExpression depth keyWidth payloadWidth sourceTag destinationTag current positive).standardCost ≤ 6 * keyWidth + 4

def Algebraic.MassProduction.Routing.predecessorCopyOutputExpression (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) (output : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))) : DeMorgan.Expression (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

One output bit of a guarded predecessor-copy pass. Keys and tags are preserved. Payload bits of a matched destination copy the predecessor; otherwise payload is the fixed dummy value false.

Equations

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

def Algebraic.MassProduction.Routing.predecessorCopyBits (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool

Semantic guarded predecessor-copy pass.

Equations

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

@[reducible]

def Algebraic.MassProduction.Routing.predecessorCopyOutputGateCount (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) (output : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))) : ℕ

Gate count emitted for one output formula.

Equations

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

def Algebraic.MassProduction.Routing.predecessorCopyCircuit (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) : Circuit DeMorgan.signature (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

Explicit circuit implementing one complete predecessor-copy pass.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.predecessorCopyCircuit_size (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) : (predecessorCopyCircuit depth keyWidth payloadWidth sourceTag destinationTag).size = ∑ output : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)), predecessorCopyOutputGateCount depth keyWidth payloadWidth sourceTag destinationTag output

@[simp]

theorem Algebraic.MassProduction.Routing.predecessorCopyCircuit_eval {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : (predecessorCopyCircuit depth keyWidth payloadWidth sourceTag destinationTag).eval DeMorgan.interpretation input = predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input

@[simp]

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordKey {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordKey (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) record = recordKey input record

A predecessor-copy pass preserves every key bit.

@[simp]

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordTag {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordTag (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) record = recordTag input record

A predecessor-copy pass preserves every type tag.

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordPayload_of_positive {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) : recordPayload (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) current = if DeMorgan.Expression.eval input (predecessorMatchExpression depth keyWidth payloadWidth sourceTag destinationTag current positive) = true then recordPayload input (predecessor current positive) else fun (x : Fin payloadWidth) => false

At a positive position, every payload bit is selected by the same same-key/source/destination guard.

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordPayload_zero {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (atZero : ↑current = 0) : recordPayload (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) current = fun (x : Fin payloadWidth) => false

The first record has no predecessor and receives the fixed dummy payload.

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordPayload_of_match {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) (sameKey : recordKey input (predecessor current positive) = recordKey input current) (previousTag : recordTag input (predecessor current positive) = sourceTag) (currentTag : recordTag input current = destinationTag) : recordPayload (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) current = recordPayload input (predecessor current positive)

A correctly tagged same-key predecessor is copied exactly.

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordPayload_of_no_match {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) (notMatch : ¬(recordKey input (predecessor current positive) = recordKey input current ∧ recordTag input (predecessor current positive) = sourceTag ∧ recordTag input current = destinationTag)) : recordPayload (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) current = fun (x : Fin payloadWidth) => false

If the predecessor match condition fails, the destination receives the fixed dummy payload.

theorem Algebraic.MassProduction.Routing.predecessorCopyOutputExpression_standardCost_le {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (output : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))) : (predecessorCopyOutputExpression depth keyWidth payloadWidth sourceTag destinationTag output).standardCost ≤ 12 * keyWidth + 12

theorem Algebraic.MassProduction.Routing.predecessorCopyCircuit_cost_le {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) : (predecessorCopyCircuit depth keyWidth payloadWidth sourceTag destinationTag).cost DeMorgan.standardCost ≤ Sorting.networkBits depth (recordWidth keyWidth payloadWidth) * (12 * keyWidth + 12)

One pass has linear record-array size and linear dependence on key width.

theorem Algebraic.MassProduction.Routing.keyAndTagFitsRecord (keyWidth payloadWidth : ℕ) : keyWidth + 1 ≤ recordWidth keyWidth payloadWidth

The key together with its following tag fits in a routing record.

@[reducible]

def Algebraic.MassProduction.Routing.sortedPredecessorCopyGateCount (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) : ℕ

Gate count of a complete sort-then-predecessor-match pass.

Equations

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

def Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuit (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) : Circuit DeMorgan.signature (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

One complete scatter-match or gather-match pass: sort by (key, tag) and perform the guarded predecessor copy.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuit_size (depth keyWidth payloadWidth : ℕ) (sourceTag destinationTag : Bool) : (sortedPredecessorCopyCircuit depth keyWidth payloadWidth sourceTag destinationTag).size = sortedPredecessorCopyGateCount depth keyWidth payloadWidth sourceTag destinationTag

def Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuitOrdered (depth keyWidth payloadWidth : ℕ) (ascending sourceTag destinationTag : Bool) : Circuit DeMorgan.signature (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

Direction-parameterized match pass. Descending order with source tag true and destination tag false is useful when a subsequent canonical sort must place destination records first without negating the tag bit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuitOrdered_size (depth keyWidth payloadWidth : ℕ) (ascending sourceTag destinationTag : Bool) : (sortedPredecessorCopyCircuitOrdered depth keyWidth payloadWidth ascending sourceTag destinationTag).size = sortedPredecessorCopyGateCount depth keyWidth payloadWidth sourceTag destinationTag

@[simp]

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuitOrdered_eval {depth keyWidth payloadWidth : ℕ} (ascending sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : (sortedPredecessorCopyCircuitOrdered depth keyWidth payloadWidth ascending sourceTag destinationTag).eval DeMorgan.interpretation input = predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag (Sorting.bitonicSortBits ⋯ depth ascending input)

@[simp]

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuit_eval {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : (sortedPredecessorCopyCircuit depth keyWidth payloadWidth sourceTag destinationTag).eval DeMorgan.interpretation input = predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag (Sorting.bitonicSortBits ⋯ depth true input)

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopy_sort_recordsPermute {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : Sorting.FlatRecordsPermute (Sorting.bitonicSortBits ⋯ depth true input) input

The sorting half of a match pass preserves every complete routing record before the local payload update.

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuit_cost_le {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) : (sortedPredecessorCopyCircuit depth keyWidth payloadWidth sourceTag destinationTag).cost DeMorgan.standardCost ≤ depth * depth * Sorting.networkRecords depth * (2 * recordWidth keyWidth payloadWidth * (2 * ((keyWidth + 1) * (6 * (keyWidth + 1) + 4)) + 4)) + Sorting.networkBits depth (recordWidth keyWidth payloadWidth) * (12 * keyWidth + 12)

Explicit cost ledger for one complete sort-and-match pass.

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuitOrdered_cost_le {depth keyWidth payloadWidth : ℕ} (ascending sourceTag destinationTag : Bool) : (sortedPredecessorCopyCircuitOrdered depth keyWidth payloadWidth ascending sourceTag destinationTag).cost DeMorgan.standardCost ≤ depth * depth * Sorting.networkRecords depth * (2 * recordWidth keyWidth payloadWidth * (2 * ((keyWidth + 1) * (6 * (keyWidth + 1) + 4)) + 4)) + Sorting.networkBits depth (recordWidth keyWidth payloadWidth) * (12 * keyWidth + 12)

The direction-parameterized pass has the same cost ledger.