[move-prover] Package integration and dependency cleanup

This PR refines the integration of the Move prover into the CLI/package system as well as the Rust test infrastructure. As a result, dependencies from the move-prover crate into other crates outside of the
language tree are also eliminated.

The user level documentation is probably the best entrypoint into this work. See [here]() for the updated user guide. It describes how to call and configure the prover via the `package` command, and how to setup tests.

One design decision here is to let the package system always verify by default a package as a whole. This is generally faster if the intent is to actually verify all modules in the package, as in tests. When working from the command line one can, however, filter prover targets, for example as in `move package prover -t DiemConfig`. The string after the `-t` works as in cargo test.

The diem framework and move-stdlib have been updated to use the new prover test infra via the CLI. The prover unit tests, however, continue to use a customized test approach, because they have different requirementa (exp files etc).

This PR introduces breaking changes for Move prover users:

- After this PR, anybody calling the prover outside of the move-prover crate should go via the `move package prove` command, as documented in the user guide.
- If one calls the prover directly, **it will not longer** pick an environment variable `MOVE_PROVER_CONFIG`. If you need to do this, use `--config $MOVE_PROVER_CONFIG` explicitly.
  (But one really only needs to do this for running prover unit tests in the move-prover tree; see below)

For prover developers, the following changes:

- Running cargo test in `move-prover` does not longer test diem-framework or move-stdlib. Use `tools/check_pr.sh` to run all relevant Move tests.
- Tests in `move-prover/tests/sources` cannot depend longer on anything else than the Move stdlib.
- Checkout the updated [tests/README.md]() for running the prover on sources in the test tree.

The PR contains a lot of .exp changes in the move-prover/tests tree.  This is because the console output has changed, because Diem dependencies have been removed, and the .cvc4_exp files where out of date wrt from a PR last week (they are not run in CI).

Closes: aptos-labs#9844

diem-move/diem-framework/src/release.rs

@@ -142,6 +142,7 @@ fn generate_error_map(package_path: &Path, output_path: &Path, build_config: Bui
         .move_model_for_package(
             package_path,
             ModelConfig {
+                target_filter: None,
                 all_files_as_targets: true,
             },
         )

diem-move/diem-framework/tests/move_verification_test.rs

@@ -0,0 +1,19 @@
+// Copyright (c) The Diem Core Contributors
+// SPDX-License-Identifier: Apache-2.0
+
+use move_cli::package::prover::ProverTest;
+
+#[test]
+fn prove_core() {
+    ProverTest::create("core").run()
+}
+
+#[test]
+fn prove_experimental() {
+    ProverTest::create("experimental").run()
+}
+
+#[test]
+fn prove_dpn() {
+    ProverTest::create("DPN").run()
+}

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

@@ -121,16 +121,9 @@ impl<'env> BoogieTranslator<'env> {
 
         let mut translated_types = BTreeSet::new();
         let mut translated_funs = BTreeSet::new();
+        let mut verified_functions_count = 0;
+        info!("generating verification conditions");
         for module_env in self.env.get_modules() {
-            log!(
-                if !module_env.is_target() {
-                    Level::Debug
-                } else {
-                    Level::Info
-                },
-                "translating module {}",
-                module_env.get_name().display(module_env.symbol_pool())
-            );
             self.writer.set_location(&module_env.env.internal_loc());
 
             spec_translator.translate_spec_vars(&module_env, mono_info.as_ref());
@@ -164,6 +157,7 @@ impl<'env> BoogieTranslator<'env> {
                 }
                 for (variant, ref fun_target) in self.targets.get_targets(fun_env) {
                     if variant.is_verified() {
+                        verified_functions_count += 1;
                         // Always produce a verified functions with an empty instantiation such that
                         // there is at least one top-level entry points for a VC.
                         FunctionTranslator {
@@ -190,6 +184,7 @@ impl<'env> BoogieTranslator<'env> {
                                 continue;
                             }
 
+                            verified_functions_count += 1;
                             FunctionTranslator {
                                 parent: self,
                                 fun_target,
@@ -224,6 +219,7 @@ impl<'env> BoogieTranslator<'env> {
         }
         // Emit any finalization items required by spec translation.
         self.spec_translator.finalize();
+        info!("{} verification conditions", verified_functions_count);
     }
 }
 

language/move-prover/bytecode/src/function_target_pipeline.rs

@@ -9,7 +9,7 @@ use crate::{
 };
 use core::fmt;
 use itertools::Itertools;
-use log::debug;
+use log::{debug, info};
 use move_model::model::{FunId, FunctionEnv, GlobalEnv, QualifiedId};
 use std::{collections::BTreeMap, fmt::Formatter, fs};
 
@@ -359,7 +359,7 @@ impl FunctionTargetPipeline {
         H2: Fn(usize, &dyn FunctionTargetProcessor, &FunctionTargetsHolder),
     {
         let topological_order = Self::sort_targets_in_topological_order(env, targets);
-
+        info!("transforming bytecode");
         hook_before_pipeline(targets);
         for (step_count, processor) in self.processors.iter().enumerate() {
             if processor.is_single_run() {

language/move-prover/doc/user/prover-guide.md

@@ -1,59 +1,144 @@
-# Move Prover User Guide (DRAFT)
+# Move Prover User Guide
 
 This is the user guide for the Move prover. This document does not describe the
 [Move specification language](spec-lang.md), but accompanies it.
 
-This guide is currently specific for the usage of the prover within the Diem repo.
+- [Running the Prover](#running-the-prover)
+    - [Target Filtering](#target-filtering)
+    - [Prover Options](#prover-options)
+    - [Prover Configuration File](#prover-configuration-file)
+    - [Prover Tests](#prover-tests)
+- [Prover Diagnosis](#prover-diagnosis)
+    - [Unexpected Abort](#unexpected-abort)
+    - [Postcondition Failure](#postcondition-failure)
+- [Debugging the Prover](#debugging-the-prover)
 
 ## Running the Prover
 
-To run the Move prover while working in the Diem tree, we recommend to use `cargo run`. You can define an alias
-as below in your `.bashrc` (or other shell configuration) to simplify this:
+The prover is invoked via the Move CLI. When working in a repo which contains the CLI, you can make it available via an
+alias as below:
 
 ```shell script
-alias mvp="cargo run --release --quiet --package move-prover --"
+alias move="cargo run --release --quiet --package move-cli --"
 ```
 
-The `--release` flag can also be omitted if you prefer faster compilation over faster execution. However, once the
-prover has been build by cargo, and provided sources have not changed, the cargo command will quickly proceed.
-Note that the Rust code of the prover (and the underlying Move compiler) is by about a factor of 20 faster in
-release mode than in debug mode.
+> NOTE: The `--release` flag can also be omitted if you prefer faster compilation over faster execution. Note, however,
+> that the Rust code part of the prover (and the underlying Move compiler) is by an order of magnitude faster
+> in release mode than in debug mode.
 
-In the sequel, we assume that `mvp` invokes the binary of the prover, either via an alias as above, or by
-other means.
+We assume in the sequel that the Move CLI is reachable from the command line via the `move` command
+(defined by an alias as above or by other means).
 
-## Command Line Interface
+In order to call the CLI, you must have a [*move package*](https://diem.github.io/move/packages.html). In the simplest
+case, a Move package is defined by a directory with a set of `.move` files in it and a manifest of the name `Move.toml`.
+You can create a package `<name>` in a sub-directory by calling `move package new <name>`.
 
-The Move prover has a traditional compiler-style command line interface: you pass a set of sources, tell it where to
-look for dependencies of those sources, and optionally provide flags to control operation:
+Now, to call the prover simply use one of the following commands:
 
 ```shell script
-> mvp --dependency . source.move
-> # Short form:
-> mvp -d . source.move
+move package -p <path> prove  # Prove the sources of the package at <path>
+move package prove            # Equivalent to move `package -p . prove`
 ```
 
-Above, we process a file `source.move` in the current directory, and tell the prover to look up any dependencies this source
-might have in the current directory (`.`). If verification succeeds, the prover will terminate with printing
-some statistics dependent on the configured verbosity level. Otherwise, it will print diagnosis, as will be
-discussed below.
+### Target Filtering
 
-## Configuration File
+By default, the `prove` command verifies all files of a package. During iterative development of larger packages, it is
+often more effective to focus verification on particular files. You do this with the
+`-t` (`--target`) option:
 
-All options available via the command line, plus some more, can be also configured via a file. Moreover, you can
-set an environment variable which contains a path to the default configuration file the prover should use. This is handy,
-for example, to let the prover automatically find dependencies to the Move standard library, as shown below:
+```shell script
+move package prove -t DiemConfig
+```
+
+In general, if the string provided via the `-t` option is contained somewhere in the file name of a source, that source
+will be included for verification.
+
+> NOTE: the Move prover ensures that there is no semantic difference between verifying modules one-by-one
+> or all at once. However, if your goal is to verify all modules, verifying them in a single
+> `move package prove` run will be significantly faster then sequentially.
+
+### Prover Options
+
+The prover has a number of options which are not directly handled by the CLI but rather passed through. You pass options
+through with an invocation like `move package prove -- <options>`. The most commonly used option is the `-t` (`--trace`)
+option which lets the prover produce richer diagnosis when it encounters errors:
 
 ```shell script
-> echo "move_deps = [\"<path-to-diem>/diem-move/diem-framework/core/sources\"]" > ~/.mvprc
-> export MOVE_PROVER_CONFIG=~/.mvprc
+move package prove -t DiemConfig -- -t
+```
+
+To see the list of all command line options, use `move package prove -- --help`.
+
+### Prover Configuration File
+
+You can also create a prover configuration file, named `Prover.toml` which lives side-by-side with the `Move.toml`
+file. For example, to enable tracing by default for a package, you use a `Prover.toml` with the following content:
+
+```toml
+[prover]
+auto_trace_level = "VerifiedFunction"
+```
+
+The most commonly used options are documented by the example toml below, which you can cut and paste and adopt for your
+needs (the displayed values are the defaults):
+
+```toml
+# Verbosity level
+# Possible values: "ERROR", "WARN", "INFO", "DEBUG". Each level subsumes the output of the previous one.
+verbosity_level = "INFO"
+
+[prover]
+# Set auto-tracing level, which enhances the diagnosis the prover produces on verification errors.
+# Possible values: "Off", "VerifiedFunction", "AllFunctions"
+auto_trace_level = "Off"
+
+# Minimal severity level for diagnosis to be reported.
+# Possible values: "Error", "Warning", "Note"
+report_severity = "Warning"
+
+[backend]
+# Timeout in seconds for the solver backend. Note that this is a soft timeout and may not always
+# be respected.
+vc_timeout = 40
+
+# Random seed for the solver backend. Different seeds can result in different verification run times,
+# as the solver uses heuristics.
+random_seed = 1
+
+# The number of processors cores to assume for concurrent check of verification conditions.
+proc_cores = 4
 ```
 
-To see the full format of the configuration file use `mvp --print-config`. This will print out the toml for
-all available options. You can use this output as a blueprint for creating your own configuration
-file.
+> HINT: for local verification, you may want to set proc_cores to an aggressive number
+> (your actual cores) to speed up the turn-around cycle.
+
+> NOTE: To let the prover dump all the available toml options, use `move package prove -- --print-config`. This
+> will, however, contain many more unrelated and potentially defunct experimental options.
+
+## Prover Tests
 
-## Diagnosis
+The prover can be run from a Rust testsuite, for example to use verification as a submit blocker. To do so, add a Rust
+file to the Rust testsuite (e.g. `<crate>/tests/move_verification_test.rs`). Assume the Rust crate contains two Move
+packages at relative paths, from the crate root,`foo` and `bar`, then your Rust source would contain:
+
+```rust
+use move_cli::package::prover::ProverTest;
+
+#[test]
+fn prove_foo() {
+    ProverTest::create("foo").run()
+}
+
+#[test]
+fn prove_bar() {
+    ProverTest::create("bar").run()
+}
+```
+
+There are multiple ways how you can configure tests, for example, setting specific options for the prover to use. See
+the `ProverTest` type for details.
+
+## Prover Diagnosis
 
 When the prover finds a verification error it prints out diagnosis in a style similar to a compiler or a debugger. We
 explain the different types of diagnoses below, based on the following evolving example:
@@ -103,10 +188,10 @@ error: abort not covered by any of the `aborts_if` clauses
    =     at tutorial.move:8:17: increment (ABORTED)
 ```
 
-The prover has generated a counter example which leads to an overflow when adding 1 the value of 255 for an `u8`.
-This happens if the function specification states something abort abort behavior, but the condition under which
-the function is aborting is not covered by the specification. And in fact, with `aborts_if !exists<Counter>(a)` we
-only cover the abort if the resource does not exists, but not the overflow.
+The prover has generated a counter example which leads to an overflow when adding 1 the value of 255 for an `u8`. This
+happens if the function specification states something abort abort behavior, but the condition under which the function
+is aborting is not covered by the specification. And in fact, with `aborts_if !exists<Counter>(a)` we only cover the
+abort if the resource does not exists, but not the overflow.
 
 Let's fix the above and add the following condition:
 
@@ -118,7 +203,7 @@ spec increment {
 
 With this, the prover will succeed without any errors.
 
-### Postcondition might not hold
+### Postcondition Failure
 
 Let us inject an error into the `ensures` condition of the above example:
 
@@ -149,52 +234,25 @@ error:  A postcondition might not hold on this return path.
 ```
 
 While we know what the error is (we just injected it), looking at the printed information makes it not particular
-obvious. This is because we don't directly see on which values the `ensures` condition was actually evaluated. To
-inspect those, we have two options. First, we can run the prover with the `--trace` option. The output then
-looks as below:
-
-```
-error:  A postcondition might not hold on this return path.
-
-    ┌── tutorial.move:14:7 ───
-    │
- 14 │       ensures global<Counter>(a).value == global<Counter>(a).value + 1;
-    │       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-    ·
- 12 │       aborts_if !exists<Counter>(a);
-    │                                  - 0x5
-    ·
- 12 │       aborts_if !exists<Counter>(a);
-    │                  ------------------ true
-    ·
- 14 │       ensures global<Counter>(a).value == global<Counter>(a).value + 1;
-    │               ------------------ M.Counter{value = 244u8}
-    ·
- 14 │       ensures global<Counter>(a).value == global<Counter>(a).value + 1;
-    │                                           ------------------ M.Counter{value = 244u8}
-    │
-    =     at tutorial.move:6:3: increment (entry)
-    =     at tutorial.move:7:15: increment
-    =         a = 0x5,
-    =         r = &M.Counter{value = 243u8}
-    =     at tutorial.move:8:17: increment
-    =         r = &M.Counter{value = 243u8}
-    =     at tutorial.move:6:3: increment
-    =     at tutorial.move:6:3: increment (exit)
-```
+obvious. This is because we don't directly see on which values the `ensures` condition was actually evaluated. To see
+this, use the `-t` (`--trace`) option; this is not enabled by default because it makes the verification problem slightly
+harder for the solver.
 
-> Note: the `--trace` option is currently known to sometimes produce false positives.
+Instead or in addition to the `--trace` option, one can also use the builtin function `TRACE(exp)` in conditions to
+explicitly mark expressions whose value should be printed on verification failures.
 
-Instead of the `--trace` option, one can also use the builtin function `TRACE(exp)` in conditions to explicitly
-mark expressions whose value should be printed on verification failures.
+> NOTE: expressions which depend on quantified symbols cannot be traced. Also, expressions appearing in
+> specification functions can currently not be traced.
 
-## Debugging
+## Debugging the Prover
 
-The Move prover is still an evolving tool with bugs and deficiencies. Sometimes it might be necessary to debug
-a problem based on the output it passes to the underlying backends. There are two options to this end:
+The Move prover is an evolving tool with bugs and deficiencies. Sometimes it might be necessary to debug a problem based
+on the output it passes to the underlying backends. There are the following options to this end:
 
-- By default, the prover will place the generated Boogie code in a file `output.bpl`, and the errors Boogie reported
-  in a file `output.bpl.log`.
-- With the option `-C backend.generate_smt=true` the prover will generate, for each verification problem, a file in
-  the smtlib format. The file is named after the verified function. This file contains the output Boogie
-  passes on to Z3 or other connected SMT solvers.
+- If you prove the option `-k` (`--keep`), the prover will place the generated Boogie code in a file `output.bpl`, and
+  the errors Boogie reported in a file `output.bpl.log`.
+- If you prove the option `--dump-bytecode`, the prover will dump the original Move bytecode as well as the Prover
+  bytecode as it is transformed during compilation.
+- With the option `-C backend.generate_smt=true` the prover will generate, for each verification problem, a file in the
+  smtlib format. The file is named after the verified function. This file contains the output Boogie passes on to Z3 or
+  other connected SMT solvers.

language/move-prover/docgen/tests/testsuite.rs

@@ -18,7 +18,7 @@ use std::{fs::File, io::Read};
 const FLAGS: &[&str] = &[
     "--verbose=warn",
     "--dependency=../../move-stdlib/sources",
-    "--dependency=../../../diem-move/diem-framework/core/sources",
+    "--named-addresses=Std=0x1",
     "--docgen",
 ];