v1.8.0 (FEAT-016 slice-2b-ii): octagon relational product wired into the analyzer

[avrabe]

Summary

The octagon relational domain is now carried through the structured-CFG interpreter, so a loop counter bounded by a variable relation (i < n, n not constant) stays bounded — where the interval domain + v1.6 constant-guard refinement alone widen it to ⊤. This moves the FEAT-016 acceptance criterion (a relational constraint between two locals preserved across loop iterations without false widening), so FEAT-016 → implemented.

Builds on the v1.7 octagon primitives (#42).

What changed — crates/scry-analyze-core

• FuncCtx.octagon (dim = local count), joined / widened / narrowed in lockstep with the interval locals at every merge point — block exit, the loop entry ⊔ back-edges join, the widening threshold, and the narrowing phase. Octagon widening drops the slowly-growing i − n bound to ⊤ exactly as interval widening drops a counter, so narrowing (v1.7's narrow) is what re-derives it. The branch break-state carries the octagon too.
• try_guard_brif_rel — local.get A; local.get B; <signed cmp>; br_if D adds the octagon difference constraint A − B ≤ c on each edge (the variable-relation case the constant peephole can't reach).
• octagon_transfer / classify_store — a local.set/local.tee is classified by look-behind into x := c / x := y / x := y ± c (the in-place increment uses v1.7's shift). Safety net: any write the transfer does not model forgets that variable's relations — never retain a stale one. br_table/unsupported → octagon reset to ⊤.
• reduce_locals / inject_intervals — reduced product at emission: inject interval bounds into the octagon, close, project back, meet (i ≤ n ∧ n ≤ 10 ⟹ i ≤ 10; no WIT change). The loop entry octagon is seeded with the entry interval bounds so the relation survives the first join. A top octagon projects to the identity, so all prior interval-only behaviour is preserved exactly.

Evidence

• fixture-11-var-bound (counter bounded by i < n, n in a local) + native oracle feat016_octagon_var_bounds_counter: i converges to [0,10] (hi ≤ 10), where interval + constant-guard alone give ⊤.
• Fixture added to the live scry-mcdc corpus; MC/DC proved 164 → 180 (mac local; CI/linux is the gate), floor held at 155 (monotone).
• Soundness composes proven/falsified pieces applied at the established merge points: v1.7 γ-sweep-falsified octagon transfers; OctagonProject.v projection rounding (proj_interval_sound); LoopFixpoint.v post-fixpoint soundness (loop_postfixpoint_sound) instantiated at the octagon transfer; injecting true interval bounds only tightens. The integration gate is the host soundness oracle over the whole fixture corpus (abstract ⊒ concrete) + the forget-on-unmodelled-write net.

Falsification statement

A loop counter bounded by a variable relation i < n converges to a finite interval, soundly. Falsifier: fixture-11-var-bound counts i up while i < n with n = 10 in a local; if the analyzer reports i as ⊤ after the loop, or if the concrete 10 falls outside i's interval, the claim is false. Does not claim Miné strong/tight closure (AC-011, the remaining slice-3) or relations beyond a single guarded-counter difference.

Scope

FEAT-016 → implemented (AC met). Slice-3 (Miné strong closure) remains as a precision-only follow-up.

🤖 Generated with Claude Code

[github-actions]

📐 rivet artifact delta

PR: #43 Base SHA: 47344cd8

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
  status: - proposed -> + implemented

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.