Exact packed scatter-evaluate-gather-decode pipeline

This module composes the finite correctness interfaces. It assumes one supplied groups-copy circuit for each shorter Boolean resource function, wires them to canonical scatter slots, gathers the resulting field values back to fixed incidence records, and applies the fixed XOR decoder.

theorem Algebraic.MassProduction.PackedPipeline.gather_evaluatedPackedResources_routes_incidence {Prefix : Type u} {width groups groupBitWidth totalRequests orderWidth requestsPerGroup dimension suffixWidth scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (targets : Fin totalRequests → Fin dimension → BinaryExtension width) (directions : Fin totalRequests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (pointFormula : ∀ (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), GroupedScheduler.requestScheduledLinePoint widthPositive capacity scheduleOutput request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (withinGroupDisjoint : ∀ (left right : Fin totalRequests), (GroupedScheduler.requestGroupSlot capacity left).1 = (GroupedScheduler.requestGroupSlot capacity right).1 → left ≠ right → Disjoint (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput left) (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput right)) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (requestSuffix : Fin totalRequests → Fin suffixWidth → Bool) (scatterDestinationSuffix : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin suffixWidth → Bool) (scatterPaddingSuffix : Fin scatterPaddingCount → Fin suffixWidth → Bool) (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 placement function point bit) groups)) (gatherDestinationValues : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width) → Fin width → Bool) (gatherPaddingValues : Fin gatherPaddingCount → Fin width → Bool) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity scheduleOutput requestSuffix scatterDestinationSuffix scatterPaddingSuffix scatterRecordCount; have scatterDestinationFits := ⋯; have resourceValues := ResourceEvaluation.evaluatedResourceValues groupsPositive groupBitWidth dimension width scatterDepth suffixWidth scatterDestinationFits resourceCircuits scatterOutput; have gatherOutput := GatherRouting.canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity scheduleOutput resourceValues gatherDestinationValues gatherPaddingValues gatherRecordCount; have gatherDestinationFits := ⋯; RoutingMetadata.recordValue gatherOutput (Fin.castLE gatherDestinationFits incidence) = fun (bit : Fin width) => decodeBinaryExtension widthPositive (packedEvaluationResource widthPositive placement function (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).2 (requestSuffix (IncidenceRouting.incidenceAt incidence).1)) bit

Scatter, shorter-resource evaluation, and gather return every incidence's complete encoded field value on its literal row-major output record.

theorem Algebraic.MassProduction.PackedPipeline.decoder_recovers_of_gatheredPackedResources {Prefix : Type u} {width totalRequests groups requestsPerGroup dimension suffixWidth gatherDepth groupBitWidth orderWidth : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (requestSource : Fin totalRequests → Prefix) (requestSuffix : Fin totalRequests → Fin suffixWidth → Bool) (gatherOutput : Fin (Sorting.networkBits gatherDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width)) → Bool) (gatherDestinationFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords gatherDepth) (gatherCorrect : ∀ (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)), RoutingMetadata.recordValue gatherOutput (Fin.castLE gatherDestinationFits incidence) = fun (bit : Fin width) => decodeBinaryExtension widthPositive (packedEvaluationResource widthPositive placement function (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).2 (requestSuffix (IncidenceRouting.incidenceAt incidence).1)) bit) (lineRecovers : ∀ (request : Fin totalRequests), ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), decodeBinaryExtension widthPositive (packedEvaluationResource widthPositive placement function (GroupedScheduler.requestScheduledLinePoint widthPositive capacity scheduleOutput request scalar) (requestSuffix request)) (placement (requestSource request)).2 = function (requestSource request) (requestSuffix request)) : (GatherDecoder.circuit gatherDestinationFits fun (request : Fin totalRequests) => (placement (requestSource request)).2).eval DeMorgan.interpretation gatherOutput = fun (request : Fin totalRequests) => function (requestSource request) (requestSuffix request)

Once the fixed gather invariant is available, the explicit XOR circuit recovers all requested Boolean values in request order.

theorem Algebraic.MassProduction.PackedPipeline.scatter_evaluate_gather_decode_recovers {Prefix : Type u} {width dimension groups groupBitWidth totalRequests orderWidth requestsPerGroup suffixWidth scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (dimensionPositive : 0 < dimension) (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (requestSource : Fin totalRequests → Prefix) (requestSuffix : Fin totalRequests → Fin suffixWidth → Bool) (directions : Fin totalRequests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (pointFormula : ∀ (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), GroupedScheduler.requestScheduledLinePoint widthPositive capacity scheduleOutput request scalar = packedTargetPoint widthPositive placement (requestSource request) + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (setFormula : ∀ (request : Fin totalRequests), GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput request = ForbiddenRanks.binaryExtensionPuncturedLine (packedTargetPoint widthPositive placement (requestSource request)) (directions request)) (withinGroupDisjoint : ∀ (left right : Fin totalRequests), (GroupedScheduler.requestGroupSlot capacity left).1 = (GroupedScheduler.requestGroupSlot capacity right).1 → left ≠ right → Disjoint (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput left) (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput right)) (scatterDestinationSuffix : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin suffixWidth → Bool) (scatterPaddingSuffix : Fin scatterPaddingCount → Fin suffixWidth → Bool) (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 placement function point bit) groups)) (gatherDestinationValues : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width) → Fin width → Bool) (gatherPaddingValues : Fin gatherPaddingCount → Fin width → Bool) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity scheduleOutput requestSuffix scatterDestinationSuffix scatterPaddingSuffix scatterRecordCount; have scatterDestinationFits := ⋯; have resourceValues := ResourceEvaluation.evaluatedResourceValues groupsPositive groupBitWidth dimension width scatterDepth suffixWidth scatterDestinationFits resourceCircuits scatterOutput; have gatherOutput := GatherRouting.canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity scheduleOutput resourceValues gatherDestinationValues gatherPaddingValues gatherRecordCount; have gatherDestinationFits := ⋯; (GatherDecoder.circuit gatherDestinationFits fun (request : Fin totalRequests) => (placement (requestSource request)).2).eval DeMorgan.interpretation gatherOutput = fun (request : Fin totalRequests) => function (requestSource request) (requestSuffix request)

Finite end-to-end correctness of the exact manuscript pipeline. Under the scheduler's geometric invariants and correct shorter-resource circuits, the explicit fixed-wire decoder returns every requested value of function.

theorem Algebraic.MassProduction.PackedPipeline.grouped_scatter_evaluate_gather_decode_recovers {Prefix : Type u} {width dimension groups groupBitWidth totalRequests orderWidth schedulerDepth suffixWidth scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (dimensionPositive : 0 < dimension) (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (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))) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (requestSource : Fin totalRequests → Prefix) (requestSuffix : Fin totalRequests → Fin suffixWidth → Bool) (dummyTarget : Fin dimension → BinaryExtension width) (scatterDestinationSuffix : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin suffixWidth → Bool) (scatterPaddingSuffix : Fin scatterPaddingCount → Fin suffixWidth → Bool) (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 placement function point bit) groups)) (gatherDestinationValues : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width) → Fin width → Bool) (gatherPaddingValues : Fin gatherPaddingCount → Fin width → Bool) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : have targets := fun (request : Fin totalRequests) => packedTargetPoint widthPositive placement (requestSource request); let groupSize := GroupedScheduler.requestGroupSize totalRequests groups; have capacity := ⋯; have paddedTargets := GroupedScheduler.paddedGroupedTargets capacity targets dummyTarget; have scheduleOutput := GroupedScheduler.groupedScheduleOutput dimension widthPositive schedulerDepth groups groupSize allFit paddedTargets; have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity scheduleOutput requestSuffix scatterDestinationSuffix scatterPaddingSuffix scatterRecordCount; have scatterDestinationFits := ⋯; have resourceValues := ResourceEvaluation.evaluatedResourceValues groupsPositive groupBitWidth dimension width scatterDepth suffixWidth scatterDestinationFits resourceCircuits scatterOutput; have gatherOutput := GatherRouting.canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity scheduleOutput resourceValues gatherDestinationValues gatherPaddingValues gatherRecordCount; have gatherDestinationFits := ⋯; (GatherDecoder.circuit gatherDestinationFits fun (request : Fin totalRequests) => (placement (requestSource request)).2).eval DeMorgan.interpretation gatherOutput = fun (request : Fin totalRequests) => function (requestSource request) (requestSuffix request)

The deterministic grouped greedy scheduler supplies all geometric hypotheses of the finite end-to-end pipeline.