diff --git a/.cursor/rules/air-pv.mdc b/.cursor/rules/air-pv.mdc new file mode 100644 index 000000000..6c7e5896c --- /dev/null +++ b/.cursor/rules/air-pv.mdc @@ -0,0 +1,42 @@ +--- +description: +globs: +alwaysApply: false +--- + +Following the structure of [pcs-shots.mdc](mdc:.cursor/rules/pcs-shots.mdc), + we describe the steps of Prover and Verifier for AIR constraints consis in this document. +We present each step marked with P or V depending on whether Prover or Verifier performs the step. +In terms of interaction with the challenger, + steps with the same numbers correpond to the dual steps between Prover and Verifier + (e.g. if a step 3P correponds to `pcs.open`, then 3V will correspond to `pcs.verify`), + steps without a P or V correpond to both Prover and Verifier doing the same thing. + + +1: Compute `trace_domain` and `quotient_domain`. + +2P: Commit to given `trace`. + +3: Include the trace commitment, public values and logarithm of trace degree in transcript. + +4P. Evaluate the trace on quotient domain. + +5. Sample challenge `alpha` from transcript. + +6P. Compute the values of quotient on all of quotient domain (using parallel SIMD-enabled loop), using AIR constraints as `Q(X) = C(X) / Z_{quotient_domain}(X)` (where `C(X)` is the folded constraints). + +7P. Split the quotient polynomial into chunks, commit to the chunks. + +8. Include the commitment to quotient chunks in the transcript. + +9. Sample challenge `zeta` and compute `zeta_next`. + +10P. Open the trace at points `zeta` and `zeta_next`, and quotient chunks at `zeta`. + +10V. Verify the openings from step 10P. + +11V. Reconstruct the value of quotient at `zeta` from the opening values. + +12V. Compute the value of folded constraints polynomial at `zeta` using the opened values. + +13V. Ensure that quotient value computed from folded constraints matches the one reconstructed from chunks. diff --git a/.cursor/rules/pv-steps.mdc b/.cursor/rules/pv-steps.mdc new file mode 100644 index 000000000..7474e1304 --- /dev/null +++ b/.cursor/rules/pv-steps.mdc @@ -0,0 +1,810 @@ +--- +description: testgjgj +globs: +alwaysApply: false +--- + +You are assisting the user in writing ZK code using Plonky3 library. +The user will ask you to write code snippet by snippet with each prompt. +Below are given "few shots" examples for the different kinds of prompts you could get, + and the ideal responses expected from you. +When asked on actual prompts, use the examples to satisfy it to the best of your ability. +Each example consists of four sections: + +1. Prompt: what the user has asked, with optional clarifications given in brackets (not part of user's direct speech). +2. Inputs: what varibles this prompt expects to find in context. + Some of such variables may be directly referenced in the user's prompt (e.g. "do something with `t`" means `t` is such input), + while others may be implicit and you must find them by looking at their relationship to the things referred to by the prompt. + Some of such variables must be initialized if they are not yet present in context, + in that case "Inputs" section will explain how to initialize them + (if you initialize them in your generated code, keep them around for use in future). +3. Response: the output ideally expected from you. + It will always contain some snippet of Rust code that you must insert into user's program. + There may be more than one snippet given with some instructions on how to choose one of them or assemble them into what you insert into user's program. + Feel free to complement your reponse with comments or explanations of your reasoning when you respond to the user. +4. Outputs: the values inroduced into context by "Response" Rust code that were the goal of running that code. + Make sure you produce them and keep them in the context, + but also take note of them for future queries since they are very likely to serve as "Inputs" to the future prompts. + In the descriptions below, the Outputs may be supplied with comments explaining their purpose; + use that info to detect when these Output will need to serve as Inputs to the other code generation requests. + +The following are the values that should be available for all of the examples below. +I.e. you can treat them as global inputs for all of the examples. +In practice, these are usually passed as arguments to the Prover function or initialized at the very top of Prover to make them available to all of the Prover logic. + +```rust +config: &SC, + where SC: StarkGenericConfig +// must be given as an argument to the Prover function, never initialize challenger inside theProver +challenger: &mut Challenger +// the following may be initialized in your response if not already present +let pcs = config.pcs(); +``` + +One type synonym we will use here is + +```rust +type Pcs = SC::Pcs as Pcs +``` + +[config.rs](mdc:uni-stark/src/config.rs) +[lib.rs](mdc:challenger/src/lib.rs) +[pcs.rs](mdc:commit/src/pcs.rs) + +## Example: Committing to Trace + +### Prompt + +Commit to the trace (aka witness) `trace: RowMajorMatrix>`. + +[dense.rs](mdc:matrix/src/dense.rs) + +### Inputs + +These values are expected to be in context. + +```rust +let trace = // ... +let trace_domain = pcs.natural_domain_for_degree(degree); +let degree = trace.height(); +let log_degree = log2_strict_usize(degree); +``` + +### Response + +```rust +let (trace_commit, trace_data) = pcs.commit(vec![(trace_domain, trace)]); +let trace_ix = 0; // this is the index of (trace_domain, trace) inside the vector passed to pcs.commit +``` + +[pcs.rs](mdc:commit/src/pcs.rs) + +### Outputs + +The `trace_commit`, `trace_data`, `trace_ix` are the main results of this operation. + + +## Example: Computing Quotient Domain + +### Prompt: + +Initialize the quotient domain for trace `trace: RowMajorMatrix>`. + +### Inputs + +```rust +let constraint_degree = // maximum degree of the constraints that define the quotient, this highly depends on the statement the user is proving and the user must supply you with enough info to determine it +// The following may be initialized if not already present +let log_quotient_degree = log2_ceil_usize(constraint_degree - 1); +let degree = trace.height(); +let log_degree = log2_strict_usize(degree); +``` + +### Response + +```rust +let quotient_domain = + trace_domain.create_disjoint_domain(1 << (log_degree + log_quotient_degree)); +``` + +### Outputs + +`quotient_domain` + + +## Example: Evaluating Trace on quotient domain + +### Prompt + +Evaluate the previously committed trace given by `trace_data: Pcs::ProverData` on domain `d :: Pcs::Domain`. + +(Commonly used domain for this operation is the quotient domain.) + +### Inputs + +```rust +let trace_data = // obtained by committing to the trace +let trace_ix = // index of the trace in the evaluations vector passed to `pcs.commit` when obtaining `trace_data` +let d = // domain; very often we will use d = quotient_domain from the previous example +``` + +### Response + +```rust +let trace_on_d = pcs.get_evaluations_on_domain(&trace_data, ix, d); +``` + +### Outputs + +`trace_on_d` + + +## Sample a challenge + +### Prompt + +Sample a challenge `alpha`. + +### Inputs + +None. + +### Response + +```rust +let alpha: SC::Challenge = challenger.sample_ext_element(); +``` + +### Outputs + +`alpha` + +## Example: observe a value with transcript + +### Prompt + +Observe (or "include in transcript") `x`. + +### Inputs + +`x` + +### Response + +One of the following: + +`challenger.observe(x)`, `challenger.observe_slice(x)`, or `challenger.observe_ext_element(x)` +depending on the type of `x` and with appropriate borrowing/cloning. + +If the value to be observed is a Rust builtin integer type like `usize`, + convert it to `Val` appropriately. +For example, `i: usize` can be observed with `challenger.observe(Val::::from_canonical_usize(i))`. + +Comment: at the beginnging of a protocol (before sampling any pseudorandom values from the transcript), + one will typically observe `trace_commit` value + together some other public data that indentifes the instance; + so that all the future randomness obtained from challenger depends on this data. +For example, `public_values: &Vec>` (public inputs of the constraint system, aka instance) + and `log_degree = log2_strict_usize(trace.height())` should, when possible, + be included in the transcript together with the `trace_commit`: + +```rust +challenger.observe(trace_commit.clone()); +challenger.observe(Val::::from_canonical_usize(log_degree)); +challenger.observe_slice(public_values); +``` + +### Outputs + +None. + + +## Example: Break quotient values into chunks + +### Prompt + +Break down `quotient_values: Vec` evaluated on `quotient_domain: Pcs::Domain` into chunks. + +### Inputs + +```rust +let quotient_domain = // ...; +let quotient_values = // values of quotient polynomial on quotient_domain +``` + +### Response + +```rust +let quotient_flat = RowMajorMatrix::new_col(quotient_values).flatten_to_base(); +let quotient_chunks = quotient_domain.split_evals(quotient_degree, quotient_flat); +let quotient_chunks_domains = quotient_domain.split_domains(quotient_degree); +``` + +[dense.rs](mdc:matrix/src/dense.rs) [domain.rs](mdc:commit/src/domain.rs) + +### Outputs + +`quotient_chunks`, `quotient_chunks_domains` + + +## Commit to quotient chunks + +### Prompt + +Commit to `quotient_chunks` + +### Inputs + +```rust +let (quotient_chunks_domains, quotient_chunks) = // results of breaking down the quotient evaluations into chunks +``` + +### Response + +```rust +use itertools::{izip}; + +let (quotient_chunks_commit, quotient_chunks_data) = pcs.commit(izip!(quotient_chunks_domains, quotient_chunks).collect_vec()) +``` + +[pcs.rs](mdc:commit/src/pcs.rs) + + +## Example: open the values that connect trace to the quotient + +### Prompt + +Open the values that connect trace to the quotient, where the committed trace is defined by `trace_data` and committed quotient chunks are defined by `quotient_chunks_data`. + +### Inputs + +`trace_data` and `quotient_chunks_data` obtained (earlier) with calls like below. + +```rust +let (trace_commit, trace_data) = pcs.commit(vec![(trace_domain, trace)]); +let (quotient_chunks_commit, quotient_chunks_data) = pcs.commit(izip!(quotient_chunks_domains, quotient_chunks).collect_vec() +``` + +### Response + +```rust +// sample the challenge +let zeta: SC::Challenge = challenger.sample(); +let zeta_next = trace_domain.next_point(zeta).unwrap(); + +// open the values +let (opened_values, opening_proof) = pcs.open( + vec![ + (&trace_data, vec![vec![zeta, zeta_next]]), + ( + "ient_chunks_data, + // open every chunk at zeta + (0..quotient_degree).map(|_| vec![zeta]).collect_vec(), + ), + ], + challenger, +); + +// extract the values into variables with descriptive names +let trace_local_value = opened_values[0][0][0].clone(); +let trace_next_value = opened_values[0][0][1].clone(); +let quotient_chunks_values = opened_values[1].iter().map(|v| v[0].clone()).collect_vec(); +``` + +[pcs.rs](mdc:commit/src/pcs.rs) [proof.rs](mdc:uni-stark/src/proof.rs) + +The above opens only `zeta` and `zeta_next` points of trace + because we assume that a constraint may look at at most one row ahead of the current one. +I.e. a constraint polynomial may only depend on `t_w(X)` and `t_w(g * X)`, + where `t_w(X)` is the polynomial encoded by the `w`-th column of the trace + and `g` is the generator of the trace domain. +If one needs constraints that also look further, say, at `t_w(g^2 * X)`, + one would also need to open `trace_domain.next(zeta_next).unwrap()`. + +The indices used for extraction in the last lines follow + the structure of arguments to `pcs.commit` that obtained the `trace_data` and `quotient_chunks_data`. +If `v` is the vector passed as first argument to `let opened_values = pcs.open(v, challenger)` in the response above, + then `opened_values[i][j][k][l]` is the value of polynomial numer `l` from commitment data `v[i].0` + (i.e. the column `l` from the matrix that `v[i].0` resulted from) + at the point `(v[i].1)[j][k]`. +So when we take `opened_values[0][0][0]`, + this corresponds to the vector of evaluations of all trace polynomials (one polynomial per register) + on point `zeta`; + similarly, `opened_values[0][0][1]` are the evaluations of the same polynomials at point `zeta_next`. +And `opened_values[1][j][0][l]` is the evaluation of polynomial number `l` from chunk number `j` on point `zeta`; + this way `quotient_chunks_values[j] = opened_values[1][j][0]` is the two-dimensional + matrix with evaluations of all polynomials of chunk `j` on `zeta`. + +### Outputs + +`opening_proof`, `trace_local_value`, `trace_next_value`, `quotient_chunks_values` + + +## Example: (Verifier) verify opened points from the prover + +This should be done in Verifier, + symmetrically + (in terms of their interaction with the challenger) + to the Prover opening the values. +Prover's `opened_values` and `opening_proof` should be included + in the (non-interactive) proof which is then passed as an argument + to the verifier and made available to this prompt. + +### Prompt + +Verify that `opening_proof` correcly certifies that `opened_values` + (corresponding to `trace` and `quotient_chunks` evaluations in randomly chosen challenge points) + are correct. + +### Inputs + +```rust +// Commitments to the trace and quotient chunks, computed by the Prover and +// provided to Verifier through the proof +let trace_commit: Pcs::Commitment = // +let quotient_chunks_commit: Pcs::Commitment = // + +// The evaluation domains for trace and quotient, computed (deterministically) +// by both Prover and Verifier +let trace_domain: Pcs::Domain = // +let quotient_chunks_domains: Pcs::Domain = // + +// The challenge sampled from transcript (same for Prover and Verifier) and its +// next value (with respect to trace domain generator) +let zeta: Challenge = // +let zeta_next: Challenge = // + +// Values opened by the Prover and provided to Verifier as part of the proof +let trace_local_value: Vec = // +let trace_next_value: Vec = // +let quotient_chunks_values: Vec> = // + +// Opening proof for the values above, produced by the Prover and provided to +// verifier as part of the Proof +let opening_proof: Pcs::Proof = // +``` + +### Response + +```rust +pcs.verify( + vec![ + ( + trace_commit.clone(), + vec![( + trace_domain, + vec![ + (zeta, trace_local_value.clone()), + (zeta_next, trace_next_value.clone()), + ], + )], + ), + ( + quotient_chunks_commit.clone(), + quotient_chunks_domains + .iter() + .zip("ient_chunks_values) + .map(|(domain, values)| (*domain, vec![(zeta, values.clone())])) + .collect_vec(), + ), + ], + opening_proof, + challenger, +) +.map_err(VerificationError::InvalidOpeningArgument)?; +``` + +The order of elements in the vector passed as the first argument + must match the order of elements passed by Prover to `psc.open` + when it obtained the `opening_proof`. + +### Outputs + +None. + +## Example: (Verifier) compute Lagrange selectors in a point + +### Prompt + +Calculate Lagrange selectors for `trace_domain: Domain` on `zeta: Challenge`. + +### Inputs + +```rust +let trace_domain = pcs.natural_domain_for_degree(degree); +let zeta: Challenge = // challenge sampled from transcript +// where: +let degree = trace.height(); +// for our `trace` +``` + +### Response + +```rust +let sels = trace_domain.selectors_at_point(zeta); +``` + +### Outputs + +`sels` + + +## Example: (Prover) compute Lagrange selectors on domain + +### Prompt + +Calculate Lagrange selectors for `trace_domain: Domain` on `quotient_domain: Domain`. + +### Inputs + +```rust +let trace_domain = pcs.natural_domain_for_degree(degree); +let quotient_domain = + trace_domain.create_disjoint_domain(1 << (log_degree + log_quotient_degree)); +// where: +let degree = trace.height(); +let log_degree = log2_strict_usize(degree); +let log_quotient_degree = log2_ceil_usize(constraint_degree - 1); +// for our `trace` and `constraint_degree` +``` + +### Response + +```rust +let sels = trace_domain.selectors_on_coset(quotient_domain); +``` + +Alternatively, if we intend to work with packed slices of these selectors, + they may need to be padded with dummy values to the packing width + (the dummy values will be discarded later, we only need them to avoid having to check extra conditions in the calculations on packed `sels` slices): + +```rust +let mut sels = trace_domain.selectors_on_coset(quotient_domain); +// We take PackedVal::::WIDTH worth of values at a time from a quotient_size slice, so we need to +// pad with default values in the case where quotient_size is smaller than PackedVal::::WIDTH. +for _ in quotient_size..PackedVal::::WIDTH { + sels.is_first_row.push(Val::::default()); + sels.is_last_row.push(Val::::default()); + sels.is_transition.push(Val::::default()); + sels.inv_zeroifier.push(Val::::default()); +} +let sels = sels; +``` + +[domain.rs](mdc:commit/src/domain.rs) + +### Outputs + +`sels`. +Here `sels.is_first_row`, `sels.is_last_row` and `sels.is_transition` are used when calculating the constraint polynomial, + and `sels.inv_zeroifier` is multiplied by constraint polynomial to obtain quotient. + + +## Example: (Prover) efficient parallel and SIMD-enabled quotient evaluation + +This is only needed on Prover, + since Prover has to evaluate quotient on all of quotient domain. +Verifier evalues quotient only at a chosen challenge point, + therefore, it doesn't need parallelism or SIMD. + +### Prompt + +Implement a loop for quotient evalution + (that uses multiple parallel threads, and and packs the values for SIMD processing). +Leave the placeholder in the place where actual constraint expression should be, + but prepare all the (packed) values necessary for constraint expression + (such as selectors, two main matrix rows, alpha powers, public values). + +### Inputs + +```rust +let public_values: &Vec> = // public inputs of the constraint system (aka instance), given as an argument to prover and verifier + +let trace_domain: Domain = //trace domain +let quotient_domain: Domain = //quotient domain + +let sels = // Lagrange selectors precomputed as shown above with padding to PackedVal::::WIDTH +let trace_on_quotient_domain = // trace compute on quotient domain as shown above + +let qdb = log2_strict_usize(quotient_domain.size()) - log2_strict_usize(trace_domain.size()); +// next_step is the degree multiplicity of `trace_domain` generator with respect to `quotient_domain` generator, +// i.e. `g_trace = g_quotient^(next_step). +// we use it below to calculate what "next row" of trace in trace domain means on quotient domain. +let next_step = 1 << qdb; + +let alpha: SC::Challenge = // challenge sampled from transcript +let constraint_count = // number of constraints +// powers of alpha +let mut alpha_powers = alpha.powers().take(constraint_count).collect_vec(); +alpha_powers.reverse(); +let alpha_powers = alpha_powers; +``` + +### Response + +```rust +let result: Vec = (0..quotient_size) + .into_par_iter() + .step_by(PackedVal::::WIDTH) + .flat_map_iter(|i_start| { + let i_range = i_start..i_start + PackedVal::::WIDTH; + + let is_first_row = *PackedVal::::from_slice(&sels.is_first_row[i_range.clone()]); + let is_last_row = *PackedVal::::from_slice(&sels.is_last_row[i_range.clone()]); + let is_transition = *PackedVal::::from_slice(&sels.is_transition[i_range.clone()]); + let inv_zeroifier = *PackedVal::::from_slice(&sels.inv_zeroifier[i_range.clone()]); + + let main = RowMajorMatrix::new( + trace_on_quotient_domain.vertically_packed_row_pair(i_start, next_step), + width, + ); + + // PLACEHOLDER: compute the constraints value here using + // `main`, the `is_first_row`, `is_last_row`, `is_transition`, `inv_zeroifier` selectors, + // as well as `alpha_powers` and `public_values`. + let constraints: PackedChallenge = _; + + // quotient(x) = constraints(x) / Z_H(x) + let quotient = constraints * inv_zeroifier; + + // "Transpose" D packed base coefficients into WIDTH scalar extension coefficients. + (0..core::cmp::min(quotient_size, PackedVal::::WIDTH)).map(move |idx_in_packing| { + SC::Challenge::from_base_fn(|coeff_idx| { + quotient.as_base_slice()[coeff_idx].as_slice()[idx_in_packing] + }) + }) + }) + .collect(); +``` + +## Example: (Prover) AIR constraint evaluation with constraint folder + +The prompt should be invoked from inside a parallel loop traversing and packing the points of quotient domain for SIMD processing. +All inputs and outputs of this prompt are per-iteration, i.e. correspond to packed evaluations of polynomials on `PackedVal::::WIDTH` points on the quotient domain. +The response of this prompt should go in place of PLACEHOLDER from the previous example, + and most of the inputs described here are shown how to precompute in the previous example. + +### Prompt + +Evaluate AIR constraints described by `air` on trace values given by (two column) matrix `main`, + using `public_values` instance. +You can use precomputed selectors `inv_zeroifier`, `is_transition`, `is_last_row`, `is_first_row`, as well as `alpha_powers`. + +### Inputs + +```rust +let public_values: &Vec> = // argument of prover and verifier, public instance + +let air: &A = // argument of prover and verifier, describes constraint system + where Air>> + for<'a> Air> +let symbolic_constraints = get_symbolic_constraints::, A>(air, 0, public_values.len()); +let constraint_count = symbolic_constraints.len(); + +let alpha_powers: = // `constraint_count` number of powers of challenge `alpha: SC::Challenge` + +// the following are packed and computed per iteration of the parallel traversal of quotient domain + +let main: DenseMatrix::Packing> = // ... +let (inv_zeroifier, is_transition, is_last_row, is_first_row) = // computed by taking out a slice of points from selectors `sels` and packing them +``` + +### Response + +```rust +// initialize the constraint folder +let accumulator = PackedChallenge::::ZERO; +let mut folder = ProverConstraintFolder { + main: main.as_view(), + public_values, + is_first_row, + is_last_row, + is_transition, + alpha_powers: &alpha_powers, + accumulator, + constraint_index: 0, +}; + +// compute all constraints one by one +air.eval(&mut folder); + +// extract the result of all constraints +let constraint: PackedChallenge = folder.accumulator; +``` + +#### Comment + +We may want to fold more than one different set of constraints with one folder. +In that case, the `folder` needs to be initialized only once and the constraints + from both sets are computed in sequence. +For example, if we want to evaluate two sets of constraints given by two AIR values, we would do `let my folder = _; air1.eval(&mut folder); air2.eval(&mut folder); let constraint = folder.accumulator;`. +In that case, the `constraint_count` is the sum of constraint counts of all the applied sets. + +Running `air.eval(&mut folder);` is not the only way to compute constraints, + one may choose to call the methods of `folder` directly or, in principle, + avoid using `folder` altogether and directly compute `constraint` value from the inputs of this prompt (but user needs to request this explicitly). + +### Outputs + +`folder` and `constraint` + + +## Example: (Verifier) Reconstruct quotient evaluation from chunks evaluations + +The prover who has opened the evaluations of quotient chunks, + includes them in the proof that is then passed to Verifier. +This example shows how Verifier reconstructs the evaluation of quotient at challenge point + from the evaluations of all chunks in that challenge point. + +### Prompt + +Reconstruct the value of quotient polynomial in point `zeta` + from the values of quotient chunks at `zeta`, given by `quotient_chunks`. + +### Inputs + +```rust +let zeta: Challenge = // sampled from challenger symmetrically to Prover + +let quotient_chunks_domains: Vec::Domain> = // must be computed in the same way as the domains used to split quotient polynomial into chunks + +let quotient_chunks_values: Vec> = // extracted from proof Verifier gets from Prover +``` + +### Response + +```rust +let zps = quotient_chunks_domains + .iter() + .enumerate() + .map(|(i, domain)| { + quotient_chunks_domains + .iter() + .enumerate() + .filter(|(j, _)| *j != i) + .map(|(_, other_domain)| { + other_domain.zp_at_point(zeta) + * other_domain.zp_at_point(domain.first_point()).inverse() + }) + .product::() + }) + .collect_vec(); + +let quotient = opened_values + .quotient_chunks_values + .iter() + .enumerate() + .map(|(ch_i, ch)| { + ch.iter() + .enumerate() + .map(|(e_i, &c)| zps[ch_i] * SC::Challenge::monomial(e_i) * c) + .sum::() + }) + .sum::(); +``` + +### Outputs + +`quotient: Challenge` + + +## Example: Compute the Maximum Degree and the number of Air constraints + +### Prompt + +Compute the maximum degree and the number of AIR constraints. + +### Inputs + +```rust +let air: Air>> = // Given as argument to the Prover and Verifier +let public_values = // Given as an argument to the Prover and Verifier +let public_values_len = public_values.len(); +``` + +### Response + +```rust +let symbolic_constraints = get_symbolic_constraints::, A>(air, 0, public_values_len); +let constraint_count = symbolic_constraints.len(); +let constraint_degree = symbolic_constraints + .iter() + .map(SymbolicExpression::degree_multiple) + .max() + .unwrap_or(0); +``` + +### Outputs + +`constraint_count: usize` and `constraint_degree: usize` + +## Example: (Verifier) Evaluate folded constraints at challenge point + +### Prompt + +Evaluate the value of constraint polynomial. +Use: + +- `air` constraints +- `trace_local_value` and `trace_next_value` trace evaluations (at `zeta`), +- `public_values` +- `sels` values of selector polynomials (at `zeta`), +- `alpha` challenge value + +### Inputs + +```rust +let air: &A = // argument of prover and verifier, describes constraint system + where A: for<'a> Air> + +let public_values: Vec> = // public instance, received as an argument to Verifier + +// extracted from the proof Verifier got from Prover +let trace_local_value: Vec = // +let trace_next_value: Vec = // + +let trace_domain = // computed in the same way as on Prover +let sels: LagrangeSelectors = trace_domain.selectors_at_point(zeta); + +let alpha: Challenge = // sampled from transcript symmetrically to the Prover +``` + +### Response + +```rust +let main = VerticalPair::new( + RowMajorMatrixView::new_row(&opened_values.trace_local), + RowMajorMatrixView::new_row(&opened_values.trace_next), +); + +let mut folder = VerifierConstraintFolder { + main, + public_values, + is_first_row: sels.is_first_row, + is_last_row: sels.is_last_row, + is_transition: sels.is_transition, + alpha, + accumulator: SC::Challenge::ZERO, +}; +air.eval(&mut folder); +let folded_constraints = folder.accumulator; +``` + +### Output + +`folded_constraints: Challenge` + + +## Example: (Verifier) Check that the opened quotient value is correct + +At this stage, the user requests to check that + + `folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)`. + +### Prompt + +Check that the `quotient`, opened value of quotient polynomial at `zeta`, is correct; + use `constraints`, the value of folded contraints polynomial at `zeta`, + and `sels`, the selector polynomials evaluated in point `zeta`. + +### Inputs + +```rust +let folded_constraints: Challenge = // computed using the opened values from Prover + +let trace_domain: Pcs::Domain = // computed in the same way as on Prover +let sels: LagrangeSelectors = trace_domain.selectors_at_point(zeta); + +let quotient: Challenge = // computed by restoring quotient from chunks we got from Prover +``` + +### Response + +```rust +if folded_constraints * sels.inv_zeroifier != quotient { + return Err(VerificationError::OodEvaluationMismatch); +} +``` + +### Outputs + +None. diff --git a/.cursor/rules/pv-sync.mdc b/.cursor/rules/pv-sync.mdc new file mode 100644 index 000000000..28a2fb70c --- /dev/null +++ b/.cursor/rules/pv-sync.mdc @@ -0,0 +1,166 @@ +--- +description: +globs: +alwaysApply: false +--- + +## Prover and Verifier Function Types + +### Prover + +The following is the skeleton for prover function type; + it returns a proof structure that depends on its implementation. + +```rust +pub struct Proof { + // contents depend on the prover implementation, +} + +pub fn prove( + config: &SC, + predicate_description: &A /* depends on the statement that is proven */, + challenger: &mut SC::Challenger, + trace: RowMajorMatrix>, + public_values: &Vec>, +) -> Proof +where + SC: StarkGenericConfig, +{ +} +``` + +The type of `predicate_description` parameter depends on the statement (aka circuit) this prover is proving. +For example, for AIR constraints prover, + the type of `predicate_description` will be quantified as + +```rust +where + A: Air>> + for<'a> Air> +``` + +the AIR constraints description. +The `SymbolicAirBuilder` is needed to calculate the constraints count and degree + (if these are known beforehand, `SymbolicAirBuilder` can be omitted); + while `ProverConstraintFolder` implements actual constraint polynomial evaluation. + +### Verifier + +```rust +pub struct VerificationError { + // will depend on the Verifier implementation +} + +pub fn verify( + config: &SC, + predicate_description: /* depends on the statement that is proven */, + challenger: &mut SC::Challenger, + proof: &Proof, + public_values: &Vec>, +) -> Result<(), VerificationError>> +where + SC: StarkGenericConfig, +{ +} +``` + +Note that the Proof taken as an argument by Verifier is the Proof returned by the Prover. + +Similarly to Prover above, + the type of `predicate_description` will depend on the circuit that this Verifier is verifying + (proven by its corresponding Prover). +For AIR constraints verifier, + it will be + +```rust +where + A: Air>> + for<'a> Air>, +``` + +The `SymbolicAirBuilder` is needed as in Prover, to compute the constraint count and degree. +The `VerifierConstraintFolder` is needed to comute the value of the folded constraint polynomial at the challenge point. + +### Imports + +The examples above use the following imports. +All the crates with names prefixed with `p3_` are from Plonky3, + feel free to check source code in this repo. +When preparing Prover and Verifier function signatures, + be sure to add these imports so the implementation can refer to them later. + +```rust +use p3_air::{Air, BaseAir}; +use p3_challenger::{CanObserve, CanSample, FieldChallenger}; +use p3_commit::{Pcs, PolynomialSpace}; +use p3_field::{Field, FieldAlgebra, FieldExtensionAlgebra, PackedValue}; +use p3_matrix::dense::{RowMajorMatrixView, RowMajorMatrix}; +use p3_matrix::Matrix; +use p3_matrix::stack::VerticalPair; +use p3_maybe_rayon::prelude::*; +use p3_uni_stark::{ + Commitments, + Domain, + get_symbolic_constraints, + PackedChallenge, + PackedVal, + PcsError, + ProverConstraintFolder, + StarkGenericConfig, + SymbolicAirBuilder, + SymbolicExpression, + Val, + VerifierConstraintFolder, +}; +use p3_uni_stark::symbolic_builder::{get_log_quotient_degree}; +use p3_util::{log2_ceil_usize, log2_strict_usize}; +#[macro_use] +use alloc::vec::Vec; +use itertools::Itertools; +``` + +## Synchronizing Prover and Verifier + +The `Challenger` interface we use here is the same is the same for both Prover and Verifier + (same trait with the same methods): + - "observe" methods (`observe`, `observe_slice` and `observe_ext_element`) that append new messages (from Prover to Verifier in the interactive setting) to the transcript, + - "sample" methods (`sample`, `sample_array`, `sample_vec` and `sample_ext_element`) that compute pseudorandom values by hashing the current transcript contents (correspond to random messages sent by Verifier to the Prover). + +The trace of calls that a Prover does to "observe" and "sample" methods of a prover must match the trace of such calls of the Verifier it runs with. + +The general pattern is that a Prover function returns a proof value (the type and layout of which depends on concrete statement this specific Prover is computing). +And its corresponding verifier will accept this Proof value as input. +Prover and Verifier both accept a mutable reference to a Challenger, + and whatever logic they perform must apply symmetric operations to the Challenger + (note that symmetry must only hold with respect to Challenger updates, the actions that don't touch the Challenger will often differ between the Prover and Verifier). +The values Prover adds to Challenger transcript (with "observe" methods) must be reconstructible by the Verifier as well, + it's the job of proof produced by the Prover to make sure of that; + one straightforward way to ensure that is to directly include + such observed values in the proof. +When Prover is calling a functon that modifies the Challenger transcript, Verifier must call its dual of that function. +For example, `pcs.verify` is Verifier's dual of Prover's `pcs.open` + (assuming the verifier is passing to `pcs.verify` the opening proof and values + that Prover got from the `pcs.open` call); + any "observe" or "sample" function is dual to itself. + +As a rule, all values Prover opens through `pcs.open` must be included + in the proof (together with the opening proofs) to ensure that + Verifier can make the corresponding `pcs.verify` call. + +A Prover and Verifier that are in sync and handle Challenger transcript correctly + may be used by another Prover' and Verifier' if Prover' calls Prover at a stage that corresponds to Verifier' calling Verifier. +This way, Prover-Verifier pairs may be re-used + as subroutines by other Provers and Verifiers if the calls are in sync. +This way, Verifier is dual of its Prover, + and another Prover' calling Prover requires Verifier' calling Verifier. +(The functions like `pcs.commit` or `pcs.get_evaluations_on_domain`, for example, + on the other hand, + don't require Verifier to do anything special + because the functions touch the Challenger. +) + +Following the rules above, + the code of Prover and Verifier must be written side by side, + ensuring that their actions on Challenger in sequence are synchronized. +It's best to first come up with this kind of unified flow of logic for both, and only then extract the corresponding Rust functions for Prover and Verifier. +The high-level pseudocode logic is best to include in the comment to the Rust functions to it more accessible. +When reading new code of Prover and Verifier, + come up with this kind of high-level correspondence (by syntactically observing the use of Challenger) between their actions and only then answer any queries.