Executable Graph Types And Lowering🔗

Torch.TypedGraph stores shape-indexed executable functions for forward evaluation, JVPs, and VJPs, together with a typed reference selecting its output. The supported canonical IR fragment lowers instead to Runtime.Autograd.IRExec.ForwardGraph, a forward-only shape-indexed form. Importing forward semantics does not supply a derivative rule, so the two executable graph types remain separate. Runtime and Autograd prints the type constructors side by side and explains what each one can therefore justify.

The principal executable paths are:

-- Follow the executable export route separately from its
-- semantic evidence.
GraphSpec.Chain ── toProgram ──> TorchLean.Program
                                             │
                                             ├── Autodiff.lowerToTypedGraph
                                             │   ──> Torch.TypedGraph
                                             │        (forward + JVP + VJP)
                                             │
                                             └── Verification.lowerForwardToIR
                                                 ──> NN.IR.Graph
                                                       │
                                                       └── IRExec.lowerToForwardGraph
                                                           ──> IRExec.ForwardGraph
                                                                (forward only)

NN.IR.Graph ── kernel selection ──> GraphKernelPlan
                                     (metadata only)

The diagram separates forward execution from execution with derivative rules. The TypedGraph branch records forward, JVP, and VJP operations; the IR branch reaches a forward-only executable. The kernel-selection branch produces metadata that must later be connected to runtime handlers.

TorchLean.Program is an operation-polymorphic function, not a stored graph. The broad lowerForwardToIR pass executes that function with an IR-building interpreter and validates the graph it produces. It does not by itself carry an end-to-end source-lowering theorem.

The theorem-backed source path is deliberately separate:

-- This proved route has its own supported program fragment.
Proved.ForwardProgram ── Proved.lowerForwardProgramToIR ──> NN.IR.Graph
          │                                                        │
   Proved.evalForward                                      runForwardIR
          │                                                        │
          └──────────────────── equal by theorem ──────────────────┘

Proved.ForwardProgram is a smaller first-order let-chain whose constructors expose the fragment covered by the theorem. It is not an alias for the general TorchLean.Program interface.

To apply a source-lowering theorem, the source must belong to the language it covers. A successful export from a general TorchLean.Program does not supply a term of Proved.ForwardProgram or a proof about that export.

MLP Graph Structure🔗

The running example is

G(x)=\tanh\!\left( \sum_k \left[W_2\operatorname{ReLU}(W_1x+b_1)+b_2\right]_k \right),

with x\in\mathbb{R}^4, a hidden width of five, and an output width of three. W_1x+b_1 produces five hidden preactivations; ReLU preserves their shape. The second affine layer produces three coordinates, the sum reduces them to a scalar, and tanh bounds that scalar. This gives us external parameters, a piecewise-linear activation, a rank-changing reduction, and a nonlinear interval rule in one small graph.

TorchLean stores it as six nodes, and the graph is ordinary Lean data, so we can just print it:

0: input parents=[] out=[4]
1: linear(payload=node_id) parents=[0] out=[5]
2: relu parents=[1] out=[5]
3: linear(payload=node_id) parents=[2] out=[3]
4: sum parents=[3] out=[]
5: tanh parents=[4] out=[]

The parent list gives data dependencies. Because every parent id is smaller than the node id, array order is already a topological execution order, so validation and evaluation can scan left to right without a graph search. linear(payload=node_id) is the pretty-printer telling you that this node's weights are not in the node; they are fetched from a payload keyed by the node id, which is the subject of a later section.

That listing renders the stored node array. Here is the source that produced it, quoted from the example file:

-- The node array gives a topological program; parameters
-- remain in a separate payload.
def graph : NN.IR.Graph :=
  let inputNode : NN.IR.Node :=
    { id := 0, parents := #[], kind := .input, outShape := input }
  let hiddenLinearNode : NN.IR.Node :=
    { id := 1, parents := #[0], kind := .linear, outShape := hiddenShape }
  let hiddenActivationNode : NN.IR.Node :=
    { id := 2, parents := #[1], kind := .relu, outShape := hiddenShape }
  let outputLinearNode : NN.IR.Node :=
    { id := 3, parents := #[2], kind := .linear, outShape := output }
  let reductionNode : NN.IR.Node :=
    { id := 4, parents := #[3], kind := .sum, outShape := [] }
  let outputNode : NN.IR.Node :=
    { id := 5, parents := #[4], kind := .tanh, outShape := [] }
  { nodes :=
      #[inputNode, hiddenLinearNode, hiddenActivationNode, outputLinearNode, reductionNode,
        outputNode] }

Unlike GraphSpec, this datatype does not make every edge shape-correct by construction. Node ids, raw axis numbers, and declared output shapes are ordinary data. That is deliberate: an importer must be able to construct a candidate graph from an external document before Lean knows it is valid. The representation therefore needs an explicit validation phase before its shape declarations can be used.

There is also a GraphViz rendering for when six nodes become sixty:

digraph IR {
  rankdir=LR;
  node [shape=box, fontsize=10];
  n0 [label="0: input\nout=[4]"];
  n1 [label="1: linear(payload=node_id)\nout=[5]"];
  n2 [label="2: relu\nout=[5]"];
  n3 [label="3: linear(payload=node_id)\nout=[3]"];
  n4 [label="4: sum\nout=[]"];
  n5 [label="5: tanh\nout=[]"];
  n0 -> n1;
  n1 -> n2;
  n2 -> n3;
  n3 -> n4;
  n4 -> n5;
}

Write that to a file and run dot -Tpng g.dot -o g.png. Edges point from producer to consumer, matching the dataflow picture the frameworks use. Neither printer is a serialization format, and Pretty.lean says so in its module docstring: the IR gains operations and invariants over time, and the pretty output should not become a compatibility obligation.

The shape [] on the last two nodes denotes a scalar, with one value. When inspecting a larger graph, follow the edges as well as the shapes: an edge that bypasses ReLU may still connect compatible shapes while changing the computation.

PyTorch Graph Capture🔗

PyTorch's op-tagged graph exposes the same computation through a different node interface. Write the network with nn.Linear, copy in the same weights, and trace it ((Reed et al., 2022)):

# Build the matching tensor computation before comparing the
# exported FX structure.
import torch, torch.nn as nn, torch.fx as fx

W1 = torch.tensor([[.15, -.12, .08, .05], [.02, .11, -.09, .07],
                   [-.04, .06, .10, -.03], [.09, .01, .04, .13],
                   [-.07, .03, .12, -.02]])
b1 = torch.tensor([.01, -.02, .03, 0., .02])
W2 = torch.tensor([[.05, .08, -.06, .03, .07],
                   [-.04, .02, .09, -.01, .06],
                   [.10, -.03, .04, .05, -.08]])
b2 = torch.tensor([.02, -.01, 0.])

class G(nn.Module):
    def __init__(self):
        super().__init__()
        self.l1 = nn.Linear(4, 5); self.l2 = nn.Linear(5, 3)
        with torch.no_grad():
            self.l1.weight.copy_(W1); self.l1.bias.copy_(b1)
            self.l2.weight.copy_(W2); self.l2.bias.copy_(b2)
    def forward(self, x):
        return torch.tanh(self.l2(torch.relu(self.l1(x))).sum())

m = G().eval()
x0 = torch.tensor([0.3, -0.2, 0.1, 0.4])
print("torch y(x0) = %.6f" % m(x0).item())
g = fx.symbolic_trace(m)
for n in g.graph.nodes:
    print("%-14s %-8s %-10s %s" % (n.name, n.op, n.target, n.args))
print("fx node has a shape field:", hasattr(list(g.graph.nodes)[0], "shape"))

The recorded run prints:

torch y(x0) = 0.027713
x              placeholder x          ()
l1             call_module l1         (x,)
relu           call_function <built-in method relu of type object ...> (l1,)
l2             call_module l2         (relu,)
sum_1          call_method sum        (l2,)
tanh           call_function <built-in method tanh of type object ...> (sum_1,)
output         output   output     (tanh,)
fx node has a shape field: False

Compare the operation names, shapes, parameter references, and output selection with the six-node listing above.

An FX node's target is a Python object: a builtin, a submodule path, a method name, or any function you happened to call. TorchLean's kind is a constructor of a single inductive type with a few dozen operations, so a pass must provide exhaustive case handling. A wildcard branch can still accept or reject many cases together, so compilation alone does not prove each operation has the intended support.

The FX node has no shape field in its core record. Shape information can be attached as metadata, for example by propagating a concrete input (other capture paths can use symbolic or fake-tensor metadata):

# Run shape propagation to see which metadata comes from
# executing example inputs.
from torch.fx.passes.shape_prop import ShapeProp
print("before:", {n.name: sorted(n.meta.keys()) for n in g.graph.nodes})
ShapeProp(g).propagate(x0)
print("after: ", {n.name: tuple(n.meta["tensor_meta"].shape)
                  for n in g.graph.nodes if "tensor_meta" in n.meta})

before: {'x': [], 'l1': ['nn_module_stack'], 'relu': [], 'l2': ['nn_module_stack'],
         'sum_1': [], 'tanh': [], 'output': []}
after:  {'x': (4,), 'l1': (5,), 'relu': (5,), 'l2': (3,), 'sum_1': (), 'tanh': (), 'output': ()}

Those are the right shapes, and they agree with TorchLean's declared ones. But they are a record of what happened on one input, obtained by executing the graph. TorchLean's shapes are a claim, made before execution, that a checker validates and a theorem ties to the semantics.

call_module l1 means "go find the submodule named l1 and call it", so the parameters are inside the traced object. TorchLean keeps the graph free of tensors and passes a payload separately, which is what makes it possible to run the same graph with interval parameters later in this chapter.

FX adds an explicit output node, so its listing has seven nodes. TorchLean names the output by id, and Graph.denote takes outputId := 5. The extra FX node selects the result; it adds no tensor calculation.

The PyTorch output at x0 is 0.027713. We will compare it with the IR evaluator after supplying the parameter payload.

The Node Record🔗

The node record stores the information that validation and evaluation will use:

/-- Node in the graph. Edges are implicit via parent indices. -/
structure Node where
  /-- Node id. By convention this is also the node's index in `Graph.nodes`. -/
  id       : Nat
  /-- Parent node ids, i.e. data dependencies. Each parent must be smaller than `id`. -/
  parents  : Array Nat
  /-- Operation tag and any operation-local metadata. -/
  kind     : OpKind
  /-- Declared output shape. `NN.IR.Infer` can recompute/check this from parents. -/
  outShape : Shape
  deriving Repr

kind carries operation-local data such as an axis, a permutation, convolution geometry, or a hard mask. Large tensor values do not belong there; constants and learned parameters live in the payload. To evaluate this record safely, id must agree with the array position, every parent must already exist, the parent count must suit the operation, and outShape must agree with independent inference. These are checks on the record as a whole; the operation tag alone does not establish them.

This separation of operation data from validation also appears in MLIR ((Lattner et al., 2021)); ONNX similarly stores initializers separately from operations. Here we can inspect both the checks and the Lean theorems connecting them to the graph semantics.

Structural And Shape Validation🔗

Validation separates graph structure from operation-specific shape consistency.

Graph.checkWellFormed checks structure only: node id equals array position, parents occur earlier in topological order, the operation has an admissible number of parents, and designated input and constant nodes have the required arity. Graph.checkShapes then runs the operation-specific shape rules from Infer.lean. Our graph passes both:

Except.ok ()

Except.ok ()

Now break it three ways, one field at a time. First, declare the wrong output shape on the ReLU node, leaving the structure untouched:

Except.ok ()

Except.error "IR graph: node 2: outShape mismatch: inferred=[5], declared=[4] (Node(id=2, kind=relu, parents=#[1], outShape=[4]))"

The parent edge still points to an earlier node, so the structural check succeeds. ReLU must preserve its parent's shape, however, and [4] disagrees with the parent's [5]. The shape checker reports that mismatch. The evaluator performs additional checks and can also reject it before downstream use; a successful structural check alone does not establish shape consistency.

Second, break the topological order by pointing node 2 at node 3:

Except.error "IR graph: node 2: parent id 3 is not < 2 (Node(id=2, kind=relu, parents=#[3], outShape=[5]))"

Third, break the id discipline, which is the invariant that lets ids double as array indices:

Except.error "IR graph: id discipline violated at index 2: nodes[2].id = 7"

Each failed check returns an Except.error that identifies the inconsistent field. Every failure is a value in Except String, because the caller that reads an untrusted file is supposed to be able to report the problem rather than crash.

Each diagnostic points to a different repair. Changing a tensor dimension will not repair the forward reference, and renumbering a node will not establish that ReLU has the declared output shape.

@Graph.checkShapes_sound : ∀ {α : Type} [inst : Storage α] [inst_1 : Context α] (g : Graph) (payload : Payload α)
  (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)),
  g.checkShapes = Except.ok () →
    g.denoteAll payload input = Except.ok vals →
      ∀ (i : ℕ) (hi : i < g.nodes.size) (hiv : i < vals.size), vals[i].shape = g.nodes[i].outShape

#[[4], [5], [5], [3], [], []]

Except.ok #[[4], [5], [5], [3], [], []]

Parameter Payloads🔗

The two .linear nodes mention only their activation parent. Their weights and biases come from a payload keyed by node id, and this is the real definition from the example:

-- Resolve the two linear nodes to parameter tensors with
-- their own checked dimensions.
def payload {α : Type} [TorchLean.Storage α] [Context α]
    (parameters : Parameters α) : NN.IR.Payload α :=
  { linear? := fun id =>
      if id = 1 then
        some {
          outDim := hiddenWidth
          inDim := inputWidth
          W := parameters.hiddenWeight
          b := parameters.hiddenBias
        }
      else if id = 3 then
        some {
          outDim := outputWidth
          inDim := hiddenWidth
          W := parameters.outputWeight
          b := parameters.outputBias
        }
      else
        none }

The scalar type parameter and the Storage and Context instances determine the payload's tensor values. The node ids stay fixed when we change this scalar interpretation, so the same graph can later read interval parameters.

Separating structure from values has practical consequences:

• one graph can be reused with initial, trained, or bounded parameters;

• checkpoint loading changes the payload without rebuilding the node array;

• a verifier can replace concrete parameters by interval metadata;

• an exporter can emit graph nodes and initializers through different channels.

It also creates an obligation that no type will discharge for you. The payload's LinearWB record carries its own outDim and inDim, and its W : Tensor α [outDim, inDim] is shape-correct with respect to those fields, not with respect to the node. So a payload can be internally consistent and still disagree with the graph. Keying by node id makes that failure possible; here it is:

Except.error "IR eval: linear 1: declared outShape mismatch: [5] vs expected [3]"

The lookup at key 1 succeeds, but its three-output matrix disagrees with node 1's declared five-output shape. Evaluation reports both dimensions and names the node.

The shared NN.IR.Payload currently has typed records for constants, linear weights and bias, convolution parameters, layer-normalization parameters, and eval-mode channel-axis BatchNorm parameters. Other operations obtain their values from parent edges. Adding a new payload-backed operation requires coordinated changes to the payload type, shape inference, denotation, import/export adapters, and every runtime or verifier that claims to support it, which is a good reason to prefer an operation that reads its inputs from edges when either would do.

Equal dimensions would still not prove that the correct checkpoint tensor had been assigned to a node. The GraphSpec bias-swap example passed that check while changing the output.

A Heterogeneous Value Table🔗

During evaluation, node 0 holds a vector of four, nodes 1 and 2 hold five, node 3 holds three, and nodes 4 and 5 hold scalars. One homogeneous Lean array cannot directly contain all those tensor types, so the evaluator stores the specification layer's shape-erased tensor:

-- The existential package retains a tensor together with
-- the shape indexing its type.
structure Spec.SomeTensor (α : Type) where
  shape : Shape
  tensor : TorchLean.Tensor α shape

This is a dependent pair of a runtime shape and a tensor with exactly that shape. Graph.expectShape recovers a statically typed tensor only after checking the stored shape, and Runtime and Autograd shows the cast that demands a proof and the round-trip theorem saying nothing was lost. Model code never builds this table; its inputs stay Tensor α shape.

For node 1, evaluation performs:

1. fetch parent 0 from the value table;

2. fetch the linear payload keyed by 1;

3. check the parent tag equals [4];

4. check the declared output equals [5];

5. call the pure linearSpec;

6. store the result as a Spec.SomeTensor α.

Step 4 is the one that produced the error message in the previous section. Failures are reported as Except String; malformed imported data does not receive a fabricated proof cast.

We can read every intermediate value from this table to locate where two evaluations diverge:

Except.ok #["[0.300000, -0.200000, 0.100000, 0.400000]", "[0.107000, -0.017000, 0.004000, 0.081000, -0.003000]",
  "[0.107000, 0.000000, 0.004000, 0.081000, 0.000000]", "[0.027540, -0.014730, 0.014910]", "0.027720", "0.027713"]

Node 1 is the affine layer, node 2 is the same vector with its two negative entries clamped to zero, node 3 is the second affine layer, node 4 sums the three components to 0.027720, and node 5 applies tanh to get 0.027713. The tanh barely moves the value because tanh x ≈ x near zero. This gives us a reference for the interval calculation: the reduction and final output at the center are both close to 0.028.

Scalar Interpretations🔗

Graph.denote folds over the node array using the spec operations and a scalar Context α. Nothing in NN.IR.Graph mentions α at all, which is why one piece of graph data can be read at:

• α := ℝ, for exact-real theorem statements;

• α := FP32, for finite rounded-real analysis;

• α := ExecFloat.Binary 8 23, for executable binary32 behavior;

• another valid FloatLib binary format, for typed CPU execution at a different precision;

• α := Float, for the ordinary runtime scalar;

• interval endpoints over any of those, for bound propagation.

The graph is the same data and the meaning of arithmetic changes with α. This is the same tagless-final move the runtime uses for its two Ops instances (Kiselyov (2012)), except that here the interpreter is a fold over stored data rather than an instance chosen by unification.

We can compare two executable choices directly:

Except.ok "0.027713"

Except.ok "0.027713"

The displayed evaluations agree to six decimals: Lean's hardware Float, FloatLib's software binary32, and the recorded PyTorch run. The explicit conversion after evaluation selects the same decimal display; the graph itself still computes in binary32. The first uses the machine's double-precision arithmetic, the second simulates binary32 with explicit rounding ((Goldberg, 1991)), and the third calls into LibTorch. The shared printed output does not tell us whether their stored values agree. Floating-Point Semantics follows individual rounding steps to explain how such differences arise.

The other two instantiations are noncomputable, which is a fact about their scalars and not about the graph:

propagateRealBounds : Graph.ParamStore ℝ → Array (Option (FlatBox ℝ))

propagateFP32Bounds : Graph.ParamStore Floats.FP32 → Array (Option (FlatBox Floats.FP32))

These functions use the same graph and propagation algorithm to construct boxes for mathematical reasoning. ℝ is Mathlib's real numbers ((Community, 2020)); FP32 models binary32 precision and gradual underflow using rounded real values, without an upper exponent cutoff. Flocq provides a related formal account of floating-point rounding ((Boldo and Melquiond, 2011)). Relating different scalar interpretations requires explicit hypotheses; The Specification Layer explains those relationships.

The Option entries in the return types allow a node to lack a derived bound. Even when the graph evaluates successfully, propagation may leave part of the enclosure trace unavailable.

Interval Bound Propagation🔗

Bound propagation replaces each value by an interval and each operation by an operation on intervals, then reads the output interval. This is interval bound propagation, the simplest member of the family that CROWN and its descendants refine ((Gowal et al., 2018); (Zhang et al., 2018)). It runs on our graph unchanged: the node array does not know it is being interpreted over boxes.

Take the center input x_0=(0.3,-0.2,0.1,0.4) and an \ell_\infty ball of radius 0.05 around it, then print the box at every node:

node 0: [0.250000, -0.250000, 0.050000, 0.350000] .. [0.350000, -0.150000, 0.150000, 0.450000]
node 1: [0.087000, -0.031500, -0.007500, 0.067500, -0.015000] .. [0.127000, -0.002500, 0.015500, 0.094500, 0.009000]
node 2: [0.087000, 0.000000, 0.000000, 0.067500, 0.000000] .. [0.127000, 0.000000, 0.015500, 0.094500, 0.009000]
node 3: [0.025445, -0.016025, 0.011355] .. [0.029815, -0.012220, 0.018045]
node 4: [0.020775] .. [0.035640]
node 5: [-1.000000] .. [1.000000]

Node 0 is the input box, the center plus and minus 0.05 in each coordinate. Node 1 applies the affine interval rule to that box and records one lower and upper bound per output coordinate. These bounds include endpoint rounding; the printed decimals do not assert an exact image of the box. Compare node 2 with node 1: every negative lower bound has become exactly 0.000000, and the upper bounds are unchanged except where they were negative too. That is interval ReLU, and zero-based coordinate 1 of node 2 is the degenerate interval [0, 0] because the whole input interval for that coordinate was negative. Node 3 is the second affine layer, node 4 sums the three coordinates, and the resulting scalar interval is [0.020775, 0.035640], which does contain the value 0.027720 we computed at the center.

Node 5 widens the result to [-1, 1], a global enclosure of the range of tanh. To explain that loss of information, we need to inspect the interval rule selected for this scalar type.

An interval at a node encloses the values allowed by the input box and the transfer rules used so far. It can lose correlations between two parents that depend on the same input. For example, separately enclosing a value and its negation does not retain the fact that their sum is exactly zero. This loss of dependence can widen later intervals even with exact endpoint arithmetic. Rounded endpoints introduce another issue: they must move outward to preserve enclosure. A wide interval can therefore reflect the abstraction, the rounding policy, or a deliberately coarse nonlinear rule, and those causes call for different improvements.

some (-1.000000, 1.000000)

(0.020772, 0.035625)

Sampled Containment And Enclosure Theorems🔗

The whole experiment is one command:

# Check sampled executions against the intervals derived for
# this example.
lake exe torchlean one_semantic_universe --samples 50

The following transcript predates the FloatLib migration and retains its recorded scalar labels and numerical results. Current .ieee execution uses FloatLib binary32.

== One semantic universe tutorial ==
graph nodes = 6
[eval IEEE32Exec] y(x0) = 0.027713
[IBP IEEE endpoints] lo = -1.000000
[IBP IEEE endpoints] hi = 1.000000
consistency: 50/50 samples satisfied evalIEEE(x) ∈ IBP(B)
checker theorem: `NN.MLTheory.CROWN.Box.containsDecBool_sound`

The transcript reports an evaluation, an interval, a sampled comparison, and a checker theorem:

1. The graph evaluator produced one binary32 result at the center input.

2. Interval propagation produced one output interval for the input box.

3. Fifty sampled evaluations landed inside that interval.

4. A named theorem says the Boolean containment check means what it appears to mean.

For statement 3, all fifty samples fall in [-1, 1], a global enclosure for ideal real tanh. This supplies little information about tightness, since the interval rule discarded the input range. The comparison can still expose NaNs, broken dispatch, or an invalid range result, making it useful as a regression check.

Statement 4 refers to this pointwise theorem:

@Box.containsDecBool_sound : ∀ {α : Type} [inst : Storage α] [inst_1 : Context α]
  [inst_2 : DecidableRel fun x1 x2 => x1 ≤ x2] {s : Shape} (b : Box α s) (x : Tensor α s),
  b.containsDecBool x = true → b.contains x

It upgrades a Boolean to a proposition about the point that was checked. It says nothing about the other points in the box, and it is not the enclosure theorem.

The enclosure theorem quantifies over graph evaluations under explicit coverage and input assumptions:

runIBP_encloses_evalGraphRec : ∀ (g : NN.MLTheory.CROWN.Graph) (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs : Std.HashMap ℕ Val),
  TopoSorted g →
    EngineCore g →
      IBPCovers g (runIBP? g ps) →
        InputsEnclosed g ps inputs →
          ∀ id < g.nodes.size,
            ∀ (B : NN.MLTheory.CROWN.FlatBox ℝ) (v : Val),
              (g.runIBP ps)[id]! = some B → (evalGraphRec g ps inputs)[id]! = some v → EnclosesBox B v

The theorem assumes that the graph is topologically sorted, its operations belong to EngineCore, the proof-side pass covers every node, and the input boxes enclose the inputs. Under those assumptions, a box returned by the engine encloses a value returned by the evaluator at the same node. It does not by itself establish successful evaluation at every node.

The operation restriction matters for our example. EngineCore admits inputs, constants, detach, addition, subtraction, elementwise multiplication, ReLU, linear layers, matrix multiplication, softplus, and safe log. It excludes both sum and tanh, which occur at nodes 4 and 5. Consequently this theorem does not cover the six-node graph as written, even after changing its scalar type to ℝ. Extending the enclosure proof to those operations is a separate requirement from changing the scalar semantics.

The scalar in the theorem is ParamStore ℝ, whereas the run above used FloatLib binary32. Relating that rounded propagation to real arithmetic requires another argument, developed in Verification And Certificates and Floating-Point Soundness. Applying the enclosure theorem to an execution requires both its graph, coverage, and input hypotheses and this connection between scalar semantics.

IBPCovers requires a box for every node in the proof-side pass. InputsEnclosed supplies the initial enclosure from which the propagation proof starts. The sampled checker only compares an already supplied point and box; it performs neither this induction nor a check of universal input hypotheses.

Executable Coverage And Proof Coverage🔗

Runtime.Autograd.IRExec.lowerToForwardGraph validates the graph and lowers the current IR vocabulary operation by operation: elementwise arithmetic, seeded masks, broadcasting, reductions, matrix multiplication and linear layers with any shared leading shape (so batched and rank-four products are covered), convolution payloads, pooling, normalization, reshape and permutation, concatenation along any axis, and scalar MSE. Lowering rejects a shape or axis that the IR semantics itself rejects; it does not panic and it does not guess.

On our graph it succeeds, and the result records the input shape and one shape per lowered node:

Except.ok ([4], [[5], [5], [3], [], []])

[4] is the input shape; the five entries in exec.ss are the shapes of nodes 1 through 5. Together they retain the original node order in a typed SSA context, where later operations select previously computed values with known shapes.

The semantic-equivalence theorem covers every operation the lowering accepts, with one named side condition:

@denoteAll_eq_of_lowerToForwardGraph : ∀ {α : Type} [inst : Storage α] [inst_1 : Context α] (g : Graph)
  (payload : Payload α) (exec : ForwardGraph α),
  NoRawLog g →
    lowerToForwardGraph g payload = Except.ok exec →
      ∀ (x : Tensor α exec.inShape),
        g.denoteAll payload { shape := exec.inShape, tensor := x } = Except.ok (exec.denoteAll x)

NoRawLog g excludes raw-log nodes from the graph altogether. It is not a positivity predicate on a particular input. The IR evaluator rejects nonpositive raw-log inputs while the lowered closure uses a total specification logarithm; this theorem avoids that difference by excluding the operation. A theorem admitting raw log on positive intermediates would need a different hypothesis.

For a concrete graph the condition is decidable, and discharging it is one line:

decide checks the concrete node array for raw-log operations. The resulting proof discharges NoRawLog graph, allowing the equivalence theorem to apply to every input whenever lowering succeeds. Per-operation lemmas live under NN.Runtime.Autograd.IRExec.Correctness.Ops, and Common.lean carries noRawLog_of_forall_mem precisely so that every caller does not redo the same case analysis inline.

For this graph, the successful lowering supplies a typed executable, and irNoRawLog supplies the side condition needed to identify its full value table with IR denotation on every input. Keeping the condition attached to the executable follows the proof-carrying-code principle: the consumer needs evidence about the particular code it receives (Necula (1997)).

The proof-bearing source lowering under NN.Verification.Builtin.Proved relates its first-order source evaluator to IR denotation, and its theorem is likewise not a wildcard over every TorchLean.Program or every OpKind the broad executable lowering accepts.

Axis Operations And Lowering Coverage🔗

An axis is stored as data, but changing it changes which coordinates an operation combines. The following example uses an interior axis so the shape rules must account for dimensions on both sides:

# Exercise nontrivial axes so a last-axis-only
# implementation cannot pass unnoticed.
lake exe torchlean ir_axis_ops

== IR axis ops tutorial ==
The runtime validates each graph and evaluates its selected output.

-- softmax axis=1 on shape [2,3,4]
[softmax_middle_axis] output shape: [2, 3, 4]

-- layernorm axis=1 on shape [2,3,4]
PyTorch meaning: normalized_shape = x.shape[axis:] = [3,4]
[layernorm_middle_axis] output shape: [2, 3, 4]

-- concat axis=1: [2,3,4] ++ [2,5,4] -> [2,8,4]
[concat_middle_axis] output shape: [2, 8, 4]

The full transcript also prints the leading scalars. The example calls Runtime.Autograd.IRExec.evaluate, which checks the graph and input shapes, lowers the graph, and returns the selected output. The tutorial supplies the graphs and prints the results; validation and execution live in the runtime library.

The selected dimension is part of the operation, so axis zero, an interior axis, and the final axis all retain their usual tensor meaning. LayerNorm folds the dimensions before the axis into rows and the dimensions from the axis onward into the normalized extent, which is PyTorch's normalized_shape = x.shape[axis:]. Unsupported lowering and invalid shapes return errors. Execution alone does not establish equivalence with the specification; that is the role of the semantic preservation theorem and its hypotheses.

Change concat axis=1 to an out-of-range axis in IRAxisOps.lean and shape inference rejects the node before evaluation, with the same kind of error message the broken graphs produced earlier.

On [2,3,4], softmax along axis one normalizes three entries while holding the first and last coordinates fixed. LayerNorm starting at that axis combines twelve entries into each row's statistics. Concatenation instead changes one extent and retains the others. These examples exercise choices that a last-axis-only test would miss.

The axis and shape attributes are part of an operation's meaning, even when they do not alter the final tensor shape. For example, two different normalization axes of a square matrix can both return that matrix's shape while producing different values. Shape soundness therefore cannot establish the axis choice by itself. The semantic preservation result must read the same attribute as the source operation and identify the resulting values.

Kernel Planning🔗

The backend adapter maps each operation tag to a backend operation, chooses an admissible kernel capsule for every runtime-relevant node, and preserves node identity so the plan can be audited against the graph. On our graph, with the default CPU policy and the maintained capsule modules:

Except.ok (#[1, 2, 3, 4, 5],
 #["reference.linear", "reference.relu", "reference.linear", "reference.reduce_sum", "reference.tanh"])

Five capsules for six nodes. Node 0 is absent because .input needs no runtime work: op? maps it to none, as it does for .const and .detach. Notice also that the .sum tag was planned as reference.reduce_sum, because the backend vocabulary has one reduction operation where the IR has both a full sum and an axis reduction.

A KernelCapsule describes the selected contract. It contains no executable closure, so planning node 1 for nativeCuda does not call a CUDA kernel. Eager execution must bind the selected capsule to a typed handler with the same operation, provider, and device before that handler can run, and the current typed graph trainer does not consume a plan at all. Backend Selection follows the selection and assurance model in detail.

The distinction prevents a common architecture mistake:

-- Each stage below answers a different question about
-- backend support.
registered     ≠ selectable
selectable     ≠ executable
executable     ≠ proved correct

Moving between these states requires availability checks, runtime dispatch, and evidence for the selected implementation. The capsule's numerical policy also determines whether an arithmetic bound for a particular reduction order applies to the proposed kernel.

Canonical IR And Autograd Tapes🔗

The canonical IR records a persistent model computation. An eager autograd tape records one execution, and carries what an execution has:

• concrete runtime tensor handles;

• which values require gradients;

• saved forward values needed by VJPs;

• the actual order in which wrappers ran.

The tape may contain enough information to reconstruct an IR-like graph, but it is not NN.IR.Graph. Conversely, the canonical IR does not own mutable gradient buffers or optimizer state. Runtime and Autograd builds a tape by hand and shows exactly what those four bullet points look like as data.

This difference is also why LibTorch forward can participate in a TorchLean-owned backward path: the TorchLean wrapper records a local tape node even when an external provider computes the forward value. The canonical semantic graph and the execution tape remain distinct objects connected by the operation contract.

A forward value table is also insufficient to reconstruct a proved reverse pass on its own. A reverse computation needs the selected VJP for every operation, the saved inputs that rule reads, and a consistent accumulation of cotangents at shared parents. Two tapes may agree on every forward value while disagreeing on one of those backward choices. The forward lowering theorem is valuable because it fixes the denotation being differentiated; the autograd link must additionally connect the reverse rules to derivatives of that denotation.

Graph Results And Validation Evidence🔗

For any graph-based claim, locate:

1. the exact graph representation;

2. its concrete parameter payload;

3. the structural and shape checks that ran;

4. the scalar context used by denotation;

5. the lowering theorem and fragment, if lowering was used;

6. the capsule selected for each native operation;

7. the provider branch that actually executed it.

These records distinguish a shape-checking failure from a payload mismatch, a lowering restriction, or an unavailable runtime provider.

The source map is:

• Graph.lean for nodes and operation tags;

• Infer.lean and Check.lean for shape inference and the two validation levels;

• Semantics.lean for pure denotation;

• ShapeSoundness.lean for the proof that validation and denotation agree on shapes;

• Pretty.lean for the listing and the GraphViz output;

• Backend/IR.lean for capsule planning;

• IRExec for the forward lowering and its correctness proofs;

• OneSemanticUniverse.lean for the complete six-node experiment.

Variations On The Six-Node Graph🔗

Changing one field at a time isolates the checks and interpretations used above.

1. Add a seventh node, .relu on node 5, and predict which of the two checkers complains before running either. Then give it output shape [3] and predict again.

2. Swap the two .linear payload keys so node 1 gets node 3's weights. Predict which of the six evaluation steps fails and with which message.

3. Change the input box radius from 0.05 to 0.5 and look at node 2. At what radius does the interval for zero-based coordinate 1 stop being [0, 0]?

4. Replace the final .tanh with .sigmoid and rerun the interval block. Explain the output box from the instance definitions rather than from the numbers.

5. Replace it with .abs instead, which has a real interval rule at FloatLib binary32, and see the output interval become informative again.

6. Add a .log node and try to reprove irNoRawLog with by decide. The failure is the side condition doing its job.

7. Plan the graph with a policy asking for a provider this build does not have, and read the error. It comes from the backend boundary, not from the graph.

Graph Verification Requirements🔗

The six-node example separates two remaining verification tasks. The interval rule must preserve enclosure under the chosen scalar semantics, and the resulting interval must be tight enough for the property being checked. The global tanh range demonstrated why these are separate: every sample passed containment while the final rule discarded the narrow interval from node 4.

Verification And Certificates develops the enclosure arguments and their graph hypotheses. Floating-Point Soundness studies how rounding affects those arguments. Applying them to a particular execution requires checking both its operations and its scalar backend against the hypotheses of the theorem being used.