v1.9.0 (FEAT-016 slice-3, AC-011): octagon Miné strong closure

CHANGELOG.md

@@ -7,6 +7,56 @@ Versioning: [SemVer 2.0](https://semver.org/spec/v2.0.0.html).
 
 ## [Unreleased]
 
+## [1.9.0] — 2026-06-14
+
+Headline: **the octagon gains Miné strong (tight) closure — pure algebra,
+no analyzer output change.** This closes the referenced-paper precision item
+AC-011 (FEAT-016 slice-3). Strong closure derives a ±difference bound between
+two variables from their unary bounds (`x ≤ 10 ∧ y ≥ 0 ⟹ x − y ≤ 10`) that
+plain Floyd–Warshall cannot. FEAT-016's acceptance criterion was already met in
+v1.8.0; this is the final precision refinement of the octagon arc.
+
+### Added
+
+- **`scry_octagon::strong_close`** — Floyd–Warshall closure followed by the
+  octagon tightening `m[i][j] := min(m[i][j], ⌊(m[i][ī] + m[j̄][j])/2⌋)` and a
+  re-close. Sound for integers via the floor (`div_euclid`), matching
+  `bound_of`'s projection rounding. `bound_of` now projects through
+  `strong_close`.
+- **Mechanized soundness** (`proofs/rocq/OctagonStrongClose.v`,
+  `strong_close_step_sound`): from `−2·vi ≤ a` and `2·vj ≤ b`, the tightened
+  bound `⌊(a+b)/2⌋` over-approximates `vj − vi` — the step drops no concrete
+  integer point. No admits/axioms; verified by the `rocq-proofs` CI job (and
+  locally with Coq 9.0.1).
+- **3 new γ-sweep tests** in scry-octagon: the precision win
+  (`strong_close_derives_difference_from_unary_bounds`: derives `x_0 − x_1 ≤ 10`
+  from unary where `close` gives INF), concretization-preservation over a grid,
+  and bottom-preservation.
+
+### Not changed (honest scope)
+
+- **The analyzer output is identical to v1.8.0.** Strong closure tightens
+  difference/sum bounds, never a variable's own unary bound, and the analyzer
+  projects the octagon back to **per-variable intervals** (which read unary
+  bounds) — so on the current corpus, where the analyzer generates only
+  difference + unary constraints, strong vs. plain closure is invisible at the
+  output. All fixture invariants (08–11) are byte-identical. `SCRY_VERSION` →
+  1.9.0 is a release stamp. The precision becomes observable only when a
+  consumer reads the relational (off-diagonal) bounds or the analyzer generates
+  sum constraints — future work, not claimed here.
+
+### Falsification statement
+
+What v1.9 claims, made falsifiable: **strong closure is sound (drops no
+concrete point) and strictly more precise than Floyd–Warshall on a constraint
+system where a difference is implied only by unary bounds.** Falsifier: the
+γ-sweep test asserts `strong_close` and the base system admit exactly the same
+concrete points (soundness), and `strong_close_derives_difference_from_unary_bounds`
+asserts it derives `x_0 − x_1 ≤ 10` where `close` leaves INF (precision); the
+Rocq `strong_close_step_sound` independently proves the tightening step. What
+v1.9 does **not** claim: any change to the analyzer's interval output (see
+above), nor the full integer tight closure's extra unary even-ification.
+
 ## [1.8.0] — 2026-06-13
 
 Headline: **the octagon relational product is wired into the analyzer — a loop

artifacts/roadmap-2.0.yaml

@@ -751,6 +751,24 @@ artifacts:
       post-fixpoint (instantiated at the octagon transfer) + host oracle over
       all fixtures. REMAINING (precision only, NOT the AC): slice-3 Miné
       strong/tight closure (referenced-paper AC-011).
+
+      EVIDENCE (v1.9.0 — slice-3 per DD-015, AC-011): Miné STRONG closure landed
+      in scry-octagon (strong_close: Floyd-Warshall + the m[i][j] :=
+      min(m[i][j], floor((m[i][ī]+m[j̄][j])/2)) tightening + re-close), deriving
+      a difference bound from two unary bounds (x≤10 ∧ y≥0 ⟹ x-y≤10) that plain
+      close cannot. Sound (γ-sweep concretization-preservation) + strictly more
+      precise (γ-sweep precision test) + mechanized: proofs/rocq/
+      OctagonStrongClose.v strong_close_step_sound (the tightening drops no
+      concrete integer point, admit-free). bound_of projects through
+      strong_close. HONEST SCOPE: NO analyzer output change — strong closure
+      tightens difference/sum bounds, never a variable's own unary bound, and
+      the analyzer projects octagon→per-variable intervals (unary), so on the
+      current difference+unary corpus strong vs plain closure is invisible at
+      the output (fixtures 08-11 byte-identical). The precision becomes
+      observable only when a consumer reads relational bounds or the analyzer
+      generates sum constraints (future work). With slice-3 landed, the octagon
+      arc (slices 1/2a/2b-i/2b-ii/3) is complete; FEAT-016 implemented (could go
+      verified on an assessor/qualification pass).
     tags: [capability, relational, octagon, precision, v1.4]
     fields:
       phase: phase-2

crates/scry-analyze-core/src/lib.rs

@@ -300,7 +300,7 @@ mod domain {
         scry_taint::join(a, b)
     }
 }
-const SCRY_VERSION: &str = "1.8.0";
+const SCRY_VERSION: &str = "1.9.0";
 const INVARIANT_SCHEMA_URL: &str = "https://pulseengine.eu/scry-invariants/v1";
 
 /// Default Wasm linear-memory page size (64 KiB).

crates/scry-octagon/src/lib.rs

@@ -171,6 +171,51 @@ pub fn close(o: &Octagon) -> Octagon {
     r
 }
 
+/// Miné **strong** closure (FEAT-016 slice-3, AC-011). After the standard
+/// Floyd–Warshall [`close`], apply the octagon tightening
+///
+/// ```text
+///   m[i][j] := min( m[i][j], ⌊ (m[i][ī] + m[j̄][j]) / 2 ⌋ )      ī = i^1
+/// ```
+///
+/// then re-close to propagate the new bounds. This derives a ±difference/sum
+/// bound between two variables from their UNARY bounds — e.g. from `x ≤ 10`
+/// and `y ≥ 0` it derives `x − y ≤ 10`, which plain Floyd–Warshall (no edge
+/// between `x` and `y`) cannot. Sound for integers: `v(ī) − v(i) = −2·v(i) ≤
+/// m[i][ī]` and `v(j) − v(j̄) = 2·v(j) ≤ m[j̄][j]`, so `2·(v(j) − v(i)) ≤
+/// m[i][ī] + m[j̄][j]`, hence `v(j) − v(i) ≤ ⌊·/2⌋` (the integer floor only
+/// tightens, never drops a concrete point). The `/2` floor is via
+/// `div_euclid`, matching [`bound_of`]'s projection rounding.
+///
+/// Scope note: the tightening lands on DIFFERENCE/SUM entries, never on a
+/// variable's own unary bound (`m[2k+1][2k]`, the source of the derivation),
+/// so projecting a closed octagon back to per-variable intervals via
+/// [`bound_of`] sees no change from strong vs. plain closure. The precision is
+/// realised by consumers that read the relational (off-diagonal) bounds.
+pub fn strong_close(o: &Octagon) -> Octagon {
+    let c = close(o);
+    if is_bottom(&c) {
+        return c;
+    }
+    let n = c.n();
+    let mut r = c.clone();
+    for i in 0..n {
+        let a = c.at(i, i ^ 1); // bounds −2·v(i)
+        for j in 0..n {
+            let b = c.at(j ^ 1, j); // bounds 2·v(j)
+            let t = sadd(a, b);
+            if t != INF {
+                let cand = t.div_euclid(2); // ⌊(a+b)/2⌋ — sound integer floor
+                if cand < r.at(i, j) {
+                    r.set(i, j, cand);
+                }
+            }
+        }
+    }
+    // Propagate the tightened relational bounds.
+    close(&r)
+}
+
 /// `a ⊑ b` — the octagon partial order, i.e. `γ(a) ⊆ γ(b)`. Computed by
 /// closing `a` (so all implied bounds are explicit) and checking it is
 /// pointwise at least as tight as `b`. A bottom `a` is `⊑` everything.
@@ -426,7 +471,11 @@ pub fn assign_add_const(o: &Octagon, k: u32, src: u32, c: i64) -> Octagon {
 /// iff the octagon is infeasible (⊥ — no concrete point, i.e. unreachable).
 /// Sound: the returned interval over-approximates `{ x_k : point ∈ γ(o) }`.
 pub fn bound_of(o: &Octagon, k: u32) -> Option<(i64, i64)> {
-    let c = close(o);
+    // Project through the STRONG closure (FEAT-016 slice-3): for the current
+    // analyzer this matches plain `close` on unary bounds, but it keeps the
+    // projection correct for any relational constraints a richer
+    // constraint-generation would add (sum/difference tightening).
+    let c = strong_close(o);
     if is_bottom(&c) {
         return None;
     }
@@ -856,6 +905,65 @@ mod tests {
         assert_eq!(bound_of(&o, 0), None);
     }
 
+    /// Strong closure PRECISION: from the unary bounds `x_0 ≤ 10` and
+    /// `x_1 ≥ 0` it derives the difference bound `x_0 − x_1 ≤ 10`, which plain
+    /// Floyd–Warshall cannot (there is no edge between `x_0` and `x_1`). This
+    /// is the AC-011 win that distinguishes strong closure from `close`.
+    #[test]
+    fn strong_close_derives_difference_from_unary_bounds() {
+        let o = top(2);
+        let o = set_upper(&o, 0, 10); // x_0 ≤ 10
+        let o = set_lower(&o, 1, 0); // x_1 ≥ 0
+        // x_0 − x_1 = v(0) − v(2) ≤ c  ⇒  cell m[2][0].
+        let n = o.n();
+        let cell = 2 * n; // m[2][0]
+        assert_eq!(
+            close(&o).m[cell],
+            INF,
+            "plain Floyd–Warshall cannot relate independent x_0, x_1"
+        );
+        assert_eq!(
+            strong_close(&o).m[cell],
+            10,
+            "strong closure must derive x_0 − x_1 ≤ 10 from x_0 ≤ 10 ∧ x_1 ≥ 0"
+        );
+    }
+
+    /// Strong closure is SOUND: like `close`, it only makes implied bounds
+    /// explicit — it never adds or drops a concrete point. Swept over a grid
+    /// of constraint systems (a difference + two unary bounds).
+    #[test]
+    fn strong_close_preserves_concretization() {
+        let base = {
+            let o = top(2);
+            let o = add_diff(&o, 0, 1, 4); // x_0 − x_1 ≤ 4
+            let o = set_lower(&o, 0, -3);
+            let o = set_upper(&o, 0, 8);
+            let o = set_lower(&o, 1, -2);
+            set_upper(&o, 1, 6)
+        };
+        let s = strong_close(&base);
+        for a in -6..=11 {
+            for b in -5..=9 {
+                assert_eq!(
+                    gamma(&base, &[a, b]),
+                    gamma(&s, &[a, b]),
+                    "strong closure changed γ at ({a},{b})"
+                );
+            }
+        }
+    }
+
+    /// Strong closure of an infeasible system stays ⊥ (it detects the
+    /// contradiction via the underlying `close`).
+    #[test]
+    fn strong_close_keeps_bottom() {
+        let o = top(1);
+        let o = set_lower(&o, 0, 5);
+        let o = set_upper(&o, 0, 2); // 5 ≤ x_0 ≤ 2 : infeasible
+        assert!(is_bottom(&strong_close(&o)));
+    }
+
     /// `narrow` recovers an `INF` bound (that widening discarded) from the
     /// re-applied candidate, while keeping already-finite bounds.
     #[test]

proofs/rocq/BUILD.bazel

@@ -149,3 +149,19 @@ rocq_proof_test(
     deps = [":octagonproject"],
     tags = ["rocq", "verification", "feat-016"],
 )
+
+# FEAT-016 slice-3 (v1.9): mechanized soundness of the Miné STRONG-closure
+# tightening step — deriving a difference bound `⌊(m[i][ī] + m[j̄][j])/2⌋` from
+# two unary bounds never excludes a concrete integer point (AC-011). No admits,
+# no axioms (DD-015).
+rocq_library(
+    name = "octagonstrongclose",
+    srcs = ["OctagonStrongClose.v"],
+    tags = ["rocq", "verification", "feat-016"],
+)
+
+rocq_proof_test(
+    name = "octagonstrongclose_test",
+    deps = [":octagonstrongclose"],
+    tags = ["rocq", "verification", "feat-016"],
+)

proofs/rocq/OctagonStrongClose.v

@@ -0,0 +1,62 @@
+(** * FEAT-016 slice-3 — Soundness of the octagon strong-closure step (Rocq).
+
+    v1.9 adds Miné's STRONG closure to `crates/scry-octagon` (AC-011): after the
+    Floyd–Warshall closure it tightens each DBM entry with
+
+        m[i][j] := min( m[i][j], ⌊ (m[i][ī] + m[j̄][j]) / 2 ⌋ )
+
+    deriving a ±difference bound between two variables from their UNARY bounds
+    (e.g. `x ≤ 10 ∧ y ≥ 0 ⟹ x − y ≤ 10`), which plain Floyd–Warshall — having no
+    edge between `x` and `y` — cannot. The lattice laws and the closure's
+    concretization-preservation are falsified by the γ-sweep tests in that crate
+    (its established evidence kind). This file mechanizes the one NEW arithmetic
+    obligation the step introduces: that the tightened bound is SOUND — it never
+    excludes a concrete integer point.
+
+    The encoding (Miné): variable `x_k` has a positive form (`v = x_k`) and a
+    negative form (`v = −x_k`). The cell `m[i][ī]` (ī flips the form) bounds
+    `v(ī) − v(i) = −2·v(i)`, and `m[j̄][j]` bounds `v(j) − v(j̄) = 2·v(j)`. So
+    with `a := m[i][ī]` and `b := m[j̄][j]`, the new bound on `v(j) − v(i)` is
+    `⌊(a + b)/2⌋`, and soundness is exactly that every integer `v(j) − v(i)`
+    consistent with the two unary bounds respects it. `⌊·/2⌋` is `Z.div _ 2`
+    (floor), matching the Rust `i64::div_euclid(2)`. No admits, no axioms (the
+    proof-in-slice gate, DD-015).
+
+    Build:  bazel build //proofs/rocq:octagonstrongclose
+    Test:   bazel test  //proofs/rocq:octagonstrongclose_test
+*)
+
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Lia.
+
+Open Scope Z_scope.
+
+(** * The strong-closure tightening is sound.
+
+    Let `vi`, `vj` be the concrete values of two octagon variable forms, and
+    `a`, `b` the unary bounds the DBM holds: `−2·vi ≤ a` (from `m[i][ī]`) and
+    `2·vj ≤ b` (from `m[j̄][j]`). Then the tightened difference bound
+    `⌊(a + b)/2⌋` over-approximates `vj − vi` — it is never violated by a
+    concrete point. Hence replacing `m[i][j]` with `min(m[i][j], ⌊(a+b)/2⌋)`
+    drops no concrete point: the strong closure is sound. *)
+Theorem strong_close_step_sound : forall vi vj a b : Z,
+  -2 * vi <= a -> 2 * vj <= b -> vj - vi <= (a + b) / 2.
+Proof.
+  intros vi vj a b Hi Hj.
+  (* 2·(vj − vi) ≤ a + b, then halve with the floor-division facts. *)
+  pose proof (Z.div_mod (a + b) 2 ltac:(lia)) as HM.
+  pose proof (Z.mod_pos_bound (a + b) 2 ltac:(lia)) as HB.
+  lia.
+Qed.
+
+(** The floor is the TIGHTEST sound integer bound the halving admits:
+    `2·⌊(a+b)/2⌋ ≤ a + b`, so rounding down keeps the bound attainable rather
+    than over-tightening past an integer the constraints permit. *)
+Theorem strong_close_floor_tight : forall a b : Z,
+  2 * ((a + b) / 2) <= a + b.
+Proof.
+  intros a b.
+  pose proof (Z.div_mod (a + b) 2 ltac:(lia)) as HM.
+  pose proof (Z.mod_pos_bound (a + b) 2 ltac:(lia)) as HB.
+  lia.
+Qed.