Skip to content

Commit

Permalink
add head
Browse files Browse the repository at this point in the history
  • Loading branch information
@UIZorrot
UIZorrot committed Jul 21, 2023
1 parent c1fa01c commit 22977e3
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 27 deletions.
21 changes: 10 additions & 11 deletions aptos-move/framework/aptos-framework/doc/vesting.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3012,8 +3012,7 @@ 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> opaque;
<pre><code><b>pragma</b> opaque;
<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;{contract_address: vesting_contract_address};
<b>ensures</b> [abstract] result == <a href="vesting.md#0x1_vesting_spec_shareholder">spec_shareholder</a>(vesting_contract_address, shareholder_or_beneficiary);
</code></pre>
Expand Down Expand Up @@ -3113,7 +3112,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>aborts_if</b> len(contract_addresses) == 0;
<b>include</b> <a href="vesting.md#0x1_vesting_PreconditionAbortsIf">PreconditionAbortsIf</a>;
</code></pre>
Expand Down Expand Up @@ -3148,7 +3147,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>aborts_if</b> len(contract_addresses) == 0;
<b>include</b> <a href="vesting.md#0x1_vesting_PreconditionAbortsIf">PreconditionAbortsIf</a>;
</code></pre>
Expand Down Expand Up @@ -3179,7 +3178,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;;
<b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
<b>include</b> <a href="vesting.md#0x1_vesting_WithdrawStakeAbortsIf">WithdrawStakeAbortsIf</a> { vesting_contract };
Expand All @@ -3198,7 +3197,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>aborts_if</b> len(contract_addresses) == 0;
</code></pre>

Expand All @@ -3215,7 +3214,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;;
<b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
<b>include</b> <a href="vesting.md#0x1_vesting_WithdrawStakeAbortsIf">WithdrawStakeAbortsIf</a> { vesting_contract };
Expand All @@ -3234,7 +3233,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
<b>aborts_if</b> vesting_contract.state != <a href="vesting.md#0x1_vesting_VESTING_POOL_TERMINATED">VESTING_POOL_TERMINATED</a>;
<b>include</b> <a href="vesting.md#0x1_vesting_VerifyAdminAbortsIf">VerifyAdminAbortsIf</a>;
Expand All @@ -3254,7 +3253,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>include</b> <a href="vesting.md#0x1_vesting_VerifyAdminAbortsIf">VerifyAdminAbortsIf</a>;
<b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
<b>let</b> acc = vesting_contract.signer_cap.<a href="account.md#0x1_account">account</a>;
Expand Down Expand Up @@ -3567,7 +3566,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>include</b> <a href="vesting.md#0x1_vesting_UnlockStakeAbortsIf">UnlockStakeAbortsIf</a>;
</code></pre>

Expand Down Expand Up @@ -3602,7 +3601,7 @@ This address should be deterministic for the same admin and vesting contract cre



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>include</b> <a href="vesting.md#0x1_vesting_WithdrawStakeAbortsIf">WithdrawStakeAbortsIf</a>;
</code></pre>

Expand Down
25 changes: 9 additions & 16 deletions aptos-move/framework/aptos-framework/sources/vesting.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,6 @@ spec aptos_framework::vesting {
spec fun spec_shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address;

spec shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address {
pragma verify = true;
pragma opaque;
include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
ensures [abstract] result == spec_shareholder(vesting_contract_address, shareholder_or_beneficiary);
Expand Down Expand Up @@ -151,7 +150,6 @@ spec aptos_framework::vesting {
// TODO: Calls `unlock_stake` which is not verified.
// Current verification times out.
pragma verify = false;

include UnlockRewardsAbortsIf;
}

Expand Down Expand Up @@ -179,21 +177,20 @@ spec aptos_framework::vesting {

spec unlock_rewards_many(contract_addresses: vector<address>) {
// TODO: Calls `unlock_rewards` in loop.
pragma aborts_if_is_partial;
pragma verify = false;
aborts_if len(contract_addresses) == 0;
include PreconditionAbortsIf;
}

spec vest(contract_address: address) {
// TODO: Calls `staking_contract::distribute` which is not verified.
pragma verify = false;

include UnlockRewardsAbortsIf;
}

spec vest_many(contract_addresses: vector<address>) {
// TODO: Calls `vest` in loop.
pragma aborts_if_is_partial;
pragma verify = false;
aborts_if len(contract_addresses) == 0;
include PreconditionAbortsIf;
}
Expand All @@ -207,8 +204,7 @@ spec aptos_framework::vesting {

spec distribute(contract_address: address) {
// TODO: Can't handle abort in loop.
pragma aborts_if_is_partial;

pragma verify = false;
include ActiveVestingContractAbortsIf<VestingContract>;

let vesting_contract = global<VestingContract>(contract_address);
Expand All @@ -217,14 +213,13 @@ spec aptos_framework::vesting {

spec distribute_many(contract_addresses: vector<address>) {
// TODO: Calls `distribute` in loop.
pragma aborts_if_is_partial;
pragma verify = false;
aborts_if len(contract_addresses) == 0;
}

spec terminate_vesting_contract(admin: &signer, contract_address: address) {
// TODO: Calls `staking_contract::distribute` which is not verified.
pragma aborts_if_is_partial;

pragma verify = false;
include ActiveVestingContractAbortsIf<VestingContract>;

let vesting_contract = global<VestingContract>(contract_address);
Expand All @@ -233,13 +228,12 @@ spec aptos_framework::vesting {

spec admin_withdraw(admin: &signer, contract_address: address) {
// TODO: Calls `withdraw_stake` which is not verified.
pragma aborts_if_is_partial;
pragma verify = false;

let vesting_contract = global<VestingContract>(contract_address);
aborts_if vesting_contract.state != VESTING_POOL_TERMINATED;

include VerifyAdminAbortsIf;

include WithdrawStakeAbortsIf { vesting_contract };
}

Expand All @@ -250,7 +244,7 @@ spec aptos_framework::vesting {
commission_percentage: u64,
) {
// TODO: Calls `staking_contract::switch_operator` which is not verified.
pragma aborts_if_is_partial;
pragma verify = false;

include VerifyAdminAbortsIf;

Expand Down Expand Up @@ -422,7 +416,7 @@ spec aptos_framework::vesting {

spec unlock_stake(vesting_contract: &VestingContract, amount: u64) {
// TODO: Calls `staking_contract::unlock_stake` which is not verified.
pragma aborts_if_is_partial;
pragma verify = false;
include UnlockStakeAbortsIf;
}

Expand All @@ -443,8 +437,7 @@ spec aptos_framework::vesting {

spec withdraw_stake(vesting_contract: &VestingContract, contract_address: address): Coin<AptosCoin> {
// TODO: Calls `staking_contract::distribute` which is not verified.
pragma aborts_if_is_partial;

pragma verify = false;
include WithdrawStakeAbortsIf;
}

Expand Down
Binary file modified aptos-move/framework/cached-packages/generated/head.mrb
View file
Binary file not shown.

0 comments on commit 22977e3

Please sign in to comment.