One boundary-width derivation: mark the throw payload, classify pointer-ness from the base (#1255, #1256, #1269) - #1273
Conversation
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (11)
🔗 Linked repositories identifiedCodeRabbit considers these linked repositories for cross-repo context during reviews:
📝 WalkthroughWalkthroughVera now resolves aliases and refinements for GC-pointer classification and write-boundary widths. Closure indirect calls use declared formal widths. Exception dispatch preserves cell metadata and applies payload-width handling. Regression tests and project metrics were updated. ChangesBoundary correctness
Estimated code review effort: 4 (Complex) | ~45 minutes Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 8✅ Passed checks (8 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## release/v0.1.10 #1273 +/- ##
===================================================
- Coverage 94.05% 94.04% -0.01%
===================================================
Files 100 100
Lines 35594 35616 +22
Branches 458 458
===================================================
+ Hits 33477 33496 +19
- Misses 2104 2107 +3
Partials 13 13
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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 77: Fix the Markdown table row containing
test_closure_boundary_widths_1255_1256_1269.py so embedded refinement separators
are escaped or isolated and markdownlint parses exactly four cells. Preserve the
spacing required by scripts/check_doc_counts.py, and verify all documented
validation scripts continue to pass.
In `@vera/wasm/inference.py`:
- Around line 2237-2257: Update _translate_handle_exn in calls_handlers.py to
obtain family_base through self._boundary_base(type_arg) instead of
independently composing _family_base and _resolve_base_type_name. Preserve the
existing family assignment and all other exception-translation behavior.
🪄 Autofix
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: 898da56f-779e-413a-8d5e-7ca57587269f
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (18)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/test_closure_boundary_widths_1255_1256_1269.pytests/test_closure_lift_boundaries_1234_1235_1245.pytests/test_exn_throw_payload_1268.pyvera/README.mdvera/codegen/assembly.pyvera/codegen/closures.pyvera/codegen/functions.pyvera/wasm/calls.pyvera/wasm/calls_handlers.pyvera/wasm/closures.pyvera/wasm/helpers.pyvera/wasm/inference.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
💤 Files with no reviewable changes (1)
- KNOWN_ISSUES.md
Adversarial review record — round 1 (
|
Round-1 dispositions (
|
Verify pass (independent,
|
Three burndown defects of one seam: a boundary asks what a declared type IS and answers from something other than that type. refinement or alias over Byte/Bool was rooted on the shadow stack at the closure parameter, return and capture and at the two named-function twins. The issue counted eleven sites; six of them, all in vera/wasm/, are measured to receive names their producers already resolve, and each shares its name with the element size/load/store decisions beside it — resolving one conjunct there would desync the layout from the rooting, so those six are left alone deliberately. The five genuinely syntactic sites now ask `is_gc_pointer_base`, which states the rule once and requires a representation base. The heap-layout invariant the defect was inert behind is enforced at build rather than assumed, and the two constants that create its margin are named where the layout is computed. width from the ARGUMENT while the lifted closure's own signature took it from the declared formal, so a @byte formal fed an int literal registered two incompatible closure_sig types and trapped. The parameters now come from the closure type, through the same walker the result has used since #630; the argument coerces at the boundary instead of dictating it. resolved i32 width, so the width derivation was never wrong; the thrown literal simply defaulted to i64.const because throw's payload was not registered as a @byte write boundary. It is one now, through the same marking every other boundary drives. The #1268 runtime guard on that payload is a separate obligation and is not in this change. Every #1212 boundary holding a type expression resolves its representation base through one derivation (`WasmContext._boundary_base`) rather than each composing its own two hops. Proof: 20 of the new suite's cases are RED on the base commit and all 49 green here; all 254 corpus programs emit byte-identical WAT, against a differential shown to move 23 of them when the pointer rule is mutated. test_exn_throw_payload_1268's satisfying-literal case, static only because of #1269, now runs. Closes #1255 Closes #1256 Closes #1269 Co-Authored-By: Claude <noreply@anthropic.invalid>
Adversarial round 1 found _boundary_base had two consumers where the thesis claims one. Five sites still spelled the composition themselves. Three were refactor-only (calls_handlers' State-cell and Exn-tag bases; the throw payload's call-site hop, which cannot call the named helper because the registry carries a name rather than a type expression, and now says so). Two MEASURABLY DIVERGED and are a behaviour change. The @int->@nat narrowing gate and the @Nat->@int widening gate chased the return alias by NAME, which drops an application's type arguments: under `type Ident<T> = T; type Count = Ident<Nat>;` both answered the bare head `Ident`, neither gate fired, and `f(0 - 5)` returned -5 through the @nat slot — #983's silent negative one spelling over. Both now ask _boundary_base, which resolves the type expression. The refinement exclusion beside the narrowing gate is a separate conjunct and is untouched, so an alias to a refinement keeps its single boundary guard. Reproduced independently before fixing: widen_alias emitted no guard where widen_plain did, and the narrow twin let -5 into a @nat slot. 7 new cases in test_codegen_nat_guards, 3 RED on the previous commit, each parameterised case paired with its unparameterised twin as the oracle plus the refinement-over-application control. Corpus: 0 movers against both the base commit and the previous one, and the 2 programs whose base SPELLING moves are inert for stated reasons (ch02_refinement_base_param_alias's `T`->`Nat` is excluded by the refinement conjunct; scoreboard's `Map`->`Map<String, Int>` is neither gate's value). The harness is shown to reach the gates: forcing the widen gate on moves 16 corpus programs. Also from the round: the cross-module registration-parity test the reviewer named as unprobed (a refined-Byte payload declared and used in a library, with a decoy alias of the same name over a different base in the importer, plus a companion proving the width assertion can go red); TESTING.md pipe escaping; is_gc_pointer_base narrowed to str, the unreachable None branch deleted; the false no-cover pragma on the heap-layout guard removed; the apply_fn Unit-arm comment rewritten to the chain it now consults; and a KNOWN_ISSUES row for #1276, which this work unmasked but does not fix. Co-Authored-By: Claude <noreply@anthropic.invalid>
The #1255 CHANGELOG bullet argued a hypothetical alongside the measurement: that resolving one conjunct at the six already-resolved wasm/ sites would desync layout from rooting. The operative fact is simply that those sites receive names their producers have already resolved — the array-element deciders are handed `Byte`, never the alias — so there is nothing there to fix. Recorded from adversarial round 1. Skip-changelog: reworded an existing [Unreleased] bullet, no behaviour change Co-Authored-By: Claude <noreply@anthropic.invalid>
The verify pass found TestParameterisedAliasReturnGuard1256's _REFINED_OVER_APPLICATION did not discriminate the conjunct it names. Reproduced: with `_refinement_guard_parts` dropped from the narrowing gate the control still passed, because a @nat body into a @Nat-based return is no narrowing leaf at all — the leaf collector returns empty and the absence of `i64.lt_s` holds either way. The parameter is now @int with `requires(@Int.0 >= 18)` and an @Int.0 body, so the body genuinely narrows and the exclusion has something to exclude. Re-measured over the whole suite with the conjunct dropped: this control goes red, together with #983's unparameterised twin, and those two alone — so the exclusion is now tested at both spellings and by nothing incidental. Also from the pass: The #1256 CHANGELOG bullet states the severity plainly. Verified end to end rather than asserted: on the previous commit's gates `vera run --fn f -- -5` on an `Ident<Nat>` return prints -5, with no trap and no diagnostic; here it traps, and 7 still returns 7. A caller-side guard in front of such a function was masking, not preventing. The calls.py residue chase is recorded as untested — deleting it stays green because `family_base_name` already answers `Byte` for every refinement and alias reachable today, so no producer stores a base that still needs chasing. The comment says what a fixture would need. Skip-changelog: test fixture correction plus comment and severity wording; no behaviour change Co-Authored-By: Claude <noreply@anthropic.invalid>
Rebased onto 9d83df1 (PR #1272). Only doc and count files conflicted; vera/codegen/functions.py and vera/wasm/calls_handlers.py — the two sources both PRs touch — auto-merged, and the boundary suite, the cross-module parity test and the nat-guard suite all stay green, so the _boundary_base consumers and the CellNames threading survive C1's monomorphization and routing work intact. Conflict resolutions, all mechanical: CHANGELOG [Unreleased] — union. C1's five bullets and this branch's four, none dropped, none reworded. The last hunk was NOT a union: it carried C1's five plus a STALE copy of this branch's own bullet against the updated copy, so a blind union would have duplicated it; resolved to C1's five plus the updated one, verified single. KNOWN_ISSUES — both sides' row operations applied by ROW ID, never by position. C1 deleted #1207/#1223/#1241/#1243/#1244/#1253 and added #1271/#1274; this branch deleted #1255/#1256/#1269 and adds #1276. Verified by set comparison over the whole file: every deletion absent, every addition present, no duplicates. Count-bearing prose — structure from upstream (it carries C1's 207 conformance programs and 157 test files), every NUMBER re-derived by scripts/check_doc_counts.py against the merged tree rather than merged from either side: 10,138 tests across 157 files, 9,980 passed + 26 stress + 132 skipped. docs/* — regenerated by build_site.py, never hand-merged. Content integrity: the diff over vera/ and tests/ (excluding the count-bearing vera/README.md paragraph) is identical before and after the rebase, modulo hunk offsets. Full manual gate re-run, hooks not having fired on rebase --continue: pytest 9,980 passed / 132 skipped, mypy clean, ruff and ruff --select S clean, 207 conformance, 42 examples, 255 corpus programs canonical, doc counts consistent, site assets coherent, diagnostic fields, limitations sync and explicit encoding all OK. Skip-changelog: rebase conflict resolution over count-bearing prose; no behaviour change Co-Authored-By: Claude <noreply@anthropic.invalid>
1 participant
Part of the #1213 burndown (PR C7) — the closure-boundary width-and-classification family. One commit.
Root-cause verdicts, which decided the tools
#1269 — the marking machinery, not the classification (
f64def84). TheExn<E>tag was already declared at the payload's resolved i32 width; only the thrown literal defaulted toi64.const, becausethrow's payload had never been registered as a@Bytewrite boundary.thrownow carries aCellNamesbeside its dispatch target — from both registration paths — and drives the same_mark_byte_write_valueevery other boundary drives;Exn.throw(v)delegates to the bare dispatcher exactly asState.put(v)does.#1255 — the issue's 11-site count was wrong; five sites are the bug. Measured empirically: all six
wasm/sites receive names their producers already resolve (_element_wasm_typeis handedByte, not the alias), and each shares its name with the element size/load/store decisions beside it — so resolving one conjunct would desync layout from rooting, and they are deliberately untouched. The five genuinely syntactic sites (closures.py ×3, functions.py ×2) now classify throughis_gc_pointer_baseover a representation base. Thegc_heap_start > 259reliance is closed structurally: a build guard plus namedGC_STACK_SIZE/GC_WORKLIST_SIZEconstants — the margin is 80 KiB before the data section contributes, so the issue's "empty string pool" exposure was never real, and that fact is now a test rather than an assumption.#1256 and #1269 share the mechanism, so they are single-sourced:
WasmContext._boundary_baseis one derivation consumed by the return boundary, theapply_fnargument, and thethrowpayload — the return boundary previously spelled its own different two hops.The differential, with its sensitivity proof
Base → fixed over all 254 corpus programs: zero WAT movement — and that zero is a measurement, not a blind instrument: the mutant (dropping the scalar exclusion from the new classifier) moves 23 programs, enumerated in the review record.
Tests
tests/test_closure_boundary_widths_1255_1256_1269.py: 49 tests, 20 RED on the base. Rooting is proved by a base-vs-alias differential with the base count pinned beside it (the bodies must allocate, so an absolute count would measure its own intermediates), pointer controls at all four boundaries, andVERA_EAGER_GC=1runs. The #1268 satisfying-literal test now runs as well as verifies. The two recorded smalls from PR #1250's closeout landed: the ancestry comment names the deeper rooting, and the daemon-thread question is decided (subprocess rework rejected, reasoning recorded in the harness docstring). A latent inference — "has a cell recorded" standing in for "is a State op", true only while State was the sole cell-carrying effect — was fixed and mutation-validated in passing, since this PR makesExnthe second cell-carrying effect.Gates
pytest 9,926 passed / 131 skipped; mypy clean; ruff +
--select Sclean; conformance 206/206; examples 42/42; corpus canonical 254/254; doc counts (10,083 / 152), site assets, diagnostic fields, explicit encoding, limitations sync all green; full pre-commit chain on the commit.Closes #1255.
Closes #1256.
Closes #1269.
(Keywords take effect at the release PR.)
Summary by CodeRabbit
Bug Fixes
Tests
Documentation