timestamp - [devnet]

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
}