Fixed-wire line decoder

Gather places incidence (request, scalar) at its row-major record index. The decoder therefore needs no compaction or dynamic lookup: for each request it XORs the selected field-bit coordinate across all nonzero scalars.

noncomputable def Algebraic.MassProduction.GatherDecoder.gatheredValueInputIndex {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 (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))

Physical gather-input wire holding one selected incidence value bit.

Equations

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

noncomputable def Algebraic.MassProduction.GatherDecoder.decoderExpression {totalRequests width depth valueWidth keyWidth metadataWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (selectedBit : Fin totalRequests → Fin valueWidth) (request : Fin totalRequests) : Arithmetic.Expression Bool (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))

XOR expression for one request's selected field coordinate.

Equations

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

@[reducible]

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

Gate count emitted by translating one request's XOR expression.

Equations

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

noncomputable def Algebraic.MassProduction.GatherDecoder.circuit {totalRequests width depth valueWidth keyWidth metadataWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (selectedBit : Fin totalRequests → Fin valueWidth) : Circuit DeMorgan.signature (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) totalRequests

Complete row-major gather decoder.

Equations

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

@[simp]

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

@[simp]

theorem Algebraic.MassProduction.GatherDecoder.circuit_eval_apply {totalRequests width depth valueWidth keyWidth metadataWidth : ℕ} (destinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (selectedBit : Fin totalRequests → Fin valueWidth) (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (request : Fin totalRequests) : (circuit destinationFits selectedBit).eval DeMorgan.interpretation input request = ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), RoutingMetadata.recordValue input (Fin.castLE destinationFits (finProdFinEquiv (request, scalar))) (selectedBit request)

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

@[simp]

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

The decoder ledger is linear in the number of incidences.

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

Any fixed-wire incidence-value invariant immediately lifts to exact per-request XOR recovery.