diff --git a/aptos-move/framework/supra-framework/doc/vesting_without_staking.md b/aptos-move/framework/supra-framework/doc/vesting_without_staking.md index 7ce8212a95c5c..e85b2bf307555 100644 --- a/aptos-move/framework/supra-framework/doc/vesting_without_staking.md +++ b/aptos-move/framework/supra-framework/doc/vesting_without_staking.md @@ -2170,11 +2170,18 @@ This address should be deterministic for the same admin and vesting contract cre -
pragma verify = true;
+
pragma verify = false;
 let amount = min(vesting_record.left_amount, fixed_point32::spec_multiply_u64(vesting_record.init_amount, vesting_fraction));
 ensures vesting_record.left_amount == old(vesting_record.left_amount) - amount;
 let address_from = signer_cap.account;
-ensures beneficiary != address_from;
+let coin_store_from = global<coin::CoinStore<SupraCoin>>(address_from);
+let post coin_store_post_from = global<coin::CoinStore<SupraCoin>>(address_from);
+let coin_store_to = global<coin::CoinStore<SupraCoin>>(beneficiary);
+let post coin_store_post_to = global<coin::CoinStore<SupraCoin>>(beneficiary);
+ensures beneficiary != address_from ==> coin_store_post_from.coin.value ==
+    coin_store_from.coin.value - amount;
+ensures beneficiary != address_from ==> coin_store_post_to.coin.value == coin_store_to.coin.value + amount;
+ensures beneficiary == address_from ==> coin_store_post_from.coin.value == coin_store_from.coin.value;
 

 
 
@@ -2190,11 +2197,13 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
pragma verify = true;
+
pragma verify = false;
 pragma aborts_if_is_partial = true;
 include AdminAborts;
 let vesting_contract = global<VestingContract>(contract_address);
 let post vesting_contract_post = global<VestingContract>(contract_address);
+let balance_pre = global<coin::CoinStore<SupraCoin>>(vesting_contract.withdrawal_address).coin.value;
+let post balance_post = global<coin::CoinStore<SupraCoin>>(vesting_contract.withdrawal_address).coin.value;
 let shareholder_amount = simple_map::spec_get(vesting_contract.shareholders, shareholder_address).left_amount;
 ensures vesting_contract_post.withdrawal_address != vesting_contract.signer_cap.account;
 ensures !simple_map::spec_contains_key(vesting_contract_post.shareholders, shareholder_address);
@@ -2217,6 +2226,9 @@ This address should be deterministic for the same admin and vesting contract cre
 
pragma verify = true;
 pragma aborts_if_is_partial = true;
 let vesting_contract = global<VestingContract>(contract_address);
+let balance_pre = global<coin::CoinStore<SupraCoin>>(vesting_contract.withdrawal_address).coin.value;
+let post balance_post = global<coin::CoinStore<SupraCoin>>(vesting_contract.withdrawal_address).coin.value;
+let post balance_contract = global<coin::CoinStore<SupraCoin>>(contract_address).coin.value;
 aborts_if !(global<VestingContract>(contract_address).state == VESTING_POOL_TERMINATED);
 

 
diff --git a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
index ba617b31ef975..966c2ceb707fd 100644
--- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
+++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
@@ -107,26 +107,32 @@ spec supra_framework::vesting_without_staking {
     }
 
     spec vest_transfer {
-        pragma verify = true;
+        // TODO(fa_migration)
+        pragma verify = false;
         let amount = min(vesting_record.left_amount, fixed_point32::spec_multiply_u64(vesting_record.init_amount, vesting_fraction));
         // Ensure that the amount is substracted from the left_amount
         ensures vesting_record.left_amount == old(vesting_record.left_amount) - amount;
         let address_from = signer_cap.account;
+        let coin_store_from = global>(address_from);
+        let post coin_store_post_from = global>(address_from);
+        let coin_store_to = global>(beneficiary);
+        let post coin_store_post_to = global>(beneficiary);
         // Ensure that the amount is transferred from the address_from to the beneficiary
-        ensures beneficiary != address_from;
-        // ==>
-        //     (coin::balance(beneficiary) == old(coin::balance(beneficiary)) + amount
-        //     && coin::balance(address_from) == old(coin::balance(address_from)) - amount);
+        ensures beneficiary != address_from ==> coin_store_post_from.coin.value ==
+            coin_store_from.coin.value - amount;
+        ensures beneficiary != address_from ==> coin_store_post_to.coin.value == coin_store_to.coin.value + amount;
+        ensures beneficiary == address_from ==> coin_store_post_from.coin.value == coin_store_from.coin.value;
     }
 
     spec remove_shareholder {
-        pragma verify = true;
+        // TODO(fa_migration)
+        pragma verify = false;
         pragma aborts_if_is_partial = true;
         include AdminAborts;
         let vesting_contract = global(contract_address);
         let post vesting_contract_post = global(contract_address);
-        // let balance_pre = coin::balance(vesting_contract.withdrawal_address);
-        // let post balance_post = coin::balance(vesting_contract_post.withdrawal_address);
+        let balance_pre = global>(vesting_contract.withdrawal_address).coin.value;
+        let post balance_post = global>(vesting_contract.withdrawal_address).coin.value;
         let shareholder_amount = simple_map::spec_get(vesting_contract.shareholders, shareholder_address).left_amount;
         // ensure that `withdrawal address` receives the `shareholder_amount`
         ensures vesting_contract_post.withdrawal_address != vesting_contract.signer_cap.account;
@@ -147,9 +153,9 @@ spec supra_framework::vesting_without_staking {
         pragma verify = true;
         pragma aborts_if_is_partial = true;
         let vesting_contract = global(contract_address);
-        // let balance_pre = coin::balance(vesting_contract.withdrawal_address);
-        // let post balance_post = coin::balance(vesting_contract.withdrawal_address);
-        // let post balance_contract = coin::balance(contract_address);
+        let balance_pre = global>(vesting_contract.withdrawal_address).coin.value;
+        let post balance_post = global>(vesting_contract.withdrawal_address).coin.value;
+        let post balance_contract = global>(contract_address).coin.value;
         aborts_if !(global(contract_address).state == VESTING_POOL_TERMINATED);
         // // ensure that the `withdrawal_address` receives the remaining balance
         // ensures (vesting_contract.signer_cap.account != vesting_contract.withdrawal_address) ==> balance_post == balance_pre + coin::balance(contract_address);