TorchLean

8.3. Autograd and Execution🔗

The runtime has a dynamic tape for eager execution and a typed SSA builder for compiled programs. Both sit below the layer API. A separate bridge executes the supported fragment of NN.IR.Graph; its correctness theorem states the fragment explicitly.

Definition8.3.1
Group: Programs, tapes, and compiled execution. (5)
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.6
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 eager or compiled execution at the call site.

Lean code for Definition8.3.1●1 definition
  • abbrevdefined in NN/Runtime/Autograd/TorchLean/Backend.lean
    complete
    abbrev Runtime.Autograd.TorchLean.Program (α : Type) [Context α]
  [DecidableEq Spec.Shape] (ss : List Spec.Shape) (τ : Spec.Shape) :
  Type 1
    abbrev Runtime.Autograd.TorchLean.Program
  (α : Type) [Context α]
  [DecidableEq Spec.Shape]
  (ss : List Spec.Shape)
  (τ : Spec.Shape) : Type 1
    A TorchLean program is backend-polymorphic: it can run in any `m` that implements `Ops`.

In practice:
- `m := Runtime.Autograd.Session` gives you eager execution (and an autograd tape),
- `m := Runtime.Autograd.Compiled.M` records an SSA/DAG suitable for compilation/verification.
Definition8.3.2
Group: Programs, tapes, and compiled execution. (5)
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 4
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.

Lean code for Definition8.3.2●1 definition
  • structure(1 field)defined in NN/Runtime/Autograd/Engine/Core/Core.lean
    complete
    structure Runtime.Autograd.Tape (α : Type) : Type
    structure Runtime.Autograd.Tape (α : Type) : 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.
Definition8.3.3
Group: Programs, tapes, and compiled execution. (5)
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

compile 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
  • defdefined in NN/Runtime/Autograd/Compiled/Core.lean
    complete
    def Runtime.Autograd.Compiled.compile {α : Type} [DecidableEq Spec.Shape]
  {Γ ss : List Spec.Shape}
  (g : Runtime.Autograd.Compiled.GraphData α Γ ss)
  (x : Runtime.Autograd.Compiled.TList α Γ) :
  Runtime.Autograd.Tape α × Runtime.Autograd.Compiled.TList α (Γ ++ ss)
    def Runtime.Autograd.Compiled.compile
  {α : Type} [DecidableEq Spec.Shape]
  {Γ ss : List Spec.Shape}
  (g :
    Runtime.Autograd.Compiled.GraphData α
      Γ ss)
  (x :
    Runtime.Autograd.Compiled.TList α Γ) :
  Runtime.Autograd.Tape α ×
    Runtime.Autograd.Compiled.TList α
      (Γ ++ ss)
    Compile an executable `GraphData` into a runtime eager tape.

This is the bridge from the proof-compiled SSA representation to the runtime tape engine:
`Graph.compileAuxData` emits a `Runtime.Autograd.Tape` whose nodes replay the graph and whose
backward closures implement the graph's VJP rules.

PyTorch comparison: conceptually similar to the front half of `torch.compile` / TorchDynamo
(tracing a computation to an IR), except our target is an explicit autograd tape for which we
also maintain proof links.
Theorem8.3.4
Group: Programs, tapes, and compiled execution. (5)
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 over a commutative semiring, dense reverse accumulation on the compiled tape equals proof-level graph backpropagation after both contexts are converted to the tape's value array.

Lean code for Theorem8.3.4●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Runtime/Link/BackwardGraphData.lean
    complete
    theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAuxData_eq_backpropAllCtx
  {α Δ : Type} [DecidableEq Spec.Shape] [CommSemiring α]
  {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Algebra.GraphData α Δ Γ ss)
  (x : Proofs.Autograd.Algebra.TList α Γ) (d0 : Δ)
  (seed : Proofs.Autograd.Algebra.TList α (Γ ++ ss)) :
  (Proofs.Autograd.Algebra.Graph.compileAuxData g x
            d0).1.backwardDenseFrom
      seed.toAnyArray =
    Except.ok (g.backpropAllCtx x d0 seed).toAnyArray
    theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAuxData_eq_backpropAllCtx
  {α Δ : Type} [DecidableEq Spec.Shape]
  [CommSemiring α]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.GraphData α Δ
      Γ ss)
  (x : Proofs.Autograd.Algebra.TList α Γ)
  (d0 : Δ)
  (seed :
    Proofs.Autograd.Algebra.TList α
      (Γ ++ ss)) :
  (Proofs.Autograd.Algebra.Graph.compileAuxData
            g x d0).1.backwardDenseFrom
      seed.toAnyArray =
    Except.ok
      (g.backpropAllCtx x d0
          seed).toAnyArray
    Variant of `backwardDenseFrom_compileAux_eq_backpropAllCtx` for the `GraphData` interface.

This is useful when a graph carries extra payload `Δ` (e.g. parameters/config) through forward and
backward closures.
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.

Theorem8.3.5
Group: Programs, tapes, and compiled execution. (5)
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

For a linked-session snapshot, dense reverse accumulation on the compiled tape agrees with proof-level graph backpropagation.

Lean code for Theorem8.3.5●1 theorem
  • theoremdefined in NN/Runtime/Autograd/Torch/LinkedSession/Autograd.lean
    complete
    theorem Runtime.Autograd.Torch.Internal.SessionIR.backwardDenseFrom_compileAuxData_eq_backpropAllCtx
  {α : Type} [DecidableEq Spec.Shape] [CommSemiring α]
  (st : Runtime.Autograd.Torch.Internal.SessionIRState α)
  (seed : Proofs.Autograd.Algebra.TList α (st.Γ ++ st.ss)) :
  (Proofs.Autograd.Algebra.Graph.compileAuxData st.g st.x
            st.nat).1.backwardDenseFrom
      seed.toAnyArray =
    Except.ok (st.g.backpropAllCtx st.x st.nat seed).toAnyArray
    theorem Runtime.Autograd.Torch.Internal.SessionIR.backwardDenseFrom_compileAuxData_eq_backpropAllCtx
  {α : Type} [DecidableEq Spec.Shape]
  [CommSemiring α]
  (st :
    Runtime.Autograd.Torch.Internal.SessionIRState
      α)
  (seed :
    Proofs.Autograd.Algebra.TList α
      (st.Γ ++ st.ss)) :
  (Proofs.Autograd.Algebra.Graph.compileAuxData
            st.g st.x
            st.nat).1.backwardDenseFrom
      seed.toAnyArray =
    Except.ok
      (st.g.backpropAllCtx st.x st.nat
          seed).toAnyArray
    Core proof-link: running the runtime reverse-mode loop on the compiled tape equals proved backprop.

This theorem is the "hook" that lets a session-style API be backed by the proved IR:
`compileAuxData` produces a tape, and `Tape.backwardDenseFrom` is shown equal to
`GraphData.backpropAllCtx` (up to the `TList.toAnyArray` representation change).
Proof for Theorem 8.3.5
uses 1

The linked-session hook specializes the graph-data backward theorem to the session's graph, inputs, and auxiliary index environment.

Definition8.3.6
Group: Programs, tapes, and compiled execution. (5)
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.6●1 definition
  • inductive(2 constructors, 2 parameters)defined in NN/Runtime/Autograd/TorchLean/NN/Seq.lean
    complete
    inductive Runtime.Autograd.TorchLean.NN.Seq : Spec.Shape → Spec.Shape → Type 2
    inductive Runtime.Autograd.TorchLean.NN.Seq :
  Spec.Shape → Spec.Shape → Type 2
    Sequential composition of `LayerDef`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.

    Constructors

    Runtime.Autograd.TorchLean.NN.Seq.id (s : Spec.Shape) :
  Runtime.Autograd.TorchLean.NN.Seq s s
    The empty sequence, which leaves a tensor unchanged. 
    Runtime.Autograd.TorchLean.NN.Seq.cons
  {σ τ υ : Spec.Shape} :
  Runtime.Autograd.TorchLean.NN.LayerDef σ τ →
    Runtime.Autograd.TorchLean.NN.Seq τ υ →
      Runtime.Autograd.TorchLean.NN.Seq σ υ
    Run one layer, then the remaining sequence.
Definition8.3.7
groupuses 1used by 1✓L∃∀N

After structural validation, the supported shared IR operations are lowered to a typed executable graph for forward evaluation.

Lean code for Definition8.3.7●1 definition
  • defdefined in NN/Runtime/Autograd/Compiled/IRExec/API.lean
    complete
    def Runtime.Autograd.Compiled.execGraphOfIR {α : Type} [Context α]
  [DecidableEq Spec.Shape] (g : NN.IR.Graph)
  (payload : NN.IR.Payload α) :
  Except String (Runtime.Autograd.Compiled.ExecGraphData α)
    def Runtime.Autograd.Compiled.execGraphOfIR
  {α : Type} [Context α]
  [DecidableEq Spec.Shape]
  (g : NN.IR.Graph)
  (payload : NN.IR.Payload α) :
  Except String
    (Runtime.Autograd.Compiled.ExecGraphData
      α)
    Compile an op-tagged IR graph into an executable SSA graph (`GraphData`) for forward evaluation.

Requirements:
- Node id 0 must be `.input`.
- The graph must satisfy `Graph.checkWellFormed`.
- The external payload must contain entries for every `.const`/`.linear`/`.conv2d` node id.

This returns an `ExecGraphData` whose `eval` computes all node values in topo order.

This is the main API consumed by runtime callers that want executable evaluation while remaining
aligned with the shared `NN.IR.Graph` semantics.
Theorem8.3.8
group
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.20
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Successful compilation agrees with IR denotation when the graph satisfies NoMSELoss, NoRawLog, and NoConcat.

Lean code for Theorem8.3.8●1 theorem
  • theoremdefined in NN/Runtime/Autograd/Compiled/IRExec/Correctness/SemanticEquivalence.lean
    complete
    theorem Runtime.Autograd.Compiled.execGraphOfIR_semantics_eq {α : Type}
  [Context α] [DecidableEq Spec.Shape] (g : NN.IR.Graph)
  (payload : NN.IR.Payload α)
  (exec : Runtime.Autograd.Compiled.ExecGraphData α)
  (hNoMSE : Runtime.Autograd.Compiled.NoMSELoss g)
  (hNoRawLog : Runtime.Autograd.Compiled.NoRawLog g)
  (hNoConcat : Runtime.Autograd.Compiled.NoConcat g)
  (h :
    Runtime.Autograd.Compiled.execGraphOfIR g payload = Except.ok exec)
  (x : Spec.Tensor α exec.inShape) :
  g.denoteAll payload (NN.IR.DVal.mk exec.inShape x) =
    Except.ok (exec.denoteAll x)
    theorem Runtime.Autograd.Compiled.execGraphOfIR_semantics_eq
  {α : Type} [Context α]
  [DecidableEq Spec.Shape]
  (g : NN.IR.Graph)
  (payload : NN.IR.Payload α)
  (exec :
    Runtime.Autograd.Compiled.ExecGraphData
      α)
  (hNoMSE :
    Runtime.Autograd.Compiled.NoMSELoss g)
  (hNoRawLog :
    Runtime.Autograd.Compiled.NoRawLog g)
  (hNoConcat :
    Runtime.Autograd.Compiled.NoConcat g)
  (h :
    Runtime.Autograd.Compiled.execGraphOfIR
        g payload =
      Except.ok exec)
  (x : Spec.Tensor α exec.inShape) :
  g.denoteAll payload
      (NN.IR.DVal.mk exec.inShape x) =
    Except.ok (exec.denoteAll x)
    End-to-end semantic equivalence for successful IR compilation over the named supported fragment.

If `execGraphOfIR` returns an executable graph, evaluating that executable graph on any input
matches the denotational semantics of the original IR graph, provided the graph avoids operators
whose current compiler proof needs extra side conditions.
Proof for Theorem 8.3.8
Proof uses 3
Proof dependency previews
Preview
Definition 8.1.18
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

After unfolding the IR compiler, the proof peels off the structural check and input node. The recursive lowering invariant then matches each compiled value with the corresponding denotational value.