TorchLean-executable model: ResNet-18 (GraphSpec.DAG-backed)

This is the executable-facing wrapper for NN.GraphSpec.Models.ResNet18.

Important design point:

• TorchLean NN.Seq is sequential, so it cannot directly represent residual DAGs.
• GraphSpec.DAG can represent them, and can compile to a backend-generic TorchLean program.

So we expose:

• resnet18Model: the DAG Model (parameters + typed body),
• resnet18Program: a TorchLean.Program you can run on eager/compiled backends,
• resnet18InitParams: deterministic Float initialization matching the parameter layout.

def NN.GraphSpec.Models.TorchLean.resnet18Model (inC h w numClasses : ℕ) (h_inC : inC > 0) (h_h : h > 0) (h_w : w > 0) (h_cls : numClasses > 0) : DAG.Model (ResNet18.params inC numClasses) [Shape.CHW inC h w] (Shape.Vec numClasses)

The ResNet-18 model as a GraphSpec.DAG.Model (typed residual graph).

def NN.GraphSpec.Models.TorchLean.resnet18Program (inC h w numClasses : ℕ) (h_inC : inC > 0) (h_h : h > 0) (h_w : w > 0) (h_cls : numClasses > 0) {α : Type} [Context α] [DecidableEq Spec.Shape] : Runtime.Autograd.TorchLean.Program α (ResNet18.params inC numClasses ++ [Shape.CHW inC h w]) (Shape.Vec numClasses)

Compile resnet18Model into a backend-polymorphic TorchLean program.

You can run this on the eager backend or record it into the compiled backend.

def NN.GraphSpec.Models.TorchLean.resnet18InitParams (inC h w numClasses : ℕ) (h_inC : inC > 0) (h_h : h > 0) (h_w : w > 0) (h_cls : numClasses > 0) : Runtime.Autograd.Torch.TList Float (ResNet18.params inC numClasses)

Deterministic Float initialization for the ResNet-18 parameter list.