Repository: aptos-labs/aptos-core (language: python)

Issue:
[Feature Request][Prover] Support vector operation in spec function
# 🚀 Feature Request

<!-- A clear and concise description of the feature you are requesting -->

## Motivation

Currently, when a Move function contains expression `vector[...]`, it cannot be translated into a spec function. We want to support it to improve expressiveness of the prover.


Discussion / hints:

Fix patch:
diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
index 48bac0b40d94c..53235c65f1116 100644
--- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
@@ -973,6 +973,24 @@ impl<'env> SpecTranslator<'env> {
                 // Skip freeze operation
                 self.translate_exp(&args[0])
             },
+            Operation::Vector if args.is_empty() => {
+                self.translate_primitive_inst_call(node_id, "$EmptyVec", args)
+            },
+            Operation::Vector if args.len() == 1 => self.translate_primitive_call("MakeVec1", args),
+            Operation::Vector if args.len() == 2 => self.translate_primitive_call("MakeVec2", args),
+            Operation::Vector if args.len() == 3 => self.translate_primitive_call("MakeVec3", args),
+            Operation::Vector if args.len() == 4 => self.translate_primitive_call("MakeVec4", args),
+            Operation::Vector => {
+                let mut count = 0;
+                for arg in &args[0..args.len() - 1] {
+                    emit!(self.writer, "ConcatVec(");
+                    self.translate_call(node_id, oper, &[arg.clone()]);
+                    emit!(self.writer, ",");
+                    count += 1;
+                }
+                self.translate_call(node_id, oper, &[args[args.len() - 1].clone()]);
+                emit!(self.writer, &")".repeat(count));
+            },
             Operation::MoveFunction(_, _)
             | Operation::BorrowGlobal(_)
             | Operation::Borrow(..)
@@ -980,7 +998,6 @@ impl<'env> SpecTranslator<'env> {
             | Operation::MoveTo
             | Operation::MoveFrom
             | Operation::Abort
-            | Operation::Vector
             | Operation::Old => {
                 panic!("operation unexpected: {}", oper.display(self.env, node_id))
             },


Test patch:
diff --git a/third_party/move/move-prover/tests/sources/functional/verify_vector.move b/third_party/move/move-prover/tests/sources/functional/verify_vector.move
index 0ddfdda7d98b0..ae0c70bce42f4 100644
--- a/third_party/move/move-prover/tests/sources/functional/verify_vector.move
+++ b/third_party/move/move-prover/tests/sources/functional/verify_vector.move
@@ -88,7 +88,7 @@ module 0x42::VerifyVector {
     spec verify_singleton {
         aborts_if false;
         ensures len(result) == 1;
-        ensures result[0] == e;
+        ensures result == vector[e];
     }
 
     // Reverses the order of the elements in the vector in place.
@@ -409,4 +409,38 @@ module 0x42::VerifyVector {
         ensures v == old(update(v,i,v[len(v)-1])[0..len(v)-1]);
         ensures old(v[i]) == result;
     }
+
+    fun vector_operator_in_function<Element: copy + drop>(e1: Element, e2: Element, e3: Element): vector<Element> {
+        vector[e1, e2, e3]
+    }
+
+    fun spec_with_vector_operator<Element: copy + drop>(e1: Element, e2: Element, e3: Element): (vector<Element>, vector<Element>) {
+        let v0 = vector::empty();
+        let v3 = vector::empty();
+        vector::push_back(&mut v3, e1);
+        spec {
+            assert v3 == vector[e1];
+        };
+        vector::push_back(&mut v3, e2);
+        spec {
+            assert v3 == vector[e1, e2];
+        };
+        vector::push_back(&mut v3, e3);
+        spec {
+            assert v3 == vector_operator_in_function(e1, e2, e3);
+        };
+        vector::push_back(&mut v3, e1);
+        spec {
+            assert v3 == vector[e1, e2, e3, e1];
+        };
+        vector::push_back(&mut v3, e2);
+        spec {
+            assert v3 == vector[e1, e2, e3, e1, e2];
+        };
+        (v3, v0)
+    }
+    spec spec_with_vector_operator {
+        ensures result_2 == vector[];
+        ensures result_1 == concat(vector_operator_in_function(e1, e2, e3), vector[e1, e2]);
+    }
 }