Runtime schedule-input assembly

This module pads runtime-computed targets into the rectangular grouped scheduler input and preserves each processed request's suffix and selector. All padding and projection layers are explicit zero-cost wiring circuits.

Runtime target padding and scheduler input

noncomputable def Algebraic.MassProduction.RuntimePipeline.paddedTargetSpecification (totalRequests groups requestsPerGroup dimension width suffixWidth : ℕ) (widthPositive : 0 < width) (dummyTarget : Fin dimension → BinaryExtension width) : Fin (groups * (requestsPerGroup * SchedulerIteration.pointBitWidth dimension width)) → DeMorgan.Wiring (totalRequests * requestDataCount dimension width suffixWidth)

Wire actual runtime target bits into a rectangular grouped target array; unused request slots receive a fixed dummy point.

Equations

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

noncomputable def Algebraic.MassProduction.RuntimePipeline.paddedTargetCircuit (totalRequests groups requestsPerGroup dimension width suffixWidth : ℕ) (widthPositive : 0 < width) (dummyTarget : Fin dimension → BinaryExtension width) : Circuit DeMorgan.signature (totalRequests * requestDataCount dimension width suffixWidth) (groups * (requestsPerGroup * SchedulerIteration.pointBitWidth dimension width))

Zero-cost rectangular padding of the actual runtime target array.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.paddedTargetCircuit_size (totalRequests groups requestsPerGroup dimension width suffixWidth : ℕ) (widthPositive : 0 < width) (dummyTarget : Fin dimension → BinaryExtension width) : (paddedTargetCircuit totalRequests groups requestsPerGroup dimension width suffixWidth widthPositive dummyTarget).size = ∑ output : Fin (groups * (requestsPerGroup * SchedulerIteration.pointBitWidth dimension width)), (paddedTargetSpecification totalRequests groups requestsPerGroup dimension width suffixWidth widthPositive dummyTarget output).expression.gateCount

The exact gate count of paddedTargetCircuit.

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.paddedTargetCircuit_cost {width dimension totalRequests groups requestsPerGroup suffixWidth : ℕ} (widthPositive : 0 < width) (dummyTarget : Fin dimension → BinaryExtension width) : (paddedTargetCircuit totalRequests groups requestsPerGroup dimension width suffixWidth widthPositive dummyTarget).cost DeMorgan.standardCost = 0

theorem Algebraic.MassProduction.RuntimePipeline.paddedTargetCircuit_eval {width totalRequests groups requestsPerGroup dimension suffixWidth : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (dummyTarget : Fin dimension → BinaryExtension width) (targets : Fin totalRequests → Fin dimension → BinaryExtension width) (input : Fin (totalRequests * requestDataCount dimension width suffixWidth) → Bool) (targetCorrect : ∀ (request : Fin totalRequests) (bit : Fin (dimension * width)), input (finProdFinEquiv (request, requestDataTargetIndex dimension width suffixWidth bit)) = binaryExtensionVectorBits widthPositive (targets request) bit) : (paddedTargetCircuit totalRequests groups requestsPerGroup dimension width suffixWidth widthPositive dummyTarget).eval DeMorgan.interpretation input = GroupedScheduler.groupedTargetArrayBits widthPositive (GroupedScheduler.paddedGroupedTargets capacity targets dummyTarget)

Schedule, suffix, and selector assembly

def Algebraic.MassProduction.RuntimePipeline.processedSuffixArray {totalRequests dimension width suffixWidth : ℕ} (input : Fin (totalRequests * requestDataCount dimension width suffixWidth) → Bool) : Fin (totalRequests * suffixWidth) → Bool

Row-major suffix view of processed request data.

Equations

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

def Algebraic.MassProduction.RuntimePipeline.processedSelectorArray {totalRequests dimension width suffixWidth : ℕ} (input : Fin (totalRequests * requestDataCount dimension width suffixWidth) → Bool) : Fin (totalRequests * width) → Bool

Row-major selector view of processed request data.

Equations

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

@[reducible]

def Algebraic.MassProduction.RuntimePipeline.suffixSelectorCount (totalRequests suffixWidth width : ℕ) : ℕ

Processed suffixes followed by processed runtime selectors.

Equations

• Algebraic.MassProduction.RuntimePipeline.suffixSelectorCount totalRequests suffixWidth width = totalRequests * suffixWidth + totalRequests * width

noncomputable def Algebraic.MassProduction.RuntimePipeline.suffixSelectorSpecification (totalRequests dimension width suffixWidth : ℕ) : Fin (suffixSelectorCount totalRequests suffixWidth width) → DeMorgan.Wiring (totalRequests * requestDataCount dimension width suffixWidth)

Zero-cost wiring specification that retains every processed suffix and selector.

Equations

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

noncomputable def Algebraic.MassProduction.RuntimePipeline.suffixSelectorCircuit (totalRequests dimension width suffixWidth : ℕ) : Circuit DeMorgan.signature (totalRequests * requestDataCount dimension width suffixWidth) (suffixSelectorCount totalRequests suffixWidth width)

Wiring circuit that exposes processed suffixes and runtime selectors.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.suffixSelectorCircuit_size (totalRequests dimension width suffixWidth : ℕ) : (suffixSelectorCircuit totalRequests dimension width suffixWidth).size = ∑ output : Fin (suffixSelectorCount totalRequests suffixWidth width), (suffixSelectorSpecification totalRequests dimension width suffixWidth output).expression.gateCount

The exact gate count of suffixSelectorCircuit.

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.suffixSelectorCircuit_eval {totalRequests dimension width suffixWidth : ℕ} (input : Fin (totalRequests * requestDataCount dimension width suffixWidth) → Bool) : (suffixSelectorCircuit totalRequests dimension width suffixWidth).eval DeMorgan.interpretation input = Fin.append (processedSuffixArray input) (processedSelectorArray input)

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.suffixSelectorCircuit_cost {totalRequests dimension width suffixWidth : ℕ} : (suffixSelectorCircuit totalRequests dimension width suffixWidth).cost DeMorgan.standardCost = 0

noncomputable def Algebraic.MassProduction.RuntimePipeline.scheduleSuffixSelectorCircuit (totalRequests groups requestsPerGroup dimension width suffixWidth schedulerDepth : ℕ) (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) : Circuit DeMorgan.signature (totalRequests * requestDataCount dimension width suffixWidth) (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width) + suffixSelectorCount totalRequests suffixWidth width)

Scheduler output followed by runtime suffixes and one-hot selectors.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.scheduleSuffixSelectorCircuit_size (totalRequests groups requestsPerGroup dimension width suffixWidth schedulerDepth : ℕ) (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) : (scheduleSuffixSelectorCircuit totalRequests groups requestsPerGroup dimension width suffixWidth schedulerDepth widthPositive allFit dummyTarget).size = (paddedTargetCircuit totalRequests groups requestsPerGroup dimension width suffixWidth widthPositive dummyTarget).size + groups * SchedulerIteration.greedyScheduleGateCount dimension widthPositive schedulerDepth requestsPerGroup + (suffixSelectorCircuit totalRequests dimension width suffixWidth).size

The exact gate count of scheduleSuffixSelectorCircuit.

theorem Algebraic.MassProduction.RuntimePipeline.scheduleSuffixSelectorCircuit_eval {width requestsPerGroup schedulerDepth totalRequests groups dimension suffixWidth : ℕ} (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (capacity : totalRequests ≤ groups * requestsPerGroup) (dummyTarget : Fin dimension → BinaryExtension width) (targets : Fin totalRequests → Fin dimension → BinaryExtension width) (input : Fin (totalRequests * requestDataCount dimension width suffixWidth) → Bool) (targetCorrect : ∀ (request : Fin totalRequests) (bit : Fin (dimension * width)), input (finProdFinEquiv (request, requestDataTargetIndex dimension width suffixWidth bit)) = binaryExtensionVectorBits widthPositive (targets request) bit) : (scheduleSuffixSelectorCircuit totalRequests groups requestsPerGroup dimension width suffixWidth schedulerDepth widthPositive allFit dummyTarget).eval DeMorgan.interpretation input = Fin.append (GroupedScheduler.groupedScheduleOutput dimension widthPositive schedulerDepth groups requestsPerGroup allFit (GroupedScheduler.paddedGroupedTargets capacity targets dummyTarget)) (Fin.append (processedSuffixArray input) (processedSelectorArray input))

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.scheduleSuffixSelectorCircuit_cost {width requestsPerGroup schedulerDepth dimension totalRequests groups suffixWidth : ℕ} (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (dummyTarget : Fin dimension → BinaryExtension width) : (scheduleSuffixSelectorCircuit totalRequests groups requestsPerGroup dimension width suffixWidth schedulerDepth widthPositive allFit dummyTarget).cost DeMorgan.standardCost = (GroupedScheduler.groupedScheduleCircuit dimension widthPositive schedulerDepth groups requestsPerGroup allFit).cost DeMorgan.standardCost