Enforce decreases clauses at run time (the E525 promise) - #1179
Conversation
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughThe checker validates ChangesDecreases enforcement
Estimated code review effort: 4 (Complex) | ~60 minutes Sequence Diagram(s)sequenceDiagram
participant Checker
participant CodeGenerator
participant WASMRuntime
Checker->>Checker: validate decreases measure type
Checker->>CodeGenerator: provide decreases obligation
CodeGenerator->>WASMRuntime: emit guard and ranking helpers
WASMRuntime->>WASMRuntime: compare measure and restore guard state
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 6 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (6 passed)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1179 +/- ##
==========================================
- Coverage 93.78% 93.75% -0.03%
==========================================
Files 99 99
Lines 33651 33945 +294
Branches 458 458
==========================================
+ Hits 31558 31826 +268
- Misses 2080 2106 +26
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:
|
91ea207 to
db7567f
Compare
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 15
🤖 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 `@AGENTS.md`:
- Line 11: Update the negative-fixture documentation in AGENTS.md by changing
“seventeen” to “eighteen” and adding ch05_decreases_float_rejected to both
enumerated negative-fixture lists, including the list near the conformance
overview and the corresponding list near the later invariant. Keep the lists
synchronized and preserve the existing formatting.
In `@CHANGELOG.md`:
- Line 14: Update the runtime-guard documentation to qualify that entry guards
are generated only for translatable decreases measures, and that self-tail-call
optimization applies only when the call-site check can be generated; otherwise
use plain-call fallbacks. In CHANGELOG.md at line 14 and SKILL.md at lines
1319-1320, retain the existing mutual-tail fallback description while explicitly
including untranslatable measures and demoted self-tail calls.
In `@TESTING.md`:
- Line 170: Synchronize all conformance documentation totals in TESTING.md:
update the stale 840 parametrized-test count to 855, add
ch05_decreases_float_rejected with its E127 expectation to the check-level
enumeration, change the negative-test total from 17 to 18, and correct the
skipped-test summary to 59 level-limited plus four environment-gated skips.
- Line 9: Regenerate the aggregate test counts in the Tests row of TESTING.md
using pytest collection or scripts/check_doc_counts.py as the canonical source,
ensuring the total equals the sum of passed, stress, and skipped tests. Update
all displayed component values and the total consistently.
In `@tests/conformance/manifest.json`:
- Around line 1313-1324: Update the expected_error value for the
ch07_bare_effect_op_rejected manifest entry from E217 to E219, keeping the rest
of the conformance case unchanged.
In `@tests/test_codegen_decreases_guard.py`:
- Around line 329-367: Update test_lexicographic_ackermann_runs to use an
asymmetric Ackermann entry point instead of only ackermann(2, 2), asserting the
expected non-equal result for either ackermann(1, 2) or ackermann(2, 1) so
argument order and decreases tuple slot mapping are exercised. Keep the
compilation and generated $dec_active_ackermann assertions intact.
- Around line 235-255: Update test_lexicographic_violation_traps to use distinct
initial arguments so the decreases tuple slot order is observable, then add a
mirrored recursive case where the first component decreases while the second
grows and assert that it does not trap. Keep the existing lexicographic
violation coverage while ensuring the cases distinguish the correct component
ordering from a swapped ordering.
- Around line 600-606: Update all four `$dec_active_*` WAT assertions, including
the negative assertion in the shown test and the positive checks near the other
referenced locations, to match complete symbol names with a trailing boundary
lookahead rather than plain substring membership. Ensure suffixed symbols such
as `$dec_active_length$Int` do not satisfy an assertion intended for the bare
parameterized measure.
- Around line 47-60: Update the shared _compile helper to unlink its
delete=False temporary .vera file after parsing/compilation, while preserving
the path for parse_file and compile. Refactor
test_tier3_decreases_obligation_has_emitted_guard to reuse a shared helper
returning (prog, source, path) instead of creating its own tempfile block,
ensuring cleanup occurs for every compilation path.
- Around line 77-84: Remove the unused _run_trap_message helper and the wasmtime
import that exists only for it; keep trap assertions routed through _run_cli and
_assert_termination_trap. If retaining the helper for an in-process test,
restrict its exception handling to the repository’s WasmTrapError
contract_violation path instead of accepting generic wasmtime or RuntimeError
exceptions.
In `@vera/checker/core.py`:
- Around line 875-886: Update the well-foundedness check around the local base
calculation to repeatedly unwrap RefinedType layers until reaching the
underlying type, rather than peeling only one layer. Preserve the existing
UnknownType skip and INT/NAT or registered AdtType checks once the fully
unwrapped base is reached.
In `@vera/codegen/contracts.py`:
- Around line 1139-1212: Update _dec_rank_helper to snapshot
self._dec_rank_helpers on entry and restore its contents in place whenever the
recursive walk fails, including nested helper reservations and bodies created
during the attempt. Preserve successful helper generation and the existing
recursive reservation behavior, and do not rebind the shared accumulator object.
In `@vera/codegen/functions.py`:
- Around line 587-590: Wrap the `_compile_decreases_entry` call in the same
contract-predicate degradation dispatcher used by the precondition,
refinement-guard, and postcondition paths. Ensure `CodegenSkip`,
`AdtEqNotDerivableError`, and `CodegenInvariantError` from decreases expression
translation are converted to the established `E602` degradation behavior rather
than escaping as a traceback, while preserving normal instruction emission for
supported predicates.
- Around line 1134-1142: Prevent decreases guards from being generated for
functions whose effect declares Exn by adding an early return in
_compile_decreases_entry after locating the Decreases contract, preserving the
existing no-contract behavior. Update the trailing restore comment near
dec_restore_instrs to acknowledge that return_call paths restore inline and that
the block is not exhaustive; remove the incorrect claim that guarded functions
cannot contain return_call.
In `@vera/README.md`:
- Line 135: Fix the Markdown table row for contracts.py in the module map to
remove leading spaces from inside the inline code span while preserving the
intended tree indentation outside the span, or use an equivalent HTML code
representation with non-breaking spaces.
🪄 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: 75a64e04-da56-4c18-abb0-2fb518f7f2e2
⛔ Files ignored due to path filters (8)
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/**examples/gc_pressure.verais excluded by!**/*.veratests/conformance/ch05_decreases_float_rejected.verais excluded by!**/*.veratests/conformance/ch05_decreases_guard.verais excluded by!**/*.vera
📒 Files selected for processing (21)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/05-functions.mdtests/conformance/manifest.jsontests/test_codegen_decreases_guard.pytests/test_verifier_adt_decreases.pyvera/README.mdvera/_since.pyvera/checker/core.pyvera/codegen/assembly.pyvera/codegen/contracts.pyvera/codegen/core.pyvera/codegen/functions.pyvera/errors.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
There was a problem hiding this comment.
Actionable comments posted: 6
♻️ Duplicate comments (3)
vera/codegen/functions.py (2)
1134-1142: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winThe comment contradicts the code, and an exception unwind skips the restores.
Two separate points.
The comment claims "no
return_callsurvives in a guarded function (the revert above)". Theelif dec_restore_instrs:branch at Lines 970-1016 deliberately keepsreturn_callfor a self-recursive site (Line 1005) and for an unguarded target (Line 1015). Behaviour is correct — those sites carry their restores inline — but the comment will mislead the next maintainer into treating this block as exhaustive.
vera/codegen/assembly.pyLines 373-376 emit(tag $exn_<T>), so a guarded function that declaresExn<E>canthrow. A WASMthrowunwinds past these trailing instructions, so$dec_active_<f>stays1and$dec_prev_<f>_kkeeps the aborted activation's measure. A later unrelated call tofreadssaved_active == 1, compares against that stale baseline, and traps withdecreases() measure in 'f' failed to decreaseon a terminating program. The per-activation baseline lives in locals, so the restore cannot move into acatch.🐛 Proposed fix — correct the comment and decline the guard for `Exn` functions
Gate
_compile_decreases_entryinvera/codegen/contracts.pyright after the contract lookup:if contract is None: return [], [], None # An `Exn` throw unwinds past the exit restores, leaving # `$dec_active_<fn>` set and `$dec_prev_<fn>_k` holding the aborted # activation's measure — a later unrelated call would then trap # spuriously. Emit no guard rather than a leaky one. if _declares_exn(decl.effect): return [], [], NoneAnd correct the comment here:
- # `#1172`: decreases-guard restores — every non-trap exit puts the - # function's chain state back to what this activation saved, so a - # finished call leaves no residue that would spuriously trap a - # sibling call. Trap paths need no restore (the instance dies), - # and no `return_call` survives in a guarded function (the revert - # above), so this single exit point covers every live return. + # `#1172`: decreases-guard restores for the FALL-THROUGH exit — the + # function's chain state goes back to what this activation saved, so + # a finished call leaves no residue that would spuriously trap a + # sibling call. Trap paths need no restore (the instance dies). A + # surviving `return_call` does NOT reach here: the tail-call patching + # above prepends `dec_self_tail` (self-recursive) or + # `dec_restore_instrs` (unguarded target) at each such site instead.🤖 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 `@vera/codegen/functions.py` around lines 1134 - 1142, Update _compile_decreases_entry in vera/codegen/contracts.py to return no decreases guard when _declares_exn(decl.effect) is true, immediately after the contract lookup and its None check, preventing exception unwinds from leaving stale guard state. Also revise the trailing restore comment near dec_restore_instrs to acknowledge that return_call sites can retain inline restores and that this block is not exhaustive.
577-591: 🩺 Stability & Availability | 🔴 Critical | ⚡ Quick win
_compile_decreases_entrystill sits outside the contract-predicate degradation net.The call lowers contract predicates:
vera/codegen/contracts.pyLines 878 and 1024 callctx.translate_expron everydecreasescomponent. That path raisesCodegenSkipfor an unsupported construct,AdtEqNotDerivableErrorfor a non-Eq composite==, andCodegenInvariantErrorfor a dangling slot.The precondition and refinement-guard block above (Lines 513-573) and the postcondition block below (Lines 839-867) both carry the full net.
_emit_contract_predicate_degradationstates the invariant at Lines 99-102: a user program must never surface a Python traceback from a contract predicate.decreaseswas not lowered before this PR, so the gap is newly reachable —decreases(hash(@Tree.0))now crashesvera compileon acheck-green program.🔒️ Proposed fix — reuse the existing dispatcher
- dec_entry_instrs, dec_restore_instrs, dec_self_tail = ( - self._compile_decreases_entry(ctx, decl, env) - ) + try: + dec_entry_instrs, dec_restore_instrs, dec_self_tail = ( + self._compile_decreases_entry(ctx, decl, env) + ) + except (AdtEqNotDerivableError, CodegenSkip) as exc: + self._emit_contract_predicate_degradation(ctx, exc, decl) + return None + except CodegenInvariantError as inv: + self._harvest_interp_inference_failures(ctx) + self._error( + inv.node if inv.node is not None else decl, + f"Internal compiler error while compiling '{decl.name}': " + f"{inv.msg}", + rationale="This is a codegen invariant violation — the type " + "checker should have rejected the input before it reached this " + "point. Please file a bug report with the offending program.", + error_code="E699", + ) + return None pre_instrs = pre_instrs + dec_entry_instrs🤖 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 `@vera/codegen/functions.py` around lines 577 - 591, Wrap the _compile_decreases_entry call in the same contract-predicate degradation dispatcher used by the precondition and postcondition lowering blocks, so CodegenSkip, AdtEqNotDerivableError, and CodegenInvariantError are degraded consistently instead of escaping as Python tracebacks. Preserve the existing decreases entry, restore, and tail-instruction behavior for successfully lowered predicates.vera/codegen/contracts.py (1)
1139-1212: 🩺 Stability & Availability | 🔴 Critical | ⚡ Quick winA partially-successful rank walk still commits an orphaned helper.
Line 1207 removes only this walk's own reservation. A nested helper committed a real body at Line 1211 during the same walk, and that body contains
call $dec_size_<T>for the name just deleted.vera/codegen/assembly.pyLines 586-588 emit every non-empty entry, sowat2wasmfails withunknown funcand the whole compile dies on acheck-green program — worse than the intended "no guard".Snapshot the accumulator on entry and restore it in place on failure, the same discipline
_lift_pending_closuresuses.🔒️ Proposed fix — roll back the whole accumulator
layouts = self._adt_layouts.get(adt_name) if not layouts: return None + # Roll back EVERY helper this walk committed, not just our own + # reservation: a nested helper stored a real body that calls our + # short-circuited name, so keeping it dangles `unknown func`. + snapshot = dict(self._dec_rank_helpers) # Reserve the name first so a recursive field type terminates. self._dec_rank_helpers[fn_name] = ""if not ok: - del self._dec_rank_helpers[fn_name] + self._dec_rank_helpers.clear() + self._dec_rank_helpers.update(snapshot) return NoneMutate the dict in place.
AssemblyMixinandContractsMixinshare the one attribute onCodeGenerator.🤖 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 `@vera/codegen/contracts.py` around lines 1139 - 1212, In _dec_rank_helper, snapshot the entire _dec_rank_helpers accumulator before reserving the current helper, and on any failure restore that snapshot in place rather than deleting only fn_name. Preserve the shared dictionary object used by AssemblyMixin and ContractsMixin, while retaining successful helper bodies when the walk completes.Source: Learnings
🤖 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 `@AGENTS.md`:
- Line 11: Update the conformance documentation in AGENTS.md to match the
complete cross-module program set documented by SKILL.md, including all
companion-module exceptions from Chapters 7–9. Prefer deriving or validating the
list against tests/conformance/manifest.json so AGENTS.md and SKILL.md use one
canonical description and remain synchronized with the codebase.
In `@spec/05-functions.md`:
- Line 135: Update the ordering requirement sentence in the specification to use
the RFC 2119 keyword “MUST” instead of lowercase “must,” preserving the
surrounding wording and semantics.
- Line 135: Update the termination-measure description in the relevant section
to state that Float64 is rejected with E127 because it lacks a supported
well-founded ordering, not because its domain is unbounded. Document how NaN and
positive or negative infinity are handled by the runtime check.
- Line 160: Update the runtime-checking description to specify tuple handling
separately: on each re-entry, first validate that every lexicographic measure
component is non-negative, then require the tuple to be strictly smaller
lexicographically than the previous activation. Do not state or imply that every
component must decrease; retain the existing scalar and ADT structural-size
behavior.
- Line 163: Update the ADT measure guidance in the specification to state that
parameterisation disables runtime ranking, but static verification still
classifies the obligation as Tier 1, Tier 2, or Tier 3; reserve Tier 3 only for
obligations that static verification cannot discharge.
In `@tests/test_codegen_decreases_guard.py`:
- Around line 154-189: Extend TestNonTerminatingTraps with coverage for guarded
self-tail-call preservation: compile a decreasing recursive function and assert
its generated WAT retains return_call for the self-recursive site, then execute
it with sufficiently deep recursion and verify the expected result to pin
constant-stack-depth behavior. Reuse the existing _compile_ok and _run helpers,
and add the check as a separate test from
test_constant_int_measure_tail_call_traps.
---
Duplicate comments:
In `@vera/codegen/contracts.py`:
- Around line 1139-1212: In _dec_rank_helper, snapshot the entire
_dec_rank_helpers accumulator before reserving the current helper, and on any
failure restore that snapshot in place rather than deleting only fn_name.
Preserve the shared dictionary object used by AssemblyMixin and ContractsMixin,
while retaining successful helper bodies when the walk completes.
In `@vera/codegen/functions.py`:
- Around line 1134-1142: Update _compile_decreases_entry in
vera/codegen/contracts.py to return no decreases guard when
_declares_exn(decl.effect) is true, immediately after the contract lookup and
its None check, preventing exception unwinds from leaving stale guard state.
Also revise the trailing restore comment near dec_restore_instrs to acknowledge
that return_call sites can retain inline restores and that this block is not
exhaustive.
- Around line 577-591: Wrap the _compile_decreases_entry call in the same
contract-predicate degradation dispatcher used by the precondition and
postcondition lowering blocks, so CodegenSkip, AdtEqNotDerivableError, and
CodegenInvariantError are degraded consistently instead of escaping as Python
tracebacks. Preserve the existing decreases entry, restore, and tail-instruction
behavior for successfully lowered predicates.
🪄 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: 3d6c7acf-52c2-49b1-8589-0b6cb3ae5324
⛔ Files ignored due to path filters (8)
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/**examples/gc_pressure.verais excluded by!**/*.veratests/conformance/ch05_decreases_float_rejected.verais excluded by!**/*.veratests/conformance/ch05_decreases_guard.verais excluded by!**/*.vera
📒 Files selected for processing (21)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/05-functions.mdtests/conformance/manifest.jsontests/test_codegen_decreases_guard.pytests/test_verifier_adt_decreases.pyvera/README.mdvera/_since.pyvera/checker/core.pyvera/codegen/assembly.pyvera/codegen/contracts.pyvera/codegen/core.pyvera/codegen/functions.pyvera/errors.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
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)
TESTING.md (1)
668-668: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winKeep the site-fact validation documentation aligned.
Line 668 says
check_site_assets.pynow covers generated-asset freshness only.CHANGELOG.mdLines 11–13 sayscheck_fact_coherence()independently validates facts acrossdocs/index.htmlanddocs/index.md. Keep both checks documented, or update the implementation and CHANGELOG together.As per path instructions, Markdown documentation must match the codebase.
🤖 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 `@TESTING.md` at line 668, Update the site-fact validation documentation around check_site_assets.py to also describe check_fact_coherence() and its validation of facts across docs/index.html and docs/index.md. Keep TESTING.md and CHANGELOG.md consistent with the current implementation, or update the implementation and both documents together if the validation behavior is changing.Source: Path instructions
🤖 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`:
- Around line 9-11: Update the TESTING.md validation inventory by adding
test_eq_contract_874.py to the Test Files table with its 13 tests and adjusting
the overview totals to include them. Also expand the check_site_assets.py entry
to document check_fact_coherence() validation for docs/index.html and
docs/index.md.
---
Outside diff comments:
In `@TESTING.md`:
- Line 668: Update the site-fact validation documentation around
check_site_assets.py to also describe check_fact_coherence() and its validation
of facts across docs/index.html and docs/index.md. Keep TESTING.md and
CHANGELOG.md consistent with the current implementation, or update the
implementation and both documents together if the validation behavior is
changing.
🪄 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: 635c54bd-44c4-4c6b-ac77-02e6ba9d911d
⛔ Files ignored due to path filters (2)
docs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (12)
AGENTS.mdCHANGELOG.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/05-functions.mdtests/test_codegen_decreases_guard.pyvera/checker/core.pyvera/codegen/contracts.pyvera/codegen/core.pyvera/codegen/functions.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
dc5c799 to
45ded6b
Compare
There was a problem hiding this comment.
Actionable comments posted: 5
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/codegen/contracts.py (1)
1-1: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winBoth measure-component loops can commit a rank helper and then decline the guard.
_dec_rank_helperrolls back what a failed rank walk commits, but neither component loop snapshotsself._dec_rank_helpersbefore it can succeed on one component and bail on a later one.vera/codegen/assembly.pyLines 586-588 then emit the orphaned$dec_size_<T>for a function that received no guard, and the entry path only setsself._needs_memoryat Line 959 — after the loop that emitted a helper containingi32.load.
vera/codegen/contracts.py#L888-904: snapshotself._dec_rank_helpersbefore the loop and restore it at each of the three early returns.vera/codegen/contracts.py#L1033-1048: apply the same snapshot and restore at eachreturn Nonein this loop.🤖 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 `@vera/codegen/contracts.py` at line 1, Update both measure-component loops in the relevant contract-generation methods to snapshot self._dec_rank_helpers before iteration and restore that snapshot before every early return (including all three returns in the first loop and each return None in the second). Preserve helpers only when the complete loop succeeds, preventing orphaned rank helpers from being emitted without a corresponding guard.Source: Learnings
♻️ Duplicate comments (1)
tests/test_codegen_decreases_guard.py (1)
145-180: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winThe headline TCO claim is still unpinned.
The module docstring at Lines 14-21 states that a self-recursive
return_callkeeps TCO under the guard, andvera/codegen/functions.pyLines 1022-1029 implement exactly that.test_constant_int_measure_tail_call_trapsproves only that the trap fires; it passes equally if that branch demoted every self-tail site to a plaincall. Both the structural property and the constant-stack-depth property remain unchecked, so a regression that silently demotes guarded self-tail calls surfaces only when a deep program exhausts the stack.As per path instructions: "Missing edge cases for new compiler features" and "A test for a non-commutative op that only checks a commutative case (or whose inputs are symmetric) cannot catch a slot-order bug."💚 Pin the structural and the depth property
def test_guarded_self_tail_keeps_return_call(self) -> None: """The guard must not demote a self-recursive tail call (`#517`).""" source = """\ private fn drain(`@Int`, `@Int` -> `@Int`) requires(true) ensures(true) decreases(`@Int.1`) effects(pure) { if `@Int.1` <= 0 then { `@Int.0` } else { drain(`@Int.0` + 1, `@Int.1` - 1) } } public fn main(`@Unit` -> `@Int`) requires(true) ensures(true) effects(pure) { drain(0, 200000) } """ result = _compile_ok(source) assert re.search(r"return_call \$drain(?![A-Za-z0-9_])", result.wat), ( "a guarded self-recursive tail call must keep return_call" ) # Without TCO this depth exhausts the native stack. assert _run(source, fn="main") == 200000Note the asymmetric slot use:
decreases(@Int.1)measures the counter while@Int.0accumulates, so a swapped slot mapping changes the result rather than staying green.🤖 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_decreases_guard.py` around lines 145 - 180, Add a regression test alongside TestNonTerminatingTraps named test_guarded_self_tail_keeps_return_call that compiles a guarded self-recursive drain function with decreases(`@Int.1`) and an accumulating `@Int.0`, asserts the generated WAT retains return_call $drain, and runs a sufficiently deep counter to verify constant-stack execution and the expected result. Use asymmetric argument roles so slot-order regressions are detected.Source: Path instructions
🤖 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 `@FAQ.md`:
- Line 252: Update the test count from 8,558 to 8,639 in FAQ.md at lines
252-252. README.md at lines 266-266 and ROADMAP.md at lines 15-15 already use
the correct count and require no direct changes.
In `@spec/05-functions.md`:
- Line 162: Revise the self-recursion statement in the tail-call optimization
documentation to qualify the constant-stack guarantee: it applies only when the
self-tail site is successfully translated. Document that when
_dec_self_tail_prefix returns None, _compile_fn lowers the self-targeted
return_call to call; the existing entry guard still checks the measure on each
re-entry, but execution uses the native stack.
In `@vera/codegen/contracts.py`:
- Around line 888-904: Snapshot the rank-helper accumulator at the start of the
enclosing component-processing method, and restore that snapshot before every
early return caused by translation failure, unsupported measure type, missing
ADT name, or missing rank helper. Apply the same rollback discipline to the
related _dec_self_tail_prefix path so partial processing cannot leave committed
helpers behind.
- Around line 1033-1048: Apply the same rollback/checkpoint pattern used by the
entry loop to the component loop building comp_values. Ensure any helpers
registered through _dec_rank_helper for earlier expressions are removed when a
later translation, type, ADT-name, or rank-helper lookup returns None, so failed
compilation leaves no unused helper registrations.
In `@vera/README.md`:
- Line 135: Update the contracts.py module-map entry in README.md to mention
runtime enforcement of decreases clauses, including the associated
termination-state handling, while preserving the existing description of runtime
pre/postconditions and old state snapshots.
---
Outside diff comments:
In `@vera/codegen/contracts.py`:
- Line 1: Update both measure-component loops in the relevant
contract-generation methods to snapshot self._dec_rank_helpers before iteration
and restore that snapshot before every early return (including all three returns
in the first loop and each return None in the second). Preserve helpers only
when the complete loop succeeds, preventing orphaned rank helpers from being
emitted without a corresponding guard.
---
Duplicate comments:
In `@tests/test_codegen_decreases_guard.py`:
- Around line 145-180: Add a regression test alongside TestNonTerminatingTraps
named test_guarded_self_tail_keeps_return_call that compiles a guarded
self-recursive drain function with decreases(`@Int.1`) and an accumulating `@Int.0`,
asserts the generated WAT retains return_call $drain, and runs a sufficiently
deep counter to verify constant-stack execution and the expected result. Use
asymmetric argument roles so slot-order regressions are detected.
🪄 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: 2c5a5319-578d-4eef-88fa-41db1dd3713e
⛔ Files ignored due to path filters (8)
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/**examples/gc_pressure.verais excluded by!**/*.veratests/conformance/ch05_decreases_float_rejected.verais excluded by!**/*.veratests/conformance/ch05_decreases_guard.verais excluded by!**/*.vera
📒 Files selected for processing (21)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/05-functions.mdtests/conformance/manifest.jsontests/test_codegen_decreases_guard.pytests/test_verifier_adt_decreases.pyvera/README.mdvera/_since.pyvera/checker/core.pyvera/codegen/assembly.pyvera/codegen/contracts.pyvera/codegen/core.pyvera/codegen/functions.pyvera/errors.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
|
@coderabbitai On the three outside-diff findings: all fixed in b34c082. (1) TESTING.md's check_site_assets entries — both the one-line script row and the test_build_site row — now document check_fact_coherence() and its docs/index.html↔docs/index.md validation. (2) Both measure-component loops in vera/codegen/contracts.py (entry and self-tail prefix) snapshot the rank-helper accumulator and restore it on every early return; the escaped helpers were internally valid dead code rather than dangling references, rolled back regardless so the helper⇔guard invariant is total. (3) tests/test_codegen_decreases_guard.py's test_guarded_self_tail_keeps_return_call pins return_call in the guarded WAT plus a 300,000-hop constant-stack run with asymmetric counter/accumulator roles. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --no-ext-diff --format=fuller --stat b34c082d
printf '\n--- changed hunks ---\n'
git show --no-ext-diff --format= --unified=35 b34c082d -- \
TESTING.md \
vera/codegen/contracts.py \
tests/test_codegen_decreases_guard.pyLength of output: 126780
The documentation entry is present. Both measure-component loops restore the rank-helper accumulator on early return. The self-tail regression test checks No further action is required. You are interacting with an AI system. |
Reconcile every test total against one live collected number (8,621 from
`pytest --collect-only -q`): the TESTING.md headline parenthetical summed to
8,601, and the per-file table summed to 8,607 because `test_eq_contract_874.py`
carried stale counts (11/378, live 13/430) inside a padded `| 378 |` cell
that `check_doc_counts.py`'s row regex could not match, so the gate never saw
it. Normalising the cell puts all 131 files under the gate, and the headline,
the table sum, and `8,503 passed + 26 stress, 92 skipped` now all agree.
FAQ.md's 8,558 is brought to the same number. The `test_stress.py` row's 16 is
correct and stays: 16 instances live in that file, the suite-wide 26 adds the
10 stress-marked tests in `test_codegen_gc_reclamation.py`.
Fix the `test_exn_redeclaration_rejected` rationale, which still described
`Exn<E>` as codegen-only and absent from `TypeEnv.effects` — this PR is what
changed that. Add `test_exn_needs_no_declaration` for the other half: `throw`
and `handle[Exn<E>]` in scope with no block, which is E330 without the registry
entry.
Complete the §9.5.1 IO operations table with `read_char`, `sleep`, `time` and
`stderr` — the registry has eleven operations and the table listed seven, which
the amended sentence ("the operations above are in scope") now leans on. Correct
§9.5.2: for `State.get` it is the state-type selection that is implicit, not the
`Unit` argument, which is written out as `get(())`.
Assert the `vera effects --json` payload's exact (name, kind) set against both
registries rather than only its length: a count-only check stays green if an
effect is dropped and an ability added, or if a name is emitted under the wrong
`kind`, which is what a consumer discriminates on.
Rename the two `unresolved_db_*_spelling` tests to
`shadow_declaring_other_op_still_gated_*`. Traced which frame reaches
`_check_sql_provenance`: the `ping`-shadow fixture now goes through the
resolved-op gate, not the unresolved-spelling fallback its name claimed. With
the built-in `DB` always registering `query`/`execute`, no source can make that
lookup fail, so the fallback is unreachable from source; it is kept as defence
in depth and both the branch comment and the tests now say so rather than
claiming coverage they no longer provide.
Two findings declined, both on file-wide convention. The `vera/README.md` module
map spells every indented row with leading spaces inside the code span, so
converting one row for MD038 breaks the convention (identical findings were
declined on #1178 and #1179). MD040 on the §7.2 fences: `spec/07-effects.md`
has 0 ```vera and 42 bare fences, the spec has 94 against 657, and no
markdownlint runs in pre-commit or CI — tagging three fences in a chapter with
none makes it less consistent, not more.
Co-Authored-By: Claude <noreply@anthropic.invalid>
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)
vera/codegen/contracts.py (1)
887-915: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winDuplicated rank-helper rollback loop across two call sites.
_compile_decreases_entryand_dec_self_tail_prefixeach carry a near-identical loop that translates everydecreases()component, resolves ADT ranks via_dec_rank_helper, and rolls backself._dec_rank_helpersto a pre-loop snapshot on any failure. This duplication is exactly why the rollback fix needed two separate review rounds to land — one per copy. Extract one shared_dec_translate_measure(ctx, contract, env) -> list[list[str]] | Nonehelper that both call sites use, so the rollback discipline is written once.
vera/codegen/contracts.py#L887-L915: replace the inline loop in_compile_decreases_entrywith a call to the shared helper, mappingNonetoreturn [], [], None.vera/codegen/contracts.py#L1044-L1068: replace the inline loop in_dec_self_tail_prefixwith the same shared helper, mappingNonetoreturn None.🤖 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 `@vera/codegen/contracts.py` around lines 887 - 915, Extract the duplicated decreases-component translation and rank-helper rollback logic into a shared _dec_translate_measure(ctx, contract, env) helper returning list[list[str]] | None, preserving the pre-loop snapshot and rollback on every failure. In vera/codegen/contracts.py lines 887-915, update _compile_decreases_entry to call it and map None to return [], [], None; in lines 1044-1068, update _dec_self_tail_prefix to call it and map None to return None.
🤖 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 `@spec/05-functions.md`:
- Around line 160-164: Revise the Tier 3 runtime-checking paragraph to limit
enforcement to statically unproved decreases obligations for which the backend
can generate a supported runtime guard. Qualify the non-terminating-recursion
trap guarantee with the same condition, and explicitly exclude parameterized or
indirectly parameterized ADT measures and functions declaring Exn, preserving
the existing details for supported guards.
---
Outside diff comments:
In `@vera/codegen/contracts.py`:
- Around line 887-915: Extract the duplicated decreases-component translation
and rank-helper rollback logic into a shared _dec_translate_measure(ctx,
contract, env) helper returning list[list[str]] | None, preserving the pre-loop
snapshot and rollback on every failure. In vera/codegen/contracts.py lines
887-915, update _compile_decreases_entry to call it and map None to return [],
[], None; in lines 1044-1068, update _dec_self_tail_prefix to call it and map
None to return None.
🪄 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: c48ee9d6-01d6-49f4-895e-80bda49a3175
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (9)
AGENTS.mdFAQ.mdREADME.mdROADMAP.mdTESTING.mdspec/05-functions.mdtests/test_codegen_decreases_guard.pyvera/README.mdvera/codegen/contracts.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
b34c082 to
e93b10d
Compare
Reconcile every test total against one live collected number (8,621 from
`pytest --collect-only -q`): the TESTING.md headline parenthetical summed to
8,601, and the per-file table summed to 8,607 because `test_eq_contract_874.py`
carried stale counts (11/378, live 13/430) inside a padded `| 378 |` cell
that `check_doc_counts.py`'s row regex could not match, so the gate never saw
it. Normalising the cell puts all 131 files under the gate, and the headline,
the table sum, and `8,503 passed + 26 stress, 92 skipped` now all agree.
FAQ.md's 8,558 is brought to the same number. The `test_stress.py` row's 16 is
correct and stays: 16 instances live in that file, the suite-wide 26 adds the
10 stress-marked tests in `test_codegen_gc_reclamation.py`.
Fix the `test_exn_redeclaration_rejected` rationale, which still described
`Exn<E>` as codegen-only and absent from `TypeEnv.effects` — this PR is what
changed that. Add `test_exn_needs_no_declaration` for the other half: `throw`
and `handle[Exn<E>]` in scope with no block, which is E330 without the registry
entry.
Complete the §9.5.1 IO operations table with `read_char`, `sleep`, `time` and
`stderr` — the registry has eleven operations and the table listed seven, which
the amended sentence ("the operations above are in scope") now leans on. Correct
§9.5.2: for `State.get` it is the state-type selection that is implicit, not the
`Unit` argument, which is written out as `get(())`.
Assert the `vera effects --json` payload's exact (name, kind) set against both
registries rather than only its length: a count-only check stays green if an
effect is dropped and an ability added, or if a name is emitted under the wrong
`kind`, which is what a consumer discriminates on.
Rename the two `unresolved_db_*_spelling` tests to
`shadow_declaring_other_op_still_gated_*`. Traced which frame reaches
`_check_sql_provenance`: the `ping`-shadow fixture now goes through the
resolved-op gate, not the unresolved-spelling fallback its name claimed. With
the built-in `DB` always registering `query`/`execute`, no source can make that
lookup fail, so the fallback is unreachable from source; it is kept as defence
in depth and both the branch comment and the tests now say so rather than
claiming coverage they no longer provide.
Two findings declined, both on file-wide convention. The `vera/README.md` module
map spells every indented row with leading spaces inside the code span, so
converting one row for MD038 breaks the convention (identical findings were
declined on #1178 and #1179). MD040 on the §7.2 fences: `spec/07-effects.md`
has 0 ```vera and 42 bare fences, the spec has 94 against 657, and no
markdownlint runs in pre-commit or CI — tagging three fences in a chapter with
none makes it less consistent, not more.
Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai On the outside-diff extraction: done in 68605e5 — _dec_translate_measure is the single home for the component translation, ADT ranking, and snapshot/rollback discipline; _compile_decreases_entry maps its None to ([], [], None) and _dec_self_tail_prefix maps it to None, exactly as proposed. Guard suite 23/23, mypy clean. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --no-ext-diff --format=fuller --stat 68605e5f
printf '\n--- relevant diff ---\n'
git show --no-ext-diff --format= --unified=25 68605e5f -- vera/codegen/contracts.py
printf '\n--- named symbols on PR branch ---\n'
ast-grep outline vera/codegen/contracts.py --items all --type method,function --match 'dec_translate_measure|compile_decreases_entry|dec_self_tail_prefix'Length of output: 100742
I did not independently run the guard suite or mypy in the sandbox. ✏️ Learnings added
You are interacting with an AI system. |
Adversarial review — independent attacker, 18 repro programs, branch tip 68605e5Verdict: sound-with-findings. The guard machinery itself survived every structural attack — per-clone globals for monomorphized instantiations, module/where-helper name mangling, interleaved cross-instantiation nesting, 1M-depth self-tail TCO, the amended lexicographic semantics verified component-by-component against the WAT, State-effect interleaving, F1 (High — pre-existing verifier bug, made observable by this PR). The verifier's F2 (Medium-High — this PR's own gap). A guarded function tail-calling an unguarded trampoline that tail-calls back loops forever with zero checks: the unguarded-target tail branch prepends the restores (chain zeroed) and keeps F3 (Medium — inherent, newly exposed). Measure evaluation uses machine i64 arithmetic where Z3 proved over unbounded integers: F4 (Low — fidelity note). Spec §5.6.1's runtime paragraph implies only unproved obligations are enforced; the implementation guards all tiers (belt-and-braces — precisely what made F1/F3 observable). Disposition: reword the spec sentence to match the implementation; the dynamic-re-entry-vs-static-call-site strengthening is already disclosed by the "on each re-entry" wording. Clean lenses, for the record: lexicographic deciding-component semantics (later components unconstrained — confirmed clean; deciding-component floor — confirmed trap), mono-clone guard isolation, imported/where-helper naming, i32_pair self-tail capture ordering, mutual-tail demotion is not a regression (v0.1.8 parity confirmed), Exn is the only unwind mechanism (State clauses are single-tail-resume or skip), no Fixes for F1/F2 land in this PR before any merge-ready call; F3/F4 land as documentation in the same round. |
Reconcile every test total against one live collected number (8,621 from
`pytest --collect-only -q`): the TESTING.md headline parenthetical summed to
8,601, and the per-file table summed to 8,607 because `test_eq_contract_874.py`
carried stale counts (11/378, live 13/430) inside a padded `| 378 |` cell
that `check_doc_counts.py`'s row regex could not match, so the gate never saw
it. Normalising the cell puts all 131 files under the gate, and the headline,
the table sum, and `8,503 passed + 26 stress, 92 skipped` now all agree.
FAQ.md's 8,558 is brought to the same number. The `test_stress.py` row's 16 is
correct and stays: 16 instances live in that file, the suite-wide 26 adds the
10 stress-marked tests in `test_codegen_gc_reclamation.py`.
Fix the `test_exn_redeclaration_rejected` rationale, which still described
`Exn<E>` as codegen-only and absent from `TypeEnv.effects` — this PR is what
changed that. Add `test_exn_needs_no_declaration` for the other half: `throw`
and `handle[Exn<E>]` in scope with no block, which is E330 without the registry
entry.
Complete the §9.5.1 IO operations table with `read_char`, `sleep`, `time` and
`stderr` — the registry has eleven operations and the table listed seven, which
the amended sentence ("the operations above are in scope") now leans on. Correct
§9.5.2: for `State.get` it is the state-type selection that is implicit, not the
`Unit` argument, which is written out as `get(())`.
Assert the `vera effects --json` payload's exact (name, kind) set against both
registries rather than only its length: a count-only check stays green if an
effect is dropped and an ability added, or if a name is emitted under the wrong
`kind`, which is what a consumer discriminates on.
Rename the two `unresolved_db_*_spelling` tests to
`shadow_declaring_other_op_still_gated_*`. Traced which frame reaches
`_check_sql_provenance`: the `ping`-shadow fixture now goes through the
resolved-op gate, not the unresolved-spelling fallback its name claimed. With
the built-in `DB` always registering `query`/`execute`, no source can make that
lookup fail, so the fallback is unreachable from source; it is kept as defence
in depth and both the branch comment and the tests now say so rather than
claiming coverage they no longer provide.
Two findings declined, both on file-wide convention. The `vera/README.md` module
map spells every indented row with leading spaces inside the code span, so
converting one row for MD038 breaks the convention (identical findings were
declined on #1178 and #1179). MD040 on the §7.2 fences: `spec/07-effects.md`
has 0 ```vera and 42 bare fences, the spec has 94 against 657, and no
markdownlint runs in pre-commit or CI — tagging three fences in a chapter with
none makes it less consistent, not more.
Co-Authored-By: Claude <noreply@anthropic.invalid>
dec11b3 to
e101650
Compare
E525 said a Tier-3 termination metric "will be checked at runtime"; decreases had no runtime lowering, so a non-terminating recursion passed check, passed verify, and hung at run (VeraBench v0.0.18, VB-T4-006). Every decreases function now carries the guard: entry saves the per-function chain globals, evaluates the measure (scalars by value, concrete ADTs by a generated structural-size helper, lexicographic tuples componentwise per spec 5.6.1), and traps through the contract-violation channel unless a re-entry strictly decreases while staying non-negative; every exit restores the saved state. Self-recursive tail calls keep TCO: the return_call is prefixed with a call-site check (arguments captured, measure evaluated over them against the live chain globals, activation state closed out, arguments re-pushed), so the documented pure-iteration idiom keeps its constant-stack 1M-depth property (#517 batteries pass unchanged) — closing #1176's ask in the same change. Mutual-tail calls between guarded functions demote to plain calls (no restore placement both preserves and unwinds the chain across an elided frame); an untranslatable site demotes identically, never a partial check. Alongside: new E127 rejects measures with no well-founded ordering (Float64/String/Bool were silently decorative; spec 5.6.1(3) is normative), spec 5.6.1's own lexicographic Ackermann example is corrected (as printed its permuted arguments cycled forever), the well-founded list gains ADTs, and a parameterized ADT measure is honestly unguarded (generic layouts do not describe concrete construction — #1177) rather than wrongly ranked. Closes #1172 Closes #1176 Co-Authored-By: Claude <noreply@anthropic.invalid>
…wrap, skip net
Review round (15 findings, 4 behavioral — each live-reproduced first):
- A failed rank walk now rolls back EVERY helper it committed
(snapshot/restore, the _lift_pending_closures discipline): a nested
helper completed through the reservation short-circuit could survive
calling the deleted name, killing the whole compile at wat2wasm on a
check-green program.
- An Exn-declaring function gets no runtime guard: a thrown exception
unwinds past the exit restores, and the stale chain state trapped a
later terminating call. _dec_declares_exn gates both the entry
emission and the _dec_collect pre-pass so tail-call patches stay in
sync; spec §5.6.1, SKILL, and CHANGELOG state the limit.
- The E127 well-foundedness check unwraps nested refinement layers in a
loop; { { Int | P } | Q } no longer draws a spurious error.
- _compile_decreases_entry now sits in the contract-predicate
degradation net (CodegenSkip -> E602, CodegenInvariantError -> E699),
matching the sibling pre/postcondition paths.
Tests: four RED-first regressions plus a lexicographic component-order
mirror (asymmetric lexy/Ackermann entries; reversing the guard's
component order is mutation-verified RED), boundary-safe WAT pins,
tempfile unlink, unused helper removed. Docs: TESTING enumeration and
counts regenerated from live runs (incl. the stale E219 -> actual E217),
AGENTS negative lists synced, guard-limit qualifications everywhere.
Co-Authored-By: Claude <noreply@anthropic.invalid>
- Spec section 5.6.1: the runtime lexicographic rule now states the true semantics (first differing component strictly less AND non-negative, earlier components equal, later components checked on the hop where they decide) instead of an ambiguous componentwise claim; the Float64 rejection names the real reason (no well-founded ordering the runtime can check, NaN/infinities unordered, floats never reach the runtime check); the parameterized-ADT and Exn limitation bullets no longer imply Tier 3 is forced (static classification is independent; only the runtime fallback is absent); the self-tail TCO claim is qualified by the untranslatable-site demotion; the well-foundedness requirement uses MUST per the chapter's RFC 2119 convention. - Both measure-component loops snapshot and restore the rank-helper accumulator on every early return, making "a helper exists iff a guard calls it" total rather than incidental (the escaped helpers were valid-but-unused dead code, not dangling). - New test pins the #517 property in both directions: return_call survives in the guarded self-tail WAT, and a 300,000-hop run completes — plain-call recursion at that depth exhausts the native stack, so finishing is the constant-stack proof. Asymmetric counter/accumulator roles make a slot-order swap trap. - AGENTS.md conformance description no longer enumerates companions (17 fixtures import; a non-enumerating sentence cannot drift); FAQ test count refreshed; TESTING gains the 874 row correction and the check_fact_coherence() documentation; vera/README's contracts.py row describes the guard machinery. Co-Authored-By: Claude <noreply@anthropic.invalid>
Review round: the spec's Runtime checking paragraph promised enforcement unconditionally in its lead and walked it back in bullets — the lead now carries the supported-guard condition and names the exclusions, and the trap guarantee is scoped to guarded functions. The duplicated component-translation/rank-rollback loops collapse into one _dec_translate_measure helper shared by the entry check and the self-tail site check. Co-Authored-By: Claude <noreply@anthropic.invalid>
Independent adversarial review of the guard (18 attack programs; the full report is on the PR): - F1: the verifier's decreases call-walker skipped HandleExpr (body, clauses, state exprs), AnonFn bodies, constructor/qualified/module call arguments, IndexExpr, ArrayLit, InterpolatedString, and assert/assume — a measure-violating recursive call hidden there rode a false Tier-1 proof that the new guard exposed as a verify-green run-time trap. The walker now descends into every value-carrying node, conservatively (no path-condition extension). Two review repro programs pin the obligations as not-verified. - F2: a guarded function tail-calling an UNGUARDED trampoline that tail-calls back looped forever with zero checks — the old prepend-restores-then-return_call sequence zeroed the chain before every re-entry. Guarded-to-unguarded tail sites now demote to plain calls (the mutual-tail treatment); the review's trampoline repro traps instead of hanging. - F3 (documented limitation): the measure evaluates with machine i64 arithmetic where the prover reasons over unbounded integers, so a near-edge measure can overflow-trap on a proved obligation — KNOWN_ISSUES limitation row + spec note. - F4: spec section 5.6.1's runtime paragraph now states the guard runs for every tier (belt-and-braces), not only Tier 3. Co-Authored-By: Claude <noreply@anthropic.invalid>
e101650 to
30a428b
Compare
|
@coderabbitai The remaining outside-diff finding (duplicated rank-helper rollback loop in vera/codegen/contracts.py) is fixed in e583b17: |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --no-ext-diff --format=fuller --stat e583b170
printf '\n--- relevant commit diff ---\n'
git show --no-ext-diff --format= --unified=30 e583b170 -- vera/codegen/contracts.py
printf '\n--- relevant symbols on PR branch ---\n'
ast-grep outline vera/codegen/contracts.py \
--items all \
--type method,function \
--match 'dec_translate_measure|compile_decreases_entry|dec_self_tail_prefix'
printf '\n--- relevant call and return contexts ---\n'
rg -n -A18 -B12 \
'def _dec_translate_measure|def _compile_decreases_entry|def _dec_self_tail_prefix|_dec_translate_measure\(' \
vera/codegen/contracts.pyLength of output: 1168 🏁 Script executed: #!/bin/bash
set -euo pipefail
gh api \
-H 'Accept: application/vnd.github+json' \
'repos/aallan/vera/commits/e583b170' \
--jq '{
sha,
html_url,
commit: {
message: .commit.message,
author: .commit.author
},
files: [
.files[]
| select(.filename == "vera/codegen/contracts.py")
| {
filename,
status,
additions,
deletions,
patch
}
]
}'Length of output: 7279
On a translation failure, The remaining outside-diff finding is addressed. You are interacting with an AI system. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --no-ext-diff --format=fuller --stat b34c082d
printf '\n--- requested file diffs ---\n'
git show --no-ext-diff --format= --unified=20 b34c082d -- \
TESTING.md \
vera/codegen/contracts.py \
tests/test_codegen_decreases_guard.pyLength of output: 795 🏁 Script executed: #!/bin/bash
set -euo pipefail
gh api \
-H 'Accept: application/vnd.github+json' \
'repos/aallan/vera/commits/b34c082d' \
--jq '{
sha,
html_url,
files: [
.files[]
| select(
.filename == "TESTING.md"
or .filename == "vera/codegen/contracts.py"
or .filename == "tests/test_codegen_decreases_guard.py"
)
| {filename, status, additions, deletions, patch}
]
}'Length of output: 21593
Both measure-component loops snapshot and restore
The three outside-diff findings are addressed. You are interacting with an AI system. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --no-ext-diff --format='commit %H%n%s' --stat b34c082d
printf '\n--- targeted diff ---\n'
git show --no-ext-diff --format= --unified=20 b34c082d -- \
TESTING.md \
vera/codegen/contracts.py \
tests/test_codegen_decreases_guard.py
printf '\n--- relevant symbols at commit ---\n'
git show b34c082d:vera/codegen/contracts.py > /tmp/contracts-b34c082d.py
ast-grep outline /tmp/contracts-b34c082d.py \
--items all --type method,function \
--match 'compile_decreases_entry|dec_self_tail_prefix|dec_translate_measure'
printf '\n--- targeted source contexts at commit ---\n'
git show b34c082d:TESTING.md | rg -n -C3 'check_site_assets|check_fact_coherence|test_build_site'
git show b34c082d:vera/codegen/contracts.py | rg -n -C10 \
'def _compile_decreases_entry|def _dec_self_tail_prefix|rank_helpers|_dec_rank_helpers'
git show b34c082d:tests/test_codegen_decreases_guard.py | rg -n -C12 \
'def test_guarded_self_tail_keeps_return_call|return_call|300_000|300000'Length of output: 1534 🏁 Script executed: #!/bin/bash
set -euo pipefail
gh api \
-H 'Accept: application/vnd.github+json' \
'repos/aallan/vera/commits/b34c082d' \
--jq '{
sha,
html_url,
message: .commit.message,
files: [
.files[]
| select(
.filename == "TESTING.md"
or .filename == "vera/codegen/contracts.py"
or .filename == "tests/test_codegen_decreases_guard.py"
)
| {filename, status, additions, deletions, patch}
]
}'Length of output: 23440
Both component loops snapshot and restore
The three outside-diff findings are addressed. You are interacting with an AI system. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '--- commit summary ---'
git show --no-ext-diff --format=fuller --stat e583b170
printf '%s\n' '--- relevant commit diff ---'
git show --no-ext-diff --format= --unified=35 e583b170 -- vera/codegen/contracts.py
printf '%s\n' '--- method outline ---'
ast-grep outline vera/codegen/contracts.py \
--items all \
--type method,function \
--match 'dec_translate_measure|compile_decreases_entry|dec_self_tail_prefix'
printf '%s\n' '--- implementation contexts ---'
rg -n -A100 -B8 \
'def _dec_translate_measure|def _compile_decreases_entry|def _dec_self_tail_prefix' \
vera/codegen/contracts.pyLength of output: 1190 🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '--- current revision ---'
git rev-parse HEAD
git status --short --branch
printf '%s\n' '--- relevant method outline ---'
ast-grep outline vera/codegen/contracts.py \
--items all \
--type method,function \
--match 'dec_translate_measure|compile_decreases_entry|dec_self_tail_prefix'
printf '%s\n' '--- method bodies and call sites ---'
rg -n -A130 -B10 \
'def _dec_translate_measure|def _compile_decreases_entry|def _dec_self_tail_prefix|_dec_translate_measure\(' \
vera/codegen/contracts.pyLength of output: 19502 🏁 Script executed: #!/bin/bash
set -euo pipefail
gh api \
-H 'Accept: application/vnd.github+json' \
'repos/aallan/vera/commits/e583b170' \
--jq '{
sha,
html_url,
commit: {message: .commit.message},
files: [
.files[]
| select(.filename == "vera/codegen/contracts.py")
| {filename, status, patch}
]
}'Length of output: 7027
This removes the duplicated rollback loops and preserves rollback on every failed translation path. The outside-diff finding is addressed. You are interacting with an AI system. |
CodeRabbit round on PR #1188: TESTING.md's test-level inventory had drifted across three merges — the check-level prose lists and the level-limited skip table were missing ch05_reserved_fn_name_rejected (E153, this PR), ch07_old_outside_ensures_rejected (E174, #1180), and ch09_builtin_effect_redefinition_rejected (E152, #1182), and the skip-table rows for ch05_decreases_float_rejected (E127, #1179) were absent too. Regenerated against the manifest: twenty-eight check-level programs, twenty-one negatives, 69 level-limited skips, and the table verified complete for every check-level fixture. FAQ.md's test count catches up to the live 8,724 (the doc-counts oracle does not gate that line — noted for the wave-4 hardening). Skip-changelog: documentation-inventory reconciliation only, no compiler change Co-Authored-By: Claude <noreply@anthropic.invalid>
…1202) Four review lenses (code review, test-coverage mutation battery, comment-accuracy audit, silent-failure hunt) produced this round: - The nat-binding walker now descends assert/assume CONDITIONS — a provably-negative narrowing argument inside one (`assert(takes_nat(0 - 5) > 0)`) recorded nothing and passed silently; it now fires the same loud E503 as direct position — and carries the #597 WALKER_COVERAGE marker, so check_walker_coverage.py (now 13 walkers) enforces its case split from here on. - Fourteen mutation-derived tests close the review's headline hole: a combined mutant deleting BOTH of the nat-binding walker's new container arms and walking closures with the dishonest enclosing env passed the entire suite. The new battery kills it: scope-honesty pins for the nat-binding walker (closure and handler-clause narrowings never prove against the outer requires), enclosing-scope precision pins (handle body, handler state-init, forall domain), the exists-predicate leg, clause state-update descent, refined closure narrowing disclosure (tier3_unguarded + E506), loud-parity for assert/index in closures, and the ensures-position quantifier shape. A compile-and-run differential proves the interior closure let-guard the tier3 records claim (TestClosureInteriorBindingDifferential779). - Comment/doc accuracy: the stale "AnonFn stays a terminal" and "#1179 mirror" comments now describe the descent; OldExpr/NewExpr dispositions are per-walker-accurate; the spec §7.5.1 pointer, FAQ's pre-fix parenthetical, the primitive-ops class docstring, and the universal-Tier-3 over-claims in spec/comment prose are all corrected to the slot-dependent/literal split; KNOWN_ISSUES #439's headline narrows to value-dependent contracts; clause-scope comments note the handler state slot. - The review also surfaced a pre-existing false Tier-1 (State<Nat> cell writes neither obligated nor guarded) — filed as #1203 with a KNOWN_ISSUES row and a #754 cross-link; deferred from this PR because the fix is codegen guard emission with its own blast radius, not walker scope. The silent-failure hunt's HIGH finding is fixed: a NESTED constructor sub-pattern narrowing on an unprojectable scrutinee (under the descent, every match in a closure) silently vanished from the stream while codegen's per-bind guard trapped it — verify-clean, bare anon_0 trap. The nested branch now records the same honest static fallbacks as its direct siblings (nat: guarded tier3, probe-verified in both positions; refined: unguarded E506 — the refined nested bind genuinely does NOT trap, so #765 narrows to that residual, probe-verified and commented; widen: guarded tier3), mutation-validated with a run differential. Four stale `pragma: no cover` annotations on now-hot fallback branches are removed, and two pre-existing discoveries are tracked: #1203 (State<Nat> cell writes unobligated+unguarded, KNOWN_ISSUES row) and #1204 (array-domain quantifiers fail WASM translation, KNOWN_ISSUES row). The nested-closure differential pin tightens to an exact-count assertion, and the CHANGELOG names the dominant new corpus obligation kind (int_overflow). Co-Authored-By: Claude <noreply@anthropic.invalid>
1 participant
E525told users a Tier-3 termination metric "will be checked at runtime". Nothing checked it:decreaseshad no runtime lowering at all, so a non-terminating recursion passedcheck, passedverify, and hung atrun(VeraBench v0.0.18,VB-T4-006). Its siblings E521–E524 fall back onrequires/ensures, which emit real assertions — E525 was the one member of the family whose promised fallback was empty.The guard
Every function with a
decreasesclause now carries a runtime termination guard, mirroring_verify_decreases's Z3 rule:$dec_prev_<f>_<k>/$dec_active_<f>globals) is saved to locals; the measure components are evaluated over the parameters — scalars by value, an ADT component through a generated structural-size helper ($dec_size_<T>); if a previous activation is live, the components must decrease lexicographically while staying non-negative (spec §5.6.1's tuples — the runtime side now handles what the prover still reads only the first component of), or the program traps through$vera.contract_failwith a message naming the function.return_callis prefixed with a call-site check: arguments captured into locals, the measure evaluated over them against the live chain globals, the activation's state closed out (the$gc_sppattern), arguments re-pushed, transfer. The chain rides the site checks at constant stack depth. A mutual-tail call between two guarded functions falls back to a plain call (with the frame elided, no restore placement both preserves the chain and unwinds it); an untranslatable site demotes the same way — a check is never partially emitted. Closes the TCO-restoration follow-up in the same change.Alongside, because building it surfaced them
E127: a measure with no well-founded ordering (Float64halves forever without crossing a floor;String/Boolhave no order) was accepted silently, making the clause decorative. Spec §5.6.1(3) is normative; the checker now rejects, with a conformance negative. Zero collateral across the corpus.A(1,1) → A(2,0)cycle, "protected" by the empty promise this PR closes. Corrected, and the classical version is the new run-level conformance program (with a structural ADT measure alongside).Honest limits (disclosed, not silent)
List<Int>, or a concrete type whose recursion rides a parameterized field) gets no guard: the registered generic layout does not describe concrete construction, and both wrong alternatives were caught live — a frozen rank false-trappingch02_adt_recursive, and a wild pointer walk on the base-name variant. Such measures stay statically checked and Tier-3-disclosed; per-instantiation helpers (the$eq_<type>pattern) are Runtime-rank parameterized ADT decreases measures (per-instantiation size helpers) #1177, with a KNOWN_ISSUES limitation row.Tests
tests/test_codegen_decreases_guard.py(17): six non-terminating shapes trap instead of hanging (the issue's ADT repro, constant-measure tail call, growing measure, negative floor, lexicographic violation, mutualwhererecursion — subprocess-with-timeout, RED as hangs pre-fix); terminating programs stay clean with the guard emitted (Tier-1 countdown, corrected Ackermann, sequential siblings pinning the exit restore, concrete ADT measure); the tier3-obligation ⇒ emitted-guard differential the issue asked for; E127 rejection × 4 + acceptance of the well-founded family; the parameterized-measure no-guard pin. Five-mutant matrix (entry check, exit restore, lex chain, rank helper, floor leg) — each killed by a distinct named test. The existing #517/#549/#983 TCO batteries pass unchanged, pinning the preserved 1M-depth property.Conformance: 169 → 171 (
ch05_decreases_guardrun-level positive,ch05_decreases_float_rejectedE127 negative).Closes #1172
Closes #1176
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
decreasesclauses using scalar, structural ADT, and lexicographic measures.Documentation
Tests