feat: VER001/VER002 — unenforced effect declarations below enforcement floor (closes #80)#82
Open
marcelofarias wants to merge 2 commits into
Open
feat: VER001/VER002 — unenforced effect declarations below enforcement floor (closes #80)#82marcelofarias wants to merge 2 commits into
marcelofarias wants to merge 2 commits into
Conversation
…forcement floor (?bs < 0.9) 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 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Adds early, non-blocking version-floor warnings (VER001/VER002) to highlight that reads {} / writes {} / throws {} annotations are documentation-only in files pinned below ?bs 0.9, plus updates to the MCP explain surface and diagnostic documentation.
Changes:
- Introduces
passVerCheckto emit VER001 (reads/writes) and VER002 (throws) warnings for?bs < 0.9, and wires it into the compiler pipeline. - Registers VER001/VER002 in compiler error-code registry and adds MCP long-form explanations + MCP known-codes test updates.
- Adds a dedicated compiler test suite for VER001/VER002 and refreshes docs tables (AGENTS/README).
Reviewed changes
Copilot reviewed 8 out of 8 changed files in this pull request and generated 9 comments.
Show a summary per file
| File | Description |
|---|---|
| README.md | Updates advertised MCP explain diagnostic-code coverage list. |
| AGENTS.md | Backfills diagnostic-code reference table with newer codes, including VER001/VER002. |
| packages/compiler/src/transform.ts | Inserts verCheck pass into the compiler pipeline to surface warnings. |
| packages/compiler/src/passes/ver-check.ts | New pass that scans fn headers and emits VER001/VER002 warnings below ?bs 0.9. |
| packages/compiler/src/error-codes.ts | Adds VER001/VER002 entries (rule/idiom/rewrite/example) for bs explain. |
| packages/compiler/tests/ver-check.test.ts | New tests validating warning emission, gating, and empty-clause behavior. |
| packages/mcp/src/explanations.ts | Adds MCP explain content for VER001/VER002. |
| packages/mcp/tests/server.test.ts | Extends MCP known-codes contract test to include VER001/VER002. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| if (atLeast(version.resolved, "0.9")) return { code: src, warnings: [] }; | ||
|
|
||
| const allowGenerics = atLeast(version.resolved, "0.4"); | ||
| const program = parseProgram(src, { allowGenerics, includeNestedFns: false }); |
| 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`, |
Comment on lines
+411
to
+417
| "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", |
Comment on lines
+531
to
+545
| "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.", |
| 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/); |
| | 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. | | ||
| | 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. | |
| | `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 a stable diagnostic code (`BS001`, `BS002`, `CAP001`, `CAP002`, `UNS001`–`UNS004`, `RES001`, `FMT001`, `INT001`, `SYN001`) plus a fails/passes example pair. | | ||
| | `explain` | `{ code: string }` | Long-form explanation for a stable diagnostic code (`BS001`, `BS002`, `CAP001`–`CAP003`, `UNS001`–`UNS004`, `RES001`, `FMT001`, `INT001`–`INT002`, `SYN001`, `EFF002`–`EFF004`, `DEP001`–`DEP002`, `THR001`, `THR003`, `VER001`–`VER002`) plus a fails/passes example pair. | |
Comment on lines
67
to
+69
| "UNS004", | ||
| "VER001", | ||
| "VER002", |
Comment on lines
+20
to
+27
| 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); |
- 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
| | RES001 | (0.3+) `Result.try` / `Result.tryAsync` with no body. | `Result.try { <body that may throw> }`. | | ||
| | 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. | |
| | 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. | | ||
| | 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. | |
Comment on lines
+68
to
+69
| // early so it can see the full, unmodified header. Not run at 0.9+ because | ||
| // the enforcement passes (depCheck, thrCheck) already validate the claims. |
Comment on lines
+56
to
+60
| 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; | ||
|
|
| * 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). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
reads {}orwrites {}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.throws {}(THR001/THR002 enforcement floor).severity: "warning") inTransformResult.warnings, so compilation succeeds.reads {}/throws {}on old pins are likely intentional forward-declaration placeholders.explainrow with all codes added since SYN001 (CAP003, INT002, EFF002–EFF004, DEP001–DEP002, THR001, THR003).Closes #80.
How it works
passVerCheckruns early in the pipeline (before?bs 0.9enforcement passes). It is skipped entirely whenversion.resolved >= "0.9"— at that point DEP001/DEP002/THR001/THR002 actively enforce the claims, so the warning would be redundant. For older pins it scans fn declarations and emits VER001/VER002 for any fn with a non-empty unenforced annotation.Test plan
pnpm -r build && pnpm test— 611/611 pass (15 new tests inver-check.test.ts)reads {}at?bs 0.8→ VER001 warningwrites {}at?bs 0.8→ VER001 warningreads {}andwrites {}→ single VER001 warning with both clausesthrows {}at?bs 0.8→ VER002 warningreads {}at?bs 0.8→ no VER001writes {}/throws {}→ no VER001 / VER002?bs 0.9→ no warnings (enforcement active)bs explain VER001/bs explain VER002returns rule/idiom/rewrite🤖 Generated with Claude Code