starcoin-framework

Module 0x1::Timestamp

The module implements onchain timestamp oracle. Timestamp is updated on each block. It always steps forward, and never come backward.

• Resource CurrentTimeMilliseconds
• Resource TimeHasStarted
• Constants
• Function initialize
• Function update_global_time
• Function now_seconds
• Function now_milliseconds
• Function set_time_has_started
• Function is_genesis
• Function assert_genesis
• Module Specification

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

Resource CurrentTimeMilliseconds

struct CurrentTimeMilliseconds has key

Fields

milliseconds: u64

Resource TimeHasStarted

A singleton resource used to determine whether time has started. This is called at the end of genesis.

struct TimeHasStarted has key

Fields

dummy_field: bool

Constants

const EINVALID_TIMESTAMP: u64 = 14;

const ENOT_GENESIS: u64 = 12;

const ENOT_INITIALIZED: u64 = 101;

Conversion factor between seconds and milliseconds

const MILLI_CONVERSION_FACTOR: u64 = 1000;

Function initialize

public fun initialize(account: &signer, genesis_timestamp: u64)

Implementation

public fun initialize(account: &signer, genesis_timestamp: u64) {
    // Only callable by the Genesis address
    CoreAddresses::assert_genesis_address(account);
    let milli_timer = CurrentTimeMilliseconds {milliseconds: genesis_timestamp};
    move_to<CurrentTimeMilliseconds>(account, milli_timer);
}

Specification

aborts_if Signer::address_of(account) != CoreAddresses::SPEC_GENESIS_ADDRESS();
aborts_if exists<CurrentTimeMilliseconds>(Signer::address_of(account));
ensures exists<CurrentTimeMilliseconds>(Signer::address_of(account));

Function update_global_time

public fun update_global_time(account: &signer, timestamp: u64)

Implementation

public fun update_global_time(account: &signer, timestamp: u64) acquires CurrentTimeMilliseconds {
    CoreAddresses::assert_genesis_address(account);
    //Do not update time before time start.
    let global_milli_timer = borrow_global_mut<CurrentTimeMilliseconds>(CoreAddresses::GENESIS_ADDRESS());
    assert!(timestamp > global_milli_timer.milliseconds, Errors::invalid_argument(EINVALID_TIMESTAMP));
    global_milli_timer.milliseconds = timestamp;
}

Specification

aborts_if Signer::address_of(account) != CoreAddresses::SPEC_GENESIS_ADDRESS();
aborts_if !exists<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS());
aborts_if timestamp <= global<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS()).milliseconds;
ensures global<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS()).milliseconds == timestamp;

Function now_seconds

public fun now_seconds(): u64

Implementation

public fun now_seconds(): u64 acquires CurrentTimeMilliseconds {
    now_milliseconds() / MILLI_CONVERSION_FACTOR
}

Specification

aborts_if !exists<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS());
ensures result == now_milliseconds() / MILLI_CONVERSION_FACTOR;

fun spec_now_seconds(): u64 {
   global<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS()).milliseconds / MILLI_CONVERSION_FACTOR
}

Function now_milliseconds

public fun now_milliseconds(): u64

Implementation

public fun now_milliseconds(): u64 acquires CurrentTimeMilliseconds {
    borrow_global<CurrentTimeMilliseconds>(CoreAddresses::GENESIS_ADDRESS()).milliseconds
}

Specification

aborts_if !exists<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS());
ensures result == global<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS()).milliseconds;

fun spec_now_millseconds(): u64 {
   global<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS()).milliseconds
}

Function set_time_has_started

Marks that time has started and genesis has finished. This can only be called from genesis.

public fun set_time_has_started(account: &signer)

Implementation

public fun set_time_has_started(account: &signer) {
    CoreAddresses::assert_genesis_address(account);

    // Current time must have been initialized.
    assert!(
        exists<CurrentTimeMilliseconds>(CoreAddresses::GENESIS_ADDRESS()),
        Errors::invalid_state(ENOT_INITIALIZED)
    );
    move_to(account, TimeHasStarted{});
}

Specification

aborts_if Signer::address_of(account) != CoreAddresses::SPEC_GENESIS_ADDRESS();
aborts_if !exists<CurrentTimeMilliseconds>(Signer::address_of(account));
aborts_if exists<TimeHasStarted>(Signer::address_of(account));
ensures exists<TimeHasStarted>(Signer::address_of(account));

Function is_genesis

Helper function to determine if the blockchain is in genesis state.

public fun is_genesis(): bool

Implementation

public fun is_genesis(): bool {
    !exists<TimeHasStarted>(CoreAddresses::GENESIS_ADDRESS())
}

Specification

aborts_if false;
ensures result == !exists<TimeHasStarted>(CoreAddresses::SPEC_GENESIS_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();
}

schema AbortsIfTimestampNotExists {
    aborts_if !exists<CurrentTimeMilliseconds>(CoreAddresses::SPEC_GENESIS_ADDRESS());
}

Module Specification

pragma verify;
pragma aborts_if_is_strict;

This site is open source. Improve this page.