diff --git a/aptos-move/framework/aptos-framework/doc/account.md b/aptos-move/framework/aptos-framework/doc/account.md index 383d4918dd700..9566844a0f739 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 a5073c231961b..227aaf4e82b41 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 c90cc82da7e23..a016def9bf443 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 268d0618fb722..dc982b152e0d7 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 4df4a2f99b301..c00fc63568ee4 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 4117c18c99106..0b6aa0e44dd7a 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/randomness.md b/aptos-move/framework/aptos-framework/doc/randomness.md
index fa210cfb1023a..f822c004caaa7 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 8505a6f3f18d2..77881697ab612 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/type_info.md b/aptos-move/framework/aptos-stdlib/doc/type_info.md
index 2e73ef96f80ab..ea35286e1f1d6 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 baeb685729360..78fef563ffebc 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 e5604063b6071..f812bbbec7e9d 100644
--- a/aptos-move/framework/move-stdlib/doc/features.md
+++ b/aptos-move/framework/move-stdlib/doc/features.md
@@ -144,7 +144,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)
@@ -3619,35 +3618,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/aptos-move/framework/src/aptos.rs b/aptos-move/framework/src/aptos.rs
index 6717a00135be4..9e030e69b30bf 100644
--- a/aptos-move/framework/src/aptos.rs
+++ b/aptos-move/framework/src/aptos.rs
@@ -113,7 +113,7 @@ impl ReleaseTarget {
                     output_format: None,
                 }),
                 skip_fetch_latest_git_deps: true,
-                ..BuildOptions::default()
+                ..BuildOptions::move_2()
             },
             packages: packages.iter().map(|(path, _)| path.to_owned()).collect(),
             rust_bindings: packages