From 8784277474b071133d00c150a235fb0133610e0d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 14 Jul 2026 20:50:49 +0200 Subject: [PATCH] =?UTF-8?q?rivet:=20reframe=20FEAT-057=20slice-2=20?= =?UTF-8?q?=E2=80=94=20straight-line=20poly=20is=20vacuous=20over=20wrappi?= =?UTF-8?q?ng=20ints?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Records the 2026-07-14 discovery: the intended additive straight-line polyhedra pass (mirroring the bits/float passes) is near-vacuous for a SOUND reason. Over Wasm's wrapping i32, a general-coefficient fact (z = x+y) is unsound unless no-wrap is proven, which needs bounds → guards → the fixpoint. So the poly body requires the full fixpoint integration (Poly on FuncCtx in lockstep with the octagon, wrap-aware transfers, guards, Poly::project) — a multi-slice arc, not a straight-line shortcut. Slice-1 (the crate) shipped in 3.2.1; this honestly re-scopes slice-2. Co-Authored-By: Claude Opus 4.8 --- artifacts/roadmap-3.0.yaml | 36 ++++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index cf31634..13a18aa 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -674,18 +674,30 @@ artifacts: Convex polyhedra (Cousot-Halbwachs 1978, AC-012; DD-019) for exact linear inequalities Σ a_i·x_i ≤ c above the octagon, made tractable by ELINA-style online constraint decomposition into independent variable blocks (TE-012). - Sequenced AFTER v3.2 segmentation. Planned slices: - 1. New pure crate `scry-sai-poly` — constraint-form polyhedra with join = - convex hull, meet = constraint union, and standard polyhedra widening; - ELINA-style block decomposition for cost. Native γ-sweep falsifier. - Admit-free Rocq for the LATTICE algebra (proofs/rocq/Poly.v: order / - join-upper-bound / meet-glb). - 2. Wire in as an optional relational domain above the octagon; surface - inferred linear invariants through the FEAT-041 relational-invariant - output (REQ-016). - 3. Precision + cost differential vs the octagon on a corpus (falsify the - "infers invariants the octagon cannot" claim); a cost gate bounds the - decomposition blow-up. + Sequenced AFTER v3.2 segmentation. Slices: + 1. SHIPPED (#104, published 3.2.1): pure crate `scry-sai-poly` — + constraint-form polyhedra with meet = constraint union (exact), + Fourier-Motzkin entailment, a sound entailed-by-both join + (over-approximation of the hull; the exact double-description hull + + ELINA decomposition are deferred), and widening. Native γ-sweep; + admit-free Rocq LATTICE proof (proofs/rocq/Poly.v). Clean-room SOUND. + 2. REFRAMED — wire into the analyzer. **Discovery (2026-07-14):** the + intended additive STRAIGHT-LINE pass (mirroring the bits/float passes) + is near-VACUOUS for polyhedra, and for a SOUND reason. Polyhedra's + value is general-coefficient facts (`z = x + y`), but over Wasm's + WRAPPING i32 that equality is unsound unless no-wrap is proven — which + needs value BOUNDS, which come from GUARDS, which need the FIXPOINT. + On straight-line code with unbounded params, every arithmetic result + may wrap ⇒ no octagon-beating fact is soundly emittable. (Unlike + bits/float, which are wrap-internal.) So the poly BODY requires the + full fixpoint integration: a `Poly` on FuncCtx threaded in LOCKSTEP + with the octagon (join/widen at every merge), wrap-AWARE assignment + transfers gated on the interval domain's no-wrap result (scry_interval + i32_add returns ⊤ exactly when wrap is possible), guard refinement, + and `Poly::project` (FM variable elimination) for reassignments. This + is a multi-slice arc like the octagon's v1.7–1.9 — tracked as its own + sub-arc, not crammed. Surface via the FEAT-041 relational output. + 3. Precision + cost differential vs the octagon on a corpus. HONESTY (carried from the WasmCert-Coq pass): full convex-hull / Fourier- Motzkin soundness is NOT cheaply mechanizable — Poly.v mechanizes the lattice algebra only; the transfer functions are γ-sweep-validated and the