update

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):

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):

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
 });

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)
+}

aptos-move/framework/src/natives/mod.rs

@@ -5,13 +5,15 @@
 pub mod account;
 pub mod aggregator_natives;
 pub mod code;
+pub mod consensus_config;
 pub mod create_signer;
 pub mod cryptography;
 pub mod debug;
 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)
 }

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)
+}

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;
+    }
 }