feat: add u256 -> Felt scale down procedure

crates/miden-agglayer/Cargo.toml

@@ -27,6 +27,9 @@ miden-protocol   = { workspace = true }
 miden-standards  = { workspace = true }
 miden-utils-sync = { workspace = true }
 
+# External dependencies
+primitive-types = { workspace = true }
+
 [dev-dependencies]
 miden-agglayer = { features = ["testing"], path = "." }
 

crates/miden-agglayer/asm/bridge/agglayer_faucet.masm

@@ -1,11 +1,13 @@
 use miden::agglayer::bridge_in
 use miden::agglayer::asset_conversion
+use miden::agglayer::eth_address
 use miden::protocol::active_account
 use miden::protocol::active_note
 use miden::standards::faucets
 use miden::protocol::note
 use miden::protocol::tx
 use miden::core::mem
+use miden::core::word
 
 
 # CONSTANTS
@@ -34,6 +36,12 @@ const OUTPUT_NOTE_SERIAL_NUM_MEM_ADDR = 568
 const OUTPUT_NOTE_ASSET_AMOUNT_MEM_ADDR_0 = 548
 const OUTPUT_NOTE_ASSET_AMOUNT_MEM_ADDR_1 = 552
 
+const DESTINATION_ADDRESS_4 = 547
+const DESTINATION_ADDRESS_3 = 546
+const DESTINATION_ADDRESS_2 = 545
+const DESTINATION_ADDRESS_1 = 544
+const DESTINATION_ADDRESS_0 = 543
+
 # P2ID output note constants
 const P2ID_SCRIPT_ROOT = [13362761878458161062, 15090726097241769395, 444910447169617901, 3558201871398422326]
 const P2ID_NOTE_NUM_INPUTS = 2
@@ -128,6 +136,27 @@ proc batch_pipe_double_words
     exec.mem::pipe_double_words_preimage_to_memory drop
 end
 
+#! Extracts the destination account ID as address[5] from memory.
+#!
+#! This procedure reads the destination address from the leaf data and converts it from
+#! Ethereum address format to AccountId format (prefix, suffix).
+#!
+#! Inputs:  []
+#! Outputs: [prefix, suffix]
+#!
+#! Invocation: exec
+proc get_destination_account_id_data
+    mem_load.DESTINATION_ADDRESS_4
+    mem_load.DESTINATION_ADDRESS_3
+    mem_load.DESTINATION_ADDRESS_2
+    mem_load.DESTINATION_ADDRESS_1
+    mem_load.DESTINATION_ADDRESS_0
+    # => [address[5]]
+
+    exec.eth_address::to_account_id
+    # => [prefix, suffix]
+end
+
 #! Builds a P2ID output note for the claim recipient.
 #!
 #! This procedure expects the claim data to be already written to memory via batch_pipe_double_words.
@@ -139,6 +168,12 @@ end
 #!
 #! Note: This procedure will be refactored in a follow-up to use leaf data to build the output note.
 proc build_p2id_output_note
+    exec.get_destination_account_id_data
+    # => [prefix, suffix]
+
+    mem_store.1 mem_store.0
+    # => []
+
     # Build P2ID output note
     push.P2ID_SCRIPT_ROOT[0..4]
     # => [SCRIPT_ROOT]
@@ -149,12 +184,6 @@ proc build_p2id_output_note
     push.P2ID_NOTE_NUM_INPUTS
     # => [num_output_note_inputs, SERIAL_NUM, SCRIPT_ROOT]
 
-    exec.get_destination_account_id
-    # => [account_id_prefix, account_id_suffix, num_output_note_inputs, SERIAL_NUM, SCRIPT_ROOT]
-
-    mem_store.0 mem_store.1
-    # => [num_output_note_inputs, SERIAL_NUM, SCRIPT_ROOT]
-
     push.OUTPUT_NOTE_INPUTS_MEM_ADDR
     # => [inputs_ptr = 0, num_output_note_inputs, SERIAL_NUM, SCRIPT_ROOT]
 
@@ -171,7 +200,7 @@ proc build_p2id_output_note
     # => [AMOUNT[1], AMOUNT[0], tag, note_type, RECIPIENT]
 
     # TODO: implement scale down logic; stubbed out for now
-    exec.asset_conversion::scale_u256_to_native_amount
+    exec.asset_conversion::scale_u256_to_native_amount_stubbed
     # => [amount, tag, note_type, RECIPIENT]
 
     exec.faucets::distribute

crates/miden-agglayer/asm/bridge/asset_conversion.masm

@@ -6,9 +6,13 @@ use miden::core::word
 
 const MAX_SCALING_FACTOR=18
 
-# ERRORS
+# ERRORS
 # =================================================================================================
+
 const ERR_SCALE_AMOUNT_EXCEEDED_LIMIT="maximum scaling factor is 18"
+const ERR_X_TOO_LARGE="x must fit into 128 bits (x4..x7 must be 0)"
+const ERR_UNDERFLOW="x < y*10^s (underflow detected)"
+const ERR_REMAINDER_TOO_LARGE="remainder z must be < 10^s"
 
 #! Calculate 10^scale where scale is a u8 exponent.
 #!
@@ -105,10 +109,104 @@ pub proc scale_native_amount_to_u256
     # => [RESULT_U256[0], RESULT_U256[1]]
 end
 
-#! TODO: implement scaling down
-#! 
-#! Inputs: [U256[0], U256[1]]
-#! Outputs: [amount]
+#! Scale a U256 EVM amount down to a Miden amount (Felt) by dividing by 10^scale_exp.
+#!
+#! Prover provides y = floor(x / 10^s) via advice stack.
+#! Verifier proves correctness by checking:
+#!   prod = y * 10^s
+#!   z = x - prod  (no underflow)
+#!   z < 10^s
+#!
+#! NOTE: This verifier currently enforces x < 2^128 (x4..x7 == 0) to keep the proof cheap.
+#!
+#! Inputs:  [x0, x1, x2, x3, x4, x5, x6, x7, scale_exp]
+#!          (x0 is least-significant limb; x0 is on top of the stack)
+#! AS:      [y]
+#! Outputs: [y]
 pub proc scale_u256_to_native_amount
-    repeat.7 drop end
+    # --- enforce x < 2^128 (x4..x7 == 0) ---
+    dup.4 eq.0 assert.err=ERR_X_TOO_LARGE
+    dup.5 eq.0 assert.err=ERR_X_TOO_LARGE
+    dup.6 eq.0 assert.err=ERR_X_TOO_LARGE
+    dup.7 eq.0 assert.err=ERR_X_TOO_LARGE
+
+    # drop x4..x7
+    swapw dropw
+    # => [x0, x1, x2, x3, scale_exp]
+
+    # make pairs: (x3,x2) and (x1,x0)
+    exec.word::reverse
+    # => [x3, x2, x1, x0, scale_exp]
+
+    # scale = 10^scale_exp (keep a copy for z<scale check)
+    movup.4
+    exec.pow10
+    # => [scale, x3, x2, x1, x0]
+
+    dup
+    # => [scale_mul, scale_cmp, x3, x2, x1, x0]
+
+    # y from advice; duplicate so we can return it
+    adv_push.1
+    dup
+    # => [y_mul, y_ret, scale_mul, scale_cmp, x3, x2, x1, x0]
+
+    # --- prod = y * scale as 128-bit (4x u32 limbs) ---
+    u32split
+    # => [y_hi, y_lo, y_ret, scale_mul, scale_cmp, x3, x2, x1, x0]
+
+    movup.3 u32split
+    # => [scale_hi, scale_lo, y_hi, y_lo, y_ret, scale_cmp, x3, x2, x1, x0]
+
+    exec.u64::overflowing_mul
+    # => [p3, p2, p1, p0, y_ret, scale_cmp, x3, x2, x1, x0]
+
+    # --- low64: (x1,x0) - (p1,p0) ---
+    movup.9     # x0
+    movup.9     # x1
+    movup.5     # p0
+    movup.5     # p1
+    exec.u64::overflowing_sub
+    # => [under0, z1, z0, p3, p2, y_ret, scale_cmp, x3, x2]
+
+    # --- high64: (x3,x2) - (p3,p2) ---
+    movup.8     # x2
+    movup.8     # x3
+    movup.6     # p2
+    movup.6     # p3
+    exec.u64::overflowing_sub
+    # => [under1, t_hi, t_lo, under0, z1, z0, y_ret, scale_cmp]
+
+    # subtract borrow under0 from high64
+    swap.3
+    push.0
+    exec.u64::overflowing_sub
+    # => [under2, z_hi, z_lo, under1, z1, z0, y_ret, scale_cmp]
+
+    # underflow = under1 OR under2
+    movup.3 or
+    eq.0 assert.err=ERR_UNDERFLOW
+    # => [z_hi, z_lo, z1, z0, y_ret, scale_cmp]
+
+    # --- enforce z < scale_cmp (scale_cmp fits in u64) ---
+    # if z < scale_cmp <= 2^64, then high64(z) must be zero
+    dup eq.0 assert.err=ERR_REMAINDER_TOO_LARGE
+    dup.1 eq.0 assert.err=ERR_REMAINDER_TOO_LARGE
+    drop drop
+    # => [z1, z0, y_ret, scale_cmp]
+
+    # compare low64(z) < scale_cmp
+    movup.3 u32split
+    # => [scale_hi, scale_lo, z1, z0, y_ret]
+
+    exec.u64::lt
+    # => [is_lt, y_ret]
+
+    assert.err=ERR_REMAINDER_TOO_LARGE
+    # => [y_ret]
 end
+
+# TODO: Rm & use scale_u256_to_native_amount
+pub proc scale_u256_to_native_amount_stubbed
+    repeat.7 drop end
+end