[sui-verifier] Small cleanup + comments (MystenLabs#3076)

* [sui-verifier] Small cleanup + comments

- Removed id_immutable pass, it is covered by `VersionedID` not having `drop`
- Removed check for types with `key` not having `drop`, it is covered by `VersionedID`
- Added doc comment to `struct_with_key_verifier`

* Update crates/sui-verifier/src/struct_with_key_verifier.rs

Co-authored-by: Sam Blackshear <[email protected]>

crates/sui-verifier-transactional-tests/tests/id_immutable/mut_borrow_generic_key_struct_id_field.exp

@@ -1,5 +1,5 @@
 processed 1 task
 
 task 0 'publish'. lines 4-18:
-Error: Transaction Effects Status: MiscellaneousError
-Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: ModuleVerificationFailure, source: Some("In function foo: ID field of struct Foo cannot be mut borrowed because ID is immutable.") } }
+created: object(103)
+written: object(102)

crates/sui-verifier-transactional-tests/tests/id_immutable/mut_borrow_key_struct_id_field.exp

@@ -1,5 +1,5 @@
 processed 1 task
 
 task 0 'publish'. lines 4-18:
-Error: Transaction Effects Status: MiscellaneousError
-Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: ModuleVerificationFailure, source: Some("In function foo: ID field of struct Foo cannot be mut borrowed because ID is immutable.") } }
+created: object(103)
+written: object(102)

crates/sui-verifier-transactional-tests/tests/id_immutable/write_id_field.exp

@@ -0,0 +1,5 @@
+processed 1 task
+
+task 0 'publish'. lines 4-20:
+Error: Transaction Effects Status: MiscellaneousError
+Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: VmError, source: Some(VMError { major_status: WRITEREF_WITHOUT_DROP_ABILITY, sub_status: None, message: None, exec_state: None, location: Module(ModuleId { address: _, name: Identifier("m") }), indices: [(FunctionDefinition, 0)], offsets: [(FunctionDefinitionIndex(0), 5)] }) } }

crates/sui-verifier-transactional-tests/tests/id_immutable/write_id_field.mvir

@@ -0,0 +1,20 @@
+// Copyright (c) 2022, Mysten Labs, Inc.
+// SPDX-License-Identifier: Apache-2.0
+
+//# publish
+module 0x0.m {
+    import 0x2.id;
+
+    struct Foo has key {
+        id: id.VersionedID,
+    }
+
+    foo(f: Self.Foo, id: id.VersionedID) {
+        let x: &mut id.VersionedID;
+        label l0:
+        x = &mut (&mut f).Foo::id;
+        *move(x) = move(id);
+        abort 0;
+    }
+
+}

crates/sui-verifier-transactional-tests/tests/struct_with_key/key_struct_with_drop.exp

@@ -1,5 +1,5 @@
 processed 1 task
 
-task 0 'publish'. lines 4-10:
+task 0 'publish'. lines 4-11:
 Error: Transaction Effects Status: MiscellaneousError
-Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: ModuleVerificationFailure, source: Some("Struct S cannot have both key and drop abilities") } }
+Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: VmError, source: Some(VMError { major_status: FIELD_MISSING_TYPE_ABILITY, sub_status: None, message: None, exec_state: None, location: Module(ModuleId { address: _, name: Identifier("m") }), indices: [(StructDefinition, 0)], offsets: [] }) } }

crates/sui-verifier-transactional-tests/tests/struct_with_key/key_struct_with_drop.mvir

@@ -5,6 +5,7 @@
 module 0x0.m {
     import 0x2.id;
     struct S has key, drop {
+        id: id.VersionedID,
         flag: bool
     }
 }

crates/sui-verifier/src/entry_points_verifier.rs

@@ -29,7 +29,6 @@ pub const INIT_FN_NAME: &IdentStr = ident_str!("init");
 /// - The function must have the name specified by `INIT_FN_NAME`
 /// - The function must have `Visibility::Private`
 /// - The function can have a single parameter: &mut TxContext (see `is_tx_context`)
-/// - Alternatively, the function can have zero parameters
 ///
 /// For transaction entry points
 /// - The function must have `is_entry` true

crates/sui-verifier/src/lib.rs

@@ -5,7 +5,6 @@ pub mod verifier;
 
 pub mod entry_points_verifier;
 pub mod global_storage_access_verifier;
-pub mod id_immutable_verifier;
 pub mod id_leak_verifier;
 pub mod private_generics;
 pub mod struct_with_key_verifier;

crates/sui-verifier/src/struct_with_key_verifier.rs

@@ -1,13 +1,23 @@
 // Copyright (c) 2022, Mysten Labs, Inc.
 // SPDX-License-Identifier: Apache-2.0
 
+//! This pass verifies necessary properties for Move Objects, i.e. structs with the `key` ability.
+//! The properties checked are
+//! - The first field is named "id"
+//! - The first field has type `sui::id::VersionedID`
+
 use crate::verification_failure;
 use move_binary_format::{
     access::ModuleAccess,
     binary_views::BinaryIndexedView,
     file_format::{CompiledModule, SignatureToken},
 };
-use sui_types::{error::ExecutionError, fp_ensure, SUI_FRAMEWORK_ADDRESS};
+use sui_types::{
+    error::ExecutionError,
+    fp_ensure,
+    id::{ID_MODULE_NAME, VERSIONED_ID_STRUCT_NAME},
+    SUI_FRAMEWORK_ADDRESS,
+};
 
 pub fn verify_module(module: &CompiledModule) -> Result<(), ExecutionError> {
     verify_key_structs(module)
@@ -22,16 +32,6 @@ fn verify_key_structs(module: &CompiledModule) -> Result<(), ExecutionError> {
             continue;
         }
         let name = view.identifier_at(handle.name);
-        // Check that a struct with key ability must not have drop ability.
-        // A struct with key ability represents a sui object.
-        // We want to ensure that sui objects cannot be arbitrarily dropped.
-        // For example, *x = new_object shouldn't work for a key object x.
-        if handle.abilities.has_drop() {
-            return Err(verification_failure(format!(
-                "Struct {} cannot have both key and drop abilities",
-                name
-            )));
-        }
 
         // Check that the first field of the struct must be named "id".
         let first_field = match def.field(0) {
@@ -63,14 +63,14 @@ fn verify_key_structs(module: &CompiledModule) -> Result<(), ExecutionError> {
         };
         // Chech that the struct type for "id" field must be SUI_FRAMEWORK_ADDRESS::ID::ID.
         let id_type_struct = module.struct_handle_at(*id_field_type);
-        let id_type_struct_name = view.identifier_at(id_type_struct.name).as_str();
+        let id_type_struct_name = view.identifier_at(id_type_struct.name);
         let id_type_module = module.module_handle_at(id_type_struct.module);
         let id_type_module_address = module.address_identifier_at(id_type_module.address);
-        let id_type_module_name = module.identifier_at(id_type_module.name).to_string();
+        let id_type_module_name = module.identifier_at(id_type_module.name);
         fp_ensure!(
-            id_type_struct_name == "VersionedID"
+            id_type_struct_name == VERSIONED_ID_STRUCT_NAME
                 && id_type_module_address == &SUI_FRAMEWORK_ADDRESS
-                && id_type_module_name == "id",
+                && id_type_module_name == ID_MODULE_NAME,
             verification_failure(format!(
                 "First field of struct {} must be of type {}::id::VersionedID, {}::{}::{} type found",
                 name,

crates/sui-verifier/src/verifier.rs

@@ -7,15 +7,14 @@ use move_binary_format::file_format::CompiledModule;
 use sui_types::error::ExecutionError;
 
 use crate::{
-    entry_points_verifier, global_storage_access_verifier, id_immutable_verifier, id_leak_verifier,
-    private_generics, struct_with_key_verifier,
+    entry_points_verifier, global_storage_access_verifier, id_leak_verifier, private_generics,
+    struct_with_key_verifier,
 };
 
 /// Helper for a "canonical" verification of a module.
 pub fn verify_module(module: &CompiledModule) -> Result<(), ExecutionError> {
     struct_with_key_verifier::verify_module(module)?;
     global_storage_access_verifier::verify_module(module)?;
-    id_immutable_verifier::verify_module(module)?;
     id_leak_verifier::verify_module(module)?;
     private_generics::verify_module(module)?;
     entry_points_verifier::verify_module(module)