From e9283bd14b9bcd25387346414a6329fa5d59d785 Mon Sep 17 00:00:00 2001 From: franck44 Date: Mon, 23 Dec 2024 09:08:57 +1100 Subject: [PATCH] Formatting [Move] see #116 --- .../sources/native_bridge.move | 403 ++++++++++-------- .../sources/native_bridge.spec.move | 328 +++++++------- 2 files changed, 389 insertions(+), 342 deletions(-) diff --git a/aptos-move/framework/aptos-framework/sources/native_bridge.move b/aptos-move/framework/aptos-framework/sources/native_bridge.move index e425f59fd9c22..7db68c689cb9c 100644 --- a/aptos-move/framework/aptos-framework/sources/native_bridge.move +++ b/aptos-move/framework/aptos-framework/sources/native_bridge.move @@ -2,9 +2,9 @@ module aptos_framework::native_bridge { use std::features; use aptos_std::smart_table::{Self, SmartTable}; - use aptos_framework::ethereum::{Self, EthereumAddress}; + use aptos_framework::ethereum::{Self, EthereumAddress}; use aptos_framework::account; - use aptos_framework::event::{Self, EventHandle}; + use aptos_framework::event::{Self, EventHandle}; use aptos_framework::signer; use aptos_framework::system_addresses; #[test_only] @@ -37,19 +37,19 @@ module aptos_framework::native_bridge { friend aptos_framework::genesis; struct AptosCoinBurnCapability has key { - burn_cap: BurnCapability, + burn_cap: BurnCapability } struct AptosCoinMintCapability has key { - mint_cap: MintCapability, + mint_cap: MintCapability } struct AptosFABurnCapabilities has key { - burn_ref: BurnRef, + burn_ref: BurnRef } struct AptosFAMintCapabilities has key { - burn_ref: MintRef, + burn_ref: MintRef } #[event] @@ -59,7 +59,7 @@ module aptos_framework::native_bridge { initiator: address, recipient: vector, amount: u64, - nonce: u64, + nonce: u64 } #[event] @@ -69,13 +69,13 @@ module aptos_framework::native_bridge { initiator: vector, recipient: address, amount: u64, - nonce: u64, + nonce: u64 } /// This struct will store the event handles for bridge events. struct BridgeEvents has key, store { bridge_transfer_initiated_events: EventHandle, - bridge_transfer_completed_events: EventHandle, + bridge_transfer_completed_events: EventHandle } /// A nonce to ensure the uniqueness of bridge transfers @@ -85,7 +85,7 @@ module aptos_framework::native_bridge { /// A smart table wrapper struct SmartTableWrapper has key, store { - inner: SmartTable, + inner: SmartTable } /// Details on the outbound transfer @@ -93,35 +93,35 @@ module aptos_framework::native_bridge { bridge_transfer_id: vector, initiator: address, recipient: EthereumAddress, - amount: u64, + amount: u64 } struct BridgeConfig has key { bridge_relayer: address, - bridge_fee: u64, + bridge_fee: u64 } #[event] /// Event emitted when the bridge relayer is updated. struct BridgeConfigRelayerUpdated has store, drop { old_relayer: address, - new_relayer: address, + new_relayer: address } #[event] /// An event triggered upon change of bridgefee struct BridgeFeeChangedEvent has store, drop { old_bridge_fee: u64, - new_bridge_fee: u64, + new_bridge_fee: u64 } /// Converts a u64 to a 32-byte vector. - /// + /// /// @param value The u64 value to convert. /// @return A 32-byte vector containing the u64 value in little-endian order. - /// + /// /// How BCS works: https://github.com/zefchain/bcs?tab=readme-ov-file#booleans-and-integers - /// + /// /// @example: a u64 value 0x12_34_56_78_ab_cd_ef_00 is converted to a 32-byte vector: /// [0x00, 0x00, ..., 0x00, 0x12, 0x34, 0x56, 0x78, 0xab, 0xcd, 0xef, 0x00] public(friend) fun normalize_u64_to_32_bytes(value: &u64): vector { @@ -134,7 +134,9 @@ module aptos_framework::native_bridge { /// Checks if a bridge transfer ID is associated with an inbound nonce. /// @param bridge_transfer_id The bridge transfer ID. /// @return `true` if the ID is associated with an existing inbound nonce, `false` otherwise. - public(friend) fun is_inbound_nonce_set(bridge_transfer_id: vector): bool acquires SmartTableWrapper { + public(friend) fun is_inbound_nonce_set( + bridge_transfer_id: vector + ): bool acquires SmartTableWrapper { let table = borrow_global, u64>>(@aptos_framework); smart_table::contains(&table.inner, bridge_transfer_id) } @@ -147,8 +149,12 @@ module aptos_framework::native_bridge { /// @param nonce The unique nonce for the transfer. /// @return A `BridgeTransferDetails` object. /// @abort If the amount is zero or locks are invalid. - public(friend) fun create_details(initiator: address, recipient: EthereumAddress, amount: u64, nonce: u64) - : OutboundTransfer { + public(friend) fun create_details( + initiator: address, + recipient: EthereumAddress, + amount: u64, + nonce: u64 + ): OutboundTransfer { assert!(amount > 0, EZERO_AMOUNT); // Create a bridge transfer ID algorithmically @@ -159,22 +165,18 @@ module aptos_framework::native_bridge { vector::append(&mut combined_bytes, bcs::to_bytes(&nonce)); let bridge_transfer_id = keccak256(combined_bytes); - OutboundTransfer { - bridge_transfer_id, - initiator, - recipient, - amount, - } + OutboundTransfer { bridge_transfer_id, initiator, recipient, amount } } - /// Record details of an initiated transfer for quick lookup of details, mapping bridge transfer ID to transfer details + /// Record details of an initiated transfer for quick lookup of details, mapping bridge transfer ID to transfer details /// /// @param bridge_transfer_id Bridge transfer ID. /// @param details The bridge transfer details public(friend) fun add(nonce: u64, details: OutboundTransfer) acquires SmartTableWrapper { assert!(features::abort_native_bridge_enabled(), ENATIVE_BRIDGE_NOT_ENABLED); - let table = borrow_global_mut>(@aptos_framework); + let table = + borrow_global_mut>(@aptos_framework); smart_table::add(&mut table.inner, nonce, details); } @@ -182,11 +184,14 @@ module aptos_framework::native_bridge { /// /// @param bridge_transfer_id Bridge transfer ID. /// @param details The bridge transfer details - public(friend) fun set_bridge_transfer_id_to_inbound_nonce(bridge_transfer_id: vector, inbound_nonce: u64) acquires SmartTableWrapper { + public(friend) fun set_bridge_transfer_id_to_inbound_nonce( + bridge_transfer_id: vector, inbound_nonce: u64 + ) acquires SmartTableWrapper { assert!(features::abort_native_bridge_enabled(), ENATIVE_BRIDGE_NOT_ENABLED); assert_valid_bridge_transfer_id(&bridge_transfer_id); - let table = borrow_global_mut, u64>>(@aptos_framework); + let table = + borrow_global_mut, u64>>(@aptos_framework); smart_table::add(&mut table.inner, bridge_transfer_id, inbound_nonce); } @@ -194,7 +199,9 @@ module aptos_framework::native_bridge { /// /// @param bridge_transfer_id The bridge transfer ID to validate. /// @abort If the ID is invalid. - public(friend) fun assert_valid_bridge_transfer_id(bridge_transfer_id: &vector) { + public(friend) fun assert_valid_bridge_transfer_id( + bridge_transfer_id: &vector + ) { assert!(vector::length(bridge_transfer_id) == 32, EINVALID_BRIDGE_TRANSFER_ID); } @@ -202,7 +209,12 @@ module aptos_framework::native_bridge { /// /// @param details The bridge transfer details. /// @return The generated bridge transfer ID. - public(friend) fun bridge_transfer_id(initiator: address, recipient: EthereumAddress, amount: u64, nonce: u64) : vector { + public(friend) fun bridge_transfer_id( + initiator: address, + recipient: EthereumAddress, + amount: u64, + nonce: u64 + ): vector { // Serialize each param let initiator_bytes = bcs::to_bytes
(&initiator); let recipient_bytes = ethereum::get_inner_ethereum_address(recipient); @@ -216,15 +228,18 @@ module aptos_framework::native_bridge { vector::append(&mut combined_bytes, nonce_bytes); keccak256(combined_bytes) } - + #[view] /// Gets the bridge transfer details (`OutboundTransfer`) from the given nonce. /// @param nonce The nonce of the bridge transfer. /// @return The `OutboundTransfer` struct containing the transfer details. /// @abort If the nonce is not found in the smart table. - public fun get_bridge_transfer_details_from_nonce(nonce: u64): OutboundTransfer acquires SmartTableWrapper { - let table = borrow_global>(@aptos_framework); - + public fun get_bridge_transfer_details_from_nonce( + nonce: u64 + ): OutboundTransfer acquires SmartTableWrapper { + let table = + borrow_global>(@aptos_framework); + // Check if the nonce exists in the table assert!(smart_table::contains(&table.inner, nonce), ENONCE_NOT_FOUND); @@ -237,22 +252,24 @@ module aptos_framework::native_bridge { /// @param bridge_transfer_id The ID bridge transfer. /// @return the nonce /// @abort If the nonce is not found in the smart table. - public fun get_inbound_nonce_from_bridge_transfer_id(bridge_transfer_id: vector): u64 acquires SmartTableWrapper { + public fun get_inbound_nonce_from_bridge_transfer_id( + bridge_transfer_id: vector + ): u64 acquires SmartTableWrapper { let table = borrow_global, u64>>(@aptos_framework); - // Check if the nonce exists in the table + // Check if the nonce exists in the table assert!(smart_table::contains(&table.inner, bridge_transfer_id), ENONCE_NOT_FOUND); // If it exists, return the associated nonce *smart_table::borrow(&table.inner, bridge_transfer_id) } - /// Increment and get the current nonce - fun increment_and_get_nonce(): u64 acquires Nonce { - let nonce_ref = borrow_global_mut(@aptos_framework); - nonce_ref.value = nonce_ref.value + 1; - nonce_ref.value - } + /// Increment and get the current nonce + fun increment_and_get_nonce(): u64 acquires Nonce { + let nonce_ref = borrow_global_mut(@aptos_framework); + nonce_ref.value = nonce_ref.value + 1; + nonce_ref.value + } /// Initializes the module and stores the `EventHandle`s in the resource. public fun initialize(aptos_framework: &signer) { @@ -260,7 +277,7 @@ module aptos_framework::native_bridge { let bridge_config = BridgeConfig { bridge_relayer: signer::address_of(aptos_framework), - bridge_fee: 40_000_000_000, + bridge_fee: 40_000_000_000 }; move_to(aptos_framework, bridge_config); @@ -271,24 +288,27 @@ module aptos_framework::native_bridge { ); // Create the Nonce resource with an initial value of 0 - move_to(aptos_framework, Nonce { - value: 0 - }); + move_to(aptos_framework, Nonce { value: 0 }); - move_to(aptos_framework, BridgeEvents { - bridge_transfer_initiated_events: account::new_event_handle(aptos_framework), - bridge_transfer_completed_events: account::new_event_handle(aptos_framework), - }); - system_addresses::assert_aptos_framework(aptos_framework); + move_to( + aptos_framework, + BridgeEvents { + bridge_transfer_initiated_events: account::new_event_handle< + BridgeTransferInitiatedEvent>(aptos_framework), + bridge_transfer_completed_events: account::new_event_handle< + BridgeTransferCompletedEvent>(aptos_framework) + } + ); + system_addresses::assert_aptos_framework(aptos_framework); let nonces_to_details = SmartTableWrapper { - inner: smart_table::new(), + inner: smart_table::new() }; move_to(aptos_framework, nonces_to_details); let ids_to_inbound_nonces = SmartTableWrapper, u64> { - inner: smart_table::new(), + inner: smart_table::new() }; move_to(aptos_framework, ids_to_inbound_nonces); @@ -317,7 +337,9 @@ module aptos_framework::native_bridge { /// /// @param aptos_framework The signer representing the Aptos framework. /// @param burn_cap The burn capability for AptosCoin. - public fun store_aptos_coin_burn_cap(aptos_framework: &signer, burn_cap: BurnCapability) { + public fun store_aptos_coin_burn_cap( + aptos_framework: &signer, burn_cap: BurnCapability + ) { system_addresses::assert_aptos_framework(aptos_framework); if (features::operations_default_to_fa_apt_store_enabled()) { let burn_ref = coin::convert_and_take_paired_burn_ref(burn_cap); @@ -331,7 +353,9 @@ module aptos_framework::native_bridge { /// /// @param aptos_framework The signer representing the Aptos framework. /// @param mint_cap The mint capability for AptosCoin. - public fun store_aptos_coin_mint_cap(aptos_framework: &signer, mint_cap: MintCapability) { + public fun store_aptos_coin_mint_cap( + aptos_framework: &signer, mint_cap: MintCapability + ) { system_addresses::assert_aptos_framework(aptos_framework); move_to(aptos_framework, AptosCoinMintCapability { mint_cap }) } @@ -344,10 +368,13 @@ module aptos_framework::native_bridge { public(friend) fun mint(recipient: address, amount: u64) acquires AptosCoinMintCapability { assert!(features::abort_native_bridge_enabled(), ENATIVE_BRIDGE_NOT_ENABLED); - coin::deposit(recipient, coin::mint( - amount, - &borrow_global(@aptos_framework).mint_cap - )); + coin::deposit( + recipient, + coin::mint( + amount, + &borrow_global(@aptos_framework).mint_cap + ) + ); } /// Burns a specified amount of AptosCoin from an address. @@ -361,75 +388,74 @@ module aptos_framework::native_bridge { coin::burn_from( from, amount, - &borrow_global(@aptos_framework).burn_cap, + &borrow_global(@aptos_framework).burn_cap ); } /// Initiate a bridge transfer of MOVE from Movement to Ethereum - /// Anyone can initiate a bridge transfer from the source chain - /// The amount is burnt from the initiator and the module-level nonce is incremented - /// @param initiator The initiator's Ethereum address as a vector of bytes. - /// @param recipient The address of the recipient on the Aptos blockchain. - /// @param amount The amount of assets to be locked. - public entry fun initiate_bridge_transfer( - initiator: &signer, - recipient: vector, - amount: u64 + /// Anyone can initiate a bridge transfer from the source chain + /// The amount is burnt from the initiator and the module-level nonce is incremented + /// @param initiator The initiator's Ethereum address as a vector of bytes. + /// @param recipient The address of the recipient on the Aptos blockchain. + /// @param amount The amount of assets to be locked. + public entry fun initiate_bridge_transfer( + initiator: &signer, recipient: vector, amount: u64 ) acquires BridgeEvents, Nonce, AptosCoinBurnCapability, AptosCoinMintCapability, SmartTableWrapper, BridgeConfig { - let initiator_address = signer::address_of(initiator); - let ethereum_address = ethereum::ethereum_address_20_bytes(recipient); + let initiator_address = signer::address_of(initiator); + let ethereum_address = ethereum::ethereum_address_20_bytes(recipient); // Ensure the amount is enough for the bridge fee and charge for it let new_amount = charge_bridge_fee(amount); - // Increment and retrieve the nonce - let nonce = increment_and_get_nonce(); - - // Create bridge transfer details - let details = create_details( - initiator_address, - ethereum_address, - new_amount, - nonce - ); - - let bridge_transfer_id = bridge_transfer_id( - initiator_address, - ethereum_address, - new_amount, + // Increment and retrieve the nonce + let nonce = increment_and_get_nonce(); + + // Create bridge transfer details + let details = create_details( + initiator_address, + ethereum_address, + new_amount, nonce - ); - - // Add the transfer details to storage + ); + + let bridge_transfer_id = + bridge_transfer_id( + initiator_address, + ethereum_address, + new_amount, + nonce + ); + + // Add the transfer details to storage add(nonce, details); - // Burn the amount from the initiator - burn(initiator_address, amount); + // Burn the amount from the initiator + burn(initiator_address, amount); let bridge_events = borrow_global_mut(@aptos_framework); // Emit an event with nonce - event::emit_event( - &mut bridge_events.bridge_transfer_initiated_events, - BridgeTransferInitiatedEvent { - bridge_transfer_id, + event::emit_event( + &mut bridge_events.bridge_transfer_initiated_events, + BridgeTransferInitiatedEvent { + bridge_transfer_id, initiator: initiator_address, - recipient, + recipient, amount: new_amount, - nonce, - } - ); + nonce + } + ); } /// Completes a bridge transfer on the destination chain. - /// - /// @param caller The signer representing the bridge relayer. - /// @param initiator The initiator's Ethereum address as a vector of bytes. - /// @param bridge_transfer_id The unique identifier for the bridge transfer. - /// @param recipient The address of the recipient on the Aptos blockchain. - /// @param amount The amount of assets to be locked. - /// @param nonce The unique nonce for the transfer. - /// @abort If the caller is not the bridge relayer or the transfer has already been processed. + /// + /// @param caller The signer representing the bridge relayer. + /// @param initiator The initiator's Ethereum address as a vector of bytes. + /// @param bridge_transfer_id The unique identifier for the bridge transfer. + /// @param recipient The address of the recipient on the Aptos blockchain. + /// @param amount The amount of assets to be locked. + /// @param nonce The unique nonce for the transfer. + /// @abort If the caller is not the bridge relayer or the transfer has already been processed. public entry fun complete_bridge_transfer( caller: &signer, bridge_transfer_id: vector, @@ -457,7 +483,9 @@ module aptos_framework::native_bridge { vector::append(&mut combined_bytes, amount_bytes); vector::append(&mut combined_bytes, nonce_bytes); - assert!(keccak256(combined_bytes) == bridge_transfer_id, EINVALID_BRIDGE_TRANSFER_ID); + assert!( + keccak256(combined_bytes) == bridge_transfer_id, EINVALID_BRIDGE_TRANSFER_ID + ); // Record the transfer as completed by associating the bridge_transfer_id with the inbound nonce set_bridge_transfer_id_to_inbound_nonce(bridge_transfer_id, nonce); @@ -474,17 +502,17 @@ module aptos_framework::native_bridge { initiator, recipient, amount, - nonce, - }, + nonce + } ); } /// Charge bridge fee to the initiate bridge transfer. - /// + /// /// @param initiator The signer representing the initiator. /// @param amount The amount to be charged. /// @return The new amount after deducting the bridge fee. - fun charge_bridge_fee(amount: u64) : u64 acquires AptosCoinMintCapability, BridgeConfig { + fun charge_bridge_fee(amount: u64): u64 acquires AptosCoinMintCapability, BridgeConfig { let bridge_fee = bridge_fee(); let bridge_relayer = bridge_relayer(); assert!(amount > bridge_fee, EINVALID_AMOUNT); @@ -498,8 +526,9 @@ module aptos_framework::native_bridge { /// @param aptos_framework The signer representing the Aptos framework. /// @param new_relayer The new address to be set as the bridge relayer. /// @abort If the current relayer is the same as the new relayer. - public fun update_bridge_relayer(aptos_framework: &signer, new_relayer: address - ) acquires BridgeConfig { + public fun update_bridge_relayer( + aptos_framework: &signer, new_relayer: address + ) acquires BridgeConfig { system_addresses::assert_aptos_framework(aptos_framework); let bridge_config = borrow_global_mut(@aptos_framework); let old_relayer = bridge_config.bridge_relayer; @@ -508,20 +537,16 @@ module aptos_framework::native_bridge { bridge_config.bridge_relayer = new_relayer; event::emit( - BridgeConfigRelayerUpdated { - old_relayer, - new_relayer, - }, + BridgeConfigRelayerUpdated { old_relayer, new_relayer } ); } /// Updates the bridge fee, requiring relayer validation. - /// + /// /// @param relayer The signer representing the Relayer. /// @param new_bridge_fee The new bridge fee to be set. /// @abort If the new bridge fee is the same as the old bridge fee. - public fun update_bridge_fee(relayer: &signer, new_bridge_fee: u64 - ) acquires BridgeConfig { + public fun update_bridge_fee(relayer: &signer, new_bridge_fee: u64) acquires BridgeConfig { assert_is_caller_relayer(relayer); let bridge_config = borrow_global_mut(@aptos_framework); let old_bridge_fee = bridge_config.bridge_fee; @@ -529,10 +554,7 @@ module aptos_framework::native_bridge { bridge_config.bridge_fee = new_bridge_fee; event::emit( - BridgeFeeChangedEvent { - old_bridge_fee, - new_bridge_fee, - }, + BridgeFeeChangedEvent { old_bridge_fee, new_bridge_fee } ); } @@ -546,7 +568,7 @@ module aptos_framework::native_bridge { #[view] /// Retrieves the current bridge fee. - /// + /// /// @return The current bridge fee. public fun bridge_fee(): u64 acquires BridgeConfig { borrow_global_mut(@aptos_framework).bridge_fee @@ -556,9 +578,12 @@ module aptos_framework::native_bridge { /// /// @param caller The signer whose authority is being checked. /// @abort If the caller is not the current bridge relayer. - public(friend) fun assert_is_caller_relayer(caller: &signer - ) acquires BridgeConfig { - assert!(borrow_global(@aptos_framework).bridge_relayer == signer::address_of(caller), EINVALID_BRIDGE_RELAYER); + public(friend) fun assert_is_caller_relayer(caller: &signer) acquires BridgeConfig { + assert!( + borrow_global(@aptos_framework).bridge_relayer + == signer::address_of(caller), + EINVALID_BRIDGE_RELAYER + ); } #[test(aptos_framework = @aptos_framework)] @@ -570,26 +595,25 @@ module aptos_framework::native_bridge { #[test(aptos_framework = @aptos_framework, new_relayer = @0xcafe)] /// Tests updating the bridge relayer and emitting the corresponding event. - fun test_update_bridge_relayer(aptos_framework: &signer, new_relayer: address + fun test_update_bridge_relayer( + aptos_framework: &signer, new_relayer: address ) acquires BridgeConfig { initialize_for_test(aptos_framework); update_bridge_relayer(aptos_framework, new_relayer); assert!( event::was_event_emitted( - &BridgeConfigRelayerUpdated { - old_relayer: @aptos_framework, - new_relayer, - } - ), 0); + &BridgeConfigRelayerUpdated { old_relayer: @aptos_framework, new_relayer } + ), + 0 + ); assert!(bridge_relayer() == new_relayer, 0); } #[test(aptos_framework = @aptos_framework)] /// Tests updating the bridge relayer and emitting the corresponding event. - fun test_update_bridge_fee(aptos_framework: &signer - ) acquires BridgeConfig { + fun test_update_bridge_fee(aptos_framework: &signer) acquires BridgeConfig { let new_fee = 100; initialize_for_test(aptos_framework); let old_bridge_fee = bridge_fee(); @@ -599,9 +623,11 @@ module aptos_framework::native_bridge { event::was_event_emitted( &BridgeFeeChangedEvent { old_bridge_fee: old_bridge_fee, - new_bridge_fee: new_fee, + new_bridge_fee: new_fee } - ), 0); + ), + 0 + ); assert!(bridge_fee() == new_fee, 0); } @@ -609,7 +635,8 @@ module aptos_framework::native_bridge { #[test(aptos_framework = @aptos_framework, bad = @0xbad, new_relayer = @0xcafe)] #[expected_failure(abort_code = 0x50003, location = 0x1::system_addresses)] /// Tests that updating the bridge relayer with an invalid signer fails. - fun test_failing_update_bridge_relayer(aptos_framework: &signer, bad: &signer, new_relayer: address + fun test_failing_update_bridge_relayer( + aptos_framework: &signer, bad: &signer, new_relayer: address ) acquires BridgeConfig { initialize_for_test(aptos_framework); update_bridge_relayer(bad, new_relayer); @@ -630,11 +657,15 @@ module aptos_framework::native_bridge { assert_is_caller_relayer(bad); } - #[test(aptos_framework = @aptos_framework, relayer = @0xcafe, sender = @0x726563697069656e740000000000000000000000000000000000000000000000)] + #[ + test( + aptos_framework = @aptos_framework, + relayer = @0xcafe, + sender = @0x726563697069656e740000000000000000000000000000000000000000000000 + ) + ] fun test_initiate_bridge_transfer_happy_path( - sender: &signer, - aptos_framework: &signer, - relayer: &signer + sender: &signer, aptos_framework: &signer, relayer: &signer ) acquires BridgeEvents, Nonce, AptosCoinMintCapability, AptosCoinBurnCapability, SmartTableWrapper, BridgeConfig { let sender_address = signer::address_of(sender); let relayer_address = signer::address_of(relayer); @@ -643,7 +674,7 @@ module aptos_framework::native_bridge { let amount = 1000; let bridge_fee = 40; update_bridge_fee(aptos_framework, bridge_fee); - + // Update the bridge relayer so it can receive the bridge fee update_bridge_relayer(aptos_framework, relayer_address); let bridge_relayer = bridge_relayer(); @@ -659,26 +690,23 @@ module aptos_framework::native_bridge { // Perform the bridge transfer initiate_bridge_transfer( - sender, - recipient, - amount + sender, recipient, amount ); let bridge_events = borrow_global(@aptos_framework); - let initiated_events = event::emitted_events_by_handle( - &bridge_events.bridge_transfer_initiated_events - ); + let initiated_events = + event::emitted_events_by_handle( + &bridge_events.bridge_transfer_initiated_events + ); assert!(vector::length(&initiated_events) == 1, EEVENT_NOT_FOUND); let first_elem = vector::borrow(&initiated_events, 0); assert!(first_elem.amount == amount - bridge_fee, 0); } #[test(aptos_framework = @aptos_framework, sender = @0xdaff, relayer = @0xcafe)] - #[expected_failure(abort_code = 0x10006, location = 0x1::coin)] + #[expected_failure(abort_code = 0x10006, location = 0x1::coin)] fun test_initiate_bridge_transfer_insufficient_balance( - sender: &signer, - aptos_framework: &signer, - relayer: &signer + sender: &signer, aptos_framework: &signer, relayer: &signer ) acquires BridgeEvents, Nonce, AptosCoinBurnCapability, AptosCoinMintCapability, SmartTableWrapper, BridgeConfig { let sender_address = signer::address_of(sender); let relayer_address = signer::address_of(relayer); @@ -696,17 +724,18 @@ module aptos_framework::native_bridge { aptos_account::create_account(bridge_relayer); initiate_bridge_transfer( - sender, - recipient, - amount + sender, recipient, amount ); } #[test(aptos_framework = @aptos_framework)] - fun test_complete_bridge_transfer(aptos_framework: &signer) acquires BridgeEvents, AptosCoinMintCapability, SmartTableWrapper, BridgeConfig { + fun test_complete_bridge_transfer( + aptos_framework: &signer + ) acquires BridgeEvents, AptosCoinMintCapability, SmartTableWrapper, BridgeConfig { initialize_for_test(aptos_framework); let initiator = b"5B38Da6a701c568545dCfcB03FcB875f56beddC4"; - let recipient = @0x726563697069656e740000000000000000000000000000000000000000000000; + let recipient = + @0x726563697069656e740000000000000000000000000000000000000000000000; let amount = 100; let nonce = 1; @@ -730,8 +759,12 @@ module aptos_framework::native_bridge { nonce ); - let bridge_events = borrow_global(signer::address_of(aptos_framework)); - let complete_events = event::emitted_events_by_handle(&bridge_events.bridge_transfer_completed_events); + let bridge_events = + borrow_global(signer::address_of(aptos_framework)); + let complete_events = + event::emitted_events_by_handle( + &bridge_events.bridge_transfer_completed_events + ); // Assert that the event was emitted let expected_event = BridgeTransferCompletedEvent { @@ -739,17 +772,16 @@ module aptos_framework::native_bridge { initiator, recipient, amount, - nonce, + nonce }; assert!(std::vector::contains(&complete_events, &expected_event), 0); assert!(bridge_transfer_id == expected_event.bridge_transfer_id, 0) } #[test(aptos_framework = @aptos_framework, sender = @0xdaff)] - #[expected_failure(abort_code = 11, location = Self)] + #[expected_failure(abort_code = 11, location = Self)] fun test_complete_bridge_transfer_by_non_relayer( - sender: &signer, - aptos_framework: &signer + sender: &signer, aptos_framework: &signer ) acquires BridgeEvents, AptosCoinMintCapability, SmartTableWrapper, BridgeConfig { let sender_address = signer::address_of(sender); // Create an account for our recipient @@ -770,10 +802,10 @@ module aptos_framework::native_bridge { } #[test(aptos_framework = @aptos_framework, sender = @0xdaff)] - #[expected_failure(abort_code = EINVALID_BRIDGE_TRANSFER_ID, location = Self)] // ENOT_FOUND + #[expected_failure(abort_code = EINVALID_BRIDGE_TRANSFER_ID, location = Self)] + // ENOT_FOUND fun test_complete_bridge_with_erroneous_bridge_id_by_relayer( - sender: &signer, - aptos_framework: &signer + sender: &signer, aptos_framework: &signer ) acquires BridgeEvents, AptosCoinMintCapability, SmartTableWrapper, BridgeConfig { let sender_address = signer::address_of(sender); // Create an account for our recipient @@ -796,16 +828,31 @@ module aptos_framework::native_bridge { #[test] /// Test normalisation (serialization) of u64 to 32 bytes fun test_normalize_u64_to_32_bytes() { - test_normalize_u64_to_32_bytes_helper(0x64, - vector[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0x64]); - test_normalize_u64_to_32_bytes_helper(0x6400, - vector[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0x64,0x00]); - test_normalize_u64_to_32_bytes_helper(0x00_32_00_00_64_00, - vector[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0x32,0,0,0x64,0x00]); + test_normalize_u64_to_32_bytes_helper( + 0x64, + vector[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0x64] + ); + test_normalize_u64_to_32_bytes_helper( + 0x6400, + vector[ + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0x64, 0x00 + ] + ); + test_normalize_u64_to_32_bytes_helper( + 0x00_32_00_00_64_00, + vector[ + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0x32, 0, 0, 0x64, 0x00 + ] + ); } /// Test serialization of u64 to 32 bytes - fun test_normalize_u64_to_32_bytes_helper(x: u64, expected: vector) { + fun test_normalize_u64_to_32_bytes_helper( + x: u64, expected: vector + ) { let r = normalize_u64_to_32_bytes(&x); assert!(vector::length(&r) == 32, 0); assert!(r == expected, 0); diff --git a/aptos-move/framework/aptos-framework/sources/native_bridge.spec.move b/aptos-move/framework/aptos-framework/sources/native_bridge.spec.move index 58660affaae3b..c5568808aab9d 100644 --- a/aptos-move/framework/aptos-framework/sources/native_bridge.spec.move +++ b/aptos-move/framework/aptos-framework/sources/native_bridge.spec.move @@ -2,11 +2,11 @@ spec aptos_framework::native_bridge { spec module { - axiom forall x: u64: len(bcs::to_bytes(x)) == 8; - axiom forall x: u256: len(bcs::to_bytes(x)) == 32; + axiom forall x: u64: len(bcs::to_bytes(x)) == 8; + axiom forall x: u256: len(bcs::to_bytes(x)) == 32; } - // req1. never aborts + // req1. never aborts // req2. returns a 32-byte vector spec normalize_u64_to_32_bytes { aborts_if false; @@ -15,9 +15,10 @@ spec aptos_framework::native_bridge { // If the resource exists it cannot be removed invariant update exists(@aptos_framework); - // Eevry time the Nonce is updated, the value is incremented by 1 + + // Every time the Nonce is updated, the value is incremented by 1 // invariant update [global] exists(@aptos_framework) ==> - // global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; + // global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; invariant global(@aptos_framework).value >= 0; // spec module { @@ -40,7 +41,8 @@ spec aptos_framework::native_bridge { // // req 3: ensures the result is the old value of the Nonce resource + 1 ensures result == old(global(@aptos_framework).value) + 1; - ensures global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; + ensures global(@aptos_framework).value + == old(global(@aptos_framework).value) + 1; // ensures false; } @@ -69,51 +71,51 @@ spec aptos_framework::native_bridge { // .bridge_transfer_completed_events.counter == 0; } -// // spec increment_and_get_nonce { -// // aborts_if !exists(@aptos_framework); - -// // ensures global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; -// // ensures result == global(@aptos_framework).value; -// // } - -// // spec initiate_bridge_transfer( -// // initiator: &signer, -// // recipient: vector, -// // amount: u64 -// // ) { -// // aborts_if amount == 0; -// // aborts_if !exists(@aptos_framework); -// // aborts_if !exists(@aptos_framework); - -// // ensures global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; - -// // ensures -// // global(@aptos_framework).bridge_transfer_initiated_events.counter == -// // old( -// // global(@aptos_framework).bridge_transfer_initiated_events.counter -// // ) + 1; -// // } - -// // spec complete_bridge_transfer( -// // caller: &signer, -// // bridge_transfer_id: vector, -// // initiator: vector, -// // recipient: address, -// // amount: u64, -// // nonce: u64 -// // ) { -// // // Abort if the caller is not a relayer -// // aborts_if !exists(@aptos_framework); -// // aborts_if global(@aptos_framework).bridge_relayer != signer::address_of(caller); - -// // // Abort if the bridge transfer ID is already associated with an incoming nonce -// // aborts_if native_bridge_store::is_incoming_nonce_set(bridge_transfer_id); - -// // // Abort if the `BridgeEvents` resource does not exist -// // aborts_if !exists(@aptos_framework); - -// // // Ensure the bridge transfer ID is associated with an incoming nonce after execution -// // ensures native_bridge_store::is_incoming_nonce_set(bridge_transfer_id); + // // spec increment_and_get_nonce { + // // aborts_if !exists(@aptos_framework); + + // // ensures global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; + // // ensures result == global(@aptos_framework).value; + // // } + + // // spec initiate_bridge_transfer( + // // initiator: &signer, + // // recipient: vector, + // // amount: u64 + // // ) { + // // aborts_if amount == 0; + // // aborts_if !exists(@aptos_framework); + // // aborts_if !exists(@aptos_framework); + + // // ensures global(@aptos_framework).value == old(global(@aptos_framework).value) + 1; + + // // ensures + // // global(@aptos_framework).bridge_transfer_initiated_events.counter == + // // old( + // // global(@aptos_framework).bridge_transfer_initiated_events.counter + // // ) + 1; + // // } + + // // spec complete_bridge_transfer( + // // caller: &signer, + // // bridge_transfer_id: vector, + // // initiator: vector, + // // recipient: address, + // // amount: u64, + // // nonce: u64 + // // ) { + // // // Abort if the caller is not a relayer + // // aborts_if !exists(@aptos_framework); + // // aborts_if global(@aptos_framework).bridge_relayer != signer::address_of(caller); + + // // // Abort if the bridge transfer ID is already associated with an incoming nonce + // // aborts_if native_bridge_store::is_incoming_nonce_set(bridge_transfer_id); + + // // // Abort if the `BridgeEvents` resource does not exist + // // aborts_if !exists(@aptos_framework); + + // // // Ensure the bridge transfer ID is associated with an incoming nonce after execution + // // ensures native_bridge_store::is_incoming_nonce_set(bridge_transfer_id); // // Ensure the event counter is incremented by 1 // ensures @@ -126,136 +128,135 @@ spec aptos_framework::native_bridge { // spec aptos_framework::native_bridge_core { - // spec initialize(aptos_framework: &signer) { - // pragma aborts_if_is_partial = true; +// spec initialize(aptos_framework: &signer) { +// pragma aborts_if_is_partial = true; - // aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); - // aborts_if exists(@aptos_framework); - // aborts_if exists(@aptos_framework); +// aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); +// aborts_if exists(@aptos_framework); +// aborts_if exists(@aptos_framework); - // ensures exists(@aptos_framework); - // ensures exists(@aptos_framework); - // } - // spec store_aptos_coin_burn_cap(aptos_framework: &signer, burn_cap: BurnCapability) { - // aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); - // aborts_if exists(@aptos_framework); +// ensures exists(@aptos_framework); +// ensures exists(@aptos_framework); +// } +// spec store_aptos_coin_burn_cap(aptos_framework: &signer, burn_cap: BurnCapability) { +// aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); +// aborts_if exists(@aptos_framework); - // ensures exists(@aptos_framework); - // } +// ensures exists(@aptos_framework); +// } - // spec store_aptos_coin_mint_cap(aptos_framework: &signer, mint_cap: MintCapability) { - // aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); - // aborts_if exists(@aptos_framework); +// spec store_aptos_coin_mint_cap(aptos_framework: &signer, mint_cap: MintCapability) { +// aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); +// aborts_if exists(@aptos_framework); - // ensures exists(@aptos_framework); - // } +// ensures exists(@aptos_framework); +// } - // spec mint(recipient: address, amount: u64) { - // aborts_if !exists(@aptos_framework); - // aborts_if amount == 0; +// spec mint(recipient: address, amount: u64) { +// aborts_if !exists(@aptos_framework); +// aborts_if amount == 0; - // ensures coin::balance(recipient) == old(coin::balance(recipient)) + amount; - // } +// ensures coin::balance(recipient) == old(coin::balance(recipient)) + amount; +// } - // spec burn(from: address, amount: u64) { - // aborts_if !exists(@aptos_framework); - // aborts_if coin::balance(from) < amount; +// spec burn(from: address, amount: u64) { +// aborts_if !exists(@aptos_framework); +// aborts_if coin::balance(from) < amount; - // ensures coin::balance(from) == old(coin::balance(from)) - amount; - // } +// ensures coin::balance(from) == old(coin::balance(from)) - amount; +// } // } // spec aptos_framework::native_bridge_store { - - // spec bcs_u64 { - // aborts_if false; - // ensures len(result) == 8; - // } +// spec bcs_u64 { +// aborts_if false; +// ensures len(result) == 8; +// } - // spec ascii_hex_to_u8 { - // requires ch >= 0x30 && ch <= 0x39 || ch >= 0x41 && ch <= 0x46 || ch >= 0x61 && ch <= 0x66; - // } +// spec ascii_hex_to_u8 { +// requires ch >= 0x30 && ch <= 0x39 || ch >= 0x41 && ch <= 0x46 || ch >= 0x61 && ch <= 0x66; +// } - // spec initialize(aptos_framework: &signer) { - // aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); +// spec initialize(aptos_framework: &signer) { +// aborts_if !system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework)); - // ensures exists>(@aptos_framework); - // ensures exists, u64>>(@aptos_framework); - // } +// ensures exists>(@aptos_framework); +// ensures exists, u64>>(@aptos_framework); +// } - // spec is_incoming_nonce_set(bridge_transfer_id: vector): bool { - // ensures result == exists, u64>>(@aptos_framework) - // && smart_table::spec_contains( - // global, u64>>(@aptos_framework).inner, - // bridge_transfer_id - // ); - // } +// spec is_incoming_nonce_set(bridge_transfer_id: vector): bool { +// ensures result == exists, u64>>(@aptos_framework) +// && smart_table::spec_contains( +// global, u64>>(@aptos_framework).inner, +// bridge_transfer_id +// ); +// } - // spec create_details( - // initiator: address, - // recipient: EthereumAddress, - // amount: u64, - // nonce: u64 - // ): OutboundTransfer { - // aborts_if amount == 0; - - // ensures result.bridge_transfer_id == bridge_transfer_id( - // initiator, - // recipient, - // amount, - // nonce - // ); - // ensures result.initiator == initiator; - // ensures result.recipient == recipient; - // ensures result.amount == amount; - // } +// spec create_details( +// initiator: address, +// recipient: EthereumAddress, +// amount: u64, +// nonce: u64 +// ): OutboundTransfer { +// aborts_if amount == 0; + +// ensures result.bridge_transfer_id == bridge_transfer_id( +// initiator, +// recipient, +// amount, +// nonce +// ); +// ensures result.initiator == initiator; +// ensures result.recipient == recipient; +// ensures result.amount == amount; +// } - // spec add(nonce: u64, details: OutboundTransfer) { - // aborts_if !exists>(@aptos_framework); - // aborts_if smart_table::spec_contains( - // global>(@aptos_framework).inner, - // nonce - // ); - - // ensures smart_table::spec_contains( - // global>(@aptos_framework).inner, - // nonce - // ); - // ensures smart_table::spec_len( - // global>(@aptos_framework).inner - // ) == old(smart_table::spec_len( - // global>(@aptos_framework).inner - // )) + 1; - // } +// spec add(nonce: u64, details: OutboundTransfer) { +// aborts_if !exists>(@aptos_framework); +// aborts_if smart_table::spec_contains( +// global>(@aptos_framework).inner, +// nonce +// ); + +// ensures smart_table::spec_contains( +// global>(@aptos_framework).inner, +// nonce +// ); +// ensures smart_table::spec_len( +// global>(@aptos_framework).inner +// ) == old(smart_table::spec_len( +// global>(@aptos_framework).inner +// )) + 1; +// } - // spec set_bridge_transfer_id_to_inbound_nonce( - // bridge_transfer_id: vector, - // inbound_nonce: u64 - // ) { - // aborts_if !exists, u64>>(@aptos_framework); +// spec set_bridge_transfer_id_to_inbound_nonce( +// bridge_transfer_id: vector, +// inbound_nonce: u64 +// ) { +// aborts_if !exists, u64>>(@aptos_framework); - // ensures smart_table::spec_contains( - // global, u64>>(@aptos_framework).inner, - // bridge_transfer_id - // ); - // } - /* - spec bridge_transfer_id( - initiator: address, - recipient: EthereumAddress, - amount: u64, - nonce: u64 - ): vector { - let combined_bytes = vec_empty(); - combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&initiator)); - combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&recipient)); - combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&amount)); - combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&nonce)); - - ensures result == aptos_std::aptos_hash::keccak256(combined_bytes); - } - */ +// ensures smart_table::spec_contains( +// global, u64>>(@aptos_framework).inner, +// bridge_transfer_id +// ); +// } +/* +spec bridge_transfer_id( + initiator: address, + recipient: EthereumAddress, + amount: u64, + nonce: u64 +): vector { + let combined_bytes = vec_empty(); + combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&initiator)); + combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&recipient)); + combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&amount)); + combined_bytes = vector::append(combined_bytes, bcs::to_bytes(&nonce)); + + ensures result == aptos_std::aptos_hash::keccak256(combined_bytes); +} +*/ // } // spec aptos_framework::native_bridge_configuration { @@ -302,18 +303,17 @@ spec aptos_framework::native_bridge { // spec aptos_framework::native_bridge_store { // spec module { -// axiom forall x: u64: len(bcs::to_bytes(x)) == 8; -// axiom forall x: u256: len(bcs::to_bytes(x)) == 32; +// axiom forall x: u64: len(bcs::to_bytes(x)) == 8; +// axiom forall x: u256: len(bcs::to_bytes(x)) == 32; // } -// // req1. never aborts +// // req1. never aborts // // req2. returns a 32-byte vector // spec normalize_u64_to_32_bytes { // aborts_if false; // ensures len(result) == 32; // } - // // spec bcs_u64 { // // aborts_if false; // // ensures len(result) == 8;