fix(verdict): report kernel fuel failures and document limits

WONTFIX.txt

@@ -112,6 +112,16 @@ F32 NaN payload bits are not preserved on the JS lane (#797, #872)
   dependent tag takes the two lanes down two arms, and the arm JS takes may
   duplicate an affine value (#872). The C lane is the reference there too.
 
+The BendTT kernel may exhaust a conversion's fuel (#1193, #1322)
+  Its evaluator unfolds Nat literals in unary and does not share repeated
+  subterms as bend2's checker does. A comparison around 3,000,000 or a
+  deeply shared graph can run out of fuel; combining computations in one
+  equality spends one conversion budget. This is a resource limit, not
+  evidence that the theory disagrees with bend2. --verdict reports the
+  kernel's reason and exits nonzero: the book has not been validated.
+  Keep large constants abstract, or prove smaller computations as separate
+  equality obligations and combine their results with a generic law.
+
 RUNTIME (the theory allows it, the runtime does not run it yet; we remove
 these over time; do not open an issue)
 

bend2/main.ts

@@ -84,11 +84,6 @@ const FAIL = "SOME PROOFS FAIL";
 
 const HINT = "Use --verdict for mathematical validity.";
 
-const MISMATCH = "Sorry - this is a mismatch between the TypeScript implementation,"
-  + " and the formalized BendTT kernel. Your proofs may or may not be correct, and"
-  + " we cannot validate them yet. This will be addressed in a future update."
-  + " Meanwhile, feel free to open an issue to report this bug.";
-
 // BendHub's terms; s18.4 makes MIT-0 the default license
 const TERMS = "https://bend-lang.com/bendai/terms#s18";
 
@@ -775,8 +770,8 @@ async function pow_mine(hash: string, bytes: number): Promise<number> {
 
 // cli_verdict prints the verdict on a book bend2 checked: PASS when no
 // def outside Base relies on unsafe or foreign code and, with the kernel,
-// when BendTT checks every def too; else FAIL and why. A kernel failure is
-// a mismatch: bend2 accepted what the kernel rejects.
+// when BendTT checks every def too; else FAIL and why. Kernel resource
+// limits and out-of-scope elaboration do not establish a theory mismatch.
 function cli_verdict(book: Bend.Book, kernel: boolean): number {
   const bad = book_promises(book);
   if (bad.length !== 0) {
@@ -785,8 +780,9 @@ function cli_verdict(book: Bend.Book, kernel: boolean): number {
       + bad.map((k) => "- " + Bend.name_key(k) + "\n").join(""));
     return 1;
   }
-  if (kernel && !Safe.safe_check(book)) {
-    cli_say(2, FAIL + "\n" + MISMATCH + "\n");
+  const why = kernel ? Safe.safe_check(book) : null;
+  if (why !== null) {
+    cli_say(2, FAIL + "\nBendTT could not validate this book:\n" + why + "\n");
     return 1;
   }
   cli_say(1, PASS + "\n" + (kernel ? "" : HINT + "\n"));

bend2/safe.ts

@@ -1538,14 +1538,19 @@ export function run_read(bin: string, args: string[],
 // the kernel's verdict on a book's text: ok on exit 0 with its exact
 // success line. It checks a copy in a fresh private dir, which no one
 // else can swap, and a kernel reading /dev/stdin got EBADF (1 in 1486)
-function kernel_check(text: string): boolean {
+function kernel_check(text: string): string | null {
   const env = { ...process.env, LEAN_STACK_SIZE_KB: "4194304" };
   const dir = fs.mkdtempSync(path.join(os.tmpdir(), "bendtt-"));
   try {
     const inp = path.join(dir, "in.bendtt");
     fs.writeFileSync(inp, text, { flag: "wx" });
     const [got, out] = run_read(kernel_bin(), [inp], { env });
-    return got.status === 0 && out.trim() === "ALL PROOFS CHECK";
+    const why = out.trim();
+    if (got.status === 0 && why === "ALL PROOFS CHECK") {
+      return null;
+    }
+    return why.replace(/^SOME PROOFS FAIL\n?/, "") || got.error?.message
+      || "kernel ended with " + (got.signal ?? "exit " + got.status);
   } finally {
     fs.rmSync(dir, { recursive: true, force: true });
   }
@@ -1559,9 +1564,12 @@ export function safe_emit(book: Book, out: string): string[] {
   return got.oos.map(([k, why]) => "- " + B.name_key(k) + ": " + why + "\n");
 }
 
-// --verdict: whether every def of a book bend2 checked is in the kernel's
-// scope, and the kernel checks them all
-export function safe_check(book: Book): boolean {
+// --verdict: null only when every def is in scope and the kernel checks
+// them all; otherwise the elaborator's or kernel's reason, not a verdict
+// that mistakes exhausted conversion fuel for a theory disagreement
+export function safe_check(book: Book): string | null {
   const got = safe_book(book);
-  return got.oos.length === 0 && kernel_check(got.text);
+  return got.oos.length === 0 ? kernel_check(got.text)
+    : "out of scope:\n" + got.oos.map(([k, why]) =>
+      "- " + B.name_key(k) + ": " + why).join("\n");
 }