Binius V0

Overview

This section documents the historical Binius V0 system, which has been sunset in favor of Binius64. Binius V0 was designed as a flexible toolkit for creating verifiable VMs, heavily inspired by Plonky3, and introduced several novel features that advanced the state of SNARK design.

Novel Features of Binius V0

Binius V0 introduced two groundbreaking concepts to the SNARK ecosystem:

1. Tower Field Data Types

Unlike traditional SNARKs that use prime fields, Binius V0 pioneered the use of binary tower fields as fundamental data types. These towers provide:

Perfect correspondence between field elements and bitstrings
Natural support for binary operations (XOR, AND)
Efficient arithmetic without non-canonical field elements
A nested structure enabling powerful mathematical techniques

Learn more about tower fields and the data types built on them.

2. M3 Arithmetization

Binius V0 introduced Multi-Multiset Matching (M3), a revolutionary arithmetization paradigm that departs from traditional trace-based approaches:

No main trace: Instead of a global execution trace, M3 uses independent tables connected through channels
No temporality: Tables have no inherent notion of time or sequentiality
Flexible lengths: The prover can populate tables of arbitrary length as needed
Channel balancing: Correctness is verified through the balancing of abstract data channels

This approach eliminates multiplexing overhead and provides unprecedented flexibility in SNARK design.

Basic Concepts and Arithmetization

In SNARK design, arithmetization refers to techniques designed to reduce computational problems to mathematical problems. Computational problems are the ones we care about in day-to-day life (like verifying an Ethereum block), while mathematical problems are the ones amenable to treatment by SNARKs (involving finite fields, tables, and polynomials).

Binius V0's approach to arithmetization represents a significant departure from the status quo through its M3 framework, which we explain in detail in this section.

Section Contents

This documentation covers:

Arithmetization Background: Review of previous approaches and M3's innovations
Tower Fields: Mathematical foundation of binary tower fields
Data Types: The fundamental bitstring types used in Binius V0
M3 Arithmetization: The Multi-Multiset Matching framework
- Toy Example: An accessible introduction through prime factorization
- Formal Definition: Tables, channels, constraints, and flushing rules
- Collatz Orbits: Proving termination of Collatz sequences
- Lasso Lookup: Implementing lookups within the M3 framework

Comparison with Binius64

For a detailed comparison between Binius V0 and the current Binius64 system, see Binius64 vs. Binius V0. For the strategic decisions behind the transition, refer to our announcement blog post.