libZK: a zero-knowledge proof library

2.2.1. Extend method in Field F_p

The extend(f, n, m) method interprets the array f[0..n] as the evaluations of a polynomial P of degree less than n at the points 0,...,n-1, and returns the evaluations of the same P at the points 0,...,m-1. For sufficiently large fields |F_p| = p >= n, polynomial P is uniquely determined by the input, and thus extend is well defined.¶

As there are several algorithms for efficiently performing the extend operation, the implementor can choose a suitable one. In some cases, the brute force method of using Lagrange interpolation formulas to compute each output point independently may suffice. One can employ a convolution to implement the extend operation, and in some cases, either the Number Theoretic Transform or Nussbaumer's algorithm can be used to efficiently compute a convolution.¶

2.2.2. Extend method in Field GF 2^k

The previous section described an extend method that applies to odd prime-order finite fields which contain the elements 0,1,2...,m. In the special case of GF(2^k), the extend operator is defined in an opinionated way inspired by the Additive FFT algorithm by Lin et al [additivefft]. Lin et al. define a novel polynomial basis for polynomials as an alternative to the usual monomial basis xⁱ, and give an algorithm for evaluating a degree-(d-1) polynomial at all d points in a subspace, for d=2^ell, and for polynomials expressed in the novel basis.¶

Specifically, we implement GF(2¹²⁸) as GF{2}[x] / (Q(x)) where¶

    Q(x) = x^{128} + x^{7} + x^{2} + x + 1

With this choice of Q(x), x is a generator of the multiplicative group of the field. Next, we choose GF(2¹⁶) as the subfield of GF(2¹²⁸) with g=x^{(2^{128}-1) / (2^{16}-1)} as its generator, and beta_i=g^i^ for 0 <= i < 16 as the basis of the subfield. For relevant problem sizes, this allows us to encode elements in our commitment scheme with 16-bits instead of 128.¶

Writing j_i for the i-th bit of the binary representation of j, that is,¶

    j = sum_{0 <= i < k} j_i 2^i     j_i \in {0,1}

we inject integer j into a field element inj(j) by interpreting the bits of j as coordinates in terms of the basis:¶

    inj(j) = sum_{0 <= i < k} j_i beta_i

We define the extend operator to interpret the array f[0..n] to consist of the evaluations of a polynomial p(x) of degree at most n-1 at the n points x \in { inj(i) : 0 <= i < n } and to return the set { p(inj(i)) : 0 <= i < m} which consist of the evaluations of the same polynomial p(x) at the injected points 0,...,m-1.¶

This convention allows this operation to be completed efficiently using various forms of the additive FFT as described in [libzk] [additivefft].¶

3.1.1. Initialization

At the beginning of the protocol, the transcript object must be initialized.¶

• transcript.init(session_id): The initialization begins by selecting an oracle, which concretely consists of selecting a fresh session identifier. This process is handled by the encapsulating protocol---for example, the transcript that is used for key exchange for a session can be used as the session identifier as it is guaranteed to be unique.¶

3.1.2. Writing to the transcript

The transcript object supports a write method that is used to record the Prover's messages. To produce the verifier's challenge message, the transcript object internally maintains a Fiat-Shamir Pseudo-random Function (FSPRF) object that generates a stream of pseudo-random bytes. Each invocation of write creates a new FSPRF object, which we denote by fs.¶

• transcript.write(msg): appends the Prover's next message to the transcript.¶

There are three types of messages that can be appended to the transcript: a field element, an array of bytes, or an array of field elements.¶

• To append a field element, first the byte designator 0x1 is appended, and then the canonical byte serialization of the field element is appended.¶

• To append an array of bytes, first the byte designator 0x2 is appended, an 8-byte little-endian encoding of the number of bytes in the array is appended, and then the bytes of the array are appended.¶

• To append an array of field elements, the byte designator 0x3 is added, an 8-byte little-endian encoding of the number of field elements is appended, and finally, all of the field elements in array order are serialized and appended.¶

3.1.3. Special rules for the first message

The write method for the first prover message incorporates additional steps that enhance the correlation-intractability property of the oracle. To process the Prover's first message (which is usually a commitment):¶

1. The Prover message is appended to the transcript. Specifically, the length of the message, as per the above convention, is appended, and then the bytes of the message are appended.¶
2. Next, an encoding of the statement to be proven, which consists of the circuit identifier, and a serialization of the input and output of the statement is appended. Each of these three message are added as byte sequences, with their length appended as per convention.¶
3. Finally, the transcript is augmented by the byte-array 0^|C|, which consists of |C| bytes of zeroes.¶

One might at first think of performing steps 2 and 3 first so as to simplify the description of the protocol, and moreover step 3 may appear to be unnecessary. Performing the steps in the indicated order protects against the attack described in [krs], under the assumption that it is infeasible for a circuit C that contains |C| arithmetic gates to compute the hash of a string of length |C|.¶

Subsequent calls to the write method are used to record the Prover's response messages msg. In this case, the message is appended following the conventions described above.¶

5.2.1. Remark

Let m <= n, A = bindv(EQ_{m}, X) and B = bindv(EQ_{n}, X). It is true that A[i] = B[i] for i < m. However, it is also true that A[i] = 0 for i >= m, whereas B[i] is in general nonzero. Thus, care must be taken when computing a further binding bindv(A, Y), which is in general not the same as bindv(B, Y). A second binding is not needed in this document, but certain closed-form expressions for the binding found in the literature agree with these definitions only when m is a power of 2.¶

5.3.1. Layered circuits

A circuit consists of NL layers. By convention, layer j computes wires V[j] given wires V[j + 1], where each V[j] is an array of field elements. A wire is an element V[j][w] for some j and w. Thus, V[0] denotes the output wires of the entire circuit, and V[NL] denotes the input wires.¶

A circuit is intended to check that some property of the input holds, and by convention, the check is considered successful if all output wires are 0, that is, if V[0][w] = 0 for all w.¶

5.3.2. Quad representation

The computation of circuit is defined by a set of quads Q[j], one per layer. Given the output of layer j + 1, the output of of layer j is given by the following equation:¶

  V[j][g] = SUM_{l, r} Q[j][g, l, r] V[j + 1][l] V[j + 1][r] .

The quad Q[j][] is thus a three-dimensional array in the indices g, l, and r where 0 <= g < NW[j] and 0 <= l, r < NW[j + 1]. In practice, Q[j][] is sparse.¶

The specification of the circuit contains an auxiliary vector of quantities LV[j] with the property that V[j][w] = 0 for all w >= 2^{LV[j]}. Informally, LV[j] is the number of bits needed to name a wire at layer j, but LV[j] may be larger than the minimum required value.¶

5.3.3. In-circuit assertions

In the libzk system, a theorem is represented by a circuit such that the theorem is true if and only if all outputs of the circuit are zero. It happens in practice that many output wires are computed early in the circuit (i.e., in a layer closer to the input), but because of layering, they need to be copied all the way to output layer in order to be compared against zero. This copy seems to introduce large overheads in practice.¶

A special convention can mitigate this problem. Abstractly, a layer is represented by two quads Q and Z, and the operation of the layer is described by the two equations¶

  V[j][g] = SUM_{l, r} Q[j][g, l, r] V[j + 1][l] V[j + 1][r]
       0  = SUM_{l, r} Z[j][g, l, r] V[j + 1][l] V[j + 1][r]

Thus, the Z quad asserts that, for given layer j and output wire g, a certain quadratic combination of the input wires is zero.¶

The actual protocol verifies a random linear combination of those two equations, effectively operating on a combined quad QZ = Q + beta * Z for some random beta.¶

To allow for a compact representation of the two quads without losing any real generality, the following conditions are imposed:¶

• The two quads Q and Z are disjoint: for all layers j and output wire g, if any Q[j][g, ., .] are nonzero, then all Z[j][g, ., .] are zero, and vice versa.¶
• Z is binary: Z[j][g, l, r] \in {0, 1}¶

With these choices, the two quads allow a compact sparse representation as a single list of 4-tuples (g, l, r, v) with the following conventions:¶

• If v = 0, the 4-tuple represents an element of Z, and Z[j][g, l, r] = 1.¶
• If v != 0, the 4-tuple represents an element of Q, and Q[j][g, l, r] = v.¶
• All other elements of Q and Z not specified by the list are zero.¶

Moreover, this compact representation can be transformed into a representation of QZ = Q + beta * Z by replacing all v = 0 with v = beta.¶

6.1.1. Constructing a Merkle tree from n digests

struct {
   Digest a[2 * n]
} MerkleTree

def set_leaf(M, pos, leaf) {
  assert(pos < M.n)
  M.a[pos + n] = leaf
}

def build_tree(M) {
  FOR M.n < i <= 1 DO
    M.a[i] = hash(M.a[2 * i] || M.a[2 * i + 1])
  return M.a[1]
}

6.1.2. Constructing a proof of inclusion

This application of the Merkle tree requires verifying that a batch of k input digests at indicies i[0],...,i[k-1] belong to the tree. The simplest way to generate such a proof is to produce independent proofs for each of the k leaves. However, this turns out to be wasteful in that internal nodes could be included multiple times along different paths, and some nodes may not need to be included at all because they are implied by nodes that have already been included.¶

To address these inefficiencies, this section explains how to produce a batch proof of inclusion for k leaves. The main idea is to start from the requested set of leaves and build all of the implied internal nodes given the leaves. For example, if sibling leaves are included, then their parent is implied, and the parent need not be included in the compressed proof. Then it suffices to revisit the same tree and include the necessary siblings along all of the Merkle paths. It is assumed that the verifier already has the leaf digests that are at the indicies, and thus the proof only contains the necessary internal nodes of the Merkle tree that are used to verify the claim.¶

It is important in this formulation to treat the input digests as a sequence, i.e. with a given order. Both the prover and verifier of this batch proof needs to use the same order of the requested_leaves array.¶

def compressed_proof(M, requested_leaves[], n) {
  marked = mark_tree(requested_leaves, n)
  FOR n < i <= 1 DO
    IF (marked[i]) {
      child = 2 * i
      IF (marked[child]) {
        child += 1
      }
      IF (!marked[child]) {
        proof.append(M.a[child])
      }
    }
  return proof
}

def mark_tree(requested_leaves[], n) {
  bool marked[2 * n]   // initialized to false

  for(index i : requested_leaves)
    marked[i + n] = true

  FOR n < i <= 1 DO
    // mark parent if child is marked
    marked[i] = marked[2 * i] || marked[2 * i + 1];

  return marked
}

6.1.3. Verifying a proof of inclusion

This section describes how to verify a compressed Merkle proof. The claim to verify is that "the commitment root defines an n-leaf Merkle tree that contains k digests s[0],..s[k-1] at corresponding indicies i[0],...i[k-1]." The strategy of this verification procedure is to deduce which nodes are needed along the k verification paths from index to root, then read these values from the purported proof, and then recompute the Merkle tree and the consistency of the root digest. As an optimization, the defined[] array avoids recomputing internal portions of the Merkle tree that are not relevant to the verification. By convention, a proof for the degenerate case of k=0 digests is defined to fail.¶

def verify_merkle(root, n, k,  s[], indicies[], proof[]) {
  tmp = []
  defined = []

  proof_index = 0
  marked = mark_tree(indicies, n)
  FOR n < i <= 1 DO
    if (marked[i]) {
      child = 2 * i
      if (marked[child]) {
        child += 1
      }
      if (!marked[child]) {
        if proof_index > |proof| {
          return false
        }
        tmp[child] = proof[proof_index++]
        defined[child] = true
      }
    }

  FOR 0 <= i < k DO
    tmp[indicies[i] + n] = s[i]
    defined[indicies[i] + n] = true

  FOR n < j <= 1 DO
    if defined[2 * i] && defined[2 * i + 1] {
      tmp[i] = hash(tmp[2 * i] || tmp[2 * i + 1])
      defined[i] = true
    }

  return defined[1] && tmp[1] = root
}

6.2.1. Constraints on parameters

• BLOCK < |F_q| The block size must be smaller than the field size.¶
• BLOCK > NREQ The block size must be larger than the number of columns requested.¶
• BLOCK >= 2 * (NREQ + QR) + (NREQ + WR) - 2¶
• WR >= QR.¶
• BLOCK >= 2 * (NREQ + WR) - 1.¶
• QR >= NREQ (and thus WR >= NREQ) to avoid wasting too much space.¶

6.4.1. Low-degree test

In the low-degree test, the verifier sends a challenge vector consisting of NROW field elements, u[0..NROW]. This challenge is generated via the Fiat-Shamir transform. The prover computes the sum of u[i]*T[i] where T[i] is the i-th row of the tableau, and returns the first BLOCK elements of the result. The verifier applies the extend method to this response, and then verifies that the extended row is consistent with the positions of the Merkle tree that the verifier will later request from the Prover.¶

The Prover's task is therefore to compute a summation. For efficiency, set u[0]=1 because this first row corresponds to a random row meant to ``pad" the witnesses for zero-knowledge.¶

6.4.2. Linear and Quadratic constraints

The linear test is represented by a matrix A, and a vector b, and aims to verify that A*w = b. The constraint matrix A is given as input in a sparse form: it is an array of triples (c,w,k) in which c indicates the constraint number or row of A, w represents the index of the witness or column of A, and k represents the constant factor. For example, if the first constraint (at index 0) was w[2] + 2w[3] = 3, then the linear constraints array contains the triples (0,2,1), (0,3,2) and the b vector has b[0]=3.¶

The quadratic constraints are given as input as an array names lqc[] that contains triples (x,y,z); one such triple represents the constraint that w[x] * w[y] = w[z]. To process quadratic constraints, the Tableau is augmented with 3 extra rows, called Ax, Ay, and Az which hold copied witnesses and their products. If the i-th quadratic constraint is (x,y,z), then the prover sets Ax[i] = w[x], Ay[i]=w[y] and Az[i]= w[x] * w[y]. Next, the prover adds a linear constraint that Ax[i] - w[x] = 0, Ay[i] - w[y] = 0 and Az[i] - w[z] = 0 to ensure that the copied witness is consistent.¶

In this sense, the quadratic constraints are reduced to linear constraints, and the additional requirement for the verifier to check that each index of the Az row is the product of its counterpart in the Ax and Ay row.¶

6.4.3. Ligero Prover procedure

def prove(transcript, digest, linear[], lqc[])  {

    u = transcript.generate_challenge([BLOCK]);
    transcript.write(digest)

    ldt[0..BLOCK] = T[0][0..BLOCK]

    for(i=1; i < NROW; ++i) {
      ldt[0..BLOCK] += u[i] * T[i][0..BLOCK]
    }

    alpha_l = transcript.generate_challenge([NL]);
    alpha_q = transcript.generate_challenge([NQ,3]);

    A = inner_product_vector(linear, alpha_l, lqc, alpha_q);

    dot = dot_proof(A);

    transcript.write(ldt);
    transcript.write(dot);

    challenge_indicies = transcript.generate_challenge([NREQ]);

    columns = requested_columns(challenge_indicies);

    mt_proof = M.compressed_proof(challenge_indicies);

    return (ldt, dot, columns, mt_proof)
  }

Input:
- linear: array of (w,c,k) triples specifying the linear constraints
- alpha_l: array of challenges for the linear constraints
- lqc: array of (x,y,z) triples specifying the quadratic constraints
- alpha_q: array of challenges for the quadratic constraints

Output:
- A: a vector of size WR x NROW that contains the combined
     witness constraints.
     The first NW * W positions correspond to coefficients
     for the linear constraints on witnesses.
     The next 3*NQ positions correspond to coefficients
     for the quadratic constraints.

def inner_product_vector(A, linear, alpha_l, lqc, alpha_q) {
  A = [0]

  // random linear combinations of the linear constraints
  FOR 0 <= i < NL DO
    assert(linear[i].w < NW)
    assert(linear[i].c < NL)
    A[ linear[i].w ] += alpha_l[ linear[i].c ] * linear[i].k

  // pointers to terms for quadratic constraints
  a_x = NW * W
  a_y = NW * W + (NQ * W)
  a_z = NW * W + 2 * (NQ * W)

  FOR 0 <= i < NQT DO
    FOR 0 <= j < QR DO
      IF (j + i * QR < NQ)
        ilqc = j + i * QR  // index into lqc
        ia   = j + i * WR  // index into Ax,Ay,Az sub-arrays
        (x,y,z) = lqc[ilqc]

        // add constraints that the copies are correct
        A[a_x + ia] += alpha_q[ilqc][0]
        A[x]        -= alpha_q[ilqc][0]

        A[a_y + ia] += alpha_q[ilqc][1]
        A[y]        -= alpha_q[ilqc][1]

        A[a_z + ia] += alphaq[ilqc][2]
        A[z]        -= alphaq[ilqc][2]

  return A
}

def dot_proof(A) {
  y = T[IDOT][0..BLOCK]

  Aext[0..BLOCK] = [0]
  FOR 0 <= i < NQW DO
    Aext[0..R]  = [0]
    Aext[R..R + WR] = A[i * WR..(i+1) * WR]
    Af = extend(Aext, R+WR, BLOCK)

    add(BLOCK, y,
               times(BLOCK, Af[0..BLOCK],
                            T[i + IW][0...BLOCK]))

  return y
}

def requested_columns(challenge_indicies) {
  cols = []   // array of columns of T
  FOR (index i : challenge_indicies) {
    cols.append( [ T[0..NROW][i] ] )
  }
  return cols
}

7.2.1. Serializing a single field element

Unless specified otherwise, a field element, referred to as an Elt, is serialized to bytes in little-endian order. For example, a 256-bit element of the finite field F_p256 is serialized into 32-bytes starting with the least-significant byte.¶

• write_elt(e, F): produces a byte encoding of a field element e in field F.¶

7.2.2. Serializing an element of a subfield

In some cases, when both Prover and Verifier can explicitly conclude that a field element belongs to a smaller subfield, then both parties can use a more efficient sub-field serialization method. This optimization can be used when the larger field F is a field extension of a smaller field, and both parties can conclude that the serialized element belongs to the smaller subfield.¶

• write_subfield(Elt e, F2, F1): produce a byte encoding of a field element e that belongs to a subfield F2 of field F1.¶

B.1.1. Vector 1

• Leaves: 4bf5122f344554c53bde2ebb8cd2b7e3d1600ad631c385a5d7cce23c7785459a dbc1b4c900ffe48d575b5da5c638040125f65db0fe3e24494b76ea986457d986 084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5 e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71 e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db¶
• Root: f22f4501ffd3bdffcecc9e4cd6828a4479aeedd6aa484eb7c1f808ccf71c6e76¶
• Proof for leaves (0,1): 084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5 f03808f5b8088c61286d505e8e93aa378991d9889ae2d874433ca06acabcd493¶
• Proof for leaves (1,3): e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db 084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5 4bf5122f344554c53bde2ebb8cd2b7e3d1600ad631c385a5d7cce23c7785459a¶

B.2.1. Vector 1

• Description: Circuit C(n, m, s) = 0 if and only if n is the m-th s-gonal number in F_p128. This circuit verifies that 2n = (s-2)m^2 - (s - 4)*m.¶
• Field: 2¹²⁸ - 2¹⁰⁸ + 1 (Field ID 6)¶
• Depth: 3 Quads: 11 Terms: 11¶
• Serialization: 01060000010000010000020000040000020000040000ffffffffffffffffffffffffffefffff00000000000000000000000000f0ffff01000000000000000000000000000000fdffffffffffffffffffffffffefffff030000060000030000000000020000000000000000000000080000040000010000000000030000020000020000020000040000080000000000000000000000020000060000000000000000000000040000000000000000030000090000020000000000020000020000020000000000020000020000020000000000020000040000000000000000020000030000030000040000020000¶

B.3.1. Vector 1

• Description: Circuit C(n, m, s) = 0 if and only if n is the m-th s-gonal number in F_p128. This circuit verifies that 2n = (s-2)m^2 - (s - 4)*m.¶
• Field: 2¹²⁸ - 2¹⁰⁸ + 1 (Field id 6)¶
• Fiat-Shamir initialized with¶
• Serialization: 90e734c42b5f14ee432a0ed95ba2ada05c3f9ecc9b026ded61f00bf57434f93c6f70e9c8b6e3de005ba8b4da93b5fa35fc3efae1e6068399c7f7d009ab5a2711084c97cd5a6e28dd30c598907b328d81915e487c34dbf80aa5da14f0621011a33d838a7b0d9a03533c63c6606f5360f88cf97c728630afdcb9755894a6f5c9068e1fc29f97efc125ba580de64089c6e72433de2a3267b90daeaf418ac8a3df3bbddc6cb141c764c8262346baac2e28033778b1a71f153ba571e80ab29951f9440ba93fede225a35accf6e0114d5240ae92df02d2870e5258ebba416f3d815e1554b05627998fc9d3bf354b89394b27b39f69c6538dbc968a779369e47f214252e0955624e9f4d6dc2a95cf41c57703b8749b959315458d4076f0daf5fdbde23e16c10394ac884ab9cad0782e8f472cb4edb69682d17465363691aafc31b83cd764fb909b50e2fe907fd2137566ddb8c47cc13974957e7f76180860571035f7a4d2658a82e1be8fe155353bc10feae9541365926f0646b4a5351907cbd5d9dbb4¶

B.4.1. Vector 1

• Description: Circuit C(n, m, s) = 0 if and only if n is the m-th s-gonal number in F_p128. This circuit verifies that 2n = (s-2)m^2 - (s - 4)*m.¶
• Field: 2¹²⁸ - 2¹⁰⁸ + 1 (Field id 6)¶
• Witness vector: [1, 45, 5, 6]¶
• Pad elements: [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 4, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 4]¶

• Parameters:¶

  • NREQ: 6¶
  • RATE: 4¶
  • WR: 20¶
  • QR: 2¶
  • NROW: 7¶
  • NQ: 1¶
  • BLOCK: 51¶
• Commitment: 738d2ffb3a8bf24e7aedb94be59041fb2dc13da30fe6b05ebe5126ef8fc36ec2¶
• Proof size: 3180 bytes¶
• Proof: fa8d88a73b3a0f9c067658c45bb394a602000000000000000000000000000000fa8d8...2cd5f61cd2b2eb84c79e1707cbad0048fcd820c716584f31991cf1628fb041¶