IR To Executable Graph Lowering

Public entrypoint for validating and lowering a complete shared IR graph.

def Runtime.Autograd.IRExec.lowerToForwardGraph {α : Type} [TorchLean.Storage α] [Context α] (g : NN.IR.Graph) (payload : NN.IR.Payload α) : Except String (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.

def Runtime.Autograd.IRExec.evaluate {α : Type} [TorchLean.Storage α] [Context α] {σ : Spec.Shape} (g : NN.IR.Graph) (payload : NN.IR.Payload α) (x : TorchLean.Tensor α σ) (outputId : Fin g.nodes.size) : Except String (Spec.SomeTensor α)

Validate an IR graph and evaluate its selected output on a shape-checked input.

Structural, declared-shape, payload, and lowering errors are returned to the caller. The input shape is checked against node zero before execution. This evaluates the forward graph; it does not compare floating-point results with a second semantics or assert numerical equivalence.