Invalid define.go for complex Guard

[DavePearce]

Minimal example:

(module test)
(defcolumns X (BYTE :array[0:1]))
(defconstraint test
    (:guard (reduce + (for k [1:1] [BYTE k])))
  (vanishes! X))

This produces the following define.go:

package define

import (
	_ "embed"

	"github.com/consensys/zkevm-monorepo/prover/symbolic"
)

func ZkEVMDefine(build *Builder) {
	//
	// Corset-computed columns
	//
	test__BYTE_0 := build.RegisterCommit("test.BYTE_0", build.Settings.Traces.Test)
	test__BYTE_1 := build.RegisterCommit("test.BYTE_1", build.Settings.Traces.Test)
	test__X := build.RegisterCommit("test.X", build.Settings.Traces.Test)

        ...

	build.GlobalConstraint("test.test", test__BYTE_1.AsVariable(),.Mul(test__X.AsVariable()))
}

Note the last line contains a syntax error: ... AsVariable(),.Mul( ...

[DavePearce]

So, the issue is with this section of code:

fn render_expression(cs: &ConstraintSet, e: &Node) -> String {
    match e.e() {
       ...
        Expression::List(constraints) => constraints
            .iter()
            .map(|e| render_expression(cs, e))
            .map(|mut x| {
                if let Some(true) = x.chars().last().map(|c| c != ',') {
                    x.push(',');
                }
                x
            })
            .collect::<Vec<_>>()
            .join("\n"),

In essence, we have a List with a single item which is causing the problem.

Q) Does it even make sense to be rendering a List at this stage? I don't see how the above code would even work in the case of a list with more than one element?

UPDATE: Seems that this is only arising in the case of :guard?

[DavePearce]

Ok, we can fix the above by a slight modification in generator::apply_form which handles the case for unit lists differently from others. However, this actually doesn't address the problem which gave rose to this issue. Minimal case for that is actually:

(module test)
(defcolumns X (BYTE :array[0:2]))
(defconstraint test
  (:guard (+ (for k [0:2] [BYTE k])))
    (vanishes! X))

Does this seem syntactically malformed? Its curious that corset doesn't report any problem with it.

UPDATE: in the body of a constraint, this has an effect (though not the desired one). For example, this:

(module test)
(defcolumns X (BYTE :array[0:2]))
(defconstraint test
  ()
  (vanishes! (+ (for k [0:2] [BYTE k]))))

Generates three vanishing constraints:

	build.GlobalConstraint("test.test#0", test__BYTE_0.AsVariable())
	build.GlobalConstraint("test.test#1", test__BYTE_1.AsVariable())
	build.GlobalConstraint("test.test#2", test__BYTE_2.AsVariable())

But, I suppose the problem is that, in the context of a guard I suppose this doesn't even make sense.

[delehef]

(+ (for k [0:2] [BYTE k]))

This should fail at the verification of the arguments to +, that accepts multiple arguments, but not an argument that is a list.

In this case, the appropriate guard expression would be (reduce + (for k [0:2] [BYTE k]))

[DavePearce]

This should fail at the verification of the arguments to +, that accepts multiple arguments, but not an argument that is a list.

Yeah, that makes sense. I will look into doing that tomorrow :)

[DavePearce]

Ok, merged in fix for the minimal example at top of this issue (which uses a reduce). Have opened #191 for case when reduce omitted.