implement rust logics and specs

aptos-move/e2e-move-tests/src/tests/gas.rs

@@ -30,7 +30,7 @@ use aptos_types::{
     transaction::{EntryFunction, TransactionPayload},
 };
 use aptos_vm_environment::prod_configs::set_paranoid_type_checks;
-use move_core_types::{identifier::Identifier, language_storage::ModuleId};
+use move_core_types::{identifier::Identifier, language_storage::ModuleId, value::MoveValue};
 use rand::{rngs::StdRng, SeedableRng};
 use sha3::{Digest, Sha3_512};
 use std::path::Path;
@@ -57,7 +57,9 @@ fn test_modify_gas_schedule_check_hash() {
         "set_for_next_epoch_check_hash",
         vec![],
         vec![
-            bcs::to_bytes(&CORE_CODE_ADDRESS).unwrap(),
+            MoveValue::Signer(CORE_CODE_ADDRESS)
+                .simple_serialize()
+                .unwrap(),
             bcs::to_bytes(&old_hash).unwrap(),
             bcs::to_bytes(&bcs::to_bytes(&gas_schedule).unwrap()).unwrap(),
         ],
@@ -66,7 +68,9 @@ fn test_modify_gas_schedule_check_hash() {
     harness
         .executor
         .exec("reconfiguration_with_dkg", "finish", vec![], vec![
-            bcs::to_bytes(&CORE_CODE_ADDRESS).unwrap(),
+            MoveValue::Signer(CORE_CODE_ADDRESS)
+                .simple_serialize()
+                .unwrap(),
         ]);
 
     let (_, gas_params) = harness.get_gas_params();

aptos-move/e2e-tests/src/executor.rs

@@ -67,6 +67,7 @@ use move_core_types::{
     identifier::Identifier,
     language_storage::{ModuleId, StructTag, TypeTag},
     move_resource::{MoveResource, MoveStructType},
+    value::MoveValue,
 };
 use move_vm_runtime::{
     module_traversal::{TraversalContext, TraversalStorage},
@@ -998,13 +999,23 @@ impl FakeExecutor {
             let mut arg = args.clone();
             match &dynamic_args {
                 ExecFuncTimerDynamicArgs::DistinctSigners => {
-                    arg.insert(0, bcs::to_bytes(&extra_accounts.pop().unwrap()).unwrap());
+                    arg.insert(
+                        0,
+                        MoveValue::Signer(extra_accounts.pop().unwrap())
+                            .simple_serialize()
+                            .unwrap(),
+                    );
                 },
                 ExecFuncTimerDynamicArgs::DistinctSignersAndFixed(signers) => {
                     for signer in signers.iter().rev() {
-                        arg.insert(0, bcs::to_bytes(&signer).unwrap());
+                        arg.insert(0, MoveValue::Signer(*signer).simple_serialize().unwrap());
                     }
-                    arg.insert(0, bcs::to_bytes(&extra_accounts.pop().unwrap()).unwrap());
+                    arg.insert(
+                        0,
+                        MoveValue::Signer(extra_accounts.pop().unwrap())
+                            .simple_serialize()
+                            .unwrap(),
+                    );
                 },
                 _ => {},
             }

aptos-move/framework/aptos-framework/doc/transaction_context.md

@@ -1029,6 +1029,7 @@ Returns the inner entry function payload of the multisig payload.
 
 
 <pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> [abstract] <b>false</b>;
 <b>ensures</b> [abstract] result == <a href="transaction_context.md#0x1_transaction_context_spec_generate_unique_address">spec_generate_unique_address</a>();
 </code></pre>
 
@@ -1055,6 +1056,7 @@ Returns the inner entry function payload of the multisig payload.
 
 
 <pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> [abstract] <b>false</b>;
 // This enforces <a id="high-level-req-3" href="#high-level-req">high-level requirement 3</a>:
 <b>ensures</b> [abstract] result == <a href="transaction_context.md#0x1_transaction_context_spec_generate_unique_address">spec_generate_unique_address</a>();
 </code></pre>

aptos-move/framework/aptos-framework/sources/permissioned_signer.spec.move

@@ -0,0 +1,177 @@
+spec aptos_framework::permissioned_signer {
+
+    spec module {
+        axiom forall a: GrantedPermissionHandles:
+            (forall i in 0..len(a.active_handles):
+                forall j in 0..len(a.active_handles):
+                    i != j ==> a.active_handles[i] != a.active_handles[j]
+            );
+    }
+
+    spec fun spec_is_permissioned_signer(s: signer): bool;
+
+    spec is_permissioned_signer(s: &signer): bool {
+        pragma opaque;
+        aborts_if [abstract] false;
+        ensures [abstract] result == spec_is_permissioned_signer(s);
+    }
+
+    spec fun spec_permission_signer(s: signer): signer;
+
+    spec permission_signer(permissioned: &signer): signer {
+        pragma opaque;
+        aborts_if [abstract] !spec_is_permissioned_signer(permissioned);
+        ensures [abstract] result == spec_permission_signer(permissioned);
+    }
+
+    spec fun spec_signer_from_permissioned_impl(master_addr: address, permission_addr: address): signer;
+
+    spec signer_from_permissioned_impl(master_addr: address, permission_addr: address): signer {
+        pragma opaque;
+        ensures [abstract] result == spec_signer_from_permissioned_impl(master_addr, permission_addr);
+    }
+
+    spec create_permissioned_handle(master: &signer): PermissionedHandle {
+        use aptos_framework::transaction_context;
+        pragma opaque;
+        aborts_if [abstract] spec_is_permissioned_signer(master);
+        let permission_addr = transaction_context::spec_generate_unique_address();
+        modifies global<PermStorage>(permission_addr);
+        let master_addr = signer::address_of(master);
+        ensures result.master_addr == master_addr;
+        ensures result.permission_addr == permission_addr;
+    }
+
+    spec create_storable_permissioned_handle(master: &signer, expiration_time: u64): StorablePermissionedHandle {
+        use aptos_framework::transaction_context;
+        pragma opaque;
+        aborts_if [abstract] spec_is_permissioned_signer(master);
+        let permission_addr = transaction_context::spec_generate_unique_address();
+        modifies global<PermStorage>(permission_addr);
+        let master_addr = signer::address_of(master);
+        modifies global<GrantedPermissionHandles>(master_addr);
+        ensures result.master_addr == master_addr;
+        ensures result.permission_addr == permission_addr;
+        ensures result.expiration_time == expiration_time;
+        ensures vector::spec_contains(global<GrantedPermissionHandles>(master_addr).active_handles, permission_addr);
+        ensures exists<GrantedPermissionHandles>(master_addr);
+    }
+
+    spec destroy_permissioned_handle(p: PermissionedHandle) {
+        ensures !exists<PermStorage>(p.permission_addr);
+    }
+
+    spec destroy_storable_permissioned_handle(p: StorablePermissionedHandle) {
+        ensures !exists<PermStorage>(p.permission_addr);
+        let post granted_permissions = global<GrantedPermissionHandles>(p.master_addr);
+        // ensures [abstract] !vector::spec_contains(granted_permissions.active_handles, p.permission_addr);
+    }
+
+    spec revoke_permission_handle(s: &signer, permission_addr: address) {
+        aborts_if spec_is_permissioned_signer(s);
+    }
+
+    spec authorize<PermKey: copy + drop + store>(
+    master: &signer,
+    permissioned: &signer,
+    capacity: u256,
+    perm: PermKey
+    ) {
+
+        use aptos_std::type_info;
+        use std::bcs;
+        pragma aborts_if_is_partial;
+        aborts_if !spec_is_permissioned_signer(permissioned);
+        aborts_if spec_is_permissioned_signer(master);
+        aborts_if signer::address_of(permissioned) != signer::address_of(master);
+        ensures exists<PermStorage>(signer::address_of(spec_permission_signer(permissioned)));
+        // let perms = global<PermStorage>(permission_signer_addr).perms;
+        // let post post_perms = global<PermStorage>(permission_signer_addr).perms;
+        // let key = Any {
+        //     type_name: type_info::type_name<SmartTable<Any, u256>>(),
+        //     data: bcs::serialize(perm)
+        // };
+        // ensures smart_table::spec_contains(perms, key) ==>
+        //     smart_table::spec_get(post_perms, key) == old(smart_table::spec_get(perms, key)) + capacity;
+        // ensures !smart_table::spec_contains(perms, key) ==>
+        //     smart_table::spec_get(post_perms, key) == capacity;
+    }
+
+    spec check_permission_exists<PermKey: copy + drop + store>(
+    s: &signer,
+    perm: PermKey
+    ): bool {
+        pragma opaque;
+        aborts_if false;
+        ensures result == spec_check_permission_exists(s, perm);
+    }
+
+    spec fun spec_check_permission_exists<PermKey: copy + drop + store>(
+        s: signer,
+        perm: PermKey
+    ): bool {
+        use aptos_std::type_info;
+        use std::bcs;
+        let addr = signer::address_of(spec_permission_signer(s));
+        let key = Any {
+            type_name: type_info::type_name<PermKey>(),
+            data: bcs::serialize(perm)
+        };
+        if (!spec_is_permissioned_signer(s)) {
+            true
+        } else if(!exists<PermStorage>(addr)) {
+            false
+        } else {
+            simple_map::spec_contains_key(global<PermStorage>(addr).perms, key)
+        }
+    }
+
+    spec check_permission_capacity_above<PermKey: copy + drop + store>(
+    s: &signer,
+    threshold: u256,
+    perm: PermKey
+    ): bool {
+        use aptos_std::type_info;
+        use std::bcs;
+        let permissioned_signer_addr = signer::address_of(spec_permission_signer(s));
+        ensures !spec_is_permissioned_signer(s) ==> result == true;
+        ensures (spec_is_permissioned_signer(s) && !exists<PermStorage>(permissioned_signer_addr)) ==> result == false;
+        let key = Any {
+            type_name: type_info::type_name<SimpleMap<Any, u256>>(),
+            data: bcs::serialize(perm)
+        };
+        // ensures (spec_is_permissioned_signer(s) && exists<PermStorage>(permissioned_signer_addr) && !smart_table::spec_contains(global<PermStorage>(permissioned_signer_addr).perms, key)) ==>
+        //     result == false;
+        // ensures (spec_is_permissioned_signer(s) && exists<PermStorage>(permissioned_signer_addr) && smart_table::spec_contains(global<PermStorage>(permissioned_signer_addr).perms, key)) ==>
+        //     result == (smart_table::spec_get(global<PermStorage>(permissioned_signer_addr).perms, key) > threshold);
+    }
+
+    spec check_permission_consume<PermKey: copy + drop + store>(
+    s: &signer,
+    threshold: u256,
+    perm: PermKey
+    ): bool {
+        let permissioned_signer_addr = signer::address_of(spec_permission_signer(s));
+        ensures !spec_is_permissioned_signer(s) ==> result == true;
+        ensures (spec_is_permissioned_signer(s) && !exists<PermStorage>(permissioned_signer_addr)) ==> result == false;
+
+    }
+
+    spec capacity<PermKey: copy + drop + store>(s: &signer, perm: PermKey): Option<u256> {
+        aborts_if !spec_is_permissioned_signer(s);
+        let permissioned_signer_addr = signer::address_of(spec_permission_signer(s));
+        ensures !exists<PermStorage>(permissioned_signer_addr) ==> option::is_none(result);
+    }
+
+    spec consume_permission<PermKey: copy + drop + store>(
+        perm: &mut 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);
+    }
+
+}

aptos-move/framework/aptos-framework/sources/transaction_context.spec.move

@@ -58,11 +58,13 @@ spec aptos_framework::transaction_context {
     }
     spec generate_unique_address(): address {
         pragma opaque;
+        aborts_if [abstract] false;
         ensures [abstract] result == spec_generate_unique_address();
     }
     spec fun spec_generate_unique_address(): address;
     spec generate_auid_address(): address {
         pragma opaque;
+        aborts_if [abstract] false;
         // property 3: Generating the unique address should return a vector with 32 bytes, if the auid feature flag is enabled.
         /// [high-level-req-3]
         ensures [abstract] result == spec_generate_unique_address();

aptos-move/framework/aptos-stdlib/doc/smart_table.md

@@ -1479,6 +1479,7 @@ map_spec_has_key = spec_contains;
 
 
 <pre><code><b>pragma</b> verify = <b>false</b>;
+<b>pragma</b> opaque;
 </code></pre>
 
 
@@ -1495,6 +1496,7 @@ map_spec_has_key = spec_contains;
 
 
 <pre><code><b>pragma</b> verify = <b>false</b>;
+<b>pragma</b> opaque;
 </code></pre>
 
 

aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move

@@ -24,10 +24,12 @@ spec aptos_std::smart_table {
 
     spec destroy<K: drop, V: drop>(self: SmartTable<K, V>) {
         pragma verify = false;
+        pragma opaque;
     }
 
     spec clear<K: drop, V: drop>(self: &mut SmartTable<K, V>) {
         pragma verify = false;
+        pragma opaque;
     }
 
     spec split_one_bucket<K, V>(self: &mut SmartTable<K, V>) {

aptos-move/framework/src/aptos.rs

@@ -113,7 +113,7 @@ impl ReleaseTarget {
                     output_format: None,
                 }),
                 skip_fetch_latest_git_deps: true,
-                ..BuildOptions::default()
+                ..BuildOptions::move_2()
             },
             packages: packages.iter().map(|(path, _)| path.to_owned()).collect(),
             rust_bindings: packages

aptos-move/framework/src/natives/mod.rs

@@ -15,6 +15,7 @@ pub mod function_info;
 pub mod hash;
 pub mod object;
 pub mod object_code_deployment;
+pub mod permissioned_signer;
 pub mod randomness;
 pub mod state_storage;
 pub mod string_utils;
@@ -91,6 +92,10 @@ pub fn all_natives(
         "dispatchable_fungible_asset",
         dispatchable_fungible_asset::make_all(builder)
     );
+    add_natives_from_module!(
+        "permissioned_signer",
+        permissioned_signer::make_all(builder)
+    );
 
     if inject_create_signer_for_gov_sim {
         add_natives_from_module!(