Input layout for a halving scheduler buffer

Completed records contain original request data and a complete point list. Pending records contain original request data only. All phase inputs are free selections from this buffer; scalar-validity flags are fixed constants.

@[reducible, inline]

abbrev Algebraic.MassProduction.Nonuniform.BufferInput.storedWidth (requestWidth slots keyWidth : ℕ) : ℕ

Width of a completed request together with its stored point list.

Equations

• Algebraic.MassProduction.Nonuniform.BufferInput.storedWidth requestWidth slots keyWidth = requestWidth + slots * keyWidth

@[reducible, inline]

abbrev Algebraic.MassProduction.Nonuniform.BufferInput.inputWidth (completed pending requestWidth slots keyWidth : ℕ) : ℕ

Completed records followed by pending request records.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferInput.encode {completed requestWidth slots keyWidth : ℕ} {Value : Sort u_1} {pending : ℕ} (completedRecords : Fin completed → Fin (storedWidth requestWidth slots keyWidth) → Value) (pendingRecords : Fin pending → Fin requestWidth → Value) : Fin (inputWidth completed pending requestWidth slots keyWidth) → Value

Flatten the two record arrays into the buffer input.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferInput.map_encode {Value : Sort u_1} {Result : Sort u_2} {completed requestWidth slots keyWidth pending : ℕ} (f : Value → Result) (completedRecords : Fin completed → Fin (storedWidth requestWidth slots keyWidth) → Value) (pendingRecords : Fin pending → Fin requestWidth → Value) : (fun (bit : Fin (inputWidth completed pending requestWidth slots keyWidth)) => f (encode completedRecords pendingRecords bit)) = encode (fun (record : Fin completed) (bit : Fin (storedWidth requestWidth slots keyWidth)) => f (completedRecords record bit)) fun (record : Fin pending) (bit : Fin requestWidth) => f (pendingRecords record bit)

Applying a function to a buffer acts independently on its stored fields.

def Algebraic.MassProduction.Nonuniform.BufferInput.completedWire {completed requestWidth slots keyWidth : ℕ} (pending : ℕ) (record : Fin completed) (bit : Fin (storedWidth requestWidth slots keyWidth)) : DeMorgan.Wiring (inputWidth completed pending requestWidth slots keyWidth)

One bit of an already completed record.

Equations

• Algebraic.MassProduction.Nonuniform.BufferInput.completedWire pending record bit = Algebraic.DeMorgan.Wiring.input (Fin.castAdd (pending * requestWidth) (finProdFinEquiv (record, bit)))

def Algebraic.MassProduction.Nonuniform.BufferInput.pendingWire {pending requestWidth : ℕ} (completed slots keyWidth : ℕ) (record : Fin pending) (bit : Fin requestWidth) : DeMorgan.Wiring (inputWidth completed pending requestWidth slots keyWidth)

One bit of a pending request's original data.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferInput.pointWire {completed slots keyWidth : ℕ} (pending requestWidth : ℕ) (source : Fin (completed * slots)) (bit : Fin keyWidth) : DeMorgan.Wiring (inputWidth completed pending requestWidth slots keyWidth)

A stored occupied-point address, with source records flattened by request and slot.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferInput.flagWire {slots completed : ℕ} (inputs : ℕ) (valid : Fin slots → Bool) (source : Fin (completed * slots)) : DeMorgan.Wiring inputs

Scalar-validity flags are repeated for every stored completed request.

Equations

• Algebraic.MassProduction.Nonuniform.BufferInput.flagWire inputs valid source = Algebraic.DeMorgan.Wiring.constant (valid (finProdFinEquiv.symm source).2)

theorem Algebraic.MassProduction.Nonuniform.BufferInput.completedWire_eval {completed requestWidth slots keyWidth pending : ℕ} (completedRecords : Fin completed → Fin (storedWidth requestWidth slots keyWidth) → Bool) (pendingRecords : Fin pending → Fin requestWidth → Bool) (record : Fin completed) (bit : Fin (storedWidth requestWidth slots keyWidth)) : DeMorgan.Wiring.eval (encode completedRecords pendingRecords) (completedWire pending record bit) = completedRecords record bit

Reading a completed record recovers its exact stored bit.

theorem Algebraic.MassProduction.Nonuniform.BufferInput.pendingWire_eval {completed requestWidth slots keyWidth pending : ℕ} (completedRecords : Fin completed → Fin (storedWidth requestWidth slots keyWidth) → Bool) (pendingRecords : Fin pending → Fin requestWidth → Bool) (record : Fin pending) (bit : Fin requestWidth) : DeMorgan.Wiring.eval (encode completedRecords pendingRecords) (pendingWire completed slots keyWidth record bit) = pendingRecords record bit

Reading a pending record recovers its exact original request bit.

theorem Algebraic.MassProduction.Nonuniform.BufferInput.pointWire_eval {completed requestWidth slots keyWidth pending : ℕ} (completedRecords : Fin completed → Fin (storedWidth requestWidth slots keyWidth) → Bool) (pendingRecords : Fin pending → Fin requestWidth → Bool) (record : Fin completed) (slot : Fin slots) (bit : Fin keyWidth) : DeMorgan.Wiring.eval (encode completedRecords pendingRecords) (pointWire pending requestWidth (finProdFinEquiv (record, slot)) bit) = completedRecords record (Fin.natAdd requestWidth (finProdFinEquiv (slot, bit)))

Each occupied-point query uses the stored point-list suffix.

theorem Algebraic.MassProduction.Nonuniform.BufferInput.flagWire_eval {slots inputs completed : ℕ} (valid : Fin slots → Bool) (input : Fin inputs → Bool) (record : Fin completed) (slot : Fin slots) : DeMorgan.Wiring.eval input (flagWire inputs valid (finProdFinEquiv (record, slot))) = valid slot

Repeated validity flags depend only on the scalar slot.