miden-core-lib 0.24.2

Miden VM core library
Documentation
# ===== WORD FUNCTIONS ==========================================================================

#! Reverses order of the first four elements on the stack
#!
#! Note: This functionality is also available as the `reversew` instruction
#!
#! Inputs:  [a, b, c, d, ...]
#! Outputs: [d, c, b, a, ...]
#!
#! Cycles: 3
pub proc reverse(input: word) -> word
    reversew
end

# CONVERSION UTILITIES
#! Writes the components of a word to memory as eight u32 limbs in little-endian order.
#!
#! Inputs:  [w0, w1, w2, w3, out_ptr, ...]
#! Outputs: [...]
#!
#! Where:
#! - `w*` are the felts of the input word. Each felt is split into a low and high 32-bit limb.
#! - `out_ptr` is an element address in memory.
#! - Memory layout after the call: `[w0_lo, w0_hi, w1_lo, w1_hi, w2_lo, w2_hi, w3_lo, w3_hi]`.
#!
#! Cycles: 22
pub proc store_word_u32s_le
    swap u32split
    # => [w1_lo, w1_hi, w0, w2, w3, out_ptr, ...]

    movup.2 u32split
    # => [w0_lo, w0_hi, w1_lo, w1_hi, w2, w3, out_ptr, ...]

    # Store w0 and w1 limbs, then drop them from the stack
    dup.6 mem_storew_le dropw
    # => [w2, w3, out_ptr, ...]

    swap u32split
    # => [w3_lo, w3_hi, w2, out_ptr, ...]

    movup.2 u32split
    # => [w2_lo, w2_hi, w3_lo, w3_hi, out_ptr, ...]

    # Store w2 and w3 limbs at out_ptr+4
    movup.4 add.4 mem_storew_le dropw
    # => [...]
end

# COMPARISON OPERATIONS
#! Returns a boolean indicating whether the input word is [0, 0, 0, 0].
#!
#! Inputs:  [INPUT_WORD]
#! Outputs: [is_empty_word]
#!
#! Where:
#! - INPUT_WORD is the word to compare against [0, 0, 0, 0].
#! - is_empty_word is a boolean indicating whether INPUT_WORD is all zeros.
#!
#! Cycles: 10
pub proc eqz(input: word) -> i1
    eq.0
    repeat.3
        swap eq.0 and
    end
end

#! Returns a boolean indicating whether the input word is [0, 0, 0, 0]. Unlike eqz, this does not
#! consume the inputs.
#!
#! Inputs:  [INPUT_WORD]
#! Outputs: [is_empty_word, INPUT_WORD]
#!
#! Where:
#! - INPUT_WORD is the word to compare against [0, 0, 0, 0].
#! - is_empty_word is a boolean indicating whether INPUT_WORD is all zeros.
#!
#! Cycles: 11
pub proc testz(input: word) -> (i1, word)
    repeat.4
        dup.3 eq.0
    end
    and and and
end
# -------------------------------------------------------------------------------------------------

#! Returns true if LHS is strictly greater than RHS, false otherwise.
#!
#! This compares words using the same ordering as Merkle tree key comparisons.
#!
#! The implementation avoids branching for performance reasons.
#!
#! For reference, this is equivalent to the following Rust function:
#!
#! fn is_word_greater(word1: Word, word2: Word) -> bool {
#!     let mut result = false;
#!     let mut cont = true;
#!
#!     for i in (0..4).rev() {
#!         let gt = word1[i].as_canonical_u64() > word2[i].as_canonical_u64();
#!         let eq = word1[i].as_canonical_u64() == word2[i].as_canonical_u64();
#!         result |= gt & cont;
#!         cont &= eq;
#!     }
#!
#!     result
#! }
#!
#! Inputs:  [RHS, LHS]
#! Outputs: [is_lhs_greater]
#!
#! Cycles: 133
pub proc gt(rhs: word, lhs: word) -> i1
    # Input words are in LE order (word[0] on top)
    # => [r_0, r_1, r_2, r_3, l_0, l_1, l_2, l_3]
    exec.arrange_words_adjacent_le
    # => [l_3, r_3, l_2, r_2, l_1, r_1, l_0, r_0]

    push.1.0
    # => [is_lhs_less, continue, l_3, r_3, l_2, r_2, l_1, r_1, l_0, r_0]

    repeat.4
        movup.3 movup.3
        # => [l_x, r_x, is_lhs_less, continue, <remaining_felts>]

        # check r_x == l_x; if so, we continue
        dup dup.2 eq
        # => [is_felt_eq, l_x, r_x, is_lhs_less, continue, <remaining_felts>]

        movdn.3
        # => [l_x, r_x, is_lhs_less, is_felt_eq, continue, <remaining_felts>]

        # check r_x < l_x
        lt
        # => [is_felt_lt, is_lhs_less, is_felt_eq, continue, <remaining_felts>]

        dup.3 and
        # => [is_felt_lt_if_continue, is_lhs_less, is_felt_eq, continue, <remaining_felts>]

        or movdn.2
        # => [is_felt_eq, continue, is_lhs_less, <remaining_felts>]

        # keeps continue at 1 if the felts are equal
        # sets continue to 0 if the felts are not equal
        and
        # => [continue, is_lhs_less, <remaining_felts>]

        swap
        # => [is_lhs_less, continue, <remaining_felts>]
    end
    # => [is_lhs_less, continue]

    swap drop
    # => [is_lhs_less]
end

#! Returns true if LHS is greater than or equal to RHS.
#!
#! Inputs:  [RHS, LHS]
#! Outputs: [is_lhs_greater_or_equal]
#!
#! Cycles: 130
pub proc gte(rhs: word, lhs: word) -> i1
    exec.lt
    not
end

#! Returns true if LHS is strictly less than RHS, false otherwise.
#!
#! The implementation avoids branching for performance reasons.
#!
#! From an implementation standpoint this is exactly the same as `word::gt` except it uses
#! `lt` rather than `gt`. See its docs for details.
#!
#! Inputs:  [RHS, LHS]
#! Outputs: [is_lhs_lesser]
#!
#! Cycles: 129
pub proc lt(rhs: word, lhs: word) -> i1
    # Input words are in LE order (word[0] on top)
    # => [r_0, r_1, r_2, r_3, l_0, l_1, l_2, l_3]
    exec.arrange_words_adjacent_le
    # => [l_3, r_3, l_2, r_2, l_1, r_1, l_0, r_0]

    push.1.0
    # => [is_lhs_greater, continue, l_3, r_3, l_2, r_2, l_1, r_1, l_0, r_0]

    repeat.4
        movup.3 movup.3
        # => [l_x, r_x, is_lhs_greater, continue, <remaining_felts>]

        # check r_x == l_x; if so, we continue
        dup dup.2 eq
        # => [is_felt_eq, l_x, r_x, is_lhs_greater, continue, <remaining_felts>]

        movdn.3
        # => [l_x, r_x, is_lhs_greater, is_felt_eq, continue, <remaining_felts>]

        # check r_x > l_x
        gt
        # => [is_felt_gt, is_lhs_greater, is_felt_eq, continue, <remaining_felts>]

        dup.3 and
        # => [is_felt_gt_if_continue, is_lhs_greater, is_felt_eq, continue, <remaining_felts>]

        or movdn.2
        # => [is_felt_eq, continue, is_lhs_greater, <remaining_felts>]

        # keeps continue at 1 if the felts are equal
        # sets continue to 0 if the felts are not equal
        and
        # => [continue, is_lhs_greater, <remaining_felts>]

        swap
        # => [is_lhs_greater, continue, <remaining_felts>]
    end
    # => [is_lhs_greater, continue]

    swap drop
    # => [is_lhs_greater]
end

#! Returns true if LHS is less than or equal to RHS, false otherwise.
#!
#! Inputs:  [RHS, LHS]
#! Outputs: [is_lhs_less_or_equal]
#!
#! Cycles: 134
pub proc lte(rhs: word, lhs: word) -> i1
    exec.gt
    not
end

#! Returns true if LHS is exactly equal to RHS, false otherwise.
#!
#! The implementation does not branch, and always performs the same number of comparisons.
#!
#! This is currently equivalent to the eqw instruction.
#!
#! Inputs:  [RHS, LHS]
#! Outputs: [lhs_eq_rhs]
#!
#! Cycles: 13
pub proc eq(rhs: word, lhs: word) -> i1
    # => [l0, l1, l2, l3, r0, r1, r2, r3]

    movup.4 eq swap
    # => [l1, eq, l2, l3, r1, r2, r3]

    movup.4 eq and swap
    # => [l2, eq, l3, r2, r3]

    movup.3 eq and
    # => [eq, l3, r3]

    movdn.2 eq and
    # => [eq]
end

#! Returns true if LHS is exactly equal to RHS, false otherwise. Preserves stack inputs.
#!
#! Like word::eq, the implementation does not branch, and always performs the same number
#! of comparisons.
#!
#! Inputs:  [RHS, LHS]
#! Outputs: [lhs_eq_rhs, RHS, LHS]
#!
#! Cycles: 15
pub proc test_eq(rhs: word, lhs: word) -> (i1, word, word)
    dup.7 dup.4 eq
    dup.7 dup.4 eq and
    dup.6 dup.3 eq and
    dup.5 dup.2 eq and
end

# HELPER PROCEDURES
# -------------------------------------------------------------------------------------------------

#! Arranges LE words for comparison.
#!
#! Inputs:  [r_0, r_1, r_2, r_3, l_0, l_1, l_2, l_3]
#! Outputs: [l_3, r_3, l_2, r_2, l_1, r_1, l_0, r_0]
#!
#! Cycles: 13
proc arrange_words_adjacent_le
    # Get l_3 and r_3 to top (MSB pair)
    movup.7 movup.4 swap
    # => [l_3, r_3, r_0, r_1, r_2, l_0, l_1, l_2]

    # Get l_2 and r_2
    movup.7 movdn.2 movup.5 movdn.3
    # => [l_3, r_3, l_2, r_2, r_0, r_1, l_0, l_1]

    # Get l_1 and r_1
    movup.7 movdn.4 movup.6 movdn.5
    # => [l_3, r_3, l_2, r_2, l_1, r_1, r_0, l_0]

    # Get l_0 and r_0
    movup.7 movdn.6
    # => [l_3, r_3, l_2, r_2, l_1, r_1, l_0, r_0]
end