more nla spec

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

@@ -116,10 +116,18 @@ spec aptos_framework::transaction_context {
     spec monotonically_increasing_counter_internal(timestamp_us: u64): u128 {
         //TODO: temporary mockup
         pragma opaque;
+        aborts_if [abstract] false;
     }
 
     spec monotonically_increasing_counter_internal_for_test_only(): u128 {
         //TODO: temporary mockup
         pragma opaque;
+        aborts_if [abstract] false;
+    }
+
+    spec monotonically_increasing_counter(): u128 {
+        pragma opaque;
+        // Assume that the monotonically increasing counter is always increasing.
+        aborts_if [abstract] false;
     }
 }

aptos-move/framework/aptos-stdlib/sources/math64.move

@@ -87,6 +87,9 @@ module aptos_std::math64 {
                 res += n;
             };
             n >>= 1;
+        } spec {
+            invariant (res as u64) + 2 * (n as u64) <= 64;
+            invariant n == 0 ==> (res as u64) <= 63;
         };
         res
     }

aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move

@@ -4,6 +4,8 @@ spec aptos_std::math_fixed {
     /// No loop in the body, so callers can inline without havocing.
     spec sqrt(x: FixedPoint32): FixedPoint32 {
         aborts_if false;
+        // Zero input → zero output, directly from math128::sqrt's ensures.
+        ensures x.get_raw_value() == 0 ==> result.get_raw_value() == 0;
     }
 
     /// `mul_div` aborts when z is zero or when x * y / z overflows u64.

aptos-move/framework/move-stdlib/sources/string.spec.move

@@ -24,6 +24,12 @@ spec std::string {
         String{bytes}
     }
 
+    spec utf8(bytes: vector<u8>): String {
+        pragma opaque;
+        aborts_if !spec_internal_check_utf8(bytes);
+        ensures result == spec_utf8(bytes);
+    }
+
     spec module {
         fun spec_internal_check_utf8(v: vector<u8>): bool;
         fun spec_internal_is_char_boundary(v: vector<u8>, i: u64): bool;

third_party/move/move-prover/boogie-backend/src/prelude/native.bpl

@@ -226,6 +226,43 @@ procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), i: int,
     }
 }
 
+// `vector::move_range(from, removal_position, length, to, insert_position)` extracts the
+// half-open range `[removal_position, removal_position+length)` from `from` and splices it
+// into `to` at `insert_position`, shifting `to[insert_position..]` to the right. Move enforces
+// that `from` and `to` are distinct (no aliasing of mutable references).
+procedure {:inline 1} $1_vector_move_range{{S}}(
+    from: $Mutation (Vec ({{T}})),
+    removal_position: int,
+    length: int,
+    to: $Mutation (Vec ({{T}})),
+    insert_position: int
+) returns (from': $Mutation (Vec ({{T}})), to': $Mutation (Vec ({{T}})))
+{
+    var from_v: Vec ({{T}});
+    var to_v: Vec ({{T}});
+    var middle: Vec ({{T}});
+    from_v := $Dereference(from);
+    to_v := $Dereference(to);
+    // The `< 0` checks are defensive — Move's u64 arguments are non-negative by typing,
+    // but Boogie ints can be arbitrary so we guard explicitly. Matches the convention
+    // used in `$1_vector_insert` above.
+    if (removal_position < 0
+        || length < 0
+        || removal_position + length > LenVec(from_v)
+        || insert_position < 0
+        || insert_position > LenVec(to_v)) {
+        call $ExecFailureAbort();
+        return;
+    }
+    middle := SliceVec(from_v, removal_position, removal_position + length);
+    from' := $UpdateMutation(from,
+        ConcatVec(SliceVec(from_v, 0, removal_position),
+                  SliceVec(from_v, removal_position + length, LenVec(from_v))));
+    to' := $UpdateMutation(to,
+        ConcatVec(SliceVec(to_v, 0, insert_position),
+                  ConcatVec(middle, SliceVec(to_v, insert_position, LenVec(to_v)))));
+}
+
 procedure {:inline 1} $1_vector_length{{S}}(v: Vec ({{T}})) returns (l: int) {
     l := LenVec(v);
 }