[compiler-v2] Making v2 the basis of the prover (step #1) (aptos-labs#12462)

* [compiler-v2] Making v2 the basis of the prover (step #1)

This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following:

- There are two new env processors, the spec_checker and the spec_rewriter:
    - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain.
    - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself.
- Inlining has been extended to deal with specification constructs.
- To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it.
- A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2.
- Multiple test cases have been added.
- The prover driver has been adapted to use the new components.

* Fixing some unit tests

* Making hopefully all tests pass:

- Adding tuple support to the specification language as they are created by the inliner.
- Fixing an issue in memory usage calculation
- Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI.

* Disabling a condition for CI because of timeout.

* Rebasing

Author: wrwg

Cargo.lock

@@ -164,8 +164,10 @@ Abort if no DKG is in progress.
 <b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
 <b>include</b> <a href="stake.md#0x1_stake_ResourceRequirement">stake::ResourceRequirement</a>;
 <b>include</b> <a href="stake.md#0x1_stake_GetReconfigStartTimeRequirement">stake::GetReconfigStartTimeRequirement</a>;
-<b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>() ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
+<b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>(
+) ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
 <b>aborts_if</b> <b>false</b>;
+<b>pragma</b> verify_duration_estimate = 600;
 </code></pre>
 
 

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

@@ -12,8 +12,10 @@ spec aptos_framework::reconfiguration_with_dkg {
         requires chain_status::is_operating();
         include stake::ResourceRequirement;
         include stake::GetReconfigStartTimeRequirement;
-        include features::spec_periodical_reward_rate_decrease_enabled() ==> staking_config::StakingRewardsConfigEnabledRequirement;
+        include features::spec_periodical_reward_rate_decrease_enabled(
+        ) ==> staking_config::StakingRewardsConfigEnabledRequirement;
         aborts_if false;
+        pragma verify_duration_estimate = 600; // TODO: set because of timeout (property proved).
     }
 
     spec finish(account: &signer) {
@@ -59,5 +61,4 @@ spec aptos_framework::reconfiguration_with_dkg {
         requires dkg::has_incomplete_session();
         aborts_if false;
     }
-
 }

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

@@ -123,7 +123,7 @@ impl ProverOptions {
     ) -> anyhow::Result<()> {
         let now = Instant::now();
         let for_test = self.for_test;
-        let model = build_model(
+        let mut model = build_model(
             dev_mode,
             package_path,
             named_addresses,
@@ -162,7 +162,7 @@ impl ProverOptions {
                 )],
             });
         let mut writer = StandardStream::stderr(ColorChoice::Auto);
-        move_prover::run_move_prover_with_model(&model, &mut writer, options, Some(now))?;
+        move_prover::run_move_prover_with_model(&mut model, &mut writer, options, Some(now))?;
         Ok(())
     }
 

aptos-move/framework/src/prover.rs

@@ -2446,7 +2446,7 @@ object "test_A2_M_test_abi_String" {
                 case 2 {
                     // label L5
                     // assert Le($t1, $t4)
-                    // assert forall j: num: Range(0, $t1): ascii::$is_valid_char(Index($t0, j))
+                    // assert forall j: num: Range(0, $t1): ascii::is_valid_char(Index($t0, j))
                     // $t6 := <($t1, $t4)
                     $t6 := $Lt(i, $t4)
                     // if ($t6) goto L1 else goto L0
@@ -2474,7 +2474,7 @@ object "test_A2_M_test_abi_String" {
                 case 5 {
                     // label L0
                     // assert Eq<u64>($t1, $t4)
-                    // assert forall j: num: Range(0, $t4): ascii::$is_valid_char(Index($t0, j))
+                    // assert forall j: num: Range(0, $t4): ascii::is_valid_char(Index($t0, j))
                     // $t14 := move($t0)
                     $t14 := mload($locals)
                     // $t15 := pack ascii::String($t14)

third_party/move/evm/move-to-yul/tests/TestABIStructs.exp

@@ -37,7 +37,7 @@ log = { version = "0.4.14", features = ["serde"] }
 num = "0.4.0"
 once_cell = "1.7.2"
 #paste = "1.0.5"
-#petgraph = "0.5.1"
+petgraph = "0.6.4"
 serde = { version = "1.0.124", features = ["derive"] }
 
 [dev-dependencies]

third_party/move/move-compiler-v2/Cargo.toml

@@ -6,11 +6,14 @@
 
 // TODO: move all other `&mut GlobalEnv` processors into this module.
 
-use log::debug;
+use log::trace;
 use move_model::model::GlobalEnv;
 use std::io::Write;
 
 pub mod lambda_lifter;
+pub mod rewrite_target;
+pub mod spec_checker;
+pub mod spec_rewriter;
 
 /// Represents a pipeline of processors working on the global environment.
 #[derive(Default)]
@@ -32,10 +35,10 @@ impl<'a> EnvProcessorPipeline<'a> {
     /// Runs the pipeline. Running will be ended if any of the steps produces an error.
     /// The function returns true if all steps succeeded without errors.
     pub fn run(&self, env: &mut GlobalEnv) -> bool {
-        debug!("before env processor pipeline: {}", env.dump_env());
+        trace!("before env processor pipeline: {}", env.dump_env());
         for (name, proc) in &self.processors {
             proc(env);
-            debug!("after env processor {}", name);
+            trace!("after env processor {}", name);
             if env.has_errors() {
                 return false;
             }
@@ -47,13 +50,13 @@ impl<'a> EnvProcessorPipeline<'a> {
     /// only.
     pub fn run_and_record(&self, env: &mut GlobalEnv, w: &mut impl Write) -> anyhow::Result<bool> {
         let msg = format!("before env processor pipeline:\n{}\n", env.dump_env());
-        debug!("{}", msg);
+        trace!("{}", msg);
         writeln!(w, "// -- Model dump {}", msg)?;
         for (name, proc) in &self.processors {
             proc(env);
             if !env.has_errors() {
                 let msg = format!("after env processor {}:\n{}\n", name, env.dump_env());
-                debug!("{}", msg);
+                trace!("{}", msg);
                 writeln!(w, "// -- Model dump {}", msg)?;
             } else {
                 return Ok(false);

third_party/move/move-compiler-v2/src/env_pipeline/mod.rs

@@ -0,0 +1,206 @@
+// Copyright © Aptos Foundation
+// SPDX-License-Identifier: Apache-2.0
+
+use move_model::{
+    ast::{Exp, Spec, SpecBlockTarget},
+    model::{FunId, GlobalEnv, NodeId, QualifiedId, SpecFunId},
+};
+use std::{
+    collections::{BTreeMap, BTreeSet},
+    mem,
+};
+
+/// Represents a target for rewriting.
+#[derive(Debug, PartialOrd, Ord, PartialEq, Eq, Clone)]
+pub enum RewriteTarget {
+    /// A Move function
+    MoveFun(QualifiedId<FunId>),
+    /// A specification function
+    SpecFun(QualifiedId<SpecFunId>),
+    /// A specification block, which can be attached to a Move function, struct, or module.
+    SpecBlock(SpecBlockTarget),
+}
+
+/// Represents the state of a rewriting target.
+#[derive(Debug, Clone, Eq, PartialEq)]
+pub enum RewriteState {
+    /// The target has not been changed
+    Unchanged,
+    /// The definition of a Move or spec function has changed
+    Def(Exp),
+    /// A specification block has changed.
+    Spec(Spec),
+    /// The target is 'abstract', i.e. does have a definition.
+    Abstract,
+}
+
+/// Scope for collecting targets.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Ord, PartialOrd)]
+pub enum RewritingScope {
+    /// Including only targets for which `module.is_target()` is true.
+    CompilationTarget,
+    /// Include everything.
+    Everything,
+}
+
+/// Represents a set of rewriting targets in the given state.
+#[derive(Clone)]
+pub struct RewriteTargets {
+    pub targets: BTreeMap<RewriteTarget, RewriteState>,
+}
+
+impl RewriteTargets {
+    /// Create a new set of rewrite targets, collecting them as specified by `scope`.
+    /// Those targets are initially associated with `Unchanged` state.
+    pub fn create(env: &GlobalEnv, scope: RewritingScope) -> Self {
+        let mut targets = vec![];
+        let add_spec =
+            |targets: &mut Vec<RewriteTarget>, sb_target: SpecBlockTarget, spec: &Spec| {
+                if !spec.is_empty() {
+                    targets.push(RewriteTarget::SpecBlock(sb_target))
+                }
+            };
+        for module in env.get_modules() {
+            if scope == RewritingScope::Everything || module.is_target() {
+                for func in module.get_functions() {
+                    let id = func.get_qualified_id();
+                    targets.push(RewriteTarget::MoveFun(id));
+                    add_spec(
+                        &mut targets,
+                        SpecBlockTarget::Function(id.module_id, id.id),
+                        &func.get_spec(),
+                    );
+                }
+                for (spec_fun_id, _) in module.get_spec_funs() {
+                    targets.push(RewriteTarget::SpecFun(
+                        module.get_id().qualified(*spec_fun_id),
+                    ));
+                }
+                for struct_env in module.get_structs() {
+                    add_spec(
+                        &mut targets,
+                        SpecBlockTarget::Struct(module.get_id(), struct_env.get_id()),
+                        &struct_env.get_spec(),
+                    )
+                }
+                if !module.get_spec().is_empty() {
+                    add_spec(
+                        &mut targets,
+                        SpecBlockTarget::Module(module.get_id()),
+                        &module.get_spec(),
+                    );
+                }
+            }
+        }
+        Self {
+            targets: targets
+                .into_iter()
+                .map(|target| (target, RewriteState::Unchanged))
+                .collect(),
+        }
+    }
+
+    /// Filters the targets according to the predicate.
+    pub fn filter(&mut self, pred: impl Fn(&RewriteTarget, &RewriteState) -> bool) {
+        self.targets = mem::take(&mut self.targets)
+            .into_iter()
+            .filter(|(t, s)| pred(t, s))
+            .collect();
+    }
+
+    /// Iterates all targets.
+    pub fn iter(&self) -> impl Iterator<Item = (&RewriteTarget, &RewriteState)> + '_ {
+        self.targets.iter()
+    }
+
+    /// Returns an iteration of the target keys.
+    pub fn keys(&self) -> impl Iterator<Item = RewriteTarget> + '_ {
+        self.targets.keys().cloned()
+    }
+
+    /// Adds a new rewrite target in state `Unchanged` if it doesn't exist yet. Returns
+    /// a boolean whether the entry is new and a mutable reference to the state.
+    pub fn entry(&mut self, target: RewriteTarget) -> (bool, &mut RewriteState) {
+        let mut is_new = false;
+        let state = self.targets.entry(target).or_insert_with(|| {
+            is_new = true;
+            RewriteState::Unchanged
+        });
+        (is_new, state)
+    }
+
+    /// Gets the current state of the target.
+    pub fn state(&self, target: &RewriteTarget) -> &RewriteState {
+        self.targets.get(target).expect("state defined")
+    }
+
+    /// Gets the mutable current state of the target.
+    pub fn state_mut(&mut self, target: &RewriteTarget) -> &mut RewriteState {
+        self.targets.get_mut(target).expect("state defined")
+    }
+
+    /// Updates the global env based on the current state. This consumes
+    /// the rewrite targets.
+    pub fn write_to_env(self, env: &mut GlobalEnv) {
+        for (target, state) in self.targets {
+            use RewriteState::*;
+            use RewriteTarget::*;
+            match (target, state) {
+                (_, Unchanged) => {},
+                (MoveFun(fnid), Def(def)) => env.set_function_def(fnid, def),
+                (SpecFun(fnid), Def(def)) => env.get_spec_fun_mut(fnid).body = Some(def),
+                (SpecBlock(sb_target), Spec(spec)) => {
+                    *env.get_spec_block_mut(&sb_target) = spec;
+                },
+                _ => panic!("unexpected rewrite target and result combination"),
+            }
+        }
+    }
+}
+
+impl RewriteTarget {
+    /// Gets the call sites for the target.
+    pub fn called_funs_with_call_sites(
+        &self,
+        env: &GlobalEnv,
+    ) -> BTreeMap<QualifiedId<FunId>, BTreeSet<NodeId>> {
+        use RewriteTarget::*;
+        match self {
+            MoveFun(id) => env
+                .get_function(*id)
+                .get_def()
+                .map(|e| e.called_funs_with_callsites())
+                .unwrap_or_default(),
+            SpecFun(id) => env
+                .get_spec_fun(*id)
+                .body
+                .as_ref()
+                .map(|e| e.called_funs_with_callsites())
+                .unwrap_or_default(),
+            SpecBlock(target) => {
+                let spec = env.get_spec_block(target);
+                spec.called_funs_with_callsites()
+            },
+        }
+    }
+
+    /// Get the environment state of this target in form of a RewriteState.
+    pub fn get_env_state(&self, env: &GlobalEnv) -> RewriteState {
+        use RewriteState::*;
+        use RewriteTarget::*;
+        match self {
+            MoveFun(fid) => env
+                .get_function(*fid)
+                .get_def()
+                .map(|e| Def(e.clone()))
+                .unwrap_or(Abstract),
+            SpecFun(fid) => env
+                .get_spec_fun(*fid)
+                .body
+                .clone()
+                .map(Def)
+                .unwrap_or(Abstract),
+            SpecBlock(sb_target) => Spec(env.get_spec_block(sb_target).clone()),
+        }
+    }
+}