Runtime-prefix mass-production pipeline

Building on the focused request, scheduling, and dynamic-pipeline layers, this module replaces the hardwired-prefix front end of RoutingAssembly. Every request supplies its prefix and suffix at runtime. The prefix determines both its tensor-code target point and a one-hot basis-coordinate selector; the suffix is passed unchanged to the routed resource bank.

All reindexing and padding layers are explicit zero-gate wiring circuits. No type-class instances are introduced.

Complete runtime-prefix assembly

def Algebraic.MassProduction.RuntimePipeline.runtimeSuffixArray {totalRequests prefixWidth suffixWidth : ℕ} (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) : Fin (totalRequests * suffixWidth) → Bool

Row-major suffix array of the original runtime request input.

Equations

• Algebraic.MassProduction.RuntimePipeline.runtimeSuffixArray input flat = Algebraic.MassProduction.RuntimePipeline.requestSuffix input (finProdFinEquiv.symm flat).1 (finProdFinEquiv.symm flat).2

noncomputable def Algebraic.MassProduction.RuntimePipeline.runtimeSelectorArray {prefixWidth dimension width totalRequests suffixWidth : ℕ} (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) : Fin (totalRequests * width) → Bool

Row-major one-hot selectors determined by all runtime prefixes.

Equations

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

theorem Algebraic.MassProduction.RuntimePipeline.processedSuffixArray_requestDataArray {width dimension totalRequests prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) : processedSuffixArray ((requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input) = runtimeSuffixArray input

theorem Algebraic.MassProduction.RuntimePipeline.processedSelectorArray_requestDataArray {width dimension prefixWidth totalRequests suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) : processedSelectorArray ((requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input) = runtimeSelectorArray packingFits input

noncomputable def Algebraic.MassProduction.RuntimePipeline.runtimeScheduleSuffixSelectorCircuit (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) : Circuit DeMorgan.signature (totalRequests * requestInputCount prefixWidth suffixWidth) (groups * (GroupedScheduler.requestGroupSize totalRequests groups * SchedulerIteration.lineBitWidth dimension width) + suffixSelectorCount totalRequests suffixWidth width)

Runtime packing for every request, followed by deterministic grouped scheduling and retention of every suffix and selector bit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.runtimeScheduleSuffixSelectorCircuit_size (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) : (runtimeScheduleSuffixSelectorCircuit totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth widthPositive gridPositive allFit dummyTarget).size = (requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).size + (scheduleSuffixSelectorCircuit totalRequests groups (GroupedScheduler.requestGroupSize totalRequests groups) dimension width suffixWidth schedulerDepth widthPositive allFit dummyTarget).size

The exact gate count of runtimeScheduleSuffixSelectorCircuit.

theorem Algebraic.MassProduction.RuntimePipeline.runtimeScheduleSuffixSelectorCircuit_eval {width dimension groups prefixWidth totalRequests schedulerDepth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) : (runtimeScheduleSuffixSelectorCircuit totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth widthPositive gridPositive allFit dummyTarget).eval DeMorgan.interpretation input = let groupSize := GroupedScheduler.requestGroupSize totalRequests groups; have capacity := ⋯; have paddedTargets := GroupedScheduler.paddedGroupedTargets capacity (requestTarget widthPositive packingFits input) dummyTarget; Fin.append (GroupedScheduler.groupedScheduleOutput dimension widthPositive schedulerDepth groups groupSize allFit paddedTargets) (Fin.append (runtimeSuffixArray input) (runtimeSelectorArray packingFits input))

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.runtimeScheduleSuffixSelectorCircuit_cost {width dimension totalRequests groups schedulerDepth prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) : (runtimeScheduleSuffixSelectorCircuit totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth widthPositive gridPositive allFit dummyTarget).cost DeMorgan.standardCost = (GroupedScheduler.groupedScheduleCircuit dimension widthPositive schedulerDepth groups (GroupedScheduler.requestGroupSize totalRequests groups) allFit).cost DeMorgan.standardCost + totalRequests * (RuntimePacking.circuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost

def Algebraic.MassProduction.RuntimePipeline.requestFunction {prefixWidth suffixWidth : ℕ} (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) : ScalarFunction Bool (requestInputCount prefixWidth suffixWidth)

The complete exact mass-production circuit with runtime prefix and suffix bits for every request.

Equations

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

theorem Algebraic.MassProduction.RuntimePipeline.directProduct_requestFunction_apply {prefixWidth suffixWidth totalRequests : ℕ} (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) (request : Fin totalRequests) : directProduct (requestFunction function) totalRequests input request = function (requestSource input request) (requestSuffix input request)

noncomputable def Algebraic.MassProduction.RuntimePipeline.circuit {width dimension groups totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (prefixWidth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (dummyTarget : Fin dimension → BinaryExtension width) (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 (totalRequests * requestInputCount prefixWidth suffixWidth) totalRequests

Complete runtime mass-production circuit: schedule, scatter, evaluate, gather, and decode every requested output.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.circuit_size {width dimension groups totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (prefixWidth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (dummyTarget : Fin dimension → BinaryExtension width) (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 prefixWidth widthPositive gridPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).size = (runtimeScheduleSuffixSelectorCircuit totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth widthPositive gridPositive allFit dummyTarget).size + (dynamicAssembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits ⋯ scatterRecordCount resourceCircuits gatherRecordCount).size

The exact gate count of circuit.

theorem Algebraic.MassProduction.RuntimePipeline.circuit_recovers {width dimension groups prefixWidth totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (dimensionPositive : 0 < dimension) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (groupFits : groups ≤ 2 ^ groupBitWidth) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (directionCapacity : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (dummyTarget : Fin dimension → BinaryExtension width) (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) (computes : ∀ (point : Fin (ResourceEvaluation.pointCount dimension width)) (bit : Fin width), (resourceCircuits (ResourceEvaluation.resourceMemberIndex point bit)).ComputesWith DeMorgan.interpretation (directProduct (ResourceEvaluation.packedResourceFunction widthPositive (CanonicalPacking.packedPlacement widthPositive packingFits) function point bit) groups)) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) : (circuit prefixWidth widthPositive gridPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = fun (request : Fin totalRequests) => function (requestSource input request) (requestSuffix input request)

The complete runtime circuit returns every requested value in its original request position. In particular, the selected prefixes are runtime data, not nonuniform parameters of the constructed circuit.

theorem Algebraic.MassProduction.RuntimePipeline.circuit_computes {width dimension groups prefixWidth totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (dimensionPositive : 0 < dimension) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (groupFits : groups ≤ 2 ^ groupBitWidth) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (directionCapacity : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (dummyTarget : Fin dimension → BinaryExtension width) (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) (computes : ∀ (point : Fin (ResourceEvaluation.pointCount dimension width)) (bit : Fin width), (resourceCircuits (ResourceEvaluation.resourceMemberIndex point bit)).ComputesWith DeMorgan.interpretation (directProduct (ResourceEvaluation.packedResourceFunction widthPositive (CanonicalPacking.packedPlacement widthPositive packingFits) function point bit) groups)) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (circuit prefixWidth widthPositive gridPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).ComputesWith DeMorgan.interpretation (directProduct (requestFunction function) totalRequests)

Public direct-product form of circuit_recovers: the constructed circuit computes the standard row-major totalRequests-fold direct product.

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.circuit_cost {width dimension groups totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (dummyTarget : Fin dimension → BinaryExtension width) (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 prefixWidth widthPositive gridPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost = (GroupedScheduler.groupedScheduleCircuit dimension widthPositive schedulerDepth groups (GroupedScheduler.requestGroupSize totalRequests groups) allFit).cost DeMorgan.standardCost + totalRequests * (RuntimePacking.circuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost + ((gatherWithSelectorsCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits ⋯ scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost + totalRequests * (LineEnumeration.nonzeroScalarCount width * width * 5))

theorem Algebraic.MassProduction.RuntimePipeline.circuit_cost_expanded {width dimension groups totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (dummyTarget : Fin dimension → BinaryExtension width) (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 prefixWidth widthPositive gridPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost = (GroupedScheduler.groupedScheduleCircuit dimension widthPositive schedulerDepth groups (GroupedScheduler.requestGroupSize totalRequests groups) allFit).cost DeMorgan.standardCost + totalRequests * (RuntimePacking.circuit prefixWidth dimension widthPositive gridPositive).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 + (CanonicalMetadataRouting.matchedCanonicalRoutingCircuit gatherDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width).cost DeMorgan.standardCost + totalRequests * (LineEnumeration.nonzeroScalarCount width * width * 5)

Fully expanded finite ledger. All zero-cost wiring has disappeared; the only terms are packing, scheduling, the shorter resource circuits, two routing passes, and runtime decoding.