Merge pull request #182 from Consensys/178-distinguishing-between-inp…

…uts-assignments-and-constraints

Distinguish Inputs, Assignments and Constraints

pkg/air/eval.go

@@ -2,14 +2,14 @@ package air
 
 import (
 	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
-	"github.com/consensys/go-corset/pkg/table"
+	"github.com/consensys/go-corset/pkg/trace"
 )
 
 // EvalAt evaluates a column access at a given row in a trace, which returns the
 // value at that row of the column in question or nil is that row is
 // out-of-bounds.
-func (e *ColumnAccess) EvalAt(k int, tbl table.Trace) *fr.Element {
-	val := tbl.ColumnByIndex(e.Column).Get(k + e.Shift)
+func (e *ColumnAccess) EvalAt(k int, tr trace.Trace) *fr.Element {
+	val := tr.ColumnByIndex(e.Column).Get(k + e.Shift)
 
 	var clone fr.Element
 	// Clone original value
@@ -18,45 +18,45 @@ func (e *ColumnAccess) EvalAt(k int, tbl table.Trace) *fr.Element {
 
 // EvalAt evaluates a constant at a given row in a trace, which simply returns
 // that constant.
-func (e *Constant) EvalAt(k int, tbl table.Trace) *fr.Element {
+func (e *Constant) EvalAt(k int, tr trace.Trace) *fr.Element {
 	var clone fr.Element
 	// Clone original value
 	return clone.Set(e.Value)
 }
 
 // EvalAt evaluates a sum at a given row in a trace by first evaluating all of
 // its arguments at that row.
-func (e *Add) EvalAt(k int, tbl table.Trace) *fr.Element {
+func (e *Add) EvalAt(k int, tr trace.Trace) *fr.Element {
 	fn := func(l *fr.Element, r *fr.Element) { l.Add(l, r) }
-	return evalExprsAt(k, tbl, e.Args, fn)
+	return evalExprsAt(k, tr, e.Args, fn)
 }
 
 // EvalAt evaluates a product at a given row in a trace by first evaluating all of
 // its arguments at that row.
-func (e *Mul) EvalAt(k int, tbl table.Trace) *fr.Element {
+func (e *Mul) EvalAt(k int, tr trace.Trace) *fr.Element {
 	fn := func(l *fr.Element, r *fr.Element) { l.Mul(l, r) }
-	return evalExprsAt(k, tbl, e.Args, fn)
+	return evalExprsAt(k, tr, e.Args, fn)
 }
 
 // EvalAt evaluates a subtraction at a given row in a trace by first evaluating all of
 // its arguments at that row.
-func (e *Sub) EvalAt(k int, tbl table.Trace) *fr.Element {
+func (e *Sub) EvalAt(k int, tr trace.Trace) *fr.Element {
 	fn := func(l *fr.Element, r *fr.Element) { l.Sub(l, r) }
-	return evalExprsAt(k, tbl, e.Args, fn)
+	return evalExprsAt(k, tr, e.Args, fn)
 }
 
 // EvalExprsAt evaluates all expressions in a given slice at a given row on the
 // table, and fold their results together using a combinator.
-func evalExprsAt(k int, tbl table.Trace, exprs []Expr, fn func(*fr.Element, *fr.Element)) *fr.Element {
+func evalExprsAt(k int, tr trace.Trace, exprs []Expr, fn func(*fr.Element, *fr.Element)) *fr.Element {
 	// Evaluate first argument
-	val := exprs[0].EvalAt(k, tbl)
+	val := exprs[0].EvalAt(k, tr)
 	if val == nil {
 		return nil
 	}
 
 	// Continue evaluating the rest
 	for i := 1; i < len(exprs); i++ {
-		ith := exprs[i].EvalAt(k, tbl)
+		ith := exprs[i].EvalAt(k, tr)
 		fn(val, ith)
 	}
 

pkg/air/expr.go

@@ -2,7 +2,7 @@ package air
 
 import (
 	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
-	"github.com/consensys/go-corset/pkg/table"
+	"github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 )
 
@@ -19,7 +19,7 @@ type Expr interface {
 	// "nil".  An expression can be undefined for several reasons: firstly, if
 	// it accesses a row which does not exist (e.g. at index -1); secondly, if
 	// it accesses a column which does not exist.
-	EvalAt(int, table.Trace) *fr.Element
+	EvalAt(int, trace.Trace) *fr.Element
 
 	// String produces a string representing this as an S-Expression.
 	String() string

pkg/air/gadgets/bits.go

@@ -5,15 +5,15 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
 	"github.com/consensys/go-corset/pkg/air"
-	"github.com/consensys/go-corset/pkg/table"
+	"github.com/consensys/go-corset/pkg/schema/assignment"
 )
 
 // ApplyBinaryGadget adds a binarity constraint for a given column in the schema
 // which enforces that all values in the given column are either 0 or 1. For a
 // column X, this corresponds to the vanishing constraint X * (X-1) == 0.
 func ApplyBinaryGadget(column uint, schema *air.Schema) {
 	// Determine column name
-	name := schema.Column(column).Name()
+	name := schema.Columns().Nth(column).Name()
 	// Construct X
 	X := air.NewColumnAccess(column, 0)
 	// Construct X-1
@@ -27,7 +27,7 @@ func ApplyBinaryGadget(column uint, schema *air.Schema) {
 // ApplyBitwidthGadget ensures all values in a given column fit within a given
 // number of bits.  This is implemented using a *byte decomposition* which adds
 // n columns and a vanishing constraint (where n*8 >= nbits).
-func ApplyBitwidthGadget(column uint, nbits uint, schema *air.Schema) {
+func ApplyBitwidthGadget(col uint, nbits uint, schema *air.Schema) {
 	if nbits%8 != 0 {
 		panic("asymmetric bitwidth constraints not yet supported")
 	} else if nbits == 0 {
@@ -37,44 +37,24 @@ func ApplyBitwidthGadget(column uint, nbits uint, schema *air.Schema) {
 	n := nbits / 8
 	es := make([]air.Expr, n)
 	fr256 := fr.NewElement(256)
-	name := schema.Column(column).Name()
+	name := schema.Columns().Nth(col).Name()
 	coefficient := fr.NewElement(1)
+	// Add decomposition assignment
+	index := schema.AddAssignment(assignment.NewByteDecomposition(name, n))
 	// Construct Columns
 	for i := uint(0); i < n; i++ {
-		// Determine name for the ith byte column
-		colName := fmt.Sprintf("%s:%d", name, i)
 		// Create Column + Constraint
-		colIndex := schema.AddColumn(colName, true)
-		es[i] = air.NewColumnAccess(colIndex, 0).Mul(air.NewConstCopy(&coefficient))
+		es[i] = air.NewColumnAccess(index+i, 0).Mul(air.NewConstCopy(&coefficient))
 
-		schema.AddRangeConstraint(colIndex, &fr256)
+		schema.AddRangeConstraint(index+i, &fr256)
 		// Update coefficient
 		coefficient.Mul(&coefficient, &fr256)
 	}
 	// Construct (X:0 * 1) + ... + (X:n * 2^n)
 	sum := &air.Add{Args: es}
 	// Construct X == (X:0 * 1) + ... + (X:n * 2^n)
-	X := air.NewColumnAccess(column, 0)
+	X := air.NewColumnAccess(col, 0)
 	eq := X.Equate(sum)
 	// Construct column name
 	schema.AddVanishingConstraint(fmt.Sprintf("%s:u%d", name, nbits), nil, eq)
-	// Finally, add the necessary byte decomposition computation.
-	schema.AddComputation(table.NewByteDecomposition(name, nbits))
-}
-
-// AddBitArray adds an array of n bit columns using a given prefix, including
-// the necessary binarity constraints.
-func AddBitArray(prefix string, count int, schema *air.Schema) []uint {
-	bits := make([]uint, count)
-
-	for i := 0; i < count; i++ {
-		// Construct bit column name
-		ith := fmt.Sprintf("%s:%d", prefix, i)
-		// Add (synthetic) column
-		bits[i] = schema.AddColumn(ith, true)
-		// Add binarity constraints (i.e. to enfoce that this column is a bit).
-		ApplyBinaryGadget(bits[i], schema)
-	}
-	//
-	return bits
 }

pkg/air/gadgets/column_sort.go

@@ -4,7 +4,7 @@ import (
 	"fmt"
 
 	"github.com/consensys/go-corset/pkg/air"
-	"github.com/consensys/go-corset/pkg/table"
+	"github.com/consensys/go-corset/pkg/schema/assignment"
 )
 
 // ApplyColumnSortGadget adds sorting constraints for a column where the
@@ -18,13 +18,13 @@ import (
 // This gadget does not attempt to sort the column data during trace expansion,
 // and assumes the data either comes sorted or is sorted by some other
 // computation.
-func ApplyColumnSortGadget(column uint, sign bool, bitwidth uint, schema *air.Schema) {
+func ApplyColumnSortGadget(col uint, sign bool, bitwidth uint, schema *air.Schema) {
 	var deltaName string
 	// Determine column name
-	name := schema.Column(column).Name()
+	name := schema.Columns().Nth(col).Name()
 	// Configure computation
-	Xk := air.NewColumnAccess(column, 0)
-	Xkm1 := air.NewColumnAccess(column, -1)
+	Xk := air.NewColumnAccess(col, 0)
+	Xkm1 := air.NewColumnAccess(col, -1)
 	// Account for sign
 	var Xdiff air.Expr
 	if sign {
@@ -34,10 +34,8 @@ func ApplyColumnSortGadget(column uint, sign bool, bitwidth uint, schema *air.Sc
 		Xdiff = Xkm1.Sub(Xk)
 		deltaName = fmt.Sprintf("-%s", name)
 	}
-	// Add delta column
-	deltaIndex := schema.AddColumn(deltaName, true)
-	// Add diff computation
-	schema.AddComputation(table.NewComputedColumn(deltaName, Xdiff))
+	// Add delta assignment
+	deltaIndex := schema.AddAssignment(assignment.NewComputedColumn(deltaName, Xdiff))
 	// Add necessary bitwidth constraints
 	ApplyBitwidthGadget(deltaIndex, bitwidth, schema)
 	// Configure constraint: Delta[k] = X[k] - X[k-1]