Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
zjma committed Feb 27, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent 2eb6add commit 3bd0154
Showing 7 changed files with 103 additions and 0 deletions.
2 changes: 2 additions & 0 deletions aptos-move/framework/aptos-stdlib/doc/simple_map.md
Original file line number Diff line number Diff line change
@@ -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):
Original file line number Diff line number Diff line change
@@ -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):
1 change: 1 addition & 0 deletions aptos-move/framework/src/aptos.rs
Original file line number Diff line number Diff line change
@@ -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
});
31 changes: 31 additions & 0 deletions aptos-move/framework/src/natives/consensus_config.rs
Original file line number Diff line number Diff line change
@@ -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)
}
4 changes: 4 additions & 0 deletions aptos-move/framework/src/natives/mod.rs
Original file line number Diff line number Diff line change
@@ -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)
}
58 changes: 58 additions & 0 deletions aptos-move/framework/src/natives/randomness.rs
Original file line number Diff line number Diff line change
@@ -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)
}
5 changes: 5 additions & 0 deletions third_party/move/move-stdlib/sources/hash.move
Original file line number Diff line number Diff line change
@@ -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;
}
}

0 comments on commit 3bd0154

Please sign in to comment.