Two-pass scatter and gather stages

Both halves of the manuscript's four-pass router have the same shape. First sort by (key, tag) and copy a matching predecessor's payload; then sort the updated complete records by a caller-selected canonical output tuple. This module composes the already verified circuits, records the exact semantics, and gives the additive gate ledger. Instantiating it once for scatter and once for gather accounts for all four sorting passes.

@[reducible]

def Algebraic.MassProduction.Routing.matchThenOrderGateCount (depth keyWidth payloadWidth outputKeyWidth : ℕ) (_outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) : ℕ

Gate count emitted by a match pass followed by a canonical-order pass.

Equations

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

def Algebraic.MassProduction.Routing.matchThenOrderCircuit (depth keyWidth payloadWidth outputKeyWidth : ℕ) (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) : Circuit DeMorgan.signature (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (recordWidth keyWidth payloadWidth))

One complete two-pass stage of the router. outputOrder maps the virtual canonical-order key and payload positions back to the physical record layout.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.matchThenOrderCircuit_size (depth keyWidth payloadWidth outputKeyWidth : ℕ) (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) : (matchThenOrderCircuit depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits sourceTag destinationTag).size = matchThenOrderGateCount depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits sourceTag destinationTag

def Algebraic.MassProduction.Routing.matchThenOrderBits (depth keyWidth payloadWidth outputKeyWidth : ℕ) (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool

Pure semantics of one match-then-order stage.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.matchThenOrderCircuit_eval {keyWidth payloadWidth outputKeyWidth depth : ℕ} (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : (matchThenOrderCircuit depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits sourceTag destinationTag).eval DeMorgan.interpretation input = matchThenOrderBits depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits sourceTag destinationTag input

theorem Algebraic.MassProduction.Routing.matchThenOrderCircuit_keysSorted {keyWidth payloadWidth outputKeyWidth depth : ℕ} (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : Sorting.FlatKeysSortedBy outputOrder outputKeyFits true ((matchThenOrderCircuit depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits sourceTag destinationTag).eval DeMorgan.interpretation input)

The second pass establishes its selected canonical output order.

theorem Algebraic.MassProduction.Routing.matchThenOrderCircuit_recordsPermuteMatched {keyWidth payloadWidth outputKeyWidth depth : ℕ} (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) : Sorting.FlatRecordsPermute ((matchThenOrderCircuit depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits sourceTag destinationTag).eval DeMorgan.interpretation input) (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag (Sorting.bitonicSortBits ⋯ depth true input))

The canonical-order pass moves complete records and therefore preserves every payload produced by the matching pass.

theorem Algebraic.MassProduction.Routing.matchThenOrderCircuit_cost_le {keyWidth payloadWidth outputKeyWidth depth : ℕ} (outputOrder : Equiv.Perm (Fin (recordWidth keyWidth payloadWidth))) (outputKeyFits : outputKeyWidth ≤ recordWidth keyWidth payloadWidth) (sourceTag destinationTag : Bool) : (matchThenOrderCircuit depth keyWidth payloadWidth outputKeyWidth outputOrder outputKeyFits 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) + depth * depth * Sorting.networkRecords depth * (2 * recordWidth keyWidth payloadWidth * (2 * (outputKeyWidth * (6 * outputKeyWidth + 4)) + 4))

Explicit cost of a two-pass stage: one (key,tag) sorter, one guarded linear scan, and one caller-selected canonical-order sorter.

def Algebraic.MassProduction.Routing.fourPassRoutingCost (depth keyWidth scatterPayloadWidth gatherPayloadWidth scatterOutputKeyWidth gatherOutputKeyWidth : ℕ) (scatterOrder : Equiv.Perm (Fin (recordWidth keyWidth scatterPayloadWidth))) (gatherOrder : Equiv.Perm (Fin (recordWidth keyWidth gatherPayloadWidth))) (scatterKeyFits : scatterOutputKeyWidth ≤ recordWidth keyWidth scatterPayloadWidth) (gatherKeyFits : gatherOutputKeyWidth ≤ recordWidth keyWidth gatherPayloadWidth) : ℕ

The combined gate cost of the scatter pair and gather pair. The resource evaluation circuits sit between these stages and are intentionally not part of this routing-only ledger.

Equations

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