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

Distinguish Inputs, Assignments and Constraints #182

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 13 additions & 13 deletions pkg/air/eval.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
}

Expand Down
4 changes: 2 additions & 2 deletions pkg/air/expr.go
Original file line number Diff line number Diff line change
Expand Up @@ -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"
)

Expand All @@ -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
Expand Down
38 changes: 9 additions & 29 deletions pkg/air/gadgets/bits.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 {
Expand All @@ -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
}
16 changes: 7 additions & 9 deletions pkg/air/gadgets/column_sort.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 {
Expand All @@ -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]
Expand Down
Loading