Skip to content

A Lookup Construction

A full construction of the popular primitive

Lookups are important in modern proofs systems. They allow a prover to prove that a particular column's values are all contained within a table of values already known to the verifier. A simple way to capture this in our constraint system is to prove that all values in one column appear somewhere in a transparent table column. In this section we will construct a constraint system for this purpose, along with a prover and verifier to utilize the constraint system for a complete working proof system.

Throughout three pages we will build a lookup gadget. It will take inputs an oracle table and an oracle lookup_value, and ensure that all values in the lookup_values column appear in the table column.

Subsection Directory

This section contains the following subsections:

  • Gadget Design. Here, we present our main gadget design, which uses the concepts of "multiplicities" and "components". Channel-balancing is also central to the discussion.
  • Creating Components. Here, we explain how to create a get_components gadget, which plays a critical role in our lookup gadget.
  • Example Application. Here, we design prover and verifier functions invoking the lookup gadget for u8 by u8 multiplications.

We recommend that you follow the full code example as you proceed through these pages to help keep track of where each code snippet fits in the with the rest.

Relation to Lasso

In relation to Lasso or read-only-memory (ROM) based lookups, the lookup construction presented here has both similarities and differences. Both constructions can be built using M3 arithmetization, which is built on the idea of pushing and pulling things to and from a channel, and ensuring that the channel is ultimately empty (or balanced). While the concept at the heart of Lasso (and ROM more generally) is timestamps, the concept at the heart of the construction presented here is multiplicities. Rather than keeping track of a timestamp for each value in the lookup table, the prover keeps track of the multiplicity of each value in the lookup table, that is the number of times that value is looked up.

There is a difference in cost as well. If we think of the ratio of the number of values looked up to the number of values in the table, Lasso is a better choice when this ratio is small, while the constructed presented here is more cost-effective when the ratio is large.