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 syntax (NN.GraphSpec.Chain + >>>) for chain models and its lowering into DAG,
• the Spec semantics (NN.GraphSpec.Interp.spec) and TorchLean lowering (NN.GraphSpec.Chain.toProgram),
• sequential and DAG primitive packs,
• the GraphSpec example architectures (NN.GraphSpec.Models),
• the optional lowering to Runtime.Autograd.Model.Layers.Seq when primitives provide toLayerM?,
• 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 Chain pipelines can be lowered to DAG via Core.LowerToDAG.Chain.toDAGTerm and Core.LowerToDAG.Chain.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 Spec.Shape) (τ : Spec.Shape) : Type 1

A small “model” wrapper around DAG terms.

This mirrors the sequential Chain 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} [TorchLean.Storage α] [Context α] : TorchLean.TensorPack α ps → TorchLean.TensorPack α ins → TorchLean.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.toProgram {ps ins : List Spec.Shape} {τ : Spec.Shape} (m : Model ps ins τ) {α : Type} [TorchLean.Storage α] [Context α] : Runtime.Autograd.Model.Program α (ps ++ ins) τ

Lower a DAG model to an execution-polymorphic TorchLean program.

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