diff --git a/Cargo.lock b/Cargo.lock
index 6dada90d6c061..60ff109e9b00f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -11127,6 +11127,7 @@ dependencies = [
"evm-exec-utils",
"hex",
"itertools 0.10.5",
+ "log",
"move-abigen",
"move-binary-format",
"move-bytecode-source-map",
diff --git a/aptos-move/framework/aptos-framework/doc/staking_config.md b/aptos-move/framework/aptos-framework/doc/staking_config.md
index 0f89c9afc8de1..1dced05834f3d 100644
--- a/aptos-move/framework/aptos-framework/doc/staking_config.md
+++ b/aptos-move/framework/aptos-framework/doc/staking_config.md
@@ -1405,7 +1405,8 @@ Caller must be @aptos_framework.
StakingRewardsConfig is under the @aptos_framework.
-
include StakingRewardsConfigRequirement;
+pragma verify_duration_estimate = 120;
+include StakingRewardsConfigRequirement;
let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
diff --git a/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move b/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move
index 878da8fa9daa2..3cf9045c52457 100644
--- a/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move
+++ b/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]
diff --git a/aptos-move/framework/aptos-stdlib/sources/data_structures/tests/smart_vector_test.move b/aptos-move/framework/aptos-stdlib/sources/data_structures/tests/smart_vector_test.move
index 40ce2c417e4e4..ed7cb50af35f6 100644
--- a/aptos-move/framework/aptos-stdlib/sources/data_structures/tests/smart_vector_test.move
+++ b/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 });
diff --git a/aptos-move/framework/move-stdlib/doc/features.md b/aptos-move/framework/move-stdlib/doc/features.md
index 88e231ad57113..86e55abc9cf5b 100644
--- a/aptos-move/framework/move-stdlib/doc/features.md
+++ b/aptos-move/framework/move-stdlib/doc/features.md
@@ -2882,6 +2882,9 @@ Helper to check whether a feature flag is enabled.
aborts_if signer::address_of(framework) != @std;
+pragma opaque;
+modifies global<Features>(@std);
+modifies global<PendingFeatures>(@std);
diff --git a/aptos-move/framework/move-stdlib/sources/configs/features.spec.move b/aptos-move/framework/move-stdlib/sources/configs/features.spec.move
index 996091fe88508..1246a616d8489 100644
--- a/aptos-move/framework/move-stdlib/sources/configs/features.spec.move
+++ b/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, disable: vector) {
aborts_if signer::address_of(framework) != @std;
// TODO(tengzhang): add functional spec
+ // TODO(#12526): undo declaring opaque once fixed
+ pragma opaque;
+ modifies global(@std);
+ modifies global(@std);
}
spec fun spec_contains(features: vector, feature: u64): bool {
diff --git a/aptos-move/framework/src/built_package.rs b/aptos-move/framework/src/built_package.rs
index 5fbf1c7c00c52..c69610146b1f0 100644
--- a/aptos-move/framework/src/built_package.rs
+++ b/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,
})
}
diff --git a/aptos-move/framework/src/prover.rs b/aptos-move/framework/src/prover.rs
index 5614c273b435b..20adcad9e6b5c 100644
--- a/aptos-move/framework/src/prover.rs
+++ b/aptos-move/framework/src/prover.rs
@@ -8,6 +8,7 @@ use codespan_reporting::{
};
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 @@ impl ProverOptions {
package_path: &Path,
named_addresses: BTreeMap,
bytecode_version: Option,
+ compiler_version: Option,
skip_attribute_checks: bool,
known_attributes: &BTreeSet,
) -> anyhow::Result<()> {
@@ -129,7 +131,7 @@ impl ProverOptions {
named_addresses,
self.filter.clone(),
bytecode_version,
- None, // compiler_version
+ compiler_version,
skip_attribute_checks,
known_attributes.clone(),
)?;
@@ -162,7 +164,11 @@ impl ProverOptions {
)],
});
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(())
}
diff --git a/aptos-move/framework/tests/move_prover_tests.rs b/aptos-move/framework/tests/move_prover_tests.rs
index 54947cb469e9a..defcf9e69b26c 100644
--- a/aptos-move/framework/tests/move_prover_tests.rs
+++ b/aptos-move/framework/tests/move_prover_tests.rs
@@ -58,6 +58,7 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into) {
pkg_path.as_path(),
BTreeMap::default(),
None,
+ None,
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
index cde0fe0703b89..899d11cdf4f4e 100644
--- a/crates/aptos/src/move_tool/mod.rs
+++ b/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(),
)
diff --git a/third_party/move/evm/move-to-yul/src/functions.rs b/third_party/move/evm/move-to-yul/src/functions.rs
index 7dd8776998bd1..1187a3cc652a6 100644
--- a/third_party/move/evm/move-to-yul/src/functions.rs
+++ b/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
},
}
diff --git a/third_party/move/move-compiler-v2/src/bytecode_generator.rs b/third_party/move/move-compiler-v2/src/bytecode_generator.rs
index fe6d26423dca3..3e245a7f2f89d 100644
--- a/third_party/move/move-compiler-v2/src/bytecode_generator.rs
+++ b/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::>();
let mut rhs_vars = rhs
- .used_temporaries(self.env())
+ .used_temporaries_with_types(self.env())
.into_iter()
.map(|t| param_symbols[t.0])
.collect::>();
diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
index 2bcf54fe92fd2..4e608d72f2165 100644
--- a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
+++ b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
@@ -3,21 +3,25 @@
use crate::{
file_format_generator::{
- module_generator::{ModuleContext, ModuleGenerator},
+ module_generator::{ModuleContext, ModuleGenerator, SOURCE_MAP_OK},
MAX_FUNCTION_DEF_COUNT, MAX_LOCAL_COUNT,
},
pipeline::livevar_analysis_processor::LiveVarAnnotation,
};
-use move_binary_format::file_format as FF;
+use move_binary_format::{
+ file_format as FF,
+ file_format::{CodeOffset, FunctionDefinitionIndex},
+};
use move_model::{
- ast::TempIndex,
- model::{FunId, FunctionEnv, Loc, QualifiedId, StructId, TypeParameter},
+ ast::{ExpData, Spec, SpecBlockTarget, TempIndex},
+ exp_rewriter::{ExpRewriter, ExpRewriterFunctions, RewriteTarget},
+ model::{FunId, FunctionEnv, Loc, NodeId, Parameter, QualifiedId, StructId, TypeParameter},
ty::{PrimitiveType, Type},
};
use move_stackless_bytecode::{
function_target::FunctionTarget,
function_target_pipeline::FunctionVariant,
- stackless_bytecode::{AssignKind, Bytecode, Constant, Label, Operation},
+ stackless_bytecode::{AssignKind, AttrId, Bytecode, Constant, Label, Operation},
};
use std::collections::{BTreeMap, BTreeSet};
@@ -25,7 +29,7 @@ pub struct FunctionGenerator<'a> {
/// The underlying module generator.
gen: &'a mut ModuleGenerator,
/// The set of temporaries which need to be pinned to locals because references are taken for
- /// them.
+ /// them, or they are used in specs.
pinned: BTreeSet,
/// A map from a temporary to information associated with it.
temps: BTreeMap,
@@ -35,6 +39,8 @@ pub struct FunctionGenerator<'a> {
locals: Vec,
/// A map from branching labels to information about them.
label_info: BTreeMap