FEAT-057 measured before building: the surface is real and NOT coverage-gated - #199
Merged
Conversation
…ge-gated FEAT-057 slice 2 (wire polyhedra into the fixpoint) is the only unbuilt work left in v3.3.0/v3.4.0. FEAT-069 taught the rule -- measure the ceiling before building -- so this measures it, on scry's own scry_mcdc.wasm: 851 functions, 23,772 program points. THE OPPORTUNITY IS REAL, which is the opposite of what the same pre-build measurement found for FEAT-069. The octagon already emits ProgramPoint.relational, filtered to constraints NOT implied by the unary intervals; those carry information at 4,749 of 23,772 points (19.98%) across 197 of 851 functions. The octagon is exact for two-variable constraints, so polyhedra can only exceed it where three or more locals are mutually constrained: 2,512 points, 10.57%, in 83 functions. Diff/Sum is 24,321/4,053, so the octagon's non-difference power is in use -- these are not degenerate difference bounds. I EXPECTED TO ADD `depends-on FEAT-095` AND LET THE ORDERING GATE FIRE. The measurement says not to. 2,165 of the 2,512 wide points are in functions that degrade SOMEWHERE, which reads exactly like FEAT-069's 92.5%-in-degraded-functions and is a DIFFERENT claim: gaps are per-pc and write-set havoc widens only the locals a region writes, so a wide point can sit nowhere near a gap. Measured directly, only 13 of 2,512 have a gap at or before them. Manufacturing the dependency to exercise my own gate would have been backwards, so no link was added. BOTH BOUNDS RUN IN THE DIRECTION YOU MIGHT NOT EXPECT, and the residual says so. "3+ mutually constrained locals" is OPPORTUNITY, not realized gain -- it bounds the ceiling from above and shows no point would in fact improve. "No gap at or before it" is an UPPER bound on unaffected points, not a lower one: program order is not dataflow order, and a gap inside a loop reaches earlier pcs through the back edge. A VACUOUS PROXY WAS CAUGHT AND REMOVED rather than reported. Sizing the loop caveat by counting functions where the fixpoint revisited a pc printed "0 functions" -- and the vacuity check built into it reported zero duplicate (func, pc) pairs. ProgramPoint is one per pc, so that proxy could only ever return zero; publishing "0 functions with loops" would have been this repo's dominant failure class. The loop shortfall is left UNQUANTIFIED, which is the honest state. The harness is committed, not run and discarded, for one narrow reason: its numbers are cited on FEAT-057 to justify a scheduling decision, and a bare number in an artifact is the drift hazard that left "the dev REQ-* carry no verifies link by construction" false for months. Re-run it after FEAT-095 lands. Refs: FEAT-057 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
📐 rivet artifact deltaPR: #199 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
I wrote the harness and never ran `cargo fmt`, so PR #199 landed with 12 of 13 checks green and Format red. Only this file is affected; the rest of the tree was already clean. Re-ran the measurement after formatting and diffed it against the pre-format output: byte-identical. Worth doing rather than assuming, because these numbers are cited on FEAT-057 to justify a scheduling decision — "formatting cannot change behaviour" is exactly the kind of thing that is true right up until a macro or a raw string makes it false. Refs: FEAT-057 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
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-057 slice 2 (wire polyhedra into the fixpoint) is the only unbuilt work left in v3.3.0/v3.4.0. FEAT-069 taught the rule — measure the ceiling before building — so this measures it, on scry's own
scry_mcdc.wasm: 851 functions, 23,772 program points.The opportunity is real — the opposite of what FEAT-069 found
The octagon already emits
ProgramPoint.relational, filtered to constraints not implied by the unary intervals. Those carry information at 4,749 of 23,772 points (19.98%) across 197 of 851 functions.The octagon is exact for two-variable constraints, so polyhedra can only exceed it where three or more locals are mutually constrained:
The Sum share means the octagon's non-difference power is genuinely in use — these are not degenerate difference bounds.
I expected to add
depends-on FEAT-095and let the ordering gate fireThe measurement says not to.
2,165 of the 2,512 wide points sit in functions that degrade somewhere — which reads exactly like FEAT-069's "92.5% of unproven obligations in degraded functions" and is a different claim. Gaps are per-pc, and write-set havoc widens only the locals a region writes, so a wide point can sit nowhere near a gap.
Measured directly: only 13 of 2,512 wide points have a gap at or before them.
So FEAT-057 is not coverage-gated, no link was added, and the gate correctly stays green. Manufacturing the dependency to exercise my own gate would have been backwards.
Both bounds run in the direction you might not expect
A vacuous proxy was caught and removed rather than reported
Sizing the loop caveat by counting functions where the fixpoint revisited a pc printed "0 functions" — and the vacuity check built into it reported zero duplicate
(func, pc)pairs.ProgramPointis one per pc, so the proxy could only ever return zero. Publishing "0 functions with loops" would have been this repo's dominant documented failure class.The loop-induced shortfall is left unquantified, which is the honest state. Sizing it needs the operator stream (back edges), which this harness does not have.
Why the harness is committed
Narrow reason: its numbers are cited on FEAT-057 to justify a scheduling decision, and a bare number in an artifact is the drift hazard that left "the dev REQ-* carry no verifies link by construction" checked in and false for months (#198). Re-run it after FEAT-095 lands — the docstring says so.
What this does not establish
The size of the win — only that the surface exists. Slice 2 remains a multi-slice arc mirroring the octagon's v1.7–v1.9: a
PolyonFuncCtxthreaded in lockstep with the octagon, wrap-aware transfers gated on the interval domain's no-wrap result, guard refinement, andPoly::project.Refs: FEAT-057
🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc