feat: Kani formal verification of collateral, payoff and fee arithmetic (#119)

[Whiznificent]

Closes #119.

What

Formally verifies the fund-critical arithmetic with Kani bounded model checking — proofs over the whole bounded input domain, not sampled examples:

• src/math_fixed.rs — integer-scaled prototypes of collateral::collateral_required, the payoff.rs intrinsic/P&L arithmetic, and protocol-fee rounding, with rounding always up (protocol-favouring).
• src/kani_proofs.rs — 8 proof harnesses, gated behind #[cfg(kani)] so normal cargo test/clippy builds never pay for them:
  1. collateral is never negative;
  2. collateral is monotonic in contracts;
  3. collateral is monotonic in strike;
  4. short-put collateral ≥ the maximum possible loss (spot at zero), so collateral always covers the payoff at expiry;
  5. long leg + mirrored short leg P&L is exactly zero;
  6. intrinsic value never dips below the zero floor;
  7. fee rounding favours the protocol by less than one fee unit;
  8. no arithmetic overflow inside the documented bounds.
• .github/workflows/kani.yml — proofs run in CI via kani-github-action on every PR, push to main, and nightly (45-min budget, superseded runs auto-cancelled).
• docs/verification.md — the verification report: property table, reproduction, expected output, counterexample policy, and the precise f64 gap.

Proof output

All 8 harnesses verified in CI:

Checking harness kani_proofs::no_overflow_inside_the_documented_domain...
VERIFICATION:- SUCCESSFUL
...
Complete - 8 successfully verified harnesses, 0 failures, 8 total.

Full run: 1m21s including Kani setup.

The f64 gap (as scoped by the issue)

Verifying f64 Black-Scholes with BMC is out of scope (not tractable), so the proofs target integer-scaled prototypes of the same formulas. docs/verification.md documents the mapping precisely, including that fee_fixed pins the rounding direction before any fee-charging code exists. When the fixed-point migration lands, these same properties port to the production width unchanged.

Notes on tractability

The word width is deliberately narrow (i16, MAX_INPUT = 50): Kani's SAT encoding of symbolic multiply/divide grows superlinearly with bit width, and 32-bit versions of these exact harnesses were run and did not finish inside a 45-minute budget (5/8 verified before cancellation). At 16 bits all 8 harnesses verify fully symbolically in about a minute. The proven properties are algebraic facts about the formulas and do not depend on magnitude — this trade-off, and the porting path to the production width, are recorded in docs/verification.md.

Test evidence

fmt, clippy -D warnings, test, and cargo kani (8/8 verified) all pass on the branch.

[drips-wave]

@Whiznificent Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits