From 66826a8981457fb651d5e6b1a3d0e9597f7c6da6 Mon Sep 17 00:00:00 2001 From: obanai9 Date: Mon, 1 Jun 2026 18:55:19 +0000 Subject: [PATCH] test(#50): add property-based invariant tests for leverage math MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds proptest as a dev-dependency and a new test_proptest.rs module with 7 invariants run over 1 000 cases each: supply ≥ borrow, net equity equals initial, geometric-series bound, HF monotonicity, compute_step supply equals balance, final borrow is zero, and no panic on extreme i128 inputs. Closes #50 Co-Authored-By: Claude Sonnet 4.6 --- .../strategies/blend_leverage/Cargo.toml | 1 + .../strategies/blend_leverage/src/lib.rs | 2 + .../blend_leverage/src/test_proptest.rs | 161 ++++++++++++++++++ 3 files changed, 164 insertions(+) create mode 100644 contracts/strategies/blend_leverage/src/test_proptest.rs diff --git a/contracts/strategies/blend_leverage/Cargo.toml b/contracts/strategies/blend_leverage/Cargo.toml index 85108d8..97c36e3 100644 --- a/contracts/strategies/blend_leverage/Cargo.toml +++ b/contracts/strategies/blend_leverage/Cargo.toml @@ -16,6 +16,7 @@ blend-contract-sdk = "2.25.0" [dev-dependencies] soroban-sdk = { version = "25.3.0", features = ["testutils"] } blend-contract-sdk = { version = "2.25.0", features = ["testutils"] } +proptest = "1" [profile.release] opt-level = "z" diff --git a/contracts/strategies/blend_leverage/src/lib.rs b/contracts/strategies/blend_leverage/src/lib.rs index d878a71..c826126 100644 --- a/contracts/strategies/blend_leverage/src/lib.rs +++ b/contracts/strategies/blend_leverage/src/lib.rs @@ -11,6 +11,8 @@ mod storage; mod test_leverage; #[cfg(test)] mod test_integration; +#[cfg(test)] +mod test_proptest; use constants::SCALAR_12; pub use defindex_strategy_core::{event, DeFindexStrategyTrait, StrategyError}; diff --git a/contracts/strategies/blend_leverage/src/test_proptest.rs b/contracts/strategies/blend_leverage/src/test_proptest.rs new file mode 100644 index 0000000..7f21d9a --- /dev/null +++ b/contracts/strategies/blend_leverage/src/test_proptest.rs @@ -0,0 +1,161 @@ +#![cfg(test)] +extern crate std; + +//! Property-based invariant tests for leverage math using proptest. +//! +//! Each property is run with at least 1 000 randomly-generated cases. Failing +//! inputs are automatically shrunk to the smallest reproducing example by the +//! proptest framework. +//! +//! Invariants verified: +//! 1. total_supply >= total_borrow (borrow never exceeds supply) +//! 2. total_supply - total_borrow == initial (net equity preserved) +//! 3. total_supply <= initial / (1 - c) (geometric-series upper bound) +//! 4. HF is monotone in c_factor (higher c → strictly higher HF) +//! 5. compute_step supply == balance (supply leg is always the full balance) +//! 6. compute_step final borrow == 0 (no borrow on the last step) +//! 7. no overflow / panic on large inputs (graceful saturation via checked_mul) + +use crate::constants::SCALAR_7; +use crate::leverage::{compute_health_factor, compute_step, compute_totals}; +use proptest::prelude::*; + +/// Run every proptest property with at least 1 000 cases. +const CASES: u32 = 1_000; + +proptest! { + #![proptest_config(ProptestConfig::with_cases(CASES))] + + // ── Invariant 1 ───────────────────────────────────────────────────────── + // total_supply is always >= total_borrow for any valid inputs. + // Rationale: borrowing is always a fraction (c < 1) of supply, so the + // cumulative sum of borrows can never exceed the cumulative sum of supplies. + #[test] + fn inv_total_supply_gte_total_borrow( + initial in 1i128..=1_000_000_000_000i128, + c_factor in 100_000i128..=9_900_000i128, + n_loops in 0u32..=20u32, + ) { + let (total_supply, total_borrow) = compute_totals(initial, c_factor, n_loops); + prop_assert!( + total_supply >= total_borrow, + "total_supply ({}) < total_borrow ({}) with initial={}, c={}, n={}", + total_supply, total_borrow, initial, c_factor, n_loops + ); + } + + // ── Invariant 2 ───────────────────────────────────────────────────────── + // total_supply - total_borrow == initial (net equity equals initial deposit). + // Each loop borrows exactly what the next loop supplies, so the only + // "free" supply is the original deposit. + #[test] + fn inv_net_equity_equals_initial( + initial in 1i128..=1_000_000_000_000i128, + c_factor in 100_000i128..=9_900_000i128, + n_loops in 0u32..=20u32, + ) { + let (total_supply, total_borrow) = compute_totals(initial, c_factor, n_loops); + prop_assert_eq!( + total_supply - total_borrow, + initial, + "net equity {} != initial {} (c={}, n={})", + total_supply - total_borrow, initial, c_factor, n_loops + ); + } + + // ── Invariant 3 ───────────────────────────────────────────────────────── + // total_supply <= initial * SCALAR_7 / (SCALAR_7 - c_factor). + // This is the geometric-series upper bound (leverage ≤ 1 / (1 - c)). + // We allow +1 for integer truncation rounding. + #[test] + fn inv_leverage_bounded_by_geometric_series( + initial in 1i128..=1_000_000_000i128, // keep small enough that max_supply fits i128 + c_factor in 100_000i128..=9_500_000i128, // cap at 95% so denominator >= 500_000 + n_loops in 0u32..=20u32, + ) { + let (total_supply, _) = compute_totals(initial, c_factor, n_loops); + let denominator = SCALAR_7 - c_factor; + // max_supply = initial × SCALAR_7 / (SCALAR_7 - c_factor) + // Use i128 arithmetic carefully; denominator >= 500_000 and initial <= 1e9, + // so initial * SCALAR_7 <= 1e9 * 1e7 = 1e16, well within i128. + let max_supply = initial * SCALAR_7 / denominator; + prop_assert!( + total_supply <= max_supply + 1, + "total_supply {} exceeds geometric bound {} (initial={}, c={}, n={})", + total_supply, max_supply, initial, c_factor, n_loops + ); + } + + // ── Invariant 4 ───────────────────────────────────────────────────────── + // HF is monotone (non-decreasing) in c_factor for fixed positions and rates. + // A higher collateral factor means the same supply is worth more as + // collateral, so the health factor can only increase. + #[test] + fn inv_hf_monotone_in_c_factor( + b_tokens in 1i128..=1_000_000_000i128, + d_tokens in 1i128..=500_000_000i128, + rate in 1_000_000_000_000i128..=2_000_000_000_000i128, + c_low in 1_000_000i128..=4_999_999i128, + c_high in 5_000_000i128..=9_900_000i128, + ) { + let hf_low = compute_health_factor(b_tokens, d_tokens, rate, rate, c_low); + let hf_high = compute_health_factor(b_tokens, d_tokens, rate, rate, c_high); + if let (Ok(hf_l), Ok(hf_h)) = (hf_low, hf_high) { + prop_assert!( + hf_h >= hf_l, + "HF not monotone: c_low={} → hf={}, c_high={} → hf={}", + c_low, hf_l, c_high, hf_h + ); + } + } + + // ── Invariant 5 ───────────────────────────────────────────────────────── + // compute_step: the supply leg always equals `balance`, regardless of + // c_factor or is_final. + #[test] + fn inv_compute_step_supply_equals_balance( + balance in 0i128..=1_000_000_000_000i128, + c_factor in 0i128..=9_999_999i128, + is_final in proptest::bool::ANY, + ) { + let (supply, _borrow) = compute_step(balance, c_factor, is_final); + prop_assert_eq!( + supply, balance, + "supply {} != balance {} (c={}, final={})", + supply, balance, c_factor, is_final + ); + } + + // ── Invariant 6 ───────────────────────────────────────────────────────── + // compute_step: borrow is exactly 0 on the final step. + // The last iteration only supplies; no further borrowing is needed. + #[test] + fn inv_compute_step_final_borrow_is_zero( + balance in 0i128..=1_000_000_000_000i128, + c_factor in 0i128..=9_999_999i128, + ) { + let (_supply, borrow) = compute_step(balance, c_factor, true); + prop_assert_eq!( + borrow, 0i128, + "final step borrow {} != 0 (balance={}, c={})", + borrow, balance, c_factor + ); + } + + // ── Invariant 7 ───────────────────────────────────────────────────────── + // compute_totals must not panic on extreme inputs. + // checked_mul saturates to 0 on overflow (unwrap_or(0)), so the function + // should always return without panicking. + #[test] + fn inv_no_panic_on_extreme_inputs( + initial in 1i128..=i128::MAX / SCALAR_7, + c_factor in 0i128..=9_999_999i128, + n_loops in 0u32..=20u32, + ) { + // Must not panic + let (total_supply, total_borrow) = compute_totals(initial, c_factor, n_loops); + // Basic sanity: supply and borrow are non-negative + prop_assert!(total_supply >= 0, "total_supply {} < 0", total_supply); + prop_assert!(total_borrow >= 0, "total_borrow {} < 0", total_borrow); + } +}