Skip to content

Concepts

Overview of the core concepts of verifiable computing

What is a SNARK?

SNARKs are a powerful cryptographic tool that unlocks verifiable computing, a paradigm best summarized by this quote from [BFLS91]:

In this setup, a single reliable PC can monitor the operation of a herd of supercomputers working with possibly extremely powerful but unreliable software and untested hardware. –Babai, Fortnow, Levin, Szegedy, 1991

Roughly, a SNARK (a succinct, noninteractive argument of knowledge) is a proof of a computation. Let's say you're interested in learning the output of some costly, long-running computation—for example, a financial query on a large database of historical market data. Instead of forcing you to run the computation yourself, I, the prover, just tell you the output and additionally give to you a small proof file, which your computer can check very quickly.

If this system is designed well, it should satisfy two properties:

  • Soundness. Checking the proof alerts you if my claimed output is wrong. If I try to trick you with a false output, then your computer rejects it immediately. Consequently, if your computer does accept the proof, then you should be completely convinced that the output is correct.
  • Succinctness. The proof should be much smaller than the full size of the input data would have been. In this way, I can save in how much data I have to transmit to you. It should also be much more efficient to check it than to run the full-blown program.

What is a ZK-SNARK?

Some SNARKs provide an additional guarantee, called zero-knowledge. This means that while you know the computation output that I claim, and some of the inputs, the prover can compute with additional private information, and the proof file doesn't leak any new information about it. In our example of a financial query, the prover could claim that they know a trading strategy that would have outperformed the market. They could provide a proof of the returns their strategy obtained, without giving away any other secrets.

What Makes Binius Different?

Binius is far from the only SNARK construction, but most others struggle to efficiently prove bitwise operations. Bitwise operations are a key bottleneck in proving classical hash functions, which is an especially important use case for SNARKs. Binius is able to prove bitwise operations much more efficiently than competing approaches by combining two crucial design features: binary fields and the sumcheck protocol.

Binary fields have several important properties that we make good use of. Firstly, all binary fields, by definition, contain a 1-bit subfield known as GF(2), which is of course the smallest field. Second, binary field addition corresponds directly with bitwise XOR, which is a common operation. And binary fields are used widely in classic symmetric cryptography primitives, notably in the AES encryption cipher and GMAC algebraic message authentication code. For this reason, modern processors have dedicated instructions, like CLMUL on x86-64 and PMULL on ARM64, for accelerating binary field arithmetic for cryptographic applications.

The benefits of binary fields are amplified in combination with the sumcheck protocol, which dates back to [LFKN92]. Using the sumcheck protocol, we are able to encode individual bits very efficiently using techniques we developed in [DP24]. The sumcheck protocol furthermore unlocks efficient protocols for checking bitwise AND constraints and bitwise shifts.