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/create_signer.md b/aptos-move/framework/aptos-framework/doc/create_signer.md
index 5c15eb6bec51fd..a66df38b9c601e 100644
--- a/aptos-move/framework/aptos-framework/doc/create_signer.md
+++ b/aptos-move/framework/aptos-framework/doc/create_signer.md
@@ -127,16 +127,6 @@ Convert address to singer and return.
 
pragma opaque;
 aborts_if [abstract] false;
 ensures [abstract] signer::address_of(result) == addr;
-ensures [abstract] result == spec_create_signer(addr);
-

-
-
-
-
-
-
-
-
fun spec_create_signer(addr: address): signer;
 

 
 
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
index 801de443139aaf..36c930a7430824 100644
--- a/aptos-move/framework/aptos-framework/doc/permissioned_signer.md
+++ b/aptos-move/framework/aptos-framework/doc/permissioned_signer.md
@@ -38,14 +38,21 @@ for blind signing.
 -  [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 `get_key`](#0x1_permissioned_signer_get_key)
+-  [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)
@@ -250,7 +257,7 @@ for blind signing.
 
 
 
-
enum StoredPermission has drop, store
+
enum StoredPermission has copy, drop, store
 

 
 
@@ -315,7 +322,7 @@ for blind signing.
 
 
 

-Capacity
+V1
 
 
 

@@ -336,7 +343,7 @@ for blind signing.
 
 
 

-capacity: u256
+perm: permissioned_signer::StoredPermission
 

 

 
@@ -489,7 +496,9 @@ the current transaction.
 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(friend) for now.
+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
@@ -501,7 +510,7 @@ This is as dangerous as key delegation, thus it remains public(friend) for now.
 Implementation
 
 
-
public(friend) fun create_storable_permissioned_handle(
+
public(package) fun create_storable_permissioned_handle(
     master: &signer, expiration_time: u64
 ): StorablePermissionedHandle acquires GrantedPermissionHandles {
     assert_master_signer(master);
@@ -584,7 +593,7 @@ Destroys a storable permission handle. Clean up the permission stored in that ha
 Implementation
 
 
-
public(friend) fun destroy_storable_permissioned_handle(
+
public(package) fun destroy_storable_permissioned_handle(
     p: StorablePermissionedHandle
 ) acquires PermissionStorage, GrantedPermissionHandles {
     let StorablePermissionedHandle::V1 {
@@ -697,7 +706,7 @@ Generate the permissioned signer based on the storable permission handle.
 Implementation
 
 
-
public(friend) fun signer_from_storable_permissioned_handle(
+
public(package) fun signer_from_storable_permissioned_handle(
     p: &StorablePermissionedHandle
 ): signer {
     assert!(
@@ -809,7 +818,7 @@ Revoke all storable permission handle of the signer immediately.
 
 ## Function `permissions_storage_address`
 
-Return the permission handle address so that it could be used for revokation purpose.
+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
@@ -821,7 +830,7 @@ Return the permission handle address so that it could be used for revokation pur
 Implementation
 
 
-
public(friend) fun permissions_storage_address(
+
public(package) fun permissions_storage_address(
     p: &StorablePermissionedHandle
 ): address {
     p.permissions_storage_addr
@@ -859,9 +868,138 @@ Helper function that would abort if the signer passed in is a permissioned signe
 
 

 
-
+
 
-## Function `authorize`
+## 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
@@ -870,6 +1008,88 @@ Authorizes permissioned with the given permission. This requires to
 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)
 

 
@@ -891,21 +1111,57 @@ signer.
             && signer::address_of(master) == signer::address_of(permissioned),
         error::permission_denied(ECANNOT_AUTHORIZE)
     );
-    let permission_signer_addr = permission_address(permissioned);
-    let perms =
-        &mut borrow_global_mut<PermissionStorage>(permission_signer_addr).perms;
-    let key = copyable_any::pack(perm);
-    if (simple_map::contains_key(perms, &key)) {
-        let entry = simple_map::borrow_mut(perms, &key);
-        match (entry) {
-            StoredPermission::Capacity(current_capacity) => {
-                *current_capacity = *current_capacity + capacity;
-            }
-            StoredPermission::Unlimited => (),
-        }
-    } else {
-        simple_map::add(perms, key, StoredPermission::Capacity(capacity));
-    }
+    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,
+    )
 }
 

 
@@ -931,18 +1187,7 @@ signer.
 
public fun check_permission_exists<PermKey: copy + drop + store>(
     s: &signer, perm: PermKey
 ): bool acquires PermissionStorage {
-    if (!is_permissioned_signer(s)) {
-        // master signer has all permissions
-        return true
-    };
-    let addr = permission_address(s);
-    if (!exists<PermissionStorage>(addr)) {
-        return false
-    };
-    simple_map::contains_key(
-        &borrow_global<PermissionStorage>(addr).perms,
-        &copyable_any::pack(perm)
-    )
+    check_permission_capacity_above(s, 0, perm)
 }
 

 
@@ -972,20 +1217,14 @@ signer.
         // master signer has all permissions
         return true
     };
-    let addr = permission_address(s);
-    if (!exists<PermissionStorage>(addr)) {
-        return false
-    };
-    let key = copyable_any::pack(perm);
-    let storage = &borrow_global<PermissionStorage>(addr).perms;
-    if (!simple_map::contains_key(storage, &key)) {
-        return false
-    };
-    let perm = simple_map::borrow(storage, &key);
-    match (perm) {
-        StoredPermission::Capacity(capacity) => *capacity > threshold,
-        StoredPermission::Unlimited => true
-    }
+    map_or(
+        s,
+        perm,
+        |stored_permission| {
+            is_above(stored_permission, threshold)
+        },
+        false,
+    )
 }
 

 
@@ -1015,25 +1254,14 @@ signer.
         // master signer has all permissions
         return true
     };
-    let addr = permission_address(s);
-    if (!exists<PermissionStorage>(addr)) {
-        return false
-    };
-    let key = copyable_any::pack(perm);
-    let storage = &mut borrow_global_mut<PermissionStorage>(addr).perms;
-    if (!simple_map::contains_key(storage, &key)) {
-        return false
-    };
-    let perm = simple_map::borrow_mut(storage, &key);
-    match (perm) {
-        StoredPermission::Capacity(current_capacity) => {
-            if (*current_capacity >= threshold) {
-                *current_capacity = *current_capacity - threshold;
-                true
-            } else { false }
-        }
-        StoredPermission::Unlimited => true
-    }
+    map_or(
+        s,
+        perm,
+        |stored_permission| {
+             consume_capacity(stored_permission, threshold)
+        },
+        false,
+    )
 }
 

 
@@ -1062,21 +1290,17 @@ signer.
     if (!is_permissioned_signer(s)) {
         return option::some(U256_MAX)
     };
-    let addr = permission_address(s);
-    if (!exists<PermissionStorage>(addr)) {
-        return option::none()
-    };
-    let perm_storage = &borrow_global<PermissionStorage>(addr).perms;
-    let key = copyable_any::pack(perm);
-    if (simple_map::contains_key(perm_storage, &key)) {
-        let perm = simple_map::borrow(perm_storage, &key);
-        option::some(match (perm) {
-            StoredPermission::Capacity(capacity) => *capacity,
-            StoredPermission::Unlimited => U256_MAX,
-        })
-    } else {
-        option::none()
-    }
+    map_or(
+        s,
+        perm,
+        |stored_permission: &mut StoredPermission| {
+            option::some(match (stored_permission) {
+                StoredPermission::Capacity(capacity) => *capacity,
+                StoredPermission::Unlimited => U256_MAX,
+            })
+        },
+        option::none(),
+    )
 }
 

 
@@ -1127,10 +1351,11 @@ signer.
 
 ## Function `extract_permission`
 
+=====================================================================================================
 Another flavor of api to extract and store permissions
 
 
-
public fun extract_permission<PermKey: copy, drop, store>(s: &signer, weight: u256, perm: PermKey): permissioned_signer::Permission<PermKey>
+
public(friend) fun extract_permission<PermKey: copy, drop, store>(s: &signer, weight: u256, perm: PermKey): permissioned_signer::Permission<PermKey>
 

 
 
@@ -1139,17 +1364,17 @@ Another flavor of api to extract and store permissions
 Implementation
 
 
-
public fun extract_permission<PermKey: copy + drop + store>(
+
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::Capacity {
+    Permission::V1 {
         owner_address: signer::address_of(s),
         key: perm,
-        capacity: weight
+        perm: StoredPermission::Capacity(weight),
     }
 }
 

@@ -1158,13 +1383,13 @@ Another flavor of api to extract and store permissions
 
 
 
-
+
 
-## Function `get_key`
+## Function `extract_all_permission`
 
 
 
-
public fun get_key<PermKey>(perm: &permissioned_signer::Permission<PermKey>): &PermKey
+
public(friend) fun extract_all_permission<PermKey: copy, drop, store>(s: &signer, perm_key: PermKey): permissioned_signer::Permission<PermKey>
 

 
 
@@ -1173,8 +1398,27 @@ Another flavor of api to extract and store permissions
 Implementation
 
 
-
public fun get_key<PermKey>(perm: &Permission<PermKey>): &PermKey {
-    &perm.key
+
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,
+    }
 }
 

 
@@ -1188,7 +1432,7 @@ Another flavor of api to extract and store permissions
 
 
 
-
public fun address_of<PermKey>(perm: &permissioned_signer::Permission<PermKey>): address
+
public(friend) fun address_of<PermKey>(perm: &permissioned_signer::Permission<PermKey>): address
 

 
 
@@ -1197,7 +1441,7 @@ Another flavor of api to extract and store permissions
 Implementation
 
 
-
public fun address_of<PermKey>(perm: &Permission<PermKey>): address {
+
public(package) fun address_of<PermKey>(perm: &Permission<PermKey>): address {
     perm.owner_address
 }
 

@@ -1212,7 +1456,7 @@ Another flavor of api to extract and store permissions
 
 
 
-
public fun consume_permission<PermKey: copy, drop, store>(perm: &mut permissioned_signer::Permission<PermKey>, weight: u256, perm_key: PermKey): bool
+
public(friend) fun consume_permission<PermKey: copy, drop, store>(perm: &mut permissioned_signer::Permission<PermKey>, weight: u256, perm_key: PermKey): bool
 

 
 
@@ -1221,18 +1465,13 @@ Another flavor of api to extract and store permissions
 Implementation
 
 
-
public fun consume_permission<PermKey: copy + drop + store>(
+
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
     };
-    if (perm.capacity >= weight) {
-        perm.capacity = perm.capacity - weight;
-        return true
-    } else {
-        return false
-    }
+    consume_capacity(&mut perm.perm, weight)
 }
 

 
@@ -1246,7 +1485,7 @@ Another flavor of api to extract and store permissions
 
 
 
-
public fun store_permission<PermKey: copy, drop, store>(s: &signer, perm: permissioned_signer::Permission<PermKey>)
+
public(friend) fun store_permission<PermKey: copy, drop, store>(s: &signer, perm: permissioned_signer::Permission<PermKey>)
 

 
 
@@ -1255,40 +1494,28 @@ Another flavor of api to extract and store permissions
 Implementation
 
 
-
public fun store_permission<PermKey: copy + drop + store>(
+
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::Capacity { key, capacity, owner_address } = perm;
+    let Permission::V1 { key, perm, owner_address } = perm;
 
     assert!(
         signer::address_of(s) == owner_address,
         error::permission_denied(E_PERMISSION_MISMATCH)
     );
 
-    let permission_signer_addr = permission_address(s);
-
-    if (!exists<PermissionStorage>(permission_signer_addr)) {
-        let signer = create_signer(permission_signer_addr);
-        move_to(&signer, PermissionStorage::V1 { perms: simple_map::new() });
-    };
-    let perms =
-        &mut borrow_global_mut<PermissionStorage>(permission_signer_addr).perms;
-    let key = copyable_any::pack(key);
-    if (simple_map::contains_key(perms, &key)) {
-        let entry = simple_map::borrow_mut(perms, &key);
-        match (entry) {
-            StoredPermission::Capacity(current_capacity) => {
-                *current_capacity = *current_capacity + capacity;
-            }
-            StoredPermission::Unlimited => (),
-        }
-    } else {
-        simple_map::add(perms, key, StoredPermission::Capacity(capacity))
-    }
+    insert_or(
+        s,
+        key,
+        |stored_permission| {
+            merge(stored_permission, perm);
+        },
+        perm,
+    )
 }
 

 
@@ -1300,10 +1527,6 @@ Another flavor of api to extract and store permissions
 
 ## Function `is_permissioned_signer`
 
-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.
 
 Check whether this is a permissioned signer.
 
@@ -1351,7 +1574,10 @@ Return the address used for storing permissions. Aborts if not a permissioned si
 
 ## 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))),
 
@@ -1621,22 +1847,12 @@ signer::address_of(master) == signer::address_of(signer_from_permissioned_handle
 ### Function `consume_permission`
 
 
-
public fun consume_permission<PermKey: copy, drop, store>(perm: &mut permissioned_signer::Permission<PermKey>, weight: u256, perm_key: PermKey): bool
+
public(friend) fun consume_permission<PermKey: copy, drop, store>(perm: &mut permissioned_signer::Permission<PermKey>, weight: u256, perm_key: PermKey): bool
 

 
 
 
 
-
ensures perm.key != perm_key ==> result == false;
-ensures perm.key == perm_key && old(perm.capacity) < weight ==> result == false;
-ensures perm.key == perm_key
-    && perm.capacity >= weight ==>
-    (perm.capacity == old(perm.capacity) - weight
-        && result == true);
-

-
-
-
 
 
 ### Function `is_permissioned_signer`
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 737366c5714f8d..d781cb2bf9cd85 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,62 +1,62 @@
 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:9
-   =     at tests/sources/functional/enum.move:10
+   =     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
diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp
index 32b6d76bc6da8b..828edd8c598d7d 100644
--- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp
+++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp
@@ -45,8 +45,8 @@ error: induction case of the loop invariant does not hold
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = 
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         a = 
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = 
    =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2
@@ -105,7 +105,6 @@ error: unknown assertion failed
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = 
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         a = 
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = 
diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
index 3738bf28760678..27ff0c5bf280b9 100644
--- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
@@ -40,8 +40,6 @@ error: induction case of the loop invariant does not hold
    =         y = 
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
-   =         a = 
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = 
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =          = 
@@ -98,6 +96,7 @@ error: unknown assertion failed
    =         y = 
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         a = 
    =         b = 
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =          =