4.3.1. Why GraphSpec Exists🔗

A raw IR graph is excellent for a verifier, but it is not the right authoring surface for every architecture. A public nn.Sequential model is direct enough for tutorials, but it does not always expose the architecture-level facts we want to reason about: ordered parameter shapes, reused intermediates, residual branches, and paired pure/executable interpretations.

GraphSpec exists for that middle layer.

Read the layers this way:

• nn.Sequential: beginner model code and training tutorials.

• GraphSpec sequential Graph ps σ τ: typed architectures with an explicit parameter list.

• GraphSpec DAG models: residual branches, sharing, and multiple inputs.

• NN.IR.Graph: verification, export, widgets, and bound propagation.

4.3.2. What GraphSpec Adds🔗

The graph taxonomy belongs in Graphs and IR. The additional point here is more specific: GraphSpec gives architectures a typed authoring language before they are lowered into a runtime program or the shared op-level IR.

That authoring layer adds three things that a raw IR graph does not try to provide:

• a parameter ABI in the type, so the order and shapes of trainable tensors are part of the model interface;

• architecture-level sharing, so residual branches and reused intermediates can be written directly;

• paired interpreters, so the same architecture object has a pure Spec meaning and an executable TorchLean program.

In short: GraphSpec records architecture facts before the model becomes a runtime or verifier artifact.

4.3.3. Two Authoring Surfaces🔗

GraphSpec exposes two related surfaces because a linear chain and a general DAG with sharing are different authoring problems.

Graph ps σ τ

[Mat outDim inDim, Vec outDim]

4.3.4. Parameter ABI🔗

GraphSpec treats parameter layout as part of the architecture. Parameter shapes and ordering live in the type.

By parameter ABI, we mean the ordered list of parameter tensor shapes that every interpreter, compiler, importer, or checker agrees to use. In:

Graph ps σ τ

the model maps input shape σ to output shape τ and expects parameters with shapes ps, in that order. This ordered list is the model's parameter ABI.

That gives the architecture layer two practical benefits:

• parameter ABI is explicit and stable enough to reason about, and

• the same model can be interpreted, lowered, and checked against a single declared parameter order.

Many downstream artifacts assume an exact parameter order, so GraphSpec makes that order part of the model interface instead of leaving it implicit in helper code.

4.3.5. Choosing The Right Surface🔗

Use the smallest surface that still says what you need to say.

• Use nn.Sequential for ordinary tutorials and model training files.

• Use sequential GraphSpec when the model is still a chain, but the parameter ABI and pure semantics should be explicit.

• Use GraphSpec DAG models when the architecture has sharing, residual branches, or multiple inputs.

• Use NN.IR.Graph when the consumer is a verifier, exporter, or graph level analysis pass.

Each layer stays explicit: architecture authoring stays readable, while verifier-facing code still receives a precise op-level graph after lowering.

4.3.6. Two Semantics From One Model🔗

GraphSpec is valuable because it does not force an early choice between a clean mathematical object and an executable object.

For sequential graphs, the main names are:

• NN.GraphSpec.Interp.spec

• NN.GraphSpec.Compile.torchProgram

For DAG models, the corresponding names are:

• NN.GraphSpec.Model.specFwd

• NN.GraphSpec.Model.torchProgram

The pattern is the same in both cases:

• the Spec semantics supplies a pure forward meaning in Lean,

• the TorchLean compiler supplies an executable program in the runtime layer.

GraphSpec packages this semantic alignment at the architecture-authoring level.

The declarations worth recognizing in the infoview are:

#check NN.GraphSpec.Interp.spec
#check NN.GraphSpec.Compile.torchProgram
#check NN.GraphSpec.DAG.Model.specFwd
#check NN.GraphSpec.DAG.Model.torchProgram
#check NN.GraphSpec.Model.specFwd
#check NN.GraphSpec.Model.torchProgram
#check NN.GraphSpec.ToTorchLean.toSeq

4.3.7. Worked Micro-Example🔗

The smallest useful GraphSpec check sequence is the one from the README:

import NN.Entrypoint.GraphSpec

open NN
open NN.GraphSpec
open Spec

def g (inDim hidDim outDim : Nat) :=
  GraphSpec.Models.mlp inDim hidDim outDim

-- Pure semantics: parameters to input to output.
#check GraphSpec.Interp.spec (g 4 8 2)

-- Executable TorchLean program.
#check GraphSpec.Compile.torchProgram (g 4 8 2)

-- Optional lowering into the general DAG model representation.
#check GraphSpec.LowerToDAG.Graph.toDAGModelZeroInit (g 4 8 2)

The important lesson is not just that these names exist. The lesson is that one architecture can be read at three levels:

• as typed authoring syntax,

• as pure semantics,

• and as executable runtime code.

4.3.8. Residual Sharing As A Tiny DAG🔗

A residual block is the first example where the DAG surface is more natural than a chain. The architecture says:

y = f(x)
z = y + x

The value x is used twice. In a purely sequential chain, that sharing is awkward because the input would have to be carried forward as an explicit side value. In a DAG model, the intermediate names are part of the authoring language.

This is the reason examples such as Models.residualLinear and Models.ResNet18.model use the DAG surface: their architecture contains skip connections, so shared values should be represented directly.

4.3.9. Lowering Paths🔗

GraphSpec supports several lowering paths. They are not competing APIs; they answer different questions about the same architecture.

The names below are not meant to be memorized. They are the bridges to look for when debugging how a GraphSpec model becomes a runnable TorchLean program or a verifier-facing DAG.

4.3.10. Model Zoo Landmarks🔗

For model definitions used in examples and examples, NN.GraphSpec.Models is the most convenient single import surface.

The current zoo includes both sequential and DAG-native models:

• Models.mlp for the smallest sequential path,

• Models.cnn2 and cnn2DAGModelZeroInit for "same model, different representation" comparisons,

• Models.residualLinear for a small residual/shared example,

• Models.ResNet18.model for a substantial DAG-authored architecture.

The GraphSpec README suggests this order:

1. Models.mlp

2. Models.cnn2

3. Models.residualLinear

4. Models.ResNet18.model

4.3.11. Reading Rule🔗

When reading a GraphSpec model, look for four things:

1. the input and output shapes;

2. the parameter-shape list;

3. whether the model is sequential or DAG-native;

4. which lowering or theorem cites it.

That is the information GraphSpec contributes beyond the public tutorial syntax. It is not another training API; it is the architecture layer that preserves parameter ABI and sharing before runtime or verification lowering.

4.3.12. Proof Alignment Checks🔗

GraphSpec also has a small but important proof side. The declarations below are compact alignment statements: they connect GraphSpec syntax to reference specs, deterministic parameter initialization, and the embedding of sequential primitives into DAG primitives.

The entrypoint NN.Entrypoint.GraphSpec re-exports the proof-facing names readers are most likely to check first:

#check NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward
#check NN.GraphSpec.Models.mlp_detInitParams_eq_torchlean_linear_inits
#check NN.GraphSpec.Primitive.toDAGPrimOp_specFwd_eq

These are worth knowing about for two reasons:

• they confirm that GraphSpec is meant to support theorem statements, not only code generation,

• and they illustrate the "extend op by op" development style that also shows up in the verified runtime and verification layers.

4.3.13. Best First Path🔗

One concrete reading order:

1. Read the GraphSpec README.

2. Open the GraphSpec tutorial API.

3. Run: lake exe torchlean graphspec --backend compiled

4. Read the residual linear model API.

5. Read the ResNet-18 GraphSpec API.

That path moves from "author a typed MLP and lower it into the training API" to "author a real residual DAG with explicit sharing."

4.3.14. Where It Fits In The System🔗

GraphSpec refines TorchLean's semantic model at the architecture boundary. In a Python codebase, architecture authoring and execution are often bundled together. GraphSpec separates them just enough to make semantics and proofs easier, without abandoning runnable models.

To inspect the implementation, start with the GraphSpec README, then move to the sequential and DAG cores, then to the model zoo. The GraphSpec to TorchLean API gives the lowering path into TorchLean Seq, and the GraphSpec TorchLean models expose runtime model programs.

Next: Runtime and Autograd (execution), Graphs and IR (shared op-level graph), Verification (certificates and bounds).

4.3.15. References🔗

• TorchLean paper: https://arxiv.org/abs/2602.22631

• ResNet reference: He et al., "Deep Residual Learning for Image Recognition" (CVPR 2016). https://arxiv.org/abs/1512.03385