Parallel evaluation of shorter resource functions

After scatter, each canonical (group, point) record contains one suffix. For every affine point and every field-basis coordinate, this module wires those group slots into one supplied mass-production circuit for the shorter Boolean resource function. All wiring is explicit and costs no gates.

@[reducible]

def Algebraic.MassProduction.ResourceEvaluation.pointCount (dimension width : ℕ) : ℕ

Number of raw affine-point bit vectors.

Equations

• Algebraic.MassProduction.ResourceEvaluation.pointCount dimension width = 2 ^ (dimension * width)

@[reducible]

def Algebraic.MassProduction.ResourceEvaluation.resourceBitCount (dimension width : ℕ) : ℕ

One resource member for every (point, field bit) pair.

Equations

• Algebraic.MassProduction.ResourceEvaluation.resourceBitCount dimension width = Algebraic.MassProduction.ResourceEvaluation.pointCount dimension width * width

def Algebraic.MassProduction.ResourceEvaluation.resourceMemberIndex {dimension width : ℕ} (point : Fin (pointCount dimension width)) (bit : Fin width) : Fin (resourceBitCount dimension width)

Row-major resource-member index.

Equations

• Algebraic.MassProduction.ResourceEvaluation.resourceMemberIndex point bit = finProdFinEquiv (point, bit)

def Algebraic.MassProduction.ResourceEvaluation.resourceMemberAt {dimension width : ℕ} (member : Fin (resourceBitCount dimension width)) : Fin (pointCount dimension width) × Fin width

Decode a resource-member index.

Equations

• Algebraic.MassProduction.ResourceEvaluation.resourceMemberAt member = finProdFinEquiv.symm member

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.resourceMemberAt_index {dimension width : ℕ} (point : Fin (pointCount dimension width)) (bit : Fin width) : resourceMemberAt (resourceMemberIndex point bit) = (point, bit)

noncomputable def Algebraic.MassProduction.ResourceEvaluation.resourceSlotDestination {groups : ℕ} (groupBitWidth dimension width : ℕ) (group : Fin groups) (point : Fin (pointCount dimension width)) : Fin (2 ^ (groupBitWidth + dimension * width))

Canonical full-key-space destination for a valid group and raw point-bit vector.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.lexBitVectorAt_resourceSlotDestination {groups dimension width groupBitWidth : ℕ} (group : Fin groups) (point : Fin (pointCount dimension width)) : lexBitVectorAt (resourceSlotDestination groupBitWidth dimension width group point) = Fin.append (finiteIndexBits groupBitWidth group) (lexBitVectorAt point)

noncomputable def Algebraic.MassProduction.ResourceEvaluation.scheduledIncidencePointIndex {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin (pointCount dimension width)

Raw point-bit index of one scheduled incidence.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.lexBitVectorAt_scheduledIncidencePointIndex {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : lexBitVectorAt (scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence) = binaryExtensionVectorBits widthPositive (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).2

theorem Algebraic.MassProduction.ResourceEvaluation.pointCoordinate_scheduledIncidencePointIndex {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : binaryExtensionVectorCoordinate widthPositive (lexBitVectorAt (scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence)) = (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).2

Decoding the scheduled point index returns the geometric incidence point.

theorem Algebraic.MassProduction.ResourceEvaluation.resourceSlotDestination_scheduledIncidence {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : resourceSlotDestination groupBitWidth dimension width (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).1 (scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence) = IncidenceRouting.fullIncidenceDestination widthPositive groupBitWidth capacity scheduleOutput incidence

The separately decoded group and point indices identify exactly the same full scatter slot as the incidence key.

noncomputable def Algebraic.MassProduction.ResourceEvaluation.resourceCircuitInputIndex {groupBitWidth dimension width routingDepth groups suffixWidth : ℕ} (destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords routingDepth) (member : Fin (resourceBitCount dimension width)) (input : Fin (groups * suffixWidth)) : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth))

Physical scatter-output wire used as one local resource-circuit input.

Equations

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

noncomputable def Algebraic.MassProduction.ResourceEvaluation.resourceBankCircuit {groupBitWidth dimension width routingDepth groups suffixWidth : ℕ} (destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) : Circuit DeMorgan.signature (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) (resourceBitCount dimension width * groups)

Put every supplied groups-copy resource circuit in parallel and wire its inputs directly to the corresponding fixed scatter slots.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.resourceBankCircuit_size {groupBitWidth dimension width routingDepth groups suffixWidth : ℕ} (destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) : (resourceBankCircuit destinationFits resourceCircuits).size = ∑ member : Fin (resourceBitCount dimension width), (resourceCircuits member).size

The bank has exactly the resource circuits' gates combined; routing each circuit to its destination block is pure wiring.

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.resourceBankCircuit_eval_apply {groupBitWidth dimension width routingDepth groups suffixWidth : ℕ} (destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (scatterOutput : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) → Bool) (point : Fin (pointCount dimension width)) (bit : Fin width) (group : Fin groups) : (resourceBankCircuit destinationFits resourceCircuits).eval DeMorgan.interpretation scatterOutput (finProdFinEquiv (resourceMemberIndex point bit, group)) = (resourceCircuits (resourceMemberIndex point bit)).eval DeMorgan.interpretation (scatterOutput ∘ resourceCircuitInputIndex destinationFits (resourceMemberIndex point bit)) group

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.resourceBankCircuit_cost {groupBitWidth dimension width routingDepth groups suffixWidth : ℕ} (destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) : (resourceBankCircuit destinationFits resourceCircuits).cost DeMorgan.standardCost = ∑ member : Fin (resourceBitCount dimension width), (resourceCircuits member).cost DeMorgan.standardCost

Exact bank cost: resource circuits share no gates with one another, while the fixed input wiring is free.

Incidence semantics

theorem Algebraic.MassProduction.ResourceEvaluation.resourceBankCircuit_eval_incidence {width groups groupBitWidth totalRequests requestsPerGroup dimension suffixWidth paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (groupFits : groups ≤ 2 ^ groupBitWidth) (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)) (requestSuffix : Fin totalRequests → Fin suffixWidth → Bool) (destinationSuffix : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin suffixWidth → Bool) (paddingSuffix : Fin paddingCount → Fin suffixWidth → Bool) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (resourceFunctions : Fin (pointCount dimension width) → Fin width → ScalarFunction Bool suffixWidth) (computes : ∀ (point : Fin (pointCount dimension width)) (bit : Fin width), (resourceCircuits (resourceMemberIndex point bit)).ComputesWith DeMorgan.interpretation (directProduct (resourceFunctions point bit) groups)) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (bit : Fin width) : have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity scheduleOutput requestSuffix destinationSuffix paddingSuffix recordCount; have destinationFits := ⋯; have point := scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence; have group := (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).1; (resourceBankCircuit destinationFits resourceCircuits).eval DeMorgan.interpretation scatterOutput (finProdFinEquiv (resourceMemberIndex point bit, group)) = resourceFunctions point bit (requestSuffix (IncidenceRouting.incidenceAt incidence).1)

A resource circuit sees the suffix routed to its fixed (group, point) slot. Hence its output for a scheduled incidence is the corresponding shorter resource function evaluated on that request's suffix.

Viewing bank outputs as a complete source-slot array

noncomputable def Algebraic.MassProduction.ResourceEvaluation.fullDestinationGroupBits (groupBitWidth pointWidth : ℕ) (destination : Fin (2 ^ (groupBitWidth + pointWidth))) : Fin groupBitWidth → Bool

Group-prefix bits of one canonical full-key destination.

Equations

• Algebraic.MassProduction.ResourceEvaluation.fullDestinationGroupBits groupBitWidth pointWidth destination bit = Algebraic.MassProduction.lexBitVectorAt destination (Fin.castAdd pointWidth bit)

noncomputable def Algebraic.MassProduction.ResourceEvaluation.fullDestinationPointBits (groupBitWidth pointWidth : ℕ) (destination : Fin (2 ^ (groupBitWidth + pointWidth))) : Fin pointWidth → Bool

Point-suffix bits of one canonical full-key destination.

Equations

• Algebraic.MassProduction.ResourceEvaluation.fullDestinationPointBits groupBitWidth pointWidth destination bit = Algebraic.MassProduction.lexBitVectorAt destination (Fin.natAdd groupBitWidth bit)

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.fullDestinationGroupBits_resourceSlotDestination {groups dimension width groupBitWidth : ℕ} (group : Fin groups) (point : Fin (pointCount dimension width)) : fullDestinationGroupBits groupBitWidth (dimension * width) (resourceSlotDestination groupBitWidth dimension width group point) = finiteIndexBits groupBitWidth group

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.fullDestinationPointBits_resourceSlotDestination {groups dimension width groupBitWidth : ℕ} (group : Fin groups) (point : Fin (pointCount dimension width)) : fullDestinationPointBits groupBitWidth (dimension * width) (resourceSlotDestination groupBitWidth dimension width group point) = lexBitVectorAt point

noncomputable def Algebraic.MassProduction.ResourceEvaluation.decodedGroupOrZero {groups : ℕ} (groupsPositive : 0 < groups) (groupBitWidth : ℕ) (bits : Fin groupBitWidth → Bool) : Fin groups

Decode a valid group encoding; unused raw encodings are sent to group zero. This is a nonuniform wire-selection function, not a circuit or an instance.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.decodedGroupOrZero_finiteIndexBits {groups groupBitWidth : ℕ} (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (group : Fin groups) : decodedGroupOrZero groupsPositive groupBitWidth (finiteIndexBits groupBitWidth group) = group

noncomputable def Algebraic.MassProduction.ResourceEvaluation.fullDestinationPointIndex (groupBitWidth dimension width : ℕ) (destination : Fin (2 ^ (groupBitWidth + dimension * width))) : Fin (pointCount dimension width)

Point-member index decoded from a complete canonical destination.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.fullDestinationPointIndex_resourceSlotDestination {groups dimension width groupBitWidth : ℕ} (group : Fin groups) (point : Fin (pointCount dimension width)) : fullDestinationPointIndex groupBitWidth dimension width (resourceSlotDestination groupBitWidth dimension width group point) = point

noncomputable def Algebraic.MassProduction.ResourceEvaluation.resourceValuesFromBank {groups : ℕ} (groupsPositive : 0 < groups) (groupBitWidth dimension width : ℕ) (bankOutput : Fin (resourceBitCount dimension width * groups) → Bool) (destination : Fin (2 ^ (groupBitWidth + dimension * width))) : Fin width → Bool

Interpret a resource-bank output as one value for every raw full-key source slot. Invalid group encodings may select an arbitrary group-zero value because no scheduled incidence can request them.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ResourceEvaluation.resourceValuesFromBank_resourceSlotDestination {groups groupBitWidth dimension width : ℕ} (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (bankOutput : Fin (resourceBitCount dimension width * groups) → Bool) (group : Fin groups) (point : Fin (pointCount dimension width)) : resourceValuesFromBank groupsPositive groupBitWidth dimension width bankOutput (resourceSlotDestination groupBitWidth dimension width group point) = fun (bit : Fin width) => bankOutput (finProdFinEquiv (resourceMemberIndex point bit, group))

theorem Algebraic.MassProduction.ResourceEvaluation.resourceValuesFromBank_fullIncidenceDestination {width groups groupBitWidth totalRequests requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (bankOutput : Fin (resourceBitCount dimension width * groups) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : resourceValuesFromBank groupsPositive groupBitWidth dimension width bankOutput (IncidenceRouting.fullIncidenceDestination widthPositive groupBitWidth capacity scheduleOutput incidence) = fun (bit : Fin width) => bankOutput (finProdFinEquiv (resourceMemberIndex (scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence) bit, (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).1))

In particular, the total source-slot view selects the actual incidence's group and point bank output.

noncomputable def Algebraic.MassProduction.ResourceEvaluation.evaluatedResourceValues {groups : ℕ} (groupsPositive : 0 < groups) (groupBitWidth dimension width routingDepth suffixWidth : ℕ) (destinationFits : 2 ^ (groupBitWidth + dimension * width) ≤ Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (scatterOutput : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) → Bool) : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin width → Bool

Complete resource-source values obtained by evaluating the wired bank on one fixed scatter output.

Equations

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

theorem Algebraic.MassProduction.ResourceEvaluation.evaluatedResourceValues_routes_incidence {width groups groupBitWidth totalRequests requestsPerGroup dimension suffixWidth paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (groupFits : groups ≤ 2 ^ groupBitWidth) (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)) (requestSuffix : Fin totalRequests → Fin suffixWidth → Bool) (destinationSuffix : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin suffixWidth → Bool) (paddingSuffix : Fin paddingCount → Fin suffixWidth → Bool) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) (resourceCircuits : Fin (resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (resourceFunctions : Fin (pointCount dimension width) → Fin width → ScalarFunction Bool suffixWidth) (computes : ∀ (point : Fin (pointCount dimension width)) (bit : Fin width), (resourceCircuits (resourceMemberIndex point bit)).ComputesWith DeMorgan.interpretation (directProduct (resourceFunctions point bit) groups)) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : have scatterOutput := CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity scheduleOutput requestSuffix destinationSuffix paddingSuffix recordCount; have destinationFits := ⋯; evaluatedResourceValues groupsPositive groupBitWidth dimension width routingDepth suffixWidth destinationFits resourceCircuits scatterOutput (IncidenceRouting.fullIncidenceDestination widthPositive groupBitWidth capacity scheduleOutput incidence) = fun (bit : Fin width) => resourceFunctions (scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence) bit (requestSuffix (IncidenceRouting.incidenceAt incidence).1)

The complete source-slot view of the bank agrees with the intended shorter resource function on every actually scheduled incidence.

Packed evaluation-code resources

noncomputable def Algebraic.MassProduction.ResourceEvaluation.packedResourceFunction {Prefix : Type u} {width dimension suffixWidth : ℕ} (widthPositive : 0 < width) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (point : Fin (pointCount dimension width)) (bit : Fin width) : ScalarFunction Bool suffixWidth

Boolean resource function for one affine point and one field-basis bit.

Equations

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

theorem Algebraic.MassProduction.ResourceEvaluation.packedResourceFunction_scheduledIncidencePoint {Prefix : Type u} {width totalRequests groups requestsPerGroup dimension suffixWidth : ℕ} (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) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (bit : Fin width) (suffix : Fin suffixWidth → Bool) : packedResourceFunction widthPositive placement function (scheduledIncidencePointIndex widthPositive capacity scheduleOutput incidence) bit suffix = decodeBinaryExtension widthPositive (packedEvaluationResource widthPositive placement function (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).2 suffix) bit

At an incidence point, the indexed resource function is exactly the selected basis bit of the manuscript's field-valued resource.