The ResNet-34 parameters in net.paramShapes (= func-arg) order, names + types. The forward, the eval forward and the train step all take their signature from here, so the arity/type/order contract the driver relies on cannot drift between renders.

110 at the shipped convBias := false — stem 3 + 13 identity blocks × 6 + 3 downsample blocks × 9 + dense 2 — and 146 with the conv biases in. Every writer below omits the argument, so every committed artifact is the 110 one; the biases are zeroBiasPrelude's zero constants.

The 72 running-stat inputs — 36 BN layers × (μ, var), each [oc], in BN-forward order: stem, then per identity block n1 n2, per downsample block n1 n2 np. This is exactly the order VerifiedNet.bnChannels is listed in, which is how the driver packs runningBnStats (bnChannels.foldl (fun acc c => acc ++ #[#[c], #[c]])) — μ and var interleaved per layer, NOT all-μ-then-all-var. Appended after the parameters, so @resnet34_fwd_eval takes 1 + 110 + 72 = 183 inputs as committed (1 + 146 + 72 = 219 at convBias := true).

@resnet34_fwd_eval rendered ENTIRELY from the verified AST — the inference forward, with every BN site consuming frozen per-channel running stats (bnPerChannelEvalF) instead of reducing statistics out of its activation. Same net, same parameters in the same order, plus the 72 stat inputs of r34StatSigList: 183 inputs as committed, returning logits [B, nClasses].

This is the eval partner of resnet34AdamTrainStepText (this file), whose 72 returned batch statistics the driver EMAs into exactly these slots.

Identity block forward: conv1→BN1→relu1→conv2→BN2→(+x)→relu, all at N := B.

Downsample block forward: strided body + strided projection skip. cin→c, 2hh→hh.

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/resnet34_<variant>_train_step.mlir, the entry point is @resnet34_<variant>_train_step, and LEAN_MLIR_VARIANT selects it.

All three must agree. The shim checks the entry name and refuses a mismatch outright ("entry mismatch") rather than running the wrong graph — which is exactly what it did the first time the DP render kept the single-device name. Deriving the name here, from the same two numbers the render is built from, is what stops it drifting from the #eval paths below; the #guards at the bottom pin those literal paths against this function.

B = 32 is deliberately unsuffixed, so the two existing artifacts keep their names and bytes.

Stem forward: 7×7/s2 conv → batch BN → relu → He et al.'s 3×3/s2 max-pool, on %x. A 2×2 non-overlapping .maxPool would give the identical 112→56 output shape and be a different function, so no shape check tells them apart.

Head forward: GAP(7×7) → dense(512→nClasses) on the last block's output xName. Returns the text and the GAP and logit names.

The ResNet-34 forward chain at the BATCHED index — one traversal, consumed by both @resnet34_fwd and every train step that differentiates it.

@resnet34_fwd rendered from the BATCHED chain — the same traversal every batch-BN train step in this file differentiates, so the net that scores and the net that trains are one graph by construction. The writer of verified_mlir/resnet34_fwd.mlir. Takes %x plus the parameters in r34SigList order — 111 inputs at the shipped convBias := false — and returns logits [B, nClasses].

ResNet-34 [3,4,6,3] AdamW train step, batch-BN, rendered from the verified AST at N := B. 407 inputs at the shipped convBias := false (%x, 110 θ, 110 m, 110 v, %lr/%bc1/%bc2, 72 running-stat slots, %onehot) and 405 outputs (110 θ', 110 m', 110 v', %loss/%bc1/%bc2, 72 batch stats); 146 θ at convBias := true. Parameter ORDER comes from r34SigList, the same single source both forwards use, so the arity/order contract cannot drift between them.