Handler semantics: deterministic ops, enclosing-context clauses, complete registration (#1210, #1211, #1215) - #1232
Merged
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 PR makes effect-operation resolution deterministic, preserves handler clause scope during WebAssembly lowering, adds State/Exn registration coverage, bounds nested clause expansion, and updates specifications, tests, documentation, and project totals. ChangesEffect handler semantics
Estimated code review effort: 4 (Complex) | ~45 minutes Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 6 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (6 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## release/v0.1.10 #1232 +/- ##
===================================================
+ Coverage 93.93% 93.95% +0.02%
===================================================
Files 100 100
Lines 34838 35057 +219
Branches 458 458
===================================================
+ Hits 32725 32938 +213
- Misses 2100 2106 +6
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: 7
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@README.md`:
- Line 266: Synchronize the documentation metrics: in README.md at lines
266-266, change conformance programmes from 196 to 199; keep CLAUDE.md lines
61-63 at 247 corpus programmes and update AGENTS.md to 247; in vera/README.md
lines 126-126, revise the Code Generation codegen/ and wasm/ line totals to
match the module map.
In `@spec/07-effects.md`:
- Around line 73-74: Remove the alphabetical canonical-form requirement from
§7.3.2 for effect rows. Preserve the source-written order when representing or
comparing rows, so bare operation resolution continues to follow declaration
order as specified in §7.4; retain set equality only for effect containment.
In `@tests/test_nested_handler_clause_ops.py`:
- Around line 291-300: Extend the _CASES coverage with both missing
no-enclosing-handler scenarios: a single handle[State<T>] inside a function
declaring effects(<State<T>>) whose clause body uses bare get/put and must route
to the host cell rather than the handler clause, and an outermost handler in a
pure function where decl_effect_ops is empty. Add corresponding fixtures and
expected results, preserving the existing cases.
In `@tests/test_state_exn_registration.py`:
- Around line 279-283: Import VeraError and narrow the exception handler in the
corpus-sweep block around parse_file(), transform(), and codegen_compile() to
catch only VeraError. Preserve the continue behavior for declared
parse/transform failures, while allowing unexpected code-generation exceptions
to propagate.
In `@vera/codegen/compilability.py`:
- Around line 510-514: Update the Exn branch in the effect registration handler
to check the boolean result of _register_exn_tag(type_arg). When registration
fails, append type_arg to _unregistrable_state_cells (or the corresponding
existing failure-tracking collection) so the function is skipped and receives
the same E612 diagnostic path as failed State registration; retain successful
registration behavior unchanged.
In `@vera/environment.py`:
- Around line 2211-2275: Update ordered_effect_row() so its fallback sorting is
total and hash-seed independent for repeated effect names, using a stable
structural key derived from each EffectInstance’s type arguments in addition to
name. Add a regression test that leaves current_effect_order empty with
State<Int> and State<Bool> instances and verifies deterministic ordering and
_effect_type_mapping() selection.
In `@vera/README.md`:
- Line 96: Remove the leading space from the inline code label for helpers.py in
the documentation table, keeping any visual indentation outside the backticks so
the markdownlint MD038 violation is resolved.
🪄 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: 3f19950f-4d29-48b4-b123-a872ae4446e3
⛔ Files ignored due to path filters (18)
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/**tests/conformance/ch07_clause_body_op_enclosing.verais excluded by!**/*.veratests/conformance/ch07_effect_op_source_order.verais excluded by!**/*.veratests/conformance/ch07_handler_registration_positions.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/g1_array.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p17b_state_string_minimal.verais excluded by!**/*.veratests/probes/state_handlers/checker_gates/e128_array.verais excluded by!**/*.veratests/probes/state_handlers/checker_gates/e337_user_effect_exn.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/a11_refined_pattern.verais excluded by!**/*.veratests/probes/state_handlers/dispatch_paths/p9_cross_family.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p11_init_nested.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p13_exn_in_clause.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p17_string_outer.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p17c_option_outer.verais excluded by!**/*.vera
📒 Files selected for processing (28)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/07-effects.mdtests/conformance/manifest.jsontests/probes/README.mdtests/probes/state_handlers/README.mdtests/test_effect_op_determinism.pytests/test_nested_handler_clause_ops.pytests/test_state_exn_registration.pyvera/README.mdvera/checker/calls.pyvera/checker/control.pyvera/checker/core.pyvera/checker/resolution.pyvera/codegen/compilability.pyvera/codegen/core.pyvera/codegen/functions.pyvera/environment.pyvera/wasm/calls_handlers.pyvera/wasm/context.pyvera/wasm/helpers.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
`Environment.lookup_effect_op` picked a bare op's signature by iterating `ConcreteEffectRow.effects` — a frozenset. When two effects in one row declare the same op name, which one bound was a function of PYTHONHASHSEED, not of the program. No user `effect` declaration is needed to reach it: the built-in `State` and `Http` both declare `get`, so `effects(<State<Int>, Http>)` ran to 70 on some interpreter starts and failed E217 on others, from identical source. The row now travels beside an ordered tuple of the same instances, taken from the `ast.EffectSet`'s own sequence — `_resolve_effect_row_ordered` produces both views from one resolution, so they cannot come to describe different effects. A handler pushes its own effect to the FRONT of that order for the duration of its body, which makes the whole rule one ordered walk: innermost handler, then each enclosing handler, then the declared row in source order, then the registered effects in registration order (a dict, hence insertion order — now documented as the deterministic fallback it is rather than left implicit). `ordered_effect_row` is total over the row: a member the order tuple does not mention is not dropped but sorted by name after the ordered prefix, so a row assigned outside the checker stays deterministic too. Clause bodies are checked outside their own handler's scope, so a bare op there resolves against the enclosing context — the checker side of the #1211 alignment, noted where the order is pushed. Spec §7.4 states the resolution order, §7.3.2 notes that set equality governs containment rather than this tie-break, and §7.4.1 now says what the compiler does with an unqualified ambiguous call instead of claiming it is rejected. Co-Authored-By: Claude <noreply@anthropic.invalid>
A handler clause is not part of the body it refines. The checker says so structurally: clauses are checked before the handled effect joins the effect row, so a bare `get`/`put` written in a clause body resolves against whatever encloses the `handle` expression — the same rule that already gave clause-body SLOT references the declaration scope (#1202). Codegen disagreed. Inlining a clause body cleared `_state_clause_ops` (enough to stop a clause re-entering itself) but left `_effect_ops` pointing at the handler's OWN host-cell imports. With two nested handlers over different cell families, a bare `put` in the inner handler's clause body wrote the INNER cell while the checker had typed it against the outer one: check-green, verify-clean, valid WASM, and a silently wrong number. The clause registry now carries the whole declaration-time scope in one record — `StateClauseEntry` replaces the seven-tuple — instead of the slot environment alone, which is what let the two halves drift. The inline restores all four registries around the clause body and its `with` expression. The two op RESULT-TYPE mirrors travel with them and are separately load-bearing: a bare `get(())` in match-scrutinee (`_effect_op_result_wt`) or array-element (`_effect_op_result_vera`) position inside a clause body emitted invalid WASM for a check-green program without them. `resume` keeps the clause's own family — it types this op's result, not the scope the body compiles in. Termination becomes a property of the data rather than of a clear: the restored registry is the one from strictly OUTSIDE this handler, so it can never contain this clause, and each re-entry from a clause body moves one handler outwards through a finite nesting. The load-bearing comment is rewritten to that invariant. The verifier is unchanged, verified rather than assumed: the obligation stream (tier-1 / tier-3 / total) over every shape is identical before and after. Across the whole 494-program corpus — examples/, tests/conformance/, tests/probes/ — exactly two programs moved: p9_cross_family (100000111 -> 301000, the checker's value) and p17c_option_outer (invalid WASM -> 3). The registry record drops the effect argument's alias-opaque source spelling: nothing that unpacked the tuple ever read it. Spec §7.5.2 states the rule for both halves — slot references and operations — and names the termination consequence. Co-Authored-By: Claude <noreply@anthropic.invalid>
Codegen decides which host-cell imports and exception tags a module DECLARES in one pass and which ones it CALLS in another. The declaration pass walked a `handle` expression's BODY alone — not its clause bodies, not a clause's `with` state update, not its own state-init expression — so a family reached only through one of those went unregistered while the lowering emitted its calls regardless. The result was a check-green, verify-clean program that died at whole-module WAT compilation with `unknown func $vera.state_push_Nat` or `unknown tag $exn_Int`. The same three positions are now walked by the IO / Markdown / Regex host-import scan too, which had the identical orphaned-import shape for a host builtin in a clause body. The `i32_pair` cell the walk used to skip in SILENCE — a `handle[State<String>]` inside a `pure` function, where the declared-effect gate never runs — is now the same loud E607 that gate emits, reported at the offending cell's own location. Both paths were open-coding the accept-and-register decision; they now share one derivation each (`_register_state_cell`, `_register_exn_tag`), so they cannot come to accept different cell types. TESTS. Four shapes, one per position the walk missed, each required to compile and produce a value derived from the language rules rather than from what codegen emits; plus the E607 shape, asserted on the code and on the ABSENCE of its old `state_push_String` symptom. The permanent check is a REGISTRATION-COMPLETENESS DIFFERENTIAL, because a unit test on either pass cannot see the two drift apart: over every `examples/` and `tests/conformance/` program that compiles (223 programs, 103 distinct `state_*`/`exn_*` symbol references), every symbol the emitted WAT references must have a matching import or tag declaration. It carries floors on both counts and a can-go-red test that strips the import lines and requires the extraction to report exactly those symbols. PROMOTION (#1213 burndown). Three conformance programs, suite now 199: `ch07_clause_body_op_enclosing` (§7.5.2, the clause-body operation scope across two nesting depths and a `with` expression), `ch07_handler_ registration_positions` (§7.5, all four handler sub-expression positions), and `ch07_effect_op_source_order` (§7.4, source-order and innermost-handler resolution — the E217 half is already pinned by `ch07_bare_effect_op_rejected`). Ten probes are dispositioned and deleted: seven whose shapes these programs and the three new regression suites now carry, and three parse-broken ones — `checker_gates/e337_user_effect_exn` (repaired it yields E152, which `ch09_builtin_effect_redefinition_rejected` already pins), `checker_gates/e128_array` (its subject, the E128 array quantifier domain, is closed and pinned by `ch06_quantifier_array_domain_rejected`; the file was broken on unrelated lambda-contract syntax and never exercised it), and `clause_scoping/a11_refined_pattern` (its premise, that a refined clause pattern erases to the base name, was answered NO by the #1208 retreat, and its `@Nat{self >= 0}` is not Vera's refinement spelling). Both probe READMEs are updated. Co-Authored-By: Claude <noreply@anthropic.invalid>
The op-NAME fix's own hash-seed sweep surfaced the type-ARGUMENT leg of the same lottery. Spec §7.3.3 permits one effect twice with different type arguments — `effects(<State<Int>, State<Bool>>)` is two independent cells — but `_effect_type_mapping`'s row fallback iterated the row's frozenset on the recorded premise that "a declared row cannot meaningfully carry two instantiations of one effect". It can, and the identical program checked clean on four of the first eight PYTHONHASHSEED values and failed E121 (`body has type Bool, expected Int`) on the other four. The row leg now walks `ordered_effect_row()` — the same ordered candidate list bare op-name resolution uses — so the first instantiation written in the row governs. That alone left a deterministic desync: codegen builds its per-function `effect_ops` by looping the declared row and letting each State effect OVERWRITE the last, so it emitted `state_get_Bool` (i32) for a call the checker had just settled as `Int` (i64) — invalid WASM from a check-green program. Codegen is aligned to the checker: first in source order wins, for `get`, `put`, and `throw` alike. The eight-seed sweep now returns one value at every seed, and it is the source-order-first cell's (33, against a Bool cell holding `true` — a value no default or other cell can produce). A corpus differential over `examples/`, `tests/conformance/` and `tests/probes/` shows nothing else moved. Co-Authored-By: Claude <noreply@anthropic.invalid>
Skip-changelog: attribution edit inside the existing bullet Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
force-pushed
the
fix/1210-1211-1215-handler-semantics
branch
from
August 7, 2026 13:44
13de07d to
89d54ca
Compare
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/README.md (1)
27-30: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winNumber
Resolveas an independent pipeline stage.The document states that the compiler has seven independently testable stages, but the text version labels
Resolveas2bandExecuteas6. This presents six numbered stages and makesResolveappear to be a Transform sub-stage.Number
Resolveas3and shift later stages to4–7, or state explicitly that2bis not one of the seven stages.As per coding guidelines: keep parse, transform, resolve, typecheck, verify, compile, and execute as seven independently testable stages.
🤖 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/README.md` around lines 27 - 30, Update the pipeline-stage numbering in the README so Parse, Transform, Resolve, Type Check, Verify, Compile, and Execute are explicitly numbered as seven independent stages. Change Resolve from 2b to 3 and shift all subsequent stage numbers through Execute from 4 to 7, preserving the existing stage descriptions and order.Sources: Coding guidelines, 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.
Outside diff comments:
In `@vera/README.md`:
- Around line 27-30: Update the pipeline-stage numbering in the README so Parse,
Transform, Resolve, Type Check, Verify, Compile, and Execute are explicitly
numbered as seven independent stages. Change Resolve from 2b to 3 and shift all
subsequent stage numbers through Execute from 4 to 7, preserving the existing
stage descriptions and order.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 1a5ce9fe-241b-4e63-924a-70cb20fa6a50
⛔ Files ignored due to path filters (2)
docs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (10)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdvera/README.mdvera/environment.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Owner
Author
Adversarial review recordTwo independent hostile reviewers audited the branch at its pre-rebase head (the rebase that followed reconciled documentation counts only; every handler-code change replayed byte-identical, verified by differential). A consolidated fix round covering both reviews plus the CodeRabbit round is in flight; its per-finding dispositions will be appended here. Round 1 — semantics lensHeld under attack: the #1215/#1231 ordering (27 probes × 8 hash seeds all uniform; three-instantiation rows and duplicate spellings first-wins with checker=codegen=runtime agreement; a source-order-sensitive narrowing where the verifier's E503 and the runtime trap agree — base diverges with a missing guard on the wrongly-resolved cell); the #1211 matrix (20/20 ordered cross-family pairs from {Int, Nat, Bool, Float64, Byte} at the independently-derived values — base fails all 20, five of them silently wrong); snapshot nesting at depth 2; Findings:
Round 2 — validation-honesty lensHeld under attack: all eight #1211 matrix pins hand-derived from spec §7.5.1/§7.5.2 with a checker-side instrument (negative-literal probes producing E503 exactly where the middle cell binds — proving "one level out, not all the way") — no agreement bias; all six pre-fix values reproduced at base; probe READMEs exact (240 files ↔ 240 rows); all three parse-broken deletion reasons verified against history; KNOWN_ISSUES one-to-one with the expected fixed-on-branch delta; the seed sweeps are real subprocess-per-seed with fixed seeds that catch the original bug deterministically (4 of the 6 chosen seeds fail at base). Findings — a 13-mutant battery, 10 killed, 3 SURVIVED:
Rebase noteAfter the docs PR (#1230) merged, this branch conflicted on five documentation files (20 hunks, all count-class). Resolved by taking #1230's table structures, re-applying this branch's semantic rows, and setting every number from the doc-counts oracle (9,445 tests / 146 files / 199 conformance / 247 corpus — neither side's numbers were right). CHANGELOG unioned cleanly. Full gate green post-rebase; CI green at the rebased head. |
…not honour (#1210, #1211, #1215) Six code fixes, the §7.5.2 reconciliation they force, and the tests that distinguish each one. REGISTRATION (#1210) - The handler walk's Exn arm called the shared tag registration and threw the boolean away, so `handle[Exn<Unit>]` in a `pure` function registered no tag and still compiled — `unknown tag $exn_Unit` at whole-module WAT, where the declared-row spelling of the same payload had always been a clean [E612] function drop. Both arms now record what they could not register and the entry point drops the function, with the gate's own wording extracted so the two paths cannot say different things. - The walk stopped at `decl.body`, but a contract is LOWERED code: a `handle[State<Nat>]` in a `requires`, an `ensures`, an `assert`, or a `decreases` measure emitted `state_push_Nat` against an import that was never declared. Both pre-scans now walk the contract predicates through one shared enumeration (`contract_exprs`) — `decreases` needed it, carrying `exprs` rather than `expr`, which the old attribute-name shortcut skipped — and both walkers descend `assert` / `assume` / quantifier positions their coverage tables had declared structurally handler-free. CLAUSE-BODY OPERATIONS (#1211, #1233) - Same-family nesting is refused instead of lowered. The clause TRANSFORM half routes outward correctly, but the host intrinsics address only the innermost pushed cell of a family, so `handle[State<Int>]` inside `handle[State<Int>]` (or inside a function declaring `effects(<State<Int>>)`) would write the INNER cell where §7.5.2 names an outer one. That shape is now a loud [E602] citing #1233. The gate keys on the whole pushed-cell stack rather than the adjacent handler, so an Int/Nat/Int/Nat nest — whose third level routes to the second while its `state_put_Nat` addresses the fourth's cell — is caught too; the index it compares against travels with the clause entry, exactly like the op registries, so a nested handler's own body keeps addressing its own cell. - The outward re-entry is bounded. Each clause-body operation re-expands another clause, so the emitted code is exponential in the nesting depth (850 / 1,582 / 4,330 / 15,143 WAT lines at depths 2 / 4 / 6 / 8; ~2M by 18). `STATE_CLAUSE_INLINE_DEPTH_CAP` = 8 follows the `DERIVED_HELPER_DEPTH_CAP` precedent: past it the function is a loud [E602] naming the cap, and the legitimate matrix reaches depth 2. - The handler lowering saves and restores its op registries the way the clause inline already did — whole-dict replacement inside a try/finally, not in-place mutation with the restore outside it — so a `CodegenSkip` out of a handled body cannot leak this handler's `get`/`put` into the scope that catches it. Same treatment for the `Exn` twin. RESOLUTION ORDER (#1215) - `ordered_effect_row()`'s fallback for a row member no order tuple mentions sorted by effect NAME alone, which is not a total order: §7.3.3 lets one effect appear twice with different arguments, so `State<Int>` and `State<Bool>` tie and a stable sort hands back the frozenset's own iteration order — the seed dependence the method exists to remove, inside the method itself. The key is now structural (name plus rendered type arguments), which `_effect_type_mapping` inherits. SPEC §7.5.2, §7.4, §7.4.1, §7.3.2 §7.5.2 held two incompatible readings of the same operation: one bullet said an operation inside a clause body performs the INTRINSIC operation, the next said it belongs to the enclosing context. They disagree exactly when the enclosing handler declares a clause for it, and the shipped semantics is the coherent one — the inner handle expression is lexically part of the outer handled body, so an operation emerging from it is an outer-body operation SITE and the outer clause runs on it. The old bullet is scoped to what is actually true of it (transforms do not cross a CALL boundary; a clause never re-enters ITSELF), and a third bullet states the same-family limitation. §7.4's final resolution step names the REGISTERED effects in registration order, matching the implementation; §7.4.1 says "not rejected for ambiguity" is not "always accepted"; and §7.3.2 drops its claim of an alphabetical canonical form — written order is meaningful and `vera fmt` preserves it, so imposing one would change what a program means. TESTS Mutation-validated where a mutant is named: reverting the `_effect_ops` restore reddens the new declared-row case alone; clearing rather than restoring the clause registry turns the enclosing-clause case from 300100 to 300050; dropping the `_scan_io_ops` HandleExpr legs reproduces `unknown func $vera.print`; a name-only effect sort key gives two distinct outcomes across six seeds. The registration differential gains a validation leg — every swept module goes through `wasmtime.Module`, because a symbol declared at the WRONG TYPE passes the name comparison while being invalid WASM — with a planted retyped import proving it can go red, an Exn half for the strip-and-compare red-proof, and honest floors (the summed reference count and the globally distinct count are different numbers and both are floored). Its corpus loop no longer swallows every exception: declared parse/transform failures skip, anything else propagates. The #1203 clause-body-put fixture moves from one family to two. It handled `State<Nat>` while declaring `effects(<State<Nat>>)`, which is precisely the unaddressable shape above; the @nat narrowing boundary it exists to pin is unchanged, and removing the bare-path guard still reddens it. DOCS `ch07_clause_body_op_enclosing`'s three-deep case reads the middle cell's initial value into its result before the inner clause overwrites it, so no constant is inert. The seed-count claim in the determinism suite matches what was measured. The pipeline documentation numbers seven stages, because there are seven — `vera/README.md` said "seven-stage" and then numbered Resolve as "2b", and `assets/diagrams/architecture.svg` carried the same half-numbering, while the resolver has its own public entry point, its own `cli.py` step, its own diagnostics and its own stage column in the module map. Module-map line totals, test counts and the corpus count are re-synced to the tree. Refs #1210, #1211, #1215, #1231, #1233 Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Round-3 dispositions (appending to the review record above)All findings from both adversarial rounds + the CodeRabbit round landed in
Suite: 9,465 tests / 199 conformance / 247 corpus; full gate sweep green. CI + fresh CR pass at |
Owner
Author
|
@coderabbitai Outside-diff finding on vera/README.md (pipeline-stage numbering): fixed in a3bd7e6 — and reality pointed to renumbering rather than keeping the sub-stage: |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo '== matching documentation references =='
rg -n -i -C 2 'seven-stage|2b|resolve imports|resolve_imports|Parse|Execute' \
vera/README.md architecture.svg 2>/dev/null || true
echo
echo '== resolve_imports definition and CLI call sites =='
rg -n -C 4 '(^\s*(def|async def)\s+resolve_imports\b|\bresolve_imports\s*\()' \
--type py vera 2>/dev/null || true
echo
echo '== repository-wide 2b references =='
rg -n -i -C 1 '\b2b\b' . -g '!**/.git/**' || trueLength of output: 48421
The correction is not complete. You are interacting with an AI system. |
… too Skip-changelog: SVG source-comment sync with the stage renumbering Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai Fixed in the just-pushed commit — and your line-74 catch generalized: the ENTIRE source-comment chain lagged the badge renumbering (2b·Resolve, 3·Type Check, 4·Verify, 5·Compile, 6·Execute). All seven comments now read 1·Parse through 7·Execute, matching the displayed badges; site-assets gate green. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
svg="assets/diagrams/architecture.svg"
echo "== Stage source comments =="
rg -n '<!--\s*[1-7](?:[a-z])?\s*·' "$svg" || true
echo
echo "== Obsolete numbering references =="
rg -n -i '2b\s*·\s*Resolve|seven-stage|stages-five-and-six' "$svg" || true
echo
echo "== Visible stage labels =="
rg -n 'Parse|Resolve|Type Check|Verify|Compile|Execute' "$svg" || trueLength of output: 1598
You are interacting with an AI system. |
Owner
Author
Review record — round 4 (fixed-point on the round-3 fix,
|
There was a problem hiding this comment.
Actionable comments posted: 9
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/codegen/functions.py (1)
216-240: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winPrevent later
Stateinstances from remapping shadowed operationsThe checker resolves a user-defined
getbefore effect operations, but codegen checks_effect_opsbefore user functions. WithState<Int>, State<Bool>, codegen can therefore routegettostate_get_Boolandputtostate_put_Int. Keep shadowed operations out of the effect table, or apply consistent shadowing to both operations.🤖 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 216 - 240, Update the State effect handling that populates effect_ops for “get” and “put” so once either operation is shadowed by a user-defined function, later State instances cannot register or remap it. Apply the same shadowing rule consistently to both operations, preserving the first valid State operation in the effect table.
🤖 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 `@KNOWN_ISSUES.md`:
- Line 30: Add a regression case to _SAME_FAMILY_CASES in
tests/test_nested_handler_clause_ops.py for the four-level Int/Nat/Int/Nat
nested handler shape, asserting the expected E602 codegen skip when the target
family appears in the shadowed addressable slice. If this behavior is not
intended to be tested, remove the at-distance claim from KNOWN_ISSUES.md
instead.
In `@spec/07-effects.md`:
- Around line 71-73: Update the §7.3 lead-in to define an effect row as a
written, ordered sequence of effects while stating that containment uses set
equality per §7.3.2. Remove the conflicting “unordered set” description and
preserve the surrounding explanation that source order remains meaningful for
effect resolution and formatting.
In `@tests/test_nat_narrowing_return_differential.py`:
- Around line 1612-1618: Add an explicit zero-value test alongside
test_clause_body_put_negative_traps and test_clause_body_put_non_negative_passes
for _PUT_IN_CLAUSE_BODY, asserting _run(..., "go", 0) returns 0. Keep the
existing negative-trap and positive-value coverage unchanged.
In `@tests/test_nested_handler_clause_ops.py`:
- Around line 714-752: Add a boundary test for
`_deep_nest(STATE_CLAUSE_INLINE_DEPTH_CAP + 1)` that compiles the source and
asserts it emits E602, includes the cap value, and reports the
exponential-expansion message. Keep the existing at-cap test and the `CAP + 2`
test unchanged.
In `@vera/codegen/compilability.py`:
- Around line 32-37: Update contract_exprs to explicitly dispatch the supported
function-contract types Requires, Ensures, Decreases, and Invariant, yielding
each type’s appropriate expression field. Remove the getattr-based fallback and
raise an error for any unsupported Contract type, so mypy validates field access
and new types cannot be silently skipped.
- Around line 546-548: Initialize _unregistrable_exn_tags in
CodeGenerator.__init__ alongside _unregistrable_state_cells, while preserving
the existing per-function reset in _scan_body_for_state_handlers.
In `@vera/environment.py`:
- Around line 36-48: Update _effect_sort_key to include repr(ei.type_args) in
its returned tuple so refinement predicates and `#b` markers remain
distinguishable during deterministic sorting. Add coverage for the
State<Pos>/State<Neg> seed sweep using an empty current_effect_order, preserving
distinct ordering across hash seeds.
In `@vera/wasm/calls_handlers.py`:
- Around line 1920-1938: Move the STATE_CLAUSE_INLINE_DEPTH_CAP check in the
clause expansion flow before any registry or state mutations, including the
_addressable_from assignment, so CodegenSkip cannot leave partial state behind.
Remove the manual _addressable_from restoration from the early-exit branch, and
retain saved_addressable plus the addressable assignment immediately before the
existing try/finally; keep _clause_inline_depth incrementing unchanged.
- Around line 1700-1714: The family comparison in the call-handling logic must
avoid mangling the already-mangled result of _state_import_family(). Keep
entry.family comparisons compatible with the unmangled family values, but
compare bare-import target_family directly against the appropriately mangled
shadowed families so composite same-family nesting returns through CodegenSkip
instead of targeting the innermost cell. Add a regression covering bare-import
composite same-family nesting.
---
Outside diff comments:
In `@vera/codegen/functions.py`:
- Around line 216-240: Update the State effect handling that populates
effect_ops for “get” and “put” so once either operation is shadowed by a
user-defined function, later State instances cannot register or remap it. Apply
the same shadowing rule consistently to both operations, preserving the first
valid State operation in the effect table.
🪄 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: a4f7851d-e923-415f-b0ed-581e85df6818
⛔ Files ignored due to path filters (4)
assets/diagrams/architecture.svgis excluded by!**/*.svgdocs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**tests/conformance/ch07_clause_body_op_enclosing.verais excluded by!**/*.vera
📒 Files selected for processing (22)
AGENTS.mdCHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/07-effects.mdtests/test_effect_op_determinism.pytests/test_nat_narrowing_return_differential.pytests/test_nested_handler_clause_ops.pytests/test_state_exn_registration.pyvera/README.mdvera/codegen/compilability.pyvera/codegen/functions.pyvera/environment.pyvera/skip.pyvera/wasm/calls.pyvera/wasm/calls_handlers.pyvera/wasm/context.pyvera/wasm/helpers.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…lling (#1210, #1211) Three more positions reached the lowering without reaching either pre-scan walker, and a fourth defect let a whole class of same-family nests past the gate that exists to refuse them. `LetDestruct.value` was absent from the `Block` dispatch of BOTH walkers, so `let Tuple<@nat, @nat> = f(handle[State<Nat>] ...)` emitted `state_push_Nat` against no import — and, because the round-3 uncompilable-payload gate is driven by the same walk, an `Exn<Unit>` payload written there bypassed E612 outright where its `LetStmt` twin is a clean function drop. `ModuleCall.args` sat in both coverage tables as "tracked by the imported module's own scan", true of the callee and false of the arguments, which are this module's own lowered expressions. And a SIGNATURE REFINEMENT predicate — a `{ @base | P }` parameter or return type has `P` emitted as a boundary guard, and is reached through the alias table rather than structurally, so no walk from `decl.body` can find it; `_signature_refinement_predicates` is the signature's `contract_exprs`, mirroring `_refinement_guard_parts`'s two bails so registration equals what is emitted rather than exceeding it. None of the three had a corpus instance, so the corpus-anchored differential could not have found any of them. The walkers now carry a schema-driven FIELD-coverage gate: it reads the dataclass fields of `vera/ast.py` and fails on any node class with an expression-carrying field that neither walker dispatches on, unless the class is in an explicit ten-entry justified-ignore table naming the route its expressions ARE reached by. It is deliberately stronger than `scripts/check_walker_coverage.py`, whose canonical set is the `Expr` subclasses (`LetDestruct` is a `Stmt`) and whose verdict is "the class is NAMED" (`ModuleCall` was named, with a disposition covering half the node). The same-family refusal compared family names in two spellings. `_pushed_cell_families` and a clause registry entry carry the canonical family (`Option<Int>`); an import name carries the mangled one (`Option_LInt_R`); and mangling is not idempotent, so re-mangling the already-mangled side made every COMPOSITE family compare unequal to itself and the gate returned instead of refusing. `handle[State<Option<Int>>]` nested in `handle[State<Option<Int>>]` with no outer `put` clause compiled and ran, returning 5100 where the enclosing-context rule says 5042 — on the exact shape its scalar `Int` twin was refusing correctly the whole time. Both sides now normalise once, and the message names the canonical cell. The structural tiebreak that removed the row-order hash-seed dependence had the same bug one level down: it rendered type arguments with `pretty_type`, a presentation renderer that elides a refinement's predicate and strips a type variable's built-in marker, so `effects(<State<Pos>, State<Neg>>)` over two refinement aliases of one base tied again and fell back to frozenset order. Also in this round: the clause-inline depth cap checks before it mutates (its skip was the one exit that left the six clause registries replaced); the same-family message covers the qualified `State.put` spelling that routes through the same gate; `contract_exprs` dispatches on the real contract types instead of probing for an attribute, and raises on an unknown one; the Exn half of the walk's unregistrable-type record is declared beside its State sibling; the registration differential validates through the exceptions- enabled engine `execute()` uses and filters the conformance negatives out of its sweep, with its scope and its two limits stated on the test; spec 7.3's lead-in stops calling an effect row an unordered set, and 7.5.2's same-family lead-in states the precise claim. New pins: the composite gate bypass in both its branches with a scalar differential and a different-family positive control, the four-level Int/Nat/Int/Nat shadow-at-a-distance the KNOWN_ISSUES row asserts, the qualified spelling, depth exactly CAP+1, the refinement-alias seed sweep, the zero boundary of the clause-body put guard, and the declared-row op registry's shadow symmetry across two State instantiations. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Review record — round 5 (
|
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 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 104: Fix the Markdown table row around the differential-test entry so it
contains exactly four cells: escape the literal pipe character inside the long
description, and remove only spaces immediately inside the affected backtick
code spans to satisfy MD038. Preserve the table content otherwise, then rerun
markdownlint-cli2 and confirm the MD056 and MD038 violations are resolved.
- Around line 9-11: Correct the affected table row in TESTING.md to satisfy
markdownlint MD056 and MD038, then ensure the documented test counts are
regenerated or verified by rerunning the count gate with pytest available. Keep
the reported counts accurate and preserve the stale-count scan result.
In `@tests/test_walker_defensive_branches_597.py`:
- Around line 398-413: Update the conformance coverage around _canonical_classes
and the Line 484 validation to track each (class_name, field_name) obligation
instead of reducing classes to set(canonical). Require every descendable field
to have either a walker dispatch route or an explicitly justified ignore route,
and add a mutation regression that removes a field route from an
already-dispatched AST class and verifies the check fails.
In `@vera/environment.py`:
- Around line 67-70: Update the FunctionType branch of _structural_type_key to
replace pretty_effect() with a recursive structural effect-row key that
preserves the row variable and sorted structural keys for nested EffectInstance
values. Ensure _effect_sort_key() deterministically distinguishes outer effect
instances so _effect_type_mapping() selects the same bare-operation type across
PYTHONHASHSEED values, and add cross-seed regressions covering refinement
predicates and builtin type-variable markers.
🪄 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: 53e3eb76-6b0b-442b-ac8c-b6395fefa653
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (19)
CHANGELOG.mdFAQ.mdREADME.mdROADMAP.mdTESTING.mdspec/07-effects.mdtests/codegen_helpers.pytests/test_codegen_effects.pytests/test_effect_op_determinism.pytests/test_nat_narrowing_return_differential.pytests/test_nested_handler_clause_ops.pytests/test_state_exn_registration.pytests/test_walker_defensive_branches_597.pyvera/README.mdvera/codegen/compilability.pyvera/codegen/core.pyvera/codegen/functions.pyvera/environment.pyvera/wasm/calls_handlers.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Owner
Author
Review record — round 6 (fixed-point on
|
The signature enumeration the pre-scans consume reached the boundary-guard emitters by one of their four routes, because it was written as a copy of what one of them does. The guard layer is also entered by decomposing a tuple PARAMETER into its components, by decomposing a tuple RETURN, and from a closure's own refined formals and return — each lowering predicates nothing registered. A `Tuple<Big, Int>` parameter, a `Tuple<Big, Int>` return, and `fn(@BIG -> @int)` / `fn(@int -> @BIG)` behind an `apply_fn` all died at whole-module WAT with `unknown func $vera.state_push_Nat`, from check-green, verify-clean programs. There is now ONE derivation of what those guards check, living beside the emitters it must equal. `_tuple_component_guard_sites` owns the tuple decomposition — the component classification, the `@Unit`-component skip, the heap layout, and the fail-closed depth limit — and the emitter, the return-epilogue gate and the host-import pre-scan all read it, where they used to carry three hand-kept copies and the pre-scan's copy did not exist. `_signature_refinement_predicates` enumerates on top of it and of `_refinement_guard_parts`, so its two bails ARE the emitter's bails rather than a mirror of them. Registration equals emission in both directions. Component decomposition stays a named-function leg because the closure path emits no component guards, so enumerating it for a closure would declare a host import nothing calls — measured at 4 spurious imports for one closure formal. Both walkers now descend an `AnonFn`'s signature as well as its body, cycle-guarded: `type R = { @int | ... fn(@r -> @int) ... }` type-checks, so expanding a refinement that contains a closure refined by itself is a real cycle, and unguarded the walk blows the recursion limit on a check-green program. Two instruments were claiming more than they held. The pre-scans' field-coverage gate said a new FIELD on a dispatched class was loud; it was class-granular, so a field added to a class that already had a branch passed silently. It now compares each dispatched class's descendable fields against the names that walker's source reads — the name-based limit is stated on the gate rather than papered over. A new callgraph gate asserts the structure that keeps the derivation single: every consumer reads the shared decomposition, and none reclassifies behind it. And the `RefinementType` justified-ignore entry now names the derivation and all four routes it covers, which is what it was asserting all along. `_error_once` replaces the bespoke E618 site set, since the depth-limit E617 is now reachable from three consumers of one derivation. Two count claims corrected: 31 was the number of distinct state/exn SYMBOLS in the corpus, not of handler-bearing modules, which is 30. The bare-engine rationale is scoped to the claim that holds — on wasmtime 47.0.1 exceptions default on, so the helper exists for the supported versions where they do not, and what that costs is measured directly (10 of the 30 fail with `wasm_exceptions` off). Co-Authored-By: Claude <noreply@anthropic.invalid>
The #1229 row was owed since its filing; #1234/#1235 are round-7 discoveries (the closure-lift non-termination and the closure-boundary component-guard gap), both pre-existing and tabled for PR C. Skip-changelog: three-row bug-table bookkeeping, no compiler change Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Review record — round 7 (
|
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 `@KNOWN_ISSUES.md`:
- Line 23: Update the `#1234` table row in KNOWN_ISSUES.md by escaping the pipe
inside the inline code example as \|, matching the neighbouring rows. Preserve
the existing code example and issue link so the Markdown table has exactly two
columns.
In `@vera/README.md`:
- Around line 129-141: Recalculate the line counts for every tracked module
listed under the codegen/ table in vera/README.md, then update the directory
total and each module’s count, including api.py, modules.py, monomorphize.py,
and assembly.py. Preserve the existing table structure and descriptions.
🪄 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: 9f992234-3c1f-4228-93ad-c36902f6b7f8
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (14)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/codegen_helpers.pytests/test_refinement_binder_convergence_1208.pytests/test_state_exn_registration.pytests/test_walker_defensive_branches_597.pyvera/README.mdvera/codegen/compilability.pyvera/codegen/contracts.pyvera/codegen/core.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Owner
Author
|
@coderabbitai Outside-diff finding on vera/codegen/functions.py (State get/put shadowing consistency): verified and skipped — the code already guards both operations identically. Instrumented WasmContext population across three programs: each op checks |
Owner
Author
Review record — round 8 (closer,
|
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo '== Codegen function outline =='
ast-grep outline vera/codegen/functions.py --items all --type function --match 'scan|state|handler|effect' || true
echo
echo '== State get/put registration guards =='
rg -n -C 8 'State|effect_ops|_fn_sigs|\bget\b|\bput\b' vera/codegen/functions.py
echo
echo '== Shadowing regression references =='
rg -n -C 6 'shadow|first.*(?:win|registr)|State.*(?:get|put)|(?:get|put).*State' \
tests/test_codegen_effects.py tests 2>/dev/null || trueLength of output: 200644 🏁 Script executed: #!/bin/bash
set -euo pipefail
echo '== State registration branches in vera/codegen/functions.py =='
rg -n -C 16 \
'if .*["'\'']get["'\''].*not in self\._fn_sigs|if .*["'\'']put["'\''].*not in self\._fn_sigs|effect_ops\[['\'']get['\'']\]|effect_ops\[['\'']put['\'']\]' \
vera/codegen/functions.py || true
echo
echo '== Relevant test definitions in tests/test_codegen_effects.py =='
rg -n -C 18 \
'^def test_.*(?:shadow|State)|^ def test_.*(?:shadow|State)|shadowing.*(?:get|put)|(?:get|put).*shadow' \
tests/test_codegen_effects.py || trueLength of output: 5791
In "get" not in self._fn_sigs and "get" not in effect_opsLine 232 applies the equivalent guard to
The finding does not apply. I withdraw it. You are interacting with an AI system. |
…down (#1210, #1215) The pre-scan coverage gate obligated CLASSES. A class discharged its obligation the moment it had any `isinstance` branch, so a new expression-carrying field on an already-dispatched class — the commonest way an AST grows — was left to a second, weaker screen beside the gate. The obligation is now one per `(class, field)` pair, discharged by the conjunction (branch AND field read) or by a justified-ignore entry, and the two checks are one gate: 39 obligations, 28 dispatch-routed, 11 justified through 9 class-level entries and 2 per-pair ones. `HandlerClause` carries two fields and so is written per pair; a class-level entry is permitted only while its class has a single field, because otherwise it would exempt whatever field the class grows next — the same class-keyed hole one table down. Both can-go-red proofs and the gate call one `_pair_holes`, so the mutations exercise the check that runs. The effect-order tiebreak's structural key stopped one level short. A type argument may itself be a function type, and a function type carries its own effect ROW, whose leg was rendered by `pretty_effect` — which renders each member through `pretty_type`, the presentation renderer that elides a refinement's predicate and strips a type variable's built-in marker. Two outer instances differing only inside a nested row therefore tied for a third time and fell back to `frozenset` order. `_structural_effect_key` renders the row structurally and sorts its members on the same key the tiebreak uses, so the two mutually recurse; both nested cases are swept across six `PYTHONHASHSEED` values, asserted separately so a regression names the elision that came back. `_signature_refinement_predicates`'s deliberate closure-path asymmetry now names its tracker. Table rows in `TESTING.md` and `KNOWN_ISSUES.md` escape the pipes inside their refinement spellings, so the rows carry the cell count the rest of their tables do. Every count in `vera/README.md`'s module map is re-measured from the tracked files, and the trailing total with them. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Review record — round 9 (
|
This was referenced Aug 7, 2026
6 tasks
aallan
added a commit
to chethanuk/vera
that referenced
this pull request
Aug 13, 2026
Spec §7.5 makes two cells distinct exactly when their resolved types are,
and a refinement is part of that type: `EffectInstance` holds the
`RefinedType`, §7.5.1 already required the state declaration to match it
"predicate included", and E125 refuses to pass one where another is
required. Codegen collapsed it away — `family_name` stripped the
refinement before rendering — so under `type Pos = {@int | @Int.0 > 0}` and
`type Neg = {@int | @Int.0 < 0}` all three of `State<Pos>`, `State<Neg>` and
`State<Int>` shared one host cell.
A `Pos` handler wrapping a `Neg` handler, with a callee declaring
`effects(<State<Pos>>)` called inside the inner one, sent that callee's
`put(111)` to the `Neg` cell: `main` returned 1. Check-green, verify-green,
silently wrong. The family now renders the whole resolved type through
`types.structural_type_key`, so each of the three routes to its own cell.
The measured matrix, all four flips value-oracled in
`tests/test_family_naming.py` §8:
Pos outside / Neg inside, callee bound to Pos 1 -> 111
Neg outside / Pos inside, callee bound to Neg -1 -> -222
Int outside / Pos inside, callee bound to Int 0 -> 7
three-deep Pos/Neg/Pos, middle clause body E602 refusal -> 42
The last one is the PR aallan#1232 addressability-gate interaction: with all three
collapsed to `Int` the gate saw a same-family nest and refused the program
outright. Distinct families make the shape legal again, and it routes per
§7.5.2 — the middle (Neg) clause body's bare `put` reaches the outermost Pos
handler, whose cell is the Pos family's innermost by then.
IDENTITY is now separate from REPRESENTATION, and that split is the rest of
the change. Every decision keyed on the family's TEXT — i32/i64/f64,
pointer-ness for the GC shadow stack, pair-ness for a `String` payload, and
which aallan#1203 write guard applies — takes `naming.family_base_name` instead: a
family that discriminates the predicate matches nothing in the `"Nat"` /
`"Int"` / `"Byte"` / `"Bool"` / `"String"` tables, so one name doing both
jobs would have switched all of them off SILENTLY while the verifier went on
recording the guards as `tier3_runtime`. The two are derived side by side
from one type expression and carried together (`CellNames`), never
substituted for each other. A differential pins it: the refined `@Nat` cell
emits guard-for-guard what the bare one does, and routing the clause-path
guard back onto the identity drops it from two sites to one.
The seam that made this dangerous is gone rather than repaired. Two sites
recovered a cell family by SLICING it back out of its own mangled
`$vera.state_put_…` dispatch target — the addressability gate and the bare
`put` guard — a second derivation that worked only because `Nat`/`Int`/
`Byte` mangle to themselves, and the one aallan#1233 round 5 found re-mangling an
already-mangled name at. Both now read `_effect_op_cells`, a fourth
registry in lock-step with `_effect_ops`, so one canonical family is
threaded to both consumers and `_state_import_family` is deleted.
Host surfaces verified rather than assumed: the browser bundle's
`/^state_get_(.+)$/` synthesis splits the 223-character mangled suffixes,
keeps the two cells apart, and returns 111 under Node — the same answer
wasmtime gives. The WASI target gates every `State` program before its
narrower import regex, unchanged.
Corpus: `ch07_state_refined_cell_family` promotes the repro at run level
with the 111 oracle. `alias_families/p9_refined_state_minimal` and
`p25_refined_cell` asked "does a refined cell compile, and into what
family?"; both are dispositioned into that program and the guard
differential. Nine probe programs' family symbols rename deterministically
and one, `write_guards/p8_refined_state`, splits 4 -> 8 imports — a refined
cell nested in its own base, which was one cell and is now correctly two.
Nothing else in the corpus moves.
Co-Authored-By: Claude <noreply@anthropic.invalid>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Handler semantics: deterministic op ownership, enclosing-context clause ops, complete registration (#1210, #1211, #1215, #1231)
Part of the #1213 burndown (integration branch
release/v0.1.10; PR B of the plan on the #1213 thread). Five commits, each through the full gate.#1215 — bare effect-op resolution is deterministic and source-ordered. Two effects declaring one op name (builtin
StateandHttpboth declareget— no user effect needed) bound by frozenset iteration: the same program compiled on hash seeds 3/4 and failed E217 on the rest. The row now travels with theast.EffectSetdeclaration order; resolution walks innermost enclosing handler → enclosing handlers outward → the declared row in SOURCE order → registered effects in registration order. Seed matrix 0–7: uniform. The reversed row proves source-order (E217 namingHttp.getdeterministically); a handled-inner shape proves precedence. Spec §7.4 gains the rule; §7.4.1 corrected (it claimed ambiguous bare calls are rejected — they are not).#1231 — the type-argument leg of the same lottery, found by this fix's own seed sweep. Spec §7.3.3 permits
effects(<State<Int>, State<Bool>>);_effect_type_mapping's frozenset fallback made the same program check-clean on half the seeds and E121 on the other half — and fixing it exposed a deterministic codegen desync underneath (the last State instantiation overwrote the first:state_get_Booli32 emitted for a checker-typedInti64). Both sides now walk the ordered row, first-written wins.#1211 — a clause body's bare ops lower against the enclosing context. The checker has always resolved a nested handler's clause-body
get/putagainst the context where the handler is declared; codegen lowered them against the handler's own cell — silent wrong values.StateClauseEntrynow carries the whole declaration-time scope (the four op/result mirrors beside the existingdecl_env), restored around clause-body andwith-expression translation;_state_clause_familydeliberately stays at the clause's own values (it typesresume). Termination invariant rewritten: the restored registry is from strictly outside the handler, so re-entry walks outward through finite nesting. The checker=codegen=verifier matrix (8 shapes, nesting depths 1–3, bare + qualified ops, both result-type mirrors individually mutation-validated) pins every value to the checker's story — with verifier tier counts identical before/after, so "verifier already agrees" is verified, not assumed. Spec §7.5.2 gains the explicit sentence. Corpus: exactly two probe programs moved, both to their header-documented checker values.#1210 — State/Exn registration walks every handler position. Clause bodies, state-init expressions, and
withupdates never registered the families their lowerings reference: check-green programs died at whole-module WAT compile (unknown func $vera.state_push_Bool), and the i32_pair silent skip madehandle[State<String>]in a pure fn invalid WASM. All positions now register through one shared derivation, and the silent skip is the same loud E607 the declared path emits. Permanent cross-component differential:test_every_referenced_state_exn_symbol_is_declaredsweeps 226 compiled programs / 132 distinct symbols with floors and its own red-proof.Probes: conformance 196 → 199 (three run-level programs: clause-body enclosing, registration positions, op source-order); the #1210/#1211/#1215 probe pools promoted or deleted with per-file reasoning; all three remaining parse-broken probes dispositioned (two deleted as subject-covered-elsewhere, one deleted as premise-refuted); probes 250 → 240, parse-broken 5 → 2. KNOWN_ISSUES rows for the three issues deleted; CHANGELOG bullets name all four issues.
Closes #1210. Closes #1211. Closes #1215. Closes #1231.
(Close-keywords take effect at the release PR to main, per the integration-branch model.)
Review provenance
Implemented by the burndown's agent process on the post-consolidation shape; adversarial review to fixed-point and CodeRabbit ledger convergence follow on this PR before self-merge into the integration branch, per the #1213 protocol.
Summary by CodeRabbit
New Features
getandput.Bug Fixes
Documentation