Free buffer compaction after a geometric phase

Preserve previously completed records, append the accepted prefix with its full point lists, and retain only original request data for the pending suffix. These operations are all fixed wiring; the phase is charged once.

def Algebraic.MassProduction.Nonuniform.BufferAdvance.acceptedIndex {accepted remaining pending : ℕ} (split : accepted + remaining = pending) (index : Fin accepted) : Fin pending

Literal position of an accepted prefix record.

Equations

• Algebraic.MassProduction.Nonuniform.BufferAdvance.acceptedIndex split index = Fin.castLE ⋯ index

def Algebraic.MassProduction.Nonuniform.BufferAdvance.pendingIndex {accepted remaining pending : ℕ} (split : accepted + remaining = pending) (index : Fin remaining) : Fin pending

Literal position of a record in the remaining suffix.

Equations

• Algebraic.MassProduction.Nonuniform.BufferAdvance.pendingIndex split index = ⟨accepted + ↑index, ⋯⟩

theorem Algebraic.MassProduction.Nonuniform.BufferAdvance.acceptedIndex_injective {accepted remaining pending : ℕ} (split : accepted + remaining = pending) : Function.Injective (acceptedIndex split)

Prefix positions are distinct.

theorem Algebraic.MassProduction.Nonuniform.BufferAdvance.pendingIndex_injective {accepted remaining pending : ℕ} (split : accepted + remaining = pending) : Function.Injective (pendingIndex split)

Suffix positions are distinct.

def Algebraic.MassProduction.Nonuniform.BufferAdvance.completedWires {accepted remaining pending : ℕ} (completed requestWidth slots keyWidth : ℕ) (split : accepted + remaining = pending) (record : Fin (completed + accepted)) (bit : Fin (BufferInput.storedWidth requestWidth slots keyWidth)) : DeMorgan.Wiring (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth) + BufferInput.inputWidth completed pending requestWidth slots keyWidth)

Preserve old completed records and append the newly accepted point lists.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferAdvance.pendingWires {accepted remaining pending : ℕ} (completed requestWidth slots keyWidth : ℕ) (split : accepted + remaining = pending) (record : Fin remaining) (bit : Fin requestWidth) : DeMorgan.Wiring (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth) + BufferInput.inputWidth completed pending requestWidth slots keyWidth)

Keep the pending suffix's original request data and discard its unused point lists.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferAdvance.wiring {accepted remaining pending : ℕ} (completed requestWidth slots keyWidth : ℕ) (split : accepted + remaining = pending) : Fin (BufferInput.inputWidth (completed + accepted) remaining requestWidth slots keyWidth) → DeMorgan.Wiring (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth) + BufferInput.inputWidth completed pending requestWidth slots keyWidth)

The complete fixed wiring for the next scheduler buffer.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferAdvance.circuit {completed pending requestWidth slots keyWidth accepted remaining : ℕ} (phase : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth slots keyWidth) (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth))) (split : accepted + remaining = pending) : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth slots keyWidth) (BufferInput.inputWidth (completed + accepted) remaining requestWidth slots keyWidth)

Run the phase once and compact its results into the next buffer.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.BufferAdvance.circuit_size {completed pending requestWidth slots keyWidth accepted remaining : ℕ} (phase : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth slots keyWidth) (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth))) (split : accepted + remaining = pending) : (circuit phase split).size = (PreparedInputs.circuit phase).size + ∑ output : Fin (BufferInput.inputWidth (completed + accepted) remaining requestWidth slots keyWidth), (wiring completed requestWidth slots keyWidth split output).expression.gateCount

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.BufferAdvance.circuit_eval {completed pending requestWidth slots keyWidth accepted remaining : ℕ} (phase : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth slots keyWidth) (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth))) (split : accepted + remaining = pending) (completedRecords : Fin completed → Fin (BufferInput.storedWidth requestWidth slots keyWidth) → Bool) (pendingRecords : Fin pending → Fin requestWidth → Bool) : have input := BufferInput.encode completedRecords pendingRecords; have output := phase.eval DeMorgan.interpretation input; (circuit phase split).eval DeMorgan.interpretation input = BufferInput.encode (Fin.append completedRecords fun (fresh : Fin accepted) (bit : Fin (BufferInput.storedWidth requestWidth slots keyWidth)) => output (finProdFinEquiv (acceptedIndex split fresh, Fin.natAdd 1 bit))) fun (waiting : Fin remaining) (bit : Fin requestWidth) => output (finProdFinEquiv (pendingIndex split waiting, Fin.natAdd 1 (Fin.castAdd (slots * keyWidth) bit)))

Exact semantics of buffer compaction: old records, accepted point lists, and the pending original-data suffix all appear at their fixed positions.

theorem Algebraic.MassProduction.Nonuniform.BufferAdvance.circuit_cost {completed pending requestWidth slots keyWidth accepted remaining : ℕ} (phase : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth slots keyWidth) (pending * (1 + BufferInput.storedWidth requestWidth slots keyWidth))) (split : accepted + remaining = pending) : (circuit phase split).cost DeMorgan.standardCost = phase.cost DeMorgan.standardCost

Buffer compaction adds no charged gates.