[Spec] Add boogie natives for newly added public methods in vector (a…

…ptos-labs#7558) * new boogie natives for vector * new vector intrinsics
Yolley · Apr 5, 2023 · 85f562b · 85f562b
1 parent ab39502
commit 85f562b
Show file tree

Hide file tree

Showing 4 changed files with 265 additions and 7 deletions.
diff --git a/aptos-move/framework/move-stdlib/doc/vector.md b/aptos-move/framework/move-stdlib/doc/vector.md
@@ -43,12 +43,19 @@ the return on investment didn't seem worth it for these simple functions.
     -  [Helper Functions](#@Helper_Functions_2)
     -  [Function `singleton`](#@Specification_1_singleton)
     -  [Function `reverse`](#@Specification_1_reverse)
+    -  [Function `reverse_slice`](#@Specification_1_reverse_slice)
     -  [Function `append`](#@Specification_1_append)
+    -  [Function `reverse_append`](#@Specification_1_reverse_append)
+    -  [Function `trim`](#@Specification_1_trim)
+    -  [Function `trim_reverse`](#@Specification_1_trim_reverse)
     -  [Function `is_empty`](#@Specification_1_is_empty)
     -  [Function `contains`](#@Specification_1_contains)
     -  [Function `index_of`](#@Specification_1_index_of)
+    -  [Function `insert`](#@Specification_1_insert)
     -  [Function `remove`](#@Specification_1_remove)
     -  [Function `swap_remove`](#@Specification_1_swap_remove)
+    -  [Function `rotate`](#@Specification_1_rotate)
+    -  [Function `rotate_slice`](#@Specification_1_rotate_slice)
 
 
 <pre><code></code></pre>
@@ -823,6 +830,22 @@ Check if <code>v</code> contains <code>e</code>.
 
 
 
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_reverse_slice"></a>
+
+### Function `reverse_slice`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_reverse_slice">reverse_slice</a>&lt;Element&gt;(v: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, left: u64, right: u64)
+</code></pre>
+
+
+
+
 <pre><code><b>pragma</b> intrinsic = <b>true</b>;
 </code></pre>
 
@@ -839,6 +862,54 @@ Check if <code>v</code> contains <code>e</code>.
 
 
 
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_reverse_append"></a>
+
+### Function `reverse_append`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_reverse_append">reverse_append</a>&lt;Element&gt;(lhs: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, other: <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;)
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_trim"></a>
+
+### Function `trim`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_trim">trim</a>&lt;Element&gt;(v: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, new_len: u64): <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_trim_reverse"></a>
+
+### Function `trim_reverse`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_trim_reverse">trim_reverse</a>&lt;Element&gt;(v: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, new_len: u64): <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;
+</code></pre>
+
+
+
+
 <pre><code><b>pragma</b> intrinsic = <b>true</b>;
 </code></pre>
 
@@ -887,6 +958,22 @@ Check if <code>v</code> contains <code>e</code>.
 
 
 
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_insert"></a>
+
+### Function `insert`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_insert">insert</a>&lt;Element&gt;(v: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, i: u64, e: Element)
+</code></pre>
+
+
+
+
 <pre><code><b>pragma</b> intrinsic = <b>true</b>;
 </code></pre>
 
@@ -919,6 +1006,38 @@ Check if <code>v</code> contains <code>e</code>.
 
 
 
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_rotate"></a>
+
+### Function `rotate`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_rotate">rotate</a>&lt;Element&gt;(v: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, rot: u64): u64
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> intrinsic = <b>true</b>;
+</code></pre>
+
+
+
+<a name="@Specification_1_rotate_slice"></a>
+
+### Function `rotate_slice`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="vector.md#0x1_vector_rotate_slice">rotate_slice</a>&lt;Element&gt;(v: &<b>mut</b> <a href="vector.md#0x1_vector">vector</a>&lt;Element&gt;, left: u64, rot: u64, right: u64): u64
+</code></pre>
+
+
+
+
 <pre><code><b>pragma</b> intrinsic = <b>true</b>;
 </code></pre>
 

diff --git a/aptos-move/framework/move-stdlib/sources/vector.move b/aptos-move/framework/move-stdlib/sources/vector.move
@@ -84,6 +84,9 @@ module std::vector {
             right = right - 1;
         }
     }
+    spec reverse_slice {
+        pragma intrinsic = true;
+    }
 
     /// Pushes all of the elements of the `other` vector into the `lhs` vector.
     public fun append<Element>(lhs: &mut vector<Element>, other: vector<Element>) {
@@ -106,13 +109,19 @@ module std::vector {
         };
         destroy_empty(other);
     }
+    spec reverse_append {
+        pragma intrinsic = true;
+    }
 
     /// Trim a vector to a smaller size, returning the evicted elements in order
     public fun trim<Element>(v: &mut vector<Element>, new_len: u64): vector<Element> {
         let res = trim_reverse(v, new_len);
         reverse(&mut res);
         res
     }
+    spec trim {
+        pragma intrinsic = true;
+    }
 
     /// Trim a vector to a smaller size, returning the evicted elements in reverse order
     public fun trim_reverse<Element>(v: &mut vector<Element>, new_len: u64): vector<Element> {
@@ -125,6 +134,9 @@ module std::vector {
         };
         result
     }
+    spec trim_reverse {
+        pragma intrinsic = true;
+    }
 
 
     /// Return `true` if the vector `v` has no elements and `false` otherwise.
@@ -172,6 +184,9 @@ module std::vector {
             i = i + 1;
         };
     }
+    spec insert {
+        pragma intrinsic = true;
+    }
 
     /// Remove the `i`th element of the vector `v`, shifting all subsequent elements.
     /// This is O(n) and preserves ordering of elements in the vector.
@@ -329,6 +344,9 @@ module std::vector {
         let len = length(v);
         rotate_slice(v, 0, rot, len)
     }
+    spec rotate {
+        pragma intrinsic = true;
+    }
 
     /// Same as above but on a sub-slice of an array [left, right) with left <= rot <= right
     /// returns the
@@ -343,6 +361,9 @@ module std::vector {
         reverse_slice(v, left, right);
         left + (right - rot)
     }
+    spec rotate_slice {
+        pragma intrinsic = true;
+    }
 
     /// Partition the array based on a predicate p, this routine is stable and thus
     /// preserves the relative order of the elements in the two partitions.

diff --git a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl
@@ -115,6 +115,117 @@ procedure {:inline 1} $1_vector_reverse{{S}}(m: $Mutation (Vec ({{T}}))) returns
     m' := $UpdateMutation(m, ReverseVec($Dereference(m)));
 }
 
+procedure {:inline 1} $1_vector_reverse_append{{S}}(m: $Mutation (Vec ({{T}})), other: Vec ({{T}})) returns (m': $Mutation (Vec ({{T}}))) {
+    m' := $UpdateMutation(m, ConcatVec($Dereference(m), ReverseVec(other)));
+}
+
+procedure {:inline 1} $1_vector_trim_reverse{{S}}(m: $Mutation (Vec ({{T}})), new_len: int) returns (v: (Vec ({{T}})), m': $Mutation (Vec ({{T}}))) {
+    var len: int;
+    v := $Dereference(m);
+    if (LenVec(v) < new_len) {
+        call $ExecFailureAbort();
+        return;
+    }
+    v := SliceVec(v, new_len, LenVec(v));
+    v := ReverseVec(v);
+    m' := $UpdateMutation(m, SliceVec($Dereference(m), 0, new_len));
+}
+
+procedure {:inline 1} $1_vector_trim{{S}}(m: $Mutation (Vec ({{T}})), new_len: int) returns (v: (Vec ({{T}})), m': $Mutation (Vec ({{T}}))) {
+    var len: int;
+    v := $Dereference(m);
+    if (LenVec(v) < new_len) {
+        call $ExecFailureAbort();
+        return;
+    }
+    v := SliceVec(v, new_len, LenVec(v));
+    m' := $UpdateMutation(m, SliceVec($Dereference(m), 0, new_len));
+}
+
+procedure {:inline 1} $1_vector_reverse_slice{{S}}(m: $Mutation (Vec ({{T}})), left: int, right: int) returns (m': $Mutation (Vec ({{T}}))) {
+    var left_vec: Vec ({{T}});
+    var mid_vec: Vec ({{T}});
+    var right_vec: Vec ({{T}});
+    var v: Vec ({{T}});
+    if (left > right) {
+        call $ExecFailureAbort();
+        return;
+    }
+    if (left == right) {
+        m' := m;
+        return;
+    }
+    v := $Dereference(m);
+    if (!(right >= 0 && right <= LenVec(v))) {
+        call $ExecFailureAbort();
+        return;
+    }
+    left_vec := SliceVec(v, 0, left);
+    right_vec := SliceVec(v, right, LenVec(v));
+    mid_vec := ReverseVec(SliceVec(v, left, right));
+    m' := $UpdateMutation(m, ConcatVec(left_vec, ConcatVec(mid_vec, right_vec)));
+}
+
+procedure {:inline 1} $1_vector_rotate{{S}}(m: $Mutation (Vec ({{T}})), rot: int) returns (n: int, m': $Mutation (Vec ({{T}}))) {
+    var v: Vec ({{T}});
+    var len: int;
+    var left_vec: Vec ({{T}});
+    var right_vec: Vec ({{T}});
+    v := $Dereference(m);
+    if (!(rot >= 0 && rot <= LenVec(v))) {
+        call $ExecFailureAbort();
+        return;
+    }
+    left_vec := SliceVec(v, 0, rot);
+    right_vec := SliceVec(v, rot, LenVec(v));
+    m' := $UpdateMutation(m, ConcatVec(right_vec, left_vec));
+    n := LenVec(v) - rot;
+}
+
+procedure {:inline 1} $1_vector_rotate_slice{{S}}(m: $Mutation (Vec ({{T}})), left: int, rot: int, right: int) returns (n: int, m': $Mutation (Vec ({{T}}))) {
+    var left_vec: Vec ({{T}});
+    var mid_vec: Vec ({{T}});
+    var right_vec: Vec ({{T}});
+    var mid_left_vec: Vec ({{T}});
+    var mid_right_vec: Vec ({{T}});
+    var v: Vec ({{T}});
+    v := $Dereference(m);
+    if (!(left <= rot && rot <= right)) {
+        call $ExecFailureAbort();
+        return;
+    }
+    if (!(right >= 0 && right <= LenVec(v))) {
+        call $ExecFailureAbort();
+        return;
+    }
+    v := $Dereference(m);
+    left_vec := SliceVec(v, 0, left);
+    right_vec := SliceVec(v, right, LenVec(v));
+    mid_left_vec := SliceVec(v, left, rot);
+    mid_right_vec := SliceVec(v, rot, right);
+    mid_vec := ConcatVec(mid_right_vec, mid_left_vec);
+    m' := $UpdateMutation(m, ConcatVec(left_vec, ConcatVec(mid_vec, right_vec)));
+    n := left + (right - rot);
+}
+
+procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), i: int, e: {{T}}) returns (m': $Mutation (Vec ({{T}}))) {
+    var left_vec: Vec ({{T}});
+    var right_vec: Vec ({{T}});
+    var v: Vec ({{T}});
+    v := $Dereference(m);
+    if (!(i >= 0 && i <= LenVec(v))) {
+        call $ExecFailureAbort();
+        return;
+    }
+    if (i == LenVec(v)) {
+        m' := $UpdateMutation(m, ExtendVec(v, e));
+    } else {
+        left_vec := ExtendVec(SliceVec(v, 0, i), e);
+        right_vec := SliceVec(v, i, LenVec(v));
+        m' := $UpdateMutation(m, ConcatVec(left_vec, right_vec));
+    }
+}
+
 procedure {:inline 1} $1_vector_length{{S}}(v: Vec ({{T}})) returns (l: int) {
     l := LenVec(v);
 }

diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp
@@ -44,9 +44,12 @@ error: unknown assertion failed
    =     at tests/sources/functional/loops_with_memory_ops.move:74: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
-   =         b = <redacted>
-   =         b = <redacted>
-   =         a = <redacted>
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =     at <internal>:1
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
@@ -99,10 +102,14 @@ error: induction case of the loop invariant does not hold
    =     at tests/sources/functional/loops_with_memory_ops.move:74: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
-   =         b = <redacted>
-   =         b = <redacted>
-   =         a = <redacted>
-   =         a = <redacted>
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =     at <internal>:1
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2