[Bug][move-compiler-v2] move-prover tests timeout more with MOVE_COMPILER_V2=true after PR#13184

[brmataptos]

🐛 Bug

PR #13184 fixes many things but seems to increase timeouts in move-prover tests with MOVE_COMPILER_V2=true. This is likely due to attempts to prove things about library dependencies, since the timeouts were accompanied by poiters to the function std::fixed_point32::round(), although the exact cause is unclear. This was temporarily worked around by the following change to move-stdlib:

diff --git a/third_party/move/move-stdlib/sources/fixed_point32.move b/third_party/move/move-stdlib/sources/fixed_point32.move
index d756ae2825..b3edc4dc5d 100644
--- a/third_party/move/move-stdlib/sources/fixed_point32.move
+++ b/third_party/move/move-stdlib/sources/fixed_point32.move
@@ -271,6 +271,7 @@ module std::fixed_point32 {
         }
     }
     spec round {
+        pragma verify=false; // TODO(13186): fix this.
         pragma opaque;
         pragma timeout = 120;
         aborts_if false;

This needs more investigation. It seems likely that the assignment of input files to "primary target sources", "non-primary target sources" and "dependences" is somehow incorrect in the move-prover case.

[brmataptos]

@rahxephon89 fyi

[brmataptos]

@wrwg fyi

[brmataptos]

This issue originally also mentioned a different test output difference that appeared after PR#13184, but this has been removed from the issue summary after some more study. Here is a little discussion:

The first error mentioned related to some checks for modules with identical names if letter case is ignored:

• third_party/move/tools/move-package/tests/test_sources/compilation/case_insensitive_check/Move.v2_exp loses some errors

This seems to be a harmless difference. Firstly, it's not clear what is the motivation for this concern, but as a build of a package produces a file foo.mv for each module foo, it seems reasonable to be concerned about conflicts that might show up on case-insensitive platforms (e.g., Windows) but not others. Apparently packages compiled with V1 see script functions compared to module names in this process, which can lead to some errors which don't seem valid. V2 does not see such conflicts, although it might see conflicts between identical module names with different addresses in some other context, but that's a different error.

The detailed change here is captured by he following diff:

*** third_party/move/tools/move-package/tests/test_sources/compilation/case_insensitive_check/Move.exp  Fri May  3 23:15:50 2024
--- third_party/move/tools/move-package/tests/test_sources/compilation/case_insensitive_check/Move.v2_exp   Fri May  3 23:15:43 2024
***************
*** 1,11 ****
  Module and/or script names found that would cause failures on case insensitive file systems when compiling package 'case_insensitive_check':
- The following modules and/or scripts would collide as 'a' on the file system:
-   Module 'A' at path 'tests/test_sources/compilation/case_insensitive_check/sources/a.move'
-   Script 'a' at path 'tests/test_sources/compilation/case_insensitive_check/sources/a_script.move'
  The following modules and/or scripts would collide as 'set' on the file system:
    Module 'Set' at path 'tests/test_sources/compilation/case_insensitive_check/sources/Set.move'
    Module 'set' at path 'tests/test_sources/compilation/case_insensitive_check/sources/foo.move'
    Module 'seT' at path 'tests/test_sources/compilation/case_insensitive_check/sources/otherModule.move'
-   Script 'sEt' at path 'tests/test_sources/compilation/case_insensitive_check/sources/script.move'
  Please rename these scripts and/or modules to resolve these conflicts.
--- 1,6 ----

The difference comes down to the use of script functions, and their potential conflict with modules due to case insensitivity. This shouldn't be an issue with V2 as scripts and functions are canonicalized.

I'm renaming this issue and changing the summary to focus on the move-prover timeouts with MOVE_COMPILER_V2.

[rahxephon89]

Hi @brmataptos, I tried using aptos move prove against framework code but could not see the difference on the verification target between V1 and V2.

[brmataptos]

If you undo the fix mentioned above in fixed_point32.move

+        pragma verify=false; // TODO(13186): fix this.

then you can see timeouts in several tests. Actually, even with that fix we see timeouts in some .v2_exp files which aren't in the corresponding .exp files for move-prover. For example, I'm seeing it in

./third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp

but I'm unfamiliar with how to debug this situation. How can I see the full boogie input/output for these test cases (e.g., for V1 and V2)?

Are there "debugging move-prover" best practices that could be shared in our doc?

[brmataptos]

Fixed by #13270