TorchLean

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.

Definition8.3.1
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Definition 8.3.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The operation interface describes programs over shape-indexed tensors and scalar operations without choosing the eager tape or the typed graph recorder at the call site.

Lean code for Definition8.3.1●1 definition
  • abbrevdefined in NN/Runtime/Autograd/Model/Program.lean
    complete
    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.
Definition8.3.2
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 5
Reverse dependency previews
Preview
Definition 8.3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

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
  • structure(1 field)defined in NN/Runtime/Autograd/Engine/Tape.lean
    complete
    structure Runtime.Autograd.Tape (V : Type) : Type
    structure Runtime.Autograd.Tape (V : Type) : Type
    Autograd tape: a grow-only array of nodes.

Node ids are array indices (`Nat`). All operations append exactly one node and return its id, so
reverse mode traverses ids in reverse order.

    Fields

    nodes : Array (Runtime.Autograd.Node V)
    Tape nodes in evaluation order (id = index).
Definition8.3.3
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Graph.lowerGraphDataToTape takes executable typed graph data, its input context and auxiliary data, then returns a runtime tape together with the typed list of inputs and intermediate values.

Lean code for Definition8.3.3●1 definition
  • defdefined in NN/Proofs/Autograd/Runtime/Link/Core.lean
    complete
    def Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape {α Δ : Type}
  [TorchLean.Storage α] {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Algebra.GraphData α Δ Γ ss)
  (x : TorchLean.TensorPack α Γ) (d : Δ) :
  Runtime.Autograd.Tape (Spec.SomeTensor α) ×
    TorchLean.TensorPack α (Γ ++ ss)
    def Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape
  {α Δ : Type} [TorchLean.Storage α]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.GraphData α Δ
      Γ ss)
  (x : TorchLean.TensorPack α Γ) (d : Δ) :
  Runtime.Autograd.Tape
      (Spec.SomeTensor α) ×
    TorchLean.TensorPack α (Γ ++ ss)
    Lower an executable graph (`GraphData`) to a runtime tape by evaluating forward nodes and storing
each node's `vjp` program in its runtime `backward` closure.

PyTorch analogy: this corresponds to building a tape of autograd nodes during the forward pass,
where each node stores enough information to compute parent contributions when given an upstream
cotangent.
Theorem8.3.4
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

For executable typed graph data with Storage and Add, 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. This operational equality retains scalar addition order and needs no commutative-semiring laws, so it does not assume exact real arithmetic for rounded carriers.

Lean code for Theorem8.3.4●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Runtime/Link/BackwardGraph.lean
    complete
    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
    **Main runtime/link theorem**: running the runtime dense backward loop on a tape produced by
`lowerGraphDataToTape` matches the proved full backpropagation `GraphData.backpropAllCtx`.

This is the formal statement that the executable engine implements the same reverse-mode
accumulation semantics as the proved tape model.
Proof for Theorem 8.3.4
uses 0

Induction over the typed graph keeps the forward context and tape indices aligned while the reverse loop accumulates each node's contribution.

Definition8.3.5
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

Checked execution validates and evaluates each node while retaining an indexed primal context and local reverse programs in Compiled. Checked and pure VJP calls use this saved execution through proved compiler simplifications; the reverse-mode Jacobian transforms call it directly.

Lean code for Definition8.3.5●1 definition
  • defdefined in NN/Runtime/Autograd/TypedGraph/Compiled.lean
    complete
    def Runtime.Autograd.TypedGraph.compileChecked {α Δ : Type}
  [TorchLean.Storage α] {Γ ss : List Spec.Shape}
  (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss)
  (inputs : TorchLean.TensorPack α Γ) (data : Δ) :
  Runtime.Autograd.Result (Runtime.Autograd.TypedGraph.Compiled α Γ ss)
    def Runtime.Autograd.TypedGraph.compileChecked
  {α Δ : Type} [TorchLean.Storage α]
  {Γ ss : List Spec.Shape}
  (graph :
    Proofs.Autograd.Algebra.GraphData α Δ
      Γ ss)
  (inputs : TorchLean.TensorPack α Γ)
  (data : Δ) :
  Runtime.Autograd.Result
    (Runtime.Autograd.TypedGraph.Compiled
      α Γ ss)
    Validate and evaluate each node once while recording its certified local reverse program.
Theorem8.3.6
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Taking the tape and forward context from a compiled execution gives the complete result of lowerToTapeChecked, including the same failures, runtime tape, and full primal context.

Lean code for Theorem8.3.6●1 theorem
  • theoremdefined in NN/Runtime/Autograd/TypedGraph/Compiled.lean
    complete
    theorem Runtime.Autograd.TypedGraph.compileChecked_eq_lowerToTapeChecked
  {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape}
  (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss)
  (inputs : TorchLean.TensorPack α Γ) (data : Δ) :
  Except.map
      (fun compiled => (compiled.toTape, compiled.context.toPack))
      (Runtime.Autograd.TypedGraph.compileChecked graph inputs data) =
    Runtime.Autograd.TypedGraph.lowerToTapeChecked graph inputs data
    theorem Runtime.Autograd.TypedGraph.compileChecked_eq_lowerToTapeChecked
  {α Δ : Type} [TorchLean.Storage α]
  {Γ ss : List Spec.Shape}
  (graph :
    Proofs.Autograd.Algebra.GraphData α Δ
      Γ ss)
  (inputs : TorchLean.TensorPack α Γ)
  (data : Δ) :
  Except.map
      (fun compiled =>
        (compiled.toTape,
          compiled.context.toPack))
      (Runtime.Autograd.TypedGraph.compileChecked
        graph inputs data) =
    Runtime.Autograd.TypedGraph.lowerToTapeChecked
      graph inputs data
    Saved execution and tape lowering agree on failures, the tape and every forward value.
Proof for Theorem 8.3.6
uses 0

Each prepared node preserves its forward, validation, and dense VJP programs. The checked lowering induction keeps these programs and the indexed context aligned with the original pack interface.

Theorem8.3.7
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

After successful checked compilation, Compiled.backwardDenseFrom agrees with dense backward on the original lowered tape for every seed pack and every gradient entry. The hypotheses require Storage and Add, preserving the chosen carrier's scalar addition order.

Lean code for Theorem8.3.7●1 theorem
  • theoremdefined in NN/Runtime/Autograd/TypedGraph/Compiled.lean
    complete
    theorem Runtime.Autograd.TypedGraph.compileChecked_backwardDenseFrom_eq_tape
  {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape}
  (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss)
  (inputs : TorchLean.TensorPack α Γ) (data : Δ)
  (compiled : Runtime.Autograd.TypedGraph.Compiled α Γ ss)
  (checked :
    Runtime.Autograd.TypedGraph.compileChecked graph inputs data =
      Except.ok compiled)
  (seed : TorchLean.TensorPack α (Γ ++ ss)) :
  Except.ok (compiled.backwardDenseFrom seed) =
    (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape graph inputs
            data).1.backwardDenseFrom
      seed.toShapeErasedArray
    theorem Runtime.Autograd.TypedGraph.compileChecked_backwardDenseFrom_eq_tape
  {α Δ : Type} [TorchLean.Storage α]
  [Add α] {Γ ss : List Spec.Shape}
  (graph :
    Proofs.Autograd.Algebra.GraphData α Δ
      Γ ss)
  (inputs : TorchLean.TensorPack α Γ)
  (data : Δ)
  (compiled :
    Runtime.Autograd.TypedGraph.Compiled α
      Γ ss)
  (checked :
    Runtime.Autograd.TypedGraph.compileChecked
        graph inputs data =
      Except.ok compiled)
  (seed :
    TorchLean.TensorPack α (Γ ++ ss)) :
  Except.ok
      (compiled.backwardDenseFrom seed) =
    (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape
            graph inputs
            data).1.backwardDenseFrom
      seed.toShapeErasedArray
    The fast backward interface also agrees with the existing dense runtime Tape engine.
Proof for Theorem 8.3.7
uses 1

Saved backward agrees with graph backpropagation for the complete seed context. Composing this with the dense tape agreement gives the result. Neither equality supplies a real derivative law for unrestricted IEEE arithmetic or a GPU kernel theorem.

Theorem8.3.8
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

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, with auxiliary data held fixed.

Lean code for Theorem8.3.8●1 theorem
  • theoremdefined in NN/Runtime/Autograd/TypedGraph/Core.lean
    complete
    theorem Runtime.Autograd.TypedGraph.backwardDenseAllFrom_lowerGraphDataToTape_eq_backpropAllCtx
  {α Δ : Type} [TorchLean.Storage α] [Add α] [Zero α]
  {Γ ss : List Spec.Shape} {τ : Spec.Shape}
  (g : Proofs.Autograd.Algebra.GraphData α Δ Γ ss)
  (x : TorchLean.TensorPack α Γ) (data : Δ)
  (output : Proofs.Idx (Γ ++ ss) τ) (seed : TorchLean.Tensor α τ) :
  Runtime.Autograd.TypedGraph.backwardDenseAllFrom
      (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape g x data).1
      output seed =
    Except.ok
      (g.backpropAllCtx x data
          (Proofs.Autograd.Algebra.TensorPack.single output
            seed)).toShapeErasedArray
    theorem Runtime.Autograd.TypedGraph.backwardDenseAllFrom_lowerGraphDataToTape_eq_backpropAllCtx
  {α Δ : Type} [TorchLean.Storage α]
  [Add α] [Zero α]
  {Γ ss : List Spec.Shape}
  {τ : Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.GraphData α Δ
      Γ ss)
  (x : TorchLean.TensorPack α Γ)
  (data : Δ)
  (output : Proofs.Idx (Γ ++ ss) τ)
  (seed : TorchLean.Tensor α τ) :
  Runtime.Autograd.TypedGraph.backwardDenseAllFrom
      (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape
          g x data).1
      output seed =
    Except.ok
      (g.backpropAllCtx x data
          (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`.
Proof for Theorem 8.3.8
uses 0

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.

Definition8.3.9
Group: Programs, tapes, and typed graphs. (8)
Group member previews
Preview
Definition 8.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

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.9●1 definition
  • inductive(2 constructors, 2 parameters)defined in NN/Runtime/Autograd/Model/Layers/Seq.lean
    complete
    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.