From 5c74e1a286d1d2de95995aec41b15d2ff5ed6e14 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 08:45:45 +0100 Subject: [PATCH 1/4] wpfacts: interval rule results are not widened, and a counter write on a leaving path keeps the narrowed reads (R1 range tightening) --- changelog.d/wpfacts-range-tightening.md | 1 + crates/perry-wpfacts/src/gen.rs | 18 ++ crates/perry-wpfacts/src/gen/narrow.rs | 88 ++++++++++ crates/perry-wpfacts/src/gen/walk.rs | 16 ++ crates/perry-wpfacts/src/lib.rs | 12 ++ crates/perry-wpfacts/src/model.rs | 8 + crates/perry-wpfacts/src/solve.rs | 38 ++++ crates/perry-wpfacts/src/solve/apply.rs | 8 +- crates/perry-wpfacts/src/tests.rs | 1 + .../src/tests/range_tightening.rs | 160 +++++++++++++++++ .../perry/src/commands/compile/compile_env.rs | 2 + .../src/commands/compile/compile_env/tests.rs | 13 ++ .../src/commands/compile/program_facts.rs | 16 ++ scripts/test-verify-facts-s0.py | 2 + .../verify_facts_s0/leaving-write-negative.ts | 26 +++ scripts/verify_facts_s0/range-sum-negative.ts | 20 +++ .../language/array/test_range_tightening.ts | 165 ++++++++++++++++++ 17 files changed, 593 insertions(+), 1 deletion(-) create mode 100644 changelog.d/wpfacts-range-tightening.md create mode 100644 crates/perry-wpfacts/src/tests/range_tightening.rs create mode 100644 scripts/verify_facts_s0/leaving-write-negative.ts create mode 100644 scripts/verify_facts_s0/range-sum-negative.ts create mode 100644 tests/parity/language/array/test_range_tightening.ts diff --git a/changelog.d/wpfacts-range-tightening.md b/changelog.d/wpfacts-range-tightening.md new file mode 100644 index 00000000000..763146a4a13 --- /dev/null +++ b/changelog.d/wpfacts-range-tightening.md @@ -0,0 +1 @@ +Performance: two integer-interval looseness causes in the whole-program facts are gone. The result of an interval rule (`a + b`, `r * 16 + f`, a loop test's clip) is now the rule over its operands' intervals and is no longer widened on its own: only copy targets (a loop counter, a `let`) climb the widening ladder and the loop test clips them back, so `r * 16 + f` over two counters in `[0, 7]` is `[0, 119]` instead of `[0, 255]`, and `r + f` is `[0, 14]` instead of `[0, 127]`. A write of a narrowed counter in a branch that always leaves (`if ((sq & 0x88) !== 0) { sq += 7; continue; }`) no longer ends the counter's narrowed reads after the branch, when every way out of the branch lands outside the narrowed code: an unlabeled `break` or `continue` with no loop or `switch` in between, a `return` or `throw` with no `try` in between; a labeled jump, or a write that falls through to a read, keeps the read wide. Field read calls such as `this.at(r * 16 + f)` and `this.at(sq)` on a 0x88 board are then in the board's floor. `PERRY_FACTS_EXACT_RULES=0` and `PERRY_FACTS_LEAVING_WRITES=0` turn each off; `PERRY_FACTS_SABOTAGE=exactrule` and `leavingwrite` are the negative controls. diff --git a/crates/perry-wpfacts/src/gen.rs b/crates/perry-wpfacts/src/gen.rs index a444310db8b..95d0ef7a8ed 100644 --- a/crates/perry-wpfacts/src/gen.rs +++ b/crates/perry-wpfacts/src/gen.rs @@ -368,6 +368,20 @@ pub struct Gen<'a> { /// Guards narrow locals by presence: a truthy or non-nullish test /// filters out `null`/`undefined` (`FactsConfig::no_guard_presence`). pub guard_presence: bool, + /// R1: a write of a narrowed local in a branch that always leaves past + /// the narrowing's code does not end its narrowed reads after the branch + /// (`gen::narrow`, "Writes on a leaving path"; + /// `FactsConfig::no_leaving_writes`). + pub leaving_writes: bool, + /// Negative control (`PERRY_FACTS_SABOTAGE=leavingwrite`): every + /// branch's writes are dropped from the reads after it, also a branch + /// that falls through to them. + pub leaving_write_sabotage: bool, + /// The loops and `switch`es (`jumps`) and `try` statements (`tries`) + /// the walk is inside: where an unlabeled `break`/`continue` lands, and + /// whether a `throw` or a `finally` stays inside a narrowing's code. + pub jumps: u32, + pub tries: u32, /// The `import()` / `require(expr)` specifiers of the bodies walked, by /// module (`live_dynamic_imports`): in the activation pass, the sites a /// body that can run holds. @@ -694,6 +708,10 @@ impl<'a> Gen<'a> { new_array_site: None, guard_ranges: true, guard_presence: true, + leaving_writes: true, + leaving_write_sabotage: false, + jumps: 0, + tries: 0, dynimport_seen: Default::default(), dynamic_only: Default::default(), roots: Vec::new(), diff --git a/crates/perry-wpfacts/src/gen/narrow.rs b/crates/perry-wpfacts/src/gen/narrow.rs index fa3a38cd287..178c506f5b1 100644 --- a/crates/perry-wpfacts/src/gen/narrow.rs +++ b/crates/perry-wpfacts/src/gen/narrow.rs @@ -35,6 +35,27 @@ //! The bound is a literal, a local, or a local's `length` (an Array's //! carries its length interval, `solve::arr_len`). //! +//! ## Writes on a leaving path +//! +//! A write ends the start reads for the code it can reach, not for the +//! program text after it. A branch of an `if` that always leaves +//! (`always_exits`) reaches the code after the `if` only through its jumps, +//! so after the branch each narrowing's `written` is what it was before it +//! when every way out of the branch lands outside the narrowing's code +//! (`jumps_leave`): +//! - an unlabeled `break`/`continue` out of the branch, with no loop or +//! `switch` between the `if` and the narrowing (`Gen::jumps`): it lands at +//! the narrowed loop's update (which reads the end node) or past the +//! guarded code; +//! - a `return` or `throw`, and any exception, with no `try` between them +//! (`Gen::tries`): no `catch` or `finally` of the narrowing's code runs +//! after it; +//! - no labeled jump (where it lands is not followed). +//! +//! The write still reaches the end node and the local, so the update and +//! every read the jump reaches see it. `PERRY_FACTS_LEAVING_WRITES=0` ends +//! the start reads at the first write in the text again. +//! //! The rule only applies where no other code can write `i` during the loop: //! `i` is declared by the loop's `init` and no closure appears in the loop. //! A nested loop that writes `i` ends the start reads before it (its body @@ -55,6 +76,10 @@ pub(crate) struct Narrow { /// The update is walked: it reads the end node, and its write (which /// runs after the body) reaches only the counter. in_update: bool, + /// `Gen::jumps` and `Gen::tries` where the narrowed code starts (for a + /// loop, inside it): "Writes on a leaving path". + jumps: u32, + tries: u32, } fn expr_has(e: &Expr, p: &mut impl FnMut(&Expr) -> bool) -> bool { @@ -160,6 +185,8 @@ impl<'a> Gen<'a> { end, written: false, in_update: false, + jumps: self.jumps, + tries: self.tries, }); true } @@ -205,6 +232,34 @@ impl<'a> Gen<'a> { } } + /// Before walking a branch of an `if`: each narrowing's `written`. + pub(crate) fn narrow_snapshot(&self) -> Vec { + if !self.leaving_writes { + return Vec::new(); + } + self.narrow.iter().map(|n| n.written).collect() + } + + /// After walking `branch` (`pre` from `narrow_snapshot` before it): a + /// write in a branch that always leaves past a narrowing's code does + /// not reach the reads after the `if` (module docs, "Writes on a + /// leaving path"). + pub(crate) fn narrow_leave(&mut self, branch: &[Stmt], pre: Vec) { + if pre.is_empty() { + return; + } + let sabotage = self.leaving_write_sabotage; + if !sabotage && !(always_exits(branch) && jumps_leave(branch)) { + return; + } + let (f, jumps, tries) = (self.m.cur_fn, self.jumps, self.tries); + for (n, w) in self.narrow.iter_mut().zip(pre) { + if n.f == f && (sabotage || (n.jumps == jumps && n.tries == tries)) { + n.written = w; + } + } + } + /// Before walking a nested loop: a narrowed counter it writes is read /// through the end node inside it (a read there may follow the write). pub(crate) fn narrow_enter_loop(&mut self, s: &Stmt) { @@ -437,6 +492,37 @@ pub(crate) fn always_exits(ss: &[Stmt]) -> bool { ) } +/// Whether every jump out of `ss` lands where an unlabeled jump at the +/// statement around `ss` lands, or leaves the function: no labeled `break` +/// or `continue` (where it lands is not followed). A `break` inside a loop +/// or `switch` of `ss`, and a `continue` inside a loop of it, stay in `ss`. +/// Nested function bodies are expressions: not walked. +pub(crate) fn jumps_leave(ss: &[Stmt]) -> bool { + ss.iter().all(|s| match s { + Stmt::LabeledBreak(_) | Stmt::LabeledContinue(_) => false, + Stmt::If { + then_branch, + else_branch, + .. + } => jumps_leave(then_branch) && else_branch.as_deref().is_none_or(jumps_leave), + Stmt::While { body, .. } | Stmt::DoWhile { body, .. } | Stmt::For { body, .. } => { + jumps_leave(body) + } + Stmt::Switch { cases, .. } => cases.iter().all(|c| jumps_leave(&c.body)), + Stmt::Try { + body, + catch, + finally, + } => { + jumps_leave(body) + && catch.as_ref().is_none_or(|c| jumps_leave(&c.body)) + && finally.as_deref().is_none_or(jumps_leave) + } + Stmt::Labeled { body, .. } => jumps_leave(std::slice::from_ref(body)), + _ => true, + }) +} + /// Whether running `ss` may reach its end: a function body that does /// returns `undefined` there. Conservative: a `return` or `throw` on every /// path (through `if`/`else`, `try`, a `switch` with a `default` and an @@ -929,6 +1015,8 @@ impl<'a> Gen<'a> { end, written: false, in_update: false, + jumps: self.jumps, + tries: self.tries, }); pushed += 1; } diff --git a/crates/perry-wpfacts/src/gen/walk.rs b/crates/perry-wpfacts/src/gen/walk.rs index 02fa4444565..b2937576083 100644 --- a/crates/perry-wpfacts/src/gen/walk.rs +++ b/crates/perry-wpfacts/src/gen/walk.rs @@ -1206,34 +1206,44 @@ impl<'a> Gen<'a> { guard: Some((t, then_test)), ..fx.clone() }; + // A branch that always leaves: its writes reach only where + // it jumps to (`narrow_leave`). + let pre = self.narrow_snapshot(); let k = self.narrow_guard(fx, condition, true); self.stmts(&then_fx, then_branch); self.narrow_pop(k); + self.narrow_leave(then_branch, pre); self.own_guard_done(own); if let Some(e) = else_branch { let else_fx = Fx { guard: Some((t, else_test)), ..fx.clone() }; + let pre = self.narrow_snapshot(); let k = self.narrow_guard(fx, condition, false); self.stmts(&else_fx, e); self.narrow_pop(k); + self.narrow_leave(e, pre); } } Stmt::While { condition, body } => { self.narrow_enter_loop(s); self.loop_depth += 1; + self.jumps += 1; let _ = self.expr(fx, condition); let k = self.narrow_guard(fx, condition, true); self.stmts(fx, body); self.narrow_pop(k); + self.jumps -= 1; self.loop_depth -= 1; } Stmt::DoWhile { body, condition } => { self.narrow_enter_loop(s); self.loop_depth += 1; + self.jumps += 1; let _ = self.expr(fx, condition); self.stmts(fx, body); + self.jumps -= 1; self.loop_depth -= 1; } Stmt::For { @@ -1247,6 +1257,7 @@ impl<'a> Gen<'a> { self.stmt(fx, i); } self.loop_depth += 1; + self.jumps += 1; if let Some(c) = condition { let _ = self.expr(fx, c); } @@ -1274,6 +1285,7 @@ impl<'a> Gen<'a> { if narrowed { self.narrow_end(); } + self.jumps -= 1; self.loop_depth -= 1; } Stmt::Labeled { body, .. } => self.stmt(fx, body), @@ -1303,6 +1315,7 @@ impl<'a> Gen<'a> { // finally run in the enclosing one. let rt = self.m.node_l("RAISE-try"); let outer = std::mem::replace(&mut self.m.gen_region, Some(rt)); + self.tries += 1; self.stmts(fx, body); self.m.gen_region = outer; if let Some(c) = catch { @@ -1319,6 +1332,7 @@ impl<'a> Gen<'a> { if let Some(f) = finally { self.stmts(fx, f); } + self.tries -= 1; } Stmt::Switch { discriminant, @@ -1327,12 +1341,14 @@ impl<'a> Gen<'a> { let d = self.expr(fx, discriminant); // `===` against case values: no coercion. let _ = d; + self.jumps += 1; for c in cases { if let Some(t) = &c.test { let _ = self.expr(fx, t); } self.stmts(fx, &c.body); } + self.jumps -= 1; } } } diff --git a/crates/perry-wpfacts/src/lib.rs b/crates/perry-wpfacts/src/lib.rs index df839dc2c68..d96d71080b6 100644 --- a/crates/perry-wpfacts/src/lib.rs +++ b/crates/perry-wpfacts/src/lib.rs @@ -90,6 +90,14 @@ pub struct FactsConfig { /// No `Rep::Arr` for a field and no in-floor field read call /// (`PERRY_FACTS_ARRAY_FIELDS=0`, DESIGN-p4l1 PR-C3). pub no_array_fields: bool, + /// R1: a `Cons::Range` result widens like any node again, after + /// `WIDEN_STEPS` growths (`PERRY_FACTS_EXACT_RULES=0`; + /// `solve::grow_rule_range`). + pub no_exact_rules: bool, + /// R1: a write of a narrowed local in a branch that always leaves ends + /// the narrowed reads after the branch again (`PERRY_FACTS_LEAVING_WRITES=0`; + /// `gen::narrow`, "Writes on a leaving path"). + pub no_leaving_writes: bool, /// An element read's past-the-end `undefined` is unconditional again /// (`PERRY_FACTS_ELEM_UNDEF=0`, PR-C1: `Cons::ElemUndef`). pub no_elem_undef: bool, @@ -488,6 +496,10 @@ fn generate<'a>( g.m.arr_front_sabotage = cfg.sabotage.as_deref() == Some("arrfront"); g.m.array_fields = !cfg.no_array_fields; g.m.arr_field_sabotage = cfg.sabotage.as_deref() == Some("arrfield"); + g.m.exact_rules = !cfg.no_exact_rules; + g.m.exact_rule_sabotage = cfg.sabotage.as_deref() == Some("exactrule"); + g.leaving_writes = !cfg.no_leaving_writes; + g.leaving_write_sabotage = cfg.sabotage.as_deref() == Some("leavingwrite"); g.int_ranges = !cfg.no_int_ranges; g.arr_lengths = g.int_ranges && !cfg.no_array_lengths; g.guard_ranges = g.int_ranges && !cfg.no_guard_ranges; diff --git a/crates/perry-wpfacts/src/model.rs b/crates/perry-wpfacts/src/model.rs index ff608963fd4..b87551cee15 100644 --- a/crates/perry-wpfacts/src/model.rs +++ b/crates/perry-wpfacts/src/model.rs @@ -1259,6 +1259,14 @@ pub struct Model { /// `+` interval rule drops its right operand, a wrong transfer the /// int32 witnesses must catch. pub range_sabotage: bool, + /// R1: a `Cons::Range` result takes the join of its rule's evaluations + /// without widening (`solve::grow_rule_range`); only copy targets widen. + /// `PERRY_FACTS_EXACT_RULES=0` widens a result like any node. + pub exact_rules: bool, + /// Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): a rule result + /// keeps its first interval, a claim too narrow for the values its + /// operands grow to, which the witnesses must catch. + pub exact_rule_sabotage: bool, /// Negative control (`PERRY_FACTS_SABOTAGE=arrlen`): every index store /// counts as one inside its array's birth length (`arr_len_index`). pub arr_len_sabotage: bool, diff --git a/crates/perry-wpfacts/src/solve.rs b/crates/perry-wpfacts/src/solve.rs index 37a7f7a732f..d8f1482999a 100644 --- a/crates/perry-wpfacts/src/solve.rs +++ b/crates/perry-wpfacts/src/solve.rs @@ -1929,3 +1929,41 @@ pub(crate) fn grow_range(node: &mut Node, iv: Iv) -> bool { node.drange = true; true } + +/// Join `iv` into the result of a [`Cons::Range`] rule (R1, sum widening). +/// +/// The rule's result is `op` over its operands' intervals at each +/// evaluation, and every operand only grows, so the join is the rule over +/// the operands' last intervals: a rule result needs no widening of its own. +/// The operands are what widen: a loop counter (a copy target, `grow_range`) +/// climbs the ladder and the loop test clips it back (`gen::narrow`), so +/// `r * 16 + f` over `r, f` in `[0, 7]` is `[0, 119]`, where widening the +/// sum after `WIDEN_STEPS` of its operands' growths jumped to a rung (127, +/// then 255). +/// +/// Termination: the rule results form no cycle among themselves (each +/// rule's operands exist before its result node is ruled, and a result has +/// one rule), so every cycle passes a copy target, which widens, and a +/// result grows at most once per operand growth. Past `WIDEN_LIMIT` growths +/// it still climbs the ladder (a backstop that bounds even a cycle the +/// argument missed). +pub(crate) fn grow_rule_range(node: &mut Node, iv: Iv, sabotage: bool) -> bool { + use crate::model::range::{widen, WIDEN_LIMIT}; + // Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): the result keeps + // its first interval, whatever its operands grow to. + if sabotage && !node.range.is_empty() { + return false; + } + let joined = node.range.join(iv); + if joined == node.range { + return false; + } + node.rsteps = node.rsteps.saturating_add(1); + node.range = if node.rsteps > WIDEN_LIMIT { + widen(node.range, joined) + } else { + joined + }; + node.drange = true; + true +} diff --git a/crates/perry-wpfacts/src/solve/apply.rs b/crates/perry-wpfacts/src/solve/apply.rs index ca8fa1546c5..0595f933230 100644 --- a/crates/perry-wpfacts/src/solve/apply.rs +++ b/crates/perry-wpfacts/src/solve/apply.rs @@ -1487,7 +1487,13 @@ impl Model { .unwrap_or_else(|| crate::model::range::eval(op, l, r)) } }; - if crate::solve::grow_range(&mut self.nodes[dst as usize], iv) { + let d = &mut self.nodes[dst as usize]; + let grew = if self.exact_rules { + crate::solve::grow_rule_range(d, iv, self.exact_rule_sabotage) + } else { + crate::solve::grow_range(d, iv) + }; + if grew { let d = &mut self.nodes[dst as usize]; if !d.in_wl { d.in_wl = true; diff --git a/crates/perry-wpfacts/src/tests.rs b/crates/perry-wpfacts/src/tests.rs index c667ca327fb..eab85d6f9f7 100644 --- a/crates/perry-wpfacts/src/tests.rs +++ b/crates/perry-wpfacts/src/tests.rs @@ -143,6 +143,7 @@ mod proto_lock_keys; mod proto_value; mod protocol_calls; mod protocol_keys; +mod range_tightening; mod reach_accessor; mod receiver_slots; mod receiver_this; diff --git a/crates/perry-wpfacts/src/tests/range_tightening.rs b/crates/perry-wpfacts/src/tests/range_tightening.rs new file mode 100644 index 00000000000..0638efdca41 --- /dev/null +++ b/crates/perry-wpfacts/src/tests/range_tightening.rs @@ -0,0 +1,160 @@ +//! R1 (range tightening): a rule's result is not widened past the rule over +//! its operands (`solve::grow_rule_range`), and a counter write in a branch +//! that always leaves does not end the narrowed reads after it +//! (`gen::narrow`, "Writes on a leaving path"). Each verdict is read where it +//! is consumed: the key interval of a field read call (`at(k)` over a board +//! born dense with 128 elements) and whether it is in the floor. + +use super::*; + +/// `(call text, key interval, in floor)` of every field read call of `src`. +fn keys(src: &str, cfg: FactsConfig) -> Vec<(String, Option<(i64, i64)>, bool)> { + let pf = facts_with(src, cfg); + let mut out = Vec::new(); + for mb in &pf.bindings { + for (offset, c) in &mb.field_read_calls { + // Offsets are 1-based. + let rest = &src[*offset as usize - 1..]; + let end = rest.find(';').unwrap_or(rest.len()); + let key = mb + .call_arg_ranges + .binary_search_by_key(offset, |(o, _)| *o) + .ok() + .and_then(|at| mb.call_arg_ranges[at].1.get(c.index_arg as usize).copied()) + .flatten(); + out.push((rest[..end].to_string(), key, c.in_floor)); + } + } + out +} + +fn call(calls: &[(String, Option<(i64, i64)>, bool)], text: &str) -> (Option<(i64, i64)>, bool) { + let c = calls + .iter() + .find(|(t, ..)| t.starts_with(text)) + .unwrap_or_else(|| panic!("no call {text}: {calls:?}")); + (c.1, c.2) +} + +const BOARD: &str = "class B {\n\ + board: number[] = new Array(128).fill(0);\n\ + at(i: number): number { return this.board[i] ?? 0; }\n"; + +fn program(methods: &str, calls: &str) -> String { + format!("{BOARD}{methods}\n}}\nconst b = new B();\nconsole.log({calls});\n") +} + +/// The shapes of the C3 probe (qb9 c3/probe/rg): one method per key. +fn probe() -> String { + program( + " mulOnly(): number { let s = 0; for (let r = 0; r < 8; r++) s += this.at(r * 16); return s; }\n\ + mulAdd(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); return s; }\n\ + addOnly(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r + f); return s; }\n\ + down(): number { let s = 0; for (let r = 7; r >= 0; r--) for (let f = 0; f < 8; f++) s += this.at(r * 16 - f + 7); return s; }\n\ + skip(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 7; continue; } s += this.at(q + 0); } return s; }\n\ + plain(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) continue; s += this.at(q - 0); } return s; }\n\ + elseLeaves(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) === 0) { s += 1; } else { q += 7; continue; } s += this.at(q * 1); } return s; }", + "b.mulOnly(), b.mulAdd(), b.addOnly(), b.down(), b.skip(), b.plain(), b.elseLeaves()", + ) +} + +#[test] +fn a_sum_of_two_counters_is_their_hull() { + let calls = keys(&probe(), FactsConfig::default()); + assert_eq!(call(&calls, "this.at(r * 16)"), (Some((0, 112)), true)); + assert_eq!(call(&calls, "this.at(r * 16 + f)"), (Some((0, 119)), true)); + assert_eq!(call(&calls, "this.at(r + f)"), (Some((0, 14)), true)); + assert_eq!( + call(&calls, "this.at(r * 16 - f + 7)"), + (Some((0, 119)), true) + ); +} + +#[test] +fn a_write_in_a_branch_that_leaves_keeps_the_narrowed_reads() { + let calls = keys(&probe(), FactsConfig::default()); + assert_eq!(call(&calls, "this.at(q + 0)"), (Some((0, 127)), true)); + assert_eq!(call(&calls, "this.at(q - 0)"), (Some((0, 127)), true)); + assert_eq!(call(&calls, "this.at(q * 1)"), (Some((0, 127)), true)); +} + +#[test] +fn the_switches_off_give_the_widened_intervals_back() { + let rules_off = keys( + &probe(), + FactsConfig { + no_exact_rules: true, + ..Default::default() + }, + ); + let (k, _) = call(&rules_off, "this.at(r + f)"); + assert!(k.is_some_and(|(_, hi)| hi > 14), "{k:?}"); + let (k, in_floor) = call(&rules_off, "this.at(r * 16 + f)"); + assert!(k.is_some_and(|(_, hi)| hi > 127) && !in_floor, "{k:?}"); + let writes_off = keys( + &probe(), + FactsConfig { + no_leaving_writes: true, + ..Default::default() + }, + ); + let (k, in_floor) = call(&writes_off, "this.at(q + 0)"); + assert!(k.is_some_and(|(_, hi)| hi > 127) && !in_floor, "{k:?}"); + // A bare `continue` writes nothing: narrowed either way. + assert_eq!(call(&writes_off, "this.at(q - 0)"), (Some((0, 127)), true)); +} + +/// Negative controls: a write that reaches a later read keeps it wide. +fn reaching() -> String { + program( + " falls(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 7; } s += this.at(q + 0); } return s; }\n\ + inSwitch(k: number): number { let s = 0; for (let q = 0; q < 128; q++) { switch (k) { case 1: if (q > 3) { q += 200; break; } s += 1; } s += this.at(q - 0); } return s; }\n\ + inTry(): number { let s = 0; for (let q = 0; q < 128; q++) { try { if (q > 3) { q += 200; continue; } } finally { s += this.at(q * 1); } } return s; }\n\ + labeled(): number { let s = 0; outer: for (let q = 0; q < 128; q++) { if (q > 3) { q += 200; continue outer; } s += this.at(q | 0); } return s; }\n\ + sumPast(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f + 9); return s; }", + "b.falls(), b.inSwitch(1), b.inSwitch(2), b.inTry(), b.labeled(), b.sumPast()", + ) +} + +#[test] +fn a_write_that_reaches_a_later_read_keeps_it_wide() { + let calls = keys(&reaching(), FactsConfig::default()); + for (text, reach) in [ + // `q + 7` falls through to the read. + ("this.at(q + 0)", 134), + // The `break` lands after the `switch`, before the read. + ("this.at(q - 0)", 327), + // The `finally` runs after the `continue`. + ("this.at(q * 1)", 327), + // A labeled jump is not followed (conservative). + ("this.at(q | 0)", 327), + // The sum's hull is past the floor. + ("this.at(r * 16 + f + 9)", 128), + ] { + let (k, in_floor) = call(&calls, text); + assert!( + k.is_none_or(|(_, hi)| hi >= reach) && !in_floor, + "{text}: {k:?} {in_floor}" + ); + } +} + +#[test] +fn the_sabotage_arms_claim_a_read_in_the_floor_that_is_not() { + let leaving = keys( + &reaching(), + FactsConfig { + sabotage: Some("leavingwrite".into()), + ..Default::default() + }, + ); + assert!(call(&leaving, "this.at(q + 0)").1, "{leaving:?}"); + let exact = keys( + &reaching(), + FactsConfig { + sabotage: Some("exactrule".into()), + ..Default::default() + }, + ); + assert!(call(&exact, "this.at(r * 16 + f + 9)").1, "{exact:?}"); +} diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs index dd784b9a12c..5fdc3b42873 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -73,10 +73,12 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[ "PERRY_FACTS_CONST_LENGTH", "PERRY_FACTS_CONST_NUMBERS", "PERRY_FACTS_ELEM_UNDEF", + "PERRY_FACTS_EXACT_RULES", "PERRY_FACTS_FIELD_READ_CALLS", "PERRY_FACTS_CANONICAL_NUMBERS", "PERRY_FACTS_GUARD_PRESENCE", "PERRY_FACTS_GUARD_RANGES", + "PERRY_FACTS_LEAVING_WRITES", "PERRY_FACTS_SITE_ARGS", "PERRY_FACTS_SABOTAGE", "PERRY_FACTS_SUPPRESS_BIRTH", diff --git a/crates/perry/src/commands/compile/compile_env/tests.rs b/crates/perry/src/commands/compile/compile_env/tests.rs index ee554d4f850..3645665e5b1 100644 --- a/crates/perry/src/commands/compile/compile_env/tests.rs +++ b/crates/perry/src/commands/compile/compile_env/tests.rs @@ -346,3 +346,16 @@ fn const_number_switch_is_a_cache_input() { "PERRY_FACTS_CONST_NUMBERS must key the compile caches" ); } + +/// R1: the range-tightening switches change the facts' intervals (and with +/// them in-floor reads and int32 locals), so `=0` must never reuse an `=1` +/// object. +#[test] +fn range_tightening_switches_are_cache_inputs() { + for name in ["PERRY_FACTS_EXACT_RULES", "PERRY_FACTS_LEAVING_WRITES"] { + assert!( + COMPILE_ENV_VARS.contains(&name), + "{name} must key the compile caches" + ); + } +} diff --git a/crates/perry/src/commands/compile/program_facts.rs b/crates/perry/src/commands/compile/program_facts.rs index e6e253f60f9..a3262748c2c 100644 --- a/crates/perry/src/commands/compile/program_facts.rs +++ b/crates/perry/src/commands/compile/program_facts.rs @@ -151,6 +151,14 @@ pub(crate) fn run( std::env::var("PERRY_FACTS_ARRAY_FIELDS").as_deref(), Ok("0") | Ok("off") | Ok("false") ), + no_exact_rules: matches!( + std::env::var("PERRY_FACTS_EXACT_RULES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), + no_leaving_writes: matches!( + std::env::var("PERRY_FACTS_LEAVING_WRITES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), no_elem_undef: matches!( std::env::var("PERRY_FACTS_ELEM_UNDEF").as_deref(), Ok("0") | Ok("off") | Ok("false") @@ -896,6 +904,14 @@ pub(crate) fn activation( std::env::var("PERRY_FACTS_ARRAY_FIELDS").as_deref(), Ok("0") | Ok("off") | Ok("false") ), + no_exact_rules: matches!( + std::env::var("PERRY_FACTS_EXACT_RULES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), + no_leaving_writes: matches!( + std::env::var("PERRY_FACTS_LEAVING_WRITES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), no_elem_undef: matches!( std::env::var("PERRY_FACTS_ELEM_UNDEF").as_deref(), Ok("0") | Ok("off") | Ok("false") diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py index c925fbb5ad0..0047d8a4ddf 100644 --- a/scripts/test-verify-facts-s0.py +++ b/scripts/test-verify-facts-s0.py @@ -119,6 +119,8 @@ def oracle(source, *argv): ("array-front-negative", "arrfront", "array rep"), ("array-field-negative", "arrfield", "array rep"), ("array-b1-negative", "arrb1", "array rep"), + ("range-sum-negative", "exactrule", "array rep"), + ("leaving-write-negative", "leavingwrite", "array rep"), ("number-call-negative", "numbercall", "numeric result"), ("field-read-call-negative", "fieldreadcall", "field read call"), ("array-undef-negative", "arrundef", "element floor"), diff --git a/scripts/verify_facts_s0/leaving-write-negative.ts b/scripts/verify_facts_s0/leaving-write-negative.ts new file mode 100644 index 00000000000..a28ad65fa2f --- /dev/null +++ b/scripts/verify_facts_s0/leaving-write-negative.ts @@ -0,0 +1,26 @@ +// `at` is a field element read, and `board` is born dense with 16 +// elements. In `walk` the counter write `q += 20` is in a branch that falls +// through to the read, so the read's key reaches past the floor (its value +// is the `?? 0`). Under PERRY_FACTS_SABOTAGE=leavingwrite every branch's +// writes are dropped from the reads after it, so the facts claim the key is +// the loop test's `[0, 15]`, in the floor, and the call loads the slot with +// no bound. The element tier's witness must report the false proof at the +// key. +class Board { + board: number[] = new Array(16).fill(1); + at(sq: number): number { + return this.board[sq] ?? 0; + } + walk(n: number): number { + let s = 0; + for (let q = 0; q < 16; q++) { + if (q === n) { + q += 20; + } + s += this.at(q); + } + return s; + } +} +const b = new Board(); +console.log(b.walk(process.argv.length > 100 ? 99 : 5)); diff --git a/scripts/verify_facts_s0/range-sum-negative.ts b/scripts/verify_facts_s0/range-sum-negative.ts new file mode 100644 index 00000000000..4a5671fa7e3 --- /dev/null +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -0,0 +1,20 @@ +// `at` is a field element read, and `board` is born dense with 64 +// elements. `sum` reads the keys `r * 16 + f` for `r, f` in `[0, 7]`: the +// hull `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. +// Under PERRY_FACTS_SABOTAGE=exactrule an interval rule's result keeps its +// first interval, so the facts claim the key is in the floor and the call +// loads the slot with no bound. The element tier's witness must report the +// false proof at the key. +class Board { + board: number[] = new Array(64).fill(1); + at(sq: number): number { + return this.board[sq] ?? 0; + } + sum(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); + return s; + } +} +const b = new Board(); +console.log(b.sum()); diff --git a/tests/parity/language/array/test_range_tightening.ts b/tests/parity/language/array/test_range_tightening.ts new file mode 100644 index 00000000000..dbbd9bcebe2 --- /dev/null +++ b/tests/parity/language/array/test_range_tightening.ts @@ -0,0 +1,165 @@ +// R1 (range tightening): keys whose intervals the facts now prove tighter, +// and the negative controls that must stay wide. Every read goes through +// `at`, a field read call (`this.board[i] ?? -1`) on a board born dense, so +// a key claimed in the floor that is not would read past the elements +// instead of giving -1. + +class Board { + board: number[]; + constructor(n: number) { + this.board = new Array(n).fill(0); + for (let i = 0; i < n; i++) this.board[i] = (i * 7) % 13; + } + at(i: number): number { + return this.board[i] ?? -1; + } + + // (a) sums of two counters: the hull, not the widened sum. + rankFile(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); + return s; + } + diagonal(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r + f); + return s; + } + window(file: number): number { + let s = 0; + for (let r = 1; r >= 0 && r < 8; r++) { + for (let f = Math.max(0, file - 1); f <= Math.min(7, file + 1); f++) s += this.at(r * 16 + f); + } + return s; + } + // Negative control: the hull is past a 128 floor; the last keys are -1. + pastHull(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f + 9); + return s; + } + + // (b) a counter write in a branch that leaves. + skip(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if ((q & 0x88) !== 0) { q += 7; continue; } + s += this.at(q); + } + return s; + } + skipElse(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if ((q & 0x88) === 0) { s += 1; } else { q += 7; continue; } + s += this.at(q); + } + return s; + } + skipReturn(stop: number): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if (q === stop) { q += 500; return s + this.at(q); } + s += this.at(q); + } + return s; + } + skipBreak(stop: number): number { + let s = 0; + let q = 0; + for (q = 0; q < 128; q++) { + if (q === stop) { q += 500; break; } + s += this.at(q); + } + return s * 1000 + this.at(q); + } + guarded(x: number): number { + if (x < 100) { + if (x === 42) { x += 1000; return this.at(x); } + return this.at(x); + } + return -7; + } + + // Negative controls: the write reaches a later read. + falls(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if ((q & 0x88) !== 0) { q += 7; } + s += this.at(q) + 2; + } + return s; + } + inSwitch(k: number): number { + let s = 0; + for (let q = 0; q < 128; q++) { + switch (k) { + case 1: + if (q > 100) { q += 200; break; } + s += 1; + } + s += this.at(q); + } + return s; + } + inTry(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + try { + if (q > 100) { q += 200; continue; } + } finally { + s += this.at(q); + } + } + return s; + } + inCatch(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + try { + if (q > 100) { q += 200; throw new Error("x"); } + } catch (e) { + s += this.at(q) * 3; + } + } + return s; + } + labeled(): number { + let s = 0; + outer: for (let q = 0; q < 128; q++) { + if (q > 100) { q += 200; continue outer; } + s += this.at(q); + } + return s; + } + innerLoop(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + for (let j = 0; j < 2; j++) { + if (q > 100 && j === 1) { q += 200; continue; } + s += this.at(q); + } + s += this.at(q); + } + return s; + } + guardedLoop(x: number): number { + let s = 0; + if (x < 100) { + for (let j = 0; j < 3; j++) { + if (j === 1) { x += 1000; break; } + } + s += this.at(x); + } + return s; + } +} + +const b = new Board(128); +console.log(b.rankFile(), b.diagonal(), b.window(0), b.window(3), b.window(7), b.pastHull()); +console.log(b.skip(), b.skipElse(), b.skipReturn(40), b.skipReturn(999), b.skipBreak(17), b.skipBreak(999)); +console.log(b.guarded(5), b.guarded(42), b.guarded(150)); +console.log(b.falls(), b.inSwitch(1), b.inSwitch(2), b.inTry(), b.inCatch(), b.labeled(), b.innerLoop()); +console.log(b.guardedLoop(3), b.guardedLoop(120)); +const small = new Board(64); +console.log(small.rankFile(), small.diagonal(), small.skip(), small.falls()); From 1231ef360a31c8d3fb1fd11eccb5a884bcbf18ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 08:52:27 +0100 Subject: [PATCH 2/4] wpfacts: R1 test: the labeled control's test implies no clip --- crates/perry-wpfacts/src/tests/range_tightening.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/perry-wpfacts/src/tests/range_tightening.rs b/crates/perry-wpfacts/src/tests/range_tightening.rs index 0638efdca41..5fb773f1f55 100644 --- a/crates/perry-wpfacts/src/tests/range_tightening.rs +++ b/crates/perry-wpfacts/src/tests/range_tightening.rs @@ -110,7 +110,7 @@ fn reaching() -> String { " falls(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 7; } s += this.at(q + 0); } return s; }\n\ inSwitch(k: number): number { let s = 0; for (let q = 0; q < 128; q++) { switch (k) { case 1: if (q > 3) { q += 200; break; } s += 1; } s += this.at(q - 0); } return s; }\n\ inTry(): number { let s = 0; for (let q = 0; q < 128; q++) { try { if (q > 3) { q += 200; continue; } } finally { s += this.at(q * 1); } } return s; }\n\ - labeled(): number { let s = 0; outer: for (let q = 0; q < 128; q++) { if (q > 3) { q += 200; continue outer; } s += this.at(q | 0); } return s; }\n\ + labeled(): number { let s = 0; outer: for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 200; continue outer; } s += this.at(q | 0); } return s; }\n\ sumPast(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f + 9); return s; }", "b.falls(), b.inSwitch(1), b.inSwitch(2), b.inTry(), b.labeled(), b.sumPast()", ) From 93bb48b2f2db14e49e5dbbc8dd6a54682fe4f790 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 10:18:10 +0100 Subject: [PATCH 3/4] wpfacts: R1 exactrule sabotage is a deterministic wrong sum (the operands' hull) --- crates/perry-wpfacts/src/model.rs | 6 +++--- crates/perry-wpfacts/src/solve.rs | 7 +------ crates/perry-wpfacts/src/solve/apply.rs | 6 +++++- scripts/verify_facts_s0/range-sum-negative.ts | 12 ++++++------ 4 files changed, 15 insertions(+), 16 deletions(-) diff --git a/crates/perry-wpfacts/src/model.rs b/crates/perry-wpfacts/src/model.rs index 988cd36b101..9bc979dff00 100644 --- a/crates/perry-wpfacts/src/model.rs +++ b/crates/perry-wpfacts/src/model.rs @@ -1263,9 +1263,9 @@ pub struct Model { /// without widening (`solve::grow_rule_range`); only copy targets widen. /// `PERRY_FACTS_EXACT_RULES=0` widens a result like any node. pub exact_rules: bool, - /// Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): a rule result - /// keeps its first interval, a claim too narrow for the values its - /// operands grow to, which the witnesses must catch. + /// Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): with the exact + /// rule results, a sum is the hull of its operands instead of their + /// sum, a claim too narrow that the witnesses must catch. pub exact_rule_sabotage: bool, /// Negative control (`PERRY_FACTS_SABOTAGE=arrlen`): every index store /// counts as one inside its array's birth length (`arr_len_index`). diff --git a/crates/perry-wpfacts/src/solve.rs b/crates/perry-wpfacts/src/solve.rs index d8f1482999a..8e0a721db1e 100644 --- a/crates/perry-wpfacts/src/solve.rs +++ b/crates/perry-wpfacts/src/solve.rs @@ -1947,13 +1947,8 @@ pub(crate) fn grow_range(node: &mut Node, iv: Iv) -> bool { /// result grows at most once per operand growth. Past `WIDEN_LIMIT` growths /// it still climbs the ladder (a backstop that bounds even a cycle the /// argument missed). -pub(crate) fn grow_rule_range(node: &mut Node, iv: Iv, sabotage: bool) -> bool { +pub(crate) fn grow_rule_range(node: &mut Node, iv: Iv) -> bool { use crate::model::range::{widen, WIDEN_LIMIT}; - // Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): the result keeps - // its first interval, whatever its operands grow to. - if sabotage && !node.range.is_empty() { - return false; - } let joined = node.range.join(iv); if joined == node.range { return false; diff --git a/crates/perry-wpfacts/src/solve/apply.rs b/crates/perry-wpfacts/src/solve/apply.rs index 0595f933230..8c5f5c7bbbb 100644 --- a/crates/perry-wpfacts/src/solve/apply.rs +++ b/crates/perry-wpfacts/src/solve/apply.rs @@ -1480,6 +1480,10 @@ impl Model { let (l, r) = if right { (ot, me) } else { (me, ot) }; if self.range_sabotage && op == RangeOp::Add { l + } else if self.exact_rule_sabotage && op == RangeOp::Add { + // Negative control (`exactrule`): a sum is the hull + // of its operands, not their sum. + l.join(r) } else { self.const_numbers .then(|| crate::model::range::eval_exact(op, l, r)) @@ -1489,7 +1493,7 @@ impl Model { }; let d = &mut self.nodes[dst as usize]; let grew = if self.exact_rules { - crate::solve::grow_rule_range(d, iv, self.exact_rule_sabotage) + crate::solve::grow_rule_range(d, iv) } else { crate::solve::grow_range(d, iv) }; diff --git a/scripts/verify_facts_s0/range-sum-negative.ts b/scripts/verify_facts_s0/range-sum-negative.ts index 4a5671fa7e3..ba87632eeea 100644 --- a/scripts/verify_facts_s0/range-sum-negative.ts +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -1,12 +1,12 @@ -// `at` is a field element read, and `board` is born dense with 64 +// `at` is a field element read, and `board` is born dense with 116 // elements. `sum` reads the keys `r * 16 + f` for `r, f` in `[0, 7]`: the -// hull `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. -// Under PERRY_FACTS_SABOTAGE=exactrule an interval rule's result keeps its -// first interval, so the facts claim the key is in the floor and the call -// loads the slot with no bound. The element tier's witness must report the +// sum `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. +// Under PERRY_FACTS_SABOTAGE=exactrule a sum's interval is the hull of its +// operands (`r * 16` is `[0, 112]`), so the facts claim the key is in the +// floor and the call loads the slot with no bound. The element tier's witness must report the // false proof at the key. class Board { - board: number[] = new Array(64).fill(1); + board: number[] = new Array(116).fill(1); at(sq: number): number { return this.board[sq] ?? 0; } From a0b546ec527ed51eb9db9bd8d465b7ce377cd23e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 13:14:04 +0100 Subject: [PATCH 4/4] S0: R1 fixtures read through the b1 call with a local key (a loop-counter key goes to the index method clone) --- .../verify_facts_s0/leaving-write-negative.ts | 32 +++++++++++-------- scripts/verify_facts_s0/range-sum-negative.ts | 22 +++++++------ 2 files changed, 30 insertions(+), 24 deletions(-) diff --git a/scripts/verify_facts_s0/leaving-write-negative.ts b/scripts/verify_facts_s0/leaving-write-negative.ts index a28ad65fa2f..13cbcf638d6 100644 --- a/scripts/verify_facts_s0/leaving-write-negative.ts +++ b/scripts/verify_facts_s0/leaving-write-negative.ts @@ -1,26 +1,30 @@ // `at` is a field element read, and `board` is born dense with 16 -// elements. In `walk` the counter write `q += 20` is in a branch that falls -// through to the read, so the read's key reaches past the floor (its value -// is the `?? 0`). Under PERRY_FACTS_SABOTAGE=leavingwrite every branch's -// writes are dropped from the reads after it, so the facts claim the key is -// the loop test's `[0, 15]`, in the floor, and the call loads the slot with -// no bound. The element tier's witness must report the false proof at the -// key. +// elements. In `walk` the guard `q < 16` narrows `q`, and the write +// `q += 20` is in a branch that falls through to the read, so the read's key +// reaches past the floor (its value is the `?? 0`). Under +// PERRY_FACTS_SABOTAGE=leavingwrite every branch's writes are dropped from +// the reads after it, so the facts claim the key is the guard's `[3, 15]`, +// in the floor, and the call loads the slot with no bound. The element +// tier's witness must report the false proof at the key. class Board { board: number[] = new Array(16).fill(1); + ep: number = process.argv.length > 100 ? 3 : 5; + far: boolean = process.argv.length < 100; at(sq: number): number { return this.board[sq] ?? 0; } - walk(n: number): number { - let s = 0; - for (let q = 0; q < 16; q++) { - if (q === n) { + walk(): number { + let q = this.ep; + if (q < 16) { + if (this.far) { q += 20; } - s += this.at(q); + return this.at(q); } - return s; + return -1; } } const b = new Board(); -console.log(b.walk(process.argv.length > 100 ? 99 : 5)); +let s = 0; +for (let i = 0; i < 3; i++) s += b.walk() + 1; +console.log(s); diff --git a/scripts/verify_facts_s0/range-sum-negative.ts b/scripts/verify_facts_s0/range-sum-negative.ts index ba87632eeea..709bdd9e652 100644 --- a/scripts/verify_facts_s0/range-sum-negative.ts +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -1,20 +1,22 @@ // `at` is a field element read, and `board` is born dense with 116 -// elements. `sum` reads the keys `r * 16 + f` for `r, f` in `[0, 7]`: the -// sum `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. +// elements. `probe` reads the key `ep + 112` with `ep` in `[3, 5]`: the sum +// `[115, 117]` leaves the floor, and the read past it is the `?? 0`. // Under PERRY_FACTS_SABOTAGE=exactrule a sum's interval is the hull of its -// operands (`r * 16` is `[0, 112]`), so the facts claim the key is in the -// floor and the call loads the slot with no bound. The element tier's witness must report the -// false proof at the key. +// operands (`[3, 112]`), so the facts claim the key is in the floor and the +// call loads the slot with no bound. The element tier's witness must report +// the false proof at the key. class Board { board: number[] = new Array(116).fill(1); + ep: number = process.argv.length > 100 ? 3 : 5; at(sq: number): number { return this.board[sq] ?? 0; } - sum(): number { - let s = 0; - for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); - return s; + probe(): number { + const ep = this.ep; + return this.at(ep) * 10 + this.at(ep + 112); } } const b = new Board(); -console.log(b.sum()); +let s = 0; +for (let i = 0; i < 3; i++) s += b.probe(); +console.log(s);