use miden::core::crypto::hashes::poseidon2
# ===== MEMORY FUNCTIONS ==========================================================================
#! Copies `n` words from `read_ptr` to `write_ptr`.
#!
#! `read_ptr` and `write_ptr` pointers *must be* word-aligned.
#!
#! Inputs: [n, read_ptr, write_ptr]
#! Outputs: []
#!
#! Where:
#! - n is the number of words which should be copied.
#! - read_ptr is the memory pointer where the words to copy are stored.
#! - write_ptr is the memory pointer where the words will be copied.
#!
#! # Panics
#!
#! Panics if the source range `[read_ptr, read_ptr + 4*n)` and destination range
#! `[write_ptr, write_ptr + 4*n)` overlap.
#!
#! Total cycles: 15 + 16 * num_words
pub proc memcopy_words
# Assert source and destination ranges do not overlap.
# Non-overlap: write_ptr >= read_ptr + 4*n OR read_ptr >= write_ptr + 4*n
dup mul.4
dup dup.3 add
dup.4 swap u32gte
swap dup.4 add
dup.3 swap u32gte
or assert.err="source and destination ranges must not overlap"
# The loop variable is changed with an add instead of sub because the former
# uses one fewer cycle. So here the counter is negated. (1 cycles)
# stack: [-n, read_ptr, write_ptr, ...]
neg
# Pad the stack because mem_loadw_le overwrites it (4 cycles)
# stack: [0, 0, 0, 0, -n, read_ptr, write_ptr, ...]
padw
# check loop condition (3 cycles)
# stack: [b, 0, 0, 0, 0, -n, read_ptr, write_ptr, ...]
dup.4 neq.0
# LOOP: [0, 0, 0, 0, -n, read_ptr, write_ptr, ...]
# while(n!=0) (16 cycles)
while.true
# perform read (2 cycles)
# stack: [w0, w1, w2, w3, -n, read_ptr, write_ptr, ...]
dup.5 mem_loadw_le
# perform write (2 cycles)
# stack: [w0, w1, w2, w3, -n, read_ptr, write_ptr, ...]
dup.6 mem_storew_le
# note: the values of the loaded word are no longer necessary, use 0 to
# signal it is padding
# stack: [-n, read_ptr, write_ptr, x, 0, 0, 0, 0, ...]
swapw
# stack: [-n+1, read_ptr+4, write_ptr+4, x, 0, 0, 0, 0, ...]
# update counters (9 cycles)
add.1 movup.3 movup.3 add.4 movup.3 add.4 movup.3
# stack: [0, 0, 0, 0, -n+1, read_ptr+4, write_ptr+4, x, ...]
swapw
dup.4 neq.0 # while(n!=0) (3 cycles)
end
# clean stack (7 cycles)
# stack: [...]
dropw drop drop drop
end
#! Copies `n` elements from `read_ptr` to `write_ptr`.
#!
#! Inputs: [n, read_ptr, write_ptr]
#! Outputs: []
#!
#! Where:
#! - n is the number of elements which should be copied.
#! - read_ptr is the memory pointer where the elements to copy are stored.
#! - write_ptr is the memory pointer where the elements will be copied.
#!
#! # Panics
#!
#! Panics if the source range `[read_ptr, read_ptr + n)` and destination range
#! `[write_ptr, write_ptr + n)` overlap.
#!
#! Total cycles: 7 + 14 * num_elements
pub proc memcopy_elements
# Assert source and destination ranges do not overlap.
# Non-overlap: write_ptr >= read_ptr + n OR read_ptr >= write_ptr + n
dup dup.2 add
dup.3 swap u32gte
dup.1 dup.4 add
dup.3 swap u32gte
or assert.err="source and destination ranges must not overlap"
# The loop variable is changed with an `add` instead of `sub` because the former uses one fewer
# cycle. So here the counter is negated. (1 cycle)
neg
# => [-n, read_ptr, write_ptr]
# check the loop condition (3 cycles)
dup neq.0
# => [loop_flag, -n, read_ptr, write_ptr]
while.true
# perform read (2 cycles)
dup.1 mem_load
# => [value_to_store, -n, read_ptr, write_ptr]
# perform write (3 cycles)
dup.3 mem_store
# => [-n, read_ptr, write_ptr]
# update the pointers and the counter (6 cycles)
add.1 movup.2 add.1 movup.2 add.1 movup.2
# => [-n+1, read_ptr+1, write_ptr+1]
# check the loop condition (3 cycles)
dup neq.0
# => [loop_flag, -n+1, read_ptr+1, write_ptr+1]
end
# => [n = 0, read_ptr + n, write_ptr + n]
# clean stack (3 cycles)
drop drop drop
end
#! Copies an even number of words from the advice_stack to memory, computing their permutation.
#!
#! Inputs: [R0, R1, C, write_ptr, end_ptr]
#! Outputs: [R0', R1', C', write_ptr]
#!
#! 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).
#! - write_ptr is the memory pointer where the words will be copied.
#! - end_ptr is the memory pointer where the copying should end.
#!
#! Notice that the `end_ptr - write_ptr` value must be positive and a multiple of 8.
#!
#! Total cycles: 9 + 6 * num_word_pairs
pub proc pipe_double_words_to_memory
dup.13 dup.13 neq # (4 cycles)
# loop until write_ptr reaches end_ptr (6 cycles per iteration + 1)
# LOOP: [b, R0, R1, C, write_ptr, end_ptr, ...]
while.true
adv_pipe exec.poseidon2::permute # (2 cycles)
# => [R0', R1', C', write_ptr', end_ptr, ...]
dup.13 dup.13 neq # (4 cycles)
# LOOP: [b, R0', R1', C', write_ptr', end_ptr, ...]
end
movup.13 drop # (5 cycles)
# [R0', R1', C', write_ptr', ...]
end
#! 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)
pub proc pipe_words_to_memory
# check if there is an odd number of words (6 cycles)
dup is_odd
# => [is_odd, num_words, write_ptr, ...]
# copy is_odd, it defines if last word requires padding (2 cycles)
dup movdn.3
# => [is_odd, num_words, write_ptr, needs_padding, ...]
# compute `end_ptr` with an even number of words (7 cycles)
sub mul.4 dup.1 add swap
# => [write_ptr, end_ptr, needs_padding, ...]
# Prepare the capacity word. We use the padding rule which sets the first capacity
# element to `len % 8` where `len` is the length of the hashed sequence. Since `len % 8`
# is either equal to 0 or 4, this is determined by the `needs_padding` flag multiplied
# by 4. (7 cycles)
dup.2 mul.4 push.0.0.0
movup.3
# => [C, write_ptr, end_ptr, needs_padding, ...]
# (C is the capacity word)
# set initial hasher state (8 cycles)
padw padw
# => [R0, R1, C, write_ptr, end_ptr, needs_padding, ...]
# (9 + 6 * num_words cycles)
exec.pipe_double_words_to_memory
# => [R0, R1, C, write_ptr, needs_padding, ...]
# (4 cycles)
movup.13
# => [needs_padding, R0, R1, C, write_ptr, ...]
# if(needs_padding) (17 cycles)
if.true
# Poseidon2 uses overwrite mode, drop R1. (4 cycles)
swapw dropw
# => [R0, C, write_ptr, ...]
# Overwrite R0 with new data from advice stack (1 cycles)
adv_loadw
# => [R0', C, write_ptr, ...]
# - get the memory address that R0' should be saved to
# - update the write_ptr to point to the next address (4 cycles)
movup.8 dup.0 add.4 movdn.5
# => [write_ptr, R0', write_ptr+4, C, ...]
# save data to memory (1 cycles)
mem_storew_le
# => [R0', write_ptr+4, C, ...]
# Fix write_ptr position (2 cycles)
movup.4 movdn.8
# => [R0', C, write_ptr+4, ...]
# Push padding word (4 cycles)
padw swapw
# => [R0', R1, C, write_ptr+4, ...]
# Run Poseidon2 permutation (1 cycles)
exec.poseidon2::permute
# => [R0'', R1', C', write_ptr+4, ...]
end
end
#! 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)
pub proc pipe_preimage_to_memory
# Copies the advice stack data to memory
exec.pipe_words_to_memory
# => [R0, R1, C, write_ptr', COMMITMENT, ...]
# Leave only the digest on the stack
exec.poseidon2::squeeze_digest
# => [DIGEST, write_ptr', COMMITMENT, ...]
# Save the write_ptr (2 cycles)
movup.4 movdn.8
# => [HASH, COMMITMENT, write_ptr', ...]
# Check the COMMITMENT (10 cycles)
assert_eqw
# => [write_ptr', ...]
end
#! 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
pub proc pipe_double_words_preimage_to_memory
# Assert precondition (8 cycles).
dup is_odd assertz.err="pipe_double_words_preimage_to_memory: num_words must be even"
# => [num_words, write_ptr, COMMITMENT, ...]
# Compute and move end_ptr (5 cycles)
mul.4 dup.1 add swap
# => [write_ptr, end_ptr, COMMITMENT, ...]
# Setup the initial hasher state [R0, R1, C] with empty capacity.
#
# (12 cycles).
exec.poseidon2::init_no_padding
# => [R0, R1, C, write_ptr, end_ptr, COMMITMENT, ...]
# (9 + 3 * num_words cycles)
# (e.g., 21 cycles for 4 words)
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: 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]`.
#!
#! 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
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