No results found

Arklib

Formally Verified Arguments of Knowledge in Lean

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 -Interactive Oracle Reductions (see OracleReduction):

  1. 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 .
  2. 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.
  1. 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).
  2. 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.
  1. -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 -IOR, we then formalize various proof systems in ProofSystem.

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.