From 635bea3070b82bba7f56f96823109d4a340dfa1f Mon Sep 17 00:00:00 2001 From: oxura Date: Sun, 11 Oct 2026 16:11:02 +0600 Subject: [PATCH 1/2] fix(verdict): report kernel rejection reasons --- WONTFIX.txt | 10 ++++++++++ bend2/main.ts | 14 +++++--------- bend2/safe.ts | 20 ++++++++++++++------ 3 files changed, 29 insertions(+), 15 deletions(-) mode change 100644 => 100755 WONTFIX.txt mode change 100644 => 100755 bend2/safe.ts diff --git a/WONTFIX.txt b/WONTFIX.txt old mode 100644 new mode 100755 index 479defde9..ca56b344d --- a/WONTFIX.txt +++ b/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) diff --git a/bend2/main.ts b/bend2/main.ts index 32cd6c871..18771db7c 100755 --- a/bend2/main.ts +++ b/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 { // 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")); diff --git a/bend2/safe.ts b/bend2/safe.ts old mode 100644 new mode 100755 index 0e0954350..ead3523d1 --- a/bend2/safe.ts +++ b/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"); } From 9d2fa2d82f59417f803e70270d87823f24d069a6 Mon Sep 17 00:00:00 2001 From: oxura Date: Sun, 11 Oct 2026 16:11:59 +0600 Subject: [PATCH 2/2] chore: preserve non-executable source modes --- WONTFIX.txt | 0 bend2/safe.ts | 0 2 files changed, 0 insertions(+), 0 deletions(-) mode change 100755 => 100644 WONTFIX.txt mode change 100755 => 100644 bend2/safe.ts diff --git a/WONTFIX.txt b/WONTFIX.txt old mode 100755 new mode 100644 diff --git a/bend2/safe.ts b/bend2/safe.ts old mode 100755 new mode 100644