libzk protocol draft
Upstream working document
This is a rendering-oriented mirror of vendor/longfellow-zk/docs/specs/libzk.md at the submodule revision pinned by this repository. Citation XML and Internet-Draft generation metadata were removed for VitePress; algorithms and pseudocode are preserved. Consult the IETF Datatracker and vendored source before treating any requirement as normative.
Abstract
This document defines an algorithm for generating and verifying a succinct non-interactive zero-knowledge argument that for a given input x and a circuit C, there exists a witness w, such that C(x,w) evaluates to 0. The technique here combines the MPC-in-the-head approach for constructing ZK arguments described in Ligero [@ligero] with a verifiable computation protocol based on sumcheck for proving that C(x,w)=0.
Introduction
A zero-knowledge (ZK) scheme allows a Prover who holds an arithmetic circuit C defined over a finite field F and two inputs (x,w) to convince a Verifier who holds only (C,x) that the Prover knows w such that C(x,w) = 0 without revealing any extra information to the Verifier.
The concept of a zero-knowledge scheme was introduced by Goldwasser, Micali, and Rackoff [@GMR], and has since been rigourously explored and optimized in the academic literature.
There are several models and efficiency goals that different ZK schemes aim to achieve, such as reducing prover time, reducing verifier time, or reducing proof size. Some ZK schemes also impose other requirements to achieve their efficienc goals. This document considers the scenario in which there are no common reference strings, or trusted parameter setups that are available to the parties. This immediately rules out several succinct ZK scheme from the literature. In addition, this document also focuses on schemes that can be instantiated from a collision-resistant hash function and require no other complexity theoretic assumption. Again, this rules out several schemes in the literature. All of the ZK schemes from the literature that remain can be defined in the Interactive Oracle Proof (IOP) model, and this document specifies a family of them that enjoys both efficiency and simplicity.
The Longfellow system
This document specifies the Longfellow ZK scheme described in the paper [@longfellow]. The scheme is constructed from two components: the first is the Ligero scheme, which provides a cryptographic commitment scheme that supports an efficient ZK argument system that enables proving linear and quadratic constraints on the committed witness, and the second is a public-coin interactive protocol (IP) for producing an argument that C(x,w)=0 where C is such a circuit, x is a public input, and w is a private witness. The overall scheme works by having the Prover commit to the witness w as well as a pad used to commit the transcript of the IP, then to run the IP with the verifier in a way that produces a commitment to the transcript of the IP, and finally, by running the Ligero proof system to prove that the transcript in the commitment induces the IP verifier to accept.
Basic Operations and Notation
The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119 [@!RFC2119].
Additionally, the key words "MIGHT", "COULD", "MAY WISH TO", "WOULD PROBABLY", "SHOULD CONSIDER", and "MUST (BUT WE KNOW YOU WON'T)" in this document are to interpreted as described in RFC 6919 [@!RFC6919].
Except if said otherwise, random choices in this specification refer to drawing with uniform distribution from a given set (i.e., "random" is short for "uniformly random"). Random choices can be replaced with fresh outputs from a cryptographically strong pseudorandom generator, according to the requirements in [@!RFC4086], or pseudorandom function.
Array primitives
The notation A[0..N] refers to the array of size N that contains A[0],A[1],...,A[N-1], i.e., the right-boundary in the notation X..Y is an exclusive index bound. The following functions are used throughout the document:
- copy(n, Dst, Src): copies n elements from Src to Dst with different strides
- axpy(n, Y, A, X): sets Y[i] += A*X[i] for 0 <= i < n.
- sum(n, A): computes the sum of the first n elements in array A
- dot(n, A, Y): computes the dot product of length n between arrays A and Y.
- add(n, A, Y): returns the array
[A[0]+Y[0], A[1]+Y[1], ..., A[n-1]+Y[n-1]]. - prod(n, A, Y): returns the array
[A[0]*Y[0], A[1]*Y[1], ..., A[n-1]*Y[n-1]]. - equal(n, A, Y): true if
A[i]==Y[i]for 0 <= i < n and false otherwise. - gather(n, A, I): returns the array
[A[I[0]], A[I[1]], ..., A[I[n-1]]. A[n][m] = [0]: initializes the 2-dimensional n x m array A to all zeroes.A[0..NREQ] = X: array assignment, this operation copies the first NREQ elements of X into the corresponding indicies of the A array.
Polynomial operations
This section describes operations on and associated with polynomials that are used in the main protocol.
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 >= m, 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.
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^i^, 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, this document implements GF(2^128^) as GF{2}[x] / (Q(x)) where
Q(x) = x^{128} + x^{7} + x^{2} + x + 1With this choice of Q(x), x is a generator of the multiplicative group of the field. Next, choose GF(2^16^) as the subfield of GF(2^128^) 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 encoding elements in a 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}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_iIn this setting, 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 [@longfellow] [@additivefft].
Fiat-Shamir primitives
A ZK protocol may in general be interactive whereby the Prover and Verifier engage in multiple rounds of communication. However, in practice, it is often more convenient to deploy a so-called non-interactive or single-message protocol that only requires a single message from Prover to Verifier. It is possible to apply the Fiat-Shamir heuristic to transform a special class of interactive protocols into single-message protocols.
The Fiat-Shamir transform is a method for generating a verifier's public coin challenges by processing the concatenation of all of the Prover's messages. The transform can be proven to be sound when applied to an interactive protocol that is round-by-round sound and when the oracle is implemented with a hash function that satisfies a correlation-intractability property with respect to the state function implied by the round-by-round soundness. See Theorem 5.8 of [@rbr] for details.
In practice, whether an implementation of the random oracle satisfies this correlation-intractability property becomes an implicit assumption. Towards that, this document adapts best practices in selecting the oracle implementation. First, the random oracle should have higher circuit depth and require more gates to compute than the circuit C that the protocol is applied to. Furthermore, the size of the messages which are used as input to the oracle to generate the Verifier's challenges should be larger than C. These choices are easy to implement and add very little processing time to the protocol. On the other hand, they seemingly avoid attacks against correlation-intractability in which the random oracle is computed within the ZK protocol thereby allowing the output of the circuit to be related to the verifier's challenge.
As an additional property, each query to the random oracle should be able to be uniquely mapped into a protocol transcript. To facilitate this property, the type and length of each message is incorporated into the query string.
Implementation of a random oracle
The Fiat-Shamir transform makes use of an ideal random oracle that maps an arbitrarily long string to a random element sampled from a specific domain. A protocol consists of multiple rounds in which a Prover sends a message, and a verifier responds with a public-coin or random challenge. The Fiat-Shamir transform for such a protocol is implemented by maintaining a transcript object. The transcript object is parameterized by a collision-resistant hash function H that is specified externally. For example, the SHA-256 function is a suitable choice.
The transcript object maintains an internal string tr that begins as the empty string.
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 nonce. 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. Thesession_idbyte string is appended to the end oftrfollowing the append conventions. This method must be called exactly once before any other method on thetranscriptobject is invoked.
Writing to the transcript
The transcript object supports a write method that is used to record the Prover's messages.
transcript.write(msg): appends the Prover's next message to the end of thetrstring that is maintained by 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
0x1is appended totr, and then the canonical byte serialization of the field element is appended totr.To append an array of bytes, first the byte designator
0x2is 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 totr.To append an array of field elements, the byte designator
0x3is appended, 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 totr.
Special rules for the first message
When used in the Longfellow system, 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:
- The Prover message is appended to
tr. Specifically, the length of the message, as per the above convention, is appended, and then the bytes of the message are appended. - 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 first as per convention.
- Finally, the transcript is augmented by the byte-array 0^|C|^, which consists of |C| bytes of zeroes.
One might 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 (with a random prefix) of length greater than |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.
The FSPRF object
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 defines an FSPRF object fs as follows. First, the append operations described above for each type of write are performed, resulting in a new tr string. Next, a seed is generated by applying the function H to the (entire) string tr. This seed is then used to define the FSPRF object.
The FSPRF object is defined to produce an infinite stream of bytes that can be used to sample all of the verifier's challenges in this round. The stream is organized in blocks of 16 bytes each, numbered consecutively starting at 0. Block i contains
AES256(SEED, ID(i))where SEED is the seed of the FSPRF object, and ID(i) is the 16-byte little-endian representation of integer i.
The FSPRF object supports a bytes method:
b = fs.bytes(n)returns the nextnbytes in the stream.
Thus, fs implicitly maintains an index into the next position in the stream. Calls to bytes without an intervening write read pseudo-random bytes from the same stream.
Generating challenges
When the prover has finished sending messages for a round in the interactive protocol, it can make a sequence of calls to transcript.generate_{nat,nats_wo_replacement,field_element,challenge} to obtain the Verifier's random challenges.
The bytes method of the FSPRF is used by the transcript object to sample pseudo-random field elements and pseudo-random integers via rejection sampling as follows:
transcript.generate_nat(m)generates a random natural between0andm-1inclusive, as follows. This method is defined whenm > 1.Let
lbe minimal such that2^l > m. Letnbytes = ceil(l / 8). Letb = fs.bytes(nbytes). Interpret bytesbas a little-endian integerk. Pickmaskto be the minimal bitmask such that(n & mask) == nand setr = k & mask. Ifr < mreturnr, otherwise start over.
def generate_nat(self, m: int) -> int:
assert m > 0, "m must be > 0"
l = m.bit_length()
nbytes = math.ceil(l / 8)
mask = (1 << l) - 1
fs = self._get_fs()
while True:
b = fs.bytes(nbytes)
k = int.from_bytes(b, 'little')
r = k & mask
if r < m:
return rtranscript.generate_nats_wo_replacement(m, n)generates a list ofndifferent, random natural numbers between0andm - 1inclusive. There are many equivalent algorithms to perform this step. The following approach requires onlyncalls to thegenerate_natmethod.
def generate_nats_wo_replacement(m: int, n: int) -> list[int]:
# assert(m > n)
A = list(range(0, m))
for i in range(0, n):
j = i + generate_nat(m - i)
A[i], A[j] = A[j], A[i]
return A[:n]transcript.generate_field_element(F)generates a field element.If the field
FisZ / (p), returngenerate_nat(fs, p)interpreted as a field element.If the field is
GF(2)[X] / (X^128 + X^7 + X^2 + X + 1), obtainb = fs.bytes(16)and interpret the 128 bits ofbas a little-endian polynomial. If the field is the sub-field of the above generated by the elementg=x^{(2^{128}-1) / (2^{16}-1)}, then obtainb = fs.bytes(2). Letb_irepresent theith bit ofbin little-endian and return the element\sum_i b_i * \beta_iwhere\beta_i = g^ias defined above in (#gf2k).This document does not specify the generation of a field element for other binary fields, but extensions SHOULD follow a similar pattern.
a = transcript.generate_challenge(F, n)generates an array ofnfield elements in the straightforward way: for0 <= i < nin ascending order, seta[i] = transcript.generate_field_element(F).
Optimizations
As described, the hash function H is applied to progressively longer and longer tr strings as the protocol evolves from round to round. In practice, most implementations of cryptographic hash functions provide a data-structure which allows incremental update of the state of the hash function while also allowing a digest to be computed at any intermediate point.
The commitment subprotocol is published separately in this site as the Ligero specification.
Overview of the Longfellow protocol
The Longfellow ZK protocol uses two protocol components. The first is a variant of the sumcheck protocol, modified to support zero knowledge. Informally, the standard sumcheck prover takes the description of a circuit and the concrete values of all the wires in the circuit, and produces a proof that all wires have been computed correctly. The proof itself is a sequence of field elements. Longfellow uses an encrypted-variant of the sumcheck prover that also takes as input a random and secret one-time pad and outputs an "encrypted" proof such that each element in this proof is the difference of the element in the standard sumcheck proof and its corresponding element in the pad. (The choice of "difference" instead of "sum" is a matter of convention.)
In this encrypted sumcheck variant, the verifier cannot check the proof directly because it cannot access the one-time pad. Instead of running the sumcheck verifier directly, a commitment scheme is used to hide the one-time pad, and the sumcheck verifier is translated into a sequence of linear and quadratic constraints on the inputs and the one-time pad. A secondary proof system is then used to produce a proof with respect to the commitment that the constraints are satisfied.
Some of the wires of the circuit are inputs, i.e., set outside the circuit and not computed by the circuit itself. Some of the inputs are public, i.e., known to both parties, and some are private, i.e., known only to the prover. Sumcheck does not use the distinction between public and private inputs. This document distinguishes private inputs from the one-time pad. The commitment scheme does not use public inputs at all, but it does treat private inputs and the one-time pad elements equally. These constraints motivate the following terminology.
- public inputs: inputs to the circuit known to both parties.
- private inputs: inputs to the circuit known to the prover but not to the verifier.
- inputs: both public and private inputs. When forming an array of all inputs, the public inputs come first, followed by the private inputs.
- witnesses: the private inputs and the elements in the one-time pad. When forming an array of all witnesses, the private inputs come first, followed by the one-time pad.
Thus, at a high level, the sequence of operations in the ZK protocol is the following:
The prover commits to all witness values.
The prover runs the encrypted sumcheck prover on the witness values to producing an encrypted proof, all-the-while sending the encrypted proof to the verifier.
Both the prover and the verifier take the public inputs and the encrypted proof and produce a sequence of constraints.
Using the commitment scheme and the witnesses, the prover generates a proof that the constraints from step 3 are satisfied.
The verifier uses the proof from step 4 and the constraints from step 3 to check the constraints.
Steps 2 and 3 are referred to as "sumcheck", and the rest as "commitment scheme". While the classification of step 3 as "sumcheck" is arbitrary, there are situations where one might want to use a commitment scheme other than the Ligero protocol specified in this document. In this case, the "commitment scheme" can change while the "sumcheck" remains unaffected.
Parameters needed to define Longfellow
Longfellow is parameterized by a sumcheck protocol, a commitment protocol, and a Fiat-Shamir instantiation. A selection of all three defines a Longfellow profile. This document introduces one opinionated profile that uses (a) The longfellow sumcheck described below, (b) the Ligero commitment described above, (c) the Fiat-Shamir instantiation defined above and using SHA-256 as the function H.
The interactive-proof component is published separately as the sumcheck specification.
Serializing objects
This section explains how a proof consists of smaller, related objects, and how to serialize each such component. First, the standard methods for serializing integers and arrays are used:
write_size(n): serializes an integer in [0, 2^{24} - 1] that represents the size of an array or an index into an array. The integer is serialized in little endian order.write_array(arr): A variable-sized array is represented astype array[]and serialized by first writing its length as a size element, and then serializing each element of the array in order.write_fixed_array(arr): When the length of the array is explicitly known to ben, it is specified astype array[n]and in this case, the array length is not written first.
Serializing structs
When a section includes just a struct definition, it is serialized in the natural way, starting from the top-most component and proceeding to the last one, each component is serialized in order.
Serializing Field elements
This section describes a method to serialize field elements, particularly when the field structure allows efficient encoding for elements of subfields.
Before a field element can be serialized, the context must specify the finite field. In most cases, the Circuit structure will specify the finite field, and all other aspects of the protocol will be defined by this field.
A finite field or FieldID is specified using a variable-length encoding. Common finite fields have been assigned special 1-byte codes. An arbitrary prime-order finite field can be specified using the special 0xF_ byte followed by a variable number of bytes to specify the prime in little-endian order. For example, the 3 byte sequence f11001 specifies F~257~. Similarly, a quadratic extension using the polynomial x^2 + 1 can be specified using the 0xE_ designators.
| Finite field | FieldID |
|---|---|
| p256 | 0x01 |
| p384 | 0x02 |
| p521 | 0x03 |
| GF(2^128^) | 0x04 |
| GF(2^16^) | 0x05 |
| 2^128^ - 2^108^ + 1 | 0x06 |
| 2^64 - 59 | 0x07 |
| 2^64 - 2^32 + 1 | 0x08 |
| F_{2^64 - 59}^2^ | 0x09 |
| secp256k1 | 0x0a |
| F_{2^{0--15}^-byte prime}^2^ | 0xe |
| F_{2^{0--15}^-byte prime} | 0xf |
| Table: Finite field identifiers. |
The GF(2^128^) field uses the irreducible polynomial x^128^ + x^7^ + x^2^ + x + 1. The p256 prime is equal to 115792089210356248762697446949407573530086143415290314195533631308867097853951, which is the base field used by the NIST P256 elliptic curve. The p384 prime is equal to 39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319 which is the base field used by the NIST P384 curve. The p512 prime is equal to 2^521^ - 1. The F_p64^2 field is the quadratic field extension of the base field defined by prime 18446744073709551557 using polynomial x^2 + 1, i.e. by injecting a square root of -1 to the field.
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.
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.
Serializing a Sumcheck Transcript
struct {
PaddedTranscriptLayer layers[]; // NL layers
} PaddedTranscript;
struct {
Elt wires[]; // array of 2 * log_w Elts that store the
// evaluations of deg-2 polynomial at 0, 2
Elt wc0;
Elt wc1;
} PaddedTranscriptLayer;The padded transcript incorporates the optimization in which the eval at 1 is omitted and reconstructed from the expected value of the previous challenge.
Serializing a Ligero Proof
def serialize_ligero_proof(C, ldt, dot, columns, mt_proof) {
write_array(ldt, C.BLOCK)
write_array(dot, C.BLOCK)
write_runs(columns, C.NREQ * C.NROW, C.subFieldID, C.FieldID)
write_merkle(mt_proof)
}The concept of a run allows saving space when a long run of field elements belong to a subfield of the Finite field. Runs consist of a 4-byte size element, and then size Elt elements that are either in the field or the subfield. Runs alternate, beginning with full field elements. In this way, rows that consist of subfield elements can save space. The maximum run length is set to 2^25^.
def write_runs(columns, N, F2, F) {
bool subfield_run = false
FOR 0 <= ci < N DO
size_t runlen = 0
while (ci + runlen < N &&
runlen < kMaxRunLen &&
columns[ci + runlen].is_in_subfield(F2) == subfield_run
) {
++runlen;
}
write_size(runlen, buf);
for (size_t i = ci; i < ci + runlen; ++i) {
if (subfield_run) {
write_subfield(columns[i], F2, F);
} else {
write_elt(columns[i], F);
}
}
ci += runlen;
subfield_run = !subfield_run;
}
def write_merkle(mt_proof) {
FOR (digest in mt_proof) DO
write_fixed_array(digest, HASH_LEN)
}Serializing a Sequence of proofs
For the multi-field optimization, the proof string consists of a sequence of two proofs. This is handled by using the circuit identifier to specify the sequence of proofs to parse.
struct {
Public pub; // Public arguments to all circuits
Proof proofs[]; // array of Proof
} Proofs;struct {
uint8 oracle[32]; // nonce used to define the random oracle,
Digest com; // commitment to the witness
PaddedTranscript sumcheck_transcript;
LigeroProof lp;
} Proof;
struct {
char* arguments[]; // array of strings representing
// public arguments to the circuit
} Public;Serializing a Circuit
A circuit structure consists of size metadata, a table of constants, and an array of structures that represent the layers of the circuit as follows.
struct {
Version version; // 1-byte identifier, 0x1.
FieldID field; // identifies the field
FieldID subfield; // identifies the subfield
size num_outputs; // number of outputs
size pub_in; // number of public inputs
size ninputs; // number of inputs, including witnesses
size num_layers; // number of layers
Elt const_table[]; // array of constants used by the quads
CircuitLayer layers[]; // array of layers of size num_layers
} Circuit;The const_table structure contains an array of Elt constants that can be referred by any of the CircuitLayer structures. This feature saves space because a typical circuit uses only a handful of constants, which can be referred by a small index value into this table.
struct {
size log_num_input_wires; // log of number of wires
size num_input_wires; // number of wires
Quads quads[]; // array of Quads
} CircuitLayer;The quads array stores the main portion of the circuit. Each Quad structure contains a g, h0, h1 and a constant v which is represented as an index into the const_table array in the Circuit. Each g,h0, and h1 is stored as a difference from the corresponding item in the previous quad. In other words, these three values are delta-encoded in order to improve the compressibility of the circuit representation. The Delta spec uses LSB as a sign bit to indicate negative numbers.
struct {
Delta g; // delta-encoded gate number
Delta h0; // delta-encoded left wire index
Delta h1; // delta-encoded right wire index
size v; // index into the const_table to specify const v
} Quad;
typedef Delta uint;Security Considerations
Both the Ligero and Longfellow systems satisfy the standard properties of a zero-knowledge argument system: completeness, soundness, and zero-knowledge.
Frigo and shelat [@longfellow] provide an analysis of the soundness of the system, as it derives from the Soundness of the Ligero proof system and the sumcheck protocol. Similarly, the zero-knowledge property derives almost entirely from the analysis of Ligero [@ligero]. It is a goal to provide a mechanically verifiable proof for a high-level statement of the soundness.
IANA Considerations
This document does not make any requests of IANA.
Acknowledgements
Concrete fixtures are published in protocol test vectors.