[move-prover] Sharding feature + re-animate Prover.toml

Boogie is using exhaustive amounts of memory if run as part of proving aptos-framework (100GB+), which makes CI and local testing fail randomly. This PR introduces a new `--shards` option which splits the Boogie job into multiple shards, if specified. Also re-animates the use of `Prover.toml` in a package directory allowing to set such options.

aptos-move/framework/aptos-framework/Prover.toml

@@ -0,0 +1,2 @@
+[backend]
+shards = 4

aptos-move/framework/aptos-stdlib/Prover.toml

@@ -0,0 +1,2 @@
+[backend]
+shards = 2

aptos-move/framework/aptos-token/Prover.toml

@@ -0,0 +1,2 @@
+[backend]
+shards = 2

aptos-move/framework/src/prover.rs

@@ -22,7 +22,7 @@ use std::{
 };
 use tempfile::TempDir;
 
-#[derive(Debug, Clone, clap::Parser, serde::Serialize, serde::Deserialize)]
+#[derive(Debug, Clone, Default, clap::Parser, serde::Serialize, serde::Deserialize)]
 pub struct ProverOptions {
     /// Verbosity level
     #[clap(long, short)]
@@ -50,20 +50,30 @@ pub struct ProverOptions {
     pub cvc5: bool,
 
     /// The depth until which stratified functions are expanded.
-    #[clap(long, default_value_t = 6)]
-    pub stratification_depth: usize,
+    #[clap(long)]
+    pub stratification_depth: Option<usize>,
 
     /// A seed for the prover.
-    #[clap(long, default_value_t = 0)]
-    pub random_seed: usize,
+    #[clap(long)]
+    pub random_seed: Option<usize>,
 
     /// The number of cores to use for parallel processing of verification conditions.
-    #[clap(long, default_value_t = 4)]
-    pub proc_cores: usize,
+    #[clap(long)]
+    pub proc_cores: Option<usize>,
+
+    /// The number of shards to split the verification problem into. Shards are
+    /// processed sequentially. This can be used to ease memory pressure for verification
+    /// of large packages.
+    #[clap(long)]
+    pub shards: Option<usize>,
+
+    /// If there are multiple shards, the shard to which verification shall be narrowed.
+    #[clap(long)]
+    pub only_shard: Option<usize>,
 
     /// A (soft) timeout for the solver, per verification condition, in seconds.
-    #[clap(long, default_value_t = 40)]
-    pub vc_timeout: usize,
+    #[clap(long)]
+    pub vc_timeout: Option<usize>,
 
     /// Whether to disable global timeout overwrite.
     /// With this flag set to true, the value set by "--vc-timeout" will be used globally
@@ -118,32 +128,6 @@ pub struct ProverOptions {
     pub for_test: bool,
 }
 
-impl Default for ProverOptions {
-    fn default() -> Self {
-        Self {
-            verbosity: None,
-            filter: None,
-            only: None,
-            trace: false,
-            cvc5: false,
-            stratification_depth: 6,
-            random_seed: 0,
-            proc_cores: 4,
-            vc_timeout: 40,
-            disallow_global_timeout_to_be_overwritten: false,
-            check_inconsistency: false,
-            unconditional_abort_as_inconsistency: false,
-            keep_loops: false,
-            loop_unroll: None,
-            stable_test_output: false,
-            dump: false,
-            benchmark: false,
-            for_test: false,
-            skip_instance_check: false,
-        }
-    }
-}
-
 impl ProverOptions {
     /// Runs the move prover on the package.
     pub fn prove(
@@ -173,7 +157,7 @@ impl ProverOptions {
             known_attributes.clone(),
             experiments.to_vec(),
         )?;
-        let mut options = self.convert_options();
+        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
@@ -225,65 +209,79 @@ impl ProverOptions {
         Ok(())
     }
 
-    fn convert_options(self) -> move_prover::cli::Options {
+    fn convert_options(self, package_path: &Path) -> anyhow::Result<Options> {
+        let prover_toml = package_path.join("Prover.toml");
+        let base_opts = if prover_toml.exists() {
+            Options::create_from_toml_file(prover_toml.to_string_lossy().as_ref())?
+        } else {
+            Options::default()
+        };
         let verbosity_level = if let Some(level) = self.verbosity {
             level
         } else if self.for_test {
             LevelFilter::Warn
         } else {
-            LevelFilter::Info
+            base_opts.verbosity_level
         };
-        let opts = move_prover::cli::Options {
+        let opts = Options {
             output_path: "".to_string(),
             verbosity_level,
             prover: move_prover_bytecode_pipeline::options::ProverOptions {
                 verify_scope: if let Some(name) = self.only {
                     VerificationScope::Only(name)
                 } else {
-                    VerificationScope::All
+                    base_opts.prover.verify_scope.clone()
                 },
-                stable_test_output: self.stable_test_output,
+                stable_test_output: self.stable_test_output || base_opts.prover.stable_test_output,
                 auto_trace_level: if self.trace {
                     move_prover_bytecode_pipeline::options::AutoTraceLevel::VerifiedFunction
                 } else {
-                    move_prover_bytecode_pipeline::options::AutoTraceLevel::Off
+                    base_opts.prover.auto_trace_level
                 },
                 report_severity: Severity::Warning,
-                dump_bytecode: self.dump,
+                dump_bytecode: self.dump || base_opts.prover.dump_bytecode,
                 dump_cfg: false,
-                check_inconsistency: self.check_inconsistency,
-                unconditional_abort_as_inconsistency: self.unconditional_abort_as_inconsistency,
-                skip_loop_analysis: self.keep_loops,
-                ..Default::default()
+                check_inconsistency: self.check_inconsistency
+                    || base_opts.prover.check_inconsistency,
+                unconditional_abort_as_inconsistency: self.unconditional_abort_as_inconsistency
+                    || base_opts.prover.unconditional_abort_as_inconsistency,
+                skip_loop_analysis: self.keep_loops
+                    || base_opts.prover.unconditional_abort_as_inconsistency,
+                ..base_opts.prover.clone()
             },
             backend: move_prover_boogie_backend::options::BoogieOptions {
-                use_cvc5: self.cvc5,
+                use_cvc5: self.cvc5 || base_opts.backend.use_cvc5,
                 boogie_flags: vec![],
-                generate_smt: self.dump,
-                stratification_depth: self.stratification_depth,
-                proc_cores: self.proc_cores,
-                vc_timeout: self.vc_timeout,
+                generate_smt: self.dump || base_opts.backend.generate_smt,
+                stratification_depth: self
+                    .stratification_depth
+                    .unwrap_or(base_opts.backend.stratification_depth),
+                proc_cores: self.proc_cores.unwrap_or(base_opts.backend.proc_cores),
+                shards: self.shards.unwrap_or(base_opts.backend.shards),
+                only_shard: self.only_shard.or(base_opts.backend.only_shard),
+                vc_timeout: self.vc_timeout.unwrap_or(base_opts.backend.vc_timeout),
                 global_timeout_overwrite: !self.disallow_global_timeout_to_be_overwritten,
-                keep_artifacts: self.dump,
-                stable_test_output: self.stable_test_output,
+                keep_artifacts: self.dump || base_opts.backend.keep_artifacts,
+                stable_test_output: self.stable_test_output || base_opts.backend.stable_test_output,
                 z3_trace_file: if self.dump {
                     Some("z3.trace".to_string())
                 } else {
                     None
                 },
                 custom_natives: None,
-                loop_unroll: self.loop_unroll,
-                skip_instance_check: self.skip_instance_check,
-                ..Default::default()
+                loop_unroll: self.loop_unroll.or(base_opts.backend.loop_unroll),
+                skip_instance_check: self.skip_instance_check
+                    || base_opts.backend.skip_instance_check,
+                ..base_opts.backend
             },
-            ..Default::default()
+            ..base_opts
         };
         if self.for_test {
             opts.setup_logging_for_test();
         } else {
             opts.setup_logging()
         }
-        opts
+        Ok(opts)
     }
 
     pub fn default_for_test() -> Self {

aptos-move/framework/tests/move_prover_tests.rs

@@ -29,7 +29,7 @@ pub fn read_env_var(v: &str) -> String {
     std::env::var(v).unwrap_or_else(|_| String::new())
 }
 
-pub fn run_prover_for_pkg(path_to_pkg: impl Into<String>) {
+pub fn run_prover_for_pkg(path_to_pkg: impl Into<String>, shards: usize) {
     let pkg_path = path_in_crate(path_to_pkg);
     let mut options = ProverOptions::default_for_test();
     let no_tools = read_env_var("BOOGIE_EXE").is_empty()
@@ -47,12 +47,14 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into<String>) {
         let unconditional_abort_inconsistency_flag =
             read_env_var(ENV_TEST_UNCONDITIONAL_ABORT_AS_INCONSISTENCY) == "1";
         let disallow_timeout_overwrite = read_env_var(ENV_TEST_DISALLOW_TIMEOUT_OVERWRITE) == "1";
+        options.shards = Some(shards);
         options.check_inconsistency = inconsistency_flag;
         options.unconditional_abort_as_inconsistency = unconditional_abort_inconsistency_flag;
         options.disallow_global_timeout_to_be_overwritten = disallow_timeout_overwrite;
         options.vc_timeout = read_env_var(ENV_TEST_VC_TIMEOUT)
             .parse::<usize>()
-            .unwrap_or(options.vc_timeout);
+            .ok()
+            .or(options.vc_timeout);
         let skip_attribute_checks = false;
         options
             .prove(
@@ -72,20 +74,20 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into<String>) {
 
 #[test]
 fn move_framework_prover_tests() {
-    run_prover_for_pkg("aptos-framework");
+    run_prover_for_pkg("aptos-framework", 4);
 }
 
 #[test]
 fn move_token_prover_tests() {
-    run_prover_for_pkg("aptos-token");
+    run_prover_for_pkg("aptos-token", 2);
 }
 
 #[test]
 fn move_aptos_stdlib_prover_tests() {
-    run_prover_for_pkg("aptos-stdlib");
+    run_prover_for_pkg("aptos-stdlib", 2);
 }
 
 #[test]
 fn move_stdlib_prover_tests() {
-    run_prover_for_pkg("move-stdlib");
+    run_prover_for_pkg("move-stdlib", 1);
 }

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

@@ -59,11 +59,15 @@ use move_stackless_bytecode::{
         Operation, PropKind,
     },
 };
-use std::collections::{BTreeMap, BTreeSet};
+use std::{
+    collections::{BTreeMap, BTreeSet},
+    hash::{DefaultHasher, Hash, Hasher},
+};
 
 pub struct BoogieTranslator<'env> {
     env: &'env GlobalEnv,
     options: &'env BoogieOptions,
+    for_shard: Option<usize>,
     writer: &'env CodeWriter,
     spec_translator: SpecTranslator<'env>,
     targets: &'env FunctionTargetsHolder,
@@ -85,12 +89,14 @@ impl<'env> BoogieTranslator<'env> {
     pub fn new(
         env: &'env GlobalEnv,
         options: &'env BoogieOptions,
+        for_shard: Option<usize>,
         targets: &'env FunctionTargetsHolder,
         writer: &'env CodeWriter,
     ) -> Self {
         Self {
             env,
             options,
+            for_shard,
             targets,
             writer,
             spec_translator: SpecTranslator::new(writer, env, options),
@@ -113,7 +119,24 @@ impl<'env> BoogieTranslator<'env> {
             .unwrap_or(default_timeout)
     }
 
-    pub fn is_not_verified_timeout(&self, fun_target: &FunctionTarget) -> bool {
+    /// Checks whether the given function is a verification target.
+    fn is_verified(&self, fun_variant: &FunctionVariant, fun_target: &FunctionTarget) -> bool {
+        if !fun_variant.is_verified() {
+            return false;
+        }
+        if let Some(shard) = self.for_shard {
+            // Check whether the shard is included.
+            if self.options.only_shard.is_some() && self.options.only_shard != Some(shard + 1) {
+                return false;
+            }
+            // Check whether it is part of the shard.
+            let mut hasher = DefaultHasher::new();
+            fun_target.func_env.get_full_name_str().hash(&mut hasher);
+            if (hasher.finish() as usize) % self.options.shards != shard {
+                return false;
+            }
+        }
+        // Check whether the estimated duration is too large for configured timeout
         let options = self.options;
         let estimate_timeout_opt = fun_target
             .func_env
@@ -123,9 +146,9 @@ impl<'env> BoogieTranslator<'env> {
                 .func_env
                 .get_num_pragma(TIMEOUT_PRAGMA)
                 .unwrap_or(options.vc_timeout);
-            estimate_timeout > timeout
+            estimate_timeout <= timeout
         } else {
-            false
+            true
         }
     }
 
@@ -279,7 +302,7 @@ impl<'env> BoogieTranslator<'env> {
                     continue;
                 }
                 for (variant, ref fun_target) in self.targets.get_targets(fun_env) {
-                    if variant.is_verified() && !self.is_not_verified_timeout(fun_target) {
+                    if self.is_verified(&variant, fun_target) {
                         verified_functions_count += 1;
                         debug!(
                             "will verify primary function `{}`",
@@ -363,7 +386,15 @@ impl<'env> BoogieTranslator<'env> {
         }
         // Emit any finalization items required by spec translation.
         self.spec_translator.finalize();
-        info!("{} verification conditions", verified_functions_count);
+        let shard_info = if let Some(shard) = self.for_shard {
+            format!(" (for shard #{} of {})", shard + 1, self.options.shards)
+        } else {
+            "".to_string()
+        };
+        info!(
+            "{} verification conditions{}",
+            verified_functions_count, shard_info
+        );
     }
 }
 
@@ -1106,7 +1137,7 @@ impl<'env> FunctionTranslator<'env> {
         }
 
         // Initial assumptions
-        if variant.is_verified() && !self.parent.is_not_verified_timeout(fun_target) {
+        if self.parent.is_verified(variant, fun_target) {
             self.translate_verify_entry_assumptions(fun_target);
         }
 

third_party/move/move-prover/boogie-backend/src/options.rs

@@ -140,6 +140,11 @@ pub struct BoogieOptions {
     pub random_seed: usize,
     /// The number of cores to use for parallel processing of verification conditions.
     pub proc_cores: usize,
+    /// The number of shards to split the verification problem into.
+    pub shards: usize,
+    /// If there are shards, specifies to only run the given shard. Shards are numbered
+    /// starting at 1.
+    pub only_shard: Option<usize>,
     /// A (soft) timeout for the solver, per verification condition, in seconds.
     pub vc_timeout: usize,
     /// Whether allow local timeout overwrites the global one
@@ -198,7 +203,9 @@ impl Default for BoogieOptions {
             vector_using_sequences: false,
             random_seed: 1,
             proc_cores: 4,
-            vc_timeout: 80,
+            shards: 1,
+            only_shard: None,
+            vc_timeout: 40,
             global_timeout_overwrite: true,
             keep_artifacts: false,
             eager_threshold: 100,

third_party/move/move-prover/lab/src/benchmark.rs

@@ -274,7 +274,7 @@ impl Runner {
         )?;
 
         // Generate boogie code.
-        let code_writer = generate_boogie(env, &self.options, &targets)?;
+        let code_writer = generate_boogie(env, &self.options, None, &targets)?;
         check_errors(
             env,
             &self.options,

third_party/move/move-prover/src/lib.rs

@@ -7,6 +7,7 @@
 use crate::cli::Options;
 use anyhow::anyhow;
 use codespan_reporting::term::termcolor::{ColorChoice, StandardStream, WriteColor};
+use itertools::Itertools;
 #[allow(unused_imports)]
 use log::{debug, info, warn};
 use move_abigen::Abigen;
@@ -28,7 +29,7 @@ use move_stackless_bytecode::function_target_pipeline::FunctionTargetsHolder;
 use std::{
     fs,
     path::{Path, PathBuf},
-    time::Instant,
+    time::{Duration, Instant},
 };
 
 pub mod cli;
@@ -146,7 +147,7 @@ pub fn run_move_prover_with_model<W: WriteColor>(
 pub fn run_move_prover_with_model_v2<W: WriteColor>(
     env: &mut GlobalEnv,
     error_writer: &mut W,
-    options: Options,
+    mut options: Options,
     start_time: Instant,
 ) -> anyhow::Result<()> {
     let build_duration = start_time.elapsed();
@@ -194,33 +195,56 @@ pub fn run_move_prover_with_model_v2<W: WriteColor>(
         "exiting with bytecode transformation errors",
     )?;
 
-    // Generate boogie code
-    let now = Instant::now();
-    let code_writer = generate_boogie(env, &options, &targets)?;
-    let gen_duration = now.elapsed();
-    check_errors(
-        env,
-        &options,
-        error_writer,
-        "exiting with condition generation errors",
-    )?;
-
-    // Verify boogie code.
-    let now = Instant::now();
-    verify_boogie(env, &options, &targets, code_writer)?;
-    let verify_duration = now.elapsed();
-
+    let mut gen_durations = vec![];
+    let mut verify_durations = vec![];
+    let has_shards = options.backend.shards > 1;
+    let output_base_file = options.output_path.clone();
+    for shard in 0..options.backend.shards {
+        // If there are shards, modify the output name
+        if has_shards {
+            options.output_path = Path::new(&output_base_file)
+                .with_extension(format!("shard_{}.bpl", shard + 1))
+                .to_string_lossy()
+                .to_string();
+        }
+        // Generate boogie code.
+        let now = Instant::now();
+        let code_writer = generate_boogie(
+            env,
+            &options,
+            if has_shards { Some(shard) } else { None },
+            &targets,
+        )?;
+        gen_durations.push(now.elapsed());
+        check_errors(
+            env,
+            &options,
+            error_writer,
+            "exiting with condition generation errors",
+        )?;
+
+        // Verify boogie code.
+        let now = Instant::now();
+        verify_boogie(env, &options, &targets, code_writer)?;
+        verify_durations.push(now.elapsed());
+    }
+    options.output_path = output_base_file;
     // Report durations.
+    let dur_list = |ds: &[Duration]| {
+        ds.iter()
+            .map(|d| format!("{:.2}", d.as_secs_f64()))
+            .join("/")
+    };
     info!(
-        "{:.3}s build, {:.3}s trafo, {:.3}s gen, {:.3}s verify, total {:.3}s",
+        "{:.2}s build, {:.2}s trafo, {}s gen, {}s verify, total {:.2}s",
         build_duration.as_secs_f64(),
         trafo_duration.as_secs_f64(),
-        gen_duration.as_secs_f64(),
-        verify_duration.as_secs_f64(),
+        dur_list(&gen_durations),
+        dur_list(&verify_durations),
         build_duration.as_secs_f64()
             + trafo_duration.as_secs_f64()
-            + gen_duration.as_secs_f64()
-            + verify_duration.as_secs_f64()
+            + gen_durations.iter().sum::<Duration>().as_secs_f64()
+            + verify_durations.iter().sum::<Duration>().as_secs_f64()
     );
     check_errors(
         env,
@@ -247,11 +271,12 @@ pub fn check_errors<W: WriteColor>(
 pub fn generate_boogie(
     env: &GlobalEnv,
     options: &Options,
+    shard: Option<usize>,
     targets: &FunctionTargetsHolder,
 ) -> anyhow::Result<CodeWriter> {
     let writer = CodeWriter::new(env.internal_loc());
     add_prelude(env, &options.backend, &writer)?;
-    let mut translator = BoogieTranslator::new(env, &options.backend, targets, &writer);
+    let mut translator = BoogieTranslator::new(env, &options.backend, shard, targets, &writer);
     translator.translate();
     Ok(writer)
 }