Graph Specifications

Curated umbrella import for GraphSpec.

Use this import when working with GraphSpec models, primitives, lowering, and bridge theorems:

import NN.GraphSpec

It gives you:

• the canonical DAG model API (NN.GraphSpec.DAG.Term, NN.GraphSpec.DAG.Model),
• the sequential authoring sugar (NN.GraphSpec.Graph + >>>) for chain models and its lowering into DAG,
• the Spec semantics (NN.GraphSpec.Interp.spec) and TorchLean compiler (NN.GraphSpec.Compile.torchProgram),
• sequential and DAG primitive packs,
• the GraphSpec example architectures (NN.GraphSpec.Models),
• the optional lowering to TorchLean.NN.Seq when primitives provide toLayerDefM?,
• and the model/primitive bridge theorems that connect GraphSpec syntax to Spec references.

Umbrella re-export; the implementation lives in the imported modules.

Unified model type

GraphSpec's canonical “runnable + spec” representation is DAG.Model.

Sequential Graph pipelines can be lowered to DAG via Core.LowerToDAG.Graph.toDAGTerm and Core.LowerToDAG.Graph.toDAGModelZeroInit, so users can author simple pipelines and still end up in the same general model representation.

@[reducible, inline]

abbrev NN.GraphSpec.Model (ps ins : List Tensor.Shape) (τ : Tensor.Shape) : Type 1

A small “model” wrapper around DAG terms.

This mirrors the sequential Graph surface:

• ps are parameter tensor shapes (tracked at the type level),
• ins are the shapes of non-parameter inputs (e.g. data tensors),
• τ is the output shape.

The model body is a Term (ps ++ ins) τ, i.e. it expects an environment that starts with parameters and then contains the actual inputs.

@[reducible, inline]

abbrev NN.GraphSpec.Model.specFwd {ps ins : List Spec.Shape} {τ : Spec.Shape} (m : Model ps ins τ) {α : Type} [Context α] : Runtime.Autograd.Torch.TList α ps → Runtime.Autograd.Torch.TList α ins → Spec.Tensor α τ

Pure forward semantics of a DAG model.

We build the full environment Γ = ps ++ ins by appending the parameter list and the input list, then evaluate the body using Term.eval.

@[reducible, inline]

abbrev NN.GraphSpec.Model.torchProgram {ps ins : List Spec.Shape} {τ : Spec.Shape} (m : Model ps ins τ) {α : Type} [Context α] [DecidableEq Spec.Shape] : Runtime.Autograd.TorchLean.Program α (ps ++ ins) τ

Compile a DAG model to a backend-generic TorchLean program.

The resulting program expects arguments in the order ps ++ ins (parameters first, then inputs), matching the environment discipline used by specFwd.