system_addresses - [mainnet]
use 0x1::error;use 0x1::signer;
Constants
The address/account did not correspond to the core framework address
const ENOT_APTOS_FRAMEWORK_ADDRESS: u64 = 3;
The address/account did not correspond to the core resource address
const ENOT_CORE_RESOURCE_ADDRESS: u64 = 1;
The address is not framework reserved address
const ENOT_FRAMEWORK_RESERVED_ADDRESS: u64 = 4;
The operation can only be performed by the VM
const EVM: u64 = 2;
Functions
assert_core_resource
public fun assert_core_resource(account: &signer)
Implementation
public fun assert_core_resource(account: &signer) { assert_core_resource_address(signer::address_of(account))}
assert_core_resource_address
public fun assert_core_resource_address(addr: address)
Implementation
public fun assert_core_resource_address(addr: address) { assert!(is_core_resource_address(addr), error::permission_denied(ENOT_CORE_RESOURCE_ADDRESS))}
is_core_resource_address
public fun is_core_resource_address(addr: address): bool
Implementation
public fun is_core_resource_address(addr: address): bool { addr == @core_resources}
assert_aptos_framework
public fun assert_aptos_framework(account: &signer)
Implementation
public fun assert_aptos_framework(account: &signer) { assert!( is_aptos_framework_address(signer::address_of(account)), error::permission_denied(ENOT_APTOS_FRAMEWORK_ADDRESS), )}
assert_framework_reserved_address
public fun assert_framework_reserved_address(account: &signer)
Implementation
public fun assert_framework_reserved_address(account: &signer) { assert_framework_reserved(signer::address_of(account));}
assert_framework_reserved
public fun assert_framework_reserved(addr: address)
Implementation
public fun assert_framework_reserved(addr: address) { assert!( is_framework_reserved_address(addr), error::permission_denied(ENOT_FRAMEWORK_RESERVED_ADDRESS), )}
is_framework_reserved_address
Return true if addr
is 0x0 or under the on chain governance’s control.
public fun is_framework_reserved_address(addr: address): bool
Implementation
public fun is_framework_reserved_address(addr: address): bool { is_aptos_framework_address(addr) || addr == @0x2 || addr == @0x3 || addr == @0x4 || addr == @0x5 || addr == @0x6 || addr == @0x7 || addr == @0x8 || addr == @0x9 || addr == @0xa}
is_aptos_framework_address
Return true if addr
is 0x1.
public fun is_aptos_framework_address(addr: address): bool
Implementation
public fun is_aptos_framework_address(addr: address): bool { addr == @aptos_framework}
assert_vm
Assert that the signer has the VM reserved address.
public fun assert_vm(account: &signer)
Implementation
public fun assert_vm(account: &signer) { assert!(is_vm(account), error::permission_denied(EVM))}
is_vm
Return true if addr
is a reserved address for the VM to call system modules.
public fun is_vm(account: &signer): bool
Implementation
public fun is_vm(account: &signer): bool { is_vm_address(signer::address_of(account))}
is_vm_address
Return true if addr
is a reserved address for the VM to call system modules.
public fun is_vm_address(addr: address): bool
Implementation
public fun is_vm_address(addr: address): bool { addr == @vm_reserved}
is_reserved_address
Return true if addr
is either the VM address or an Aptos Framework address.
public fun is_reserved_address(addr: address): bool
Implementation
public fun is_reserved_address(addr: address): bool { is_aptos_framework_address(addr) || is_vm_address(addr)}
Specification
High-level Requirements
No. | Requirement | Criticality | Implementation | Enforcement |
---|---|---|---|---|
1 | Asserting that a provided address corresponds to the Core Resources address should always yield a true result when matched. | Low | The assert_core_resource and assert_core_resource_address functions ensure that the provided signer or address belong to the @core_resources account. | Formally verified via AbortsIfNotCoreResource. |
2 | Asserting that a provided address corresponds to the Aptos Framework Resources address should always yield a true result when matched. | High | The assert_aptos_framework function ensures that the provided signer belongs to the @aptos_framework account. | Formally verified via AbortsIfNotAptosFramework. |
3 | Asserting that a provided address corresponds to the VM address should always yield a true result when matched. | High | The assert_vm function ensure that the provided signer belongs to the @vm_reserved account. | Formally verified via AbortsIfNotVM. |
Module-level Specification
pragma verify = true;pragma aborts_if_is_strict;
assert_core_resource
public fun assert_core_resource(account: &signer)
pragma opaque;include AbortsIfNotCoreResource { addr: signer::address_of(account) };
assert_core_resource_address
public fun assert_core_resource_address(addr: address)
pragma opaque;include AbortsIfNotCoreResource;
is_core_resource_address
public fun is_core_resource_address(addr: address): bool
pragma opaque;aborts_if false;ensures result == (addr == @core_resources);
assert_aptos_framework
public fun assert_aptos_framework(account: &signer)
pragma opaque;include AbortsIfNotAptosFramework;
assert_framework_reserved_address
public fun assert_framework_reserved_address(account: &signer)
aborts_if !is_framework_reserved_address(signer::address_of(account));
assert_framework_reserved
public fun assert_framework_reserved(addr: address)
aborts_if !is_framework_reserved_address(addr);
Specifies that a function aborts if the account does not have the aptos framework address.
schema AbortsIfNotAptosFramework { account: signer; // This enforces high-level requirement 2: aborts_if signer::address_of(account) != @aptos_framework with error::PERMISSION_DENIED;}
assert_vm
public fun assert_vm(account: &signer)
pragma opaque;include AbortsIfNotVM;
Specifies that a function aborts if the account does not have the VM reserved address.
schema AbortsIfNotVM { account: signer; // This enforces high-level requirement 3: aborts_if signer::address_of(account) != @vm_reserved with error::PERMISSION_DENIED;}