Merge pull request #217 from Consensys/212-test-for-lookup-involving-…

…constant-expression

Support Lookups with Constant Expressions

pkg/air/gadgets/expand.go

@@ -6,21 +6,20 @@ import (
 	"github.com/consensys/go-corset/pkg/air"
 	sc "github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/assignment"
+	"github.com/consensys/go-corset/pkg/trace"
 )
 
 // Expand converts an arbitrary expression into a specific column index.  In
 // general, this means adding a computed column to hold the value of the
 // arbitrary expression and returning its index.  However, this can be optimised
 // in the case the given expression is a direct column access by simply
 // returning the accessed column index.
-func Expand(e air.Expr, schema *air.Schema) uint {
+func Expand(ctx trace.Context, e air.Expr, schema *air.Schema) uint {
 	//
 	if ca, ok := e.(*air.ColumnAccess); ok && ca.Shift == 0 {
 		// Optimisation possible
 		return ca.Column
 	}
-	// No optimisation, therefore expand using a computedcolumn
-	ctx := e.Context(schema)
 	// Determine computed column name
 	name := e.String()
 	// Look up column

pkg/mir/lower.go

@@ -7,6 +7,7 @@ import (
 	air_gadgets "github.com/consensys/go-corset/pkg/air/gadgets"
 	sc "github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/trace"
 )
 
 // LowerToAir lowers (or refines) an MIR table into an AIR schema.  That means
@@ -61,7 +62,7 @@ func lowerConstraintToAir(c sc.Constraint, schema *air.Schema) {
 	if v, ok := c.(LookupConstraint); ok {
 		lowerLookupConstraintToAir(v, schema)
 	} else if v, ok := c.(VanishingConstraint); ok {
-		air_expr := lowerExprTo(v.Constraint().Expr, schema)
+		air_expr := lowerExprTo(v.Context(), v.Constraint().Expr, schema)
 		schema.AddVanishingConstraint(v.Handle(), v.Context(), v.Domain(), air_expr)
 	} else if v, ok := c.(*constraint.TypeConstraint); ok {
 		if t := v.Type().AsUint(); t != nil {
@@ -97,11 +98,11 @@ func lowerLookupConstraintToAir(c LookupConstraint, schema *air.Schema) {
 	//
 	for i := 0; i < len(targets); i++ {
 		// Lower source and target expressions
-		target := lowerExprTo(c.Targets()[i], schema)
-		source := lowerExprTo(c.Sources()[i], schema)
+		target := lowerExprTo(c.TargetContext(), c.Targets()[i], schema)
+		source := lowerExprTo(c.SourceContext(), c.Sources()[i], schema)
 		// Expand them
-		targets[i] = air_gadgets.Expand(target, schema)
-		sources[i] = air_gadgets.Expand(source, schema)
+		targets[i] = air_gadgets.Expand(c.TargetContext(), target, schema)
+		sources[i] = air_gadgets.Expand(c.SourceContext(), source, schema)
 	}
 	// finally add the constraint
 	schema.AddLookupConstraint(c.Handle(), c.SourceContext(), c.TargetContext(), sources, targets)
@@ -161,34 +162,36 @@ func lowerPermutationToAir(c Permutation, mirSchema *Schema, airSchema *air.Sche
 // Essentially, this means eliminating normalising expressions by introducing
 // new columns into the given table (with appropriate constraints).  This first
 // performs constant propagation to ensure lowering is as efficient as possible.
-func lowerExprTo(e1 Expr, schema *air.Schema) air.Expr {
+// A module identifier is required to determine where any computed columns
+// should be located.
+func lowerExprTo(ctx trace.Context, e1 Expr, schema *air.Schema) air.Expr {
 	// Apply constant propagation
 	e2 := applyConstantPropagation(e1)
 	// Lower properly
-	return lowerExprToInner(e2, schema)
+	return lowerExprToInner(ctx, e2, schema)
 }
 
 // Inner form is used for recursive calls and does not repeat the constant
 // propagation phase.
-func lowerExprToInner(e Expr, schema *air.Schema) air.Expr {
+func lowerExprToInner(ctx trace.Context, e Expr, schema *air.Schema) air.Expr {
 	if p, ok := e.(*Add); ok {
-		return &air.Add{Args: lowerExprs(p.Args, schema)}
+		return &air.Add{Args: lowerExprs(ctx, p.Args, schema)}
 	} else if p, ok := e.(*Constant); ok {
 		return &air.Constant{Value: p.Value}
 	} else if p, ok := e.(*ColumnAccess); ok {
 		return &air.ColumnAccess{Column: p.Column, Shift: p.Shift}
 	} else if p, ok := e.(*Mul); ok {
-		return &air.Mul{Args: lowerExprs(p.Args, schema)}
+		return &air.Mul{Args: lowerExprs(ctx, p.Args, schema)}
 	} else if p, ok := e.(*Exp); ok {
-		return lowerExpTo(p, schema)
+		return lowerExpTo(ctx, p, schema)
 	} else if p, ok := e.(*Normalise); ok {
 		// Lower the expression being normalised
-		e := lowerExprToInner(p.Arg, schema)
+		e := lowerExprToInner(ctx, p.Arg, schema)
 		// Construct an expression representing the normalised value of e.  That is,
 		// an expression which is 0 when e is 0, and 1 when e is non-zero.
 		return air_gadgets.Normalise(e, schema)
 	} else if p, ok := e.(*Sub); ok {
-		return &air.Sub{Args: lowerExprs(p.Args, schema)}
+		return &air.Sub{Args: lowerExprs(ctx, p.Args, schema)}
 	}
 	// Should be unreachable
 	panic(fmt.Sprintf("unknown expression: %s", e.String()))
@@ -197,9 +200,9 @@ func lowerExprToInner(e Expr, schema *air.Schema) air.Expr {
 // LowerTo lowers an exponent expression to the AIR level by lowering the
 // argument, and then constructing a multiplication.  This is because the AIR
 // level does not support an explicit exponent operator.
-func lowerExpTo(e *Exp, schema *air.Schema) air.Expr {
+func lowerExpTo(ctx trace.Context, e *Exp, schema *air.Schema) air.Expr {
 	// Lower the expression being raised
-	le := lowerExprToInner(e.Arg, schema)
+	le := lowerExprToInner(ctx, e.Arg, schema)
 	// Multiply it out k times
 	es := make([]air.Expr, e.Pow)
 	//
@@ -211,12 +214,12 @@ func lowerExpTo(e *Exp, schema *air.Schema) air.Expr {
 }
 
 // Lower a set of zero or more MIR expressions.
-func lowerExprs(exprs []Expr, schema *air.Schema) []air.Expr {
+func lowerExprs(ctx trace.Context, exprs []Expr, schema *air.Schema) []air.Expr {
 	n := len(exprs)
 	nexprs := make([]air.Expr, n)
 
 	for i := 0; i < n; i++ {
-		nexprs[i] = lowerExprToInner(exprs[i], schema)
+		nexprs[i] = lowerExprToInner(ctx, exprs[i], schema)
 	}
 
 	return nexprs

pkg/test/ir_test.go

@@ -374,6 +374,14 @@ func Test_Lookup_06(t *testing.T) {
 	Check(t, "lookup_06")
 }
 
+func Test_Lookup_07(t *testing.T) {
+	Check(t, "lookup_07")
+}
+
+func Test_Lookup_08(t *testing.T) {
+	Check(t, "lookup_08")
+}
+
 // ===================================================================
 // Interleaving
 // ===================================================================

testdata/lookup_07.accepts

@@ -0,0 +1,11 @@
+{ "A": [], "B": [], "X": [] }
+{ "A": [1], "B": [0], "X": [1] }
+{ "A": [1,2,3], "B": [0,1,2], "X": [1,0,0] }
+{ "A": [1,2,3], "B": [0,1,2], "X": [1,1,0] }
+{ "A": [1,2,3], "B": [0,1,2], "X": [0,1,1] }
+{ "A": [1,2,3], "B": [0,1,2], "X": [0,0,1] }
+
+{ "A": [1,2,3], "B": [1,0,2], "X": [2,0,0] }
+{ "A": [1,2,3], "B": [1,0,2], "X": [2,2,0] }
+{ "A": [1,2,3], "B": [1,0,2], "X": [0,2,2] }
+{ "A": [1,2,3], "B": [1,0,2], "X": [0,0,2] }

testdata/lookup_07.lisp

@@ -0,0 +1,4 @@
+(column A)
+(column B)
+(column X)
+(lookup test (A B) (X 0))

testdata/lookup_07.rejects

@@ -0,0 +1,10 @@
+{ "A": [0], "B": [0], "X": [1] }
+{ "A": [1], "B": [1], "X": [1] }
+{ "A": [0,1], "B": [0,1], "X": [0,1] }
+{ "A": [1,0], "B": [1,0], "X": [0,1] }
+{ "A": [0,1], "B": [0,1], "X": [0,1] }
+{ "A": [1,1], "B": [1,1], "X": [0,1] }
+{ "A": [0,1], "B": [0,1], "X": [1,0] }
+{ "A": [1,0], "B": [1,0], "X": [1,0] }
+{ "A": [0,1], "B": [0,1], "X": [1,0] }
+{ "A": [1,1], "B": [1,1], "X": [1,0] }

testdata/lookup_08.accepts

@@ -0,0 +1,11 @@
+{ "B": [], "A": [], "X": [] }
+{ "B": [1], "A": [0], "X": [1] }
+{ "B": [1,2,3], "A": [0,1,2], "X": [1,0,0] }
+{ "B": [1,2,3], "A": [0,1,2], "X": [1,1,0] }
+{ "B": [1,2,3], "A": [0,1,2], "X": [0,1,1] }
+{ "B": [1,2,3], "A": [0,1,2], "X": [0,0,1] }
+
+{ "B": [1,2,3], "A": [1,0,2], "X": [2,0,0] }
+{ "B": [1,2,3], "A": [1,0,2], "X": [2,2,0] }
+{ "B": [1,2,3], "A": [1,0,2], "X": [0,2,2] }
+{ "B": [1,2,3], "A": [1,0,2], "X": [0,0,2] }

testdata/lookup_08.lisp

@@ -0,0 +1,4 @@
+(column A)
+(column B)
+(column X)
+(lookup test (A B) (0 X))

testdata/lookup_08.rejects

@@ -0,0 +1,10 @@
+{ "B": [0], "A": [0], "X": [1] }
+{ "B": [1], "A": [1], "X": [1] }
+{ "B": [0,1], "A": [0,1], "X": [0,1] }
+{ "B": [1,0], "A": [1,0], "X": [0,1] }
+{ "B": [0,1], "A": [0,1], "X": [0,1] }
+{ "B": [1,1], "A": [1,1], "X": [0,1] }
+{ "B": [0,1], "A": [0,1], "X": [1,0] }
+{ "B": [1,0], "A": [1,0], "X": [1,0] }
+{ "B": [0,1], "A": [0,1], "X": [1,0] }
+{ "B": [1,1], "A": [1,1], "X": [1,0] }