fix: obligate + guard the Int->Nat narrowing at apply_fn arguments (#1017) - #1025
Merged
Conversation
…1017) The verifier's `apply_fn` branch obligated only the `@Nat` -> `@Int` argument WIDENING (#820); the `@Int` -> `@Nat` NARROWING dual was missing, so `apply_fn(clo_nat_formal, 0 - 5)` verified clean (a false Tier 1) and, for a runtime value, entered the `@Nat` formal reinterpreted with no trap (a silent negative). - `vera/verifier.py`: the `apply_fn` loop now emits the `@Nat` narrowing obligation (mirroring the generic call-argument path) — E503 for a provable negative, a guarded Tier 3 otherwise. - `vera/wasm/closures.py`: `_translate_apply_fn` now guards the `call_indirect` argument with `_emit_nat_bind_guard`, the narrowing dual of its widen guard. Both arms are mutation-validated independently (neuter each -> a distinct RED). A four-quadrant verifier<->codegen differential (violated / runtime-trap / proven / unobligated) is added to `test_nat_narrowing_return_differential.py`. The completeness sweep found the refined-predicate dual at the same site is still a false Tier 1 (the strict predicate beyond the `>= 0` base this fixes); filed as #1024 and swapped into the KNOWN_ISSUES / ROADMAP / SKILL rows. Co-Authored-By: Claude <noreply@anthropic.invalid>
…ntial The #1017 corpus resolved every argument to `violated` or `verified` — it never exercised a genuine Z3-`unknown` `tier3` status, so the `guarded=True` deferral path (the crux of the cross-component soundness argument) was not directly asserted. Add the opaque-`float_to_int` argument case (mirroring the #758 return `_TIER3` quadrant): the verifier records the argument nat_bind `tier3` and the SAME compiled program carries the `call_indirect` narrowing guard, so `guarded=True` can never mean "promised but never emitted". Surfaced by the adversarial code review of the #1017 fix. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
🔗 Linked repositories identifiedCodeRabbit considers these linked repositories for cross-repo context during reviews:
📝 WalkthroughWalkthroughChangesThe Apply_fn narrowing enforcement
Estimated code review effort: 3 (Moderate) | ~20 minutes Sequence Diagram(s)sequenceDiagram
participant apply_fn
participant Verifier
participant WasmTranslator
participant call_indirect
apply_fn->>Verifier: inspect closure argument narrowing
Verifier->>Verifier: record nat_bind obligation
apply_fn->>WasmTranslator: translate closure argument
WasmTranslator->>call_indirect: emit `@Nat` runtime guard
call_indirect-->>apply_fn: return or trap
Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 7 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (7 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1025 +/- ##
=======================================
Coverage 93.51% 93.51%
=======================================
Files 96 96
Lines 32019 32024 +5
Branches 456 456
=======================================
+ Hits 29943 29948 +5
Misses 2063 2063
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:
|
Greptile SummaryThis PR fixes a false Tier-1 verifier pass and missing runtime guard for
Confidence Score: 5/5Safe to merge — the verifier and codegen changes are tightly symmetric, the four-quadrant differential was mutation-validated independently for each arm, and the remaining gap (#1024) is correctly scoped as a follow-on issue. Both changed components mirror the existing #820 widening handler at the same site; no unguarded code path remains for the @Nat-base narrowing at apply_fn argument positions. No files require special attention.
|
| Filename | Overview |
|---|---|
| vera/verifier.py | Adds @int -> @nat narrowing obligation in the apply_fn branch, mirroring the existing @nat -> @int widening arm; logic is symmetric and correct. |
| vera/wasm/closures.py | Adds _emit_nat_bind_guard for @Nat-formal arguments in _translate_apply_fn, the codegen dual of the verifier's new narrowing obligation; placed correctly as the narrowing-first arm before the existing widening arm. |
| tests/test_nat_narrowing_return_differential.py | Adds four-quadrant differential for apply_fn argument narrowing (violated/runtime-trap/proven/unobligated); corpora are well-isolated. Docstring on _return_nat_bind_statuses no longer describes all callers accurately. |
| CHANGELOG.md | Adds changelog entry for #1017 fix; accurate and well-scoped. |
| KNOWN_ISSUES.md | Replaces #1017 row with #1024 (refinement-predicate narrowing), correctly tracking the remaining known gap. |
Reviews (2): Last reviewed commit: "docs: note the tier-3 quadrant in the #1..." | Re-trigger Greptile
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 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 89: The TESTING.md row for test_nat_narrowing_return_differential.py
omits the `#1017` tier3 apply_fn argument-narrowing coverage. Update that row’s
`#1017` description to include the _APPLYFN_ARG_TIER3 /
test_tier3_arg_promised_guard_is_emitted quadrant, noting that it cross-checks
the verifier’s tier3 promise with the emitted i64.lt_s/unreachable runtime guard
in one pipeline run.
🪄 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: f1b3d031-6b3d-4916-9565-739979790009
⛔ Files ignored due to path filters (2)
docs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (9)
CHANGELOG.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdtests/test_nat_narrowing_return_differential.pyvera/verifier.pyvera/wasm/closures.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
The row's #1017 description listed only the four original outcomes; the follow-on tier-3 quadrant (an opaque float_to_int argument recording tier3 with the codegen guard emitted) was added to the test file but not the prose. Add the clause so the description matches the actual coverage. 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 the false Tier-1 in #1017: the
@Int→@Natnarrowing at anapply_fnargument (into the closure's@Natformal) was not obligated by the verifier and not guarded by codegen — the narrowing dual of the #820 argument-widening handler at the same site.apply_fn(clo_nat_formal, 0 - 5)verified clean (a false Tier 1); a runtime value entered the@Natformal reinterpreted with no trap (a silent negative — worse than the issue's framing, confirmed byvera run).Fix — both surfaces, mirroring the generic call-argument path
vera/verifier.py— theapply_fnbranch now emits the@Natnarrowing obligation (_nat_binding_target+_narrows_into_nat→_check_nat_binding_obligation,guarded=True): E503 for a provably-negative value, a guarded Tier 3 for a runtime value.vera/wasm/closures.py—_translate_apply_fnnow guards thecall_indirectargument with_emit_nat_bind_guard(the narrowing dual of its existing_emit_int_widen_guard), so a Tier-3 narrowing traps at runtime rather than entering the formal silently.Validation
test_nat_narrowing_return_differential.py— provably-negative arg (E503), runtime arg (obligated +call_indirect-guarded, run traps),requires-bounded arg (Tier-1 proven, guard dead),@Nat→@Natarg (unobligated, no false guard on a u64.MAX value).@Natbase (≥ 0) and@Nat-alias formals are covered; the refined-predicate dual (the> 0part beyond the≥ 0base) is still a false Tier-1 at the same site — filed as Verifier+codegen: refined-predicate narrowing into an apply_fn closure formal is not obligated/guarded (false Tier-1) #1024 and swapped into the KNOWN_ISSUES / ROADMAP / SKILL rows.mypy, 157 conformance programs, 38 examples, 408 targeted verifier/codegen tests, doc counts (7,410).Closes #1017
🤖 Generated with Claude Code
Summary by CodeRabbit
apply_fn-related narrowing through indirect calls so@Int→@Natis now both statically obligated and runtime-guarded.call_indirectboundary to ensure invalid negative values trap as expected.apply_fnargument narrowing outcomes, including obligation and trapping behaviour.