In the past year, there have been a number of new ZK proof systems. One that interests us the most is Binius from Irreducible (formerly known as Ulvetanna). We pay specific attention to this proof system because our portfolio company, RISC Zero, who has been developing the RISC-V zkVM, told us that Binius will be the next generation proof system and we should keep an eye on. Eddy Lazzarin, CTO of a16zcrypto, also has put Binius "as a top priority" for their proof system, Jolt. We want to provide a high-level explanation of the Binius protocol. There are two papers on Binius: Ligero-Binius (2023) FRI-Binius (2024) We will dedicate two articles for Binius. In this article, we will explain Ligero-Binius, which is simpler, as the first step for understanding Binius.

Foreword: This research article was first published in the tech blog of our portfolio company, Polyhedra ($ZK), which is moving toward Bitcoin scalability and interoperability. L2 Iterative contributed this article for Polyhedra. Polyhedra has been expanding itself to work on emerging areas of the entire blockchain landscape with zero-knowledge proofs. Previously, we have been focusing on Ethereum and have research on how zero-knowledge proofs can contribute to the Ethereum ecosystem, and we built zkBridge (https://zkbridge.com/), which provides zero-knowledge proofs for securing the LayerZero cross-chain messaging protocol. Today, we turn our attention to Bitcoin. In particular, we study how to verify ZK proofs on Bitcoin. We are not the first to explore this problem. So, we start this article with a brief history of how human beings have tried to bring zero-knowledge proofs to Bitcoin. A brief history The most ambitious attempt in recent years was to verify a BLS12-381 proof on Bitcoin SV, by the team at sCrypt, but this attempt doesn’t work for Bitcoin—Bitcoin SV (BSV) is a hard fork of Bitcoin, an entirely separate chain today, with many differences. Particularly, BSV supports new opcodes that Bitcoin doesn’t support, and has higher script size limits. The transaction that sCrypt used to verify a BLS12-381 proof, which can be found here, lavishly uses these new opcodes, such as OP_NUM2BIN, OP_SPLIT, OP_CAT. This transaction is fairly big—26MB—which is not possible in Bitcoin, as the maximum possible block size is 4MB, and the Bitcoin block interval is about 10 minutes—we need to leave space for other transactions to get settled as well. image15

We recently looked into verifying FHE using zero-knowledge proofs (ZKP) because it is crucial in two emerging use cases. Off-chain computation for fhEVM: Fhenix and Inco are working on L1 chains that augment EVM with fully homomorphic encryption based on Zama's fhEVM, where fhEVM stands for fully homomorphic Ethereum Virtual Machine (EVM). Off-chain computation can save validators from the need to rerun FHE computation (scalability) and may be able to further hide the functions (privacy). FHE mining: Inspired by Aleo's proof of succinct work (PoSW) and the ZPrize initiatives, we consider FHE mining to be a notable future direction to encourage ASIC manufacture for FHE and incentivize FHE miners to become validators for fhEVM networks. The core task of FHE mining is to develop a ZKP system for PoSW in FHE contexts. Among the different FHE schemes, we are particularly interested in TFHE that Zama used. This implementation of TFHE uses a modulus p = 2^64, selected for its computational efficiency on modern CPUs and other hardware platforms. Our interest in verifying FHE in this setting stems from its immediate applicability in fhEVM. However, employing a modulus of p = 2^64 presents significant challenges for ZKPs, as there are limited zero-knowledge proof systems effectively compatible with this modulus. Most zero-knowledge proof systems are designed to operate within a field, but modulus p = 2^64 does not form a field, as exemplified by the lack of a modular inverse for 2, making it merely a ring. We have a zero-knowledge proof system called Rinocchio that is designed for rings, but it does not work here because it only supports (1) arbitrary rings if the ZKP is designated-verifier, which is not suitable for blockchain applications and (2) rings associated with secure, composite-order pairing-friendly curves, which would not be compatible with p = 2^64.