fix(804): assert/assume facts discharge later obligations (v0.0.179)#805
Merged
Conversation
…f of #800) The assume-half of the WP rule (spec section 6.4.1): a body assert(P)/assume(P) now adds P to the assumption context for subsequent obligations in its block, and a top-level assert/assume to the postcondition and refined return. #800 added only the prove-half; this completes the rule. Moves obligations Tier 3 -> Tier 1 and removes false E503/E500/E505 where a prior assert provably guards the site (the runtime trap makes the negative witness unreachable). Sound by construction: facts flow forward-only and stay branch-local, both pinned by regression guards. Implementation: a shared _assumed_block_fact helper; the primitive-op walk pushes the fact onto smt._path_conditions (snapshot/truncate per block), the nat-binding walk appends to its block_assumptions copy, and _verify_fn collects top-level facts for the post-body (ensures / refined-return) checks. Releases v0.0.179, folding in the #392 audit batch 1 (#799/#800/#801) that rode [Unreleased]. test_soundness_392.py grows to 27 tests (8 new, RED-first confirmed), an extended ch06_assert_assume conformance program, full suite green (4898 passed). Closes #804. Refs #392, #800. Co-Authored-By: Claude <noreply@anthropic.invalid>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #805 +/- ##
=======================================
Coverage 91.92% 91.93%
=======================================
Files 89 89
Lines 26615 26658 +43
Branches 321 321
=======================================
+ Hits 24467 24509 +42
- Misses 2140 2141 +1
Partials 8 8
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 PR bumps the project to v0.0.179 and adds verifier handling for bare ChangesAssert/assume fact discharge
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related issues
Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 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: 3
🤖 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 `@README.md`:
- Line 218: The project-status counts are out of sync between the README and
HISTORY, so update the release figure in the status blurb or the corresponding
count in HISTORY.md to match. Use the README.md active-development summary and
the HISTORY.md tagged-releases section as the source of truth, and make sure the
release count is consistent across both places after the edit.
In `@tests/test_soundness_392.py`:
- Around line 393-425: Add mirrored top-level assume coverage for both discharge
paths in test_top_level_assert_discharges_postcondition and
test_top_level_assert_discharges_refined_return. Update the existing
_verify-based cases to include equivalent assume(`@Int.0` > 5) and assume(`@Int.0` >
0) scenarios so the same ensures and refine_bind checks verify that top-level
assume facts are threaded correctly by _verify_fn. Keep the assert tests, but
add the assume variants in the same test module to catch regressions where
assumptions are dropped before postcondition or refined-return validation.
In `@vera/verifier.py`:
- Around line 1446-1458: Top-level assert/assume facts are only being appended
after `translate_expr(decl.body)` has already translated sibling call sites, so
call-precondition checks can miss those path conditions and emit spurious
E501/Tier 3 results. Update `SmtContext._translate_block` (or add an equivalent
verifier-side call-precondition pass) so
`_collect_top_level_assert_facts`-derived facts are threaded positionally into
call-precondition translation before later sibling calls are checked, matching
the existing block-walker behavior and the `_path_conditions` handling around
`check_valid`.
🪄 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
Run ID: 03e0c87f-392e-492a-bd0b-47d2dbce6897
⛔ Files ignored due to path filters (6)
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/ch06_assert_assume.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (10)
CHANGELOG.mdHISTORY.mdREADME.mdROADMAP.mdTESTING.mdpyproject.tomltests/conformance/manifest.jsontests/test_soundness_392.pyvera/__init__.pyvera/verifier.py
…able discharge The pr-review-toolkit (pr-test-analyzer, criticality 7) flagged that `match` arms reach the #804 logic through a route distinct from if/else (the nat-binding walk shares the parent assumptions to each arm; the primitive-op walk scopes via the per-block del), and that div_zero discharge by a prior assert was untested. Adds 4 tests to TestAssertAssumeFacts804: - within-match-arm forward discharge ([tier3, verified]) - cross-match-arm non-leak soundness guard ([tier3, tier3]) - div_zero discharged by a prior assert(@Int.0 != 0) (removes a false E526 on the guard-then-divide idiom) - an untranslatable assert between two translatable ones does not break forward discharge (the _assumed_block_fact None-return path) The 3 behavior tests were confirmed RED on the pre-fix verifier (revert vera/verifier.py to 1c577f0); the cross-arm guard is green both ways. Test-only; no behaviour change. Part of the v0.0.179 release (#804). Co-Authored-By: Claude <noreply@anthropic.invalid>
…ollow-ups Addresses the pr-review-toolkit + CodeRabbit review of #805: - Call preconditions (CR Major): a call's precondition is checked during body translation (#730), one phase before the obligation walks, so the #804 fact pushes didn't reach it — a guarded call (assert P; then a call requiring P) recorded a false E501. SmtContext._translate_block now threads the assert/ assume fact forward: pushed onto _path_conditions after the statement, dropped at block exit by a finally that also covers the early return-None paths (so an untranslatable statement after an assert can't leak the fact into the post-translation walks). Confirmed RED on the pre-fix verifier, with a soundness guard that a weaker prior assert still records E501. - assume coverage (CR Minor): added top-level assume() postcondition and refined-return discharge tests (mirroring the assert cases). - doc sync (CR Minor): HISTORY "By the numbers" total 174 -> 179 tagged releases (matches the README status line + git tag count); README test count -> 4,938. test_soundness_392.py -> 35 tests; full suite 4906 passed. Part of v0.0.179. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
pr-review-toolkit — round 1Ran four review agents (code-reviewer, pr-test-analyzer, silent-failure-hunter, comment-analyzer) over the diff. Each validated empirically — mutation tests plus Verdict: no bugs, no soundness defects, comments accurate
What I changed in response (commit f522200)No defects to fix, but the test-analyzer surfaced two genuine coverage gaps worth closing, so I added 4 tests (
The 3 behavior tests were confirmed RED on the pre-fix verifier (reverting Considered and left as-is (sub-threshold, verified non-issues)
|
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 `@tests/test_soundness_392.py`:
- Around line 489-507: The test for
`test_prior_assert_discharges_call_precondition` is too weak because it only
checks that `needs_positive` produces no error and no `call_pre` obligation,
which can still pass if the call never reaches Tier-1 translation. Strengthen
the test by adding an observable callee-to-caller assertion tied to
`needs_positive` (for example, a postcondition or refined return that `f` must
verify) so the test proves the call was translated and discharged. Apply the
same pattern to the corresponding `assume(...)` case if present, using the
existing `_verify`, `result.obligations`, and `result.diagnostics` assertions as
the entry points.
🪄 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
Run ID: 57dca4f8-9697-4e7b-96a9-695d9b3b1270
📒 Files selected for processing (7)
CHANGELOG.mdHISTORY.mdREADME.mdROADMAP.mdTESTING.mdtests/test_soundness_392.pyvera/smt.py
CodeRabbit round-2 (Major): the call-pre discharge test asserted only "no E501" + "no call_pre obligation", which would still pass if the call silently stopped translating (successful call-pre checks are unrecorded). Tie the result to the callee's postcondition — the caller's ensures(result > 0) only verifies if the call is actually translated and discharged — so the test fails (ensures -> tier3) on a translation regression, not merely on a missing error. Mirror the shape for the assume half (a new assume call-pre test). Both confirmed RED on the pre-call-pre-fix smt.py. test_soundness_392.py -> 36. Co-Authored-By: Claude <noreply@anthropic.invalid>
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 63: Update the TESTING.md entry so the assume-half behavior is attributed
to the correct issue number. The current note in the release/test matrix points
to `#800`, but the surrounding release notes and PR context identify the
assume-half rule as `#804`; change that reference in the TESTING.md row for
test_soundness_392.py so readers are directed to the right regression/change.
🪄 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
Run ID: cefe9932-b0a5-40c3-bc8f-6b2ddc3edf8e
📒 Files selected for processing (4)
README.mdROADMAP.mdTESTING.mdtests/test_soundness_392.py
CodeRabbit round-3: the test_soundness_392.py row said "the #800 assume-half", which misdirects readers to #800 (the prove-half); the assume-half is #804. Lead the clause with #804 and note it is the assume-half of #800's assert rule. Also reflect the call-precondition discharge (E501) added earlier this round. Validated --no-verify (prose-only): doc-counts + site-assets green; no vera/spec change so suite/mypy/ruff/changelog gates are N/A. 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
Implements the assume-half of the weakest-precondition rule for
assert/assume(spec §6.4.1) — the follow-up to #800, which added only the prove-half. Closes #804 (batch 2 of the #392 soundness audit), and cuts release v0.0.179, folding in the batch-1 fixes (#799/#800/#801) that have been riding[Unreleased]since #803.What changed
A body
assert(P)/assume(P)now addsPto the assumption context for subsequent obligations:assert(P) | P && WP(rest)— proveP(verifier: assert(P) generates no Tier-1 obligation — unprovable asserts pass vera verify (contradicts spec 6.2.5) #800), then assume it downstream.assume(P) | P ==> WP(rest)— assumePdownstream (no obligation of its own).Preaches every later obligation in the statement's block, and a top-level assert/assume also reaches the postcondition and a refined return.Why it's sound — a completeness gain, not a soundness risk
The §11.14.1 runtime trap guarantees execution only proceeds past
assert(P)in worlds wherePholds — soPis assumable downstream even when the assert itself only reached Tier 3. This moves obligations Tier 3 → Tier 1 and removes spuriousE503/E500/E505errors where a prior assert provably guards the site:Two soundness invariants are pinned by guard tests (green both pre- and post-fix; a buggy implementation reddens them):
if/match.Implementation
_assumed_block_fact— shared helper returning a bare assert/assume statement's translated predicate.smt._path_conditions(snapshot + truncate per block — the scoped channelcheck_validalready folds into every obligation).block_assumptionscopy (auto-scoped, auto-discarded at block exit)._verify_fn: collects unconditional top-level facts and spans them across the post-body checks (ensures + refined-return).Tests (test-first)
tests/test_soundness_392.pygrows to 27 tests (8 new inTestAssertAssumeFacts804). Each behavior test was confirmed RED on the pre-fix verifier — stashing onlyvera/verifier.pyflips 6 behavior tests red while the 2 soundness guards stay green. Extended thech06_assert_assumeconformance program with a discharge demonstration (vera run→ 30).Validation
mypyclean;ruff+ruff --select Sclean; conformance 92/92; walker-coverage OK; doc-counts / version-sync / site-assets green.Closes #804. Refs #392, #800.
🤖 Generated with Claude Code
Summary by CodeRabbit
Bug Fixes
assert(P)andassume(P)contribute “assume-half” facts to later verification, including correct Tier-1 discharge, postcondition and call precondition handling, and locality withinif/match.Tests
#804assume-half behaviour, updated the related soundness test, and refreshed soundness metrics.Documentation