The SPATIAL table, and it is the one thing that is NOT a size parameter: 224 with a 4×4/s4 patchify stem gives 56/28/14/7 at every ConvNeXt size. T, S and B differ in depth and width only, so this stays a constant and the 7s in the GAP backward stay literals.

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 SGD update wrap for ConvNeXt's stem weight, taking the gradient's SSA name explicitly: the certified SHlo ops emit a fresh %vN.

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 head LN's input-VJP: dx = lnRowBack γ=1 (rowScale γ dy). xName is the saved LN input — the GAP output — which lnRowBack re-normalises from rather than saving x̂/istd.

The head LN's γ tail — veclnGamma{Grad,Sgd} at N = 1.

The head LN's β tail — rowDenseBias{Grad,Sgd} at N = 1, reducing dims = [0,1], i.e. contracting the batch (and the single row) as a shared [d] parameter needs.

One LayerNorm input-VJP site: dx = transposeᵀ (lnRowBack γ=1 (rowScale γ dyᵀ)). xName is the saved LN INPUT — lnRowBack recomputes x̂/istd from it rather than saving them.

The γ tail for one LN site — the per-channel veclnGamma{Grad,Sgd}. The transposes of xName/cot are re-emitted here rather than threaded from lnBackSite: pretty has no CSE, but XLA does, and XLA collapses exactly this kind of duplicated subtree.

The β tail — the per-channel rowDenseBias{Grad,Sgd}. It reduces dims = [0,1], i.e. it contracts the BATCH as well as the spatial rows, which is what a shared [c] parameter needs.

The LN γ/β are [c] — the real channel-LN's per-channel affine. This list is the func signature AND the return types, so getting it wrong is not silent — the body uses %…ng at tensor<{c}xf32> and the compiler rejects a signature that disagrees with itself.

nClasses defaults to 10 (Imagenette) so every existing call site is unchanged; the ImageNet renders pass 1000. Only the head moves — 180 of the 182 entries are class-independent.

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

A namespaced public alias of allParams (this file's signature source, itself public) for the one thing outside it that needs the list — tests/TestWdExcludeTie.lean, which must read the SAME names and shapes the renderer chose %wd/%wdz from.

The full ConvNeXt-T [3,3,9,3] forward as pretty of the verified AST. 4×4/s4 patchify stem (3→96, 224→56) → 4 stages at 56/28/14/7 with 2×2/s2 downsamples between them → GAP(7×7) → head LN → dense(768→10). Every emitted line is pretty of a verified SHlo node.

There is no train/eval mode here, and there should not be — ConvNeXt normalises with LayerNorm, which reduces over the channel/spatial axes of ONE example and never over the batch. So the forward is already class-batch-independent: train == eval, and @convnext_fwd is the only forward artifact this net needs (unlike the BN nets, which need a frozen-stats peer).

@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.

β₁/β₂/ε/wd as graph constants — the committed ConvNeXt-T AdamW recipe.

wdStr is a parameter for the reason ViTRender.vitAdamConsts' is: the Imagenette and ImageNet configs disagree on it by 500×. convnextVerified's recipe is the baked 1e-4; convnextTinyImagenetConfig.weightDecay := 0.05. The default is unchanged, so every committed artifact keeps its bytes; only the ImageNet wx render passes 0.05.

The hand-written block the AdamW train-step banners name beside trainStepHandNote's list: the GAP backward (%dgi … %dgapf) on the gradient path.

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.