diff --git a/vm/framework/starcoin-framework/doc/overview.md b/vm/framework/starcoin-framework/doc/overview.md
index 5844e018b8..6fef5fb459 100644
--- a/vm/framework/starcoin-framework/doc/overview.md
+++ b/vm/framework/starcoin-framework/doc/overview.md
@@ -81,6 +81,7 @@ This is the reference documentation of the Starcoin framework.
- [`0x1::stc_block`](stc_block.md#0x1_stc_block)
- [`0x1::stc_genesis`](stc_genesis.md#0x1_stc_genesis)
- [`0x1::stc_language_version`](stc_language_version.md#0x1_stc_language_version)
+- [`0x1::stc_offer`](stc_offer.md#0x1_stc_offer)
- [`0x1::stc_transaction_fee`](stc_transaction_fee.md#0x1_stc_transaction_fee)
- [`0x1::stc_transaction_package_validation`](stc_transaction_package_validation.md#0x1_stc_transaction_package_validation)
- [`0x1::stc_transaction_timeout`](stc_transaction_timeout.md#0x1_stc_transaction_timeout)
diff --git a/vm/framework/starcoin-framework/doc/stc_offer.md b/vm/framework/starcoin-framework/doc/stc_offer.md
new file mode 100644
index 0000000000..f963daa353
--- /dev/null
+++ b/vm/framework/starcoin-framework/doc/stc_offer.md
@@ -0,0 +1,289 @@
+
+
+
+# Module `0x1::stc_offer`
+
+
+
+- [Resource `Offer`](#0x1_stc_offer_Offer)
+- [Constants](#@Constants_0)
+- [Function `create`](#0x1_stc_offer_create)
+- [Function `redeem`](#0x1_stc_offer_redeem)
+- [Function `exists_at`](#0x1_stc_offer_exists_at)
+- [Function `address_of`](#0x1_stc_offer_address_of)
+- [Specification](#@Specification_1)
+ - [Function `create`](#@Specification_1_create)
+ - [Function `redeem`](#@Specification_1_redeem)
+ - [Function `exists_at`](#@Specification_1_exists_at)
+ - [Function `address_of`](#@Specification_1_address_of)
+
+
+use 0x1::error;
+use 0x1::signer;
+use 0x1::timestamp;
+
+
+
+
+
+
+## Resource `Offer`
+
+A wrapper around value offered that can be claimed by the address stored in for when after lock time.
+
+
+struct Offer<Offered> has key
+
+
+
+
+
+Fields
+
+
+
+-
+
offered: Offered
+
+-
+
+
+-
+
for_address: address
+
+-
+
+
+-
+
time_lock: u64
+
+-
+
+
+
+
+
+
+
+
+
+## Constants
+
+
+
+
+An offer of the specified type for the account does not match
+
+
+const EOFFER_DNE_FOR_ACCOUNT: u64 = 101;
+
+
+
+
+
+
+Offer is not unlocked yet.
+
+
+const EOFFER_NOT_UNLOCKED: u64 = 102;
+
+
+
+
+
+
+## Function `create`
+
+Publish a value of type Offered under the sender's account. The value can be claimed by
+either the for address or the transaction sender.
+
+
+public fun create<Offered: store>(account: &signer, offered: Offered, for_address: address, lock_period: u64)
+
+
+
+
+
+Implementation
+
+
+public fun create<Offered: store>(account: &signer, offered: Offered, for_address: address, lock_period: u64) {
+ let time_lock = timestamp::now_seconds() + lock_period;
+ //TODO should support multi Offer?
+ move_to(account, Offer<Offered> {
+ offered,
+ for_address,
+ time_lock
+ });
+}
+
+
+
+
+
+
+
+
+## Function `redeem`
+
+Claim the value of type Offered published at offer_address.
+Only succeeds if the sender is the intended recipient stored in for or the original
+publisher offer_address, and now >= time_lock
+Also fails if no such value exists.
+
+
+public fun redeem<Offered: store>(account: &signer, offer_address: address): Offered
+
+
+
+
+
+Implementation
+
+
+public fun redeem<Offered: store>(account: &signer, offer_address: address): Offered acquires Offer {
+ let Offer<Offered> { offered, for_address, time_lock } = move_from<Offer<Offered>>(offer_address);
+ let sender = signer::address_of(account);
+ let now = timestamp::now_seconds();
+ assert!(sender == for_address || sender == offer_address, error::invalid_argument(EOFFER_DNE_FOR_ACCOUNT));
+ assert!(now >= time_lock, error::invalid_state(EOFFER_NOT_UNLOCKED));
+ offered
+}
+
+
+
+
+
+
+
+
+## Function `exists_at`
+
+Returns true if an offer of type Offered exists at offer_address.
+
+
+public fun exists_at<Offered: store>(offer_address: address): bool
+
+
+
+
+
+Implementation
+
+
+public fun exists_at<Offered: store>(offer_address: address): bool {
+ exists<Offer<Offered>>(offer_address)
+}
+
+
+
+
+
+
+
+
+## Function `address_of`
+
+Returns the address of the Offered type stored at offer_address.
+Fails if no such Offer exists.
+
+
+public fun address_of<Offered: store>(offer_address: address): address
+
+
+
+
+
+Implementation
+
+
+public fun address_of<Offered: store>(offer_address: address): address acquires Offer {
+ borrow_global<Offer<Offered>>(offer_address).for_address
+}
+
+
+
+
+
+
+
+
+## Specification
+
+
+
+pragma verify = true;
+pragma aborts_if_is_strict = true;
+
+
+
+
+
+
+### Function `create`
+
+
+public fun create<Offered: store>(account: &signer, offered: Offered, for_address: address, lock_period: u64)
+
+
+
+
+
+aborts_if timestamp::now_seconds() + lock_period > max_u64();
+aborts_if exists<Offer<Offered>>(signer::address_of(account));
+
+
+
+
+
+
+### Function `redeem`
+
+
+public fun redeem<Offered: store>(account: &signer, offer_address: address): Offered
+
+
+
+
+
+aborts_if !exists<Offer<Offered>>(offer_address);
+aborts_if
+ signer::address_of(account) != global<Offer<Offered>>(offer_address).for_address
+ && signer::address_of(account) != offer_address;
+aborts_if timestamp::now_seconds() < global<Offer<Offered>>(offer_address).time_lock;
+
+
+
+
+
+
+### Function `exists_at`
+
+
+public fun exists_at<Offered: store>(offer_address: address): bool
+
+
+
+
+
+aborts_if false;
+
+
+
+
+
+
+### Function `address_of`
+
+
+public fun address_of<Offered: store>(offer_address: address): address
+
+
+
+
+
+aborts_if !exists<Offer<Offered>>(offer_address);
+
+
+
+[move-book]: https://starcoin.dev/move/book/SUMMARY
diff --git a/vm/framework/starcoin-framework/doc/timestamp.md b/vm/framework/starcoin-framework/doc/timestamp.md
index debe001975..75451986f0 100644
--- a/vm/framework/starcoin-framework/doc/timestamp.md
+++ b/vm/framework/starcoin-framework/doc/timestamp.md
@@ -137,7 +137,7 @@ Marks that time has started. This can only be called from genesis and with the s
Updates the wall clock time by consensus. Requires VM privilege and will be invoked during block prologue.
-public fun update_global_time(account: &signer, proposer: address, timestamp: u64)
+public fun update_global_time(account: &signer, _proposer: address, timestamp: u64)
@@ -148,7 +148,7 @@ Updates the wall clock time by consensus. Requires VM privilege and will be invo
public fun update_global_time(
account: &signer,
- proposer: address,
+ _proposer: address,
timestamp: u64
) acquires CurrentTimeMicroseconds {
debug::print(&std::string::utf8(b"timestamp::update_global_time | Entered"));
@@ -324,7 +324,7 @@ Gets the current time in seconds.
### Function `update_global_time`
-public fun update_global_time(account: &signer, proposer: address, timestamp: u64)
+public fun update_global_time(account: &signer, _proposer: address, timestamp: u64)
@@ -332,7 +332,7 @@ Gets the current time in seconds.
requires chain_status::is_operating();
include UpdateGlobalTimeAbortsIf;
-ensures (proposer != @vm_reserved) ==> (spec_now_microseconds() == timestamp);
+ensures (_proposer != @vm_reserved) ==> (spec_now_microseconds() == timestamp);
@@ -343,13 +343,13 @@ Gets the current time in seconds.
schema UpdateGlobalTimeAbortsIf {
account: signer;
- proposer: address;
+ _proposer: address;
timestamp: u64;
// This enforces high-level requirement 3:
aborts_if !system_addresses::is_vm(account);
// This enforces high-level requirement 4:
- aborts_if (proposer == @vm_reserved) && (spec_now_microseconds() != timestamp);
- aborts_if (proposer != @vm_reserved) && (spec_now_microseconds() >= timestamp);
+ aborts_if (_proposer == @vm_reserved) && (spec_now_microseconds() != timestamp);
+ aborts_if (_proposer != @vm_reserved) && (spec_now_microseconds() >= timestamp);
}
diff --git a/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.exp b/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.exp
index 1f9c04882d..7e93a0dbb1 100644
--- a/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.exp
+++ b/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.exp
@@ -2,24 +2,24 @@ processed 9 tasks
task 2 'run'. lines 5-20:
{
- "gas_used": 37319,
+ "gas_used": 48026,
"status": "Executed"
}
task 4 'run'. lines 24-40:
{
- "gas_used": 141885,
+ "gas_used": 351963,
"status": "Executed"
}
-task 6 'run'. lines 45-61:
+task 6 'run'. lines 45-62:
{
- "gas_used": 141885,
+ "gas_used": 351963,
"status": "Executed"
}
-task 8 'run'. lines 66-83:
+task 8 'run'. lines 67-89:
{
- "gas_used": 138625,
+ "gas_used": 354815,
"status": "Executed"
}
diff --git a/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.move b/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.move
index e26c561e8f..6d4c226421 100644
--- a/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.move
+++ b/vm/framework/starcoin-framework/integration-tests/treasury/linear_withdraw_cap.move
@@ -5,17 +5,17 @@
//# run --signers StarcoinAssociation
script {
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury;
+ use starcoin_framework::treasury;
//use starcoin_framework::Debug;
fun mint(account: signer) {
- let cap = Treasury::remove_linear_withdraw_capability(&account);
- assert!(Treasury::get_linear_withdraw_capability_total(&cap) == 477770400000000000, 1000);
- assert!(Treasury::get_linear_withdraw_capability_withdraw(&cap) == 0, 1001);
- assert!(Treasury::get_linear_withdraw_capability_start_time(&cap) == 0, 1002);
- starcoin_framework::Debug::print(&Treasury::get_linear_withdraw_capability_period(&cap));
- assert!(Treasury::get_linear_withdraw_capability_period(&cap) ==86400, 1003);
- Treasury::add_linear_withdraw_capability(&account, cap);
+ let cap = treasury::remove_linear_withdraw_capability(&account);
+ assert!(treasury::get_linear_withdraw_capability_total(&cap) == 477770400000000000, 1000);
+ assert!(treasury::get_linear_withdraw_capability_withdraw(&cap) == 0, 1001);
+ assert!(treasury::get_linear_withdraw_capability_start_time(&cap) == 0, 1002);
+ starcoin_framework::debug::print(&treasury::get_linear_withdraw_capability_period(&cap));
+ assert!(treasury::get_linear_withdraw_capability_period(&cap) == 86400, 1003);
+ treasury::add_linear_withdraw_capability(&account, cap);
}
}
@@ -23,19 +23,19 @@ script {
//# run --signers StarcoinAssociation
script {
- use starcoin_framework::account;
+ use std::signer;
+ use starcoin_std::debug;
+ use starcoin_framework::coin;
+ use starcoin_framework::treasury;
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury;
- use starcoin_framework::Token;
- use starcoin_framework::Debug;
fun mint(account: signer) {
- let linear_cap = Treasury::remove_linear_withdraw_capability(&account);
- let token = Treasury::withdraw_with_linear_capability(&mut linear_cap);
- Debug::print(&Token::value(&token));
- assert!(Token::value(&token) == 19907100000000000, 1004);
- Treasury::add_linear_withdraw_capability(&account, linear_cap);
- coin::deposit(&account, token);
+ let linear_cap = treasury::remove_linear_withdraw_capability(&account);
+ let token = treasury::withdraw_with_linear_capability(&mut linear_cap);
+ debug::print(&coin::value(&token));
+ assert!(coin::value(&token) == 19907100000000000, 1004);
+ treasury::add_linear_withdraw_capability(&account, linear_cap);
+ coin::deposit(signer::address_of(&account), token);
}
}
@@ -44,19 +44,20 @@ script {
//# run --signers StarcoinAssociation
script {
- use starcoin_framework::account;
+ use std::signer;
+ use starcoin_std::debug;
+
+ use starcoin_framework::coin;
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury;
- use starcoin_framework::Token;
- //use starcoin_framework::Debug;
+ use starcoin_framework::treasury;
fun mint(account: signer) {
- let linear_cap = Treasury::remove_linear_withdraw_capability(&account);
- let token = Treasury::withdraw_with_linear_capability(&mut linear_cap);
- starcoin_framework::Debug::print(&Token::value(&token));
- assert!(Token::value(&token) == 19907100000000000, 1005);
- Treasury::add_linear_withdraw_capability(&account, linear_cap);
- coin::deposit(&account, token);
+ let linear_cap = treasury::remove_linear_withdraw_capability(&account);
+ let token = treasury::withdraw_with_linear_capability(&mut linear_cap);
+ debug::print(&coin::value(&token));
+ assert!(coin::value(&token) == 19907100000000000, 1005);
+ treasury::add_linear_withdraw_capability(&account, linear_cap);
+ coin::deposit(signer::address_of(&account), token);
}
}
@@ -65,19 +66,24 @@ script {
//# run --signers StarcoinAssociation
script {
- use starcoin_framework::account;
+ use std::signer;
+ use starcoin_framework::coin;
+ use starcoin_std::debug;
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury;
- use starcoin_framework::Token;
- //use starcoin_framework::Debug;
+ use starcoin_framework::treasury;
fun mint(account: signer) {
- let cap = Treasury::remove_linear_withdraw_capability(&account);
- let token = Treasury::withdraw_with_linear_capability(&mut cap);
- starcoin_framework::Debug::print(&Token::value(&token));
- assert!(Token::value(&token) == (477770400000000000 - 19907100000000000*2), 1006);
- coin::deposit(&account, token);
- assert!(Treasury::get_linear_withdraw_capability_withdraw(&cap) == Treasury::get_linear_withdraw_capability_total(&cap), 1007);
- Treasury::destroy_linear_withdraw_capability(cap);
+ let cap = treasury::remove_linear_withdraw_capability(&account);
+ let token = treasury::withdraw_with_linear_capability(&mut cap);
+ debug::print(&coin::value(&token));
+ assert!(coin::value(&token) == (477770400000000000 - 19907100000000000 * 2), 1006);
+ coin::deposit(signer::address_of(&account), token);
+ assert!(
+ treasury::get_linear_withdraw_capability_withdraw(&cap) == treasury::get_linear_withdraw_capability_total(
+ &cap
+ ),
+ 1007
+ );
+ treasury::destroy_linear_withdraw_capability(cap);
}
}
\ No newline at end of file
diff --git a/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.exp b/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.exp
index c703f3ef90..aa0e264c53 100644
--- a/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.exp
+++ b/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.exp
@@ -1,19 +1,19 @@
processed 7 tasks
-task 2 'run'. lines 7-23:
+task 2 'run'. lines 7-22:
{
"gas_used": 25085,
"status": "Executed"
}
-task 4 'run'. lines 26-45:
+task 4 'run'. lines 25-45:
{
- "gas_used": 165065,
+ "gas_used": 358818,
"status": "Executed"
}
-task 6 'run'. lines 48-59:
+task 6 'run'. lines 48-60:
{
- "gas_used": 43352,
+ "gas_used": 40447,
"status": "Executed"
}
diff --git a/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.move b/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.move
index 3c82c31d30..b3f808450e 100644
--- a/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.move
+++ b/vm/framework/starcoin-framework/integration-tests/treasury/split_linear_cap.move
@@ -7,13 +7,12 @@
//# run --signers StarcoinAssociation
script {
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury;
- //use starcoin_framework::Debug;
+ use starcoin_framework::treasury;
fun mint(account: signer) {
- let cap = Treasury::remove_linear_withdraw_capability(&account);
- assert!(Treasury::get_linear_withdraw_capability_withdraw(&cap) == 0, 1001);
- Treasury::add_linear_withdraw_capability(&account, cap);
+ let cap = treasury::remove_linear_withdraw_capability(&account);
+ assert!(treasury::get_linear_withdraw_capability_withdraw(&cap) == 0, 1001);
+ treasury::add_linear_withdraw_capability(&account, cap);
}
}
@@ -25,17 +24,18 @@ script {
//# run --signers StarcoinAssociation
script {
- use starcoin_framework::Offer;
+ use std::signer;
+ use starcoin_framework::stc_offer;
+ use starcoin_framework::coin;
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury;
- use starcoin_framework::account;
+ use starcoin_framework::treasury;
fun bob_take_linear_key_from_offer(account: signer) {
- let cap = Treasury::remove_linear_withdraw_capability(&account);
- let (token, cap2) = Treasury::split_linear_withdraw_cap(&mut cap, 47777040000000000/2);
- Offer::create(&account, cap2, @alice, 0);
- coin::deposit(&account, token);
- Treasury::add_linear_withdraw_capability(&account, cap);
+ let cap = treasury::remove_linear_withdraw_capability(&account);
+ let (token, cap2) = treasury::split_linear_withdraw_cap(&mut cap, 47777040000000000 / 2);
+ stc_offer::create(&account, cap2, @alice, 0);
+ coin::deposit(signer::address_of(&account), token);
+ treasury::add_linear_withdraw_capability(&account, cap);
}
}
@@ -47,13 +47,14 @@ script {
//# run --signers alice
script {
- use starcoin_framework::Offer;
+ use starcoin_framework::stc_offer;
use starcoin_framework::starcoin_coin::STC;
- use starcoin_framework::Treasury::{Self, LinearWithdrawCapability};
+ use starcoin_framework::treasury::{Self, LinearWithdrawCapability};
fun alice_take_linear_key_from_offer(account: signer) {
- let cap = Offer::redeem>(&account, @StarcoinAssociation);
- assert!(Treasury::get_linear_withdraw_capability_total(&cap)==47777040000000000/2, 1002);
- Treasury::add_linear_withdraw_capability(&account, cap);
+ let cap =
+ stc_offer::redeem>(&account, @StarcoinAssociation);
+ assert!(treasury::get_linear_withdraw_capability_total(&cap) == 47777040000000000 / 2, 1002);
+ treasury::add_linear_withdraw_capability(&account, cap);
}
}
\ No newline at end of file
diff --git a/vm/framework/starcoin-framework/sources/stc/oracle.move b/vm/framework/starcoin-framework/sources/stc/oracle.move
index bf674cce7a..e024817ca0 100644
--- a/vm/framework/starcoin-framework/sources/stc/oracle.move
+++ b/vm/framework/starcoin-framework/sources/stc/oracle.move
@@ -3,11 +3,11 @@ module starcoin_framework::oracle {
use std::error;
use std::signer;
use std::vector;
- use starcoin_framework::timestamp;
- use starcoin_framework::reserved_accounts_signer;
- use starcoin_framework::system_addresses;
+
use starcoin_framework::account;
use starcoin_framework::event;
+ use starcoin_framework::system_addresses;
+ use starcoin_framework::timestamp;
struct OracleInfo has key {
///The datasource counter
diff --git a/vm/framework/starcoin-framework/sources/stc/stc_offer.move b/vm/framework/starcoin-framework/sources/stc/stc_offer.move
new file mode 100644
index 0000000000..5165e4343a
--- /dev/null
+++ b/vm/framework/starcoin-framework/sources/stc/stc_offer.move
@@ -0,0 +1,101 @@
+module starcoin_framework::stc_offer {
+ use std::error;
+ use std::signer;
+ use starcoin_framework::timestamp;
+
+ spec module {
+ pragma verify = true;
+ pragma aborts_if_is_strict = true;
+ }
+
+ /// A wrapper around value `offered` that can be claimed by the address stored in `for` when after lock time.
+ struct Offer has key {
+ offered: Offered,
+ for_address: address,
+ time_lock: u64
+ }
+
+ /// An offer of the specified type for the account does not match
+ const EOFFER_DNE_FOR_ACCOUNT: u64 = 101;
+
+ /// Offer is not unlocked yet.
+ const EOFFER_NOT_UNLOCKED: u64 = 102;
+
+ /// Publish a value of type `Offered` under the sender's account. The value can be claimed by
+ /// either the `for` address or the transaction sender.
+ public fun create(account: &signer, offered: Offered, for_address: address, lock_period: u64) {
+ let time_lock = timestamp::now_seconds() + lock_period;
+ //TODO should support multi Offer?
+ move_to(account, Offer {
+ offered,
+ for_address,
+ time_lock
+ });
+ }
+
+ spec create {
+ use starcoin_framework::timestamp;
+ use starcoin_framework::signer;
+
+ // include timestamp::AbortsIfTimestampNotExists;
+ aborts_if timestamp::now_seconds() + lock_period > max_u64();
+ aborts_if exists>(signer::address_of(account));
+ }
+
+ /// Claim the value of type `Offered` published at `offer_address`.
+ /// Only succeeds if the sender is the intended recipient stored in `for` or the original
+ /// publisher `offer_address`, and now >= time_lock
+ /// Also fails if no such value exists.
+ public fun redeem(account: &signer, offer_address: address): Offered acquires Offer {
+ let Offer { offered, for_address, time_lock } = move_from>(offer_address);
+ let sender = signer::address_of(account);
+ let now = timestamp::now_seconds();
+ assert!(sender == for_address || sender == offer_address, error::invalid_argument(EOFFER_DNE_FOR_ACCOUNT));
+ assert!(now >= time_lock, error::invalid_state(EOFFER_NOT_UNLOCKED));
+ offered
+ }
+
+ spec redeem {
+ use starcoin_framework::timestamp;
+ use starcoin_framework::signer;
+
+ aborts_if !exists>(offer_address);
+ aborts_if
+ signer::address_of(account) != global>(offer_address).for_address
+ && signer::address_of(account) != offer_address;
+ aborts_if timestamp::now_seconds() < global>(offer_address).time_lock;
+ // include timestamp::AbortsIfTimestampNotExists;
+ }
+
+ /// Returns true if an offer of type `Offered` exists at `offer_address`.
+ public fun exists_at(offer_address: address): bool {
+ exists>(offer_address)
+ }
+
+ spec exists_at {
+ aborts_if false;
+ }
+
+ /// Returns the address of the `Offered` type stored at `offer_address`.
+ /// Fails if no such `Offer` exists.
+ public fun address_of(offer_address: address): address acquires Offer {
+ borrow_global>(offer_address).for_address
+ }
+
+ spec address_of {
+ aborts_if !exists>(offer_address);
+ }
+
+ // /// Take Offer and put to signer's Collection.
+ // public entry fun take_offer(
+ // signer: signer,
+ // offer_address: address,
+ // ) acquires Offer {
+ // let offered = redeem(&signer, offer_address);
+ // Collection2::put(&signer, signer::address_of(&signer), offered);
+ // }
+
+ // spec take_offer {
+ // pragma verify = false;
+ // }
+}
\ No newline at end of file
diff --git a/vm/framework/starcoin-framework/sources/stc/treasury.move b/vm/framework/starcoin-framework/sources/stc/treasury.move
index a963953a8d..7bbc5ed870 100644
--- a/vm/framework/starcoin-framework/sources/stc/treasury.move
+++ b/vm/framework/starcoin-framework/sources/stc/treasury.move
@@ -2,14 +2,15 @@
module starcoin_framework::treasury {
use std::error;
use std::signer;
- use starcoin_std::math128;
- use starcoin_std::type_info;
- use starcoin_framework::timestamp;
- use starcoin_framework::stc_util;
+
use starcoin_framework::account;
- use starcoin_framework::event;
use starcoin_framework::coin;
+ use starcoin_framework::event;
+ use starcoin_framework::stc_util;
+ use starcoin_framework::timestamp;
+ use starcoin_std::math128;
+ use starcoin_std::type_info;
struct Treasury has store, key {
balance: coin::Coin,
diff --git a/vm/framework/starcoin-framework/sources/timestamp.move b/vm/framework/starcoin-framework/sources/timestamp.move
index 936c17d41c..46a99fb487 100644
--- a/vm/framework/starcoin-framework/sources/timestamp.move
+++ b/vm/framework/starcoin-framework/sources/timestamp.move
@@ -36,7 +36,7 @@ module starcoin_framework::timestamp {
/// Updates the wall clock time by consensus. Requires VM privilege and will be invoked during block prologue.
public fun update_global_time(
account: &signer,
- proposer: address,
+ _proposer: address,
timestamp: u64
) acquires CurrentTimeMicroseconds {
debug::print(&std::string::utf8(b"timestamp::update_global_time | Entered"));
diff --git a/vm/framework/starcoin-framework/sources/timestamp.spec.move b/vm/framework/starcoin-framework/sources/timestamp.spec.move
index 74bd5581e2..d2cb143ef7 100644
--- a/vm/framework/starcoin-framework/sources/timestamp.spec.move
+++ b/vm/framework/starcoin-framework/sources/timestamp.spec.move
@@ -40,18 +40,18 @@ spec starcoin_framework::timestamp {
use starcoin_framework::chain_status;
requires chain_status::is_operating();
include UpdateGlobalTimeAbortsIf;
- ensures (proposer != @vm_reserved) ==> (spec_now_microseconds() == timestamp);
+ ensures (_proposer != @vm_reserved) ==> (spec_now_microseconds() == timestamp);
}
spec schema UpdateGlobalTimeAbortsIf {
account: signer;
- proposer: address;
+ _proposer: address;
timestamp: u64;
/// [high-level-req-3]
aborts_if !system_addresses::is_vm(account);
/// [high-level-req-4]
- aborts_if (proposer == @vm_reserved) && (spec_now_microseconds() != timestamp);
- aborts_if (proposer != @vm_reserved) && (spec_now_microseconds() >= timestamp);
+ aborts_if (_proposer == @vm_reserved) && (spec_now_microseconds() != timestamp);
+ aborts_if (_proposer != @vm_reserved) && (spec_now_microseconds() >= timestamp);
}
spec fun spec_now_microseconds(): u64 {