Abstract.
We present Accordion, a new proof system that works in two steps:
– Accumulate: The first building block is a multi-folding scheme that
efficiently accumulates k different instances of a degree-d polynomial relation into
a single accumulated instance, without using recursion. Our scheme builds on the
Protostar and Protogalaxy line of work, improving further the verifier efficiency.
It supports the same expressive class of relations, arbitrary-degree polynomial constraints,
enabling efficient folding for CCS, Plonkish constraints, and even custom gates.
– Decide: The second block is a SNARK decider for the folding scheme, which efficiently
proves the validity of the resulting accumulated instance using off-the-shelf optimized
building blocks. We give a concrete instantiation consisting of a Plonk-based proof plus
an additional KZG polynomial commitment opening.
This design is especially attractive in batch-aggregation settings where
a prover collects many independent witnesses, folds them into a single accumulator,
and then runs one succinct decider to certify the entire batch. Our scheme avoids
costly recursion overheads. We implement Accordion and evaluate it against a highly
optimized Plonk proving pipeline (midnight-zk). For k =64 instances, Accordion is
up to 2.5 times faster than computing k Plonk proofs for SHA-256 preimages,
with a 3 times faster verifier and 4 times smaller proofs. Its prover is also
an order of magnitude faster than using IVC to aggregate the k proofs.
Abstract.
Folding schemes are gaining traction recently as they unlock practical instantiations of
incrementally verifiable computation (IVC) and proof-carrying data (PCD). In particular, there has
been a growing interest in folding sches for high-degree relations, as these can efficiently arithmetize
complex computations. While the landscape of folding schemes is vast, all existing constructions based
on lattices, such as Latticefold+,(Super)Neo and Cyclo, heavily
rely on the sumcheck protocol. Sumcheck leads to very efficient proving times, but also presents draw-
backs: the folded relations must be expressed by products of multilinear polynomials, and the verifier
circuits become very large, partially because of the many random oracle calls required.
When folding sequential computations, this significantly inflates the recursive overhead, as the prover
must run the verification at every iteration.
We present ProtogaLattice, a new lattice-based folding scheme for general high-degree polynomial
relations that drastically reduces the size of the verifier’s circuits. Our folding backbone deviates from
the sumcheck approach and uses algebraic techniques. Our contribution is twofold:
i) folding scheme that combines multiple instances of polynomial relations into accumulators for a
bounded number of iterations, and
ii) a bootstrapping protocol to reduce the norm of the witnesses underlying these accumulators, which
can be used in complement to our bounded-depth folding scheme to unlock unlimited depth.
A full iteration of ProtogaLattice for witnesses of length 2^30 gives a 4 times shorter proof size than the
state-of-the-art, with only 8.13 KB. Additionally, ProtogaLattice requires less random oracle evaluations
and achieves a smaller verifier circuit than its sumcheck counterparts.
Our techniques open new directions towards building efficient lattice-based proofs for expressive
relations and that present small recursion overheads, challenging the established sumcheck-based approaches.
Abstract.
We develop formal code-based security definitions for
blockchain bridges and apply them to several bridge architectures
deployed in practice. We derive both traditional pen-and-paper
proofs and on the other, automated guarantees against bounded
counterexamples. The latter is achieved via bounded model
checking of our formally specified properties, implemented in
Quint, a specification language and model checker closely related
to TLA+.
Our definitions are expressed in a precise, code-based variant
of the Universal Composition (UC) framework. This enables the
modular use of hybrid functionalities—even for property-based
definitions—and is essential for bounded model checking, where
underlying primitives must be idealized.
Accordingly, we idealize and model-check all building blocks
used in our protocols. Notably, we formulate a novel UC ideal
functionality for Advanced Threshold Signatures (ATS) and modelcheck it for attacks to ensure its robustness.
Abstract.
In this work, we consider the setting where one or more users with low computational resources would lie to outsource
the task of proof generation for SNARKs to one external entity, named Prover.
We study the scenario in which Provers have access to all statements and witnesses to be proven beforehand. We take a different approach to proof
aggregation and design a new protocol that reduces simultaneously proving
time and communication complexity, without going through recursive proof composition.
Our two main contributions: We first design FLIP, a communication efficient folding scheme
where we apply the Inner Pairing Product Argument to fold R1CS instances of the same language into
a single relaxed R1CS instance. Then, any proof system for relaxed R1CS language can be
applied to prove the final instance. As a second contribution,
we build a novel variation of Groth16 with the same communication complexity for
relaxed R1CS and two extra pairings for verification, with an adapted trusted setup.
Compared to SnarkPack - a prior solution addressing scaling for multiple Groth16 proofs - our scheme improves
in prover complexity by orders of magnitude, if we consider the total cost to generated the SNARK proofs
one by one and the aggregation effort.
An immediate application of our solution is Filecoin, a decentralized storage network based on incentives that
generates more than 6 million SNARKs for large circuits of 100 million constraints per day.
