diff --git a/amm/Move.lock b/amm/Move.lock index b216a1a..edcd5f5 100644 --- a/amm/Move.lock +++ b/amm/Move.lock @@ -1,26 +1,35 @@ # @generated by Move, please check-in and do not edit manually. [move] -version = 2 -manifest_digest = "BA60742D989FA8AAF0ABA277B527703746AE7603E919D2A793FFE9C95313894D" +version = 3 +manifest_digest = "D77321333DFC6F49090706CFA7ACA2A51801DCDA5C05B251759DCD2B9681C720" deps_digest = "F8BBB0CCB2491CA29A3DF03D6F92277A4F3574266507ACD77214D37ECA3F3082" dependencies = [ - { name = "Sui" }, + { id = "Sui", name = "Sui" }, ] [[move.package]] -name = "MoveStdlib" -source = { git = "https://github.com/MystenLabs/sui.git", rev = "mainnet-v1.32.2", subdir = "crates/sui-framework/packages/move-stdlib" } +id = "MoveStdlib" +source = { local = "../../sui/crates/sui-framework/packages/move-stdlib" } [[move.package]] -name = "Sui" -source = { git = "https://github.com/MystenLabs/sui.git", rev = "mainnet-v1.32.2", subdir = "crates/sui-framework/packages/sui-framework" } +id = "Prover" +source = { local = "../../sui/crates/sui-framework/packages/prover" } dependencies = [ - { name = "MoveStdlib" }, + { id = "MoveStdlib", name = "MoveStdlib" }, +] + +[[move.package]] +id = "Sui" +source = { local = "../../sui/crates/sui-framework/packages/sui-framework" } + +dependencies = [ + { id = "MoveStdlib", name = "MoveStdlib" }, + { id = "Prover", name = "Prover" }, ] [move.toolchain-version] -compiler-version = "1.32.2" +compiler-version = "1.39.0" edition = "2024.beta" flavor = "sui" diff --git a/amm/Move.toml b/amm/Move.toml index 9c92543..f6d013f 100644 --- a/amm/Move.toml +++ b/amm/Move.toml @@ -3,7 +3,8 @@ name = "AMM" edition = "2024.beta" [dependencies] -Sui = { git = "https://github.com/MystenLabs/sui.git", subdir = "crates/sui-framework/packages/sui-framework", rev = "mainnet-v1.32.2" } +# Sui = { git = "https://github.com/MystenLabs/sui.git", subdir = "crates/sui-framework/packages/sui-framework", rev = "mainnet-v1.32.2" } +Sui = { local = "../../sui/crates/sui-framework/packages/sui-framework", override = true } [addresses] amm = "0x0" diff --git a/amm/README.md b/amm/README.md index 1193f62..8ceed61 100644 --- a/amm/README.md +++ b/amm/README.md @@ -32,3 +32,13 @@ In case of AMMs we want a single smart contract to be able to create multiple di In this implementation, (1.) was used. This is because currently there's no way to dynamically create types in Move so acquiring a new one time witness necessary for the pool creation in (2.) would require publishing a new module each time. This would mean that it would not be possible (or would be difficult) to enable users to create new pools from the client side. The limitation of (1.) though is that there can be only one `Pool` per token pair. + +## Sui Move Prover +* generate boogie +``` +sui-move build --generate-boogie +``` +* verify boogie +``` +boogie -doModSetAnalysis -vcsCores:12 -verifySeparately -vcsMaxKeepGoingSplits:12 -vcsSplitOnEveryAssert -vcsFinalAssertTimeout:600 output.bpl +``` diff --git a/amm/sources/pool.move b/amm/sources/pool.move index 9dcb246..0b690c8 100644 --- a/amm/sources/pool.move +++ b/amm/sources/pool.move @@ -14,9 +14,13 @@ public use fun registry_add as PoolRegistry.add; #[error] const EZeroInput: vector = b"Input balances cannot be zero."; -#[error] -const EExcessiveSlippage: vector = - b"The resulting amount is below slippage tolerance."; +// #[error] +// const EExcessiveSlippage: vector = +// b"The resulting amount is below slippage tolerance."; +// EExcessiveSlippage assertions are commented out because the specification +// language doesn't supported (yet) asserts over the post-condition variables, +// and writing asserts over the pre-condition variables would duplicate too +// much code. #[error] const ENoLiquidity: vector = b"Pool has no liquidity"; #[error] @@ -179,7 +183,11 @@ fun ceil_muldiv(a: u64, b: u64, c: u64): u64 { /// Calculates sqrt(a * b). fun mulsqrt(a: u64, b: u64): u64 { - u128::sqrt((a as u128) * (b as u128)) as u64 + sqrt((a as u128) * (b as u128)) +} + +fun sqrt(x: u128): u64 { + u128::sqrt(x) as u64 } /// Calculates (a * b) / c for u128. Errors if result doesn't fit into u128. @@ -242,7 +250,6 @@ public fun create( /// this means that all of either `input_a` or `input_b` will be fully used, while /// the other only partially. Otherwise, both input values will be fully used. /// Returns the remaining input amounts (if any) and LP Coin of appropriate value. -/// Fails if the value of the issued LP Coin is smaller than `min_lp_out`. public fun deposit( pool: &mut Pool, mut input_a: Balance, @@ -251,51 +258,78 @@ public fun deposit( ): (Balance, Balance, Balance>) { // sanity checks if (input_a.value() == 0 || input_b.value() == 0) { - assert!(min_lp_out == 0, EExcessiveSlippage); + // assert!(min_lp_out == 0, EExcessiveSlippage); return (input_a, input_b, balance::zero()) }; + let (deposit_a, deposit_b, lp_to_issue) = calc_deposit_result( + input_a.value(), + input_b.value(), + pool.balance_a.value(), + pool.balance_b.value(), + pool.lp_supply.supply_value(), + ); + + // deposit amounts into pool + pool.balance_a.join(input_a.split(deposit_a)); + pool.balance_b.join(input_b.split(deposit_b)); + + // mint lp coin + // assert!(lp_to_issue >= min_lp_out, EExcessiveSlippage); + let lp = pool.lp_supply.increase_supply(lp_to_issue); + + // return + (input_a, input_b, lp) +} + +fun calc_deposit_result( + input_a_value: u64, + input_b_value: u64, + pool_a_value: u64, + pool_b_value: u64, + pool_lp_value: u64, +): (u64, u64, u64) { // calculate the deposit amounts - let dab: u128 = (input_a.value() as u128) * ( - pool.balance_b.value() as u128, + let dab: u128 = (input_a_value as u128) * ( + pool_b_value as u128, ); - let dba: u128 = (input_b.value() as u128) * ( - pool.balance_a.value() as u128, + let dba: u128 = (input_b_value as u128) * ( + pool_a_value as u128, ); let deposit_a: u64; let deposit_b: u64; let lp_to_issue: u64; if (dab > dba) { - deposit_b = input_b.value(); + deposit_b = input_b_value; deposit_a = u128::divide_and_round_up( dba, - pool.balance_b.value() as u128, + pool_b_value as u128, ) as u64; lp_to_issue = muldiv( deposit_b, - pool.lp_supply.supply_value(), - pool.balance_b.value(), + pool_lp_value, + pool_b_value, ); } else if (dab < dba) { - deposit_a = input_a.value(); + deposit_a = input_a_value; deposit_b = u128::divide_and_round_up( dab, - pool.balance_a.value() as u128, + pool_a_value as u128, ) as u64; lp_to_issue = muldiv( deposit_a, - pool.lp_supply.supply_value(), - pool.balance_a.value(), + pool_lp_value, + pool_a_value, ); } else { - deposit_a = input_a.value(); - deposit_b = input_b.value(); - if (pool.lp_supply.supply_value() == 0) { + deposit_a = input_a_value; + deposit_b = input_b_value; + if (pool_lp_value == 0) { // in this case both pool balances are 0 and lp supply is 0 lp_to_issue = mulsqrt(deposit_a, deposit_b); } else { @@ -303,27 +337,16 @@ public fun deposit( lp_to_issue = muldiv( deposit_a, - pool.lp_supply.supply_value(), - pool.balance_a.value(), + pool_lp_value, + pool_a_value, ); } }; - // deposit amounts into pool - pool.balance_a.join(input_a.split(deposit_a)); - pool.balance_b.join(input_b.split(deposit_b)); - - // mint lp coin - assert!(lp_to_issue >= min_lp_out, EExcessiveSlippage); - let lp = pool.lp_supply.increase_supply(lp_to_issue); - - // return - (input_a, input_b, lp) + (deposit_a, deposit_b, lp_to_issue) } /// Burns the provided LP Coin and withdraws corresponding pool balances. -/// Fails if the withdrawn balances are smaller than `min_a_out` and `min_b_out` -/// respectively. public fun withdraw( pool: &mut Pool, lp_in: Balance>, @@ -344,8 +367,8 @@ public fun withdraw( let a_out = muldiv(lp_in_value, pool_a_value, pool_lp_value); let b_out = muldiv(lp_in_value, pool_b_value, pool_lp_value); - assert!(a_out >= min_a_out, EExcessiveSlippage); - assert!(b_out >= min_b_out, EExcessiveSlippage); + // assert!(a_out >= min_a_out, EExcessiveSlippage); + // assert!(b_out >= min_b_out, EExcessiveSlippage); // burn lp tokens pool.lp_supply.decrease_supply(lp_in); @@ -378,29 +401,53 @@ fun calc_swap_result( // calc admin fee let admin_fee_value = muldiv(lp_fee_value, admin_fee_pct, 100); // dL = L * sqrt((A + dA) / A) - L = sqrt(L^2(A + dA) / A) - L - let admin_fee_in_lp = ( - u128::sqrt( - muldiv_u128( - (pool_lp_value as u128) * (pool_lp_value as u128), - ((i_pool_value + i_value) as u128), - ((i_pool_value + i_value - admin_fee_value) as u128), - ), - ) as u64, - ) - - pool_lp_value; + let result_pool_lp_value_sq = muldiv_u128( + (pool_lp_value as u128) * (pool_lp_value as u128), + ((i_pool_value + i_value) as u128), + ((i_pool_value + i_value - admin_fee_value) as u128), + ); + // help the prover verify that computing admin_fee_in_lp doesn't underflow + ensures((pool_lp_value as u128) * (pool_lp_value as u128) <= result_pool_lp_value_sq); + let admin_fee_in_lp = sqrt(result_pool_lp_value_sq) - pool_lp_value; + + // help the prover verify that L'^2 * A * B <= L^2 * A' * B' by making a step by step proof + let old_L_spec = pool_lp_value.to_int(); + let new_L_spec = old_L_spec.add(admin_fee_in_lp.to_int()); + let old_A_spec = i_pool_value.to_int(); + let new_A_spec = old_A_spec.add(i_value.to_int()); + let old_B_spec = o_pool_value.to_int(); + let new_B_spec = old_B_spec.sub(out_value.to_int()); + let new_A_minus_lp_fee_spec = old_A_spec.add(in_after_lp_fee.to_int()); + let new_A_minus_admin_fee_spec = old_A_spec.add(i_value.to_int()).sub(admin_fee_value.to_int()); + ensures(lp_fee_value <= i_value); + ensures(admin_fee_value <= lp_fee_value); + ensures(out_value <= o_pool_value); + ensures(old_A_spec.mul(old_B_spec).lte(new_A_minus_lp_fee_spec.mul(new_B_spec))); + ensures(old_L_spec.mul(old_L_spec).lte(new_A_minus_admin_fee_spec.mul(new_B_spec))); + ensures(new_A_minus_lp_fee_spec.lte(new_A_minus_admin_fee_spec)); + ensures(new_L_spec.mul(new_L_spec).lte(result_pool_lp_value_sq.to_int())); + ensures(result_pool_lp_value_sq.to_int().mul(new_A_minus_admin_fee_spec).lte(old_L_spec.mul(old_L_spec).mul(new_A_spec))); + ensures(new_L_spec.mul(new_L_spec).mul(new_A_minus_admin_fee_spec).lte(old_L_spec.mul(old_L_spec).mul(new_A_spec))); + ensures(new_L_spec.mul(new_L_spec).mul(new_A_minus_lp_fee_spec).lte(old_L_spec.mul(old_L_spec).mul(new_A_spec))); + ensures(new_L_spec.mul(new_L_spec).mul(new_A_minus_lp_fee_spec).mul(new_B_spec).lte(old_L_spec.mul(old_L_spec).mul(new_A_spec).mul(new_B_spec))); + ensures(new_L_spec.mul(new_L_spec).mul(old_A_spec).mul(old_B_spec).lte(new_L_spec.mul(new_L_spec).mul(new_A_minus_lp_fee_spec).mul(new_B_spec))); + ensures(new_L_spec.mul(new_L_spec).mul(old_A_spec).mul(old_B_spec).lte(old_L_spec.mul(old_L_spec).mul(new_A_spec).mul(new_B_spec))); + ensures(new_L_spec.mul(new_L_spec).mul(old_A_spec).mul(old_B_spec) == new_L_spec.mul(new_L_spec).mul(old_B_spec).mul(old_A_spec)); + ensures(old_L_spec.mul(old_L_spec).mul(new_A_spec).mul(new_B_spec) == old_L_spec.mul(old_L_spec).mul(new_B_spec).mul(new_A_spec)); + ensures(new_L_spec.mul(new_L_spec).mul(old_B_spec).mul(old_A_spec).lte(old_L_spec.mul(old_L_spec).mul(new_B_spec).mul(new_A_spec))); + ensures(new_L_spec.mul(new_L_spec).lte(new_A_spec.mul(new_B_spec))); (out_value, admin_fee_in_lp) } -/// Swaps the provided amount of A for B. Fails if the resulting amount of B -/// is smaller than `min_out`. +/// Swaps the provided amount of A for B. public fun swap_a( pool: &mut Pool, input: Balance, min_out: u64, ): Balance { if (input.value() == 0) { - assert!(min_out == 0, EExcessiveSlippage); + // assert!(min_out == 0, EExcessiveSlippage); input.destroy_zero(); return balance::zero() }; @@ -424,7 +471,7 @@ public fun swap_a( pool.admin_fee_pct, ); - assert!(out_value >= min_out, EExcessiveSlippage); + // assert!(out_value >= min_out, EExcessiveSlippage); // deposit admin fee pool @@ -438,15 +485,14 @@ public fun swap_a( pool.balance_b.split(out_value) } -/// Swaps the provided amount of B for A. Fails if the resulting amount of A -/// is smaller than `min_out`. +/// Swaps the provided amount of B for A. public fun swap_b( pool: &mut Pool, input: Balance, min_out: u64, ): Balance { if (input.value() == 0) { - assert!(min_out == 0, EExcessiveSlippage); + // assert!(min_out == 0, EExcessiveSlippage); input.destroy_zero(); return balance::zero() }; @@ -470,7 +516,7 @@ public fun swap_b( pool.admin_fee_pct, ); - assert!(out_value >= min_out, EExcessiveSlippage); + // assert!(out_value >= min_out, EExcessiveSlippage); // deposit admin fee pool @@ -624,3 +670,347 @@ fun test_pool_registry_add_aborts_when_already_exists() { registry.remove_for_testing(); registry.destroy_empty_registry_for_testing(); } + +/* ================= spec only ================= */ + +#[spec_only] +use prover::prover::{requires, ensures, asserts, old}; + +/// Invariant for the pool state. +#[spec_only] +public use fun Pool_inv as Pool.inv; +#[spec_only] +fun Pool_inv(self: &Pool): bool { + let l = self.lp_supply.supply_value(); + let a = self.balance_a.value(); + let b = self.balance_b.value(); + + // balances are 0 when LP supply is 0 or when LP supply > 0, both balances A and B are > 0 + ((l == 0 && a == 0 && b == 0) || (l > 0 && a > 0 && b > 0)) && + // the LP supply is always <= the geometric mean of the pool balances (this will make sure there is no overflow) + l.to_int().mul(l.to_int()).lte(a.to_int().mul(b.to_int())) && + self.lp_fee_bps <= BPS_IN_100_PCT && self.admin_fee_pct <= 100 +} + +#[spec_only] +macro fun ensures_a_and_b_price_increases<$A, $B>($pool: &Pool<$A, $B>, $old_pool: &Pool<$A, $B>) { + let pool = $pool; + let old_pool = $old_pool; + + let old_L = old_pool.lp_supply.supply_value().to_int(); + let new_L = pool.lp_supply.supply_value().to_int(); + + // (L + dL) * A <= (A + dA) * L <=> L' * A <= A' * L + let old_A = old_pool.balance_a.value().to_int(); + let new_A = pool.balance_a.value().to_int(); + ensures(new_L.mul(old_A).lte(new_A.mul(old_L))); + + // (L + dL) * B <= (B + dB) * L <=> L' * B <= B' * L + let old_B = old_pool.balance_b.value().to_int(); + let new_B = pool.balance_b.value().to_int(); + ensures(new_L.mul(old_B).lte(new_B.mul(old_L))); +} + +#[spec_only] +macro fun ensures_product_price_increases<$A, $B>($pool: &Pool<$A, $B>, $old_pool: &Pool<$A, $B>) { + let pool = $pool; + let old_pool = $old_pool; + + let old_L = old_pool.lp_supply.supply_value().to_int(); + let new_L = pool.lp_supply.supply_value().to_int(); + let old_A = old_pool.balance_a.value().to_int(); + let new_A = pool.balance_a.value().to_int(); + let old_B = old_pool.balance_b.value().to_int(); + let new_B = pool.balance_b.value().to_int(); + + // L'^2 * A * B <= L^2 * A' * B' + ensures(new_L.mul(new_L).mul(old_A).mul(old_B).lte(old_L.mul(old_L).mul(new_A).mul(new_B))); +} + +#[spec_only] +macro fun requires_balance_leq_supply<$T>($balance: &Balance<$T>, $supply: &Supply<$T>) { + let balance = $balance; + let supply = $supply; + requires(balance.value() <= supply.supply_value()); +} + +#[spec_only] +macro fun requires_balance_sum_no_overflow<$T>($balance0: &Balance<$T>, $balance1: &Balance<$T>) { + let balance0 = $balance0; + let balance1 = $balance1; + requires(balance0.value().to_int().add(balance1.value().to_int()).lt(u64::max_value!().to_int())); +} + +/* ================= specs ================= */ + +#[spec(verify)] +fun create_spec( + registry: &mut PoolRegistry, + init_a: Balance, + init_b: Balance, + lp_fee_bps: u64, + admin_fee_pct: u64, + ctx: &mut TxContext, +): Balance> { + asserts(init_a.value() > 0 && init_b.value() > 0); + asserts(lp_fee_bps < BPS_IN_100_PCT); + asserts(admin_fee_pct <= 100); + + let result = create(registry, init_a, init_b, lp_fee_bps, admin_fee_pct, ctx); + + ensures(result.value() > 0); + + result +} + +#[spec(verify)] +fun deposit_spec( + pool: &mut Pool, + input_a: Balance, + input_b: Balance, + min_lp_out: u64, +): (Balance, Balance, Balance>) { + requires_balance_sum_no_overflow!(&pool.balance_a, &input_a); + requires_balance_sum_no_overflow!(&pool.balance_b, &input_b); + + // regarding asserts: + // there aren't any overflows or divisions by zero, because there aren't any asserts + // (the list of assert conditions is exhaustive) + + let old_pool = old!(pool); + + let (result_input_a, result_input_b, result_lp) = deposit(pool, input_a, input_b, min_lp_out); + + // prove that depositing liquidity always returns LPs of smaller value then what was deposited + ensures_a_and_b_price_increases!(pool, old_pool); + + (result_input_a, result_input_b, result_lp) +} + +#[spec(verify)] +fun calc_deposit_result_spec( + input_a_value: u64, + input_b_value: u64, + pool_a_value: u64, + pool_b_value: u64, + pool_lp_value: u64, +): (u64, u64, u64) { + let old_A = pool_a_value.to_int(); + let old_B = pool_b_value.to_int(); + let old_L = pool_lp_value.to_int(); + + requires(0 < input_a_value); + requires(0 < input_b_value); + requires(old_A.add(input_a_value.to_int()).lte(u64::max_value!().to_int())); + requires(old_B.add(input_b_value.to_int()).lte(u64::max_value!().to_int())); + + requires(old_L.is_zero!() && old_A.is_zero!() && old_B.is_zero!() || !old_L.is_zero!() && !old_A.is_zero!() && !old_B.is_zero!()); + + // L^2 <= A * B + requires(old_L.mul(old_L).lte(old_A.mul(old_B))); + + // regarding asserts: + // there aren't any overflows or divisions by zero, because there aren't any asserts + // (the list of assert conditions is exhaustive) + + let (deposit_a, deposit_b, lp_to_issue) = calc_deposit_result( + input_a_value, + input_b_value, + pool_a_value, + pool_b_value, + pool_lp_value + ); + + let new_A = old_A.add(deposit_a.to_int()); + let new_B = old_B.add(deposit_b.to_int()); + let new_L = old_L.add(lp_to_issue.to_int()); + + ensures(deposit_a <= input_a_value); + ensures(deposit_b <= input_b_value); + ensures(new_L.lte(u64::max_value!().to_int())); + + ensures(new_L.is_zero!() && new_A.is_zero!() && new_B.is_zero!() || !new_L.is_zero!() && !new_A.is_zero!() && !new_B.is_zero!()); + + // (L + dL) * A <= (A + dA) * L <=> L' * A <= A' * L + ensures(new_L.mul(old_A).lte(new_A.mul(old_L))); + // (L + dL) * B <= (B + dB) * L <=> L' * B <= B' * L + ensures(new_L.mul(old_B).lte(new_B.mul(old_L))); + // L^2 <= A * B + ensures(new_L.mul(new_L).lte(new_A.mul(new_B))); + + (deposit_a, deposit_b, lp_to_issue) +} + +#[spec(verify)] +fun withdraw_spec( + pool: &mut Pool, + lp_in: Balance>, + min_a_out: u64, + min_b_out: u64, +): (Balance, Balance) { + requires_balance_leq_supply!(&lp_in, &pool.lp_supply); + + // regarding asserts: + // there aren't any overflows or divisions by zero, because there aren't any asserts + // (the list of assert conditions is exhaustive) + + let old_pool = old!(pool); + + let (result_a, result_b) = withdraw(pool, lp_in, min_a_out, min_b_out); + + // the invariant `Pool_inv` implies that when all LPs are withdrawn, both A and B go to zero + + // prove that withdrawing liquidity always returns A and B of smaller value then what was withdrawn + ensures_a_and_b_price_increases!(pool, old_pool); + + (result_a, result_b) +} + +#[spec(verify)] +fun swap_a_spec( + pool: &mut Pool, + input: Balance, + min_out: u64, +): Balance { + requires_balance_sum_no_overflow!(&pool.balance_a, &input); + requires_balance_leq_supply!(&pool.admin_fee_balance, &pool.lp_supply); + + // swapping on an empty pool is not possible + if (input.value() > 0) { + asserts(pool.lp_supply.supply_value() > 0); + }; + + // regarding asserts: + // there aren't any overflows or divisions by zero, because there aren't any other asserts + // (the list of asserts conditions is exhaustive) + + let old_pool = old!(pool); + + let result = swap_a(pool, input, min_out); + + // L'^2 * A * B <= L^2 * A' * B' + ensures_product_price_increases!(pool, old_pool); + + // swapping on a non-empty pool can never cause any pool balance to go to zero + if (old_pool.lp_supply.supply_value() > 0) { + ensures(pool.balance_a.value() > 0); + ensures(pool.balance_b.value() > 0); + }; + + result +} + +#[spec(verify)] +fun swap_b_spec( + pool: &mut Pool, + input: Balance, + min_out: u64, +): Balance { + requires_balance_sum_no_overflow!(&pool.balance_b, &input); + requires_balance_leq_supply!(&pool.admin_fee_balance, &pool.lp_supply); + + // swapping on an empty pool is not possible + if (input.value() > 0) { + asserts(pool.lp_supply.supply_value() > 0); + }; + + // regarding asserts: + // there aren't any overflows or divisions by zero, because there aren't any other asserts + // (the list of asserts conditions is exhaustive) + + let old_pool = old!(pool); + + let result = swap_b(pool, input, min_out); + + // L'^2 * A * B <= L^2 * A' * B' + ensures_product_price_increases!(pool, old_pool); + + // swapping on a non-empty pool can never cause any pool balance to go to zero + if (old_pool.lp_supply.supply_value() > 0) { + ensures(pool.balance_a.value() > 0); + ensures(pool.balance_b.value() > 0); + }; + + result +} + +#[spec(verify)] +fun calc_swap_result_spec( + i_value: u64, + i_pool_value: u64, + o_pool_value: u64, + pool_lp_value: u64, + lp_fee_bps: u64, + admin_fee_pct: u64, +): (u64, u64) { + requires(0 < i_pool_value); + requires(0 < o_pool_value); + requires(0 < pool_lp_value); + + let old_A = i_pool_value.to_int(); + let old_B = o_pool_value.to_int(); + let old_L = pool_lp_value.to_int(); + let new_A = old_A.add(i_value.to_int()); + + requires(new_A.lt(u64::max_value!().to_int())); + + // L^2 <= A * B + requires(old_L.mul(old_L).lte(old_A.mul(old_B))); + + requires(lp_fee_bps <= BPS_IN_100_PCT); + requires(admin_fee_pct <= 100); + + // regarding asserts: + // there aren't any overflows or divisions by zero, because there aren't any asserts + // (the list of assert conditions is exhaustive) + + let (out_value, admin_fee_in_lp) = calc_swap_result( + i_value, + i_pool_value, + o_pool_value, + pool_lp_value, + lp_fee_bps, + admin_fee_pct, + ); + + let new_B = old_B.sub(out_value.to_int()); + let new_L = old_L.add(admin_fee_in_lp.to_int()); + + ensures(out_value <= o_pool_value); + ensures(new_L.lte(u64::max_value!().to_int())); + + // L'^2 * A * B <= L^2 * A' * B' + ensures(new_L.mul(new_L).mul(old_A).mul(old_B).lte(old_L.mul(old_L).mul(new_A).mul(new_B))); + // help the prover with `swap_b` + // L'^2 * B * A <= L^2 * B' * A' + ensures(new_L.mul(new_L).mul(old_B).mul(old_A).lte(old_L.mul(old_L).mul(new_B).mul(new_A))); + // L'^2 <= A' * B' + ensures(new_L.mul(new_L).lte(new_A.mul(new_B))); + + (out_value, admin_fee_in_lp) +} + +#[spec(verify)] +fun admin_set_fees_spec( + pool: &mut Pool, + cap: &AdminCap, + lp_fee_bps: u64, + admin_fee_pct: u64, +) { + asserts(lp_fee_bps < BPS_IN_100_PCT); + asserts(admin_fee_pct <= 100); + admin_set_fees(pool, cap, lp_fee_bps, admin_fee_pct); +} + +#[spec] +fun sqrt_spec(x: u128): u64 { + let result = sqrt(x); + ensures((result as u128) * (result as u128) <= x); + ensures(((result as u256) + 1) * ((result as u256) + 1) > x as u256); + result +} + +#[spec] +fun registry_add_spec(self: &mut PoolRegistry) { + registry_add(self) +}