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 with the identity skip (ic = oc): everything at hh×ww, block output = addVB (project-BN out) (block input). The bottleneck is LINEAR — no relu6 after the add.

EXPAND-NO-SKIP stride-1 forward (b11/b17): as irFwdSkipB but 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.

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.

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 (b1/b3/b5/b6): 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 (b2/b4): everything at hh×ww, with an addV skip on the block input (ic = oc).

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

EXPAND-NO-SKIP stride-1 forward (b11/b17): expand(1×1)→BN→relu6 → depthwise(3×3)→BN→relu6 → project(1×1)→BN. Everything at hh×ww; ic ≠ oc so NO skip (block output = project-BN out).

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.

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