[Move Prover][trivial] Eliminate reference in parameters and result t…

…ype for spec functions (#15190)

* remove ref for spec fun

* add test

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());

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)
+        }
+    }
+
+}