repsel: discharge the numeric-field proof at element-GROUP scope so proven reads drop js_number_coerce (#7770) - #7774
Conversation
📝 WalkthroughWalkthroughThe collector now computes group-wide numeric proofs for shape-proven arrays and numeric-by-construction locals. It tracks constructor, method, store, and push provenance. Tests cover valid proofs, poisoning cases, coercion behavior, and Node-equivalent output. ChangesElement-group numeric analysis
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant UseWalk
participant ElementShapeFacts
participant ptr_shape
participant prove_group_numeric_fields
participant TestRuntime
UseWalk->>ElementShapeFacts: resolve array roots and group members
UseWalk->>ptr_shape: record constructor, method, store, and push provenance
ptr_shape->>prove_group_numeric_fields: provide grouped stores and call sites
prove_group_numeric_fields-->>ptr_shape: return numeric fields per group
ptr_shape->>TestRuntime: emit optimized element accesses
TestRuntime-->>ptr_shape: produce Node-equivalent results
Possibly related PRs
Suggested reviewers: 🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Audit — everything I could check independently holds; stays draft on your own perf-floor condition, correctlyI filed #7770, so this got the full treatment. The acceptance criteria, re-verified by handCriterion 1 (the headline): on the issue's reproducer, fresh release build, Criterion 5 (the soundness direction): Criterion 4 (GC): my run is stronger than the one reported — The 11 unit tests bite: neutering The three pre-existing-failure claims all check against my records
The design judgement worth endorsing explicitlyThe soundness note is exactly right about where this can be quietly wrong: a wrongly-claimed field's read is a bare Group integrity ("any member failing rule 2 drops every member's fact, claim included") is the collapse rule that keeps the group proof from outliving its premises. And the by-construction locals collector poisoning on a no-init Not merging yet, per the PR's own gateCriterion 6 (perf floors on the bench mini) and the full gap run are the two open items, and holding as draft until they land is the discipline that #7726 taught — targeted-green is not validated. Post the floors and I'll do the merge pass. |
… proofs; super-chain group tests Review findings on PR #7774: extract chain_this_flow_verdict so the 'cand loop and prove_group_numeric_fields share the single Pass-3 obligation set (the gate licenses a bare unchecked load double — two drifting copies would be a miscompile); generalize not_bigint_locals::collect_writes to record no-init Lets as None and reuse it for the numeric-by-construction fixpoint (third hand-rolled walker deleted); bail out of the group proof before the this-flow walk when no chain field is raw-f64-declared; build the group-members map once per region. New red tests for the super()-argument resolution path under the group meet, both directions.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@changelog.d/7774-element-group-numeric-proof.md`:
- Around line 23-25: Update the read-loop measurement in the changelog entry to
match the PR description, reporting js_number_coerce sites as 2 → 0; keep the
separate benchmarked-source count of 4 at Line 33 unchanged.
🪄 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: defaults
Review profile: CHILL
Plan: Pro Plus
Run ID: b1cce794-956a-4863-83e9-da08ff62378c
📒 Files selected for processing (8)
changelog.d/7774-element-group-numeric-proof.mdcrates/perry-codegen/src/collectors/not_bigint_locals.rscrates/perry-codegen/src/collectors/ptr_shape.rscrates/perry-codegen/src/collectors/ptr_shape_elements.rscrates/perry-codegen/src/collectors/ptr_shape_elements_tests.rscrates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rscrates/perry-codegen/src/collectors/ptr_shape_numeric.rstest-files/test_gap_repsel_element_group_numeric.ts
| On the issue's reproducer the read loop's `js_number_coerce` sites go 4 → 0 | ||
| while `--opt-report` still shows the `Ptr<Shape>` promotion; output verified | ||
| byte-identical vs Node 26.5.1 across sibling/push-site/method poison |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Align the js_number_coerce count with the reported measurement.
This line states the reproducer's read loop goes from 4 sites to 0. The PR description reports the reproducer dropping from 2 to 0, while 4 sites are attributed to the benchmarked source at Line 33. Use one number per source so the release note is unambiguous.
🤖 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 `@changelog.d/7774-element-group-numeric-proof.md` around lines 23 - 25, Update
the read-loop measurement in the changelog entry to match the PR description,
reporting js_number_coerce sites as 2 → 0; keep the separate benchmarked-source
count of 4 at Line 33 unchanged.
…#7770) An element-group member (const r = a[i] / a pushed producer) stood down to zero numeric fields because its own stores cannot witness a sibling's. The E1-E5 containment that licenses the SHAPE proof also closes the store universe, so the proof is now discharged once per array root: the meet over every push's new-argument list, the union of every member's field stores, and method parameters resolved through group-merged call sites (prove_group_numeric_fields). A claim only survives if the whole group survives integrity filtering. Constructor args like new P(i, i + 1) additionally need the loop counter: collect_numeric_by_construction_locals proves locals whose every write is number-producing (optimistic fixpoint, declared types untrusted, no-init Lets poison), consulted by the expression proof in function scope. Pass 4 moved wholesale into ptr_shape_numeric.rs for the 2000-line gate.
d1138fa to
b8f5184
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 (2)
crates/perry-codegen/src/collectors/ptr_shape_numeric.rs (1)
640-661: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick winRemove the
numberdeclared-type leaf fromnot_bigint_locals.
expr_not_bigint()currently accepts an unassignedLocalGetwhen its declared type isHirType::Number. That allows an unenforcednumberannotation to letBigInt - x/BigInt & xprove the whole expressionNumber, license a bareload double, and corrupt scalar state. Keep numeric typed-array/array-element reads, but dropHirType::Numberfrom the declared-type leaf, or remove declared-type leaves entirely from this collector to match the module’s “declared types stay untrusted” contract.🤖 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 `@crates/perry-codegen/src/collectors/ptr_shape_numeric.rs` around lines 640 - 661, Update expr_not_bigint so an unassigned LocalGet with declared HirType::Number is not treated as provably non-BigInt; remove that declared-type leaf while preserving numeric typed-array and array-element read handling. Ensure binary operators in the collector cannot use an unenforced number annotation to select the Number path or emit a bare load double.CLAUDE.md (1)
146-147: 📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick winAdd an explicit CI OFF-state arm for the GC schedule knobs.
.github/workflows/test.ymlrunsscripts/gc_instrument_smoke.sh, which exercises the seeded schedule, but it does not exercise both knobs OFF.scripts/gc_schedule_fuzz.shhas an optionalBASELINEcontrol, but it defaults to zero and is not wired into CI. Add an always-run CI step forPERRY_GC_SCHEDULE_SEEDunset andPERRY_GC_SCHEDULE_RATEunset, or delete the knob branch after one release of soak.🤖 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 `@CLAUDE.md` around lines 146 - 147, Add an always-run CI OFF-state arm in the workflow invoking scripts/gc_schedule_fuzz.sh with BASELINE enabled and both PERRY_GC_SCHEDULE_SEED and PERRY_GC_SCHEDULE_RATE unset, ensuring the existing seeded schedule smoke test remains unchanged.Source: Coding guidelines
🤖 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 `@CLAUDE.md`:
- Around line 146-147: Add an always-run CI OFF-state arm in the workflow
invoking scripts/gc_schedule_fuzz.sh with BASELINE enabled and both
PERRY_GC_SCHEDULE_SEED and PERRY_GC_SCHEDULE_RATE unset, ensuring the existing
seeded schedule smoke test remains unchanged.
In `@crates/perry-codegen/src/collectors/ptr_shape_numeric.rs`:
- Around line 640-661: Update expr_not_bigint so an unassigned LocalGet with
declared HirType::Number is not treated as provably non-BigInt; remove that
declared-type leaf while preserving numeric typed-array and array-element read
handling. Ensure binary operators in the collector cannot use an unenforced
number annotation to select the Number path or emit a bare load double.
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro Plus
Run ID: ceb6fcc5-4f1e-4178-8c80-0151894d4e56
⛔ Files ignored due to path filters (1)
Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (6)
CLAUDE.mdCargo.tomlchangelog.d/7774-element-group-numeric-proof.mdcrates/perry-codegen/src/collectors/ptr_shape.rscrates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rscrates/perry-codegen/src/collectors/ptr_shape_numeric.rs
🚧 Files skipped from review as they are similar to previous changes (3)
- changelog.d/7774-element-group-numeric-proof.md
- crates/perry-codegen/src/collectors/ptr_shape.rs
- crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs
The gc-repsel liveness gate proved the scavenge arm INERT on it (counter=0): its read loop is raw f64 loads with near-zero allocation, so a registered green cell would be green for the wrong reason. Moving-GC coverage lives in the reproducer run on the PR (1,762 evacuating minors, 400,014 objects moved). Claude-Session: https://claude.ai/code/session_01Y1QZ5wUP9gRSwpiweT4Wix
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@scripts/check_test_registration.py`:
- Around line 288-290: Update the relocation-count rationale in the relevant
registration-check text to match the authoritative changelog value of 4,014
objects, replacing the inconsistent 400,014 figure while preserving the
surrounding run details.
🪄 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: defaults
Review profile: CHILL
Plan: Pro Plus
Run ID: 6cd0466a-3d50-4288-96b8-74ebbec8ec53
📒 Files selected for processing (1)
scripts/check_test_registration.py
| "relocation coverage for this feature lives in the reproducer " | ||
| "run recorded on PR #7774 (1,762 evacuating minors, 400,014 " | ||
| "objects moved, exit 0) and in the ordinary parity harness." |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== file status =="
git diff --stat || true
echo "== locate relevant files =="
fd -a 'check_test_registration\.py|7774-element-group-numeric-proof\.md' . | sed 's#^\./##'
echo "== relevant snippet in script =="
sed -n '260,300p' scripts/check_test_registration.py | cat -n
echo "== changelog content =="
if [ -f changelog.d/7774-element-group-numeric-proof.md ]; then
sed -n '1,220p' changelog.d/7074-element-group-numeric-proof.md 2>/dev/null || true
sed -n '1,220p' changelog.d/7774-element-group-numeric-proof.md | cat -n
fi
echo "== search relocation counts mentions =="
rg -n "400,014|400014|4,014|4014|relocat|evacuat|moved|moved" changelog.d scripts/check_test_registration.py .github README* 2>/dev/null || trueRepository: PerryTS/perry
Length of output: 50370
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== file status =="
git diff --stat || true
echo "== locate relevant files =="
fd -a 'check_test_registration\.py|7774-element-group-numeric-proof\.md' . | sed 's#^\./##'
echo "== relevant snippet in script =="
sed -n '260,300p' scripts/check_test_registration.py | cat -n
echo "== changelog content =="
if [ -f changelog.d/7774-element-group-numeric-proof.md ]; then
sed -n '1,220p' changelog.d/7774-element-group-numeric-proof.md | cat -n
fi
echo "== search relocation count mentions =="
rg -n "400,014|400014|4,014|4014|relocation|relocat|evacuat|minors|objects moved|moved|PERRY_GC_ZEAL=1 PERRY_GC_PROTECT_FROMSPACE=1" changelog.d scripts/check_test_registration.py .github README* 2>/dev/null || trueRepository: PerryTS/perry
Length of output: 50370
Reconcile the relocation count with the changelog.
changelog.d/7774-element-group-numeric-proof.md records PERRY_GC_ZEAL=1 PERRY_GC_PROTECT_FROMSPACE=1 relocation as 4,014 objects, while scripts/check_test_registration.py records 400,014 objects. Align this rationale so it matches the authoritative run.
🤖 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 `@scripts/check_test_registration.py` around lines 288 - 290, Update the
relocation-count rationale in the relevant registration-check text to match the
authoritative changelog value of 4,014 objects, replacing the inconsistent
400,014 figure while preserving the surrounding run details.
|
Merging per the full audit above, now that the PR is undrafted. Delta since the audit:
Closes #7770. |
1 participant
Closes #7770.
What
A
Ptr<Shape>-proven element-group member (const r = a[i], or a producer pushed into a proven array) claimed zero numeric fields (#7034 §3's stand-down), so every declared-numberfield read on it lowered through the Phase-5a checked load — an inline finite check with a coldjs_number_coercearm. On the issue's reproducer that isjs_number_coerce x2per iteration-body, one per field.Two collector extensions make the numeric proof fire:
Group-wide numeric proof (
prove_group_numeric_fields, new inptr_shape_numeric.rs). The E1–E5 containment that licenses the SHAPE proof also closes the group's store universe: while facts hold, every reference to a group's objects is a vetted producer local, a licensed element read, or the inlinenew C(...)at a push site (a[i].x = vrides an unlicensedIndexGetand disqualifies the array). So the exhaustive-reachable-store proof is discharged once per array root: constructor parameters resolved as the meet over every push'snewargument list, every member's field stores unioned, method parameters resolved through group-merged call sites. Every member carries the group verdict; group integrity keeps it honest (any member failing rule 2 drops every member's fact, claim included).Numeric-by-construction locals (
collect_numeric_by_construction_locals). The reproducer's ctor args arenew P(i, i + 1)— a mutable loop counter, which the expression proof could not resolve. A local now proves numeric when its every write is number-producing by construction (let i = 0+i++; optimistic greatest fixpoint likecollect_not_bigint_locals, but with no declared-type leaf — annotations stay untrusted, a no-initLetpoisons).Pass 4 (ParamEnv +
prove_numeric_fields) moved wholesale fromptr_shape.rsinto the existingptr_shape_numeric.rschild module for the 2000-line gate;prove_numeric_fieldsnow takes&[&[Expr]]new-arg lists (the single-candidate call passes a 1-element slice, semantics unchanged).Acceptance criteria from the issue
Zero
js_number_coerceforr.x/r.y— verified on the reproducer via--trace llvm: 4 → 0 call sites; theptr_shape_get_number.*checked-load diamonds are gone, replaced by the Phase-3b bare load (class_field_get_number.shape_proven_load).js_array_get_f64remains (the separate element-fetch issue).Promotion intact —
--opt-reportstill showslocal r -> Ptr<Shape>;PERRY_REPSEL_DEBUGnow showsnumeric_fields {"x","y"}(and, as a side benefit of computing the group verdict before the report line, the opt-report numeric count is truthful for members).Store side agrees with load side — the store channels are each red-tested: sibling member store, mixed push-site meet, producer
newargs, method-mediated store (group-merged sites), plus group-death on an undeclared-property store. Unit tests inptr_shape_group_numeric_tests.rs(11 tests, sabotage-checked: disabling the group lookup fails them in both directions); behavioral coverage intest-files/test_gap_repsel_element_group_numeric.ts, byte-identical vs Node 26.5.1 including NaN / Infinity / −0 identity through claimed slots.GC still traces correctly — no mask or runtime change in this PR (
raw_f64_maskis class-level and untouched).PERRY_GC_ZEAL=1 PERRY_GC_PROTECT_FROMSPACE=1 PERRY_GC_PROTECT_FROMSPACE_DEPTH=800on the reproducer:forced_collections=25 copying_minors=25 moved_objects=4014 loop_polls=2000, exit 0, correct output; the full gap file survives 30 copying minors byte-identical.Non-number values at runtime stay Node-identical —
(w as any).x = null / {} / 1n / true / "s"all covered in the gap test (each drops the claim through its channel; verified per-case viaPERRY_REPSEL_DEBUG). One PRE-EXISTING divergence was found nearby and filed as declared-number class field holding a string:o.x + 1coerces to NaN (Node concatenates); any-laundered add evaporates #7773 (o.x + 1on a string-holding declared-number field coerces to NaN where Node concatenates; reproduces withPERRY_PTR_SHAPE_LOCALS=0and no arrays — not introduced or affected by this PR, A/B'd both arms).Perf floors hold, and the target workload gets faster. Pinned quiet M1 mini, interleaved arm pairs, best-of-15, every output byte-verified against Node before timing, two independent runs:
bench_7770_read(the issue's loop, scaled)batch.tssuite/04_array_readsuite/09_method_callsThe A/B's subject is verified live, per CLAUDE.md failure mode 4: on the benchmarked source the base arm emits 4
js_number_coercesites and 12ptr_shape_get_number.{plain,coerce,merge}diamonds, the branch arm 0 of each. Worth recording for the next person — my first attempt at this bench put the array behind a function boundary, which is the repsel: rule-1 provenance does not survive a function boundary — a typedP[]parameter still reads fields by name (first-party half of #7152/#7170) #7766 shape this PR does not address: it kept all 4 coercion sites on both arms, so its "no regression" would have been vacuous. The array and its read loop have to be in one function for the element facts to apply.Validation so far
cargo test -p perry-codegen(full, integration suites included) — green EXCEPTlarge_object_barriers::large_local_array_push_inbounds_store_emits_precise_slot_barrier, which is pre-existing: it fails identically on pristine main @423bb4405 (fresh worktree, exit 101) and withPERRY_PTR_SHAPE_LOCALS=0(every line of this PR is behind that gate). This suite is nightly/tag-only, so it can sit red on main without a red PR check.ptr_shapelib tests 96/96; the two pre-repsel: a Ptr<Shape>-proven numeric field still loads NaN-boxed — extend the raw-f64 field load past its scalar-replaced gate #7770 stand-down assertions inptr_shape_elements_tests.rsupdated to assert the group verdict.scripts/run_gap_tests.sh, 519 tests, prebuilt dev compiler) — the parallel sweep on a loaded dev Mac reported 18 status changes; every one is host noise or pre-existing, established by serial single-test re-runs plus aPERRY_PTR_SHAPE_LOCALS=0A/B (every line of this PR sits behind that gate):6356_dynamic_parent_mixin_chain,gc_alloc_point_no_move,language_types_object_part_a,learned_inline_sizing,logical_and_value_type,map_instance_reflection_4576,repsel_scalar_replaced_locals,http_client_no_redirect_follow);fetch_request_from_node_incoming_message,http_res_socket_writable_onfinished,http_overloads_3226plus,http_req_async_iterator,net_connect_bound_value) and 5 parity failures (events_import_4995,gc_rest_argument_rooting,gc_same_module_call_argument_rooting,specabi_reassign,zlib_3285_params), the known host-local zlib/socket/GC-rooting noise.test_gap_iterator_helpers_2874parity_fail → pass.cargo fmt --check,check_file_size.sh,addr_class_inventory.py,gc_runtime_root_holders.py— clean.repsel-census— the gate fails on this branch exactly as it fails on main (main runs 31295652054 / 31240304595 are red; the job is not a required context). Root cause is pre-existing:for (const r of rows)no longer licenses element-shape facts, filed as repsel-census red on main: for (const r of rows) no longer licenses element-shape facts (fixture_ptr_shape_elements 0/3) #7777 with a minimal repro and per-form A/B against a pristine-main build. On the indexed form this PR strictly improves the census picture (form-A slice: 4 promotions with all three fields claimed, vs claims-empty on main).Soundness note (the direction this can be quietly wrong in)
A wrongly-claimed field's read is a bare raw
load doublewith no value check. The claim's license is unchanged from Phase 3b — "every reachable store is a number" — this PR only widens WHERE the proof can be discharged (a closed group instead of one unaliased local) and WHAT the expression proof can resolve (by-construction numeric locals). Declared types are still trusted nowhere in the proof; the one deliberate carry-over is the pristine never-stored field (claimed today for plain candidates too), whoseundefinedbits raw-read as NaN — coinciding withToNumber(undefined)— and stay bit-faithful in value contexts.Summary by CodeRabbit
Performance
Bug Fixes
Tests
Documentation