Skip to content

Commit

Permalink
implement rust logics and specs
Browse files Browse the repository at this point in the history
  • Loading branch information
runtian-zhou committed Jan 14, 2025
1 parent e12fcbb commit 7be76a1
Show file tree
Hide file tree
Showing 82 changed files with 711 additions and 313 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
use crate::{
gas_feature_versions::{RELEASE_V1_14, RELEASE_V1_8, RELEASE_V1_9_SKIPPED},
gas_schedule::NativeGasParameters,
ver::gas_feature_versions::{RELEASE_V1_12, RELEASE_V1_13, RELEASE_V1_23},
ver::gas_feature_versions::{RELEASE_V1_12, RELEASE_V1_13, RELEASE_V1_23, RELEASE_V1_26},
};
use aptos_gas_algebra::{
InternalGas, InternalGasPerAbstractValueUnit, InternalGasPerArg, InternalGasPerByte,
Expand All @@ -20,6 +20,11 @@ crate::gas_schedule::macros::define_gas_parameters!(
[account_create_address_base: InternalGas, "account.create_address.base", 1102],
[account_create_signer_base: InternalGas, "account.create_signer.base", 1102],

// Permissioned signer gas parameters
[permission_address_base: InternalGas, { RELEASE_V1_26 => "permissioned_signer.permission_address.base"}, 1102],
[is_permissioned_signer_base: InternalGas, { RELEASE_V1_26 => "permissioned_signer.is_permissioned_signer.base"}, 1102],
[signer_from_permissioned_handle_base: InternalGas, { RELEASE_V1_26 => "permissioned_signer.signer_from_permissioned_handle.base"}, 1102],

// BN254 algebra gas parameters begin.
// Generated at time 1701559125.5498126 by `scripts/algebra-gas/update_bn254_algebra_gas_params.py` with gas_per_ns=209.10511688369482.
[algebra_ark_bn254_fq12_add: InternalGas, { 12.. => "algebra.ark_bn254_fq12_add" }, 809],
Expand Down
1 change: 1 addition & 0 deletions aptos-move/aptos-gas-schedule/src/ver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -89,4 +89,5 @@ pub mod gas_feature_versions {
pub const RELEASE_V1_22: u64 = 26;
pub const RELEASE_V1_23: u64 = 27;
pub const RELEASE_V1_24: u64 = 28;
pub const RELEASE_V1_26: u64 = 29;
}
2 changes: 1 addition & 1 deletion aptos-move/aptos-vm-profiling/src/bins/run_move.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ fn make_native_create_signer() -> NativeFunction {

let address = pop_arg!(args, AccountAddress);

Ok(NativeResult::ok(0.into(), smallvec![Value::signer(
Ok(NativeResult::ok(0.into(), smallvec![Value::master_signer(
address
)]))
})
Expand Down
10 changes: 7 additions & 3 deletions aptos-move/e2e-move-tests/src/tests/gas.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ use aptos_types::{
transaction::{EntryFunction, TransactionPayload},
};
use aptos_vm_environment::prod_configs::set_paranoid_type_checks;
use move_core_types::{identifier::Identifier, language_storage::ModuleId};
use move_core_types::{identifier::Identifier, language_storage::ModuleId, value::MoveValue};
use rand::{rngs::StdRng, SeedableRng};
use sha3::{Digest, Sha3_512};
use std::path::Path;
Expand All @@ -55,7 +55,9 @@ fn test_modify_gas_schedule_check_hash() {
"set_for_next_epoch_check_hash",
vec![],
vec![
bcs::to_bytes(&CORE_CODE_ADDRESS).unwrap(),
MoveValue::Signer(CORE_CODE_ADDRESS)
.simple_serialize()
.unwrap(),
bcs::to_bytes(&old_hash).unwrap(),
bcs::to_bytes(&bcs::to_bytes(&gas_schedule).unwrap()).unwrap(),
],
Expand All @@ -64,7 +66,9 @@ fn test_modify_gas_schedule_check_hash() {
harness
.executor
.exec("reconfiguration_with_dkg", "finish", vec![], vec![
bcs::to_bytes(&CORE_CODE_ADDRESS).unwrap(),
MoveValue::Signer(CORE_CODE_ADDRESS)
.simple_serialize()
.unwrap(),
]);

let (_, gas_params) = harness.get_gas_params();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
[package]
name = "test"
version = "0.0.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
script {
fun main(s1: &signer, u: u64, s2: &signer) {}
}
43 changes: 41 additions & 2 deletions aptos-move/e2e-move-tests/src/tests/scripts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,9 @@ use aptos_language_e2e_tests::account::TransactionBuilder;
use aptos_types::{
account_address::AccountAddress,
on_chain_config::FeatureFlag,
transaction::{Script, TransactionArgument},
transaction::{Script, TransactionArgument, TransactionStatus},
};
use move_core_types::language_storage::TypeTag;
use move_core_types::{language_storage::TypeTag, value::MoveValue};

#[test]
fn test_script_with_object_parameter() {
Expand Down Expand Up @@ -146,6 +146,45 @@ fn test_script_with_type_parameter() {
assert_success!(status);
}

#[test]
fn test_script_with_signer_parameter() {
let mut h = MoveHarness::new();

let alice = h.new_account_at(AccountAddress::from_hex_literal("0xa11ce").unwrap());

let package = build_package(
common::test_dir_path("script_with_signer.data/pack"),
aptos_framework::BuildOptions::default(),
)
.expect("building package must succeed");

let code = package.extract_script_code().into_iter().next().unwrap();

let txn = TransactionBuilder::new(alice.clone())
.script(Script::new(code, vec![], vec![
TransactionArgument::U64(0),
TransactionArgument::Serialized(
MoveValue::Signer(*alice.address())
.simple_serialize()
.unwrap(),
),
]))
.sequence_number(10)
.max_gas_amount(1_000_000)
.gas_unit_price(1)
.sign();

let status = h.run(txn);
assert_eq!(
status,
TransactionStatus::Keep(
aptos_types::transaction::ExecutionStatus::MiscellaneousError(Some(
aptos_types::vm_status::StatusCode::INVALID_MAIN_FUNCTION_SIGNATURE
))
)
);
}

#[test]
fn test_two_to_two_transfer() {
let mut h = MoveHarness::new();
Expand Down
17 changes: 14 additions & 3 deletions aptos-move/e2e-tests/src/executor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ use move_core_types::{
identifier::Identifier,
language_storage::{ModuleId, StructTag, TypeTag},
move_resource::{MoveResource, MoveStructType},
value::MoveValue,
};
use move_vm_runtime::{
module_traversal::{TraversalContext, TraversalStorage},
Expand Down Expand Up @@ -1042,13 +1043,23 @@ impl FakeExecutor {
let mut arg = args.clone();
match &dynamic_args {
ExecFuncTimerDynamicArgs::DistinctSigners => {
arg.insert(0, bcs::to_bytes(&extra_accounts.pop().unwrap()).unwrap());
arg.insert(
0,
MoveValue::Signer(extra_accounts.pop().unwrap())
.simple_serialize()
.unwrap(),
);
},
ExecFuncTimerDynamicArgs::DistinctSignersAndFixed(signers) => {
for signer in signers.iter().rev() {
arg.insert(0, bcs::to_bytes(&signer).unwrap());
arg.insert(0, MoveValue::Signer(*signer).simple_serialize().unwrap());
}
arg.insert(0, bcs::to_bytes(&extra_accounts.pop().unwrap()).unwrap());
arg.insert(
0,
MoveValue::Signer(extra_accounts.pop().unwrap())
.simple_serialize()
.unwrap(),
);
},
_ => {},
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1029,6 +1029,7 @@ Returns the inner entry function payload of the multisig payload.


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> [abstract] <b>false</b>;
<b>ensures</b> [abstract] result == <a href="transaction_context.md#0x1_transaction_context_spec_generate_unique_address">spec_generate_unique_address</a>();
</code></pre>

Expand All @@ -1055,6 +1056,7 @@ Returns the inner entry function payload of the multisig payload.


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> [abstract] <b>false</b>;
// This enforces <a id="high-level-req-3" href="#high-level-req">high-level requirement 3</a>:
<b>ensures</b> [abstract] result == <a href="transaction_context.md#0x1_transaction_context_spec_generate_unique_address">spec_generate_unique_address</a>();
</code></pre>
Expand Down
2 changes: 2 additions & 0 deletions aptos-move/framework/aptos-framework/doc/util.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ Note that this function does not put any constraint on <code>T</code>. If code u
deserialized a linear value, its their responsibility that the data they deserialize is
owned.

Function would abort if T has signer in it.


<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="util.md#0x1_util_from_bytes">from_bytes</a>&lt;T&gt;(bytes: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): T
</code></pre>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -58,11 +58,13 @@ spec aptos_framework::transaction_context {
}
spec generate_unique_address(): address {
pragma opaque;
aborts_if [abstract] false;
ensures [abstract] result == spec_generate_unique_address();
}
spec fun spec_generate_unique_address(): address;
spec generate_auid_address(): address {
pragma opaque;
aborts_if [abstract] false;
// property 3: Generating the unique address should return a vector with 32 bytes, if the auid feature flag is enabled.
/// [high-level-req-3]
ensures [abstract] result == spec_generate_unique_address();
Expand Down
8 changes: 8 additions & 0 deletions aptos-move/framework/aptos-framework/sources/util.move
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,17 @@ module aptos_framework::util {
/// Note that this function does not put any constraint on `T`. If code uses this function to
/// deserialized a linear value, its their responsibility that the data they deserialize is
/// owned.
///
/// Function would abort if T has signer in it.
public(friend) native fun from_bytes<T>(bytes: vector<u8>): T;

public fun address_from_bytes(bytes: vector<u8>): address {
from_bytes(bytes)
}

#[test(s1 = @0x123)]
#[expected_failure(abort_code = 0x10001, location = Self)]
fun test_signer_roundtrip(s1: signer) {
from_bytes<signer>(bcs::to_bytes(&s1));
}
}
2 changes: 2 additions & 0 deletions aptos-move/framework/aptos-stdlib/doc/from_bcs.md
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,8 @@ Note that this function does not put any constraint on <code>T</code>. If code u
deserialize a linear value, its their responsibility that the data they deserialize is
owned.

Function would abort if T has signer in it.


<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="from_bcs.md#0x1_from_bcs_from_bytes">from_bytes</a>&lt;T&gt;(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): T
</code></pre>
Expand Down
2 changes: 2 additions & 0 deletions aptos-move/framework/aptos-stdlib/doc/smart_table.md
Original file line number Diff line number Diff line change
Expand Up @@ -1479,6 +1479,7 @@ map_spec_has_key = spec_contains;


<pre><code><b>pragma</b> verify = <b>false</b>;
<b>pragma</b> opaque;
</code></pre>


Expand All @@ -1495,6 +1496,7 @@ map_spec_has_key = spec_contains;


<pre><code><b>pragma</b> verify = <b>false</b>;
<b>pragma</b> opaque;
</code></pre>


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,12 @@ spec aptos_std::smart_table {

spec destroy<K: drop, V: drop>(self: SmartTable<K, V>) {
pragma verify = false;
pragma opaque;
}

spec clear<K: drop, V: drop>(self: &mut SmartTable<K, V>) {
pragma verify = false;
pragma opaque;
}

spec split_one_bucket<K, V>(self: &mut SmartTable<K, V>) {
Expand Down
8 changes: 8 additions & 0 deletions aptos-move/framework/aptos-stdlib/sources/from_bcs.move
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,8 @@ module aptos_std::from_bcs {
/// Note that this function does not put any constraint on `T`. If code uses this function to
/// deserialize a linear value, its their responsibility that the data they deserialize is
/// owned.
///
/// Function would abort if T has signer in it.
public(friend) native fun from_bytes<T>(bytes: vector<u8>): T;
friend aptos_std::any;
friend aptos_std::copyable_any;
Expand All @@ -88,4 +90,10 @@ module aptos_std::from_bcs {
let bad_vec = b"01";
to_address(bad_vec);
}

#[test(s1 = @0x123)]
#[expected_failure(abort_code = 0x10001, location = Self)]
fun test_signer_roundtrip(s1: signer) {
from_bytes<signer>(bcs::to_bytes(&s1));
}
}
1 change: 1 addition & 0 deletions aptos-move/framework/move-stdlib/doc/bcs.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ details on BCS.

## Function `to_bytes`

Note: all natives would fail if the MoveValue contains a permissioned signer in it.
Returns the binary representation of <code>v</code> in BCS (Binary Canonical Serialization) format.
Aborts with <code>0x1c5</code> error code if serialization fails.

Expand Down
22 changes: 18 additions & 4 deletions aptos-move/framework/move-stdlib/doc/signer.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,26 @@

## Function `borrow_address`

Borrows the address of the signer
Conceptually, you can think of the <code><a href="signer.md#0x1_signer">signer</a></code> as being a struct wrapper around an
address
signer is a builtin move type that represents an address that has been verfied by the VM.

VM Runtime representation is equivalent to following:
```
enum signer has drop {
Master { account: address },
Permissioned { account: address, permissions_address: address },
}
```

for bcs serialization:

```
struct signer has drop { addr: address }
struct signer has drop {
account: address,
}
```
^ The discrepency is needed to maintain backwards compatibility of signer serialization
semantics.

<code>borrow_address</code> borrows this inner field


Expand Down
2 changes: 2 additions & 0 deletions aptos-move/framework/move-stdlib/sources/bcs.move
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
module std::bcs {
use std::option::Option;

/// Note: all natives would fail if the MoveValue contains a permissioned signer in it.

/// Returns the binary representation of `v` in BCS (Binary Canonical Serialization) format.
/// Aborts with `0x1c5` error code if serialization fails.
native public fun to_bytes<MoveValue>(v: &MoveValue): vector<u8>;
Expand Down
22 changes: 18 additions & 4 deletions aptos-move/framework/move-stdlib/sources/signer.move
Original file line number Diff line number Diff line change
@@ -1,10 +1,24 @@
module std::signer {
/// Borrows the address of the signer
/// Conceptually, you can think of the `signer` as being a struct wrapper around an
/// address
/// signer is a builtin move type that represents an address that has been verfied by the VM.
///
/// VM Runtime representation is equivalent to following:
/// ```
/// struct signer has drop { addr: address }
/// enum signer has drop {
/// Master { account: address },
/// Permissioned { account: address, permissions_address: address },
/// }
/// ```
///
/// for bcs serialization:
///
/// ```
/// struct signer has drop {
/// account: address,
/// }
/// ```
/// ^ The discrepency is needed to maintain backwards compatibility of signer serialization
/// semantics.
///
/// `borrow_address` borrows this inner field
native public fun borrow_address(s: &signer): &address;

Expand Down
2 changes: 2 additions & 0 deletions aptos-move/framework/move-stdlib/src/natives/bcs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ fn native_to_bytes(
let val = ref_to_val.read_ref()?;

let serialized_value = match ValueSerDeContext::new()
.with_legacy_signer()
.with_func_args_deserialization(context.function_value_extension())
.serialize(&val, &layout)?
{
Expand Down Expand Up @@ -136,6 +137,7 @@ fn serialized_size_impl(
let ty_layout = context.type_to_type_layout(ty)?;

ValueSerDeContext::new()
.with_legacy_signer()
.with_func_args_deserialization(context.function_value_extension())
.with_delayed_fields_serde()
.serialized_size(&value, &ty_layout)
Expand Down
2 changes: 1 addition & 1 deletion aptos-move/framework/move-stdlib/src/natives/unit_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ fn native_create_signers_for_testing(
let num_signers = safely_pop_arg!(args, u64);

let signers = Value::vector_for_testing_only(
(0..num_signers).map(|i| Value::signer(AccountAddress::new(to_le_bytes(i)))),
(0..num_signers).map(|i| Value::master_signer(AccountAddress::new(to_le_bytes(i)))),
);

Ok(smallvec![signers])
Expand Down
8 changes: 8 additions & 0 deletions aptos-move/framework/move-stdlib/tests/bcs_tests.move
Original file line number Diff line number Diff line change
Expand Up @@ -157,4 +157,12 @@ module std::bcs_tests {

assert!(std::cmp::compare(&bytes_val, &bytes_other).is_lt());
}

#[test(s1 = @0x123)]
fun test_signer_serialization(s1: signer) {
assert!(
bcs::to_bytes(&s1) == bcs::to_bytes(&@0x123),
1
);
}
}
Loading

0 comments on commit 7be76a1

Please sign in to comment.