Runtime-selected gather decoder

The fixed decoder chooses one field coordinate nonuniformly for every request. For the actual direct-product circuit that coordinate comes from the runtime prefix. This module appends a one-hot coordinate selector to the gather output and compiles the bilinear XOR

XOR_(scalar, bit) selector(request, bit) AND value(request, scalar, bit).

Thus the selected coordinate remains runtime data, while the cost stays linear in the number of gathered field bits. No type-class instances are introduced.

@[reducible]

def Algebraic.MassProduction.DynamicGatherDecoder.selectorBitCount (totalRequests valueWidth : ℕ) : ℕ

Number of one-hot selector bits appended after the gather records.

Equations

• Algebraic.MassProduction.DynamicGatherDecoder.selectorBitCount totalRequests valueWidth = totalRequests * valueWidth

@[reducible]

def Algebraic.MassProduction.DynamicGatherDecoder.inputCount (depth keyWidth metadataWidth valueWidth totalRequests : ℕ) : ℕ

Full input width: gather records followed by row-major selector bits.

Equations

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

noncomputable def Algebraic.MassProduction.DynamicGatherDecoder.gatheredInputIndex {totalRequests width depth valueWidth keyWidth metadataWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) (bit : Fin valueWidth) : Fin (inputCount depth keyWidth metadataWidth valueWidth totalRequests)

A gathered value wire, embedded in the left part of the decoder input.

Equations

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

def Algebraic.MassProduction.DynamicGatherDecoder.selectorInputIndex {totalRequests valueWidth : ℕ} (depth keyWidth metadataWidth : ℕ) (request : Fin totalRequests) (bit : Fin valueWidth) : Fin (inputCount depth keyWidth metadataWidth valueWidth totalRequests)

A row-major selector wire, embedded in the right part of the input.

Equations

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

def Algebraic.MassProduction.DynamicGatherDecoder.gatherInput {depth keyWidth metadataWidth valueWidth totalRequests : ℕ} (input : Fin (inputCount depth keyWidth metadataWidth valueWidth totalRequests) → Bool) : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool

Restrict the combined input to its gather-record prefix.

Equations

• Algebraic.MassProduction.DynamicGatherDecoder.gatherInput input index = input (Fin.castAdd (Algebraic.MassProduction.DynamicGatherDecoder.selectorBitCount totalRequests valueWidth) index)

def Algebraic.MassProduction.DynamicGatherDecoder.selectorInput {depth keyWidth metadataWidth valueWidth totalRequests : ℕ} (input : Fin (inputCount depth keyWidth metadataWidth valueWidth totalRequests) → Bool) (request : Fin totalRequests) (bit : Fin valueWidth) : Bool

Read one request's runtime one-hot selector bit.

Equations

• Algebraic.MassProduction.DynamicGatherDecoder.selectorInput input request bit = input (Algebraic.MassProduction.DynamicGatherDecoder.selectorInputIndex depth keyWidth metadataWidth request bit)

@[simp]

theorem Algebraic.MassProduction.DynamicGatherDecoder.gatherInput_append {depth keyWidth metadataWidth valueWidth totalRequests : ℕ} (gather : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (selectors : Fin (selectorBitCount totalRequests valueWidth) → Bool) : gatherInput (Fin.append gather selectors) = gather

@[simp]

theorem Algebraic.MassProduction.DynamicGatherDecoder.selectorInput_append {depth keyWidth metadataWidth valueWidth totalRequests : ℕ} (gather : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (selectors : Fin (selectorBitCount totalRequests valueWidth) → Bool) (request : Fin totalRequests) (bit : Fin valueWidth) : selectorInput (Fin.append gather selectors) request bit = selectors (finProdFinEquiv (request, bit))

noncomputable def Algebraic.MassProduction.DynamicGatherDecoder.decoderExpression {totalRequests width depth keyWidth metadataWidth valueWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin totalRequests) : Arithmetic.Expression Bool (inputCount depth keyWidth metadataWidth valueWidth totalRequests)

Bilinear decoding expression for one request.

Equations

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

@[reducible]

noncomputable def Algebraic.MassProduction.DynamicGatherDecoder.decoderGateCount {totalRequests width depth : ℕ} (keyWidth metadataWidth valueWidth : ℕ) (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin totalRequests) : ℕ

Gate count produced for one request.

Equations

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

noncomputable def Algebraic.MassProduction.DynamicGatherDecoder.circuit {totalRequests width depth keyWidth metadataWidth valueWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : Circuit DeMorgan.signature (inputCount depth keyWidth metadataWidth valueWidth totalRequests) totalRequests

Complete runtime-selected row-major gather decoder.

Equations

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

@[simp]

theorem Algebraic.MassProduction.DynamicGatherDecoder.circuit_size {totalRequests width depth keyWidth metadataWidth valueWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (circuit destinationFits).size = ∑ request : Fin totalRequests, decoderGateCount keyWidth metadataWidth valueWidth destinationFits request

@[simp]

theorem Algebraic.MassProduction.DynamicGatherDecoder.circuit_eval_apply {totalRequests width depth keyWidth metadataWidth valueWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (input : Fin (inputCount depth keyWidth metadataWidth valueWidth totalRequests) → Bool) (request : Fin totalRequests) : (circuit destinationFits).eval DeMorgan.interpretation input request = ∑ flat : Fin (LineEnumeration.nonzeroScalarCount width * valueWidth), have scalarAndBit := finProdFinEquiv.symm flat; selectorInput input request scalarAndBit.2 * RoutingMetadata.recordValue (gatherInput input) (Fin.castLE destinationFits (finProdFinEquiv (request, scalarAndBit.1))) scalarAndBit.2

theorem Algebraic.MassProduction.DynamicGatherDecoder.decoderExpression_cost {totalRequests width depth keyWidth metadataWidth valueWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin totalRequests) : (DeMorgan.ArithmeticExpression.circuit (decoderExpression destinationFits request)).cost DeMorgan.standardCost = LineEnumeration.nonzeroScalarCount width * valueWidth * 5

Exact De Morgan cost of one request's bilinear decoder.

@[simp]

theorem Algebraic.MassProduction.DynamicGatherDecoder.circuit_cost {totalRequests width depth keyWidth metadataWidth valueWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (circuit destinationFits).cost DeMorgan.standardCost = totalRequests * (LineEnumeration.nonzeroScalarCount width * valueWidth * 5)

The full runtime decoder remains linear in the gathered field bits.

theorem Algebraic.MassProduction.DynamicGatherDecoder.circuit_recovers {totalRequests width depth valueWidth keyWidth metadataWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (selectedBit : Fin totalRequests → Fin valueWidth) (input : Fin (inputCount depth keyWidth metadataWidth valueWidth totalRequests) → Bool) (incidenceValue : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width) → Fin valueWidth → Bool) (answer : Fin totalRequests → Bool) (valuesCorrect : ∀ (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)), RoutingMetadata.recordValue (gatherInput input) (Fin.castLE destinationFits incidence) = incidenceValue incidence) (selectorCorrect : ∀ (request : Fin totalRequests) (bit : Fin valueWidth), selectorInput input request bit = decide (bit = selectedBit request)) (xorRecovers : ∀ (request : Fin totalRequests), ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), incidenceValue (finProdFinEquiv (request, scalar)) (selectedBit request) = answer request) : (circuit destinationFits).eval DeMorgan.interpretation input = answer

A one-hot runtime selector reduces the bilinear decoder to the same coordinate XOR used by the fixed decoder.

theorem Algebraic.MassProduction.DynamicGatherDecoder.circuit_eval_append_oneHot {totalRequests width depth valueWidth keyWidth metadataWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (selectedBit : Fin totalRequests → Fin valueWidth) (gather : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : (circuit destinationFits).eval DeMorgan.interpretation (Fin.append gather fun (flat : Fin (selectorBitCount totalRequests valueWidth)) => have requestAndBit := finProdFinEquiv.symm flat; decide (requestAndBit.2 = selectedBit requestAndBit.1)) = (GatherDecoder.circuit destinationFits selectedBit).eval DeMorgan.interpretation gather

Appending a one-hot runtime selector makes the dynamic decoder extensionally equal to the corresponding fixed-coordinate decoder.