Try   HackMD

Open VM STARK back-end

STARK engine trait

StarkEngine is a helper trait to collect the different steps in multi-trace STARK keygen and proving.

run_test_impl is a testing method that runs a single end-to-end test for a given set of chips and traces partitions:

  • Verifying key generation,
  • Creating the proof,
  • Verifying the proof.

MultiStarkProvingKey generation

MultiStarkProvingKey is a proving key that aggregates multiple STARK proving keys (StarkProvingKey) for different AIRs (Algebraic Intermediate Representations). It enables a prover to generate proofs for multiple AIRs in a single proof system while ensuring all constraints are satisfied.

The MultiStarkProvingKey is generated through a builder pattern via MultiStarkKeygenBuilder.

  1. Creation of the keygen builder MultiStarkKeygenBuilder.
  2. Add all AIRs to the builder via add_air.
  3. Compute the highest constraint degree accross all AIRs.
  4. Compute symbolic constraints for each AIR.
  5. Use RAP (Randomized AIR with Preprocessing) to compute partial proving keys.
  6. Generate proving keys for each AIR, containing:
    • Verification key (vk) – Stores constraints, preprocessed data, and parameters.
    • Preprocessed data – Required for faster proof generation.
    • RAP partial proving key – Enforces permutation constraints across AIR instances.
  7. Constructs the final MultiStarkProvingKey, which aggregates:
    • Proving keys for each AIR.
    • Maximum constraint degree to ensure polynomial validity.

Proof generation

The STARK proof is generated from the MultiStarkProvingKey and the ProofInput.

  1. Extract AIR IDs from proof input.
  2. Commits execution traces to the STARK proof system:
    • If traces are missing, they are computed and stored in the prover's memory.
    • If traces exist, the commitment data (PcsData) is reused.
  3. Prepare the proving context for each AIR, we store:
    • Committed traces
    • Common main trace
    • Public values (e.g., boundary constraints)
  4. The proving key (mpk) is transferred to the computational device (CpuDevice).
  5. Calls prove() on the prover, passing:
    • The proving key view (mpk_view).
    • The proving context (ctx).

Specialized proving phase

Then we enter the specialized proving phase for interactive AIRs. It assumes that the main traces have been generated and committed already, only handling the trace generation of the permutation traces.

  1. Validation: Ensures that the proving context (ctx) is compatible with the proving key (mpk).
  2. Extracts execution trace data for each AIR:
    • cached_commits_per_air: Commitments for the main trace segments.
    • cached_views_per_air: Data views of cached execution traces.
    • common_main_per_air: Common execution traces (if shared across AIRs).
    • pvs_per_air: Public values (boundary conditions for verification).
  3. Commitment of main traces, ordered by AIR id (all traces commitment that do not require challenges).
  4. Prepare trace views
    • Maps execution traces into PairView structures.
    • Extracts logarithmic trace heights (for STARK polynomial commitments).
    • Prepares public values for inclusion in the proof.
  5. The cryptographic challenger observes:
    • Public values (inputs to the proof).
    • Commitments of preprocessed data and main traces.
    • Trace domain sizes (encoded as logarithmic values).
  6. Partially proving RAP (randomized AIR with preprocessing) phases
    • Uses verifier randomness for probabilistic constraint checks.
    • Stores data after challenge phases (prover_data_after).
    • Observes additional commitments generated during RAP phases.
  7. Extracts prover-exposed values for verification.
  8. Compute and commit quotient polynomial
    • Computes the quotient polynomial to ensure constraints hold.
    • Commits the quotient polynomial and makes it observable to the verifier.
  9. Uses polynomial commitment schemes (PCS) to create opening proofs.
  10. Assemble the proof with:
    • Commitments (traces, challenges, quotient polynomial).
    • Opening proofs (polynomial openings).
    • RAP proof data.

Verify the proof

The verify() function in MultiTraceStarkVerifier is responsible for verifying a STARK proof by checking constraints, commitments, and polynomial evaluations. Below is a step-by-step explanation of how the verification process works.

  1. Initial setup and observations
    • Extracts relevant verifying keys for the AIRs present in the proof.
    • Calls verify_raps(), which handles the verification of RAP (Randomized AIR with Preprocessing) constraints.
  2. Challenger observes public values
    • Observes public values that were committed by the prover.
    • This ensures the prover did not tamper with known public values.
  3. Challenger observes preprocessed commitments
    • Observes commitments of preprocessed trace data (if any).
    • This ensures that the commitments match what was expected.
  4. Challenger observes main trace commitments
    • Observes the main execution trace commitments to verify that they match the prover’s claim.
    • Observes trace domain sizes, which encode the length of the execution trace for each AIR.
  5. Prepares data for RAP constraint verification, including:
    • Exposed values from the proof.
    • Permutation check values (which verify trace consistency).
  6. Partially verifies RAP constraints, ensuring:
    • Random challenges were correctly incorporated into the proof.
    • Interaction constraints between different AIRs were respected.
  7. Sampling challenges (alpha and zeta)
    • Samples a random challenge alpha, which will be used in quotient polynomial checks.
    • Observes the commitment to the quotient polynomial.
    • Samples another challenge zeta, which is used for polynomial evaluations.
  8. Verify polynomial opening proofs
    • Computes the polynomial evaluation domains for:
      • The main execution trace.
      • The quotient polynomial.
    • Splits quotient polynomial domains for batched polynomial evaluations.
  9. Verify commitment openings
    • Build the opening rounds:
      • The preprocessed trace openings
      • The main trace openings
      • Then we handle the trace openings that take place after challenges
    • Checks that the prover’s opening proofs match the claimed commitments.
    • If an opening proof fails, the function returns an invalid proof error.
  10. Verifies all STARK constraints for each AIR:
    • Preprocessed trace constraints.
    • Main execution trace constraints.
    • After-challenge constraints.
    • Quotient polynomial consistency.

Let us now detail the partially_verify phase which only supports LogUp for now.

FRI LogUp partially_verify

The partially_verify function in FriLogUpPhase is responsible for partially verifying the STARK proof's RAP (Randomized AIR with Preprocessing) phase by checking the cumulative sum constraint that ensures correctness across multiple AIRs. It is part of the logup phase in STARK proofs, which handles interactions and permutations.

  • It checks that the cumulative sum of permutations across AIRs is zero, ensuring correctness.
  • It samples new challenges, observes commitments, and verifies consistency.
  • It transforms exposed values into constraints that must hold for the proof to be valid.

Here is a step by step explanation.

  1. Check if any exposed values exist
    • If no interactions require verification, it exits early with a successful result.
  2. The verifier generates random field elements (challenges) using the challenger to ensure soundness.
  3. The challenger observes the exposed values from each phase, which are cumulative sums of permutation constraints.
  4. The verifier records the first commitment to ensure the prover cannot manipulate it.
  5. Extract the cumulative sum
    • Extracts cumulative sum values from the proof to check correctness.
    • Ensures only one phase is used (this implementation does not support multiple challenge phases).
  6. Check if the cumulative sum is zero
    • Computes the sum of all cumulative sums across different AIRs.
    • If the sum is not zero, the proof fails because the consistency check has been violated.
  7. Return the verification result
    • The function returns the challenges used in the verification phase.
    • If the sum was zero, verification succeeds; otherwise, it fails.
Last changed by 
 
Thomas Coratger
0
18

Read more

beam call #2

Plonky3 looks most promising, on a modern CPU (e.g. i9-13900K, M3 Max), it can do:

Feb 28, 2025
Circuit gadgets

CycleBits<T, N> represents a cycle of N bits, where only one bit is active (set to 1) at a time.

Feb 24, 2025
Hashcaster - Part 3: boolcheck

The boolcheck protocol as proposed in Hashcaster provides a novel and efficient method for verifying quadratic Boolean formulas over polynomial coordinates. Boolean formulas are represented as polynomials over a finite field \mathbb{F}_{2^{128}}, where input variables correspond to coefficients of these polynomials. The primary objective is to verify the correctness of quadratic boolean formulas while minimizing prover and verifier effort. For simplicity of exposition, we will restrict ourselves to the andcheck, but generally this construction will work for any homogeneous quadratic Boolean formula (and non-homogeneous quadratic formulas can also fit with a bit of adjustment). To better understand this proposed technique, we will first go into Frobenius theory and these concepts will help us better understand why we chose such a technique for our boolcheck algorithm.

Feb 18, 2025
Hashcaster - Part 2: The challenges of Sumcheck in binary fields

The smallest possible field is the field of arithmetic modulo 2. This field, often denoted as ( \mathbb{F}_2 ), is so small that we can explicitly write out its addition and multiplication tables:

Feb 3, 2025
Read more from Thomas Coratger
Published on HackMD