Composable buffer transformation contract

A buffer circuit preserves one original dataset and its geometric targets, updates only the completed/pending state, and retains pairwise disjointness. This property composes directly for circuits with successive buffer sizes.

def Algebraic.MassProduction.Nonuniform.BufferModel.Transforms {width dimension requestWidth completed pending nextCompleted nextPending : ℕ} (positive : 0 < width) (targetProjection : Fin (dimension * width) → Fin requestWidth) (circuit : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth (2 ^ width) (dimension * width)) (BufferInput.inputWidth nextCompleted nextPending requestWidth (2 ^ width) (dimension * width))) (total : ℕ) : Prop

A circuit maps every valid encoded input state to a valid encoded output state over the same original request dataset and targets.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferModel.Transforms.comp {width dimension requestWidth completed pending middleCompleted middlePending nextCompleted nextPending total : ℕ} (positive : 0 < width) (targetProjection : Fin (dimension * width) → Fin requestWidth) (first : Circuit DeMorgan.signature (BufferInput.inputWidth completed pending requestWidth (2 ^ width) (dimension * width)) (BufferInput.inputWidth middleCompleted middlePending requestWidth (2 ^ width) (dimension * width))) (last : Circuit DeMorgan.signature (BufferInput.inputWidth middleCompleted middlePending requestWidth (2 ^ width) (dimension * width)) (BufferInput.inputWidth nextCompleted nextPending requestWidth (2 ^ width) (dimension * width))) (firstCorrect : Transforms positive targetProjection first total) (lastCorrect : Transforms positive targetProjection last total) : Transforms positive targetProjection (last.comp first) total

Model-preserving buffer circuits compose with no change to their shared dataset.