Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding features to move the "glue" toward a corset implementation #409

Open
AlexandreBelling opened this issue Nov 29, 2024 · 1 comment
Labels
enhancement New feature or request

Comments

@AlexandreBelling
Copy link
Collaborator

This is an evolving list of the required features to move the glue implementation into go-corset. The target is to be able to write the whole zk-EVM system in that language.

Support for projection queries

A projection query between sets (columnsA,filterA) and (columnsB,filterB) asserts whether the columnsA filtered by filterA is the same as columnsB filtered by filterB, preserving the order. The constraint (improperly named query) can be enforced by the prover using a custom probabilistic wizard sub-protocol. The role of corset would be to only pass it down the compilation layers and provide it to the prover, similar to what is done for lookups.

Example

FilterA = (1,0,0,1,1), ColumnA := (aO,a1,a2,a3,a4)
FilterB := (0,0,1,0,0,0,0,0,1,1), ColumnB :=(b0,b1,b2,b3,b4,b5,b6,b7,b8,b9)

Here,

* ColumnA being filtered by FilterA = (a0,a3,a4)
* ColumnB being filtered by FilterB  = (b2,b8,b9)

The projection query checks if a0 = b2, a3 = b8, a4 = b9

Note that the query imposes that:

  • the number of 1 in the filters are equal
  • the order of filtered elements is preserved

Generating a column via a projection query

As "projection query" denotes a constraint between two couples of columns (CA, FA) (CB, FB). In practice, we will want to use to generate columns as follows:

  • FilterAndStack(CA, FA) -> (CB, FB)

From a pair of columns, generates a column CB containing all the values of CA at rows matching FA=1, stacked in the same order. Depending on the context, we will want to stack them either at the bottom or at the top of CB. FB is generated by stacking the relevant number of 1s either at the top of at the end of the column.

  • ImportFromCol(CA, FA, FB) -> CB

Generate CB so that it satisfies the constraints and so that FB=0 => CB=0 (for the unfiltered values). Similar to filter and stack but allows the caller to control the positions of the "projected" values.

AdHoc queries for the precompiles

Many predicates of the EVM involve operations that we do not write in corset at the moment. For instance,

isEcRecover(address, signature, msgHash)

These are handled by Plonk circuits and we should expect no action from corset aside passing down the constraint. The Plonk circuits take as input a pair of columns (Data, Filter) and works over that.

Columns generated by an expression involving several columns

I am sure this overlaps with other existing issues here, so I'll just phrase what we expect. The idea is that we would like to declare and assign columns as corset expressions. In this context, the rows of the generated column or columns can be generated in parallel: meaning the expression is of the form A, B = f(C, D) and A cannot be the operands of B.

It would cover the following "basic" features

  • Arithmetic expressions
  • Limbs/BIts/Bytes decompositions/recomposition

But also more custom things

  • MiMC compression function (to be replaced by Poseidon2 when we switch to smaller fields)
  • Keccakf compression functions
  • Other precompiles functions: (ECPair, ECMul, ECAdd, Keccakf, Secp, ...)

Columns generated by an expression involving itself

The difference with the above point is that here, the generation is sequential and can be of the form a[i+1] = f(a[i], b[i+1]). In term of constraint generation, this should not make a big difference with the non-sequential part but this drastically changes the evaluation.

@AlexandreBelling AlexandreBelling added the enhancement New feature or request label Nov 29, 2024
@DavePearce
Copy link
Collaborator

DavePearce commented Dec 2, 2024

Projection

Notes on projection. Let 'A' be a data column, F a binary "filter" column and A' the projection of A with respect to F. There are two aspects of projection:

  • (Projection Constraint). This is a primitive constraint form which checks that A' is indeed a true projection (see below for more on this).
  • (Projection Computation). This is an assignment which computes a projection from a given data column and filter. There are different ways this can be done, but we can assume e.g. all selected elements are placed (stacked) first, etc.

Projection Constraint

(Def. Projection) Let A be a data column and F a binary "filter" column of the same height n. Suppose F has exactly m rows holding the value 1. Then, A(F) is the projection of A according to F. Specifically, it contains only those values A[i] where F[i]==1 in the order of occurrence. Thus, the A(F) has size m. Furthermore, there is exactly one possible instance of A(F).

For example, suppose A=[1,2,3,4] and F=[1,0,1,0] then A(F)=[1,3]. Observe that the ordering is important, and hence, A(F)=[3,1] cannot hold.

(Def. Projection Constraint). Let A1 .. Ax be x data columns and P a binary "filter" column, all of which have the same height n. Let B1 .. Bx be data columns and Q a binary "filter" column, again all of which have the same height m. Then, the projection constraint (A1..Ax,P) ~ (B1..Bx,Q) checks that A1(P) == B1(Q) .. Ax(P) == Bx(Q) all hold.

Projection

The suggested corset syntax for a projection is:

(defprojection (Q B1 .. Bn ) (P A1 .. An))

where A1 .. An and P are the "source columns" and B1 .. Bn and Q are the "target columns". Like for a defpermutation this will generate a projection constraint (as above) and also an assignment which will compute values for the target columns. Specifically, it will default to packing the projection at the start of the target columns and then padding out the remainder with 0 so the resulting columns have the same height.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants