pub mod aux_trace
pub mod constraints_eval
pub mod deep_queries
pub mod ood_frames
pub mod public_inputs
use miden::core::stark::verifier
use miden::core::stark::constants
# Acceptable security parameters for Miden VM proof verification.
# These define the security policy enforced by `assert_acceptable_options`.
# If the protocol security level changes, update these constants accordingly.
const ACCEPTABLE_NUM_QUERIES = 27
const ACCEPTABLE_QUERY_POW_BITS = 16
const ACCEPTABLE_DEEP_POW_BITS = 12
const ACCEPTABLE_FOLDING_POW_BITS = 4
# RELATION_DIGEST = hash(PROTOCOL_ID, CIRCUIT_COMMITMENT).
# This is a compile-time constant computed once per AIR that binds the Fiat-Shamir
# transcript to the relation (AIR structure + fix protocol parameter choices).
#
# PROTOCOL_ID (defined in circuit_evaluation.rs) implicitly covers every hardcoded
# protocol choice: hash function, field, blowup factor, FRI folding factor, coset
# offset, max remainder degree, etc. It must be bumped when any of these change.
# CIRCUIT_COMMITMENT covers the AIR constraints (via the encoded ACE circuit hash).
const RELATION_DIGEST_0 = 17246763836728246237
const RELATION_DIGEST_1 = 9838047215024765106
const RELATION_DIGEST_2 = 15366705014579132635
const RELATION_DIGEST_3 = 14157638374955997968
#! Loads security parameters from the advice stack and stores them in memory.
#!
#! The advice stack must contain, in order:
#! [num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits]
#!
#! After this procedure, all four values are available in memory via the corresponding
#! accessors in constants.masm (get_number_queries, get_query_pow_bits, etc.).
#!
#! Input: [...]
#! Output: [...]
proc load_security_params
adv_push exec.constants::set_number_queries
adv_push exec.constants::set_query_pow_bits
adv_push exec.constants::set_deep_pow_bits
adv_push exec.constants::set_folding_pow_bits
end
#! Asserts that the security parameters in memory meet the Miden VM security policy.
#!
#! Input: [...]
#! Output: [...]
proc assert_acceptable_options
exec.constants::get_number_queries
push.ACCEPTABLE_NUM_QUERIES assert_eq.err="num_queries does not match acceptable security policy"
exec.constants::get_query_pow_bits
push.ACCEPTABLE_QUERY_POW_BITS assert_eq.err="query_pow_bits does not match acceptable security policy"
exec.constants::get_deep_pow_bits
push.ACCEPTABLE_DEEP_POW_BITS assert_eq.err="deep_pow_bits does not match acceptable security policy"
exec.constants::get_folding_pow_bits
push.ACCEPTABLE_FOLDING_POW_BITS assert_eq.err="folding_pow_bits does not match acceptable security policy"
end
#! Verifies a STARK proof attesting to the correct execution of a program in the Miden VM.
#!
#! Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are
#! loaded from the advice stack, validated against the acceptable security policy, and
#! stored in memory for use by the generic verifier.
#!
#! - The public inputs are composed of the input and output stacks, of fixed size equal to 16, as
#! well as the program and the kernel procedures digests.
#! - There are two trace segments, main and auxiliary. It is assumed that the main trace segment
#! is 73 columns wide while the auxiliary trace segment is 8 columns wide. Note that we pad the main
#! trace to the next multiple of 8.
#! - The OOD evaluation frame is composed of two concatenated rows, current and next, each composed
#! of 73 elements representing the main trace portion and 8 elements for the auxiliary trace one.
#! Note that, due to the padding of the main trace columns, the number of OOD evaluations per row
#! is 80 for the main trace.
#!
#! Inputs: [log(core_trace_length), log(chiplets_trace_length)]
#! Outputs: []
pub proc verify_proof
# --- Load and validate security parameters from advice stack ---
exec.load_security_params
exec.assert_acceptable_options
# => [log(core_tl), log(chiplets_tl)]
# --- Get constants -------------------------------------------------------
# Push RELATION_DIGEST below the two log heights.
push.RELATION_DIGEST_3.RELATION_DIGEST_2.RELATION_DIGEST_1.RELATION_DIGEST_0
# => [rd0, rd1, rd2, rd3, log_core, log_chiplets]
# Bring log_core to top, then log_chiplets underneath, restoring the verifier signature.
movup.4
# => [log_core, rd0, rd1, rd2, rd3, log_chiplets]
movup.5
# => [log_chiplets, log_core, rd0, rd1, rd2, rd3]
swap
# => [log_core, log_chiplets, rd0, rd1, rd2, rd3]
# --- Load the digests of all dynamically invoked procedures --------------
procref.deep_queries::compute_deep_composition_polynomial_queries
procref.constraints_eval::execute_constraint_evaluation_check
procref.ood_frames::process_row_ood_evaluations
procref.public_inputs::process_public_inputs
procref.aux_trace::observe_aux_trace
# => [D0, D1, D2, D3, D4, log_core, log_chiplets, rd0, rd1, rd2, rd3]
# --- Call the core verification procedure from `core-lib` ------------------
exec.verifier::verify
# => [...]
end