A single Hadamard-style sumcheck — but the causal-mask verifier is O(log s), not O(s). The lower-triangular mask MLE is evaluated in closed form (eval_zeroifier_mle); only the local sliding-window mask needs an extra sumcheck.

• Correction: our old page said the verifier sweeps the triangular MLE in $O(s)$ via a prefix sum. The code evaluates the lower-triangular (zeroifier) MLE and the row/column less-than polynomials in closed form — the full causal-mask verifier is $O(\log s)$.
• The verifier negates $D_2$'s $-\infty$ contribution first, reducing to a plain Hadamard check against the triangular $D_1$. It slots into single-head attention between the score matmul and the softmax.
• The $O(s)$ cost only appears for the local sliding-window mask (Gemma-style), which needs an extra sumcheck plus an $O(s)$ shift-matrix evaluation. The plain causal mask does not.
• zkGPT's evaluated model has no attention mask at all.

There is no masking PIOP because the mask is a baked constant: future positions carry a large-negative quantized sentinel that flows through the softmax as ≈0. Nothing separate is proven.

• In the traced model the causal mask is applied before quantization (att.masked_fill(bias==0, -10) in models/transformer/gen.py), so by the time the score matrix reaches the prover the upper triangle is already a constant.
• The softmax test layout documents the exact sentinel: upper-triangular entries use -(11 << 12) = -45056 (a $-\infty$ proxy at scale 12). It is just a very small input to the exp lookup, which returns ≈0 — no triangular-MLE argument, no Hadamard correction.
• So Jolt Atlas needs neither DeepProve's prefix-sum triangular trick nor a masking cost line: masking is absorbed into the softmax it already proves.