Gather routing assembly

This module turns a grouped scheduler output and a complete resource bank into the fixed metadata-bearing record layout consumed by canonical gather routing. Record assembly is zero-cost wiring; the routing network returns resource values to incidence order.

Gather inputs

@[reducible]

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherAssemblyInputCount (groups requestsPerGroup dimension width : ℕ) : ℕ

Scheduler output followed by the complete resource-bank output.

Equations

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

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherScheduleInputIndex {groups requestsPerGroup dimension width : ℕ} (index : Fin (scheduleBitCount groups requestsPerGroup dimension width)) : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width)

Embed one scheduler bit in the gather-assembly input.

Equations

• Algebraic.MassProduction.RoutingAssembly.gatherScheduleInputIndex index = Fin.castAdd (Algebraic.MassProduction.ResourceEvaluation.resourceBitCount dimension width * groups) index

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherBankInputIndex {dimension width groups requestsPerGroup : ℕ} (index : Fin (ResourceEvaluation.resourceBitCount dimension width * groups)) : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width)

Embed one resource-bank output bit in the gather-assembly input.

Equations

• Algebraic.MassProduction.RoutingAssembly.gatherBankInputIndex index = Fin.natAdd (Algebraic.MassProduction.RoutingAssembly.scheduleBitCount groups requestsPerGroup dimension width) index

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherScheduleInput {groups requestsPerGroup dimension width : ℕ} (input : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width) → Bool) : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool

Scheduler view of a gather-assembly input.

Equations

• Algebraic.MassProduction.RoutingAssembly.gatherScheduleInput input index = input (Algebraic.MassProduction.RoutingAssembly.gatherScheduleInputIndex index)

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherBankInput {groups requestsPerGroup dimension width : ℕ} (input : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width) → Bool) : Fin (ResourceEvaluation.resourceBitCount dimension width * groups) → Bool

Resource-bank view of a gather-assembly input.

Equations

• Algebraic.MassProduction.RoutingAssembly.gatherBankInput input index = input (Algebraic.MassProduction.RoutingAssembly.gatherBankInputIndex index)

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.gatherScheduleInput_append {groups requestsPerGroup dimension width : ℕ} (schedule : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool) (bank : Fin (ResourceEvaluation.resourceBitCount dimension width * groups) → Bool) : gatherScheduleInput (Fin.append schedule bank) = schedule

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.gatherBankInput_append {groups requestsPerGroup dimension width : ℕ} (schedule : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool) (bank : Fin (ResourceEvaluation.resourceBitCount dimension width * groups) → Bool) : gatherBankInput (Fin.append schedule bank) = bank

Zero-cost record assembly

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherSourceKeyWiring {inputs : ℕ} (groupBitWidth dimension width : ℕ) (source : Fin (2 ^ (groupBitWidth + dimension * width))) : Fin (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) → DeMorgan.Wiring inputs

Every full resource-source key is a construction-time constant.

Equations

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

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherSourcePayloadWiring {groups dimension width requestsPerGroup : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (source : Fin (2 ^ (groupBitWidth + dimension * width))) : Fin (orderWidth + 1 + width) → DeMorgan.Wiring (gatherAssemblyInputCount groups requestsPerGroup dimension width)

The resource value attached to a full-key source is selected directly from the corresponding resource-bank output. Invalid group encodings use the same fixed group-zero convention as resourceValuesFromBank.

Equations

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

theorem Algebraic.MassProduction.RoutingAssembly.gatherSourcePayloadWiring_eval {groups requestsPerGroup dimension width : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (input : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width) → Bool) (source : Fin (2 ^ (groupBitWidth + dimension * width))) : (fun (bit : Fin (orderWidth + 1 + width)) => DeMorgan.Wiring.eval input (gatherSourcePayloadWiring groupsPositive groupBitWidth orderWidth source bit)) = Fin.append (GatherRouting.resourceSourceMetadata orderWidth source) (ResourceEvaluation.resourceValuesFromBank groupsPositive groupBitWidth dimension width (gatherBankInput input) source)

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherDestinationKeyWiring {totalRequests groups requestsPerGroup width dimension : ℕ} (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) → DeMorgan.Wiring (gatherAssemblyInputCount groups requestsPerGroup dimension width)

A gather destination uses the same scheduled matching key as the corresponding scatter source.

Equations

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

theorem Algebraic.MassProduction.RoutingAssembly.gatherDestinationKeyWiring_eval {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (input : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : (fun (bit : Fin (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width)) => DeMorgan.Wiring.eval input (gatherDestinationKeyWiring groupBitWidth capacity incidence bit)) = IncidenceRouting.scheduledIncidenceKeyBits widthPositive groupBitWidth capacity (gatherScheduleInput input) incidence

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherDestinationPayloadWiring {totalRequests width orderWidth inputs : ℕ} (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin (orderWidth + 1 + width) → DeMorgan.Wiring inputs

Destination ordering metadata is constant and its unused value field is initialized to zero.

Equations

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

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherPaddingPayloadWiring {inputs : ℕ} (orderWidth width : ℕ) : Fin (orderWidth + 1 + width) → DeMorgan.Wiring inputs

Gather padding uses a reserved metadata marker and a zero value.

Equations

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

theorem Algebraic.MassProduction.RoutingAssembly.gatherDestinationPayloadWiring_eval {totalRequests width orderWidth inputs : ℕ} (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (input : Fin inputs → Bool) : (fun (bit : Fin (orderWidth + 1 + width)) => DeMorgan.Wiring.eval input (gatherDestinationPayloadWiring incidenceFits incidence bit)) = Fin.append (CanonicalMetadataRouting.destinationOrderMetadata incidenceFits incidence) fun (_bit : Fin width) => false

theorem Algebraic.MassProduction.RoutingAssembly.gatherPaddingPayloadWiring_eval {inputs : ℕ} (orderWidth width : ℕ) (input : Fin inputs → Bool) : (fun (bit : Fin (orderWidth + 1 + width)) => DeMorgan.Wiring.eval input (gatherPaddingPayloadWiring orderWidth width bit)) = Fin.append (paddingRoutingKey fun (x : Fin orderWidth) => false) fun (_bit : Fin width) => false

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherAssemblySpecification {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1 + width))) → DeMorgan.Wiring (gatherAssemblyInputCount groups requestsPerGroup dimension width)

Pure wiring specification for the gather-routing input array.

Equations

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

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherAssemblyCircuit {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : Circuit DeMorgan.signature (gatherAssemblyInputCount groups requestsPerGroup dimension width) (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1 + width)))

Gather record assembly uses only wire selection and constants.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.gatherAssemblyCircuit_size {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : (gatherAssemblyCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).size = ∑ output : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1 + width))), (gatherAssemblySpecification groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount output).expression.gateCount

The exact gate count of gatherAssemblyCircuit.

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.gatherAssemblyCircuit_cost {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : (gatherAssemblyCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).cost DeMorgan.standardCost = 0

theorem Algebraic.MassProduction.RoutingAssembly.gatherAssemblyCircuit_eval {groups width totalRequests requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (widthPositive : 0 < width) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) (input : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width) → Bool) : (gatherAssemblyCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).eval DeMorgan.interpretation input = Routing.routingInputBits (IncidenceRouting.fullResourceDestinationKeyBits groupBitWidth dimension width) (fun (source : Fin (2 ^ (groupBitWidth + dimension * width))) => Fin.append (GatherRouting.resourceSourceMetadata orderWidth source) (ResourceEvaluation.resourceValuesFromBank groupsPositive groupBitWidth dimension width (gatherBankInput input) source)) (IncidenceRouting.scheduledIncidenceKeyBits widthPositive groupBitWidth capacity (gatherScheduleInput input)) (fun (destination : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) => Fin.append (CanonicalMetadataRouting.destinationOrderMetadata incidenceFits destination) fun (_bit : Fin width) => false) (fun (_padding : Fin paddingCount) => IncidenceRouting.incidencePaddingKey groupBitWidth dimension width) (fun (_padding : Fin paddingCount) => Fin.append (paddingRoutingKey fun (x : Fin orderWidth) => false) fun (_bit : Fin width) => false) recordCount

Routed gather

noncomputable def Algebraic.MassProduction.RoutingAssembly.gatherRoutingCircuit {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : Circuit DeMorgan.signature (gatherAssemblyInputCount groups requestsPerGroup dimension width) (Sorting.networkBits routingDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width))

Complete metadata-preserving gather routing, including zero-cost record assembly.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.gatherRoutingCircuit_size {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : (gatherRoutingCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).size = (gatherAssemblyCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).size + (CanonicalMetadataRouting.matchedCanonicalRoutingCircuit routingDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width).size

The exact gate count of gatherRoutingCircuit.

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.gatherRoutingCircuit_cost {groups totalRequests width requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) : (gatherRoutingCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).cost DeMorgan.standardCost = (CanonicalMetadataRouting.matchedCanonicalRoutingCircuit routingDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width).cost DeMorgan.standardCost

theorem Algebraic.MassProduction.RoutingAssembly.gatherRoutingCircuit_eval {groups width totalRequests requestsPerGroup dimension paddingCount routingDepth : ℕ} (groupsPositive : 0 < groups) (widthPositive : 0 < width) (groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + paddingCount = Sorting.networkRecords routingDepth) (input : Fin (gatherAssemblyInputCount groups requestsPerGroup dimension width) → Bool) : (gatherRoutingCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity recordCount).eval DeMorgan.interpretation input = GatherRouting.canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity (gatherScheduleInput input) (ResourceEvaluation.resourceValuesFromBank groupsPositive groupBitWidth dimension width (gatherBankInput input)) (fun (_destination : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (_bit : Fin width) => false) (fun (_padding : Fin paddingCount) (_bit : Fin width) => false) recordCount