Executable Modules

Executable module operations for manual runtime and example code.

structure TorchLean.Module.RuntimeState (α : Type) [Storage α] [Context α] (stateShapes : List Shape) : Type

Live parameter and buffer storage shared by executable modules.

The shape list remains in the type, so replacing the state cannot silently reorder parameters or load tensors with incompatible dimensions. Mutation is confined to this runtime object; model and layer definitions remain immutable values that can be lowered and reasoned about.

• stateRef : Runtime.Autograd.Torch.ParamList α stateShapes
• runtime : TorchLean.Runtime.Config
• modeRef : IO.Ref TorchLean.nn.Mode
• rngCounter : IO.Ref ℕ

opaque TorchLean.Module.RuntimeState.Internal.create {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (stateRef : Runtime.Autograd.Torch.ParamList α stateShapes) (runtime : Runtime.Config) (modeRef : IO.Ref nn.Mode) (rngCounter : IO.Ref ℕ) : RuntimeState α stateShapes

Assemble runtime state from storage that has already been allocated.

def TorchLean.Module.RuntimeState.Internal.instantiate {α : Type} [Storage α] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {stateShapes : List Shape} (initial : TensorPack Float stateShapes) (runtimeInit : Option (RuntimeInit.Plan stateShapes)) (requiresGrad : Array Bool) (runtime : Runtime.Config) (cast : Float → α) : IO (RuntimeState α stateShapes)

Instantiate runtime state after converting semantic initializer tensors to α.

opaque TorchLean.Module.RuntimeState.Internal.stateRef {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : Runtime.Autograd.Torch.ParamList α stateShapes

Reveal parameter storage only to executable-module implementation code.

opaque TorchLean.Module.RuntimeState.Internal.runtime {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : Runtime.Config

Reveal runtime configuration only to executable-module implementation code.

opaque TorchLean.Module.RuntimeState.Internal.modeRef {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : IO.Ref nn.Mode

Reveal the train/eval mode cell only to executable-module implementation code.

opaque TorchLean.Module.RuntimeState.Internal.rngCounter {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : IO.Ref ℕ

Preserve random-operation order across successive forwards of the same module.

def TorchLean.Module.RuntimeState.mode {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : IO nn.Mode

Read the current behavior of training-sensitive layers.

def TorchLean.Module.RuntimeState.train {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : IO Unit

Enable training behavior.

def TorchLean.Module.RuntimeState.eval {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : IO Unit

Enable evaluation behavior.

def TorchLean.Module.RuntimeState.isTraining {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (state : RuntimeState α stateShapes) : IO Bool

Return true exactly when the state uses training behavior.

def TorchLean.Module.RuntimeState.state {α : Type} [Storage α] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] {stateShapes : List Shape} (runtimeState : RuntimeState α stateShapes) : IO (nn.State α stateShapes)

Read all parameters and buffers, synchronizing device storage when necessary.

def TorchLean.Module.RuntimeState.setState {α : Type} [Storage α] [Context α] {stateShapes : List Shape} (runtimeState : RuntimeState α stateShapes) (values : nn.State α stateShapes) : IO Unit

Replace all parameters and buffers with a shape-compatible state.

structure TorchLean.nn.Module (α : Type) [Storage α] [Context α] {σ τ : Shape} (model : Sequential σ τ) : Type

An ordinary tensor model with live, mutable runtime state.

nn.Sequential remains the immutable, shape-checked model definition used by proofs and graph lowering. An nn.Module is its runtime counterpart: it owns one parameter set and a mutable train/eval flag. This separation gives executable code the familiar module lifecycle without hiding mutation inside the mathematical model.

• runtimeState : TorchLean.Module.RuntimeState α (Runtime.Autograd.Model.Layers.Seq.stateShapes model)

structure TorchLean.nn.IndexedModule (α β : Type) [Storage α] [Storage β] [Context α] {σ τ : Shape} (model : IndexedModel σ τ β) : Type

An indexed-input model with live, mutable runtime state.

• runtimeState : TorchLean.Module.RuntimeState α model.stateShapes

opaque TorchLean.nn.Module.Internal.fromRuntimeState {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (state : Module.RuntimeState α (stateShapes model)) : Module α model

Wrap live runtime state behind the public module boundary.

opaque TorchLean.nn.Module.Internal.runtimeState {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (module : Module α model) : Module.RuntimeState α (stateShapes model)

Reveal live runtime state only to module implementation code.

def TorchLean.nn.Module.instantiate {σ τ : Shape} (model : Sequential σ τ) (runtime : Runtime.Config := { }) (α : Type := Float32) [Storage α] [Context α] [Runtime.FromFloat α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] : IO (Module α model)

Instantiate a checked model with mutable parameter and buffer storage.

Native binary32 is the default. Select another supported element type with nn.Module.instantiate model (α := Float).

def TorchLean.nn.Module.mode {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (module : Module α model) : IO Mode

Read whether training-sensitive layers currently use training or evaluation behavior.

def TorchLean.nn.Module.train {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (module : Module α model) : IO Unit

Enable training behavior for dropout, normalization buffers, and similar layers.

def TorchLean.nn.Module.eval {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (module : Module α model) : IO Unit

Enable deterministic evaluation behavior for training-sensitive layers.

def TorchLean.nn.Module.isTraining {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (module : Module α model) : IO Bool

Return true exactly when this module uses training behavior.

def TorchLean.nn.Module.state {σ τ : Shape} {α : Type} [Storage α] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] {model : Sequential σ τ} (module : Module α model) : IO (State α (stateShapes model))

Read the complete parameter-and-buffer state, synchronizing device storage when necessary.

def TorchLean.nn.Module.setState {σ τ : Shape} {α : Type} [Storage α] [Context α] {model : Sequential σ τ} (module : Module α model) (state : State α (stateShapes model)) : IO Unit

Replace the complete shape-indexed parameter-and-buffer state.

def TorchLean.nn.Module.Internal.forwardWithMode {σ τ : Shape} {α : Type} [Storage α] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {model : Sequential σ τ} (module : Module α model) (mode : Mode) (input : Tensor α σ) : IO (Tensor α τ)

Execute one ordinary module forward in an explicit mode without changing its mode cell.

def TorchLean.nn.Module.forward {σ τ : Shape} {α : Type} [Storage α] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {model : Sequential σ τ} (module : Module α model) (input : Tensor α σ) : IO (Tensor α τ)

Evaluate one concrete input without constructing a backward tape.

The module's mode controls training-sensitive layer behavior. Training forwards update running buffers from their actual activations and advance the module's random stream. This concrete call does not construct a backward tape; differentiable model programs use nn.forward.

def TorchLean.nn.Module.predict {σ τ : Shape} {α : Type} [Storage α] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {model : Sequential σ τ} (module : Module α model) (input : Tensor α σ) : IO (Tensor α τ)

Evaluation-mode inference without changing the module's persistent mode.

Keeping the override local to this call prevents concurrent forwards from observing a temporary mode change.

opaque TorchLean.nn.IndexedModule.Internal.fromRuntimeState {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (state : Module.RuntimeState α model.stateShapes) : IndexedModule α β model

Wrap live runtime state behind the public indexed-module boundary.

opaque TorchLean.nn.IndexedModule.Internal.runtimeState {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) : Module.RuntimeState α model.stateShapes

Reveal live runtime state only to indexed-module implementation code.

def TorchLean.nn.IndexedModule.instantiate {σ τ : Shape} {β : Type} [Storage β] (model : IndexedModel σ τ β) (runtime : Runtime.Config := { }) (α : Type := Float32) [Storage α] [Context α] [Runtime.FromFloat α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] : IO (IndexedModule α β model)

Instantiate an indexed model. Native binary32 is the default runtime element type.

def TorchLean.nn.IndexedModule.mode {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) : IO Mode

Read the current behavior of training-sensitive layers.

def TorchLean.nn.IndexedModule.train {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) : IO Unit

Enable training behavior.

def TorchLean.nn.IndexedModule.eval {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) : IO Unit

Enable evaluation behavior.

def TorchLean.nn.IndexedModule.isTraining {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) : IO Bool

Return true exactly when the module uses training behavior.

def TorchLean.nn.IndexedModule.state {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) : IO (State α model.stateShapes)

Read the complete parameter-and-buffer state.

def TorchLean.nn.IndexedModule.setState {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) (state : State α model.stateShapes) : IO Unit

Replace the complete shape-indexed parameter-and-buffer state.

def TorchLean.nn.IndexedModule.Internal.forwardWithMode {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) (mode : Mode) (input : Tensor β σ) : IO (Tensor α τ)

Execute one indexed module forward in an explicit mode without changing its mode cell.

def TorchLean.nn.IndexedModule.forward {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) (input : Tensor β σ) : IO (Tensor α τ)

Evaluate one validated index tensor without constructing a backward tape.

def TorchLean.nn.IndexedModule.predict {σ τ : Shape} {α β : Type} [Storage α] [Storage β] [Context α] [tensorTransfer : Runtime.Autograd.Torch.TensorTransfer α] {model : IndexedModel σ τ β} (module : IndexedModule α β model) (input : Tensor β σ) : IO (Tensor α τ)

Evaluation-mode inference without changing the module's persistent mode.

Keeping the override local to this call prevents concurrent forwards from observing a temporary mode change.

def TorchLean.Module.Supervised.predict {σ τ : Shape} {α : Type} [Storage α] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] (options : Runtime.Config) (model : nn.Sequential σ τ) (objective : Objective α Unit (Runtime.Autograd.Model.Layers.Seq.stateShapes model) [σ, τ]) (input : Tensor α σ) : IO (Tensor α τ)

Run evaluation-mode prediction through a supervised runtime module.

def TorchLean.Module.Internal.sampleLoss {σ τ : Shape} {α : Type} [Storage α] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] (model : nn.Sequential σ τ) (objective : Objective α Unit (Runtime.Autograd.Model.Layers.Seq.stateShapes model) [σ, τ]) (sample : Sample.Supervised α σ τ) : IO α

Evaluate one supervised sample through a runtime module and return the scalar loss value.

This packages the common internal pattern Module.Objective.loss ...; Tensor.item.

def TorchLean.Module.Internal.bindOptimizer {α β : Type} [Storage α] [Storage β] [Context α] {stateShapes inputShapes dataInputShapes : List Shape} (objective : Objective α β stateShapes inputShapes dataInputShapes) (optimizer : Runtime.Autograd.Model.Optim.Optimizer α stateShapes) : IO (Runtime.Autograd.Model.Module.BoundOptimizer α β stateShapes inputShapes dataInputShapes optimizer.State)

Bind an optimizer to the hidden runtime objective.

def TorchLean.Module.Objective.dataLossEvaluator {α β : Type} [Storage α] [Storage β] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] {stateShapes : List Shape} {firstShape secondShape : Shape} (objective : Objective α β stateShapes [] [firstShape, secondShape]) (definition : ObjectiveDefinition β stateShapes [] [firstShape, secondShape]) : IO (Tensor β firstShape → Tensor β secondShape → IO (Tensor α []))

Create a reusable evaluator for a data-only objective that shares an executable module's state.

The returned function accepts ordinary tensors and hides both the heterogeneous pack representation and the reusable eager session used underneath.

def TorchLean.Module.Objective.indexedPredictor {α β : Type} [Storage α] [Storage β] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] {stateShapes : List Shape} {σ τ : Shape} (objective : Objective α β stateShapes [] [σ, σ]) (model : nn.IndexedModel σ τ β) : IO (Tensor β σ → IO (Tensor α τ))

Create a reusable evaluation-mode predictor for an indexed model sharing this objective's state.

This is useful after training an indexed loss: prediction sees the updated parameters without requiring callers to construct a runtime program, evaluator, or tensor pack.

def TorchLean.Module.Internal.withConfiguredOptimizer {α Result : Type} [Storage α] [Context α] [Runtime.FromFloat α] {stateShapes : List Shape} (runtime : Runtime.Config) (config : optim.Optimizer) (continuation : Runtime.Autograd.Model.Optim.Optimizer α stateShapes → IO Result) : IO Result

Validate and instantiate the optimizer shared by manual and mixed-dtype module loops.

def TorchLean.Module.Internal.packStep {α : Type} [Storage α] [Context α] [Runtime.FromFloat α] {stateShapes inputShapes : List Shape} (objective : Objective α Unit stateShapes inputShapes) (config : optim.Optimizer) : IO (Arguments α inputShapes → IO Unit)

Create a one-step update function for any typed module input pack from the public optimizer config used by the trainer API.

Generic bridge for custom training loops: richer examples can keep their own control flow while still choosing a public optim.* config through the same API as Trainer.RunConfig.

def TorchLean.Module.Objective.dataStep {α β : Type} [Storage α] [Storage β] [Context α] [Runtime.FromFloat α] {stateShapes : List Shape} {firstShape secondShape : Shape} (objective : Objective α β stateShapes [] [firstShape, secondShape]) (config : optim.Optimizer) : IO (Tensor β firstShape → Tensor β secondShape → IO Unit)

Create a two-input update function for a mixed-dtype, data-only objective.

The returned function takes ordinary typed tensors. Optimizer state and heterogeneous runtime packs remain implementation details. Configuration values must remain in their required domains after conversion to the optimizer scalar, as checked by its Runtime.FromFloat instance. CUDA also requires binary32-valid settings even when the host scalar is Float.