Which dataset a verified trainer runs on. Picks the loader, the eval-split name, and whether the training images need a 256²→224² center-crop per batch.

• mnist : VerifiedData

  MNIST idx files directly under dataDir (28×28×1, no crop).

• cifar : VerifiedData

  CIFAR-10 .bin records under dataDir/cifar-10 (32×32×3, no crop).

• imagenette : VerifiedData

  Imagenette under dataDir/imagenette — train stored at 256² (center-cropped to 224² per batch), val at 224².

• imagenet : VerifiedData

  Full 1000-class ImageNet, streamed from the generated tfds shim. 1,281,167 train / 50,000 val at 224².

  Unlike every case above, this one is NOT preloaded: at f32 the train split is ~938 GiB of host RAM against a 188 GB box, so it cannot be. Batches arrive over a pipe from that net's own jax/.lake/build/generated_*_imagenet_shim.py (VerifiedNet.shimScript), already augmented, mean/std-normalized and flattened to (B, 3·224·224) — so the Lean side does no augmentation at all for this dataset, which is the point: there is exactly one definition of the transform and it is the one the JAX reference trainer uses.

  The shim is per net: each is generated from the TrainConfig that net's reference trainer runs, so the transform has one definition per net and the net selects it.

  The VAL split is streamed per pass too (spawnValStream); 49,920 images after tfds drop_remainder, the same count the reference run reported.

A verified-vocabulary layer. Restricted to ops with proven HasVJP witnesses; each carries enough to derive its slice of the param layout.

• convBn (ic oc k stride : Nat) : VLayer

  conv (oc←ic, k×k, stride) → per-channel BN → relu. Params {W,b,γ,β}.

• convBnNB (ic oc k stride : Nat) : VLayer

  conv → per-channel BN → relu with no conv bias — {W, γ, β}. BN removes a conv bias ((x+b) − mean(x+b) = x − mean(x)), so a BN-followed conv carries none in He et al.'s .convBn; ResNet-34 uses this and the nets that ship a bias use convBn (tests/TestConvBiasZero.lean measures that the BN-followed conv biases get zero gradient).

• maxPool (k stride : Nat) : VLayer

  max pool k×k / stride. No params.

• residualStage (ic oc nBlocks stride : Nat) : VLayer

  A basic-block residual stage: nBlocks blocks at oc channels. The first block downsamples (and projects the skip) iff stride ≠ 1 ∨ ic ≠ oc; the rest are identity.

• bottleneckStage (ic oc nBlocks stride : Nat) : VLayer

  A bottleneck residual stage (ResNet-50/101/152): nBlocks blocks, each 1×1 (oc/4) → BN → relu, 3×3 (oc/4) → BN → relu, 1×1 (oc) → BN, +skip, relu. The first block projects the skip (1×1 → BN) iff stride ≠ 1 ∨ ic ≠ oc — the same dispatch residualStage uses, and for R50 that fires on all four stages, because stage 1 changes 64→256 at stride 1 where R34's stage 1 is ic = oc.

  This is ResNet v1.5, not He et al.'s v1: the stride sits on the 3×3 (and on the projection), with the leading 1×1 at stride 1, as in the reference (jax/Jax/Codegen.lean's bottleneck_block_down). Putting it on the first 1×1 compiles, trains, descends and is a different net.

  No conv biases — every conv here is BN-followed, so a bias cannot reach the output (convBnNB's argument, four convs at a time). torchvision's R50 carries none either, which is why the derived count lands on the reference's 25,557,032 with no adjustment.

• globalAvgPool : VLayer

  global average pool. No params.

• dense (ic oc : Nat) : VLayer

  dense ic→oc. Params {W,b}.

• relu : VLayer

  ReLU activation (pointwise). No params.

• conv (ic oc k stride : Nat) : VLayer

  plain conv (oc←ic, k×k, stride) + bias, NO batch-norm. Params {W,b}.

• flatten : VLayer

  flatten [C,H,W] → vector. No params (a reshape).

• bn : VLayer

  scalar-global BatchNorm (the proven bnForward): normalize over the whole c·h·w feature map per example, scalar γ/β. Params {γ, β} (rank-0).

• bnPerChannel (oc : Nat) : VLayer

  per-channel (per-example) BatchNorm (the proven bnPerChannelFlat, m=h·w): normalize each of oc channels over its own h·w spatial map per example, per-channel γ/β [oc]. Train=eval (no running stats). Params {γ:[oc], β:[oc]}.

• invertedResidual (ic mid oc stride : Nat) : VLayer

  MobileNetV2 inverted-residual block (ic→mid→oc, depthwise stride): expand 1×1 conv→per-channel BN→relu6, depthwise 3×3→BN→relu6, project 1×1→BN (linear bottleneck),

  • residual when stride=1 ∧ ic=oc. Params {W,b,γ,β} ×3 (expand/depthwise/project).
• invertedResidualNB (ic mid oc stride : Nat) : VLayer

  MobileNetV2 inverted-residual block with no conv biases — {W,γ,β} ×3. Every conv in the block is BN-followed, so a bias cannot reach the output (the convBnNB argument, three convs at a time); the torchvision/JAX reference carries none, and with this constructor the derived count matches the reference's. Kept beside invertedResidual for convBnNB's reason — a net whose blocks ship biases can still say so.

• mbConvSE (ic mid oc r k : Nat) : VLayer

  EfficientNet MBConv block (ic→mid=t·ic→oc, depthwise k×k, SE ratio r): expand 1×1 (skipped when mid=ic, i.e. t=1) → BN → swish, depthwise k×k → BN → swish, squeeze-excite (Ws₁[mid,r],bs₁[r],Ws₂[r,mid],bs₂[mid], sigmoid gate), project 1×1 → BN. Params: (expand{W,b,γ,β} if t≠1) ++ depthwise{W,b,γ,β} ++ SE{Ws₁,bs₁,Ws₂,bs₂} ++ project{W,b,γ,β}.

• mbConvSENB (ic mid oc r k : Nat) : VLayer

  EfficientNet MBConv with no conv biases on the BN-followed convs — expand/depthwise/ project become {W,γ,β}. The squeeze-excite biases stay: SE's two 1×1 convs are followed by an activation (the sigmoid gate), not BN, so nothing absorbs them and the reference carries them; only a BN-followed conv can drop its bias. With both rules the derived count matches the reference's 5,288,548 at 1000 classes.

• uib (ic oc expand stride preDWk postDWk : Nat) : VLayer

  MobileNetV4 Universal Inverted Bottleneck: optional pre-DW (preDWk) → 1×1 expand ic→mid → optional post-DW (postDWk) → 1×1 project mid→oc, every conv BN-followed and therefore bias-free (convBnNB's argument, and what Spec.lean's baseline count assumes). mid = ic * expand.

  k = 0 means "omit that depthwise", which is how one constructor expresses all four of MNv4's block families — ExtraDW (both DWs), IB/MBConv (post only), ConvNeXt-like (pre only), FFN (neither).

  A wrong pre/post dispatch is invisible to this function: a pre-DW and a post-DW at the same k and the same channel count contribute identical parameter shapes, so emitting one where the table says the other yields a net that type-checks, trains, descends, and is not MobileNetV4. R50's stride-on-the-3×3 and the 2×2 stem pool are invisible in the same way. The check is a forward tie against the reference on shared weights, not a parameter count.

• fusedMbConvNB (ic oc expand k stride : Nat) : VLayer

  Fused inverted bottleneck, single block, no squeeze-excite — EfficientNetV2's early-stage block, and MobileNetV4's stage 0. k×k regular conv ic→mid (stride) → BN → swish → 1×1 project mid→oc → BN, no activation after the project; skip iff stride = 1 ∧ ic = oc. "Fused" = the MBConv expand-1×1 and depthwise collapse into ONE regular k×k conv, which is why nothing here is depthwise. mid = ic * expand. Bias-free — both convs are BN-followed.

  ReLU, as timm's EdgeResidual in mobilenetv4_conv_medium.

  Narrower than the baseline Layer.fusedMbConv, which also carries nBlocks and useSE. MNv4 uses n = 1, useSE = false, and no render exists for the other settings, so the constructor cannot express them.

• convNextBlock (c : Nat) : VLayer

  ConvNeXt block @ c channels (expand ratio 4): depthwise 7×7 → scalar-LN → 1×1 expand c→4c → GELU → 1×1 project 4c→c → layerScale (per-channel γ). Params: depthwise{W,b}; LN{γ,β scalar}; expand{W,b}; project{W,b}; layerScale{γ:[c]}.

• convNextBlockCh (c : Nat) : VLayer

  ConvNeXt block with the channel LayerNorm — γ,β : [c] instead of two rank-0 scalars. The normalisation axis changes with it (over c per spatial position, not over the whole c·h·w map), but that is invisible to the LAYOUT; what the layout sees is the affine going from 2 floats to 2c. Kept beside convNextBlock for convBnNB's reason.

• layerNorm (d : Nat) : VLayer

  Per-channel LayerNorm over d features (normalize ∘ [d] affine). Params {γ:[d], β:[d]} — the non-scalar form (cf. bn, which is scalar-global).

• transformerBlock (d m : Nat) : VLayer

  Pre-norm transformer block (dim d, MLP hidden m): LN1 → MHSA (Wq/Wk/Wv/Wo [d,d]) → +x → LN2 → MLP (d→m→d) → +x. Params: LN1{γ,β}; {Wq,bq,Wk,bk,Wv,bv,Wo,bo}; LN2{γ,β}; {Wfc1[d,m],bfc1, Wfc2[m,d],bfc2} (per-channel [d] LN).

• param (dims : Array Nat) (kind : Nat) : VLayer

  A bare learned parameter tensor (dims, initKind) — e.g. ViT's CLS token / positional embedding (not produced by any standard layer).