FEAT-095: file the dominant precision limit, which nothing tracked - #193
Merged
Conversation
Modelling if/else regions instead of havocking them is upstream of most of what scry cannot prove, and it had NO artifact and NO issue. Grepping every artifact title and every open issue returned two false positives and the consumer request (#114) -- nothing named the gap itself. MEASURED on scry_mcdc.wasm. Of 8,162 unproven out-of-bounds obligations, 7,553 (92.5%) are in a function already carrying a precision gap -- unmodeled-control- flow 1,639, unsupported-op 623, unmodeled-branch 12 -- and only 609 (7.5%) are in a cleanly-modelled function where scry reached the bounds question and failed. 636 of 766 functions with advisories (83%) are degraded. So the headline number points the wrong way. "0.67% proven" reads as a weak bounds domain and invites work there, which could address at most the 7.5%. It is a COVERAGE problem upstream of the prover, not a precision problem inside it. `havoc_region` is HONEST -- it records GapKind::UnmodeledControlFlow rather than silently going top (REQ-017), which is the only reason this was measurable. It is also the single biggest thing between scry and a useful proven rate. AC3 is the one that matters: joining two arms that assign different values to one local must OVER-APPROXIMATE. A join that picks a branch is a false proof -- the FEAT-089 failure mode one level up, and this feature makes scry emit PROVEN-SAFE where it currently does not. ALSO MADE AN EXISTING INVERSION MACHINE-VISIBLE. I wrote that v3.3.0 now has two ordering inversions, then ran the check and it reported ONE. FEAT-064's dependency on FEAT-077/FEAT-087 was recorded in PROSE (inside an AC), so no tool could see it -- the #187 finding was unenforceable by construction. Both are now typed `depends-on` links, and the check reports: FEAT-064 (v3.3.0) depends-on FEAT-077 (v3.4.0) FEAT-064 (v3.3.0) depends-on FEAT-087 (v3.4.0) FEAT-069 (v3.3.0) depends-on FEAT-095 (v3.5.0) Two of v3.3.0's three remaining items are blocked on later releases. That strengthens #187's recommendation rather than adding a new problem: the release, as scoped, cannot be cut in sequence. 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: #193 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.
Modelling
if/elseregions instead of havocking them is upstream of most of what scrycannot prove — and it had no artifact and no issue. Grepping every artifact title and
every open issue returned two false positives and the consumer request (#114). Nothing
named the gap itself.
Measured on scry_mcdc.wasm
Of 8,162 unproven out-of-bounds obligations:
Causes:
unmodeled-control-flow1,639 ·unsupported-op623 ·unmodeled-branch12.636 of 766 functions with advisories (83%) are degraded.
The headline number points the wrong way
"0.67% proven" reads as a weak bounds domain and invites work there — which could
address at most 7.5%. The analyzer gives up on 83% of functions before the bounds
question is reached. It's a coverage problem upstream of the prover, not a precision
problem inside it.
havoc_regionis honest — it recordsGapKind::UnmodeledControlFlowrather thansilently going ⊤ (REQ-017), which is the only reason this was measurable at all. It's also
the single biggest thing between scry and a useful proven rate.
AC3 is the one that matters: joining two arms that assign different values to one local
must over-approximate. A join that picks a branch is a false proof — FEAT-089's failure
mode one level up, and this feature makes scry emit PROVEN-SAFE where it currently doesn't.
And it made an existing finding enforceable
I wrote that v3.3.0 now had two ordering inversions, ran the check, and it reported one.
FEAT-064's dependency on FEAT-077/087 was recorded in prose inside an AC — so no tool
could see it. #187's finding was unenforceable by construction.
Both are now typed
depends-onlinks, and the check reports:Two of v3.3.0's three remaining items are blocked on later releases. That strengthens
#187's recommendation rather than adding a new problem.
rivet=0 claim-check=0 fmt=0 drift-gate=0🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc