Skip to content

Latest commit

 

History

History
512 lines (271 loc) · 17.1 KB

DiemTimestamp.md

File metadata and controls

512 lines (271 loc) · 17.1 KB
Raw

Module 0x1::DiemTimestamp

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
  • VASP: to keep track of when credentials expire
  • DiemSystem, DiemAccount, DiemConfig: to check if the current state is in the genesis state
  • DiemBlock: to reach consensus on the global wall clock time
  • AccountLimits: to limit the time of account limits

This module moreover enables code to assert that it is running in genesis (Self::assert_genesis) or after genesis (Self::assert_operating). These are essentially distinct states of the system. Specifically, if Self::assert_operating succeeds, assumptions about invariants over the global state can be made which reflect that the system has been successfully initialized.

use 0x1::CoreAddresses;
use 0x1::Errors;

Resource CurrentTimeMicroseconds

A singleton resource holding the current Unix time in microseconds

resource struct CurrentTimeMicroseconds
Fields
microseconds: u64

Constants

The blockchain is not in the genesis state anymore

const ENOT_GENESIS: u64 = 0;

The blockchain is not in an operating state yet

const ENOT_OPERATING: u64 = 1;

An invalid timestamp was provided

const ETIMESTAMP: u64 = 2;

Conversion factor between seconds and microseconds

const MICRO_CONVERSION_FACTOR: u64 = 1000000;

Function set_time_has_started

Marks that time has started and genesis has finished. This can only be called from genesis and with the root account.

public fun set_time_has_started(dr_account: &signer)
Implementation 
public fun set_time_has_started(dr_account: &signer) {
    assert_genesis();
    CoreAddresses::assert_diem_root(dr_account);
    let timer = CurrentTimeMicroseconds { microseconds: 0 };
    move_to(dr_account, timer);
}
Specification

Verification of this function is turned off because it cannot be verified without genesis execution context. After time has started, all invariants guarded by DiemTimestamp::is_operating will become activated and need to hold.

pragma verify = false;
include AbortsIfNotGenesis;
include CoreAddresses::AbortsIfNotDiemRoot{account: dr_account};
ensures is_operating();

Function 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 {
    assert_operating();
    // Can only be invoked by DiemVM signer.
    CoreAddresses::assert_vm(account);

    let global_timer = borrow_global_mut<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS());
    let now = global_timer.microseconds;
    if (proposer == CoreAddresses::VM_RESERVED_ADDRESS()) {
        // NIL block with null address as proposer. Timestamp must be equal.
        assert(now == timestamp, Errors::invalid_argument(ETIMESTAMP));
    } else {
        // Normal block. Time must advance
        assert(now < timestamp, Errors::invalid_argument(ETIMESTAMP));
    };
    global_timer.microseconds = timestamp;
}
Specification 
include AbortsIfNotOperating;
include CoreAddresses::AbortsIfNotVM;

let now = spec_now_microseconds();
aborts_if [assume]
    (if (proposer == CoreAddresses::VM_RESERVED_ADDRESS()) {
        now != timestamp
     } else  {
        now >= timestamp
     }
    )
    with Errors::INVALID_ARGUMENT;
ensures spec_now_microseconds() == timestamp;

Function now_microseconds

Gets the current time in microseconds.

public fun now_microseconds(): u64
Implementation 
public fun now_microseconds(): u64 acquires CurrentTimeMicroseconds {
    assert_operating();
    borrow_global<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS()).microseconds
}
Specification 
pragma opaque;
include AbortsIfNotOperating;
ensures result == spec_now_microseconds();


define spec_now_microseconds(): u64 {
   global<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS()).microseconds
}

Function now_seconds

Gets the current time in seconds.

public fun now_seconds(): u64
Implementation 
public fun now_seconds(): u64 acquires CurrentTimeMicroseconds {
    now_microseconds() / MICRO_CONVERSION_FACTOR
}
Specification 
pragma opaque;
include AbortsIfNotOperating;
ensures result == spec_now_microseconds() /  MICRO_CONVERSION_FACTOR;


define spec_now_seconds(): u64 {
   global<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS()).microseconds / MICRO_CONVERSION_FACTOR
}

Function is_genesis

Helper function to determine if Diem is in genesis state.

public fun is_genesis(): bool
Implementation 
public fun is_genesis(): bool {
    !exists<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS())
}

Function assert_genesis

Helper function to assert genesis state.

public fun assert_genesis()
Implementation 
public fun assert_genesis() {
    assert(is_genesis(), Errors::invalid_state(ENOT_GENESIS));
}
Specification 
pragma opaque = true;
include AbortsIfNotGenesis;

Helper schema to specify that a function aborts if not in genesis.

schema AbortsIfNotGenesis {
    aborts_if !is_genesis() with Errors::INVALID_STATE;
}

Function is_operating

Helper function to determine if Diem is operating. This is the same as !is_genesis() and is provided for convenience. Testing is_operating() is more frequent than is_genesis().

public fun is_operating(): bool
Implementation 
public fun is_operating(): bool {
    exists<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS())
}

Function assert_operating

Helper function to assert operating (!genesis) state.

public fun assert_operating()
Implementation 
public fun assert_operating() {
    assert(is_operating(), Errors::invalid_state(ENOT_OPERATING));
}
Specification 
pragma opaque = true;
include AbortsIfNotOperating;

Helper schema to specify that a function aborts if not operating.

schema AbortsIfNotOperating {
    aborts_if !is_operating() with Errors::INVALID_STATE;
}

Module Specification

After genesis, CurrentTimeMicroseconds is published forever

invariant [global] is_operating() ==> exists<CurrentTimeMicroseconds>(CoreAddresses::DIEM_ROOT_ADDRESS());

After genesis, time progresses monotonically.

invariant update [global]
    old(is_operating()) ==> old(spec_now_microseconds()) <= spec_now_microseconds();

All functions which do not have an aborts_if specification in this module are implicitly declared to never abort.

pragma aborts_if_is_strict;