miden-stdlib 0.19.1

Miden VM standard library
Documentation
use.std::crypto::stark::constants
use.std::crypto::hashes::rpo
use.std::crypto::stark::random_coin

#! Loads the execution trace and the quotient trace evaluation frames.
#! 
#! This also computes Q^z(alpha) and Q^gz(alpha) where:
#!
#! Q^z(alpha) = (q_z_0, q_z_1) = \sum_{i=0}^{n+m+l} S_i * alpha^i
#!
#! and 
#!
#! Q^gz(alpha) = (q_gz_0, q_gz_1) = \sum_{i=0}^{n+m+l} T_i * alpha^i 
#!
#! where:
#!
#! 1. n, m and l are the widths of the main segment, auxiliary segment and constraint composition
#!    traces, respectively.
#! 2. S_i are the evaluations of columns in the main segment, auxiliary segment and constraint
#!    composition at the the out-of-domain point z.
#! 3. T_i are the evaluations of columns in the main segment, auxiliary segment and constraint
#!    composition at the the out-of-domain point gz.
#! 4. alpha is the randomness used in order to build the DEEP polynomial.
#!
#! Q^z(alpha) and Q^gz(alpha) is then stored, as a word, at OOD_FIXED_TERM_HORNER_EVALS_PTR
#!
#! Inputs:  []
#! Outputs: []
export.load_and_horner_eval_ood_frames
    # --- Load the random challenge used in computing the DEEP polynomial -----

    # We use this challenge to compute the constant terms needed in the computation of the DEEP
    # queries. Although this challenge is generated only after all the OOD evaluations are received
    # by the verifier, we use non-determinism to generate it before doing so. This is done so that
    # we can hash, memory store and Horner evaluate in parallel.
    # The check for the correctness of the use of this non-determinism is checked in
    # `std::crypto::stark::random_coin::generate_deep_composition_random_coefficients`
    
    ## Load the random challenge non-deterministically
    adv_push.2
    # => [alpha_1, alpha_0]

    # Save the random challenge
    dup.1 dup.1
    exec.constants::deep_rand_alpha_nd_ptr mem_storew_be
    # => [Y]

    # --- Compute Q^z(alpha) --------------------------------------------------

    ## 1) Set up the stack for `horner_eval_ext` to compute Q^z(alpha)

    ### a) Set up the initial accumulator and the pointers to alpha and a pointer to some memory
    ###    region to which we save the OOD.
    push.0.0
    exec.constants::deep_rand_alpha_nd_ptr
    exec.constants::ood_evaluations_ptr
    # => [ood_evaluations_ptr, deep_rand_alpha_ptr, 0, 0, Y]
    # => [U, Y]

    ## 2) Process the fully aligned OOD `current` evaluations at z of the execution trace
    ##    and constraints polynomials evaluations.
    ##    Note that, by the assumption on the widths of committed traces, the capacity portion
    ##    of the sponge state is always initialized to `[0, 0, 0, 0]`.

    ### a) Set up the hasher state
    padw padw     
    # => [ZERO, 0, 0, 0, 0, U, Y]
    movupw.3
    # => [Y, ZERO, 0, 0, 0, 0, U]

    ### b) Process the `current` OOD evaluations
    exec.process_row_ood_evaluations
    # => [Y, Y, C, ood_frame_ptr, alpha_ptr, acc1, acc0]

    ### c) Save -Q^z(alpha)
    swapw.3
    # => [ood_frame_ptr, alpha_ptr, acc1, acc0, Y, C, Y]
    movup.3 neg
    movup.3 neg
    push.0.0
    exec.constants::ood_fixed_term_horner_evaluations_ptr mem_storew_be
    # => [0, 0, -acc1, -acc0, ood_frame_ptr, alpha_ptr, Y, C, Y]

    # --- Compute Q^gz(alpha) -------------------------------------------------

    # Reset the Horner accumulator
    movdn.5 movdn.5 drop drop
    # => [ood_frame_ptr, alpha_ptr, 0, 0, Y, C, Y]

    # Load the `next` trace polynomials OOD evaluations.
    swapw.3
    # => [Y, Y, C, ood_frame_ptr, alpha_ptr, 0, 0]
    exec.process_row_ood_evaluations
    # => [Y, D, C, ood_frame_ptr, alpha_ptr, acc1, acc0]

    # Reseed with the digest of the OOD evaluations
    swapw
    exec.random_coin::reseed
    # => [Y, C, ood_frame_ptr, alpha_ptr, acc1, acc0]

    # Negate Q^z(alpha) and save it
    dropw dropw drop drop
    # => [acc1, acc0]
    neg
    exec.constants::ood_fixed_term_horner_evaluations_ptr add.3 mem_store
    # => [acc0]
    neg
    exec.constants::ood_fixed_term_horner_evaluations_ptr add.2 mem_store
    # => []
end

#! Processes the out-of-domain (OOD) evaluations of all committed polynomials.
#!
#! Takes as input an RPO hasher state and a pointer, and loads from the advice provider the OOD
#! evaluations and stores at memory region using pointer `ptr` while absorbing the evaluations
#! into the hasher state and simultaneously computing a random linear combination using Horner
#! evaluation.
#!
#! Inputs:  [R2, R1, C, ptr, acc1, acc0]
#! Outputs: [R2, R1, C, ptr, acc1`, acc0`]
proc.process_row_ood_evaluations
    exec.constants::get_procedure_digest_process_row_ood_evaluations_ptr dynexec
end