From 358c1b2ef5507c3bebf1c24a61fa3d9908edc7d6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 03:24:07 +0200 Subject: [PATCH] FEAT-069 re-measured post-FEAT-089: unchanged, and the problem is not 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 --- artifacts/roadmap-3.0.yaml | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 9c6e54f..d298764 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -1330,6 +1330,30 @@ artifacts: correct and nearly empty file. Precision work (FEAT-089 and the region-havoc family) should land first, and this AC should be re-measured after it, not before. + + RE-MEASURED 2026-08-28, POST-FEAT-089 — which this artifact's own note + said had to happen before the AC was judged. Result: 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, so the + precision work that landed does not help this feature. The precondition + is discharged; the answer is no. + AND THE FOLLOW-UP MEASUREMENT REFRAMES THE PROBLEM. 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. + It is that 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%. + CONSEQUENCE FOR THIS FEATURE: FEAT-069 stays blocked, but on a DIFFERENT + unblocker than the one previously named. The lever is modelling `if`/ + `else` regions instead of havocking them (the dominant single cause at + 1,639), not a better interval/bounds argument. Re-measure again after + that, not after any other precision work. tags: [bounds-elision, synth, interop, embedded, v3.3] fields: phase: phase-3