Skip to content

doc: advice provider layout for recursive verifier #2056

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Al-Kindi-0 wants to merge 4 commits into
base: next
Choose a base branch
from
Draft

doc: advice provider layout for recursive verifier #2056

Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
894aed1
doc: advice provider layout for recursive verifier
Al-Kindi-0 Aug 7, 2025
8fb632d
fix lints
Al-Kindi-0 Aug 7, 2025
31972d8
address comments
Al-Kindi-0 Aug 8, 2025
38e41d8
fix typo
Al-Kindi-0 Aug 11, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
64 changes: 60 additions & 4 deletions stdlib/tests/crypto/stark/verifier_recursive/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,62 @@ pub struct VerifierData {
pub advice_map: Vec<(Word, Vec<Felt>)>,
}

/// Generates advice inputs required for recursive STARK proof verification in Miden VM.
///
/// During the course of its execution, the recursive verifier will make use of non-deterministic
/// advice data through the advice provider.
/// In what follows is a description of the expected layout per component of the advice provider.
/// We also include the expected layout of the operand stack for completness.
///
/// # Operand Stack Layout
///
/// ```
/// | Position | Content | Size (in Felt) | Description |
/// | -------- | ----------------- | -------------- | -------------------------------- |
/// | 0 | grinding_factor | 1 | Proof-of-work difficulty in bits |
/// | 1 | num_queries | 1 | Number of FRI queries |
/// | 2 | trace_length_log2 | 1 | Log2 of execution trace length |
/// ```
///
/// # Advice Stack Layout
///
/// ```
/// | Position | Content | Size (in Felt) | Description |
/// | -------- | ---------------------- | -------------- | ----------------------------------------------------- |
/// | 0 | variable_len_pi_size | 1 | Size of variable length PI in Felt |
/// | 1-n | public_inputs_data | varies | Input/output stacks + Program digest + kernel digests |
/// | n+1-n+4 | aux_randomness | 4 | β = (β₀, β₁), ɑ = (ɑ₀, ɑ₁) |
/// | n+5 | num_kernel_procedures | 1 | Count of kernel procedure digests |
/// | n+6-m | trace_commitments | 4 or 8 | Main/auxiliary trace segment commitments |
/// | m+1-p | constraint_commitment | 4 | Constraint composition commitment |
/// | p+1-p+2 | alpha_deep_placeholder | 2 | Deep composition randomness |
/// | p+3-q | ood_evaluations | varies | Out-of-domain trace and constraint evals |
/// | q+1-r | fri_commitments | varies | FRI layer commitment digests |
/// | r+1-s | fri_remainder_poly | varies | FRI remainder polynomial coefficients |
/// | s+1 | pow_nonce | 1 | Proof-of-work nonce |
Copy link
Contributor

@bobbinth bobbinth Aug 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not for this PR, but a few thoughts on these (specifically in the context of #2045):

It is not yet clear to me how these would get onto the advice stack. Generally, there are two options for accomplishing this:

  1. There could be a specialized event that, based on the data on the operand stack, would identify the relevant data in the advice map. Based on this data it would construct the advice stack.
  2. There would be an entry in the advice map with this data. The key for this entry would be something we can derive deterministically from the data on the operand stack.

Some of the data seems to be specific to Miden VM proofs. For example, num_kernel_procedures is probably not something that's relevant for a generic STARK proof.

It may make sense to remove things like variable_len_pi_size and public_inputs_data from the advice stack. Instead, they these could be loaded onto the advice stack using their commitments (via the adv.push_mapvaln instruction). For example, if the commitment to public inputs is on the operand stack, and there is an entry in the advice map for PUB_INPUTS_COMMITMENT |-> [PUB INPUTS DATA], we could load the public inputs onto the advice stack from within MASM.

Lastly, I wonder if it is possible to have the data on the advice stack basically be the transcript of the interaction between the prover and the verifier. Then, the verifier would be able to read it off the advice stack, absorb it into the hasher state, and then, at the end of proof verification, compare it to the transcript "commitment" that it may get via regular inputs (or in some other way).

Copy link
Contributor Author

@Al-Kindi-0 Al-Kindi-0 Aug 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not for this PR, but a few thoughts on these (specifically in the context of #2045):

It is not yet clear to me how these would get onto the advice stack. Generally, there are two options for accomplishing this:

1. There could be a specialized event that, based on the data on the operand stack, would identify the relevant data in the advice map. Based on this data it would construct the advice stack.

Could you elaborate more here? Especially the "identify the relevant data" part?

2. There would be an entry in the advice map with this data. The key for this entry would be something we can derive deterministically from the data on the operand stack.

Indeed, this would be similar to the proposal in #2045 , where this is derived from the public inputs, AIR commitment and protocol identifier.

Some of the data seems to be specific to Miden VM proofs. For example, num_kernel_procedures is probably not something that's relevant for a generic STARK proof.

Not really, num_kernel_procedures is nothing but the number of messages/interactions in the first (and only) group/table of variable length public inputs. So as part of the transformation from Proof to its parts in the advice provider, we have to count the number of messages per table in the variable length public inputs and add this number to the advice stack.

It may make sense to remove things like variable_len_pi_size and public_inputs_data from the advice stack. Instead, they these could be loaded onto the advice stack using their commitments (via the adv.push_mapvaln instruction). For example, if the commitment to public inputs is on the operand stack, and there is an entry in the advice map for PUB_INPUTS_COMMITMENT |-> [PUB INPUTS DATA], we could load the public inputs onto the advice stack from within MASM.

I think it is cleaner to keep it here as it doesn't make sense, neither conceptually nor performance wise, to commit to them together with the public inputs.

Lastly, I wonder if it is possible to have the data on the advice stack basically be the transcript of the interaction between the prover and the verifier. Then, the verifier would be able to read it off the advice stack, absorb it into the hasher state, and then, at the end of proof verification, compare it to the transcript "commitment" that it may get via regular inputs (or in some other way).

Not sure I follow completely. Is the intention here to have the data on the advice stack be exactly the one, without any for example out of order advice data, resulting from the interactions between prover and verifier?
If so, then I think this is a significant limitation and in my mind unnecessary.

/// ```
///
/// # Advice Merkle Store Content
///
/// ```
/// | Merkle trees |
/// | ---------------------------- |
/// | Main trace segment tree |
/// | Auxiliary trace segment tree |
/// | Constraint composition tree |
/// | FRI layers commitment trees |
/// ```
///
/// # Advice Map Layout
///
/// ```
/// | Key (Word) | Value (Vec<Felt>) |
/// | -------------------------------------------------------- | ----------------------------------- |
/// | Leaf hash of main trace segment tree at query index | Main trace evaluations |
/// | Leaf hash of auxiliary trace segment tree at query index | Auxiliary trace evaluations |
/// | Leaf hash of constraint composition tree at query index | Constraint evaluations |
/// | FRI layer evaluations at folded query index | FRI codeword evaluations on a coset |
/// ```
pub fn generate_advice_inputs(
proof: Proof,
pub_inputs: <ProcessorAir as Air>::PublicInputs,
Expand All @@ -39,9 +95,9 @@ pub fn generate_advice_inputs(
// note that since we are padding the fixed length inputs, in our case the program digest, to
// be double-word aligned, we have to subtract `2 * WORD_SIZE` instead of `WORD_SIZE` for
// the program digest
let digests_elements = num_elements_pi - MIN_STACK_DEPTH * 2 - 2 * WORD_SIZE;
assert_eq!(digests_elements % WORD_SIZE, 0);
let num_kernel_procedures_digests = digests_elements / (2 * WORD_SIZE);
let variable_len_pi_size = num_elements_pi - MIN_STACK_DEPTH * 2 - 2 * WORD_SIZE;
assert_eq!(variable_len_pi_size % WORD_SIZE, 0);
let num_kernel_procedures_digests = variable_len_pi_size / (2 * WORD_SIZE);

// we need to provide the following instance specific data through the operand stack
let initial_stack = vec![
Expand All @@ -53,7 +109,7 @@ pub fn generate_advice_inputs(
// build a seed for the public coin; the initial seed is the hash of public inputs and proof
// context, but as the protocol progresses, the coin will be reseeded with the info received
// from the prover
let mut advice_stack = vec![digests_elements as u64];
let mut advice_stack = vec![variable_len_pi_size as u64];
let mut public_coin_seed = proof.context.to_elements();
public_coin_seed.extend_from_slice(&pub_inputs_elements);

Expand Down