diff --git a/aptos-move/framework/aptos-framework/doc/randomness.md b/aptos-move/framework/aptos-framework/doc/randomness.md index da444511bfb86..36969528f8bfc 100644 --- a/aptos-move/framework/aptos-framework/doc/randomness.md +++ b/aptos-move/framework/aptos-framework/doc/randomness.md @@ -3,25 +3,35 @@ # Module `0x1::randomness` -On-chain randomness utils. +This module provides access to *instant* secure randomness generated by the Aptos validators, as documented in +[AIP-41](https://github.com/aptos-foundation/AIPs/blob/main/aips/aip-41.md). + +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. - [Resource `PerBlockRandomness`](#0x1_randomness_PerBlockRandomness) +- [Struct `RandomnessGeneratedEvent`](#0x1_randomness_RandomnessGeneratedEvent) - [Resource `Ghost$var`](#0x1_randomness_Ghost$var) - [Constants](#@Constants_0) - [Function `initialize`](#0x1_randomness_initialize) - [Function `on_new_block`](#0x1_randomness_on_new_block) -- [Function `next_blob`](#0x1_randomness_next_blob) +- [Function `next_32_bytes`](#0x1_randomness_next_32_bytes) +- [Function `bytes`](#0x1_randomness_bytes) - [Function `u8_integer`](#0x1_randomness_u8_integer) - [Function `u16_integer`](#0x1_randomness_u16_integer) - [Function `u32_integer`](#0x1_randomness_u32_integer) - [Function `u64_integer`](#0x1_randomness_u64_integer) - [Function `u128_integer`](#0x1_randomness_u128_integer) - [Function `u256_integer`](#0x1_randomness_u256_integer) +- [Function `u256_integer_internal`](#0x1_randomness_u256_integer_internal) - [Function `u8_range`](#0x1_randomness_u8_range) - [Function `u16_range`](#0x1_randomness_u16_range) - [Function `u32_range`](#0x1_randomness_u32_range) - [Function `u64_range`](#0x1_randomness_u64_range) +- [Function `u64_range_internal`](#0x1_randomness_u64_range_internal) - [Function `u128_range`](#0x1_randomness_u128_range) - [Function `u256_range`](#0x1_randomness_u256_range) - [Function `permutation`](#0x1_randomness_permutation) @@ -32,7 +42,7 @@ On-chain randomness utils. - [Specification](#@Specification_1) - [Function `initialize`](#@Specification_1_initialize) - [Function `on_new_block`](#@Specification_1_on_new_block) - - [Function `next_blob`](#@Specification_1_next_blob) + - [Function `next_32_bytes`](#@Specification_1_next_32_bytes) - [Function `u8_integer`](#@Specification_1_u8_integer) - [Function `u16_integer`](#@Specification_1_u16_integer) - [Function `u32_integer`](#@Specification_1_u32_integer) @@ -48,7 +58,8 @@ On-chain randomness utils. - [Function `is_safe_call`](#@Specification_1_is_safe_call) -
use 0x1::hash;
+use 0x1::event;
+use 0x1::hash;
use 0x1::option;
use 0x1::system_addresses;
use 0x1::transaction_context;
@@ -96,6 +107,35 @@ This resource is updated in every block prologue.
+
+
+
+
+## Struct `RandomnessGeneratedEvent`
+
+Event emitted every time a public randomness API in this module is called.
+
+
+#[event]
+struct RandomnessGeneratedEvent has drop, store
+
+
+
+
+
+Fields
+
+
+
+-
+
dummy_field: bool
+
+-
+
+
+
+
+
@@ -130,6 +170,15 @@ This resource is updated in every block prologue.
## Constants
+
+
+
+
+const MAX_U256: u256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
+
+
+
+
@@ -211,14 +260,15 @@ Invoked in block prologues to update the block-level randomness seed.
-
+
-## Function `next_blob`
+## Function `next_32_bytes`
-Generate 32 random bytes.
+Generate the next 32 random bytes. Repeated calls will yield different results (assuming the collision-resistance
+of the hash function).
-public fun next_blob(): vector<u8>
+fun next_32_bytes(): vector<u8>
@@ -227,12 +277,13 @@ Generate 32 random bytes.
Implementation
-public fun next_blob(): vector<u8> acquires PerBlockRandomness {
+fun next_32_bytes(): vector<u8> acquires PerBlockRandomness {
assert!(is_safe_call(), E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT);
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());
@@ -242,6 +293,46 @@ Generate 32 random bytes.
+
+
+
+
+## Function `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::append(&mut v, blob);
+
+ c = c + 32;
+ };
+
+ if (c > n) {
+ vector::trim(&mut v, n);
+ };
+
+ event::emit(RandomnessGeneratedEvent {});
+
+ v
+}
+
+
+
+
@@ -261,8 +352,11 @@ Generates an u8 uniformly at random.
public fun u8_integer(): u8 acquires PerBlockRandomness {
- let raw = next_blob();
+ let raw = next_32_bytes();
let ret: u8 = vector::pop_back(&mut raw);
+
+ event::emit(RandomnessGeneratedEvent {});
+
ret
}
@@ -288,13 +382,16 @@ Generates an u16 uniformly at random.
public fun u16_integer(): u16 acquires PerBlockRandomness {
- let raw = next_blob();
+ 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
}
@@ -320,13 +417,16 @@ Generates an u32 uniformly at random.
public fun u32_integer(): u32 acquires PerBlockRandomness {
- let raw = next_blob();
+ 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
}
@@ -352,13 +452,16 @@ Generates an u64 uniformly at random.
public fun u64_integer(): u64 acquires PerBlockRandomness {
- let raw = next_blob();
+ 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
}
@@ -384,13 +487,21 @@ Generates an u128 uniformly at random.
public fun u128_integer(): u128 acquires PerBlockRandomness {
- let raw = next_blob();
+ let raw = next_32_bytes();
let i = 0;
let ret: u128 = 0;
while (i < 16) {
+ spec {
+ // TODO: Prove these with proper loop invaraints.
+ assume ret * 256 + 255 <= MAX_U256;
+ assume len(raw) > 0;
+ };
ret = ret * 256 + (vector::pop_back(&mut raw) as u128);
i = i + 1;
};
+
+ event::emit(RandomnessGeneratedEvent {});
+
ret
}
@@ -416,10 +527,41 @@ Generates a u256 uniformly at random.
public fun u256_integer(): u256 acquires PerBlockRandomness {
- let raw = next_blob();
+ event::emit(RandomnessGeneratedEvent {});
+ u256_integer_internal()
+}
+
+
+
+
+
+
+
+
+## Function `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) {
+ spec {
+ // TODO: Prove these with proper loop invaraints.
+ assume ret * 256 + 255 <= MAX_U256;
+ assume len(raw) > 0;
+ };
ret = ret * 256 + (vector::pop_back(&mut raw) as u256);
i = i + 1;
};
@@ -452,7 +594,10 @@ If you need perfect uniformity, consider implement your own via rejection sampli
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() % range) as u8);
+ let sample = ((u256_integer_internal() % range) as u8);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -482,7 +627,10 @@ If you need perfect uniformity, consider implement your own via rejection sampli
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() % range) as u16);
+ let sample = ((u256_integer_internal() % range) as u16);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -512,7 +660,10 @@ If you need perfect uniformity, consider implement your own via rejection sampli
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() % range) as u32);
+ let sample = ((u256_integer_internal() % range) as u32);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -541,8 +692,35 @@ If you need perfect uniformity, consider implement your own via rejection sampli
public fun u64_range(min_incl: u64, max_excl: u64): u64 acquires PerBlockRandomness {
+ event::emit(RandomnessGeneratedEvent {});
+
+ u64_range_internal(min_incl, max_excl)
+}
+
+
+
+
+
+
+
+
+## Function `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() % range) as u64);
+ let sample = ((u256_integer_internal() % range) as u64);
+
min_incl + sample
}
@@ -572,7 +750,10 @@ If you need perfect uniformity, consider implement your own via rejection sampli
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() % range) as u128);
+ let sample = ((u256_integer_internal() % range) as u128);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -602,8 +783,8 @@ If you need perfect uniformity, consider implement your own with u256_range(min_incl: u256, max_excl: u256): u256 acquires PerBlockRandomness {
let range = max_excl - min_incl;
- let r0 = u256_integer();
- let r1 = u256_integer();
+ let r0 = u256_integer_internal();
+ let r1 = u256_integer_internal();
// Will compute sample := (r0 + r1*2^256) % range.
@@ -624,6 +805,8 @@ If you need perfect uniformity, consider implement your own with event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -637,6 +820,7 @@ If you need perfect uniformity, consider implement your own with permutation(n: u64): vector<u64>
@@ -651,6 +835,10 @@ Generate a permutation of [0, 1, ..., n-1]
uniformly at random.
public fun permutation(n: u64): vector<u64> acquires PerBlockRandomness {
let values = vector[];
+ if(n == 0) {
+ return vector[]
+ };
+
// Initialize into [0, 1, ..., n-1].
let i = 0;
while ({
@@ -675,7 +863,7 @@ Generate a permutation of [0, 1, ..., n-1]
uniformly at random.
};
tail > 0
}) {
- let pop_position = u64_range(0, tail + 1);
+ let pop_position = u64_range_internal(0, tail + 1);
spec {
assert pop_position < len(values);
};
@@ -683,6 +871,8 @@ Generate a permutation of [0, 1, ..., n-1]
uniformly at random.
tail = tail - 1;
};
+ event::emit(RandomnessGeneratedEvent {});
+
values
}
@@ -851,12 +1041,12 @@ Called in each randomness generation function to ensure certain safety invariant
-
+
-### Function `next_blob`
+### Function `next_32_bytes`
-public fun next_blob(): vector<u8>
+fun next_32_bytes(): vector<u8>
@@ -1068,7 +1258,6 @@ Called in each randomness generation function to ensure certain safety invariant
pragma aborts_if_is_partial;
-aborts_if n == 0;
@@ -1086,7 +1275,7 @@ Called in each randomness generation function to ensure certain safety invariant
aborts_if m < b;
-aborts_if a < m - b && a + b > MAX_U256;
+aborts_if a < m - b && a + b > MAX_U256;
ensures result == spec_safe_add_mod(a, b, m);
diff --git a/aptos-move/framework/aptos-framework/sources/randomness.move b/aptos-move/framework/aptos-framework/sources/randomness.move
index 2bcf385a3f57f..4679146cd2713 100644
--- a/aptos-move/framework/aptos-framework/sources/randomness.move
+++ b/aptos-move/framework/aptos-framework/sources/randomness.move
@@ -1,13 +1,22 @@
-/// On-chain randomness utils.
+/// This module provides access to *instant* secure randomness generated by the Aptos validators, as documented in
+/// [AIP-41](https://github.com/aptos-foundation/AIPs/blob/main/aips/aip-41.md).
+///
+/// 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.
module aptos_framework::randomness {
use std::hash;
use std::option;
use std::option::Option;
use std::vector;
+ use aptos_framework::event;
use aptos_framework::system_addresses;
use aptos_framework::transaction_context;
#[test_only]
use aptos_std::debug;
+ #[test_only]
+ use aptos_std::table_with_length;
friend aptos_framework::block;
@@ -16,6 +25,8 @@ module aptos_framework::randomness {
/// Randomness APIs calls must originate from a private entry function. Otherwise, test-and-abort attacks are possible.
const E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT: u64 = 1;
+ const MAX_U256: u256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
+
/// 32-byte randomness seed unique to every block.
/// This resource is updated in every block prologue.
struct PerBlockRandomness has drop, key {
@@ -24,6 +35,11 @@ module aptos_framework::randomness {
seed: Option>,
}
+ #[event]
+ /// Event emitted every time a public randomness API in this module is called.
+ struct RandomnessGeneratedEvent has store, drop {
+ }
+
/// Called in genesis.move.
/// Must be called in tests to initialize the `PerBlockRandomness` resource.
public fun initialize(framework: &signer) {
@@ -52,80 +68,133 @@ module aptos_framework::randomness {
}
}
- /// Generate 32 random bytes.
- public fun next_blob(): vector acquires PerBlockRandomness {
+ /// 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 acquires PerBlockRandomness {
assert!(is_safe_call(), E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT);
let input = DST;
let randomness = borrow_global(@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)
}
+ /// Generates a sequence of bytes uniformly at random
+ public fun bytes(n: u64): vector acquires PerBlockRandomness {
+ let v = vector[];
+ let c = 0;
+ while (c < n) {
+ let blob = next_32_bytes();
+ vector::append(&mut v, blob);
+
+ c = c + 32;
+ };
+
+ if (c > n) {
+ vector::trim(&mut v, n);
+ };
+
+ event::emit(RandomnessGeneratedEvent {});
+
+ v
+ }
+
/// Generates an u8 uniformly at random.
public fun u8_integer(): u8 acquires PerBlockRandomness {
- let raw = next_blob();
+ let raw = next_32_bytes();
let ret: u8 = vector::pop_back(&mut raw);
+
+ event::emit(RandomnessGeneratedEvent {});
+
ret
}
/// Generates an u16 uniformly at random.
public fun u16_integer(): u16 acquires PerBlockRandomness {
- let raw = next_blob();
+ 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
}
/// Generates an u32 uniformly at random.
public fun u32_integer(): u32 acquires PerBlockRandomness {
- let raw = next_blob();
+ 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
}
/// Generates an u64 uniformly at random.
public fun u64_integer(): u64 acquires PerBlockRandomness {
- let raw = next_blob();
+ 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
}
/// Generates an u128 uniformly at random.
public fun u128_integer(): u128 acquires PerBlockRandomness {
- let raw = next_blob();
+ let raw = next_32_bytes();
let i = 0;
let ret: u128 = 0;
while (i < 16) {
+ spec {
+ // TODO: Prove these with proper loop invaraints.
+ assume ret * 256 + 255 <= MAX_U256;
+ assume len(raw) > 0;
+ };
ret = ret * 256 + (vector::pop_back(&mut raw) as u128);
i = i + 1;
};
+
+ event::emit(RandomnessGeneratedEvent {});
+
ret
}
/// Generates a u256 uniformly at random.
public fun u256_integer(): u256 acquires PerBlockRandomness {
- let raw = next_blob();
+ event::emit(RandomnessGeneratedEvent {});
+ u256_integer_internal()
+ }
+
+ /// Generates a u256 uniformly at random.
+ fun u256_integer_internal(): u256 acquires PerBlockRandomness {
+ let raw = next_32_bytes();
let i = 0;
let ret: u256 = 0;
while (i < 32) {
+ spec {
+ // TODO: Prove these with proper loop invaraints.
+ assume ret * 256 + 255 <= MAX_U256;
+ assume len(raw) > 0;
+ };
ret = ret * 256 + (vector::pop_back(&mut raw) as u256);
i = i + 1;
};
@@ -138,7 +207,10 @@ module aptos_framework::randomness {
/// If you need perfect uniformity, consider implement your own via rejection sampling.
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() % range) as u8);
+ let sample = ((u256_integer_internal() % range) as u8);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -148,7 +220,10 @@ module aptos_framework::randomness {
/// If you need perfect uniformity, consider implement your own via rejection sampling.
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() % range) as u16);
+ let sample = ((u256_integer_internal() % range) as u16);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -158,7 +233,10 @@ module aptos_framework::randomness {
/// If you need perfect uniformity, consider implement your own via rejection sampling.
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() % range) as u32);
+ let sample = ((u256_integer_internal() % range) as u32);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -167,8 +245,15 @@ module aptos_framework::randomness {
/// 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 acquires PerBlockRandomness {
+ event::emit(RandomnessGeneratedEvent {});
+
+ u64_range_internal(min_incl, max_excl)
+ }
+
+ 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() % range) as u64);
+ let sample = ((u256_integer_internal() % range) as u64);
+
min_incl + sample
}
@@ -178,7 +263,10 @@ module aptos_framework::randomness {
/// If you need perfect uniformity, consider implement your own via rejection sampling.
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() % range) as u128);
+ let sample = ((u256_integer_internal() % range) as u128);
+
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
@@ -188,8 +276,8 @@ module aptos_framework::randomness {
/// 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 acquires PerBlockRandomness {
let range = max_excl - min_incl;
- let r0 = u256_integer();
- let r1 = u256_integer();
+ let r0 = u256_integer_internal();
+ let r1 = u256_integer_internal();
// Will compute sample := (r0 + r1*2^256) % range.
@@ -210,13 +298,20 @@ module aptos_framework::randomness {
assert sample >= 0 && sample < max_excl - min_incl;
};
+ event::emit(RandomnessGeneratedEvent {});
+
min_incl + sample
}
/// 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 acquires PerBlockRandomness {
let values = vector[];
+ if(n == 0) {
+ return vector[]
+ };
+
// Initialize into [0, 1, ..., n-1].
let i = 0;
while ({
@@ -241,7 +336,7 @@ module aptos_framework::randomness {
};
tail > 0
}) {
- let pop_position = u64_range(0, tail + 1);
+ let pop_position = u64_range_internal(0, tail + 1);
spec {
assert pop_position < len(values);
};
@@ -249,6 +344,8 @@ module aptos_framework::randomness {
tail = tail - 1;
};
+ event::emit(RandomnessGeneratedEvent {});
+
values
}
@@ -311,4 +408,172 @@ module aptos_framework::randomness {
let num = u64_integer();
debug::print(&num);
}
+
+ #[test_only]
+ fun assert_event_count_equals(count: u64) {
+ let events = event::emitted_events();
+ assert!(vector::length(&events) == count, 0);
+ }
+
+ #[test(fx = @aptos_framework)]
+ fun test_emit_events(fx: signer) acquires PerBlockRandomness {
+ initialize_for_testing(&fx);
+
+ let c = 0;
+ assert_event_count_equals(c);
+
+ let _ = bytes(1);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u8_integer();
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u16_integer();
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u32_integer();
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u64_integer();
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u128_integer();
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u256_integer();
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u8_range(0, 255);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u16_range(0, 255);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u32_range(0, 255);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u64_range(0, 255);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u128_range(0, 255);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = u256_range(0, 255);
+ c = c + 1;
+ assert_event_count_equals(c);
+
+ let _ = permutation(6);
+ c = c + 1;
+ assert_event_count_equals(c);
+ }
+
+ #[test(fx = @aptos_framework)]
+ fun test_bytes(fx: signer) acquires PerBlockRandomness {
+ initialize_for_testing(&fx);
+
+ let v = bytes(0);
+ assert!(vector::length(&v) == 0, 0);
+
+ let v = bytes(1);
+ assert!(vector::length(&v) == 1, 0);
+ let v = bytes(2);
+ assert!(vector::length(&v) == 2, 0);
+ let v = bytes(3);
+ assert!(vector::length(&v) == 3, 0);
+ let v = bytes(4);
+ assert!(vector::length(&v) == 4, 0);
+ let v = bytes(30);
+ assert!(vector::length(&v) == 30, 0);
+ let v = bytes(31);
+ assert!(vector::length(&v) == 31, 0);
+ let v = bytes(32);
+ assert!(vector::length(&v) == 32, 0);
+
+ let v = bytes(33);
+ assert!(vector::length(&v) == 33, 0);
+ let v = bytes(50);
+ assert!(vector::length(&v) == 50, 0);
+ let v = bytes(63);
+ assert!(vector::length(&v) == 63, 0);
+ let v = bytes(64);
+ assert!(vector::length(&v) == 64, 0);
+ }
+
+ #[test_only]
+ fun is_permutation(v: &vector): bool {
+ let present = vector[];
+
+ // Mark all elements from 0 to n-1 as not present
+ let n = vector::length(v);
+ for (i in 0..n) {
+ vector::push_back(&mut present, false);
+ };
+
+ for (i in 0..n) {
+ let e = vector::borrow(v, i);
+ let bit = vector::borrow_mut(&mut present, *e);
+ *bit = true;
+ };
+
+ for (i in 0..n) {
+ let bit = vector::borrow(&present, i);
+ if(*bit == false) {
+ return false
+ };
+ };
+
+ true
+ }
+
+ #[test(fx = @aptos_framework)]
+ fun test_permutation(fx: signer) acquires PerBlockRandomness {
+ initialize_for_testing(&fx);
+
+ let v = permutation(0);
+ assert!(vector::length(&v) == 0, 0);
+
+ test_permutation_internal(1);
+ test_permutation_internal(2);
+ test_permutation_internal(3);
+ test_permutation_internal(4);
+ }
+
+ #[test_only]
+ /// WARNING: Do not call this with a large `size`, since execution time will be \Omega(size!), where ! is the factorial
+ /// operator.
+ fun test_permutation_internal(size: u64) acquires PerBlockRandomness {
+ let num_permutations = 1;
+ let c = 1;
+ for (i in 0..size) {
+ num_permutations = num_permutations * c;
+ c = c + 1;
+ };
+
+ let permutations = table_with_length::new, bool>();
+
+ // This loop will not exit until all permutations are created
+ while(table_with_length::length(&permutations) < num_permutations) {
+ let v = permutation(size);
+ assert!(vector::length(&v) == size, 0);
+ assert!(is_permutation(&v), 0);
+
+ if(table_with_length::contains(&permutations, v) == false) {
+ table_with_length::add(&mut permutations, v, true);
+ }
+ };
+
+ table_with_length::drop_unchecked(permutations);
+ }
}
diff --git a/aptos-move/framework/aptos-framework/sources/randomness.spec.move b/aptos-move/framework/aptos-framework/sources/randomness.spec.move
index 1214c45425667..b0b060005dce5 100644
--- a/aptos-move/framework/aptos-framework/sources/randomness.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/randomness.spec.move
@@ -40,7 +40,7 @@ spec aptos_framework::randomness {
ensures exists(@aptos_framework) ==> global(@aptos_framework).round == round;
}
- spec next_blob(): vector {
+ spec next_32_bytes(): vector {
use std::hash;
include NextBlobAbortsIf;
let input = b"APTOS_RANDOMNESS";
@@ -118,7 +118,6 @@ spec aptos_framework::randomness {
// TODO(tengzhang): complete the aborts_if conditions
// include n > 1 ==> NextBlobAbortsIf;
// aborts_if n > 1 && !exists(@aptos_framework);
- aborts_if n == 0;
}
spec safe_add_mod_for_verification(a: u256, b: u256, m: u256): u256 {