Skip to content

Commit

Permalink
[Spec] Added more specs to the coin and account modules (#5832)
Browse files Browse the repository at this point in the history 
- this PR completes many TODOs in the specs of coin and account modules.
  • Loading branch information
@junkil-park
junkil-park authored Jan 4, 2023
1 parent 1d122fb commit 2743b5d
Show file tree
Hide file tree
Showing 12 changed files with 411 additions and 64 deletions.
65 changes: 59 additions & 6 deletions aptos-move/framework/aptos-framework/doc/account.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1724,7 +1724,20 @@ The length of new_auth_key is 32.



<pre><code><b>pragma</b> aborts_if_is_partial;
<pre><code><b>include</b> scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_NewUnvalidatedPublicKeyFromBytesAbortsIf">ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf</a> { bytes: public_key_bytes };
<b>include</b> scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_NewSignatureFromBytesAbortsIf">ed25519::NewSignatureFromBytesAbortsIf</a> { bytes: signature };
<b>aborts_if</b> scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> && !<a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_spec_signature_verify_strict_t">ed25519::spec_signature_verify_strict_t</a>(
<a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_Signature">ed25519::Signature</a> { bytes: signature },
<a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_UnvalidatedPublicKey">ed25519::UnvalidatedPublicKey</a> { bytes: public_key_bytes },
challenge
);
<b>include</b> scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_NewUnvalidatedPublicKeyFromBytesAbortsIf">multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf</a> { bytes: public_key_bytes };
<b>include</b> scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_NewSignatureFromBytesAbortsIf">multi_ed25519::NewSignatureFromBytesAbortsIf</a> { bytes: signature };
<b>aborts_if</b> scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> && !<a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_spec_signature_verify_strict_t">multi_ed25519::spec_signature_verify_strict_t</a>(
<a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_Signature">multi_ed25519::Signature</a> { bytes: signature },
<a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_UnvalidatedPublicKey">multi_ed25519::UnvalidatedPublicKey</a> { bytes: public_key_bytes },
challenge
);
<b>aborts_if</b> scheme != <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> && scheme != <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a>;
</code></pre>

Expand Down Expand Up @@ -1767,9 +1780,37 @@ The Account existed under the signer.
The authentication scheme is ED25519_SCHEME and MULTI_ED25519_SCHEME.


<pre><code><b>pragma</b> aborts_if_is_partial;
<b>let</b> source_address = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>);
<pre><code><b>let</b> source_address = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>);
<b>let</b> account_resource = <b>global</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(source_address);
<b>let</b> proof_challenge = <a href="account.md#0x1_account_SignerCapabilityOfferProofChallengeV2">SignerCapabilityOfferProofChallengeV2</a> {
sequence_number: account_resource.sequence_number,
source_address,
recipient_address,
};
<b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(recipient_address);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(source_address);
<b>include</b> account_scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_NewUnvalidatedPublicKeyFromBytesAbortsIf">ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf</a> { bytes: account_public_key_bytes };
<b>aborts_if</b> account_scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> && ({
<b>let</b> expected_auth_key = <a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_spec_public_key_bytes_to_authentication_key">ed25519::spec_public_key_bytes_to_authentication_key</a>(account_public_key_bytes);
account_resource.authentication_key != expected_auth_key
});
<b>include</b> account_scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_NewSignatureFromBytesAbortsIf">ed25519::NewSignatureFromBytesAbortsIf</a> { bytes: signer_capability_sig_bytes };
<b>aborts_if</b> account_scheme == <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> && !<a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_spec_signature_verify_strict_t">ed25519::spec_signature_verify_strict_t</a>(
<a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_Signature">ed25519::Signature</a> { bytes: signer_capability_sig_bytes },
<a href="../../aptos-stdlib/doc/ed25519.md#0x1_ed25519_UnvalidatedPublicKey">ed25519::UnvalidatedPublicKey</a> { bytes: account_public_key_bytes },
proof_challenge
);
<b>include</b> account_scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_NewUnvalidatedPublicKeyFromBytesAbortsIf">multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf</a> { bytes: account_public_key_bytes };
<b>aborts_if</b> account_scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> && ({
<b>let</b> expected_auth_key = <a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_spec_public_key_bytes_to_authentication_key">multi_ed25519::spec_public_key_bytes_to_authentication_key</a>(account_public_key_bytes);
account_resource.authentication_key != expected_auth_key
});
<b>include</b> account_scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> ==&gt; <a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_NewSignatureFromBytesAbortsIf">multi_ed25519::NewSignatureFromBytesAbortsIf</a> { bytes: signer_capability_sig_bytes };
<b>aborts_if</b> account_scheme == <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a> && !<a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_spec_signature_verify_strict_t">multi_ed25519::spec_signature_verify_strict_t</a>(
<a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_Signature">multi_ed25519::Signature</a> { bytes: signer_capability_sig_bytes },
<a href="../../aptos-stdlib/doc/multi_ed25519.md#0x1_multi_ed25519_UnvalidatedPublicKey">multi_ed25519::UnvalidatedPublicKey</a> { bytes: account_public_key_bytes },
proof_challenge
);
<b>aborts_if</b> account_scheme != <a href="account.md#0x1_account_ED25519_SCHEME">ED25519_SCHEME</a> && account_scheme != <a href="account.md#0x1_account_MULTI_ED25519_SCHEME">MULTI_ED25519_SCHEME</a>;
<b>modifies</b> <b>global</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(source_address);
</code></pre>
Expand Down Expand Up @@ -1853,7 +1894,19 @@ The Account existed under the signer
The value of signer_capability_offer.for of Account resource under the signer is to_be_revoked_address


<pre><code><b>pragma</b> verify = <b>false</b>;
<pre><code><b>pragma</b> opaque;
<b>pragma</b> aborts_if_is_strict = <b>false</b>;
<b>aborts_if</b> [abstract] <b>false</b>;
<b>ensures</b> [abstract] result == <a href="account.md#0x1_account_spec_create_resource_address">spec_create_resource_address</a>(source, seed);
</code></pre>




<a name="0x1_account_spec_create_resource_address"></a>


<pre><code><b>fun</b> <a href="account.md#0x1_account_spec_create_resource_address">spec_create_resource_address</a>(source: <b>address</b>, seed: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <b>address</b>;
</code></pre>


Expand Down Expand Up @@ -1970,8 +2023,8 @@ The guid_creation_num of the Account is up to MAX_U64.



<pre><code><b>pragma</b> aborts_if_is_partial;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(account_addr);
<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(account_addr);
<b>aborts_if</b> !<a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_spec_is_struct">type_info::spec_is_struct</a>&lt;CoinType&gt;();
<b>modifies</b> <b>global</b>&lt;<a href="account.md#0x1_account_Account">Account</a>&gt;(account_addr);
</code></pre>

Expand Down
4 changes: 2 additions & 2 deletions aptos-move/framework/aptos-framework/doc/coin.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2310,11 +2310,11 @@ An account can only be registered once.
Updating <code>Account.guid_creation_num</code> will not overflow.


<pre><code><b>pragma</b> aborts_if_is_partial;
<b>let</b> account_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>);
<pre><code><b>let</b> account_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>);
<b>let</b> acc = <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(account_addr);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">CoinStore</a>&lt;CoinType&gt;&gt;(account_addr) && acc.guid_creation_num + 2 &gt; <a href="coin.md#0x1_coin_MAX_U64">MAX_U64</a>;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">CoinStore</a>&lt;CoinType&gt;&gt;(account_addr) && !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(account_addr);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">CoinStore</a>&lt;CoinType&gt;&gt;(account_addr) && !<a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_spec_is_struct">type_info::spec_is_struct</a>&lt;CoinType&gt;();
<b>ensures</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">CoinStore</a>&lt;CoinType&gt;&gt;(account_addr);
</code></pre>

Expand Down
64 changes: 57 additions & 7 deletions aptos-move/framework/aptos-framework/sources/account.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,8 +81,21 @@ spec aptos_framework::account {
}

spec assert_valid_signature_and_get_auth_key(scheme: u8, public_key_bytes: vector<u8>, signature: vector<u8>, challenge: &RotationProofChallenge): vector<u8> {
// TODO: complex aborts conditions.
pragma aborts_if_is_partial;
include scheme == ED25519_SCHEME ==> ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: public_key_bytes };
include scheme == ED25519_SCHEME ==> ed25519::NewSignatureFromBytesAbortsIf { bytes: signature };
aborts_if scheme == ED25519_SCHEME && !ed25519::spec_signature_verify_strict_t(
ed25519::Signature { bytes: signature },
ed25519::UnvalidatedPublicKey { bytes: public_key_bytes },
challenge
);

include scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: public_key_bytes };
include scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewSignatureFromBytesAbortsIf { bytes: signature };
aborts_if scheme == MULTI_ED25519_SCHEME && !multi_ed25519::spec_signature_verify_strict_t(
multi_ed25519::Signature { bytes: signature },
multi_ed25519::UnvalidatedPublicKey { bytes: public_key_bytes },
challenge
);
aborts_if scheme != ED25519_SCHEME && scheme != MULTI_ED25519_SCHEME;
}

Expand Down Expand Up @@ -116,11 +129,43 @@ spec aptos_framework::account {
account_public_key_bytes: vector<u8>,
recipient_address: address
) {
// TODO: complex aborts conditions.
pragma aborts_if_is_partial;
let source_address = signer::address_of(account);
let account_resource = global<Account>(source_address);
let proof_challenge = SignerCapabilityOfferProofChallengeV2 {
sequence_number: account_resource.sequence_number,
source_address,
recipient_address,
};

aborts_if !exists<Account>(recipient_address);
aborts_if !exists<Account>(source_address);

include account_scheme == ED25519_SCHEME ==> ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: account_public_key_bytes };
aborts_if account_scheme == ED25519_SCHEME && ({
let expected_auth_key = ed25519::spec_public_key_bytes_to_authentication_key(account_public_key_bytes);
account_resource.authentication_key != expected_auth_key
});
include account_scheme == ED25519_SCHEME ==> ed25519::NewSignatureFromBytesAbortsIf { bytes: signer_capability_sig_bytes };
aborts_if account_scheme == ED25519_SCHEME && !ed25519::spec_signature_verify_strict_t(
ed25519::Signature { bytes: signer_capability_sig_bytes },
ed25519::UnvalidatedPublicKey { bytes: account_public_key_bytes },
proof_challenge
);

include account_scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: account_public_key_bytes };
aborts_if account_scheme == MULTI_ED25519_SCHEME && ({
let expected_auth_key = multi_ed25519::spec_public_key_bytes_to_authentication_key(account_public_key_bytes);
account_resource.authentication_key != expected_auth_key
});
include account_scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewSignatureFromBytesAbortsIf { bytes: signer_capability_sig_bytes };
aborts_if account_scheme == MULTI_ED25519_SCHEME && !multi_ed25519::spec_signature_verify_strict_t(
multi_ed25519::Signature { bytes: signer_capability_sig_bytes },
multi_ed25519::UnvalidatedPublicKey { bytes: account_public_key_bytes },
proof_challenge
);

aborts_if account_scheme != ED25519_SCHEME && account_scheme != MULTI_ED25519_SCHEME;

modifies global<Account>(source_address);
}

Expand Down Expand Up @@ -160,9 +205,15 @@ spec aptos_framework::account {
/// The Account existed under the signer
/// The value of signer_capability_offer.for of Account resource under the signer is to_be_revoked_address
spec create_resource_address(source: &address, seed: vector<u8>): address {
pragma verify = false;
pragma opaque;
pragma aborts_if_is_strict = false;
// This function should not abort assuming the result of `sha3_256` is deserializable into an address.
aborts_if [abstract] false;
ensures [abstract] result == spec_create_resource_address(source, seed);
}

spec fun spec_create_resource_address(source: address, seed: vector<u8>): address;

spec create_resource_account(source: &signer, seed: vector<u8>): (signer, SignerCapability) {
pragma verify = false;
}
Expand Down Expand Up @@ -210,9 +261,8 @@ spec aptos_framework::account {
}

spec register_coin<CoinType>(account_addr: address) {
// TODO: Add the abort condition about `type_info::type_of`
pragma aborts_if_is_partial;
aborts_if !exists<Account>(account_addr);
aborts_if !type_info::spec_is_struct<CoinType>();
modifies global<Account>(account_addr);
}

Expand Down
3 changes: 1 addition & 2 deletions aptos-move/framework/aptos-framework/sources/coin.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,12 +218,11 @@ spec aptos_framework::coin {
/// An account can only be registered once.
/// Updating `Account.guid_creation_num` will not overflow.
spec register<CoinType>(account: &signer) {
// TODO: Add the abort condition about `type_info::type_of`
pragma aborts_if_is_partial;
let account_addr = signer::address_of(account);
let acc = global<account::Account>(account_addr);
aborts_if !exists<CoinStore<CoinType>>(account_addr) && acc.guid_creation_num + 2 > MAX_U64;
aborts_if !exists<CoinStore<CoinType>>(account_addr) && !exists<account::Account>(account_addr);
aborts_if !exists<CoinStore<CoinType>>(account_addr) && !type_info::spec_is_struct<CoinType>();
ensures exists<CoinStore<CoinType>>(account_addr);
}

Expand Down
Loading

0 comments on commit 2743b5d

Please sign in to comment.