diff --git a/aptos-move/framework/aptos-framework/doc/account.md b/aptos-move/framework/aptos-framework/doc/account.md index 383d4918dd7001..9566844a0f7394 100644 --- a/aptos-move/framework/aptos-framework/doc/account.md +++ b/aptos-move/framework/aptos-framework/doc/account.md @@ -1428,7 +1428,7 @@ to rotate his address to Alice's address in the first place. ) acquires Account, OriginatingAddress { assert!(exists_at(rotation_cap_offerer_address), error::not_found(EOFFERER_ADDRESS_DOES_NOT_EXIST)); - // Check that there exists a rotation capability offer at the offerer's account resource for the delegate. + // Check that there exists a rotation capability offer at the offerer's account resource for the delegate. let delegate_address = signer::address_of(delegate_signer); let offerer_account_resource = borrow_global<Account>(rotation_cap_offerer_address); assert!( @@ -1508,7 +1508,7 @@ offer, calling this function will replace the previous recipient_addresslet addr = signer::address_of(account); assert!(exists_at(recipient_address), error::not_found(EACCOUNT_DOES_NOT_EXIST)); - // proof that this account intends to delegate its rotation capability to another account + // proof that this account intends to delegate its rotation capability to another account let account_resource = borrow_global_mut<Account>(addr); let proof_challenge = RotationCapabilityOfferProofChallengeV2 { chain_id: chain_id::get(), @@ -1548,7 +1548,7 @@ offer, calling this function will replace the previous recipient_addressabort error::invalid_argument(EINVALID_SCHEME) }; - // update the existing rotation capability offer or put in a new rotation capability offer for the current account + // update the existing rotation capability offer or put in a new rotation capability offer for the current account option::swap_or_fill(&mut account_resource.rotation_capability_offer.for, recipient_address); } @@ -1757,7 +1757,7 @@ to the account owner's signer capability). let source_address = signer::address_of(account); assert!(exists_at(recipient_address), error::not_found(EACCOUNT_DOES_NOT_EXIST)); - // Proof that this account intends to delegate its signer capability to another account. + // Proof that this account intends to delegate its signer capability to another account. let proof_challenge = SignerCapabilityOfferProofChallengeV2 { sequence_number: get_sequence_number(source_address), source_address, @@ -1766,7 +1766,7 @@ to the account owner's signer capability). verify_signed_message( source_address, account_scheme, account_public_key_bytes, signer_capability_sig_bytes, proof_challenge); - // Update the existing signer capability offer or put in a new signer capability offer for the recipient. + // Update the existing signer capability offer or put in a new signer capability offer for the recipient. let account_resource = borrow_global_mut<Account>(source_address); option::swap_or_fill(&mut account_resource.signer_capability_offer.for, recipient_address); } @@ -1913,7 +1913,7 @@ at the offerer's address.
public fun create_authorized_signer(account: &signer, offerer_address: address): signer acquires Account {
     assert!(exists_at(offerer_address), error::not_found(EOFFERER_ADDRESS_DOES_NOT_EXIST));
 
-    // Check if there's an existing signer capability offer from the offerer.
+    // Check if there's an existing signer capability offer from the offerer.
     let account_resource = borrow_global<Account>(offerer_address);
     let addr = signer::address_of(account);
     assert!(
@@ -2289,7 +2289,7 @@ Coin management methods.
 Capability based functions for efficient use.
 
 
-
public fun create_signer_with_capability(capability: &account::SignerCapability): signer
+
public fun create_signer_with_capability(capability: &account::SignerCapability): signer
 
@@ -2298,8 +2298,8 @@ Capability based functions for efficient use. Implementation -
public fun create_signer_with_capability(capability: &SignerCapability): signer {
-    let addr = &capability.account;
+
public fun create_signer_with_capability(capability: &SignerCapability): signer {
+    let addr = &capability.account;
     create_signer(*addr)
 }
 
@@ -2314,7 +2314,7 @@ Capability based functions for efficient use. -
public fun get_signer_capability_address(capability: &account::SignerCapability): address
+
public fun get_signer_capability_address(capability: &account::SignerCapability): address
 
@@ -2323,8 +2323,8 @@ Capability based functions for efficient use. Implementation -
public fun get_signer_capability_address(capability: &SignerCapability): address {
-    capability.account
+
public fun get_signer_capability_address(capability: &SignerCapability): address {
+    capability.account
 }
 
@@ -3506,13 +3506,13 @@ The guid_creation_num of the Account is up to MAX_U64. ### Function `create_signer_with_capability` -
public fun create_signer_with_capability(capability: &account::SignerCapability): signer
+
public fun create_signer_with_capability(capability: &account::SignerCapability): signer
 
-
let addr = capability.account;
+
let addr = capability.account;
 ensures signer::address_of(result) == addr;
 
diff --git a/aptos-move/framework/aptos-framework/doc/aggregator_v2.md b/aptos-move/framework/aptos-framework/doc/aggregator_v2.md index a5073c231961bf..227aaf4e82b41b 100644 --- a/aptos-move/framework/aptos-framework/doc/aggregator_v2.md +++ b/aptos-move/framework/aptos-framework/doc/aggregator_v2.md @@ -49,20 +49,6 @@ read, read_snapshot, read_derived_string - [Function `derive_string_concat`](#0x1_aggregator_v2_derive_string_concat) - [Function `copy_snapshot`](#0x1_aggregator_v2_copy_snapshot) - [Function `string_concat`](#0x1_aggregator_v2_string_concat) -- [Function `verify_aggregator_try_add_sub`](#0x1_aggregator_v2_verify_aggregator_try_add_sub) -- [Function `verify_aggregator_add_sub`](#0x1_aggregator_v2_verify_aggregator_add_sub) -- [Function `verify_correct_read`](#0x1_aggregator_v2_verify_correct_read) -- [Function `verify_invalid_read`](#0x1_aggregator_v2_verify_invalid_read) -- [Function `verify_invalid_is_least`](#0x1_aggregator_v2_verify_invalid_is_least) -- [Function `verify_copy_not_yet_supported`](#0x1_aggregator_v2_verify_copy_not_yet_supported) -- [Function `verify_string_concat1`](#0x1_aggregator_v2_verify_string_concat1) -- [Function `verify_aggregator_generic`](#0x1_aggregator_v2_verify_aggregator_generic) -- [Function `verify_aggregator_generic_add`](#0x1_aggregator_v2_verify_aggregator_generic_add) -- [Function `verify_aggregator_generic_sub`](#0x1_aggregator_v2_verify_aggregator_generic_sub) -- [Function `verify_aggregator_invalid_type1`](#0x1_aggregator_v2_verify_aggregator_invalid_type1) -- [Function `verify_snapshot_invalid_type1`](#0x1_aggregator_v2_verify_snapshot_invalid_type1) -- [Function `verify_snapshot_invalid_type2`](#0x1_aggregator_v2_verify_snapshot_invalid_type2) -- [Function `verify_aggregator_valid_type`](#0x1_aggregator_v2_verify_aggregator_valid_type) - [Specification](#@Specification_1) - [Struct `Aggregator`](#@Specification_1_Aggregator) - [Function `max_value`](#@Specification_1_max_value) @@ -82,23 +68,10 @@ read, read_snapshot, read_derived_string - [Function `derive_string_concat`](#@Specification_1_derive_string_concat) - [Function `copy_snapshot`](#@Specification_1_copy_snapshot) - [Function `string_concat`](#@Specification_1_string_concat) - - [Function `verify_aggregator_try_add_sub`](#@Specification_1_verify_aggregator_try_add_sub) - - [Function `verify_aggregator_add_sub`](#@Specification_1_verify_aggregator_add_sub) - - [Function `verify_invalid_read`](#@Specification_1_verify_invalid_read) - - [Function `verify_invalid_is_least`](#@Specification_1_verify_invalid_is_least) - - [Function `verify_copy_not_yet_supported`](#@Specification_1_verify_copy_not_yet_supported) - - [Function `verify_aggregator_generic`](#@Specification_1_verify_aggregator_generic) - - [Function `verify_aggregator_generic_add`](#@Specification_1_verify_aggregator_generic_add) - - [Function `verify_aggregator_generic_sub`](#@Specification_1_verify_aggregator_generic_sub) - - [Function `verify_aggregator_invalid_type1`](#@Specification_1_verify_aggregator_invalid_type1) - - [Function `verify_snapshot_invalid_type1`](#@Specification_1_verify_snapshot_invalid_type1) - - [Function `verify_snapshot_invalid_type2`](#@Specification_1_verify_snapshot_invalid_type2) - - [Function `verify_aggregator_valid_type`](#@Specification_1_verify_aggregator_valid_type)
use 0x1::error;
 use 0x1::features;
-use 0x1::option;
 use 0x1::string;
 
@@ -807,430 +780,6 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI - - - - -## Function `verify_aggregator_try_add_sub` - - - -
#[verify_only]
-fun verify_aggregator_try_add_sub(): aggregator_v2::Aggregator<u64>
-
- - - -
-Implementation - - -
fun verify_aggregator_try_add_sub(): Aggregator<u64> {
-    let agg = create_aggregator(10);
-    spec {
-        assert spec_get_max_value(agg) == 10;
-        assert spec_get_value(agg) == 0;
-    };
-    let x = try_add(&mut agg, 5);
-    spec {
-        assert x;
-        assert is_at_least(agg, 5);
-    };
-    let y = try_sub(&mut agg, 6);
-    spec {
-        assert !y;
-        assert spec_get_value(agg) == 5;
-        assert spec_get_max_value(agg) == 10;
-    };
-    let y = try_sub(&mut agg, 4);
-    spec {
-        assert y;
-        assert spec_get_value(agg) == 1;
-        assert spec_get_max_value(agg) == 10;
-    };
-    let x = try_add(&mut agg, 11);
-    spec {
-        assert !x;
-        assert spec_get_value(agg) == 1;
-        assert spec_get_max_value(agg) == 10;
-    };
-    let x = try_add(&mut agg, 9);
-    spec {
-        assert x;
-        assert spec_get_value(agg) == 10;
-        assert spec_get_max_value(agg) == 10;
-    };
-    agg
-}
-
- - - -
- - - -## Function `verify_aggregator_add_sub` - - - -
#[verify_only]
-fun verify_aggregator_add_sub(sub_value: u64, add_value: u64)
-
- - - -
-Implementation - - -
fun verify_aggregator_add_sub(sub_value: u64, add_value: u64) {
-    let agg = create_aggregator(10);
-    add(&mut agg, add_value);
-    spec {
-        assert spec_get_value(agg) == add_value;
-    };
-    sub(&mut agg, sub_value);
-    spec {
-        assert spec_get_value(agg) == add_value - sub_value;
-    };
-}
-
- - - -
- - - -## Function `verify_correct_read` - - - -
#[verify_only]
-fun verify_correct_read()
-
- - - -
-Implementation - - -
fun verify_correct_read() {
-    let snapshot = create_snapshot(42);
-    spec {
-        assert spec_read_snapshot(snapshot) == 42;
-    };
-    let derived = create_derived_string(std::string::utf8(b"42"));
-    spec {
-        assert spec_read_derived_string(derived).bytes == b"42";
-    };
-}
-
- - - -
- - - -## Function `verify_invalid_read` - - - -
#[verify_only]
-fun verify_invalid_read(aggregator: &aggregator_v2::Aggregator<u8>): u8
-
- - - -
-Implementation - - -
fun verify_invalid_read(aggregator: &Aggregator<u8>): u8 {
-    read(aggregator)
-}
-
- - - -
- - - -## Function `verify_invalid_is_least` - - - -
#[verify_only]
-fun verify_invalid_is_least(aggregator: &aggregator_v2::Aggregator<u8>): bool
-
- - - -
-Implementation - - -
fun verify_invalid_is_least(aggregator: &Aggregator<u8>): bool {
-    is_at_least(aggregator, 0)
-}
-
- - - -
- - - -## Function `verify_copy_not_yet_supported` - - - -
#[verify_only]
-fun verify_copy_not_yet_supported()
-
- - - -
-Implementation - - -
fun verify_copy_not_yet_supported() {
-    let snapshot = create_snapshot(42);
-    copy_snapshot(&snapshot);
-}
-
- - - -
- - - -## Function `verify_string_concat1` - - - -
#[verify_only]
-fun verify_string_concat1()
-
- - - -
-Implementation - - -
fun verify_string_concat1() {
-    let snapshot = create_snapshot(42);
-    let derived = derive_string_concat(std::string::utf8(b"before"), &snapshot, std::string::utf8(b"after"));
-    spec {
-        assert spec_read_derived_string(derived).bytes ==
-            concat(b"before", concat(spec_get_string_value(snapshot).bytes, b"after"));
-    };
-}
-
- - - -
- - - -## Function `verify_aggregator_generic` - - - -
#[verify_only]
-fun verify_aggregator_generic<IntElement1: copy, drop, IntElement2: copy, drop>(): (aggregator_v2::Aggregator<IntElement1>, aggregator_v2::Aggregator<IntElement2>)
-
- - - -
-Implementation - - -
fun verify_aggregator_generic<IntElement1: copy + drop, IntElement2: copy+drop>(): (Aggregator<IntElement1>,  Aggregator<IntElement2>){
-    let x = create_unbounded_aggregator<IntElement1>();
-    let y = create_unbounded_aggregator<IntElement2>();
-    (x, y)
-}
-
- - - -
- - - -## Function `verify_aggregator_generic_add` - - - -
#[verify_only]
-fun verify_aggregator_generic_add<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
-
- - - -
-Implementation - - -
fun verify_aggregator_generic_add<IntElement: copy + drop>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
-    try_add(aggregator, value);
-    is_at_least_impl(aggregator, value);
-    // cannot specify aborts_if condition for generic `add`
-    // because comparison is not supported by IntElement
-    add(aggregator, value);
-}
-
- - - -
- - - -## Function `verify_aggregator_generic_sub` - - - -
#[verify_only]
-fun verify_aggregator_generic_sub<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
-
- - - -
-Implementation - - -
fun verify_aggregator_generic_sub<IntElement: copy + drop>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
-    try_sub(aggregator, value);
-    // cannot specify aborts_if condition for generic `sub`
-    // because comparison is not supported by IntElement
-    sub(aggregator, value);
-}
-
- - - -
- - - -## Function `verify_aggregator_invalid_type1` - - - -
#[verify_only]
-fun verify_aggregator_invalid_type1()
-
- - - -
-Implementation - - -
fun verify_aggregator_invalid_type1() {
-    create_unbounded_aggregator<u8>();
-}
-
- - - -
- - - -## Function `verify_snapshot_invalid_type1` - - - -
#[verify_only]
-fun verify_snapshot_invalid_type1()
-
- - - -
-Implementation - - -
fun verify_snapshot_invalid_type1() {
-    use std::option;
-    create_snapshot(option::some(42));
-}
-
- - - -
- - - -## Function `verify_snapshot_invalid_type2` - - - -
#[verify_only]
-fun verify_snapshot_invalid_type2()
-
- - - -
-Implementation - - -
fun verify_snapshot_invalid_type2() {
-    create_snapshot(vector[42]);
-}
-
- - - -
- - - -## Function `verify_aggregator_valid_type` - - - -
#[verify_only]
-fun verify_aggregator_valid_type()
-
- - - -
-Implementation - - -
fun verify_aggregator_valid_type() {
-    let _agg_1 = create_unbounded_aggregator<u64>();
-    spec {
-        assert spec_get_max_value(_agg_1) == MAX_U64;
-    };
-    let _agg_2 = create_unbounded_aggregator<u128>();
-    spec {
-        assert spec_get_max_value(_agg_2) == MAX_U128;
-    };
-    create_aggregator<u64>(5);
-    create_aggregator<u128>(5);
-}
-
- - -
@@ -1618,213 +1167,4 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
- - - -### Function `verify_aggregator_try_add_sub` - - -
#[verify_only]
-fun verify_aggregator_try_add_sub(): aggregator_v2::Aggregator<u64>
-
- - - - -
ensures spec_get_max_value(result) == 10;
-ensures spec_get_value(result) == 10;
-ensures read(result) == 10;
-
- - - - - -### Function `verify_aggregator_add_sub` - - -
#[verify_only]
-fun verify_aggregator_add_sub(sub_value: u64, add_value: u64)
-
- - - - -
pragma aborts_if_is_strict;
-aborts_if add_value > 10;
-aborts_if sub_value > add_value;
-
- - - - - -### Function `verify_invalid_read` - - -
#[verify_only]
-fun verify_invalid_read(aggregator: &aggregator_v2::Aggregator<u8>): u8
-
- - - - -
aborts_if true;
-
- - - - - -### Function `verify_invalid_is_least` - - -
#[verify_only]
-fun verify_invalid_is_least(aggregator: &aggregator_v2::Aggregator<u8>): bool
-
- - - - -
aborts_if true;
-
- - - - - -### Function `verify_copy_not_yet_supported` - - -
#[verify_only]
-fun verify_copy_not_yet_supported()
-
- - - - -
aborts_if true;
-
- - - - - -### Function `verify_aggregator_generic` - - -
#[verify_only]
-fun verify_aggregator_generic<IntElement1: copy, drop, IntElement2: copy, drop>(): (aggregator_v2::Aggregator<IntElement1>, aggregator_v2::Aggregator<IntElement2>)
-
- - - - -
aborts_if type_info::type_name<IntElement1>().bytes != b"u64" && type_info::type_name<IntElement1>().bytes != b"u128";
-aborts_if type_info::type_name<IntElement2>().bytes != b"u64" && type_info::type_name<IntElement2>().bytes != b"u128";
-
- - - - - -### Function `verify_aggregator_generic_add` - - -
#[verify_only]
-fun verify_aggregator_generic_add<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
-
- - - - -
aborts_if type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
-
- - - - - -### Function `verify_aggregator_generic_sub` - - -
#[verify_only]
-fun verify_aggregator_generic_sub<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
-
- - - - -
aborts_if type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
-
- - - - - -### Function `verify_aggregator_invalid_type1` - - -
#[verify_only]
-fun verify_aggregator_invalid_type1()
-
- - - - -
aborts_if true;
-
- - - - - -### Function `verify_snapshot_invalid_type1` - - -
#[verify_only]
-fun verify_snapshot_invalid_type1()
-
- - - - -
aborts_if true;
-
- - - - - -### Function `verify_snapshot_invalid_type2` - - -
#[verify_only]
-fun verify_snapshot_invalid_type2()
-
- - - - -
aborts_if true;
-
- - - - - -### Function `verify_aggregator_valid_type` - - -
#[verify_only]
-fun verify_aggregator_valid_type()
-
- - - - -
aborts_if false;
-
- - [move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md index c90cc82da7e235..a016def9bf443b 100644 --- a/aptos-move/framework/aptos-framework/doc/aptos_governance.md +++ b/aptos-move/framework/aptos-framework/doc/aptos_governance.md @@ -61,7 +61,6 @@ on a proposal multiple times as long as the total voting power of these votes do - [Function `get_signer`](#0x1_aptos_governance_get_signer) - [Function `create_proposal_metadata`](#0x1_aptos_governance_create_proposal_metadata) - [Function `assert_voting_initialization`](#0x1_aptos_governance_assert_voting_initialization) -- [Function `initialize_for_verification`](#0x1_aptos_governance_initialize_for_verification) - [Specification](#@Specification_1) - [High-level Requirements](#high-level-req) - [Module-level Specification](#module-level-spec) @@ -96,7 +95,6 @@ on a proposal multiple times as long as the total voting power of these votes do - [Function `get_signer`](#@Specification_1_get_signer) - [Function `create_proposal_metadata`](#@Specification_1_create_proposal_metadata) - [Function `assert_voting_initialization`](#@Specification_1_assert_voting_initialization) - - [Function `initialize_for_verification`](#@Specification_1_initialize_for_verification)
use 0x1::account;
@@ -1888,7 +1886,7 @@ Only called in testnet where the core resources account exists and has been gran
 
public fun get_signer_testnet_only(
     core_resources: &signer, signer_address: address): signer acquires GovernanceResponsbility {
     system_addresses::assert_core_resource(core_resources);
-    // Core resources account only has mint capability in tests/testnets.
+    // Core resources account only has mint capability in tests/testnets.
     assert!(aptos_coin::has_mint_capability(core_resources), error::unauthenticated(EUNAUTHORIZED));
     get_signer(signer_address)
 }
@@ -2017,36 +2015,6 @@ Return a signer for making changes to 0x1 as part of on-chain governance proposa
 
 
 
-
-
-
-
-## Function `initialize_for_verification`
-
-
-
-
#[verify_only]
-public fun initialize_for_verification(aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
-
- - - -
-Implementation - - -
public fun initialize_for_verification(
-    aptos_framework: &signer,
-    min_voting_threshold: u128,
-    required_proposer_stake: u64,
-    voting_duration_secs: u64,
-) {
-    initialize(aptos_framework, min_voting_threshold, required_proposer_stake, voting_duration_secs);
-}
-
- - -
@@ -3240,22 +3208,4 @@ pool_address must exist in StakePool.
- - - -### Function `initialize_for_verification` - - -
#[verify_only]
-public fun initialize_for_verification(aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
-
- - -verify_only - - -
pragma verify = false;
-
- - [move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/aptos-framework/doc/delegation_pool.md b/aptos-move/framework/aptos-framework/doc/delegation_pool.md index 268d0618fb722f..dc982b152e0d76 100644 --- a/aptos-move/framework/aptos-framework/doc/delegation_pool.md +++ b/aptos-move/framework/aptos-framework/doc/delegation_pool.md @@ -2895,7 +2895,7 @@ The existing voter will be replaced. The function is permissionless. let delegation_pool = borrow_global<DelegationPool>(pool_address); let stake_pool_signer = retrieve_stake_pool_owner(delegation_pool); - // delegated_voter is managed by the stake pool itself, which signer capability is managed by DelegationPool. + // delegated_voter is managed by the stake pool itself, which signer capability is managed by DelegationPool. // So voting power of this stake pool can only be used through this module. stake::set_delegated_voter(&stake_pool_signer, signer::address_of(&stake_pool_signer)); diff --git a/aptos-move/framework/aptos-framework/doc/genesis.md b/aptos-move/framework/aptos-framework/doc/genesis.md index 4df4a2f99b3011..c00fc63568ee43 100644 --- a/aptos-move/framework/aptos-framework/doc/genesis.md +++ b/aptos-move/framework/aptos-framework/doc/genesis.md @@ -21,7 +21,6 @@ - [Function `create_initialize_validator`](#0x1_genesis_create_initialize_validator) - [Function `initialize_validator`](#0x1_genesis_initialize_validator) - [Function `set_genesis_end`](#0x1_genesis_set_genesis_end) -- [Function `initialize_for_verification`](#0x1_genesis_initialize_for_verification) - [Specification](#@Specification_1) - [High-level Requirements](#high-level-req) - [Module-level Specification](#module-level-spec) @@ -31,7 +30,6 @@ - [Function `create_initialize_validators`](#@Specification_1_create_initialize_validators) - [Function `create_initialize_validator`](#@Specification_1_create_initialize_validator) - [Function `set_genesis_end`](#@Specification_1_set_genesis_end) - - [Function `initialize_for_verification`](#@Specification_1_initialize_for_verification)
use 0x1::account;
@@ -47,7 +45,6 @@
 use 0x1::create_signer;
 use 0x1::error;
 use 0x1::execution_config;
-use 0x1::features;
 use 0x1::fixed_point32;
 use 0x1::gas_schedule;
 use 0x1::reconfiguration;
@@ -825,80 +822,6 @@ The last step of genesis.
 
 
 
-
-
-
-
-## Function `initialize_for_verification`
-
-
-
-
#[verify_only]
-fun initialize_for_verification(gas_schedule: vector<u8>, chain_id: u8, initial_version: u64, consensus_config: vector<u8>, execution_config: vector<u8>, epoch_interval_microsecs: u64, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64, aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64, accounts: vector<genesis::AccountMap>, employee_vesting_start: u64, employee_vesting_period_duration: u64, employees: vector<genesis::EmployeeAccountMap>, validators: vector<genesis::ValidatorConfigurationWithCommission>)
-
- - - -
-Implementation - - -
fun initialize_for_verification(
-    gas_schedule: vector<u8>,
-    chain_id: u8,
-    initial_version: u64,
-    consensus_config: vector<u8>,
-    execution_config: vector<u8>,
-    epoch_interval_microsecs: u64,
-    minimum_stake: u64,
-    maximum_stake: u64,
-    recurring_lockup_duration_secs: u64,
-    allow_validator_set_change: bool,
-    rewards_rate: u64,
-    rewards_rate_denominator: u64,
-    voting_power_increase_limit: u64,
-    aptos_framework: &signer,
-    min_voting_threshold: u128,
-    required_proposer_stake: u64,
-    voting_duration_secs: u64,
-    accounts: vector<AccountMap>,
-    employee_vesting_start: u64,
-    employee_vesting_period_duration: u64,
-    employees: vector<EmployeeAccountMap>,
-    validators: vector<ValidatorConfigurationWithCommission>
-) {
-    initialize(
-        gas_schedule,
-        chain_id,
-        initial_version,
-        consensus_config,
-        execution_config,
-        epoch_interval_microsecs,
-        minimum_stake,
-        maximum_stake,
-        recurring_lockup_duration_secs,
-        allow_validator_set_change,
-        rewards_rate,
-        rewards_rate_denominator,
-        voting_power_increase_limit
-    );
-    features::change_feature_flags_for_verification(aptos_framework, vector[1, 2], vector[]);
-    initialize_aptos_coin(aptos_framework);
-    aptos_governance::initialize_for_verification(
-        aptos_framework,
-        min_voting_threshold,
-        required_proposer_stake,
-        voting_duration_secs
-    );
-    create_accounts(aptos_framework, accounts);
-    create_employee_validators(employee_vesting_start, employee_vesting_period_duration, employees);
-    create_initialize_validators_with_commission(aptos_framework, true, validators);
-    set_genesis_end(aptos_framework);
-}
-
- - -
@@ -1156,22 +1079,4 @@ The last step of genesis.
- - - -### Function `initialize_for_verification` - - -
#[verify_only]
-fun initialize_for_verification(gas_schedule: vector<u8>, chain_id: u8, initial_version: u64, consensus_config: vector<u8>, execution_config: vector<u8>, epoch_interval_microsecs: u64, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64, aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64, accounts: vector<genesis::AccountMap>, employee_vesting_start: u64, employee_vesting_period_duration: u64, employees: vector<genesis::EmployeeAccountMap>, validators: vector<genesis::ValidatorConfigurationWithCommission>)
-
- - - - -
pragma verify_duration_estimate = 120;
-include InitalizeRequires;
-
- - [move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/aptos-framework/doc/multisig_account.md b/aptos-move/framework/aptos-framework/doc/multisig_account.md index 4117c18c991060..0b6aa0e44dd7ad 100644 --- a/aptos-move/framework/aptos-framework/doc/multisig_account.md +++ b/aptos-move/framework/aptos-framework/doc/multisig_account.md @@ -2090,7 +2090,7 @@ account. // Rotate the account's auth key to 0x0, which effectively revokes control via auth key. let multisig_address = address_of(multisig_account); account::rotate_authentication_key_internal(multisig_account, ZERO_AUTH_KEY); - // This also needs to revoke any signer capability or rotation capability that exists for the account to + // This also needs to revoke any signer capability or rotation capability that exists for the account to // completely remove all access to the account. if (account::is_signer_capability_offered(multisig_address)) { account::revoke_any_signer_capability(multisig_account); @@ -2168,7 +2168,7 @@ account. // Rotate the account's auth key to 0x0, which effectively revokes control via auth key. let multisig_address = address_of(multisig_account); account::rotate_authentication_key_internal(multisig_account, ZERO_AUTH_KEY); - // This also needs to revoke any signer capability or rotation capability that exists for the account to + // This also needs to revoke any signer capability or rotation capability that exists for the account to // completely remove all access to the account. if (account::is_signer_capability_offered(multisig_address)) { account::revoke_any_signer_capability(multisig_account); diff --git a/aptos-move/framework/aptos-framework/doc/permissioned_signer.md b/aptos-move/framework/aptos-framework/doc/permissioned_signer.md new file mode 100644 index 00000000000000..36c930a7430824 --- /dev/null +++ b/aptos-move/framework/aptos-framework/doc/permissioned_signer.md @@ -0,0 +1,1931 @@ + + + +# Module `0x1::permissioned_signer` + +A _permissioned signer_ consists of a pair of the original signer and a generated +address which is used store information about associated permissions. + +A permissioned signer is a restricted version of a signer. Functions move_to and +address_of behave the same, and can be passed wherever signer is needed. However, +code can internally query for the permissions to assert additional restrictions on +the use of the signer. + +A client which is interested in restricting access granted via a signer can create a permissioned signer +and pass on to other existing code without changes to existing APIs. Core functions in the framework, for +example account functions, can then assert availability of permissions, effectively restricting +existing code in a compatible way. + +After introducing the core functionality, examples are provided for withdraw limit on accounts, and +for blind signing. + + +- [Resource `GrantedPermissionHandles`](#0x1_permissioned_signer_GrantedPermissionHandles) +- [Enum `PermissionedHandle`](#0x1_permissioned_signer_PermissionedHandle) +- [Enum `StorablePermissionedHandle`](#0x1_permissioned_signer_StorablePermissionedHandle) +- [Enum Resource `PermissionStorage`](#0x1_permissioned_signer_PermissionStorage) +- [Enum `StoredPermission`](#0x1_permissioned_signer_StoredPermission) +- [Enum `Permission`](#0x1_permissioned_signer_Permission) +- [Constants](#@Constants_0) +- [Function `create_permissioned_handle`](#0x1_permissioned_signer_create_permissioned_handle) +- [Function `create_storable_permissioned_handle`](#0x1_permissioned_signer_create_storable_permissioned_handle) +- [Function `destroy_permissioned_handle`](#0x1_permissioned_signer_destroy_permissioned_handle) +- [Function `destroy_storable_permissioned_handle`](#0x1_permissioned_signer_destroy_storable_permissioned_handle) +- [Function `destroy_permissions_storage_address`](#0x1_permissioned_signer_destroy_permissions_storage_address) +- [Function `signer_from_permissioned_handle`](#0x1_permissioned_signer_signer_from_permissioned_handle) +- [Function `signer_from_storable_permissioned_handle`](#0x1_permissioned_signer_signer_from_storable_permissioned_handle) +- [Function `revoke_permission_storage_address`](#0x1_permissioned_signer_revoke_permission_storage_address) +- [Function `revoke_all_handles`](#0x1_permissioned_signer_revoke_all_handles) +- [Function `permissions_storage_address`](#0x1_permissioned_signer_permissions_storage_address) +- [Function `assert_master_signer`](#0x1_permissioned_signer_assert_master_signer) +- [Function `is_above`](#0x1_permissioned_signer_is_above) +- [Function `consume_capacity`](#0x1_permissioned_signer_consume_capacity) +- [Function `increase_capacity`](#0x1_permissioned_signer_increase_capacity) +- [Function `merge`](#0x1_permissioned_signer_merge) +- [Function `map_or`](#0x1_permissioned_signer_map_or) +- [Function `insert_or`](#0x1_permissioned_signer_insert_or) +- [Function `authorize`](#0x1_permissioned_signer_authorize) +- [Function `authorize_unlimited`](#0x1_permissioned_signer_authorize_unlimited) +- [Function `check_permission_exists`](#0x1_permissioned_signer_check_permission_exists) +- [Function `check_permission_capacity_above`](#0x1_permissioned_signer_check_permission_capacity_above) +- [Function `check_permission_consume`](#0x1_permissioned_signer_check_permission_consume) +- [Function `capacity`](#0x1_permissioned_signer_capacity) +- [Function `revoke_permission`](#0x1_permissioned_signer_revoke_permission) +- [Function `extract_permission`](#0x1_permissioned_signer_extract_permission) +- [Function `extract_all_permission`](#0x1_permissioned_signer_extract_all_permission) +- [Function `address_of`](#0x1_permissioned_signer_address_of) +- [Function `consume_permission`](#0x1_permissioned_signer_consume_permission) +- [Function `store_permission`](#0x1_permissioned_signer_store_permission) +- [Function `is_permissioned_signer`](#0x1_permissioned_signer_is_permissioned_signer) +- [Function `permission_address`](#0x1_permissioned_signer_permission_address) +- [Function `signer_from_permissioned_handle_impl`](#0x1_permissioned_signer_signer_from_permissioned_handle_impl) +- [Specification](#@Specification_1) + - [Function `create_permissioned_handle`](#@Specification_1_create_permissioned_handle) + - [Function `create_storable_permissioned_handle`](#@Specification_1_create_storable_permissioned_handle) + - [Function `destroy_permissioned_handle`](#@Specification_1_destroy_permissioned_handle) + - [Function `destroy_storable_permissioned_handle`](#@Specification_1_destroy_storable_permissioned_handle) + - [Function `revoke_permission_storage_address`](#@Specification_1_revoke_permission_storage_address) + - [Function `authorize`](#@Specification_1_authorize) + - [Function `check_permission_exists`](#@Specification_1_check_permission_exists) + - [Function `check_permission_capacity_above`](#@Specification_1_check_permission_capacity_above) + - [Function `check_permission_consume`](#@Specification_1_check_permission_consume) + - [Function `capacity`](#@Specification_1_capacity) + - [Function `consume_permission`](#@Specification_1_consume_permission) + - [Function `is_permissioned_signer`](#@Specification_1_is_permissioned_signer) + - [Function `permission_address`](#@Specification_1_permission_address) + - [Function `signer_from_permissioned_handle_impl`](#@Specification_1_signer_from_permissioned_handle_impl) + + +
use 0x1::copyable_any;
+use 0x1::create_signer;
+use 0x1::error;
+use 0x1::option;
+use 0x1::signer;
+use 0x1::simple_map;
+use 0x1::timestamp;
+use 0x1::transaction_context;
+use 0x1::vector;
+
+ + + + + +## Resource `GrantedPermissionHandles` + + + +
struct GrantedPermissionHandles has key
+
+ + + +
+Fields + + +
+
+active_handles: vector<address> +
+
+ +
+
+ + +
+ + + +## Enum `PermissionedHandle` + + + +
enum PermissionedHandle
+
+ + + +
+Variants + + +
+V1 + + +
+Fields + + +
+
+master_account_addr: address +
+
+ +
+
+permissions_storage_addr: address +
+
+ +
+
+ + +
+ +
+ +
+ + + +## Enum `StorablePermissionedHandle` + + + +
enum StorablePermissionedHandle has store
+
+ + + +
+Variants + + +
+V1 + + +
+Fields + + +
+
+master_account_addr: address +
+
+ +
+
+permissions_storage_addr: address +
+
+ +
+
+expiration_time: u64 +
+
+ +
+
+ + +
+ +
+ +
+ + + +## Enum Resource `PermissionStorage` + + + +
enum PermissionStorage has key
+
+ + + +
+Variants + + +
+V1 + + +
+Fields + + +
+
+perms: simple_map::SimpleMap<copyable_any::Any, permissioned_signer::StoredPermission> +
+
+ +
+
+ + +
+ +
+ +
+ + + +## Enum `StoredPermission` + + + +
enum StoredPermission has copy, drop, store
+
+ + + +
+Variants + + +
+Unlimited + + +
+Fields + + +
+
+ + +
+ +
+ +
+Capacity + + +
+Fields + + +
+
+0: u256 +
+
+ +
+
+ + +
+ +
+ +
+ + + +## Enum `Permission` + + + +
enum Permission<K>
+
+ + + +
+Variants + + +
+V1 + + +
+Fields + + +
+
+owner_address: address +
+
+ +
+
+key: K +
+
+ +
+
+perm: permissioned_signer::StoredPermission +
+
+ +
+
+ + +
+ +
+ +
+ + + +## Constants + + + + +Cannot authorize a permission. + + +
const ECANNOT_AUTHORIZE: u64 = 2;
+
+ + + + + +signer doesn't have enough capacity to extract permission. + + +
const ECANNOT_EXTRACT_PERMISSION: u64 = 4;
+
+ + + + + +Trying to grant permission using master signer. + + +
const ENOT_MASTER_SIGNER: u64 = 1;
+
+ + + + + +Access permission information from a master signer. + + +
const ENOT_PERMISSIONED_SIGNER: u64 = 3;
+
+ + + + + +destroying permission handle that has already been revoked or not owned by the +given master signer. + + +
const E_NOT_ACTIVE: u64 = 8;
+
+ + + + + +permission handle has expired. + + +
const E_PERMISSION_EXPIRED: u64 = 5;
+
+ + + + + +storing extracted permission into a different signer. + + +
const E_PERMISSION_MISMATCH: u64 = 6;
+
+ + + + + +permission handle has been revoked by the original signer. + + +
const E_PERMISSION_REVOKED: u64 = 7;
+
+ + + + + + + +
const U256_MAX: u256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
+
+ + + + + +## Function `create_permissioned_handle` + +Create an ephermeral permission handle based on the master signer. + +This handle can be used to derive a signer that can be used in the context of +the current transaction. + + +
public fun create_permissioned_handle(master: &signer): permissioned_signer::PermissionedHandle
+
+ + + +
+Implementation + + +
public fun create_permissioned_handle(master: &signer): PermissionedHandle {
+    assert_master_signer(master);
+    let permissions_storage_addr = generate_auid_address();
+    let master_account_addr = signer::address_of(master);
+
+    move_to(
+        &create_signer(permissions_storage_addr),
+        PermissionStorage::V1 { perms: simple_map::new() }
+    );
+
+    PermissionedHandle::V1 { master_account_addr, permissions_storage_addr }
+}
+
+ + + +
+ + + +## Function `create_storable_permissioned_handle` + +Create an storable permission handle based on the master signer. + +This handle can be used to derive a signer that can be stored by a smart contract. +This is as dangerous as key delegation, thus it remains public(package) for now. + +The caller should check if expiration_time is not too far in the future. + + +
public(friend) fun create_storable_permissioned_handle(master: &signer, expiration_time: u64): permissioned_signer::StorablePermissionedHandle
+
+ + + +
+Implementation + + +
public(package) fun create_storable_permissioned_handle(
+    master: &signer, expiration_time: u64
+): StorablePermissionedHandle acquires GrantedPermissionHandles {
+    assert_master_signer(master);
+    let permissions_storage_addr = generate_auid_address();
+    let master_account_addr = signer::address_of(master);
+
+    assert!(
+        timestamp::now_seconds() < expiration_time,
+        error::permission_denied(E_PERMISSION_EXPIRED)
+    );
+
+    if (!exists<GrantedPermissionHandles>(master_account_addr)) {
+        move_to<GrantedPermissionHandles>(
+            master, GrantedPermissionHandles { active_handles: vector::empty() }
+        );
+    };
+
+    vector::push_back(
+        &mut borrow_global_mut<GrantedPermissionHandles>(master_account_addr).active_handles,
+        permissions_storage_addr
+    );
+
+    move_to(
+        &create_signer(permissions_storage_addr),
+        PermissionStorage::V1 { perms: simple_map::new() }
+    );
+
+    StorablePermissionedHandle::V1 {
+        master_account_addr,
+        permissions_storage_addr,
+        expiration_time
+    }
+}
+
+ + + +
+ + + +## Function `destroy_permissioned_handle` + +Destroys an ephermeral permission handle. Clean up the permission stored in that handle + + +
public fun destroy_permissioned_handle(p: permissioned_signer::PermissionedHandle)
+
+ + + +
+Implementation + + +
public fun destroy_permissioned_handle(p: PermissionedHandle) acquires PermissionStorage {
+    let PermissionedHandle::V1 { master_account_addr: _, permissions_storage_addr } =
+        p;
+    destroy_permissions_storage_address(permissions_storage_addr);
+}
+
+ + + +
+ + + +## Function `destroy_storable_permissioned_handle` + +Destroys a storable permission handle. Clean up the permission stored in that handle + + +
public(friend) fun destroy_storable_permissioned_handle(p: permissioned_signer::StorablePermissionedHandle)
+
+ + + +
+Implementation + + +
public(package) fun destroy_storable_permissioned_handle(
+    p: StorablePermissionedHandle
+) acquires PermissionStorage, GrantedPermissionHandles {
+    let StorablePermissionedHandle::V1 {
+        master_account_addr,
+        permissions_storage_addr,
+        expiration_time: _
+    } = p;
+
+    assert!(
+        exists<GrantedPermissionHandles>(master_account_addr),
+        error::permission_denied(E_PERMISSION_REVOKED),
+    );
+    let granted_permissions =
+        borrow_global_mut<GrantedPermissionHandles>(master_account_addr);
+    let (found, idx) = vector::index_of(
+        &granted_permissions.active_handles, &permissions_storage_addr
+    );
+
+    // Removing the address from the active handle list if it's still active.
+    if(found) {
+        vector::swap_remove(&mut granted_permissions.active_handles, idx);
+    };
+
+    destroy_permissions_storage_address(permissions_storage_addr);
+}
+
+ + + +
+ + + +## Function `destroy_permissions_storage_address` + + + +
fun destroy_permissions_storage_address(permissions_storage_addr: address)
+
+ + + +
+Implementation + + +
inline fun destroy_permissions_storage_address(
+    permissions_storage_addr: address
+) acquires PermissionStorage {
+    if (exists<PermissionStorage>(permissions_storage_addr)) {
+        let PermissionStorage::V1 { perms } =
+            move_from<PermissionStorage>(permissions_storage_addr);
+        simple_map::destroy(
+            perms,
+            |_dk| {},
+            |_dv| {}
+        );
+    }
+}
+
+ + + +
+ + + +## Function `signer_from_permissioned_handle` + +Generate the permissioned signer based on the ephermeral permission handle. + +This signer can be used as a regular signer for other smart contracts. However when such +signer interacts with various framework functions, it would subject to permission checks +and would abort if check fails. + + +
public fun signer_from_permissioned_handle(p: &permissioned_signer::PermissionedHandle): signer
+
+ + + +
+Implementation + + +
public fun signer_from_permissioned_handle(p: &PermissionedHandle): signer {
+    signer_from_permissioned_handle_impl(
+        p.master_account_addr, p.permissions_storage_addr
+    )
+}
+
+ + + +
+ + + +## Function `signer_from_storable_permissioned_handle` + +Generate the permissioned signer based on the storable permission handle. + + +
public(friend) fun signer_from_storable_permissioned_handle(p: &permissioned_signer::StorablePermissionedHandle): signer
+
+ + + +
+Implementation + + +
public(package) fun signer_from_storable_permissioned_handle(
+    p: &StorablePermissionedHandle
+): signer {
+    assert!(
+        timestamp::now_seconds() < p.expiration_time,
+        error::permission_denied(E_PERMISSION_EXPIRED)
+    );
+    assert!(
+        exists<PermissionStorage>(p.permissions_storage_addr),
+        error::permission_denied(E_PERMISSION_REVOKED)
+    );
+    signer_from_permissioned_handle_impl(
+        p.master_account_addr, p.permissions_storage_addr
+    )
+}
+
+ + + +
+ + + +## Function `revoke_permission_storage_address` + +Revoke a specific storable permission handle immediately. This would disallow owner of +the storable permission handle to derive signer from it anymore. + + +
public entry fun revoke_permission_storage_address(s: &signer, permissions_storage_addr: address)
+
+ + + +
+Implementation + + +
public entry fun revoke_permission_storage_address(
+    s: &signer, permissions_storage_addr: address
+) acquires GrantedPermissionHandles, PermissionStorage {
+    assert!(
+        !is_permissioned_signer(s), error::permission_denied(ENOT_MASTER_SIGNER)
+    );
+    let master_account_addr = signer::address_of(s);
+
+    assert!(
+        exists<GrantedPermissionHandles>(master_account_addr),
+        error::permission_denied(E_PERMISSION_REVOKED),
+    );
+    let granted_permissions =
+        borrow_global_mut<GrantedPermissionHandles>(master_account_addr);
+    let (found, idx) = vector::index_of(
+        &granted_permissions.active_handles, &permissions_storage_addr
+    );
+
+    // The address has to be in the activated list in the master account address.
+    assert!(found, error::permission_denied(E_NOT_ACTIVE));
+    vector::swap_remove(&mut granted_permissions.active_handles, idx);
+    destroy_permissions_storage_address(permissions_storage_addr);
+}
+
+ + + +
+ + + +## Function `revoke_all_handles` + +Revoke all storable permission handle of the signer immediately. + + +
public entry fun revoke_all_handles(s: &signer)
+
+ + + +
+Implementation + + +
public entry fun revoke_all_handles(s: &signer) acquires GrantedPermissionHandles, PermissionStorage {
+    assert!(
+        !is_permissioned_signer(s), error::permission_denied(ENOT_MASTER_SIGNER)
+    );
+    let master_account_addr = signer::address_of(s);
+    if (!exists<GrantedPermissionHandles>(master_account_addr)) { return };
+
+    let granted_permissions =
+        borrow_global_mut<GrantedPermissionHandles>(master_account_addr);
+    let delete_list = vector::trim_reverse(
+        &mut granted_permissions.active_handles, 0
+    );
+    vector::destroy(
+        delete_list,
+        |address| {
+            destroy_permissions_storage_address(address);
+        }
+    )
+}
+
+ + + +
+ + + +## Function `permissions_storage_address` + +Return the permission handle address so that it could be used for revocation purpose. + + +
public(friend) fun permissions_storage_address(p: &permissioned_signer::StorablePermissionedHandle): address
+
+ + + +
+Implementation + + +
public(package) fun permissions_storage_address(
+    p: &StorablePermissionedHandle
+): address {
+    p.permissions_storage_addr
+}
+
+ + + +
+ + + +## Function `assert_master_signer` + +Helper function that would abort if the signer passed in is a permissioned signer. + + +
public fun assert_master_signer(s: &signer)
+
+ + + +
+Implementation + + +
public fun assert_master_signer(s: &signer) {
+    assert!(
+        !is_permissioned_signer(s), error::permission_denied(ENOT_MASTER_SIGNER)
+    );
+}
+
+ + + +
+ + + +## Function `is_above` + +===================================================================================================== +StoredPermission operations + +check if StoredPermission has at least threshold capacity. + + +
fun is_above(perm: &permissioned_signer::StoredPermission, threshold: u256): bool
+
+ + + +
+Implementation + + +
fun is_above(perm: &StoredPermission, threshold: u256): bool {
+    match (perm) {
+        StoredPermission::Capacity(capacity) => *capacity > threshold,
+        StoredPermission::Unlimited => true,
+    }
+}
+
+ + + +
+ + + +## Function `consume_capacity` + +consume threshold capacity from StoredPermission + + +
fun consume_capacity(perm: &mut permissioned_signer::StoredPermission, threshold: u256): bool
+
+ + + +
+Implementation + + +
fun consume_capacity(perm: &mut StoredPermission, threshold: u256): bool {
+    match (perm) {
+        StoredPermission::Capacity(current_capacity) => {
+            if (*current_capacity >= threshold) {
+                *current_capacity = *current_capacity - threshold;
+                true
+            } else { false }
+        }
+        StoredPermission::Unlimited => true
+    }
+}
+
+ + + +
+ + + +## Function `increase_capacity` + +increase threshold capacity from StoredPermission + + +
fun increase_capacity(perm: &mut permissioned_signer::StoredPermission, threshold: u256)
+
+ + + +
+Implementation + + +
fun increase_capacity(perm: &mut StoredPermission, threshold: u256) {
+    match (perm) {
+        StoredPermission::Capacity(current_capacity) => {
+            *current_capacity = *current_capacity + threshold;
+        }
+        StoredPermission::Unlimited => (),
+    }
+}
+
+ + + +
+ + + +## Function `merge` + +merge the two stored permission + + +
fun merge(lhs: &mut permissioned_signer::StoredPermission, rhs: permissioned_signer::StoredPermission)
+
+ + + +
+Implementation + + +
fun merge(lhs: &mut StoredPermission, rhs: StoredPermission) {
+    match (rhs) {
+        StoredPermission::Capacity(new_capacity) => {
+            match (lhs) {
+                StoredPermission::Capacity(current_capacity) => {
+                    *current_capacity = *current_capacity + new_capacity;
+                }
+                StoredPermission::Unlimited => (),
+            }
+        }
+        StoredPermission::Unlimited => *lhs = StoredPermission::Unlimited,
+    }
+}
+
+ + + +
+ + + +## Function `map_or` + +===================================================================================================== +Permission Management + +Authorizes permissioned with the given permission. This requires to have access to the master +signer. + + +
fun map_or<PermKey: copy, drop, store, T>(permissioned: &signer, perm: PermKey, mutate: |&mut permissioned_signer::StoredPermission|T, default: T): T
+
+ + + +
+Implementation + + +
inline fun map_or<PermKey: copy + drop + store, T>(
+    permissioned: &signer,
+    perm: PermKey,
+    mutate: |&mut StoredPermission| T,
+    default: T,
+): T {
+    let permission_signer_addr = permission_address(permissioned);
+    assert!(
+        exists<PermissionStorage>(permission_signer_addr),
+        error::permission_denied(E_NOT_ACTIVE)
+    );
+    let perms =
+        &mut borrow_global_mut<PermissionStorage>(permission_signer_addr).perms;
+    let key = copyable_any::pack(perm);
+    if (simple_map::contains_key(perms, &key)) {
+        mutate(simple_map::borrow_mut(perms, &key))
+    } else {
+        default
+    }
+}
+
+ + + +
+ + + +## Function `insert_or` + + + +
fun insert_or<PermKey: copy, drop, store>(permissioned: &signer, perm: PermKey, mutate: |&mut permissioned_signer::StoredPermission|, default: permissioned_signer::StoredPermission)
+
+ + + +
+Implementation + + +
inline fun insert_or<PermKey: copy + drop + store>(
+    permissioned: &signer,
+    perm: PermKey,
+    mutate: |&mut StoredPermission|,
+    default: StoredPermission,
+) {
+    let permission_signer_addr = permission_address(permissioned);
+    assert!(
+        exists<PermissionStorage>(permission_signer_addr),
+        error::permission_denied(E_NOT_ACTIVE)
+    );
+    let perms =
+        &mut borrow_global_mut<PermissionStorage>(permission_signer_addr).perms;
+    let key = copyable_any::pack(perm);
+    if (simple_map::contains_key(perms, &key)) {
+        mutate(simple_map::borrow_mut(perms, &key));
+    } else {
+        simple_map::add(perms, key, default);
+    }
+}
+
+ + + +
+ + + +## Function `authorize` + + + +
public fun authorize<PermKey: copy, drop, store>(master: &signer, permissioned: &signer, capacity: u256, perm: PermKey)
+
+ + + +
+Implementation + + +
public fun authorize<PermKey: copy + drop + store>(
+    master: &signer,
+    permissioned: &signer,
+    capacity: u256,
+    perm: PermKey
+) acquires PermissionStorage {
+    assert!(
+        is_permissioned_signer(permissioned)
+            && !is_permissioned_signer(master)
+            && signer::address_of(master) == signer::address_of(permissioned),
+        error::permission_denied(ECANNOT_AUTHORIZE)
+    );
+    insert_or(
+        permissioned,
+        perm,
+        |stored_permission| {
+            increase_capacity(stored_permission, capacity);
+        },
+        StoredPermission::Capacity(capacity),
+    )
+}
+
+ + + +
+ + + +## Function `authorize_unlimited` + +Authorizes permissioned with the given unlimited permission. +Unlimited permission can be consumed however many times. + + +
public fun authorize_unlimited<PermKey: copy, drop, store>(master: &signer, permissioned: &signer, perm: PermKey)
+
+ + + +
+Implementation + + +
public fun authorize_unlimited<PermKey: copy + drop + store>(
+    master: &signer,
+    permissioned: &signer,
+    perm: PermKey
+) acquires PermissionStorage {
+    assert!(
+        is_permissioned_signer(permissioned)
+            && !is_permissioned_signer(master)
+            && signer::address_of(master) == signer::address_of(permissioned),
+        error::permission_denied(ECANNOT_AUTHORIZE)
+    );
+    insert_or(
+        permissioned,
+        perm,
+        |stored_permission| {
+            *stored_permission = StoredPermission::Unlimited;
+        },
+        StoredPermission::Unlimited,
+    )
+}
+
+ + + +
+ + + +## Function `check_permission_exists` + + + +
public fun check_permission_exists<PermKey: copy, drop, store>(s: &signer, perm: PermKey): bool
+
+ + + +
+Implementation + + +
public fun check_permission_exists<PermKey: copy + drop + store>(
+    s: &signer, perm: PermKey
+): bool acquires PermissionStorage {
+    check_permission_capacity_above(s, 0, perm)
+}
+
+ + + +
+ + + +## Function `check_permission_capacity_above` + + + +
public fun check_permission_capacity_above<PermKey: copy, drop, store>(s: &signer, threshold: u256, perm: PermKey): bool
+
+ + + +
+Implementation + + +
public fun check_permission_capacity_above<PermKey: copy + drop + store>(
+    s: &signer, threshold: u256, perm: PermKey
+): bool acquires PermissionStorage {
+    if (!is_permissioned_signer(s)) {
+        // master signer has all permissions
+        return true
+    };
+    map_or(
+        s,
+        perm,
+        |stored_permission| {
+            is_above(stored_permission, threshold)
+        },
+        false,
+    )
+}
+
+ + + +
+ + + +## Function `check_permission_consume` + + + +
public fun check_permission_consume<PermKey: copy, drop, store>(s: &signer, threshold: u256, perm: PermKey): bool
+
+ + + +
+Implementation + + +
public fun check_permission_consume<PermKey: copy + drop + store>(
+    s: &signer, threshold: u256, perm: PermKey
+): bool acquires PermissionStorage {
+    if (!is_permissioned_signer(s)) {
+        // master signer has all permissions
+        return true
+    };
+    map_or(
+        s,
+        perm,
+        |stored_permission| {
+             consume_capacity(stored_permission, threshold)
+        },
+        false,
+    )
+}
+
+ + + +
+ + + +## Function `capacity` + + + +
public fun capacity<PermKey: copy, drop, store>(s: &signer, perm: PermKey): option::Option<u256>
+
+ + + +
+Implementation + + +
public fun capacity<PermKey: copy + drop + store>(
+    s: &signer, perm: PermKey
+): Option<u256> acquires PermissionStorage {
+    if (!is_permissioned_signer(s)) {
+        return option::some(U256_MAX)
+    };
+    map_or(
+        s,
+        perm,
+        |stored_permission: &mut StoredPermission| {
+            option::some(match (stored_permission) {
+                StoredPermission::Capacity(capacity) => *capacity,
+                StoredPermission::Unlimited => U256_MAX,
+            })
+        },
+        option::none(),
+    )
+}
+
+ + + +
+ + + +## Function `revoke_permission` + + + +
public fun revoke_permission<PermKey: copy, drop, store>(permissioned: &signer, perm: PermKey)
+
+ + + +
+Implementation + + +
public fun revoke_permission<PermKey: copy + drop + store>(
+    permissioned: &signer, perm: PermKey
+) acquires PermissionStorage {
+    if (!is_permissioned_signer(permissioned)) {
+        // Master signer has no permissions associated with it.
+        return
+    };
+    let addr = permission_address(permissioned);
+    if (!exists<PermissionStorage>(addr)) { return };
+    let perm_storage = &mut borrow_global_mut<PermissionStorage>(addr).perms;
+    let key = copyable_any::pack(perm);
+    if (simple_map::contains_key(perm_storage, &key)) {
+        simple_map::remove(
+            &mut borrow_global_mut<PermissionStorage>(addr).perms,
+            &copyable_any::pack(perm)
+        );
+    }
+}
+
+ + + +
+ + + +## Function `extract_permission` + +===================================================================================================== +Another flavor of api to extract and store permissions + + +
public(friend) fun extract_permission<PermKey: copy, drop, store>(s: &signer, weight: u256, perm: PermKey): permissioned_signer::Permission<PermKey>
+
+ + + +
+Implementation + + +
public(package) fun extract_permission<PermKey: copy + drop + store>(
+    s: &signer, weight: u256, perm: PermKey
+): Permission<PermKey> acquires PermissionStorage {
+    assert!(
+        check_permission_consume(s, weight, perm),
+        error::permission_denied(ECANNOT_EXTRACT_PERMISSION)
+    );
+    Permission::V1 {
+        owner_address: signer::address_of(s),
+        key: perm,
+        perm: StoredPermission::Capacity(weight),
+    }
+}
+
+ + + +
+ + + +## Function `extract_all_permission` + + + +
public(friend) fun extract_all_permission<PermKey: copy, drop, store>(s: &signer, perm_key: PermKey): permissioned_signer::Permission<PermKey>
+
+ + + +
+Implementation + + +
public(package) fun extract_all_permission<PermKey: copy + drop + store>(
+    s: &signer, perm_key: PermKey
+): Permission<PermKey> acquires PermissionStorage {
+    assert!(
+        is_permissioned_signer(s),
+        error::permission_denied(ECANNOT_EXTRACT_PERMISSION)
+    );
+    let addr = permission_address(s);
+    assert!(
+        exists<PermissionStorage>(addr),
+        error::permission_denied(ECANNOT_EXTRACT_PERMISSION)
+    );
+    let key = copyable_any::pack(perm_key);
+    let storage = &mut borrow_global_mut<PermissionStorage>(addr).perms;
+    let (_, value) = simple_map::remove(storage, &key);
+
+    Permission::V1 {
+        owner_address: signer::address_of(s),
+        key: perm_key,
+        perm: value,
+    }
+}
+
+ + + +
+ + + +## Function `address_of` + + + +
public(friend) fun address_of<PermKey>(perm: &permissioned_signer::Permission<PermKey>): address
+
+ + + +
+Implementation + + +
public(package) fun address_of<PermKey>(perm: &Permission<PermKey>): address {
+    perm.owner_address
+}
+
+ + + +
+ + + +## Function `consume_permission` + + + +
public(friend) fun consume_permission<PermKey: copy, drop, store>(perm: &mut permissioned_signer::Permission<PermKey>, weight: u256, perm_key: PermKey): bool
+
+ + + +
+Implementation + + +
public(package) fun consume_permission<PermKey: copy + drop + store>(
+    perm: &mut Permission<PermKey>, weight: u256, perm_key: PermKey
+): bool {
+    if (perm.key != perm_key) {
+        return false
+    };
+    consume_capacity(&mut perm.perm, weight)
+}
+
+ + + +
+ + + +## Function `store_permission` + + + +
public(friend) fun store_permission<PermKey: copy, drop, store>(s: &signer, perm: permissioned_signer::Permission<PermKey>)
+
+ + + +
+Implementation + + +
public(package) fun store_permission<PermKey: copy + drop + store>(
+    s: &signer, perm: Permission<PermKey>
+) acquires PermissionStorage {
+    assert!(
+        is_permissioned_signer(s),
+        error::permission_denied(ENOT_PERMISSIONED_SIGNER)
+    );
+    let Permission::V1 { key, perm, owner_address } = perm;
+
+    assert!(
+        signer::address_of(s) == owner_address,
+        error::permission_denied(E_PERMISSION_MISMATCH)
+    );
+
+    insert_or(
+        s,
+        key,
+        |stored_permission| {
+            merge(stored_permission, perm);
+        },
+        perm,
+    )
+}
+
+ + + +
+ + + +## Function `is_permissioned_signer` + + +Check whether this is a permissioned signer. + + +
public fun is_permissioned_signer(s: &signer): bool
+
+ + + +
+Implementation + + +
public native fun is_permissioned_signer(s: &signer): bool;
+
+ + + +
+ + + +## Function `permission_address` + +Return the address used for storing permissions. Aborts if not a permissioned signer. + + +
fun permission_address(permissioned: &signer): address
+
+ + + +
+Implementation + + +
native fun permission_address(permissioned: &signer): address;
+
+ + + +
+ + + +## Function `signer_from_permissioned_handle_impl` + +Creates a permissioned signer from an existing universal signer. The function aborts if the +given signer is already a permissioned signer. + +The implementation of this function requires to extend the value representation for signers in the VM. +invariants: +signer::address_of(master) == signer::address_of(signer_from_permissioned_handle(create_permissioned_handle(master))), + + +
fun signer_from_permissioned_handle_impl(master_account_addr: address, permissions_storage_addr: address): signer
+
+ + + +
+Implementation + + +
native fun signer_from_permissioned_handle_impl(
+    master_account_addr: address, permissions_storage_addr: address
+): signer;
+
+ + + +
+ + + +## Specification + + + +
axiom forall a: GrantedPermissionHandles:
+    (
+        forall i in 0..len(a.active_handles):
+            forall j in 0..len(a.active_handles):
+                i != j ==>
+                    a.active_handles[i] != a.active_handles[j]
+    );
+
+ + + + + + + +
fun spec_is_permissioned_signer(s: signer): bool;
+
+ + + + + +### Function `create_permissioned_handle` + + +
public fun create_permissioned_handle(master: &signer): permissioned_signer::PermissionedHandle
+
+ + + + +
pragma opaque;
+aborts_if [abstract] spec_is_permissioned_signer(master);
+let permissions_storage_addr = transaction_context::spec_generate_unique_address();
+modifies global<PermissionStorage>(permissions_storage_addr);
+let master_account_addr = signer::address_of(master);
+ensures result.master_account_addr == master_account_addr;
+ensures result.permissions_storage_addr == permissions_storage_addr;
+
+ + + + + +### Function `create_storable_permissioned_handle` + + +
public(friend) fun create_storable_permissioned_handle(master: &signer, expiration_time: u64): permissioned_signer::StorablePermissionedHandle
+
+ + + + +
pragma opaque;
+aborts_if [abstract] spec_is_permissioned_signer(master);
+let permissions_storage_addr = transaction_context::spec_generate_unique_address();
+modifies global<PermissionStorage>(permissions_storage_addr);
+let master_account_addr = signer::address_of(master);
+modifies global<GrantedPermissionHandles>(master_account_addr);
+ensures result.master_account_addr == master_account_addr;
+ensures result.permissions_storage_addr == permissions_storage_addr;
+ensures result.expiration_time == expiration_time;
+ensures vector::spec_contains(
+    global<GrantedPermissionHandles>(master_account_addr).active_handles,
+    permissions_storage_addr
+);
+ensures exists<GrantedPermissionHandles>(master_account_addr);
+
+ + + + + +### Function `destroy_permissioned_handle` + + +
public fun destroy_permissioned_handle(p: permissioned_signer::PermissionedHandle)
+
+ + + + +
ensures !exists<PermissionStorage>(p.permissions_storage_addr);
+
+ + + + + +### Function `destroy_storable_permissioned_handle` + + +
public(friend) fun destroy_storable_permissioned_handle(p: permissioned_signer::StorablePermissionedHandle)
+
+ + + + +
ensures !exists<PermissionStorage>(p.permissions_storage_addr);
+let post granted_permissions = global<GrantedPermissionHandles>(
+    p.master_account_addr
+);
+
+ + + + + +### Function `revoke_permission_storage_address` + + +
public entry fun revoke_permission_storage_address(s: &signer, permissions_storage_addr: address)
+
+ + + + + + +### Function `authorize` + + +
public fun authorize<PermKey: copy, drop, store>(master: &signer, permissioned: &signer, capacity: u256, perm: PermKey)
+
+ + + + +
pragma aborts_if_is_partial;
+aborts_if !spec_is_permissioned_signer(permissioned);
+aborts_if spec_is_permissioned_signer(master);
+aborts_if signer::address_of(permissioned) != signer::address_of(master);
+ensures exists<PermissionStorage>(
+    spec_permission_address(permissioned)
+);
+
+ + + + + +### Function `check_permission_exists` + + +
public fun check_permission_exists<PermKey: copy, drop, store>(s: &signer, perm: PermKey): bool
+
+ + + + +
pragma opaque;
+aborts_if false;
+ensures result == spec_check_permission_exists(s, perm);
+
+ + + + + + + +
fun spec_check_permission_exists<PermKey: copy + drop + store>(s: signer, perm: PermKey): bool {
+   use aptos_std::type_info;
+   use std::bcs;
+   let addr = spec_permission_address(s);
+   let key = Any {
+       type_name: type_info::type_name<PermKey>(),
+       data: bcs::serialize(perm)
+   };
+   if (!spec_is_permissioned_signer(s)) { true }
+   else if (!exists<PermissionStorage>(addr)) { false }
+   else {
+       simple_map::spec_contains_key(global<PermissionStorage>(addr).perms, key)
+   }
+}
+
+ + + + + +### Function `check_permission_capacity_above` + + +
public fun check_permission_capacity_above<PermKey: copy, drop, store>(s: &signer, threshold: u256, perm: PermKey): bool
+
+ + + + +
let permissioned_signer_addr = spec_permission_address(s);
+ensures !spec_is_permissioned_signer(s) ==> result == true;
+ensures (
+    spec_is_permissioned_signer(s)
+        && !exists<PermissionStorage>(permissioned_signer_addr)
+) ==> result == false;
+let key = Any {
+    type_name: type_info::type_name<SimpleMap<Any, u256>>(),
+    data: bcs::serialize(perm)
+};
+
+ + + + + +### Function `check_permission_consume` + + +
public fun check_permission_consume<PermKey: copy, drop, store>(s: &signer, threshold: u256, perm: PermKey): bool
+
+ + + + +
let permissioned_signer_addr = spec_permission_address(s);
+ensures !spec_is_permissioned_signer(s) ==> result == true;
+ensures (
+    spec_is_permissioned_signer(s)
+        && !exists<PermissionStorage>(permissioned_signer_addr)
+) ==> result == false;
+
+ + + + + +### Function `capacity` + + +
public fun capacity<PermKey: copy, drop, store>(s: &signer, perm: PermKey): option::Option<u256>
+
+ + + + + + +### Function `consume_permission` + + +
public(friend) fun consume_permission<PermKey: copy, drop, store>(perm: &mut permissioned_signer::Permission<PermKey>, weight: u256, perm_key: PermKey): bool
+
+ + + + + + +### Function `is_permissioned_signer` + + +
public fun is_permissioned_signer(s: &signer): bool
+
+ + + + +
pragma opaque;
+aborts_if [abstract] false;
+ensures [abstract] result == spec_is_permissioned_signer(s);
+
+ + + + + + + +
fun spec_permission_address(s: signer): address;
+
+ + + + + +### Function `permission_address` + + +
fun permission_address(permissioned: &signer): address
+
+ + + + +
pragma opaque;
+aborts_if [abstract]!spec_is_permissioned_signer(permissioned);
+ensures [abstract] result == spec_permission_address(permissioned);
+
+ + + + + + + +
fun spec_signer_from_permissioned_handle_impl(
+   master_account_addr: address, permissions_storage_addr: address
+): signer;
+
+ + + + + +### Function `signer_from_permissioned_handle_impl` + + +
fun signer_from_permissioned_handle_impl(master_account_addr: address, permissions_storage_addr: address): signer
+
+ + + + +
pragma opaque;
+ensures [abstract] result
+    == spec_signer_from_permissioned_handle_impl(
+        master_account_addr, permissions_storage_addr
+    );
+
+ + +[move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/aptos-framework/doc/randomness.md b/aptos-move/framework/aptos-framework/doc/randomness.md index fa210cfb1023a5..f822c004caaa76 100644 --- a/aptos-move/framework/aptos-framework/doc/randomness.md +++ b/aptos-move/framework/aptos-framework/doc/randomness.md @@ -37,7 +37,6 @@ Security holds under the same proof-of-stake assumption that secures the Aptos n - [Function `permutation`](#0x1_randomness_permutation) - [Function `safe_add_mod`](#0x1_randomness_safe_add_mod) - [Function `take_first`](#0x1_randomness_take_first) -- [Function `safe_add_mod_for_verification`](#0x1_randomness_safe_add_mod_for_verification) - [Function `fetch_and_increment_txn_counter`](#0x1_randomness_fetch_and_increment_txn_counter) - [Function `is_unbiasable`](#0x1_randomness_is_unbiasable) - [Specification](#@Specification_1) @@ -55,7 +54,6 @@ Security holds under the same proof-of-stake assumption that secures the Aptos n - [Function `u64_range`](#@Specification_1_u64_range) - [Function `u256_range`](#@Specification_1_u256_range) - [Function `permutation`](#@Specification_1_permutation) - - [Function `safe_add_mod_for_verification`](#@Specification_1_safe_add_mod_for_verification) - [Function `fetch_and_increment_txn_counter`](#@Specification_1_fetch_and_increment_txn_counter) - [Function `is_unbiasable`](#@Specification_1_is_unbiasable) @@ -924,36 +922,6 @@ Compute (a + b) % m, assuming m >= 1, 0 <= a < m, 0& - - - - -## Function `safe_add_mod_for_verification` - - - -
#[verify_only]
-fun safe_add_mod_for_verification(a: u256, b: u256, m: u256): u256
-
- - - -
-Implementation - - -
fun safe_add_mod_for_verification(a: u256, b: u256, m: u256): u256 {
-    let neg_b = m - b;
-    if (a < neg_b) {
-        a + b
-    } else {
-        a - neg_b
-    }
-}
-
- - -
@@ -1297,25 +1265,6 @@ function as its payload. - - -### Function `safe_add_mod_for_verification` - - -
#[verify_only]
-fun safe_add_mod_for_verification(a: u256, b: u256, m: u256): u256
-
- - - - -
aborts_if m < b;
-aborts_if a < m - b && a + b > MAX_U256;
-ensures result == spec_safe_add_mod(a, b, m);
-
- - - diff --git a/aptos-move/framework/aptos-framework/doc/version.md b/aptos-move/framework/aptos-framework/doc/version.md index 8505a6f3f18d2c..77881697ab612d 100644 --- a/aptos-move/framework/aptos-framework/doc/version.md +++ b/aptos-move/framework/aptos-framework/doc/version.md @@ -134,7 +134,7 @@ Publishes the Version config. system_addresses::assert_aptos_framework(aptos_framework); move_to(aptos_framework, Version { major: initial_version }); - // Give aptos framework account capability to call set version. This allows on chain governance to do it through + // Give aptos framework account capability to call set version. This allows on chain governance to do it through // control of the aptos framework account. move_to(aptos_framework, SetVersionCapability {}); } diff --git a/aptos-move/framework/aptos-stdlib/doc/big_vector.md b/aptos-move/framework/aptos-stdlib/doc/big_vector.md index 7d785a5b730a13..da978bc07ff9ec 100644 --- a/aptos-move/framework/aptos-stdlib/doc/big_vector.md +++ b/aptos-move/framework/aptos-stdlib/doc/big_vector.md @@ -502,7 +502,7 @@ Aborts if i is out of bounds. if (self.end_index == i) { return last_val }; - // because the lack of mem::swap, here we swap remove the requested value from the bucket + // because the lack of mem::swap, here we swap remove the requested value from the bucket // and append the last_val to the bucket then swap the last bucket val back let bucket = table_with_length::borrow_mut(&mut self.buckets, i / self.bucket_size); let bucket_len = vector::length(bucket); diff --git a/aptos-move/framework/aptos-stdlib/doc/type_info.md b/aptos-move/framework/aptos-stdlib/doc/type_info.md index 2e73ef96f80ab5..ea35286e1f1d6a 100644 --- a/aptos-move/framework/aptos-stdlib/doc/type_info.md +++ b/aptos-move/framework/aptos-stdlib/doc/type_info.md @@ -15,15 +15,12 @@ - [Function `type_name`](#0x1_type_info_type_name) - [Function `chain_id_internal`](#0x1_type_info_chain_id_internal) - [Function `size_of_val`](#0x1_type_info_size_of_val) -- [Function `verify_type_of`](#0x1_type_info_verify_type_of) -- [Function `verify_type_of_generic`](#0x1_type_info_verify_type_of_generic) - [Specification](#@Specification_1) - [Function `chain_id`](#@Specification_1_chain_id) - [Function `type_of`](#@Specification_1_type_of) - [Function `type_name`](#@Specification_1_type_name) - [Function `chain_id_internal`](#@Specification_1_chain_id_internal) - [Function `size_of_val`](#@Specification_1_size_of_val) - - [Function `verify_type_of_generic`](#@Specification_1_verify_type_of_generic)
use 0x1::bcs;
@@ -291,77 +288,20 @@ analysis of vector size dynamism.
 
 
 
-
-
-## Function `verify_type_of`
-
-
-
-
#[verify_only]
-fun verify_type_of()
-
- - - -
-Implementation - - -
fun verify_type_of() {
-    let type_info = type_of<TypeInfo>();
-    let account_address = account_address(&type_info);
-    let module_name = module_name(&type_info);
-    let struct_name = struct_name(&type_info);
-    spec {
-        assert account_address == @aptos_std;
-        assert module_name == b"type_info";
-        assert struct_name == b"TypeInfo";
-    };
-}
-
- - - -
- - - -## Function `verify_type_of_generic` - - + -
#[verify_only]
-fun verify_type_of_generic<T>()
-
+## Specification -
-Implementation + -
fun verify_type_of_generic<T>() {
-    let type_info = type_of<T>();
-    let account_address = account_address(&type_info);
-    let module_name = module_name(&type_info);
-    let struct_name = struct_name(&type_info);
-    spec {
-        assert account_address == type_of<T>().account_address;
-        assert module_name == type_of<T>().module_name;
-        assert struct_name == type_of<T>().struct_name;
-    };
-}
+
native fun spec_is_struct<T>(): bool;
 
-
- - - -## Specification - - ### Function `chain_id` @@ -454,30 +394,4 @@ analysis of vector size dynamism.
- - - -### Function `verify_type_of_generic` - - -
#[verify_only]
-fun verify_type_of_generic<T>()
-
- - - - -
aborts_if !spec_is_struct<T>();
-
- - - - - - - -
native fun spec_is_struct<T>(): bool;
-
- - [move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/move-stdlib/doc/bit_vector.md b/aptos-move/framework/move-stdlib/doc/bit_vector.md index baeb685729360a..78fef563ffebc5 100644 --- a/aptos-move/framework/move-stdlib/doc/bit_vector.md +++ b/aptos-move/framework/move-stdlib/doc/bit_vector.md @@ -14,7 +14,6 @@ - [Function `is_index_set`](#0x1_bit_vector_is_index_set) - [Function `length`](#0x1_bit_vector_length) - [Function `longest_set_sequence_starting_at`](#0x1_bit_vector_longest_set_sequence_starting_at) -- [Function `shift_left_for_verification_only`](#0x1_bit_vector_shift_left_for_verification_only) - [Specification](#@Specification_1) - [Struct `BitVector`](#@Specification_1_BitVector) - [Function `new`](#@Specification_1_new) @@ -23,7 +22,6 @@ - [Function `shift_left`](#@Specification_1_shift_left) - [Function `is_index_set`](#@Specification_1_is_index_set) - [Function `longest_set_sequence_starting_at`](#@Specification_1_longest_set_sequence_starting_at) - - [Function `shift_left_for_verification_only`](#@Specification_1_shift_left_for_verification_only)
@@ -345,78 +343,6 @@ sequence, then 0 is returned. - - - - -## Function `shift_left_for_verification_only` - - - -
#[verify_only]
-public fun shift_left_for_verification_only(self: &mut bit_vector::BitVector, amount: u64)
-
- - - -
-Implementation - - -
public fun shift_left_for_verification_only(self: &mut BitVector, amount: u64) {
-    if (amount >= self.length) {
-        let len = vector::length(&self.bit_field);
-        let i = 0;
-        while ({
-            spec {
-                invariant len == self.length;
-                invariant forall k in 0..i: !self.bit_field[k];
-                invariant forall k in i..self.length: self.bit_field[k] == old(self).bit_field[k];
-            };
-            i < len
-        }) {
-            let elem = vector::borrow_mut(&mut self.bit_field, i);
-            *elem = false;
-            i = i + 1;
-        };
-    } else {
-        let i = amount;
-
-        while ({
-            spec {
-                invariant i >= amount;
-                invariant self.length == old(self).length;
-                invariant forall j in amount..i: old(self).bit_field[j] == self.bit_field[j - amount];
-                invariant forall j in (i-amount)..self.length : old(self).bit_field[j] == self.bit_field[j];
-                invariant forall k in 0..i-amount: self.bit_field[k] == old(self).bit_field[k + amount];
-            };
-            i < self.length
-        }) {
-            if (is_index_set(self, i)) set(self, i - amount)
-            else unset(self, i - amount);
-            i = i + 1;
-        };
-
-
-        i = self.length - amount;
-
-        while ({
-            spec {
-                invariant forall j in self.length - amount..i: !self.bit_field[j];
-                invariant forall k in 0..self.length - amount: self.bit_field[k] == old(self).bit_field[k + amount];
-                invariant i >= self.length - amount;
-            };
-            i < self.length
-        }) {
-            unset(self, i);
-            i = i + 1;
-        }
-    }
-}
-
- - -
@@ -624,26 +550,4 @@ sequence, then 0 is returned.
- - - -### Function `shift_left_for_verification_only` - - -
#[verify_only]
-public fun shift_left_for_verification_only(self: &mut bit_vector::BitVector, amount: u64)
-
- - - - -
aborts_if false;
-ensures amount >= self.length ==> (forall k in 0..self.length: !self.bit_field[k]);
-ensures amount < self.length ==>
-    (forall i in self.length - amount..self.length: !self.bit_field[i]);
-ensures amount < self.length ==>
-    (forall i in 0..self.length - amount: self.bit_field[i] == old(self).bit_field[i + amount]);
-
- - [move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/move-stdlib/doc/features.md b/aptos-move/framework/move-stdlib/doc/features.md index 3919625f4ff9cb..6bfd2a4d4554ad 100644 --- a/aptos-move/framework/move-stdlib/doc/features.md +++ b/aptos-move/framework/move-stdlib/doc/features.md @@ -142,7 +142,6 @@ return true. - [Function `contains`](#0x1_features_contains) - [Function `apply_diff`](#0x1_features_apply_diff) - [Function `ensure_framework_signer`](#0x1_features_ensure_framework_signer) -- [Function `change_feature_flags_for_verification`](#0x1_features_change_feature_flags_for_verification) - [Specification](#@Specification_1) - [Resource `Features`](#@Specification_1_Features) - [Resource `PendingFeatures`](#@Specification_1_PendingFeatures) @@ -3562,35 +3561,6 @@ Helper to check whether a feature flag is enabled. - - - - -## Function `change_feature_flags_for_verification` - - - -
#[verify_only]
-public fun change_feature_flags_for_verification(framework: &signer, enable: vector<u64>, disable: vector<u64>)
-
- - - -
-Implementation - - -
public fun change_feature_flags_for_verification(
-    framework: &signer,
-    enable: vector<u64>,
-    disable: vector<u64>
-) acquires Features {
-    change_feature_flags_internal(framework, enable, disable)
-}
-
- - -
diff --git a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs index 661c782d8aac84..c6f7d718394159 100644 --- a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs +++ b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs @@ -445,7 +445,12 @@ impl<'env> StructTranslator<'env> { "", // not inlined! &format!("$IsValid'{}'(s: {}): bool", suffix_variant, struct_name), || { - if struct_env.is_intrinsic() || struct_env.get_field_count() == 0 { + if struct_env.is_intrinsic() + || struct_env + .get_fields_of_variant(variant) + .collect_vec() + .is_empty() + { emitln!(writer, "true") } else { let mut sep = ""; diff --git a/third_party/move/move-prover/tests/sources/functional/enum.exp b/third_party/move/move-prover/tests/sources/functional/enum.exp index 914ff680e45c20..a4b90881bf5027 100644 --- a/third_party/move/move-prover/tests/sources/functional/enum.exp +++ b/third_party/move/move-prover/tests/sources/functional/enum.exp @@ -2,23 +2,29 @@ Move prover returns: exiting with model building errors error: unsupported language construct ┌─ tests/sources/functional/enum.move:3:5 │ -3 │ enum CommonFields has copy, drop { +3 │ enum TestNoField has copy, drop { │ ^^^^ Move 2 language construct is not enabled: enum types error: unsupported language construct - ┌─ tests/sources/functional/enum.move:10:25 + ┌─ tests/sources/functional/enum.move:11:5 │ -10 │ invariant (self is CommonFields::Bar) ==> self.z > 10; +11 │ enum CommonFields has copy, drop { + │ ^^^^ Move 2 language construct is not enabled: enum types + +error: unsupported language construct + ┌─ tests/sources/functional/enum.move:18:25 + │ +18 │ invariant (self is CommonFields::Bar) ==> self.z > 10; │ ^^ Move 2 language construct is not enabled: `is` expression error: unsupported language construct - ┌─ tests/sources/functional/enum.move:39:9 + ┌─ tests/sources/functional/enum.move:47:9 │ -39 │ match (&common) { +47 │ match (&common) { │ ^^^^^ Move 2 language construct is not enabled: match expression error: unsupported language construct - ┌─ tests/sources/functional/enum.move:49:5 + ┌─ tests/sources/functional/enum.move:57:5 │ -49 │ enum CommonFieldsVector has drop { +57 │ enum CommonFieldsVector has drop { │ ^^^^ Move 2 language construct is not enabled: enum types diff --git a/third_party/move/move-prover/tests/sources/functional/enum.move b/third_party/move/move-prover/tests/sources/functional/enum.move index 9ac6876a401862..89d005e08f2a33 100644 --- a/third_party/move/move-prover/tests/sources/functional/enum.move +++ b/third_party/move/move-prover/tests/sources/functional/enum.move @@ -1,5 +1,13 @@ module 0x815::m { + enum TestNoField has copy, drop { + NoField + } + + fun test_no_field(): TestNoField { + TestNoField::NoField + } + enum CommonFields has copy, drop { Foo{x: u64, y: u8}, Bar{x: u64, y: u8, z: u32} diff --git a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp index a4c03bfa8340fb..9a4eed455c87bf 100644 --- a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp @@ -1,63 +1,63 @@ Move prover returns: exiting with verification errors error: data invariant does not hold - ┌─ tests/sources/functional/enum.move:9:9 - │ -9 │ invariant self.x > 20; - │ ^^^^^^^^^^^^^^^^^^^^^^ - │ - = at tests/sources/functional/enum.move:15: t9_common_field - = at tests/sources/functional/enum.move:16: t9_common_field - = at tests/sources/functional/enum.move:17: t9_common_field - = at tests/sources/functional/enum.move:14: t9_common_field - = at tests/sources/functional/enum.move:9 - = at tests/sources/functional/enum.move:10 - = at tests/sources/functional/enum.move:14: t9_common_field - = common = - = at tests/sources/functional/enum.move:19: t9_common_field - = at tests/sources/functional/enum.move:9 + ┌─ tests/sources/functional/enum.move:17:9 + │ +17 │ invariant self.x > 20; + │ ^^^^^^^^^^^^^^^^^^^^^^ + │ + = at tests/sources/functional/enum.move:23: t9_common_field + = at tests/sources/functional/enum.move:24: t9_common_field + = at tests/sources/functional/enum.move:25: t9_common_field + = at tests/sources/functional/enum.move:22: t9_common_field + = at tests/sources/functional/enum.move:17 + = at tests/sources/functional/enum.move:18 + = at tests/sources/functional/enum.move:22: t9_common_field + = common = + = at tests/sources/functional/enum.move:27: t9_common_field + = at tests/sources/functional/enum.move:17 error: data invariant does not hold - ┌─ tests/sources/functional/enum.move:10:9 + ┌─ tests/sources/functional/enum.move:18:9 │ -10 │ invariant (self is CommonFields::Bar) ==> self.z > 10; +18 │ invariant (self is CommonFields::Bar) ==> self.z > 10; │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ - = at tests/sources/functional/enum.move:25: test_data_invariant - = at tests/sources/functional/enum.move:26: test_data_invariant - = at tests/sources/functional/enum.move:27: test_data_invariant - = at tests/sources/functional/enum.move:24: test_data_invariant - = at tests/sources/functional/enum.move:9 - = at tests/sources/functional/enum.move:10 - = at tests/sources/functional/enum.move:24: test_data_invariant + = at tests/sources/functional/enum.move:33: test_data_invariant + = at tests/sources/functional/enum.move:34: test_data_invariant + = at tests/sources/functional/enum.move:35: test_data_invariant + = at tests/sources/functional/enum.move:32: test_data_invariant + = at tests/sources/functional/enum.move:17 + = at tests/sources/functional/enum.move:18 + = at tests/sources/functional/enum.move:32: test_data_invariant = common = - = at tests/sources/functional/enum.move:29: test_data_invariant + = at tests/sources/functional/enum.move:37: test_data_invariant = = = z = - = at tests/sources/functional/enum.move:30: test_data_invariant - = at tests/sources/functional/enum.move:9 - = at tests/sources/functional/enum.move:10 + = at tests/sources/functional/enum.move:38: test_data_invariant + = at tests/sources/functional/enum.move:17 + = at tests/sources/functional/enum.move:18 error: unknown assertion failed - ┌─ tests/sources/functional/enum.move:68:13 + ┌─ tests/sources/functional/enum.move:76:13 │ -68 │ assert _common_vector_1.x != _common_vector_2.x; // this fails +76 │ assert _common_vector_1.x != _common_vector_2.x; // this fails │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ - = at tests/sources/functional/enum.move:56: test_enum_vector - = at tests/sources/functional/enum.move:55: test_enum_vector - = _common_vector_1 = - = at tests/sources/functional/enum.move:59: test_enum_vector - = at tests/sources/functional/enum.move:60: test_enum_vector - = at tests/sources/functional/enum.move:61: test_enum_vector - = at tests/sources/functional/enum.move:58: test_enum_vector - = at tests/sources/functional/enum.move:9 - = at tests/sources/functional/enum.move:10 - = at tests/sources/functional/enum.move:58: test_enum_vector - = _common_fields = = at tests/sources/functional/enum.move:64: test_enum_vector - = at tests/sources/functional/enum.move:65: test_enum_vector - = at tests/sources/functional/enum.move:9 - = at tests/sources/functional/enum.move:65: test_enum_vector = at tests/sources/functional/enum.move:63: test_enum_vector - = _common_vector_2 = + = _common_vector_1 = + = at tests/sources/functional/enum.move:67: test_enum_vector = at tests/sources/functional/enum.move:68: test_enum_vector + = at tests/sources/functional/enum.move:69: test_enum_vector + = at tests/sources/functional/enum.move:66: test_enum_vector + = at tests/sources/functional/enum.move:17 + = at tests/sources/functional/enum.move:18 + = at tests/sources/functional/enum.move:66: test_enum_vector + = _common_fields = + = at tests/sources/functional/enum.move:72: test_enum_vector + = at tests/sources/functional/enum.move:73: test_enum_vector + = at tests/sources/functional/enum.move:17 + = at tests/sources/functional/enum.move:73: test_enum_vector + = at tests/sources/functional/enum.move:71: test_enum_vector + = _common_vector_2 = + = at tests/sources/functional/enum.move:76: test_enum_vector