Semantic model of the halving scheduler buffer

Completed and pending positions partition the original request identities. Completed records store a direction's full affine point list; validity flags turn these stored lists into exactly the occupied punctured lines.

structure Algebraic.MassProduction.Nonuniform.BufferModel.State (total completed pending dimension width : ℕ) : Type

Request partition and chosen directions for completed requests.

• order : Fin completed ⊕ Fin pending ≃ Fin total

  Every original request occurs at exactly one completed or pending position.

• directions : Fin completed → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)

  Recovery direction assigned to each completed request.

def Algebraic.MassProduction.Nonuniform.BufferModel.pendingTargets {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin pending) : Fin dimension → BinaryExtension width

Target tuple in current pending order.

Equations

• Algebraic.MassProduction.Nonuniform.BufferModel.pendingTargets state targets request = targets (state.order (Sum.inr request))

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.line {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin completed) : Finset (Fin dimension → BinaryExtension width)

Recovery line stored at a completed position.

Equations

• Algebraic.MassProduction.Nonuniform.BufferModel.line state targets request = Algebraic.MassProduction.puncturedLine (targets (state.order (Sum.inl request))) (state.directions request)

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.occupied {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) : Finset (Fin dimension → BinaryExtension width)

Union of every completed recovery line.

Equations

• Algebraic.MassProduction.Nonuniform.BufferModel.occupied state targets = Finset.univ.biUnion (Algebraic.MassProduction.Nonuniform.BufferModel.line state targets)

def Algebraic.MassProduction.Nonuniform.BufferModel.WellScheduled {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) : Prop

The geometric invariant for completed requests.

Equations

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

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.completedRecord {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin completed) : Fin (BufferInput.storedWidth requestWidth (2 ^ width) (dimension * width)) → Bool

Original data followed by a complete scalar-indexed affine point list.

Equations

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

def Algebraic.MassProduction.Nonuniform.BufferModel.pendingRecord {total completed pending dimension width requestWidth : ℕ} (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (request : Fin pending) : Fin requestWidth → Bool

Pending records contain only their original request data.

Equations

• Algebraic.MassProduction.Nonuniform.BufferModel.pendingRecord state data request = data (state.order (Sum.inr request))

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.input {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) : Fin (BufferInput.inputWidth completed pending requestWidth (2 ^ width) (dimension * width)) → Bool

The concrete input encoding represented by a scheduler state.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferModel.pendingRecord_injective {total completed pending dimension width requestWidth : ℕ} (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (distinct : Function.Injective data) : Function.Injective (pendingRecord state data)

Pending request identities remain distinct in the buffer.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.completedRecord_data {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin completed) (bit : Fin requestWidth) : completedRecord positive state data targets request (Fin.castAdd (2 ^ width * (dimension * width)) bit) = data (state.order (Sum.inl request)) bit

The original-data projection of a completed record is unchanged.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.completedRecord_point {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin completed) (slot : Fin (2 ^ width)) (bit : Fin (dimension * width)) : completedRecord positive state data targets request (Fin.natAdd requestWidth (finProdFinEquiv (slot, bit))) = binaryExtensionVectorBits positive (PaddedLinePoints.point positive (targets (state.order (Sum.inl request))) (state.directions request) slot) bit

The point-list projection contains the represented affine-line point.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.pointWire_eval {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin completed) (slot : Fin (2 ^ width)) (bit : Fin (dimension * width)) : DeMorgan.Wiring.eval (input positive state data targets) (BufferInput.pointWire pending requestWidth (finProdFinEquiv (request, slot)) bit) = binaryExtensionVectorBits positive (PaddedLinePoints.point positive (targets (state.order (Sum.inl request))) (state.directions request) slot) bit

The source wires of the buffer expose the represented stored point.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.pendingWire_eval {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin pending) (bit : Fin requestWidth) : DeMorgan.Wiring.eval (input positive state data targets) (BufferInput.pendingWire completed (2 ^ width) (dimension * width) request bit) = data (state.order (Sum.inr request)) bit

Reading the pending-data wires gives the original request record.