[oxura]

The kernel already prints out of fuel, but the CLI then calls it a TypeScript/kernel mismatch. The notice now says the proofs could not be validated, without claiming the two checkers disagreed. It still appears on every rejection.

This takes #1322's diagnostic/documentation option: WONTFIX now gives the 400,000,000-step conversion budget and the split-equality workaround. No fuel increase or Nat evaluator change.

Checked on Linux x86_64 with the unchanged Lean 4.34.0 kernel: the 3M comparison still exits 1 with its fuel detail and empty stdout; the paired 1.6M equalities pass; #1623 still rejects with expected/observed. The real safe worker still classifies the rejection correctly. Repo gate: 54/54.

Dropped the old stub assertion that pinned the notice's prose; the update-notice/safe-worker test stays. Full ping gate skipped because the site checkout is absent.

Fixes #1322 (the reporting/documentation option). AI-assisted.

[Lorenzobattistela]

Thanks @oxura, but we're closing this one too.

• Running out of fuel stays a MISMATCH, and the notice keeps saying so (fix(verdict): report kernel fuel failures and document limits #1487, fix(cli): distinguish exhausted kernel conversion budget #1552). Bend accepted a proof the kernel didn't confirm, and the notice should say exactly that.
• The WONTFIX entry is the one we declined in fix(cli): distinguish exhausted kernel conversion budget #1552. The existing "checker is not optimal" entry already covers this.
• The change to gates/ping.ts deletes the check that pins this notice. That check is there on purpose, and gate changes aren't something a PR like this can make.
• This doesn't fix --verdict: the kernel runs out of fuel on a closed Nat comparison of literals around 3 000 000 that bend2 checks at once (2.0.34) #1322. The kernel still can't check Nat literals in the millions, and the issue stays open as kernel work.

Please don't open another PR that only changes this message or adds to WONTFIX for #1322. A change to the kernel itself, such as a native path for Nat literals, would be welcome.

[oxura]

Got it — I misread the scope of #1487/#1552. I'll leave the notice, gates and WONTFIX alone and won't resubmit this. #1322 needs a kernel change.