Support the custom boogie file (aptos-labs#3206)

- Added `aptos-natives.bpl`
- `Aptos CLI` includes it in invoking Prover
- Separated the spec from the code
- Prover should finish without error for the Aptos Framework

Author: junkil-park

.dockerignore

@@ -16,6 +16,7 @@
 !**/*.mrb
 !config/src/config/test_data
 !aptos-move/framework/
+!crates/aptos/src/move_tool/*.bpl
 !api/doc/
 !ecosystem/indexer/migrations/**/*.sql
 !terraform/helm/aptos-node/

Cargo.lock

@@ -0,0 +1,17 @@
+spec aptos_framework::aggregator {
+    spec add { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec sub { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec read { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec destroy { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

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

@@ -0,0 +1,5 @@
+spec aptos_framework::aggregator_factory {
+    spec new_aggregator { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

aptos-move/framework/aptos-framework/sources/aggregator/aggregator_factory.spec.move

@@ -0,0 +1,5 @@
+spec aptos_framework::state_storage {
+    spec get_state_storage_usage_only_at_epoch_beginning { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

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

@@ -1,10 +1,12 @@
 spec aptos_framework::timestamp {
     spec set_time_has_started {
+        use std::signer;
         /// This function can't be verified on its own and has to be verified in the context of Genesis execution.
         ///
         /// After time has started, all invariants guarded by `Timestamp::is_operating` will become activated
         /// and need to hold.
         pragma delegate_invariants_to_caller;
+        aborts_if exists<CurrentTimeMicroseconds>(signer::address_of(account));
         include AbortsIfNotGenesis;
         include system_addresses::AbortsIfNotAptosFramework{account};
         ensures is_operating();
@@ -52,11 +54,6 @@ spec aptos_framework::timestamp {
         spec_now_microseconds() / MICRO_CONVERSION_FACTOR
     }
 
-    spec assert_genesis {
-        pragma opaque = true;
-        include AbortsIfNotGenesis;
-    }
-
     /// Helper schema to specify that a function aborts if not in genesis.
     spec schema AbortsIfNotGenesis {
         aborts_if !is_genesis() with error::INVALID_STATE;

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

@@ -6,7 +6,7 @@ version = "1.0.0"
 std = "0x1"
 aptos_std = "0x1"
 aptos_framework = "0x1"
-Extensions = "0x1" # TODO: Needed for Prover to instantiate `{{Ext}}` in prelude.
+Extensions = "0x1" # For Prover to instantiate `{{Ext}}` in prelude.
 
 [dependencies]
 MoveStdlib = { local = "../move-stdlib" }

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

@@ -190,14 +190,4 @@ module std::capability {
             vector::push_back(v, x)
         }
     }
-
-    /// Helper specification function to check whether a capability exists at address.
-    spec fun spec_has_cap<Feature>(addr: address): bool {
-        exists<CapState<Feature>>(addr)
-    }
-
-    /// Helper specification function to obtain the delegates of a capability.
-    spec fun spec_delegates<Feature>(addr: address): vector<address> {
-        global<CapState<Feature>>(addr).delegates
-    }
 }

aptos-move/framework/aptos-stdlib/sources/capability.move

@@ -0,0 +1,11 @@
+spec std::capability {
+    /// Helper specification function to check whether a capability exists at address.
+    spec fun spec_has_cap<Feature>(addr: address): bool {
+        exists<CapState<Feature>>(addr)
+    }
+
+    /// Helper specification function to obtain the delegates of a capability.
+    spec fun spec_delegates<Feature>(addr: address): vector<address> {
+        global<CapState<Feature>>(addr).delegates
+    }
+}

aptos-move/framework/aptos-stdlib/sources/capability.spec.move

@@ -302,9 +302,6 @@ module aptos_std::bls12381 {
         public_key: vector<u8>,
         proof_of_possesion: vector<u8>
     ): bool;
-    spec verify_proof_of_possession { // TODO: temporary mockup.
-        pragma opaque;
-    }
 
     /// CRYPTOGRAPHY WARNING: Assumes the public key has a valid proof-of-possesion (PoP). This prevents rogue-key
     /// attacks later on during signature aggregation.

aptos-move/framework/aptos-stdlib/sources/cryptography/bls12381.move

@@ -0,0 +1,37 @@
+spec aptos_std::bls12381 {
+    spec aggregate_pubkeys_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec aggregate_signatures_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec validate_pubkey_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec signature_subgroup_check_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec verify_aggregate_signature_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec verify_multisignature_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec verify_normal_signature_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec verify_proof_of_possession_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec verify_signature_share_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/cryptography/bls12381.spec.move

@@ -0,0 +1,9 @@
+spec aptos_std::ed25519 {
+    spec public_key_validate_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec signature_verify_strict_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move

@@ -0,0 +1,5 @@
+spec aptos_std::secp256k1 {
+    spec ecdsa_recover_internal { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/cryptography/secp256k1.spec.move

@@ -41,17 +41,11 @@ module aptos_std::event {
     public fun guid<T: drop + store>(handle_ref: &EventHandle<T>): &GUID {
         &handle_ref.guid
     }
-    spec guid {
-        pragma intrinsic = false;
-    }
 
     /// Return the current counter associated with this EventHandle
     public fun counter<T: drop + store>(handle_ref: &EventHandle<T>): u64 {
         handle_ref.counter
     }
-    spec counter {
-        pragma intrinsic = false;
-    }
 
     /// Log `msg` as the `count`th event associated with the event stream identified by `guid`
     native fun write_to_event_store<T: drop + store>(guid: vector<u8>, count: u64, msg: T);
@@ -68,21 +62,4 @@ module aptos_std::event {
         let EventHandle<T> { counter: _, guid } = new_event_handle<T>(s);
         guid
     }
-
-    // ****************** SPECIFICATIONS *******************
-    spec module {} // switch documentation context to module
-
-    spec module {
-        /// Functions of the event module are mocked out using the intrinsic
-        /// pragma. They are implemented in the prover's prelude.
-        pragma intrinsic = true;
-
-        /// Determines equality between the guids of two event handles. Since fields of intrinsic
-        /// structs cannot be accessed, this function is provided.
-        fun spec_guid_eq<T>(h1: EventHandle<T>, h2: EventHandle<T>): bool {
-            // The implementation currently can just use native equality since the mocked prover
-            // representation does not have the `counter` field.
-            h1 == h2
-        }
-    }
 }

aptos-move/framework/aptos-stdlib/sources/event.move

@@ -0,0 +1,18 @@
+spec aptos_std::event {
+    // ****************** SPECIFICATIONS *******************
+    spec module {} // switch documentation context to module
+
+    spec module {
+        /// Functions of the event module are mocked out using the intrinsic
+        /// pragma. They are implemented in the prover's prelude.
+        pragma intrinsic = true;
+
+        /// Determines equality between the guids of two event handles. Since fields of intrinsic
+        /// structs cannot be accessed, this function is provided.
+        fun spec_guid_eq<T>(h1: EventHandle<T>, h2: EventHandle<T>): bool {
+            // The implementation currently can just use native equality since the mocked prover
+            // representation does not have the `counter` field.
+            h1 == h2
+        }
+    }
+}

aptos-move/framework/aptos-stdlib/sources/event.spec.move

@@ -9,9 +9,4 @@ module aptos_std::aptos_hash {
 
         sip_hash(bytes)
     }
-
-    spec sip_hash_from_value {
-        // TODO: temporary mockup.
-        pragma opaque;
-    }
 }

aptos-move/framework/aptos-stdlib/sources/hash.move

@@ -0,0 +1,11 @@
+spec aptos_std::aptos_hash {
+    spec sip_hash_from_value {
+        // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec sip_hash {
+        // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/hash.spec.move

@@ -22,10 +22,6 @@ module aptos_std::type_info {
     public native fun type_of<T>(): TypeInfo;
     public native fun type_name<T>(): string::String;
 
-    spec type_of { // TODO: temporary mockup.
-        pragma opaque;
-    }
-
     #[test]
     fun test() {
         let type_info = type_of<TypeInfo>();

aptos-move/framework/aptos-stdlib/sources/type_info.move

@@ -0,0 +1,9 @@
+spec aptos_std::type_info {
+    spec type_of { // TODO: temporary mockup.
+        pragma opaque;
+    }
+
+    spec type_name { // TODO: temporary mockup.
+        pragma opaque;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/type_info.spec.move

@@ -4,6 +4,3 @@ version = "1.5.0"
 
 [addresses]
 std = "0x1"
-
-[dev-addresses]
-std = "0x1"

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

@@ -35,6 +35,7 @@ move-ir-compiler = { git = "https://github.com/move-language/move", rev = "41395
 move-model = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }
 move-package = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }
 move-prover = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }
+move-prover-boogie-backend = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }
 move-prover-test-utils = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }
 move-resource-viewer = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }
 move-stackless-bytecode-interpreter = { git = "https://github.com/move-language/move", rev = "413955ea9246356b18af006584eb73283e9508da" }

aptos-move/move-deps/Cargo.toml

@@ -15,6 +15,7 @@ pub use move_ir_compiler;
 pub use move_model;
 pub use move_package;
 pub use move_prover;
+pub use move_prover_boogie_backend;
 pub use move_prover_test_utils;
 pub use move_resource_viewer;
 pub use move_stackless_bytecode_interpreter;

aptos-move/move-deps/src/lib.rs

@@ -0,0 +1,2 @@
+// Copyright (c) Aptos
+// SPDX-License-Identifier: Apache-2.0

crates/aptos/src/move_tool/aptos-natives.bpl

@@ -48,7 +48,7 @@ use move_deps::{
         language_storage::{ModuleId, TypeTag},
     },
     move_package::{source_package::layout::SourcePackageLayout, BuildConfig},
-    move_prover,
+    move_prover, move_prover_boogie_backend,
     move_unit_test::UnitTestingConfig,
 };
 use std::fmt::{Display, Formatter};
@@ -322,6 +322,16 @@ impl CliCommand<&'static str> for ProvePackage {
             install_dir: self.move_options.output_dir.clone(),
             ..Default::default()
         };
+
+        const APTOS_NATIVE_TEMPLATE: &[u8] = include_bytes!("aptos-natives.bpl");
+
+        let mut options = move_prover::cli::Options::default();
+        options.backend.custom_natives =
+            Some(move_prover_boogie_backend::options::CustomNativeOptions {
+                template_bytes: APTOS_NATIVE_TEMPLATE.to_vec(),
+                module_instance_names: vec![],
+            });
+
         let result = task::spawn_blocking(move || {
             move_cli::base::prove::run_move_prover(
                 config,