release: v0.1.4 — the second burndown (19 bug fixes) - #1016
Merged
Conversation
…stream (#974) The verify summary was hand-accumulated across ~94 counter writes that could desync from the obligation stream a consumer reads — on three call-demotion examples, tier1_verified + tier3_runtime = total + 1 (#967). The summary is now derived: summarize(obligations) is the single source of truth, exposed as a computed property on ContractVerifier, on both the cold verify path and the warm VerificationSession. verify --json additionally exposes the obligations array with normalized per-obligation locations that join to diagnostics on (file, line, column). CI and CodeRabbit now cover PRs targeting release/** branches, with workflow concurrency cancelling superseded PR runs. Closes #967 Co-Authored-By: Claude <noreply@anthropic.invalid>
The checker bound handler state into the handled body's slot scope — a binding neither the verifier nor the WASM backend models — so a body state-slot read passed check and verify, then crashed compile with a dangling-slot E699 (and silently desynced checker/codegen slot identity when a same-typed parameter was in scope). Per spec §7.5 and DESIGN principles 2/3/6, state is in scope in handler clauses only: the body reaches it through get(())/put(...), and a body slot read is now E130 with a get(()) hint (gated on no real binding of the type existing and the innermost enclosing handler's state type; clause checks mask the hint). Slot identity is pinned end-to-end at run level. Review of this PR also surfaced #976 (State handler clauses type-checked but never executed), filed with tracker rows. Closes #973 Co-Authored-By: Claude <noreply@anthropic.invalid>
… parameter slot (#977) The checker checked where-helper bodies (and their contracts) while the parent function's value-slot scope was still pushed, so an outer parameter slot resolved at check and verify, then crashed compile with a dangling-slot E699 — the backends compile each helper as an independent param-rooted scope. Per spec §5 and DESIGN principles 2/5, helpers are closed param-rooted scopes: the parent's value scope now pops before the where-fn loop, an outer slot read (body or contract clause) is E130 with a pass-as-argument hint (gated to the immediate parent's param types; handler-state hint takes precedence inside handled bodies), and parent type params remain available. With #973 and this both sealed, the E699 dangling-slot guard's known source routes are gone (guard kept as a soundness net). Review of this PR surfaced #978 (nested where-helpers never emitted by the non-generic codegen path), filed with tracker rows. Closes #969 Co-Authored-By: Claude <noreply@anthropic.invalid>
…red forall var (#980) A bare nullary constructor under forall — None returned as @option<T>, bound by let, or unified across match arms — minted a fresh type variable instead of adopting the declared forall var, rejecting well-typed programs with E121/E170/E302 messages describing types that unify trivially. The fix is a one-line relaxation in _ctor_result_type's bidirectional fill: an expected argument that is itself a TypeVar is now adopted. Soundness rests on the same-ADT guard (a constructor only ever adopts its own parent declaration's variable) and argument-driven inference keeping priority (Some(5) under forall<T> still rejects, with negative pins). Pinned across all three positions, at two instantiation types, at the verify layer, and end-to-end via the 148th conformance program. Review of this PR surfaced and filed #979 (nested constructor fields) and #981 (comparison operands) — the same family through the two remaining propagation paths. Closes #971 Co-Authored-By: Claude <noreply@anthropic.invalid>
… collide with user forall vars (#982) The inference skip-guard compared a concrete argument's type-args against the callee's forall_vars by name, and the builtin registry named its internal generics T/U/A/B/E/K/V — so a user forall var sharing any of those names silently aborted unification. The filed bare-shape repro was masked by the name coincidence; the live defect was a spurious E202 whenever the colliding user var was the immediate type-argument of a compound argument type, across every generic-builtin family, in bodies, contract clauses, and where-helpers. Every registry internal var is now alpha-renamed at registration with a parser-unwritable #b suffix (forall_vars, param/return types, AND ability constraints — no drift), the marker is stripped from every user-facing surface, and the rename exposed and closed a dual gap: a concrete argument now overrides a type variable leaked unresolved from a nested generic call, pinned in both argument orders. Guarded by a 19-pair collide-vs-control battery (29 tests), per-name mutation validation, a run-level conformance program, and an extended doc-counts gate covering the previously gate-blind prose sites. Closes #970 Co-Authored-By: Claude <noreply@anthropic.invalid>
…ion return position (#983) A @nat function return whose body narrows from @int was neither statically obligated nor runtime-guarded: to_nat(@int -> @nat){ @Int.0 } verified clean at Tier 1 and to_nat(0 - 5) returned -5 through the @nat slot. The verifier's new step-7d emits the nat_bind result >= 0 obligation at the return slot under the body's path conditions, descending if/match joins to their leaf expressions (the target-typed body masks narrowing arms); examples/absolute_value.vera proves at Tier 1. Codegen mirrors it with per-leaf return guards — narrowing leaves trap inline while non-narrowing leaves, including @nat -> @nat recursive tail calls, keep return_call (TCO preserved at 200k depth). Both codegen return gates (narrow and the pre-existing #813 widen sibling) resolve type aliases, closing a verify-promised-but-unemitted guard hole on alias-typed returns. The verifier<->codegen agreement is pinned by a four-quadrant differential (violated/tier3/proven, alias, join and let shapes). Review of this PR surfaced #984 (closure return narrowing unguarded), filed with tracker rows. The corpus tier pins and differential oracle now measure the CLI pipeline exactly (resolver + semantic-type artifacts), closing a long-standing two-obligation measurement divergence. Closes #758 Co-Authored-By: Claude <noreply@anthropic.invalid>
…d the remaining @Nat->@int widening sites (#986) The checker's expr_target_types side-table now reaches code generation, and the @Nat->@int widening is obligated and runtime-guarded at the array-element, tuple construction/destructure, heterogeneous if/match per-arm, and closure argument/return/capture sites. Review round hardened the per-arm machinery: target-aware gate (no false trap in @Nat-returning joins), tail-call arms keep a live guard (plain call) while genuine @int arms keep TCO, vera test threads the artifact tables, a user data Tuple no longer takes the builtin carrier path, and imported bodies are excluded from span-keyed recovery (a proven collision could false-guard). Residuals filed: #985 (nested-closure reporting gap), #987 (cross-module guard emission). Closes #820 Co-Authored-By: Claude <noreply@anthropic.invalid>
…ed paths (#989) The non-generic Pass-2 emission loop, the Pass-1.6 ability-op rewrite, and the imported-module registration each recursed only one level of a function's where-helper tree while the checker, verifier, and registration recursed fully — so a helper's own where-helpers were checked and verified but never emitted, and a check-green program failed vera compile with an internal unknown-func error. All three now walk the full tree via a shared _flatten_where_fns (pre-order DFS), pinned by run-level tests at 2/3 levels, branching-at-depth, eq/compare in grandchild bodies and contracts, cross-module chains, and the shadowed-import path, plus tests/conformance/ch05_nested_where_helpers.vera. Review round filed three pre-existing bugs with tracker rows riding this PR: #990, #991, #992. Closes #978 Co-Authored-By: Claude <noreply@anthropic.invalid>
…nd comparison operands (#994) The two remaining checker mechanisms of the fresh-ctor-var family after #971: the constructor-argument loop now forwards typevar-bearing expected field types into nested constructor arguments (Some(None) as @option<Option<T>> adopts the declared var at every level), and the ==/!= comparison synthesis re-synthesizes an unresolved constructor operand with the sibling's concrete ADT type (ensures(@option<T>.result == None) checks; the concrete form was broken too and is fixed). Review round fixed the same payload-less-ctor gap in two downstream components the newly-accepted shapes reach: the SMT layer's nullary sort resolution (crashed vera verify with a Z3 sort mismatch; now hinted from recorded types with an honest Tier-3 backstop) and the structural-Eq derivation (spurious E613; now recovers the concrete type from the sibling operand — load-bearing for soundness). Sixth family mechanism filed as #993 with tracker rows riding this PR; conformance sentinel chain now runtime-enforced. Closes #979 Closes #981 Co-Authored-By: Claude <noreply@anthropic.invalid>
…at closure returns (#995) The closure body's return leaf was the one narrowing site neither obligated nor guarded — fn(@int -> @nat) { @Int.0 } applied to a negative returned it through the @nat slot silently on a verify-clean program. Both sides in lockstep at the hooks #820 built for the widening dual: a shallow tier3 nat_bind on the verifier's AnonFn arm (body opaque to SMT — never a false Tier-1) and per-leaf return guards in the lifted closure (a whole-body wrap would false-trap a captured @nat above 2^63-1 in a heterogeneous body). Review round: zero findings against the fix logic from four reviewers; hardening applied (trap-kind pins, sign-boundary class, measured zero-guard pin on the refinement exclusion, defensive leaf-set reset); the once-observed conformance trap is tracked as #996 (unreproducible in ~960 attempts); #985's scope extended to the narrowing direction; docs coverage rows qualified against the #765/#985 exceptions. Closes #984 Co-Authored-By: Claude <noreply@anthropic.invalid>
…t the #820 widening guards (#997) The #820 per-component @nat -> @int widening guards were dropped for imported module bodies (Pass 2.5/2.6): the checker's span-keyed target tables were main-file-only, so the library's Tier-3 promise was silently broken through the import door (u64.MAX -> -1). Checker artifacts now carry per-module tables (opt-in, codegen-bound commands only), threaded into imported-body compilation; the #986 suppression becomes the fallback. Residual for imported generic mono clones tracked as #998. Closes #987 Co-Authored-By: Claude <noreply@anthropic.invalid>
…thread origin-module tables into imported-generic clones (#1001) Nested forall<T> where-helpers under non-generic parents are now monomorphization bases — one shared collector feeds both codegen Pass 1.5 and the verifier's instance discovery, so nested instantiations are emitted AND verified per-monomorphization in lockstep (#990). Clones of imported generics carry their origin module and compile against that module's span tables, so the #820 widen guards fire at every instantiation through the import door — main-worklist, shadowed mod$ clones, transitive chase, and hoisted where-helpers (#998). Adversarial panel: zero findings. Siblings found by this PR's reviews filed as #999, #1000, #1002. Closes #990 Closes #998 Co-Authored-By: Claude <noreply@anthropic.invalid>
…nsic-hybrid semantics (#1003) Clause bodies and 'with' state-update expressions were type-checked but never lowered. Under the maintainer-pinned option-C semantics: put stores / get reads intrinsically; the matching clause body executes with resume(value) as the op's result; 'with @t = expr' overrides the intrinsic store; @T.0 is captured pre-store (keep-old via 'with @t = @T.0'). Inline lowering over the existing host-cell imports — no host changes, browser in lockstep, wasi-p2 unchanged. resume is single-shot with a structural tail gate; clauses are lexical to the handled body's own op sites; nested handlers own their op names wholesale; a pre-existing init-expression cell misread is fixed. Corpus migrated off the formerly-no-op 'with @t = @T.0'. Spec §7.5 rewritten. Review round: 3 agents + 2-lens panel; siblings filed as #1004, #1005, #1006. Closes #976 Closes #988 Co-Authored-By: Claude <noreply@anthropic.invalid>
#1007) The Pass-1.6 ability-op rewrite (eq -> BinaryExpr, compare -> if-chain) never ran over _imported_fn_decls / _shadowed_module_fns, so an eq anywhere in an imported body stayed a raw call codegen cannot lower — the body dropped and the importer's call dangled (unknown func) on a check-green, verify-green pair. The rewrite now runs over every imported entry via a factored helper shared with the mono loop. Sibling pre-existing find filed as #1008 (ctor layouts gated on the importer's type import). Closes #992 Co-Authored-By: Claude <noreply@anthropic.invalid>
…, and init positions (#993) (#1009) * fix(checker): adopt expected types for bare nullary ctors in call, op, and init positions (#993) Final mechanism of the fresh-ctor-var family (#971 return/let/match, #979 nested fields, #981 comparison operands): five argument-position sites still minted an unresolvable T$n and rejected well-typed programs. - The #971 bidirectional fill now overrides a tentative type-arg binding whose value is a bare fresh var (the #293 fresh-is-tentative precedence), fixing MkA(None) under a bare forall var (E121). - The generic-call argument loop treats a residual type variable on either side as a structural wildcard before rejecting (E202), while cross-ADT and concrete-leaf mismatches stay rejected. - Ability-op constructor arguments re-synthesize against the resolved parameter type (E241), at concrete and forall expected types alike. - The handler-state initializer synthesizes with the declared state type expected (E331). - A both-constructor comparison may adopt from a resolved ctor sibling (E142); None == None stays rejected. Pinned by eight tests (six fixed shapes + two guardrails) with a seven-mutant battery. Co-Authored-By: Claude <noreply@anthropic.invalid> * fix(checker): scope #993 wildcards to unresolved vars; re-anchor ability mapping on resolved args (PR #1009 review) All five CodeRabbit round-1 findings verified live and fixed: - _compatible_modulo_typevars takes the enclosing forall params as a RIGID set (env.type_params): only fresh T$n, builtin-marked, and leaked callee vars are wildcards. The first cut wildcarded every TypeVar, silently accepting g(@option<T>.0) where Option<Int> is required — a soundness regression, now E202 again and pinned. - The FunctionType branch requires is_effect_subtype: <IO> can never satisfy a pure formal through the wildcard path (defense-in-depth; unit-pinned — not surface-constructible at head since builtin unresolved vars are UnknownType and bypass the compat path). - _ability_type_mapping applies the #293 fresh-is-tentative precedence: eq(None, Some(5)) and ensures(eq(None, result)) check in both operand orders; eq(None, None) stays rejected via a new fresh-param gate on the ctor re-synth. - _resynth_eq_ctor_operand's adoption guards use the new contains_fresh_typevar walker: Some(@T.0) == None under forall<T where Eq<T>> checks; None == None stays rejected. - Reversed-order pins for every shape + handler-init IntLit coercion pin (reviewer Note B). Test class grows 8 -> 18 with a 12-mutant battery (all killed). The review also surfaced pre-existing #1010 (static E503 narrowing obligation lost when a ctor argument's param type contains a typevar) — filed, with KNOWN_ISSUES + SKILL rows riding this PR. Co-Authored-By: Claude <noreply@anthropic.invalid> --------- Co-authored-by: Claude <noreply@anthropic.invalid>
…concrete Nat components obligate (#1010) (#1011) * fix(checker): re-synth ctor args against partially-generic params so concrete Nat components obligate (#1010) Every re-synthesis in the generic-call argument loop was gated on the WHOLE parameter being typevar-free, so a constructor argument against @pair<Nat, T> was never re-typed against its instantiated parameter — the concrete Nat component's narrowing target went unrecorded and the E503 obligation was silently lost (verify-clean negative into a Nat; the fully-concrete analogue obligates). Constructor-expression arguments now re-synth against the instantiated param even when typevars remain: the #971 fill adopts component-wise, typevar components stay unconstrained, and each field's target records exactly as on the concrete path. Provably-negative and unconstrained @int shapes are E503; requires(@Int.0 >= 0) discharges Tier-1; genuine Nat values stay clean. Runtime-guard half for generic fields unchanged (documented under #754/#757) — the static promise is what #1010 restored. Found by the PR #1009 review. Five pinning tests, revert mutant killed. Co-Authored-By: Claude <noreply@anthropic.invalid> * docs(changelog): reconcile the #993 entry's #1010 pointer with the fix entry above The #993 bullet said #1010 was 'tracked in KNOWN_ISSUES'; its fix now sits directly above in the same [Unreleased] batch and the row is deleted, so the clause was self-contradictory in the extracted notes. Skip-changelog: prose reconciliation within [Unreleased] itself, no code change Co-Authored-By: Claude <noreply@anthropic.invalid> * test(verifier): assert exact E503 codes and Tier-1 discharge in the #1010 pins (PR #1011 review) The E503 shapes now assert error_code explicitly and the constrained case asserts the nat_bind obligation status is 'verified' — mere error-absence could not distinguish a Tier-3 runtime fallback. Skip-changelog: test-assertion strengthening only, behavior unchanged Co-Authored-By: Claude <noreply@anthropic.invalid> --------- Co-authored-by: Claude <noreply@anthropic.invalid>
… the verifier's helper lookup (#991) (#1013) Closes #991 Parent-qualifies non-generic where-helper names and threads lexical helper resolution through checker, verifier, and codegen so all three agree on helper-name scoping. Four review rounds hardened it against ancestor-capture (silent wrong value + false Tier-1), verifier enclosing-scope drop, the checker false-rejection leg, and the import-shadow set. Discovered pre-existing issues #1012, #1014, #1015 filed with tracker rows. Co-Authored-By: Claude <noreply@anthropic.invalid>
Version 0.1.3 -> 0.1.4 across the six-file surface; CHANGELOG [Unreleased] -> [0.1.4] with compare links; HISTORY Stage 19+20 row; ROADMAP bug-sprint section for the ten review-surfaced residuals; site assets regenerated. The docs sweep found no stale-workaround prose for the 19 fixed bugs — the per-PR lockstep kept the reference docs current; the KNOWN_ISSUES Bugs table holds exactly the 11 open rows. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
Too many files changed for review. ( Bypass the limit by tagging |
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 14 minutes 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 ignored due to path filters (2)
📒 Files selected for processing (5)
📝 WalkthroughWalkthroughVera 0.1.4 updates compiler, verifier, WebAssembly code generation, State handler semantics, generic inference, cross-module artefact propagation, regression coverage, documentation, release metadata, and CI/review configuration. ChangesVera 0.1.4 compiler and release update
Estimated code review effort: 5 (Critical) | ~120 minutes Sequence Diagram(s)sequenceDiagram
participant CLI
participant TypeChecker
participant Verifier
participant CodeGenerator
participant WasmRuntime
CLI->>TypeChecker: typecheck_with_artifacts
TypeChecker-->>CLI: semantic, target, and module artefacts
CLI->>Verifier: verify with artefacts
Verifier-->>CLI: obligations and derived summary
CLI->>CodeGenerator: compile with target and module artefacts
CodeGenerator-->>WasmRuntime: guarded WebAssembly
WasmRuntime-->>CLI: execution result or trap
Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 7 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (7 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1016 +/- ##
==========================================
+ Coverage 93.41% 93.51% +0.09%
==========================================
Files 96 96
Lines 31479 32005 +526
Branches 456 456
==========================================
+ Hits 29406 29928 +522
- Misses 2060 2064 +4
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: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
tests/test_nat_narrowing_return_differential.py (1)
522-554: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winUnused
statusesintest_refined_return_single_guard_no_double.
statusesis unpacked from_statuses_and_wat(_CLOSURE_REFINED)but never asserted — onlywatis used. Given this test's whole point is confirming the#984narrowing gate doesn't double-fire on a refined return, asserting the obligation-status side (e.g. no spuriousnat_bind) would close the loop rather than relying solely on the WAT-string absence ofi64.lt_s.🧪 Suggested fix
statuses, wat = _statuses_and_wat(_CLOSURE_REFINED) + assert statuses == [], ( + f"refined closure return should carry no nat_bind obligation " + f"(handled by refine_bind instead): {statuses}" + ) anon = wat[wat.index("(func $anon_"):]🤖 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_nat_narrowing_return_differential.py` around lines 522 - 554, Use the unpacked statuses in test_refined_return_single_guard_no_double by asserting the expected obligation status for _CLOSURE_REFINED, specifically that no spurious nat_bind is present. Keep the existing WAT guard-count and runtime assertions unchanged.Source: Path instructions
vera/codegen/core.py (1)
1544-1567: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winDuplicate ability-op rewrite logic — use the new
_rewrite_fn_ability_opshelper.The
program.declarationsloop (lines 1547-1564) re-implements exactly what_rewrite_fn_ability_ops(added in this same diff) already does — rewrite body,where_fns, and contracts, then replace on change. Calling the new helper here removes the duplication and the risk of the two copies drifting apart on a future edit (e.g. if_rewrite_fn_ability_opsgains another rewritten field, this inline copy silently falls behind).♻️ Proposed refactor
for tld in program.declarations: if isinstance(tld.decl, ast.FnDecl) and not tld.decl.forall_vars: - new_body = self._rewrite_ops_in_expr( - tld.decl.body, ability_ops) - new_where = self._rewrite_where_fns( - tld.decl.where_fns, ability_ops) - new_contracts = self._rewrite_ops_in_contracts( - tld.decl.contracts, ability_ops) - if (new_body is not tld.decl.body - or new_where is not tld.decl.where_fns - or new_contracts is not tld.decl.contracts): - new_decl = _replace( - tld.decl, body=new_body, # type: ignore[arg-type] - where_fns=new_where, - contracts=new_contracts) - tld = _replace(tld, decl=new_decl) + new_decl = self._rewrite_fn_ability_ops(tld.decl, ability_ops) + if new_decl is not tld.decl: + tld = _replace(tld, decl=new_decl) prog_changed = True new_tlds.append(tld)Also applies to: 1592-1611
🤖 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/core.py` around lines 1544 - 1567, Replace the inline body, where_fns, and contracts rewriting in the program.declarations loop with the existing _rewrite_fn_ability_ops helper. Preserve the current non-generic FnDecl filtering and declaration replacement behavior, and apply the same helper-based refactor to the corresponding logic around the second affected declaration loop.
🤖 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 205-209: Update the check-level summary in TESTING.md to change
“Fifteen programs” to “Sixteen programs” and add ch08_xmod_widen_lib to the
listed check-level programs, preserving the existing classifications and
details.
In `@vera/codegen/closures.py`:
- Around line 273-275: Update the closure setup calls to
ctx.set_expr_semantic_types and ctx.set_expr_target_types by casting each
optional Type-valued side-table to the setter’s expected dictionary type,
matching the cast approach used for module_tables in functions.py.
In `@vera/verifier.py`:
- Around line 3208-3230: Update the special-case apply_fn handling to also
validate `@Int` arguments passed to `@Nat` closure formals. In the formals loop
using _closure_arg_param_types, mirror the generic call path’s
_nat_binding_target and _narrows_into_nat logic, applying the required verifier
obligation and call_indirect guard while preserving the existing `@Nat-to-`@Int
widening check.
---
Outside diff comments:
In `@tests/test_nat_narrowing_return_differential.py`:
- Around line 522-554: Use the unpacked statuses in
test_refined_return_single_guard_no_double by asserting the expected obligation
status for _CLOSURE_REFINED, specifically that no spurious nat_bind is present.
Keep the existing WAT guard-count and runtime assertions unchanged.
In `@vera/codegen/core.py`:
- Around line 1544-1567: Replace the inline body, where_fns, and contracts
rewriting in the program.declarations loop with the existing
_rewrite_fn_ability_ops helper. Preserve the current non-generic FnDecl
filtering and declaration replacement behavior, and apply the same helper-based
refactor to the corresponding logic around the second affected declaration loop.
🪄 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: 76b7e021-8eeb-4409-924c-6dcdb3a915a4
⛔ Files ignored due to path filters (22)
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/effect_handler.verais excluded by!**/*.veratests/conformance/ch04_nat_return_obligation.verais excluded by!**/*.veratests/conformance/ch05_closure_nat_return.verais excluded by!**/*.veratests/conformance/ch05_nested_where_helpers.verais excluded by!**/*.veratests/conformance/ch05_where_helper_outer_slot_rejected.verais excluded by!**/*.veratests/conformance/ch07_handler_state_body_scope_rejected.verais excluded by!**/*.veratests/conformance/ch07_nested_handlers.verais excluded by!**/*.veratests/conformance/ch07_state_clause_transform.verais excluded by!**/*.veratests/conformance/ch07_state_composite.verais excluded by!**/*.veratests/conformance/ch07_state_handler.verais excluded by!**/*.veratests/conformance/ch08_xmod_widen.verais excluded by!**/*.veratests/conformance/ch08_xmod_widen_lib.verais excluded by!**/*.veratests/conformance/ch09_generic_builtin_typevar.verais excluded by!**/*.veratests/conformance/ch09_generic_none_nested.verais excluded by!**/*.veratests/conformance/ch09_generic_none_return.verais excluded by!**/*.veratests/conformance/ch09_generic_where_nongeneric_parent.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (84)
.coderabbit.yaml.github/workflows/ci.ymlAGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdHISTORY.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdpyproject.tomlscripts/check_doc_counts.pyspec/02-types.mdspec/05-functions.mdspec/06-contracts.mdspec/07-effects.mdspec/11-compilation.mdtests/conformance/manifest.jsontests/test_browser.pytests/test_builtin_typevar_collision_970.pytests/test_checker_effects.pytests/test_checker_functions.pytests/test_checker_types.pytests/test_cli.pytests/test_codegen_effects.pytests/test_codegen_modules.pytests/test_codegen_monomorphize.pytests/test_codegen_nat_guards.pytests/test_codegen_nested_nullary_ctor_994.pytests/test_codegen_where_helper_mangling_991.pytests/test_generic_where_helper_990.pytests/test_hetero_widen_tailcall.pytests/test_int_widening_codegen.pytests/test_int_widening_differential.pytests/test_monomorphize_differential.pytests/test_nat_int_widening.pytests/test_nat_narrowing_return_differential.pytests/test_obligations.pytests/test_state_clause_semantics.pytests/test_tester_artifacts.pytests/test_verifier_adt_decreases.pytests/test_verifier_contracts.pytests/test_verifier_nat_obligations.pytests/test_verifier_nullary_ctor_sort_994.pytests/test_verifier_where_helper_scope_991.pytests/test_xmod_ability_ops_992.pytests/test_xmod_artifact_collection.pytests/test_xmod_generic_widen_gap.pytests/test_xmod_span_collision.pytests/test_xmod_where_helper_import_991.pytests/test_xmod_widening_differential.pyvera/README.mdvera/__init__.pyvera/checker/calls.pyvera/checker/control.pyvera/checker/core.pyvera/checker/expressions.pyvera/checker/resolution.pyvera/cli.pyvera/codegen/api.pyvera/codegen/closures.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/modules.pyvera/codegen/monomorphize.pyvera/environment.pyvera/monomorphize.pyvera/obligations/cache.pyvera/obligations/core.pyvera/obligations/session.pyvera/registration.pyvera/smt.pyvera/tester.pyvera/types.pyvera/verifier.pyvera/wasm/calls.pyvera/wasm/calls_handlers.pyvera/wasm/closures.pyvera/wasm/context.pyvera/wasm/data.pyvera/wasm/inference.pyvera/wasm/operators.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)
- tests/test_browser.py
There was a problem hiding this comment.
Actionable comments posted: 5
🤖 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 224: Update the project-status test count in FAQ.md from 7,347 to 7,391,
preserving the existing 157-program conformance-suite wording and keeping it
consistent with README.md, TESTING.md, ROADMAP.md, and the count check.
In `@vera/codegen/functions.py`:
- Around line 449-470: In the nat_leaf_ids setup and the corresponding logic
around the other referenced guard path, replace the inlined
_resolve_base_type_name and string comparison with the shared
ctx._type_expr_base_is_nat/_type_expr_base_is_int helpers used by closures.py.
Preserve the existing refinement exclusion and narrowing-leaf collection
behavior while keeping function and closure guard setup aligned.
In `@vera/environment.py`:
- Around line 1906-1912: In the TypeEnv construction logic around original_vars,
remove the separate renamed_name comprehension and derive renamed_name from the
existing rename mapping using each TypeVar’s name, preserving the current
key/value behavior.
In `@vera/wasm/closures.py`:
- Around line 150-167: Update _translate_apply_fn’s argument translation loop to
also emit the existing _emit_nat_bind_guard when a closure formal type is Nat
and the corresponding argument result is Int. Preserve the current
_emit_int_widen_guard behavior for Nat arguments passed to Int formals, and
apply the Nat guard using the same formal_types and per-argument checks.
In `@vera/wasm/inference.py`:
- Around line 1654-1682: Extract the duplicated _closure_arg_param_types logic
into a shared free function in vera/monomorphize.py alongside
resolve_fn_type_alias, accepting closure_arg, type_aliases, and
type_alias_params. Update the implementations in the three owning classes/files
to delegate to that helper, preserving SlotRef alias resolution, AnonFn
parameter handling, and None for unsupported expressions.
🪄 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: 76b7e021-8eeb-4409-924c-6dcdb3a915a4
⛔ Files ignored due to path filters (22)
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/effect_handler.verais excluded by!**/*.veratests/conformance/ch04_nat_return_obligation.verais excluded by!**/*.veratests/conformance/ch05_closure_nat_return.verais excluded by!**/*.veratests/conformance/ch05_nested_where_helpers.verais excluded by!**/*.veratests/conformance/ch05_where_helper_outer_slot_rejected.verais excluded by!**/*.veratests/conformance/ch07_handler_state_body_scope_rejected.verais excluded by!**/*.veratests/conformance/ch07_nested_handlers.verais excluded by!**/*.veratests/conformance/ch07_state_clause_transform.verais excluded by!**/*.veratests/conformance/ch07_state_composite.verais excluded by!**/*.veratests/conformance/ch07_state_handler.verais excluded by!**/*.veratests/conformance/ch08_xmod_widen.verais excluded by!**/*.veratests/conformance/ch08_xmod_widen_lib.verais excluded by!**/*.veratests/conformance/ch09_generic_builtin_typevar.verais excluded by!**/*.veratests/conformance/ch09_generic_none_nested.verais excluded by!**/*.veratests/conformance/ch09_generic_none_return.verais excluded by!**/*.veratests/conformance/ch09_generic_where_nongeneric_parent.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (84)
.coderabbit.yaml.github/workflows/ci.ymlAGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdHISTORY.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdpyproject.tomlscripts/check_doc_counts.pyspec/02-types.mdspec/05-functions.mdspec/06-contracts.mdspec/07-effects.mdspec/11-compilation.mdtests/conformance/manifest.jsontests/test_browser.pytests/test_builtin_typevar_collision_970.pytests/test_checker_effects.pytests/test_checker_functions.pytests/test_checker_types.pytests/test_cli.pytests/test_codegen_effects.pytests/test_codegen_modules.pytests/test_codegen_monomorphize.pytests/test_codegen_nat_guards.pytests/test_codegen_nested_nullary_ctor_994.pytests/test_codegen_where_helper_mangling_991.pytests/test_generic_where_helper_990.pytests/test_hetero_widen_tailcall.pytests/test_int_widening_codegen.pytests/test_int_widening_differential.pytests/test_monomorphize_differential.pytests/test_nat_int_widening.pytests/test_nat_narrowing_return_differential.pytests/test_obligations.pytests/test_state_clause_semantics.pytests/test_tester_artifacts.pytests/test_verifier_adt_decreases.pytests/test_verifier_contracts.pytests/test_verifier_nat_obligations.pytests/test_verifier_nullary_ctor_sort_994.pytests/test_verifier_where_helper_scope_991.pytests/test_xmod_ability_ops_992.pytests/test_xmod_artifact_collection.pytests/test_xmod_generic_widen_gap.pytests/test_xmod_span_collision.pytests/test_xmod_where_helper_import_991.pytests/test_xmod_widening_differential.pyvera/README.mdvera/__init__.pyvera/checker/calls.pyvera/checker/control.pyvera/checker/core.pyvera/checker/expressions.pyvera/checker/resolution.pyvera/cli.pyvera/codegen/api.pyvera/codegen/closures.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/modules.pyvera/codegen/monomorphize.pyvera/environment.pyvera/monomorphize.pyvera/obligations/cache.pyvera/obligations/core.pyvera/obligations/session.pyvera/registration.pyvera/smt.pyvera/tester.pyvera/types.pyvera/verifier.pyvera/wasm/calls.pyvera/wasm/calls_handlers.pyvera/wasm/closures.pyvera/wasm/context.pyvera/wasm/data.pyvera/wasm/inference.pyvera/wasm/operators.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)
- tests/test_browser.py
- TESTING.md: the check-level prose listed 15 programs but the table (and doc-counts gate) count 16 — add ch08_xmod_widen_lib (CodeRabbit). - File #1017: the @int->@nat narrowing into an apply_fn @nat closure formal is not obligated (false Tier-1, pre-existing, narrowing dual of the #820 widening handler) — KNOWN_ISSUES + SKILL rows + ROADMAP PR D. Skip-changelog: docs + tracker rows on the release PR; #1017's fix carries the entry Co-Authored-By: Claude <noreply@anthropic.invalid>
…AQ count (PR #1016 review) - HISTORY: v0.1.3 and v0.1.4 rows trimmed from paragraphs to concise one-liners matching the row style. - ROADMAP Stage 19: removed backward-looking narration (the #820 'landed / now retired' commentary and the burndown-history framing) — the roadmap states future work; that history lives in CHANGELOG. - FAQ.md: stale test count 7,347 -> 7,391 (CodeRabbit). Skip-changelog: docs-only prose/count edits on the release PR Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai On the two batch-1 outside-diff findings: (1) |
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 (3)
FAQ.md (1)
181-181: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winNarrow the JustHTML claim or cite the exact post.
The December 2025 material supports an LLM-assisted HTML implementation driven by the html5lib conformance suite, but this wording additionally claims it implemented a specification the model had little training data for. Please link the specific post and narrow the claim to what it demonstrates. (feeds.simonwillison.net)
As per path instructions, Markdown changes must be checked for factual accuracy against the codebase and cited sources.
🤖 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 `@FAQ.md` at line 181, The FAQ paragraph’s JustHTML comparison overstates what the cited material demonstrates. Update the final sentence to link directly to Simon Willison’s specific JustHTML post and limit the claim to LLM-assisted implementation guided by the html5lib conformance suite, removing the unsupported assertion about limited training data or learning an unfamiliar specification.Source: Path instructions
SKILL.md (2)
415-415: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winCorrect the documented type of
array_length.This paragraph says
array_lengthis declared as@Int, but the built-in reference later inSKILL.mdsays it returnsNat. That changes whether the example represents anInt→Natnarrowing and could cause agents to apply the wrong obligation or conversion.As per path instructions, Markdown changes must be checked for factual accuracy against the codebase and the rest of the reference documentation.
🤖 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 `@SKILL.md` at line 415, Correct the `array_length` type claim in the Int/Nat interoperability paragraph to match the built-in reference and codebase declaration: it returns `@Nat`, not `@Int`. Update the surrounding explanation so it no longer describes `array_length` as an Int-to-Nat flow, while preserving the documented conversion and obligation rules.Source: Path instructions
415-415: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winDo not claim one-to-one guard coverage here.
KNOWN_ISSUES.mddocuments three statically obligated narrowing sites that still lack runtime guards: effect-operation arguments, generic-instantiated constructor fields, andnat_to_int/nat_to_string. This sentence says only nested closure returns remain exceptional, overstating the runtime safety guarantee. Align the two documents before release.As per path instructions, Markdown changes must be checked for factual accuracy against 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 `@SKILL.md` at line 415, Update the Int/Nat interoperability paragraph in SKILL.md to remove the claim that runtime guards and verifier obligations match one-to-one except for nested closures. Explicitly acknowledge the three documented narrowing sites without runtime guards—effect-operation arguments, generic-instantiated constructor fields, and nat_to_int/nat_to_string—and ensure the wording matches KNOWN_ISSUES.md and the codebase.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 `@ROADMAP.md`:
- Line 35: Align Stage 19 in ROADMAP.md with KNOWN_ISSUES.md by either adding
issue `#985` and its nested-closure return-coercion work to the stage’s scope and
exit criterion, or narrowing the “whole verification-completeness family”
wording and criterion to only the explicitly listed issues; keep the roadmap
consistent with the tracking document.
---
Outside diff comments:
In `@FAQ.md`:
- Line 181: The FAQ paragraph’s JustHTML comparison overstates what the cited
material demonstrates. Update the final sentence to link directly to Simon
Willison’s specific JustHTML post and limit the claim to LLM-assisted
implementation guided by the html5lib conformance suite, removing the
unsupported assertion about limited training data or learning an unfamiliar
specification.
In `@SKILL.md`:
- Line 415: Correct the `array_length` type claim in the Int/Nat
interoperability paragraph to match the built-in reference and codebase
declaration: it returns `@Nat`, not `@Int`. Update the surrounding explanation
so it no longer describes `array_length` as an Int-to-Nat flow, while preserving
the documented conversion and obligation rules.
- Line 415: Update the Int/Nat interoperability paragraph in SKILL.md to remove
the claim that runtime guards and verifier obligations match one-to-one except
for nested closures. Explicitly acknowledge the three documented narrowing sites
without runtime guards—effect-operation arguments, generic-instantiated
constructor fields, and nat_to_int/nat_to_string—and ensure the wording matches
KNOWN_ISSUES.md and the codebase.
🪄 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: 480debda-bf04-4efb-99fa-1ff45c16e2fe
⛔ Files ignored due to path filters (2)
docs/SKILL.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (6)
FAQ.mdHISTORY.mdKNOWN_ISSUES.mdROADMAP.mdSKILL.mdTESTING.md
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
|
Both noted as deferred for that follow-up sprint. ✅ Action performedComments resolved. Approval is disabled; enable |
…here Swept the reference docs (all except CHANGELOG/HISTORY) for backward-looking narration and process/provenance commentary, reframing to present state: - ROADMAP: 'how this file works' + Stage 20 intro no longer narrate past sweeps/audits/contributions; present-tense description of what each stage does. - KNOWN_ISSUES: dropped 'found by the PR #NNN review' / 'surfaced during the #NNN audit' / 'pre-existing' provenance from bug rows. - spec/06: 'no longer verifies cleanly' -> 'does not'; 'the audit principle' -> 'the guiding principle'. - TESTING: removed development-process narration from the per-file coverage rows — 'Test-first: fails on the pre-fix verifier', 'PR #NNN review adds', 'round N', 'per CR <id>', 'flipped from', 'switched to in v0.0.NNN', 'Pre-#549 would have been impossible' — keeping the coverage descriptions. Provenance and how-we-got-here belong in CHANGELOG; every other doc states present reality and future work. Skip-changelog: docs-only prose edits on the release PR Co-Authored-By: Claude <noreply@anthropic.invalid>
…ard/obligation residuals (PR #1016 review) - ROADMAP Stage 19: add #985 (nested-closure return-coercion reporting gap) to the table so the stage scope matches KNOWN_ISSUES' verification- completeness family and its exit criterion. - FAQ: temper the JustHTML sentence to the defensible claim (an LLM-assisted implementation guided by the html5lib conformance suite), dropping the unsupported 'little training data' / 'learn new languages' assertions. - SKILL Int/Nat paragraph: the guard/obligation correspondence has residuals in BOTH directions — acknowledge the three obligated-but-unguarded narrowing sites (#754/#757 effect-op arg + generic ctor field, nat_to_int/nat_to_string) alongside the guarded-but-unreported #985, matching KNOWN_ISSUES. array_length returns @int (spec §2.2.1, monomorphize return-type table, and a live nat_bind narrowing obligation all agree) — the 'returns @nat' finding is declined. Skip-changelog: docs-only accuracy edits on the release PR Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai On the three outside-diff findings: FAQ.md:181 (JustHTML) — fixed in 5c9b2e5. Tempered the sentence to the defensible claim — an LLM-assisted implementation guided by the html5lib conformance suite conforming to the spec via its tests — and dropped the unsupported 'a spec it had little training data for' and 'models can learn new languages remarkably well' assertions. I did not add a direct URL: I can't verify the exact post link from here, and inventing one would be worse than omitting it. SKILL.md:415 ( SKILL.md:415 (guard/obligation one-to-one) — fixed in 5c9b2e5. The claim now acknowledges residuals in both directions: the guarded-but-unreported #985, and the three obligated-but-unguarded narrowing sites (the effect-operation argument and generic-instantiated constructor field, #754/#757, plus |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
rg -n "array_length" vera/monomorphize.py spec/02-types.md SKILL.md | head -50Length of output: 6114
|
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 (2)
ROADMAP.md (1)
23-31: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winAlign the Stage 19 scope summary with its PR clusters.
Line 23 describes all eleven bugs as monomorphiser/import or verifier-walker gaps, but the listed clusters also include effect-operation lowering (
#1005/#1006) and CLI diagnostic surfacing (#1004). Update the summary to cover those areas.As per path instructions, Markdown changes must remain factually accurate against 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 `@ROADMAP.md` around lines 23 - 31, Update the Stage 19 scope summary opening sentence in ROADMAP.md to explicitly include effect-operation lowering and CLI diagnostic surfacing alongside monomorphizer/import and verifier-walker gaps. Keep it factually consistent with the PR B and PR C clusters and leave the detailed issue grouping unchanged.Source: Path instructions
TESTING.md (1)
70-70: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winDo not overstate runtime guard coverage.
These descriptions imply that effect-operation arguments and constructor-field narrowings are codegen-guarded, but
KNOWN_ISSUES.mdandspec/06-contracts.mdstate that effect-operation arguments and generic-instantiated constructor fields remain unguarded. Qualify the descriptions to distinguish concrete guarded sites from the residualE504/E531cases.As per path instructions, Markdown changes must remain factually accurate against the codebase.
Also applies to: 120-120
🤖 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 70, Update the test_verifier_nat_obligations.py descriptions at both listed entries to avoid implying universal codegen guard coverage for effect-operation arguments and constructor-field narrowings. Distinguish concrete guarded sites from unguarded residual E504/E531 cases, including generic-instantiated constructor fields, while preserving the existing obligation and test references.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 `@KNOWN_ISSUES.md`:
- Around line 32-33: Clarify the runtime guard coverage in the first table entry
by changing “sub-pattern” to explicitly mean direct/non-nested constructor
sub-patterns. Keep the following entry’s statement that nested constructor
sub-patterns remain unguarded, ensuring the documented guarantees are
consistent.
---
Outside diff comments:
In `@ROADMAP.md`:
- Around line 23-31: Update the Stage 19 scope summary opening sentence in
ROADMAP.md to explicitly include effect-operation lowering and CLI diagnostic
surfacing alongside monomorphizer/import and verifier-walker gaps. Keep it
factually consistent with the PR B and PR C clusters and leave the detailed
issue grouping unchanged.
In `@TESTING.md`:
- Line 70: Update the test_verifier_nat_obligations.py descriptions at both
listed entries to avoid implying universal codegen guard coverage for
effect-operation arguments and constructor-field narrowings. Distinguish
concrete guarded sites from unguarded residual E504/E531 cases, including
generic-instantiated constructor fields, while preserving the existing
obligation and test references.
🪄 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: 3b18ddbe-f902-4456-b418-a9ccf007824e
📒 Files selected for processing (4)
KNOWN_ISSUES.mdROADMAP.mdTESTING.mdspec/06-contracts.md
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…s only (PR #1016 review) Line 32's 'every concrete binding site' could read as covering nested constructor sub-patterns, which the #765 row says are unguarded. Qualified to 'every concrete direct binding site' with the nested exception noted. Skip-changelog: docs-only accuracy clarification on the release PR Co-Authored-By: Claude <noreply@anthropic.invalid>
…erage (PR #1016 review) - ROADMAP Stage 19 bug-sprint intro: the eleven bugs span four areas (mono/import, verifier walkers, effect-op codegen, CLI diagnostics), not the two the summary named. - TESTING test_verifier_nat_obligations row: distinguish the concrete codegen-guarded sites from the effect-op-argument and generic-instantiated constructor-field E504 residuals (obligated but unguarded, #754/#757), matching KNOWN_ISSUES and spec/06. Skip-changelog: docs-only accuracy edits on the release PR Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai Both outside-diff findings from the c0810b4 review are fixed in 87cb607:
|
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
git log --oneline -5
echo "---ROADMAP---"
rg -n -A3 -B3 "Stage 19" ROADMAP.md | head -80
echo "---TESTING---"
rg -n -A3 -B3 "test_verifier_nat_obligations" TESTING.md | head -60Length of output: 4443 🏁 Script executed: #!/bin/bash
sed -n '17,45p' ROADMAP.mdLength of output: 4691 Both fixes check out.
Both addressed. |
This was referenced Jul 13, 2026
This was referenced Aug 7, 2026
Merged
This was referenced Aug 14, 2026
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.
v0.1.4 — the second burndown
Integration branch
release/v0.1.4→main. Nineteenbug-labelled issues fixed one-PR-per-bug over 17 serially-merged PRs (#974–#1013), plus the §7.5 spec contradiction #976 resolved. Release machinery and the docs sweep ride this final commit.What landed (19 fixes)
forall— a bareNone/ nullary constructor now adopts its expected type at return/let/match (#971), nested constructor fields (#979), comparison operands (#981), and call/op/init arguments (#993); and the static E503@Nat-narrowing obligation fires for concrete components of a partially-generic constructor argument (#1010).handle[State<T>]clause bodies andwith-expressions now execute under intrinsic-hybrid semantics (#976, closing the §7.5 spec contradiction #988); handler state-slot reads in the handled body are rejected (#973).@Nat/@Intobligations —@Int → @Natnarrowing is obligated and guarded at the function-return position (#758) and closure returns (#984); the@Nat → @Intwidening guards fire per-component including imported bodies (#820, #987, #998).forallvars (#970).vera verify --json's summary is derived from the reified obligation stream (#967).What's deferred
Each fix's own review surfaced further edge cases in the same two subsystems. Ten remain, filed and grouped into a bug sprint at the front of ROADMAP Stage 19 (three PRs by shared fix machinery): the mono/import-door cluster (#999, #1000, #1002, #1008, #1012, #1014, #1015), effect-op positional lowering (#1005, #1006), and CLI diagnostic surfacing (#1004). The unreproducible conformance flake #996 stays a watch-only row. KNOWN_ISSUES keeps its 11 open Bugs rows; "No known bugs." is not restored.
Release machinery
Version
0.1.3 → 0.1.4across the six-file surface; CHANGELOG[Unreleased] → [0.1.4]with compare links; HISTORY Stage 19+20 row; ROADMAP bug-sprint section + counts; site assets regenerated. Full gate green: 7,391 tests, 157 conformance, 37 examples, mypy/ruff, doc-counts/version-sync/limitations-sync/site-assets.Merge reserved for the maintainer — a merge commit to keep the per-fix squashed commits bisectable on
main, then tagv0.1.4on the merge commit.Closes #758
Closes #820
Closes #967
Closes #969
Closes #970
Closes #971
Closes #973
Closes #976
Closes #978
Closes #979
Closes #981
Closes #984
Closes #987
Closes #988
Closes #990
Closes #991
Closes #992
Closes #993
Closes #998
Closes #1010
🤖 Generated with Claude Code
Summary by CodeRabbit
verify --jsonnow includes anobligationsarray with per-obligation locations, statuses, and error codes.Nat/Intruntime guarding and verifier/diagnostic consistency across arrays, tuples, closures, effect handlers, and imported code.where-helper scoping/name collisions and monomorphization/emission edge cases (including imported generics).release/**branches with improved concurrency handling.