Skip to content

Commit

Permalink
Use newest spec but disable verification because of fa
Browse files Browse the repository at this point in the history
  • Loading branch information
@axiongsupra
axiongsupra committed Oct 16, 2024
1 parent 4c59725 commit b3432ad
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 14 deletions.
18 changes: 15 additions & 3 deletions aptos-move/framework/supra-framework/doc/vesting_without_staking.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2170,11 +2170,18 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> verify = <b>true</b>;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>let</b> amount = <b>min</b>(vesting_record.left_amount, <a href="../../aptos-stdlib/../move-stdlib/doc/fixed_point32.md#0x1_fixed_point32_spec_multiply_u64">fixed_point32::spec_multiply_u64</a>(vesting_record.init_amount, vesting_fraction));
<b>ensures</b> vesting_record.left_amount == <b>old</b>(vesting_record.left_amount) - amount;
<b>let</b> address_from = signer_cap.<a href="account.md#0x1_account">account</a>;
<b>ensures</b> beneficiary != address_from;
<b>let</b> coin_store_from = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(address_from);
<b>let</b> <b>post</b> coin_store_post_from = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(address_from);
<b>let</b> coin_store_to = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(beneficiary);
<b>let</b> <b>post</b> coin_store_post_to = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(beneficiary);
<b>ensures</b> beneficiary != address_from ==&gt; coin_store_post_from.<a href="coin.md#0x1_coin">coin</a>.value ==
coin_store_from.<a href="coin.md#0x1_coin">coin</a>.value - amount;
<b>ensures</b> beneficiary != address_from ==&gt; coin_store_post_to.<a href="coin.md#0x1_coin">coin</a>.value == coin_store_to.<a href="coin.md#0x1_coin">coin</a>.value + amount;
<b>ensures</b> beneficiary == address_from ==&gt; coin_store_post_from.<a href="coin.md#0x1_coin">coin</a>.value == coin_store_from.<a href="coin.md#0x1_coin">coin</a>.value;
</code></pre>


Expand All @@ -2190,11 +2197,13 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> verify = <b>true</b>;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>pragma</b> aborts_if_is_partial = <b>true</b>;
<b>include</b> <a href="vesting_without_staking.md#0x1_vesting_without_staking_AdminAborts">AdminAborts</a>;
<b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting_without_staking.md#0x1_vesting_without_staking_VestingContract">VestingContract</a>&gt;(contract_address);
<b>let</b> <b>post</b> vesting_contract_post = <b>global</b>&lt;<a href="vesting_without_staking.md#0x1_vesting_without_staking_VestingContract">VestingContract</a>&gt;(contract_address);
<b>let</b> balance_pre = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(vesting_contract.withdrawal_address).<a href="coin.md#0x1_coin">coin</a>.value;
<b>let</b> <b>post</b> balance_post = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(vesting_contract.withdrawal_address).<a href="coin.md#0x1_coin">coin</a>.value;
<b>let</b> shareholder_amount = <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_get">simple_map::spec_get</a>(vesting_contract.shareholders, shareholder_address).left_amount;
<b>ensures</b> vesting_contract_post.withdrawal_address != vesting_contract.signer_cap.<a href="account.md#0x1_account">account</a>;
<b>ensures</b> !<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(vesting_contract_post.shareholders, shareholder_address);
Expand All @@ -2217,6 +2226,9 @@ This address should be deterministic for the same admin and vesting contract cre
<pre><code><b>pragma</b> verify = <b>true</b>;
<b>pragma</b> aborts_if_is_partial = <b>true</b>;
<b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting_without_staking.md#0x1_vesting_without_staking_VestingContract">VestingContract</a>&gt;(contract_address);
<b>let</b> balance_pre = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(vesting_contract.withdrawal_address).<a href="coin.md#0x1_coin">coin</a>.value;
<b>let</b> <b>post</b> balance_post = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(vesting_contract.withdrawal_address).<a href="coin.md#0x1_coin">coin</a>.value;
<b>let</b> <b>post</b> balance_contract = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;SupraCoin&gt;&gt;(contract_address).<a href="coin.md#0x1_coin">coin</a>.value;
<b>aborts_if</b> !(<b>global</b>&lt;<a href="vesting_without_staking.md#0x1_vesting_without_staking_VestingContract">VestingContract</a>&gt;(contract_address).state == <a href="vesting_without_staking.md#0x1_vesting_without_staking_VESTING_POOL_TERMINATED">VESTING_POOL_TERMINATED</a>);
</code></pre>

Expand Down
28 changes: 17 additions & 11 deletions aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<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);
// Ensure that the amount is transferred from the address_from to the beneficiary
ensures beneficiary != address_from;
// ==>
// (coin::balance<SupraCoin>(beneficiary) == old(coin::balance<SupraCoin>(beneficiary)) + amount
// && coin::balance<SupraCoin>(address_from) == old(coin::balance<SupraCoin>(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<VestingContract>(contract_address);
let post vesting_contract_post = global<VestingContract>(contract_address);
// let balance_pre = coin::balance<SupraCoin>(vesting_contract.withdrawal_address);
// let post balance_post = coin::balance<SupraCoin>(vesting_contract_post.withdrawal_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;
// ensure that `withdrawal address` receives the `shareholder_amount`
ensures vesting_contract_post.withdrawal_address != vesting_contract.signer_cap.account;
Expand All @@ -147,9 +153,9 @@ spec supra_framework::vesting_without_staking {
pragma verify = true;
pragma aborts_if_is_partial = true;
let vesting_contract = global<VestingContract>(contract_address);
// let balance_pre = coin::balance<SupraCoin>(vesting_contract.withdrawal_address);
// let post balance_post = coin::balance<SupraCoin>(vesting_contract.withdrawal_address);
// let post balance_contract = coin::balance<SupraCoin>(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);
// // 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<SupraCoin>(contract_address);
Expand Down

0 comments on commit b3432ad

Please sign in to comment.