[move] Remove proptests from execution version cut (MystenLabs#17240)

## Description 

- Removed proptests from execution version cut
- As a result, we no longer need invalid-mutations in the cut

## Test plan 

- CI

---

## Release notes

Check each box that your changes affect. If none of the boxes relate to
your changes, release notes aren't required.

For each box you select, include information after the relevant heading
that describes the impact of your changes that a user might notice and
any actions they must take to implement updates.

- [ ] Protocol: 
- [ ] Nodes (Validators and Full nodes): 
- [ ] Indexer: 
- [ ] JSON-RPC: 
- [ ] GraphQL: 
- [ ] CLI: 
- [ ] Rust SDK:

Cargo.toml

@@ -6,6 +6,7 @@ exclude = [
   "external-crates/move/crates/bytecode-interpreter-testsuite",
   "external-crates/move/crates/bytecode-verifier-libfuzzer",
   "external-crates/move/crates/bytecode-verifier-tests",
+  "external-crates/move/crates/bytecode-verifier-prop-tests",
   "external-crates/move/crates/bytecode-verifier-transactional-tests",
   "external-crates/move/crates/enum-compat-util",
   "external-crates/move/crates/invalid-mutations",

external-crates/move/Cargo.toml

@@ -7,10 +7,6 @@ members = [
     "move-execution/v1/crates/bytecode-verifier-tests",
     "move-execution/v2/crates/bytecode-verifier-tests",
     # "move-execution/$CUT/crates/bytecode-verifier-tests",
-    "move-execution/v0/crates/invalid-mutations",
-    "move-execution/v1/crates/invalid-mutations",
-    "move-execution/v2/crates/invalid-mutations",
-    # "move-execution/$CUT/crates/invalid-mutations",
     "move-execution/v0/crates/move-bytecode-verifier",
     "move-execution/v1/crates/move-bytecode-verifier",
     "move-execution/v2/crates/move-bytecode-verifier",

external-crates/move/crates/bytecode-verifier-prop-tests/Cargo.toml

@@ -0,0 +1,28 @@
+[package]
+name = "bytecode-verifier-prop-tests"
+version = "0.1.0"
+authors = ["Diem Association <opensource@diem.com>"]
+description = "Diem bytecode verifier tests"
+repository = "https://github.com/diem/diem"
+homepage = "https://diem.com"
+license = "Apache-2.0"
+publish = false
+edition = "2021"
+
+[dev-dependencies]
+petgraph.workspace = true
+proptest.workspace = true
+fail = { workspace = true, features = ["failpoints"] }
+hex.workspace = true
+
+invalid-mutations.workspace = true
+move-binary-format = { workspace = true, features = ["fuzzing"] }
+move-bytecode-verifier.workspace = true
+move-bytecode-verifier-meter.workspace = true
+move-core-types.workspace = true
+move-vm-config.workspace = true
+
+[features]
+fuzzing = ["move-binary-format/fuzzing"]
+
+[dependencies]

external-crates/move/crates/bytecode-verifier-prop-tests/src/lib.rs

@@ -0,0 +1,5 @@
+// Copyright (c) The Move Contributors
+// SPDX-License-Identifier: Apache-2.0
+
+#[cfg(test)]
+pub mod unit_tests;

external-crates/move/crates/bytecode-verifier-prop-tests/src/unit_tests/mod.rs

@@ -0,0 +1,4 @@
+// Copyright (c) The Move Contributors
+// SPDX-License-Identifier: Apache-2.0
+
+pub mod prop_tests;

external-crates/move/crates/bytecode-verifier-prop-tests/src/unit_tests/prop_tests.rs

@@ -0,0 +1,161 @@
+// Copyright (c) The Move Contributors
+// SPDX-License-Identifier: Apache-2.0
+
+use invalid_mutations::{
+    bounds::{
+        ApplyCodeUnitBoundsContext, ApplyOutOfBoundsContext, CodeUnitBoundsMutation,
+        OutOfBoundsMutation,
+    },
+    signature::{FieldRefMutation, SignatureRefMutation},
+};
+use move_binary_format::{
+    check_bounds::BoundsChecker, file_format::CompiledModule,
+    proptest_types::CompiledModuleStrategyGen,
+};
+use move_bytecode_verifier::{
+    ability_field_requirements, constants, instantiation_loops::InstantiationLoopChecker,
+    DuplicationChecker, InstructionConsistency, RecursiveStructDefChecker, SignatureChecker,
+};
+use move_core_types::{
+    account_address::AccountAddress, identifier::Identifier, vm_status::StatusCode,
+};
+use proptest::{collection::vec, prelude::*, sample::Index as PropIndex};
+
+proptest! {
+    // Generating arbitrary compiled modules is really slow, possibly because of
+    // https://github.com/AltSysrq/proptest/issues/143.
+    #![proptest_config(ProptestConfig::with_cases(16))]
+
+    #[test]
+    fn valid_ability_transitivity(module in CompiledModule::valid_strategy(20)) {
+        prop_assert!(ability_field_requirements::verify_module(&module).is_ok());
+    }
+
+    #[test]
+    fn valid_bounds(_module in CompiledModule::valid_strategy(20)) {
+        // valid_strategy will panic if there are any bounds check issues.
+    }
+
+    #[test]
+    fn invalid_out_of_bounds(
+        module in CompiledModule::valid_strategy(20),
+        oob_mutations in vec(OutOfBoundsMutation::strategy(), 0..40),
+    ) {
+        let (module, expected_violations) = {
+            let oob_context = ApplyOutOfBoundsContext::new(module, oob_mutations);
+            oob_context.apply()
+        };
+
+        let actual_violations = BoundsChecker::verify_module(&module);
+        prop_assert_eq!(expected_violations.is_empty(), actual_violations.is_ok());
+    }
+
+    #[test]
+    fn code_unit_out_of_bounds(
+        mut module in CompiledModule::valid_strategy(20),
+        mutations in vec(CodeUnitBoundsMutation::strategy(), 0..40),
+    ) {
+        let expected_violations = {
+            let context = ApplyCodeUnitBoundsContext::new(&mut module, mutations);
+            context.apply()
+        };
+
+        let actual_violations = BoundsChecker::verify_module(&module);
+        prop_assert_eq!(expected_violations.is_empty(), actual_violations.is_ok());
+    }
+
+    #[test]
+    fn no_module_handles(
+        identifiers in vec(any::<Identifier>(), 0..20),
+        address_identifiers in vec(any::<AccountAddress>(), 0..20),
+    ) {
+        // If there are no module handles, the only other things that can be stored are intrinsic
+        // data.
+        let module = CompiledModule {
+            identifiers,
+            address_identifiers,
+            ..Default::default()
+        };
+
+        prop_assert_eq!(
+            BoundsChecker::verify_module(&module).map_err(|e| e.major_status()),
+            Err(StatusCode::NO_MODULE_HANDLES)
+        );
+    }
+
+    /// Make sure that garbage inputs don't crash the bounds checker.
+    #[test]
+    fn garbage_inputs(module in any_with::<CompiledModule>(16)) {
+        let _ = BoundsChecker::verify_module(&module);
+    }
+
+    #[test]
+    fn valid_generated_constants(module in CompiledModule::valid_strategy(20)) {
+        prop_assert!(constants::verify_module(&module).is_ok());
+    }
+
+    #[test]
+    fn valid_duplication(module in CompiledModule::valid_strategy(20)) {
+        prop_assert!(DuplicationChecker::verify_module(&module).is_ok());
+    }
+
+    #[test]
+    fn check_verifier_passes(module in CompiledModule::valid_strategy(20)) {
+        DuplicationChecker::verify_module(&module).expect("DuplicationChecker failure");
+        SignatureChecker::verify_module(&module).expect("SignatureChecker failure");
+        InstructionConsistency::verify_module(&module).expect("InstructionConsistency failure");
+        constants::verify_module(&module).expect("constants failure");
+        ability_field_requirements::verify_module(&module).expect("ability_field_requirements failure");
+        RecursiveStructDefChecker::verify_module(&module).expect("RecursiveStructDefChecker failure");
+        InstantiationLoopChecker::verify_module(&module).expect("InstantiationLoopChecker failure");
+    }
+
+    #[test]
+    fn valid_signatures(module in CompiledModule::valid_strategy(20)) {
+        prop_assert!(SignatureChecker::verify_module(&module).is_ok())
+    }
+
+    #[test]
+    fn double_refs(
+        mut module in CompiledModule::valid_strategy(20),
+        mutations in vec((any::<PropIndex>(), any::<PropIndex>()), 0..20),
+    ) {
+        let context = SignatureRefMutation::new(&mut module, mutations);
+        let expected_violations = context.apply();
+
+        let result = SignatureChecker::verify_module(&module);
+
+        prop_assert_eq!(expected_violations, result.is_err());
+    }
+
+    #[test]
+    fn field_def_references(
+        mut module in CompiledModule::valid_strategy(20),
+        mutations in vec((any::<PropIndex>(), any::<PropIndex>()), 0..40),
+    ) {
+        let context = FieldRefMutation::new(&mut module, mutations);
+        let expected_violations = context.apply();
+
+        let result = SignatureChecker::verify_module(&module);
+
+        prop_assert_eq!(expected_violations, result.is_err());
+    }
+
+    #[test]
+    fn valid_recursive_struct_defs(module in CompiledModule::valid_strategy(20)) {
+        prop_assert!(RecursiveStructDefChecker::verify_module(&module).is_ok());
+    }
+}
+
+/// Ensure that valid modules that don't have any members (e.g. function args, struct fields) pass
+/// bounds checks.
+///
+/// There are some potentially tricky edge cases around ranges that are captured here.
+#[test]
+fn valid_bounds_no_members() {
+    let mut gen = CompiledModuleStrategyGen::new(20);
+    gen.zeros_all();
+    proptest!(|(_module in gen.generate())| {
+        // gen.generate() will panic if there are any bounds check issues.
+    });
+}

external-crates/move/crates/bytecode-verifier-tests/Cargo.toml

@@ -11,19 +11,15 @@ edition = "2021"
 
 [dev-dependencies]
 petgraph.workspace = true
-proptest.workspace = true
 fail = { workspace = true, features = ["failpoints"] }
 hex.workspace = true
 
-# referred to via path for execution versioning
-invalid-mutations = { path = "../invalid-mutations" }
 move-binary-format = { workspace = true, features = ["fuzzing"] }
-move-bytecode-verifier.workspace = true
+# referred to via path for execution versioning
+move-bytecode-verifier = { path = "../move-bytecode-verifier" }
 move-bytecode-verifier-meter.workspace = true
 move-core-types.workspace = true
 move-vm-config.workspace = true
 
 [features]
 fuzzing = ["move-binary-format/fuzzing"]
-
-[dependencies]