chore: opinionated improvements to #2528

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]

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

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<u64> {
     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(())
 }