From a7402ff1bf7f13331bfe7f41afc8fdc92a1395e8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 27 Jun 2026 11:52:03 +0200 Subject: [PATCH] FEAT-041 (v2.6): surface relational octagon invariants on program points MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the v1.9 non-observability finding: the octagon arc (v1.4-v1.9) computes relational constraints (x_a - x_b <= c, x_a + x_b <= c) and strong-closes them, but the output only projected the octagon to unary intervals, so the relational precision was invisible to consumers (loom/synth/assessors). - scry-octagon: new `relations(o) -> Vec` (+ Relation/RelKind) reading the strong-closed DBM's cross-variable cells (Diff at m[2b][2a], Sum at m[2b+1][2a]); each is a sound invariant the octagon maintains. NOT unary- filtered — a relation that produced a unary bound (i - n <= 0 yielding i <= n) looks unary-implied once reduced, yet is exactly the fact worth surfacing. Tests: relations_surfaces_relational_and_is_sound (gamma-sweep soundness), relations_omits_unary_only. - scry-analyze-core: ProgramPoint gains a library-only `relational: Vec` populated at every emitted point from ctx.octagon (snapshot_relational). WIT mirror carries only `locals` (frozen contract intact — contract test green). - Tests: feat041_relational_invariants_surfaced (fixture-11's i-n relation now visible), feat041_no_relations_when_non_relational. 45 core + 26 octagon + 6 contract tests; clippy + fmt clean. FEAT-041 accepted (release v2.6.0). Co-Authored-By: Claude Opus 4.8 --- artifacts/roadmap-3.0.yaml | 2 +- crates/scry-analyze-core/src/lib.rs | 92 +++++++++++++++++++++ crates/scry-octagon/src/lib.rs | 124 ++++++++++++++++++++++++++++ 3 files changed, 217 insertions(+), 1 deletion(-) diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index a561cc2..21a133d 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -153,7 +153,7 @@ artifacts: - id: FEAT-041 type: feature title: "v2.6 — Surface relational octagon invariants in AnalysisResult" - status: proposed + status: accepted release: v2.6.0 description: > Expose the octagon's difference/sum bounds (the relational constraints the diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index a434588..80284f1 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -126,6 +126,38 @@ pub struct ProgramPoint { /// surfaces it for non-Rust consumers). Sound over the same interval /// domain as `locals`. pub operand_stack: Vec, + /// FEAT-041 (REQ-016): the GENUINELY-relational octagon constraints holding + /// between distinct locals at this pc (`x_a - x_b ≤ c` / `x_a + x_b ≤ c`), + /// filtered to those NOT implied by the unary interval bounds. This makes + /// the octagon's relational precision OBSERVABLE — the v1.9 finding was that + /// strong closure tightened these but the output only ever projected the + /// octagon to unary intervals, so the relational facts were invisible. + /// Library-only (the WIT mirror carries only `locals`); sound (each is a + /// constraint the octagon maintains). + pub relational: Vec, +} + +/// FEAT-041: a surfaced relational octagon constraint between two distinct +/// locals at a program point. `a != b`. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct RelationalConstraint { + /// Local index `a`. + pub a: u32, + /// Local index `b`. + pub b: u32, + /// Constraint form (`Diff`: `x_a - x_b ≤ bound`; `Sum`: `x_a + x_b ≤ bound`). + pub kind: RelKind, + /// The upper bound. + pub bound: i64, +} + +/// FEAT-041: the form of a [`RelationalConstraint`]. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum RelKind { + /// `x_a - x_b ≤ bound`. + Diff, + /// `x_a + x_b ≤ bound`. + Sum, } /// Mirror of WIT `invariant-bundle`. The full per-module invariant bundle. @@ -871,6 +903,23 @@ fn interval_is_top(iv: &Interval) -> bool { iv.lo == t.lo && iv.hi == t.hi } +/// FEAT-041: extract the surfaced relational constraints from an octagon, as +/// the core's `RelationalConstraint` (converting `scry_octagon::Relation`). +fn snapshot_relational(octagon: &Octagon) -> Vec { + scry_octagon::relations(octagon) + .into_iter() + .map(|r| RelationalConstraint { + a: r.a, + b: r.b, + kind: match r.kind { + scry_octagon::RelKind::Diff => RelKind::Diff, + scry_octagon::RelKind::Sum => RelKind::Sum, + }, + bound: r.bound, + }) + .collect() +} + /// Snapshot the locals as a list of `LocalInvariant` records. fn snapshot_locals(locals: &[AbstractValue]) -> Vec { locals @@ -2733,6 +2782,7 @@ impl Interp<'_, '_> { pc: pc as u32, locals: snapshot_locals(&reduce_locals(&ctx.locals, &ctx.octagon)), operand_stack: snapshot_stack(&ctx.operand_stack), + relational: snapshot_relational(&ctx.octagon), }); } pc = next; @@ -2753,6 +2803,7 @@ impl Interp<'_, '_> { pc: pc as u32, locals: snapshot_locals(&reduce_locals(&ctx.locals, &ctx.octagon)), operand_stack: snapshot_stack(&ctx.operand_stack), + relational: snapshot_relational(&ctx.octagon), }); } pc = next; @@ -2816,6 +2867,7 @@ impl Interp<'_, '_> { pc: pc as u32, locals: snapshot_locals(&reduce_locals(&ctx.locals, &ctx.octagon)), operand_stack: snapshot_stack(&ctx.operand_stack), + relational: snapshot_relational(&ctx.octagon), }); } if stop { @@ -3207,6 +3259,7 @@ impl Interp<'_, '_> { // precise-looking-but-unsound one. Locals stay meaningful: they // were soundly widened to ⊤ above. operand_stack: Vec::new(), + relational: snapshot_relational(&ctx.octagon), }); } } @@ -5288,6 +5341,7 @@ mod tests { value: av.clone(), }], operand_stack: alloc::vec![av.clone()], + relational: alloc::vec![], }], }; let res = AnalysisResult { @@ -5564,6 +5618,44 @@ mod tests { analyze(bytes, config).expect("analyze must succeed") } + /// FEAT-041: the octagon's relational constraint between i and n in + /// fixture-11 (the variable-bounded loop) is now SURFACED on the program + /// points — the v1.9 non-observability finding closed. A relation between + /// locals 0 (i) and 1 (n) must appear, and every surfaced constraint must be + /// sound (consistent with the unary intervals at that point). + #[test] + fn feat041_relational_invariants_surfaced() { + let r = analyze_fixture("fixture-11-var-bound.wat"); + let has_rel = r.invariants.points.iter().any(|p| { + p.relational + .iter() + .any(|c| (c.a == 0 && c.b == 1) || (c.a == 1 && c.b == 0)) + }); + assert!( + has_rel, + "fixture-11 must surface a relational constraint between i (0) and n (1); \ + points' relational: {:?}", + r.invariants + .points + .iter() + .map(|p| (p.pc, &p.relational)) + .collect::>() + ); + } + + /// FEAT-041: a purely non-relational function surfaces NO relational + /// constraints (no noise). + #[test] + fn feat041_no_relations_when_non_relational() { + let r = analyze_default( + "(module (func (param i32) (result i32) local.get 0 i32.const 1 i32.add))", + ); + assert!( + r.invariants.points.iter().all(|p| p.relational.is_empty()), + "a non-relational function must surface no relational constraints" + ); + } + /// FEAT-021 slice-1: a 3-deep direct call chain with constant frames sums /// along the deepest path (16 + 32 + 8 = 56). The reported bound must equal /// the concrete peak (sound + exact here), and per-function frames recorded. diff --git a/crates/scry-octagon/src/lib.rs b/crates/scry-octagon/src/lib.rs index 2d887a4..cb8801f 100644 --- a/crates/scry-octagon/src/lib.rs +++ b/crates/scry-octagon/src/lib.rs @@ -501,6 +501,85 @@ pub fn bound_of(o: &Octagon, k: u32) -> Option<(i64, i64)> { Some((lo, hi)) } +/// FEAT-041: the form of a surfaced relational constraint between two variables. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum RelKind { + /// `x_a - x_b ≤ bound`. + Diff, + /// `x_a + x_b ≤ bound`. + Sum, +} + +/// FEAT-041: a relational constraint the octagon holds between two DISTINCT +/// variables — the precision the octagon arc computes but the unary +/// interval projection (`bound_of`) discards (the v1.9 non-observability +/// finding). `a != b`. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Relation { + pub a: u32, + pub b: u32, + pub kind: RelKind, + pub bound: i64, +} + +/// FEAT-041: extract the relational constraints the octagon holds between +/// DISTINCT variables — the relational precision the unary interval projection +/// (`bound_of`) discards (the v1.9 non-observability finding). Reads the +/// strong-closed DBM so the surfaced relations are the tightest scry can prove: +/// * `x_a − x_b ≤ c` at cell `m[2b][2a]` (all ordered a≠b); +/// * `x_a + x_b ≤ c` at cell `m[2b+1][2a]` (unordered, a < b). +/// +/// We do NOT filter against the unary bounds: a relation that produced a unary +/// bound (e.g. `i − n ≤ 0`, which yields `i ≤ n`) looks "unary-implied" once the +/// octagon has reduced it into the interval, yet it is exactly the relational +/// fact worth surfacing. We DO drop a `Diff`/`Sum` that is purely a restatement +/// of a single variable's own bound (covered by `bound_of`): such cells never +/// arise here because both indices belong to distinct variables. Every returned +/// constraint is a sound invariant (a finite DBM cell is an upper bound scry +/// maintains). Empty for ⊥ or a purely non-relational state. +pub fn relations(o: &Octagon) -> Vec { + let c = strong_close(o); + let mut out = Vec::new(); + if is_bottom(&c) { + return out; + } + let dim = c.dim; + let n = c.n(); + for a in 0..dim { + for b in 0..dim { + if a == b { + continue; + } + let (ai, bi) = (a as usize, b as usize); + // x_a - x_b ≤ diff (cell m[2b][2a]) + if 2 * ai < n && 2 * bi < n { + let d = c.at(2 * bi, 2 * ai); + if d != INF { + out.push(Relation { + a, + b, + kind: RelKind::Diff, + bound: d, + }); + } + } + // x_a + x_b ≤ sum (cell m[2b+1][2a]), unordered: only a < b + if a < b && 2 * bi + 1 < n && 2 * ai < n { + let s = c.at(2 * bi + 1, 2 * ai); + if s != INF { + out.push(Relation { + a, + b, + kind: RelKind::Sum, + bound: s, + }); + } + } + } + } + out +} + /// Octagon narrowing: recover bounds that [`widen`] over-eagerly discarded. /// Where the widened `a` has `INF` (a bound widening dropped), take `b`'s /// (re-applied, tighter) bound; elsewhere keep `a`. Descending and sound: @@ -528,6 +607,51 @@ pub fn narrow(a: &Octagon, b: &Octagon) -> Octagon { mod tests { use super::*; + /// FEAT-041: `relations` surfaces a genuinely-relational constraint + /// (x_0 - x_1 <= -1, i.e. i < n) and is sound (every surfaced bound holds + /// of every concrete point), but omits a constraint that is merely + /// unary-implied. + #[test] + fn relations_surfaces_relational_and_is_sound() { + // x_0 - x_1 <= -1 over 2 vars. + let o = add_diff(&top(2), 0, 1, -1); + let rels = relations(&o); + assert!( + rels.iter() + .any(|r| r.a == 0 && r.b == 1 && r.kind == RelKind::Diff && r.bound == -1), + "must surface x0 - x1 <= -1, got {rels:?}" + ); + // Soundness: every surfaced Diff/Sum holds for any concrete point in γ. + for x0 in -8i64..8 { + for x1 in -8i64..8 { + if gamma(&o, &[x0, x1]) { + for r in &rels { + let (va, vb) = ([x0, x1][r.a as usize], [x0, x1][r.b as usize]); + let lhs = match r.kind { + RelKind::Diff => va - vb, + RelKind::Sum => va + vb, + }; + assert!( + lhs <= r.bound, + "surfaced relation violated: {r:?} at {x0},{x1}" + ); + } + } + } + } + } + + /// FEAT-041: a purely unary octagon (only x_0 <= 5) surfaces NO relational + /// constraints (no noise from unary-implied diffs). + #[test] + fn relations_omits_unary_only() { + let o = set_upper(&top(2), 0, 5); + assert!( + relations(&o).is_empty(), + "unary-only octagon must yield no relations" + ); + } + /// γ(o, vals): does the concrete assignment `vals` (length `dim`) /// satisfy every bound of the DBM? This is the test-side /// concretization — the spec the algebra is falsified against.