spec: correct §11.8 — contracts are always emitted regardless of tier (#958)#1023
Conversation
…#958) Spec §11.8 claimed Tier-1-proved contracts are omitted from the compiled output, contradicting both the rest of the chapter (§11.2's 'type-driven, not tier-driven') and the code (vera/codegen/contracts.py has no notion of tiers). Correct it to always-emit: every non-trivial contract compiles to a runtime check regardless of the verifier's tier; a Tier-1 proof means the check provably never fires, not that it is absent. This is the deliberate backstop that keeps a false Tier-1 (e.g. the open #1017) a loud runtime trap rather than a silent wrong answer. Pin the invariant with a differential test (Tier-1 verify + contract_fail present in the WAT) so the omission cannot be silently introduced; align TESTING's tier explanation; retire the #958 ROADMAP row. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 1 minute Your organization has reached its usage spending cap. Adjust your spending cap in the billing tab. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
📝 WalkthroughWalkthroughThe change documents tier-agnostic runtime contract emission, adds a Tier-1 regression test confirming the generated guard remains present, updates testing coverage descriptions and counts, and removes the completed roadmap item. ChangesContract guard alignment
Estimated code review effort: 2 (Simple) | ~10 minutes Suggested labels: 🚥 Pre-merge checks | ✅ 8✅ Passed checks (8 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 #1023 +/- ##
=======================================
Coverage 93.51% 93.51%
=======================================
Files 96 96
Lines 32019 32019
Branches 456 456
=======================================
Hits 29943 29943
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 corrects spec §11.8 to match the actual code generation behaviour: every non-trivial contract is compiled as a runtime check regardless of the verifier's tier, and it adds a differential regression test that pins this always-emit backstop.
Confidence Score: 5/5Safe to merge — the change corrects a false spec claim, all doc counters are consistent, and the new regression test correctly pins the always-emit behaviour. All code changes are either documentation or a single well-scoped regression test. The spec correction is empirically validated in the PR description, existing tests confirm the always-emit path, and the new test adds a differential pin using the established _verify + WAT inspection pattern already present across the suite. The new test in tests/test_codegen_contracts.py calls _compile instead of _compile_ok, which would produce an opaque assertion failure rather than surfacing compile diagnostics if the source ever stops compiling cleanly.
|
| Filename | Overview |
|---|---|
| spec/11-compilation.md | §11.8 corrected to always-emit semantics; Tier 1/3 distinction now accurately described as a static-proof classification, not a code-emission gate. |
| tests/test_codegen_contracts.py | Adds regression test pinning always-emit backstop for Tier-1-proved contracts; uses _compile instead of _compile_ok, which would obscure diagnostics on a compile failure. |
| CLAUDE.md | Release workflow clarified: HISTORY.md one-liners are added at release-cut time, not in the issue-closing PR; speculative pending rows explicitly prohibited. |
| CHANGELOG.md | Documentation section added under [Unreleased] for the §11.8 spec correction; entry is accurate and well-referenced. |
| TESTING.md | Test count updated to 7,405 (7,309 passed + 26 stress + 70 skipped); contract verification coverage description updated to reflect always-emit semantics. |
| ROADMAP.md | Removes the closed #958 entry and updates test count; consistent with project workflow. |
| README.md | Test count updated from 7,404 to 7,405 to reflect the new regression test. |
Reviews (3): Last reviewed commit: "docs: correct the HISTORY-one-liner timi..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
![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 `@tests/test_codegen_contracts.py`:
- Line 595: Update the assertion in the relevant code-generation contract test
to verify the emitted instruction `call $vera.contract_fail`, rather than only
searching for the `contract_fail` symbol name. Use a boundary-safe exact
instruction match against the WAT returned by `_compile(src).wat`, ensuring
imports alone cannot satisfy the test.
🪄 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: 080b3064-691c-41ae-827b-a8c7c6fca81e
📒 Files selected for processing (6)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdspec/11-compilation.mdtests/test_codegen_contracts.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
CodeRabbit flagged that `"contract_fail" in wat` also matches the always-present import declaration, so the differential could pass even if the guard call were omitted. Assert the exact `call $vera.contract_fail` instruction (boundary-safe, one line stripped) so the pin genuinely fails if the tier-omission were ever implemented. Co-Authored-By: Claude <noreply@anthropic.invalid>
…e review) The `contract_fail` host import is lazy — emitted only when a guard is actually called — so the prior comment's claim that "a substring check would pass on the import alone" was inaccurate: with no call there is no import either. Reworded to state the real reason for asserting the exact `call $vera.contract_fail` instruction: a direct check that the guard is invoked, rather than a substring match on the symbol. Co-Authored-By: Claude <noreply@anthropic.invalid>
CLAUDE.md said to add a HISTORY.md one-liner "when an issue is closed by a PR", which mandates a row this PR (riding [Unreleased]) does not add and which Greptile flagged. The doc was wrong, not the PR: HISTORY version-rows are written at release-cut time, keyed to a shipped vX.Y.Z. A fix riding CHANGELOG [Unreleased] is recorded there and rolls into the HISTORY row when the version is tagged. Clarify the rule and warn against the speculative "Pending" row that was reverted on #1020. Co-Authored-By: Claude <noreply@anthropic.invalid>
1 participant
Summary
Fixes the spec to match code generation (maintainer's decision: keep always-emitting).
Spec §11.8 claimed:
That is false, and it contradicted the rest of the same chapter (§11.2: the guards are "type-driven, not tier-driven … emitted at every site regardless of the verifier's tier"). Code generation is tier-agnostic —
cmd_compilenever calls the verifier andvera/codegen/contracts.pyhas no notion of tiers — so every non-trivial contract is compiled as a runtime check regardless of the verifier's tier; only trivial contracts (§11.8.1) are eliminated.This isn't cosmetic. The always-emit guard is the backstop that keeps a false Tier 1 — a verifier proving something it shouldn't, like the still-open #1017 — a loud runtime trap rather than a silent wrong answer. Implementing §11.8's omission optimisation while any false Tier-1 exists would convert every one into a silent miscompile.
Change
spec/11-compilation.md§11.8 — corrected to always-emit; the Tier 1 / Tier 3 distinction is reframed as static proof, not code emission, cross-referenced to §11.2 and §11.8.1.TESTING.md— aligned the tier explanation (dropped "no runtime overhead").tests/test_codegen_contracts.py— a differential pin: anensures(@Int.result == @Int.0)contract verifies Tier-1 (0 Tier-3), yet the compiled WAT still contains thecontract_failguard. Were §11.8's omission ever implemented, this fails loudly — the invariant is now enforced, not just documented.Validation
Empirically confirmed before writing the spec:
vera verify --jsonreports the contracttier1_verified(0 Tier-3), andvera compile --watstill emitscall $vera.contract_fail+ the postcondition trap.check_spec_examples,check_doc_counts, andcheck_site_assetsall green.Closes #958
🤖 Generated with Claude Code
Summary by CodeRabbit