[compiler-v2][prover] Move prover blows up for emojicoin arena package even without any specs #15605
Labels
bug
Something isn't working
Comments
|
This might be an instance of #14205, which we thought was fixed. I can reduce this back to the use of TypeParamInfo in specification functions. This is done by |
wrwg
added a commit
that referenced
this issue
Dec 15, 2024
When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now. Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.
wrwg
added a commit
that referenced
this issue
Dec 15, 2024
When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now. Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.
wrwg
added a commit
that referenced
this issue
Dec 16, 2024
…15606) When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now. Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.
|
I added some more tracing output to identify the functions which are actually verified and it appears we are hitting a Boogie bug. In an upcoming PR, one can see with The many variants via type instantiations are a result of the provers monormphization technique. In order to prove the properties of a generic function to universally hold in the current known program, it proves it for a number of instantiations. This makes the code here explode a bit. However, the problem is truly in boogie. After the boogie command is launched above, the process hangs, and no z3 process ever comes up, it appears. |
3 tasks
wrwg
added a commit
that referenced
this issue
Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
|
In PR #15636 benchmarking functionality is added to Raw data: The problem isn't solved but now we have at least better indication for this and future examples what goes wrong. |
wrwg
added a commit
that referenced
this issue
Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
|
Filed an issue on boogie github repo: boogie-org/boogie#993 |
|
I now also connected verification scoping to the Aptos CLI in #15636. Now with |
wrwg
added a commit
that referenced
this issue
Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
wrwg
added a commit
that referenced
this issue
Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
wrwg
added a commit
that referenced
this issue
Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
wrwg
added a commit
that referenced
this issue
Dec 20, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
georgemitenkov
pushed a commit
that referenced
this issue
Jan 6, 2025
…15606) When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now. Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.
georgemitenkov
pushed a commit
that referenced
this issue
Jan 6, 2025
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
@brmataptos @fEst1ck @georgemitenkov @gregnazario @rahxephon89 @runtian-zhou @vineethk @wrwg
I originally though that maybe I had an issue with a global invariant as per econia-labs/emojicoin-dot-fun#408 (comment), however it turns out that even without any specs whatsoever the prover blows up for the given package. To reproduce:
aptos move prove --dev --move-2[INFO] preparing module 0xaaa::pseudo_randomness [INFO] preparing module 0xaaa::emojicoin_arena [INFO] transforming bytecode [INFO] generating verification conditions [INFO] 50 verification conditions [INFO] running solver { "Error": "Move Prover failed: [internal] boogie exited with compilation errors:\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32395,288): Error: cannot refer to a global variable in this context: #1_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32395,300): Error: cannot refer to a global variable in this context: #1_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32395,312): Error: cannot refer to a global variable in this context: #1_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32395,462): Error: cannot refer to a global variable in this context: #1_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32395,474): Error: cannot refer to a global variable in this context: #1_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32395,486): Error: cannot refer to a global variable in this context: #1_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32400,288): Error: cannot refer to a global variable in this context: #2_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32400,300): Error: cannot refer to a global variable in this context: #2_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32400,312): Error: cannot refer to a global variable in this context: #2_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32400,462): Error: cannot refer to a global variable in this context: #2_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32400,474): Error: cannot refer to a global variable in this context: #2_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32400,486): Error: cannot refer to a global variable in this context: #2_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32405,288): Error: cannot refer to a global variable in this context: #3_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32405,300): Error: cannot refer to a global variable in this context: #3_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32405,312): Error: cannot refer to a global variable in this context: #3_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32405,462): Error: cannot refer to a global variable in this context: #3_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32405,474): Error: cannot refer to a global variable in this context: #3_info\n/Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl(32405,486): Error: cannot refer to a global variable in this context: #3_info\n18 name resolution errors detected in /Users/yours-truly/repos/emojicoin-dot-fun/src/move/emojicoin_arena/boogie.bpl\n" }The text was updated successfully, but these errors were encountered: