Complete finite pipeline assembly

This module composes scatter routing, shorter-resource evaluation, gather routing, and decoding into one circuit whose input is an already-computed schedule followed by the request suffixes. It proves the circuit's exact semantics, recovery theorem, and gate-cost ledger.

Complete assembled finite pipeline

noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterResourceGatherCircuit {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) (scatterDestinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ 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 (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) (Sorting.networkBits gatherDepth (RoutingMetadata.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width))

Scatter, resource evaluation, and gather as a single circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.scatterResourceGatherCircuit_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) (scatterDestinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ 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) : (scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount scatterDestinationFits resourceCircuits gatherRecordCount).size = (scatterResourceCircuit suffixWidth groupBitWidth capacity scatterRecordCount scatterDestinationFits resourceCircuits).size + (gatherRoutingCircuit groupsPositive groupBitWidth orderWidth incidenceFits capacity gatherRecordCount).size

The exact gate count of scatterResourceGatherCircuit.

theorem Algebraic.MassProduction.RoutingAssembly.scatterResourceGatherCircuit_eval {groups width totalRequests requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (widthPositive : 0 < width) (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) (scatterDestinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ 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 (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) : (scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount scatterDestinationFits resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = have schedule := scatterScheduleInput input; have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity schedule (scatterSuffixInput input) (fun (_destination : Fin (2 ^ (groupBitWidth + dimension * width))) (_bit : Fin suffixWidth) => false) (fun (_padding : Fin scatterPaddingCount) (_bit : Fin suffixWidth) => false) scatterRecordCount; have bankOutput := (ResourceEvaluation.resourceBankCircuit scatterDestinationFits resourceCircuits).eval DeMorgan.interpretation scatterOutput; GatherRouting.canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity schedule (ResourceEvaluation.resourceValuesFromBank groupsPositive groupBitWidth dimension width bankOutput) (fun (_destination : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (_bit : Fin width) => false) (fun (_padding : Fin gatherPaddingCount) (_bit : Fin width) => false) gatherRecordCount

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.scatterResourceGatherCircuit_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) (scatterDestinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ 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) : (scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount scatterDestinationFits resourceCircuits gatherRecordCount).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

noncomputable def Algebraic.MassProduction.RoutingAssembly.assembledPipelineCircuit {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) : Circuit DeMorgan.signature (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) totalRequests

The complete scatter-evaluate-gather-decode circuit on an already computed schedule and its request suffixes. Both sorter-capacity inclusions are derived from the exact padding equations, so callers do not supply redundant proof arguments.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.assembledPipelineCircuit_size {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) : (assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).size = (scatterResourceGatherCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity scatterRecordCount ⋯ resourceCircuits gatherRecordCount).size + ∑ request : Fin totalRequests, GatherDecoder.decoderGateCount (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) ⋯ (fun (request : Fin totalRequests) => (placement (requestSource request)).2) request

The assembled pipeline has exactly the gates of scatter, resource evaluation and gather, followed by one fixed decoder per request.

theorem Algebraic.MassProduction.RoutingAssembly.assembledPipelineCircuit_eval {Prefix : Type u} {groups width totalRequests requestsPerGroup dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (groupsPositive : 0 < groups) (widthPositive : 0 < width) (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 (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) : (assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = have scatterDestinationFits := ⋯; have gatherDestinationFits := ⋯; have schedule := scatterScheduleInput input; have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity schedule (scatterSuffixInput input) (fun (_destination : Fin (2 ^ (groupBitWidth + dimension * width))) (_bit : Fin suffixWidth) => false) (fun (_padding : Fin scatterPaddingCount) (_bit : Fin suffixWidth) => false) scatterRecordCount; have bankOutput := (ResourceEvaluation.resourceBankCircuit scatterDestinationFits resourceCircuits).eval DeMorgan.interpretation scatterOutput; have gatherOutput := GatherRouting.canonicalGatherBits widthPositive groupBitWidth orderWidth incidenceFits capacity schedule (ResourceEvaluation.resourceValuesFromBank groupsPositive groupBitWidth dimension width bankOutput) (fun (_destination : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (_bit : Fin width) => false) (fun (_padding : Fin gatherPaddingCount) (_bit : Fin width) => false) gatherRecordCount; (GatherDecoder.circuit gatherDestinationFits fun (request : Fin totalRequests) => (placement (requestSource request)).2).eval DeMorgan.interpretation gatherOutput

theorem Algebraic.MassProduction.RoutingAssembly.assembledPipelineCircuit_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) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (requestSource : Fin totalRequests → Prefix) (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests 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 (scatterScheduleInput input) request scalar = packedTargetPoint widthPositive placement (requestSource request) + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (setFormula : ∀ (request : Fin totalRequests), GroupedScheduler.requestScheduledLineSet widthPositive capacity (scatterScheduleInput input) 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 (scatterScheduleInput input) left) (GroupedScheduler.requestScheduledLineSet widthPositive capacity (scatterScheduleInput input) right)) (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)) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = fun (request : Fin totalRequests) => function (requestSource request) (scatterSuffixInput input request)

End-to-end correctness of the single assembled finite circuit. Given the geometric scheduler invariants and correct shorter-resource circuits, it returns every requested Boolean value in its original request position.

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.assembledPipelineCircuit_cost {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) : (assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).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 * 4)

Exact cost ledger for the assembled finite circuit. Record assembly, schedule preservation, and all fixed reindexings contribute zero gates.