farming-pool: no property-based test enforces that total accrued credits are independent of checkpoint frequency

[prodbycorne]

Problem

The credit-accrual system has an implicit invariant that the test suite verifies only pointwise, never generally: total accrued credits for a given total stake amount over a given elapsed ledger range should not depend on how the stake was split across multiple stake()/set_boost() calls, nor on how many times it was checkpointed in between.

Tests like test_additional_stake_checkpoints_credits and test_boost_can_be_updated_repeatedly_without_losing_credits each hand-verify one specific sequence of operations against one hand-computed expected value:

#[test]
fn test_additional_stake_checkpoints_credits() {
    // Stake 1000, earn 10 ledgers (= 10000 credits), then stake 500 more.
    let t = setup(1, 1);
    t.client.stake(&t.user, &1_000);
    advance_ledgers(&t.env, 10);
    t.client.stake(&t.user, &500);
    advance_ledgers(&t.env, 10);
    assert_eq!(t.client.get_credits(&t.user), 25_000);
}

There is no property-based/fuzz test that instead generates random sequences of stake/set_boost/unstake calls with random amounts, random allocation_pct, random ledger-advance intervals, and asserts a general invariant such as: total credits banked is always non-negative, monotonically non-decreasing as elapsed ledgers grow for a fixed stake, and bounded above by (max possible effective stake given elapsed time and multiplier bounds). Given the amount of subtlety already found in this accrual system (see companion issues on truncation-driven path-dependence for small stakes, and retroactive multiplier repricing for uncheckpointed users), example-based tests alone are demonstrably insufficient to catch this class of bug — both of those bugs pass every existing example-based test in farming-pool/src/test.rs.

Impact

• Testing gap enabling exactly the bugs already found in this campaign: neither the truncation/path-dependence issue nor the multiplier-retroactivity issue would be caught by any test currently in the suite; a property-based test targeting the general invariant would have caught both.
• No regression protection for future accrual-formula changes: any future change to compute_credits/compute_total_stake/checkpoint risks reintroducing either bug class with no test failing.

Fix

Add proptest (or a hand-rolled pseudo-random sweep using a seeded PRNg, if pulling in proptest as a dev-dependency is undesirable for a no_std contract crate) exercising the invariant:

// dev-dependency: proptest = "1"
proptest! {
    #[test]
    fn credits_are_monotonic_and_path_independent(
        amount in 1i128..1_000_000,
        allocation_pct in 1u32..=100,
        multiplier in 1u32..10,
        splits in 1usize..10,
        elapsed in 1u32..1000,
    ) {
        // Stake `amount` in one lump sum vs. `splits` incremental stakes of amount/splits each,
        // over the same total elapsed ledgers, and assert the resulting credits are equal
        // (or, if the design intentionally accepts truncation loss, bounded within a documented
        // tolerance rather than differing by multiples).
    }
}

Acceptance Criteria

• proptest (or equivalent) added as a dev-dependency to farming-pool/Cargo.toml.
• A property test asserts total credits for a fixed total stake/elapsed-time are path-independent of deposit granularity within a documented tolerance (tying into the small-stake truncation issue's resolution).
• A property test asserts credits are monotonically non-decreasing in elapsed ledgers for a fixed stake/multiplier/allocation.
• A property test asserts get_credits/calculate_credits never return a negative value for any valid input combination.
• The property tests run as part of cargo test --workspace in CI without requiring network access or excessive runtime (bound case counts appropriately).

Further Investigation

Why this is a spike, not a mechanical fix: the invariant this issue wants tested ("total credits are path-independent of checkpoint frequency") has never been formally stated anywhere in the codebase, and there are at least two subtly different candidate invariants that are not equivalent given the current integer-truncating implementation:

• compute_total_stake (soroban/contracts/farming-pool/src/lib.rs:131-136) computes boosted = amount * allocation_pct as i128 / 100 — integer division that truncates. Splitting one amount into two stake() calls of amount/2 each changes the truncation remainder at each call site, so exact path-independence is provably false for allocation_pct values that don't evenly divide the split amounts. Any property test that asserts strict equality will fail on legitimate, non-buggy behavior; the "tolerance" the issue body already flags (... or bounded within a documented tolerance ...) has to be derived, not guessed, and the derivation depends on how many splits n you allow (worst-case truncation loss grows with n, roughly O(n) in the worst case since each stake() call independently floors its own boosted term).
• checkpoint() (lib.rs:148-162) re-reads read_credit_rate/read_global_multiplier at every call, so a property test that also randomizes admin set_credit_rate/set_global_multiplier calls interleaved with checkpoints (which is realistic — see farming-pool: set_global_multiplier and set_credit_rate accept unbounded values with no sanity ceiling, guaranteeing compute_credits overflow at scale #89 on unbounded ceiling for those setters) needs to decide whether "path independence" holds per rate-regime (sum of credits earned under each historical rate) or is expected to break entirely across a rate change — the existing example test test_credit_rate_change_does_not_retroactively_alter_staked_credits (farming-pool/src/test.rs:369) implies the former, but no property test currently encodes that as a general rule.

Tradeoff approaches

1. Strict tolerance-bounded proptest: derive the exact worst-case truncation bound analytically (splits * (100 truncation units) roughly) and assert |lump_sum_credits - split_credits| <= bound. Precise but requires the derivation to be correct or the test is either too loose (misses real bugs) or flaky (fails on correct behavior).
2. Relative/percentage tolerance: assert the two values are within e.g. 0.01% of each other. Simpler to write, but doesn't scale correctly for small amount values where truncation dominates (this is exactly the companion small-stake truncation bug class the issue body references) — should probably be paired with a floor on amount in the generator (e.g. amount in 10_000i128..1_000_000) to keep the property meaningful.
3. Split into two properties: (a) a strict-equality property for the no-checkpoint-in-between case (single lump stake vs. stake immediately followed by another stake in the same ledger, elapsed = 0 for the second), which should hold exactly since no accrual happens before the second checkpoint; (b) a documented-tolerance property for the multi-checkpoint-over-time case. This decomposition is likely the cleanest because it separates "is the split-deposit truncation bug present" from "is checkpoint frequency independence violated," which are conceptually different bugs the issue's own text conflates.

Edge cases to add to the generator

• allocation_pct at the boundary values 1 and 100 (already unit-tested individually, but not combined with random splits).
• Interaction with farming-pool: unstake() cannot partially withdraw a stake, unlike unlock_assets()'s partial-unlock support #77 (if unstake gains a partial-withdrawal amount parameter): a property test should also cover stake → partial unstake → stake more → checkpoint, since partial unstake introduces a new path through checkpoint() that wasn't exercised when unstake only supported full withdrawal.
• Interaction with farming-pool: set_global_multiplier and set_credit_rate accept unbounded values with no sanity ceiling, guaranteeing compute_credits overflow at scale #89: if set_credit_rate/set_global_multiplier gain upper ceilings, the proptest generator's ranges for multiplier/credit_rate should be updated to match the new ceiling constants rather than arbitrary ranges, so the fuzz test doesn't waste cases on now-rejected inputs.

Test plan

• Add farming-pool/Cargo.toml dev-dependency proptest = "1" (confirm this doesn't break the #![no_std] contract build — proptest must be dev-only, gated behind #[cfg(test)] in test.rs, which is already how soroban-sdk's own testutils feature is scoped in this crate's Cargo.toml).
• Add credits_path_independent_within_tolerance_for_split_deposits (property 3a/3b above) and credits_monotonic_nondecreasing_in_elapsed_ledgers and credits_never_negative as named proptest functions in farming-pool/src/test.rs.
• Cross-reference: farming-pool: no fuzz/boundary test exercises i128 overflow boundaries in compute_credits/compute_total_stake #76 (overflow fuzz — could share the same proptest dev-dependency addition, coordinate to avoid adding it twice), farming-pool: set_global_multiplier and set_credit_rate accept unbounded values with no sanity ceiling, guaranteeing compute_credits overflow at scale #89 (ceiling constants the generator ranges should respect), farming-pool: unstake() cannot partially withdraw a stake, unlike unlock_assets()'s partial-unlock support #77 (partial-unstake path to add once that lands).

[Cyber-Mitch]

i'm a smart contract engineer, i have experience in writing reviewing and testing Soroban Smart contracts. I will complete this issue in 2 days