diff --git a/README.md b/README.md index 2b49ecb..964a366 100644 --- a/README.md +++ b/README.md @@ -156,6 +156,38 @@ The suite covers the full lifecycle, both default paths, the authorisation boundary, and an accounting invariant asserting that after a complete cycle every member is square to the stroop and the contract holds nothing. +### Property-based testing + +In addition to the hand-written scenarios, `contracts/circle/src/proptest_harness.rs` +runs a property-based harness using [proptest](https://docs.rs/proptest). It +generates random circles — varying member counts (3–24), contribution sizes +(1–1 000 000 stroops), round durations (1 s – 30 days) — and executes full +lifecycles with random per-member, per-round actions: + +| Action | Meaning | +|--------|---------| +| `Pay` | Member contributes on time | +| `Default` | Member skips; deposit covers the gap (or is exhausted) | +| `DefaultThenTopUp` | Member skips then calls `top_up` to restore the deposit | + +After every run the harness asserts four invariants: + +| ID | Invariant | +|----|-----------| +| I-1 | `status == Complete` after the last round | +| I-2 | Every member's `received` flag is `true` | +| I-3 | Contract token balance is `0` after all withdrawals | +| I-4 | Token conservation: `Σ balance_after == Σ balance_before_join` | + +Counterexamples are shrunk automatically by proptest to the smallest failing +input. If the harness finds a bug, the output names the violated invariant and +the exact `CircleParams` and action matrix that triggered it. + +```sh +cargo test -p circlefi-circle # runs scenario tests + property tests +PROPTEST_CASES=1000 cargo test # run more cases for a deeper search +``` + ## Licence Apache-2.0. diff --git a/contracts/circle/Cargo.toml b/contracts/circle/Cargo.toml index 59cf8ba..f8dbd7e 100644 --- a/contracts/circle/Cargo.toml +++ b/contracts/circle/Cargo.toml @@ -13,6 +13,7 @@ soroban-sdk = "27" [dev-dependencies] soroban-sdk = { version = "27", features = ["testutils"] } +proptest = "1" [features] testutils = ["soroban-sdk/testutils"] diff --git a/contracts/circle/src/lib.rs b/contracts/circle/src/lib.rs index ee597c5..2c528b8 100644 --- a/contracts/circle/src/lib.rs +++ b/contracts/circle/src/lib.rs @@ -499,3 +499,6 @@ impl Circle { } mod test; + +#[cfg(test)] +mod proptest_harness; diff --git a/contracts/circle/src/proptest_harness.rs b/contracts/circle/src/proptest_harness.rs new file mode 100644 index 0000000..d6ee99a --- /dev/null +++ b/contracts/circle/src/proptest_harness.rs @@ -0,0 +1,537 @@ +#![cfg(test)] + +//! Property-based tests for the CircleFi circle contract. +//! +//! ## Why this file exists +//! +//! The hand-written scenarios in `test.rs` are necessary but not sufficient. +//! They verify the accounting invariant: +//! +//! > *Every member receives their payout exactly once, and after all deposits +//! > are withdrawn the contract holds zero tokens.* +//! +//! against the handful of sequences the author thought to write down. A +//! property-based harness generates thousands of random circles - varying +//! member counts, contribution sizes, and patterns of who pays, who defaults, +//! and who tops-up - and asserts the same invariant after every complete +//! lifecycle. This is the kind of test that finds the bug nobody wrote a case +//! for. +//! +//! ## Approach +//! +//! We use proptest because it: +//! +//! * Generates structured, valid inputs (no rejected cases from a naive fuzzer). +//! * Shrinks counterexamples automatically to the smallest failing input. +//! * Integrates with `#[test]` so `cargo test` runs everything without extra +//! tooling. +//! +//! ## Invariants checked +//! +//! | ID | Statement | +//! |-----|-----------| +//! | I-1 | `status == Complete` after the last round. | +//! | I-2 | Every member's `received` flag is `true`. | +//! | I-3 | The contract's token balance is `0` after all deposit withdrawals. | +//! | I-4 | Token conservation: sum(balance_after) == sum(balance_before_join). | +//! +//! ## Test matrix +//! +//! | Property | Description | +//! |----------|-------------| +//! | `prop_accounting_is_sound` | Random params + random action matrix | +//! | `prop_happy_path_always_balances` | All members pay every round | +//! | `prop_all_default_every_round` | Nobody ever contributes | +//! | `prop_single_rotating_defaulter` | One member defaults per round, rotating | +//! | `prop_default_then_top_up_every_round` | Everyone defaults then tops up | + +use super::*; +use proptest::prelude::*; +use soroban_sdk::{ + testutils::{Address as _, Ledger as _}, + token, Address, Env, +}; + +// ============================================================================ +// Domain model +// ============================================================================ + +/// A complete, valid set of circle parameters generated by the harness. +/// +/// All fields are chosen within the bounds enforced by the constructor so +/// that `env.register(Circle, ...)` never panics. +#[derive(Debug, Clone, Copy)] +struct CircleParams { + /// Number of members (== number of rounds). Range: [3, 24]. + capacity: u32, + /// Token amount each member must contribute per round. Range: [1, 1_000_000]. + /// + /// The upper bound ensures that even 24 members x 24 rounds x 3 top-ups + /// never overflows i128 or exhausts the minted supply. + contribution: i128, + /// Length of each round in seconds. Range: [1, 2_592_000] (1 s - 30 days). + round_seconds: u64, +} + +/// What a single member does in a given round. +/// +/// These three variants cover every branch in `settle`'s deposit-drawdown +/// logic: +/// +/// 1. `Pay` - the happy path; deposit is never touched. +/// 2. `Default` - deposit covers the round (or is exhausted, member goes delinquent). +/// 3. `DefaultThenTopUp` - deposit is drawn down, then `top_up` restores it +/// before the next round; tests that the restore path is sound. +#[derive(Debug, Clone, Copy)] +enum RoundAction { + /// Member calls `contribute` before the deadline. + Pay, + /// Member skips the round. Their deposit absorbs the gap, or is exhausted + /// and they become delinquent. + Default, + /// Member skips the round but then calls `top_up` to restore the deposit + /// after `settle` runs. + DefaultThenTopUp, +} + +/// Tracks how many rounds each member actually paid vs defaulted on. +/// +/// Used in error messages to make counterexamples easier to debug. +struct MemberLedger { + paid_rounds: u32, + defaulted_rounds: u32, +} + +// ============================================================================ +// Strategies +// ============================================================================ + +/// Generates a valid circle capacity in [MIN_CAPACITY, MAX_CAPACITY] = [3, 24]. +/// +/// MIN_CAPACITY is 3 (a two-member circle is just a loan) and +/// MAX_CAPACITY is 24 (bounded so `settle` stays within a single +/// transaction''s resource budget). +fn arb_capacity() -> impl Strategy { + 3u32..=24u32 +} + +/// Generates a strictly positive contribution amount in [1, 1_000_000]. +/// +/// The upper bound is chosen so that even the most expensive scenario - +/// 24 members, 24 rounds, every member tops up after every default - stays +/// well inside i128 and within the minted token supply. +fn arb_contribution() -> impl Strategy { + 1i128..=1_000_000i128 +} + +/// Generates a round duration from one second to thirty days. +/// +/// The lower bound of 1 s lets the harness advance the clock cheaply. +/// The upper bound of 30 days matches the constant used in the scenario tests. +fn arb_round_seconds() -> impl Strategy { + 1u64..=2_592_000u64 +} + +prop_compose! { + /// Generates a random, valid CircleParams. + /// + /// All three fields are generated independently; their ranges are chosen + /// so every combination is a legal constructor argument. + fn arb_circle_params()( + capacity in arb_capacity(), + contribution in arb_contribution(), + round_seconds in arb_round_seconds(), + ) -> CircleParams { + CircleParams { capacity, contribution, round_seconds } + } +} + +/// Generates a single member''s action for one round. +/// +/// Weights: Pay=6, Default=3, DefaultThenTopUp=1 (60/30/10 split). +/// The bias towards paying keeps most circles solvent to exercise the payout +/// path. Defaults are common enough to stress deposit coverage without +/// making the harness degenerate into all-default runs (covered separately). +fn arb_round_action() -> impl Strategy { + prop_oneof![ + 6 => Just(RoundAction::Pay), + 3 => Just(RoundAction::Default), + 1 => Just(RoundAction::DefaultThenTopUp), + ] +} + +/// Generates the full capacity x capacity action matrix. +/// +/// Outer vec (length capacity): one entry per round. +/// Inner vec (length capacity): one action per member in that round. +/// +/// Dimensions are determined by `capacity` so the matrix is always +/// consistent with the circle''s term sheet. +fn arb_all_actions(capacity: u32) -> impl Strategy>> { + let n = capacity as usize; + proptest::collection::vec( + proptest::collection::vec(arb_round_action(), n), + n, + ) +} + +// ============================================================================ +// Test driver +// ============================================================================ + +/// Runs a complete circle lifecycle through the Soroban mock environment and +/// asserts all four accounting invariants. +/// +/// # Lifecycle phases +/// +/// 1. Setup: deploy token, mint balances, deploy circle. +/// 2. Snapshot: record balances before join (I-4 baseline). +/// 3. Join: all members join, locking one contribution as a deposit. +/// 4. Rounds: for each of the `capacity` rounds: +/// a. Apply every member''s RoundAction (contribute or skip). +/// b. Advance clock past round_ends_at so settle cannot be blocked. +/// c. Call settle. +/// d. For DefaultThenTopUp members, call top_up if deposit was drawn down. +/// 5. Assert I-1 and I-2. +/// 6. Withdraw all remaining deposits. +/// 7. Assert I-3 and I-4. +/// +/// # Returns +/// +/// `Ok(())` if every invariant holds; `Err(description)` naming the first +/// violated invariant. +fn run_circle_scenario( + params: CircleParams, + all_actions: &[Vec], +) -> Result<(), String> { + // -- Phase 1: environment and token --------------------------------------- + let env = Env::default(); + env.mock_all_auths(); + + let issuer = Address::generate(&env); + let token_id = env.register_stellar_asset_contract_v2(issuer).address(); + let minter = token::StellarAssetClient::new(&env, &token_id); + + let n = params.capacity as usize; + + // Mint enough per member to cover: + // deposit : 1 x contribution (paid on join) + // round payments : capacity x contribution (if they pay every round) + // top-ups : capacity x contribution (if they top-up every round) + // total : (2 x capacity + 1) x contribution ~= 3 x capacity + // + // SAFETY: capacity <= 24 and contribution <= 1_000_000, so + // 3 x 24 x 1_000_000 = 72_000_000, far below i128::MAX. + let per_member_mint = params.contribution + .saturating_mul(params.capacity as i128 * 3) + .max(params.contribution * 10); + + let members: Vec
= (0..n).map(|_| Address::generate(&env)).collect(); + for m in &members { + minter.mint(m, &per_member_mint); + } + + // -- Phase 1b: circle deployment ----------------------------------------- + let admin = Address::generate(&env); + let contract_id = env.register( + Circle, + ( + admin, + token_id.clone(), + params.contribution, + params.round_seconds, + params.capacity, + ), + ); + let client = CircleClient::new(&env, &contract_id); + let token = token::Client::new(&env, &token_id); + + // -- Phase 2: balance snapshot (I-4 baseline) ---------------------------- + // Capture balances immediately before join so the conservation check uses + // the same reference point regardless of when members were funded. + let balance_before_join: Vec = members.iter().map(|m| token.balance(m)).collect(); + + // -- Phase 3: join ------------------------------------------------------- + for m in &members { + client.join(m); + } + + // -- Phase 4: rounds ----------------------------------------------------- + let mut ledger: Vec = (0..n) + .map(|_| MemberLedger { paid_rounds: 0, defaulted_rounds: 0 }) + .collect(); + + for round_idx in 0..n { + let round_actions = &all_actions[round_idx]; + + // 4a. Apply each member''s action. + for (mi, &action) in round_actions.iter().enumerate() { + match action { + RoundAction::Pay => { + // On-time contribution: transfers `contribution` from + // member to contract. + client.contribute(&members[mi]); + ledger[mi].paid_rounds += 1; + } + RoundAction::Default | RoundAction::DefaultThenTopUp => { + // Do not call contribute. The deposit will cover the gap + // (or be exhausted) when settle runs. + ledger[mi].defaulted_rounds += 1; + } + } + } + + // 4b. Advance the ledger timestamp past the round deadline. + // This ensures settle is never blocked by RoundStillOpen even when + // some members defaulted. + let ends_at = client.get_state().round_ends_at; + env.ledger().set_timestamp(ends_at + 1); + + // 4c. Settle the round. + // settle covers all unpaid contributions from the defaulters'' deposits, + // pays the round''s recipient, and opens the next round. + client.settle(); + + // 4d. Restore deposits for DefaultThenTopUp members. + // + // We use try_top_up rather than top_up because there are cases where + // the deposit is already intact and top_up would correctly reject: + // e.g. a member who was already delinquent with deposit == 0 from a + // prior round -- their deposit stays 0 after settle, but top_up can + // still charge them `contribution` to restore it, so we check + // rec.deposit < contribution explicitly before calling. + for (mi, &action) in round_actions.iter().enumerate() { + if matches!(action, RoundAction::DefaultThenTopUp) { + let rec = client.get_member(&members[mi]).unwrap(); + if rec.deposit < params.contribution { + // Deposit was drawn down. Restore it. + let _ = client.try_top_up(&members[mi]); + } + } + } + } + + // -- Phase 5: invariant assertions --------------------------------------- + + // I-1: The circle must be Complete. + let st = client.get_state(); + if st.status != Status::Complete { + return Err(format!( + "I-1 violated: status is {:?} after {} rounds (expected Complete)", + st.status, params.capacity, + )); + } + + // I-2: Every member must have received their payout. + // `settle` marks received = true on the round''s recipient. If this flag + // is false, the settle loop skipped or exited early for that member. + for (i, m) in members.iter().enumerate() { + let rec = client.get_member(m).unwrap(); + if !rec.received { + return Err(format!( + "I-2 violated: member {i} never received their payout \ + (paid_rounds={}, defaulted_rounds={})", + ledger[i].paid_rounds, ledger[i].defaulted_rounds, + )); + } + } + + // -- Phase 6: withdraw all remaining deposits ---------------------------- + for m in &members { + let rec = client.get_member(m).unwrap(); + if rec.deposit > 0 { + client.withdraw_deposit(m); + } + } + + // -- Phase 7: final invariant checks ------------------------------------- + + // I-3: The contract must hold exactly zero tokens after all withdrawals. + // Tokens held by the contract come from contributions and deposits. Both + // are paid out (contributions to recipients, deposits back to members). + // Any residual indicates a phantom balance. + let contract_balance = token.balance(&contract_id); + if contract_balance != 0 { + return Err(format!( + "I-3 violated: contract holds {contract_balance} stroops after \ + all withdrawals (expected 0)" + )); + } + + // I-4: Token conservation. + // + // Proof sketch: + // No tokens are created or destroyed during the lifecycle. + // join : member -> contract (deposit) + // contribute : member -> contract + // top_up : member -> contract (deposit restore) + // settle : contract -> recipient + // withdraw : contract -> member + // => At any point: sum(member_balance) + contract_balance = const + // => When contract_balance = 0: sum(member_balance) = sum(before_join) + // + // This is logically equivalent to I-3 when the supply is fixed, but + // asserted independently so a failure message names the violated invariant. + let total_before: i128 = balance_before_join.iter().sum(); + let balance_after: Vec = members.iter().map(|m| token.balance(m)).collect(); + let total_after: i128 = balance_after.iter().sum(); + + if total_after != total_before { + return Err(format!( + "I-4 violated: token conservation broken -- \ + total before join = {total_before}, total after all ops = {total_after}, \ + delta = {} stroops", + total_after - total_before, + )); + } + + Ok(()) +} + +// ============================================================================ +// Property tests +// ============================================================================ + +proptest! { + // -- Property A: general accounting soundness ---------------------------- + // + // For any valid circle parameters and any pattern of payments and defaults, + // the accounting invariant holds: every member receives exactly once and + // the contract drains to zero after all deposit withdrawals. + // + // Parameters and the action matrix are generated together via flat_map so + // that the matrix dimensions are always consistent with capacity. Using a + // separate arb_capacity() draw inside arb_all_actions would risk generating + // a matrix sized for a different capacity than the one used to register + // the circle. + #[test] + fn prop_accounting_is_sound( + (params, actions) in arb_circle_params().prop_flat_map(|p| { + arb_all_actions(p.capacity).prop_map(move |a| (p, a)) + }), + ) { + let result = run_circle_scenario(params, &actions); + prop_assert!( + result.is_ok(), + "accounting invariant violated\nparams = {:?}\ncause = {}", + params, + result.unwrap_err(), + ); + } + + // -- Property B: happy-path baseline ------------------------------------- + // + // When every member pays every round on time, all four invariants must + // hold for any valid set of parameters. This is a targeted sanity check: + // if the happy path fails under the harness, the driver itself has a bug, + // not the contract. + #[test] + fn prop_happy_path_always_balances(params in arb_circle_params()) { + let n = params.capacity as usize; + let actions: Vec> = vec![vec![RoundAction::Pay; n]; n]; + let result = run_circle_scenario(params, &actions); + prop_assert!( + result.is_ok(), + "happy-path invariant violated\nparams = {:?}\ncause = {}", + params, + result.unwrap_err(), + ); + } + + // -- Property C: all-default stress test --------------------------------- + // + // When every member defaults on every round, each deposit is drawn down in + // round 1 (deposit == contribution => covered exactly). From round 2 the + // deposit is 0, the member is delinquent, and their contribution to the + // pot is 0. The pots after round 1 are therefore 0, but the contract must + // still end at zero and every member''s received flag must still be set. + // + // This is the scenario most likely to expose an off-by-one in the deposit + // drawdown or delinquency logic. + #[test] + fn prop_all_default_every_round(params in arb_circle_params()) { + let n = params.capacity as usize; + let actions: Vec> = vec![vec![RoundAction::Default; n]; n]; + let result = run_circle_scenario(params, &actions); + prop_assert!( + result.is_ok(), + "all-default invariant violated\nparams = {:?}\ncause = {}", + params, + result.unwrap_err(), + ); + } + + // -- Property D: single rotating defaulter ------------------------------- + // + // Each round, exactly one member defaults while all others pay on time. + // The defaulter rotates: member[r % n] defaults in round r. This exercises + // the deposit-coverage path in a structured way and is the generalised + // version of the hand-written `a_missed_round_is_covered_by_the_defaulters_own_deposit` + // test, extended to all valid capacities and contribution sizes. + #[test] + fn prop_single_rotating_defaulter(params in arb_circle_params()) { + let n = params.capacity as usize; + let actions: Vec> = (0..n) + .map(|r| { + (0..n) + .map(|mi| { + if mi == r % n { + RoundAction::Default + } else { + RoundAction::Pay + } + }) + .collect() + }) + .collect(); + let result = run_circle_scenario(params, &actions); + prop_assert!( + result.is_ok(), + "rotating-defaulter invariant violated\nparams = {:?}\ncause = {}", + params, + result.unwrap_err(), + ); + } + + // -- Property E: deposit restore path ------------------------------------ + // + // Every member defaults every round and then immediately tops up their + // deposit after each settle. This verifies that repeated default -> top_up + // cycles do not corrupt the member record or create phantom balances in + // the contract. + // + // Net flow per member (contribution = c, capacity = n): + // join deposit : -c + // n x default : deposit drawn down by c each time + // n x top_up : +c back into the contract each time + // payout (1 round) : +(n x c) [pot is full since deposits cover] + // withdraw deposit : +c [restored by the last top_up] + // net : -c + n*c - n*c + n*c + c = n*c ... wait + // + // Actually for member[0] in a 3-member circle: + // join : -100 (balance: B-100) + // round 0 default : deposit 100->0 (settle takes 100 from deposit) + // round 0 top_up : -100 (balance: B-200, deposit restored to 100) + // round 0 settle -> member[0] gets pot = 300 (+300, balance: B+100) + // round 1 default : deposit 100->0 + // round 1 top_up : -100 (balance: B) + // round 2 default : deposit 100->0 + // round 2 top_up : -100 (balance: B-100) + // withdraw deposit : +100 (balance: B) + // net : 0 [member ends where they started] CHECK + // + // The conservation invariant must hold across all of these transfers. + #[test] + fn prop_default_then_top_up_every_round(params in arb_circle_params()) { + let n = params.capacity as usize; + let actions: Vec> = + vec![vec![RoundAction::DefaultThenTopUp; n]; n]; + let result = run_circle_scenario(params, &actions); + prop_assert!( + result.is_ok(), + "default-then-top-up invariant violated\nparams = {:?}\ncause = {}", + params, + result.unwrap_err(), + ); + } +}