8.3. Autograd and Execution
The runtime has a dynamic tape for eager execution and a typed SSA builder for typed graph
execution. Both sit below the layer API. A separate bridge executes NN.IR.Graph through a
forward-only graph; its correctness theorem names its single remaining side condition.
The operation interface describes programs over shape-indexed tensors and scalar operations without choosing eager or typed graph execution at the call site.
Lean code for Definition8.3.1●1 definition
Associated Lean declarations
-
Runtime.Autograd.Model.Program[complete]
-
Runtime.Autograd.Model.Program[complete]
-
abbrevdefined in NN/Runtime/Autograd/Model/Program.leancomplete
abbrev Runtime.Autograd.Model.Program (α : Type) [TorchLean.Storage α] [Context α] (ss : List Spec.Shape) (τ : Spec.Shape) : Type 1
abbrev Runtime.Autograd.Model.Program (α : Type) [TorchLean.Storage α] [Context α] (ss : List Spec.Shape) (τ : Spec.Shape) : Type 1
An execution-polymorphic differentiable tensor program.
The CPU tape is a dynamic computation DAG. It stores shape-erased values and accumulates reverse-mode gradients by node index.
Shape erasure lets one array hold a vector input, a matrix intermediate, and a scalar loss. Typed graph lowering must preserve which index names each value. During reverse accumulation, multiple uses of an intermediate contribute to the same stored cotangent, so index alignment matters for both reading forward values and adding backward contributions.
Lean code for Definition8.3.2●1 definition
Associated Lean declarations
-
Runtime.Autograd.Tape[complete]
-
Runtime.Autograd.Tape[complete]
-
structuredefined in NN/Runtime/Autograd/Engine/Core/Base.leancomplete
structure Runtime.Autograd.Tape (α : Type) [TorchLean.Storage α] : Type
structure Runtime.Autograd.Tape (α : Type) [TorchLean.Storage α] : Type
Autograd tape: a grow-only array of nodes. Node ids are array indices (`Nat`). All ops append exactly one node and return its id. This makes it easy to implement reverse-mode by traversing ids in reverse order.
Fields
nodes : Array (Runtime.Autograd.Node α)
Tape nodes in evaluation order. Node ids are array indices (`Nat`). Each tape op appends exactly one node and returns its id.
lowerToTape takes executable typed graph data and its input context, then returns a
runtime tape together with the typed list of inputs and intermediate
values.
Lean code for Definition8.3.3●1 definition
Associated Lean declarations
-
Runtime.Autograd.TypedGraph.lowerToTape[complete]
-
Runtime.Autograd.TypedGraph.lowerToTape[complete]
-
defdefined in NN/Runtime/Autograd/TypedGraph/Core.leancomplete
def Runtime.Autograd.TypedGraph.lowerToTape {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : Runtime.Autograd.TypedGraph.GraphData α Γ ss) (x : TorchLean.TensorPack α Γ) : Runtime.Autograd.Tape α × TorchLean.TensorPack α (Γ ++ ss)
def Runtime.Autograd.TypedGraph.lowerToTape {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : Runtime.Autograd.TypedGraph.GraphData α Γ ss) (x : TorchLean.TensorPack α Γ) : Runtime.Autograd.Tape α × TorchLean.TensorPack α (Γ ++ ss)
Lower an executable `GraphData` into a runtime tape. This is the bridge from the shape-indexed SSA representation to the runtime tape engine: `Graph.lowerGraphDataToTape` emits a `Runtime.Autograd.Tape` whose nodes replay the graph and whose backward closures implement the graph's VJP rules. The graph remains the persistent artifact; the tape contains the runtime closures needed for one execution and reverse pass.
For executable typed graph data over a commutative semiring, dense reverse accumulation on the lowered tape equals proof-level graph backpropagation after both contexts are converted to the tape's value array.
This is agreement with the graph's stored executable backward rules. It shows that lowering and accumulation preserve those rules; it does not establish their derivative formulas. Local derivative laws are a separate obligation. The commutative-semiring hypotheses also matter: they support the algebra used to combine contributions and cannot be assumed for arbitrary rounded arithmetic.
Lean code for Theorem8.3.4●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Proofs/Autograd/Runtime/Link/BackwardGraphData.leancomplete
theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphDataToTape_eq_backpropAllCtx {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (g : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d0 : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape g x d0).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (g.backpropAllCtx x d0 seed).toShapeErasedArray
theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphDataToTape_eq_backpropAllCtx {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (g : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d0 : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape g x d0).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (g.backpropAllCtx x d0 seed).toShapeErasedArray
Variant of `backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx` for the `GraphData` interface. This is useful when a graph carries extra payload `Δ` (e.g. parameters/config) through forward and backward closures.
Induction over the typed graph keeps the forward context and tape indices aligned while the reverse loop accumulates each node's contribution.
For any typed output reference, including an input or intermediate node, lowering to the runtime tape and running reverse mode agrees with seeding that same output in executable graph backpropagation.
Lean code for Theorem8.3.5●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Runtime/Autograd/TypedGraph/Core.leancomplete
theorem Runtime.Autograd.TypedGraph.backwardDenseAllFrom_lowerToTape_eq_backpropAllCtx {α : Type} [CommSemiring α] {Γ ss : List Spec.Shape} {τ : Spec.Shape} (g : Runtime.Autograd.TypedGraph.GraphData α Γ ss) (x : TorchLean.TensorPack α Γ) (output : Proofs.Idx (Γ ++ ss) τ) (seed : TorchLean.Tensor α τ) : Runtime.Autograd.TypedGraph.backwardDenseAllFrom (Runtime.Autograd.TypedGraph.lowerToTape g x).1 output seed = Except.ok (Proofs.Autograd.Algebra.GraphData.backpropAllCtx g x () (Proofs.Autograd.Algebra.TensorPack.single output seed)).toShapeErasedArray
theorem Runtime.Autograd.TypedGraph.backwardDenseAllFrom_lowerToTape_eq_backpropAllCtx {α : Type} [CommSemiring α] {Γ ss : List Spec.Shape} {τ : Spec.Shape} (g : Runtime.Autograd.TypedGraph.GraphData α Γ ss) (x : TorchLean.TensorPack α Γ) (output : Proofs.Idx (Γ ++ ss) τ) (seed : TorchLean.Tensor α τ) : Runtime.Autograd.TypedGraph.backwardDenseAllFrom (Runtime.Autograd.TypedGraph.lowerToTape g x).1 output seed = Except.ok (Proofs.Autograd.Algebra.GraphData.backpropAllCtx g x () (Proofs.Autograd.Algebra.TensorPack.single output seed)).toShapeErasedArray
Lowering a typed graph to the runtime tape preserves reverse mode from any typed output reference. The result covers outputs that are inputs or intermediate nodes, not only the final recorded node. It states fidelity to the executable VJP stored in `GraphData`; derivative correctness requires the separate local laws carried by `Proofs.Autograd.Algebra.Node`.
The general graph-data lowering theorem is instantiated with a seed context containing the supplied cotangent at exactly the selected output reference.
Selecting an intermediate asks for the sensitivity of that intermediate, rather than of the last node in the graph. Selecting an input is meaningful too. The seed identifies both the value being differentiated and the cotangent applied there, so both routes must seed the same reference.
For the executable graph data in a typed-graph session snapshot, dense reverse accumulation on
the lowered tape agrees with graph backpropagation. Runtime leaf
names and requiresGrad masks are attached after this raw graph-data lowering theorem.
Lean code for Theorem8.3.6●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Runtime/Autograd/Torch/TypedGraphSession/Autograd.leancomplete
theorem Runtime.Autograd.Torch.Internal.TypedGraphSession.backwardDenseFrom_lowerGraphDataToTape_eq_backpropAllCtx {α : Type} [TorchLean.Storage α] [CommSemiring α] (st : Runtime.Autograd.Torch.Internal.TypedGraphSessionState α) (seed : TorchLean.TensorPack α (st.Γ ++ st.ss)) : (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape st.g st.x st.nat).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (st.g.backpropAllCtx st.x st.nat seed).toShapeErasedArray
theorem Runtime.Autograd.Torch.Internal.TypedGraphSession.backwardDenseFrom_lowerGraphDataToTape_eq_backpropAllCtx {α : Type} [TorchLean.Storage α] [CommSemiring α] (st : Runtime.Autograd.Torch.Internal.TypedGraphSessionState α) (seed : TorchLean.TensorPack α (st.Γ ++ st.ss)) : (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape st.g st.x st.nat).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (st.g.backpropAllCtx st.x st.nat seed).toShapeErasedArray
Running the runtime reverse-mode loop on the lowered tape equals `GraphData` backpropagation. `lowerGraphDataToTape` produces a tape, and `Tape.backwardDenseFrom` is equal to `GraphData.backpropAllCtx` up to the `TorchLean.TensorPack.toShapeErasedArray` representation change. This theorem proves the lowering faithful to the stored VJP program. It does not prove that the VJP is the derivative of the stored forward function; that stronger statement requires proof-carrying `Node`s.
The typed-graph session theorem specializes the graph-data backward theorem to the session's graph, inputs, and auxiliary index environment.
Layer definitions carry parameter and buffer initialization, training or evaluation mode, and shape-checked sequential composition. They build their computations through the runtime operation interface.
Lean code for Definition8.3.7●1 definition
Associated Lean declarations
-
Runtime.Autograd.Model.Layers.Seq[complete]
-
Runtime.Autograd.Model.Layers.Seq[complete]
-
inductivedefined in NN/Runtime/Autograd/Model/Layers/Seq.leancomplete
inductive Runtime.Autograd.Model.Layers.Seq : Spec.Shape → Spec.Shape → Type 1
inductive Runtime.Autograd.Model.Layers.Seq : Spec.Shape → Spec.Shape → Type 1
Sequential composition of `Layer`s, indexed by input/output shape. This is the builder-layer analogue of `torch.nn.Sequential`: a `Seq σ τ` represents a model that takes an input of shape `σ` and produces an output of shape `τ` by running layers left-to-right. `Seq` lives in `Type 1`, and no lower. Each `Layer` stores its forward pass as an execution-polymorphic `Program`, which quantifies over the scalar type `α : Type` and the interpreter monad `m : Type → Type`, so `Layer σ τ : Type 1` and any type that stores a `Layer` is at least `Type 1`. Consequently `IO (Seq σ τ)` is ill-typed; build models purely with `nn.build seed builder`, draw a seed in `IO` with `nn.buildIO`, or pass the model to a continuation with `nn.withModel`.
Constructors
Runtime.Autograd.Model.Layers.Seq.id (s : Spec.Shape) : Runtime.Autograd.Model.Layers.Seq s s
The empty sequence, which leaves a tensor unchanged.
Runtime.Autograd.Model.Layers.Seq.cons {σ τ υ : Spec.Shape} : Runtime.Autograd.Model.Layers.Layer σ τ → Runtime.Autograd.Model.Layers.Seq τ υ → Runtime.Autograd.Model.Layers.Seq σ υ
Run one layer, then the remaining sequence.
Lean code for Definition8.3.8●1 definition
Associated Lean declarations
-
defdefined in NN/Runtime/Autograd/IRExec/API.leancomplete
def Runtime.Autograd.IRExec.lowerToForwardGraph {α : Type} [TorchLean.Storage α] [Context α] (g : NN.IR.Graph) (payload : NN.IR.Payload α) : Except String (Runtime.Autograd.IRExec.ForwardGraph α)
def Runtime.Autograd.IRExec.lowerToForwardGraph {α : Type} [TorchLean.Storage α] [Context α] (g : NN.IR.Graph) (payload : NN.IR.Payload α) : Except String (Runtime.Autograd.IRExec.ForwardGraph α)
Lower an op-tagged IR graph into an executable `ForwardGraph`. Requirements: - Node id 0 must be `.input`. - The graph must satisfy `Graph.checkWellFormed`. - The external payload must contain entries for every `.const`/`.linear`/`.conv` node id. This returns a `ForwardGraph` whose `eval` computes all node values in topological order. The artifact is intentionally forward-only; it is distinct from the differentiable `Torch.TypedGraph` used by the autograd lowering path. This is the main API consumed by runtime callers that want executable evaluation while remaining aligned with the shared `NN.IR.Graph` semantics.
Lean code for Theorem8.3.9●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Runtime/Autograd/IRExec/Correctness/SemanticEquivalence.leancomplete
theorem Runtime.Autograd.IRExec.denoteAll_eq_of_lowerToForwardGraph {α : Type} [TorchLean.Storage α] [Context α] (g : NN.IR.Graph) (payload : NN.IR.Payload α) (exec : Runtime.Autograd.IRExec.ForwardGraph α) (hNoRawLog : Runtime.Autograd.IRExec.NoRawLog g) (h : Runtime.Autograd.IRExec.lowerToForwardGraph g payload = Except.ok exec) (x : TorchLean.Tensor α exec.inShape) : g.denoteAll payload { shape := exec.inShape, tensor := x } = Except.ok (exec.denoteAll x)
theorem Runtime.Autograd.IRExec.denoteAll_eq_of_lowerToForwardGraph {α : Type} [TorchLean.Storage α] [Context α] (g : NN.IR.Graph) (payload : NN.IR.Payload α) (exec : Runtime.Autograd.IRExec.ForwardGraph α) (hNoRawLog : Runtime.Autograd.IRExec.NoRawLog g) (h : Runtime.Autograd.IRExec.lowerToForwardGraph g payload = Except.ok exec) (x : TorchLean.Tensor α exec.inShape) : g.denoteAll payload { shape := exec.inShape, tensor := x } = Except.ok (exec.denoteAll x)
End-to-end semantic equivalence for successful IR lowering. If `lowerToForwardGraph` returns an executable graph, evaluating that executable graph on any input matches the denotational semantics of the original IR graph. One side condition remains. `NoRawLog` excludes raw `.log`: the IR evaluator rejects nonpositive inputs while the lowered closure applies `Tensor.logSpec` to every input, so the two can only be compared under a positivity precondition the theorem does not carry. Every other operation kind is covered, including `.mseLoss` and `.concat` along any axis. The lowering accepts exactly the shapes the IR semantics accepts for `.matmul` and `.linear` (any shared leading shape, so rank at least four matmul and batched linear are covered); shapes rejected by the lowering never reach this theorem because `lowerToForwardGraph` returns an error for them.