FEAT-041 (v2.6): surface relational octagon invariants#77
Merged
Conversation
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>` (+ 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<RelationalConstraint>` 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 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #77 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Second feature of v2.6.0. Closes the v1.9 non-observability finding — the octagon's relational precision is now visible in the output.
What
relations(o) -> Vec<Relation>extracts the cross-variable constraints (x_a − x_b ≤ c,x_a + x_b ≤ c) from the strong-closed DBM. γ-sweep test proves every surfaced relation is sound.ProgramPoint.relational: Vec<RelationalConstraint>(library-only) populated at each emitted point. fixture-11'si − nloop-invariant relation is now observable where before only the unary projection (i ≤ 10) showed.Deliberately not unary-filtered: a relation that produced a unary bound (
i − n ≤ 0⇒i ≤ n) looks unary-implied once the octagon reduces it, yet it's exactly the relational fact to surface (that subtlety was a clean-room finding mid-implementation).Soundness / posture
Library-only — WIT mirror carries only
locals; frozen v1 JSON contract unchanged (contract test green). Each surfaced constraint is a sound invariant the octagon maintains. 45 core + 26 octagon + 6 contract tests; clippy + fmt clean.Traces REQ-016.
release: v2.6.0.🤖 Generated with Claude Code