From 3bd015468bb85aefb7ebc37c91c36c039399a187 Mon Sep 17 00:00:00 2001
From: "zhoujun.ma" <zhoujun@aptoslabs.com>
Date: Tue, 27 Feb 2024 02:47:57 -0800
Subject: [PATCH] update

---
 .../framework/aptos-stdlib/doc/simple_map.md  |  2 +
 .../aptos-stdlib/sources/simple_map.spec.move |  2 +
 aptos-move/framework/src/aptos.rs             |  1 +
 .../framework/src/natives/consensus_config.rs | 31 ++++++++++
 aptos-move/framework/src/natives/mod.rs       |  4 ++
 .../framework/src/natives/randomness.rs       | 58 +++++++++++++++++++
 .../move/move-stdlib/sources/hash.move        |  5 ++
 7 files changed, 103 insertions(+)
 create mode 100644 aptos-move/framework/src/natives/consensus_config.rs
 create mode 100644 aptos-move/framework/src/natives/randomness.rs

diff --git a/aptos-move/framework/aptos-stdlib/doc/simple_map.md b/aptos-move/framework/aptos-stdlib/doc/simple_map.md
index 844de13914d3c..c114cfab0f38f 100644
--- a/aptos-move/framework/aptos-stdlib/doc/simple_map.md
+++ b/aptos-move/framework/aptos-stdlib/doc/simple_map.md
@@ -734,6 +734,7 @@ Remove a key/value pair from the map. The key must exist.
 
 <pre><code><b>pragma</b> intrinsic;
 <b>pragma</b> opaque;
+<b>aborts_if</b> [abstract] <b>false</b>;
 <b>ensures</b> [abstract] <a href="simple_map.md#0x1_simple_map_spec_len">spec_len</a>(result) == 0;
 <b>ensures</b> [abstract] <b>forall</b> k: Key: !<a href="simple_map.md#0x1_simple_map_spec_contains_key">spec_contains_key</a>(result, k);
 </code></pre>
@@ -753,6 +754,7 @@ Remove a key/value pair from the map. The key must exist.
 
 <pre><code><b>pragma</b> intrinsic;
 <b>pragma</b> opaque;
+<b>aborts_if</b> [abstract] <b>false</b>;
 <b>ensures</b> [abstract] <a href="simple_map.md#0x1_simple_map_spec_len">spec_len</a>(result) == len(keys);
 <b>ensures</b> [abstract] <b>forall</b> k: Key: <a href="simple_map.md#0x1_simple_map_spec_contains_key">spec_contains_key</a>(result, k) &lt;==&gt; <a href="../../move-stdlib/doc/vector.md#0x1_vector_spec_contains">vector::spec_contains</a>(keys, k);
 <b>ensures</b> [abstract] <b>forall</b> i in 0..len(keys):
diff --git a/aptos-move/framework/aptos-stdlib/sources/simple_map.spec.move b/aptos-move/framework/aptos-stdlib/sources/simple_map.spec.move
index 9071fc043610c..fefe52ee5d18f 100644
--- a/aptos-move/framework/aptos-stdlib/sources/simple_map.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/simple_map.spec.move
@@ -71,6 +71,7 @@ spec aptos_std::simple_map {
     spec new<Key: store, Value: store>(): SimpleMap<Key, Value> {
         pragma intrinsic;
         pragma opaque;
+        aborts_if [abstract] false;
         ensures [abstract] spec_len(result) == 0;
         ensures [abstract] forall k: Key: !spec_contains_key(result, k);
     }
@@ -81,6 +82,7 @@ spec aptos_std::simple_map {
     ): SimpleMap<Key, Value> {
         pragma intrinsic;
         pragma opaque;
+        aborts_if [abstract] false;
         ensures [abstract] spec_len(result) == len(keys);
         ensures [abstract] forall k: Key: spec_contains_key(result, k) <==> vector::spec_contains(keys, k);
         ensures [abstract] forall i in 0..len(keys):
diff --git a/aptos-move/framework/src/aptos.rs b/aptos-move/framework/src/aptos.rs
index a78b0e7bbda4f..b27745c8eb289 100644
--- a/aptos-move/framework/src/aptos.rs
+++ b/aptos-move/framework/src/aptos.rs
@@ -187,6 +187,7 @@ static NAMED_ADDRESSES: Lazy<BTreeMap<String, NumericalAddress>> = Lazy::new(||
     result.insert("aptos_token".to_owned(), three);
     result.insert("aptos_token_objects".to_owned(), four);
     result.insert("core_resources".to_owned(), resources);
+    result.insert("vm".to_owned(), zero);
     result.insert("vm_reserved".to_owned(), zero);
     result
 });
diff --git a/aptos-move/framework/src/natives/consensus_config.rs b/aptos-move/framework/src/natives/consensus_config.rs
new file mode 100644
index 0000000000000..0d15f084b7f3d
--- /dev/null
+++ b/aptos-move/framework/src/natives/consensus_config.rs
@@ -0,0 +1,31 @@
+// Copyright © Aptos Foundation
+
+use aptos_native_interface::{
+    safely_pop_arg, RawSafeNative, SafeNativeBuilder, SafeNativeContext, SafeNativeResult,
+};
+use aptos_types::on_chain_config::OnChainConsensusConfig;
+use move_vm_runtime::native_functions::NativeFunction;
+use move_vm_types::{loaded_data::runtime_types::Type, values::Value};
+use smallvec::{smallvec, SmallVec};
+use std::collections::VecDeque;
+
+pub fn validator_txn_enabled(
+    _context: &mut SafeNativeContext,
+    _ty_args: Vec<Type>,
+    mut args: VecDeque<Value>,
+) -> SafeNativeResult<SmallVec<[Value; 1]>> {
+    let config_bytes = safely_pop_arg!(args, Vec<u8>);
+    let config = bcs::from_bytes::<OnChainConsensusConfig>(&config_bytes).unwrap_or_default();
+    Ok(smallvec![Value::bool(config.is_vtxn_enabled())])
+}
+
+pub fn make_all(
+    builder: &SafeNativeBuilder,
+) -> impl Iterator<Item = (String, NativeFunction)> + '_ {
+    let natives = vec![(
+        "validator_txn_enabled_internal",
+        validator_txn_enabled as RawSafeNative,
+    )];
+
+    builder.make_named_natives(natives)
+}
diff --git a/aptos-move/framework/src/natives/mod.rs b/aptos-move/framework/src/natives/mod.rs
index 408b9f660c11d..9f5cdf25b6cab 100644
--- a/aptos-move/framework/src/natives/mod.rs
+++ b/aptos-move/framework/src/natives/mod.rs
@@ -5,6 +5,7 @@
 pub mod account;
 pub mod aggregator_natives;
 pub mod code;
+pub mod consensus_config;
 pub mod create_signer;
 pub mod cryptography;
 pub mod debug;
@@ -12,6 +13,7 @@ pub mod event;
 pub mod hash;
 pub mod object;
 pub mod object_code_deployment;
+pub mod randomness;
 pub mod state_storage;
 pub mod string_utils;
 pub mod transaction_context;
@@ -62,6 +64,7 @@ pub fn all_natives(
     add_natives_from_module!("type_info", type_info::make_all(builder));
     add_natives_from_module!("util", util::make_all(builder));
     add_natives_from_module!("from_bcs", util::make_all(builder));
+    add_natives_from_module!("randomness", randomness::make_all(builder));
     add_natives_from_module!(
         "ristretto255_bulletproofs",
         cryptography::bulletproofs::make_all(builder)
@@ -79,6 +82,7 @@ pub fn all_natives(
     add_natives_from_module!("object", object::make_all(builder));
     add_natives_from_module!("debug", debug::make_all(builder));
     add_natives_from_module!("string_utils", string_utils::make_all(builder));
+    add_natives_from_module!("consensus_config", consensus_config::make_all(builder));
 
     make_table_from_iter(framework_addr, natives)
 }
diff --git a/aptos-move/framework/src/natives/randomness.rs b/aptos-move/framework/src/natives/randomness.rs
new file mode 100644
index 0000000000000..b35ca1e47b769
--- /dev/null
+++ b/aptos-move/framework/src/natives/randomness.rs
@@ -0,0 +1,58 @@
+// Copyright © Aptos Foundation
+
+use aptos_native_interface::{
+    RawSafeNative, SafeNativeBuilder, SafeNativeContext, SafeNativeResult,
+};
+use better_any::{Tid, TidAble};
+use move_vm_runtime::native_functions::NativeFunction;
+use move_vm_types::{loaded_data::runtime_types::Type, values::Value};
+use smallvec::{smallvec, SmallVec};
+use std::collections::VecDeque;
+
+/// A txn-local counter that increments each time a random 32-byte blob is requested.
+#[derive(Tid, Default)]
+pub struct RandomnessContext {
+    txn_local_state: Vec<u8>, //   8-byte counter
+}
+
+impl RandomnessContext {
+    pub fn new() -> Self {
+        Self {
+            txn_local_state: vec![0; 8],
+        }
+    }
+
+    pub fn increment(&mut self) {
+        for byte in self.txn_local_state.iter_mut() {
+            if *byte < 255 {
+                *byte += 1;
+                break;
+            } else {
+                *byte = 0;
+            }
+        }
+    }
+}
+
+pub fn fetch_and_increment_txn_counter(
+    context: &mut SafeNativeContext,
+    _ty_args: Vec<Type>,
+    _args: VecDeque<Value>,
+) -> SafeNativeResult<SmallVec<[Value; 1]>> {
+    // TODO: charge gas?
+    let rand_ctxt = context.extensions_mut().get_mut::<RandomnessContext>();
+    let ret = rand_ctxt.txn_local_state.to_vec();
+    rand_ctxt.increment();
+    Ok(smallvec![Value::vector_u8(ret)])
+}
+
+pub fn make_all(
+    builder: &SafeNativeBuilder,
+) -> impl Iterator<Item = (String, NativeFunction)> + '_ {
+    let natives = vec![(
+        "fetch_and_increment_txn_counter",
+        fetch_and_increment_txn_counter as RawSafeNative,
+    )];
+
+    builder.make_named_natives(natives)
+}
diff --git a/third_party/move/move-stdlib/sources/hash.move b/third_party/move/move-stdlib/sources/hash.move
index daadc4e815770..ad1d0ae794afa 100644
--- a/third_party/move/move-stdlib/sources/hash.move
+++ b/third_party/move/move-stdlib/sources/hash.move
@@ -5,4 +5,9 @@
 module std::hash {
     native public fun sha2_256(data: vector<u8>): vector<u8>;
     native public fun sha3_256(data: vector<u8>): vector<u8>;
+
+    spec sha3_256(data: vector<u8>): vector<u8> {
+        aborts_if [abstract] false;
+        ensures [abstract] len(result) == 32;
+    }
 }