From d0ff21dc7aa512d1675e2b1ad5519f45060c99ea Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 14 Jul 2026 13:58:02 +0000 Subject: [PATCH] prop-amm: bound the Kani harnesses so the weekly proofs terminate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first scheduled Kani run to include prop-amm (13 Jul) hit the GitHub-hosted runner's 6-hour hard limit: every other crate's proofs finished in under 3 minutes, but prop-amm's "Run Kani" step ran from 07:08 to 13:08 and was killed, surfacing as a cancelled run. The culprit is proof_quote_brackets_oracle, which left the oracle price at the full u64 range while multiplying it by the symbolic spread — a 64x14-bit nonlinear multiply plus 128-bit divisions, the worst case for the bit-precise solver (the old comment called this "linear", but both operands are symbolic). Cap the price at 16 bits: the rounding identities depend only on the product's residue mod 10_000, which a 16-bit price against the full spread range already covers exhaustively. Also tighten the symbolic-divisor harnesses (buy/sell to 8-bit amounts/prices, the chained round trip to 6-bit) to match the bounds the other finance proof crates stay tractable with, and give the verify job a 45-minute timeout so a blown-up harness fails fast and loudly instead of burning 6 hours and showing up as "cancelled". Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01FYjBwE7n8i1J3ycYD8ebup --- .github/workflows/kani.yml | 6 ++++ finance/prop-amm/kani-proofs/src/lib.rs | 41 ++++++++++++++++--------- 2 files changed, 32 insertions(+), 15 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index ae3e5b27..3b7181e8 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -76,6 +76,12 @@ jobs: name: Kani proofs (${{ matrix.program }}) if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest + # Every crate's proofs complete in under ~3 minutes. A harness whose bounds + # make the solver blow up otherwise runs into the runner's 6-hour hard + # limit and surfaces as an easy-to-miss "cancelled" run (this happened: + # prop-amm's quote-bracketing harness with an unbounded u64 price). Fail + # fast and loudly instead. + timeout-minutes: 45 strategy: fail-fast: false matrix: diff --git a/finance/prop-amm/kani-proofs/src/lib.rs b/finance/prop-amm/kani-proofs/src/lib.rs index e3e17e95..b648c9fe 100644 --- a/finance/prop-amm/kani-proofs/src/lib.rs +++ b/finance/prop-amm/kani-proofs/src/lib.rs @@ -49,9 +49,16 @@ pub fn bid_price(oracle_price: u64, spread_bps: u16) -> Option { fn proof_quote_brackets_oracle() { let price: u64 = kani::any(); let spread_bps: u16 = kani::any(); - // The full price range is linear arithmetic and stays tractable; the - // spread is validated `1..10_000` by initialize_market / set_quote. - kani::assume(price >= 1); + // Bounded model checking: `price * (BPS ± spread)` multiplies two symbolic + // values — nonlinear arithmetic, the worst case for the bit-precise solver + // (an unbounded u64 price makes this harness run for hours; see the 6-hour + // CI timeout this bound fixed). The rounding behaviour of the divisions by + // BASIS_POINTS depends only on the product's residue mod 10_000, and a + // 16-bit price against the full spread range already exercises every + // residue and carry pattern — larger prices add magnitude, not new + // rounding edges. The spread is validated `1..10_000` by + // initialize_market / set_quote, so that range stays exact. + kani::assume(price >= 1 && price <= 0xFFFF); kani::assume(spread_bps >= 1 && (spread_bps as u128) < BASIS_POINTS); let ask = ask_price(price, spread_bps).expect("ask computes"); @@ -132,13 +139,16 @@ fn proof_buy_never_exceeds_oracle_value() { let quote_decimals: u8 = kani::any(); // Bounded model checking: the division by a *symbolic* ask is the hard - // part for the bit-precise solver. Amounts and price are capped, and the - // decimal exponents are kept small (the identity is independent of the - // exponents' actual values — they enter both sides of the comparison - // symmetrically — so tiny exponents exercise the same rounding edges as - // scale 8 and 6/6 decimals). - kani::assume(quote_in <= 1023); - kani::assume(price >= 1 && price <= 1023); + // part for the bit-precise solver, and its cost grows with the divisor's + // bit-width (ask spans one more bit than price). Amounts and price are + // capped at 8 bits — in line with the symbolic-divisor bounds the other + // finance proof crates stay tractable with — and the decimal exponents + // are kept small (the identity is independent of the exponents' actual + // values — they enter both sides of the comparison symmetrically — so + // tiny exponents exercise the same rounding edges as scale 8 and 6/6 + // decimals). + kani::assume(quote_in <= 255); + kani::assume(price >= 1 && price <= 255); kani::assume(spread_bps >= 1 && (spread_bps as u128) < BASIS_POINTS); kani::assume(oracle_scale <= 2); kani::assume(base_decimals <= 2 && quote_decimals <= 2); @@ -168,8 +178,9 @@ fn proof_sell_never_exceeds_oracle_value() { let base_decimals: u8 = kani::any(); let quote_decimals: u8 = kani::any(); - kani::assume(base_in <= 1023); - kani::assume(price >= 1 && price <= 1023); + // Same bounds as the buy side (see proof_buy_never_exceeds_oracle_value). + kani::assume(base_in <= 255); + kani::assume(price >= 1 && price <= 255); kani::assume(spread_bps >= 1 && (spread_bps as u128) < BASIS_POINTS); kani::assume(oracle_scale <= 2); kani::assume(base_decimals <= 2 && quote_decimals <= 2); @@ -205,9 +216,9 @@ fn proof_round_trip_never_profits_the_trader() { let quote_decimals: u8 = kani::any(); // Two symbolic divisions chained — the hardest harness here; keep the - // amount bound tight. - kani::assume(quote_in <= 255); - kani::assume(price >= 1 && price <= 255); + // amount and price bounds tighter than the single-division harnesses'. + kani::assume(quote_in <= 63); + kani::assume(price >= 1 && price <= 63); kani::assume(spread_bps >= 1 && (spread_bps as u128) < BASIS_POINTS); kani::assume(oracle_scale <= 2); kani::assume(base_decimals <= 2 && quote_decimals <= 2);