Proposal for development of a "universal verifier" #511
Comments
|
Great proposal, universal verifier is very necessary. The size of a single vk is a little bit larger than that of a specific stark vk (it doesn't matter, it's basically a constant size anyway), but if there are multiple projects, one universal vk is enough instead of multiple. By the way, if proofs can be stored in ephemeral data areas, such as blobs, can existing stark projects do this? Why do zkrollup such as zksync need to wrap a layer of snark to increase the prove work? |
Thanks for the feedback! I agree that "true" verification keys could get quite large since they have to include the a full description of the AIR constraints. For example, the Risc0 recursive STARK constraints encodes the constraints into 643 instructions, which would serialize to about 9kb given their current implementation. In the future, it could make sense for this project to evolve to also define a "universal prover", with a fixed arithmetization that could be hard-coded into the deployed verification algorithm. The main purpose of the VM would be recursive verification, making it easy to "wrap" a non-native proof into a native one for this verifier. Specifying such a prover could prove complicated as it requires
It may however be a lot simpler to let blockchains that implement this verifier to provide a set of enshrined verification keys for some well-established provers. When using one of these provers, users would only have to send a hash of the verification key rather than the key itself. User-supplied verification keys for custom arithmetizations would still be supported. Moreover, it makes it easier to upgrade keys in the case where the constraints may be unsound.
As I understand it on Ethereum, proofs must be included in the calldata rather than blobdata since the latter is not accessible by the smart contract. So while it is possible to verify STARK proofs on-chain, it can get very expensive due to the large proof sizes. By wrapping a STARK proof in a Groth16/PlonK proof, the transaction gets a lot cheaper since there is less data to store, but this comes at the cost of extra latency. One of the reasons why contracts cannot access blob data is that the contract must ensure that the state can be recomputed and verified when the blob data is no longer available. There would have to be special semantics to indicate that the function which verifies the STARK proof only needs to be run during the first ~18 days after the transaction was posted. After that, we can trust that enough validators have actually verified the proof and skip verification of the public IO. In other words, ZK proofs within a transaction need to be handled separately from the state transition so that they can be safely purged once the transaction is accepted into the blockchain's state. This verifier allows blockchains to start experimenting with storing proofs in blob data independently from the execution layer. For instance, they could start be allowing the signature to be replaced by STARK proof, as a way of asserting that the transaction as a whole is valid, enabling more complex authentication methods. Blockchains could also expose STARK verification as a precompile which would have special access to the proof in the blobs. |
Ah yes, I forgot it. Thanks for the detailed reply! |
For constraint encoding, I want to propose using the format defined here. It is currently specified using JSON, the encoding could be changed pretty easily (some options could be efficient binary encoding, encoding as a stream of field elements etc.). Rust-based representation should be pretty close to how Plonky3 The main advantage of the format is that is is quite general and should accomodate basically any type of AIR constraints. For example, it supports:
As far as I can tell, the main drawback of the format is that it only encodes a single "chiplet" (or "chip"). So, to handle multi-chiplet AIR constraints, it would need to be extended - but I don't think that should be too difficult. |
|
Thank you very much for sharing this document, it's great to see other efforts that are pushing for more compatibility between projects! As you correctly identified, it is almost exactly what we would need for the proposal, modulo support for multiple chips for which I wanted to share some more details here, and some background for those following along. Background on multiple chipsA multi-chip STARK can be viewed as a batched proof of multiple smaller traces. Here we refer to a trace as a list of multiple segments, where each segment corresponds to a matrix of witness values committed to in a distinct IOP round. Each segment in a trace has the same height, but the width may vary. It's common for a trace to have 3 segments for the preprocessed, main, and permutation rounds. When there are multiple chips, each trace can have a different height, which avoids having to pad columns for different independent constraints to the same size. Using the Mixed Matrix commitment scheme, the prover can batch-commit to all the chips' segment of a given round as a single Merkle tree. This optimized commitment scheme requires the multi-FRI PCS implemented in plonky3 and is the used by several existing STARK projects. For this reason, we want to support the concept of multiple chips to ensure these projects can be compatible with this verifier. The set of constraints for each chip are related in two ways. First, they all have access to the same set of global variables which include the public input vector, as well as all the challenges sampled in each round. Having access to the same permutation challenges is the second way in which chips can be related, since it enables the chips to participate in a shared permutation/lookup argument. Concretely, these arguments are usually implemented using product/sum-check, where the prover supplies for each chip one or more claimed partial products/sums of values in the trace, which are stored as part of a chip's local variables. The verifier then asserts that the product/sum of all these elements over all traces equals one/zero. To capture the many different implementations of these arguments across projects, these conditions will also have to be encoded as constraints, which is what the Proposed modificationAfter playing around with a toy implementation of the format, I propose the following modifications that would allow the same format to be used to describe both local/chip constraints and global constraints. The top-level evaluator struct would have to contain a list of descriptions for each chip, which would additionally define how many local variables it expects. These would refer to any permutation "hints" and can be referenced both by the local chip and global constrains. We also need to modify the Global constraints will need additional restrictions in order to be considered valid:
With this modified format, it remains possible to derive the constraints of a single chip with the original format, with the following steps:
Finally, I think it's interesting to note that with the above modifications, the format differs from the verification key format in only a few fields. Namely, we would only need to add some metadata fields for the hash and commitment scheme, as well as a commitment for the preprocessed segments. Let me know if you have any thoughts on my proposed changes. |
Scope
STARKs (Scalable Transparent Argument of Knowledge) are increasingly favored as a proof system due to their ease of use and continuously improving performance characteristics. Their growing popularity is largely driven by the plonky3 project, which offers a comprehensive toolbox of cryptographic building blocks that can be readily combined to create a complete STARK prover and verifier.
The main drawback of STARKs v.s. SNARKs is the poly-logarithmic proof size, stemming from the use of Merkle trees as commitment scheme. This makes them very expensive to verify on-chain, and as a result, the proofs are commonly "wrapped" in a SNARK proof that simply verifies the STARK proof, resulting in a constant-sized proof. Unfortunately, this approach greatly increases the proving time latency, since the proof must be iteratively verified by provers in different configurations in order to transform it into a format that can be handled by a SNARK. The current cost modeling in blockchains currently makes it impossible to take any other approach, since the storage cost of the proof, and the large number of hash computations would cost far too much gas.
In the last few years, the blockchains have started experimenting with and adopting the idea of ephemeral storage for transaction data. The main observation is that a subset of the transaction data does not need to be permanently stored on-chain, but only made available for a certain time window. This includes for example the actual signature, or "blobs" that enable fraud proofs. The transaction becomes part of the chain history once this data has been verified by a sufficient number of nodes during this period.
With this point of view, a STARK proof that validates a transaction can also be considered as ephemeral data, just like a signature. The proof no longer needs to be stored permanently, as long as nodes are able to verify the proof during the availability window.
In order to enable blockchains to start experimenting with this type of STARK verification, they will need access to a verifier that would enable them to accept proofs produced by different projects. It should be simple, and absolve them of having to handle the many different ways of defining a STARK. This verifier is expected to evolve over time as new research is published, techniques are discovered, and underlying primitives advance.
The goal of this issue is to work towards defining the requirement and initial plonky3-based implementation of a "universal verifier" and gather feedback and input from other STARK-based zkVM projects.
Doing so will enable the definition of a stable verifier and proof format specification, reducing risk of adopting STARK verification for use in low-velocity codebases (e.g. blockchains).
By targetting this verifier, STARK provers would be able to drastically reduce their latency by replacing their STARK-to-SNARK pipeline with a single compression step.
In this document, we propose an initial step in this direction with a draft specification of the types of STARK proofs, which follows from an analysis of various configuration options the verifier would support, both initially and in future versions.
We invite projects to review and propose any changes required to support their proving system.
The ultimate goal would be in enabling wider adoption of STARK proofs for every zkVM.
We note that the initial version of the prover will likely be limited to verifying proofs created with a plonky3-based prover, as it relies on existing implementations of certain primitives. Initially, projects would be able to configure a specialized version of their recursive prover to target this verifier, using the same versions of the primitives used by the verifier. In the future, it may be possible to support simplified versions of the primitive to enhance interoperability with other provers. Accepting that some project outside of the plonky3 ecosystem may find that targetting this verifier to be too complex, this project could evolve to define a prover capable of verifying different proof formats/systems.
In this document, we will outline a set of modalities we think this verifier should incorporate. The criteria for selecting them should take into account the impact on
plonky3toolboxChoice of parameters
There are many different ways to configure a STARK prover, ranging from the choice of cryptographic primitives (hash function, field, PCS), the Air definition (description of constraints, lookups, and trace shapes), to the security parameters (blowup factor, number of queries). Supporting all these variants in a single verifier would increase complexity and make it harder for implementers to choose the appropriate ones.
We propose a conservative set of parameters that should garner wide support among existing projects, acknowledging that these will likely evolve as new primitives and techniques are adopted
Cryptographic primitives
In plonky3, the base cryptographic primitives of a STARK configuration are given as associated types of a
StarkGenericConfig. They implicitly define the hash function used for Fiat-Shamir challenger, the field (and extension) over which the Air constraints are defined, and the polynomial commitment scheme.Since these parameters are generic, the verifier will have to be instantiated with a few select triples of possible configurations.
Hash functions and Challenger
plonky3 exposes several base hash functions that are used to instantiate the
Challengerabstraction for Fiat-Shamir. Since the verifier would be deployed within a blockchain node, we chose to ignore set of algebraic hashes as these are mainly useful in the context of a recursive verifier. At the moment, plonky3 supports both BLAKE3 and Keccak as native hashes as they lead to optimal proving time.Most blockchains already incorporate Keccak into their stack, though BLAKE3 does not have as much support (though several blockchains support the previous BLAKE2b). This is not necessarily an deployment problem, since the implementation of the verifier would not be calling into the existing interfaces for these, and instead rely on the libraries already included in plonky3. However, some blockchains may be more reticent to including a new hash function into their overall cryptographic stack.
We propose that the initial version of the verifier only exposes Keccak due to its wider adoption and existing support in most blockchains.
Regarding the challenger abstraction, we can use one of the existing
DuplexChallengerorHashChallenger.Note
Feedback would be appreciated to understand which trait to use, specifically in the case where Keccak is the underlying hash/permutation.
Field
One of the core use-cases of this universal verifier will be to recursively verify a larger STARK prover with parameters optimized for maximum prover performance. The field used by the verifier will therefore have to be the same in order to avoid non-native field arithmetic. We will want to be compatible with these configurations.
Most currently deployed STARKs are currently using either the
baby-bearorgoldilocksfields, as they exhibit both high two adicity and good prover performance on either CPUs or GPUs. Recent works have also shown the practicality of using themersenne-31field, enabling faster arithmetic. We also note the lesser-knownkoala-bearthat would improve the performance of the Poseidon2 hash function for a recursive prover.For an initial verifier implementation, limiting the suites to only include
baby-bearandgoldilockswould ensure compatibility with almost all existing proof systems. It would also lay the ground work for including other fields such asmersenne-31andkoala-bearin future iterations, when they start being adopted by more projects.PCS (Commitment scheme and opening protocol)
plonky3 currently only supports the FRI polynomial commitment scheme (including the CircleSTARK variation for
mersenne-31), using the Mixed Matrix Commitment Scheme (MMCS) for committing to multiple traces of varying sizes using a single Merkle tree. More precisely, the opening protocol actually implements Multi-FRI in order to take advantage of this specialized commitment scheme. The initial version of the verifier would be limited to supporting this configuration since others are not yet implemented.While both the commitment scheme and opening protocol are tightly linked, it might be beneficial to consider both as separate configuration options. In the case where the PCS opening protocol supported by the verifier is upgraded while remaining compatible with existing commitments, existing verification keys containing preprocessed trace commitments could stay the same. The specific version of the opening protocol would therefore become a configuration option defined by the proof itself.
Supporting
mersenne31with CircleFRI in a future iteration seems obvious, and it will make sense to upgrade verifier with support for it once it becomes more widely adopted by existing projects. We will also likely see an implementation of STIR added to plonky3. While it may require some extra work to be compatible with the aforementioned MMCS protocol, the improvements in verifying time and proof size may warrant the introduction of a simplified commitment scheme using the same rate for every column, at the cost of potentially introducing padding.While it would be relatively easy for plonky3 based projects to create proofs for the PCS supported by the verifier, projects based on other stacks may find it hard to support the exact same implementation and serialization format. If there is enough support from these teams, we could in the future consider supporting a "simplified" PCS which would be easier to implement a compatible prover using a different stack. One candidate would be a version of FRI restricted to a single matrix, or SMCS (Single Matrix Commitment Scheme).
Note
Compatibility with existing proofs could also be achieved by using a plonky3-based prover, and use it to verify a STARK produced by a non-plonky3 prover. This is however beyond the scope of the current proposal, as we are not interested in defining a "universal prover" at this stage.
Initially, we propose only supporting the current FRI implementation in plonky3 for the
baby-bearandgoldilocksfields. Once there is more adoption, adoptingmersenne31with circle FRI would be a clear future goal.In order to minimize the maintenance burden from supporting multiple PCS in the future, a deprecation protocol could be put into place to upgrade the set of selected PCSs. If a "simplified" PCS is supported at some point for maximizing compatibility, it would make sense to offer a longer support commitment. This allows us to restrict the number of supported PCSs to at most two per field at any given time.
Proposed Configurations
The following table summarizes the different configurations that could be supported, and an approximate time-line of when they might be integrated.
babybear,goldilockskeccackMMCSFRImersenne31C-FRIkoalabearblake3SMCSSTIR,C-STIR?,"SimpleFRI"Verification key and proof structure
The Verifier Key should represent a succinct representation of a VM's arithmetization over a specified field. This is not currently the case for most deployed verifiers, as parts of VM's description are hardcoded into the algorithm itself (number of columns, constraints, ...). To accommodate all VMs, this verifier will have to define a fixed format for encoding the arithmetization, with the goal that it does not require upgrading with potential future updates to the verifier. It would be conceivable that the verification key format adopts more configuration options over time, as new features are implemented in the verifier that enable more efficient arithmetizations. Previous versions would remain supported unless there are clear reasons (mainly security) for dropping support. For this reason, it is important to version verification keys and proofs.
Serialization
The verification key itself should be serializable, and will have to be provided as input to the
verifyfunction at every call, along with a proof. Figuring out whether certain configuration options should be kept in the key or the proof will require consensus among different parties. For example, we could store all the contents of the verification key inside the proof, and only pass a hash of the key to theverifyfunction, and let the verifier ensure the hash matches. While this would require significantly less long-term storage, it would increase the proof size with data that would be identical for all proofs of that key. In contrast, the full verification key could be stored on a blockchain ensuring proofs only contain data pertinent to a particular execution. While we explore the tradeoff space of these options and whether these different modalities make sense, we propose the second option as it provides an easier starting point.Practically, we propose using JSON as the serialization format to maximize compatibility.
Security
Another crucial aspect of a VM's configuration is the security level that should be enforced for a specific proof. While it would be possible to encode a desired security level in either the verification key or the proof, we argue that it should be a separate parameter to the
verifyfunction. The application itself should be able to decide what level of security it requires. For the same VM arithmetization, the number of bits of security could depend on the outcome that gets executed if the proof is accepted. Many projects will also have different threat models affecting whether any conjectures can be acceptable.Concretely, the caller specifies a minimum number of bits of security, along with
Supported STARK shapes
The "shape" of a STARK can be viewed as the parameters of the underlying IOP. While it would be possible to define the verifier in a way that supports arbitrary IOPs, we chose to restrict it to the one deployed by most current projects. That is, we want to support STARK composed of
Given the broad usage of MMCS by plonky3 projects, commitments should be able to represent multiple matrices. This can be represented using the established chip notion in plonky3. Each chip represents an independent Air, which can be connected to each other using the permutation argument. Since each chip defines its own quotient, we can view this construction as a batched STARK. The shapes of these chips would be defined as part of the verification key.
Constraint encoding
Each chip defines its own constraints which includes any permutation constraints implementing a permutation or multi-set argument. By specifying a generic encoding for these polynomial constraints, the verifier can support arbitrary constraints without needing to enshrine a particular permutation protocol.
As a starter, constraints could be encoded by serializing the
SymbolicExpressionthough it would need to be adapted to work for constraints defined over extension field elements as well, in a similar way to Valida'sSymbolicExpressionExt. A more optimal format could be inspired by Risc0's implementation of constraints, where they are represented as a list of operations resulting in the evaluation of a polynomial.While most plonky3 projects only define Airs with constraints spanning over two consecutive rows, supporting arbitrary window sizes would make it easier to support existing VMs that make use of the feature.
Draft structures
As an initial draft, we propose the following high level description of the structures representing a verification key and a proof. These are likely to change to mirror a concrete implementation of the verifier.
The text was updated successfully, but these errors were encountered: