Merge pull request #11 from aldrin-labs/remove-prover-specs

Remove Sui Move Prover specs
aldrin-labs · Mar 5, 2024 · c76caa1 · c76caa1
2 parents f44787d + 584daf6
commit c76caa1
Show file tree

Hide file tree

Showing 20 changed files with 389 additions and 724 deletions.
diff --git a/ramm-sui/Move.lock b/ramm-sui/Move.lock
@@ -2,7 +2,7 @@
 
 [move]
 version = 0
-manifest_digest = "A58C4DBBBBFB6082AB1CA78C64AAB0617451D817CFCF4CA6EDCDEDC14002E878"
+manifest_digest = "C38B0A789416AADBCC8558671B942576B831C3E0D0837DEB1A19A250FA0F15AA"
 deps_digest = "060AD7E57DFB13104F21BE5F5C3759D03F0553FC3229247D9A7A6B45F50D03A3"
 
 dependencies = [

diff --git a/ramm-sui/Move.toml b/ramm-sui/Move.toml
@@ -1,7 +1,6 @@
 [package]
 name = "ramm_sui"
 version = "0.0.1"
-edition = "2024.alpha"
 
 [dependencies]
 Sui = { git = "https://github.com/MystenLabs/sui.git", subdir = "crates/sui-framework/packages/sui-framework", rev = "testnet" }

diff --git a/ramm-sui/sources/events.move b/ramm-sui/sources/events.move
@@ -27,7 +27,7 @@ module ramm_sui::events {
     As such, they are defined here.
     */
 
-    public struct PoolStateEvent has copy, drop {
+    struct PoolStateEvent has copy, drop {
         ramm_id: ID,
         sender: address,
         asset_types: vector<TypeName>,
@@ -54,16 +54,16 @@ module ramm_sui::events {
     }
 
     /// Phantom type to mark a `TradeEvent` as the result of `trade_amount_in`
-    public struct TradeIn {}
+    struct TradeIn {}
     /// Phantom type to mark a `TradeEvent` as the result of `trade_amount_out`
-    public struct TradeOut {}
+    struct TradeOut {}
 
     /// Datatype used to emit, to the Sui blockchain, information on a successful trade.
     ///
     /// A phantom type is used to mark whether it's the result of a call to `trade_amount_in`
     /// (selling an exact amount of an asset to the RAMM), or to `trade_amount_out` (buying
     /// an exact amount of an asset from the RAMM).
-    public struct TradeEvent<phantom TradeType> has copy, drop {
+    struct TradeEvent<phantom TradeType> has copy, drop {
         ramm_id: ID,
         trader: address,
         token_in: TypeName,
@@ -105,7 +105,7 @@ module ramm_sui::events {
     /// A phantom type is used to mark whether it's the result of a call to `trade_amount_in`
     /// (selling an exact amount of an asset to the RAMM), or to `trade_amount_out` (buying
     /// an exact amount of an asset from the RAMM).
-    public struct TradeFailure<phantom TradeType> has copy, drop {
+    struct TradeFailure<phantom TradeType> has copy, drop {
         ramm_id: ID,
         trader: address,
         token_in: TypeName,
@@ -137,7 +137,7 @@ module ramm_sui::events {
     }
 
     /// Datatype used to emit, to the Sui blockchain, information on a successful liquidity deposit.
-    public struct LiquidityDepositEvent has copy, drop {
+    struct LiquidityDepositEvent has copy, drop {
         ramm_id: ID,
         trader: address,
         token_in: TypeName,
@@ -166,7 +166,7 @@ module ramm_sui::events {
     }
 
     /// Datatype describing a Sui event for a given RAMM's liquidity withdrawal.
-    public struct LiquidityWithdrawalEvent has copy, drop {
+    struct LiquidityWithdrawalEvent has copy, drop {
         ramm_id: ID,
         trader: address,
         token_out: TypeName,
@@ -198,7 +198,7 @@ module ramm_sui::events {
     }
 
     /// Datatype describing a Sui event for a given RAMM's fee collection.
-    public struct FeeCollectionEvent has copy, drop {
+    struct FeeCollectionEvent has copy, drop {
         ramm_id: ID,
         admin: address,
         fee_collector: address,

diff --git a/ramm-sui/sources/interface2.move b/ramm-sui/sources/interface2.move
@@ -77,9 +77,9 @@ module ramm_sui::interface2 {
         ramm::check_trade_amount_in<AssetIn>(self, (coin::value(&amount_in) as u256));
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -159,7 +159,7 @@ module ramm_sui::interface2 {
         let amount_out_u64: u64 = (amount_out_u256 as u64);
             if (ramm::execute(&trade)) {
                 if (amount_out_u64 >= min_ao) {
-                let mut amount_in: Balance<AssetIn> = coin::into_balance(amount_in);
+                let amount_in: Balance<AssetIn> = coin::into_balance(amount_in);
 
                 let fee: u64 = (ramm::protocol_fee(&trade) as u64);
                 let fee_bal: Balance<AssetIn> = balance::split(&mut amount_in, fee);
@@ -230,9 +230,9 @@ module ramm_sui::interface2 {
         ramm::check_trade_amount_out<AssetOut>(self, (amount_out as u256));
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -305,8 +305,8 @@ module ramm_sui::interface2 {
         let max_ai_u64: u64 = coin::value(&max_ai);
         if (ramm::execute(&trade)) {
             if (trade_amount <= max_ai_u64) {
-                let mut max_ai: Balance<AssetIn> = coin::into_balance(max_ai);
-                let mut amount_in: Balance<AssetIn> = balance::split(&mut max_ai, trade_amount);
+                let max_ai: Balance<AssetIn> = coin::into_balance(max_ai);
+                let amount_in: Balance<AssetIn> = balance::split(&mut max_ai, trade_amount);
                 let remainder = max_ai;
 
                 let fee: u64 = (ramm::protocol_fee(&trade) as u64);
@@ -375,9 +375,9 @@ module ramm_sui::interface2 {
         let oth = ramm::get_asset_index<Other>(self);
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -493,9 +493,9 @@ module ramm_sui::interface2 {
         let o   = ramm::get_asset_index<AssetOut>(self);
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -526,7 +526,7 @@ module ramm_sui::interface2 {
             self, snd, *vec_map::get(&new_prices, &snd), *vec_map::get(&new_price_timestamps, &snd)
         );
 
-        let mut volatility_fees: VecMap<u8, u256> = vec_map::empty();
+        let volatility_fees: VecMap<u8, u256> = vec_map::empty();
         vec_map::insert(&mut volatility_fees, fst, fst_vol_fee);
         vec_map::insert(&mut volatility_fees, snd, snd_vol_fee);
         /*
@@ -581,7 +581,7 @@ module ramm_sui::interface2 {
         };
 
         let burn_amount: u64 = (*lpt_amount as u64);
-        let mut lp_token: Balance<LP<AssetOut>> = coin::into_balance(lp_token);
+        let lp_token: Balance<LP<AssetOut>> = coin::into_balance(lp_token);
         let burn_tokens: Balance<LP<AssetOut>> = balance::split(&mut lp_token, burn_amount);
         // Update RAMM's untyped count of LP tokens for outgoing asset
         ramm::decr_lptokens_issued<AssetOut>(self, burn_amount);
@@ -621,8 +621,8 @@ module ramm_sui::interface2 {
 
         // Build required data structures for liquidity withdrawal event emission.
 
-        let mut amounts_out_u64: VecMap<TypeName, u64> = vec_map::empty();
-        let mut fees_u64: VecMap<TypeName, u64> = vec_map::empty();
+        let amounts_out_u64: VecMap<TypeName, u64> = vec_map::empty();
+        let fees_u64: VecMap<TypeName, u64> = vec_map::empty();
         vec_map::insert(&mut amounts_out_u64, type_name::get<Asset1>(), (*vec_map::get(&amounts_out, &fst) as u64));
         vec_map::insert(&mut fees_u64, type_name::get<Asset1>(), (*vec_map::get(&fees, &fst) as u64));
         if (vec_map::contains(&amounts_out, &snd)) {
@@ -667,7 +667,7 @@ module ramm_sui::interface2 {
         let value_fst: u64 = coin::value(&fst);
         let value_snd: u64 = coin::value(&snd);
 
-        let mut collected_fees: VecMap<TypeName, u64> = vec_map::empty();
+        let collected_fees: VecMap<TypeName, u64> = vec_map::empty();
         vec_map::insert(&mut collected_fees, type_name::get<Asset1>(), value_fst);
         vec_map::insert(&mut collected_fees, type_name::get<Asset2>(), value_snd);
 
@@ -684,17 +684,4 @@ module ramm_sui::interface2 {
 
         ramm::check_ramm_invariants_2<Asset1, Asset2>(self);
     }
-
-    spec collect_fees_2 {
-        pragma opaque = true;
-
-        pragma aborts_if_is_partial = true;
-
-        aborts_if self.admin_cap_id != object::id(admin_cap);
-        aborts_if self.asset_count != TWO;
-
-        ensures self.asset_count == TWO;
-
-        // More can be only when `VecMap` offers an API within the MSL.
-    }
 }
diff --git a/ramm-sui/sources/interface3.move b/ramm-sui/sources/interface3.move
@@ -41,7 +41,6 @@ module ramm_sui::interface3 {
     const EInvalidWithdrawal: u64 = 12;
 
     /// Trading function for a RAMM with three (3) assets.
-    ///
     /// Used to deposit a given amount of asset `T_i`, in exchange for asset `T_o`.
     ///
     /// # Aborts
@@ -80,9 +79,9 @@ module ramm_sui::interface3 {
         let oth = ramm::get_asset_index<Other>(self);
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -183,7 +182,7 @@ module ramm_sui::interface3 {
         let amount_out_u64: u64 = (amount_out_u256 as u64);
         if (ramm::execute(&trade)) {
             if (amount_out_u64 >= min_ao) {
-                let mut amount_in: Balance<AssetIn> = coin::into_balance(amount_in);
+                let amount_in: Balance<AssetIn> = coin::into_balance(amount_in);
 
                 let fee: u64 = (ramm::protocol_fee(&trade) as u64);
                 let fee_bal: Balance<AssetIn> = balance::split(&mut amount_in, fee);
@@ -258,9 +257,9 @@ module ramm_sui::interface3 {
         ramm::check_trade_amount_out<AssetOut>(self, (amount_out as u256));
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -360,8 +359,8 @@ module ramm_sui::interface3 {
         let max_ai_u64: u64 = coin::value(&max_ai);
         if (ramm::execute(&trade)) {
             if (trade_amount <= max_ai_u64) {
-                let mut max_ai: Balance<AssetIn> = coin::into_balance(max_ai);
-                let mut amount_in: Balance<AssetIn> = balance::split(&mut max_ai, trade_amount);
+                let max_ai: Balance<AssetIn> = coin::into_balance(max_ai);
+                let amount_in: Balance<AssetIn> = balance::split(&mut max_ai, trade_amount);
                 let remainder = max_ai;
 
                 let fee: u64 = (ramm::protocol_fee(&trade) as u64);
@@ -432,9 +431,9 @@ module ramm_sui::interface3 {
         let anoth = ramm::get_asset_index<Another>(self);
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -580,9 +579,9 @@ module ramm_sui::interface3 {
         let o   = ramm::get_asset_index<AssetOut>(self);
 
         let current_timestamp: u64 = clock::timestamp_ms(clock);
-        let mut new_prices = vec_map::empty<u8, u256>();
-        let mut factors_for_prices = vec_map::empty<u8, u256>();
-        let mut new_price_timestamps = vec_map::empty<u8, u64>();
+        let new_prices = vec_map::empty<u8, u256>();
+        let factors_for_prices = vec_map::empty<u8, u256>();
+        let new_price_timestamps = vec_map::empty<u8, u64>();
         ramm::check_feed_and_get_price_data(
             self,
             current_timestamp,
@@ -625,7 +624,7 @@ module ramm_sui::interface3 {
             self, trd, *vec_map::get(&new_prices, &trd), *vec_map::get(&new_price_timestamps, &trd)
         );
 
-        let mut volatility_fees: VecMap<u8, u256> = vec_map::empty();
+        let volatility_fees: VecMap<u8, u256> = vec_map::empty();
         vec_map::insert(&mut volatility_fees, fst, fst_vol_fee);
         vec_map::insert(&mut volatility_fees, snd, snd_vol_fee);
         vec_map::insert(&mut volatility_fees, trd, trd_vol_fee);
@@ -687,7 +686,7 @@ module ramm_sui::interface3 {
         };
 
         let burn_amount: u64 = (*lpt_amount as u64);
-        let mut lp_token: Balance<LP<AssetOut>> = coin::into_balance(lp_token);
+        let lp_token: Balance<LP<AssetOut>> = coin::into_balance(lp_token);
         let burn_tokens: Balance<LP<AssetOut>> = balance::split(&mut lp_token, burn_amount);
         // Update RAMM's untyped count of LP tokens for outgoing asset
         ramm::decr_lptokens_issued<AssetOut>(self, burn_amount);
@@ -735,8 +734,8 @@ module ramm_sui::interface3 {
 
         // Build required data structures for liquidity withdrawal event emission.
 
-        let mut amounts_out_u64: VecMap<TypeName, u64> = vec_map::empty();
-        let mut fees_u64: VecMap<TypeName, u64> = vec_map::empty();
+        let amounts_out_u64: VecMap<TypeName, u64> = vec_map::empty();
+        let fees_u64: VecMap<TypeName, u64> = vec_map::empty();
         vec_map::insert(&mut amounts_out_u64, type_name::get<Asset1>(), (*vec_map::get(&amounts_out, &fst) as u64));
         vec_map::insert(&mut fees_u64, type_name::get<Asset1>(), (*vec_map::get(&fees, &fst) as u64));
         if (vec_map::contains(&amounts_out, &snd)) {
@@ -789,7 +788,7 @@ module ramm_sui::interface3 {
         let value_snd: u64 = coin::value(&snd);
         let value_trd: u64 = coin::value(&trd);
 
-        let mut collected_fees: VecMap<TypeName, u64> = vec_map::empty();
+        let collected_fees: VecMap<TypeName, u64> = vec_map::empty();
         vec_map::insert(&mut collected_fees, type_name::get<Asset1>(), value_fst);
         vec_map::insert(&mut collected_fees, type_name::get<Asset2>(), value_snd);
         vec_map::insert(&mut collected_fees, type_name::get<Asset3>(), value_trd);
@@ -808,15 +807,4 @@ module ramm_sui::interface3 {
 
         ramm::check_ramm_invariants_3<Asset1, Asset2, Asset3>(self);
     }
-
-    spec collect_fees_3 {
-        pragma opaque = true;
-
-        pragma aborts_if_is_partial = true;
-
-        aborts_if self.admin_cap_id != object::id(admin_cap);
-        aborts_if self.asset_count != THREE;
-
-        ensures self.asset_count == THREE;
-    }
 }