Skip to content
Draft
Changes from 2 commits
Commits
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
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 | β = (β₀, β₁), ɑ = (ɑ₀, ɑ₁) (filled later) |
Copy link
Contributor

Choose a reason for hiding this comment

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

What does "filled later" mean here? (and same question for line 55 below).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

What I was trying to say, in a succinct way, is that these values are out-of-order with respect to the interaction transcript. Thus, in the advice tape, we push place holders for these values and only later on in the interaction can we fill these place holders with the appropriate values.
Probably "filled late" is just confusing without enough context, so I have just removed it

Copy link
Contributor

Choose a reason for hiding this comment

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

What does "placeholder" mean in this context? My understanding was that we put real values onto the advice stack, but then use the "optimistically" - and only later confirm that the values we used were indeed derived correctly. Or does it mean something else?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is used to signify that it is an out-of-sequence value on the stack that is filled later on in the interaction.
This is probably just confusing and not informative, so I have removed it

Copy link
Contributor

Choose a reason for hiding this comment

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

Ah - so it meant that we insert these values into the advice stack later (e.g., using something adv.push_mapval instruction)?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Just on the Rust size. We basically, push say a [0 ,0] and record the index before this push. Later on when we can generate the random challenge, we can do something like advice_tape[index] = alpha_0 and advice_tape[index + 1] = alpha_1.
Overall, this is just a Rust implementation detail i.e., it could be done differently

/// | 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 (filled later) |
/// | 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 |
/// ```
///
/// # 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>) |
/// | ------------------------------ | ----------------------------------- |
/// | Query index | Main trace evaluations |
/// | Query index | Auxiliary trace evaluations |
/// | Query index | Constraint evaluations |
/// | FRI layer (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