Runtime-selected pipeline assembly

This module preserves the runtime one-hot selectors beside the scheduled scatter input, runs scatter, resource evaluation, and gather, then performs dynamic coordinate selection. It proves exact agreement with the established fixed-selector pipeline and records the selector-decoding cost.

Dynamic scatter, evaluation, gather, and decoding

@[reducible]

noncomputable def Algebraic.MassProduction.RuntimePipeline.scheduledDataCount (groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ) : ℕ

Scheduler output, then row-major suffixes, then row-major selectors.

Equations

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

noncomputable def Algebraic.MassProduction.RuntimePipeline.scheduledScatterInputIndex {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (index : Fin (RoutingAssembly.scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)) : Fin (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth)

Embed the scheduler-and-suffix prefix consumed by scatter routing.

Equations

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

noncomputable def Algebraic.MassProduction.RuntimePipeline.scheduledSelectorInputIndex {totalRequests width groups requestsPerGroup dimension suffixWidth : ℕ} (selector : Fin (totalRequests * width)) : Fin (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth)

Embed the final selector block.

Equations

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

noncomputable def Algebraic.MassProduction.RuntimePipeline.scheduledScatterInput {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (input : Fin (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) : Fin (RoutingAssembly.scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool

Scheduler-and-suffix view of scheduled runtime data.

Equations

• Algebraic.MassProduction.RuntimePipeline.scheduledScatterInput input index = input (Algebraic.MassProduction.RuntimePipeline.scheduledScatterInputIndex index)

noncomputable def Algebraic.MassProduction.RuntimePipeline.scheduledSelectorInput {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (input : Fin (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) : Fin (totalRequests * width) → Bool

Selector view of scheduled runtime data.

Equations

• Algebraic.MassProduction.RuntimePipeline.scheduledSelectorInput input selector = input (Algebraic.MassProduction.RuntimePipeline.scheduledSelectorInputIndex selector)

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.scheduledScatterInput_append {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (schedule : Fin (RoutingAssembly.scheduleBitCount groups requestsPerGroup dimension width) → Bool) (suffixes : Fin (totalRequests * suffixWidth) → Bool) (selectors : Fin (totalRequests * width) → Bool) : scheduledScatterInput (Fin.append schedule (Fin.append suffixes selectors)) = Fin.append schedule suffixes

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.scheduledSelectorInput_append {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (schedule : Fin (RoutingAssembly.scheduleBitCount groups requestsPerGroup dimension width) → Bool) (suffixes : Fin (totalRequests * suffixWidth) → Bool) (selectors : Fin (totalRequests * width) → Bool) : scheduledSelectorInput (Fin.append schedule (Fin.append suffixes selectors)) = selectors

noncomputable def Algebraic.MassProduction.RuntimePipeline.gatherWithSelectorsCircuit {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : Circuit DeMorgan.signature (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth) (Sorting.networkBits gatherDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width) + totalRequests * width)

Preserve runtime selectors alongside the gathered incidence records.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.gatherWithSelectorsCircuit_size {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (gatherWithSelectorsCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).size = (RoutingAssembly.scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount ⋯ resourceCircuits gatherRecordCount).size

Carrying the runtime selectors alongside the gathered records is pure wiring.

theorem Algebraic.MassProduction.RuntimePipeline.gatherWithSelectorsCircuit_eval {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) (input : Fin (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) : (gatherWithSelectorsCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = have scatterDestinationFits := ⋯; Fin.append ((RoutingAssembly.scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount scatterDestinationFits resourceCircuits gatherRecordCount).eval DeMorgan.interpretation (scheduledScatterInput input)) (scheduledSelectorInput input)

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.gatherWithSelectorsCircuit_cost {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (gatherWithSelectorsCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost = (RoutingAssembly.scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount ⋯ resourceCircuits gatherRecordCount).cost DeMorgan.standardCost

noncomputable def Algebraic.MassProduction.RuntimePipeline.dynamicAssembledPipelineCircuit {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : Circuit DeMorgan.signature (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth) totalRequests

Scatter, resource evaluation, gather, and runtime-selected decoding.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.dynamicAssembledPipelineCircuit_size {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (dynamicAssembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).size = (gatherWithSelectorsCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).size + ∑ request : Fin totalRequests, DynamicGatherDecoder.decoderGateCount (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width ⋯ request

The dynamic pipeline has exactly the gates of the gather stage followed by one runtime decoder per request.

theorem Algebraic.MassProduction.RuntimePipeline.dynamicAssembledPipelineCircuit_eq_fixed {Prefix : Type u} {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) (input : Fin (scheduledDataCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) (selectorCorrect : ∀ (request : Fin totalRequests) (bit : Fin width), scheduledSelectorInput input (finProdFinEquiv (request, bit)) = decide (bit = (placement (requestSource request)).2)) : (dynamicAssembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = (RoutingAssembly.assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation (scheduledScatterInput input)

When the appended selectors are one-hot at the specified coordinates, the dynamic pipeline is exactly the established fixed-selector pipeline.

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.dynamicAssembledPipelineCircuit_cost {groups totalRequests width requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (suffixWidth groupBitWidth orderWidth : ℕ) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (dynamicAssembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost = (gatherWithSelectorsCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost + totalRequests * (LineEnumeration.nonzeroScalarCount width * width * 5)