remove v1 in prover

aptos-labs · Feb 8, 2025 · ac2e834 · ac2e834
1 parent b421423
commit ac2e834
Show file tree

Hide file tree

Showing 133 changed files with 353 additions and 4,564 deletions.
diff --git a/aptos-move/framework/src/prover.rs b/aptos-move/framework/src/prover.rs
@@ -10,7 +10,7 @@ use codespan_reporting::{
 use log::{info, LevelFilter};
 use move_core_types::account_address::AccountAddress;
 use move_model::{
-    metadata::{CompilerVersion, LanguageVersion},
+    metadata::LanguageVersion,
     model::{GlobalEnv, VerificationScope},
 };
 use move_prover::cli::Options;
@@ -136,7 +136,6 @@ impl ProverOptions {
         package_path: &Path,
         named_addresses: BTreeMap<String, AccountAddress>,
         bytecode_version: Option<u32>,
-        compiler_version: Option<CompilerVersion>,
         language_version: Option<LanguageVersion>,
         skip_attribute_checks: bool,
         known_attributes: &BTreeSet<String>,
@@ -151,7 +150,7 @@ impl ProverOptions {
             named_addresses,
             self.filter.clone(),
             bytecode_version,
-            compiler_version,
+            None,
             language_version,
             skip_attribute_checks,
             known_attributes.clone(),
@@ -160,13 +159,6 @@ impl ProverOptions {
         let mut options = self.convert_options(package_path)?;
         options.language_version = language_version;
         options.model_builder.language_version = language_version.unwrap_or_default();
-        if compiler_version.unwrap_or_default() >= CompilerVersion::V2_0
-            || language_version
-                .unwrap_or_default()
-                .is_at_least(LanguageVersion::V2_0)
-        {
-            options.compiler_v2 = true;
-        }
         // Need to ensure a distinct output.bpl file for concurrent execution. In non-test
         // mode, we actually want to use the static output.bpl for debugging purposes
         let _temp_holder = if for_test {
@@ -195,16 +187,7 @@ impl ProverOptions {
             run_prover_benchmark(package_path, &mut model, options)?;
         } else {
             let mut writer = StandardStream::stderr(ColorChoice::Auto);
-            if compiler_version.unwrap_or_default() == CompilerVersion::V1 {
-                move_prover::run_move_prover_with_model(
-                    &mut model,
-                    &mut writer,
-                    options,
-                    Some(now),
-                )?;
-            } else {
-                move_prover::run_move_prover_with_model_v2(&mut model, &mut writer, options, now)?;
-            }
+            move_prover::run_move_prover_with_model_v2(&mut model, &mut writer, options, now)?;
         }
         Ok(())
     }

diff --git a/aptos-move/framework/tests/move_prover_tests.rs b/aptos-move/framework/tests/move_prover_tests.rs
@@ -3,7 +3,7 @@
 
 use aptos_framework::{extended_checks, prover::ProverOptions};
 use move_binary_format::file_format_common::VERSION_DEFAULT;
-use move_model::metadata::{CompilerVersion, LanguageVersion};
+use move_model::metadata::LanguageVersion;
 use std::{collections::BTreeMap, path::PathBuf};
 
 const ENV_TEST_INCONSISTENCY: &str = "MVP_TEST_INCONSISTENCY";
@@ -67,7 +67,6 @@ pub fn run_prover_for_pkg(
                 pkg_path.as_path(),
                 BTreeMap::default(),
                 Some(VERSION_DEFAULT),
-                Some(CompilerVersion::latest_stable()),
                 Some(LanguageVersion::latest_stable()),
                 skip_attribute_checks,
                 extended_checks::get_all_attribute_names(),

diff --git a/crates/aptos/src/move_tool/mod.rs b/crates/aptos/src/move_tool/mod.rs
@@ -669,9 +669,6 @@ 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()));
@@ -682,7 +679,6 @@ impl CliCommand<&'static str> for ProvePackage {
                 move_options.get_package_path()?.as_path(),
                 move_options.named_addresses(),
                 fix_bytecode_version(move_options.bytecode_version, language_version),
-                compiler_version,
                 language_version,
                 move_options.skip_attribute_checks,
                 extended_checks::get_all_attribute_names(),

diff --git a/third_party/move/move-prover/move-docgen/tests/testsuite.rs b/third_party/move/move-prover/move-docgen/tests/testsuite.rs
@@ -90,7 +90,6 @@ fn test_docgen(path: &Path, mut options: Options, suffix: &str) -> anyhow::Resul
     temp_path.push(&base_name);
 
     if path.to_str().is_some_and(|s| s.contains(V2_TEST_DIR)) {
-        options.compiler_v2 = true;
         options.language_version = Some(LanguageVersion::latest_stable());
     }
 

diff --git a/third_party/move/move-prover/src/cli.rs b/third_party/move/move-prover/src/cli.rs
@@ -15,9 +15,7 @@ use move_compiler::{command_line::SKIP_ATTRIBUTE_CHECKS, shared::NumericalAddres
 use move_docgen::DocgenOptions;
 use move_errmapgen::ErrmapOptions;
 use move_model::{
-    metadata::{CompilerVersion, LanguageVersion},
-    model::VerificationScope,
-    options::ModelBuilderOptions,
+    metadata::LanguageVersion, model::VerificationScope, options::ModelBuilderOptions,
 };
 use move_prover_boogie_backend::{
     options,
@@ -79,8 +77,6 @@ pub struct Options {
     pub experimental_pipeline: bool,
     /// Whether to skip checking for unknown attributes
     pub skip_attribute_checks: bool,
-    /// Whether to use compiler v2 to compile Move code
-    pub compiler_v2: bool,
     /// The language version to use
     pub language_version: Option<LanguageVersion>,
     /// BEGIN OF STRUCTURED OPTIONS. DO NOT ADD VALUE FIELDS AFTER THIS
@@ -120,10 +116,6 @@ impl Default for Options {
             errmapgen: ErrmapOptions::default(),
             experimental_pipeline: false,
             skip_attribute_checks: false,
-            compiler_v2: match CompilerVersion::default() {
-                CompilerVersion::V1 => false,
-                CompilerVersion::V2_0 | CompilerVersion::V2_1 => true,
-            },
             language_version: Some(LanguageVersion::default()),
         }
     }
@@ -815,9 +807,6 @@ impl Options {
                 .move_named_address_values
                 .push("Extensions=0x1".to_string())
         }
-        if matches.get_flag("compiler-v2") {
-            options.compiler_v2 = true;
-        }
         if matches.contains_id("language-version") {
             options.language_version = matches
                 .get_one::<LanguageVersion>("language-version")

diff --git a/third_party/move/move-prover/src/lib.rs b/third_party/move/move-prover/src/lib.rs
@@ -11,13 +11,10 @@ use itertools::Itertools;
 #[allow(unused_imports)]
 use log::{debug, info, warn};
 use move_abigen::Abigen;
-use move_compiler::shared::{known_attributes::KnownAttribute, PackagePaths};
-use move_compiler_v2::{env_pipeline::rewrite_target::RewritingScope, Experiment};
 use move_docgen::Docgen;
 use move_errmapgen::ErrmapGen;
 use move_model::{
     code_writer::CodeWriter, metadata::LATEST_STABLE_COMPILER_VERSION_VALUE, model::GlobalEnv,
-    parse_addresses_from_options, run_model_builder_with_options,
 };
 use move_prover_boogie_backend::{
     add_prelude, boogie_wrapper::BoogieWrapper, bytecode_translator::BoogieTranslator,
@@ -42,31 +39,6 @@ pub fn run_move_prover_errors_to_stderr(options: Options) -> anyhow::Result<()>
     run_move_prover_v2(&mut error_writer, options)
 }
 
-pub fn run_move_prover<W: WriteColor>(
-    error_writer: &mut W,
-    options: Options,
-) -> anyhow::Result<()> {
-    let now = Instant::now();
-    let addrs = parse_addresses_from_options(options.move_named_address_values.clone())?;
-    let mut env = run_model_builder_with_options(
-        vec![PackagePaths {
-            name: None,
-            paths: options.move_sources.clone(),
-            named_address_map: addrs.clone(),
-        }],
-        vec![],
-        vec![PackagePaths {
-            name: None,
-            paths: options.move_deps.clone(),
-            named_address_map: addrs,
-        }],
-        options.model_builder.clone(),
-        options.skip_attribute_checks,
-        KnownAttribute::get_all_attribute_names(),
-    )?;
-    run_move_prover_with_model(&mut env, error_writer, options, Some(now))
-}
-
 pub fn run_move_prover_v2<W: WriteColor>(
     error_writer: &mut W,
     options: Options,
@@ -121,29 +93,6 @@ pub fn create_init_num_operation_state(env: &GlobalEnv) {
     env.set_extension(global_state);
 }
 
-pub fn run_move_prover_with_model<W: WriteColor>(
-    env: &mut GlobalEnv,
-    error_writer: &mut W,
-    options: Options,
-    timer: Option<Instant>,
-) -> anyhow::Result<()> {
-    let now = timer.unwrap_or_else(Instant::now);
-    debug!("global env before prover run: {}", env.dump_env_all());
-
-    // Run the compiler v2 checking and rewriting pipeline
-    let compiler_options = move_compiler_v2::Options::default()
-        .set_experiment(Experiment::OPTIMIZE, false)
-        .set_experiment(Experiment::SPEC_REWRITE, true);
-    env.set_extension(compiler_options.clone());
-    let pipeline = move_compiler_v2::check_and_rewrite_pipeline(
-        &compiler_options,
-        true,
-        RewritingScope::Everything,
-    );
-    pipeline.run(env);
-    run_move_prover_with_model_v2(env, error_writer, options, now)
-}
-
 pub fn run_move_prover_with_model_v2<W: WriteColor>(
     env: &mut GlobalEnv,
     error_writer: &mut W,

diff --git a/third_party/move/move-prover/src/main.rs b/third_party/move/move-prover/src/main.rs
@@ -5,7 +5,7 @@
 #![forbid(unsafe_code)]
 
 use codespan_reporting::term::termcolor::{ColorChoice, StandardStream};
-use move_prover::{cli::Options, run_move_prover, run_move_prover_v2};
+use move_prover::{cli::Options, run_move_prover_v2};
 use std::env;
 
 fn main() {
@@ -30,9 +30,5 @@ fn run() -> anyhow::Result<()> {
     };
     options.setup_logging();
     let mut error_writer = StandardStream::stderr(color);
-    if options.compiler_v2 {
-        run_move_prover_v2(&mut error_writer, options)
-    } else {
-        run_move_prover(&mut error_writer, options)
-    }
+    run_move_prover_v2(&mut error_writer, options)
 }
diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.exp b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.exp
@@ -3,7 +3,7 @@ error: caller does not have permission to modify `B::T` at given address
    ┌─ tests/sources/functional/ModifiesErrorTest.move:38:17
    │
 38 │         let t = borrow_global_mut<T>(addr1);
-   │                 ^^^^^^^^^^^^^^^^^
+   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
    │
    =     at tests/sources/functional/ModifiesErrorTest.move:36: mutate_at_test_incorrect
    =     at tests/sources/functional/ModifiesErrorTest.move:47: mutate_at_test_incorrect (spec)
@@ -18,7 +18,7 @@ error: caller does not have permission to modify `B::T` at given address
    ┌─ tests/sources/functional/ModifiesErrorTest.move:52:9
    │
 52 │         move_to<T>(account, T{x: 2});
-   │         ^^^^^^^
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    │
    =     at tests/sources/functional/ModifiesErrorTest.move:50: move_to_test_incorrect
    =     at tests/sources/functional/ModifiesErrorTest.move:60: move_to_test_incorrect (spec)
@@ -33,7 +33,7 @@ error: caller does not have permission to modify `B::T` at given address
    ┌─ tests/sources/functional/ModifiesErrorTest.move:65:17
    │
 65 │         let v = move_from<T>(addr1);
-   │                 ^^^^^^^^^
+   │                 ^^^^^^^^^^^^^^^^^^^
    │
    =     at tests/sources/functional/ModifiesErrorTest.move:63: move_from_test_incorrect
    =     at tests/sources/functional/ModifiesErrorTest.move:74: move_from_test_incorrect (spec)

diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp
diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesSchemaTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesSchemaTest.v2_exp
diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesTypeTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesTypeTest.v2_exp