Oh Just a Stark Technical Analysis

Below are a number of steps examining the in-depth processes of STARK.

Step1 - Build Trace（fib2-example)

The numbers marked in ‘red’ are public info.

Some assertion:
Form: [register, step, value]
examples: [0,0,1], [1,0,1], [1,7,987]

Step2 - Prover for Trace

Selection of the protocol parameter:

pub struct ProofOptions {
    num_queries: u8, // number of queries to increase reliability
    blowup_factor: u8, // domain extension factor
    grinding_factor: u8, // ？nonce security parameter, for the security selection of query position
    hash_fn: HashFunction, // Hash Function blake3-259/192, sha3-256
    field_extension: FieldExtension, // Whether the field extension is conducted
    fri_folding_factor: u8, // The folding factor of Fri protocol 4-8-16
    fri_max_remainder_size: u8, // The max remainder of Fri protocol
}

1. AIR Instantiation

FibAir {
            context: AirContext::new(trace_info, degrees, options),
            result: pub_inputs,
        }

        AirContext {
            options, // protocol parameters
            trace_info, // trace parameters: row number and col number
            transition_constraint_degrees, // transition the constraint degree, and if the multiplication of two registers is involved, then degree = 2; similarly, if the multiplication of three registers is involved, then degree = 3; if periodic column exists, then degree = base + period.length – 1
            ce_blowup_factor, // constraint computational domain extension factor   trace_domain < ce_domain < lde_domain
            trace_domain_generator: B::get_root_of_unity(log2(trace_length)),
            lde_domain_generator: B::get_root_of_unity(log2(lde_domain_size)),
        }

2. Verify the Consistency of AIR and Trace (Debug module)

2.1 Verify Basic Parameters

Trace.width = air.trace_width

2.2 Verify the Validity of Assertion (Boundary cs)

Trace[assertion_i.register][assertion_i.step] = assertion_i.value

2.2 Verify if Trace Holds Transition cs (Debug Module)

Loop:
For every two adjacent rows:
pub struct EvaluationFrame<E: FieldElement> {
    current: Vec<E>,
    next: Vec<E>,
}
Holds:
next[0] == cur[0] + cur[1]
next[1] == next[0] + cur[1]

The number of times of Loop: Trace.length - 1

Transcript

write.into(air, public info)

3. Commit for Trace

Domain parameter selection:

StarkDomain {
            trace_twiddles, /ntt twiddle factor
            ce_domain_size: air.ce_domain_size(), //constraint computational domain
            ce_to_lde_blowup: air.lde_domain_size() / air.ce_domain_size(), // LDE domain
            domain_offset: air.domain_offset(), //domain offset
}

3.1 Interpolate -> LDE -> evaluate over LDE-domain

3.2 Commitment

Transcript

write.into(cm_to_trace)

4.Evaluate CS

4.1 Obtain Linear Composition Coefficients

Ok(ConstraintCompositionCoefficients {
            transition: t_coefficients,
            boundary: b_coefficients,
})

The number of coefficients is consistent with that of constraints
In this example (fib2-example), there are 2 transition cs and 3 boundary cs.

4.2 Establish the Evaluator for t-cs and b-cs

4.2.1 t-cs

1. Obtain the degree of t-cs (In this example, the degree is [1,1], refer to Chapter 2.3)

2. Establish the t-cs group (record the parameters needed for reaching the object of degree -> compose degree（ce_domain_size - 1）
    Loop:
Calculate the evaluate-degree = base * （trace.length - 1） + tracce.length / period.cycle *(period.length - 1) of every t-cs
Establish the t-cs group according to the degree: 
    TransitionConstraintGroup {
            degree, // the degree of t-cs
            degree_adjustment, // The space to reach the object degree, target_degree = composition_degree + trace_poly_degree(vanish poly-degree), degree_adjustment = (target_degree - evaluation_degree)
            indexes: vec![],
            coefficients: vec![],
        }
Record index and distribution coefficient “coef”

Cycle each t-cs (In fib2-example, cycle twice)

3. Establish the period value table
4. Set the divisor for t-cs, with all t-cs having the same form
    z(x) = x^n-1 / x - g^{n-1} // The last value does not satisfy the condition

4.2.2 b-cs

1. The divisor of each b-cs is not necessarily the same

2. Judge that if the number of assertions is the same as the number of coefficients to be distributed
    assertion.len() == coefficients.len()
3. Establish the b-cs group
    Loop:
Obtain the type and initial step of the assertion
Establish the b-cs group
    BoundaryConstraintGroup {
            constraints: Vec::new(),
            divisor, //  The divisor corresponding to the boundary
            degree_adjustment, target//The space to reach the object degree, target_degree = composition_degree + divisor.degree()，degree_adjustment = (target_degree - trace_poly_degree)  
    }
Add b-cs forms
    air::BoundaryConstraint {
            register: assertion.register, // Corresponding register index
            poly, // assertion value polynomial, interpolation is required for multiple values; otherwise, it is a single value
            poly_offset, //offset information. If the assert is in the first step, it is [0,1], otherwise it is [1, T]
            cc, // Coefficient distributed to this b-cs
    }
    prover::BoundaryConstraintGroup {
            degree_adjustment: group.degree_adjustment(),
            single_value_constraints: Vec::new(),// corresponding Sigle value assertion
            small_poly_constraints: Vec::new(),//assertion whose assertion value num is smaller than 63
            large_poly_constraints: Vec::new(),//assertion whose assertion value num is larger than 63, the values in ce_domain are needed to conduct Pre_compute
    };

4.3 Evaluate t/s-cs Over ce_domain

4.3.1 Define Evaluator Table

ConstraintEvaluationTable<B: StarkField, E: FieldElement<BaseField = B>> {
evaluations: Vec<Vec<E>>, //[ce_domain_size][t_cs_merge_value (0): b_cs_values(1...)]
divisors: Vec<ConstraintDivisor<B>>, // [t-cs divisor, b-cs divisor]
domain_offset: B,
trace_length: usize,
#[cfg(debug_assertions)]
t_evaluations: Vec<Vec<B>>,
#[cfg(debug_assertions)]
t_expected_degrees: Vec<usize>,
}

evaluations[step_i][0]  += sum_{j}(evaluation[j] * (coefficients.0 + coefficients.1 * xp) // The divisor is identical.
evaluations[step_i][j]  += (evframe.cur().state[register] - value) * (coefficients.0 + coefficients.1 * xp) // for single assertion
evaluations[step_i][j]  += (evframe.cur().state[register] - polynom::eval(&self.poly, x * self.x_offset)) * (coefficients.0 + coefficients.1 * xp) // for multiassertion // for multi-assertion
evaluations[step_i][j]  += (evframe.cur().state[register] - self.values[values_index]) * (coefficients.0 + coefficients.1 * xp) // for multiassertion // for multi-assertion large poly 

5. Commitment to Evaluate CS

5.1 Establish Constraints Composition Polynomial

5.2 Commitment to Composition Poly

Example:
Compose_poly = a * x^3 + b * x^2 + c * x + d = (a * x^2 + c) * x^ + (b * x^2 + d) (a * x^2 + c) and (b *x^2 +d) correspond to two columns, respectively.

6. Establish DEEP Composition Polynomial

The general formal: f(x) = q(x)* t(x)
Need check at random z

1. f(z) = q(z) * t(z)

   
   

2. f(x),q(x),t(x) indeed equal respectively f(z), q(z), t(z)

   
   

3. calculate Deep_composition = (q(x) - q(z)) / (x - z)

   
   

4. Check LDT for q_q(x)

6.1 Select z which out of Domain(ood)

Draw an out-of-domain point z. Depending on the type of E, the point is drawn either from the base field or from an extension field defined by E.
The purpose of sampling from the extension field here (instead of the base field) is to increase security

6.2 Evaluate Trace and Constraint Polynomials at the OOD Point z

6.2.1 trace_poly at z & z * g

ood_frame = {cur: [trace_poly_0(z), trace_poly_1(z)], next: [trace_poly_0(z * g), trace_poly_1(z * g)]}

6.2.2 Composition Poly at z

iter!(self.columns).map(|p| polynom::eval(p, z^m)).collect() // m is the column num of the composition poly

6.3 Establish Deep Composition Polynomial

6.3.1 Generate Random Numbers

pub struct DeepCompositionCoefficients<E: FieldElement> {
    /// Trace polynomial composition coefficients $\alpha_i$, $\beta_i$, and $\gamma_i$.
    pub trace: Vec<(E, E, E)>,
    /// Constraint column polynomial composition coefficients $\delta_j$.
    pub constraints: Vec<E>,
    /// Degree adjustment composition coefficients $\lambda$ and $\mu$.
    pub degree: (E, E),
}

6.3.2 Cal Quotient Poly

=> for trace polynomial

T`(x) = alpha * (T(x) - T(z)) // degree = trace.length - 1
T``(x) = beta * (T(x) - T(z * g))
T```(x) = gamma * (T(x) - T(z_conjugate))

merge_trace_composition_poly = T(x) / (x - z) + T``(x) / (x - z * g) + T```(x) / (x - z_conjugate)

Degree = trace.lengh - 2

=> for composition polynomial

compute H'_i(x) = (H_i(x) - H_i(z^m)) / (x - z^m)
sum(H`_i(x) * cc_i)

Deep_composition_polynomial = merge_trace_composition_poly  + sum(H`_i(x) * cc_i)
Degree = trace.length - 2

=> Deep_composition_polynomial degree adjustment

Deep_composition_polynomial = Deep_composition_polynomial * (cc_0 + x * cc_1)
Degree = trace.length – 1

6.4 Evaluate Deep over LDE

deep_evaluations<lde_domain_size> = deep_composition_poly.evaluate(&domain);

7. Calculate the FRI Layer num of Deep

trace.length() =  fold_factor ^ Layer_num + remainder_size;
fold_factor = {4, 8, 16}
remainder_size < remainder_max_size == 256

8. Determine Positions of the Query

Select multiple positions of the query from lde_domain.

fold_position = source_position % (fold_domain)
fold_domain = source_domain / fold_factor

9. Establish Proof Objects

9.1 Generate FRI proof

pub struct FriProof {
    layers: Vec<FriProofLayer>,
    remainder: Vec<u8>, // last poly <all coefficients>
    num_partitions: u8, // stored as power of 2
}
pub struct FriProofLayer {
    values: Vec<u8>,
    paths: Vec<u8>,
}

9.2 Query Trace Poly at Above Positions

Similar to the above

Queries::new(trace_proof, trace_states)

9.3 Query Constraint Poly at Above Positions

Similar to the above

Queries::new(merkle_proof, evaluations)

9.4 Establish the STARK Proof

StarkProof {
            context: self.context,
            commitments: self.commitments,
            ood_frame: self.ood_frame,
            trace_queries,
            constraint_queries,
            fri_proof,
            pow_nonce: self.pow_nonce,
}

Step3 - Verify the Proof

Read pub-info from the transcript to obtain relevant data, and then to execute the verification process.

1. Ood Consistency Check

Verify the consistency of the mathematical relationship described in Chapter 5.2

=> for Boundary

    b(z) = q_b(x) * b_divisor(z)

=> for composition poly

    t(z) = q_z(x) * t_divisor(z)

2. Instantiate the FRI-Verifier Object

pub struct FriVerifier<B, E, C, H>
where
    B: StarkField,
    E: FieldElement<BaseField = B>,
    C: VerifierChannel<E, Hasher = H>,
    H: ElementHasher<BaseField = B>,
{
    max_poly_degree: usize,
    domain_size: usize,
    domain_generator: B,
    layer_commitments: Vec<H::Digest>, //flod_poly commitment
    layer_alphas: Vec<E>, // random numbers
    options: FriOptions,
    num_partitions: usize,
    _channel: PhantomData<C>,
}

3. Calculate Deep Poly on Query Positions

The calculating method is the same as that in Chapter 6.4

4. Execute the FRI VERIFY process