[Prover] Use compiler V2 by default in Move prover (#14948)

* using compiler V2 by default in prover

* compiler v2 latest

aptos-move/framework/tests/move_prover_tests.rs

@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0
 
 use aptos_framework::{extended_checks, prover::ProverOptions};
+use move_binary_format::file_format_common::VERSION_DEFAULT;
+use move_model::metadata::{CompilerVersion, LanguageVersion};
 use std::{collections::BTreeMap, path::PathBuf};
 
 const ENV_TEST_INCONSISTENCY: &str = "MVP_TEST_INCONSISTENCY";
@@ -57,9 +59,9 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into<String>) {
                 false,
                 pkg_path.as_path(),
                 BTreeMap::default(),
-                None,
-                None,
-                None,
+                Some(VERSION_DEFAULT),
+                Some(CompilerVersion::latest_stable()),
+                Some(LanguageVersion::latest_stable()),
                 skip_attribute_checks,
                 extended_checks::get_all_attribute_names(),
                 &[],

aptos-move/move-examples/Cargo.toml

@@ -19,6 +19,7 @@ aptos-types = { workspace = true }
 aptos-vm ={ workspace = true, features = ["testing"] }
 clap = { workspace = true }
 move-cli = { workspace = true }
+move-model = { workspace = true }
 move-package = { workspace = true }
 move-prover = { workspace = true }
 move-unit-test = { workspace = true }

aptos-move/move-examples/tests/move_prover_tests.rs

@@ -4,6 +4,7 @@
 use aptos_framework::extended_checks;
 use aptos_types::account_address::AccountAddress;
 use move_cli::base::prove::run_move_prover;
+use move_model::metadata::{CompilerVersion, LanguageVersion};
 use move_package::CompilerConfig;
 use std::{collections::BTreeMap, path::PathBuf};
 use tempfile::tempdir;
@@ -28,6 +29,8 @@ pub fn run_prover_for_pkg(
         install_dir: Some(tempdir().unwrap().path().to_path_buf()),
         compiler_config: CompilerConfig {
             known_attributes: extended_checks::get_all_attribute_names().clone(),
+            compiler_version: Some(CompilerVersion::latest_stable()),
+            language_version: Some(LanguageVersion::latest_stable()),
             ..Default::default()
         },
         ..Default::default()

crates/aptos/CHANGELOG.md

@@ -7,6 +7,7 @@ All notable changes to the Aptos CLI will be captured in this file. This project
 - Add `aptos update prover-dependencies`, which installs the dependency of Move prover, boogie, z3 and cvc5.
 - Update the default version of `movefmt` to be installed from 1.0.4 to 1.0.5
 - Update the local-testnet logs to use `println` for regular output and reserve `eprintln` for errors.
+- Set compiler V2 as default when using `aptos move prove`.
 
 ## [4.2.3] - 2024/09/20
 - Fix the broken indexer in localnet in 4.2.2, which migrates table info from sycn to async ways.

crates/aptos/src/move_tool/mod.rs

@@ -644,14 +644,21 @@ impl CliCommand<&'static str> for ProvePackage {
             prover_options,
         } = self;
 
+        let compiler_version = move_options
+            .compiler_version
+            .or_else(|| Some(CompilerVersion::latest_stable()));
+        let language_version = move_options
+            .language_version
+            .or_else(|| Some(LanguageVersion::latest_stable()));
+
         let result = task::spawn_blocking(move || {
             prover_options.prove(
                 move_options.dev,
                 move_options.get_package_path()?.as_path(),
                 move_options.named_addresses(),
-                fix_bytecode_version(move_options.bytecode_version, move_options.language_version),
-                move_options.compiler_version,
-                move_options.language_version,
+                fix_bytecode_version(move_options.bytecode_version, language_version),
+                compiler_version,
+                language_version,
                 move_options.skip_attribute_checks,
                 extended_checks::get_all_attribute_names(),
                 &[],

third_party/move/move-model/src/metadata.rs

@@ -145,6 +145,16 @@ impl CompilerVersion {
         }
     }
 
+    /// The latest compiler version.
+    pub fn latest() -> Self {
+        CompilerVersion::V2_1
+    }
+
+    /// The latest stable compiler version.
+    pub fn latest_stable() -> Self {
+        CompilerVersion::V2_0
+    }
+
     /// Check whether the compiler version supports the given language version,
     /// generates an error if not.
     pub fn check_language_support(self, version: LanguageVersion) -> anyhow::Result<()> {
@@ -236,6 +246,16 @@ impl LanguageVersion {
         }
     }
 
+    /// The latest language version.
+    pub fn latest() -> Self {
+        LanguageVersion::V2_1
+    }
+
+    /// The latest stable language version.
+    pub fn latest_stable() -> Self {
+        LanguageVersion::V2_0
+    }
+
     /// Whether the language version is equal to greater than `ver`
     pub fn is_at_least(&self, ver: LanguageVersion) -> bool {
         *self >= ver

third_party/move/tools/move-cli/src/base/prove.rs

@@ -6,8 +6,9 @@ use anyhow::bail;
 use clap::Parser;
 use codespan_reporting::term::termcolor::{ColorChoice, StandardStream};
 use colored::Colorize;
+use move_model::metadata::{CompilerVersion, LanguageVersion};
 use move_package::{BuildConfig, ModelConfig};
-use move_prover::run_move_prover_with_model;
+use move_prover::run_move_prover_with_model_v2;
 use std::{
     io::Write,
     path::{Path, PathBuf},
@@ -127,7 +128,10 @@ impl ProverTest {
             for_test: true,
             options: Some(ProverOptions::Options(std::mem::take(&mut self.options))),
         };
-        let res = cmd.execute(Some(pkg_path), move_package::BuildConfig::default());
+        let mut build_config = BuildConfig::default();
+        build_config.compiler_config.language_version = Some(LanguageVersion::latest_stable());
+        build_config.compiler_config.compiler_version = Some(CompilerVersion::latest_stable());
+        let res = cmd.execute(Some(pkg_path), build_config);
         std::env::set_current_dir(saved_cd).expect("restore current directory");
         res.unwrap()
     }
@@ -212,7 +216,7 @@ pub fn run_move_prover(
     } else {
         None
     };
-    let res = run_move_prover_with_model(&mut model, &mut error_writer, options, Some(now));
+    let res = run_move_prover_with_model_v2(&mut model, &mut error_writer, options, now);
     if for_test {
         let basedir = path
             .file_name()