FEAT-041 (v2.6): surface relational octagon invariants

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

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<AbstractValue>,
+    /// 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<RelationalConstraint>,
+}
+
+/// 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<RelationalConstraint> {
+    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<LocalInvariant> {
     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::<alloc::vec::Vec<_>>()
+        );
+    }
+
+    /// 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.

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<Relation> {
+    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.