From b038478198bc51970ec749ced4d0b6b18dc6c0d2 Mon Sep 17 00:00:00 2001 From: hpmaxi <358059+hpmaxi@users.noreply.github.com> Date: Wed, 23 Sep 2026 15:36:48 -0300 Subject: [PATCH 1/2] test: verify conversion arithmetic invariants --- contracts/async-vault/Cargo.toml | 1 + contracts/async-vault/src/test/conversions.rs | 201 ++++++++++++++++++ 2 files changed, 202 insertions(+) diff --git a/contracts/async-vault/Cargo.toml b/contracts/async-vault/Cargo.toml index 2da5c3d..570854b 100644 --- a/contracts/async-vault/Cargo.toml +++ b/contracts/async-vault/Cargo.toml @@ -28,3 +28,4 @@ proptest = "1" [features] upgrade_wasm = [] +kani = [] diff --git a/contracts/async-vault/src/test/conversions.rs b/contracts/async-vault/src/test/conversions.rs index 90f2848..921aceb 100644 --- a/contracts/async-vault/src/test/conversions.rs +++ b/contracts/async-vault/src/test/conversions.rs @@ -76,3 +76,204 @@ fn conversion_arithmetic_holds_its_rounding_direction() { prop_assert!(back <= shares); }); } + +#[test] +fn deposit_and_redeem_round_trip_never_manufactures_assets() { + let env = Env::default(); + env.cost_estimate().budget().reset_unlimited(); + + // Property holds across massive scale (up to 10^30), handled via I256 scaling. + proptest!(|( + assets in 0i128..=1_000_000_000_000_000_000_000_000_000_000i128, + price in 1i128..=1_000_000_000_000_000_000_000_000_000_000i128, + )| { + if let Some(shares) = checked_mul_div_floor(&env, &assets, &WAD_SCALE, &price) { + if let Some(back_assets) = checked_mul_div_floor(&env, &shares, &price, &WAD_SCALE) { + // Invariant: round-trip through shares can never yield more assets than started. + prop_assert!(back_assets <= assets); + } + } + }); +} + +#[test] +fn redeem_and_deposit_round_trip_never_manufactures_shares() { + let env = Env::default(); + env.cost_estimate().budget().reset_unlimited(); + + proptest!(|( + shares in 0i128..=1_000_000_000_000_000_000_000_000_000_000i128, + price in 1i128..=1_000_000_000_000_000_000_000_000_000_000i128, + )| { + if let Some(assets) = checked_mul_div_floor(&env, &shares, &price, &WAD_SCALE) { + if let Some(back_shares) = checked_mul_div_floor(&env, &assets, &WAD_SCALE, &price) { + // Invariant: round-trip through assets can never yield more shares than started. + prop_assert!(back_shares <= shares); + } + } + }); +} + +#[test] +fn deposit_floor_is_strictly_tight() { + let env = Env::default(); + env.cost_estimate().budget().reset_unlimited(); + + proptest!(|( + assets in 0i128..=1_000_000_000_000_000i128, + price in 1i128..=1_000_000_000_000_000i128, + )| { + let shares = checked_mul_div_floor(&env, &assets, &WAD_SCALE, &price).unwrap(); + + // Never mints more shares than backed by assets. + prop_assert!(shares * price <= assets * WAD_SCALE); + // Floor is tight: not a single additional share could be minted. + prop_assert!((shares + 1) * price > assets * WAD_SCALE); + }); +} + +#[test] +fn conversion_monotonicity_in_amount_and_price() { + let env = Env::default(); + env.cost_estimate().budget().reset_unlimited(); + + proptest!(|( + a1 in 0i128..=1_000_000_000_000_000_000_000i128, + a2 in 0i128..=1_000_000_000_000_000_000_000i128, + p1 in 1i128..=1_000_000_000_000_000_000_000i128, + p2 in 1i128..=1_000_000_000_000_000_000_000i128, + )| { + let (amin, amax) = if a1 <= a2 { (a1, a2) } else { (a2, a1) }; + let (pmin, pmax) = if p1 <= p2 { (p1, p2) } else { (p2, p1) }; + + // Monotonic in amount: + if let (Some(s_low), Some(s_high)) = ( + checked_mul_div_floor(&env, &amin, &WAD_SCALE, &pmin), + checked_mul_div_floor(&env, &amax, &WAD_SCALE, &pmin), + ) { + prop_assert!(s_low <= s_high); + } + + if let (Some(a_low), Some(a_high)) = ( + checked_mul_div_floor(&env, &amin, &pmin, &WAD_SCALE), + checked_mul_div_floor(&env, &amax, &pmin, &WAD_SCALE), + ) { + prop_assert!(a_low <= a_high); + } + + // Monotonic in price: + if let (Some(s_cheap), Some(s_dear)) = ( + checked_mul_div_floor(&env, &amax, &WAD_SCALE, &pmin), + checked_mul_div_floor(&env, &amax, &WAD_SCALE, &pmax), + ) { + prop_assert!(s_dear <= s_cheap); + } + + if let (Some(a_cheap), Some(a_dear)) = ( + checked_mul_div_floor(&env, &amax, &pmin, &WAD_SCALE), + checked_mul_div_floor(&env, &amax, &pmax, &WAD_SCALE), + ) { + prop_assert!(a_cheap <= a_dear); + } + }); +} + +#[test] +fn wind_down_pro_rata_sum_never_exceeds_pot() { + let env = Env::default(); + env.cost_estimate().budget().reset_unlimited(); + + proptest!(|( + pot in 1i128..=1_000_000_000_000_000_000_000_000i128, + e1 in 1i128..=1_000_000_000_000_000_000i128, + e2 in 1i128..=1_000_000_000_000_000_000i128, + e3 in 1i128..=1_000_000_000_000_000_000i128, + )| { + let snapshot = e1 + e2 + e3; + let delta = checked_mul_div_floor(&env, &pot, &WAD_SCALE, &snapshot).unwrap(); + + let c1 = checked_mul_div_floor(&env, &e1, &delta, &WAD_SCALE).unwrap(); + let c2 = checked_mul_div_floor(&env, &e2, &delta, &WAD_SCALE).unwrap(); + let c3 = checked_mul_div_floor(&env, &e3, &delta, &WAD_SCALE).unwrap(); + + let total_paid = c1 + c2 + c3; + // The vault can never overpay capital during wind-down distribution. + prop_assert!(total_paid <= pot); + }); +} + +#[test] +fn negative_control_ceil_division_violates_conservation() { + // Demonstration that ceiling division allows arbitrage (value creation). + // If an investor deposits 100 assets at price 3, ceil gives ceil(100 * 10 / 3) = 334. + // Redeeming 334 shares at price 3 with ceil gives ceil(334 * 3 / 10) = 101 > 100! + fn ceil_div(x: i128, y: i128) -> i128 { + (x + y - 1) / y + } + + let assets: i128 = 100; + let price: i128 = 3; + let scale: i128 = 10; + + let shares_ceil = ceil_div(assets * scale, price); + let redeemed_ceil = ceil_div(shares_ceil * price, scale); + + // Ceil manufactures an extra asset unit (101 > 100): + assert!(redeemed_ceil > assets); + + // In contrast, floor division guarantees non-inflationary conservation: + let env = Env::default(); + let shares_floor = checked_mul_div_floor(&env, &assets, &scale, &price).unwrap(); + let redeemed_floor = checked_mul_div_floor(&env, &shares_floor, &price, &scale).unwrap(); + assert!(redeemed_floor <= assets); +} + +// Bounded symbolic model checking harnesses for Kani (cbmc backend). +// When run under `cargo kani` (or `--features kani`), these verify the invariants symbolically. +#[cfg(feature = "kani")] +mod kani_proofs { + #[kani::proof] + fn prove_round_trip_deposit_redeem_conservation() { + let assets: i128 = kani::any(); + let price: i128 = kani::any(); + let wad: i128 = 1_000_000_000_000_000_000; + + kani::assume(assets >= 0 && assets <= 1_000_000_000_000); + kani::assume(price > 0 && price <= 1_000_000_000_000); + + let shares = (assets * wad) / price; + let redeemed = (shares * price) / wad; + + assert!(redeemed <= assets); + } + + #[kani::proof] + fn prove_round_trip_redeem_deposit_conservation() { + let shares: i128 = kani::any(); + let price: i128 = kani::any(); + let wad: i128 = 1_000_000_000_000_000_000; + + kani::assume(shares >= 0 && shares <= 1_000_000_000_000); + kani::assume(price > 0 && price <= 1_000_000_000_000); + + let assets = (shares * price) / wad; + let minted = (assets * wad) / price; + + assert!(minted <= shares); + } + + #[kani::proof] + fn prove_floor_tightness() { + let assets: i128 = kani::any(); + let price: i128 = kani::any(); + let wad: i128 = 1_000_000_000_000_000_000; + + kani::assume(assets >= 0 && assets <= 1_000_000_000_000); + kani::assume(price > 0 && price <= 1_000_000_000_000); + + let shares = (assets * wad) / price; + + assert!(shares * price <= assets * wad); + assert!((shares + 1) * price > assets * wad); + } +} From 9d95e6c45e67b525d8186179664c3e9180bc38c4 Mon Sep 17 00:00:00 2001 From: hpmaxi <358059+hpmaxi@users.noreply.github.com> Date: Fri, 25 Sep 2026 07:42:13 -0300 Subject: [PATCH 2/2] test: check wind-down payouts against the accumulator and drop kani The wind-down property now follows the accumulator and earned - paid across rounds and claims. The Kani harnesses never ran and proved a hand-written formula; the helper's overflow path goes through the host's I256, which Kani cannot model. --- contracts/async-vault/Cargo.toml | 1 - .../proptest-regressions/test/conversions.txt | 7 ++ contracts/async-vault/src/test/conversions.rs | 98 +++++++------------ 3 files changed, 41 insertions(+), 65 deletions(-) create mode 100644 contracts/async-vault/proptest-regressions/test/conversions.txt diff --git a/contracts/async-vault/Cargo.toml b/contracts/async-vault/Cargo.toml index 570854b..2da5c3d 100644 --- a/contracts/async-vault/Cargo.toml +++ b/contracts/async-vault/Cargo.toml @@ -28,4 +28,3 @@ proptest = "1" [features] upgrade_wasm = [] -kani = [] diff --git a/contracts/async-vault/proptest-regressions/test/conversions.txt b/contracts/async-vault/proptest-regressions/test/conversions.txt new file mode 100644 index 0000000..1ea3f4f --- /dev/null +++ b/contracts/async-vault/proptest-regressions/test/conversions.txt @@ -0,0 +1,7 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc 4d14c32ed3dd0df31ca20a986ba42cc3ce1721d2f02745dc8f4d0f7146813253 # shrinks to entitlements = [142643168002378746, 489350658678829759, 832474737339641506], pots = [542590092922923427742683, 58710666963727846758920], claims = [[false, false, false], [false, false, false], [false, false, false], [false, false, false], [false, false, false], [false, false, false]] diff --git a/contracts/async-vault/src/test/conversions.rs b/contracts/async-vault/src/test/conversions.rs index 921aceb..05cbb67 100644 --- a/contracts/async-vault/src/test/conversions.rs +++ b/contracts/async-vault/src/test/conversions.rs @@ -179,26 +179,46 @@ fn conversion_monotonicity_in_amount_and_price() { } #[test] -fn wind_down_pro_rata_sum_never_exceeds_pot() { +fn wind_down_accumulator_never_pays_more_than_it_credits() { let env = Env::default(); env.cost_estimate().budget().reset_unlimited(); proptest!(|( - pot in 1i128..=1_000_000_000_000_000_000_000_000i128, - e1 in 1i128..=1_000_000_000_000_000_000i128, - e2 in 1i128..=1_000_000_000_000_000_000i128, - e3 in 1i128..=1_000_000_000_000_000_000i128, + entitlements in prop::array::uniform3(1i128..=1_000_000_000_000_000_000i128), + pots in prop::collection::vec(1i128..=1_000_000_000_000_000_000_000_000i128, 1..6), + claims in prop::collection::vec(any::<[bool; 3]>(), 6), )| { - let snapshot = e1 + e2 + e3; - let delta = checked_mul_div_floor(&env, &pot, &WAD_SCALE, &snapshot).unwrap(); - - let c1 = checked_mul_div_floor(&env, &e1, &delta, &WAD_SCALE).unwrap(); - let c2 = checked_mul_div_floor(&env, &e2, &delta, &WAD_SCALE).unwrap(); - let c3 = checked_mul_div_floor(&env, &e3, &delta, &WAD_SCALE).unwrap(); + let floor = |x: i128, y: i128, d: i128| checked_mul_div_floor(&env, &x, &y, &d).unwrap(); + let snapshot: i128 = entitlements.iter().sum(); + let mut acc = 0i128; + let mut owed = 0i128; + let mut paid = [0i128; 3]; + + for (round, &pot) in pots.iter().enumerate() { + let delta = floor(pot, WAD_SCALE, snapshot); + if delta == 0 { + continue; + } + let acc_after = acc + delta; + let credited = floor(snapshot, acc_after, WAD_SCALE) - floor(snapshot, acc, WAD_SCALE); + prop_assert!(credited <= pot); + acc = acc_after; + owed += credited; + + for (i, &claims_now) in claims[round].iter().enumerate() { + if claims_now { + let earned = floor(entitlements[i], acc, WAD_SCALE); + prop_assert!(earned >= paid[i]); + paid[i] = earned; + } + } + prop_assert!(paid.iter().sum::() <= owed); + } - let total_paid = c1 + c2 + c3; - // The vault can never overpay capital during wind-down distribution. - prop_assert!(total_paid <= pot); + for i in 0..3 { + paid[i] = floor(entitlements[i], acc, WAD_SCALE); + } + prop_assert!(paid.iter().sum::() <= owed); }); } @@ -227,53 +247,3 @@ fn negative_control_ceil_division_violates_conservation() { let redeemed_floor = checked_mul_div_floor(&env, &shares_floor, &price, &scale).unwrap(); assert!(redeemed_floor <= assets); } - -// Bounded symbolic model checking harnesses for Kani (cbmc backend). -// When run under `cargo kani` (or `--features kani`), these verify the invariants symbolically. -#[cfg(feature = "kani")] -mod kani_proofs { - #[kani::proof] - fn prove_round_trip_deposit_redeem_conservation() { - let assets: i128 = kani::any(); - let price: i128 = kani::any(); - let wad: i128 = 1_000_000_000_000_000_000; - - kani::assume(assets >= 0 && assets <= 1_000_000_000_000); - kani::assume(price > 0 && price <= 1_000_000_000_000); - - let shares = (assets * wad) / price; - let redeemed = (shares * price) / wad; - - assert!(redeemed <= assets); - } - - #[kani::proof] - fn prove_round_trip_redeem_deposit_conservation() { - let shares: i128 = kani::any(); - let price: i128 = kani::any(); - let wad: i128 = 1_000_000_000_000_000_000; - - kani::assume(shares >= 0 && shares <= 1_000_000_000_000); - kani::assume(price > 0 && price <= 1_000_000_000_000); - - let assets = (shares * price) / wad; - let minted = (assets * wad) / price; - - assert!(minted <= shares); - } - - #[kani::proof] - fn prove_floor_tightness() { - let assets: i128 = kani::any(); - let price: i128 = kani::any(); - let wad: i128 = 1_000_000_000_000_000_000; - - kani::assume(assets >= 0 && assets <= 1_000_000_000_000); - kani::assume(price > 0 && price <= 1_000_000_000_000); - - let shares = (assets * wad) / price; - - assert!(shares * price <= assets * wad); - assert!((shares + 1) * price > assets * wad); - } -}