Formally Verified Cryptographic Arguments
This library aims to provide a modular and composable framework for formally verifying (succinct) cryptographic arguments (e.g. SNARKs) based on Interactive (Oracle) Proofs. This is done as part of the verified-zkevm effort.
In the first stage of this library's development, we plan to formalize interactive (oracle) reductions (a modular way of stating IOPs) and prove information-theoretic completeness and soundness for a select list of protocols (see the list of active formalizations below).
For each protocol, we aim to provide:
- A specification based on
Mathlib
polynomials, - An implementation of the prover and verifier using computable representations of polynomials,
- Proofs of completeness and round-by-round knowledge soundness for the specification, and proofs that the implementations refine the specifications.
Library Structure
The core of our library is a mechanized theory of
- An
-IOR is an interactive protocol between a prover and a verifier to reduce a relation on some public statement & private witness to another relation . - The verifier may not see the messages sent by the prover in the clear, but can make oracle queries to these messages using a specified oracle interface;
- For example, one can view the message as a vector, and query entries of that vector. Alternatively, one can view the message as a polynomial, and query for its evaluation at some given points.
- We can compose multiple
-IORs with compatible relations together (e.g. and ), allowing us to build existing protocols (e.g. Plonk) from common sub-routines (e.g. zero check, permutation check, quotienting). - We can also carry out the BCS transform, which takes an
-IOR and compose it with -commitment schemes to result in an interactive argument.
- Roughly speaking, an
-commitment scheme is a commitment scheme with an associated opening argument for the correctness of the specified oracle interface. - The BCS transform then replaces every oracle message from the prover with a commitment to that message, and runs an opening argument for each oracle query the verifier makes to the prover's messages.
-IOR is a natural notion and related versions have appeared in various places in the literature (see BACKGROUND for a detailed comparison). Our library takes these existing threads and formalizes them into a cohesive theory.
Using the theory of
Active Formalizations (last updated: April 30th 20205)
The library is currently in development. Alongside general development of the library's underlying theory, the following cryptographic components are actively being worked on:
- The sumcheck protocol
- A blueprint for FRI and coding theory pre-requisites
- A blueprint for STIR and WHIR
- Binius
VCV-io, ArkLib's main dependency alongside mathlib is also being developed in parallel.
Roadmap & Contributing
We welcome outside contributions to the library! Please see CONTRIBUTING and, the list of issues for immediate tasks, and the ROADMAP for a list of desired contributions.
If you're interested in working on any of the items mentioned in the list of issues or the roadmap, please see verified-zkevm.org, contact the authors, or open a new issue.