Going Deep into the Specification for Marlin

Arkworks for Marlin
Marlin
Fractal

R1CS

Zero-knowledge proof algorithm Marlin is a R1CS based proof system, that, given a coefficient matrix parameter I = (F, n, m, A, B, C) and a set of valid assignments z = (x, w) ∈ F^n, among which x is public information, namely Instance and is private information, namely, witness if Az ∘ Bz = Cz is established, R1CS is established.

If we let z_A=Az, z_B = Bz, z_C = Cz the above formula can be transformed into z_A ∘ z_B = z_C.

Therefore, if we can prove that there are four vectors z_A, z_B, z_C, z that satisfy

R1CS is established.

Transition into Polynomial (Efficiency)

Prepare

1. Vanish Polynomial

   

2. Derivative of Vanish Polynomial

It’s a non-zero value if and only if

Define Polynomial

1. Define polynomial (LDE) ^zA(X), ^zB(X), ^zC(X) ∈ F<|H| + b[X]z^A(X), z^B(X), z^C(X) ∈ F< |H| + b[X] for vectors z_A, z_B, z_C satisfying that the value on the group H is consistent with the vector, where the order of the group H are equal to the length of the vector (assuming they are both), that is:

Add b redundant point without exposing any information of w

2. Define polynomial (LDE) for vector z = (x, w)
3. Define a polynomial ^x(X) ∈ F^{<|H_{[<=|x|]}|}[X] for x, satisfying

4. Define a polynomial for w
   

   Define a polynomial ^w(X) (LDE) for a vector bar{w}, satisfying

Then the polynomial hat{z}(X) is

3. Define Polynomials for Matrices A, B, C (Holographic)

   
   

   In order to reduce the computational complexity for the verifier (seepaper 5.2.1 ), we use a special form to represent the matrix. Below is an example using matrix A.

Define:

Where t_k is the row index of the kth non-zero value of the matrix,

maps the index to the computational domain, and ^val(k) is the kth non-zero value of the matrix, which can be divisible by

Therefore, a polynomial can be expressed as

Linearity Check

In order to prove ^z_A(X) = A^z(X), define the polynomial

Which should satisfy

The relationship among ^z_A(X), A, ^z(X) in the group H is as shown in the following figure

Now, we multiply a factor r(α, X) for each element of ^z_A(X) on group H, then in order to ensure balance, we should multiply a factor r(α,X) for the A^z(X) which is as shown in the following figure

It can be seen that when the polynomial t(X) traverses the value of group H, the following is satisfied

Likewise, we can also derive it from the formula

That is, if it can be proved that the accumulation of polynomials q(X) on group H is 0, the linear relationship among ^z_A(X), A, ^z(X) is established.

AHP for R1CS

Common

Given a polynomial

Compute polynomial h_0(X) satisfying

Generate random polynomials

Prover

=> Prover
a. Commit to ^z_A(X), ^z_B(X), ^z_C(X), ^w(X) , h_0(X), s(X)
b. Transcript.write δ1,cm∗

=> Oracle

Generate random numbers α, η_A, η_B, η_C

=> Prover - sumcheck-1

Sumcheck for

c. Compute polynomials h_1(X)and g_1(X) such that

d. Commit to h_1(X), g_1(X)
e. Transcript.write cm_h1, cm_g1
=> Oracle

Generate random number β1

=> Prover - sumcheck-1
a. Compute s(β_1), h_1(β_1), g_1(β_1), ^z_A(β_1), ^z_B(β_1), ^z_C(β_1), ^w(β_1)
b. If we send these numbers to the verifier, the verifier needs to compute

Its computational complexity is Ω(|H||K|), therefore, this part of the calculation needs to be executed by the Prover as a proxy.

=> Prover -sumcheck-2

Sumcheck for ∑_{X ∈ H} r(α, X) (η_A^A} (X, β_1) + η_B^B(X,β_1) + η_C^C}(X, β_1))

a. Compute polynomials h_2(X) and g_2(X) such that

b. Commit to h_2(X), g_2(X)
c. Transcript.write δ_2, cm_h_2, cm_g_2

=> Oracle

Generate random number β2

=> Prover - sumcheck-2
a. Compute h_2(β_2), g_2(β_2)
b. If we send these numbers to the verifier, the verifier needs to compute
i. v_H(β_2), r(α, β_2)
ii. ^A(β_2, β_1), ^B(β_2, β_1), ^C(β_2, β_1)

Its computational complexity is Ω(|K|), therefore, this part of the calculation needs to be executed by Prover as a proxy.

=> Prover - sumcheck-3

Sumcheck for

Define the polynomial

which can be combined as: a(X) − b(X)(Xg_3(X) + δ3/|K|) = h_3(X)v_K(X)

where

b. Commit to h_3(x), g_3(x))
c. Transcript.write δ3, cm_h_3, cm_g_3

=> Oracle

Generate random number β_3

=> Prover - sumcheck-3

a. Compute

b. Send to the verifier

Verifier

=> Verifier-sumcheck-3

a. Compute

b. Verify

If it passes the verification, it means that the value computed by the Prover

is valid, then go to the previous level for verification.

=> Verifier-sumcheck-2

Recall the equality

a. Compute
i. v_H(β2)
b. Verify

If it passes the verification, it means that the value computed by the Prover

is valid, then go to the previous level for verification.

=> Verifier-sumcheck-1

Recall the equality

a. Compute
i. v_H(β_1)
ii. r(α, β1)
iii. v_H[≤|x|](β_1)
iv. ^z(β_1) = ^w(β_1) v_{H[<=|x|]}(β_1) + ^x(β_1)
b. Verify

If it passes the verification, it means that the polynomials ^z_A(X), ^z_B(X), ^z_C(X) and ^z(X) satisfy a linear relationship.

=> Verifier

Verify ^z_A(β_1) . ^z_B(β_1) - ^z_C(β_1) = h_0(β_1)v_H(β_1)

Polynomial Commitment

The protocol has carried out three rounds of interaction in total. The polynomials of each round of interaction commitment and the query points are as follows:

Sumcheck - 1

Sumcheck - 2

Sumcheck - 3

Extended KZG10 (cross multi-poly)

Optimization

Sum(s(X)) = 0

Generate random polynomials

Then, for sumcheck - 1

Reduce sumcheck

According to the optimization mentioned in the paper COS20. Claim6.7（Fractal）we make

For matrices A, B, C the transformed matrices are

Define polynomial t(X)
Then, for sumcheck - 1，the formula becomes

Common

Given the polynomial

Compute polynomial h_0(X) satisfying

Generate random polynomials

Prover

=> Prover

a. Commit to ^z_A(X), ^z_B(X), ^z_C(X), ^w(X) ,h_0(X), s(X)
b. Transcript.write δ1,cm∗δ1,cm∗

=> Oracle

Generate random number α, η_A, η_B, η_C

=> Prover-sumcheck - 1

Sumcheck for

a. Compute polynomials h_1(X) and g_1(X) such that:

b. Commit to h_1(X), g_1(X)
c. Transcript.write cm_h_1, cm_g_1

=> Oracle

Generate random number β_1

=> Prover-sumcheck - 1

a. Compute  s(β_1), h_1(β_1), g_1(β_1), ^z_A(β_1), ^zB(β_1), ^zC(β_1), ^w(β_1)*
b. i. If we send these numbers to the verifier, the verifier needs to compute
i. v_H(β_1), v*{H[<=|x|]}(β_1), r(α, β_1)
ii. ^z(β_1) = ^w(β_1) v{H[<=|x|]}(β_1) + ^x(β_1)
iii. t(β_1) = η_AA^(β_1, α) + η_BB^(β_1, α) + η_CC^*(β_1, α)

Its computational complexity is Ω(|K|), Therefore, this part of the calculation needs to be executed by Prover as a proxy.

=> Prover - sumcheck-2

Sumcheck for

Define the polynomial

a. Compute polynomials h_2(x) and g_2(x) such that

which can be combined as a(X) − b(X)(Xg_2(X) + t(β1)/|K|) = h2(X)v_K(X)

where

b. Commit to h_2(x), g_2(x)
c. Transcript.write t(β1), cm_h_2, cm_g_2

=> Oracle

Generate random number β_2

=> Prover - sumcheck-2

1. Compute

   

2. b. Send them to the verifier

Verifier

=> Verifier sumcheck - 2

1. Compute
   a. v_K(β2)
   b.

   

   2. Verify

   

   If it passes the verification, it means that the calculation t(β1) calculated by the Prover is valid, then it goes up to the previous verification.

   
   

   => Verifier sumcheck - 1

   
   

   Recall the equality

   

   a. Compute
   i. v_H(β1)
   ii. μ(α, β1)
   iii. v_H[≤|x|](β1)
   iv. ^z(β_1) = ^w(β_1) v_{H[<=|x|]}(β_1) + ^x(β_1)

3. Verify

If it passes the verification, it means that the polynomials ^z_A(X), ^z_B(X), ^z_C(X) satisfy a linear relationship.

=> Verifier

Verify ^z_A(β_1) . ^z_B(β_1) - ^z_C(β_1) = h_0(β_1)v_H(β_1)

Reduce polynomial numbers for Sumcheck - 2

Compress the current verification of the three matrices into the verification of one matrix, namely

Represent this polynomial as a sparse matrix.

Matrix polynomials are reduced from 9 to 3.

Set b = 1

Set b = 1

Final Protocol

Marlin in Arkworks