diff --git a/crates/miden-agglayer/asm/agglayer/bridge/bridge_in.masm b/crates/miden-agglayer/asm/agglayer/bridge/bridge_in.masm index 182c345a46..d56f85e31e 100644 --- a/crates/miden-agglayer/asm/agglayer/bridge/bridge_in.masm +++ b/crates/miden-agglayer/asm/agglayer/bridge/bridge_in.masm @@ -79,10 +79,6 @@ const CLAIM_OUTPUT_NOTE_FAUCET_AMOUNT = 568 const CLAIM_PROOF_DATA_KEY_MEM_ADDR = 700 const CLAIM_LEAF_DATA_KEY_MEM_ADDR = 704 -# Memory addresses for the faucet ID looked up during claim (used by claim procedure) -const CLAIM_FAUCET_ID_PREFIX_MEM_ADDR = 708 -const CLAIM_FAUCET_ID_SUFFIX_MEM_ADDR = 709 - # Memory addresses for leaf data fields (derived from leaf data layout at CLAIM_LEAF_DATA_START_PTR=536) const ORIGIN_TOKEN_ADDRESS_0 = 538 const ORIGIN_TOKEN_ADDRESS_1 = 539 @@ -330,26 +326,23 @@ pub proc claim exec.verify_leaf_bridge # => [pad(16)] - # Look up the faucet account ID from the origin token address once, - # and store it in global memory for use by verify_claim_amount and - # create_mint_note_with_attachment. + # Look up the faucet account ID from the origin token address exec.get_origin_token_address # => [origin_token_addr(5), pad(16)] exec.bridge_config::lookup_faucet_by_token_address # => [faucet_id_prefix, faucet_id_suffix, pad(16)] - mem_store.CLAIM_FAUCET_ID_PREFIX_MEM_ADDR - mem_store.CLAIM_FAUCET_ID_SUFFIX_MEM_ADDR - # => [pad(16)] + dup.1 dup.1 + # => [faucet_id_prefix, faucet_id_suffix, faucet_id_prefix, faucet_id_suffix, pad(16)] # Verify faucet_mint_amount matches the leaf data amount exec.verify_claim_amount - # => [pad(16)] + # => [faucet_id_prefix, faucet_id_suffix, pad(16)] # Build MINT output note targeting the aggfaucet loc_load.CLAIM_DEST_ID_SUFFIX_LOCAL loc_load.CLAIM_DEST_ID_PREFIX_LOCAL - # => [destination_id_prefix, destination_id_suffix, pad(16)] + # => [destination_id_prefix, destination_id_suffix, faucet_id_prefix, faucet_id_suffix, pad(16)] exec.build_mint_output_note # => [pad(16)] @@ -362,13 +355,12 @@ end #! scaled down by the faucet's scale factor. #! #! This procedure: -#! 1. Reads the faucet account ID from global memory (looked up once in `claim`). -#! 2. Performs an FPI call to the faucet's `get_scale` procedure to retrieve the scale factor. -#! 3. Loads the raw U256 amount from the leaf data in memory. -#! 4. Calls `verify_u256_to_native_amount_conversion` to assert that: +#! 1. Performs an FPI call to the faucet's `get_scale` procedure to retrieve the scale factor. +#! 2. Loads the raw U256 amount from the leaf data in memory. +#! 3. Calls `verify_u256_to_native_amount_conversion` to assert that: #! faucet_mint_amount == floor(raw_amount / 10^scale) #! -#! Inputs: [] +#! Inputs: [faucet_id_prefix, faucet_id_suffix] #! Outputs: [] #! #! Panics if: @@ -378,15 +370,13 @@ end #! Invocation: exec proc verify_claim_amount # Step 1: Pad the stack explicitly for FPI call (get_scale takes no inputs) - padw padw padw padw - # => [pad(16)] - - # Step 2: Load the faucet account ID from global memory - mem_load.CLAIM_FAUCET_ID_SUFFIX_MEM_ADDR - mem_load.CLAIM_FAUCET_ID_PREFIX_MEM_ADDR + padw padw + movup.9 movup.9 + padw padw + movup.9 movup.9 # => [faucet_id_prefix, faucet_id_suffix, pad(16)] - # Step 3: FPI call to faucet's get_scale procedure + # Step 2: FPI call to faucet's get_scale procedure procref.agglayer_faucet::get_scale # => [PROC_MAST_ROOT(4), faucet_id_prefix, faucet_id_suffix, pad(16)] @@ -400,22 +390,19 @@ proc verify_claim_amount movdn.15 dropw dropw dropw drop drop drop # => [scale] - # Step 4: Load the raw U256 amount from leaf data memory + # Step 3: Load the raw U256 amount from leaf data memory exec.get_raw_claim_amount # => [x7, x6, x5, x4, x3, x2, x1, x0, scale] - # Step 5: Load faucet_mint_amount (y) and position it for verification + # Step 4: Load faucet_mint_amount (y) and position it for verification mem_load.CLAIM_OUTPUT_NOTE_FAUCET_AMOUNT # => [y, x7, x6, x5, x4, x3, x2, x1, x0, scale] movdn.9 # => [x7, x6, x5, x4, x3, x2, x1, x0, scale, y] - # Step 6: Verify that y = floor(x / 10^scale) + # Step 5: Verify that y = floor(x / 10^scale) exec.asset_conversion::verify_u256_to_native_amount_conversion - # => [y] - - drop # => [] end @@ -588,20 +575,20 @@ end #! a PUBLIC P2ID note on consumption. This procedure orchestrates three steps: #! 1. Write all 18 MINT note storage items to global memory. #! 2. Build the MINT note recipient digest from the storage. -#! 3. Look up the faucet, create the output note, and set the attachment. +#! 3. Create the output note, and set the attachment. #! -#! Inputs: [destination_id_prefix, destination_id_suffix] +#! Inputs: [destination_id_prefix, destination_id_suffix, faucet_id_prefix, faucet_id_suffix] #! Outputs: [] #! #! Invocation: exec proc build_mint_output_note # Step 1: Write all 18 MINT note storage items to global memory exec.write_mint_note_storage - # => [] + # => [faucet_id_prefix, faucet_id_suffix] # Step 2: Build the MINT note recipient digest exec.build_mint_recipient - # => [MINT_RECIPIENT] + # => [MINT_RECIPIENT, faucet_id_prefix, faucet_id_suffix] # Step 3: Create the output note and set the faucet attachment exec.create_mint_note_with_attachment @@ -716,39 +703,38 @@ end #! Creates the MINT output note and sets the NetworkAccountTarget attachment on it. #! -#! Reads the faucet account ID from global memory (looked up once in `claim`), -#! creates a public output note with no assets, and sets the attachment so only the +#! Creates a public output note with no assets, and sets the attachment so only the #! target faucet can consume the note. #! -#! Inputs: [MINT_RECIPIENT] +#! Inputs: [MINT_RECIPIENT, faucet_id_prefix, faucet_id_suffix] #! Outputs: [] #! #! Invocation: exec proc create_mint_note_with_attachment # Create the MINT output note targeting the faucet push.OUTPUT_NOTE_TYPE_PUBLIC - # => [note_type, MINT_RECIPIENT] + # => [note_type, MINT_RECIPIENT, faucet_id_prefix, faucet_id_suffix] - # Load the faucet account ID from global memory (looked up once in `claim`) - mem_load.CLAIM_FAUCET_ID_PREFIX_MEM_ADDR - # => [faucet_id_prefix, note_type, MINT_RECIPIENT] + dup.5 + # => [faucet_id_prefix, note_type, MINT_RECIPIENT, faucet_id_prefix, faucet_id_suffix] # Compute note tag targeting the faucet account exec.note_tag::create_account_target - # => [faucet_tag, note_type, MINT_RECIPIENT] + # => [faucet_tag, note_type, MINT_RECIPIENT, faucet_id_prefix, faucet_id_suffix] # Create the output note (no assets - MINT notes carry no assets) exec.output_note::create - # => [note_idx] + # => [note_idx, faucet_id_prefix, faucet_id_suffix] + movdn.2 + # => [faucet_id_prefix, faucet_id_suffix, note_idx] # Set the attachment on the MINT note to target the faucet account # NetworkAccountTarget attachment: targets the faucet so only it can consume the note # network_account_target::new expects [prefix, suffix, exec_hint] # and returns [attachment_scheme, attachment_kind, ATTACHMENT] push.ALWAYS # exec_hint = ALWAYS - mem_load.CLAIM_FAUCET_ID_SUFFIX_MEM_ADDR - mem_load.CLAIM_FAUCET_ID_PREFIX_MEM_ADDR - # => [faucet_prefix, faucet_suffix, exec_hint, note_idx] + movdn.2 + # => [faucet_id_prefix, faucet_id_suffix, exec_hint, note_idx] exec.network_account_target::new # => [attachment_scheme, attachment_kind, ATTACHMENT, note_idx] diff --git a/crates/miden-agglayer/asm/agglayer/common/asset_conversion.masm b/crates/miden-agglayer/asm/agglayer/common/asset_conversion.masm index bc455ab001..77bfa65cc6 100644 --- a/crates/miden-agglayer/asm/agglayer/common/asset_conversion.masm +++ b/crates/miden-agglayer/asm/agglayer/common/asset_conversion.masm @@ -231,7 +231,7 @@ end #! Inputs: [x0, x1, x2, x3, scale_exp, y] #! Where x is encoded as 4 u32 limbs in little-endian order. #! (x0 is least significant limb) -#! Outputs: [y] +#! Outputs: [] #! #! Where: #! - x: The original amount as an unsigned 128-bit integer (U128). @@ -275,30 +275,28 @@ pub proc verify_u128_to_native_amount_conversion movup.5 # => [y, scale_exp, x0, x1, x2, x3] - dup.1 dup.1 - # => [y, scale_exp, y, scale_exp, x0, x1, x2, x3] + # Duplicate scale_exp (needed later for remainder bound check in Step 4) + dup.1 swap + # => [y, scale_exp, scale_exp, x0, x1, x2, x3] exec.scale_native_amount_to_u256 - # => [y_scaled0..y_scaled7, y, scale_exp, x0, x1, x2, x3] + # => [y_scaled0..y_scaled7, scale_exp, x0, x1, x2, x3] # Drop the upper word as it's guaranteed to be zero since y_scaled will fit in 123 bits # (amount: 63 bits, 10^target_scale: 60 bits). swapw dropw - # => [y_scaled0, y_scaled1, y_scaled2, y_scaled3, y, scale_exp, x0, x1, x2, x3] + # => [y_scaled0, y_scaled1, y_scaled2, y_scaled3, scale_exp, x0, x1, x2, x3] # ============================================================================================= # Step 3: Compute z = x - y_scaled and prove no underflow # z := x - y_scaled # Constraint: y_scaled <= x # ============================================================================================= - movup.5 movup.5 - # => [y, scale_exp, y_scaled0, y_scaled1, y_scaled2, y_scaled3, x0, x1, x2, x3] - - movdn.9 movdn.9 - # => [y_scaled0, y_scaled1, y_scaled2, y_scaled3, x0, x1, x2, x3, y, scale_exp] + movup.4 movdn.8 + # => [y_scaled0, y_scaled1, y_scaled2, y_scaled3, x0, x1, x2, x3, scale_exp] exec.u128_sub_no_underflow - # => [z0, z1, z2, z3, y, scale_exp] + # => [z0, z1, z2, z3, scale_exp] # ============================================================================================= # Step 4: Enforce z < 10^scale_exp (remainder bound) @@ -310,24 +308,24 @@ pub proc verify_u128_to_native_amount_conversion # Therefore any valid remainder z < 10^scale_exp must be < 2^60 and thus must have z2 == z3 == 0. # ============================================================================================= exec.word::reverse - # => [z3, z2, z1, z0, y, scale_exp] + # => [z3, z2, z1, z0, scale_exp] assertz.err=ERR_REMAINDER_TOO_LARGE # z3 == 0 assertz.err=ERR_REMAINDER_TOO_LARGE # z2 == 0 - # => [z1, z0, y, scale_exp] + # => [z1, z0, scale_exp] - movup.3 + movup.2 exec.pow10 - # => [scale, z1, z0, y] + # => [scale, z1, z0] u32split - # => [scale_hi, scale_lo, z1, z0, y] + # => [scale_hi, scale_lo, z1, z0] exec.u64::lt - # => [is_lt, y] + # => [is_lt] assert.err=ERR_REMAINDER_TOO_LARGE - # => [y] + # => [] end #! Verify conversion from an AggLayer U256 amount to a Miden native amount (Felt) @@ -355,7 +353,7 @@ end #! Where x is encoded as 8 u32 limbs in big-endian order. #! (x7 is most significant limb and is at the top of the stack) #! Each limb is expected to contain little-endian bytes. -#! Outputs: [y] +#! Outputs: [] #! #! Where: #! - x: The original AggLayer amount as an unsigned 256-bit integer (U256). @@ -387,5 +385,5 @@ pub proc verify_u256_to_native_amount_conversion # Delegate to verify_u128_to_native_amount_conversion for the remaining verification exec.verify_u128_to_native_amount_conversion - # => [y] + # => [] end diff --git a/crates/miden-testing/tests/agglayer/asset_conversion.rs b/crates/miden-testing/tests/agglayer/asset_conversion.rs index 868c3257de..b577ac2d2f 100644 --- a/crates/miden-testing/tests/agglayer/asset_conversion.rs +++ b/crates/miden-testing/tests/agglayer/asset_conversion.rs @@ -149,8 +149,11 @@ fn build_scale_down_script(x: EthAmount, scale_exp: u32, y: u64) -> String { async fn assert_scale_down_ok(x: EthAmount, scale: u32) -> anyhow::Result { let y = x.scale_to_token_amount(scale).unwrap().as_int(); let script = build_scale_down_script(x, scale, y); - let out = execute_masm_script(&script).await?; - assert_eq!(out.stack[0].as_int(), y); + let output = execute_masm_script(&script).await?; + assert!( + output.stack.is_empty(), + "verify_u256_to_native_amount_conversion should leave an empty stack after truncate_stack" + ); Ok(y) } @@ -317,19 +320,19 @@ async fn test_verify_scale_down_inline() -> anyhow::Result<()> { use miden::agglayer::common::asset_conversion begin - # Push y (expected quotient) + # Push expected quotient y used for verification (not returned as an output) push.{} # Push scale_exp push.{} - # Push x as 8 u32 limbs (little-endian, x0 at top) + # Push x as 8 u32 limbs in the order expected by the verifier push.{}.{}.{}.{}.{}.{}.{}.{} - # Call the scale down procedure + # Call the scale down procedure (verifies conversion and may panic on failure) exec.asset_conversion::verify_u256_to_native_amount_conversion - # Truncate stack to just return y + # Truncate stack so the program returns with no public outputs (Outputs: []) exec.sys::truncate_stack end "#, @@ -345,12 +348,9 @@ async fn test_verify_scale_down_inline() -> anyhow::Result<()> { x_felts[0].as_int(), ); - // Execute the script - let exec_output = execute_masm_script(&script_code).await?; - - // Verify the result - let result = exec_output.stack[0].as_int(); - assert_eq!(result, y); + // Execute the script - verify_u256_to_native_amount_conversion panics on invalid + // conversions, so successful execution is sufficient validation + execute_masm_script(&script_code).await?; Ok(()) }