[prover] Added a Boogie model for vector::insert function (#831)

* [prover] Added a Boogie model for vector::insert function

* Simplified ensures clause for testing vector::insert

* Removed unnecessary new line

* Updated test output

* Replaced a broken link with another one

Author: awelc

devtools/x-lint/src/lib.rs

@@ -5,7 +5,7 @@
 //! Lint engine.
 //!
 //! The overall design is generally inspired by
-//! [Arcanist](https://secure.phabricator.com/book/phabricator/article/arcanist_lint)'s lint engine.
+//! Arcanist](https://www.phacility.com/phabricator/arcanist)'s lint engine.
 
 pub mod content;
 pub mod file_path;

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

@@ -187,6 +187,25 @@ procedure {:inline 1} $1_vector_remove{{S}}(m: $Mutation (Vec ({{T}})), i: int)
     m' := $UpdateMutation(m, RemoveAtVec(v, i));
 }
 
+procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), val: {{T}}, i: int) returns (m': $Mutation (Vec ({{T}}))) {
+
+    var len: int;
+    var v: Vec ({{T}});
+
+    v := $Dereference(m);
+
+    len := LenVec(v);
+    if (i < 0 || i > len) {
+        call $ExecFailureAbort();
+        return;
+    }
+    if (i == len) {
+        m' := $UpdateMutation(m, ExtendVec(v, val));
+    } else {
+        m' := $UpdateMutation(m, InsertAtVec(v, i, val));
+    }
+}
+
 procedure {:inline 1} $1_vector_swap_remove{{S}}(m: $Mutation (Vec ({{T}})), i: int) returns (e: {{T}}, m': $Mutation (Vec ({{T}})))
 {
     var len: int;

language/move-prover/boogie-backend/src/prelude/vector-array-intern-theory.bpl

@@ -87,6 +87,17 @@ function {:inline} RemoveAtVec<T>(v: Vec T, i: int): Vec T {
         l)))
 }
 
+function {:inline} InsertAtVec<T>(v: Vec T, i: int, elem: T): Vec T {
+    (var l := l#Vec(v) + 1;
+    VecIntern(Vec(
+        (lambda j: int ::
+         if j >= 0 && j < l then
+           if j < i then v#Vec(v)[j]
+           else if j > i then v#Vec(v)[j-1] else elem
+         else DefaultVecElem()),
+        l)))
+}
+
 function {:inline} ConcatVec<T>(v1: Vec T, v2: Vec T): Vec T {
     (var l1, m1, l2, m2 := l#Vec(v1), v#Vec(v1), l#Vec(v2), v#Vec(v2);
     VecIntern(Vec(

language/move-prover/boogie-backend/src/prelude/vector-array-theory.bpl

@@ -64,6 +64,17 @@ function {:inline} RemoveAtVec<T>(v: Vec T, i: int): Vec T {
         l))
 }
 
+function {:inline} InsertAtVec<T>(v: Vec T, i: int, elem: T): Vec T {
+    (var l := l#Vec(v) + 1;
+    Vec(
+        (lambda j: int ::
+         if j >= 0 && j < l then
+           if j < i then v#Vec(v)[j]
+           else if j > i then v#Vec(v)[j-1] else elem
+         else DefaultVecElem()),
+        l))
+}
+
 function {:inline} ConcatVec<T>(v1: Vec T, v2: Vec T): Vec T {
     (var l1, m1, l2, m2 := l#Vec(v1), v#Vec(v1), l#Vec(v2), v#Vec(v2);
     Vec(

language/move-prover/tests/sources/functional/loops_with_memory_ops.exp

@@ -47,7 +47,8 @@ error: unknown assertion failed
    =         b = <redacted>
    =         b = <redacted>
    =         a = <redacted>
-   =         a = <redacted>
+   =     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
@@ -98,11 +99,12 @@ 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>
    =     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
+   =         a = <redacted>
+   =         a = <redacted>
    =     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

language/move-prover/tests/sources/functional/verify_vector.move

@@ -291,6 +291,18 @@ module 0x42::VerifyVector {
         ensures old(v[i]) == result;
     }
 
+    // Add an element to the vector at index.
+    fun verify_model_insert<Element>(v: &mut vector<Element>, e: Element, i: u64) {
+        vector::insert(v, e, i); // inlining the built-in Boogie procedure
+    }
+    spec verify_model_insert {
+        aborts_if i > len(v);
+        ensures len(v) == len(old(v)) + 1;
+        ensures v[i] == e;
+        ensures old(v[0..i]) == v[0..i];
+        ensures old(v)[i..len(old(v))] == v[i+1..len(v)];
+    }
+
     // Remove the `i`th element E of the vector by swapping it with the last element,
     // and then popping it off
     // It is O(1), but does not preserve ordering