fix(verifier,codegen): obligate + guard @Int->@Nat narrowing at function return position (#758) - #983
Merged
Merged
Conversation
…ion return position (#758) A `@Int` value narrowing into a `@Nat` return slot was neither statically obligated nor runtime-guarded: `fn to_nat(@int -> @nat) { @Int.0 }` verified clean at Tier 1, yet `to_nat(0 - 5)` returned -5 through the `@Nat` slot with no trap. The narrowing walker obligated every binding site (let, call-arg, constructor-field, match-bind, destructure — #552/#747) but never the function's own return slot, and codegen emitted no return coercion guard, so `vera verify`-clean was not a "no negative @nat" guarantee at the return. Verifier: a new step-7d block emits the `nat_bind` `result >= 0` obligation at the return slot — the dual of #813's 7c `@Nat -> @Int` widen-return — reusing the existing `_check_nat_binding_obligation`. Detection descends if/match joins to their leaf return expressions (`_return_narrows_into_nat`): the whole target-typed body reads as `@Nat` in the checker's side-table, masking a narrowing `_` arm, so the per-leaf check restores parity with codegen. The obligation folds in the body's path conditions via `check_valid`, so an `if @Int.0 >= 0 then @Int.0 else 0 - @Int.0` tail (and `examples/absolute_value.vera`) proves at Tier 1; an unconstrained narrowing is a loud E503; an opaque one (`array_length(...)` over a let-bound array) is an honest Tier-3. Refined-over-@nat returns stay on 7b (`>= 0 && P`), so 7d gates on the bare @nat primitive (R9 disjointness). Codegen: a mirroring return narrow guard (`_emit_nat_bind_guard`) so an unverified compile traps rather than returning a reinterpreted negative. It is excluded when the body is intrinsically @nat by value (`_result_is_nat`), which keeps a genuine `@Nat -> @Nat` tail call (`count_down(@Nat.0 - 1)`) from looking like a narrowing and reverting its `return_call` (TCO). Codegen's `_result_is_nat` gains a declared-return-type fallback so it resolves a user `@Nat` return without the checker side-table (mirroring the verifier's `env.lookup_function` path), matching the site set the verifier obligates. The two sides are pinned by a return-position verifier<->codegen differential (`tests/test_nat_narrowing_return_differential.py`) — mutation-validated: removing the verifier obligation flips the differential + Tier-1/E503 tests RED; removing the codegen guard flips the differential + runtime-trap/WAT tests RED. Conformance program `ch04_nat_return_obligation.vera` (run-level, 150th) proves the absolute-value/requires/match-arm shapes at Tier 1 and runs. Corpus tier deltas (all new return obligations, none verify-RED): +1 Tier-1 each on `absolute_value.vera`, `ch03_slot_result.vera`, `ch04_nat_subtraction.vera`, `ch06_ensures.vera` (provable narrowings); +1 Tier-3 on `nested_closures.vera` (`three_d_count` returns `array_length(...)`, an opaque @int narrowing, honest runtime-guarded). Example corpus 281/97/378 -> 282/98/380. Refs #758 Co-Authored-By: Claude <noreply@anthropic.invalid>
… review) The examples-corpus tier pin and the differential oracle's _cold_verify helper called verify() without resolved modules (and without the #747 semantic-type side-tables), so modules.vera's two imported-function obligations read Tier-3 in-process while vera verify proves them Tier-1 — the pins measured a pipeline no user runs, and the divergence had produced contradictory corpus figures across review rounds (281/97 in-process vs 283/95 by CLI, pre-#758). Both loops now resolve imports and thread the artifacts exactly as cmd_verify does; the pin moves to the CLI-true 284/96/380 and TESTING.md's contract row to 284 of 380 (74.7%). Skip-changelog: test-measurement fidelity within this PR, no compiler change Co-Authored-By: Claude <noreply@anthropic.invalid>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## release/v0.1.4 #983 +/- ##
===============================================
Coverage 93.42% 93.42%
===============================================
Files 96 96
Lines 31408 31457 +49
Branches 456 456
===============================================
+ Hits 29342 29388 +46
- Misses 2053 2056 +3
Partials 13 13
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
📝 WalkthroughWalkthroughThe verifier now creates return-position ChangesNat return narrowing soundness
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant FunctionBody
participant Verifier
participant Codegen
participant Wasmtime
FunctionBody->>Verifier: inspect `@Int` result returned as `@Nat`
Verifier->>Verifier: create and discharge nat_bind obligation
Verifier-->>Codegen: retain return narrowing status
Codegen->>Wasmtime: emit result >= 0 guard
Wasmtime-->>FunctionBody: return value or trap
Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 8✅ Passed checks (8 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@TESTING.md`:
- Line 110: Update the test_codegen_nat_guards.py inventory row in TESTING.md to
include `@Int` -> `@Nat` function-return guard coverage, matching the implementation
and dedicated differential test near line 89.
In `@tests/test_codegen_nat_guards.py`:
- Around line 1087-1101: Update test_guard_emitted_in_wat_for_return_narrowing
to locate the exact $to_nat function symbol using a boundary-safe trailing
delimiter or the file’s existing regex-based WAT lookup pattern, preventing
matches on names such as to_nat$...; keep the subsequent body extraction and
guard assertions unchanged.
- Around line 1074-1081: Update test_negative_return_narrowing_traps_at_runtime
to expect the project’s normalized WasmTrapError from execute(), replacing the
raw wasmtime.WasmtimeError, wasmtime.Trap, and RuntimeError tuple while
preserving the same to_nat(-5) invocation.
In `@tests/test_nat_narrowing_return_differential.py`:
- Around line 63-87: Update the _run helper to catch the execute() contract’s
WasmTrapError directly instead of WasmtimeError, Trap, or RuntimeError. Import
WasmTrapError from its defining module if needed, and return None only for that
exception so unexpected RuntimeError failures propagate.
In `@vera/codegen/functions.py`:
- Around line 631-638: Update the `narrow_guarded` condition in the return-body
emission logic to check the resolved base type rather than the raw
`decl.return_type` slot name, so aliases such as `Count = Nat` are recognized;
reuse `ctx._result_is_nat` or the existing type-resolution helper while
preserving the refinement-type exclusion and guard conditions.
In `@vera/README.md`:
- Line 735: Update the verification-gaps table row in README.md to separate
static obligations from runtime guards: state that all narrowing binding sites
and function returns are statically obligated, but do not claim every binding
site is codegen-guarded; explicitly retain that effect-operation arguments and
generic-instantiated constructor fields lack runtime guards.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: eaac00ae-0eb5-49d1-b0cd-38474fdcb031
⛔ Files ignored due to path filters (6)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**tests/conformance/ch04_nat_return_obligation.verais excluded by!**/*.vera
📒 Files selected for processing (19)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdROADMAP.mdSKILL.mdTESTING.mdspec/06-contracts.mdspec/11-compilation.mdtests/conformance/manifest.jsontests/test_codegen_nat_guards.pytests/test_nat_narrowing_return_differential.pytests/test_verifier_adt_decreases.pytests/test_verifier_nat_obligations.pyvera/README.mdvera/codegen/functions.pyvera/verifier.pyvera/wasm/operators.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
💤 Files with no reviewable changes (1)
- SKILL.md
Greptile SummaryThis PR closes the
Confidence Score: 5/5Safe to merge — fixes a confirmed soundness gap with test-enforced lockstep between the verifier obligation and the codegen runtime guard. Both sides of the fix are implemented in precise lockstep: the verifier's new 7d step and the codegen's per-leaf guard cover identical tree shapes, enforced by a differential test that fails if they desync. Per-leaf guard correctly preserves TCO (verified by a 200k-depth regression). No pre-existing passing behavior is regressed. No files require special attention — all core implementation files are well-covered by the new differential and unit tests.
|
| Filename | Overview |
|---|---|
| vera/verifier.py | Adds step-7d: emits nat_bind return obligation for @Int -> @Nat narrowing functions via new _return_narrows_into_nat leaf descent. Correctly gates on bare @nat (not refined), and the obligation folds path conditions so provable joins (abs-value) discharge at Tier 1. |
| vera/codegen/functions.py | Per-leaf narrowing guard for @int->@nat return: collects nat_leaf_ids pre-translation and subtracts them from tail_sites, so TCO is preserved for non-narrowing @Nat->@nat recursive calls. Also fixes the widen guard alias-blindness (_resolve_base_type_name replaces raw _type_expr_to_slot_name). |
| vera/wasm/operators.py | Adds _collect_narrowing_return_leaves / _collect_narrowing_return_leaves_into / _guard_nat_return_leaf. Extends _result_is_nat with a no-side-table fallback using _fn_ret_type_exprs for callee @nat detection without the checker's resolved-type table. |
| vera/wasm/context.py | Adds _nat_return_leaf_ids: set[int] to WasmContext, initialized empty per-function by _compile_fn. Applies _guard_nat_return_leaf at the trailing expr of every block, covering both top-level body and if-branch trailing expressions. |
| vera/wasm/data.py | Applies _guard_nat_return_leaf at both match arm body emit sites. Block arm bodies correctly no-op because their leaf is guarded in translate_block; bare-expr arm bodies are guarded here. |
| tests/test_nat_narrowing_return_differential.py | New differential test covering UNPROVEN/PROVEN/TIER-3 quadrants, threading the full CLI pipeline. |
| tests/test_codegen_nat_guards.py | Three new test classes for return guard, alias handling, and per-leaf TCO. All wasmtime exception references updated to WasmTrapError. |
| tests/test_verifier_nat_obligations.py | New TestNatReturnObligation758 with 8 test cases covering E503, Tier-1, and Tier-3 shapes. |
| tests/test_obligations.py | Fidelity fix: _cold_verify threads expr_types/expr_target_types to verify(), matching the real CLI pipeline. |
| tests/test_verifier_adt_decreases.py | Tier-count pin updated 283/95/378 -> 284/96/380 with import resolution and artifact threading for CLI parity. |
Reviews (3): Last reviewed commit: "review(983): WasmTrapError catches, boun..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
tests/test_verifier_adt_decreases.py (1)
346-346: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winStale summary header — doesn't match the final assertions in the same test.
The docstring header says
282 T1 / 98 T3 / 380 total (current), but the assertions this test actually enforces (Lines 572-574) aret1 == 284,t3 == 96,total == 380. Tracing the trajectory notes below:282/98/380is the intermediate figure before the "Method correction" step (which moves 2modules.veraobligations from Tier-3 to Tier-1, landing at284/96/380). The header wasn't updated to reflect that final correction, even though it's labelled "(current)".This also matches the PR's own stated corpus pin ("284 Tier-1, 96 Tier-3, and 380 total"), so the header is simply the odd one out.
📝 Proposed fix
- """All examples together: 282 T1 / 98 T3 / 380 total (current). + """All examples together: 284 T1 / 96 T3 / 380 total (current).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_verifier_adt_decreases.py` at line 346, Update the summary docstring in the test to state 284 T1 / 96 T3 / 380 total (current), matching the final assertions and corrected corpus totals.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@TESTING.md`:
- Line 17: Synchronize the contract-verification figures in TESTING.md: update
the later coverage table to match the CLI-true totals of 284 Tier-1 obligations,
96 Tier-3 obligations, and 380 total, preserving the corresponding percentage
and ensuring all related documentation entries are consistent.
---
Outside diff comments:
In `@tests/test_verifier_adt_decreases.py`:
- Line 346: Update the summary docstring in the test to state 284 T1 / 96 T3 /
380 total (current), matching the final assertions and corrected corpus totals.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: a6dbdced-512c-44ea-b6c4-462e2491be12
📒 Files selected for processing (3)
TESTING.mdtests/test_obligations.pytests/test_verifier_adt_decreases.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
… differential quadrants, #984 rows The #983 review round on PR #758's @int->@nat return-narrowing fix: - CRITICAL: the codegen return gates now resolve type aliases (via ctx._resolve_base_type_name, the resolver the let-site guard already uses) so a `type Count = Nat` return is narrow-guarded and a `type MyInt = Int` return with a @nat body is widen-guarded — matching the verifier's alias-resolving 7d/7c gates. Pre-fix the raw slot name masked the alias, so verify obligated the coercion while codegen emitted no guard and run(-5) returned -5 silently. An alias-to-refinement (`type Pos = { @nat | ... }`) is excluded from the narrow gate via _refinement_guard_parts so it keeps its single 7b refinement-boundary guard, not a double guard. - MAJOR (TCO): the @int->@nat narrow guard is now emitted PER NARROWING LEAF during body translation (mirroring the verifier 7d leaf descent) instead of wrapping the whole body. The whole-body wrap reverted every return_call, so a mixed-arm recursion `drain(@int -> @nat) { if @Int.0 == 0 then @Int.0 else drain(@Int.0 - 1) }` lost TCO and stack-exhausted at ~35k depth; per-leaf emission leaves the non-narrowing @Nat->@nat recursive return_call intact and drain(200000) runs constant-stack. A narrowing-leaf that is itself a tail call is excluded from tail_sites so it lowers to a plain call the inline guard can follow. - Differential: fidelity fix (thread file= + resolved_modules= through the verify side, matching the _run sibling) plus the tier3 quadrant (opaque float_to_int, verify + compile in one run), let_before_tail / nested_if_join join shapes, and a type-alias case. - #984 (closure @int->@nat return narrowing, not fixed here) documented in KNOWN_ISSUES.md + SKILL.md with a verified workaround (named where-helper or let @nat binding inside the closure). - Docs: tier-count header (284 T1 / 96 T3), absolute_value else-arm citation (-@Int.0), PR #983 review tags, the no-side-table fallback caveat, and the README/TESTING/ROADMAP counts (7,058 tests, 150 conformance). Refs #758 #984 Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Adversarial review panel + pr-review — recordFour panel lenses (false-Tier-1 hunt, TCO/emission, corpus differential, shape-gap matrix — 18 agents, 2 skeptics per finding) plus three review agents. This round earned its cost: the fix was correct for literally-written types, and three real defects lived exactly one step outside every instrument that had validated it. All fixed in 4659347. Confirmed findings (3) — fixed
Refuted by skeptics (4): an pr-review findings — fixed
Measurement fidelity (carried in this PR): the corpus tier pins and the differential oracle previously measured an artifact-less, resolver-less pipeline no user runs — the source of contradictory corpus figures across three earlier review rounds (281/97 in-process vs 283/95 by CLI). Both now mirror |
…cision (CodeRabbit round) Sixteen raw wasmtime-tuple trap catches across the nat-guard and differential tests now assert WasmTrapError (execute() normalizes traps; a stray RuntimeError could read as the expected trap); the to_nat WAT lookup is delimiter-terminated; vera/README's narrowing row no longer overclaims guard coverage (closure returns are #984); TESTING's contract-verification metric table and the nat-guards row match the CLI-true 284/96/380 and the return-guard coverage. Skip-changelog: test/doc precision within this PR's review round Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (4)
tests/test_codegen_nat_guards.py (2)
1103-1108: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAssert that the proven path still emits its dead guard.
This test only checks outputs, so it remains green if codegen removes the return guard entirely. Inspect
_fn_body(result.wat, "f")for bothi64.lt_sandunreachablebefore the runtime assertions.Based on the PR objectives, proven return narrowings must retain the matching per-leaf runtime guard.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_codegen_nat_guards.py` around lines 1103 - 1108, The test does not verify that the proven return narrowing retains its dead runtime guard. In test_provable_abs_return_does_not_trap, inspect _fn_body(result.wat, "f") from the generated output and assert it contains both i64.lt_s and unreachable before the existing runtime assertions, while preserving the checks for -5 and 7.
1052-1154: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAdd a match-shaped return fixture.
The new tests cover bare,
if, builtin, and alias returns, but nomatchwhose arms narrow into@Nat. A regression affecting one match leaf could therefore escape these tests. Add asymmetric arms and execute both negative and non-negative cases.As per path instructions, tests for new compiler features must cover relevant edge cases.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_codegen_nat_guards.py` around lines 1052 - 1154, The return-guard tests lack coverage for match expressions with arms narrowing into `@Nat`. Add a match-shaped fixture alongside TestNatReturnRuntimeGuard758 with asymmetric arms, then execute inputs selecting both a negative arm (asserting WasmTrapError) and a non-negative arm (asserting the returned value), ensuring the `@Int-to-`@Nat return guard is applied across every match leaf.Source: Path instructions
tests/test_nat_narrowing_return_differential.py (2)
252-274: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winExercise the tier-3 guard at runtime.
This test verifies only the
tier3status and WAT tokens. A misplaced or dead guard would still pass. Execute the opaquefloat_to_intfixture with a negative witness and a safe witness, asserting that only the negative case traps.As per path instructions, codegen/runtime tests should cover runtime edge cases, not only generated WAT.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_nat_narrowing_return_differential.py` around lines 252 - 274, The tier-3 test only inspects verifier status and WAT, so it must also validate runtime behavior. Extend test_tier3_return_promised_guard_is_emitted to execute the opaque float_to_int fixture with both a negative witness and a safe witness, asserting the negative input traps while the safe input completes successfully.Source: Path instructions
121-132: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winDistinguish the expected narrowing trap from other runtime failures.
_runcurrently maps everyWasmTrapErrortoNone, so an unrelated trap can satisfy the negative case and hide a codegen regression. CheckWasmTrapError.kindand only swallow the expected return-narrowing trap.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_nat_narrowing_return_differential.py` around lines 121 - 132, Update _run to inspect WasmTrapError.kind in the exception handler and return None only for the expected return-narrowing trap; re-raise all other WasmTrapError instances so unrelated runtime failures are not masked.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@tests/test_codegen_nat_guards.py`:
- Around line 1103-1108: The test does not verify that the proven return
narrowing retains its dead runtime guard. In
test_provable_abs_return_does_not_trap, inspect _fn_body(result.wat, "f") from
the generated output and assert it contains both i64.lt_s and unreachable before
the existing runtime assertions, while preserving the checks for -5 and 7.
- Around line 1052-1154: The return-guard tests lack coverage for match
expressions with arms narrowing into `@Nat`. Add a match-shaped fixture alongside
TestNatReturnRuntimeGuard758 with asymmetric arms, then execute inputs selecting
both a negative arm (asserting WasmTrapError) and a non-negative arm (asserting
the returned value), ensuring the `@Int-to-`@Nat return guard is applied across
every match leaf.
In `@tests/test_nat_narrowing_return_differential.py`:
- Around line 252-274: The tier-3 test only inspects verifier status and WAT, so
it must also validate runtime behavior. Extend
test_tier3_return_promised_guard_is_emitted to execute the opaque float_to_int
fixture with both a negative witness and a safe witness, asserting the negative
input traps while the safe input completes successfully.
- Around line 121-132: Update _run to inspect WasmTrapError.kind in the
exception handler and return None only for the expected return-narrowing trap;
re-raise all other WasmTrapError instances so unrelated runtime failures are not
masked.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 4ee513d9-adeb-461a-9604-7ee173ea3fd3
📒 Files selected for processing (4)
TESTING.mdtests/test_codegen_nat_guards.pytests/test_nat_narrowing_return_differential.pyvera/README.md
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
aallan
added a commit
that referenced
this pull request
Jul 11, 2026
…ware gate, tester/user-Tuple/import doors Review round on PR #986 (3 pr-review agents + 4-lens adversarial panel): - Per-arm hetero widen guard vs return_call: an arm whose @nat value is a tail call lowered to return_call and the appended guard was dead code (verify said tier3-guarded, run(u64.MAX) returned -1). Collect the call ids under guarded arms (_collect_hetero_widen_arm_calls, mirroring the #983 narrowing-leaf machinery) and subtract them from tail_sites so the guard stays live; the genuine @int arm keeps its recursive return_call. - Target-aware gate: the per-arm gate never consulted the join's target (unlike the verifier's _is_hetero_int_widen_join), so a hetero join in a @Nat-returning function false-trapped a legal @nat above 2^63-1 on a verify-clean Tier-1 program. Shared _is_hetero_int_widen_join now gates both emitters and the collector. - vera test compiled and verified without the checker artifacts, so the new guards vanished from tester-compiled WASM while the verifier claimed tier3; cmd_test now uses typecheck_with_artifacts and threads both tables through the Tester. - A user `data Tuple<A, B>` matched the builtin-carrier name gate; codegen guarded a construction the verifier never obligated. Gate on the variadic carrier's empty layout, not the name. - Imported bodies are excluded from span-keyed target-table recovery (_compile_fn(imported=True)): an engineered cross-file span collision produced a spurious guard that false-trapped a legal @nat. The guards are still not EMITTED for imported bodies (single-module table) — filed as #987 with KNOWN_ISSUES/SKILL/spec/CHANGELOG disclosure. - Test-coverage gaps closed: CLI-level threading pins (vera run traps, --wat carries the guard, verify --json surface pin; cmd_serve infeasible — documented), middle-match-arm + else-if-arm differential rows, 2^63-1 boundary controls at all six new sites, closure-return test comment/count pin corrected. - Docs: stale guarded/unguarded enumerations in verifier docstrings and the E531 rationale updated; "#758 widening residual" mis-references corrected to #813; spec/11 closure-recovery attribution fixed; #985 nested-closure reporting residual disclosed (KNOWN_ISSUES + CHANGELOG); counts reconciled (7,129 tests / 109 files). Refs #820. Cross-module residual: #987. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
added a commit
that referenced
this pull request
Aug 10, 2026
Adversarial round 1 found _boundary_base had two consumers where the thesis claims one. Five sites still spelled the composition themselves. Three were refactor-only (calls_handlers' State-cell and Exn-tag bases; the throw payload's call-site hop, which cannot call the named helper because the registry carries a name rather than a type expression, and now says so). Two MEASURABLY DIVERGED and are a behaviour change. The @int->@nat narrowing gate and the @Nat->@int widening gate chased the return alias by NAME, which drops an application's type arguments: under `type Ident<T> = T; type Count = Ident<Nat>;` both answered the bare head `Ident`, neither gate fired, and `f(0 - 5)` returned -5 through the @nat slot — #983's silent negative one spelling over. Both now ask _boundary_base, which resolves the type expression. The refinement exclusion beside the narrowing gate is a separate conjunct and is untouched, so an alias to a refinement keeps its single boundary guard. Reproduced independently before fixing: widen_alias emitted no guard where widen_plain did, and the narrow twin let -5 into a @nat slot. 7 new cases in test_codegen_nat_guards, 3 RED on the previous commit, each parameterised case paired with its unparameterised twin as the oracle plus the refinement-over-application control. Corpus: 0 movers against both the base commit and the previous one, and the 2 programs whose base SPELLING moves are inert for stated reasons (ch02_refinement_base_param_alias's `T`->`Nat` is excluded by the refinement conjunct; scoreboard's `Map`->`Map<String, Int>` is neither gate's value). The harness is shown to reach the gates: forcing the widen gate on moves 16 corpus programs. Also from the round: the cross-module registration-parity test the reviewer named as unprobed (a refined-Byte payload declared and used in a library, with a decoy alias of the same name over a different base in the importer, plus a companion proving the width assertion can go red); TESTING.md pipe escaping; is_gc_pointer_base narrowed to str, the unreachable None branch deleted; the false no-cover pragma on the heap-layout guard removed; the apply_fn Unit-arm comment rewritten to the chain it now consults; and a KNOWN_ISSUES row for #1276, which this work unmasked but does not fix. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
added a commit
that referenced
this pull request
Aug 10, 2026
Adversarial round 1 found _boundary_base had two consumers where the thesis claims one. Five sites still spelled the composition themselves. Three were refactor-only (calls_handlers' State-cell and Exn-tag bases; the throw payload's call-site hop, which cannot call the named helper because the registry carries a name rather than a type expression, and now says so). Two MEASURABLY DIVERGED and are a behaviour change. The @int->@nat narrowing gate and the @Nat->@int widening gate chased the return alias by NAME, which drops an application's type arguments: under `type Ident<T> = T; type Count = Ident<Nat>;` both answered the bare head `Ident`, neither gate fired, and `f(0 - 5)` returned -5 through the @nat slot — #983's silent negative one spelling over. Both now ask _boundary_base, which resolves the type expression. The refinement exclusion beside the narrowing gate is a separate conjunct and is untouched, so an alias to a refinement keeps its single boundary guard. Reproduced independently before fixing: widen_alias emitted no guard where widen_plain did, and the narrow twin let -5 into a @nat slot. 7 new cases in test_codegen_nat_guards, 3 RED on the previous commit, each parameterised case paired with its unparameterised twin as the oracle plus the refinement-over-application control. Corpus: 0 movers against both the base commit and the previous one, and the 2 programs whose base SPELLING moves are inert for stated reasons (ch02_refinement_base_param_alias's `T`->`Nat` is excluded by the refinement conjunct; scoreboard's `Map`->`Map<String, Int>` is neither gate's value). The harness is shown to reach the gates: forcing the widen gate on moves 16 corpus programs. Also from the round: the cross-module registration-parity test the reviewer named as unprobed (a refined-Byte payload declared and used in a library, with a decoy alias of the same name over a different base in the importer, plus a companion proving the width assertion can go red); TESTING.md pipe escaping; is_gc_pointer_base narrowed to str, the unreachable None branch deleted; the false no-cover pragma on the heap-layout guard removed; the apply_fn Unit-arm comment rewritten to the chain it now consults; and a KNOWN_ISSUES row for #1276, which this work unmasked but does not fix. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
added a commit
that referenced
this pull request
Aug 10, 2026
The verify pass found TestParameterisedAliasReturnGuard1256's _REFINED_OVER_APPLICATION did not discriminate the conjunct it names. Reproduced: with `_refinement_guard_parts` dropped from the narrowing gate the control still passed, because a @nat body into a @Nat-based return is no narrowing leaf at all — the leaf collector returns empty and the absence of `i64.lt_s` holds either way. The parameter is now @int with `requires(@Int.0 >= 18)` and an @Int.0 body, so the body genuinely narrows and the exclusion has something to exclude. Re-measured over the whole suite with the conjunct dropped: this control goes red, together with #983's unparameterised twin, and those two alone — so the exclusion is now tested at both spellings and by nothing incidental. Also from the pass: The #1256 CHANGELOG bullet states the severity plainly. Verified end to end rather than asserted: on the previous commit's gates `vera run --fn f -- -5` on an `Ident<Nat>` return prints -5, with no trap and no diagnostic; here it traps, and 7 still returns 7. A caller-side guard in front of such a function was masking, not preventing. The calls.py residue chase is recorded as untested — deleting it stays green because `family_base_name` already answers `Byte` for every refinement and alias reachable today, so no producer stores a base that still needs chasing. The comment says what a fixture would need. Skip-changelog: test fixture correction plus comment and severity wording; no behaviour change Co-Authored-By: Claude <noreply@anthropic.invalid>
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
1 participant
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
Fixes #758 — the
@Natnarrowing soundness hole at function return position.fn to_nat(@Int -> @Nat) requires(true) ensures(true) { @Int.0 }wasvera verify-clean at Tier 1, andto_nat(0 - 5)returned-5through the@Natslot with no obligation and no trap:verify-clean was not a "no negative@Nat" guarantee at the return boundary. The narrowing walker obligated every binding site (let, call-arg, constructor-field, match-bind, destructure — #552/#747) but never the function's own return slot, and codegen emitted no return coercion guard.The fix — both sides, in lockstep (the #813 dual)
nat_bindresult >= 0obligation at the return slot, reusing the existing_check_nat_binding_obligation— no parallel machinery. Detection descendsBlock/if/matchjoins to their leaf return expressions (_return_narrows_into_nat): the body is target-typed to the@Natreturn, so the checker's side-table masks a narrowing_arm if you consult the whole expression. The obligation folds in path conditions, soif @Int.0 >= 0 then { @Int.0 } else { 0 - @Int.0 }— andexamples/absolute_value.vera— prove at Tier 1; an unconstrained narrowing is a loud E503-family diagnostic; an opaque one is an honest Tier-3. Refined-over-@Natreturns stay on the existing 7b refinement check, so 7d gates on the bare primitive and the two never co-fire.@Natslot. Gated identically to 7d (bare@Nat, side-table-aware_result_is_nat), which also preserves TCO: a genuine@Nat -> @Nattail call would look like a narrowing through WASM's erased i64 return and wrongly lose itsreturn_call; the intrinsically-@Natclassifier excludes it.tests/test_nat_narrowing_return_differential.py) asserts the statically-obligated site set and the runtime-guarded site set agree across a battery of shapes — per the project's rule that cross-component soundness invariants need a differential, not unit tests.Scope honesty
The issue also names value-position tuple/constructor components: their static obligations already exist (re-verified — both shapes E503 today); the runtime-guard residual for those components is #820's per-component metadata family and stays there. This PR is the return-position scalar.
Evidence
to_natverify-clean +run(-5)=-5(the Auditsmt.pyZ3 translation layer for verification soundness #392-class proved-then-violated differential).absolute_value.verastays verify-green with its new obligation discharging Tier-1._cold_verifycalledverify()without resolved modules or the Generalize @Nat narrowing obligation to projection binding sites (ADT sub-pattern, non-literal destructure) #747 side-tables, somodules.vera's two imported-function obligations read Tier-3 in-process while the CLI proves them Tier-1 — the pins measured a pipeline no user runs, and the divergence had quietly produced contradictory corpus figures across earlier review rounds. Both loops now mirrorcmd_verifyexactly; the pin sits at the CLI-true 284/96/380.Docs lockstep
#758 rows deleted from KNOWN_ISSUES.md and SKILL.md; the "not obligated at return position" prose in spec/06 and vera/README updated to present reality; CHANGELOG
[Unreleased]bullet covers both the obligation and the trap; counts reconciled (150 conformance; the extended doc-counts gate now covers the previously blind prose sites).Closes #758
Summary by CodeRabbit
@Int→@Natnarrowing at function return boundaries: verification now enforces anat_bindreturn obligation, and codegen emits a corresponding runtime trap/guard unless proven non-negative.@Natreturn obligations and guard coverage, and refreshed conformance-suite sizing to 150 programs (plus updated status totals).