From f79a5bfe2d4e1bfb9fba587ad6b7ec0d5b4c7684 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Mon, 10 Aug 2026 17:01:33 +0200 Subject: [PATCH 1/3] refactor(repsel): one safety gate + one write walker for both numeric proofs; super-chain group tests MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .../src/collectors/not_bigint_locals.rs | 28 ++- .../perry-codegen/src/collectors/ptr_shape.rs | 115 +++++++---- .../ptr_shape_group_numeric_tests.rs | 114 +++++++++++ .../src/collectors/ptr_shape_numeric.rs | 184 ++++-------------- 4 files changed, 243 insertions(+), 198 deletions(-) diff --git a/crates/perry-codegen/src/collectors/not_bigint_locals.rs b/crates/perry-codegen/src/collectors/not_bigint_locals.rs index e6e056a29b..1997cdda04 100644 --- a/crates/perry-codegen/src/collectors/not_bigint_locals.rs +++ b/crates/perry-codegen/src/collectors/not_bigint_locals.rs @@ -51,7 +51,7 @@ pub fn collect_not_bigint_locals( // into closure bodies so a `LocalSet` to an ENCLOSING local inside a // closure is captured (LocalIds are unique per function, so the write is // recorded against the enclosing id). - let mut writes: HashMap> = HashMap::new(); + let mut writes: HashMap>> = HashMap::new(); let mut candidates: HashSet = HashSet::new(); collect_writes(stmts, &mut writes, &mut candidates); @@ -70,8 +70,11 @@ pub fn collect_not_bigint_locals( // A declared-but-never-assigned `let x;` is `undefined` — a // non-BigInt — so no writes means the local stays. .map(|ws| { - ws.iter() - .all(|rhs| expr_not_bigint(rhs, &types, ¬_bigint, &numeric_locals)) + ws.iter().all(|rhs| match rhs { + // A `let x;` binding is `undefined` — a non-BigInt. + None => true, + Some(rhs) => expr_not_bigint(rhs, &types, ¬_bigint, &numeric_locals), + }) }) .unwrap_or(true); if !all_ok { @@ -217,18 +220,25 @@ fn index_receiver_is_numeric(object: &Expr, types: &HashMap) -> bo } /// Record every write (Let init + `LocalSet` rhs) per local, gather the set of -/// analyzed candidate ids, and descend into closure bodies. -fn collect_writes<'a>( +/// `Let`-bound candidate ids, and descend into closure bodies. A `Let` with no +/// initializer records `None` (the binding is `undefined` until assigned). +/// +/// Shared with `ptr_shape/ptr_shape_numeric.rs`'s numeric-by-construction +/// fixpoint (#7770) — the two analyses differ only in how they judge a write +/// (`undefined` is a fine non-BigInt and a fatal non-number), so ONE walker +/// keeps them from drifting by a `Stmt` variant, the bug class +/// `ptr_shape_elements.rs`'s doc warns about. +pub(super) fn collect_writes<'a>( stmts: &'a [Stmt], - writes: &mut HashMap>, + writes: &mut HashMap>>, candidates: &mut HashSet, ) { for s in stmts { match s { Stmt::Let { id, init, .. } => { candidates.insert(*id); + writes.entry(*id).or_default().push(init.as_ref()); if let Some(e) = init { - writes.entry(*id).or_default().push(e); collect_writes_expr(e, writes, candidates); } } @@ -314,11 +324,11 @@ fn collect_writes<'a>( fn collect_writes_expr<'a>( e: &'a Expr, - writes: &mut HashMap>, + writes: &mut HashMap>>, candidates: &mut HashSet, ) { if let Expr::LocalSet(id, rhs) = e { - writes.entry(*id).or_default().push(rhs.as_ref()); + writes.entry(*id).or_default().push(Some(rhs.as_ref())); } // Closure bodies are statements, not expression children, so descend // explicitly. A write to an enclosing local inside the closure body targets diff --git a/crates/perry-codegen/src/collectors/ptr_shape.rs b/crates/perry-codegen/src/collectors/ptr_shape.rs index 4cb01b5a60..68a24165c1 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape.rs @@ -451,10 +451,12 @@ pub(crate) fn collect_shape_proven_ptr_locals( // claim is honest even though member verdicts are not in yet: group // integrity below drops EVERY member's fact when any member fails, and a // dropped fact takes its claim with it. + let groups = element_facts.group_members(); let group_numeric = prove_group_numeric_fields( classes, module_dispatch, element_facts, + &groups, &roots, &field_stores, &method_calls, @@ -499,46 +501,28 @@ pub(crate) fn collect_shape_proven_ptr_locals( let chain = chain_classes(classes, class_name); let fields = chain_field_names(&chain); let methods = chain_method_map(&chain); + let called = method_calls.get(id); // Constructor chain + field initializers must not leak `this`. All // methods called on the local must be `this`-flow safe and the module - // must prove the method table stable. - let mut analysis = ThisFlowAnalysis { - chain: &chain, - fields: &fields, - methods: &methods, - visited: HashSet::new(), - store_records: Vec::new(), - super_call_args: HashMap::new(), - internally_invoked: HashSet::new(), - allow_this_in_store_values: false, - }; - if !analysis.ctor_chain_safe() { - deny(id, class_name, report::THIS_ESCAPE); - continue; - } - let called = method_calls.get(id); - if let Some(called) = called { - if !module_dispatch.prototype_is_stable(classes, class_name) { - deny(id, class_name, report::UNSTABLE_PROTOTYPE); - continue; - } - for m in called.keys() { - if fields.contains(m.as_str()) { - // A name that is both a field and a method is ambiguous - // under own-property shadowing — bail. - deny(id, class_name, report::FIELD_METHOD_AMBIGUITY); - continue 'cand; - } - let Some((owner, func)) = methods.get(m.as_str()) else { - deny(id, class_name, report::ESC_UNRESOLVED_METHOD); - continue 'cand; - }; - if !analysis.method_safe(owner, func) { - deny(id, class_name, report::METHOD_THIS_ESCAPE); - continue 'cand; - } + // must prove the method table stable. ONE implementation, shared with + // the group-scope numeric proof (#7770) — this gate licenses a bare + // unchecked `load double`, so two drifting copies would be a + // miscompile waiting to happen, not a missed optimization. + let mut analysis = match chain_this_flow_verdict( + classes, + module_dispatch, + class_name, + &chain, + &fields, + &methods, + called, + ) { + Ok(analysis) => analysis, + Err(why) => { + deny(id, class_name, why); + continue 'cand; } - } + }; let store_records = std::mem::take(&mut analysis.store_records); let super_call_args = std::mem::take(&mut analysis.super_call_args); let internally_invoked = std::mem::take(&mut analysis.internally_invoked); @@ -612,7 +596,7 @@ pub(crate) fn collect_shape_proven_ptr_locals( // group is therefore all-or-nothing. Dropping is the conservative // direction and needs no fixpoint: removing members never admits one. if !element_facts.is_empty() { - for (_, members) in element_facts.group_members() { + for members in groups.values() { if members.iter().any(|m| !out.contains_key(m)) { // The insert loop above gives every ALIAS of a promoted root // the same fact, because an alias holds the same object. The @@ -1338,6 +1322,61 @@ struct ThisStoreRecord<'a> { context: Option<(String, String, Vec)>, } +/// Pass-3 safety verdict for one class chain plus the methods invoked on the +/// value: `this`-flow containment of the constructor chain, prototype +/// stability when any method is called, field/method name-ambiguity, and +/// per-method `this`-flow safety. Returns the analysis (holding the store +/// records, `super(...)` argument lists, and internally-invoked set the +/// numeric proof consumes) or the FIRST failed obligation. +/// +/// This is the single implementation behind both the per-candidate `'cand` +/// loop and the group-scope numeric proof (#7770, +/// `ptr_shape_numeric.rs::prove_group_numeric_fields`). The verdict licenses +/// a bare unchecked `load double`; keeping the two callers on one function +/// is what makes "tighten an obligation" a one-place change. +fn chain_this_flow_verdict<'a, 'b>( + classes: &HashMap, + module_dispatch: &ModuleDispatchFacts, + class_name: &str, + chain: &'b [&'a Class], + fields: &'b HashSet, + methods: &'b HashMap, + called: Option<&HashMap>>, +) -> Result, ShapeDenial> { + let mut analysis = ThisFlowAnalysis { + chain, + fields, + methods, + visited: HashSet::new(), + store_records: Vec::new(), + super_call_args: HashMap::new(), + internally_invoked: HashSet::new(), + allow_this_in_store_values: false, + }; + if !analysis.ctor_chain_safe() { + return Err(report::THIS_ESCAPE); + } + if let Some(called) = called { + if !called.is_empty() && !module_dispatch.prototype_is_stable(classes, class_name) { + return Err(report::UNSTABLE_PROTOTYPE); + } + for m in called.keys() { + if fields.contains(m.as_str()) { + // A name that is both a field and a method is ambiguous + // under own-property shadowing — bail. + return Err(report::FIELD_METHOD_AMBIGUITY); + } + let Some((owner, func)) = methods.get(m.as_str()) else { + return Err(report::ESC_UNRESOLVED_METHOD); + }; + if !analysis.method_safe(owner, func) { + return Err(report::METHOD_THIS_ESCAPE); + } + } + } + Ok(analysis) +} + pub(super) struct ThisFlowAnalysis<'a, 'b> { chain: &'b [&'a Class], fields: &'b HashSet, diff --git a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs index 7bb11dd242..f54d154d20 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs @@ -18,6 +18,9 @@ use perry_hir::{BinaryOp, ClassField, CompareOp, Function, Module, Param, Update /// the tests use, mirroring the module-wide id allocator. const CTOR_PX: u32 = 100; const CTOR_PY: u32 = 101; +/// `Base`'s ctor param and `D`'s super-feeding param (the subclass tests). +const CTOR_PZ: u32 = 102; +const CTOR_PZ2: u32 = 103; /// Method parameter id for `setX(v)`. const METH_PV: u32 = 110; @@ -501,6 +504,117 @@ fn method_site_string_arg_drops_the_field() { ); } +/// `class Base { z; constructor(z) { this.z = z } }`. +fn class_base() -> Class { + let mut b = class_p(); + b.name = "Base".to_string(); + b.fields = vec![field("z")]; + b.constructor = Some(Function { + id: 902, + name: "constructor".to_string(), + type_params: Vec::new(), + params: vec![num_param(CTOR_PZ, "z")], + return_type: Type::Void, + body: vec![this_store("z", Expr::LocalGet(CTOR_PZ))], + is_async: false, + is_generator: false, + is_strict: true, + is_exported: false, + captures: Vec::new(), + decorators: Vec::new(), + was_plain_async: false, + was_unrolled: false, + }); + b +} + +/// `class D extends Base { x; constructor(x, z) { super(z); this.x = x } }`. +fn class_d_extends_base() -> Class { + let mut d = class_p(); + d.id = 1; + d.name = "D".to_string(); + d.extends_name = Some("Base".to_string()); + d.fields = vec![field("x")]; + d.constructor = Some(Function { + id: 903, + name: "constructor".to_string(), + type_params: Vec::new(), + params: vec![num_param(CTOR_PX, "x"), num_param(CTOR_PZ2, "z")], + return_type: Type::Void, + body: vec![ + Stmt::Expr(Expr::SuperCall(vec![Expr::LocalGet(CTOR_PZ2)])), + this_store("x", Expr::LocalGet(CTOR_PX)), + ], + is_async: false, + is_generator: false, + is_strict: true, + is_exported: false, + captures: Vec::new(), + decorators: Vec::new(), + was_plain_async: false, + was_unrolled: false, + }); + d +} + +/// The super()-argument resolution path under the group MEET — the one place +/// a parent-constructor parameter environment is derived from MULTIPLE +/// provenance `new`s. A wrong index or an unresolved caller env here would +/// grant an unsound claim on `z` (a bare raw load), so both directions get a +/// red test: all-numeric sites prove BOTH the derived and the inherited +/// field; one string at the super-feeding position drops exactly `z`, +/// group-wide, while `x` survives. +#[test] +fn super_chain_params_resolve_under_the_group_meet() { + let cs = [class_base(), class_d_extends_base()]; + let classes = classes_of(&cs); + let read_loop = |idx: u32, r: u32| { + counted_loop( + idx, + arr_len(1), + vec![let_elem(r, 1, idx, "D"), read_field(r, "z")], + ) + }; + let stmts_ok = vec![ + let_arr(1, "D"), + counted_loop( + 2, + Expr::Number(4.0), + vec![push( + 1, + new_of("D", vec![Expr::LocalGet(2), counter_plus_one(2)]), + )], + ), + read_loop(5, 6), + ]; + let promoted_ok = promote(&stmts_ok, &classes); + assert_eq!( + promoted_ok.get(&6).expect("reader promotes").numeric_fields, + names(&["x", "z"]), + "super(z) must resolve Base's parameter through the caller env" + ); + + let stmts_poison = vec![ + let_arr(1, "D"), + push(1, new_of("D", vec![Expr::Number(1.0), Expr::Number(2.0)])), + push( + 1, + new_of("D", vec![Expr::Number(3.0), Expr::String("s".to_string())]), + ), + read_loop(5, 6), + ]; + let promoted_poison = promote(&stmts_poison, &classes); + assert_eq!( + promoted_poison + .get(&6) + .expect("reader promotes") + .numeric_fields, + names(&["x"]), + "one string at the super-feeding position must drop `z` for the whole \ + group and leave `x` standing" + ); +} + /// The group claim dies with the group: an undeclared-property store on one /// member removes every member's FACT, claim included. #[test] diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs index 69b33bba18..75b9cf5acb 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs @@ -286,6 +286,7 @@ pub(super) fn prove_group_numeric_fields<'a>( classes: &HashMap, module_dispatch: &ModuleDispatchFacts, element_facts: &ElementShapeFacts, + groups: &HashMap>, roots: &HashMap, field_stores: &HashMap)>>, method_calls: &HashMap>>, @@ -296,7 +297,7 @@ pub(super) fn prove_group_numeric_fields<'a>( numeric_locals: &HashSet, ) -> HashMap> { let mut out: HashMap> = HashMap::new(); - 'group: for (root, members) in element_facts.group_members() { + 'group: for (&root, members) in groups { let Some(class_name) = element_facts.root_class(root) else { continue; }; @@ -304,12 +305,22 @@ pub(super) fn prove_group_numeric_fields<'a>( if chain.is_empty() { continue; } + // Nothing raw-f64-declared anywhere on the chain means there is no + // claim to make — skip the whole this-flow walk for such groups + // (proven arrays of string/object-only records are common). + if !chain.iter().any(|c| { + c.fields + .iter() + .any(|f| crate::typed_shape::type_is_raw_f64_candidate(&f.ty)) + }) { + continue; + } let fields = chain_field_names(&chain); let methods = chain_method_map(&chain); // Merge method call sites group-wide: a method's parameter is numeric // only when every site on every member passes a numeric argument. let mut merged_calls: HashMap> = HashMap::new(); - for m in &members { + for m in members { if let Some(mc) = method_calls.get(m) { for (name, sites) in mc { merged_calls @@ -320,35 +331,19 @@ pub(super) fn prove_group_numeric_fields<'a>( } } // The same obligations the `'cand` loop imposes before it trusts a - // method walk, re-checked here so a claim can never rest on a weaker - // basis than the per-candidate proof it extends. - if !merged_calls.is_empty() && !module_dispatch.prototype_is_stable(classes, class_name) { - continue; - } - let mut analysis = ThisFlowAnalysis { - chain: &chain, - fields: &fields, - methods: &methods, - visited: HashSet::new(), - store_records: Vec::new(), - super_call_args: HashMap::new(), - internally_invoked: HashSet::new(), - allow_this_in_store_values: false, + // method walk — literally the same function, so the group claim can + // never rest on a weaker basis than the per-candidate proof. + let Ok(mut analysis) = super::chain_this_flow_verdict( + classes, + module_dispatch, + class_name, + &chain, + &fields, + &methods, + Some(&merged_calls), + ) else { + continue 'group; }; - if !analysis.ctor_chain_safe() { - continue; - } - for name in merged_calls.keys() { - if fields.contains(name.as_str()) { - continue 'group; - } - let Some((owner, func)) = methods.get(name.as_str()) else { - continue 'group; - }; - if !analysis.method_safe(owner, func) { - continue 'group; - } - } // One argument list per push — ALL of them, or no claim. A producer // whose `new_args` went unrecorded, or a push shape E2 would never // have admitted, forfeits the group's claim rather than narrowing @@ -380,7 +375,7 @@ pub(super) fn prove_group_numeric_fields<'a>( ) .collect(); let mut merged_stores: Vec<(String, StoreValue<'a>)> = Vec::new(); - for m in &members { + for m in members { if let Some(fs) = field_stores.get(m) { merged_stores.extend(fs.iter().cloned()); } @@ -435,12 +430,13 @@ pub(super) fn collect_numeric_by_construction_locals<'a>( not_bigint_locals: &HashSet, const_local_inits: &HashMap>, ) -> HashSet { - let mut scan = WriteScan { - writes: HashMap::new(), - let_bound: HashSet::new(), - }; - scan.walk_stmts(stmts); - let WriteScan { writes, let_bound } = scan; + // ONE write walker for both fixpoints (`collect_not_bigint_locals` and + // this one) — see its doc for why sharing is load-bearing. `None` = a + // no-init `Let`, which THIS consumer treats as fatal (`undefined` is not + // a number) where the non-BigInt one treats it as fine. + let mut writes: HashMap>> = HashMap::new(); + let mut let_bound: HashSet = HashSet::new(); + super::super::not_bigint_locals::collect_writes(stmts, &mut writes, &mut let_bound); let empty_members: HashSet = HashSet::new(); let empty_fields: HashSet = HashSet::new(); let mut numeric: HashSet = let_bound @@ -484,120 +480,6 @@ pub(super) fn collect_numeric_by_construction_locals<'a>( numeric } -/// Write collector for [`collect_numeric_by_construction_locals`]. Descends -/// into closure bodies — ids are unique per lowering context, so a closure's -/// write to an enclosing local records against the right id. -struct WriteScan<'a> { - /// id -> every write's RHS; `None` = a `Let` with no initializer. - writes: HashMap>>, - /// ids bound by at least one `Stmt::Let` in the region. - let_bound: HashSet, -} - -impl<'a> WriteScan<'a> { - fn walk_stmts(&mut self, stmts: &'a [Stmt]) { - for s in stmts { - self.walk_stmt(s); - } - } - - fn walk_stmt(&mut self, s: &'a Stmt) { - match s { - Stmt::Let { id, init, .. } => { - self.let_bound.insert(*id); - self.writes.entry(*id).or_default().push(init.as_ref()); - if let Some(e) = init { - self.walk_expr(e); - } - } - Stmt::Expr(e) | Stmt::Throw(e) => self.walk_expr(e), - Stmt::Return(opt) => { - if let Some(e) = opt { - self.walk_expr(e); - } - } - Stmt::If { - condition, - then_branch, - else_branch, - } => { - self.walk_expr(condition); - self.walk_stmts(then_branch); - if let Some(eb) = else_branch { - self.walk_stmts(eb); - } - } - Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => { - self.walk_expr(condition); - self.walk_stmts(body); - } - Stmt::For { - init, - condition, - update, - body, - } => { - if let Some(i) = init { - self.walk_stmt(i.as_ref()); - } - if let Some(c) = condition { - self.walk_expr(c); - } - if let Some(u) = update { - self.walk_expr(u); - } - self.walk_stmts(body); - } - Stmt::Try { - body, - catch, - finally, - } => { - self.walk_stmts(body); - if let Some(c) = catch { - self.walk_stmts(&c.body); - } - if let Some(f) = finally { - self.walk_stmts(f); - } - } - Stmt::Switch { - discriminant, - cases, - } => { - self.walk_expr(discriminant); - for case in cases { - if let Some(t) = &case.test { - self.walk_expr(t); - } - self.walk_stmts(&case.body); - } - } - Stmt::Labeled { body, .. } => self.walk_stmt(body.as_ref()), - Stmt::Break - | Stmt::Continue - | Stmt::LabeledBreak(_) - | Stmt::LabeledContinue(_) - | Stmt::PreallocateBoxes(_) - | Stmt::PreallocateTdzBoxes(_) => {} - } - } - - fn walk_expr(&mut self, e: &'a Expr) { - match e { - Expr::LocalSet(id, rhs) => { - self.writes.entry(*id).or_default().push(Some(rhs)); - self.walk_expr(rhs); - } - // Closure bodies are `Vec`, invisible to the child walker. - Expr::Closure { body, .. } => self.walk_stmts(body), - _ => { - perry_hir::walker::walk_expr_children(e, &mut |c| self.walk_expr(c)); - } - } - } -} - // ── The expression-level proof ───────────────────────────────────────────── /// Number-by-construction: the expression's runtime value is a JS Number for From 02e507408d37188bf0b984883a035cb17e28d179 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Mon, 10 Aug 2026 17:28:50 +0200 Subject: [PATCH 2/3] docs: record the #7770 bench-mini floor results in the changelog fragment --- changelog.d/7774-element-group-numeric-proof.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/changelog.d/7774-element-group-numeric-proof.md b/changelog.d/7774-element-group-numeric-proof.md index 747f9bd942..825d6eee0f 100644 --- a/changelog.d/7774-element-group-numeric-proof.md +++ b/changelog.d/7774-element-group-numeric-proof.md @@ -1,4 +1,4 @@ -**repsel: element-group members now claim numeric fields — proven reads drop `js_number_coerce` (#7770, PR #7774).** +**repsel: element-group members now claim numeric fields (~10-12% on the target read loop) — proven reads drop `js_number_coerce` (#7770, PR #7774).** A `Ptr`-proven `const r = a[i]` (or a producer pushed into an element-shape-proven array) stood down to zero numeric fields, so every @@ -26,7 +26,14 @@ byte-identical vs Node 26.5.1 across sibling/push-site/method poison channels, NaN / Infinity / −0 payloads, and `null`/`{}`/`1n`/`true` stores (`test-files/test_gap_repsel_element_group_numeric.ts`), and a `PERRY_GC_ZEAL=1 PERRY_GC_PROTECT_FROMSPACE=1` run relocated 4014 objects -under the bare loads with a clean verdict. Pass 4 moved wholesale into the +under the bare loads with a clean verdict. On the pinned quiet mini +(interleaved, best-of-15, two runs) the issue's read loop goes 101/102 ms -> +91/90 ms while `batch.ts`, `suite/04_array_read` and `suite/09_method_calls` +are unchanged; the A/B's subject is verified live (base arm emits 4 +`js_number_coerce` sites and 12 checked-load diamonds on the benchmarked +source, branch arm zero) -- note that benchmarking this needs the array and +its read loop in ONE function, since an array crossing a function boundary is +the #7766 shape this change does not address. Pass 4 moved wholesale into the `ptr_shape_numeric.rs` child module for the 2000-line gate. A neighbouring PRE-EXISTING divergence found during validation (`o.x + 1` coercing where Node concatenates, plus an evaporating any-laundered add) is filed as #7773. From 5852fa2bb94d4a8d59a0f484fff35bd69d1f7cdd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Mon, 10 Aug 2026 19:52:49 +0200 Subject: [PATCH 3/3] docs: changelog fragment for PR #7788 --- changelog.d/7788-shared-this-flow-gate.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 changelog.d/7788-shared-this-flow-gate.md diff --git a/changelog.d/7788-shared-this-flow-gate.md b/changelog.d/7788-shared-this-flow-gate.md new file mode 100644 index 0000000000..18b91b3a8b --- /dev/null +++ b/changelog.d/7788-shared-this-flow-gate.md @@ -0,0 +1,19 @@ +**repsel: one Pass-3 safety gate and one write walker for both numeric proofs (#7788, follow-up to #7770/#7774).** + +No behavior change. `prove_group_numeric_fields` had grown an independent copy +of the `'cand` loop's obligation set (`ctor_chain_safe`, `prototype_is_stable`, +field/method ambiguity, per-method `method_safe`); that verdict licenses a bare +unchecked `load double`, so two copies drifting is a miscompile rather than a +missed optimization. Extracted as `chain_this_flow_verdict`, the single +implementation both callers share. Likewise +`collect_numeric_by_construction_locals`'s hand-rolled write collector is gone: +`not_bigint_locals::collect_writes` now records a no-init `Let` as `None` (fine +for the non-BigInt fixpoint, fatal for the numeric one) and serves both. + +Adds the coverage gap the review found: the `super(...)` parameter-resolution +path became reachable through the group MEET in #7770 and had no group-scope +test (every fixture was `extends: None`), so a wrong index there would have +granted an unsound claim silently. `super_chain_params_resolve_under_the_group_meet` +covers both directions. Also skips the group proof's this-flow walk when no +chain field is raw-f64-declared, and computes `group_members()` once per region +instead of twice.