test(pm): replay test — leverage/margin math invariants (t17)

[chiliec]

Summary

Companion to the settlement replay test — adds t17_leverage_math_invariants.cpp, which links the real leverage/margin math (libraries/chain/pm/leverage.cpp) and asserts the safety properties the margin subsystem depends on, across adversarial + fuzzed inputs. No chain build required (see tests/pm/replay/README.md); runs in seconds.

Invariants checked

• I — bounded k on buy: new_reserve_a × new_reserve_b ∈ (k − divisor, k]. The CPMM floor never lets the product exceed the stored k (no phantom constant-product accruing to the pool) and loses at most one divisor-unit, so tokens_out is not unboundedly inflated in the bettor's favour. The stored k is not reassigned on a bet, so the bound holds bet-over-bet.
• II — round-trip non-profit: buy amount, immediately cancel the tokens at the same reserves → cancel_value ≤ amount. A self-sandwich cannot mint against the curve.
• III — monotonicity: cancel_value_after_opposing is non-increasing in the opposing bet m — the property that makes worst_opposing_bet the actual worst case for the open-time solvency check.
• IV — solvency: max_leverage_loan only returns a loan L for which the worst-case cancel value cvw ≥ threshold_safe (= liquidation_threshold(L) × (1 + s%)); it never hands out an under-margined loan, and returns 0 when nothing qualifies.
• V — fuzz: 400,000 randomized positions over the reachable reserve range — no negative outputs, no 128-bit wrap, k bounded, round-trip-safe. 0 violations.

Note

The k bound is the exact floor guarantee: new_out = floor(k / new_in) ⇒ new_in × new_out ∈ (k − new_in, k]. My first draft asserted the wrong direction (and used the wrong reserve as the divisor); the math is correct — pinning the exact bound is what the exercise surfaced, and it's now documented in the test.

Verification

Built and run green with g++:

ALL LEVERAGE-MATH INVARIANTS HOLD — no curve leak, no round-trip profit, solvent loans (0 failing assertions)

Registered in tests/pm/replay/build.sh; existing linked cases (t10/t15) still pass — no regression.