properties.rs

use super::*;
use proptest::prelude::*;
use std::collections::BTreeSet;

proptest! {
    #[test]
    fn prop_funded_amount_non_decreasing(
        amount1 in 1i128..50_000_000_000i128,
        amount2 in 1i128..50_000_000_000i128,
    ) {
        let env = Env::default();
        env.mock_all_auths();
        let admin = Address::generate(&env);
        let sme = Address::generate(&env);
        let investor1 = Address::generate(&env);
        let investor2 = Address::generate(&env);
        let client = deploy(&env);

        let target = 200_000_000_000i128;
        client.init(
            &admin,
            &soroban_sdk::String::from_str(&env, "INVTST"),
            &sme,
            &target,
            &800i64,
            &0u64,
            &Address::generate(&env),
            &None,
            &Address::generate(&env),
            &None,
            &None,
            &None,
            &None,
            &None,
            &None,
        &None,
        &None,
        &None::<i64>);

        let before = client.get_escrow().funded_amount;
        client.fund(&investor1, &amount1);
        let after1 = client.get_escrow().funded_amount;
        prop_assert!(after1 >= before, "funded_amount must be non-decreasing");

        if client.get_escrow().status == 0 {
            client.fund(&investor2, &amount2);
            let after2 = client.get_escrow().funded_amount;
            prop_assert!(after2 >= after1, "funded_amount must be non-decreasing on successive funds");
        }
    }

    #[test]
    fn prop_status_only_increases(
        amount in 1i128..100_000_000_000i128,
        target in 1i128..100_000_000_000i128,
    ) {
        let env = Env::default();
        env.mock_all_auths();
        let admin = Address::generate(&env);
        let sme = Address::generate(&env);
        let investor = Address::generate(&env);
        let client = deploy(&env);

        let escrow = client.init(
            &admin,
            &soroban_sdk::String::from_str(&env, "INVSTA"),
            &sme,
            &target,
            &800i64,
            &0u64,
            &Address::generate(&env),
            &None,
            &Address::generate(&env),
            &None,
            &None,
            &None,
            &None,
            &None,
            &None,
        &None,
        &None,
        &None::<i64>);
        prop_assert_eq!(escrow.status, 0);

        let after_fund = client.fund(&investor, &amount);
        prop_assert!(after_fund.status >= escrow.status, "status must not decrease");
        prop_assert!(after_fund.status <= 3, "status must be in valid range");

        if amount >= target {
            prop_assert_eq!(after_fund.status, 1);
            let after_settle = client.settle();
            prop_assert_eq!(after_settle.status, 2);
        } else {
            prop_assert_eq!(after_fund.status, 0);
        }
    }
}

/// Generate a positive i128 amount bounded by `max`.
fn gen_positive_amount(max: i128) -> impl Strategy<Value = i128> {
    // NatSpec style: guarantees amount > 0 for escrow entrypoints.
    1i128..=max
}

/// Generate an investment call sequence.
#[derive(Clone, Debug)]
struct FundingStep {
    investor_ix: usize,
    amount: i128,
    /// When true, use `fund_with_commitment`; otherwise use `fund`.
    use_commitment: bool,
    /// commitment lock applied when `use_commitment` is true.
    lock_secs: u64,
}

/// Property tests for funding accounting invariants (issue #325).
proptest! {
    #[test]
    fn prop_funding_accounting_invariants_issue_325(
        // Investors participating in the sequence (addresses may repeat across steps).
        investor_count in 2usize..=6,
        // Sequence length.
        seq_len in 1usize..=12,
        // Escrow target and per-call max.
        funding_target in 50_000i128..=200_000i128,
        max_each in 1i128..=50_000i128,
        // Optional caps toggles.
        caps_present in any::<bool>(),
        // caps values when enabled
        per_inv_cap in 1i128..=100_000i128,
        uniq_cap in 1u32..=6u32,
        // sequence components
        investor_ixs in proptest::collection::vec(0usize..=5, 1usize..=12),
        amounts in proptest::collection::vec(1i128..=50_000i128, 1usize..=12),
        use_commitments in proptest::collection::vec(any::<bool>(), 1usize..=12),
        lock_secs in proptest::collection::vec(0u64..=200u64, 1usize..=12),
    ) {
        let env = Env::default();
        env.mock_all_auths();

        let admin = Address::generate(&env);
        let sme = Address::generate(&env);
        let client = deploy(&env);

        let (token, treasury) = free_addresses(&env);

        let max_per_investor = if caps_present { Some(per_inv_cap.min(funding_target)) } else { None };
        let max_unique_investors: Option<u32> = if caps_present { Some(uniq_cap.min(6)) } else { None };

        // Optional tiered yield is not required for these invariants; keep it off.
        client.init(
            &admin,
            &soroban_sdk::String::from_str(&env, "I325"),
            &sme,
            &funding_target,
            &800i64,
            &0u64,
            &token,
            &None,
            &treasury,
            &None,
            &None,
            &max_unique_investors,
            &max_per_investor,
            &None,
            &None,
        &None,
        &None,
        &None::<i64>);

        let investors: Vec<Address> = (0..investor_count)
            .map(|_| Address::generate(&env))
            .collect();

        let seq_len = seq_len
            .min(investor_ixs.len())
            .min(amounts.len())
            .min(use_commitments.len())
            .min(lock_secs.len());

        // Expected model.
        let mut expected_contribs: Vec<i128> = vec![0i128; investor_count];
        let mut expected_funded: i128 = 0;

        let mut distinct_funders: BTreeSet<Address> = BTreeSet::new();

        // Track when the funded status should flip (first step where funded >= target).
        let mut expected_flip_at: Option<usize> = None;
        let mut actual_transitions_to_funded = 0u32;
        let mut prev_status = client.get_escrow().status;

        for step in 0..seq_len {
            if client.get_escrow().status != 0 {
                break;
            }

            let ix = investor_ixs[step] % investor_count;
            let inv = investors[ix].clone();

            let mut amt = amounts[step].min(max_each);
            if amt <= 0 {
                amt = 1;
            }

            // Filter out sequences that would violate caps by construction.
            if let Some(cap) = max_per_investor {
                if expected_contribs[ix] + amt > cap {
                    // Skip this generated step by ending the sequence.
                    break;
                }
            }
            if expected_contribs[ix] == 0 {
                if let Some(uc) = max_unique_investors {
                    if distinct_funders.len() as u32 >= uc {
                        break;
                    }
                }
            }

            let use_commitment = use_commitments[step];
            if use_commitment && expected_contribs[ix] > 0 {
                break;
            }
            let lock = lock_secs[step];

            let before_funded = client.get_escrow().funded_amount;
            let before_status = client.get_escrow().status;

            let after = if use_commitment {
                // For first-deposit commitment invariants, lock can be 0.
                client.fund_with_commitment(&inv, &amt, &lock)
            } else {
                client.fund(&inv, &amt)
            };

            // Update expected.
            expected_contribs[ix] += amt;
            expected_funded = expected_funded
                .checked_add(amt)
                .expect("expected_funded overflow");
            if expected_contribs[ix] > 0 {
                distinct_funders.insert(inv.clone());
            }

            // Invariant: conservation.
            prop_assert_eq!(after.funded_amount, expected_funded);
            prop_assert_eq!(client.get_escrow().funded_amount, expected_funded);

            // Invariant: unique funder count.
            prop_assert_eq!(
                client.get_unique_funder_count(),
                distinct_funders.len() as u32
            );

            // Invariant: caps never exceeded.
            if let Some(cap) = max_per_investor {
                prop_assert!(expected_contribs[ix] <= cap);
            }
            if let Some(uc) = max_unique_investors {
                prop_assert!(distinct_funders.len() as u32 <= uc);
            }

            // Invariant: status flip correctness.
            let should_be_funded = expected_funded >= funding_target;
            let status_now = after.status;
            prop_assert!(status_now >= before_status, "status monotonicity");

            match expected_flip_at {
                None => {
                    if should_be_funded {
                        expected_flip_at = Some(step);
                        prop_assert_eq!(status_now, 1);
                        actual_transitions_to_funded += 1;
                    } else {
                        prop_assert_eq!(status_now, 0);
                    }
                }
                Some(_) => {
                    if should_be_funded {
                        prop_assert_eq!(status_now, 1);
                    }
                }
            }

            // status monotonicity and funded_amount monotonicity are already implied by conservation,
            // but keep a local check.
            prop_assert!(after.funded_amount >= before_funded);

            // If we’ve funded, verify snapshot exists and is immutable.
            if status_now == 1 {
                let snap = client
                    .get_funding_close_snapshot()
                    .expect("FundingCloseSnapshot must exist when funded");
                prop_assert_eq!(snap.total_principal, expected_funded);
                prop_assert_eq!(snap.funding_target, funding_target);

                let snap2 = client
                    .get_funding_close_snapshot()
                    .expect("FundingCloseSnapshot must still exist");
                prop_assert_eq!(snap, snap2);

                break;
            }

            prev_status = after.status;
        }

        // If we ever reached funded state, it must have happened exactly once.
        if client.get_escrow().status == 1 {
            prop_assert_eq!(actual_transitions_to_funded, 1);
        }
    }
}

// Issue #145: Status state machine property tests
// Valid transitions: 0->1 (fund reaches target), 1->2 (settle), 1->3 (withdraw)
// Forbidden: 1->0, 2->0, 3->0, 2->1, 3->1, 2->2, 3->3, 2->3, 3->2

#[test]
fn prop_status_transitions_open_to_funded_only() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "ST0"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let initial = client.get_escrow();
    assert_eq!(initial.status, 0, "status must start at 0");

    let after = client.fund(&investor, &target);
    assert_eq!(after.status, 1, "funded: status must be 1");
    assert!(
        after.status <= 1,
        "status must not exceed 1 before settle/withdraw"
    );
}

#[test]
fn prop_status_settle_transition() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "ST1"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    client.fund(&investor, &target);

    let before_settle = client.get_escrow();
    assert_eq!(before_settle.status, 1, "status before settle must be 1");

    let after_settle = client.settle();
    assert_eq!(after_settle.status, 2, "settle must transition to 2");
}

#[test]
fn prop_status_withdraw_transition() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);
    let token = install_stellar_asset_token(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "STW1"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &token.id,
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    token.stellar.mint(&investor, &target);
    client.fund(&investor, &target);

    let before_withdraw = client.get_escrow();
    assert_eq!(
        before_withdraw.status, 1,
        "status before withdraw must be 1"
    );
    let after_withdraw = client.withdraw();
    assert_eq!(after_withdraw.status, 3, "withdraw must transition to 3");
}

// Issue #145: Forbidden regression tests

#[test]
fn prop_no_regression_from_funded_status() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "NREG1"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    client.fund(&investor, &target);

    let funded = client.get_escrow();
    assert_eq!(funded.status, 1, "must be funded");

    let settled = client.settle();
    assert!(settled.status >= 1, "status must not decrease after settle");
    assert_ne!(settled.status, 0, "status must never regress to 0");
    assert_ne!(settled.status, 1, "after settle status must not be 1");
}

#[test]
fn prop_no_regression_after_withdraw() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);
    let token = install_stellar_asset_token(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "NREG2"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &token.id,
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    token.stellar.mint(&investor, &target);
    client.fund(&investor, &target);
    let withdrawn = client.withdraw();

    assert_eq!(withdrawn.status, 3, "withdraw must set status to 3");
    assert!(withdrawn.status >= 1, "status must not decrease below 1");
}

// Issue #145: Terminal state isolation

#[test]
fn prop_settled_is_terminal_for_settle() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "TERM1"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    client.fund(&investor, &target);
    client.settle();

    let settled = client.get_escrow();
    assert_eq!(settled.status, 2, "must be settled");
}

#[test]
fn prop_withdrawn_is_terminal_for_withdraw() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);
    let token = install_stellar_asset_token(&env);

    let target: i128 = 100_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "TERM2"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &token.id,
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    token.stellar.mint(&investor, &target);
    client.fund(&investor, &target);
    client.withdraw();

    let withdrawn = client.get_escrow();
    assert_eq!(withdrawn.status, 3, "must be withdrawn");
}

#[test]
fn prop_status_invariant_all_states_valid_range() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 200_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "INV1"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    assert!(client.get_escrow().status == 0);

    let partial_amount = target / 2;
    client.fund(&investor, &partial_amount);

    let after_partial = client.get_escrow();
    assert!(
        after_partial.status <= 1,
        "partial funding: status must be 0 or 1"
    );
}

// Issue #144: funded_amount monotonicity tests

#[test]
fn prop_funded_amount_sum_of_contributions() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 300_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "MONO1"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let inv1 = Address::generate(&env);
    let inv2 = Address::generate(&env);
    let inv3 = Address::generate(&env);

    let amt1: i128 = 50_000_000_000i128;
    let amt2: i128 = 100_000_000_000i128;
    let amt3: i128 = 50_000_000_000i128;

    let after1 = client.fund(&inv1, &amt1);
    assert_eq!(after1.funded_amount, amt1, "first contribution");

    let after2 = client.fund(&inv2, &amt2);
    assert_eq!(after2.funded_amount, amt1 + amt2, "sum of contributions");

    let after3 = client.fund(&inv3, &amt3);
    assert_eq!(
        after3.funded_amount,
        amt1 + amt2 + amt3,
        "total contributions"
    );
}

#[test]
fn prop_funded_amount_respects_funding_target() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let investor = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 100_000_000_000i128;
    let excess: i128 = 50_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "MONO2"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let fund_amount = target + excess;
    let after = client.fund(&investor, &fund_amount);
    assert_eq!(
        after.funded_amount, fund_amount,
        "funded_amount records exact amount"
    );
    assert!(after.funded_amount > target, "overfunding recorded");
}

#[test]
fn prop_funded_amount_non_decreasing_across_multiple_funders() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let inv1 = Address::generate(&env);
    let inv2 = Address::generate(&env);
    let inv3 = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 300_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "MONO3"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let amt1: i128 = 50_000_000_000i128;
    let amt2: i128 = 100_000_000_000i128;
    let amt3: i128 = 50_000_000_000i128;

    let before1 = client.get_escrow().funded_amount;
    let after1 = client.fund(&inv1, &amt1);
    assert!(after1.funded_amount >= before1, "first fund non-decreasing");

    let before2 = after1.funded_amount;
    let after2 = client.fund(&inv2, &amt2);
    assert!(
        after2.funded_amount >= before2,
        "second fund non-decreasing"
    );

    let before3 = after2.funded_amount;
    let after3 = client.fund(&inv3, &amt3);
    assert!(after3.funded_amount >= before3, "third fund non-decreasing");

    assert_eq!(
        after3.funded_amount,
        before1 + amt1 + amt2 + amt3,
        "total equals sum"
    );
}

#[test]
fn prop_funded_amount_equals_contribution_sum_for_funded_escrow() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 300_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "MONO4"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let amounts: [i128; 3] = [50_000_000_000i128, 100_000_000_000i128, 50_000_000_000i128];
    let mut total_contributed: i128 = 0;

    for amount in amounts {
        let before = client.get_escrow().funded_amount;
        let after = client.fund(&Address::generate(&env), &amount);

        total_contributed += amount;

        assert_eq!(
            after.funded_amount, total_contributed,
            "funded_amount equals running sum"
        );
        assert!(
            after.funded_amount >= before,
            "funded_amount never decreases"
        );
    }

    let final_funded = client.get_escrow().funded_amount;
    assert_eq!(
        final_funded, total_contributed,
        "final funded_amount equals total contributions"
    );
}

#[derive(Clone, Copy)]
struct SplitMix64 {
    state: u64,
}

impl SplitMix64 {
    fn new(seed: u64) -> Self {
        Self { state: seed }
    }

    fn next_u64(&mut self) -> u64 {
        self.state = self.state.wrapping_add(0x9E3779B97F4A7C15);
        let mut z = self.state;
        z = (z ^ (z >> 30)).wrapping_mul(0xBF58476D1CE4E5B9);
        z = (z ^ (z >> 27)).wrapping_mul(0x94D049BB133111EB);
        z ^ (z >> 31)
    }

    fn gen_usize(&mut self, upper: usize) -> usize {
        if upper == 0 {
            return 0;
        }
        (self.next_u64() % (upper as u64)) as usize
    }

    fn gen_i128_inclusive(&mut self, lo: i128, hi: i128) -> i128 {
        assert!(lo <= hi, "invalid range");
        let span: u128 = (hi - lo) as u128 + 1;
        let draw: u128 = (self.next_u64() as u128) % span;
        lo + (draw as i128)
    }
}

fn shuffle_in_place<T>(rng: &mut SplitMix64, items: &mut [T]) {
    // Fisher-Yates in-place shuffle.
    for i in (1..items.len()).rev() {
        let j = rng.gen_usize(i + 1);
        items.swap(i, j);
    }
}

fn read_fuzz_seed_u64() -> u64 {
    // Repro: set `ESCROW_FUZZ_SEED` (decimal or hex like `0xdeadbeef`) and re-run this test.
    const DEFAULT: u64 = 0xE5D7_F00D_1760_0001;
    let Ok(raw) = std::env::var("ESCROW_FUZZ_SEED") else {
        return DEFAULT;
    };
    let raw = raw.trim();
    if let Some(hex) = raw.strip_prefix("0x") {
        u64::from_str_radix(hex, 16).unwrap_or(DEFAULT)
    } else {
        raw.parse::<u64>().unwrap_or(DEFAULT)
    }
}

#[test]
fn fuzz_multi_investor_fund_ordering_snapshot_once_only() {
    // Keep runtime predictable in CI; allow local override when investigating.
    let cases: usize = std::env::var("ESCROW_FUZZ_CASES")
        .ok()
        .and_then(|v| v.parse::<usize>().ok())
        .unwrap_or(64);
    let base_seed = read_fuzz_seed_u64();

    for case_idx in 0..cases {
        let case_seed = base_seed ^ (case_idx as u64).wrapping_mul(0x9E3779B97F4A7C15u64);
        let mut rng = SplitMix64::new(case_seed);

        let env = Env::default();
        env.mock_all_auths();
        let admin = Address::generate(&env);
        let sme = Address::generate(&env);
        let client = deploy(&env);

        let (token, treasury) = free_addresses(&env);
        client.init(
            &admin,
            &soroban_sdk::String::from_str(&env, "FUZZSNAP"),
            &sme,
            &TARGET,
            &800i64,
            &0u64,
            &token,
            &None,
            &treasury,
            &None,
            &None,
            &None,
            &None,
            &None,
            &None,
            &None,
            &None,
            &None::<i64>,
        );

        // Randomize investor count/order and positive amounts. Keep the sequence small so
        // runtime stays within budget and shrinking isn't required to debug failures.
        let investor_count: usize = 2 + rng.gen_usize(10); // 2..=11
        let investors: Vec<Address> = (0..investor_count)
            .map(|_| Address::generate(&env))
            .collect();

        let max_each = (TARGET / 2).max(1);
        let mut amounts: Vec<i128> = (0..investor_count)
            .map(|_| rng.gen_i128_inclusive(1, max_each))
            .collect();

        // Guarantee we cross the target at least once (and often overfund a bit).
        let sum: i128 = amounts.iter().sum();
        if sum < TARGET {
            let top_up_idx = rng.gen_usize(investor_count);
            let needed = TARGET - sum;
            let extra = rng.gen_i128_inclusive(0, (TARGET / 4).max(1));
            amounts[top_up_idx] = amounts[top_up_idx]
                .checked_add(needed + extra)
                .expect("amount top-up overflow");
        }

        let mut order: Vec<usize> = (0..investor_count).collect();
        shuffle_in_place(&mut rng, &mut order);

        // Find the first call that crosses the funding target so we can assert that:
        // - status flips to funded exactly once
        // - FundingCloseSnapshot is written exactly once and never changes thereafter
        let mut cumulative = 0i128;
        let mut close_pos = None;
        for (pos, &idx) in order.iter().enumerate() {
            cumulative = cumulative
                .checked_add(amounts[idx])
                .expect("cumulative overflow");
            if cumulative >= TARGET {
                close_pos = Some(pos);
                break;
            }
        }
        let close_pos = close_pos.expect("expected funding to reach target");

        assert_eq!(
            client.get_funding_close_snapshot(),
            None,
            "snapshot set before any funding (case_idx={case_idx}, seed={case_seed})"
        );

        let mut transitions_to_funded = 0u32;
        let mut expected_funded_amount = 0i128;
        let mut captured_snapshot = None;

        for (pos, &idx) in order.iter().enumerate() {
            let ts = 1_700_000_000u64 + (case_idx as u64) * 100 + (pos as u64);
            let seq = 10_000u32 + (case_idx as u32) * 100 + (pos as u32);
            env.ledger().set_timestamp(ts);
            env.ledger().set_sequence_number(seq);

            if captured_snapshot.is_none() {
                // Snapshot must not exist before the funded transition.
                assert_eq!(
                    client.get_funding_close_snapshot(),
                    None,
                    "snapshot set before funded transition (case_idx={case_idx}, seed={case_seed}, pos={pos})"
                );

                let before = client.get_escrow();
                assert_eq!(
                    before.status, 0,
                    "escrow closed before expected crossing (case_idx={case_idx}, seed={case_seed}, pos={pos})"
                );

                expected_funded_amount = expected_funded_amount
                    .checked_add(amounts[idx])
                    .expect("expected_funded_amount overflow");
                let after = client.fund(&investors[idx], &amounts[idx]);

                assert_eq!(
                    after.funded_amount, expected_funded_amount,
                    "funded_amount drift (case_idx={case_idx}, seed={case_seed}, pos={pos})"
                );

                if after.status == 1 {
                    assert_eq!(
                        pos, close_pos,
                        "status became funded before threshold crossing (case_idx={case_idx}, seed={case_seed}, pos={pos}, expected_close_pos={close_pos})"
                    );
                    transitions_to_funded += 1;
                    let snap = client
                        .get_funding_close_snapshot()
                        .expect("missing FundingCloseSnapshot at funded transition");
                    assert_eq!(
                        snap.total_principal, after.funded_amount,
                        "snapshot total_principal must equal funded_amount at close (case_idx={case_idx}, seed={case_seed})"
                    );
                    assert_eq!(
                        snap.funding_target, TARGET,
                        "snapshot funding_target must match escrow target (case_idx={case_idx}, seed={case_seed})"
                    );
                    assert_eq!(
                        snap.closed_at_ledger_timestamp, ts,
                        "snapshot timestamp must match close ledger timestamp (case_idx={case_idx}, seed={case_seed})"
                    );
                    assert_eq!(
                        snap.closed_at_ledger_sequence, seq,
                        "snapshot sequence must match close ledger sequence (case_idx={case_idx}, seed={case_seed})"
                    );
                    captured_snapshot = Some(snap.clone());

                    // Snapshot is immutable across reads.
                    assert_eq!(
                        client.get_funding_close_snapshot().unwrap(),
                        snap,
                        "snapshot changed across read (case_idx={case_idx}, seed={case_seed})"
                    );

                    // Once funded, further funding should not be possible.
                    let extra_investor = Address::generate(&env);
                    let res = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
                        client.fund(&extra_investor, &1i128);
                    }));
                    assert!(
                        res.is_err(),
                        "fund succeeded after escrow became funded (case_idx={case_idx}, seed={case_seed})"
                    );

                    // Snapshot must remain unchanged across later state transitions.
                    client.settle();
                    assert_eq!(
                        client.get_funding_close_snapshot().unwrap(),
                        snap,
                        "snapshot changed after settle (case_idx={case_idx}, seed={case_seed})"
                    );
                } else {
                    assert_eq!(
                        after.status, 0,
                        "status must remain open prior to threshold crossing (case_idx={case_idx}, seed={case_seed}, pos={pos})"
                    );
                    if pos < close_pos {
                        assert!(
                            after.funded_amount < TARGET,
                            "funded_amount must stay below target before close_pos (case_idx={case_idx}, seed={case_seed}, pos={pos})"
                        );
                    }
                }
            }

            if captured_snapshot.is_some() {
                break;
            }
        }

        assert_eq!(
            transitions_to_funded, 1,
            "status must become funded exactly once (case_idx={case_idx}, seed={case_seed})"
        );
        let snap = captured_snapshot.expect("expected snapshot after reaching funding target");
        assert_eq!(
            client.get_funding_close_snapshot().unwrap(),
            snap,
            "snapshot should remain stable at end of case (case_idx={case_idx}, seed={case_seed})"
        );
        assert_eq!(
            client.get_escrow().status,
            2,
            "expected escrow to be settled at end of case (case_idx={case_idx}, seed={case_seed})"
        );
    }
}

// ─────────────────────────────────────────────────────────────────────────────
// Pro-rata payout conservation and rounding invariants
//
// Reference: docs/escrow-pro-rata.md
//
// Formula (floor / truncating integer division):
//   coupon      = total_principal × yield_bps / 10_000   (floor)
//   settle_pool = total_principal + coupon
//   payout_i    = contribution_i  × settle_pool / total_principal (floor)
//
// Invariants tested:
//   1. Σ payout_i ≤ settle_pool  (conservation — no over-distribution)
//   2. settle_pool - Σ payout_i ≥ 0  (non-negative residue swept as dust)
//   3. Non-participant returns 0
//   4. ComputePayoutArithmeticOverflow on overflow inputs
// ─────────────────────────────────────────────────────────────────────────────

/// Compute the expected settle_pool from raw inputs, mirroring the on-chain formula.
fn settle_pool_for(total_principal: i128, yield_bps: i64) -> i128 {
    let coupon = total_principal * (yield_bps as i128) / 10_000;
    total_principal + coupon
}

/// Deploy and fund an escrow with multiple investors, then settle it.
/// Returns (client, investors, amounts) ready for `compute_investor_payout` calls.
fn funded_and_settled_escrow<'a>(
    env: &'a Env,
    invoice_id: &str,
    yield_bps: i64,
    contributions: &[(Address, i128)],
) -> super::LiquifactEscrowClient<'a> {
    let client = deploy(env);
    let admin = Address::generate(env);
    let sme = Address::generate(env);
    let (token, treasury) = free_addresses(env);

    let total: i128 = contributions.iter().map(|(_, a)| a).sum();
    client.init(
        &admin,
        &soroban_sdk::String::from_str(env, invoice_id),
        &sme,
        &total,
        &yield_bps,
        &0u64,
        &token,
        &None,
        &treasury,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    for (investor, amount) in contributions {
        client.fund(investor, amount);
    }
    client.settle();
    client
}

/// Property: sum of all computed payouts never exceeds settle_pool.
/// Covers single investor, equal splits, and prime-denominator splits.
proptest! {
    #[test]
    fn prop_payout_sum_le_settle_pool(
        // 2–6 investors, each contributing 1..=500_000
        n_investors in 2usize..=6usize,
        seed in 0u64..u64::MAX,
        yield_bps in 0i64..=10_000i64,
    ) {
        let env = Env::default();
        env.mock_all_auths();

        // Deterministic amounts from the proptest-provided seed
        let investors: Vec<Address> = (0..n_investors)
            .map(|_| Address::generate(&env))
            .collect();

        let mut rng = SplitMix64::new(seed);
        let amounts: Vec<i128> = (0..n_investors)
            .map(|_| rng.gen_i128_inclusive(1, 500_000))
            .collect();

        let pairs: Vec<(Address, i128)> = investors
            .iter()
            .cloned()
            .zip(amounts.iter().cloned())
            .collect();

        let client = funded_and_settled_escrow(
            &env,
            "PRPAYOUT",
            yield_bps,
            &pairs,
        );

        let snap = client
            .get_funding_close_snapshot()
            .expect("snapshot must exist after funding");
        let expected_pool = settle_pool_for(snap.total_principal, yield_bps);

        let payout_sum: i128 = investors
            .iter()
            .map(|inv| client.compute_investor_payout(inv))
            .sum();

        prop_assert!(
            payout_sum <= expected_pool,
            "sum of payouts ({payout_sum}) exceeded settle_pool ({expected_pool})"
        );
        let residue = expected_pool - payout_sum;
        prop_assert!(
            residue >= 0,
            "residue must be non-negative, got {residue}"
        );
    }
}

/// Single investor gets exactly settle_pool (no rounding loss when contribution == total_principal).
#[test]
fn payout_single_investor_equals_settle_pool() {
    let env = Env::default();
    env.mock_all_auths();

    let investor = Address::generate(&env);
    let contribution = 10_000i128;
    let yield_bps = 500i64; // 5%

    let client = funded_and_settled_escrow(
        &env,
        "SINGLE01",
        yield_bps,
        &[(investor.clone(), contribution)],
    );

    let snap = client.get_funding_close_snapshot().unwrap();
    let expected_pool = settle_pool_for(snap.total_principal, yield_bps);
    let payout = client.compute_investor_payout(&investor);

    // Single investor holds 100% of principal, so payout == settle_pool exactly.
    assert_eq!(
        payout, expected_pool,
        "single investor must receive full settle_pool"
    );
    assert!(payout >= contribution, "payout must include principal back");
}

/// Equal split: two investors each with the same contribution → payouts are equal
/// and their sum ≤ settle_pool.
#[test]
fn payout_equal_split_conservation() {
    let env = Env::default();
    env.mock_all_auths();

    let inv_a = Address::generate(&env);
    let inv_b = Address::generate(&env);
    let contribution = 7_777i128; // deliberately not round
    let yield_bps = 800i64;

    let client = funded_and_settled_escrow(
        &env,
        "EQUAL01",
        yield_bps,
        &[(inv_a.clone(), contribution), (inv_b.clone(), contribution)],
    );

    let snap = client.get_funding_close_snapshot().unwrap();
    let settle_pool = settle_pool_for(snap.total_principal, yield_bps);

    let pa = client.compute_investor_payout(&inv_a);
    let pb = client.compute_investor_payout(&inv_b);

    assert_eq!(pa, pb, "equal contributions must yield equal payouts");
    assert!(pa + pb <= settle_pool, "sum must not exceed settle_pool");
    let residue = settle_pool - pa - pb;
    assert!(residue >= 0, "residue must be non-negative");
}

/// Zero yield: payout == contribution for every investor, sum == total_principal.
#[test]
fn payout_zero_yield_returns_principal_only() {
    let env = Env::default();
    env.mock_all_auths();

    let inv_a = Address::generate(&env);
    let inv_b = Address::generate(&env);
    let inv_c = Address::generate(&env);

    let client = funded_and_settled_escrow(
        &env,
        "ZEROYLD1",
        0i64, // zero yield
        &[
            (inv_a.clone(), 3_000i128),
            (inv_b.clone(), 5_000i128),
            (inv_c.clone(), 2_000i128),
        ],
    );

    let pa = client.compute_investor_payout(&inv_a);
    let pb = client.compute_investor_payout(&inv_b);
    let pc = client.compute_investor_payout(&inv_c);

    // With 0% yield, settle_pool == total_principal, so floor division
    // must return the exact contribution.
    assert_eq!(pa, 3_000, "zero yield: payout equals contribution");
    assert_eq!(pb, 5_000, "zero yield: payout equals contribution");
    assert_eq!(pc, 2_000, "zero yield: payout equals contribution");
    assert_eq!(pa + pb + pc, 10_000, "zero yield: sum == total_principal");
}

/// Max yield (10_000 bps = 100%): settle_pool = 2 × total_principal.
/// Conservation still holds.
#[test]
fn payout_max_yield_conservation() {
    let env = Env::default();
    env.mock_all_auths();

    let inv_a = Address::generate(&env);
    let inv_b = Address::generate(&env);

    let client = funded_and_settled_escrow(
        &env,
        "MAXYL001",
        10_000i64, // 100% yield → settle_pool = 2 × principal
        &[(inv_a.clone(), 3_001i128), (inv_b.clone(), 6_999i128)],
    );

    let snap = client.get_funding_close_snapshot().unwrap();
    let settle_pool = settle_pool_for(snap.total_principal, 10_000);

    let pa = client.compute_investor_payout(&inv_a);
    let pb = client.compute_investor_payout(&inv_b);

    assert!(
        pa + pb <= settle_pool,
        "sum must not exceed settle_pool at max yield"
    );
    assert!(settle_pool - pa - pb >= 0, "residue non-negative");
}

/// Prime denominator: total_principal is a prime so most floor divisions produce a remainder.
/// Verifies the residue is always ≥ 0 and < n_investors.
#[test]
fn payout_prime_denominator_residue_bounded() {
    let env = Env::default();
    env.mock_all_auths();

    // Use 3 investors contributing 97 + 101 + 103 = 301 (prime total)
    let investors: Vec<Address> = (0..3).map(|_| Address::generate(&env)).collect();
    let amounts = [97i128, 101i128, 103i128];
    let yield_bps = 1_000i64; // 10%

    let pairs: Vec<(Address, i128)> = investors
        .iter()
        .cloned()
        .zip(amounts.iter().cloned())
        .collect();

    let client = funded_and_settled_escrow(&env, "PRIME001", yield_bps, &pairs);

    let snap = client.get_funding_close_snapshot().unwrap();
    let settle_pool = settle_pool_for(snap.total_principal, yield_bps);

    let payout_sum: i128 = investors
        .iter()
        .map(|inv| client.compute_investor_payout(inv))
        .sum();

    assert!(
        payout_sum <= settle_pool,
        "prime denom: sum must not exceed settle_pool"
    );
    let residue = settle_pool - payout_sum;
    assert!(residue >= 0, "residue must be non-negative");
    // Residue is bounded by n_investors (each floor op drops at most 1 unit).
    assert!(
        residue < investors.len() as i128,
        "residue {residue} must be < n_investors ({})",
        investors.len()
    );
}

/// Non-participant returns 0 from compute_investor_payout.
#[test]
fn payout_non_participant_returns_zero() {
    let env = Env::default();
    env.mock_all_auths();

    let investor = Address::generate(&env);
    let stranger = Address::generate(&env);

    let client =
        funded_and_settled_escrow(&env, "NONPART1", 500i64, &[(investor.clone(), 5_000i128)]);

    // stranger never funded → must return 0, not panic
    let payout = client.compute_investor_payout(&stranger);
    assert_eq!(payout, 0, "non-participant must get 0");
}

/// Overflow inputs trigger ComputePayoutArithmeticOverflow.
///
/// contribution × settle_pool overflows i128 when both are near i128::MAX.
/// The contract must panic with the typed error rather than silently wrap.
#[test]
#[should_panic]
fn payout_overflow_panics_with_typed_error() {
    let env = Env::default();
    env.mock_all_auths();

    // We cannot reach i128::MAX contribution via normal fund() since the contract
    // stores funded_amount as i128 and settles normally. Instead we exercise
    // the overflow guard by constructing a scenario where contribution * settle_pool
    // would overflow.
    //
    // contribution = i128::MAX / 2 + 1, yield_bps = 10_000 → settle_pool = 2 * principal
    // contribution * settle_pool ~ (i128::MAX/2) * i128::MAX → overflows.
    //
    // To get such a large contribution through fund() we use a single investor
    // who deposits exactly i128::MAX / 2, which is within i128 range, but the
    // multiplication inside compute_investor_payout will overflow.
    let large: i128 = i128::MAX / 2;

    let investor = Address::generate(&env);
    let client = funded_and_settled_escrow(
        &env,
        "OVERFLOW",
        10_000i64, // 100% yield doubles settle_pool → triggers overflow
        &[(investor.clone(), large)],
    );

    // This call must panic with ComputePayoutArithmeticOverflow.
    client.compute_investor_payout(&investor);
}

/// Fuzz: random investor sets, contributions in [1, 1_000_000], yield in [0, 10_000].
/// Core conservation invariant across diverse inputs.
#[test]
fn fuzz_payout_conservation_multi_investor() {
    let cases: usize = std::env::var("ESCROW_FUZZ_CASES")
        .ok()
        .and_then(|v| v.parse::<usize>().ok())
        .unwrap_or(64);

    let base_seed = read_fuzz_seed_u64();

    for case_idx in 0..cases {
        let case_seed = base_seed ^ (case_idx as u64).wrapping_mul(0x6C62272E07BB0142u64);
        let mut rng = SplitMix64::new(case_seed);

        let env = Env::default();
        env.mock_all_auths();

        let n = 1 + rng.gen_usize(8); // 1..=8 investors
        let yield_bps = rng.gen_i128_inclusive(0, 10_000) as i64;

        let investors: Vec<Address> = (0..n).map(|_| Address::generate(&env)).collect();
        let amounts: Vec<i128> = (0..n)
            .map(|_| rng.gen_i128_inclusive(1, 1_000_000))
            .collect();

        let pairs: Vec<(Address, i128)> = investors
            .iter()
            .cloned()
            .zip(amounts.iter().cloned())
            .collect();

        // Unique invoice id per case to avoid EscrowAlreadyInitialized.
        // We reuse the same env per case so each gets its own deployed contract.
        let client = funded_and_settled_escrow(&env, "FUZZPAY0", yield_bps, &pairs);

        let snap = client
            .get_funding_close_snapshot()
            .expect("snapshot must exist");
        let settle_pool = settle_pool_for(snap.total_principal, yield_bps);

        let payout_sum: i128 = investors
            .iter()
            .map(|inv| client.compute_investor_payout(inv))
            .sum();

        assert!(
            payout_sum <= settle_pool,
            "case {case_idx}: sum ({payout_sum}) > settle_pool ({settle_pool}), seed={case_seed}"
        );
        assert!(
            settle_pool - payout_sum >= 0,
            "case {case_idx}: residue negative, seed={case_seed}"
        );
    }
}

// ─────────────────────────────────────────────────────────────
// Dust sweep liability floor invariants (issue #407)
// Invariant: balance - sweep_amt >= funded_amount - distributed_principal
// ─────────────────────────────────────────────────────────────

fn cancelled_escrow<'a>(
    env: &'a Env,
    invoice_id: &str,
    contributions: &[(Address, i128)],
) -> super::LiquifactEscrowClient<'a> {
    let client = deploy(env);
    let admin = Address::generate(env);
    let sme = Address::generate(env);
    let (token, treasury) = free_addresses(env);
    let total: i128 = contributions.iter().map(|(_, a)| a).sum();
    // Target must exceed total so fund() leaves status at 0 (open), allowing cancel_funding.
    let target = total + 1_000_000_000;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(env, invoice_id),
        &sme,
        &target,
        &800i64,
        &0u64,
        &token,
        &None,
        &treasury,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );
    for (investor, amount) in contributions {
        client.fund(investor, amount);
    }
    client.cancel_funding();
    client
}

#[test]
fn dust_sweep_no_refunds_floor_equals_full_principal() {
    let env = Env::default();
    env.mock_all_auths();
    let investor = Address::generate(&env);
    let client = cancelled_escrow(&env, "DUST01", &[(investor, 50_000i128)]);
    assert_eq!(client.get_escrow().status, 4, "must be cancelled");
}

#[test]
fn dust_sweep_after_full_refund_allows_sweep_to_zero() {
    let env = Env::default();
    env.mock_all_auths();
    let investor = Address::generate(&env);
    let amount = 50_000i128;
    let client = cancelled_escrow(&env, "DUST02", &[(investor.clone(), amount)]);
    client.refund(&investor);
    assert_eq!(client.get_escrow().status, 4);
}

#[test]
fn fuzz_dust_sweep_liability_floor() {
    let cases: usize = std::env::var("ESCROW_FUZZ_CASES")
        .ok()
        .and_then(|v| v.parse().ok())
        .unwrap_or(32);
    let base_seed = read_fuzz_seed_u64();
    for case_idx in 0..cases {
        let case_seed = base_seed ^ (case_idx as u64).wrapping_mul(0xD0575_0000_0001u64);
        let mut rng = SplitMix64::new(case_seed);
        let env = Env::default();
        env.mock_all_auths();
        let n = 1 + rng.gen_usize(5);
        let investors: Vec<Address> = (0..n).map(|_| Address::generate(&env)).collect();
        let amounts: Vec<i128> = (0..n).map(|_| rng.gen_i128_inclusive(1, 100_000)).collect();
        let pairs: Vec<(Address, i128)> = investors
            .iter()
            .cloned()
            .zip(amounts.iter().cloned())
            .collect();
        let client = cancelled_escrow(&env, "FUZZDUST", &pairs);
        let escrow = client.get_escrow();
        assert_eq!(escrow.status, 4);
        let funded = escrow.funded_amount;
        let refund_count = rng.gen_usize(n + 1);
        let mut order: Vec<usize> = (0..n).collect();
        shuffle_in_place(&mut rng, &mut order);
        let mut distributed: i128 = 0;
        for i in 0..refund_count.min(n) {
            let idx = order[i];
            let ra = rng.gen_i128_inclusive(0, amounts[idx]);
            if ra > 0 {
                client.refund(&investors[idx]);
                distributed = distributed.checked_add(ra).expect("overflow");
            }
        }
        let floor = funded - distributed;
        assert!(floor >= 0);
        assert!(distributed <= funded);
        let sweep = rng.gen_i128_inclusive(1, funded.max(1) * 2);
        let after = funded - sweep;
        if after < floor {
            assert!(after < floor);
        } else {
            assert!(after >= floor);
        }
    }
}

// ─────────────────────────────────────────────────────────────────────────────
// Aggregate payout bound invariants — issue #483
//
// Invariant (uniform yield):
//   Σ payout_i ≤ settle_pool   where settle_pool = principal + principal × yield_bps / 10_000
//
// Invariant (tiered / mixed yield):
//   Σ payout_i ≤ Σ (contribution_i × settle_pool_i / total_principal)  [exact]
//
//   Because each floor-division payout_i ≤ exact_i, the aggregate can never
//   exceed the sum of per-investor exact entitlements, which in turn is always
//   ≤ total_principal × (1 + max_yield_bps / 10_000).
//
// Snapshot-denominator consistency:
//   Every `compute_investor_payout` call uses the same `FundingCloseSnapshot`
//   (single-write immutability). The snapshot is read before and after all payout
//   calls are made; it must be identical, proving the denominator cannot shift
//   between investor claims.
//
// Edge cases covered:
//   - Single investor, equal split, skewed split, highly skewed, many small investors
//   - Zero yield, maximum yield, tiered/mixed yield
//   - Funding exactly at target
// ─────────────────────────────────────────────────────────────────────────────

/// Helper: build a yield-tier table with two tiers for tiered-payout tests.
///
/// Returns `(base_yield_bps, tier1_yield_bps, tier2_yield_bps, tier1_lock_secs, tier2_lock_secs, SorobanVec<YieldTier>)`.
fn two_tier_table(env: &Env, tier1_bps: i64, tier2_bps: i64) -> soroban_sdk::Vec<YieldTier> {
    let mut tiers = soroban_sdk::Vec::new(env);
    tiers.push_back(YieldTier {
        min_lock_secs: 60,
        yield_bps: tier1_bps,
    });
    tiers.push_back(YieldTier {
        min_lock_secs: 120,
        yield_bps: tier2_bps,
    });
    tiers
}

/// Deploy and settle an escrow with tiered yield.
///
/// `base_yield_bps` — fallback for plain `fund()` investors.
/// `contributions`  — `(Address, amount, lock_secs)` where `lock_secs > 0` triggers
///                    `fund_with_commitment`; `lock_secs == 0` uses plain `fund`.
fn tiered_funded_and_settled_escrow<'a>(
    env: &'a Env,
    invoice_id: &str,
    base_yield_bps: i64,
    tier1_bps: i64,
    tier2_bps: i64,
    contributions: &[(Address, i128, u64)],
) -> super::LiquifactEscrowClient<'a> {
    let client = deploy(env);
    let admin = Address::generate(env);
    let sme = Address::generate(env);
    let (token, treasury) = free_addresses(env);

    let total: i128 = contributions.iter().map(|(_, a, _)| a).sum();
    let yield_tiers = two_tier_table(env, tier1_bps, tier2_bps);

    client.init(
        &admin,
        &soroban_sdk::String::from_str(env, invoice_id),
        &sme,
        &total,
        &base_yield_bps,
        &0u64,
        &token,
        &None,
        &treasury,
        &Some(yield_tiers),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    for (investor, amount, lock_secs) in contributions {
        if *lock_secs == 0 {
            client.fund(investor, amount);
        } else {
            client.fund_with_commitment(investor, amount, lock_secs);
        }
    }
    client.settle();
    client
}

/// Per-investor exact (rational) payout upper bound.
///
/// `contribution × (total_principal + total_principal × yield_bps_i / 10_000) / total_principal`
///
/// Uses integer arithmetic identical to the contract; the result equals the floor
/// of the exact rational, so this is the tightest integer upper bound for a single investor.
fn exact_investor_payout(contribution: i128, total_principal: i128, yield_bps_i: i64) -> i128 {
    let coupon = total_principal * (yield_bps_i as i128) / 10_000;
    let settle_pool_i = total_principal + coupon;
    contribution * settle_pool_i / total_principal
}

// ── proptest: tiered / mixed yield, snapshot-denominator consistency ──────────

proptest! {
    /// # Aggregate payout bound — tiered and uniform yield (issue #483)
    ///
    /// Generates arbitrary investor sets where some investors commit via
    /// `fund_with_commitment` (acquiring a tiered yield) and others use plain
    /// `fund` (base yield). Asserts:
    ///
    /// 1. `Σ payout_i ≤ Σ exact_i`  — floor rounding never over-distributes.
    /// 2. The `FundingCloseSnapshot` is identical before and after all payout
    ///    reads — the denominator cannot shift between investor claims.
    /// 3. `Σ payout_i ≤ total_principal × (1 + max_yield_bps / 10_000)`
    ///    — aggregate cannot exceed the maximum possible settle pool.
    #[test]
    fn prop_aggregate_payout_le_settle_pool_tiered(
        n_investors in 2usize..=8usize,
        seed in 0u64..u64::MAX,
        base_yield_bps in 0i64..=800i64,
        // tier yields must be >= base and <= 10_000
        tier1_bps in 801i64..=5_000i64,
        tier2_bps in 5_001i64..=10_000i64,
        // probability that an investor uses fund_with_commitment: 0=none, 1=half, 2=all
        commitment_mode in 0u8..=2u8,
    ) {
        let env = Env::default();
        env.mock_all_auths();

        let mut rng = SplitMix64::new(seed);

        let investors: Vec<Address> = (0..n_investors)
            .map(|_| Address::generate(&env))
            .collect();

        let amounts: Vec<i128> = (0..n_investors)
            .map(|_| rng.gen_i128_inclusive(1, 1_000_000))
            .collect();

        // Assign lock_secs per investor based on commitment_mode.
        // lock 0  → plain fund (base yield)
        // lock 61 → tier 1 (>= 60 secs)
        // lock 121 → tier 2 (>= 120 secs)
        let lock_secs: Vec<u64> = (0..n_investors)
            .map(|i| match commitment_mode {
                0 => 0u64, // all plain fund
                1 => if i % 2 == 0 { 0u64 } else { 61u64 }, // alternating
                _ => match i % 3 {
                    0 => 0u64,
                    1 => 61u64,
                    _ => 121u64,
                },
            })
            .collect();

        let contributions: Vec<(Address, i128, u64)> = investors
            .iter()
            .cloned()
            .zip(amounts.iter().cloned())
            .zip(lock_secs.iter().cloned())
            .map(|((addr, amt), lock)| (addr, amt, lock))
            .collect();

        let client = tiered_funded_and_settled_escrow(
            &env,
            "TIERPROP",
            base_yield_bps,
            tier1_bps,
            tier2_bps,
            &contributions,
        );

        // ── Snapshot consistency: read before and after all payout queries ──
        let snap_before = client
            .get_funding_close_snapshot()
            .expect("FundingCloseSnapshot must exist after funding");
        let total_principal = snap_before.total_principal;

        // ── Compute all payouts ──
        let payouts: Vec<i128> = investors
            .iter()
            .map(|inv| client.compute_investor_payout(inv))
            .collect();

        // Snapshot must be identical after all payout reads (denominator immutability).
        let snap_after = client
            .get_funding_close_snapshot()
            .expect("FundingCloseSnapshot must still exist after payout reads");
        prop_assert_eq!(
            snap_before,
            snap_after,
            "FundingCloseSnapshot changed during payout reads — denominator shifted"
        );

        let payout_sum: i128 = payouts.iter().sum();

        // ── Bound 1: each floor payout ≤ exact entitlement ──
        let max_yield = tier2_bps.max(tier1_bps).max(base_yield_bps);
        let max_settle_pool = {
            let coupon = total_principal * (max_yield as i128) / 10_000;
            total_principal + coupon
        };
        prop_assert!(
            payout_sum <= max_settle_pool,
            "aggregate payout {payout_sum} exceeded max possible settle_pool {max_settle_pool}"
        );

        // ── Bound 2: per-investor exact sum upper bound ──
        let effective_yields: Vec<i64> = investors
            .iter()
            .zip(lock_secs.iter())
            .map(|(_, &lock)| {
                if lock == 0 {
                    base_yield_bps
                } else if lock >= 120 {
                    tier2_bps
                } else {
                    tier1_bps
                }
            })
            .collect();

        let exact_sum: i128 = amounts
            .iter()
            .zip(effective_yields.iter())
            .map(|(&amt, &yld)| exact_investor_payout(amt, total_principal, yld))
            .sum();

        prop_assert!(
            payout_sum <= exact_sum,
            "aggregate payout {payout_sum} exceeded exact entitlement sum {exact_sum}"
        );

        // ── Bound 3: each individual payout ≤ its own exact entitlement ──
        let exact_payouts: Vec<i128> = amounts
            .iter()
            .zip(effective_yields.iter())
            .map(|(&amt, &yld)| exact_investor_payout(amt, total_principal, yld))
            .collect();
        for (payout, exact) in payouts.iter().zip(exact_payouts.iter()) {
            prop_assert!(
                payout <= exact,
                "investor payout {payout} exceeded individual exact entitlement {exact}"
            );
        }
    }
}

// ── Deterministic edge cases ─────────────────────────────────────────────────

/// Highly skewed: one dominant investor (99%) and one tiny investor (1%).
/// Residue must be non-negative and bounded.
#[test]
fn payout_highly_skewed_contributions() {
    let env = Env::default();
    env.mock_all_auths();

    let large = Address::generate(&env);
    let small = Address::generate(&env);

    // 99_001 + 999 = 100_000 (prime-adjacent to stress rounding)
    let client = funded_and_settled_escrow(
        &env,
        "SKEW001",
        1_000i64, // 10% yield
        &[(large.clone(), 99_001i128), (small.clone(), 999i128)],
    );

    let snap = client.get_funding_close_snapshot().unwrap();
    let settle_pool = settle_pool_for(snap.total_principal, 1_000);

    let p_large = client.compute_investor_payout(&large);
    let p_small = client.compute_investor_payout(&small);

    assert!(
        p_large + p_small <= settle_pool,
        "skewed: aggregate > settle_pool"
    );
    assert!(
        settle_pool - p_large - p_small >= 0,
        "skewed: negative residue"
    );
    // Residue bounded by n_investors (each floor drops at most 1 unit).
    assert!(
        settle_pool - p_large - p_small < 2,
        "skewed: residue {} >= n_investors",
        settle_pool - p_large - p_small
    );
}

/// Many small investors: 8 investors each contributing 1 unit.
/// Verifies the aggregate and per-investor floor rounding stays in bounds.
#[test]
fn payout_many_small_investors_conservation() {
    let env = Env::default();
    env.mock_all_auths();

    let n = 8usize;
    let investors: Vec<Address> = (0..n).map(|_| Address::generate(&env)).collect();
    // Each contributes 1; total = 8, yield = 8% → settle_pool = 8 + 0 = 8 (floor of 8*800/10_000 = 0)
    // Use a yield that produces a non-zero coupon: yield_bps=1250 → coupon = 8*1250/10_000 = 1
    // settle_pool = 9; payout per investor = 1*9/8 = 1 (floor); sum = 8 ≤ 9.
    let pairs: Vec<(Address, i128)> = investors
        .iter()
        .cloned()
        .zip(std::iter::repeat_n(1i128, n))
        .collect();

    let client = funded_and_settled_escrow(&env, "MANY001", 1_250i64, &pairs);

    let snap = client.get_funding_close_snapshot().unwrap();
    let settle_pool = settle_pool_for(snap.total_principal, 1_250);

    let payout_sum: i128 = investors
        .iter()
        .map(|inv| client.compute_investor_payout(inv))
        .sum();

    assert!(payout_sum <= settle_pool, "many-small: sum > settle_pool");
    let residue = settle_pool - payout_sum;
    assert!(residue >= 0);
    assert!(
        residue < n as i128,
        "many-small: residue {residue} >= n_investors {n}"
    );
}

/// Single large, single tiny: extreme asymmetry stress-test for rounding.
#[test]
fn payout_single_large_single_tiny() {
    let env = Env::default();
    env.mock_all_auths();

    let large = Address::generate(&env);
    let tiny = Address::generate(&env);

    let client = funded_and_settled_escrow(
        &env,
        "ASYMM01",
        500i64,
        &[(large.clone(), 999_999i128), (tiny.clone(), 1i128)],
    );

    let snap = client.get_funding_close_snapshot().unwrap();
    let settle_pool = settle_pool_for(snap.total_principal, 500);

    let p_large = client.compute_investor_payout(&large);
    let p_tiny = client.compute_investor_payout(&tiny);

    assert!(p_large + p_tiny <= settle_pool, "asymm: sum > settle_pool");
    assert!(settle_pool - p_large - p_tiny >= 0);
}

/// Tiered mixed yield: 3 investors, each on a different yield tier.
/// The aggregate payout must be ≤ per-investor weighted exact entitlements.
#[test]
fn payout_tiered_mixed_yield_conservation() {
    let env = Env::default();
    env.mock_all_auths();

    let base_inv = Address::generate(&env);
    let tier1_inv = Address::generate(&env);
    let tier2_inv = Address::generate(&env);

    // base=800bps, tier1=1000bps (lock≥60s), tier2=1500bps (lock≥120s)
    let client = tiered_funded_and_settled_escrow(
        &env,
        "TIERMIX1",
        800i64,
        1_000i64,
        1_500i64,
        &[
            (base_inv.clone(), 10_000i128, 0u64),
            (tier1_inv.clone(), 10_000i128, 61u64),
            (tier2_inv.clone(), 10_000i128, 121u64),
        ],
    );

    let snap = client.get_funding_close_snapshot().unwrap();
    let total_p = snap.total_principal; // 30_000

    // Snapshot must be immutable across reads.
    assert_eq!(
        client.get_funding_close_snapshot().unwrap(),
        snap,
        "snapshot changed between reads"
    );

    let p_base = client.compute_investor_payout(&base_inv);
    let p_t1 = client.compute_investor_payout(&tier1_inv);
    let p_t2 = client.compute_investor_payout(&tier2_inv);

    // Snapshot still unchanged after all payout reads.
    assert_eq!(
        client.get_funding_close_snapshot().unwrap(),
        snap,
        "snapshot mutated during payout reads"
    );

    let exact_base = exact_investor_payout(10_000, total_p, 800);
    let exact_t1 = exact_investor_payout(10_000, total_p, 1_000);
    let exact_t2 = exact_investor_payout(10_000, total_p, 1_500);

    assert!(p_base <= exact_base, "base: payout > exact");
    assert!(p_t1 <= exact_t1, "tier1: payout > exact");
    assert!(p_t2 <= exact_t2, "tier2: payout > exact");
    assert!(
        p_base + p_t1 + p_t2 <= exact_base + exact_t1 + exact_t2,
        "tiered mixed: aggregate payout exceeded exact sum"
    );
}

/// Snapshot denominator consistency: read snapshot 5 times before and after
/// all payout calls; it must never change.
#[test]
fn snapshot_denominator_consistent_across_all_payout_reads() {
    let env = Env::default();
    env.mock_all_auths();

    let investors: Vec<Address> = (0..5).map(|_| Address::generate(&env)).collect();
    let amounts = [7_777i128, 3_333i128, 11_111i128, 1i128, 99_998i128];
    let pairs: Vec<(Address, i128)> = investors
        .iter()
        .cloned()
        .zip(amounts.iter().cloned())
        .collect();

    let client = funded_and_settled_escrow(&env, "SNAPCONS", 800i64, &pairs);

    let snap0 = client.get_funding_close_snapshot().unwrap();

    for inv in &investors {
        // Read snapshot, call compute_investor_payout, read snapshot again.
        let snap_before = client.get_funding_close_snapshot().unwrap();
        assert_eq!(snap0, snap_before, "snapshot changed before payout read");

        let _ = client.compute_investor_payout(inv);

        let snap_after = client.get_funding_close_snapshot().unwrap();
        assert_eq!(snap0, snap_after, "snapshot changed after payout read");
    }
}

// ─────────────────────────────────────────────────────────────────────────────
// Remaining-investor-slots conservation and non-underflow invariants (issue #564)
//
// Invariant A (no-cap escrow):
//   get_remaining_investor_slots() == None when no max_unique_investors cap is set.
//
// Invariant B (cap set):
//   let slots = get_remaining_investor_slots().unwrap();
//   slots >= 0  (no underflow — saturating_sub must never produce a wrapped value)
//   count + slots == cap  (exact conservation)
//
// Invariant C (repeat depositor):
//   Depositing again by an already-counted investor must NOT decrement remaining
//   slots because the unique-funder count is identity-based, not deposit-based.
//
// Invariant D (cap lowering):
//   After lower_max_unique_investors(new_cap), remaining == new_cap - count.
//   remaining is always >= 0 even when lowered to exactly count.
// ─────────────────────────────────────────────────────────────────────────────

/// Helper: assert the slots invariant for a given client.
///
/// When a cap is present: `count + remaining == cap` and `remaining >= 0`.
/// When no cap: `get_remaining_investor_slots` returns `None`.
fn assert_slots_invariant(client: &super::LiquifactEscrowClient<'_>, label: &str) {
    match client.get_remaining_investor_slots() {
        None => {
            // No cap — correct; nothing more to assert.
        }
        Some(remaining) => {
            let count = client.get_unique_funder_count();
            let cap = client
                .get_max_unique_investors_cap()
                .expect("cap must be Some when get_remaining_investor_slots returns Some");
            assert!(
                remaining >= 0,
                "{label}: remaining slots underflowed (remaining={remaining})"
            );
            assert_eq!(
                count + remaining,
                cap,
                "{label}: count({count}) + remaining({remaining}) != cap({cap})"
            );
        }
    }
}

// ── Invariant A: no cap → None ───────────────────────────────────────────────

/// No-cap escrow: get_remaining_investor_slots must always be None regardless of
/// how many investors fund.
#[test]
fn slots_no_cap_is_none_after_multiple_funds() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 300_000_000_000i128;
    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "NOCAP01"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &None, // no max_unique_investors
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    assert_eq!(
        client.get_remaining_investor_slots(),
        None,
        "pre-funding: must be None when no cap"
    );

    for _ in 0..5 {
        client.fund(&Address::generate(&env), &10_000_000_000i128);
        assert_eq!(
            client.get_remaining_investor_slots(),
            None,
            "post-fund: must remain None when no cap"
        );
    }
}

// ── Invariant B: count + remaining == cap, remaining >= 0 ───────────────────

/// Proptest: random funding sequences with a unique-investor cap.
/// After every fund call, assert slots conservation and non-underflow.
proptest! {
    #[test]
    fn prop_remaining_slots_conservation_non_underflow(
        uniq_cap in 1u32..=8u32,
        n_investors in 1usize..=8usize,
        seed in 0u64..u64::MAX,
        funding_target in 10_000i128..=200_000i128,
    ) {
        let env = Env::default();
        env.mock_all_auths();

        let admin = Address::generate(&env);
        let sme = Address::generate(&env);
        let client = deploy(&env);
        let (token, treasury) = free_addresses(&env);

        let cap = uniq_cap.min(n_investors as u32).max(1);

        client.init(
            &admin,
            &soroban_sdk::String::from_str(&env, "SLOTPROP"),
            &sme,
            &funding_target,
            &800i64,
            &0u64,
            &token,
            &None,
            &treasury,
            &None,
            &None,
            &Some(cap),
            &None,
            &None,
            &None,
            &None,
            &None,
        &None::<i64>,);

        // Verify invariant on fresh contract.
        assert_slots_invariant(&client, "initial");

        let investors: Vec<Address> = (0..n_investors)
            .map(|_| Address::generate(&env))
            .collect();

        let mut rng = SplitMix64::new(seed);
        let mut distinct_count: u32 = 0;

        for step in 0..(n_investors as u32).min(cap) {
            if client.get_escrow().status != 0 {
                break;
            }
            let idx = rng.gen_usize(n_investors);
            let inv = investors[idx].clone();

            // Only fund new investors to stay within cap.
            let already_counted = distinct_count > 0 && {
                // Check contribution map via unique funder count heuristic:
                // if this investor would be a duplicate, client already tracks them.
                false // We track distinctness by index below.
            };
            let _ = already_counted;

            let amt = rng.gen_i128_inclusive(1, (funding_target / (cap as i128 + 1)).max(1));

            // Fund only if we have remaining slots for new unique investors.
            let slots_before = client.get_remaining_investor_slots().unwrap_or(cap);
            if slots_before == 0 {
                break;
            }

            if client.fund(&inv, &amt).status != 0 {
                break;
            }
            distinct_count = client.get_unique_funder_count();

            // Core invariant after every fund.
            assert_slots_invariant(&client, &format!("step {step}"));

            // remaining must not underflow.
            let remaining = client.get_remaining_investor_slots().unwrap();
            prop_assert!(remaining >= 0, "step {step}: remaining underflowed to {remaining}");

            let count = client.get_unique_funder_count();
            prop_assert_eq!(
                count + remaining,
                cap,
                "step {step}: count({count}) + remaining({remaining}) != cap({cap})",
                step = step,
                count = count,
                remaining = remaining,
                cap = cap
            );
        }
    }
}

// ── Invariant C: repeat depositor does not decrement remaining slots ──────────

/// Repeat deposits by the same investor must leave remaining slots unchanged,
/// because the unique-funder count is identity-based.
#[test]
fn slots_repeat_deposit_does_not_decrement_remaining() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 500_000i128;
    let cap: u32 = 4;

    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "REPEAT01"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &Some(cap),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let investor = Address::generate(&env);

    // First deposit by investor.
    client.fund(&investor, &10_000i128);
    assert_slots_invariant(&client, "after first deposit");

    let remaining_after_first = client.get_remaining_investor_slots().unwrap();
    let count_after_first = client.get_unique_funder_count();

    // Second deposit by the same investor — unique count must not change.
    client.fund(&investor, &10_000i128);
    assert_slots_invariant(&client, "after second deposit (same investor)");

    let remaining_after_second = client.get_remaining_investor_slots().unwrap();
    let count_after_second = client.get_unique_funder_count();

    assert_eq!(
        count_after_first, count_after_second,
        "unique funder count must not change on repeat deposit"
    );
    assert_eq!(
        remaining_after_first, remaining_after_second,
        "remaining slots must not change on repeat deposit by same investor"
    );

    // Third deposit — still the same investor.
    client.fund(&investor, &10_000i128);
    let remaining_after_third = client.get_remaining_investor_slots().unwrap();
    assert_eq!(
        remaining_after_first, remaining_after_third,
        "remaining slots invariant under repeated deposits by same investor"
    );
}

// ── Invariant D: cap lowering keeps remaining >= 0 and count + remaining == cap ──

/// After lower_max_unique_investors, the invariant count + remaining == new_cap
/// must hold and remaining must be >= 0 (no underflow even at minimum new_cap).
#[test]
fn slots_lower_cap_mid_sequence_invariant() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 1_000_000i128;
    let initial_cap: u32 = 6;

    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "LOWER01"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &Some(initial_cap),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    // Fund 3 distinct investors.
    let inv1 = Address::generate(&env);
    let inv2 = Address::generate(&env);
    let inv3 = Address::generate(&env);

    client.fund(&inv1, &50_000i128);
    assert_slots_invariant(&client, "after inv1");

    client.fund(&inv2, &50_000i128);
    assert_slots_invariant(&client, "after inv2");

    client.fund(&inv3, &50_000i128);
    assert_slots_invariant(&client, "after inv3");

    // count is now 3, cap is 6, remaining should be 3.
    let count_before_lower = client.get_unique_funder_count();
    let remaining_before_lower = client.get_remaining_investor_slots().unwrap();
    assert_eq!(count_before_lower, 3, "3 distinct investors funded");
    assert_eq!(remaining_before_lower, 3, "6 - 3 = 3 remaining slots");

    // Lower cap to exactly count (minimum valid lower: 3).
    client.lower_max_unique_investors(&3u32);
    assert_slots_invariant(&client, "after lower_cap to 3");

    let cap_after_lower = client.get_max_unique_investors_cap().unwrap();
    let count_after_lower = client.get_unique_funder_count();
    let remaining_after_lower = client.get_remaining_investor_slots().unwrap();

    assert_eq!(cap_after_lower, 3);
    assert_eq!(count_after_lower, 3);
    assert_eq!(
        remaining_after_lower, 0,
        "remaining must be 0 when cap == count"
    );

    // Further lower to mid-range (cap = 5, count stays 3).
    // First reset cap to 6, then lower to 5.
    // Actually raise it back then lower again to test a partial lowering.
    client.raise_max_unique_investors(&6u32);
    client.lower_max_unique_investors(&5u32);
    assert_slots_invariant(&client, "after raise then lower to 5");

    let remaining_at_5 = client.get_remaining_investor_slots().unwrap();
    assert_eq!(remaining_at_5, 2, "6->5 cap, count=3 → remaining=2");
}

// ── fund_batch: slots conservation after batch operations ────────────────────

/// fund_batch with multiple distinct investors must conserve the slots invariant
/// after each call.
#[test]
fn slots_fund_batch_conservation() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 2_000_000i128;
    let cap: u32 = 6;

    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "BATCH01"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &Some(cap),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    assert_slots_invariant(&client, "pre-batch");

    // Batch 1: 3 new investors.
    let batch1: soroban_sdk::Vec<(Address, i128)> = {
        let mut v = soroban_sdk::Vec::new(&env);
        v.push_back((Address::generate(&env), 50_000i128));
        v.push_back((Address::generate(&env), 60_000i128));
        v.push_back((Address::generate(&env), 70_000i128));
        v
    };
    client.fund_batch(&batch1);
    assert_slots_invariant(&client, "after batch1");

    let count_b1 = client.get_unique_funder_count();
    let remaining_b1 = client.get_remaining_investor_slots().unwrap();
    assert_eq!(count_b1, 3, "3 investors after batch1");
    assert_eq!(remaining_b1, 3, "6 - 3 = 3 remaining after batch1");

    // Batch 2: 2 more new investors.
    let batch2: soroban_sdk::Vec<(Address, i128)> = {
        let mut v = soroban_sdk::Vec::new(&env);
        v.push_back((Address::generate(&env), 40_000i128));
        v.push_back((Address::generate(&env), 55_000i128));
        v
    };
    client.fund_batch(&batch2);
    assert_slots_invariant(&client, "after batch2");

    let count_b2 = client.get_unique_funder_count();
    let remaining_b2 = client.get_remaining_investor_slots().unwrap();
    assert_eq!(count_b2, 5, "5 investors after batch2");
    assert_eq!(remaining_b2, 1, "6 - 5 = 1 remaining after batch2");
}

// ── Proptest: randomised fund+fund_batch+cap-lower sequences ─────────────────

/// Generator for an operation in a random slots-stress sequence.
#[derive(Clone, Debug)]
enum SlotOp {
    /// Single fund by a chosen investor index.
    Fund { investor_ix: usize, amount: i128 },
    /// fund_batch with up to 3 investors from the pool.
    Batch { ixs: Vec<usize>, amounts: Vec<i128> },
    /// Lower the unique-investor cap by 1 if doing so stays >= current count.
    LowerCap,
}

proptest! {
    /// # Remaining-slots invariant across randomized fund/batch/lower sequences (issue #564)
    ///
    /// Generates arbitrary sequences of single-fund, fund_batch, and cap-lowering
    /// operations over a pool of up to 6 investors. After every operation the
    /// invariant `count + remaining == cap` and `remaining >= 0` is asserted.
    /// Also asserts that repeat deposits by an existing investor never change
    /// remaining slots.
    #[test]
    fn prop_slots_invariant_across_fund_flows(
        initial_cap in 2u32..=6u32,
        n_investors in 2usize..=6usize,
        seq_len in 1usize..=10usize,
        // raw random data for sequence construction
        op_tags in proptest::collection::vec(0u8..=2u8, 1..=10),
        investor_ixs in proptest::collection::vec(0usize..=5, 1..=10),
        amounts in proptest::collection::vec(1i128..=30_000i128, 1..=30),
        batch_sizes in proptest::collection::vec(1usize..=3usize, 1..=10),
        seed in 0u64..u64::MAX,
    ) {
        let env = Env::default();
        env.mock_all_auths();

        let admin = Address::generate(&env);
        let sme = Address::generate(&env);
        let client = deploy(&env);
        let (token, treasury) = free_addresses(&env);

        let cap = initial_cap.min(n_investors as u32).max(2);
        let funding_target = 10_000_000i128;

        client.init(
            &admin,
            &soroban_sdk::String::from_str(&env, "SEQSLOT1"),
            &sme,
            &funding_target,
            &800i64,
            &0u64,
            &token,
            &None,
            &treasury,
            &None,
            &None,
            &Some(cap),
            &None,
            &None,
            &None,
            &None,
            &None,
        &None::<i64>,);

        let investors: Vec<Address> = (0..n_investors)
            .map(|_| Address::generate(&env))
            .collect();

        let mut current_cap = cap;
        let mut funded_set: BTreeSet<usize> = BTreeSet::new();
        let mut amount_idx: usize = 0;
        let mut rng = SplitMix64::new(seed);

        // Initial invariant check.
        prop_assert_eq!(
            client.get_remaining_investor_slots(),
            Some(cap),
            "initial: remaining must equal cap before any fund"
        );

        let steps = seq_len
            .min(op_tags.len())
            .min(investor_ixs.len())
            .min(batch_sizes.len());

        for step in 0..steps {
            if client.get_escrow().status != 0 {
                break;
            }

            let op_tag = op_tags[step];

            match op_tag % 3 {
                // ── Single fund ───────────────────────────────────────
                0 => {
                    let ix = investor_ixs[step] % n_investors;
                    let inv = investors[ix].clone();
                    let amt = if amount_idx < amounts.len() {
                        let a = amounts[amount_idx];
                        amount_idx += 1;
                        a
                    } else {
                        1i128
                    };

                    let is_new = !funded_set.contains(&ix);
                    if is_new {
                        let slots = client.get_remaining_investor_slots().unwrap_or(0);
                        if slots == 0 {
                            continue;
                        }
                    }

                    let remaining_before = client.get_remaining_investor_slots().unwrap_or(0);
                    let _ = client.fund(&inv, &amt);
                    if is_new {
                        funded_set.insert(ix);
                    }

                    // Invariant: count + remaining == cap.
                    let count = client.get_unique_funder_count();
                    let remaining = client.get_remaining_investor_slots().unwrap_or(0);
                    prop_assert!(remaining >= 0, "step {step} (fund): remaining underflowed");
                    prop_assert_eq!(
                        count + remaining,
                        current_cap,
                        "step {step} (fund): count({count}) + remaining({remaining}) != cap({current_cap})",
                        step = step,
                        count = count,
                        remaining = remaining,
                        current_cap = current_cap
                    );

                    // Invariant C: repeat funder must not change remaining.
                    if !is_new {
                        prop_assert_eq!(
                            remaining, remaining_before,
                            "step {step}: repeat deposit changed remaining slots",
                            step = step
                        );
                    }
                }
                // ── Batch fund ────────────────────────────────────────
                1 => {
                    let bsize = batch_sizes[step].min(
                        (current_cap as usize).saturating_sub(funded_set.len()).min(3)
                    );
                    if bsize == 0 {
                        continue;
                    }

                    let mut batch_vec = soroban_sdk::Vec::new(&env);
                    let mut new_ixs: Vec<usize> = Vec::new();
                    for b in 0..bsize {
                        let ix = (investor_ixs[step].wrapping_add(b)) % n_investors;
                        let is_new = !funded_set.contains(&ix);
                        if is_new {
                            let slots_left = (current_cap as usize).saturating_sub(funded_set.len() + new_ixs.len());
                            if slots_left == 0 {
                                break;
                            }
                            new_ixs.push(ix);
                        }
                        let amt = if amount_idx < amounts.len() {
                            let a = amounts[amount_idx];
                            amount_idx += 1;
                            a
                        } else {
                            1i128
                        };
                        batch_vec.push_back((investors[ix].clone(), amt));
                    }
                    if batch_vec.is_empty() {
                        continue;
                    }

                    let _ = client.fund_batch(&batch_vec);
                    for ix in new_ixs {
                        funded_set.insert(ix);
                    }

                    // Invariant B after batch.
                    let count = client.get_unique_funder_count();
                    let remaining = client.get_remaining_investor_slots().unwrap_or(0);
                    prop_assert!(remaining >= 0, "step {step} (batch): remaining underflowed");
                    prop_assert_eq!(
                        count + remaining,
                        current_cap,
                        "step {step} (batch): count({count}) + remaining({remaining}) != cap({current_cap})",
                        step = step,
                        count = count,
                        remaining = remaining,
                        current_cap = current_cap
                    );
                }
                // ── Lower cap ─────────────────────────────────────────
                _ => {
                    let count = client.get_unique_funder_count();
                    // Lower by 1 if the result would still be >= count and > 1.
                    let target_cap = current_cap.saturating_sub(
                        rng.gen_usize(2) as u32 + 1
                    );
                    if target_cap >= count && target_cap >= 1 && target_cap < current_cap {
                        client.lower_max_unique_investors(&target_cap);
                        current_cap = target_cap;
                    }

                    // Invariant D after cap lowering.
                    let count2 = client.get_unique_funder_count();
                    let remaining = client.get_remaining_investor_slots().unwrap_or(0);
                    prop_assert!(remaining >= 0, "step {step} (lower_cap): remaining underflowed");
                    prop_assert_eq!(
                        count2 + remaining,
                        current_cap,
                        "step {step} (lower_cap): count({count2}) + remaining({remaining}) != cap({current_cap})",
                        step = step,
                        count2 = count2,
                        remaining = remaining,
                        current_cap = current_cap
                    );
                }
            }
        }
    }
}

// ── Edge case: cap exactly hit ────────────────────────────────────────────────

/// When exactly `cap` unique investors have funded, remaining must be 0 (not negative).
#[test]
fn slots_cap_exactly_hit_remaining_is_zero() {
    let env = Env::default();
    env.mock_all_auths();
    let admin = Address::generate(&env);
    let sme = Address::generate(&env);
    let client = deploy(&env);

    let target: i128 = 1_000_000i128;
    let cap: u32 = 3;

    client.init(
        &admin,
        &soroban_sdk::String::from_str(&env, "EXACTCAP"),
        &sme,
        &target,
        &800i64,
        &0u64,
        &Address::generate(&env),
        &None,
        &Address::generate(&env),
        &None,
        &None,
        &Some(cap),
        &None,
        &None,
        &None,
        &None,
        &None,
        &None::<i64>,
    );

    let investors: Vec<Address> = (0..cap as usize).map(|_| Address::generate(&env)).collect();

    for (i, inv) in investors.iter().enumerate() {
        client.fund(inv, &100_000i128);
        let remaining = client.get_remaining_investor_slots().unwrap();
        let count = client.get_unique_funder_count();
        assert!(
            remaining >= 0,
            "remaining must not underflow after investor {i}"
        );
        assert_eq!(
            count + remaining,
            cap,
            "count({count}) + remaining({remaining}) != cap({cap}) after investor {i}"
        );
    }

    // After all cap slots consumed: remaining must be 0.
    let final_remaining = client.get_remaining_investor_slots().unwrap();
    assert_eq!(
        final_remaining, 0,
        "remaining must be exactly 0 when cap is fully consumed"
    );
    assert_slots_invariant(&client, "cap exactly hit");
}