repsel: one safety gate and one write walker for both numeric proofs, plus the #7770 super-chain test and bench numbers - #7788
Open
proggeramlug wants to merge 3 commits into
Open
Conversation
added 3 commits
August 10, 2026 19:49
… 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.
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (6)
📝 WalkthroughWalkthroughThe PR centralizes ChangesElement-group numeric proof
Estimated code review effort: 4 (Complex) | ~45 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 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 |
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
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.
Follow-up to #7774 (merged as 2e5bf44). These two commits were pushed to the PR branch but were not in the rebase that got merged, so they are absent from
main; the branch was deleted on merge, so this restores them. No behavior change — a consolidation, a coverage gap, and two efficiency items, all from the code review of #7774.1. One safety gate, not two (the load-bearing one)
prove_group_numeric_fieldshad grown its own copy of the'candloop's entire Pass-3 obligation set:ThisFlowAnalysisconstruction,ctor_chain_safe,prototype_is_stable, field/method name-ambiguity, per-methodmethod_safe. That verdict is what licenses a bare uncheckedload double, so the two copies silently drifting is a miscompile, not a missed optimization — and nothing diffed them against each other.Extracted as
chain_this_flow_verdict, now the single implementation both callers use. Tightening an obligation is a one-place change again.2. The super-chain resolution path had no test at group scope
prove_numeric_fieldsresolves a parent constructor's parameters throughsuper(...)argument lists under the caller's already-resolved environment. #7774 made that path reachable through the group MEET (multiple provenancenews) for the first time, and every fixture in the new test file hadextends: None— so a wrong index or an unresolved caller env there would have granted an unsound claim with zero red tests.super_chain_params_resolve_under_the_group_meetcovers both directions: all-numeric push sites prove the derived and the inherited field; one string at the super-feeding position drops exactlyzgroup-wide whilexsurvives.3. One write walker, not three
collect_numeric_by_construction_localshad a hand-rolled fullStmt-tree write collector nearly identical tonot_bigint_locals::collect_writes— the "two traversals that must agree, drifting by oneStmtvariant" bug class thatptr_shape_elements.rs's own doc warns this file cannot afford. Generalizedcollect_writesto record a no-initLetasNone(fine for the non-BigInt fixpoint, fatal for the numeric one) and deleted the duplicate.4. Two efficiency items
group_members()rebuilt its map twice per collector run — once for the numeric proof, once for the pre-existing group-integrity pass. Computed once, passed to both.5. The perf numbers for #7770
The merged fragment stops before the bench results. Restores them: on the pinned quiet mini (interleaved arms, best-of-15, two independent runs, outputs byte-verified against Node before timing) the issue's read loop goes 101/102 ms → 91/90 ms, while
batch.ts,suite/04_array_readandsuite/09_method_callsare unchanged. Includes the trap worth recording — benchmarking this needs the array and its read loop in ONE function, because an array crossing a function boundary is the #7766 shape #7770 does not address (both arms keep all 4js_number_coercesites, and the "no regression" is vacuous).Validation
Rebased onto current
main(after #7771 and #7765, which touch neighbouring element-shape code):cargo test -p perry-codegen --lib850/850 green,cargo fmt --checkand the 2000-line file-size gate clean.Summary by CodeRabbit
Performance
Bug Fixes
Tests & Documentation