From 7a76b55b05bfc06a48c3e64761d42e820ac7eb98 Mon Sep 17 00:00:00 2001 From: "Xudong (Don) Wang" Date: Wed, 14 Jun 2023 22:08:16 +1000 Subject: [PATCH] [Spec] update specs of voting, transaction_fee, code (#8172) * [spec] update specs of voting, transaction_fee, code * [spec] add account and voting module * run linter * [spec] Fix timeout of smart_vector.move * [spec] Update docs of smart_vector --------- Co-authored-by: zorrot --- .../framework/aptos-framework/doc/account.md | 23 +- .../framework/aptos-framework/doc/code.md | 20 ++ .../framework/aptos-framework/doc/stake.md | 250 ++++++++++-------- .../aptos-framework/doc/transaction_fee.md | 19 +- .../framework/aptos-framework/doc/voting.md | 27 +- .../aptos-framework/sources/account.spec.move | 42 ++- .../aptos-framework/sources/code.spec.move | 7 + .../aptos-framework/sources/stake.spec.move | 7 + .../sources/transaction_fee.spec.move | 36 ++- .../aptos-framework/sources/voting.spec.move | 25 +- .../framework/aptos-stdlib/doc/from_bcs.md | 4 + .../aptos-stdlib/doc/smart_vector.md | 17 ++ .../data_structures/smart_vector.spec.move | 4 + .../aptos-stdlib/sources/from_bcs.spec.move | 7 + 14 files changed, 344 insertions(+), 144 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/account.md b/aptos-move/framework/aptos-framework/doc/account.md index 7c64b4cf70f47..fb6fc9b70a4d2 100644 --- a/aptos-move/framework/aptos-framework/doc/account.md +++ b/aptos-move/framework/aptos-framework/doc/account.md @@ -2224,9 +2224,16 @@ The authentication scheme is ED25519_SCHEME and MULTI_ED25519_SCHEME signature: cap_update_table, challenge: challenge, }; -pragma aborts_if_is_partial; -modifies global<Account>(addr); -modifies global<OriginatingAddress>(@aptos_framework); +let originating_addr = addr; +let new_auth_key_vector = spec_assert_valid_rotation_proof_signature_and_get_auth_key(to_scheme, to_public_key_bytes, cap_update_table, challenge); +let address_map = global<OriginatingAddress>(@aptos_framework).address_map; +let new_auth_key = from_bcs::deserialize<address>(new_auth_key_vector); +aborts_if !exists<OriginatingAddress>(@aptos_framework); +aborts_if !from_bcs::deserializable<address>(account_resource.authentication_key); +aborts_if table::spec_contains(address_map, curr_auth_key) && + table::spec_get(address_map, curr_auth_key) != originating_addr; +aborts_if !from_bcs::deserializable<address>(new_auth_key_vector); +aborts_if curr_auth_key != new_auth_key && table::spec_contains(address_map, new_auth_key); @@ -2261,7 +2268,15 @@ The authentication scheme is ED25519_SCHEME and MULTI_ED25519_SCHEME signature: cap_update_table, challenge: challenge, }; -pragma aborts_if_is_partial; +let new_auth_key_vector = spec_assert_valid_rotation_proof_signature_and_get_auth_key(new_scheme, new_public_key_bytes, cap_update_table, challenge); +let address_map = global<OriginatingAddress>(@aptos_framework).address_map; +aborts_if !exists<OriginatingAddress>(@aptos_framework); +aborts_if !from_bcs::deserializable<address>(offerer_account_resource.authentication_key); +aborts_if table::spec_contains(address_map, curr_auth_key) && + table::spec_get(address_map, curr_auth_key) != rotation_cap_offerer_address; +aborts_if !from_bcs::deserializable<address>(new_auth_key_vector); +let new_auth_key = from_bcs::deserialize<address>(new_auth_key_vector); +aborts_if curr_auth_key != new_auth_key && table::spec_contains(address_map, new_auth_key); diff --git a/aptos-move/framework/aptos-framework/doc/code.md b/aptos-move/framework/aptos-framework/doc/code.md index 3e2f788a8ae8d..e849ecef6b9ff 100644 --- a/aptos-move/framework/aptos-framework/doc/code.md +++ b/aptos-move/framework/aptos-framework/doc/code.md @@ -34,6 +34,7 @@ This module supports functionality related to code management. - [Function `check_upgradability`](#@Specification_1_check_upgradability) - [Function `check_coexistence`](#@Specification_1_check_coexistence) - [Function `check_dependencies`](#@Specification_1_check_dependencies) + - [Function `get_module_names`](#@Specification_1_get_module_names) - [Function `request_publish`](#@Specification_1_request_publish) - [Function `request_publish_with_allowed_deps`](#@Specification_1_request_publish_with_allowed_deps) @@ -986,6 +987,25 @@ Native function to initiate module loading, including a list of allowed dependen + + +### Function `get_module_names` + + +
fun get_module_names(pack: &code::PackageMetadata): vector<string::String>
+
+ + + + +
pragma opaque;
+aborts_if [abstract] false;
+ensures [abstract] len(result) == len(pack.modules);
+ensures [abstract] forall i in 0..len(result): result[i] == pack.modules[i].name;
+
+ + + ### Function `request_publish` diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md index de7e8ad6ec8ef..e838e2f4d9a33 100644 --- a/aptos-move/framework/aptos-framework/doc/stake.md +++ b/aptos-move/framework/aptos-framework/doc/stake.md @@ -105,6 +105,7 @@ or if their stake drops below the min required, they would get removed at the en - [Function `is_allowed`](#0x1_stake_is_allowed) - [Function `assert_owner_cap_exists`](#0x1_stake_assert_owner_cap_exists) - [Specification](#@Specification_1) + - [Function `initialize_validator_fees`](#@Specification_1_initialize_validator_fees) - [Function `add_transaction_fee`](#@Specification_1_add_transaction_fee) - [Function `get_validator_state`](#@Specification_1_get_validator_state) - [Function `initialize`](#@Specification_1_initialize) @@ -3539,6 +3540,140 @@ Returns validator's next epoch voting power, including pending_active, active, a + + + + +
fun spec_validators_are_initialized(validators: vector<ValidatorInfo>): bool {
+   forall i in 0..len(validators):
+       spec_has_stake_pool(validators[i].addr) &&
+           spec_has_validator_config(validators[i].addr)
+}
+
+ + + + + + + +
fun spec_validator_indices_are_valid(validators: vector<ValidatorInfo>): bool {
+   forall i in 0..len(validators):
+       global<ValidatorConfig>(validators[i].addr).validator_index < spec_validator_index_upper_bound()
+}
+
+ + + + + + + +
fun spec_validator_index_upper_bound(): u64 {
+   len(global<ValidatorPerformance>(@aptos_framework).validators)
+}
+
+ + + + + + + +
fun spec_has_stake_pool(a: address): bool {
+   exists<StakePool>(a)
+}
+
+ + + + + + + +
fun spec_has_validator_config(a: address): bool {
+   exists<ValidatorConfig>(a)
+}
+
+ + + + + + + +
fun spec_rewards_amount(
+   stake_amount: u64,
+   num_successful_proposals: u64,
+   num_total_proposals: u64,
+   rewards_rate: u64,
+   rewards_rate_denominator: u64,
+): u64;
+
+ + + + + + + +
fun spec_contains(validators: vector<ValidatorInfo>, addr: address): bool {
+   exists i in 0..len(validators): validators[i].addr == addr
+}
+
+ + + + + + + +
fun spec_is_current_epoch_validator(pool_address: address): bool {
+   let validator_set = global<ValidatorSet>(@aptos_framework);
+   !spec_contains(validator_set.pending_active, pool_address)
+       && (spec_contains(validator_set.active_validators, pool_address)
+       || spec_contains(validator_set.pending_inactive, pool_address))
+}
+
+ + + + + + + +
schema ResourceRequirement {
+    requires exists<AptosCoinCapabilities>(@aptos_framework);
+    requires exists<ValidatorPerformance>(@aptos_framework);
+    requires exists<ValidatorSet>(@aptos_framework);
+    requires exists<StakingConfig>(@aptos_framework);
+    requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled();
+    requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
+    requires exists<ValidatorFees>(@aptos_framework);
+}
+
+ + + + + +### Function `initialize_validator_fees` + + +
public(friend) fun initialize_validator_fees(aptos_framework: &signer)
+
+ + + + +
let aptos_addr = signer::address_of(aptos_framework);
+aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+aborts_if exists<ValidatorFees>(aptos_addr);
+ensures exists<ValidatorFees>(aptos_addr);
+
+ + + ### Function `add_transaction_fee` @@ -4104,119 +4239,4 @@ Returns validator's next epoch voting power, including pending_active, active, a - - - - - -
fun spec_validators_are_initialized(validators: vector<ValidatorInfo>): bool {
-   forall i in 0..len(validators):
-       spec_has_stake_pool(validators[i].addr) &&
-           spec_has_validator_config(validators[i].addr)
-}
-
- - - - - - - -
fun spec_validator_indices_are_valid(validators: vector<ValidatorInfo>): bool {
-   forall i in 0..len(validators):
-       global<ValidatorConfig>(validators[i].addr).validator_index < spec_validator_index_upper_bound()
-}
-
- - - - - - - -
fun spec_validator_index_upper_bound(): u64 {
-   len(global<ValidatorPerformance>(@aptos_framework).validators)
-}
-
- - - - - - - -
fun spec_has_stake_pool(a: address): bool {
-   exists<StakePool>(a)
-}
-
- - - - - - - -
fun spec_has_validator_config(a: address): bool {
-   exists<ValidatorConfig>(a)
-}
-
- - - - - - - -
fun spec_rewards_amount(
-   stake_amount: u64,
-   num_successful_proposals: u64,
-   num_total_proposals: u64,
-   rewards_rate: u64,
-   rewards_rate_denominator: u64,
-): u64;
-
- - - - - - - -
fun spec_contains(validators: vector<ValidatorInfo>, addr: address): bool {
-   exists i in 0..len(validators): validators[i].addr == addr
-}
-
- - - - - - - -
fun spec_is_current_epoch_validator(pool_address: address): bool {
-   let validator_set = global<ValidatorSet>(@aptos_framework);
-   !spec_contains(validator_set.pending_active, pool_address)
-       && (spec_contains(validator_set.active_validators, pool_address)
-       || spec_contains(validator_set.pending_inactive, pool_address))
-}
-
- - - - - - - -
schema ResourceRequirement {
-    requires exists<AptosCoinCapabilities>(@aptos_framework);
-    requires exists<ValidatorPerformance>(@aptos_framework);
-    requires exists<ValidatorSet>(@aptos_framework);
-    requires exists<StakingConfig>(@aptos_framework);
-    requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled();
-    requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
-    requires exists<ValidatorFees>(@aptos_framework);
-}
-
- - [move-book]: https://aptos.dev/guides/move-guides/book/SUMMARY diff --git a/aptos-move/framework/aptos-framework/doc/transaction_fee.md b/aptos-move/framework/aptos-framework/doc/transaction_fee.md index eff99bc7767f8..1111e88db5756 100644 --- a/aptos-move/framework/aptos-framework/doc/transaction_fee.md +++ b/aptos-move/framework/aptos-framework/doc/transaction_fee.md @@ -525,7 +525,14 @@ Only called during genesis. -
pragma verify=false;
+
aborts_if exists<CollectedFeesPerBlock>(@aptos_framework);
+aborts_if burn_percentage > 100;
+let aptos_addr = signer::address_of(aptos_framework);
+aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+aborts_if exists<ValidatorFees>(aptos_addr);
+include system_addresses::AbortsIfNotAptosFramework {account: aptos_framework};
+include aggregator_factory::CreateAggregatorInternalAbortsIf;
+ensures exists<ValidatorFees>(aptos_addr);
 

 
 
@@ -541,7 +548,15 @@ Only called during genesis.
 
 
 
-
pragma verify=false;
+
aborts_if new_burn_percentage > 100;
+let aptos_addr = signer::address_of(aptos_framework);
+aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+requires exists<AptosCoinCapabilities>(@aptos_framework);
+requires exists<stake::ValidatorFees>(@aptos_framework);
+requires exists<CoinInfo<AptosCoin>>(@aptos_framework);
+include RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+ensures exists<CollectedFeesPerBlock>(@aptos_framework) ==>
+    global<CollectedFeesPerBlock>(@aptos_framework).burn_percentage == new_burn_percentage;
 

 
 
diff --git a/aptos-move/framework/aptos-framework/doc/voting.md b/aptos-move/framework/aptos-framework/doc/voting.md
index 32828c52a7e56..45d08706a1f34 100644
--- a/aptos-move/framework/aptos-framework/doc/voting.md
+++ b/aptos-move/framework/aptos-framework/doc/voting.md
@@ -1637,7 +1637,16 @@ CurrentTimeMicroseconds existed under the @aptos_framework.
 
 
 
requires chain_status::is_operating();
-pragma aborts_if_is_strict = false;
+include AbortsIfNotContainProposalID<ProposalType>;
+aborts_if spec_get_proposal_state<ProposalType>(voting_forum_address, proposal_id) != PROPOSAL_STATE_SUCCEEDED;
+let voting_forum =  global<VotingForum<ProposalType>>(voting_forum_address);
+let proposal = table::spec_get(voting_forum.proposals, proposal_id);
+aborts_if proposal.is_resolved;
+aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY);
+aborts_if !simple_map::spec_contains_key(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY));
+aborts_if !from_bcs::deserializable<u64>(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)));
+aborts_if timestamp::spec_now_seconds() <= from_bcs::deserialize<u64>(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)));
+aborts_if transaction_context::spec_get_script_hash() != proposal.execution_hash;
 

 
 
@@ -1730,6 +1739,18 @@ CurrentTimeMicroseconds existed under the @aptos_framework.
 
 
 
+
+
+
+
+
fun spec_get_proposal_state<ProposalType>(
+   voting_forum_address: address,
+   proposal_id: u64,
+): u64;
+

+
+
+
 
 
 ### Function `get_proposal_state`
@@ -1741,9 +1762,11 @@ CurrentTimeMicroseconds existed under the @aptos_framework.
 
 
 
-
requires chain_status::is_operating();
+
pragma opaque;
+requires chain_status::is_operating();
 pragma addition_overflow_unchecked;
 include AbortsIfNotContainProposalID<ProposalType>;
+ensures [abstract] result == spec_get_proposal_state<ProposalType>(voting_forum_address, proposal_id);
 

 
 
diff --git a/aptos-move/framework/aptos-framework/sources/account.spec.move b/aptos-move/framework/aptos-framework/sources/account.spec.move
index 4359b39659224..14e637fa3a172 100644
--- a/aptos-move/framework/aptos-framework/sources/account.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/account.spec.move
@@ -155,18 +155,22 @@ spec aptos_framework::account {
             challenge: challenge,
         };
 
-        // let new_auth_key = spec_assert_valid_rotation_proof_signature_and_get_auth_key(to_scheme, to_public_key_bytes, cap_update_table, challenge);
+        // Verify all properties in update_auth_key_and_originating_address_table
+        let originating_addr = addr;
+        let new_auth_key_vector = spec_assert_valid_rotation_proof_signature_and_get_auth_key(to_scheme, to_public_key_bytes, cap_update_table, challenge);
 
-        // TODO: boogie error: Error: invalid type for argument 0 in application of $1_from_bcs_deserializable'address': int (expected: Vec int).
-        // include UpdateAuthKeyAndOriginatingAddressTableAbortsIf{
-        //     originating_addr: addr,
-        //     account_resource: account_resource,
-        //     new_auth_key_vector: new_auth_key
-        // };
-        pragma aborts_if_is_partial;
+        let address_map = global(@aptos_framework).address_map;
+        let new_auth_key = from_bcs::deserialize
(new_auth_key_vector);
+
+        aborts_if !exists(@aptos_framework);
+        aborts_if !from_bcs::deserializable
(account_resource.authentication_key);
+        aborts_if table::spec_contains(address_map, curr_auth_key) &&
+            table::spec_get(address_map, curr_auth_key) != originating_addr;
+
+        aborts_if !from_bcs::deserializable
(new_auth_key_vector);
+
+        aborts_if curr_auth_key != new_auth_key && table::spec_contains(address_map, new_auth_key);
 
-        modifies global(addr);
-        modifies global(@aptos_framework);
     }
 
     spec rotate_authentication_key_with_rotation_capability(
@@ -195,10 +199,20 @@ spec aptos_framework::account {
             signature: cap_update_table,
             challenge: challenge,
         };
-        // let new_auth_key = spec_assert_valid_rotation_proof_signature_and_get_auth_key(new_scheme, new_public_key_bytes, cap_update_table, challenge);
-        // TODO: Need to investigate the issue of including UpdateAuthKeyAndOriginatingAddressTableAbortsIf here.
-        // TODO: boogie error: Error: invalid type for argument 0 in application of $1_from_bcs_deserializable'address': int (expected: Vec int).
-        pragma aborts_if_is_partial;
+
+        let new_auth_key_vector = spec_assert_valid_rotation_proof_signature_and_get_auth_key(new_scheme, new_public_key_bytes, cap_update_table, challenge);
+        let address_map = global(@aptos_framework).address_map;
+
+        // Verify all properties in update_auth_key_and_originating_address_table
+        aborts_if !exists(@aptos_framework);
+        aborts_if !from_bcs::deserializable
(offerer_account_resource.authentication_key);
+        aborts_if table::spec_contains(address_map, curr_auth_key) &&
+            table::spec_get(address_map, curr_auth_key) != rotation_cap_offerer_address;
+
+        aborts_if !from_bcs::deserializable
(new_auth_key_vector);
+        let new_auth_key = from_bcs::deserialize
(new_auth_key_vector);
+
+        aborts_if curr_auth_key != new_auth_key && table::spec_contains(address_map, new_auth_key);
     }
 
     spec offer_rotation_capability(
diff --git a/aptos-move/framework/aptos-framework/sources/code.spec.move b/aptos-move/framework/aptos-framework/sources/code.spec.move
index 5e79a1ae6af4d..bcc76a388cc33 100644
--- a/aptos-move/framework/aptos-framework/sources/code.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/code.spec.move
@@ -46,4 +46,11 @@ spec aptos_framework::code {
         // TODO: loop too deep.
         pragma verify = false;
     }
+
+    spec get_module_names(pack: &PackageMetadata): vector {
+        pragma opaque;
+        aborts_if [abstract] false;
+        ensures [abstract] len(result) == len(pack.modules);
+        ensures [abstract] forall i in 0..len(result): result[i] == pack.modules[i].name;
+    }
 }
diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
index 1e59cd3968458..aa117251a0bb2 100644
--- a/aptos-move/framework/aptos-framework/sources/stake.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -27,6 +27,13 @@ spec aptos_framework::stake {
     // Function specifications
     // -----------------------
 
+    spec initialize_validator_fees(aptos_framework: &signer) {
+        let aptos_addr = signer::address_of(aptos_framework);
+        aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+        aborts_if exists(aptos_addr);
+        ensures exists(aptos_addr);
+    }
+
     // `Validator` is initialized once.
     spec initialize(aptos_framework: &signer) {
         let aptos_addr = signer::address_of(aptos_framework);
diff --git a/aptos-move/framework/aptos-framework/sources/transaction_fee.spec.move b/aptos-move/framework/aptos-framework/sources/transaction_fee.spec.move
index 34716da641497..334f046e1de14 100644
--- a/aptos-move/framework/aptos-framework/sources/transaction_fee.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/transaction_fee.spec.move
@@ -12,13 +12,41 @@ spec aptos_framework::transaction_fee {
     }
 
     spec initialize_fee_collection_and_distribution(aptos_framework: &signer, burn_percentage: u8) {
-        // TODO: monomorphization issue. duplicated boogie procedures.
-        pragma verify=false;
+        use std::signer;
+        use aptos_framework::stake::ValidatorFees;
+        use aptos_framework::aggregator_factory;
+        use aptos_framework::system_addresses;
+
+        aborts_if exists(@aptos_framework);
+        aborts_if burn_percentage > 100;
+
+        let aptos_addr = signer::address_of(aptos_framework);
+        aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+        aborts_if exists(aptos_addr);
+
+        include system_addresses::AbortsIfNotAptosFramework {account: aptos_framework};
+        include aggregator_factory::CreateAggregatorInternalAbortsIf;
+
+        ensures exists(aptos_addr);
     }
 
     spec upgrade_burn_percentage(aptos_framework: &signer, new_burn_percentage: u8) {
-        // TODO: missing aborts_if spec
-        pragma verify=false;
+        use std::signer;
+        use aptos_framework::coin::CoinInfo;
+        use aptos_framework::aptos_coin::AptosCoin;
+        // Percentage validation
+        aborts_if new_burn_percentage > 100;
+        // Signer validation
+        let aptos_addr = signer::address_of(aptos_framework);
+        aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+        // Requirements of `process_collected_fees`
+        requires exists(@aptos_framework);
+        requires exists(@aptos_framework);
+        requires exists>(@aptos_framework);
+        include RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        // The effect of upgrading the burn percentage
+        ensures exists(@aptos_framework) ==>
+            global(@aptos_framework).burn_percentage == new_burn_percentage;
     }
 
     spec register_proposer_for_fee_collection(proposer_addr: address) {
diff --git a/aptos-move/framework/aptos-framework/sources/voting.spec.move b/aptos-move/framework/aptos-framework/sources/voting.spec.move
index f887b3c7250a8..fd3625d61540e 100644
--- a/aptos-move/framework/aptos-framework/sources/voting.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/voting.spec.move
@@ -114,14 +114,23 @@ spec aptos_framework::voting {
         voting_forum_address: address,
         proposal_id: u64,
     ) {
+
         use aptos_framework::chain_status;
 
         requires chain_status::is_operating(); // Ensures existence of Timestamp
-
+        include AbortsIfNotContainProposalID;
         // If the proposal is not resolvable, this function aborts.
+        aborts_if spec_get_proposal_state(voting_forum_address, proposal_id) != PROPOSAL_STATE_SUCCEEDED;
 
-        // TODO: Find a way to specify when it will abort. The opaque with spec fun doesn't work.
-        pragma aborts_if_is_strict = false;
+        let voting_forum =  global>(voting_forum_address);
+        let proposal = table::spec_get(voting_forum.proposals, proposal_id);
+
+        aborts_if proposal.is_resolved;
+        aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY);
+        aborts_if !simple_map::spec_contains_key(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY));
+        aborts_if !from_bcs::deserializable(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)));
+        aborts_if timestamp::spec_now_seconds() <= from_bcs::deserialize(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)));
+        aborts_if transaction_context::spec_get_script_hash() != proposal.execution_hash;
     }
 
     spec resolve(
@@ -164,16 +173,25 @@ spec aptos_framework::voting {
         aborts_if false;
     }
 
+    spec fun spec_get_proposal_state(
+        voting_forum_address: address,
+        proposal_id: u64,
+    ): u64;
+
     spec get_proposal_state(
         voting_forum_address: address,
         proposal_id: u64,
     ): u64 {
+
         use aptos_framework::chain_status;
+        pragma opaque;
         requires chain_status::is_operating(); // Ensures existence of Timestamp
         // Addition of yes_votes and no_votes might overflow.
         pragma addition_overflow_unchecked;
+
         include AbortsIfNotContainProposalID;
         // Any way to specify the result?
+        ensures [abstract] result == spec_get_proposal_state(voting_forum_address, proposal_id);
     }
 
     spec get_proposal_creation_secs(
@@ -255,4 +273,5 @@ spec aptos_framework::voting {
         requires chain_status::is_operating();
         aborts_if false;
     }
+
 }
diff --git a/aptos-move/framework/aptos-stdlib/doc/from_bcs.md b/aptos-move/framework/aptos-stdlib/doc/from_bcs.md
index adb0222db0dd3..5dc4812f0bfef 100644
--- a/aptos-move/framework/aptos-stdlib/doc/from_bcs.md
+++ b/aptos-move/framework/aptos-stdlib/doc/from_bcs.md
@@ -337,6 +337,10 @@ owned.
 fun deserializable<T>(bytes: vector<u8>): bool;
 axiom<T> forall b1: vector<u8>, b2: vector<u8>:
     (deserialize<T>(b1) == deserialize<T>(b2) ==> b1 == b2);
+axiom<T> forall b1: vector<u8>, b2: vector<u8>:
+    ( b1 == b2 ==> deserializable<T>(b1) == deserializable<T>(b2) );
+axiom<T> forall b1: vector<u8>, b2: vector<u8>:
+    ( b1 == b2 ==> deserialize<T>(b1) == deserialize<T>(b2) );
 

 
 
diff --git a/aptos-move/framework/aptos-stdlib/doc/smart_vector.md b/aptos-move/framework/aptos-stdlib/doc/smart_vector.md
index c4ae93ff04641..131fa86967b39 100644
--- a/aptos-move/framework/aptos-stdlib/doc/smart_vector.md
+++ b/aptos-move/framework/aptos-stdlib/doc/smart_vector.md
@@ -31,6 +31,7 @@
     -  [Function `destroy_empty`](#@Specification_1_destroy_empty)
     -  [Function `borrow`](#@Specification_1_borrow)
     -  [Function `append`](#@Specification_1_append)
+    -  [Function `push_back`](#@Specification_1_push_back)
     -  [Function `pop_back`](#@Specification_1_pop_back)
     -  [Function `remove`](#@Specification_1_remove)
     -  [Function `swap_remove`](#@Specification_1_swap_remove)
@@ -891,6 +892,22 @@ Return true if the vector v has no elements and
 
 
 
+
pragma verify = false;
+

+
+
+
+
+
+### Function `push_back`
+
+
+
public fun push_back<T: store>(v: &mut smart_vector::SmartVector<T>, val: T)
+

+
+
+
+
 
pragma verify = false;
 

 
diff --git a/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_vector.spec.move b/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_vector.spec.move
index ba8f135b68ddf..c4bfca925cd51 100644
--- a/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_vector.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_vector.spec.move
@@ -33,6 +33,10 @@ spec aptos_std::smart_vector {
         );
     }
 
+    spec push_back(v: &mut SmartVector, val: T) {
+        pragma verify = false; // TODO: set to false because of timeout
+    }
+
     spec pop_back {
         use aptos_std::table_with_length;
 
diff --git a/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move b/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move
index 71f43efd783d7..9eeb4f025cdc2 100644
--- a/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move
@@ -14,6 +14,13 @@ spec aptos_std::from_bcs {
         axiom forall b1: vector, b2: vector:
             (deserialize(b1) == deserialize(b2) ==> b1 == b2);
 
+        // If the input are equal, the result of deserialize should be equal too
+        axiom forall b1: vector, b2: vector:
+            ( b1 == b2 ==> deserializable(b1) == deserializable(b2) );
+
+        axiom forall b1: vector, b2: vector:
+            ( b1 == b2 ==> deserialize(b1) == deserialize(b2) );
+
         // `deserialize` is an inverse function of `bcs::serialize`.
         // TODO: disabled because this generic axiom causes a timeout.
         // axiom forall v: T: deserialize(bcs::serialize(v)) == v;