[prover-v2] Connecting Prover to v2 code generation toolchain

aptos-move/framework/aptos-framework/doc/staking_config.md

@@ -1405,7 +1405,8 @@ Caller must be @aptos_framework.
 StakingRewardsConfig is under the @aptos_framework.
 
 
-<pre><code><b>include</b> <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigRequirement">StakingRewardsConfigRequirement</a>;
+<pre><code><b>pragma</b> verify_duration_estimate = 120;
+<b>include</b> <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigRequirement">StakingRewardsConfigRequirement</a>;
 <b>let</b> addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(aptos_framework);
 // This enforces <a id="high-level-req-1.6" href="#high-level-req">high-level requirement 1</a>:
 <b>aborts_if</b> addr != @aptos_framework;

aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move

@@ -237,6 +237,7 @@ spec aptos_framework::staking_config {
         rewards_rate_decrease_rate: FixedPoint64,
     ) {
         use std::signer;
+        pragma verify_duration_estimate = 120; // verified but takes long
         include StakingRewardsConfigRequirement;
         let addr = signer::address_of(aptos_framework);
         /// [high-level-req-1.6]

aptos-move/framework/aptos-stdlib/sources/data_structures/tests/smart_vector_test.move

@@ -103,6 +103,7 @@ module aptos_std::smart_vector_test {
         assert!(sum == 5050, 0);
     }
 
+    #[test]
     fun smart_vector_map_test() {
         let v = make_smart_vector(100);
         let mapped_v = V::map(v, |x| { x * 2 });

aptos-move/framework/move-stdlib/doc/features.md

@@ -2882,6 +2882,9 @@ Helper to check whether a feature flag is enabled.
 
 
 <pre><code><b>aborts_if</b> <a href="signer.md#0x1_signer_address_of">signer::address_of</a>(framework) != @std;
+<b>pragma</b> opaque;
+<b>modifies</b> <b>global</b>&lt;<a href="features.md#0x1_features_Features">Features</a>&gt;(@std);
+<b>modifies</b> <b>global</b>&lt;<a href="features.md#0x1_features_PendingFeatures">PendingFeatures</a>&gt;(@std);
 </code></pre>
 
 

aptos-move/framework/move-stdlib/sources/configs/features.spec.move

@@ -33,6 +33,10 @@ spec std::features {
     spec change_feature_flags_for_next_epoch(framework: &signer, enable: vector<u64>, disable: vector<u64>) {
         aborts_if signer::address_of(framework) != @std;
         // TODO(tengzhang): add functional spec
+        // TODO(#12526): undo declaring opaque once fixed
+        pragma opaque;
+        modifies global<Features>(@std);
+        modifies global<PendingFeatures>(@std);
     }
 
     spec fun spec_contains(features: vector<u8>, feature: u64): bool {

aptos-move/framework/src/built_package.rs

@@ -150,9 +150,11 @@ pub fn build_model(
             known_attributes,
         },
     };
+    let compiler_version = compiler_version.unwrap_or_default();
     build_config.move_model_for_package(package_path, ModelConfig {
         target_filter,
         all_files_as_targets: false,
+        compiler_version,
     })
 }
 

aptos-move/framework/src/prover.rs

@@ -8,6 +8,7 @@
 };
 use log::LevelFilter;
 use move_core_types::account_address::AccountAddress;
+use move_package::CompilerVersion;
 use std::{
     collections::{BTreeMap, BTreeSet},
     path::Path,
@@ -118,6 +119,7 @@
         package_path: &Path,
         named_addresses: BTreeMap<String, AccountAddress>,
         bytecode_version: Option<u32>,
+        compiler_version: Option<CompilerVersion>,
         skip_attribute_checks: bool,
         known_attributes: &BTreeSet<String>,
     ) -> anyhow::Result<()> {
@@ -129,7 +131,7 @@
             named_addresses,
             self.filter.clone(),
             bytecode_version,
-            None, // compiler_version
+            compiler_version,
             skip_attribute_checks,
             known_attributes.clone(),
         )?;
@@ -162,7 +164,11 @@
                 )],
             });
         let mut writer = StandardStream::stderr(ColorChoice::Auto);
-        move_prover::run_move_prover_with_model(&mut model, &mut writer, options, Some(now))?;
+        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)?;
+        }
         Ok(())
     }
 

aptos-move/framework/tests/move_prover_tests.rs

@@ -58,6 +58,7 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into<String>) {
                 pkg_path.as_path(),
                 BTreeMap::default(),
                 None,
+                None,
                 skip_attribute_checks,
                 extended_checks::get_all_attribute_names(),
             )

crates/aptos/src/move_tool/mod.rs

@@ -556,6 +556,7 @@ impl CliCommand<&'static str> for ProvePackage {
                 move_options.get_package_path()?.as_path(),
                 move_options.named_addresses(),
                 move_options.bytecode_version,
+                move_options.compiler_version,
                 move_options.skip_attribute_checks,
                 extended_checks::get_all_attribute_names(),
             )

third_party/move/evm/move-to-yul/src/functions.rs

@@ -576,7 +576,12 @@ impl<'a> FunctionGenerator<'a> {
                 }
             },
 
-            Label(_, _) | Nop(_) | SaveMem(_, _, _) | SaveSpecVar(_, _, _) | Prop(_, _, _) => {
+            SpecBlock(..)
+            | Label(_, _)
+            | Nop(_)
+            | SaveMem(_, _, _)
+            | SaveSpecVar(_, _, _)
+            | Prop(_, _, _) => {
                 // These opcodes are not needed, ignore them
             },
         }

third_party/move/move-compiler-v2/src/bytecode_generator.rs

@@ -5,7 +5,8 @@
 use codespan_reporting::diagnostic::Severity;
 use ethnum::U256;
 use move_model::{
-    ast::{Exp, ExpData, Operation, Pattern, TempIndex, Value},
+    ast::{Exp, ExpData, Operation, Pattern, SpecBlockTarget, TempIndex, Value},
+    exp_rewriter::{ExpRewriter, ExpRewriterFunctions, RewriteTarget},
     model::{
         FieldId, FunId, FunctionEnv, GlobalEnv, Loc, NodeId, Parameter, QualifiedId,
         QualifiedInstId, StructId,
@@ -451,13 +452,18 @@ impl<'env> Generator<'env> {
                     self.error(*id, "missing enclosing loop statement")
                 }
             },
-            ExpData::SpecBlock(_, spec) => {
-                let (mut code, mut update_map) = self.context.generate_spec(&self.func_env, spec);
-                self.code.append(&mut code);
-                self.func_env
-                    .get_mut_spec()
-                    .update_map
-                    .append(&mut update_map)
+            ExpData::SpecBlock(id, spec) => {
+                // Map locals in spec to assigned temporaries.
+                let mut replacer = |id, target| {
+                    if let RewriteTarget::LocalVar(sym) = target {
+                        Some(ExpData::Temporary(id, self.find_local(id, sym)).into_exp())
+                    } else {
+                        None
+                    }
+                };
+                let (_, spec) = ExpRewriter::new(self.env(), &mut replacer)
+                    .rewrite_spec_descent(&SpecBlockTarget::Inline, spec);
+                self.emit_with(*id, |attr| Bytecode::SpecBlock(attr, spec));
             },
             ExpData::Invoke(id, _, _) | ExpData::Lambda(id, _, _) => {
                 self.internal_error(*id, format!("not yet implemented: {:?}", exp))
@@ -1361,7 +1367,7 @@ impl<'env> Generator<'env> {
             .map(|p| p.0)
             .collect::<Vec<_>>();
         let mut rhs_vars = rhs
-            .used_temporaries(self.env())
+            .used_temporaries_with_types(self.env())
             .into_iter()
             .map(|t| param_symbols[t.0])
             .collect::<BTreeSet<_>>();