From 8072655966189a091e1d3df8d292247ca97e47b0 Mon Sep 17 00:00:00 2001 From: Jason <111507345+0xOutOfGas@users.noreply.github.com> Date: Wed, 14 Dec 2022 01:50:12 +0800 Subject: [PATCH] [Spec] Added specs for module gas_schedule & aptos_coin & chain_id & chain_status. (#5771) * Updated the spec of gas_schedule * add aptos_coin & chain_id & chain_status spec * Generate spec doc * Updated chain_status.spec.move * Updated chain_status.spec.move * Generate spec doc Co-authored-by: yoyoping Co-authored-by: tiutiutiu --- .../aptos-framework/doc/aptos_coin.md | 135 ++++++++++++++++++ .../framework/aptos-framework/doc/chain_id.md | 47 ++++++ .../aptos-framework/doc/chain_status.md | 41 ++++++ .../aptos-framework/doc/gas_schedule.md | 37 ++++- .../framework/aptos-framework/doc/util.md | 11 ++ .../sources/aptos_coin.spec.move | 43 ++++++ .../sources/chain_id.spec.move | 17 +++ .../sources/chain_status.spec.move | 13 ++ .../sources/configs/gas_schedule.spec.move | 33 ++++- .../aptos-framework/sources/util.spec.move | 7 +- 10 files changed, 374 insertions(+), 10 deletions(-) create mode 100644 aptos-move/framework/aptos-framework/sources/aptos_coin.spec.move create mode 100644 aptos-move/framework/aptos-framework/sources/chain_id.spec.move diff --git a/aptos-move/framework/aptos-framework/doc/aptos_coin.md b/aptos-move/framework/aptos-framework/doc/aptos_coin.md index 58cd19caded47..7c92f2b9051b3 100644 --- a/aptos-move/framework/aptos-framework/doc/aptos_coin.md +++ b/aptos-move/framework/aptos-framework/doc/aptos_coin.md @@ -20,6 +20,14 @@ modified from https://github.com/move-language/move/tree/main/language/documenta - [Function `delegate_mint_capability`](#0x1_aptos_coin_delegate_mint_capability) - [Function `claim_mint_capability`](#0x1_aptos_coin_claim_mint_capability) - [Function `find_delegation`](#0x1_aptos_coin_find_delegation) +- [Specification](#@Specification_1) + - [Function `initialize`](#@Specification_1_initialize) + - [Function `destroy_mint_cap`](#@Specification_1_destroy_mint_cap) + - [Function `configure_accounts_for_test`](#@Specification_1_configure_accounts_for_test) + - [Function `mint`](#@Specification_1_mint) + - [Function `delegate_mint_capability`](#@Specification_1_delegate_mint_capability) + - [Function `claim_mint_capability`](#@Specification_1_claim_mint_capability) + - [Function `find_delegation`](#@Specification_1_find_delegation) 
use 0x1::coin;
@@ -454,5 +462,132 @@ Claim the delegated mint capability and destroy the delegated token.
 
 
 
+
+
+## Specification
+
+
+
+
pragma verify = true;
+pragma aborts_if_is_strict;
+

+
+
+
+
+
+### Function `initialize`
+
+
+
public(friend) fun initialize(aptos_framework: &signer): (coin::BurnCapability<aptos_coin::AptosCoin>, coin::MintCapability<aptos_coin::AptosCoin>)
+

+
+
+
+
+
pragma aborts_if_is_partial;
+let addr = signer::address_of(aptos_framework);
+ensures exists<MintCapStore>(addr);
+ensures exists<coin::CoinInfo<AptosCoin>>(addr);
+

+
+
+
+
+
+### Function `destroy_mint_cap`
+
+
+
public(friend) fun destroy_mint_cap(aptos_framework: &signer)
+

+
+
+
+
+
let addr = signer::address_of(aptos_framework);
+aborts_if addr != @aptos_framework;
+aborts_if !exists<MintCapStore>(@aptos_framework);
+

+
+
+
+
+
+### Function `configure_accounts_for_test`
+
+
+
public(friend) fun configure_accounts_for_test(aptos_framework: &signer, core_resources: &signer, mint_cap: coin::MintCapability<aptos_coin::AptosCoin>)
+

+
+
+
+
+
pragma verify = false;
+

+
+
+
+
+
+### Function `mint`
+
+
+
public entry fun mint(account: &signer, dst_addr: address, amount: u64)
+

+
+
+
+
+
pragma verify = false;
+

+
+
+
+
+
+### Function `delegate_mint_capability`
+
+
+
public entry fun delegate_mint_capability(account: signer, to: address)
+

+
+
+
+
+
pragma verify = false;
+

+
+
+
+
+
+### Function `claim_mint_capability`
+
+
+
public entry fun claim_mint_capability(account: &signer)
+

+
+
+
+
+
pragma verify = false;
+

+
+
+
+
+
+### Function `find_delegation`
+
+
+
fun find_delegation(addr: address): option::Option<u64>
+

+
+
+
+
+
aborts_if !exists<Delegations>(@core_resources);
+

+
 
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-framework/doc/chain_id.md b/aptos-move/framework/aptos-framework/doc/chain_id.md
index 438c472e5dc8b..bb1ea5fe80964 100644
--- a/aptos-move/framework/aptos-framework/doc/chain_id.md
+++ b/aptos-move/framework/aptos-framework/doc/chain_id.md
@@ -11,6 +11,9 @@ This code provides a container for storing a chain id and functions to initializ
 -  [Resource `ChainId`](#0x1_chain_id_ChainId)
 -  [Function `initialize`](#0x1_chain_id_initialize)
 -  [Function `get`](#0x1_chain_id_get)
+-  [Specification](#@Specification_0)
+    -  [Function `initialize`](#@Specification_0_initialize)
+    -  [Function `get`](#@Specification_0_get)
 
 
 
use 0x1::system_addresses;
@@ -97,5 +100,49 @@ Return the chain ID of this instance.
 
 
 
+
+
+## Specification
+
+
+
+
pragma verify = true;
+pragma aborts_if_is_strict;
+

+
+
+
+
+
+### Function `initialize`
+
+
+
public(friend) fun initialize(aptos_framework: &signer, id: u8)
+

+
+
+
+
+
let addr = signer::address_of(aptos_framework);
+aborts_if addr != @aptos_framework;
+aborts_if exists<ChainId>(@aptos_framework);
+

+
+
+
+
+
+### Function `get`
+
+
+
public fun get(): u8
+

+
+
+
+
+
aborts_if !exists<ChainId>(@aptos_framework);
+

+
 
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-framework/doc/chain_status.md b/aptos-move/framework/aptos-framework/doc/chain_status.md
index dbc7bcf0304ae..d8a79897e3d77 100644
--- a/aptos-move/framework/aptos-framework/doc/chain_status.md
+++ b/aptos-move/framework/aptos-framework/doc/chain_status.md
@@ -18,6 +18,8 @@ which reflect that the system has been successfully initialized.
 -  [Function `assert_genesis`](#0x1_chain_status_assert_genesis)
 -  [Specification](#@Specification_1)
     -  [Function `set_genesis_end`](#@Specification_1_set_genesis_end)
+    -  [Function `assert_operating`](#@Specification_1_assert_operating)
+    -  [Function `assert_genesis`](#@Specification_1_assert_genesis)
 
 
 
use 0x1::error;
@@ -212,6 +214,13 @@ Helper function to assert genesis state.
 ## Specification
 
 
+
+
pragma verify = true;
+pragma aborts_if_is_strict;
+

+
+
+
 
 
 ### Function `set_genesis_end`
@@ -238,4 +247,36 @@ Helper function to assert genesis state.
 

 
 
+
+
+
+### Function `assert_operating`
+
+
+
public fun assert_operating()
+

+
+
+
+
+
aborts_if !is_operating();
+

+
+
+
+
+
+### Function `assert_genesis`
+
+
+
public fun assert_genesis()
+

+
+
+
+
+
aborts_if !is_genesis();
+

+
+
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-framework/doc/gas_schedule.md b/aptos-move/framework/aptos-framework/doc/gas_schedule.md
index 35728810aeede..af06dee5d06a7 100644
--- a/aptos-move/framework/aptos-framework/doc/gas_schedule.md
+++ b/aptos-move/framework/aptos-framework/doc/gas_schedule.md
@@ -15,6 +15,7 @@ it costs to execute Move on the network.
 -  [Function `set_gas_schedule`](#0x1_gas_schedule_set_gas_schedule)
 -  [Function `set_storage_gas_config`](#0x1_gas_schedule_set_storage_gas_config)
 -  [Specification](#@Specification_1)
+    -  [Function `initialize`](#@Specification_1_initialize)
     -  [Function `set_gas_schedule`](#@Specification_1_set_gas_schedule)
     -  [Function `set_storage_gas_config`](#@Specification_1_set_storage_gas_config)
 
@@ -255,6 +256,32 @@ This can be called by on-chain governance to update the gas schedule.
 ## Specification
 
 
+
+
pragma verify = true;
+pragma aborts_if_is_strict;
+

+
+
+
+
+
+### Function `initialize`
+
+
+
public(friend) fun initialize(aptos_framework: &signer, gas_schedule_blob: vector<u8>)
+

+
+
+
+
+
include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
+aborts_if len(gas_schedule_blob) == 0;
+aborts_if exists<GasScheduleV2>(signer::address_of(aptos_framework));
+ensures exists<GasScheduleV2>(signer::address_of(aptos_framework));
+

+
+
+
 
 
 ### Function `set_gas_schedule`
@@ -266,7 +293,12 @@ This can be called by on-chain governance to update the gas schedule.
 
 
 
-
requires chain_status::is_operating();
+
include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
+aborts_if len(gas_schedule_blob) == 0;
+let new_gas_schedule = util::spec_from_bytes<GasScheduleV2>(gas_schedule_blob);
+let gas_schedule = global<GasScheduleV2>(@aptos_framework);
+aborts_if exists<GasScheduleV2>(@aptos_framework) && new_gas_schedule.feature_version < gas_schedule.feature_version;
+ensures exists<GasScheduleV2>(signer::address_of(aptos_framework));
 

 
 
@@ -282,7 +314,8 @@ This can be called by on-chain governance to update the gas schedule.
 
 
 
-
requires chain_status::is_operating();
+
include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
+aborts_if !exists<StorageGasConfig>(@aptos_framework);
 

 
 
diff --git a/aptos-move/framework/aptos-framework/doc/util.md b/aptos-move/framework/aptos-framework/doc/util.md
index 0d809e1c1d759..9ee071c4b9414 100644
--- a/aptos-move/framework/aptos-framework/doc/util.md
+++ b/aptos-move/framework/aptos-framework/doc/util.md
@@ -84,6 +84,17 @@ owned.
 
 
 
pragma opaque;
+aborts_if [abstract] false;
+ensures [abstract] result == spec_from_bytes<T>(bytes);
+

+
+
+
+
+
+
+
+
fun spec_from_bytes<T>(bytes: vector<u8>): T;
 

 
 
diff --git a/aptos-move/framework/aptos-framework/sources/aptos_coin.spec.move b/aptos-move/framework/aptos-framework/sources/aptos_coin.spec.move
new file mode 100644
index 0000000000000..bb0898069f26c
--- /dev/null
+++ b/aptos-move/framework/aptos-framework/sources/aptos_coin.spec.move
@@ -0,0 +1,43 @@
+spec aptos_framework::aptos_coin {
+    spec module {
+        pragma verify = true;
+        pragma aborts_if_is_strict;
+    }
+
+    spec initialize {
+        pragma aborts_if_is_partial;
+        let addr = signer::address_of(aptos_framework);
+        ensures exists(addr);
+        ensures exists>(addr);
+    }
+
+    spec destroy_mint_cap {
+        let addr = signer::address_of(aptos_framework);
+        aborts_if addr != @aptos_framework;
+        aborts_if !exists(@aptos_framework);
+    }
+
+    // Test function,not needed verify.
+    spec configure_accounts_for_test {
+        pragma verify = false;
+    }
+
+    // Only callable in tests and testnets.not needed verify.
+    spec mint {
+        pragma verify = false;
+    }
+
+    // Only callable in tests and testnets.not needed verify.
+    spec delegate_mint_capability {
+        pragma verify = false;
+    }
+
+    // Only callable in tests and testnets.not needed verify.
+    spec claim_mint_capability(account: &signer) {
+        pragma verify = false;
+    }
+
+    spec find_delegation(addr: address): Option {
+        aborts_if !exists(@core_resources);
+    }
+}
diff --git a/aptos-move/framework/aptos-framework/sources/chain_id.spec.move b/aptos-move/framework/aptos-framework/sources/chain_id.spec.move
new file mode 100644
index 0000000000000..6cc04dba47093
--- /dev/null
+++ b/aptos-move/framework/aptos-framework/sources/chain_id.spec.move
@@ -0,0 +1,17 @@
+spec aptos_framework::chain_id {
+    spec module {
+        pragma verify = true;
+        pragma aborts_if_is_strict;
+    }
+
+    spec initialize {
+        use std::signer;
+        let addr = signer::address_of(aptos_framework);
+        aborts_if addr != @aptos_framework;
+        aborts_if exists(@aptos_framework);
+    }
+
+    spec get {
+        aborts_if !exists(@aptos_framework);
+    }
+}
diff --git a/aptos-move/framework/aptos-framework/sources/chain_status.spec.move b/aptos-move/framework/aptos-framework/sources/chain_status.spec.move
index 63a30dc90ca5f..3e51aa132e8fa 100644
--- a/aptos-move/framework/aptos-framework/sources/chain_status.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/chain_status.spec.move
@@ -1,4 +1,9 @@
 spec aptos_framework::chain_status {
+    spec module {
+        pragma verify = true;
+        pragma aborts_if_is_strict;
+    }
+
     spec set_genesis_end {
         pragma verify = false;
     }
@@ -6,4 +11,12 @@ spec aptos_framework::chain_status {
     spec schema RequiresIsOperating {
         requires is_operating();
     }
+
+    spec assert_operating {
+        aborts_if !is_operating();
+    }
+
+    spec assert_genesis {
+        aborts_if !is_genesis();
+    }
 }
diff --git a/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move b/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move
index ed5bacff5be3e..89611fa13bcba 100644
--- a/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move
@@ -1,11 +1,32 @@
 spec aptos_framework::gas_schedule {
-    spec set_gas_schedule {
-        use aptos_framework::chain_status;
-        requires chain_status::is_operating();
+    spec module {
+        pragma verify = true;
+        pragma aborts_if_is_strict;
     }
 
-    spec set_storage_gas_config {
-        use aptos_framework::chain_status;
-        requires chain_status::is_operating();
+    spec initialize(aptos_framework: &signer, gas_schedule_blob: vector) {
+        use std::signer;
+
+        include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
+        aborts_if len(gas_schedule_blob) == 0;
+        aborts_if exists(signer::address_of(aptos_framework));
+        ensures exists(signer::address_of(aptos_framework));
+    }
+
+    spec set_gas_schedule(aptos_framework: &signer, gas_schedule_blob: vector) {
+        use std::signer;
+        use aptos_framework::util;
+
+        include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
+        aborts_if len(gas_schedule_blob) == 0;
+        let new_gas_schedule = util::spec_from_bytes(gas_schedule_blob);
+        let gas_schedule = global(@aptos_framework);
+        aborts_if exists(@aptos_framework) && new_gas_schedule.feature_version < gas_schedule.feature_version;
+        ensures exists(signer::address_of(aptos_framework));
+    }
+
+    spec set_storage_gas_config(aptos_framework: &signer, config: StorageGasConfig) {
+        include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
+        aborts_if !exists(@aptos_framework);
     }
 }
diff --git a/aptos-move/framework/aptos-framework/sources/util.spec.move b/aptos-move/framework/aptos-framework/sources/util.spec.move
index 8447fab9df6a4..690ee63fdd553 100644
--- a/aptos-move/framework/aptos-framework/sources/util.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/util.spec.move
@@ -1,6 +1,9 @@
 spec aptos_framework::util {
-    spec from_bytes {
-        // TODO: temporary mockup.
+    spec from_bytes(bytes: vector): T {
         pragma opaque;
+        aborts_if [abstract] false;
+        ensures [abstract] result == spec_from_bytes(bytes);
     }
+
+    spec fun spec_from_bytes(bytes: vector): T;
 }