Binius's Arithmetization

In SNARK design, arithmetization refers to any among a number of techniques designed to reduce computational problems to mathematical problems. Computational problems are the ones we care about in day-to-day life. For example:

Mathematical problems are the ones amenable to treatment by SNARKs. These latter statements typically involve finite fields, tables and polynomials. For example:

Mathematical problems are the ones we can solve; computational problems are the ones we want to solve. Arithmetization amounts to bridging the gap between these two—ideally, in as efficient a way as we can.

In this section of the site, we explain Binius's approach to arithmetization.

Section Directory

This section contains the following subsections:

• Background. Here, we informally review various previous approaches to arithmetization.
• Data Types. Here, we explain the datatypes made available in our arithmetization scheme. Roughly, Binius's fundamental types are bit-strings of power-of-two width.
• Multi-Multiset Matching. Binius introduces a new arithmetization schema, which is purely declarative. In this subsection, we explain our scheme, beginning with examples, and progressing into a more formal specification.
• Merkle–Patricia Inclusion. Here, we train the full power of M3 onto a particular problem: generating proofs of Ethereum MPT membership.