Per-request runtime data

This module processes each runtime (prefix, suffix) request independently. It computes the prefix's canonical packed target and one-hot basis selector, retains the suffix by zero-cost wiring, and exposes row-major projections with exact evaluation and cost theorems.

Per-request runtime data

@[reducible]

def Algebraic.MassProduction.RuntimePipeline.requestInputCount (prefixWidth suffixWidth : ℕ) : ℕ

One request contains a little-endian prefix followed by its suffix.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestInputCount prefixWidth suffixWidth = prefixWidth + suffixWidth

@[reducible]

def Algebraic.MassProduction.RuntimePipeline.requestDataCount (dimension width suffixWidth : ℕ) : ℕ

One processed request contains target bits, selector bits, then suffix.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestDataCount dimension width suffixWidth = Algebraic.MassProduction.RuntimePacking.outputCount dimension width + suffixWidth

def Algebraic.MassProduction.RuntimePipeline.requestPrefixInputIndex (prefixWidth suffixWidth : ℕ) : Fin prefixWidth → Fin (requestInputCount prefixWidth suffixWidth)

Select the prefix block of one request.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestPrefixInputIndex prefixWidth suffixWidth = Fin.castAdd suffixWidth

def Algebraic.MassProduction.RuntimePipeline.requestSuffixInputIndex (prefixWidth suffixWidth : ℕ) : Fin suffixWidth → Fin (requestInputCount prefixWidth suffixWidth)

Select the suffix block of one request.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestSuffixInputIndex prefixWidth suffixWidth = Fin.natAdd prefixWidth

noncomputable def Algebraic.MassProduction.RuntimePipeline.requestDataCircuit {width : ℕ} (prefixWidth dimension suffixWidth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) : Circuit DeMorgan.signature (requestInputCount prefixWidth suffixWidth) (RuntimePacking.outputCount dimension width + suffixWidth)

Process one runtime prefix and retain its suffix.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.requestDataCircuit_size {width : ℕ} (prefixWidth dimension suffixWidth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) : (requestDataCircuit prefixWidth dimension suffixWidth widthPositive gridPositive).size = FixedDivision.prefixGateCount prefixWidth widthPositive prefixWidth + BaseConversion.gateCount prefixWidth gridPositive dimension + RuntimePacking.targetEncoderGateCount prefixWidth dimension width

The exact gate count of requestDataCircuit.

noncomputable def Algebraic.MassProduction.RuntimePipeline.requestDataArrayCircuit {width : ℕ} (totalRequests prefixWidth dimension suffixWidth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) : Circuit DeMorgan.signature (totalRequests * requestInputCount prefixWidth suffixWidth) (totalRequests * (RuntimePacking.outputCount dimension width + suffixWidth))

Process all request rows independently.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.requestDataArrayCircuit_size {width : ℕ} (totalRequests prefixWidth dimension suffixWidth : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) : (requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).size = totalRequests * (requestDataCircuit prefixWidth dimension suffixWidth widthPositive gridPositive).size

The exact gate count of requestDataArrayCircuit.

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

Read one request row from the complete runtime input.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestInput input request = Algebraic.MassProduction.directProductInput input request

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

Read one request's runtime prefix.

Equations

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

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

Read one request's runtime suffix.

Equations

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

def Algebraic.MassProduction.RuntimePipeline.requestDataTargetIndex (dimension width suffixWidth : ℕ) (bit : Fin (dimension * width)) : Fin (requestDataCount dimension width suffixWidth)

Local processed-request index of one target-point bit.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestDataTargetIndex dimension width suffixWidth bit = ⟨↑bit, ⋯⟩

def Algebraic.MassProduction.RuntimePipeline.requestDataSelectorIndex (dimension width suffixWidth : ℕ) (bit : Fin width) : Fin (requestDataCount dimension width suffixWidth)

Local processed-request index of one selector bit.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestDataSelectorIndex dimension width suffixWidth bit = ⟨dimension * width + ↑bit, ⋯⟩

def Algebraic.MassProduction.RuntimePipeline.requestDataSuffixIndex (dimension width suffixWidth : ℕ) (bit : Fin suffixWidth) : Fin (requestDataCount dimension width suffixWidth)

Local processed-request index of one suffix bit.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestDataSuffixIndex dimension width suffixWidth bit = ⟨Algebraic.MassProduction.RuntimePacking.outputCount dimension width + ↑bit, ⋯⟩

theorem Algebraic.MassProduction.RuntimePipeline.requestDataCircuit_eval_target {width dimension prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin (requestInputCount prefixWidth suffixWidth) → Bool) (coordinate : Fin dimension) (bit : Fin width) : (requestDataCircuit prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input (requestDataTargetIndex dimension width suffixWidth (finProdFinEquiv (coordinate, bit))) = finiteIndexBits width (CanonicalPacking.symbolDigits packingFits (RuntimePacking.source fun (prefixBit : Fin prefixWidth) => input (requestPrefixInputIndex prefixWidth suffixWidth prefixBit)) coordinate) bit

theorem Algebraic.MassProduction.RuntimePipeline.requestDataCircuit_eval_selector {width dimension prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin (requestInputCount prefixWidth suffixWidth) → Bool) (candidate : Fin width) : (requestDataCircuit prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input (requestDataSelectorIndex dimension width suffixWidth candidate) = decide (candidate = CanonicalPacking.bitIndex packingFits (RuntimePacking.source fun (prefixBit : Fin prefixWidth) => input (requestPrefixInputIndex prefixWidth suffixWidth prefixBit)))

theorem Algebraic.MassProduction.RuntimePipeline.requestDataCircuit_eval_suffix {width dimension prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (input : Fin (requestInputCount prefixWidth suffixWidth) → Bool) (bit : Fin suffixWidth) : (requestDataCircuit prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input (requestDataSuffixIndex dimension width suffixWidth bit) = input (requestSuffixInputIndex prefixWidth suffixWidth bit)

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

Prefix index represented by one runtime request row.

Equations

• Algebraic.MassProduction.RuntimePipeline.requestSource input request = Algebraic.MassProduction.RuntimePacking.source (Algebraic.MassProduction.RuntimePipeline.requestPrefix input request)

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

Canonical packed target selected by one runtime request row.

Equations

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

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

Canonical basis coordinate selected by one runtime request row.

Equations

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

theorem Algebraic.MassProduction.RuntimePipeline.requestDataArrayCircuit_eval_target {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) (request : Fin totalRequests) (bit : Fin (dimension * width)) : (requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input (finProdFinEquiv (request, requestDataTargetIndex dimension width suffixWidth bit)) = binaryExtensionVectorBits widthPositive (requestTarget widthPositive packingFits input request) bit

theorem Algebraic.MassProduction.RuntimePipeline.requestDataArrayCircuit_eval_selector {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) (request : Fin totalRequests) (candidate : Fin width) : (requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input (finProdFinEquiv (request, requestDataSelectorIndex dimension width suffixWidth candidate)) = decide (candidate = requestSelectedBit packingFits input request)

theorem Algebraic.MassProduction.RuntimePipeline.requestDataArrayCircuit_eval_suffix {width dimension totalRequests prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (input : Fin (totalRequests * requestInputCount prefixWidth suffixWidth) → Bool) (request : Fin totalRequests) (bit : Fin suffixWidth) : (requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).eval DeMorgan.interpretation input (finProdFinEquiv (request, requestDataSuffixIndex dimension width suffixWidth bit)) = requestSuffix input request bit

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.requestDataCircuit_cost {width dimension prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) : (requestDataCircuit prefixWidth dimension suffixWidth widthPositive gridPositive).cost DeMorgan.standardCost = (RuntimePacking.circuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost

@[simp]

theorem Algebraic.MassProduction.RuntimePipeline.requestDataArrayCircuit_cost {width dimension totalRequests prefixWidth suffixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) : (requestDataArrayCircuit totalRequests prefixWidth dimension suffixWidth widthPositive gridPositive).cost DeMorgan.standardCost = totalRequests * (RuntimePacking.circuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost