High-rate resource recovery from a completed scheduler buffer

This circuit reads preserved copy, basis-bit, and suffix metadata, scatters the suffixes to the exact resource bank, evaluates each resource once, gathers its point values, and XORs each recovery line. It computes the requested source function in completed-buffer order, with the original request permutation still available in the buffer.

def Algebraic.MassProduction.Nonuniform.BufferResourceEvaluation.targets {Source : Type u_1} {width dimension copies total : ℕ} (code : HighRate.LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ HighRate.InformationBit code copies) (sources : Fin total → Source) : Fin total → Fin dimension → BinaryExtension width

Information-point targets determined by each original source request.

Equations

• Algebraic.MassProduction.Nonuniform.BufferResourceEvaluation.targets code placement sources request = ↑(placement (sources request)).2.1

theorem Algebraic.MassProduction.Nonuniform.BufferResourceEvaluation.existsCircuit {Source : Type u_1} {width dimension copies suffixWidth copyBits selectorBits requestWidth total : ℕ} (positive : 0 < width) (code : HighRate.LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ HighRate.InformationBit code copies) (function : Source → (Fin suffixWidth → Bool) → Bool) (copyFits : copies ≤ 2 ^ copyBits) (selectorFits : width ≤ 2 ^ selectorBits) (copyProjection : Fin copyBits → Fin requestWidth) (selectorProjection : Fin selectorBits → Fin requestWidth) (suffixProjection : Fin suffixWidth → Fin requestWidth) (members : Fin (HighRate.ResourceLayout.count copies dimension width) → Circuit DeMorgan.signature suffixWidth 1) (membersCorrect : ∀ (resource : Fin (HighRate.ResourceLayout.count copies dimension width)) (suffix : Fin suffixWidth → Bool), (members resource).eval DeMorgan.interpretation suffix 0 = HighRate.ResourceLayout.function positive code placement function resource suffix) : ∃ (recovered : Circuit DeMorgan.signature (BufferInput.inputWidth total 0 requestWidth (2 ^ width) (dimension * width)) total), recovered.cost DeMorgan.standardCost ≤ IncidenceEvaluation.routingCost (total * 2 ^ width) (HighRate.ResourceLayout.count copies dimension width) (HighRate.ResourceLayout.keyWidth copyBits dimension width selectorBits) suffixWidth + ∑ resource : Fin (HighRate.ResourceLayout.count copies dimension width), (members resource).cost DeMorgan.standardCost + total * 2 ^ width * 4 ∧ ∀ (data : Fin total → Fin requestWidth → Bool) (sources : Fin total → Source) (suffixes : Fin total → Fin suffixWidth → Bool) (state : BufferModel.State total total 0 dimension width), BufferModel.WellScheduled state (targets code placement sources) → (∀ (request : Fin total) (bit : Fin copyBits), data request (copyProjection bit) = finiteIndexBits copyBits (placement (sources request)).1 bit) → (∀ (request : Fin total) (bit : Fin selectorBits), data request (selectorProjection bit) = finiteIndexBits selectorBits (placement (sources request)).2.2 bit) → (∀ (request : Fin total) (bit : Fin suffixWidth), data request (suffixProjection bit) = suffixes request bit) → ∀ (request : Fin total), recovered.eval DeMorgan.interpretation (BufferModel.input positive state data (targets code placement sources)) request = function (sources (state.order (Sum.inl request))) (suffixes (state.order (Sum.inl request)))

Evaluate and recover every completed request using one exact bank. The only input-dependent premise is that the buffer correctly represents a disjoint schedule and the source/copy/selector/suffix metadata.