ConvNeXt-T: [3,3,9,3] @ [96,192,384,768], 28.6 M at K=1000. The DEFAULT everywhere, so every pre-existing call site is unchanged and every committed artifact re-renders byte-identical.

ConvNeXt-S: T deepened — stage 3 goes 9 → 27, dims UNCHANGED. 50.2 M at K=1000.

ConvNeXt-B: S's depth AND a wider net — [128,256,512,1024]. 88.6 M at K=1000. B is the size that made the dims a parameter: it shares S's depth table exactly, so anything keying on block count alone cannot tell them apart.

Total ConvNeXt blocks = the reference's totalDrop, i.e. the ramp DENOMINATOR is this minus 1. Derived from the stage table the render traverses, not restated beside it — which is what makes it follow D to 36 at ConvNeXt-S without a second edit.

The ramp index of stage si's block j — the reference's dbi, which counts blocks over the WHOLE net. The single source for the drop-site numbering: the forward calls it walking the stages forwards, the backward walking them backwards, and they cannot disagree.

The number of per-example drop-path scale inputs an SD ConvNeXt render takes: one per block.

The model name a render's banner claims, DERIVED from the stage table it was rendered at.

A banner is a render's own description of what it did, and the one thing worse than not having one is having one that lies — cnxDropFwdBanner's own note says exactly that about reusing a drop-free banner on an SD artifact. Passing the name as a second parameter beside D would be two writers for one fact. So it is read off D.

It matches on the WHOLE RECORD, not on the block count, and that is not fussiness. B is [3,3,27,3] like S, so a name keyed on cnxDropTotal (36 blocks) names S and B alike and every B artifact would open by calling itself a ConvNeXt-S. The guards below enumerate all three rather than spot-checking one. An unrecognised table gets a name that SAYS it is unrecognised, rather than falling back to "ConvNeXt-T" the way a getD would.

The %dp<i>: tensor<Bxf32> inputs an SD render appends to its signature — one per block, in ramp-index order, which is the order the driver's dropScales writes them into the blob. Empty when off, which is what keeps every committed artifact byte-identical.

The %one/%zero constants the channel-LN chain binds lnRowF/lnRowBack's SCALAR γ/β to — the real per-channel affine is rowScaleF/rowBiasF downstream, exactly as ViT does it. Emitted once per module body.

Wire the operand and forget the prelude, and the artifact uses an SSA name nothing defines — iree-compile/XLA say "use of undeclared SSA value name" and nothing before them says anything. regen_verified_mlir.sh check's prelude audit is what catches it.

One LayerNorm forward site — ConvNeXt's real channel-LN: transpose to [h·w, c], normalise each spatial row over its channels at the scalar identities %one/%zero, apply the real [c] affine (vecLnSite at m = h·w), transpose back.

The HEAD LN forward site — the paper's norm(x.mean([-2,-1])).

It is cnxLnFwdSite with the two transposes DELETED, and that is the whole difference: after GAP the tensor is a single [d] row, so "normalise each spatial row over its channels" and "normalise the feature vector" are the same function at m = 1. Mirrors Proofs.StableHLO.headLNGraph op for op.

It is vecLnSite at m = 1, so every operand is annotated Vec (1 * d), never Vec d. 1 * d does NOT reduce for a VARIABLE d (Nat.mul recurses on its second argument), and d here is V.dims[3]!, which moves with the ConvNeXt size. It is the same annotation convNextBackAll's smoothing chain carries, for the same reason.

The decayed / excluded split, as the renderer computes it.

allParams is private (it is this file's internal signature source); this is the one thing outside it that legitimately needs the list — tests/TestWdExcludeTie.lean, which must read the SAME names and shapes the renderer chose %wd/%wdz from. Exposing an alias rather than dropping private keeps the surface one definition wide.

@convnext_fwd from the per-example chain — convNextFwdChain, the forward both train steps in this file emit, followed by return logits. Takes %x plus the 182 params of allParams in func-arg order (183 inputs) and returns logits [cBS, nClasses]. Around the chain the text is the signature, a banner comment and chLnPrelude.

The committed verified_mlir/convnext_fwd.mlir is written by ConvNeXtRenderB (convNextFwdRenderB); TestConvNeXtFwdBTie checks this render against it byte for byte, and scripts/regen_verified_mlir.sh check checks that its body is a prefix of convnext_train_step.mlir's.

The whole-net forward + cotangent + backward traversal, SHARED by the SGD and AdamW renders.

Returns (code, params, softmax): every emitted line; one SSA per parameter — the updated param at adam := false, the un-fused gradient at adam := true; and the softmax SSA, which the AdamW render's report-only %loss reads.

smooth is the cotangent recipe. none → the SGD render's (softmax − onehot)/B, unchanged down to the hand-written %dy divide. some (α, −α/K, B) → the label-smoothed ((softmax − onehot) + α·onehot − α/K)/B composed from kit ops, which is what the AdamW recipe trains on. ConvNeXt already spells the ÷B explicitly (unlike ViT/R34, which fold the mean into lr), so here the smoothing is the only difference between the two cotangents.

The softmax is prettyd on its own line rather than nested inside the .sub so that %loss can read it; .operand is a leaf that emits nothing, so the fresh-name sequence is the same either way.

ConvNeXt-T (full [3,3,9,3]) SGD train step rendered from the verified AST, the writer of verified_mlir/convnext_train_step.mlir: %x, the 182 params and %onehot in (184 inputs), the 182 updated params out. All 182 parameter gradients are SHlo nodes, and every parameter but the stem weight psW is updated by a fused SHlo SGD op whose output is the updated parameter. Hand-written text: the signature, the %sc/%bsc constants, chLnPrelude, the %dy divide, the GAP-backward block, and psW's update (sgdOf around the certified .convStride4WeightGrad).

The cotangent is plain CE with an explicit ÷B — unlike ViT/R34, which fold the batch mean into lr — so the committed cLR = 0.1 is an effective 0.1, the house convention spelled differently.

The driver's variant slug for a given replica count: the artifact is verified_mlir/convnext_<variant>_train_step.mlir, the entry point is @convnext_<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. The #guards at the bottom pin the literal #eval paths against this.

Unlike mnv2AdamVariant/r34AdamVariant there is no batch suffix.

The EMA renders get their OWN slugs (ema/emadp), for the reason the RMSProp ones do: a render carrying a fourth [θ|m|v|ema] region must never be able to overwrite the artifact the AdamW trainer runs, whose blob has three: two writers for one path, where the last one wins, and here it would also be an arity mismatch the driver could not survive.

ConvNeXt AdamW train step rendered from the verified AST — the wrapper ConvNeXtRenderB calls (with traversal set to its batched chain) to write convnext_adam_train_step.mlir and the other ConvNeXt AdamW/EMA artifacts.

Same backward as convnext_train_step (convNextBackAll, one traversal) but taking the un-fused gradients, each fed to the proven AdamW triple. The cotangent adds label smoothing (α = 0.1, K = nClasses); ConvNeXt already spelled the ÷B explicitly, so that is the only difference.

Interface at ConvNeXt-T, ema := false, no drop-path: 551 in (%x, 182 θ, 182 m, 182 v, %lr/%bc1/%bc2, %onehot) / 549 out (182 θ', 182 m', 182 v', %loss/%bc1/%bc2), the packed [θ|m|v] layout the AdamW trainer reads.

All 182 parameter gradients are SHlo nodes, and each update is the proven AdamW triple. Hand-written text: the signature and constants, the GAP-backward block (in convNextBackAll), the %bc1/%bc2 passthroughs, and the report-only %loss (on no gradient path).

replicas > 1 renders the DATA-PARALLEL variant to its own entry name and artifact path via cnxAdamVariant, so producing it can never clobber the one the trainer runs. The only difference is one all_reduce(add)/N per parameter gradient, between the certified gradient and the certified AdamW triple: certified gradient → trusted collective → certified AdamW. See optOne for the carve-out.