predict: envelope (interval) arithmetic for derived contract values (DBU-628)

[0xaslan]

Summary

• Every derived value in the Predict contracts — boundary prices, range probabilities, walk liabilities, corrections, reserves, free cash, market NAV, pool value — is computed as a sound envelope (fixed_math::interval::Interval{lo,hi}: the true value provably inside, maintained by directed rounding), with persistent storage kept exact-scalar and every envelope→scalar collapse an explicit site with an economically chosen side.
• New fixed_math surface: the directed pair mul_up/div_up and the interval module (no store ability — envelopes are transaction-local by the type system).
• Trade lanes commit at doctrine corners: the mint tuple commits jointly at the protocol-favored corner with its integer identity exact (entry_value = mul_up(P.hi, Q), net_premium = div_up(E, lev), floor_shares by identity; 1x zero-floor structural); redeems commit at the low corner; the trading fee now rounds up (protocol inflow); admission gates are definite-in-band; the liquidation knock-out test reads the gross envelope's low side through one predicate shared by the close classifier, the ambient sweep, and the flush scan.
• The pool flush runs entirely on envelopes: interval price memo (guard aborts only on definite surface inversion), interval walks and kill scan, per-market NAV as the per-corner defined quantity max(0, free_cash − liability), corner-wise lp_pool_value, and a two-mark drain — supply queue at the pool value's high bound, withdraw queue at its low bound, per-side executability. FlushExecuted publishes the (lo, hi) mark pair; the width is the flush's bid/ask spread.
• Backing asserts and surplus releases compare the definite (high) side of every hold (required_cash_hi).
• Design doc: packages/predict/predeploy/interval-arithmetic.md (definitions, storage classes, collapse taxonomy, side doctrine, abort inventory).

Why

• Setting: Predict prices digital range options with fixed-point math and marks an LP pool whose one frozen NAV mark prices both share supply and share withdrawal each flush.
• Problem: scalar rounding produced a recurring defect class — silent one-unit bias toward or against the pool, dust underflows able to abort settlement or valuation paths, and rounding-direction proofs that couple distant code so one edit silently invalidates another expression's safety argument. The single-scalar mark also structurally cannot favor both supply and withdrawal at once.
• Trigger: the NAV dust-invariant unwind — proving subtractions safe one at a time did not scale, and the mark-direction conflict has no scalar solution (DBU-628).

Key decisions

• Soundness once, not per site: the interval library is property-verified (directed rounding, truth containment, width laws); call sites never re-argue arithmetic safety. Aborts fire only on definite violations of the oracle vendor's monotone-surface guarantee — the flush-lane abort inventory is enumerated in the design doc and none is reachable through rounding or any admissible book.
• Storage cannot hold widths: Interval has no store ability; stored values are exact atoms, realized commitments, or defined recurrences.
• Public API criterion: transact-answers return the committed scalar; worth-answers return primitive (u64, u64) bounds; the envelope type never enters a public signature.
• Pool value is evaluated corner-wise, justified by a monotonicity argument (slope 1 or 1−share; the integer floor only absorbs steps), so the gross and exclusion terms cannot double-count width.
• The evaluation-error tiers on up_price are measured against an independent float64 reference across the admissible SVI envelope (saturated/healthy/degenerate = 8/48/1e6 raw at the 0.01 total-variance threshold, ≥2.5× pad over p99); an analytic certificate is planned hardening.

Scope / Descoped

• DRAFT for contract-shape review. Deliberately not here: unit-test re-pin (33 expectations assert pre-envelope values and the plp flow tests reference pre-envelope signatures — CI is known-red), gas measurement of the interval flush, the scalar read-lane disposition (superseded scalar flush lane still present, no production callers), sibling fee sides (builder fee, congestion penalty), oracle confidence as input width, and the oracle-surface tolerated-domain work.
• Stacked on predict: value knocked-out orders at liquidated worth in the NAV correction (DBU-605) #1153 (liquidate-during-flush): base is at/dbu-605-liquidate-during-flush, so this diff shows only the envelope work.

Test plan

• sui move build --path packages/predict --warnings-are-errors clean; packages/fixed_math suite 159/159 green (new interval property tests included)
• packages/predict/predeploy/check.py — 0 warnings
• Unit-test re-pin (separate phase; known-red set enumerated in the commit message)
• Localnet gas measurement of the full-pool interval flush (separate phase)

Pricing finalization (follow-up commits)

The interval valuation lane needs a sound pricing envelope. These commits finalize how one up_price evaluation is bounded:

• High-precision variance path. compute_nd2_terms computes total variance, sqrt(w), and d2 in u128 at 1e18 instead of flooring the b*inner product to 1e9. That flooring discarded the entire signal at short expiry (a 5-minute surface has total variance ~1e-8, about ten raw units at 1e9), inflating pricing error to ~0.4%. It now stays near the arithmetic floor.
• One certified widen. The scalar price is widened by a single constant (up_price_evaluation_error, 3e-4) to form the sound interval. One value suffices because the admission gate bounds the pricing error across the whole admitted domain; a variance-keyed table was removed as premature and, as reviewed, unsound at mid-variance.
• Admission gate + tight caps. assert_inputs_pricing_safe enforces beta^2 <= 9 * min_tv (skew vs variance, keeping the skew correction clear of the [0,1] clamp) and tight SVI caps (|a|,|m|,sigma <= 1, b <= 0.1) so the deep-ITM/OTM digital-limit saturations are genuinely exact. Real Block Scholes surfaces clear every bound with wide headroom.
• Certificate. packages/predict/predeploy/pricing_error_certificate.py is a self-contained harness (fixed-point mirror vs mpmath, verified leaf constants, the gated-box error envelope over the full moneyness range) documenting how the widen, gate, and caps were derived.

Reviewed by two independent passes (a fresh reviewer and a codex subagent); the low-level fixed-point mechanics are confirmed correct. The unit-test suite compiles against the interval-lane signatures; value expectations re-pin as the next phase. Interval-branch-and-bound verification of the widen is planned hardening before audit.