diff --git a/soroban/Cargo.lock b/soroban/Cargo.lock index 0565331..26f084f 100644 --- a/soroban/Cargo.lock +++ b/soroban/Cargo.lock @@ -158,7 +158,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "94893f1e0c6eeab764ade8dc4c0db24caf4fe7cbbaafc0eba0a9030f447b5185" dependencies = [ "num-traits", - "rand", + "rand 0.8.6", ] [[package]] @@ -185,6 +185,27 @@ version = "1.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" +[[package]] +name = "bit-set" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08807e080ed7f9d5433fa9b275196cfc35414f66a0c79d864dc51a0d825231a3" +dependencies = [ + "bit-vec", +] + +[[package]] +name = "bit-vec" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7" + +[[package]] +name = "bitflags" +version = "2.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b588b76d00fde79687d7646a9b5bdf3cc0f655e0bbd080335a95d7e96f3587da" + [[package]] name = "block-buffer" version = "0.10.4" @@ -305,7 +326,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0dc92fb57ca44df6db8059111ab3af99a63d5d0f8375d9972e319a379c6bab76" dependencies = [ "generic-array", - "rand_core", + "rand_core 0.6.4", "subtle", "zeroize", ] @@ -549,7 +570,7 @@ checksum = "70e796c081cee67dc755e1a36a0a172b897fab85fc3f6bc48307991f64e4eca9" dependencies = [ "curve25519-dalek", "ed25519", - "rand_core", + "rand_core 0.6.4", "serde", "sha2", "subtle", @@ -574,7 +595,7 @@ dependencies = [ "ff", "generic-array", "group", - "rand_core", + "rand_core 0.6.4", "sec1", "subtle", "zeroize", @@ -586,6 +607,16 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" +[[package]] +name = "errno" +version = "0.3.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" +dependencies = [ + "libc", + "windows-sys", +] + [[package]] name = "escape-bytes" version = "0.1.1" @@ -610,16 +641,23 @@ dependencies = [ name = "farming-pool" version = "0.1.0" dependencies = [ + "proptest", "soroban-sdk", ] +[[package]] +name = "fastrand" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da7c62ceae207dd37ea5b845da6a0696c799f85e97da1ab5b7910be3c1c80223" + [[package]] name = "ff" version = "0.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c0b50bfb653653f9ca9095b427bed08ab8d75a137839d9ad64eb11810d5b6393" dependencies = [ - "rand_core", + "rand_core 0.6.4", "subtle", ] @@ -689,6 +727,29 @@ dependencies = [ "wasm-bindgen", ] +[[package]] +name = "getrandom" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" +dependencies = [ + "cfg-if", + "libc", + "r-efi 5.3.0", + "wasip2", +] + +[[package]] +name = "getrandom" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099" +dependencies = [ + "cfg-if", + "libc", + "r-efi 6.0.0", +] + [[package]] name = "group" version = "0.13.0" @@ -696,7 +757,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0f9ef7462f7c099f518d754361858f86d8a07af53ba9af0fe635bbccb151a63" dependencies = [ "ff", - "rand_core", + "rand_core 0.6.4", "subtle", ] @@ -888,6 +949,12 @@ version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6d2cec3eae94f9f509c767b45932f1ada8350c4bdb85af2fcab4a3c14807981" +[[package]] +name = "linux-raw-sys" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" + [[package]] name = "log" version = "0.4.32" @@ -1039,6 +1106,31 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "proptest" +version = "1.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4b45fcc2344c680f5025fe57779faef368840d0bd1f42f216291f0dc4ace4744" +dependencies = [ + "bit-set", + "bit-vec", + "bitflags", + "num-traits", + "rand 0.9.5", + "rand_chacha 0.9.0", + "rand_xorshift", + "regex-syntax", + "rusty-fork", + "tempfile", + "unarray", +] + +[[package]] +name = "quick-error" +version = "1.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0" + [[package]] name = "quote" version = "1.0.45" @@ -1048,6 +1140,18 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "r-efi" +version = "5.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" + +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + [[package]] name = "rand" version = "0.8.6" @@ -1055,8 +1159,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5ca0ecfa931c29007047d1bc58e623ab12e5590e8c7cc53200d5202b69266d8a" dependencies = [ "libc", - "rand_chacha", - "rand_core", + "rand_chacha 0.3.1", + "rand_core 0.6.4", +] + +[[package]] +name = "rand" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41" +dependencies = [ + "rand_chacha 0.9.0", + "rand_core 0.9.5", ] [[package]] @@ -1066,7 +1180,17 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" dependencies = [ "ppv-lite86", - "rand_core", + "rand_core 0.6.4", +] + +[[package]] +name = "rand_chacha" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" +dependencies = [ + "ppv-lite86", + "rand_core 0.9.5", ] [[package]] @@ -1075,7 +1199,25 @@ version = "0.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" dependencies = [ - "getrandom", + "getrandom 0.2.17", +] + +[[package]] +name = "rand_core" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" +dependencies = [ + "getrandom 0.3.4", +] + +[[package]] +name = "rand_xorshift" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "513962919efc330f829edb2535844d1b912b0fbe2ca165d613e4e8788bb05a5a" +dependencies = [ + "rand_core 0.9.5", ] [[package]] @@ -1098,6 +1240,12 @@ dependencies = [ "syn 2.0.118", ] +[[package]] +name = "regex-syntax" +version = "0.8.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" + [[package]] name = "rfc6979" version = "0.4.0" @@ -1117,12 +1265,37 @@ dependencies = [ "semver", ] +[[package]] +name = "rustix" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190" +dependencies = [ + "bitflags", + "errno", + "libc", + "linux-raw-sys", + "windows-sys", +] + [[package]] name = "rustversion" version = "1.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" +[[package]] +name = "rusty-fork" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc6bf79ff24e648f6da1f8d1f011e9cac26491b619e6b9280f2b47f1774e6ee2" +dependencies = [ + "fnv", + "quick-error", + "tempfile", + "wait-timeout", +] + [[package]] name = "schemars" version = "0.8.22" @@ -1287,7 +1460,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de" dependencies = [ "digest", - "rand_core", + "rand_core 0.6.4", ] [[package]] @@ -1359,7 +1532,7 @@ dependencies = [ "ed25519-dalek", "elliptic-curve", "generic-array", - "getrandom", + "getrandom 0.2.17", "hex-literal", "hmac", "k256", @@ -1367,8 +1540,8 @@ dependencies = [ "num-integer", "num-traits", "p256", - "rand", - "rand_chacha", + "rand 0.8.6", + "rand_chacha 0.3.1", "sec1", "sha2", "sha3", @@ -1421,7 +1594,7 @@ dependencies = [ "ctor", "derive_arbitrary", "ed25519-dalek", - "rand", + "rand 0.8.6", "rustc_version", "serde", "serde_json", @@ -1597,6 +1770,19 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.27.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" +dependencies = [ + "fastrand", + "getrandom 0.4.3", + "once_cell", + "rustix", + "windows-sys", +] + [[package]] name = "thiserror" version = "1.0.69" @@ -1668,6 +1854,12 @@ version = "1.20.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6f5e870be6c3b371b77fe0ee0bafb859fa4964b4404c27de1d380043c4dda20" +[[package]] +name = "unarray" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94" + [[package]] name = "unicode-ident" version = "1.0.24" @@ -1698,12 +1890,30 @@ dependencies = [ "syn 2.0.118", ] +[[package]] +name = "wait-timeout" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11" +dependencies = [ + "libc", +] + [[package]] name = "wasi" version = "0.11.1+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" +[[package]] +name = "wasip2" +version = "1.0.4+wasi-0.2.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487" +dependencies = [ + "wit-bindgen", +] + [[package]] name = "wasm-bindgen" version = "0.2.125" @@ -1845,6 +2055,21 @@ dependencies = [ "windows-link", ] +[[package]] +name = "windows-sys" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" +dependencies = [ + "windows-link", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + [[package]] name = "zerocopy" version = "0.8.52" diff --git a/soroban/contracts/farming-pool/Cargo.toml b/soroban/contracts/farming-pool/Cargo.toml index bc322d0..c4e0d3a 100644 --- a/soroban/contracts/farming-pool/Cargo.toml +++ b/soroban/contracts/farming-pool/Cargo.toml @@ -18,3 +18,11 @@ soroban-sdk = { workspace = true } [dev-dependencies] soroban-sdk = { workspace = true, features = ["testutils"] } +# Property-based tests for credit-accrual invariants (#75). Deliberately a +# plain dev-dependency rather than part of the `testutils` feature above: +# `testutils` is forwarded to dependents (`factory` enables it to get +# `farming_pool::WASM`), whereas proptest is only ever needed by this crate's +# own `src/test.rs`. Dev-dependencies are not built for +# `cargo build --target wasm32v1-none --release`, so this cannot reach the +# `#![no_std]` contract binary. +proptest = "1" diff --git a/soroban/contracts/farming-pool/src/test.rs b/soroban/contracts/farming-pool/src/test.rs index 651b097..787ab38 100644 --- a/soroban/contracts/farming-pool/src/test.rs +++ b/soroban/contracts/farming-pool/src/test.rs @@ -1,7 +1,7 @@ #![cfg(test)] use super::*; use soroban_sdk::{ - testutils::{Address as _, Events, Ledger, MockAuth, MockAuthInvoke}, + testutils::{Address as _, EnvTestConfig, Events, Ledger, MockAuth, MockAuthInvoke}, token::{StellarAssetClient, TokenClient}, Address, BytesN, Env, IntoVal, Symbol, Val, }; @@ -2072,3 +2072,609 @@ fn test_emergency_withdraw_reverts_entirely_if_stake_token_naively_reenters() { let stake = client.get_stake(&user).unwrap(); assert_eq!(stake.amount, 300); } + +// ── Credit-accrual invariants, property-based (#75) ────────────────────────── +// +// Shared notation used by every derivation below. Writing +// `B(a, p) = floor(a * p / 100)` for the boosted portion computed by +// `compute_total_stake`, that function reduces algebraically to +// +// S(a, p, m) = (a - B(a, p)) + B(a, p) * m +// = a + B(a, p) * (m - 1) +// +// and `compute_credits` is `S(a, p, m) * r * elapsed`. `B` is the *only* +// nonlinearity in the whole accrual path — everything else is integer +// multiplication and addition, which are exact. +// +// Where truncation could bite, and by how much. For a partition +// `A = a_1 + ... + a_n`, write `a_i * p / 100 = q_i + f_i` with `f_i` in +// `[0, 1)`. Then `sum_i B(a_i, p) = sum_i q_i` while +// `B(A, p) = floor(sum_i (q_i + f_i)) = sum_i q_i + floor(sum_i f_i)`, so +// +// B(A, p) - sum_i B(a_i, p) = floor(sum_i f_i) in [0, n - 1] +// +// (upper bound `n - 1` because each `f_i <= 99/100`, so `sum f_i < n`; tight at +// `p = 99, a_i = 1, n = 100`). An implementation that banked each deposit's +// boosted portion *separately* would therefore lose up to +// `(n - 1) * (m - 1) * r * elapsed` credits relative to one that aggregates +// first. That is the loss issue #75 anticipated. +// +// It is not reachable by splitting a deposit, because `stake` performs +// `existing.amount += amount` *before* `B` is next evaluated, and every call +// site of `compute_total_stake` passes the cumulative `stake.amount`. `B` is +// only ever applied to the aggregate. Properties A and B below are therefore +// *strict equalities*, not tolerance-bounded comparisons: an epsilon of +// `(n - 1) * (m - 1) * r * elapsed` would be blind to a regression of exactly +// that size, which is the regression these tests exist to catch. +// +// Preconditions shared by A and B, outside which they are false *by design*: +// * `credit_rate` fixed. `checkpoint` snapshots the rate into `UserStake`, so +// a mid-flight change is priced from the next checkpoint onward — see +// `test_credit_rate_change_does_not_retroactively_alter_staked_credits`. +// * `global_multiplier` fixed. See the "Property E" note at the end of this +// section: unlike the rate, the multiplier is *not* snapshotted. +// * `allocation_pct` fixed and set before the first stake, so that +// `checkpoint`'s `get_user_boost` read is the same value at every call. + +use proptest::prelude::*; + +/// Case count for every property in this section. Deliberately modest: each +/// case registers a Stellar Asset Contract plus a pool instance and drives +/// several contract invocations, so cost per case is milliseconds rather than +/// microseconds. 64 is enough to explore the truncating region of `B` densely +/// while keeping the whole section well under a second — see #75's acceptance +/// criterion on CI runtime. +const PROP_CASES: u32 = 64; + +/// Upper bound on a single generated deposit. +/// +/// Chosen to stay far inside #89's overflow budget rather than to probe it: +/// with `multiplier <= MAX_GLOBAL_MULTIPLIER`, `credit_rate <= MAX_CREDIT_RATE`, +/// at most `MAX_DEPOSITS` deposits and a horizon under 10^5 ledgers, the worst +/// case is `6e12 * 1e3 * 1e8 * 1e5 ~= 4.5e28`, about ten orders of magnitude +/// below `i128::MAX ~= 1.7e38`. Overflow boundaries are #76's subject, not +/// this file's — these properties must fail on *accounting* errors only. +const MAX_DEPOSIT: i128 = 1_000_000_000_000; + +const MAX_DEPOSITS: usize = 6; +const MAX_CHECKPOINTS: usize = 8; + +/// Largest gap, in ledgers, generated between two timeline steps. +const MAX_GAP: u32 = 5_000; + +/// A pool configured for property testing. +/// +/// Differs from [`setup`] in three ways that matter: +/// * `capture_snapshot_at_drop: false` — soroban writes a +/// `test_snapshots/.N.json` file for every `Env` it drops +/// (soroban-sdk `src/env.rs`, `impl Drop for Env`). With one `Env` per +/// proptest case per path that would be hundreds of JSON files per run. +/// * `min_stake_amount = 1` — the loosest legal setting (`get_min_stake_amount` +/// itself defaults to 1), which is also the most adversarial: it lets a +/// deposit be split into parts as small as a single unit, maximising the +/// number of independent `floor` roundings a per-deposit implementation +/// would incur. +/// * a much larger mint, so a six-deposit schedule at `MAX_DEPOSIT` each is +/// always affordable. +fn setup_for_props(global_multiplier: u32, credit_rate: i128) -> TestEnv { + let env = Env::new_with_config(EnvTestConfig { + capture_snapshot_at_drop: false, + }); + env.mock_all_auths(); + + let admin = Address::generate(&env); + let user = Address::generate(&env); + + let token_admin = Address::generate(&env); + let asset = env.register_stellar_asset_contract_v2(token_admin.clone()); + let token_sac = StellarAssetClient::new(&env, &asset.address()); + token_sac.mint(&user, &i128::from(u64::MAX)); + + let contract_id = env.register(FarmingPool, ()); + let client = FarmingPoolClient::new(&env, &contract_id); + client.initialize( + &admin, + &asset.address(), + &global_multiplier, + &credit_rate, + &0u32, + &1i128, + ); + + let token = TokenClient::new(&env, &asset.address()); + + // SAFETY: as in `setup_with_lock_period` — `env` owns the contract and + // token registrations, so they outlive the returned struct. + let client = unsafe { + core::mem::transmute::, FarmingPoolClient<'static>>(client) + }; + let token = unsafe { core::mem::transmute::, TokenClient<'static>>(token) }; + let token_sac = unsafe { + core::mem::transmute::, StellarAssetClient<'static>>(token_sac) + }; + + TestEnv { + env, + client, + contract_id, + token, + token_sac, + admin, + user, + } +} + +/// One event on a generated timeline: `gap` ledgers elapse, then `action`. +#[derive(Clone, Copy, Debug)] +enum Action { + /// Stake this amount. + Deposit(i128), + /// Re-apply the *same* `allocation_pct`, which forces `checkpoint` to run + /// (`set_boost` checkpoints before writing) without altering any input to + /// the accrual formula. The purest available no-op checkpoint. + Checkpoint, +} + +type Step = (u32, Action); + +/// Independent oracle for the credits a schedule should produce. +/// +/// Written in the *reduced* form `S = a + B(a, p) * (m - 1)` derived at the top +/// of this section, rather than by calling `compute_total_stake`, so that these +/// properties are oracle tests rather than merely differential ones: two paths +/// through the contract cannot agree with each other *and* with this expression +/// while both being wrong in the same way. +/// +/// The oracle deliberately keeps the `floor` — it is not a rational-arithmetic +/// reference. Its job is to pin the *aggregation structure* (`B` applied once +/// per checkpoint to the running total, credits summed over intervals), which +/// is exactly what deposit granularity and checkpoint frequency could perturb. +fn oracle_total_stake(amount: i128, allocation_pct: u32, multiplier: u32) -> i128 { + amount + (amount * allocation_pct as i128 / 100) * (multiplier as i128 - 1) +} + +/// Credits accrued by `steps` followed by `tail_gap` further ledgers, given a +/// boost set before the first deposit and a fixed multiplier and rate. +/// +/// `sum_j S(A_j, p, m) * r * (t_{j+1} - t_j)` where `A_j` is the amount held +/// during interval `j`. `Checkpoint` steps contribute nothing beyond their gap, +/// which is precisely Property B's claim. +fn oracle_credits( + steps: &[Step], + allocation_pct: u32, + multiplier: u32, + credit_rate: i128, + tail_gap: u32, +) -> i128 { + let mut held = 0i128; + let mut total = 0i128; + for &(gap, action) in steps { + // `gap` ledgers elapse while `held` is staked. Before the first + // deposit `held` is 0 and the interval contributes nothing. + total += oracle_total_stake(held, allocation_pct, multiplier) * credit_rate * gap as i128; + if let Action::Deposit(amount) = action { + held += amount; + } + } + total += oracle_total_stake(held, allocation_pct, multiplier) * credit_rate * tail_gap as i128; + total +} + +/// Split `amount` into `weights.len()` positive parts in the given proportions. +/// +/// Every part is at least 1 (the pool's `min_stake_amount`), and the parts sum +/// to exactly `amount`, so the split changes deposit *granularity* and nothing +/// else. The caller must ensure `1 <= weights.len() <= amount`. +fn partition(amount: i128, weights: &[u32]) -> std::vec::Vec { + let n = weights.len() as i128; + debug_assert!(n >= 1 && n <= amount); + let weight_sum: i128 = weights.iter().map(|&w| i128::from(w)).sum(); + + let mut assigned = 0i128; + let mut parts = std::vec::Vec::with_capacity(weights.len()); + for (i, &w) in weights.iter().enumerate().take(weights.len() - 1) { + // Leave at least 1 unit for each part still to come. + let reserved = n - 1 - i as i128; + let part = (amount * i128::from(w) / weight_sum).clamp(1, amount - assigned - reserved); + parts.push(part); + assigned += part; + } + parts.push(amount - assigned); + parts +} + +// ── Generators ─────────────────────────────────────────────────────────────── +// +// Every range below is the *reachable* range for that input, so the properties +// never assert anything about a state the contract would have rejected: +// +// multiplier 1..=MAX_GLOBAL_MULTIPLIER (lib.rs, `set_global_multiplier`) +// credit_rate 1..=MAX_CREDIT_RATE (lib.rs, `set_credit_rate`) +// allocation_pct 1..=100 (lib.rs, `set_boost`) +// deposit >= min_stake_amount, > 0 (lib.rs, `stake`) +// +// Both ceilings are #89's landed constants, imported rather than re-stated, so +// this file tracks any future change to them automatically. + +/// `2..=MAX_GLOBAL_MULTIPLIER`, not `1..=`. +/// +/// At `multiplier == 1`, `S(a, p, m) = a` identically and the `floor` in `B` +/// cannot affect the result at all — a split-invariance property would pass +/// vacuously. Properties A and B exist to exercise the truncating branch, so +/// they exclude the one value that switches it off. Property D, which makes no +/// claim about truncation, keeps the full `1..=` range. +fn boosting_multiplier() -> impl Strategy { + 2..=MAX_GLOBAL_MULTIPLIER +} + +fn any_multiplier() -> impl Strategy { + 1..=MAX_GLOBAL_MULTIPLIER +} + +fn any_credit_rate() -> impl Strategy { + 1..=MAX_CREDIT_RATE +} + +fn any_allocation_pct() -> impl Strategy { + 1..=100u32 +} + +fn any_deposit() -> impl Strategy { + 1..=MAX_DEPOSIT +} + +fn any_gap() -> impl Strategy { + 0..=MAX_GAP +} + +/// A timeline mixing deposits and no-op checkpoints. +fn any_steps() -> impl Strategy> { + let action = prop_oneof![ + 3 => any_deposit().prop_map(Action::Deposit), + 1 => Just(Action::Checkpoint), + ]; + proptest::collection::vec((any_gap(), action), 1..=(MAX_DEPOSITS + MAX_CHECKPOINTS)) +} + +/// A deposits-only timeline, paired with per-deposit split weights. +fn any_deposit_schedule() -> impl Strategy)>> { + proptest::collection::vec( + ( + any_gap(), + any_deposit(), + proptest::collection::vec(1..=1_000u32, 1..=4), + ), + 1..=MAX_DEPOSITS, + ) +} + +proptest! { + #![proptest_config(ProptestConfig::with_cases(PROP_CASES))] + + /// PROPERTY A — total credits do not depend on deposit granularity. + /// + /// Claim: for a fixed schedule of deposits `(t_j, amt_j)`, subdividing any + /// `amt_j` into parts staked at the *same* ledger `t_j` leaves total + /// credits unchanged at every later ledger. Tolerance: **exactly zero**. + /// + /// Derivation. Two facts about a second `stake` call at the same ledger: + /// + /// 1. It checkpoints with `elapsed = current - stake.start_ledger = 0`, + /// so `credits_banked += S(...) * r * 0 = 0` and `start_ledger` is + /// rewritten to the value it already held. The bank is untouched, and + /// — crucially — `B` never sees the individual part. + /// 2. `existing.amount += amount` aggregates *before* `B` is next + /// evaluated, at the following checkpoint or read. + /// + /// So after subdividing, `UserStake` is field-for-field identical: + /// `{amount, start_ledger, credits_banked, credit_rate}` all match. By + /// induction over the schedule every subsequent checkpoint observes + /// identical state, hence identical credits. No rounding is introduced, + /// which is why this is `==` and not `<= epsilon`. + /// + /// What it catches: a refactor that banked each deposit's boosted portion + /// separately would lose `floor(sum_i f_i) * (m - 1) * r * elapsed` + /// credits, up to `(n - 1) * (m - 1) * r * elapsed` — the bound derived at + /// the top of this section. Strict equality detects that at `n = 2`. + #[test] + fn prop_credits_are_independent_of_deposit_granularity( + multiplier in boosting_multiplier(), + credit_rate in any_credit_rate(), + allocation_pct in any_allocation_pct(), + schedule in any_deposit_schedule(), + tail_gap in 1..=MAX_GAP, + ) { + // Coarse path: one `stake` call per scheduled deposit. + let coarse = { + let t = setup_for_props(multiplier, credit_rate); + t.client.set_boost(&t.user, &allocation_pct); + for &(gap, amount, _) in &schedule { + advance_ledgers(&t.env, gap); + t.client.stake(&t.user, &amount); + } + advance_ledgers(&t.env, tail_gap); + t.client.get_credits(&t.user) + }; + + // Fine path: identical timeline, but each deposit arrives as several + // same-ledger calls summing to the same amount. + let fine = { + let t = setup_for_props(multiplier, credit_rate); + t.client.set_boost(&t.user, &allocation_pct); + for (gap, amount, weights) in &schedule { + advance_ledgers(&t.env, *gap); + // `partition` needs at least one unit per part. + let parts = (weights.len() as i128).min(*amount).max(1) as usize; + for part in partition(*amount, &weights[..parts]) { + t.client.stake(&t.user, &part); + } + } + advance_ledgers(&t.env, tail_gap); + t.client.get_credits(&t.user) + }; + + prop_assert_eq!( + coarse, fine, + "deposit granularity changed total credits (m={}, r={}, pct={})", + multiplier, credit_rate, allocation_pct + ); + + // ...and both agree with the independent closed form, so the property + // cannot be satisfied by two identically-wrong paths. + let steps: std::vec::Vec = schedule + .iter() + .map(|&(gap, amount, _)| (gap, Action::Deposit(amount))) + .collect(); + prop_assert_eq!( + coarse, + oracle_credits(&steps, allocation_pct, multiplier, credit_rate, tail_gap), + "credits diverged from the closed-form oracle" + ); + } + + /// PROPERTY B — total credits do not depend on checkpoint frequency. + /// + /// Claim: with `amount`, `allocation_pct`, `multiplier` and `credit_rate` + /// fixed, inserting arbitrarily many extra no-op checkpoints at arbitrary + /// ledgers leaves total credits unchanged. Tolerance: **exactly zero**. + /// + /// Derivation. Chop `[t_0, T]` at `t_0 < t_1 < ... < t_k`. Because + /// `amount`, `p` and `m` are unchanged at every checkpoint, `S(A, p, m)` + /// is the *same integer* `S` at each one, so the banked total is + /// + /// sum_j S * r * (t_{j+1} - t_j) = S * r * sum_j (t_{j+1} - t_j) + /// = S * r * T + /// + /// Integer multiplication distributes exactly over integer addition, so + /// partitioning *time* introduces no rounding whatsoever. Structurally: + /// the only `floor` in the accrual path is `B(amount, pct)`, a function of + /// amount and percentage alone — it is entirely independent of `elapsed`. + /// This is why the property needs no epsilon even though #75 expected one. + /// + /// Both paths walk the identical ledger timeline; they differ only in + /// whether the `Checkpoint` steps actually invoke the contract. Deposits + /// are interleaved so the property is tested across changing amounts, not + /// only for a single static stake. + #[test] + fn prop_credits_are_independent_of_checkpoint_frequency( + multiplier in boosting_multiplier(), + credit_rate in any_credit_rate(), + allocation_pct in any_allocation_pct(), + steps in any_steps(), + tail_gap in 1..=MAX_GAP, + ) { + // Sparse path: checkpoint steps advance the ledger but do nothing. + let sparse = { + let t = setup_for_props(multiplier, credit_rate); + t.client.set_boost(&t.user, &allocation_pct); + for &(gap, action) in &steps { + advance_ledgers(&t.env, gap); + if let Action::Deposit(amount) = action { + t.client.stake(&t.user, &amount); + } + } + advance_ledgers(&t.env, tail_gap); + t.client.get_credits(&t.user) + }; + + // Dense path: same timeline, checkpoint steps actually checkpoint. + let dense = { + let t = setup_for_props(multiplier, credit_rate); + t.client.set_boost(&t.user, &allocation_pct); + for &(gap, action) in &steps { + advance_ledgers(&t.env, gap); + match action { + Action::Deposit(amount) => t.client.stake(&t.user, &amount), + // Re-applying the same pct checkpoints without changing + // any input to the accrual formula. + Action::Checkpoint => t.client.set_boost(&t.user, &allocation_pct), + } + } + advance_ledgers(&t.env, tail_gap); + t.client.get_credits(&t.user) + }; + + prop_assert_eq!( + sparse, dense, + "checkpoint frequency changed total credits (m={}, r={}, pct={})", + multiplier, credit_rate, allocation_pct + ); + + prop_assert_eq!( + sparse, + oracle_credits(&steps, allocation_pct, multiplier, credit_rate, tail_gap), + "credits diverged from the closed-form oracle" + ); + } + + /// PROPERTY C — credits are strictly increasing in elapsed ledgers. + /// + /// Claim: for fixed stake, multiplier, rate and allocation, advancing the + /// ledger by `d >= 1` strictly increases the reported credits; advancing by + /// zero leaves them unchanged. + /// + /// Derivation. `get_credits = credits_banked + S(A, p, m) * r * elapsed`, + /// and both factors of the slope are bounded below by 1: + /// + /// * `S = A + B(A, p) * (m - 1) >= A >= 1`, since `stake` asserts + /// `amount > 0`, `B >= 0` and `m >= 1`; + /// * `r >= 1`, since `credit_rate` is constrained to + /// `1..=MAX_CREDIT_RATE`. + /// + /// So `delta = S * r * d >= 1 * 1 * 1 = 1 > 0`. Unlike A and B this needs + /// no truncation argument at all: `elapsed` appears only as a multiplicand, + /// never inside a division, so there is no rounding to reason about. The + /// same argument gives the lock/`Position` path (`amount * rate * elapsed`) + /// a slope of `amount * rate >= 1`. + /// + /// Crossing a checkpoint is also safe: at the instant of banking, + /// `banked' = banked + S * r * elapsed` while `elapsed' = 0`, so the + /// observable is continuous and the sequence stays monotone. + #[test] + fn prop_credits_are_strictly_increasing_in_elapsed_ledgers( + multiplier in any_multiplier(), + credit_rate in any_credit_rate(), + allocation_pct in any_allocation_pct(), + amount in any_deposit(), + advances in proptest::collection::vec(1..=MAX_GAP, 1..=8), + ) { + let t = setup_for_props(multiplier, credit_rate); + t.client.set_boost(&t.user, &allocation_pct); + t.client.stake(&t.user, &amount); + t.client.lock_assets(&t.user, &amount); + + let mut previous_staked = t.client.get_credits(&t.user); + let mut previous_locked = t.client.calculate_credits(&t.user); + + // Advancing by zero must be a no-op for both credit systems. + advance_ledgers(&t.env, 0); + prop_assert_eq!(t.client.get_credits(&t.user), previous_staked); + prop_assert_eq!(t.client.calculate_credits(&t.user), previous_locked); + + for delta in advances { + advance_ledgers(&t.env, delta); + + let staked = t.client.get_credits(&t.user); + prop_assert!( + staked > previous_staked, + "get_credits did not increase over {} ledgers: {} -> {}", + delta, previous_staked, staked + ); + + let locked = t.client.calculate_credits(&t.user); + prop_assert!( + locked > previous_locked, + "calculate_credits did not increase over {} ledgers: {} -> {}", + delta, previous_locked, locked + ); + + previous_staked = staked; + previous_locked = locked; + } + } + + /// PROPERTY D — credits are never negative, for any reachable input. + /// + /// Claim: `get_credits` and `calculate_credits` return a non-negative + /// value for every input the contract's own validation admits. + /// + /// Derivation. `get_credits` is a sum of products of provably non-negative + /// factors: + /// + /// * `credits_banked` starts at 0 and only ever `+=` a `compute_credits` + /// result, so by induction it is non-negative; + /// * `principal = A - B(A, p) >= 0`, because `p <= 100` forces + /// `B(A, p) = floor(A * p / 100) <= A`; + /// * `virtual_stake = B(A, p) * m >= 0` since `m >= 1`; + /// * `r > 0` and `elapsed >= 0` (`saturating_sub` floors it at zero). + /// + /// "Reachable input" is what makes this a real test rather than a check on + /// an unreachable state, so the generators mirror the contract's own + /// constraints exactly: `amount > 0` and `>= min_stake_amount` + /// (`stake`), `allocation_pct in 1..=100` (`set_boost`), `multiplier in + /// 1..=MAX_GLOBAL_MULTIPLIER` and `credit_rate in 1..=MAX_CREDIT_RATE` + /// (#89). Whitelisting is left disabled, its default. `multiplier == 1` + /// and `allocation_pct == 100` are both kept in range: the latter is the + /// `S = A * m` extreme, where `principal` reaches exactly zero. + /// + /// The zero-credit boundaries are covered too — a user with no position at + /// all, and a user who has fully unstaked — since "never negative" has to + /// hold at 0, not just above it. + #[test] + fn prop_credits_are_never_negative( + multiplier in any_multiplier(), + credit_rate in any_credit_rate(), + allocation_pct in any_allocation_pct(), + amount in any_deposit(), + elapsed in 0..=MAX_GAP, + ) { + let t = setup_for_props(multiplier, credit_rate); + let stranger = Address::generate(&t.env); + + // No stake and no locked position. + prop_assert_eq!(t.client.get_credits(&stranger), 0); + prop_assert_eq!(t.client.calculate_credits(&stranger), 0); + + t.client.set_boost(&t.user, &allocation_pct); + t.client.stake(&t.user, &amount); + t.client.lock_assets(&t.user, &amount); + advance_ledgers(&t.env, elapsed); + + prop_assert!(t.client.get_credits(&t.user) >= 0); + prop_assert!(t.client.calculate_credits(&t.user) >= 0); + prop_assert!(t.client.get_banked_credits(&t.user) >= 0); + + // Unstaking banks and clears the record; the getter must return to 0 + // rather than to a negative residue. + prop_assert!(t.client.unstake(&t.user) >= 0); + prop_assert_eq!(t.client.get_credits(&t.user), 0); + + // Same for the lock system, which reports credits at withdrawal time. + t.client.unlock_assets(&t.user, &amount); + prop_assert_eq!(t.client.calculate_credits(&t.user), 0); + } +} + +// ── PROPERTY E — NOT IMPLEMENTED: needs maintainer confirmation (#75) ──────── +// +// The obvious fourth invariant — "total credits are independent of checkpoint +// frequency across a *multiplier* change", the analogue of +// `test_credit_rate_change_does_not_retroactively_alter_staked_credits` — is +// deliberately absent, because the contract's intended semantics here are not +// settled and a property test either way would encode a guess as a passing +// test. +// +// The observation. `checkpoint` treats its two admin-controlled inputs +// asymmetrically: +// +// * `credit_rate` is *snapshotted* into `UserStake.credit_rate` and the +// already-elapsed segment is priced at the snapshot, so a mid-flight +// `set_credit_rate` is not retroactive. That is asserted by +// `test_credit_rate_change_does_not_retroactively_alter_staked_credits`. +// * `global_multiplier` is *re-read* by `checkpoint` via +// `read_global_multiplier` and applied to the already-elapsed segment. It +// is not snapshotted anywhere, and `set_global_multiplier` cannot +// checkpoint other users. +// +// The consequence is directly observable. With `multiplier = 2`, +// `allocation_pct = 100`, `amount = 1_000` and ten ledgers elapsed, +// `get_credits` reports 20_000. Calling `set_global_multiplier(3)` and +// advancing *zero* ledgers changes that reading to 30_000: the past segment +// was repriced. A user who happened to checkpoint before the change keeps +// 20_000 for that segment, so total credits *do* depend on checkpoint +// frequency whenever a multiplier change is in flight. +// +// Why no test is attached. `test_admin_multiplier_change_applies_from_next_ +// checkpoint` is named as though snapshot semantics hold, but it inserts a +// no-op `set_boost` checkpoint immediately before bumping the multiplier, so +// it never exercises the mid-segment case. Nothing in the suite or the +// contract settles which behaviour is intended. +// +// QUESTION FOR THE MAINTAINER: should `global_multiplier` be snapshotted into +// `UserStake` alongside `credit_rate`, so that a multiplier change is priced +// from the next checkpoint onward and matches both the rate's documented +// semantics and the sibling test's name? Or is retroactive repricing of open +// segments the intended behaviour? Once that is answered, this becomes a +// strict-equality property in the same shape as Property B (with `multiplier` +// varying mid-timeline) or an explicit regression test pinning the retroactive +// behaviour — but not before.