Fixed the display of signer values in the error trace in Prover

- This PR fixes the signer value display in the error trace.

For example,
```
  =     at signer_display.move:5: f_incorrect
  =         account = signer{0x2}
```

Closes: aptos-labs#8989

language/move-prover/boogie-backend/src/boogie_wrapper.rs

@@ -954,10 +954,18 @@ impl ModelValue {
                     .and_then(|s| s.parse::<bool>().ok())?
                     .to_string(),
             )),
-            Type::Primitive(PrimitiveType::Address) | Type::Primitive(PrimitiveType::Signer) => {
+            Type::Primitive(PrimitiveType::Address) => {
                 let addr = BigInt::parse_bytes(&self.extract_literal()?.clone().into_bytes(), 10)?;
                 Some(PrettyDoc::text(format!("0x{}", &addr.to_str_radix(16))))
             }
+            Type::Primitive(PrimitiveType::Signer) => {
+                let l = self.extract_list("$signer")?;
+                let addr = BigInt::parse_bytes(&l[0].extract_literal()?.clone().into_bytes(), 10)?;
+                Some(PrettyDoc::text(format!(
+                    "signer{{0x{}}}",
+                    &addr.to_str_radix(16)
+                )))
+            }
             Type::Vector(param) => self.pretty_vector(wrapper, model, param),
             Type::Struct(module_id, struct_id, params) => {
                 self.pretty_struct(wrapper, model, *module_id, *struct_id, params)

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

@@ -0,0 +1,10 @@
+Move prover returns: exiting with boogie verification errors
+error: unknown assertion failed
+  ┌─ tests/sources/functional/signer_display.move:7:13
+  │
+7 │             assert Signer::spec_address_of(account) == @0x1;
+  │             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  │
+  =     at tests/sources/functional/signer_display.move:5: f_incorrect
+  =         account = <redacted>
+  =     at tests/sources/functional/signer_display.move:7: f_incorrect

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

@@ -0,0 +1,10 @@
+module 0x42::SignerDisplay {
+    use Std::Signer;
+
+    // Test the signer value display in the error trace
+    fun f_incorrect(account: &signer) {
+        spec {
+            assert Signer::spec_address_of(account) == @0x1;
+        }
+    }
+}