SE forward on c channels at hh×ww, reduce dim r: one fused seBlock, whose text computes the squeeze (GAP), reduce dense (W₁), swish and excite dense (W₂) on the way to the gate. Their SSA names (seBlockSavedNames) are the activations the SE backward reads, so the forward computes the SE once — it is pretty of the typed graph's seBlock node — rather than a second, un-fused copy beside it. Returns (code, s, e1, z, e2, seOut).

Total MBConv blocks = the reference's totalDrop, i.e. the ramp DENOMINATOR is this minus 1.

The block indices (0-based) that carry a drop site, in signature order. This is the single source: enetDropSig maps over it to build the %dp<i> inputs, the traversal passes the same i at each eFwd call site, and the driver reads it to know how many scales to supply and at which ramp index. The two routes fail LOUDLY if they disagree — an entry with no call site leaves an unused input (arity mismatch at the driver), and a call site with no entry emits an undeclared %dp<i> (rejected by the lowerer). Neither is silent.

The number of per-example drop-path scale inputs a stochastic-depth render takes.

The %dp<i>: tensor<Bxf32> inputs, appended to a render's signature when stochastic depth is on. Empty when off.

The classifier's input width — EfficientNet-B0's head channel count, i.e. the GAP output and hence the dropout mask's per-example width. Independent of nClasses.

The %do: tensor<B×1280xf32> input, appended when classifier dropout is on. Empty when off, which is what keeps the inertness gate byte-identical.

It goes after enetDropSig, i.e. dead last in every signature. Two independent reasons, and the second is the one that bites: a parameter inserted mid-list captures an existing positional slot and the driver walks these signatures positionally; and the drop-mask tail is what the DP shim shards by COUNT from the end (n_shard_tail), so a per-example input placed before them would be counted as one of them.

Stride-1 expand MBConv forward body (shared by residual + no-skip): expand 1×1 conv-bn-swish → depthwise(kd) conv-bn-swish → SE → project 1×1 conv-bn. Returns the EFwd WITHOUT the final residual (caller adds the addV for residual blocks).

Residual stride-1 MBConv forward (ic = oc): body + addV skip.

No-skip stride-1 MBConv forward (ic ≠ oc, b9/b16): body, output = project-BN out.

Strided MBConv forward (b2/b4/b6/b12): expand at the input 2hh×2ww, depthwise downsamples 2hh×2ww → hh×ww, project 1×1 at hh×ww. NO skip.

No-expand MBConv forward (b1, t=1): depthwise(kd, on ic channels)-bn-swish → SE → project 1×1 (ic→oc)-bn. NO expand, NO skip. ec/en unused; er = block input (= depthwise input).

Full 262-param EfficientNet-B0 signature, func-arg order: stem(4) + b1 no-exp(12) + b2..b16 expand(15×16) + head(4) + dense(2) = 4+12+240+4+2 = 262 tensors.

Every channel width EfficientNet-B0 uses as a conv bias — stem 32, each block's mid and oc off the [t,c,n,s,k] table, head 1280. One list feeding all four zeroBiasPrelude calls, so a convBias := false render cannot declare the constants in one artifact and not another.

NOT the SE widths. SE's two 1×1 convs are followed by an ACTIVATION, not BN, so nothing absorbs their biases and the reference carries them; they stay real parameters and are never bound to a zero constant. The rule for which biases fold — a rank-1 parameter after a rank-4 kernel — excludes them because SE's params are rank-2.

Stem forward: 3×3/s2 XLA-SAME conv (3→32, 224→112) → BN → swish, on %x.

Head forward up to the GAP: 1×1 conv (320→1280) → BN → swish → GAP(7×7), on block 16's output xName. The classifier dropout and the dense stay in the chain (cd decides the dropout).

@efficientnet_fwd rendered ENTIRELY from the verified AST — 263 inputs (%x plus the 262 params in enetSig order), returning logits [B, nClasses]. Shares enetFwdChain with the train step, so it is a byte-identical PREFIX of efficientnet_train_step.mlir, ending exactly where the loss begins. Replaces the hand-written emitter in tests/TestEfficientNetFwd.lean.

@efficientnet_fwd_eval rendered ENTIRELY from the verified AST — the inference forward, every BN site consuming frozen per-channel running stats (the bnEval descriptor, den = batchMap N bnPerChannelEvalTensor3) instead of reducing statistics out of its activation. Same 262 params in the same order, plus the 98 stat inputs (49 BN layers × μ/var, interleaved per layer in bnChannels order): 361 inputs.

This is the eval partner of efficientnet_adam_train_step, whose returned batch μ/var the driver EMAs into exactly these slots — and both sides of that contract now come off one bns list rather than two independently-written ones.

EfficientNet-B0 (full 16-MBConv) SGD train step rendered ENTIRELY from the verified AST, at the batched index N·(c·h·w). Every emitted line is pretty of a verified SHlo node. Strided stem 3×3/s2 (3→32, 224→112) → b1 (no-expand) → b2..b16 (4 strided downsamples 112→7, 9 residual skips, 2 no-skip widenings) → 1×1 conv-bn-swish head (320→1280) → GAP → dense (1280→nClasses).

The cotangent is plain softmax − onehot with the batch mean folded into lrStr — so the committed lrStr = 0.05 is an effective 1.6 on the mean loss. That is a tuned value, not a slip; the AdamW render below spells the mean explicitly instead.

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/efficientnet_<variant>_train_step.mlir, the entry point is @efficientnet_<variant>_train_step, and LEAN_MLIR_VARIANT selects it.

All three must agree, or the shim refuses the call outright ("entry mismatch") rather than running the wrong graph. Deriving the name here is what stops it drifting from the #eval paths below; the #guards at the bottom pin those literal paths against this function.

B = 32 is deliberately unsuffixed, so the two existing artifacts keep their names and bytes. Same convention as r34AdamVariant.

EfficientNet-B0 AdamW train step rendered from the verified AST. The certified peer of the hand-written tests/TestEfficientNetTrain.lean render that efficientnet-verified-adam has been training on.

Same backward as efficientnet_train_step (enetBackAll, one traversal) but taking the un-fused gradients, each fed to the proven AdamW triple. Two things differ from the SGD render and both are load-bearing:

• the cotangent is label-smoothed (α = 0.1, K = nClasses) with an explicit ÷B, where the SGD render is plain CE with the mean folded into lr. Measured against the hand-written AdamW emitter, this is the same gap ViT had; get it wrong and the tie fails in a way that looks like a bug in the gradient ops.
• it returns the BN running statistics — batch μ/var per BN layer, bnBatchMeanB/ bnBatchVarB recomputed from that layer's BN input — which the host EMAs into @efficientnet_fwd_eval's frozen stats. The SGD render has no such outputs.

Interface: 889 in (%x, 262 θ, 262 m, 262 v, %lr/%bc1/%bc2, 98 running-stat slots, %onehot) / 887 out (262 θ', 262 m', 262 v', %loss/%bc1/%bc2, 98 batch stats) — positionally identical to the hand-written render, so trainAdamSched's packed [θ|m|v] protocol is unchanged.

Unlike ViT's, this tie can pin the forward bit-exactly: EfficientNet has BatchNorm, so the returned batch statistics are a whole-net forward fingerprint no gradient touches.