Error when adding MSL specs to sui-framework modules

[rockbmb]

This is related to sui move prove like #14325 and #14337, although unlike those 2 it directly concerns the output of that command for a concrete MSL spec, instead of being an issue with the CLI.

I was attempting to contribute specifications to the ./crates/sui-framework/packages/sui-framework/sources/vec_map.move module for the VecMap type for use as a downstream consumer, but this issue occurred.

Steps to Reproduce Issue

1. Run ./crates/sui-framework/packages/sui-framework/
2. Add the following to sources/vec_map.move

   spec get_idx_opt {
   // intentionally empty
   }
   

3. Execute sui move prove -- --verify-only vec_map::get_idx_opt

Expected Result

The verification command should succeed, outputting a newline to the terminal:

$ sui move prove -- --verify-only vec_map::get_idx_opt
$

Actual Result

The following Boogie error is raised:

[internal] boogie exited with compilation errors:
output.bpl(4125,32): Error: undeclared type: $2_object_UID
output.bpl(4130,32): Error: undeclared type: $2_object_UID
2 name resolution errors detected in output.bpl

The output.bpl file with the relevant information will be present in ./crates/sui-framework/packages/sui-framework/.

System Information

$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description: Ubuntu 20.04.6 LTS
Release: 20.04
Codename: focal

$ rustc --version
rustc 1.73.0 (cc66ad468 2023-10-03)

$ sui --version
sui 1.12.0-1b5f809a1

[rockbmb]

@awelc this is the third issue I've submitted regarding sui move prove - I have to apologize for this.
I understand that this has a low priority, and that work on the Move Prover is frozen for now.

Of course, I didn't just want to open these issues and walk away - I am willing to help implement fixes for them.

[awelc]

@awelc this is the third issue I've submitted regarding sui move prove - I have to apologize for this. I understand that this has a low priority, and that work on the Move Prover is frozen for now.

Of course, I didn't just want to open these issues and walk away - I am willing to help implement fixes for them.

Thank you for all the reports! As you correctly observed, the work we can be currently doing on Move Prover support for Sui is limited. My apologies for the late response but I have been traveling recently (and also wanted to land this PR that would make the current state of affairs more explicit for those trying Move Prover with Sui).

That being said, we would be happy to welcome external contributions to improve the current level of Move Prover support for Sui, and I would be happy to review them (to the best of my abilities!).

[rockbmb]

Support for the prover is being sunset, so this can be closed; see #15480