diff --git a/aptos-framework/doc/randomness.md b/aptos-framework/doc/randomness.md index 36969528f..057c243ea 100644 --- a/aptos-framework/doc/randomness.md +++ b/aptos-framework/doc/randomness.md @@ -38,7 +38,7 @@ Security holds under the same proof-of-stake assumption that secures the Aptos n - [Function `safe_add_mod`](#0x1_randomness_safe_add_mod) - [Function `safe_add_mod_for_verification`](#0x1_randomness_safe_add_mod_for_verification) - [Function `fetch_and_increment_txn_counter`](#0x1_randomness_fetch_and_increment_txn_counter) -- [Function `is_safe_call`](#0x1_randomness_is_safe_call) +- [Function `is_unbiasable`](#0x1_randomness_is_unbiasable) - [Specification](#@Specification_1) - [Function `initialize`](#@Specification_1_initialize) - [Function `on_new_block`](#@Specification_1_on_new_block) @@ -55,7 +55,7 @@ Security holds under the same proof-of-stake assumption that secures the Aptos n - [Function `permutation`](#@Specification_1_permutation) - [Function `safe_add_mod_for_verification`](#@Specification_1_safe_add_mod_for_verification) - [Function `fetch_and_increment_txn_counter`](#@Specification_1_fetch_and_increment_txn_counter) - - [Function `is_safe_call`](#@Specification_1_is_safe_call) + - [Function `is_unbiasable`](#@Specification_1_is_unbiasable) 
use 0x1::event;
@@ -190,7 +190,8 @@ Event emitted every time a public randomness API in this module is called.
 
 
 
-Randomness APIs calls must originate from a private entry function. Otherwise, test-and-abort attacks are possible.
+Randomness APIs calls must originate from a private entry function with
+#[randomness] annotation. Otherwise, test-and-abort attacks are possible.
 
 
 
const E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT: u64 = 1;
@@ -278,7 +279,7 @@ of the hash function).
 
 
 
fun next_32_bytes(): vector<u8> acquires PerBlockRandomness {
-    assert!(is_safe_call(), E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT);
+    assert!(is_unbiasable(), E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT);
 
     let input = DST;
     let randomness = borrow_global<PerBlockRandomness>(@aptos_framework);
@@ -946,6 +947,7 @@ Compute (a + b) % m, assuming m >= 1, 0 <= a < m, 0&
 ## Function `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>
@@ -964,16 +966,17 @@ Fetches and increments a transaction-specific 32-byte randomness-related counter
 
 
 
-
+
 
-## Function `is_safe_call`
+## Function `is_unbiasable`
 
-Called in each randomness generation function to ensure certain safety invariants.
-1. Ensure that the TXN that led to the call of this function had a private (or friend) entry function as its TXN payload.
-2. TBA
+Called in each randomness generation function to ensure certain safety invariants, namely:
+1. The transaction that led to the call of this function had a private (or friend) entry
+function as its payload.
+2. The entry function had #[randomness] annotation.
 
 
-
fun is_safe_call(): bool
+
fun is_unbiasable(): bool
 

 
 
@@ -982,7 +985,7 @@ Called in each randomness generation function to ensure certain safety invariant
 Implementation
 
 
-
native fun is_safe_call(): bool;
+
native fun is_unbiasable(): bool;
 

 
 
@@ -1071,7 +1074,7 @@ Called in each randomness generation function to ensure certain safety invariant
 
schema NextBlobAbortsIf {
     let randomness = global<PerBlockRandomness>(@aptos_framework);
     aborts_if option::spec_is_none(randomness.seed);
-    aborts_if !spec_is_safe_call();
+    aborts_if !spec_is_unbiasable();
     aborts_if !exists<PerBlockRandomness>(@aptos_framework);
 }
 

@@ -1323,12 +1326,12 @@ Called in each randomness generation function to ensure certain safety invariant
 
 
 
-
+
 
-### Function `is_safe_call`
+### Function `is_unbiasable`
 
 
-
fun is_safe_call(): bool
+
fun is_unbiasable(): bool
 

 
 
@@ -1336,16 +1339,16 @@ Called in each randomness generation function to ensure certain safety invariant
 
 
pragma opaque;
 aborts_if [abstract] false;
-ensures [abstract] result == spec_is_safe_call();
+ensures [abstract] result == spec_is_unbiasable();
 

 
 
 
 
-
+
 
 
-
fun spec_is_safe_call(): bool;
+
fun spec_is_unbiasable(): bool;
 

 
 
diff --git a/aptos-framework/sources/randomness.move b/aptos-framework/sources/randomness.move
index 4679146cd..8873ce72d 100644
--- a/aptos-framework/sources/randomness.move
+++ b/aptos-framework/sources/randomness.move
@@ -22,7 +22,8 @@ module aptos_framework::randomness {
 
     const DST: vector = b"APTOS_RANDOMNESS";
 
-    /// Randomness APIs calls must originate from a private entry function. Otherwise, test-and-abort attacks are possible.
+    /// Randomness APIs calls must originate from a private entry function with
+    /// `#[randomness]` annotation. Otherwise, test-and-abort attacks are possible.
     const E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT: u64 = 1;
 
     const MAX_U256: u256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
@@ -71,7 +72,7 @@ module aptos_framework::randomness {
     /// 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);
+        assert!(is_unbiasable(), E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT);
 
         let input = DST;
         let randomness = borrow_global(@aptos_framework);
@@ -377,12 +378,14 @@ module aptos_framework::randomness {
     }
 
     /// 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.
     native fun fetch_and_increment_txn_counter(): vector;
 
-    /// Called in each randomness generation function to ensure certain safety invariants.
-    ///  1. Ensure that the TXN that led to the call of this function had a private (or friend) entry function as its TXN payload.
-    ///  2. TBA
-    native fun is_safe_call(): bool;
+    /// Called in each randomness generation function to ensure certain safety invariants, namely:
+    ///  1. The transaction that led to the call of this function had a private (or friend) entry
+    ///     function as its payload.
+    ///  2. The entry function had `#[randomness]` annotation.
+    native fun is_unbiasable(): bool;
 
     #[test]
     fun test_safe_add_mod() {
@@ -403,8 +406,8 @@ module aptos_framework::randomness {
     fun randomness_smoke_test(fx: signer) acquires PerBlockRandomness {
         initialize(&fx);
         set_seed(x"0000000000000000000000000000000000000000000000000000000000000000");
-        // Test cases should always be a safe place to do a randomness call from.
-        assert!(is_safe_call(), 0);
+        // Test cases should always have no bias for any randomness call.
+        assert!(is_unbiasable(), 0);
         let num = u64_integer();
         debug::print(&num);
     }
diff --git a/aptos-framework/sources/randomness.spec.move b/aptos-framework/sources/randomness.spec.move
index b0b060005..ded9df973 100644
--- a/aptos-framework/sources/randomness.spec.move
+++ b/aptos-framework/sources/randomness.spec.move
@@ -15,13 +15,13 @@ spec aptos_framework::randomness {
 
     spec fun spec_fetch_and_increment_txn_counter(): vector;
 
-    spec is_safe_call(): bool {
+    spec is_unbiasable(): bool {
         pragma opaque;
         aborts_if [abstract] false;
-        ensures [abstract] result == spec_is_safe_call();
+        ensures [abstract] result == spec_is_unbiasable();
     }
 
-    spec fun spec_is_safe_call(): bool;
+    spec fun spec_is_unbiasable(): bool;
 
     spec initialize(framework: &signer) {
         use std::option;
@@ -55,7 +55,7 @@ spec aptos_framework::randomness {
     spec schema NextBlobAbortsIf {
         let randomness = global(@aptos_framework);
         aborts_if option::spec_is_none(randomness.seed);
-        aborts_if !spec_is_safe_call();
+        aborts_if !spec_is_unbiasable();
         aborts_if !exists(@aptos_framework);
     }