Workshop on Cryptography for Bitcoin

Endowing Bitcoin with the ability to verify succinct proofs has been a longstanding problem with important applications such as scaling Bitcoin and allowing the Bitcoin asset to be used in other blockchains trustlessly. It is a challenging problem due to the lack of expressiveness in the Bitcoin scripting language and the small Bitcoin block space. BitVM2 is the state-of-the-art verification protocol for Bitcoin used in several mainnets and testnets, but it suffers from very high on-chain Bitcoin transaction fees in the unhappy path (over $14,000 in a recent experiment). Recent research BitVM3 dramatically reduces this on-chain cost by using a garbled SNARK verifier circuit to shift most of the verification off-chain, but each garbled circuit is 42 Gibytes in size, so the off-chain storage and setup costs are huge. This paper introduces BABE, a new proof verification protocol on Bitcoin, which preserves BitVM3's savings of on-chain costs but reduces its off-chain storage and setup costs by three orders of magnitude. BABE uses a witness encryption scheme for linear pairing relations to verify Groth16 proofs. Since Groth16 verification involves non-linear pairings, this witness encryption scheme is augmented with a secure two-party computation protocol implemented using a very efficient garbled circuit for scalar multiplication on elliptic curves. The design of this garbled circuit builds on a recent work, Argo MAC, which gives an efficient garbling scheme to compute homomorphic MACs on such curves.

Starting with the seminal work on BitVM, techniques based on Yao’s Garbled Circuit (GC) have recently emerged as a key ingredient for constructing trust-minimized Bitcoin bridges. However, GC-based techniques are often expensive in that they involve the transmission and storage of large cryptographic encodings; a naive encoding for the problem at hand has size on the order of tens of gigabytes. Exciting recent works BABE (Garg et al.) and Argo MAC (Eagen and Lai) demonstrated substantial improvement by integrating Yao-style garbling with so-called decomposable affine randomized encodings (DAREs) aka information-theoretic garbled circuits (IT-GCs). This integration led to encodings on the order of tens of megabytes — dramatically improved, but still large. The bottleneck of these recent approaches is a need to convert the way values are encoded, from simple bit-by-bit Yao-style garbled labels to efficient IT-GC-style labels. This conversion is essential, as Yao-style labels have a simple property crucial to the Bitcoin setting — projectivity, which means input values are encoded in a straightforward bit-by-bit manner. Existing works take a natural approach to the conversion, leading to the need to transmit and store an encoding whose size grows roughly quadratically in the size of the labels output by the conversion.

Our work combines and extends modern advances in garbled circuits to substantially improve this Yao-style to IT-GC-style label conversion, ultimately leading to an encoding that scales only linearly with the output labels — crossing the border is duty-free. We use our improved conversion technique as a drop-in replacement for the natural conversions used by prior works. At the cost of a modest increase in local computation, we improve the total size of the garbled encoding for BABE (resp. Argo MAC) by 45x (resp. 20x).

This work was completed in collaboration with Alpen.

Garbled circuits underpin a growing class of Bitcoin protocols — bridges, vaults, and covenant-like constructions — that express rich spending conditions without consensus changes. These rest on garbling correctness: a verifier must be convinced that a garbled circuit was produced honestly from an agreed Boolean circuit. The standard tool is cut-and-choose, in which the garbler commits to many circuit copies and opens a random subset; verifier communication and storage therefore grow as O(k·n) in the security parameter k and circuit size n.

We replace cut-and-choose with a direct succinct proof. Given a public Boolean circuit and a commitment to the garbled tables, we prove that the committed tables are a correct garbling of the circuit under a Free-XOR scheme, and recursively compose per-gate local proofs into a single final artifact. Verification then costs O(1) in added communication and storage, independent of n, for arbitrary circuits.

We present the construction and two implementations: a STARK-recursive prover for Free-XOR garbled circuits, and a Nova-based IVC prover for the same garbling-correctness statement, with the STARK prover reaching 25k gates/s on commodity hardware.

Abstract coming soon.

Abstract coming soon.

For many applications of SNARKs, a key bottleneck is proving large batches of standard cryptographic hash evaluations, such as SHA-256, Keccak, or BLAKE3. We introduce Flock, a hash-based SNARK for extremely fast proving of such batched Boolean computations. Flock proves batches of the same R1CS circuit (plus input/output relations between them), can prove hash-chains and Merkle path openings, and in principle can be extended to full-fledged hash- based signature verification. At its core, Flock combines new optimizations for the lincheck and zerocheck protocols with an aggressively optimized proof-of-concept implementation co-designed by coding agents.

On a single core of an M4 Max processor, Flock proves 82k evaluations of the BLAKE3 compression function, 42k SHA-256 compressions, and 30k Keccak permutations per second — less than a 250x overhead over native execution. On ten cores, throughput exceeds 660k BLAKE3 compressions per second; in proving SHA-256, Flock is more than 9x faster than Binius64, the prior state of the art, and more than 500x faster than the fastest elliptic curve-based SNARK we measured against.

Abstract coming soon.

Abstract coming soon.