randomness - [mainnet]

This module provides access to instant secure randomness generated by the Aptos validators, as documented in AIP-41.

Secure randomness means (1) the randomness cannot be predicted ahead of time by validators, developers or users and (2) the randomness cannot be biased in any way by validators, developers or users.

Security holds under the same proof-of-stake assumption that secures the Aptos network.

use 0x1::event;
use 0x1::hash;
use 0x1::option;
use 0x1::system_addresses;
use 0x1::transaction_context;
use 0x1::vector;

Constants

const MAX_U256: u256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935;

const DST: vector<u8> = [65, 80, 84, 79, 83, 95, 82, 65, 78, 68, 79, 77, 78, 69, 83, 83];

Randomness APIs calls must originate from a private entry function with #[randomness] annotation. Otherwise, malicious users can bias randomness result.

const E_API_USE_IS_BIASIBLE: u64 = 1;

Structs

`RandomnessGeneratedEvent`

Event emitted every time a public randomness API in this module is called.

#[event]
struct RandomnessGeneratedEvent has drop, store

Fields

dummy_field: bool

Resources

`PerBlockRandomness`

32-byte randomness seed unique to every block. This resource is updated in every block prologue.

struct PerBlockRandomness has drop, key

Fields

epoch: u64
round: u64
seed: option::Option<vector<u8>>

`Ghost$var`

struct Ghost$var has copy, drop, store, key

Fields

v: vector<u8>

Functions

`initialize`

Called in genesis.move. Must be called in tests to initialize the PerBlockRandomness resource.

public fun initialize(framework: &signer)

Implementation

public fun initialize(framework: &signer) {
    system_addresses::assert_aptos_framework(framework);
    if (!exists<PerBlockRandomness>(@aptos_framework)) {
        move_to(framework, PerBlockRandomness {
            epoch: 0,
            round: 0,
            seed: option::none(),
        });
    }
}

`on_new_block`

Invoked in block prologues to update the block-level randomness seed.

public(friend) fun on_new_block(vm: &signer, epoch: u64, round: u64, seed_for_new_block: option::Option<vector<u8>>)

Implementation

public(friend) fun on_new_block(vm: &signer, epoch: u64, round: u64, seed_for_new_block: Option<vector<u8>>) acquires PerBlockRandomness {
    system_addresses::assert_vm(vm);
    if (exists<PerBlockRandomness>(@aptos_framework)) {
        let randomness = borrow_global_mut<PerBlockRandomness>(@aptos_framework);
        randomness.epoch = epoch;
        randomness.round = round;
        randomness.seed = seed_for_new_block;
    }
}

`next_32_bytes`

Generate the next 32 random bytes. Repeated calls will yield different results (assuming the collision-resistance of the hash function).

fun next_32_bytes(): vector<u8>

Implementation

fun next_32_bytes(): vector<u8> acquires PerBlockRandomness {
    assert!(is_unbiasable(), E_API_USE_IS_BIASIBLE);

    let input = DST;
    let randomness = borrow_global<PerBlockRandomness>(@aptos_framework);
    let seed = *option::borrow(&randomness.seed);

    vector::append(&mut input, seed);
    vector::append(&mut input, transaction_context::get_transaction_hash());
    vector::append(&mut input, fetch_and_increment_txn_counter());
    hash::sha3_256(input)
}

`bytes`

Generates a sequence of bytes uniformly at random

public fun bytes(n: u64): vector<u8>

Implementation

public fun bytes(n: u64): vector<u8> acquires PerBlockRandomness {
    let v = vector[];
    let c = 0;
    while (c < n) {
        let blob = next_32_bytes();
        vector::reverse_append(&mut v, blob);

        c = c + 32;
    };

    if (c > n) {
        vector::trim(&mut v, n);
    };

    event::emit(RandomnessGeneratedEvent {});

    v
}

`u8_integer`

Generates an u8 uniformly at random.

public fun u8_integer(): u8

Implementation

public fun u8_integer(): u8 acquires PerBlockRandomness {
    let raw = next_32_bytes();
    let ret: u8 = vector::pop_back(&mut raw);

    event::emit(RandomnessGeneratedEvent {});

    ret
}

`u16_integer`

Generates an u16 uniformly at random.

public fun u16_integer(): u16

Implementation

public fun u16_integer(): u16 acquires PerBlockRandomness {
    let raw = next_32_bytes();
    let i = 0;
    let ret: u16 = 0;
    while (i < 2) {
        ret = ret * 256 + (vector::pop_back(&mut raw) as u16);
        i = i + 1;
    };

    event::emit(RandomnessGeneratedEvent {});

    ret
}

`u32_integer`

Generates an u32 uniformly at random.

public fun u32_integer(): u32

Implementation

public fun u32_integer(): u32 acquires PerBlockRandomness {
    let raw = next_32_bytes();
    let i = 0;
    let ret: u32 = 0;
    while (i < 4) {
        ret = ret * 256 + (vector::pop_back(&mut raw) as u32);
        i = i + 1;
    };

    event::emit(RandomnessGeneratedEvent {});

    ret
}

`u64_integer`

Generates an u64 uniformly at random.

public fun u64_integer(): u64

Implementation

public fun u64_integer(): u64 acquires PerBlockRandomness {
    let raw = next_32_bytes();
    let i = 0;
    let ret: u64 = 0;
    while (i < 8) {
        ret = ret * 256 + (vector::pop_back(&mut raw) as u64);
        i = i + 1;
    };

    event::emit(RandomnessGeneratedEvent {});

    ret
}

`u128_integer`

Generates an u128 uniformly at random.

public fun u128_integer(): u128

Implementation

public fun u128_integer(): u128 acquires PerBlockRandomness {
    let raw = next_32_bytes();
    let i = 0;
    let ret: u128 = 0;
    while (i < 16) {
        ret = ret * 256 + (vector::pop_back(&mut raw) as u128);
        i = i + 1;
    };

    event::emit(RandomnessGeneratedEvent {});

    ret
}

`u256_integer`

Generates a u256 uniformly at random.

public fun u256_integer(): u256

Implementation

public fun u256_integer(): u256 acquires PerBlockRandomness {
    event::emit(RandomnessGeneratedEvent {});
    u256_integer_internal()
}

`u256_integer_internal`

Generates a u256 uniformly at random.

fun u256_integer_internal(): u256

Implementation

fun u256_integer_internal(): u256 acquires PerBlockRandomness {
    let raw = next_32_bytes();
    let i = 0;
    let ret: u256 = 0;
    while (i < 32) {
        ret = ret * 256 + (vector::pop_back(&mut raw) as u256);
        i = i + 1;
    };
    ret
}

`u8_range`

Generates a number $n \in [min_incl, max_excl)$ uniformly at random.

NOTE: The uniformity is not perfect, but it can be proved that the bias is negligible. If you need perfect uniformity, consider implement your own via rejection sampling.

public fun u8_range(min_incl: u8, max_excl: u8): u8

Implementation

public fun u8_range(min_incl: u8, max_excl: u8): u8 acquires PerBlockRandomness {
    let range = ((max_excl - min_incl) as u256);
    let sample = ((u256_integer_internal() % range) as u8);

    event::emit(RandomnessGeneratedEvent {});

    min_incl + sample
}

`u16_range`

Generates a number $n \in [min_incl, max_excl)$ uniformly at random.

NOTE: The uniformity is not perfect, but it can be proved that the bias is negligible. If you need perfect uniformity, consider implement your own via rejection sampling.

public fun u16_range(min_incl: u16, max_excl: u16): u16

Implementation

public fun u16_range(min_incl: u16, max_excl: u16): u16 acquires PerBlockRandomness {
    let range = ((max_excl - min_incl) as u256);
    let sample = ((u256_integer_internal() % range) as u16);

    event::emit(RandomnessGeneratedEvent {});

    min_incl + sample
}

`u32_range`

Generates a number $n \in [min_incl, max_excl)$ uniformly at random.

NOTE: The uniformity is not perfect, but it can be proved that the bias is negligible. If you need perfect uniformity, consider implement your own via rejection sampling.

public fun u32_range(min_incl: u32, max_excl: u32): u32

Implementation

public fun u32_range(min_incl: u32, max_excl: u32): u32 acquires PerBlockRandomness {
    let range = ((max_excl - min_incl) as u256);
    let sample = ((u256_integer_internal() % range) as u32);

    event::emit(RandomnessGeneratedEvent {});

    min_incl + sample
}

`u64_range`

Generates a number $n \in [min_incl, max_excl)$ uniformly at random.

NOTE: The uniformity is not perfect, but it can be proved that the bias is negligible. If you need perfect uniformity, consider implement your own via rejection sampling.

public fun u64_range(min_incl: u64, max_excl: u64): u64

Implementation

public fun u64_range(min_incl: u64, max_excl: u64): u64 acquires PerBlockRandomness {
    event::emit(RandomnessGeneratedEvent {});

    u64_range_internal(min_incl, max_excl)
}

`u64_range_internal`

public fun u64_range_internal(min_incl: u64, max_excl: u64): u64

Implementation

public fun u64_range_internal(min_incl: u64, max_excl: u64): u64 acquires PerBlockRandomness {
    let range = ((max_excl - min_incl) as u256);
    let sample = ((u256_integer_internal() % range) as u64);

    min_incl + sample
}

`u128_range`

Generates a number $n \in [min_incl, max_excl)$ uniformly at random.

NOTE: The uniformity is not perfect, but it can be proved that the bias is negligible. If you need perfect uniformity, consider implement your own via rejection sampling.

public fun u128_range(min_incl: u128, max_excl: u128): u128

Implementation

public fun u128_range(min_incl: u128, max_excl: u128): u128 acquires PerBlockRandomness {
    let range = ((max_excl - min_incl) as u256);
    let sample = ((u256_integer_internal() % range) as u128);

    event::emit(RandomnessGeneratedEvent {});

    min_incl + sample
}

`u256_range`

Generates a number $n \in [min_incl, max_excl)$ uniformly at random.

NOTE: The uniformity is not perfect, but it can be proved that the bias is negligible. If you need perfect uniformity, consider implement your own with u256_integer() + rejection sampling.

public fun u256_range(min_incl: u256, max_excl: u256): u256

Implementation

public fun u256_range(min_incl: u256, max_excl: u256): u256 acquires PerBlockRandomness {
    let range = max_excl - min_incl;
    let r0 = u256_integer_internal();
    let r1 = u256_integer_internal();

    // Will compute sample := (r0 + r1*2^256) % range.

    let sample = r1 % range;
    let i = 0;
    while ({
        spec {
            invariant sample >= 0 && sample < max_excl - min_incl;
        };
        i < 256
    }) {
        sample = safe_add_mod(sample, sample, range);
        i = i + 1;
    };

    let sample = safe_add_mod(sample, r0 % range, range);
    spec {
        assert sample >= 0 && sample < max_excl - min_incl;
    };

    event::emit(RandomnessGeneratedEvent {});

    min_incl + sample
}

`permutation`

Generate a permutation of [0, 1, …, n-1] uniformly at random. If n is 0, returns the empty vector.

public fun permutation(n: u64): vector<u64>

Implementation

public fun permutation(n: u64): vector<u64> acquires PerBlockRandomness {
    event::emit(RandomnessGeneratedEvent {});

    let values = vector[];

    if(n == 0) {
        return vector[]
    };

    // Initialize into [0, 1, ..., n-1].
    let i = 0;
    while ({
        spec {
            invariant i <= n;
            invariant len(values) == i;
        };
        i < n
    }) {
        std::vector::push_back(&mut values, i);
        i = i + 1;
    };
    spec {
        assert len(values) == n;
    };

    // Shuffle.
    let tail = n - 1;
    while ({
        spec {
            invariant tail >= 0 && tail < len(values);
        };
        tail > 0
    }) {
        let pop_position = u64_range_internal(0, tail + 1);
        spec {
            assert pop_position < len(values);
        };
        std::vector::swap(&mut values, pop_position, tail);
        tail = tail - 1;
    };

    values
}

`safe_add_mod`

Compute (a + b) % m, assuming m >= 1, 0 <= a < m, 0<= b < m.

fun safe_add_mod(a: u256, b: u256, m: u256): u256

Implementation

fun safe_add_mod(a: u256, b: u256, m: u256): u256 {
    let a_clone = a;
    let neg_b = m - b;
    let a_less = a < neg_b;
    take_first(if (a_less) { a + b } else { a_clone - neg_b }, if (!a_less) { a_clone - neg_b } else { a + b })
}

`take_first`

fun take_first(x: u256, _y: u256): u256

Implementation

fun take_first(x: u256, _y: u256 ): u256 { x }

`fetch_and_increment_txn_counter`

Fetches and increments a transaction-specific 32-byte randomness-related counter. Aborts with E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT if randomness is not unbiasable.

fun fetch_and_increment_txn_counter(): vector<u8>

Implementation

native fun fetch_and_increment_txn_counter(): vector<u8>;

`is_unbiasable`

Called in each randomness generation function to ensure certain safety invariants, namely:

The transaction that led to the call of this function had a private (or friend) entry function as its payload.
The entry function had #[randomness] annotation.

fun is_unbiasable(): bool

Implementation

native fun is_unbiasable(): bool;

Specification

pragma verify = true;
invariant [suspendable] chain_status::is_operating() ==> exists<PerBlockRandomness>(@aptos_framework);

global var: vector<u8>;

`initialize`

public fun initialize(framework: &signer)

let framework_addr = signer::address_of(framework);
aborts_if framework_addr != @aptos_framework;

`on_new_block`

public(friend) fun on_new_block(vm: &signer, epoch: u64, round: u64, seed_for_new_block: option::Option<vector<u8>>)

aborts_if signer::address_of(vm) != @vm;
ensures exists<PerBlockRandomness>(@aptos_framework) ==> global<PerBlockRandomness>(@aptos_framework).seed == seed_for_new_block;
ensures exists<PerBlockRandomness>(@aptos_framework) ==> global<PerBlockRandomness>(@aptos_framework).epoch == epoch;
ensures exists<PerBlockRandomness>(@aptos_framework) ==> global<PerBlockRandomness>(@aptos_framework).round == round;

`next_32_bytes`

fun next_32_bytes(): vector<u8>

include NextBlobAbortsIf;
let input = b"APTOS_RANDOMNESS";
let randomness = global<PerBlockRandomness>(@aptos_framework);
let seed = option::spec_borrow(randomness.seed);
let txn_hash = transaction_context::spec_get_txn_hash();
let txn_counter = spec_fetch_and_increment_txn_counter();
ensures len(result) == 32;
ensures result == hash::sha3_256(concat(concat(concat(input, seed), txn_hash), txn_counter));

schema NextBlobAbortsIf {
    let randomness = global<PerBlockRandomness>(@aptos_framework);
    aborts_if option::spec_is_none(randomness.seed);
    aborts_if !spec_is_unbiasable();
    aborts_if !exists<PerBlockRandomness>(@aptos_framework);
}

`u8_integer`

public fun u8_integer(): u8

include NextBlobAbortsIf;

`u16_integer`

public fun u16_integer(): u16

pragma unroll = 2;
include NextBlobAbortsIf;

`u32_integer`

public fun u32_integer(): u32

pragma unroll = 4;
include NextBlobAbortsIf;

`u64_integer`

public fun u64_integer(): u64

pragma unroll = 8;
include NextBlobAbortsIf;

`u128_integer`

public fun u128_integer(): u128

pragma unroll = 16;
include NextBlobAbortsIf;

`u256_integer`

public fun u256_integer(): u256

pragma verify_duration_estimate = 300;
pragma unroll = 32;
include NextBlobAbortsIf;
ensures [abstract] result == spec_u256_integer();

`u256_integer_internal`

fun u256_integer_internal(): u256

pragma verify_duration_estimate = 300;
pragma unroll = 32;
include NextBlobAbortsIf;

fun spec_u256_integer(): u256;

`u8_range`

public fun u8_range(min_incl: u8, max_excl: u8): u8

pragma verify_duration_estimate = 120;
pragma opaque;
include NextBlobAbortsIf;
aborts_if min_incl >= max_excl;
ensures result >= min_incl && result < max_excl;

`u64_range`

public fun u64_range(min_incl: u64, max_excl: u64): u64

pragma verify_duration_estimate = 120;
include NextBlobAbortsIf;
aborts_if min_incl >= max_excl;
ensures result >= min_incl && result < max_excl;

`u256_range`

public fun u256_range(min_incl: u256, max_excl: u256): u256

pragma verify_duration_estimate = 120;
include NextBlobAbortsIf;
aborts_if min_incl >= max_excl;
ensures result >= min_incl && result < max_excl;

`permutation`

public fun permutation(n: u64): vector<u64>

pragma aborts_if_is_partial;

fun spec_safe_add_mod(a: u256, b: u256, m: u256): u256 {
   if (a < m - b) {
       a + b
   } else {
       a - (m - b)
   }
}

`fetch_and_increment_txn_counter`

fun fetch_and_increment_txn_counter(): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures [abstract] result == spec_fetch_and_increment_txn_counter();

fun spec_fetch_and_increment_txn_counter(): vector<u8>;

`is_unbiasable`

fun is_unbiasable(): bool

pragma opaque;
aborts_if [abstract] false;
ensures [abstract] result == spec_is_unbiasable();

fun spec_is_unbiasable(): bool;