The stochastic-depth sites: the block indices (into mnv4Blocks) of the 18 skip rows, in order. Site k is %dp<k>, and the driver's dropKeeps lists one keep per site in this order. The three strided rows (0, 2, 10) have no residual, so no site, as in the reference's uib_block (_drop_branch only under residual.shape == x.shape).

Block bi's drop site, none for a strided row.

The MobileNetV4-Conv-M parameter inputs, in func-arg order: stem (3), the fused stage, the 21 UIB blocks, the TWO head convs, the classifier. Single source for the signature and the return order, the same role r50ShapeList plays for R50.

This list and VLayer.toSpecs are TWO HAND-WRITTEN READINGS of the same layout — the renderer cannot import the spec without inverting the dependency, which is the same two-lists shape as toSpecs == XLayout.specs elsewhere. mnv4-fwd-smoke is the gate that pins them.

The same list as MLIR types. Derived, so the shapes have one definition.

The 154 BN running-statistic slots = 77 BN layers × (μ, var), in forward-traversal order: stem, the fused stage's two, each UIB block's (2–4 depending on family), the head.

A misaligned stat slot is SILENT: the arities still match and the wrong layer's statistics simply flow into the wrong @mnv4_fwd_eval slot. That is why the order here and the order the train step returns them in are both derived from the same block table, and why the eval forward reads them through mnv4Bn's statP rather than an independently-numbered list.

The stat slots as MLIR types. Derived, so the widths have one definition.

Fused inverted bottleneck, stride 2, no SE — MobileNetV4's stage 0 (.fusedMbConv 32 48 4 3 2 1 false) and EfficientNetV2's early stages.

  k×k regular conv ic→mid at stride 2  → BN → relu      -- 2h×2h → h×h
  1×1 project mid→oc                   → BN             -- NO activation

"Fused" means the MBConv expand-1×1 and its depthwise collapse into ONE regular k×k conv, so despite living in a mobile net there is nothing depthwise here. No skip: ic ≠ oc and stride 2.

ReLU, as timm's EdgeResidual in mobilenetv4_conv_medium (scripts/parity/mnv4_timm_parity.py). The JAX fused_mbconv_block is shared with EfficientNetV2 (swish) and takes the activation as an argument.

Block-shape dispatch, in one place. Which of the two forwards a row uses is forced by the row: stride 1 ⇒ the identity skip (ic = oc, pinned by mnv4-fwd-smoke); stride 2 ⇒ the post-DW carries it (timm's rule when both depthwise convs exist). The two cannot be one function — .depthwise and .depthwiseStrided differ in INPUT type.

Stem forward: 3×3/s2 conv (3→32), 224→112 → batch BN → relu, on %x. Symmetric (1,1) padding (.convStridedAt), as timm's conv_stem. XLA-SAME padding (.convStridedXlaAt, (0,1) for a 3×3/s2 at 224) also gives 112×112, so only a forward on shared weights sees the difference (scripts/parity/mnv4_timm_parity.py, scripts/parity/mnv4_forward_tie.py).

Head forward, timm's order: 1×1 (256→960) → BN → relu at 7×7 (Conv-M's cn_r1_k1_s1_c960), GAP(7×7), then conv_head 1×1 (960→1280) → norm_head BN → relu on the POOLED [B, 960, 1, 1], then dense. The second BN therefore normalises over the batch alone (N·1·1 cells per channel). Running conv_head at 7×7 before the pool would be a different function with the same parameter count: batch BN and relu do not commute with pooling.

The MobileNetV4-Conv-M forward chain, batch BN, at N := B, 224² → nClasses.

Transcribed 1:1 from the Conv-M table in jax/MainMobilenetV4.lean. Spatial ladder:

  224 --stem s2--> 112 --fused s2--> 56 --uib s2--> 28 --uib s2--> 14 --uib s2--> 7 --GAP--> 1

Block dispatch follows the table: the three stride-2 blocks (1, 3, 11) are ic ≠ oc and strided at the post-DW (timm's dw_mid); the eighteen stride-1 blocks are all ic = oc, hence all skip. The stride/skip split is checked by the types; which depthwise positions a block has (its family) is an if the types do not check. Families in order after the fused stage: ExtraDW ×7, ConvNeXt, FFN, ConvNeXt, ExtraDW ×4, FFN, ConvNeXt, ExtraDW ×2, FFN ×2, ConvNeXt — 13 / 4 / 4 and no IB at all.

Activations, as timm's mobilenetv4_conv_medium:

• stem and head .convBn → relu (MlirCodegen.emitConvBnTrain … useRelu := true)
• the fused stage → relu (timm's EdgeResidual)
• every UIB block → relu after the expand and the post-DW; the pre-DW (dw_start) and the project are BN only (timm's UniversalInvertedResidual)

Returns the full forward RECORD, not just (code, logits): the train step needs every saved activation the backward reads, and the alternative — a second copy of the chain inside the train step — is the two-readings defect this file exists to avoid.

Every distinct channel width a bias-free conv in this net binds %zb{c} at: the stem, the fused stage's two convs, each block's pre-DW (ic), expand and post-DW (mid) and project (oc), and the head. Derived by hand and pinned by mnv4-fwd-smoke, which fails on an unbound %zb.

@mnv4_fwd — the MobileNetV4-Conv-M forward as one MLIR module.

%x plus mnv4SigList's parameters in VLayer.toSpecs order, logits [B, nClasses]. Every conv is bias-free, so the proven conv ops' bias operands bind to the %zb{c} zero constants the prelude declares — same op, bias = 0, and x + 0.0 is exact.

zeroBiasPrelude must cover every width the chain references or the module has an unbound SSA name. That is a link error at parse time rather than a wrong number, which is the good direction, but mnv4-fwd-smoke checks it anyway so the failure arrives at lake build and not at iree-compile.

@mnv4_fwd_eval — the inference forward, every BN site reading frozen running stats. %x + 233 params + 154 stat inputs = 388 inputs (counted off mnv4_fwd_eval.mlir). This is what the driver scores through.

It is mnv4FwdChainB at .eval — the SAME traversal @mnv4_fwd and the train step use, so its BN order matches mnv4StatSigList by construction rather than by a second reading. Its typed graph is mnv4FwdGraphBFullEval at f = s / 32 (MobileNetV4FullBEval).

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/mnv4_<variant>_train_step.mlir, the entry point is @mnv4_<variant>_train_step, and LEAN_MLIR_VARIANT selects it. All three must agree — the shim checks the entry name and refuses a mismatch outright rather than running the wrong graph. B = 32 is deliberately unsuffixed so the Imagenette artifact keeps a stable name.

The variant slug of a recipe render — the JAX reference's recipe renders. opt = none is mnv4AdamVariant, so every committed spelling is unchanged. Markers in the order the driver's predicates read them (VerifiedVariant): ema first (emaOn is a PREFIX test), then the optimizer with its k (accK parses it back out after acc[dp]), the per-replica batch, wx, do, the decay mark, bf16.

MobileNetV4-Conv-M AdamW train step, batch BN, rendered from the verified AST at N := B.

858 inputs (%x, 233 θ, 233 m, 233 v, %lr/%bc1/%bc2, 154 running-stat slots, %onehot) and 856 outputs (233 θ', 233 m', 233 v', %loss/%bc1/%bc2, 154 batch stats) — counted off mnv4_adam_train_step.mlir. Parameter order comes from mnv4ShapeList — through zipPs, which builds each block's gradient list from the very same uibSig slice the signature does — and stat order from mnv4StatShapeList.

Forward, as timm's mobilenetv4_conv_medium: symmetric stem 3×3/s2 (3→32, 224→112) → fused MBConv (32→48, 112→56, ReLU) → the 21 UIB blocks (stride on the post-DW, BN-only pre-DW; ExtraDW, ConvNeXt and FFN — no IB) → 1×1 conv-BN-relu (256→960) → GAP → 1×1 conv_head (960→1280, BN over the batch at 1×1) → dense.

The cotangent is composed from kit ops (softmaxRow → subB → scaleB → addVB → shiftB → divConstB, α = 0.1, K = nClasses), and %loss is report-only and stays outside the AST — the same carve-out resnet34/mobilenetv2 take.