GraphSpec entrypoint

Curated umbrella import for GraphSpec.

This is the public single-import surface for GraphSpec users. For the full model-spec interface, use:

import NN.Entrypoint.GraphSpec

It gives you:

• the canonical DAG model surface (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.

We keep this file as an umbrella re-export (no real logic here) so the import path stays stable even as the internals evolve.

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 Shape) (τ : 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.