Support Interleaving Constraints

[DavePearce]

Example:

(defcolumns X Y)
(definterleaved (Z) (X Y))

Generates the following Go output:

func ZkEVMDefine(build *Builder) {
        //
        // Corset-computed columns
        //
        _prelude___X := build.RegisterCommit("X", build.Settings.Traces.Prelude)
        _prelude___Y := build.RegisterCommit("Y", build.Settings.Traces.Prelude)


        //
        // Interleaved columns
        //
        _prelude___Z := Interleave(_prelude___X, _prelude___Y)


        //
        // Constraints
        //
}

So, we can see that interleaved is a fundamental constraint.

[DavePearce]

A more involved example:

(defcolumns X Y)
(definterleaved (Z) (X Y))
(defconstraint c1 () (vanishes! (* X Y)))
(defconstraint c2 () (vanishes! (- 1 (~ X))))

With the following trace:

{ "<prelude>": { "X": [1], "Y": [2] } }

Using the following command:

corset compute -eeeeeN --auto-constraints nhood,sorts --trace trace.in --out trace.out interleave.lisp

Gives the following trace.out file:

{"columns":{
"Y":{
"values":["0x00","0x02"],
"padding_strategy": {"action": "prepend", "value": "0"}
}
,"X":{
"values":["0x00","0x01"],
"padding_strategy": {"action": "prepend", "value": "0"}
}
,"Z":{
"values":["0x00","0x00","0x01","0x02"],
"padding_strategy": {"action": "prepend", "value": "0"}
}
,"C/INV[X]":{
"values":["0x00","0x01"],
"padding_strategy": {"action": "prepend", "value": "0"}
}
}}

An interesting question is what exactly the padding strategy is. Is this passed to the prover?