STRIDED inverted-residual forward: expand at the input 2hh×2ww, depthwise downsamples 2hh×2ww → hh×ww, project 1×1 at hh×ww. NO skip.

STRIDE-1 inverted-residual forward, shared by the identity-skip (skip := true) and expand-no-skip block kinds: everything at hh×ww; with the skip the block output is addVB (project-BN out) (block input), without it the project-BN output directly. The bottleneck is LINEAR — no relu6 after the add. One function with a flag, as irBackStride1GradB is on the backward side, so the two kinds cannot drift. ic = oc whenever skip is true.

STRIDE-1 inverted-residual forward with the identity skip (ic = oc): irFwdStride1B at skip := true.

EXPAND-NO-SKIP stride-1 forward (b11/b17): irFwdStride1B at skip := false, for ic ≠ oc, so the block output is the project-BN output directly.

NO-EXPAND forward (b1, the canonical t = 1 block): depthwise(stride-1, on ic channels) → BN → relu6 → project(1×1 ic→oc) → BN. No expand conv, no skip. er is the depthwise INPUT (= the block input), which is what the depthwise weight gradient reads.

STRIDED backward + 12 un-fused gradients. The depthwise input gradient lands at 2hh×2ww; no skip, so the dx handed to the previous block is the expand-conv backward directly.

STRIDE-1 backward + 12 un-fused gradients, shared by the skip (skip := true) and no-skip block kinds — the ONLY difference is the skip's addVB fan-in on the dx, which is why they are one function with a flag rather than two near-copies (the double-writer disease one level down). ic = oc whenever skip is true.

NO-EXPAND backward + 8 un-fused gradients (b1). No expand conv and no skip, so the dx to the stem is the depthwise backward directly.

A 12-param inverted-residual block's signature, func-arg order.

The no-expand block's signature (b1): depthwise on ic channels + project ic→oc. 8 params.

The 210 parameters of the 17-block paper-spec net, in func-arg order. stem (4) + b1 no-expand (8) + b2..b17 (16 × 12 = 192) + head (4) + dense (2) = 210 — the same decomposition paperSig uses, at the names the committed AdamW artifact presents.

A 3-BN block's stat slots (expand-BN, depthwise-BN, project-BN).

The 104 BN running-statistic slots = 52 BN layers × (μ, var): stem 1, b1 two (no expand BN), b2..b17 three each (48), head 1. Both an input (…i) and an output slot.

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/mobilenetv2_<variant>_train_step.mlir, the entry point is @mobilenetv2_<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. B = 32 is deliberately unsuffixed so the committed artifact keeps its name. The #guards at the bottom pin the literal #eval paths against this.

Stem forward: 3×3/s2 XLA-SAME conv (3→32, 224→112) → batch BN → relu6 (no max-pool).

Head forward: 1×1 conv (320→1280) → batch BN → relu6 → GAP(7×7) → [dropout] → dense, on block 17's output xName.

The MobileNetV2 forward chain at the BATCHED index — one traversal, consumed by both @mobilenetv2_fwd and every train step that differentiates it.

This exists so @mobilenetv2_fwd and the batch-BN train steps cannot be different nets: a forward built from a PER-EXAMPLE chain (bnPerChannelF, reduce [2,3], divisor H·W) next to batch-BN train steps (reduce [0,2,3], divisor B·H·W) is a different function. This is ResNet34RenderB.r34FwdChainB's shape, for ResNet50RenderB.r50FwdChainB's reason.

The EVAL forward is deliberately NOT moved onto this chain, exactly as ResNet-34's and ResNet-50's are not: bnPerChannelEvalF reads frozen per-channel statistics and reduces nothing, so mobilenetv2_fwd_eval.mlir is BatchNorm-world-agnostic and correct against both chains; moving it buys nothing.

Extracting the traversal is byte-neutral for the train step: pretty's SSA counter follows the call SEQUENCE, and the sequence is unchanged.

@mobilenetv2_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/mobilenetv2_fwd.mlir. Takes %x plus the parameters in mnv2SigList order — 159 inputs at the shipped convBias := false — and returns logits [B, nClasses].

It normalises over the BATCH, as the AdamW and RMSProp steps whose accuracies the book quotes do. Parameter names come from mnv2SigList, this file's single source; the driver binds positionally.

MobileNetV2 (17-block paper spec) AdamW train step, batch BN, rendered from the verified AST at N := B. 739 inputs (%x, 210 θ, 210 m, 210 v, %lr/%bc1/%bc2, 104 running-stat slots, %onehot) and 737 outputs (210 θ', 210 m', 210 v', %loss/%bc1/%bc2, 104 batch stats) — the interface the committed hand-written artifact already presents, so the driver is unchanged. Parameter ORDER comes from mnv2SigList and stat order from mnv2StatSigList, the single sources, so the arity/order contract cannot drift.

Stem 3×3/s2 (3→32, 224→112, NO maxpool) → b1 (no-expand t=1, 32→16) → b2..b17 (4 stride-2 downsamples, 10 identity skips, 2 stage-first widenings) → 1×1 conv-BN-relu6 head (320→1280) → GAP → dense (1280→nClasses).

STRIDED inverted-residual forward (b2/b4/b7/b14 in mnv2FwdChain): expand at the input 2hh×2ww, depthwise downsamples 2hh×2ww → hh×ww, project 1×1 at hh×ww. NO skip.

NO-EXPAND inverted-residual forward (b1): depthwise(stride-1, on ic channels)→BN→relu6 → project(1×1 ic→oc)→BN. NO expand, NO skip. f.er = the depthwise INPUT (= block input xName), f.dr = the project input. (ec/en are unused for this block kind.)

STRIDE-1 inverted-residual forward (eval), shared by the skip and expand-no-skip block kinds — irFwdStride1B's eval twin: expand(1×1)→BN→relu6 → depthwise(3×3)→BN→relu6 → project(1×1)→BN, everything at hh×ww, then an addV skip on the block input when skip (ic = oc). The bns layout is written here once for both kinds.

STRIDE-1 inverted-residual forward (b3, b5, b6, b8–b10, b12, b13, b15, b16 in mnv2FwdChain): irFwdStride1 at skip := true, the addV skip on the block input (ic = oc).

EXPAND-NO-SKIP stride-1 forward (b11/b17): irFwdStride1 at skip := false; ic ≠ oc so NO skip (block output = project-BN out).

NO-EXPAND block sig (b1): depthwise on ic channels + project ic→oc. 8 params.

The 17-block paper-spec param signature, func-arg order: stem (4) + b1 no-expand (8) + 16×12 + head (4) + dense (2) = 210 tensors, or 158 at convBias := false (the #guards below). The signature of the eval forward @mobilenetv2_fwd_eval, in the same order as mnv2SigList under this file's eval-chain names.

The eval forward's stem: 3x3/s2 XLA-SAME conv (3->32, 224->112) -> BN (stn) -> relu6, on %x. Returns the code and the relu6 output's name.

The eval forward's head: 1x1 conv (320->1280) -> BN (hn) -> relu6 -> GAP(7x7) -> dense(1280->nClasses), on block 17's output xin. Returns the code and the logits' name.

The full 17-block paper MobileNetV2 forward as pretty of the verified AST, at the PER-EXAMPLE index. 3x3/s2 stem (3->32, 224->112) -> the [t,c,n,s] inverted-residual stack (112->56->28->14->7) -> 1x1 head (320->1280) -> GAP(7x7) -> dense(1280->nClasses).

The EVAL forward: every BN site is RenderKit.bnEvalSite (frozen running statistics), so this writes @mobilenetv2_fwd_eval only; the training forward is the batched mnv2FwdChainB.

The @mobilenetv2_fwd_eval argument signature. The 104 stat slots come off the SAME bns the traversal built — never a parallel 52-entry table.

@mobilenetv2_fwd_eval rendered ENTIRELY from the verified AST — the inference forward, every BN site consuming frozen per-channel running stats (bnPerChannelEvalF) instead of reducing statistics out of its activation. Same 210 params in the same order, plus the 104 stat inputs (52 BN layers × μ/var, interleaved per layer in bnChannels order): 315 inputs.

Its train-step partner is the batch-BN mobilenetv2_adam_train_step in MobileNetV2RenderB, whose returned batch μ/var the driver EMAs into exactly these slots. Being frozen-stat affine, this graph is the same in either BN world — which is why it can live beside the per-example chain: bnPerChannelEvalF performs no reduction, so there is no batch to be honest about.