FEAT-057 slice 2a: polyhedra wired into the fixpoint, wrap-gated — and measurably inert for the target class - #201
Merged
Conversation
Poly rides FuncCtx in LOCKSTEP with the octagon and the segmentation
(mirrored site-for-site): joined at every merge (block exit, break-state
record), widened at every loop header, reset on degrade, and PROJECTED
(new Poly::project, Fourier-Motzkin elimination) on every write the
transfer does not model — havoc'd write-sets included.
THE WRAP GATE: over Wasm's wrapping i32, an assignment equality
(z = x + y) is added ONLY when the interval domain proves no-wrap
(scry_interval::i32_add / i32_sub return TOP exactly when wrap is
possible); otherwise the assigned variable is projected. Never an
unguarded equality. Two-local signed guards refine the poly on both
edges, mirroring refine_octagon_rel.
Output: NEW additive ProgramPoint.linear (constraints over >=2 locals);
RelationalConstraint / snapshot_relational untouched (FEAT-041 contract).
Poly::project bails (coefficient overflow, pos*neg cap) all DROP
constraints — the sound direction for a projection; each direction is
stated in comments. Gamma-swept, plus a transitive-consequence
precision test so a lazy drop-everything implementation cannot pass.
Oracles (every one observed RED under a targeted mutant):
- 3-var relation z = x + y the octagon provably cannot express:
linear output must ENTAIL it AND exclude the witness (100,100,0),
which satisfies every octagon relational + interval fact at that pc.
- wrap fixture (i32::MAX + 1): concrete-run gamma-check at every pc;
no-wrap twin (5 + 7) pins the gate's other side (not inert).
- merge-join, loop-back-edge, and guard-direction gamma-checks with
per-path concrete valuations.
Mutants killed: forced equality (M1), dropped merge join (M2), dropped
back-edge join (M3), swapped guard edges (M4), no-project-on-write
(M5), project-keeps-eliminated-variable (P1).
MEASURED REALIZATION on scry_mcdc.wasm (poly_surface extended, 25,144
points): 2,020 points (8.03%) carry linear facts — all 2-variable; the
>=3-local count is ZERO. Instrumented why: 94 z := x + y sites reach
the transfer, 0 with provable no-wrap (operands interval-TOP; LLVM
bounds checks are unsigned compares guard_op soundly refuses). Wired
and sound, but INERT for the octagon-beating class on this corpus;
cost within run noise. AC#3 stays OPEN (slice 3) — FEAT-057 remains
`proposed`; residual updated with the numbers and the levers.
Refs: FEAT-057
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
📐 rivet artifact deltaPR: #201 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
…ice 2a inert (#202) FEAT-057 slice 2a (#201) shipped polyhedra into the fixpoint and MEASURED ITSELF INERT for the class it exists to serve: 5,138 linear constraints across 130 functions on scry_mcdc.wasm, and ZERO involving three or more locals -- nothing the octagon could not already express. Instrumented, not guessed: of 94 `z := x + y` sites reaching the transfer, ZERO have a provable no-wrap, because the operands are ⊤. The operands are ⊤ because the guard that would bound them is declined. `guard_op` maps only SIGNED comparisons; every `*U` variant returns `None`, and the code says why -- unsigned comparisons wrap, so refining with a signed constant is not sound. That refusal is CORRECT. It is also the most consequential precision decision in the analyzer, because LLVM emits array bounds checks as `i32.lt_u index, len`: the one idiom that would bound an index is the one shape scry declines to read. THE REFINEMENT IS AVAILABLE UNDER A SIDE CONDITION, and the side condition is exactly the bounds-check shape. For `x <u c` with `0 <= c <= 2^31`, the SIGNED interval `[0, c-1]` is sound -- unsigned `x < c <= 2^31` puts x in `[0, 2^31-1]`, representable as non-negative signed, so no wrap into the negative half. VERIFIED EXHAUSTIVELY at w=8 over all (c, x) pairs BEFORE filing, in both directions. Zero counterexamples for `0 <= c <= 2^(w-1)`. And 127 constants ABOVE it where the signed reading FAILS -- so the side condition is load-bearing, not decorative, and a version that dropped it would be unsound. A rule that held for every c would have meant I had mis-stated it. NOT A POLYHEDRA FEATURE. Bounding locals feeds the interval domain, the octagon, the no-wrap gate, the trap checks, and the OOB proven rate (FEAT-069 measured 0.67% and diagnosed PRECISION, not format). Filed as its own artifact rather than buried in FEAT-057's residual because it blocks several things and, like FEAT-095, nothing tracked it. Typed `depends-on FEAT-057 -> FEAT-098` so the dependency is machine- visible rather than prose (the FEAT-096 lesson). Both are v3.4.0, so the ordering gate stays green -- CONFIRMED IT IS ACTUALLY READ by mutating FEAT-098 into v3.5.0: the gate fired naming the new pair, then went green on revert. First inversion the gate has caught that I did not seed at build time. AC#4 and AC#5 demand the MEASURED delta after implementation -- the >=3-local count (0 today), the no-wrap-provable share of 94 sites (0 today), and FEAT-069's 0.67%. "The number did not move" is written to be a reportable outcome rather than a silent one. Refs: FEAT-098 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Contributor
Author
|
Follow-up: what came of the inert result. This PR merged reporting zero octagon-beating constraints, and that number has now been chased to a named cause and filed. Recording it here so this PR does not read as a dead end. The chain, end to end
Every linear constraint emitted is ≤2-local — nothing the octagon could not already express. Root causeThe operands are ⊤ because the guard that would bound them is declined.
That refusal is correct. It is also the most consequential precision decision in the analyzer, because LLVM emits array bounds checks as This is exactly what FEAT-057's own 2026-07-14 reframing predicted: polyhedra's value is general-coefficient facts, which over wrapping i32 are unsound without value bounds, which come from guards. Filed as FEAT-098 (#202), with the leverFor Verified exhaustively at w=8 over every
What would change the numberRe-run the harness this PR extended: FEAT-098's AC#4 requires reporting the delta on the two numbers above (0 ≥3-local, 0/94 no-wrap) after it lands — written so that "the number did not move" is a reportable outcome rather than a silent one, because the whole feature rests on this causal claim. What this PR got right, for the recordThe slice is sound and the oracles are real, not just green:
Refs: FEAT-057 · FEAT-098 |
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.
Slice 2a wires
scry-sai-poly(shipped in 3.2.1, never connected) into the analyzer's structured-CFG fixpoint. It is sound, tested, and currently produces zero octagon-beating constraints on a real module. That negative result is the most valuable thing in this PR, and it is measured rather than inferred.The number that matters
Run
examples/poly_surface.rs(on main since #199) againstscry_mcdc.wasm:The domain is live — 5,138 constraints across 130 functions — but every one is ≤2-local, i.e. nothing the octagon could not already express.
Why, instrumented rather than guessed
94
z := x + ysites reach the transfer per analysis; 0 have a provable no-wrap. Real LLVM operands are interval-⊤ at those sites (unbounded params), and LLVM emits unsigned bounds checks, whichguard_opsoundly refuses to refine.This is exactly what FEAT-057's own 2026-07-14 reframing predicted: polyhedra's value is general-coefficient facts, which over wrapping i32 are unsound without value bounds, which come from guards. The blocker is unsigned-guard refinement / bits-fed bounds /
param_rangesseeding — a slice-3+ lever, now recorded in the residual with the numbers.Cost is within run noise (~21.2–22.9s, poly vs poly-inert baseline).
Verified independently, not taken on trust
cargo test -p scry-sai-core -p scry-sai-polycargo fmt --all -- --checkRelationalConstraint/snapshot_relationalproposed— slice 2a cannot satisfy AC3if no_wrap→if true, 3 sites, applied-count asserted)feat057_wrap_gate_never_admits_unproven_equality; control restores 160 passThe discriminating oracle is real:
feat057_linear_beats_octagon_on_three_var_relationasserts both directions — that the witness(100,100,0)satisfies every surfaced octagon constraint and every interval bound (so the "octagon cannot express it" half is itself tested, not assumed), and that the linear output excludes it.The wrap-gate test pins both sides — the wrapping case must be rejected and a no-wrap twin must be admitted, because "a gate that never admits an equality would be inert, not sound."
What was built
Poly::project(Fourier–Motzkin elimination), with every bail direction stated: overflow and the pos×neg cap drop constraints (enlarging — sound for projection); keeping a row that mentions the eliminated variable is the unsound direction and is structurally impossible. γ-swept, plus a transitive-consequence test (x≤2 ∧ y≤x ⊢ y≤2) so a drop-everything implementation cannot pass.poly: PolyonFuncCtx, mirrored againstmemsite-for-site — record ×4, block merge ×2, loop entry/header/back-edge-join/widen/leq/cap/narrow/final/post, scrub, havoc-project. The two remainingmem-only resets are call sites (memory-only effects; Wasm locals are callee-inaccessible, as the octagon already relies on).i32_add/i32_sub≠ ⊤; self-referencing shapes only project.refine_poly_relmirroringrefine_octagon_relon bothbr_ifedges.ProgramPoint.linear(LinearConstraint/LinearTerm).Known asymmetry, deliberate
The octagon narrows after widening; the poly (like
mem) does not. Conservative-only.A vacuous-test bug caught mid-work
The first loop/merge fixtures used
drop— an unsupported op that scrubs the function, so the post-merge assertions were checking zero points. The committed tests assert per-pc point existence before asserting anything about it.Refs: FEAT-057
🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc