[randomness] Add entry function annotation (#12134)

Adds `#[randomness]` annotation which should be used to mark
entry functions which use randomness. For example
```
#[randomness]
entry fun foo() {
  let _ = randomness::u64_integer();
}
```

The attribute has the following semantics:
1. It can only be used for entry functions. Using it on other type
    of functions is not allowed.
2. It can be used on entry functions even if they don't use randomness.
3. If an entry function doesn't have an annotation, but uses randomness,
    the randomness call fails at runtime.

GitOrigin-RevId: 0c7a0ae23909b9a48a8ae8ca875c090b3fc108d6

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)
 
 
 <pre><code><b>use</b> <a href="event.md#0x1_event">0x1::event</a>;
@@ -190,7 +190,8 @@ Event emitted every time a public randomness API in this module is called.
 
 <a id="0x1_randomness_E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT"></a>
 
-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
+<code>#[<a href="randomness.md#0x1_randomness">randomness</a>]</code> annotation. Otherwise, test-and-abort attacks are possible.
 
 
 <pre><code><b>const</b> <a href="randomness.md#0x1_randomness_E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT">E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT</a>: u64 = 1;
@@ -278,7 +279,7 @@ of the hash function).
 
 
 <pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_next_32_bytes">next_32_bytes</a>(): <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt; <b>acquires</b> <a href="randomness.md#0x1_randomness_PerBlockRandomness">PerBlockRandomness</a> {
-    <b>assert</b>!(<a href="randomness.md#0x1_randomness_is_safe_call">is_safe_call</a>(), <a href="randomness.md#0x1_randomness_E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT">E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT</a>);
+    <b>assert</b>!(<a href="randomness.md#0x1_randomness_is_unbiasable">is_unbiasable</a>(), <a href="randomness.md#0x1_randomness_E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT">E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT</a>);
 
     <b>let</b> input = <a href="randomness.md#0x1_randomness_DST">DST</a>;
     <b>let</b> <a href="randomness.md#0x1_randomness">randomness</a> = <b>borrow_global</b>&lt;<a href="randomness.md#0x1_randomness_PerBlockRandomness">PerBlockRandomness</a>&gt;(@aptos_framework);
@@ -946,6 +947,7 @@ Compute <code>(a + b) % m</code>, assuming <code>m &gt;= 1, 0 &lt;= a &lt; m, 0&
 ## Function `fetch_and_increment_txn_counter`
 
 Fetches and increments a transaction-specific 32-byte randomness-related counter.
+Aborts with <code><a href="randomness.md#0x1_randomness_E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT">E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT</a></code> if randomness is not unbiasable.
 
 
 <pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_fetch_and_increment_txn_counter">fetch_and_increment_txn_counter</a>(): <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;
@@ -964,16 +966,17 @@ Fetches and increments a transaction-specific 32-byte randomness-related counter
 
 </details>
 
-<a id="0x1_randomness_is_safe_call"></a>
+<a id="0x1_randomness_is_unbiasable"></a>
 
-## 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 <code>#[<a href="randomness.md#0x1_randomness">randomness</a>]</code> annotation.
 
 
-<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_is_safe_call">is_safe_call</a>(): bool
+<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_is_unbiasable">is_unbiasable</a>(): bool
 </code></pre>
 
 
@@ -982,7 +985,7 @@ Called in each randomness generation function to ensure certain safety invariant
 <summary>Implementation</summary>
 
 
-<pre><code><b>native</b> <b>fun</b> <a href="randomness.md#0x1_randomness_is_safe_call">is_safe_call</a>(): bool;
+<pre><code><b>native</b> <b>fun</b> <a href="randomness.md#0x1_randomness_is_unbiasable">is_unbiasable</a>(): bool;
 </code></pre>
 
 
@@ -1071,7 +1074,7 @@ Called in each randomness generation function to ensure certain safety invariant
 <pre><code><b>schema</b> <a href="randomness.md#0x1_randomness_NextBlobAbortsIf">NextBlobAbortsIf</a> {
     <b>let</b> <a href="randomness.md#0x1_randomness">randomness</a> = <b>global</b>&lt;<a href="randomness.md#0x1_randomness_PerBlockRandomness">PerBlockRandomness</a>&gt;(@aptos_framework);
     <b>aborts_if</b> <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_none">option::spec_is_none</a>(<a href="randomness.md#0x1_randomness">randomness</a>.seed);
-    <b>aborts_if</b> !<a href="randomness.md#0x1_randomness_spec_is_safe_call">spec_is_safe_call</a>();
+    <b>aborts_if</b> !<a href="randomness.md#0x1_randomness_spec_is_unbiasable">spec_is_unbiasable</a>();
     <b>aborts_if</b> !<b>exists</b>&lt;<a href="randomness.md#0x1_randomness_PerBlockRandomness">PerBlockRandomness</a>&gt;(@aptos_framework);
 }
 </code></pre>
@@ -1323,29 +1326,29 @@ Called in each randomness generation function to ensure certain safety invariant
 
 
 
-<a id="@Specification_1_is_safe_call"></a>
+<a id="@Specification_1_is_unbiasable"></a>
 
-### Function `is_safe_call`
+### Function `is_unbiasable`
 
 
-<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_is_safe_call">is_safe_call</a>(): bool
+<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_is_unbiasable">is_unbiasable</a>(): bool
 </code></pre>
 
 
 
 
 <pre><code><b>pragma</b> opaque;
 <b>aborts_if</b> [abstract] <b>false</b>;
-<b>ensures</b> [abstract] result == <a href="randomness.md#0x1_randomness_spec_is_safe_call">spec_is_safe_call</a>();
+<b>ensures</b> [abstract] result == <a href="randomness.md#0x1_randomness_spec_is_unbiasable">spec_is_unbiasable</a>();
 </code></pre>
 
 
 
 
-<a id="0x1_randomness_spec_is_safe_call"></a>
+<a id="0x1_randomness_spec_is_unbiasable"></a>
 
 
-<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_spec_is_safe_call">spec_is_safe_call</a>(): bool;
+<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_spec_is_unbiasable">spec_is_unbiasable</a>(): bool;
 </code></pre>
 
 

aptos-framework/sources/randomness.move

@@ -22,7 +22,8 @@ module aptos_framework::randomness {
 
     const DST: vector<u8> = 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<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);
@@ -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<u8>;
 
-    /// 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);
     }

aptos-framework/sources/randomness.spec.move

@@ -15,13 +15,13 @@ spec aptos_framework::randomness {
 
     spec fun spec_fetch_and_increment_txn_counter(): vector<u8>;
 
-    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<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);
     }