From 588c02566eb709490c98cb0cd8054ff95bacc638 Mon Sep 17 00:00:00 2001 From: Marcelo Farias Date: Fri, 22 May 2026 06:44:07 -0300 Subject: [PATCH 1/3] =?UTF-8?q?feat:=20VER001/VER002=20=E2=80=94=20warn=20?= =?UTF-8?q?when=20effect=20annotations=20are=20below=20their=20enforcement?= =?UTF-8?q?=20floor=20(=3Fbs=20<=200.9)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses issue #80. reads {}/writes {} and throws {} annotations are parsed and accepted at any version, but enforcement only activates at ?bs 0.9 (DEP001/DEP002 for reads/writes, THR001/THR002 for throws). Without a warning, a reviewer reading an annotated fn header reasonably assumes the compiler has verified the claim — it has not below 0.9. VER001 warns when a non-empty reads {} or writes {} clause is declared on a fn in a file pinned below 0.9. VER002 does the same for throws {}. Both are non-blocking warnings so the "annotate now, enforce on upgrade" pattern remains valid. Empty clauses are not flagged — they are likely intentional forward-declaration placeholders and do not create false assurance. Also backfills AGENTS.md diagnostic table and README.md explain row with all codes that merged since SYN001 (CAP003, INT002, EFF002-EFF004, DEP001-DEP002, THR001, THR003) plus the new VER001/VER002. Co-Authored-By: Claude Sonnet 4.6 --- AGENTS.md | 12 +- README.md | 2 +- packages/compiler/src/error-codes.ts | 38 ++++ packages/compiler/src/passes/ver-check.ts | 108 ++++++++++ packages/compiler/src/transform.ts | 6 + packages/compiler/tests/ver-check.test.ts | 233 ++++++++++++++++++++++ packages/mcp/src/explanations.ts | 54 +++++ packages/mcp/tests/server.test.ts | 2 + 8 files changed, 453 insertions(+), 2 deletions(-) create mode 100644 packages/compiler/src/passes/ver-check.ts create mode 100644 packages/compiler/tests/ver-check.test.ts diff --git a/AGENTS.md b/AGENTS.md index ba0d01d..895730e 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -194,8 +194,18 @@ parse the resulting `{ ok: false, diagnostics: [...] }` envelope. | RES001 | (0.3+) `Result.try` / `Result.tryAsync` with no body. | `Result.try { }`. | | INT001 | (0.7+) A fn declares `intent: "pure"` but also has `uses { … }`. (0.8+) Also fires when `intent: "pure"` is combined with `reads { … }` or `writes { … }`. Pure functions may not declare capabilities or resource dependencies. | Either drop the conflicting header clause(s) or change the intent to reflect the actual behaviour. | | SYN001 | Duplicate fn header clause (e.g. two `reads { }` on the same fn, or two `intent:`), or a label inside `reads {}` / `writes {}` that is not a plain identifier. `parseFn` is version-agnostic, so SYN001 fires whenever a duplicate clause is written regardless of the `?bs` pin. | Declare each header clause once; merge label lists rather than repeating the clause; use bare identifiers (not quoted strings) as labels. | -| THR001 | (0.9+) A fn (or a same-file callee, transitively) throws an exception type not declared in the fn's `throws {}`. If `loadUser` calls `fetchRow throws { NetworkError }`, `loadUser` must also declare `throws { NetworkError }`. | Add the missing type(s) to `throws {}` at each level of the call chain. | +| INT002 | (0.8+) A fn declares `intent: "pure"` but its body calls a fn that has `uses { … }` (or is itself `unsafe`). Pure intent is enforced at the body level as well as the header. | Remove the impure callee call, or change the intent. | +| CAP003 | (0.9+, warning) A fn is declared `unsafe "reason" fn name(…)` and also has a `uses { … }` clause. The compiler cannot prove the capability is actually reached — the assertion is programmer-owned. Non-blocking; the fn compiles. | Remove the `uses {}` clause if it is not needed, or document why the assertion is trusted. | +| EFF002 | (0.8+) A callback parameter declares `uses { … }` capabilities beyond what the outer fn declares. A fn that claims `uses { net }` cannot safely accept a callback that also writes to `fs` — the outer declaration would be a lie. | Extend the outer fn's `uses {}` to cover the callback's full capability set, or narrow the callback's annotation. | +| EFF003 | (0.9+) A callback parameter declares `reads { … }` labels not covered by the outer fn's `reads {}`. Same structural rule as EFF002 applied to resource read dependencies. | Add the missing label(s) to the outer fn's `reads {}`, or narrow the callback annotation. | +| EFF004 | (0.9+) A callback parameter declares `writes { … }` labels not covered by the outer fn's `writes {}`. | Add the missing label(s) to the outer fn's `writes {}`, or narrow the callback annotation. | +| DEP001 | (0.9+) A fn's body (or a callee in the same file) reads a resource label not declared in the fn's own `reads {}`. Transitivity is enforced: if `loadUser` calls `fetchRow` which reads `userDb`, `loadUser` must also declare `reads { userDb }`. | Add the missing label(s) to `reads {}`, or remove the undeclared read. | +| DEP002 | (0.9+) Same as DEP001 but for `writes {}` labels. A fn whose callee writes a resource must declare that write in its own header. | Add the missing label(s) to `writes {}`, or remove the undeclared write. | +| THR001 | (0.9+) A fn's body (or a same-file callee) throws an exception type not declared in the fn's `throws {}`. Transitivity is enforced: if `loadUser` calls `fetchRow throws { NetworkError }`, `loadUser` must also declare `throws { NetworkError }`. | Add the missing type(s) to `throws {}`, or add a `match` / `unsafe` to suppress the propagation. | | THR002 | (0.9+) A fn body directly constructs `err(TypeName(...))`, `err(new TypeName(...))`, or `err(TypeName)` where `TypeName` (CapCase) is not declared in the fn's own `throws {}` clause. Producer-side complement to THR001. | Add `TypeName` to the fn's `throws {}`, or change the error construction to use a declared type. | +| THR003 | (0.9+) A callback parameter declares `throws { … }` types not covered by the outer fn's `throws {}`. Same structural rule as THR001 applied to callback parameters. | Add the missing type(s) to the outer fn's `throws {}`, or narrow the callback annotation. | +| VER001 | (warning, < 0.9) A non-empty `reads {}` or `writes {}` clause is declared on a fn in a file pinned below `?bs 0.9`. DEP001/DEP002 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. | +| VER002 | (warning, < 0.9) A non-empty `throws {}` clause is declared on a fn in a file pinned below `?bs 0.9`. THR001/THR002 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. | When you add a new compiler error, allocate the next free code in the same range (`BSnnn` for general parse errors, `CAPnnn` for capability checks, diff --git a/README.md b/README.md index 3914489..15c7b88 100644 --- a/README.md +++ b/README.md @@ -178,7 +178,7 @@ claude mcp add botscript -- npx -y @mbfarias/botscript-mcp | ----------- | -------------------------------------- | --------------------------------------------------------------------------------------------------- | | `primer` | (no args) | The canonical language primer (same text the `?primer` directive emits). | | `transform` | `{ source: string, filename?: string }` | `{ ok: true, code, forms, version }` on success, or `{ ok: false, diagnostics: [...] }` on failure. | -| `explain` | `{ code: string }` | Long-form explanation for any stable diagnostic code (`BS001`, `BS002`, `CAP001`–`CAP003`, `DEP001`, `DEP002`, `EFF002`–`EFF004`, `FMT001`, `INT001`, `INT002`, `RES001`, `SYN001`, `THR001`–`THR003`, `UNS001`–`UNS004`) plus a fails/passes example pair. | +| `explain` | `{ code: string }` | Long-form explanation for any stable diagnostic code (`BS001`, `BS002`, `CAP001`–`CAP003`, `DEP001`, `DEP002`, `EFF002`–`EFF004`, `FMT001`, `INT001`, `INT002`, `RES001`, `SYN001`, `THR001`–`THR003`, `UNS001`–`UNS004`, `VER001`–`VER002`) plus a fails/passes example pair. | A bot's loop becomes deterministic: `transform` → if `ok=false`, read `diagnostics[0].code` → `explain(code)` → apply `rewrite` → `transform` again. diff --git a/packages/compiler/src/error-codes.ts b/packages/compiler/src/error-codes.ts index 38c84ff..5c3764b 100644 --- a/packages/compiler/src/error-codes.ts +++ b/packages/compiler/src/error-codes.ts @@ -412,6 +412,44 @@ const E: Record = { " else ok(s)\n" + "}", }, + VER001: { + code: "VER001", + title: "reads {} / writes {} declared below the ?bs 0.9 enforcement floor — annotation is unenforced", + rule: + "DEP001/DEP002 (reads/writes transitivity) are enforced from `?bs 0.9`; a non-empty `reads {}` or " + + "`writes {}` clause on a file pinned below 0.9 is accepted but not verified — it is documentation only", + idiom: + "annotate now if you intend to enforce later, but know that reviewers reading the header " + + "cannot assume the compiler has checked it; upgrade the pin to `?bs 0.9` to activate enforcement", + rewrite: + "upgrade pin to `?bs 0.9` to activate DEP001/DEP002 enforcement", + example: + "// before — reads {} at ?bs 0.8 is documentation only (VER001 warning)\n" + + "?bs 0.8\n" + + "fn loadUser(id: string) reads { userDb } -> string = id\n\n" + + "// after — enforcement active\n" + + "?bs 0.9\n" + + "fn loadUser(id: string) reads { userDb } -> string = id", + }, + VER002: { + code: "VER002", + title: "throws {} declared below the ?bs 0.9 enforcement floor — annotation is unenforced", + rule: + "THR001/THR002 (throws transitivity and body-construction) are enforced from `?bs 0.9`; a non-empty " + + "`throws {}` clause on a file pinned below 0.9 is accepted but not verified — it is documentation only", + idiom: + "annotate now if you intend to enforce later, but know that reviewers reading the header " + + "cannot assume the compiler has checked it; upgrade the pin to `?bs 0.9` to activate enforcement", + rewrite: + "upgrade pin to `?bs 0.9` to activate THR001/THR002 enforcement", + example: + "// before — throws {} at ?bs 0.8 is documentation only (VER002 warning)\n" + + "?bs 0.8\n" + + "fn loadUser(id: string) throws { NetworkError } -> string = id\n\n" + + "// after — enforcement active\n" + + "?bs 0.9\n" + + "fn loadUser(id: string) throws { NetworkError } -> string = id", + }, }; export function getErrorCode(code: string): ErrorCodeEntry | undefined { diff --git a/packages/compiler/src/passes/ver-check.ts b/packages/compiler/src/passes/ver-check.ts new file mode 100644 index 0000000..ee82853 --- /dev/null +++ b/packages/compiler/src/passes/ver-check.ts @@ -0,0 +1,108 @@ +/** + * Version-floor warning for unenforced effect declarations (?bs < 0.9). + * + * Effect annotations are parsed and accepted at any version, but enforcement + * only kicks in from `?bs 0.9`: + * + * - `reads {}` / `writes {}` + DEP001/DEP002: enforced from `?bs 0.9` + * - `throws {}` + THR001/THR002: enforced from `?bs 0.9` + * + * When a non-empty clause is present on a file pinned below its enforcement + * floor, the compiler accepts it silently — the annotation is documentation, + * not a verified claim. A reviewer reading the header would reasonably assume + * the compiler has verified the transitivity claim; it has not. + * + * VER001 A non-empty `reads {}` or `writes {}` clause is declared on a fn + * whose file is pinned below `?bs 0.9`. DEP001/DEP002 are not + * enforced; the annotation is documentation only. + * + * VER002 A non-empty `throws {}` clause is declared on a fn whose file is + * pinned below `?bs 0.9`. THR001/THR002 are not enforced; the + * annotation is documentation only. + * + * Both VER001 and VER002 are warnings (non-blocking) — the intended pattern + * of "annotate first, then upgrade the pin" is valid. The warning makes the + * lack of enforcement visible so reviewers are not given false assurance. + * + * Only non-empty clauses are flagged. An empty `reads {}` / `throws {}` on + * an old-pin file is likely an intentional forward-declaration placeholder + * and does not create false assurance. + * + * ?bs 0.9+ This pass is not run (enforcement is active, no warning needed). + */ + +import type { Diagnostic } from "../diagnostics.js"; +import { getErrorCode } from "../error-codes.js"; +import { parseProgram } from "../parser/parse.js"; +import { locationOf } from "./_location.js"; +import { atLeast, type VersionInfo } from "./version.js"; + +export interface VerCheckResult { + code: string; + warnings: ReadonlyArray; +} + +export function passVerCheck(src: string, version: VersionInfo): VerCheckResult { + // Enforcement is active at 0.9 — no warning needed. + if (atLeast(version.resolved, "0.9")) return { code: src, warnings: [] }; + + const allowGenerics = atLeast(version.resolved, "0.4"); + const program = parseProgram(src, { allowGenerics, includeNestedFns: false }); + const warnings: Diagnostic[] = []; + + const ver001 = getErrorCode("VER001")!; + const ver002 = getErrorCode("VER002")!; + + for (const { decl } of program.fns) { + const hasUnenforceReads = (decl.reads?.length ?? 0) > 0; + const hasUnenforceWrites = (decl.writes?.length ?? 0) > 0; + const hasUnenforceThrows = (decl.throws?.length ?? 0) > 0; + + if (hasUnenforceReads || hasUnenforceWrites) { + const { line, column } = locationOf(src, decl.fnKeywordStart); + const clauses: string[] = []; + if (hasUnenforceReads) clauses.push(`reads { ${decl.reads!.join(", ")} }`); + if (hasUnenforceWrites) clauses.push(`writes { ${decl.writes!.join(", ")} }`); + const clauseStr = clauses.join(" / "); + + warnings.push({ + code: "VER001", + severity: "warning", + file: null, + line, + column, + start: decl.fnKeywordStart, + end: decl.nameStart + decl.name.length, + message: + `fn '${decl.name}' declares ${clauseStr} at ?bs ${version.resolved} — ` + + `DEP001/DEP002 enforcement requires ?bs 0.9; this annotation is unenforced`, + rule: ver001.rule, + idiom: ver001.idiom, + rewrite: ver001.rewrite, + }); + } + + if (hasUnenforceThrows) { + const { line, column } = locationOf(src, decl.fnKeywordStart); + const throwsStr = `throws { ${decl.throws!.join(", ")} }`; + + warnings.push({ + code: "VER002", + severity: "warning", + file: null, + line, + column, + start: decl.fnKeywordStart, + end: decl.nameStart + decl.name.length, + message: + `fn '${decl.name}' declares ${throwsStr} at ?bs ${version.resolved} — ` + + `THR001/THR002 enforcement requires ?bs 0.9; this annotation is unenforced`, + rule: ver002.rule, + idiom: ver002.idiom, + rewrite: ver002.rewrite, + }); + } + } + + return { code: src, warnings }; +} diff --git a/packages/compiler/src/transform.ts b/packages/compiler/src/transform.ts index c1ead85..c7e8243 100644 --- a/packages/compiler/src/transform.ts +++ b/packages/compiler/src/transform.ts @@ -7,6 +7,7 @@ import { passCapCheck } from "./passes/cap-check.js"; import { passFn } from "./passes/fn.js"; import { passImports } from "./passes/imports.js"; import { passCapAssert } from "./passes/cap-assert.js"; +import { passVerCheck } from "./passes/ver-check.js"; import { passDepCheck } from "./passes/dep-check.js"; import { passThrCheck } from "./passes/thr-check.js"; import { passEffCheck } from "./passes/eff-check.js"; @@ -62,6 +63,11 @@ const PASS_PIPELINE: ReadonlyArray = [ // message "intent says pure but has uses { net }" is seen before the // transitive capability walk, which produces noisier output. { name: "intentCheck", fn: passIntentCheck, minVersion: "0.7" }, + // verCheck: non-blocking warning (VER001/VER002) when reads/writes/throws + // annotations are declared below their enforcement floor (?bs 0.9). Runs + // early so it can see the full, unmodified header. Not run at 0.9+ because + // the enforcement passes (depCheck, thrCheck) already validate the claims. + { name: "verCheck", fn: passVerCheck }, // effCheck: header-level check that the outer fn's capabilities cover the // effect annotations on its callback parameters (EFF002). Runs alongside // intentCheck — both are header consistency checks before the body walk. diff --git a/packages/compiler/tests/ver-check.test.ts b/packages/compiler/tests/ver-check.test.ts new file mode 100644 index 0000000..ccfd151 --- /dev/null +++ b/packages/compiler/tests/ver-check.test.ts @@ -0,0 +1,233 @@ +/** + * Tests for VER001 / VER002: unenforced effect annotations below ?bs 0.9. + * + * Both codes are warnings (non-blocking). Compilation succeeds; warnings are + * returned in TransformResult.warnings. + * + * VER001 reads {} / writes {} present but DEP001/DEP002 is not enforced + * (file pinned below ?bs 0.9). + * VER002 throws {} present but THR001/THR002 is not enforced (file pinned + * below ?bs 0.9). + */ + +import { describe, expect, it } from "vitest"; +import { transform } from "../src/transform.js"; + +// --------------------------------------------------------------------------- +// VER001 — reads / writes unenforced +// --------------------------------------------------------------------------- + +describe("VER001: fires as a warning for reads/writes below 0.9", () => { + it("emits VER001 for non-empty reads at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) reads { db } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001"); + expect(warns).toHaveLength(1); + expect(warns[0]!.severity).toBe("warning"); + expect(warns[0]!.message).toMatch(/loadUser/); + expect(warns[0]!.message).toMatch(/reads \{ db \}/); + expect(warns[0]!.message).toMatch(/0\.8/); + expect(warns[0]!.message).toMatch(/DEP001\/DEP002/); + expect(warns[0]!.message).toMatch(/unenforced/); + }); + + it("emits VER001 for non-empty writes at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn saveUser(id: string) writes { db } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001"); + expect(warns).toHaveLength(1); + expect(warns[0]!.message).toMatch(/writes \{ db \}/); + }); + + it("includes both reads and writes in message when both present", () => { + const src = + "?bs 0.8\n" + + "fn syncUser(id: string) reads { cache } writes { db } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001"); + expect(warns).toHaveLength(1); + expect(warns[0]!.message).toMatch(/reads \{ cache \}/); + expect(warns[0]!.message).toMatch(/writes \{ db \}/); + }); + + it("does not throw — compilation succeeds", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) reads { db } -> string {\n" + + " id\n" + + "}\n"; + expect(() => transform(src)).not.toThrow(); + }); +}); + +// --------------------------------------------------------------------------- +// VER002 — throws unenforced +// --------------------------------------------------------------------------- + +describe("VER002: fires as a warning for throws below 0.9", () => { + it("emits VER002 for non-empty throws at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) throws { NetworkError } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER002"); + expect(warns).toHaveLength(1); + expect(warns[0]!.severity).toBe("warning"); + expect(warns[0]!.message).toMatch(/loadUser/); + expect(warns[0]!.message).toMatch(/throws \{ NetworkError \}/); + expect(warns[0]!.message).toMatch(/0\.8/); + expect(warns[0]!.message).toMatch(/THR001\/THR002/); + expect(warns[0]!.message).toMatch(/unenforced/); + }); + + it("does not throw — compilation succeeds", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) throws { NetworkError } -> string {\n" + + " id\n" + + "}\n"; + expect(() => transform(src)).not.toThrow(); + }); +}); + +// --------------------------------------------------------------------------- +// Both VER001 and VER002 together +// --------------------------------------------------------------------------- + +describe("VER001 + VER002: fires both when fn has reads/writes and throws", () => { + it("emits both warnings for a fn with reads and throws", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) reads { db } throws { NetworkError } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const v1 = result.warnings.filter((w) => w.code === "VER001"); + const v2 = result.warnings.filter((w) => w.code === "VER002"); + expect(v1).toHaveLength(1); + expect(v2).toHaveLength(1); + }); + + it("fires one warning per fn, one fn per code", () => { + const src = + "?bs 0.8\n" + + "fn fnA(x: string) reads { db } -> string {\n" + + " x\n" + + "}\n" + + "fn fnB(x: string) throws { NetworkError } -> string {\n" + + " x\n" + + "}\n"; + const result = transform(src); + const v1 = result.warnings.filter((w) => w.code === "VER001"); + const v2 = result.warnings.filter((w) => w.code === "VER002"); + expect(v1).toHaveLength(1); + expect(v1[0]!.message).toMatch(/fnA/); + expect(v2).toHaveLength(1); + expect(v2[0]!.message).toMatch(/fnB/); + }); +}); + +// --------------------------------------------------------------------------- +// Empty clauses — no false positives +// --------------------------------------------------------------------------- + +describe("VER001 / VER002: empty clauses do not fire", () => { + it("does not warn for empty reads at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) reads {} -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001"); + expect(warns).toHaveLength(0); + }); + + it("does not warn for empty writes at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn saveUser(id: string) writes {} -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001"); + expect(warns).toHaveLength(0); + }); + + it("does not warn for empty throws at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn loadUser(id: string) throws {} -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER002"); + expect(warns).toHaveLength(0); + }); +}); + +// --------------------------------------------------------------------------- +// Version gate — silent at ?bs 0.9+ +// --------------------------------------------------------------------------- + +describe("VER001 / VER002: silent at ?bs 0.9", () => { + it("does not warn for reads at ?bs 0.9 (enforcement is active)", () => { + const src = + "?bs 0.9\n" + + "fn loadUser(id: string) reads { db } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001" || w.code === "VER002"); + expect(warns).toHaveLength(0); + }); + + it("does not warn for throws at ?bs 0.9 (enforcement is active)", () => { + const src = + "?bs 0.9\n" + + "fn loadUser(id: string) throws { NetworkError } -> string {\n" + + " id\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001" || w.code === "VER002"); + expect(warns).toHaveLength(0); + }); +}); + +// --------------------------------------------------------------------------- +// No false positives for fns without effect annotations +// --------------------------------------------------------------------------- + +describe("VER001 / VER002: no false positives", () => { + it("does not warn for plain fn at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn add(a: number, b: number) -> number = pure { a + b }\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001" || w.code === "VER002"); + expect(warns).toHaveLength(0); + }); + + it("does not warn for fn with only uses clause at ?bs 0.8", () => { + const src = + "?bs 0.8\n" + + "fn fetch(url: string) uses { net } -> string {\n" + + " http.get(url)\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001" || w.code === "VER002"); + expect(warns).toHaveLength(0); + }); +}); diff --git a/packages/mcp/src/explanations.ts b/packages/mcp/src/explanations.ts index c1ab83e..7726607 100644 --- a/packages/mcp/src/explanations.ts +++ b/packages/mcp/src/explanations.ts @@ -556,6 +556,60 @@ export const EXPLANATIONS: Readonly> = { ") throws { NetworkError } -> void { handler(items[0]) }\n", }, }, + VER001: { + code: "VER001", + title: "reads {} / writes {} declared below the ?bs 0.9 enforcement floor", + body: + "From `?bs 0.9`, the compiler enforces that `reads {}` / `writes {}` annotations are " + + "transitively consistent across same-file calls (DEP001/DEP002). Below that version, " + + "the annotations are parsed and accepted silently — they are documentation, not verified claims.\n\n" + + "VER001 fires as a **warning** (non-blocking) when a non-empty `reads {}` or `writes {}` " + + "clause is declared on a fn in a file pinned below `?bs 0.9`. A reviewer reading the " + + "header would reasonably assume the compiler has checked the transitivity claim — it has not.\n\n" + + "The most common scenario: a team in mid-upgrade writes `reads { userDb }` annotations " + + "while still on `?bs 0.8`, intending to enforce later. VER001 makes the lack of " + + "enforcement visible so reviewers are not given false assurance.\n\n" + + "**Empty clauses are not flagged.** `reads {}` (no labels) on an old-pin file is likely " + + "an intentional forward-declaration placeholder and does not create false assurance.\n\n" + + "The fix is to upgrade the `?bs` pin to `0.9` (which activates DEP001/DEP002 enforcement) " + + "or to leave the annotation in place knowing it is documentation-only until the upgrade.", + example: { + fails: + "?bs 0.8\n" + + "fn loadUser(id: string) reads { userDb } -> string = id\n", + passes: + "?bs 0.9\n" + + "fn loadUser(id: string) reads { userDb } -> string = id\n", + }, + }, + VER002: { + code: "VER002", + title: "throws {} declared below the ?bs 0.9 enforcement floor", + body: + "From `?bs 0.9`, the compiler enforces that `throws {}` annotations are transitively " + + "consistent across same-file calls (THR001) and that fn bodies do not construct error " + + "types absent from the declaration (THR002). Below that version, the annotations are " + + "parsed and accepted silently — they are documentation, not verified claims.\n\n" + + "VER002 fires as a **warning** (non-blocking) when a non-empty `throws {}` clause is " + + "declared on a fn in a file pinned below `?bs 0.9`. A reviewer reading the header would " + + "reasonably assume the compiler has checked the transitivity claim — it has not.\n\n" + + "The most common scenario: a team writes `throws { NetworkError }` annotations while " + + "still on `?bs 0.8`, intending to enforce at upgrade time. When they finally pin to " + + "`?bs 0.9`, they may discover the entire call graph needs new declarations — a large, " + + "surprising diff. VER002 makes this risk visible before the upgrade.\n\n" + + "**Empty clauses are not flagged.** `throws {}` (no types) on an old-pin file is likely " + + "an intentional forward-declaration placeholder and does not create false assurance.\n\n" + + "The fix is to upgrade the `?bs` pin to `0.9` (which activates THR001/THR002 enforcement) " + + "or to leave the annotation knowing it is documentation-only until the upgrade.", + example: { + fails: + "?bs 0.8\n" + + "fn loadUser(id: string) throws { NetworkError } -> string = id\n", + passes: + "?bs 0.9\n" + + "fn loadUser(id: string) throws { NetworkError } -> string = id\n", + }, + }, }; export const KNOWN_CODES = Object.keys(EXPLANATIONS).sort(); diff --git a/packages/mcp/tests/server.test.ts b/packages/mcp/tests/server.test.ts index 36a8a44..80c470f 100644 --- a/packages/mcp/tests/server.test.ts +++ b/packages/mcp/tests/server.test.ts @@ -67,6 +67,8 @@ describe("botscript-mcp explanations", () => { "UNS002", "UNS003", "UNS004", + "VER001", + "VER002", ]); }); From 8f16d0161a83a9d1db3c36ecfc5c56fbb4a0491b Mon Sep 17 00:00:00 2001 From: Marcelo Farias Date: Fri, 22 May 2026 10:40:23 -0300 Subject: [PATCH 2/3] fix(ver-check): address Copilot review on PR #82 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - includeNestedFns: false → true so nested fn declarations get VER001/VER002 - Drop THR002 references throughout (not yet implemented); VER002 now references THR001 only - Add THR001 to MCP EXPLANATIONS/KNOWN_CODES so `bs explain THR001` works - Add nested fn test cases for VER001/VER002 - 613/613 tests pass # Conflicts: # packages/mcp/src/explanations.ts # packages/mcp/tests/server.test.ts --- AGENTS.md | 2 +- packages/compiler/src/error-codes.ts | 4 +-- packages/compiler/src/passes/ver-check.ts | 10 +++--- packages/compiler/tests/ver-check.test.ts | 38 +++++++++++++++++++++-- packages/mcp/src/explanations.ts | 5 ++- 5 files changed, 46 insertions(+), 13 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 895730e..51e7628 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -205,7 +205,7 @@ parse the resulting `{ ok: false, diagnostics: [...] }` envelope. | THR002 | (0.9+) A fn body directly constructs `err(TypeName(...))`, `err(new TypeName(...))`, or `err(TypeName)` where `TypeName` (CapCase) is not declared in the fn's own `throws {}` clause. Producer-side complement to THR001. | Add `TypeName` to the fn's `throws {}`, or change the error construction to use a declared type. | | THR003 | (0.9+) A callback parameter declares `throws { … }` types not covered by the outer fn's `throws {}`. Same structural rule as THR001 applied to callback parameters. | Add the missing type(s) to the outer fn's `throws {}`, or narrow the callback annotation. | | VER001 | (warning, < 0.9) A non-empty `reads {}` or `writes {}` clause is declared on a fn in a file pinned below `?bs 0.9`. DEP001/DEP002 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. | -| VER002 | (warning, < 0.9) A non-empty `throws {}` clause is declared on a fn in a file pinned below `?bs 0.9`. THR001/THR002 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. | +| VER002 | (warning, < 0.9) A non-empty `throws {}` clause is declared on a fn in a file pinned below `?bs 0.9`. THR001 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. | When you add a new compiler error, allocate the next free code in the same range (`BSnnn` for general parse errors, `CAPnnn` for capability checks, diff --git a/packages/compiler/src/error-codes.ts b/packages/compiler/src/error-codes.ts index 5c3764b..13c5da6 100644 --- a/packages/compiler/src/error-codes.ts +++ b/packages/compiler/src/error-codes.ts @@ -435,13 +435,13 @@ const E: Record = { code: "VER002", title: "throws {} declared below the ?bs 0.9 enforcement floor — annotation is unenforced", rule: - "THR001/THR002 (throws transitivity and body-construction) are enforced from `?bs 0.9`; a non-empty " + + "THR001 (throws transitivity) is enforced from `?bs 0.9`; a non-empty " + "`throws {}` clause on a file pinned below 0.9 is accepted but not verified — it is documentation only", idiom: "annotate now if you intend to enforce later, but know that reviewers reading the header " + "cannot assume the compiler has checked it; upgrade the pin to `?bs 0.9` to activate enforcement", rewrite: - "upgrade pin to `?bs 0.9` to activate THR001/THR002 enforcement", + "upgrade pin to `?bs 0.9` to activate THR001 enforcement", example: "// before — throws {} at ?bs 0.8 is documentation only (VER002 warning)\n" + "?bs 0.8\n" + diff --git a/packages/compiler/src/passes/ver-check.ts b/packages/compiler/src/passes/ver-check.ts index ee82853..0b810ae 100644 --- a/packages/compiler/src/passes/ver-check.ts +++ b/packages/compiler/src/passes/ver-check.ts @@ -5,7 +5,7 @@ * only kicks in from `?bs 0.9`: * * - `reads {}` / `writes {}` + DEP001/DEP002: enforced from `?bs 0.9` - * - `throws {}` + THR001/THR002: enforced from `?bs 0.9` + * - `throws {}` + THR001: enforced from `?bs 0.9` * * When a non-empty clause is present on a file pinned below its enforcement * floor, the compiler accepts it silently — the annotation is documentation, @@ -17,8 +17,8 @@ * enforced; the annotation is documentation only. * * VER002 A non-empty `throws {}` clause is declared on a fn whose file is - * pinned below `?bs 0.9`. THR001/THR002 are not enforced; the - * annotation is documentation only. + * pinned below `?bs 0.9`. THR001 is not enforced; the annotation + * is documentation only. * * Both VER001 and VER002 are warnings (non-blocking) — the intended pattern * of "annotate first, then upgrade the pin" is valid. The warning makes the @@ -47,7 +47,7 @@ export function passVerCheck(src: string, version: VersionInfo): VerCheckResult if (atLeast(version.resolved, "0.9")) return { code: src, warnings: [] }; const allowGenerics = atLeast(version.resolved, "0.4"); - const program = parseProgram(src, { allowGenerics, includeNestedFns: false }); + const program = parseProgram(src, { allowGenerics, includeNestedFns: true }); const warnings: Diagnostic[] = []; const ver001 = getErrorCode("VER001")!; @@ -96,7 +96,7 @@ export function passVerCheck(src: string, version: VersionInfo): VerCheckResult end: decl.nameStart + decl.name.length, message: `fn '${decl.name}' declares ${throwsStr} at ?bs ${version.resolved} — ` + - `THR001/THR002 enforcement requires ?bs 0.9; this annotation is unenforced`, + `THR001 enforcement requires ?bs 0.9; this annotation is unenforced`, rule: ver002.rule, idiom: ver002.idiom, rewrite: ver002.rewrite, diff --git a/packages/compiler/tests/ver-check.test.ts b/packages/compiler/tests/ver-check.test.ts index ccfd151..d61a75e 100644 --- a/packages/compiler/tests/ver-check.test.ts +++ b/packages/compiler/tests/ver-check.test.ts @@ -6,7 +6,7 @@ * * VER001 reads {} / writes {} present but DEP001/DEP002 is not enforced * (file pinned below ?bs 0.9). - * VER002 throws {} present but THR001/THR002 is not enforced (file pinned + * VER002 throws {} present but THR001 is not enforced (file pinned * below ?bs 0.9). */ @@ -88,7 +88,7 @@ describe("VER002: fires as a warning for throws below 0.9", () => { expect(warns[0]!.message).toMatch(/loadUser/); expect(warns[0]!.message).toMatch(/throws \{ NetworkError \}/); expect(warns[0]!.message).toMatch(/0\.8/); - expect(warns[0]!.message).toMatch(/THR001\/THR002/); + expect(warns[0]!.message).toMatch(/THR001/); expect(warns[0]!.message).toMatch(/unenforced/); }); @@ -206,6 +206,40 @@ describe("VER001 / VER002: silent at ?bs 0.9", () => { }); }); +// --------------------------------------------------------------------------- +// Nested fn declarations +// --------------------------------------------------------------------------- + +describe("VER001 / VER002: warns on nested fn declarations", () => { + it("emits VER001 for nested fn with reads below 0.9", () => { + const src = + "?bs 0.8\n" + + "fn outer(id: string) -> string {\n" + + " fn inner(x: string) reads { db } -> string { x }\n" + + " inner(id)\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER001"); + expect(warns).toHaveLength(1); + expect(warns[0]!.message).toMatch(/inner/); + expect(warns[0]!.message).toMatch(/reads \{ db \}/); + }); + + it("emits VER002 for nested fn with throws below 0.9", () => { + const src = + "?bs 0.8\n" + + "fn outer(id: string) -> string {\n" + + " fn inner(x: string) throws { NetworkError } -> string { x }\n" + + " inner(id)\n" + + "}\n"; + const result = transform(src); + const warns = result.warnings.filter((w) => w.code === "VER002"); + expect(warns).toHaveLength(1); + expect(warns[0]!.message).toMatch(/inner/); + expect(warns[0]!.message).toMatch(/throws \{ NetworkError \}/); + }); +}); + // --------------------------------------------------------------------------- // No false positives for fns without effect annotations // --------------------------------------------------------------------------- diff --git a/packages/mcp/src/explanations.ts b/packages/mcp/src/explanations.ts index 7726607..fbef3b5 100644 --- a/packages/mcp/src/explanations.ts +++ b/packages/mcp/src/explanations.ts @@ -587,8 +587,7 @@ export const EXPLANATIONS: Readonly> = { title: "throws {} declared below the ?bs 0.9 enforcement floor", body: "From `?bs 0.9`, the compiler enforces that `throws {}` annotations are transitively " + - "consistent across same-file calls (THR001) and that fn bodies do not construct error " + - "types absent from the declaration (THR002). Below that version, the annotations are " + + "consistent across same-file calls (THR001). Below that version, the annotations are " + "parsed and accepted silently — they are documentation, not verified claims.\n\n" + "VER002 fires as a **warning** (non-blocking) when a non-empty `throws {}` clause is " + "declared on a fn in a file pinned below `?bs 0.9`. A reviewer reading the header would " + @@ -599,7 +598,7 @@ export const EXPLANATIONS: Readonly> = { "surprising diff. VER002 makes this risk visible before the upgrade.\n\n" + "**Empty clauses are not flagged.** `throws {}` (no types) on an old-pin file is likely " + "an intentional forward-declaration placeholder and does not create false assurance.\n\n" + - "The fix is to upgrade the `?bs` pin to `0.9` (which activates THR001/THR002 enforcement) " + + "The fix is to upgrade the `?bs` pin to `0.9` (which activates THR001 enforcement) " + "or to leave the annotation knowing it is documentation-only until the upgrade.", example: { fails: From 0b1cce1d5fb690dab45ff9305e5d86a4a3553cfb Mon Sep 17 00:00:00 2001 From: Marcelo Farias Date: Fri, 22 May 2026 14:44:05 -0300 Subject: [PATCH 3/3] fix: rename hasUnenforce* to hasUnenforced*, clarify no-op comments, fix INT002/EFF002 version floors in AGENTS.md --- AGENTS.md | 4 ++-- packages/compiler/src/passes/ver-check.ts | 16 ++++++++-------- packages/compiler/src/transform.ts | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 51e7628..9904157 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -194,9 +194,9 @@ parse the resulting `{ ok: false, diagnostics: [...] }` envelope. | RES001 | (0.3+) `Result.try` / `Result.tryAsync` with no body. | `Result.try { }`. | | INT001 | (0.7+) A fn declares `intent: "pure"` but also has `uses { … }`. (0.8+) Also fires when `intent: "pure"` is combined with `reads { … }` or `writes { … }`. Pure functions may not declare capabilities or resource dependencies. | Either drop the conflicting header clause(s) or change the intent to reflect the actual behaviour. | | SYN001 | Duplicate fn header clause (e.g. two `reads { }` on the same fn, or two `intent:`), or a label inside `reads {}` / `writes {}` that is not a plain identifier. `parseFn` is version-agnostic, so SYN001 fires whenever a duplicate clause is written regardless of the `?bs` pin. | Declare each header clause once; merge label lists rather than repeating the clause; use bare identifiers (not quoted strings) as labels. | -| INT002 | (0.8+) A fn declares `intent: "pure"` but its body calls a fn that has `uses { … }` (or is itself `unsafe`). Pure intent is enforced at the body level as well as the header. | Remove the impure callee call, or change the intent. | +| INT002 | (0.7+) A fn declares `intent: "pure"` but its body directly references a stdlib capability (e.g. `http.get`, `fs.read`). Pure intent is enforced at the body level as well as the header. | Remove the stdlib call from the body, or change the intent. | | CAP003 | (0.9+, warning) A fn is declared `unsafe "reason" fn name(…)` and also has a `uses { … }` clause. The compiler cannot prove the capability is actually reached — the assertion is programmer-owned. Non-blocking; the fn compiles. | Remove the `uses {}` clause if it is not needed, or document why the assertion is trusted. | -| EFF002 | (0.8+) A callback parameter declares `uses { … }` capabilities beyond what the outer fn declares. A fn that claims `uses { net }` cannot safely accept a callback that also writes to `fs` — the outer declaration would be a lie. | Extend the outer fn's `uses {}` to cover the callback's full capability set, or narrow the callback's annotation. | +| EFF002 | (0.7+) A callback parameter declares `uses { … }` capabilities beyond what the outer fn declares. A fn that claims `uses { net }` cannot safely accept a callback that also writes to `fs` — the outer declaration would be a lie. | Extend the outer fn's `uses {}` to cover the callback's full capability set, or narrow the callback's annotation. | | EFF003 | (0.9+) A callback parameter declares `reads { … }` labels not covered by the outer fn's `reads {}`. Same structural rule as EFF002 applied to resource read dependencies. | Add the missing label(s) to the outer fn's `reads {}`, or narrow the callback annotation. | | EFF004 | (0.9+) A callback parameter declares `writes { … }` labels not covered by the outer fn's `writes {}`. | Add the missing label(s) to the outer fn's `writes {}`, or narrow the callback annotation. | | DEP001 | (0.9+) A fn's body (or a callee in the same file) reads a resource label not declared in the fn's own `reads {}`. Transitivity is enforced: if `loadUser` calls `fetchRow` which reads `userDb`, `loadUser` must also declare `reads { userDb }`. | Add the missing label(s) to `reads {}`, or remove the undeclared read. | diff --git a/packages/compiler/src/passes/ver-check.ts b/packages/compiler/src/passes/ver-check.ts index 0b810ae..cd1e83e 100644 --- a/packages/compiler/src/passes/ver-check.ts +++ b/packages/compiler/src/passes/ver-check.ts @@ -28,7 +28,7 @@ * an old-pin file is likely an intentional forward-declaration placeholder * and does not create false assurance. * - * ?bs 0.9+ This pass is not run (enforcement is active, no warning needed). + * ?bs 0.9+ This pass is a no-op (enforcement is active, no warning needed). */ import type { Diagnostic } from "../diagnostics.js"; @@ -54,15 +54,15 @@ export function passVerCheck(src: string, version: VersionInfo): VerCheckResult const ver002 = getErrorCode("VER002")!; for (const { decl } of program.fns) { - const hasUnenforceReads = (decl.reads?.length ?? 0) > 0; - const hasUnenforceWrites = (decl.writes?.length ?? 0) > 0; - const hasUnenforceThrows = (decl.throws?.length ?? 0) > 0; + const hasUnenforcedReads = (decl.reads?.length ?? 0) > 0; + const hasUnenforcedWrites = (decl.writes?.length ?? 0) > 0; + const hasUnenforcedThrows = (decl.throws?.length ?? 0) > 0; - if (hasUnenforceReads || hasUnenforceWrites) { + if (hasUnenforcedReads || hasUnenforcedWrites) { const { line, column } = locationOf(src, decl.fnKeywordStart); const clauses: string[] = []; - if (hasUnenforceReads) clauses.push(`reads { ${decl.reads!.join(", ")} }`); - if (hasUnenforceWrites) clauses.push(`writes { ${decl.writes!.join(", ")} }`); + if (hasUnenforcedReads) clauses.push(`reads { ${decl.reads!.join(", ")} }`); + if (hasUnenforcedWrites) clauses.push(`writes { ${decl.writes!.join(", ")} }`); const clauseStr = clauses.join(" / "); warnings.push({ @@ -82,7 +82,7 @@ export function passVerCheck(src: string, version: VersionInfo): VerCheckResult }); } - if (hasUnenforceThrows) { + if (hasUnenforcedThrows) { const { line, column } = locationOf(src, decl.fnKeywordStart); const throwsStr = `throws { ${decl.throws!.join(", ")} }`; diff --git a/packages/compiler/src/transform.ts b/packages/compiler/src/transform.ts index c7e8243..d48d7bb 100644 --- a/packages/compiler/src/transform.ts +++ b/packages/compiler/src/transform.ts @@ -65,7 +65,7 @@ const PASS_PIPELINE: ReadonlyArray = [ { name: "intentCheck", fn: passIntentCheck, minVersion: "0.7" }, // verCheck: non-blocking warning (VER001/VER002) when reads/writes/throws // annotations are declared below their enforcement floor (?bs 0.9). Runs - // early so it can see the full, unmodified header. Not run at 0.9+ because + // early so it can see the full, unmodified header. No-op at 0.9+ because // the enforcement passes (depCheck, thrCheck) already validate the claims. { name: "verCheck", fn: passVerCheck }, // effCheck: header-level check that the outer fn's capabilities cover the