FEAT-069 re-measured post-FEAT-089: unchanged, and the problem is not where it looked - #192
Merged
Merged
Conversation
… where it looked
This artifact's own note said the AC had to be re-measured after the precision
work landed, not before. FEAT-089 has landed, so: the OOB proven rate is
UNCHANGED at 0.67% (55 proven vs 8,162 unproven). FEAT-089 targets div-by-zero
disequalities and does not touch memory bounds. Precondition discharged, answer
is no.
The follow-up measurement is the useful part. Of the 8,162 unproven
out-of-bounds obligations:
7,553 (92.5%) are in a DEGRADED function -- one already carrying a precision
gap (unmodeled-control-flow 1,639, unsupported-op 623, unmodeled-branch
12). 636 of 766 functions with advisories (83%) are degraded.
609 (7.5%) are in a cleanly-modelled function, where scry actually reached
the bounds question and could not prove it.
So the low proven rate is NOT mainly a weakness of the bounds reasoning. The
analyzer GIVES UP on 83% of functions before the bounds question is reached.
Strengthening the bounds domain -- the obvious reading of "0.67% proven" --
could address at most the 7.5%.
A low proven rate looks like a precision problem in the prover. Here it is a
COVERAGE problem upstream of it, and the two call for opposite work.
FEAT-069 stays blocked, but on a DIFFERENT unblocker than previously named: the
lever is modelling if/else regions instead of havocking them (the dominant
single cause at 1,639), not a better interval argument. Re-measure after that,
not after any other precision work.
rivet=0 claim-check=0 fmt=0 drift-gate=0.
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #192 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.
FEAT-069's own note said its AC had to be re-measured after the precision work landed,
not before. FEAT-089 has landed, so this discharges that.
The re-measurement: unchanged
FEAT-089 targets div-by-zero disequalities and doesn't touch memory bounds. Precondition
discharged; the answer is no.
The follow-up is the useful part
Of the 8,162 unproven out-of-bounds obligations:
Degrading causes:
unmodeled-control-flow1,639 ·unsupported-op623 ·unmodeled-branch12. 636 of 766 functions with advisories (83%) are degraded.So the problem is not where "0.67% proven" points
The low rate is not mainly a weakness of the bounds reasoning. The analyzer gives up
on 83% of functions before the bounds question is reached. Strengthening the bounds
domain — the obvious reading of that number — could address at most 7.5% of the gap.
A low proven rate looks like a precision problem in the prover. Here it's a coverage
problem upstream of it, and the two call for opposite work.
What changes
FEAT-069 stays blocked, but on a different unblocker than previously named. The lever
is modelling
if/elseregions instead of havocking them — the dominant single cause at1,639 — not a better interval argument. Re-measure after that, not after any other
precision work.
rivet=0 claim-check=0 fmt=0 drift-gate=0🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc