timestamp - [mainnet]
This module keeps a global wall clock that stores the current Unix time in microseconds. It interacts with the other modules in the following ways:
- genesis: to initialize the timestamp
- block: to reach consensus on the global wall clock time
use 0x1::error;use 0x1::system_addresses;
Constants
The blockchain is not in an operating state yet
const ENOT_OPERATING: u64 = 1;
An invalid timestamp was provided
const EINVALID_TIMESTAMP: u64 = 2;
Conversion factor between seconds and microseconds
const MICRO_CONVERSION_FACTOR: u64 = 1000000;
Resources
CurrentTimeMicroseconds
A singleton resource holding the current Unix time in microseconds
struct CurrentTimeMicroseconds has key
Fields
-
microseconds: u64
Functions
set_time_has_started
Marks that time has started. This can only be called from genesis and with the aptos framework account.
public(friend) fun set_time_has_started(aptos_framework: &signer)
Implementation
public(friend) fun set_time_has_started(aptos_framework: &signer) { system_addresses::assert_aptos_framework(aptos_framework); let timer = CurrentTimeMicroseconds { microseconds: 0 }; move_to(aptos_framework, timer);}
update_global_time
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)
Implementation
public fun update_global_time( account: &signer, proposer: address, timestamp: u64) acquires CurrentTimeMicroseconds { // Can only be invoked by AptosVM signer. system_addresses::assert_vm(account);
let global_timer = borrow_global_mut<CurrentTimeMicroseconds>(@aptos_framework); let now = global_timer.microseconds; if (proposer == @vm_reserved) { // NIL block with null address as proposer. Timestamp must be equal. assert!(now == timestamp, error::invalid_argument(EINVALID_TIMESTAMP)); } else { // Normal block. Time must advance assert!(now < timestamp, error::invalid_argument(EINVALID_TIMESTAMP)); global_timer.microseconds = timestamp; };}
now_microseconds
Gets the current time in microseconds.
#[view]public fun now_microseconds(): u64
Implementation
public fun now_microseconds(): u64 acquires CurrentTimeMicroseconds { borrow_global<CurrentTimeMicroseconds>(@aptos_framework).microseconds}
now_seconds
Gets the current time in seconds.
#[view]public fun now_seconds(): u64
Implementation
public fun now_seconds(): u64 acquires CurrentTimeMicroseconds { now_microseconds() / MICRO_CONVERSION_FACTOR}
Specification
High-level Requirements
No. | Requirement | Criticality | Implementation | Enforcement |
---|---|---|---|---|
1 | There should only exist one global wall clock and it should be created during genesis. | High | The function set_time_has_started is only called by genesis::initialize and ensures that no other resources of this type exist by only assigning it to a predefined account. | Formally verified via module. |
2 | The global wall clock resource should only be owned by the Aptos framework. | High | The function set_time_has_started ensures that only the aptos_framework account can possess the CurrentTimeMicroseconds resource using the assert_aptos_framework function. | Formally verified via module. |
3 | The clock time should only be updated by the VM account. | High | The update_global_time function asserts that the transaction signer is the vm_reserved account. | Formally verified via UpdateGlobalTimeAbortsIf. |
4 | The clock time should increase with every update as agreed through consensus and proposed by the current epoch's validator. | High | The update_global_time function asserts that the new timestamp is greater than the current timestamp. | Formally verified via UpdateGlobalTimeAbortsIf. |
Module-level Specification
// This enforces high-level requirement 1 and high-level requirement 2:invariant [suspendable] chain_status::is_operating() ==> exists<CurrentTimeMicroseconds>(@aptos_framework);
update_global_time
public fun update_global_time(account: &signer, proposer: address, timestamp: u64)
requires chain_status::is_operating();include UpdateGlobalTimeAbortsIf;ensures (proposer != @vm_reserved) ==> (spec_now_microseconds() == timestamp);
schema UpdateGlobalTimeAbortsIf { account: signer; 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);}
fun spec_now_microseconds(): u64 { global<CurrentTimeMicroseconds>(@aptos_framework).microseconds}
fun spec_now_seconds(): u64 { spec_now_microseconds() / MICRO_CONVERSION_FACTOR}