The stable softmax-CE seed %g = softmax(%logits) − %onehot, row-wise over [bs, nClasses] logits of type lty (rty the per-row [bs] type). Reads %logits, %onehot, %ninf and %zero; expv names the exponential (the linear kernel's spelling is %exp).

Every PGD kernel's tail, from the input gradient %dx on: the α/0/1 broadcasts, the step and projection — L∞ (sign step, box-clip to x0 ± ε) or L2 (normalised step, rescale into the ε-ball) — then the clip to [0,1], the return and the closing braces. Reads %x, %x0, %dx, %alpha, %eps, %zero and %one. stp, pj1, clA and clB name the step, the L∞ lower clip and the two [0,1] clips (the linear kernel spells them %step, %c1, %c3, %c4).

PGD-step kernel for the linear classifier. forward → softmax-CE input gradient dx = (softmax(xW+b) − onehot)·Wᵀ (the formula of the linear input-VJP, written by hand) → step → project to the eps-ball around x0 → clip to [0,1]. linf := true: L∞ sign-step, box-clip to x0 ± eps. linf := false: L2 step on the per-sample normalised gradient, projection onto the L2 ball of radius eps around x0. Returns the advanced adversarial input x_adv. eps/alpha baked as constants (recompiled per sweep point). Invoked via the generic forwardF32 FFI with onehot+x0 in the params blob and nClasses := d0 (output size) — no new FFI/C shim. The whole PGD step runs on the GPU; the host just iterates.

PGD-step kernel for the 2-hidden-layer MLP (d0→h→h→d1, ReLU). Forward (saving the pre-activations z0,z1) → the input gradient dx = ((g·W₂ᵀ ⊙ relu'(z₁))·W₁ᵀ ⊙ relu'(z₀))·W₀ᵀ, the formula of Proofs.mlpInputGrad written by hand (ReLU masks via compare GT/select, the codegen's idiom) → L∞/L2 step + projection. Returns x_adv.

PGD-step kernel for the verified MNIST CNN (conv 1→32 → relu → conv 32→32 → relu → maxpool 28→14 → flatten → dense 6272→512 → relu → 512→512 → relu → 512→10). Forward (saving every pre-activation + the maxpool input) → softmax-CE seed → the full input-VJP dx, mirroring verified_mlir/cnn_train_step.mlir's backward ops: dot_general adjoints + ReLU masks (compare GT/select), maxpool-back (select_and_scatter, scatter the pooled cotangent to the argmax cells), and the two conv input-VJPs (transpose-o,i + spatial reverse of the kernel, then the same padded conv). The train step stops at dz1 (it only needs weight grads); here we add the final conv1 input-VJP to reach dx over the pixels. Then the L∞ sign-step / L2 projected step + ε-ball project + [0,1] clip. Architecture is fixed; only bs/eps/alpha vary.

PGD-step kernel for the verified CIFAR-10 CNN — the deeper sibling of genCnnPgdStep (conv 3→32 → relu → conv 32→32 → relu → maxpool → conv 32→64 → relu → conv 64→64 → relu → maxpool → flatten(4096) → 512 → 512 → 10). Same recipe — forward (saving every pre-activation + both maxpool inputs) → softmax-CE seed → the full input-VJP dx, mirroring verified_mlir/cifar_train_step.mlir's backward (4 conv input-VJPs, 2 select_and_scatter maxpool-backs, ReLU masks, dense adjoints) + the final conv1 input-VJP the train step omits — then the L∞/L2 step + ε-ball project + [0,1] clip. 3-channel 32×32, bs/eps/alpha vary.