Forward IR Execution

This module validates an op-tagged NN.IR.Graph and translates its nodes into the shape-indexed ForwardData representation used for evaluation. ForwardGraph packages that result with its input and intermediate shapes.

The translation is forward-only. It neither supplies derivative rules nor performs optimization, fusion, scheduling, or native code generation. The semantic-equivalence theorem for the supported IR fragment lives in NN.Runtime.Autograd.IRExec.Correctness.SemanticEquivalence so ordinary runtime imports do not pull in that proof.

Main declarations

• ForwardGraph packages a forward-only graph lowered from NN.IR.Graph.
• Internal.packedTensorsOfContext converts typed runtime contexts back into IR-style value arrays.
• Internal.buildFrom is the lowering pass from NN.IR.Graph to executable graph data.
• lowerToForwardGraph is the public lowering entry point.

Numeric IR node identifiers are converted through checked typed indices (Idx). The resulting types contain no derivative operations: lowering to ForwardGraph cannot be mistaken for an autograd lowering.

@[simp]

theorem Runtime.Autograd.IRExec.Except.ok_bind {ε α β : Type} (a : α) (f : α → Except ε β) : Except.ok a >>= f = f a

simp rule for Except-do chains: binding an .ok value is just function application.

@[simp]

theorem Runtime.Autograd.IRExec.Except.error_bind {ε α β : Type} (e : ε) (f : α → Except ε β) : Except.error e >>= f = Except.error e

simp rule for Except-do chains: binding an .error short-circuits.

Used heavily when discharging impossible branches in lowering correctness proofs.

structure Runtime.Autograd.IRExec.ForwardNode (α : Type) [TorchLean.Storage α] (Γ : List Spec.Shape) (τ : Spec.Shape) : Type

One forward-only SSA node over the typed context Γ.

• eval : TorchLean.TensorPack α Γ → TorchLean.Tensor α τ

  Evaluate the node from the graph input and all preceding node values.

inductive Runtime.Autograd.IRExec.ForwardData (α : Type) [TorchLean.Storage α] (Γ : List Spec.Shape) : List Spec.Shape → Type

A shape-indexed forward SSA graph.

Unlike autograd GraphData, this representation has no JVP or VJP fields. It is therefore impossible to request derivatives from an artifact produced by the forward IR lowering pass.

• nil {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} : ForwardData α Γ []

  A graph with no computed nodes.

• snoc {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} {τ : Spec.Shape} : ForwardData α Γ ss → ForwardNode α (Γ ++ ss) τ → ForwardData α Γ (ss ++ [τ])

  Append a node that may read the graph input and every preceding result.

def Runtime.Autograd.IRExec.ForwardData.eval {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : ForwardData α Γ ss) (x : TorchLean.TensorPack α Γ) : TorchLean.TensorPack α (Γ ++ ss)

Evaluate every node and return the input followed by all intermediate values.

structure Runtime.Autograd.IRExec.ForwardGraph (α : Type) [TorchLean.Storage α] : Type

A forward-executable SSA graph derived from an NN.IR.Graph.

The lowered graph stores:

• one distinguished input shape (inShape),
• one shape per lowered node (ss, corresponding to IR node ids 1..n-1),
• and forward-only node closures (body) consumed by ForwardData.eval.

• inShape : Spec.Shape

  The distinguished IR input node’s shape (node id 0).

• ss : List Spec.Shape

  Shapes of the IR nodes 1..(n-1) (one per executable SSA node).

• body : ForwardData α [self.inShape] self.ss

  Forward SSA/DAG for nodes 1..(n-1); inputs live in Γ := [inShape].

def Runtime.Autograd.IRExec.ForwardGraph.eval {α : Type} [TorchLean.Storage α] (e : ForwardGraph α) (x : TorchLean.Tensor α e.inShape) : TorchLean.TensorPack α ([e.inShape] ++ e.ss)

Evaluate the lowered forward graph on a concrete input tensor.

The result is the full typed runtime context [inShape] ++ ss, i.e. input followed by every lowered node value in topological order.

Denotation Table Helper

ForwardGraph.eval produces a typed runtime context TorchLean.TensorPack α ([inShape] ++ ss).

For debugging and for the forward-correctness development in NN.Runtime.Autograd.IRExec.Correctness, we provide a helper that erases this context into an IR-style value table Array (Spec.SomeTensor α) in node-id order.

def Runtime.Autograd.IRExec.Internal.packedTensorsOfContext {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} (ctx : TorchLean.TensorPack α ss) : Array (Spec.SomeTensor α)

Convert a typed runtime context TorchLean.TensorPack α ss into an IR-style value table.

This is phrased in terms of Array (Spec.SomeTensor α) because the IR denotation functions (denoteAll*) are array-based, while forward-graph execution evaluates into a typed context (TorchLean.TensorPack).

def Runtime.Autograd.IRExec.ForwardGraph.denoteAll {α : Type} [TorchLean.Storage α] (e : ForwardGraph α) (x : TorchLean.Tensor α e.inShape) : Array (Spec.SomeTensor α)

Convert the full evaluated context into an IR-style value table (one Spec.SomeTensor per node id).

This is the bridge used to compare forward-graph evaluation with NN.IR.Graph.denoteAll*.