FEAT-042 (v2.6): widening with thresholds#78
Merged
Conversation
Replace the loop-header's jump-to-±∞ widening with widening to syntactic thresholds: when a bound would go to ±∞, snap it to the nearest enclosing constant from the function's operands instead. Recovers loop bounds plain widening over-approximates to ⊤, while staying a sound, terminating widening. - scry-interval: widen_with_thresholds(a, b, &[i64]) — snaps the growing bound to the least threshold ≥ b.hi (or greatest ≤ b.lo), ±∞ fallback. Sound (result ⊒ a and ⊒ b); terminating (finite threshold ladder + ∞). Unit test widen_with_thresholds_snaps_and_terminates (soundness + ascending + reaches ∞). - scry-analyze-core: Interp carries per-function widen_thresholds (collect_widen_thresholds = the i32/i64 const operands + 0); the loop fixpoint widening uses widen_with_thresholds. Honest framing: NEUTRAL on the current fixture corpus (guard refinement + narrowing already bound those constant-guarded loops — all 45 core tests pass unchanged), but adds a sound precision lever for loops the guard-refine idiom does not catch. clippy + fmt clean. FEAT-042 accepted (release v2.6.0). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #78 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.
Third feature of v2.6.0. A sound precision lever for loops.
What
scry-interval::widen_with_thresholds(a, b, &[i64])— when a bound would jump to ±∞, snap it to the nearest enclosing syntactic threshold instead (least threshold ≥b.hi; greatest ≤b.lo; ±∞ fallback). Sound (result ⊒ both inputs), terminating (finite threshold ladder).Interpcarries per-functionwiden_thresholds(the function'si32/i64const operands + 0); the loop-header fixpoint widening uses it.Honesty
Neutral on the current fixture corpus — guard refinement + narrowing already bound the constant-guarded loops (all 45 core tests pass unchanged). This adds a sound lever for loops the guard-refine idiom doesn't catch. The mechanism's soundness + termination is unit-tested (
widen_with_thresholds_snaps_and_terminates).Traces REQ-001.
release: v2.6.0. clippy + fmt clean.🤖 Generated with Claude Code