Lasso presentation notes

Notes on the Lasso presentation and further conversations

Overall idea using an OR operation as an example:

Represent the operands as bit-vectors

Split them into eight 4-bit chunks

Join each column into an 8-bit lookup table

Lasso springs from Spartan. Spartan uses Spark. The Polynomial Commitment Scheme of Lasso is Surge

Multilinear extensions

To make use of the Sum Check protocol, we transform each function into a multilinear extension. The domain becomes the boolean hypercube, that is, sequential integer indexes are represented as bit vectors

The boolean cube is the domain for the multilinear extension of this example

As mentioned, EQ~ is defined for a bigger domain than EQ that we need for the Sum Check protocol

Jolt

While their Lasso implementation is ready to use, their Jolt implementation is under development in this branch github.com/a16z/lasso/tree/moodlezoup/jolt

Understanding Surge (the Polynomial Commitment Scheme) is needed to build a Jolt VM, but apparently only that first paragraph in the Lasso paper

Jolt API

materialise is the evaluation over the boolean hypercube. evaluate_mle is the evaluation over the extension function ~

Example of an instruction VM: 8-bit EQ instruction Implementation

Convert to bit vectors and compare each bit. If all bits are equal, then 1 else 0

A useful mental model is a lookup table. On 64 bit operands, this table becomes size 2^128. This is too big, so we need to do something else

The solution is to split the input vectors into a series of 2-bit instructions. Bitwise operations are independent.

C is the subtable dimensionality (4 in this case). This creates a set of much smaller tables

Splitting a lookup table into smaller lookup tables is efficient because the reduction is logarithmic. E.g. The cost of looking up a matrix of size (2^128) becomes the cost of looking up 2^{128/C} * (cost of constructing a structured submatrix) where C is a parameter we can choose.

• k is the number of subtable types you need to define the big table instruction
• g is how you combine subtables into a big table evaluation. In this case, it is just the product
• M is the size of the small subtables
• C is the number of subtables

Implementation of the 8-bit EQ instruction

Other considerations

• Arithmetisation is not relevant here. It's only lookups that Lasso deals with. I believe Lasso uses Hyrax as a proving system right now but that is not important for us
• Many VMs can share instructions. This is great for auditing