The 161 R50 parameter inputs, in func-arg order: stem (3), the [3,4,6,3] bottleneck stages, then the head. Single source for %p, %pm, %pv and the return order.

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

The 106 running-stat inputs — 53 BN layers × (μ, var), μ and var interleaved per layer, which is how the driver packs runningBnStats off bnChannels.

R50's stochastic-depth site count — one per bottleneck block, [3,4,6,3] = 16.

⚠ It is the count the RAMP's denominator is read against (totalDrop − 1 = 15), so it is a definition rather than a literal 16 sprinkled at three sites.

The %dp0 … %dp15 mask arguments, tensor<Bxf32> each — appended to the train step's signature only under sd. Mirrors cnxDropSig.

some i under sd, none otherwise — the per-block ramp index handed to the six block emitters. ⚠ The index is the BLOCK index and the two coincide here, because every R50 bottleneck drops; EfficientNet's do not (its reference advances the ramp counter inside a skip guard), which is why efficientnetVerified.dropKeeps is a literal array and this is a range. ⚠ At sd := false this is none at every site and NOT ONE pretty call happens, so every committed R50 artifact re-renders byte-identically.

The ResNet-50 forward chain at the BATCHED index — one traversal, consumed by both @resnet50_fwd and the train step that differentiates it.

ResNet-50 [3,4,6,3] bottleneck train step, batch-BN, rendered at N := B.

161 θ / 161 m / 161 v, %lr/%bc1/%bc2, 106 running-stat slots and %onehot in; 161 θ' / 161 m' / 161 v', %loss/%bc1/%bc2 and 106 batch stats out. Parameter ORDER comes from r50SigList, the same single source the signature and the return list use, so the arity/order contract cannot drift within this file — and it is written to agree with VerifiedSpec.bottleneckStageSpec, which is what the DRIVER walks.

⚠ The block sequence is [3,4,6,3] with block 0 of every stage projecting. Stage 1's projects at stride 1 (bnkProjFwdB); stages 2/3/4 project strided.

@resnet50in_fwd — 162 inputs (%x + 161 params), logits [B, nClasses]. Batch-statistic BN, i.e. the same forward the train step differentiates.

⚠⚠ That sentence was FALSE until 2026-08-10 and is now enforced. This built its forward from r50FwdChain .train, which reaches R34's shared bnSite and therefore bnPerChannelF — reduce [2,3], divisor H·W, PER-EXAMPLE — while resnet50TrainStepFaithfulB is bnBatchF, reduce [0,2,3], divisor B·H·W. Two different functions under one net's name (§3d(b)), and regen_verified_mlir.sh check could not see it because it only ever paired a forward with the SGD train step and R50 has none. It now renders from r50FwdChainB — literally the traversal the train step differentiates — so check_adam_prefix holds it as a byte prefix.

⚠ r50FwdChain's .train branch is now UNUSED by R50 and must stay that way; it survives only because .eval shares the function. Rendering a forward from it reopens the split.

@resnet50in_fwd_eval — the inference forward, every BN site reading frozen running stats. 161 params + 106 stat inputs + %x = 268 inputs. This is what the driver scores through, so its BN order must match r50StatSigList, which it does by sharing the chain.