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

[avrabe]

Summary

Closes the referenced-paper precision item AC-011 (FEAT-016 slice-3) — the final refinement of the octagon arc. Pure algebra; no analyzer output change (FEAT-016's acceptance criterion was already met and released in v1.8.0).

Miné strong (tight) closure derives a ±difference bound between two variables from their unary bounds — x ≤ 10 ∧ y ≥ 0 ⟹ x − y ≤ 10 — which plain Floyd–Warshall (no edge between x and y) cannot.

What changed — crates/scry-octagon

• strong_close — Floyd–Warshall close, then the tightening m[i][j] := min(m[i][j], ⌊(m[i][ī] + m[j̄][j])/2⌋), then a re-close. Sound for integers via the floor (div_euclid). bound_of now projects through it.
• 3 γ-sweep tests: the precision win (strong_close_derives_difference_from_unary_bounds — derives x_0 − x_1 ≤ 10 where close leaves INF), concretization-preservation over a grid, and bottom-preservation.

Evidence

• Rocq 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 — drops no concrete integer point. Admit-free; verified locally (Coq 9.0.1) + wired into the rocq-proofs CI job.

Honest scope — no analyzer output change

The analyzer output is byte-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 (difference + unary constraints only) strong vs. plain closure is invisible at the output (fixtures 08–11 unchanged). The precision becomes observable only when a consumer reads relational bounds or the analyzer generates sum constraints (future work). SCRY_VERSION → 1.9.0 is a release stamp.

Falsification statement

Strong closure is sound (drops no concrete point) and strictly more precise than Floyd–Warshall when a difference is implied only by unary bounds. Falsifier: the γ-sweep test asserts identical concrete-point sets (soundness) and strong_close_derives_difference_from_unary_bounds asserts the x_0 − x_1 ≤ 10 derivation (precision); the Rocq theorem proves the step. Does not claim any analyzer interval-output change, nor the full integer tight closure's unary even-ification.

Scope

FEAT-016 stays implemented; the octagon arc (slices 1 / 2a / 2b-i / 2b-ii / 3) is now complete.

🤖 Generated with Claude Code

[github-actions]

📐 rivet artifact delta

PR: #44 Base SHA: 0bf1bcbf

Validation

head — `rivet validate` result

warning: rivet doc scanner skipping ./docs/roadmap.md: no YAML frontmatter
  hint: if this is intentional, add the path to docs[].exclude in rivet.yaml
rivet docs: 8 loaded, 1 skipped (warnings above), 0 excluded by allowlist
Loaded 8 documents with 123 artifact references

Diagnostics:
  INFO: [G-003] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
 — needs an incoming `supported-by` link from one of [safety-solution]
  INFO: [G-004] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
 — needs an incoming `supported-by` link from one of [safety-solution]
  INFO: [G-005] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
 — needs an incoming `supported-by` link from one of [safety-solution]
  INFO: [G-003] Top-level safety goals should have context defining scope and assumptions — needs an incoming `scoped-by` link from one of [safety-context]
  INFO: [G-004] Top-level safety goals should have context defining scope and assumptions — needs an incoming `scoped-by` link from one of [safety-context]
  INFO: [G-005] Top-level safety goals should have context defining scope and assumptions — needs an incoming `scoped-by` link from one of [safety-context]

Result: PASS (0 warnings)
Schemas: common@0.1.0 (embedded), dev@0.1.0 (embedded), research@0.1.0 (embedded), research-ext@0.1.0 (on-disk), safety-case@0.1.0 (embedded)

base — `rivet validate` result (for comparison)

warning: rivet doc scanner skipping ./docs/roadmap.md: no YAML frontmatter
  hint: if this is intentional, add the path to docs[].exclude in rivet.yaml
rivet docs: 8 loaded, 1 skipped (warnings above), 0 excluded by allowlist
Loaded 8 documents with 123 artifact references

Diagnostics:
  INFO: [G-003] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
 — needs an incoming `supported-by` link from one of [safety-solution]
  INFO: [G-004] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
 — needs an incoming `supported-by` link from one of [safety-solution]
  INFO: [G-005] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
 — needs an incoming `supported-by` link from one of [safety-solution]
  INFO: [G-003] Top-level safety goals should have context defining scope and assumptions — needs an incoming `scoped-by` link from one of [safety-context]
  INFO: [G-004] Top-level safety goals should have context defining scope and assumptions — needs an incoming `scoped-by` link from one of [safety-context]
  INFO: [G-005] Top-level safety goals should have context defining scope and assumptions — needs an incoming `scoped-by` link from one of [safety-context]

Result: PASS (0 warnings)
Schemas: common@0.1.0 (embedded), dev@0.1.0 (embedded), research@0.1.0 (embedded), research-ext@0.1.0 (on-disk), safety-case@0.1.0 (embedded)

Artifact stats

	base	head
Total artifacts	89	89

full stats — head

Artifact summary:
  academic-reference               11
  design-decision                  15
  feature                          20
  market-finding                    5
  requirement                      10
  safety-context                    3
  safety-goal                       5
  safety-justification              3
  safety-solution                   6
  safety-strategy                   1
  technology-evaluation            10
  TOTAL                            89

Diagnostics: 0 error(s), 0 warning(s), 6 info(s)

Diff (base → head)

~ FEAT-016
  description: changed

0 added, 0 removed, 1 modified, 88 unchanged

AADL model — head

spar/scry.aadl: OK

---

Posted by the rivet-delta workflow. Informational only — does not gate the PR.