refactor

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

@@ -29,6 +29,7 @@
     -  [Function `create_initialize_validators_with_commission`](#@Specification_1_create_initialize_validators_with_commission)
     -  [Function `create_initialize_validators`](#@Specification_1_create_initialize_validators)
     -  [Function `create_initialize_validator`](#@Specification_1_create_initialize_validator)
+    -  [Function `initialize_validator`](#@Specification_1_initialize_validator)
     -  [Function `set_genesis_end`](#@Specification_1_set_genesis_end)
 
 
@@ -1028,6 +1029,22 @@ The last step of genesis.
 
 
 
+<a id="@Specification_1_initialize_validator"></a>
+
+### Function `initialize_validator`
+
+
+<pre><code><b>fun</b> <a href="genesis.md#0x1_genesis_initialize_validator">initialize_validator</a>(pool_address: <b>address</b>, validator: &<a href="genesis.md#0x1_genesis_ValidatorConfiguration">genesis::ValidatorConfiguration</a>)
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> verify_duration_estimate = 120;
+</code></pre>
+
+
+
 <a id="@Specification_1_set_genesis_end"></a>
 
 ### Function `set_genesis_end`

aptos-move/framework/aptos-framework/sources/genesis.spec.move

@@ -108,6 +108,10 @@ spec aptos_framework::genesis {
         ensures exists<transaction_fee::AptosCoinCapabilities>(@aptos_framework);
     }
 
+    spec initialize_validator {
+        pragma verify_duration_estimate = 120;
+    }
+
     spec create_initialize_validators_with_commission {
         pragma verify_duration_estimate = 120;
 

third_party/move/move-model/bytecode-test-utils/Cargo.toml

@@ -13,6 +13,7 @@ edition = "2021"
 anyhow = { workspace = true }
 codespan-reporting = { workspace = true, features = ["serde", "serialization"] }
 move-command-line-common = { workspace = true }
+move-compiler = { workspace = true }
 move-compiler-v2 = { workspace = true }
 move-model = { workspace = true }
 move-prover-test-utils = { workspace = true }

third_party/move/move-model/bytecode-test-utils/src/lib.rs

@@ -5,6 +5,7 @@
 use anyhow::anyhow;
 use codespan_reporting::{diagnostic::Severity, term::termcolor::Buffer};
 use move_command_line_common::testing::get_compiler_exp_extension;
+use move_compiler::shared::known_attributes::KnownAttribute;
 use move_compiler_v2::{self, run_move_compiler_for_analysis, Options};
 use move_model::metadata::LanguageVersion;
 use move_prover_test_utils::{baseline_test::verify_or_update_baseline, extract_test_directives};
@@ -26,16 +27,17 @@ pub fn test_runner(
     path: &Path,
     pipeline_opt: Option<FunctionTargetPipeline>,
 ) -> anyhow::Result<()> {
-    let mut options = Options {
+    let options = Options {
         sources_deps: extract_test_directives(path, "// dep:")?,
         sources: vec![path.to_string_lossy().to_string()],
         dependencies: vec![],
         named_address_mapping: move_stdlib::move_stdlib_named_addresses_strings(),
+        language_version: Some(LanguageVersion::latest()),
+        compile_verify_code: true,
+        compile_test_code: false,
+        known_attributes: KnownAttribute::get_all_attribute_names().clone(),
         ..Options::default()
     };
-    options = options.set_language_version(LanguageVersion::latest_stable());
-    options = options.set_compile_verify_code(true);
-    options = options.set_compile_test_code(false);
     let mut error_writer = Buffer::no_color();
     let env = run_move_compiler_for_analysis(&mut error_writer, options)?;
     let out = if env.has_errors() {