Execution of composed models

Sequential composition preserves the order of model state, forward calls, and buffer updates. These equations keep the execution monad and scalar backend abstract. They therefore apply to graph recording as well as eager execution, without expanding either backend's operation instance.

@[simp]

theorem Runtime.Autograd.Model.Layers.Seq.stateShapes_comp {σ τ υ : Spec.Shape} (first : Seq σ τ) (second : Seq τ υ) : (first >>> second).stateShapes = first.stateShapes ++ second.stateShapes

Composed models retain the state of the first model followed by the second model's state.

theorem Runtime.Autograd.Model.Layers.Seq.forward_apply {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {σ τ : Spec.Shape} (model : Seq σ τ) (mode : Mode) (state : RefList Ref model.stateShapes) (x : Ref σ) : (model.forward mode).uncurry (state.append (Torch.RefList.cons x Torch.RefList.nil)) = model.forwardState mode state x

Applying a model's curried program passes its state and input to the sequential evaluator.

theorem Runtime.Autograd.Model.Layers.Seq.forwardState_fromLayer_eval {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [LawfulMonad m] [Ops m α] {σ τ : Spec.Shape} (layer : Layer σ τ) (state : RefList Ref layer.stateShapes) (x : Ref σ) : (fromLayer layer).forwardState Mode.eval (state.append Torch.RefList.nil) x = layer.forwardRef Mode.eval state x

A single-layer model in evaluation mode runs that layer without a buffer-update callback.

theorem Runtime.Autograd.Model.Layers.Seq.forwardState_comp {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [LawfulMonad m] [Ops m α] {σ τ υ : Spec.Shape} (first : Seq σ τ) (second : Seq τ υ) (mode : Mode) (firstState : RefList Ref first.stateShapes) (secondState : RefList Ref second.stateShapes) (x : Ref σ) : (first >>> second).forwardState mode (⋯ ▸ firstState.append secondState) x = first.forwardState mode firstState x >>= second.forwardState mode secondState

Composed model execution is monadic composition, with the original state and effect order.

In training mode this includes buffer-update callbacks after each layer. The proof uses only monad laws; it neither commutes effects nor assumes algebraic laws on numerical operations.