Fixed-wire gather from evaluated resource slots

The gather source array contains one evaluated value for every canonical (group, point) key. Its destinations are the scheduled incidences, whose preserved metadata is their row-major (request, scalar) index. Matching routes each resource value back to its incidence; the metadata sort then puts incidence i on literal output record i.

def Algebraic.MassProduction.GatherRouting.resourceSourceMetadata {sourceCount : ℕ} (orderWidth : ℕ) (_source : Fin sourceCount) : Fin (orderWidth + 1) → Bool

Metadata attached to resource-source records is semantically irrelevant: source tags put them after every gather destination in the canonical pass.

Equations

• Algebraic.MassProduction.GatherRouting.resourceSourceMetadata orderWidth _source x✝ = false

noncomputable def Algebraic.MassProduction.GatherRouting.canonicalGatherBits {width totalRequests groups requestsPerGroup dimension valueWidth paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (resourceValues : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin valueWidth → Bool) (destinationValues : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width) → Fin valueWidth → Bool) (paddingValues : Fin paddingCount → Fin valueWidth → Bool) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : Fin (Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth)) → Bool

Canonically metadata-ordered gather output.

Equations

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

def Algebraic.MassProduction.GatherRouting.canonicalGatherCircuit (routingDepth groupBitWidth dimension width orderWidth valueWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth)) (Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth))

The reusable two-sort value-routing circuit underlying gather. Record assembly is kept explicit at the composition boundary.

Equations

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

@[simp]

theorem Algebraic.MassProduction.GatherRouting.canonicalGatherCircuit_size (routingDepth groupBitWidth dimension width orderWidth valueWidth : ℕ) : (canonicalGatherCircuit routingDepth groupBitWidth dimension width orderWidth valueWidth).size = (CanonicalMetadataRouting.matchedCanonicalRoutingCircuit routingDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth).size

canonicalGatherCircuit has exactly the gates of matchedCanonicalRoutingCircuit; the surrounding wiring adds none.

@[simp]

theorem Algebraic.MassProduction.GatherRouting.canonicalGatherCircuit_eval {routingDepth groupBitWidth dimension width orderWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth)) → Bool) : (canonicalGatherCircuit routingDepth groupBitWidth dimension width orderWidth valueWidth).eval DeMorgan.interpretation input = CanonicalMetadataRouting.matchedCanonicalRoutingBits routingDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth input

theorem Algebraic.MassProduction.GatherRouting.canonicalGatherCircuit_cost_le {routingDepth groupBitWidth dimension width orderWidth valueWidth : ℕ} : (canonicalGatherCircuit routingDepth groupBitWidth dimension width orderWidth valueWidth).cost DeMorgan.standardCost ≤ routingDepth * routingDepth * Sorting.networkRecords routingDepth * (2 * RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth * (2 * ((IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width + 1) * (6 * (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width + 1) + 4)) + 4)) + Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth) * (12 * IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width + 12) + (Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth) + routingDepth * routingDepth * Sorting.networkRecords routingDepth * (2 * RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) valueWidth * (2 * ((orderWidth + 1 + 1) * (6 * (orderWidth + 1 + 1) + 4)) + 4)))

theorem Algebraic.MassProduction.GatherRouting.canonicalGatherBits_routes_incidence {width groups groupBitWidth totalRequests orderWidth requestsPerGroup dimension valueWidth paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (groupFits : groups ≤ 2 ^ groupBitWidth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (targets : Fin totalRequests → Fin dimension → BinaryExtension width) (directions : Fin totalRequests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (pointFormula : ∀ (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), GroupedScheduler.requestScheduledLinePoint widthPositive capacity scheduleOutput request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (withinGroupDisjoint : ∀ (left right : Fin totalRequests), (GroupedScheduler.requestGroupSlot capacity left).1 = (GroupedScheduler.requestGroupSlot capacity right).1 → left ≠ right → Disjoint (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput left) (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput right)) (resourceValues : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin valueWidth → Bool) (destinationValues : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width) → Fin valueWidth → Bool) (paddingValues : Fin paddingCount → Fin valueWidth → Bool) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : have destinationFitsNetwork := ⋯; RoutingMetadata.recordValue (canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity scheduleOutput resourceValues destinationValues paddingValues recordCount) (Fin.castLE destinationFitsNetwork incidence) = resourceValues (IncidenceRouting.fullIncidenceDestination widthPositive groupBitWidth capacity scheduleOutput incidence)

Every scheduled incidence receives the value of its evaluated resource slot and lands at its row-major fixed output position.