Fix coin spec

Entropy-Foundation · Jun 27, 2024 · f21251e · f21251e
1 parent c14c516
commit f21251e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/aptos-move/framework/supra-framework/sources/coin.move b/aptos-move/framework/supra-framework/sources/coin.move
@@ -15,7 +15,6 @@ module supra_framework::coin {
     use aptos_std::type_info;
 
 	friend supra_framework::supra_coin;
-    //friend supra_framework::supra_coin;
     friend supra_framework::genesis;
     friend supra_framework::transaction_fee;
 

diff --git a/aptos-move/framework/supra-framework/sources/coin.spec.move b/aptos-move/framework/supra-framework/sources/coin.spec.move
@@ -63,11 +63,13 @@ spec supra_framework::coin {
         global supply<CoinType>: num;
         global aggregate_supply<CoinType>: num;
         apply TotalSupplyTracked<CoinType> to *<CoinType> except
-            initialize, initialize_internal, initialize_with_parallelizable_supply;
+            initialize, initialize_internal, initialize_internal_with_limit, initialize_with_parallelizable_supply,
+        initialize_with_parallelizable_supply_with_limit;
         /// [high-level-req-4]
         /// [high-level-req-9]
         apply TotalSupplyNoChange<CoinType> to *<CoinType> except mint,
-            burn, burn_from, initialize, initialize_internal, initialize_with_parallelizable_supply;
+            burn, burn_from, initialize, initialize_internal, initialize_internal_with_limit,
+        initialize_with_parallelizable_supply, initialize_with_parallelizable_supply_with_limit;
     }
 
     spec fun spec_fun_supply_tracked<CoinType>(val: u64, supply: Option<OptionalAggregator>): bool {