[move] Deprecate specs. Remove Move model's dependencies on expansion AST

Cargo.toml

@@ -38,7 +38,6 @@ exclude = [
     "external-crates/move/crates/move-package",
     "external-crates/move/crates/move-proc-macros",
     "external-crates/move/crates/move-prover",
-    "external-crates/move/crates/move-prover-boogie-backend",
     "external-crates/move/crates/move-prover-test-utils",
     "external-crates/move/crates/move-read-write-set-types",
     "external-crates/move/crates/move-stackless-bytecode",
@@ -54,9 +53,7 @@ exclude = [
     "external-crates/move/crates/move-vm-test-utils",
     "external-crates/move/crates/move-vm-transactional-tests",
     "external-crates/move/crates/move-vm-types",
-    "external-crates/move/crates/prover-mutation",
     "external-crates/move/crates/serializer-tests",
-    "external-crates/move/crates/spec-flatten",
     "external-crates/move/crates/test-generation",
     "external-crates/move/move-execution/next-vm/crates/move-bytecode-verifier",
     "external-crates/move/move-execution/next-vm/crates/move-stdlib",
@@ -537,7 +534,6 @@ move-command-line-common = { path = "external-crates/move/crates/move-command-li
 move-transactional-test-runner = { path = "external-crates/move/crates/move-transactional-test-runner" }
 move-ir-types = { path = "external-crates/move/crates/move-ir-types" }
 move-prover = { path = "external-crates/move/crates/move-prover" }
-move-prover-boogie-backend = { path = "external-crates/move/crates/move-prover-boogie-backend" }
 move-stackless-bytecode = { path = "external-crates/move/crates/move-stackless-bytecode" }
 move-symbol-pool = { path = "external-crates/move/crates/move-symbol-pool" }
 move-abstract-stack = { path = "external-crates/move/crates/move-abstract-stack" }

crates/sui-framework/CONTRIBUTING.md

@@ -14,25 +14,3 @@ cargo insta test -p sui-config --review
 ```
 
 Please use your best judgment to decide if the changes between old and new versions of the snapshots look "reasonable" (e.g., a minor change in gas costs). When in doubt, please reach out to a member of Sui core team.
-
-### Native functions integration with the Move Prover
-
-Each native function must be represented in the Move Prover model in order for the Move Prover to be able to reason about their behavior. Ideally, you would provide the actual model of a new native function expressed in the Boogie language in [crates/sui/src/sui_move/sui-natives.bpl](../sui/src/sui_move/sui-natives.bpl). Alternatively, if you do not need to have the Move Prover reason about a particular native function (you do not plan to write Move Prover specifications concerning this function), you can provide an "empty" model by defining an "stub" specification for the native function itself. A specification clause (`spec`) has the same name as the native function and the "stub" specification contains a single `pragma opaque;` statement. The specification(s) should be placed in the spec file accompanying the module file (see example below for the [bls12381](./sources/crypto/bls12381.move) module with the specifications placed in the [bls12381.spec.move](./sources/crypto/bls12381.spec.move) file):
-
-``` rust
-spec sui::bls12381 {
-    // specification for the bls12381_min_sig_verify native function
-    spec bls12381_min_sig_verify {
-        // TODO: temporary mockup.
-        pragma opaque;
-    }
-
-    // specification for the bls12381_min_pk_verify native function
-    spec bls12381_min_pk_verify {
-        // TODO: temporary mockup.
-        pragma opaque;
-    }
-}
-```
-
-You can read more about defining Move Prover specifications in the documentation for the [Move Specification Language](https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md).

crates/sui-framework/packages/move-stdlib/sources/ascii.move

@@ -10,34 +10,25 @@ module std::ascii {
     /// An invalid ASCII character was encountered when creating an ASCII string.
     const EINVALID_ASCII_CHARACTER: u64 = 0x10000;
 
-   /// The `String` struct holds a vector of bytes that all represent
-   /// valid ASCII characters. Note that these ASCII characters may not all
-   /// be printable. To determine if a `String` contains only "printable"
-   /// characters you should use the `all_characters_printable` predicate
-   /// defined in this module.
-   struct String has copy, drop, store {
-       bytes: vector<u8>,
-   }
-   spec String {
-       invariant forall i in 0..len(bytes): is_valid_char(bytes[i]);
-   }
-
-   /// An ASCII character.
-   struct Char has copy, drop, store {
-       byte: u8,
-   }
-   spec Char {
-       invariant is_valid_char(byte);
-   }
+    /// The `String` struct holds a vector of bytes that all represent
+    /// valid ASCII characters. Note that these ASCII characters may not all
+    /// be printable. To determine if a `String` contains only "printable"
+    /// characters you should use the `all_characters_printable` predicate
+    /// defined in this module.
+    struct String has copy, drop, store {
+        bytes: vector<u8>,
+    }
+
+    /// An ASCII character.
+    struct Char has copy, drop, store {
+        byte: u8,
+    }
 
     /// Convert a `byte` into a `Char` that is checked to make sure it is valid ASCII.
     public fun char(byte: u8): Char {
         assert!(is_valid_char(byte), EINVALID_ASCII_CHARACTER);
         Char { byte }
     }
-    spec char {
-        aborts_if !is_valid_char(byte) with EINVALID_ASCII_CHARACTER;
-    }
 
     /// Convert a vector of bytes `bytes` into an `String`. Aborts if
     /// `bytes` contains non-ASCII characters.
@@ -49,73 +40,41 @@ module std::ascii {
        );
        option::destroy_some(x)
     }
-    spec string {
-        aborts_if exists i in 0..len(bytes): !is_valid_char(bytes[i]) with EINVALID_ASCII_CHARACTER;
-    }
 
     /// Convert a vector of bytes `bytes` into an `String`. Returns
     /// `Some(<ascii_string>)` if the `bytes` contains all valid ASCII
     /// characters. Otherwise returns `None`.
     public fun try_string(bytes: vector<u8>): Option<String> {
-       let len = vector::length(&bytes);
-       let i = 0;
-       while ({
-           spec {
-               invariant i <= len;
-               invariant forall j in 0..i: is_valid_char(bytes[j]);
-           };
-           i < len
-       }) {
-           let possible_byte = *vector::borrow(&bytes, i);
-           if (!is_valid_char(possible_byte)) return option::none();
-           i = i + 1;
-       };
-       spec {
-           assert i == len;
-           assert forall j in 0..len: is_valid_char(bytes[j]);
-       };
-       option::some(String { bytes })
+        let len = vector::length(&bytes);
+        let i = 0;
+        while (i < len) {
+            let possible_byte = *vector::borrow(&bytes, i);
+            if (!is_valid_char(possible_byte)) return option::none();
+            i = i + 1;
+        };
+        option::some(String { bytes })
     }
 
     /// Returns `true` if all characters in `string` are printable characters
     /// Returns `false` otherwise. Not all `String`s are printable strings.
     public fun all_characters_printable(string: &String): bool {
-       let len = vector::length(&string.bytes);
-       let i = 0;
-       while ({
-           spec {
-               invariant i <= len;
-               invariant forall j in 0..i: is_printable_char(string.bytes[j]);
-           };
-           i < len
-       }) {
-           let byte = *vector::borrow(&string.bytes, i);
-           if (!is_printable_char(byte)) return false;
-           i = i + 1;
-       };
-       spec {
-           assert i == len;
-           assert forall j in 0..len: is_printable_char(string.bytes[j]);
-       };
-       true
-    }
-    spec all_characters_printable {
-        ensures result ==> (forall j in 0..len(string.bytes): is_printable_char(string.bytes[j]));
+        let len = vector::length(&string.bytes);
+        let i = 0;
+        while (i < len) {
+            let byte = *vector::borrow(&string.bytes, i);
+            if (!is_printable_char(byte)) return false;
+            i = i + 1;
+        };
+        true
     }
 
     public fun push_char(string: &mut String, char: Char) {
         vector::push_back(&mut string.bytes, char.byte);
     }
-    spec push_char {
-        ensures len(string.bytes) == len(old(string.bytes)) + 1;
-    }
 
     public fun pop_char(string: &mut String): Char {
         Char { byte: vector::pop_back(&mut string.bytes) }
     }
-    spec pop_char {
-        ensures len(string.bytes) == len(old(string.bytes)) - 1;
-    }
 
     public fun length(string: &String): u64 {
         vector::length(as_bytes(string))

crates/sui-framework/packages/move-stdlib/sources/bcs.move

@@ -8,13 +8,4 @@
 module std::bcs {
     /// Return the binary representation of `v` in BCS (Binary Canonical Serialization) format
     native public fun to_bytes<MoveValue>(v: &MoveValue): vector<u8>;
-
-    // ==============================
-    // Module Specification
-    spec module {} // switch to module documentation context
-
-    spec module {
-        /// Native function which is defined in the prover's prelude.
-        native fun serialize<MoveValue>(v: &MoveValue): vector<u8>;
-    }
 }

crates/sui-framework/packages/move-stdlib/sources/bit_vector.move

@@ -23,66 +23,30 @@ module std::bit_vector {
         assert!(length < MAX_SIZE, ELENGTH);
         let counter = 0;
         let bit_field = vector::empty();
-        while ({spec {
-            invariant counter <= length;
-            invariant len(bit_field) == counter;
-        };
-            (counter < length)}) {
+        while (counter < length) {
             vector::push_back(&mut bit_field, false);
             counter = counter + 1;
         };
-        spec {
-            assert counter == length;
-            assert len(bit_field) == length;
-        };
 
         BitVector {
             length,
             bit_field,
         }
     }
-    spec new {
-        include NewAbortsIf;
-        ensures result.length == length;
-        ensures len(result.bit_field) == length;
-    }
-    spec schema NewAbortsIf {
-        length: u64;
-        aborts_if length <= 0 with ELENGTH;
-        aborts_if length >= MAX_SIZE with ELENGTH;
-    }
 
     /// Set the bit at `bit_index` in the `bitvector` regardless of its previous state.
     public fun set(bitvector: &mut BitVector, bit_index: u64) {
         assert!(bit_index < vector::length(&bitvector.bit_field), EINDEX);
         let x = vector::borrow_mut(&mut bitvector.bit_field, bit_index);
         *x = true;
     }
-    spec set {
-        include SetAbortsIf;
-        ensures bitvector.bit_field[bit_index];
-    }
-    spec schema SetAbortsIf {
-        bitvector: BitVector;
-        bit_index: u64;
-        aborts_if bit_index >= length(bitvector) with EINDEX;
-    }
 
     /// Unset the bit at `bit_index` in the `bitvector` regardless of its previous state.
     public fun unset(bitvector: &mut BitVector, bit_index: u64) {
         assert!(bit_index < vector::length(&bitvector.bit_field), EINDEX);
         let x = vector::borrow_mut(&mut bitvector.bit_field, bit_index);
         *x = false;
     }
-    spec set {
-        include UnsetAbortsIf;
-        ensures bitvector.bit_field[bit_index];
-    }
-    spec schema UnsetAbortsIf {
-        bitvector: BitVector;
-        bit_index: u64;
-        aborts_if bit_index >= length(bitvector) with EINDEX;
-    }
 
     /// Shift the `bitvector` left by `amount`. If `amount` is greater than the
     /// bitvector's length the bitvector will be zeroed out.
@@ -119,22 +83,6 @@ module std::bit_vector {
         assert!(bit_index < vector::length(&bitvector.bit_field), EINDEX);
         *vector::borrow(&bitvector.bit_field, bit_index)
     }
-    spec is_index_set {
-        include IsIndexSetAbortsIf;
-        ensures result == bitvector.bit_field[bit_index];
-    }
-    spec schema IsIndexSetAbortsIf {
-        bitvector: BitVector;
-        bit_index: u64;
-        aborts_if bit_index >= length(bitvector) with EINDEX;
-    }
-    spec fun spec_is_index_set(bitvector: BitVector, bit_index: u64): bool {
-        if (bit_index >= length(bitvector)) {
-            false
-        } else {
-            bitvector.bit_field[bit_index]
-        }
-    }
 
     /// Return the length (number of usable bits) of this bitvector
     public fun length(bitvector: &BitVector): u64 {

crates/sui-framework/packages/move-stdlib/sources/fixed_point32.move

@@ -46,19 +46,6 @@ module std::fixed_point32 {
         assert!(product <= MAX_U64, EMULTIPLICATION);
         (product as u64)
     }
-    spec multiply_u64 {
-        pragma opaque;
-        include MultiplyAbortsIf;
-        ensures result == spec_multiply_u64(val, multiplier);
-    }
-    spec schema MultiplyAbortsIf {
-        val: num;
-        multiplier: FixedPoint32;
-        aborts_if spec_multiply_u64(val, multiplier) > MAX_U64 with EMULTIPLICATION;
-    }
-    spec fun spec_multiply_u64(val: num, multiplier: FixedPoint32): num {
-        (val * multiplier.value) >> 32
-    }
 
     /// Divide a u64 integer by a fixed-point number, truncating any
     /// fractional part of the quotient. This will abort if the divisor
@@ -76,20 +63,6 @@ module std::fixed_point32 {
         // with an arithmetic error.
         (quotient as u64)
     }
-    spec divide_u64 {
-        pragma opaque;
-        include DivideAbortsIf;
-        ensures result == spec_divide_u64(val, divisor);
-    }
-    spec schema DivideAbortsIf {
-        val: num;
-        divisor: FixedPoint32;
-        aborts_if divisor.value == 0 with EDIVISION_BY_ZERO;
-        aborts_if spec_divide_u64(val, divisor) > MAX_U64 with EDIVISION;
-    }
-    spec fun spec_divide_u64(val: num, divisor: FixedPoint32): num {
-        (val << 32) / divisor.value
-    }
 
     /// Create a fixed-point value from a rational number specified by its
     /// numerator and denominator. Calling this function should be preferred
@@ -116,34 +89,11 @@ module std::fixed_point32 {
         assert!(quotient <= MAX_U64, ERATIO_OUT_OF_RANGE);
         FixedPoint32 { value: (quotient as u64) }
     }
-    spec create_from_rational {
-        pragma opaque;
-        include CreateFromRationalAbortsIf;
-        ensures result == spec_create_from_rational(numerator, denominator);
-    }
-    spec schema CreateFromRationalAbortsIf {
-        numerator: u64;
-        denominator: u64;
-        let scaled_numerator = numerator << 64;
-        let scaled_denominator = denominator << 32;
-        let quotient = scaled_numerator / scaled_denominator;
-        aborts_if scaled_denominator == 0 with EDENOMINATOR;
-        aborts_if quotient == 0 && scaled_numerator != 0 with ERATIO_OUT_OF_RANGE;
-        aborts_if quotient > MAX_U64 with ERATIO_OUT_OF_RANGE;
-    }
-    spec fun spec_create_from_rational(numerator: num, denominator: num): FixedPoint32 {
-        FixedPoint32{value: (numerator << 64) / (denominator << 32)}
-    }
 
     /// Create a fixedpoint value from a raw value.
     public fun create_from_raw_value(value: u64): FixedPoint32 {
         FixedPoint32 { value }
     }
-    spec create_from_raw_value {
-        pragma opaque;
-        aborts_if false;
-        ensures result.value == value;
-    }
 
     /// Accessor for the raw u64 value. Other less common operations, such as
     /// adding or subtracting FixedPoint32 values, can be done using the raw
@@ -156,12 +106,4 @@ module std::fixed_point32 {
     public fun is_zero(num: FixedPoint32): bool {
         num.value == 0
     }
-
-    // **************** SPECIFICATIONS ****************
-
-    spec module {} // switch documentation context to module level
-
-    spec module {
-        pragma aborts_if_is_strict;
-    }
 }