diff --git a/changelog.d/wpfacts-range-tightening.md b/changelog.d/wpfacts-range-tightening.md new file mode 100644 index 0000000000..763146a4a1 --- /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 a444310db8..95d0ef7a8e 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 fa3a38cd28..178c506f5b 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 52c00c31ab..0647ba597a 100644 --- a/crates/perry-wpfacts/src/gen/walk.rs +++ b/crates/perry-wpfacts/src/gen/walk.rs @@ -1213,34 +1213,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 { @@ -1254,6 +1264,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); } @@ -1281,6 +1292,7 @@ impl<'a> Gen<'a> { if narrowed { self.narrow_end(); } + self.jumps -= 1; self.loop_depth -= 1; } Stmt::Labeled { body, .. } => self.stmt(fx, body), @@ -1310,6 +1322,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 { @@ -1326,6 +1339,7 @@ impl<'a> Gen<'a> { if let Some(f) = finally { self.stmts(fx, f); } + self.tries -= 1; } Stmt::Switch { discriminant, @@ -1333,6 +1347,7 @@ impl<'a> Gen<'a> { } => { let d = self.expr(fx, discriminant); // `===` against case values: no coercion. + self.jumps += 1; for c in cases { if let Some(t) = &c.test { let tv = self.expr(fx, t); @@ -1341,6 +1356,7 @@ impl<'a> Gen<'a> { } 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 0d28aa1f30..99775ede1f 100644 --- a/crates/perry-wpfacts/src/lib.rs +++ b/crates/perry-wpfacts/src/lib.rs @@ -94,6 +94,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, @@ -497,6 +505,10 @@ fn generate<'a>( g.m.arr_const_sabotage = cfg.sabotage.as_deref() == Some("arrconst"); 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 3fff300ad4..ca0eff6294 100644 --- a/crates/perry-wpfacts/src/model.rs +++ b/crates/perry-wpfacts/src/model.rs @@ -1261,6 +1261,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`): 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`). pub arr_len_sabotage: bool, diff --git a/crates/perry-wpfacts/src/solve.rs b/crates/perry-wpfacts/src/solve.rs index 21c663d593..1ad927841e 100644 --- a/crates/perry-wpfacts/src/solve.rs +++ b/crates/perry-wpfacts/src/solve.rs @@ -1975,3 +1975,36 @@ 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) -> bool { + use crate::model::range::{widen, WIDEN_LIMIT}; + 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 13c89148ed..961ad248d1 100644 --- a/crates/perry-wpfacts/src/solve/apply.rs +++ b/crates/perry-wpfacts/src/solve/apply.rs @@ -1511,6 +1511,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)) @@ -1518,7 +1522,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) + } 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 ddbbb009de..d1f237f7ad 100644 --- a/crates/perry-wpfacts/src/tests.rs +++ b/crates/perry-wpfacts/src/tests.rs @@ -148,6 +148,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 0000000000..5fb773f1f5 --- /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 & 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()", + ) +} + +#[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 6361e64b4f..e16c4dc535 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -78,10 +78,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 a974a95b5e..8bf86dc4b5 100644 --- a/crates/perry/src/commands/compile/compile_env/tests.rs +++ b/crates/perry/src/commands/compile/compile_env/tests.rs @@ -349,6 +349,19 @@ fn const_number_switch_is_a_cache_input() { ); } +/// 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" + ); + } +} + /// N4: the cold-path switch changes helper declarations, call-site /// attributes and branch weights, so `=0` must never reuse an `=1` object. #[test] diff --git a/crates/perry/src/commands/compile/program_facts.rs b/crates/perry/src/commands/compile/program_facts.rs index 7d6ee53c96..be07d4caa1 100644 --- a/crates/perry/src/commands/compile/program_facts.rs +++ b/crates/perry/src/commands/compile/program_facts.rs @@ -155,6 +155,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") @@ -910,6 +918,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 27988003dd..c0d44795a1 100644 --- a/scripts/test-verify-facts-s0.py +++ b/scripts/test-verify-facts-s0.py @@ -121,6 +121,8 @@ def oracle(source, *argv): ("const-array-negative", "arrconst", "constant array"), ("array-field-negative", "arrfield", "array rep"), ("array-b1-negative", "arrb1", "array rep"), + ("range-sum-negative", "exactrule", "array rep"), + ("leaving-write-negative", "leavingwrite", "array rep"), ("array-base-negative", "arrbase", "array rep"), ("array-base-admit-negative", "arrbaseadm", "array rep"), ("number-call-negative", "numbercall", "numeric result"), 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 0000000000..13cbcf638d --- /dev/null +++ b/scripts/verify_facts_s0/leaving-write-negative.ts @@ -0,0 +1,30 @@ +// `at` is a field element read, and `board` is born dense with 16 +// 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(): number { + let q = this.ep; + if (q < 16) { + if (this.far) { + q += 20; + } + return this.at(q); + } + return -1; + } +} +const b = new Board(); +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 new file mode 100644 index 0000000000..709bdd9e65 --- /dev/null +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -0,0 +1,22 @@ +// `at` is a field element read, and `board` is born dense with 116 +// 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 (`[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; + } + probe(): number { + const ep = this.ep; + return this.at(ep) * 10 + this.at(ep + 112); + } +} +const b = new Board(); +let s = 0; +for (let i = 0; i < 3; i++) s += b.probe(); +console.log(s); 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 0000000000..dbbd9bcebe --- /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());