Scatter and resource-stage assembly #
This module preserves grouped scheduler outputs while routing request suffixes to resource slots and evaluating every shorter resource circuit. It packages the scatter and resource bank as one independently reusable circuit stage, before any gather or decoding work.
Sequential scatter and resource evaluation #
noncomputable def
Algebraic.MassProduction.RoutingAssembly.scatterWithScheduleCircuit
{totalRequests groups requestsPerGroup width dimension paddingCount scatterDepth : ℕ}
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
:
Circuit DeMorgan.signature (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)
(scheduleBitCount groups requestsPerGroup dimension width + Sorting.networkBits scatterDepth
(Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth))
Preserve scheduler outputs alongside the routed scatter array.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.scatterWithScheduleCircuit_size
{totalRequests groups requestsPerGroup width dimension paddingCount scatterDepth : ℕ}
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
:
(scatterWithScheduleCircuit suffixWidth groupBitWidth capacity recordCount).size = (scatterRoutingCircuit suffixWidth groupBitWidth capacity recordCount).size
scatterWithScheduleCircuit has exactly the gates of scatterRoutingCircuit; the surrounding
wiring adds none.
theorem
Algebraic.MassProduction.RoutingAssembly.scatterWithScheduleCircuit_eval
{width totalRequests groups requestsPerGroup dimension paddingCount scatterDepth : ℕ}
(widthPositive : 0 < width)
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
(input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool)
:
(scatterWithScheduleCircuit suffixWidth groupBitWidth capacity recordCount).eval DeMorgan.interpretation input = Fin.append (scatterScheduleInput input)
(CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity (scatterScheduleInput input)
(scatterSuffixInput input)
(fun (_destination : Fin (2 ^ (groupBitWidth + dimension * width))) (_bit : Fin suffixWidth) => false)
(fun (_padding : Fin paddingCount) (_bit : Fin suffixWidth) => false) recordCount)
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.scatterWithScheduleCircuit_cost
{totalRequests groups requestsPerGroup width dimension paddingCount scatterDepth : ℕ}
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
:
(scatterWithScheduleCircuit suffixWidth groupBitWidth capacity recordCount).cost DeMorgan.standardCost = (CanonicalRouting.matchedCanonicalRoutingCircuit scatterDepth
(IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth).cost
DeMorgan.standardCost
@[reducible]
noncomputable def
Algebraic.MassProduction.RoutingAssembly.resourceStageInputCount
(groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth : ℕ)
:
Scheduler plus routed-scatter input consumed by resource evaluation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.MassProduction.RoutingAssembly.resourceStageScheduleInputIndex
{groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth : ℕ}
(index : Fin (scheduleBitCount groups requestsPerGroup dimension width))
:
Fin (resourceStageInputCount groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth)
Embed a scheduler bit into the combined resource-stage input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.MassProduction.RoutingAssembly.resourceStageScatterInputIndex
{scatterDepth groupBitWidth dimension width suffixWidth groups requestsPerGroup : ℕ}
(index :
Fin
(Sorting.networkBits scatterDepth
(Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)))
:
Fin (resourceStageInputCount groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth)
Embed a routed-scatter bit into the combined resource-stage input.
Equations
- Algebraic.MassProduction.RoutingAssembly.resourceStageScatterInputIndex index = Fin.natAdd (Algebraic.MassProduction.RoutingAssembly.scheduleBitCount groups requestsPerGroup dimension width) index
Instances For
noncomputable def
Algebraic.MassProduction.RoutingAssembly.resourceStageScheduleInput
{groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth : ℕ}
(input :
Fin (resourceStageInputCount groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth) → Bool)
:
Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool
Project the scheduler portion of a combined resource-stage input.
Equations
Instances For
noncomputable def
Algebraic.MassProduction.RoutingAssembly.resourceStageScatterInput
{groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth : ℕ}
(input :
Fin (resourceStageInputCount groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth) → Bool)
:
Fin
(Sorting.networkBits scatterDepth
(Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) →
Bool
Project the routed-scatter portion of a combined resource-stage input.
Equations
Instances For
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.resourceStageScheduleInput_append
{groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth : ℕ}
(schedule : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool)
(scatter :
Fin
(Sorting.networkBits scatterDepth
(Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) →
Bool)
:
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.resourceStageScatterInput_append
{groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth : ℕ}
(schedule : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool)
(scatter :
Fin
(Sorting.networkBits scatterDepth
(Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) →
Bool)
:
noncomputable def
Algebraic.MassProduction.RoutingAssembly.resourceStageCircuit
{groupBitWidth dimension width scatterDepth groups suffixWidth : ℕ}
(requestsPerGroup : ℕ)
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
:
Circuit DeMorgan.signature
(resourceStageInputCount groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth)
(scheduleBitCount groups requestsPerGroup dimension width + ResourceEvaluation.resourceBitCount dimension width * groups)
Preserve the schedule while evaluating every shorter resource circuit in
parallel on the routed scatter output. Its gates are exactly the resource circuits'
gates (resourceStageCircuit_size).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.resourceStageCircuit_size
{groupBitWidth dimension width scatterDepth groups suffixWidth : ℕ}
(requestsPerGroup : ℕ)
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
:
(resourceStageCircuit requestsPerGroup destinationFits resourceCircuits).size = ∑ member : Fin (ResourceEvaluation.resourceBitCount dimension width), (resourceCircuits member).size
The resource stage has exactly the resource circuits' gates combined; preserving the schedule and routing the scatter output are pure wiring.
theorem
Algebraic.MassProduction.RoutingAssembly.resourceStageCircuit_eval
{groupBitWidth dimension width scatterDepth groups suffixWidth requestsPerGroup : ℕ}
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
(input :
Fin (resourceStageInputCount groups requestsPerGroup dimension width scatterDepth groupBitWidth suffixWidth) → Bool)
:
(resourceStageCircuit requestsPerGroup destinationFits resourceCircuits).eval DeMorgan.interpretation input = Fin.append (resourceStageScheduleInput input)
((ResourceEvaluation.resourceBankCircuit destinationFits resourceCircuits).eval DeMorgan.interpretation
(resourceStageScatterInput input))
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.resourceStageCircuit_cost
{groupBitWidth dimension width scatterDepth groups suffixWidth requestsPerGroup : ℕ}
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
:
(resourceStageCircuit requestsPerGroup destinationFits resourceCircuits).cost DeMorgan.standardCost = ∑ member : Fin (ResourceEvaluation.resourceBitCount dimension width),
(resourceCircuits member).cost DeMorgan.standardCost
noncomputable def
Algebraic.MassProduction.RoutingAssembly.scatterResourceCircuit
{totalRequests groups requestsPerGroup width dimension paddingCount scatterDepth : ℕ}
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
:
Circuit DeMorgan.signature (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)
(scheduleBitCount groups requestsPerGroup dimension width + ResourceEvaluation.resourceBitCount dimension width * groups)
Scatter, retain its schedule, and evaluate the complete resource bank.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.scatterResourceCircuit_size
{totalRequests groups requestsPerGroup width dimension paddingCount scatterDepth : ℕ}
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
:
(scatterResourceCircuit suffixWidth groupBitWidth capacity recordCount destinationFits resourceCircuits).size = (scatterWithScheduleCircuit suffixWidth groupBitWidth capacity recordCount).size + (resourceStageCircuit requestsPerGroup destinationFits resourceCircuits).size
The exact gate count of scatterResourceCircuit.
theorem
Algebraic.MassProduction.RoutingAssembly.scatterResourceCircuit_eval
{width totalRequests groups requestsPerGroup dimension paddingCount scatterDepth : ℕ}
(widthPositive : 0 < width)
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
(input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool)
:
(scatterResourceCircuit suffixWidth groupBitWidth capacity recordCount destinationFits resourceCircuits).eval
DeMorgan.interpretation input = Fin.append (scatterScheduleInput input)
((ResourceEvaluation.resourceBankCircuit destinationFits resourceCircuits).eval DeMorgan.interpretation
(CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity (scatterScheduleInput input)
(scatterSuffixInput input)
(fun (_destination : Fin (2 ^ (groupBitWidth + dimension * width))) (_bit : Fin suffixWidth) => false)
(fun (_padding : Fin paddingCount) (_bit : Fin suffixWidth) => false) recordCount))
@[simp]
theorem
Algebraic.MassProduction.RoutingAssembly.scatterResourceCircuit_cost
{totalRequests groups requestsPerGroup width dimension paddingCount scatterDepth : ℕ}
(suffixWidth groupBitWidth : ℕ)
(capacity : totalRequests ≤ groups * requestsPerGroup)
(recordCount :
totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords scatterDepth)
(destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords scatterDepth)
(resourceCircuits :
Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups)
:
(scatterResourceCircuit suffixWidth groupBitWidth capacity recordCount destinationFits resourceCircuits).cost
DeMorgan.standardCost = (CanonicalRouting.matchedCanonicalRoutingCircuit scatterDepth
(IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth).cost
DeMorgan.standardCost + ∑ member : Fin (ResourceEvaluation.resourceBitCount dimension width),
(resourceCircuits member).cost DeMorgan.standardCost