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

Issue:
[Bug][Compiler][Move prover] A non-mutable reference parameter is translated into $Mutation type in a specification function 
# 🐛 Bug

When generating a specification function `spec fun spec_point_compress_internal(point: &RistrettoPoint): vector<u8>;` into the boogie code, the non-mutable reference parameter is mistakenly translated into a $Mutation type:

```
function  $1_ristretto255_spec_point_compress_internal(point: $Mutation ($1_ristretto255_RistrettoPoint)): Vec (int);
axiom (forall point: $Mutation ($1_ristretto255_RistrettoPoint) ::
(var $$res := $1_ristretto255_spec_point_compress_internal(point);
$IsValid'vec'u8''($$res)));
```



Discussion / hints:

Fix patch:
diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index 2f28614bdcd86..e6e1f65ff313f 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -767,6 +767,13 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
     ) {
         let name = self.symbol_pool().make(&name.0.value);
         let (type_params, params, result_type) = self.decl_ana_signature(signature, false);
+        // Eliminate references in parameters and result type for spec functions
+        // `derive_spec_fun` does the same when generating spec functions from general move functions
+        let params = params
+            .into_iter()
+            .map(|Parameter(sym, ty, loc)| Parameter(sym, ty.skip_reference().clone(), loc))
+            .collect_vec();
+        let result_type = result_type.skip_reference().clone();
 
         // Add the function to the symbol table.
         let fun_id = SpecFunId::new(self.spec_funs.len());


Test patch:
diff --git a/third_party/move/move-prover/tests/sources/functional/bug_10784.move b/third_party/move/move-prover/tests/sources/functional/bug_10784.move
new file mode 100644
index 0000000000000..ee8b38acdfa38
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bug_10784.move
@@ -0,0 +1,26 @@
+module 0x42::m {
+
+    struct RistrettoPoint has drop {
+        handle: u64
+    }
+
+    struct CompressedRistretto has copy, store, drop {
+        data: vector<u8>
+    }
+
+    native fun point_compress_internal(point: &RistrettoPoint): vector<u8>;
+
+    spec fun spec_point_compress_internal(point: &RistrettoPoint): vector<u8>;
+
+    spec point_compress_internal(point: &RistrettoPoint): vector<u8> {
+        pragma opaque;
+        ensures result == spec_point_compress_internal(point);
+    }
+
+    public fun point_compress(point: &RistrettoPoint): CompressedRistretto {
+        CompressedRistretto {
+            data: point_compress_internal(point)
+        }
+    }
+
+}