From d814a53a99b95d1874c259c8f1e737df82acfc0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Grzegorz=20=C5=9Awirski?= Date: Wed, 22 Apr 2026 15:43:56 +0200 Subject: [PATCH 1/2] update smt with domain separation --- CHANGELOG.md | 1 + Cargo.lock | 56 ++++----- Cargo.toml | 17 ++- crates/lib/core/asm/collections/smt.masm | 64 +++++----- .../lib/core/asm/crypto/hashes/poseidon2.masm | 113 ++++++++++++++++++ crates/lib/core/asm/mem.masm | 53 ++++++++ .../lib/core/docs/crypto/hashes/poseidon2.md | 3 + crates/lib/core/docs/mem.md | 1 + crates/lib/core/tests/collections/smt.rs | 59 +++++++++ 9 files changed, 305 insertions(+), 62 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f32e796956..74eddc2cce 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -36,6 +36,7 @@ - Added fuzz coverage for package semantic deserialization and project parsing, loading, and assembly ([#3015](https://github.com/0xMiden/miden-vm/pull/3015)). - Speed-up AUX range check trace generation by changing divisors to a flat Vec layout ([#2966](https://github.com/0xMiden/miden-vm/pull/2966)). - Removed AIR constraint tagging instrumentation, applied a uniform constraint description style across components, and optimized constraint evaluation ([#2856](https://github.com/0xMiden/miden-vm/pull/2856)). +- [BREAKING] Updated the Miden crypto stack to `miden-crypto` 0.25, and switched SMT leaf hashing to use Poseidon2 domain separation so masm-side leaf digests match `SmtLeaf::hash()` ([#3045](https://github.com/0xMiden/miden-vm/pull/3045)). ## 0.22.1 diff --git a/Cargo.lock b/Cargo.lock index 61ef5221a3..2361d5b2ad 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1373,7 +1373,7 @@ dependencies = [ "miden-verifier", "num", "num-bigint", - "rand 0.9.4", + "rand 0.9.3", "rand_chacha", "rstest", "thiserror", @@ -1381,14 +1381,14 @@ dependencies = [ [[package]] name = "miden-crypto" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b65e72c0e79847da910d263cfaa38572a21a381b58a06666cedb01bbe2ac353" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "blake3", "cc", "chacha20poly1305", "curve25519-dalek", + "der", "ed25519-dalek", "flume", "hkdf", @@ -1409,7 +1409,7 @@ dependencies = [ "p3-maybe-rayon", "p3-symmetric", "p3-util", - "rand 0.9.4", + "rand 0.9.3", "rand_chacha", "rand_core 0.9.5", "rand_hc", @@ -1424,9 +1424,8 @@ dependencies = [ [[package]] name = "miden-crypto-derive" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99b940316a090de8f2db8825b75ffd7975445478639f4befc0471a62f45b2f66" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "quote", "syn 2.0.117", @@ -1450,9 +1449,8 @@ dependencies = [ [[package]] name = "miden-field" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3ea5945a9bc14419b1b4cafc9762217c3f553330aa770af65c61c37268725d2e" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "miden-serde-utils", "num-bigint", @@ -1478,9 +1476,8 @@ dependencies = [ [[package]] name = "miden-lifted-air" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f14ed14fb4cb057fc3fc97a73c4467f6fbb0feefd588f1e4eff765513388f61" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "p3-air", "p3-field", @@ -1491,9 +1488,8 @@ dependencies = [ [[package]] name = "miden-lifted-stark" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "200188ccdf7cdf4d0b2a4ea81bcb698280b9218704ff92196de322c2114eb924" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "miden-lifted-air", "miden-stark-transcript", @@ -1632,9 +1628,8 @@ dependencies = [ [[package]] name = "miden-serde-utils" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94c2ae629849e1e6d851fa6ba85f9fb9715a10d6b9a8bed29a5a5403164c7595" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "p3-field", "p3-goldilocks", @@ -1642,9 +1637,8 @@ dependencies = [ [[package]] name = "miden-stark-transcript" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "40178330e5bbf29715fbf9d53fda8b6fb72d7b98e56958acc46f33545dbbacc3" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "p3-challenger", "p3-field", @@ -1654,9 +1648,8 @@ dependencies = [ [[package]] name = "miden-stateful-hasher" -version = "0.24.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "614a10d9dbba4d5984cb6ff3a30f0060660cfe3804f56c1191040584ccd638ea" +version = "0.25.0" +source = "git+https://github.com/0xMiden/crypto?branch=next#68ac2cf0b8473a63998b38149f8d599ffe3179b8" dependencies = [ "p3-field", "p3-symmetric", @@ -1775,9 +1768,8 @@ dependencies = [ [[package]] name = "midenc-hir-type" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8a9cecc109a7be41d364710d92d43c2912ef4620c8d243a2399e596f90594036" +version = "0.5.4" +source = "git+https://github.com/reilabs/midenc-hir-type?branch=crypto-0.25#1a88c86921483231242b547e5926d283a6374b11" dependencies = [ "miden-formatting", "miden-serde-utils", @@ -2362,7 +2354,7 @@ checksum = "37566cb3fdacef14c0737f9546df7cfeadbfbc9fef10991038bf5015d0c80532" dependencies = [ "bitflags", "num-traits", - "rand 0.9.4", + "rand 0.9.3", "rand_chacha", "rand_xorshift", "regex-syntax", @@ -2417,9 +2409,9 @@ checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" [[package]] name = "rand" -version = "0.9.4" +version = "0.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" +checksum = "7ec095654a25171c2124e9e3393a930bddbffdc939556c914957a4c3e0a87166" dependencies = [ "rand_chacha", "rand_core 0.9.5", diff --git a/Cargo.toml b/Cargo.toml index 2c398b9613..502059b60f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -69,10 +69,10 @@ miden-utils-testing = { path = "./crates/test-utils", package = "miden-test- miden-verifier = { path = "./verifier", version = "0.23.0", default-features = false } # Miden crates -miden-crypto = { version = "0.24", default-features = false } +miden-crypto = { version = "0.25", default-features = false } miden-formatting = { version = "0.1", default-features = false } -miden-lifted-stark = { version = "0.24", default-features = false } -midenc-hir-type = { version = "0.6.0", default-features = false } +miden-lifted-stark = { version = "0.25", default-features = false } +midenc-hir-type = { version = "0.5.4", default-features = false } # Serialization bincode = "1.3" @@ -109,3 +109,14 @@ toml = { version = "1.0", default-features = false } [workspace.lints.rust] unexpected_cfgs = { check-cfg = ['cfg(fuzzing)'], level = "warn" } + +[patch.crates-io] +miden-crypto = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-crypto-derive = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-field = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-serde-utils = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-lifted-air = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-lifted-stark = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-stark-transcript = { git = "https://github.com/0xMiden/crypto", branch = "next" } +miden-stateful-hasher = { git = "https://github.com/0xMiden/crypto", branch = "next" } +midenc-hir-type = { git = "https://github.com/reilabs/midenc-hir-type", branch = "crypto-0.25" } \ No newline at end of file diff --git a/crates/lib/core/asm/collections/smt.masm b/crates/lib/core/asm/collections/smt.masm index ba626dcc3f..a0b139ed87 100644 --- a/crates/lib/core/asm/collections/smt.masm +++ b/crates/lib/core/asm/collections/smt.masm @@ -14,6 +14,11 @@ const LEAF_DEPTH = 64 # Each key-value pair is two words, and a leaf can hold up to 1024 pairs. const MAX_LEAF_SIZE = 8192 +# Domain identifier used when hashing SMT leaves. Matches `SmtLeaf::LEAF_DOMAIN` in miden-crypto +# and is mixed into the Poseidon2 capacity word to domain-separate leaf hashes from ordinary +# inner Merkle nodes. +const LEAF_DOMAIN = 0x13af + # EXPORTS # ================================================================================================= @@ -100,9 +105,9 @@ pub proc get dupw.1 movdnw.3 # => [V, K, NV, V, R] - # Hash leaf preimage and ensure that it equals node value - # (27 cycles) - hmerge assert_eqw + # Hash leaf preimage with domain separation and ensure that it equals node value + # (28 cycles) + push.LEAF_DOMAIN exec.poseidon2::merge_in_domain assert_eqw # => [V, R] else # => [leaf_size, NV, K, R] @@ -268,8 +273,10 @@ proc get_multi_leaf_value locaddr.0 swap # => [num_words, ptr, COM, K, R] - # Cycles: 56 + 3 * num_words / 2 - exec.mem::pipe_double_words_preimage_to_memory + # Push the leaf domain so the preimage check uses the same capacity word as the Rust-side + # `SmtLeaf::hash()` for `Multiple` leaves. + # Cycles: 58 + 3 * num_words / 2 + push.LEAF_DOMAIN exec.mem::pipe_double_words_preimage_to_memory_with_domain # => [ptr_end, K, R] # (4 cycles) @@ -353,13 +360,14 @@ proc set_empty_leaf dropw #=> [V, K, R, ...] - # Update advice map (swap to put K on top for key = hash(K || V)) - swapw adv.insert_hdword swapw + # Update advice map with domain separation (swap to put K on top for the leaf-domain + # hash key hash_in_domain(K || V, LEAF_DOMAIN)). + swapw push.LEAF_DOMAIN movdn.8 adv.insert_hdword_d movup.8 drop swapw #=> [V, K, R, ...] - # Compute hash([K, V]); the new node value (NV) - # (20 cycles) - dupw.1 hmerge + # Compute hash_in_domain([K, V], LEAF_DOMAIN); the new node value (NV) + # (21 cycles) + dupw.1 push.LEAF_DOMAIN exec.poseidon2::merge_in_domain # => [NV, K, R] # Prepare stack for `mtree_set` (5 cycles) @@ -453,13 +461,14 @@ proc insert_single_leaf dropw # => [K, V_in_leaf, V, R] - # Update advice map (5 cycles, swap to put K on top for key = hash(K || V)) - movupw.2 swapw adv.insert_hdword swapw + # Update advice map with domain separation (swap to put K on top for the leaf-domain + # hash key hash_in_domain(K || V, LEAF_DOMAIN)). + movupw.2 swapw push.LEAF_DOMAIN movdn.8 adv.insert_hdword_d movup.8 drop swapw # => [V, K, V_in_leaf, R] - # Compute hash([K, V]); the new node value (NV) + # Compute hash_in_domain([K, V], LEAF_DOMAIN); the new node value (NV) # (X cycles) - dupw.1 hmerge + dupw.1 push.LEAF_DOMAIN exec.poseidon2::merge_in_domain # => [NV, K, V_in_leaf, R] # Prepare stack to update Merkle store @@ -472,9 +481,9 @@ proc insert_single_leaf # => [NV_old, R_new, K, V_in_leaf] # Confirm that claimed `V_in_leaf` from advice provider is correct by checking if - # `[K, V_in_leaf]` hashes to `NV_old` - # (33 cycles) - movupw.2 dupw.3 swapw hmerge assert_eqw + # `[K, V_in_leaf]` hashes (with LEAF_DOMAIN) to `NV_old` + # (34 cycles) + movupw.2 dupw.3 swapw push.LEAF_DOMAIN exec.poseidon2::merge_in_domain assert_eqw # => [R_new, V_in_leaf] # Clean up stack for return @@ -616,8 +625,9 @@ proc remove_single_leaf dropw # => [K, V_in_leaf, V, R] - # Update advice map (5 cycles, swap to put K on top for key = hash(K || V)) - movupw.2 swapw adv.insert_hdword swapw + # Update advice map with domain separation (swap to put K on top for the leaf-domain + # hash key hash_in_domain(K || V, LEAF_DOMAIN)). + movupw.2 swapw push.LEAF_DOMAIN movdn.8 adv.insert_hdword_d movup.8 drop swapw # => [V, K, V_in_leaf, R] # Prepare the stack for `mtree_set` @@ -631,10 +641,10 @@ proc remove_single_leaf mtree_set # => [NV_old, R_new, K, V_in_leaf, ...] - # Confirm that hmerge([K, V_in_leaf]) = NV_old - # (33 cycles) + # Confirm that hash_in_domain([K, V_in_leaf], LEAF_DOMAIN) = NV_old + # (34 cycles) movupw.2 dupw.3 - swapw hmerge + swapw push.LEAF_DOMAIN exec.poseidon2::merge_in_domain assert_eqw # => [R_new, V_in_leaf, ...] @@ -665,8 +675,8 @@ proc remove_single_leaf movupw.3 dropw # => [NV, R, K_in_leaf, V_in_leaf] - # Ensure that hash([K_in_leaf, V_in_leaf]) == NV - movupw.2 movupw.3 swapw hmerge assert_eqw + # Ensure that hash_in_domain([K_in_leaf, V_in_leaf], LEAF_DOMAIN) == NV + movupw.2 movupw.3 swapw push.LEAF_DOMAIN exec.poseidon2::merge_in_domain assert_eqw # => [R] # Prepare stack for return @@ -692,7 +702,7 @@ end @locals(8192) proc set_multi_leaf # We'll have to pipe all the pairs from the advice stack. Let's get the - # stack ready for pipe_double_words_preimage_to_memory. + # stack ready for pipe_double_words_preimage_to_memory_with_domain. movdn.12 # => [NV, V, K, leaf_size, R] @@ -713,7 +723,7 @@ proc set_multi_leaf locaddr.0 swap # => [num_words, ptr, COM; NV, K, V, leaf_size, R] - exec.mem::pipe_double_words_preimage_to_memory + push.LEAF_DOMAIN exec.mem::pipe_double_words_preimage_to_memory_with_domain # => [end_ptr; NV, K, V, leaf_size, R] movdn.12 @@ -1122,7 +1132,7 @@ proc hash_and_insert_mem dup.1 dup.1 # => [start_addr, end_addr, start_addr, end_addr, leaf_index, R, ...] - exec.poseidon2::hash_words + push.LEAF_DOMAIN exec.poseidon2::hash_words_with_domain # => [NV, start_addr, end_addr, leaf_index, R, ...] adv.insert_mem diff --git a/crates/lib/core/asm/crypto/hashes/poseidon2.masm b/crates/lib/core/asm/crypto/hashes/poseidon2.masm index 6950ba13e7..d433e710ed 100644 --- a/crates/lib/core/asm/crypto/hashes/poseidon2.masm +++ b/crates/lib/core/asm/crypto/hashes/poseidon2.masm @@ -13,6 +13,21 @@ pub proc init_no_padding padw padw padw end +#! Prepares the top of the stack with the hasher initial state, using a caller-supplied capacity +#! word. +#! +#! The caller must have placed the capacity word `C` on top of the stack before invoking this +#! procedure. No padding handling is performed: callers must absorb data which is a multiple of +#! the rate (2 words), or handle odd-length absorption themselves. +#! +#! Input: [C, ...] +#! Output: [R0=0w, R1=0w, C, ...] +#! +#! Cycles: 8 +pub proc init_with_capacity + padw padw +end + #! Given the hasher state, returns the hash output (digest). #! #! Input: [R0, R1, C, ...] @@ -169,6 +184,74 @@ pub proc hash_words # => [HASH] end +#! Hashes the memory `start_addr` to `end_addr` with a domain identifier, handling an odd number +#! of words. +#! +#! Semantically equivalent to `Poseidon2::hash_elements_in_domain(&elements, domain)` where +#! `elements` is the sequence of felts from `start_addr` to `end_addr` (exclusive). +#! +#! Requires `start_addr ≤ end_addr`, `end_addr` is not inclusive. +#! Requires `start_addr` and `end_addr` to be word-aligned. +#! +#! Input: [domain, start_addr, end_addr, ...] +#! Output: [H, ...] +#! +#! Cycles: +#! - even words: 54 cycles + 3 * words +#! - odd words: 66 cycles + 3 * words +#! where `words` is `(end_addr - start_addr) / 4`. +pub proc hash_words_with_domain + # Move the domain past the address pair so we can reuse the standard hash_words control flow. + # (1 cycle) + movdn.2 + # => [start_addr, end_addr, domain, ...] + + # enforce `start_addr ≤ end_addr` + dup.1 dup.1 u32assert2 u32gte assert + + # figure out if the range is for an odd number of words (11 cycles) + dup.1 dup.1 sub div.4 is_odd + # => [is_odd, start_addr, end_addr, domain, ...] + + # make the start/end range even (6 cycles) + movup.2 dup.1 mul.4 sub + # => [end_addr, is_odd, start_addr, domain, ...] + + # move start_addr to the right stack position (1 cycle) + movup.2 + # => [start_addr, end_addr, is_odd, domain, ...] + + # prepare hasher state with capacity `[is_odd*4, domain, 0, 0]` (14 cycles) + dup.2 mul.4 push.0.0 movup.6 movup.3 padw padw + # => [R0=0w, R1=0w, C=[is_odd*4, domain, 0, 0], start_addr, end_addr, is_odd, ...] + + # (4 + 3 * words cycles) + exec.absorb_double_words_from_memory + # => [R0', R1', C', end_addr, end_addr, is_odd, ...] + + # (1 cycle) + movup.14 + # => [is_odd, R0', R1', C', end_addr, end_addr, ...] + + # handle the odd element, if any (12 cycles) + if.true + # start_addr and end_addr are equal after calling `absorb_double_words_from_memory`, and both + # point to the last element. Load the last word (6 cycles) + dropw dup.9 mem_loadw_le + # => [W, C', end_addr, end_addr, ...] + + # set the padding and compute the permutation (5 cycles) + padw swapw exec.permute + end + + exec.squeeze_digest + # => [HASH, end_addr, end_addr, ...] + + # drop start_addr/end_addr (4 cycles) + movup.4 drop movup.4 drop + # => [HASH] +end + #! Initializes the hasher state required for the `hash_elements_with_state` procedure. #! #! Depending on the provided pad_inputs_flag, this procedure initializes the hasher state using @@ -466,6 +549,36 @@ pub proc merge hmerge end +#! Merges two words (256-bit digests) via Poseidon2 hash with a domain identifier. +#! +#! Semantically equivalent to `Poseidon2::merge_in_domain(&[B, A], domain)` in miden-crypto +#! (i.e., B is the first rate word, A is the second rate word, and the domain is placed into +#! the second element of the capacity word, matching the convention used by +#! `adv.insert_hdword_d`). +#! +#! Inputs: [domain, B, A, ...] +#! Outputs: [C, ...] +#! +#! Where: +#! - B and A are the words to be merged (B corresponds to the first rate word). +#! - C is the resulting hash, computed with capacity `[0, domain, 0, 0]`. +#! +#! Cycles: 16 +pub proc merge_in_domain + # move `domain` past the two words so we can reuse the `adv.insert_hdword_d` capacity-word + # construction pattern (1 cycle) + movdn.8 + # => [B, A, domain, ...] + + # build the hperm state [B, A, [0, domain, 0, 0]] (5 cycles) + push.0.0 movup.10 push.0 movdnw.2 + # => [B, A, [0, domain, 0, 0], ...] + + # run the permutation (1 cycle) and squeeze the digest (9 cycles) + hperm + exec.squeeze_digest +end + #! Performs Poseidon2 permutation on the hasher state. #! #! Inputs: [R0, R1, C] diff --git a/crates/lib/core/asm/mem.masm b/crates/lib/core/asm/mem.masm index 3f92b5b805..558415ae31 100644 --- a/crates/lib/core/asm/mem.masm +++ b/crates/lib/core/asm/mem.masm @@ -322,3 +322,56 @@ pub proc pipe_double_words_preimage_to_memory # Assert the commitment (11 cycles). assert_eqw.err="pipe_double_words_preimage_to_memory: COMMITMENT does not match" end + +#! Moves an even number of words from the advice stack to memory and asserts that their +#! domain-tagged sequential hash matches a given commitment. +#! +#! Like `pipe_double_words_preimage_to_memory`, but initializes the Poseidon2 capacity word to +#! `[0, domain, 0, 0]` so that the digest matches `Poseidon2::hash_elements_in_domain(&elems, domain)`. +#! +#! Inputs: [domain, num_words, write_ptr, COMMITMENT] +#! Outputs: [write_ptr'] +#! +#! Where: +#! - domain is the domain identifier placed into the second element of the capacity word. +#! - num_words is the number of words which will be copied to the memory (must be even). +#! - write_ptr is the memory pointer where the words will be copied. +#! - write_ptr' is the memory pointer to the end of the copied words. +#! - COMMITMENT is the domain-tagged digest that the preimage must hash to. +#! +#! Total cycles: 57 + 3 * num_words / 2 +pub proc pipe_double_words_preimage_to_memory_with_domain + # Bring `num_words` to the top so we can check and consume it below (1 cycle). + swap + # => [num_words, domain, write_ptr, COMMITMENT, ...] + + # Assert precondition (8 cycles). + dup is_odd assertz.err="pipe_double_words_preimage_to_memory_with_domain: num_words must be even" + # => [num_words, domain, write_ptr, COMMITMENT, ...] + + # Compute end_ptr = write_ptr + num_words * 4 and reorder the stack (5 cycles). + mul.4 dup.2 add movup.2 + # => [write_ptr, end_ptr, domain, COMMITMENT, ...] + + # Build the capacity word `[0, domain, 0, 0]` on top of the stack (4 cycles). + push.0.0 movup.4 push.0 + # => [C=[0, domain, 0, 0], write_ptr, end_ptr, COMMITMENT, ...] + + # Fill in R0 and R1 with zeros (8 cycles). + exec.poseidon2::init_with_capacity + # => [R0, R1, C, write_ptr, end_ptr, COMMITMENT, ...] + + # (9 + 3 * num_words cycles) + exec.pipe_double_words_to_memory + # => [R0', R1', C', write_ptr', COMMITMENT, ...] + + # Leave just the digest on the stack (9 cycles). + exec.poseidon2::squeeze_digest + # => [DIGEST, write_ptr', COMMITMENT, ...] + + # Move write_ptr out of the way so we can assert the commitment (2 cycles). + movup.4 movdn.8 + + # Assert the commitment (11 cycles). + assert_eqw.err="pipe_double_words_preimage_to_memory_with_domain: COMMITMENT does not match" +end diff --git a/crates/lib/core/docs/crypto/hashes/poseidon2.md b/crates/lib/core/docs/crypto/hashes/poseidon2.md index 333c7bbcf4..5bec46eea7 100644 --- a/crates/lib/core/docs/crypto/hashes/poseidon2.md +++ b/crates/lib/core/docs/crypto/hashes/poseidon2.md @@ -3,15 +3,18 @@ | Procedure | Description | | ----------- | ------------- | | init_no_padding | Prepares the top of the stack with the hasher initial state.

This procedures does not handle padding, therefore, the user is expected to
consume an amount of data which is a multiple of the rate (2 words).

Input: []
Output: [PERM, PERM, PERM, ...]

Cycles: 12
| +| init_with_capacity | Prepares the top of the stack with the hasher initial state, using a caller-supplied capacity
word.

The caller must have placed the capacity word `C` on top of the stack before invoking this
procedure. No padding handling is performed: callers must absorb data which is a multiple of
the rate (2 words), or handle odd-length absorption themselves.

Input: [C, ...]
Output: [R0=0w, R1=0w, C, ...]

Cycles: 8
| | squeeze_digest | Given the hasher state, returns the hash output (digest).

Input: [R0, R1, C, ...]
Output: [DIGEST, ...]

Where:
- `R0` is the first rate word / digest (positions 0-3, on top of stack).
- `R1` is the second rate word (positions 4-7).
- `C` is the capacity word (positions 8-11).
- `DIGEST = R0`.

Cycles: 9
| | copy_digest | Copies the digest to the top of the stack.

It is expected to have the hasher state at the top of the stack at the beginning of the procedure
execution.

Input: [R0, R1, C, ...]
Output: [DIGEST, R0, R1, C, ...]

Where:
- `R0` is the first rate word / digest (positions 0-3, on top of stack).
- `R1` is the second rate word (positions 4-7).
- `C` is the capacity word (positions 8-11).
- `DIGEST = R0`.

Cycles: 4
| | absorb_double_words_from_memory | Hashes the memory `start_addr` to `end_addr` given a Poseidon2 state specified by 3 words.

This requires that `end_addr = start_addr + 8n` where n = {0, 1, 2 ...}, otherwise the procedure
will enter an infinite loop.

Input: [R0, R1, C, start_addr, end_addr, ...]
Output: [R0', R1', C', end_addr, end_addr ...]

Where:
- `R0` is the first rate word / digest (positions 0-3, on top of stack).
- `R1` is the second rate word (positions 4-7).
- `C` is the capacity word (positions 8-11).

Cycles: 4 + 3 * words, where `words` is the `start_addr - end_addr`
| | hash_double_words | Hashes the pairs of words in the memory from `start_addr` to `end_addr`.

This procedure requires that `end_addr = start_addr + 8n` where n = {0, 1, 2 ...} (i.e. we must
always hash some number of double words), otherwise the procedure will enter an infinite loop.

Input: [start_addr, end_addr, ...]
Output: [HASH, ...]

Where:
- `HASH` is the cumulative hash of the provided memory values.

Cycles: 37 + 3 * words, where `words` is the `start_addr - end_addr`
| | hash_words | Hashes the memory `start_addr` to `end_addr`, handles odd number of elements.

Requires `start_addr ≤ end_addr`, `end_addr` is not inclusive.
Requires `start_addr` and `end_addr` to be word-aligned.

Input: [start_addr, end_addr, ...]
Output: [H, ...]

Cycles:
- even words: 53 cycles + 3 * words
- odd words: 65 cycles + 3 * words
where `words` is the `start_addr - end_addr - 1`
| +| hash_words_with_domain | Hashes the memory `start_addr` to `end_addr` with a domain identifier, handling an odd number
of words.

Semantically equivalent to `Poseidon2::hash_elements_in_domain(&elements, domain)` where
`elements` is the sequence of felts from `start_addr` to `end_addr` (exclusive).

Requires `start_addr ≤ end_addr`, `end_addr` is not inclusive.
Requires `start_addr` and `end_addr` to be word-aligned.

Input: [domain, start_addr, end_addr, ...]
Output: [H, ...]

Cycles:
- even words: 54 cycles + 3 * words
- odd words: 66 cycles + 3 * words
where `words` is `(end_addr - start_addr) / 4`.
| | prepare_hasher_state | Initializes the hasher state required for the `hash_elements_with_state` procedure.

Depending on the provided pad_inputs_flag, this procedure initializes the hasher state using
different values for capacity element:
- If pad_inputs_flag = 1 the capacity element is set to 0. This will essentially "pad" the
hashed values with zeroes to the next multiple of 8.
- If pad_inputs_flag = 0 the capacity element is set to the remainder of the division of
number of hashed elements by 8 (num_elements%8).

Inputs: [ptr, num_elements, pad_inputs_flag]
Outputs: [R0, R1, C, ptr, end_pairs_addr, num_elements%8]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- num_elements is the number of elements to be hashed.
- pad_inputs_flag is the flag which indicates whether the values which will be hashed should be
padded with zeros to the next multiple of 8.
- R0, R1, C are three words representing the hasher state (R0 on top).
- end_pairs_addr is the memory address at which the pairs of words end.
- num_elements%8 is the number of elements which didn't fit to the word pairs and should be
hashed separately.
| | hash_elements_with_state | Computes hash of Felt values starting at the specified memory address using the provided hasher
state.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `permute`
procedure.

Inputs: [R0, R1, C, ptr, end_pairs_addr, num_elements%8]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- R0, R1, C are three words representing the hasher state (R0 on top).
- end_pairs_addr is the memory address at which the pairs of words end.
- num_elements%8 is the number of elements which didn't fit to the word pairs and should be
hashed separately.
- HASH is the resulting hash of the provided memory values.
| | hash_elements | Computes hash of Felt values starting at the specified memory address.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `permute`
procedure.

Inputs: [ptr, num_elements]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- num_elements is the number of elements to be hashed.
- HASH is the resulting hash of the provided memory values.

Cycles:
- If number of elements divides by 8: 52 cycles + 3 * words
- Else: 185 cycles + 3 * words
where `words` is the number of quads of input values.
| | pad_and_hash_elements | Computes hash of Felt values starting at the specified memory address.

Notice that this procedure essentially pads the elements to be hashed to the next multiple of 8
by setting the capacity element to 0.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `permute`
procedure.

Inputs: [ptr, num_elements]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- num_elements is the number of elements to be hashed.
- HASH is the resulting hash of the provided memory values.

Cycles:
- If number of elements divides by 8: 52 cycles + 3 * words
- Else: 185 cycles + 3 * words
where `words` is the number of quads of input values.
| | hash | Computes Poseidon2 hash of a single word (256-bit input).

Inputs: [A]
Outputs: [B]

Where:
- A is the word to be hashed.
- B is the resulting hash, computed as `Poseidon2(A)`.

Cycles: 20
| | merge | Merges two words (256-bit digests) via Poseidon2 hash.

Inputs: [B, A]
Outputs: [C]

Where:
- A and B are the words to be merged.
- C is the resulting hash, computed as `Poseidon2(A \|\| B)`.

Cycles: 16
| +| merge_in_domain | Merges two words (256-bit digests) via Poseidon2 hash with a domain identifier.

Semantically equivalent to `Poseidon2::merge_in_domain(&[B, A], domain)` in miden-crypto
(i.e., B is the first rate word, A is the second rate word, and the domain is placed into
the second element of the capacity word, matching the convention used by
`adv.insert_hdword_d`).

Inputs: [domain, B, A, ...]
Outputs: [C, ...]

Where:
- B and A are the words to be merged (B corresponds to the first rate word).
- C is the resulting hash, computed with capacity `[0, domain, 0, 0]`.

Cycles: 16
| | permute | Performs Poseidon2 permutation on the hasher state.

Inputs: [R0, R1, C]
Outputs: [R0', R1', C']

Where:
- R0, R1, C are three words representing the hasher state (R0 on top).
- R0', R1', C' are the permuted state words.

Cycles: 1
| diff --git a/crates/lib/core/docs/mem.md b/crates/lib/core/docs/mem.md index 293c16a918..fe651d75af 100644 --- a/crates/lib/core/docs/mem.md +++ b/crates/lib/core/docs/mem.md @@ -8,3 +8,4 @@ | pipe_words_to_memory | Copies an arbitrary number of words from the advice stack to memory, computing their permutation.

Inputs: [num_words, write_ptr]
Outputs: [R0, R1, C, write_ptr']

Where:
- num_words is the number of words which will be copied to the memory.
- write_ptr is the memory pointer where the words will be copied.
- write_ptr' is the memory pointer to the end of the copied words.
- R0, R1, C are the final Poseidon2 hasher state (R0 on top).

Total cycles:
- Even `num_words`: 43 + 9 * num_words / 2
- Odd `num_words`: 60 + 9 * round_down(num_words / 2)
| | pipe_preimage_to_memory | Moves an arbitrary number of words from the advice stack to memory and asserts it matches the
commitment.

Inputs: [num_words, write_ptr, COMMITMENT]
Outputs: [write_ptr']

Where:
- num_words is the number of words which will be copied to the memory.
- write_ptr is the memory pointer where the words will be copied.
- write_ptr' is the memory pointer to the end of the copied words.
- COMMITMENT is the commitment that the one calculated during this procedure will be compared
with.

Total cycles:
- Even `num_words`: 62 + 9 * num_words / 2
- Odd `num_words`: 79 + 9 * round_down(num_words / 2)
| | pipe_double_words_preimage_to_memory | Moves an even number of words from the advice stack to memory and asserts that their sequential
hash matches a given commitment.

Inputs: [num_words, write_ptr, COMMITMENT]
Outputs: [write_ptr']

Where:
- num_words is the number of words which will be copied to the memory.
- write_ptr is the memory pointer where the words will be copied.
- write_ptr' is the memory pointer to the end of the copied words.
- COMMITMENT is the commitment that the one calculated during this procedure will be compared
with.

Total cycles: 56 + 3 * num_words / 2
| +| pipe_double_words_preimage_to_memory_with_domain | Moves an even number of words from the advice stack to memory and asserts that their
domain-tagged sequential hash matches a given commitment.

Like `pipe_double_words_preimage_to_memory`, but initializes the Poseidon2 capacity word to
`[0, domain, 0, 0]` so that the digest matches `Poseidon2::hash_elements_in_domain(&elems, domain)`.

Inputs: [domain, num_words, write_ptr, COMMITMENT]
Outputs: [write_ptr']

Where:
- domain is the domain identifier placed into the second element of the capacity word.
- num_words is the number of words which will be copied to the memory (must be even).
- write_ptr is the memory pointer where the words will be copied.
- write_ptr' is the memory pointer to the end of the copied words.
- COMMITMENT is the domain-tagged digest that the preimage must hash to.

Total cycles: 57 + 3 * num_words / 2
| diff --git a/crates/lib/core/tests/collections/smt.rs b/crates/lib/core/tests/collections/smt.rs index a60af5c96a..f0b29542e5 100644 --- a/crates/lib/core/tests/collections/smt.rs +++ b/crates/lib/core/tests/collections/smt.rs @@ -1,4 +1,5 @@ use miden_core_lib::handlers::smt_peek::SMT_PEEK_EVENT_NAME; +use miden_crypto::merkle::smt::LEAF_DOMAIN; use super::*; @@ -650,6 +651,64 @@ fn test_smt_leaf_hash_matches_merkle_store() { } } +/// Regression check: a single-entry leaf hash is domain-separated, so it must not equal the +/// plain `merge([K, V])` that would be produced with domain 0. +#[test] +fn test_smt_single_leaf_hash_differs_from_plain_merge() { + use miden_utils_testing::crypto::Poseidon2; + + let (key, value) = LEAVES[0]; + let smt = build_smt_from_pairs(&[(key, value)]); + + let leaf = smt.leaves().next().map(|(_, leaf)| leaf).unwrap(); + let leaf_hash = leaf.hash(); + + let plain_merge = Poseidon2::merge(&[key, value]); + let domain_merge = Poseidon2::merge_in_domain(&[key, value], LEAF_DOMAIN); + + assert_ne!( + leaf_hash, plain_merge, + "single-entry leaf hash must not equal plain merge([K, V])" + ); + assert_eq!( + leaf_hash, domain_merge, + "single-entry leaf hash must equal merge_in_domain([K, V], LEAF_DOMAIN)" + ); +} + +/// Regression check: a multi-entry leaf hash is domain-separated, so it must not equal the +/// plain `hash_elements` of its preimage. This would fail if the preimage check still used +/// domain 0 on either the Rust or MASM side. +#[test] +fn test_smt_multi_leaf_hash_differs_from_domain_zero() { + use miden_utils_testing::crypto::Poseidon2; + + let smt = build_smt_from_pairs(&LEAVES_MULTI); + + // Find the leaf that contains multiple entries (same K[0] bucket). + let multi_leaf = smt + .leaves() + .map(|(_, leaf)| leaf) + .find(|leaf| leaf.entries().len() > 1) + .expect("LEAVES_MULTI must produce at least one multi-entry leaf"); + assert!(multi_leaf.entries().len() >= 2); + + let leaf_hash = multi_leaf.hash(); + let elements: Vec = multi_leaf.to_elements().collect(); + + let plain_hash = Poseidon2::hash_elements(&elements); + let domain_hash = Poseidon2::hash_elements_in_domain(&elements, LEAF_DOMAIN); + + assert_ne!( + leaf_hash, plain_hash, + "multi-entry leaf hash must not equal plain hash_elements(preimage) (domain 0)" + ); + assert_eq!( + leaf_hash, domain_hash, + "multi-entry leaf hash must equal hash_elements_in_domain(preimage, LEAF_DOMAIN)" + ); +} + // HELPER FUNCTIONS // ================================================================================================ From cd17790bef5e5f0782ed1b96bb5f2fe67fa2f894 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Grzegorz=20=C5=9Awirski?= Date: Fri, 24 Apr 2026 14:32:08 +0200 Subject: [PATCH 2/2] bump midenc-hir-type --- Cargo.lock | 4 ++-- Cargo.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2361d5b2ad..38645a25e8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1768,8 +1768,8 @@ dependencies = [ [[package]] name = "midenc-hir-type" -version = "0.5.4" -source = "git+https://github.com/reilabs/midenc-hir-type?branch=crypto-0.25#1a88c86921483231242b547e5926d283a6374b11" +version = "0.6.0" +source = "git+https://github.com/reilabs/midenc-hir-type?branch=crypto-0.25#55d9858be2d5ed9f5935fbc031a2f06784bd7d52" dependencies = [ "miden-formatting", "miden-serde-utils", diff --git a/Cargo.toml b/Cargo.toml index 502059b60f..5a8d2b8a24 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -72,7 +72,7 @@ miden-verifier = { path = "./verifier", version = "0.23.0", default-fea miden-crypto = { version = "0.25", default-features = false } miden-formatting = { version = "0.1", default-features = false } miden-lifted-stark = { version = "0.25", default-features = false } -midenc-hir-type = { version = "0.5.4", default-features = false } +midenc-hir-type = { version = "0.6.0", default-features = false } # Serialization bincode = "1.3"