Skip to content

Commit

Permalink
Refactor Schema
Browse files Browse the repository at this point in the history 
This puts through an extensive refactoring of a `Schema`.  Specifically,
a schema is made up of three components: _input columns_, _assignments_
and _constraints_.  To facilitate this, an `iterator` framework has been
developed to simplify the grouping of things together.
  • Loading branch information
@DavePearce
DavePearce committed Jun 24, 2024
1 parent 4d054d1 commit 8c0dd5d
Show file tree
Hide file tree
Showing 34 changed files with 2,055 additions and 1,661 deletions.
38 changes: 9 additions & 29 deletions pkg/air/gadgets/bits.go
View file
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"
sc "github.com/consensys/go-corset/pkg/schema"
"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(sc.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
View file
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"
sc "github.com/consensys/go-corset/pkg/schema"
"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(sc.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
161 changes: 42 additions & 119 deletions pkg/air/gadgets/lexicographic_sort.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,8 @@ import (
"fmt"
"strings"

"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
"github.com/consensys/go-corset/pkg/air"
"github.com/consensys/go-corset/pkg/trace"
"github.com/consensys/go-corset/pkg/schema/assignment"
)

// ApplyLexicographicSortingGadget Add sorting constraints for a sequence of one
Expand Down Expand Up @@ -35,15 +34,13 @@ func ApplyLexicographicSortingGadget(columns []uint, signs []bool, bitwidth uint
// Construct a unique prefix for this sort.
prefix := constructLexicographicSortingPrefix(columns, signs, schema)
// Add trace computation
schema.AddComputation(&lexicographicSortExpander{prefix, columns, signs, bitwidth})
deltaName := fmt.Sprintf("%s:delta", prefix)
deltaIndex := schema.AddAssignment(assignment.NewLexicographicSort(prefix, columns, signs, bitwidth))
// Construct selecto bits.
bits := addLexicographicSelectorBits(prefix, columns, schema)
// Add delta column
deltaIndex := schema.AddColumn(deltaName, true)
addLexicographicSelectorBits(prefix, deltaIndex, columns, schema)
// Construct delta terms
constraint := constructLexicographicDeltaConstraint(deltaIndex, bits, columns, signs)
constraint := constructLexicographicDeltaConstraint(deltaIndex, columns, signs)
// Add delta constraint
deltaName := fmt.Sprintf("%s:delta", prefix)
schema.AddVanishingConstraint(deltaName, nil, constraint)
// Add necessary bitwidth constraints
ApplyBitwidthGadget(deltaIndex, bitwidth, schema)
Expand All @@ -56,7 +53,7 @@ func constructLexicographicSortingPrefix(columns []uint, signs []bool, schema *a
var id strings.Builder
// Concatenate column names with their signs.
for i := 0; i < len(columns); i++ {
ith := schema.Column(columns[i])
ith := schema.Columns().Nth(columns[i])
id.WriteString(ith.Name())

if signs[i] {
Expand All @@ -76,31 +73,36 @@ func constructLexicographicSortingPrefix(columns []uint, signs []bool, schema *a
//
// NOTE: this implementation differs from the original corset which used an
// additional "Eq" bit to help ensure at most one selector bit was enabled.
func addLexicographicSelectorBits(prefix string, columns []uint, schema *air.Schema) []uint {
ncols := len(columns)
// Add bits and their binary constraints.
bits := AddBitArray(prefix, ncols, schema)
func addLexicographicSelectorBits(prefix string, deltaIndex uint, columns []uint, schema *air.Schema) {
ncols := uint(len(columns))
// Calculate column index of first selector bit
bitIndex := deltaIndex + 1
// Add binary constraints for selector bits
for i := uint(0); i < ncols; i++ {
// Add binarity constraints (i.e. to enfoce that this column is a bit).
ApplyBinaryGadget(bitIndex+i, schema)
}
// Apply constraints to ensure at most one is set.
terms := make([]air.Expr, ncols)
for i := 0; i < ncols; i++ {
terms[i] = air.NewColumnAccess(bits[i], 0)
for i := uint(0); i < ncols; i++ {
terms[i] = air.NewColumnAccess(bitIndex+i, 0)
pterms := make([]air.Expr, i+1)
qterms := make([]air.Expr, i)

for j := 0; j < i; j++ {
pterms[j] = air.NewColumnAccess(bits[j], 0)
qterms[j] = air.NewColumnAccess(bits[j], 0)
for j := uint(0); j < i; j++ {
pterms[j] = air.NewColumnAccess(bitIndex+j, 0)
qterms[j] = air.NewColumnAccess(bitIndex+j, 0)
}
// (∀j<=i.Bj=0) ==> C[k]=C[k-1]
pterms[i] = air.NewColumnAccess(bits[i], 0)
pterms[i] = air.NewColumnAccess(bitIndex+i, 0)
pDiff := air.NewColumnAccess(columns[i], 0).Sub(air.NewColumnAccess(columns[i], -1))
pName := fmt.Sprintf("%s:%d:a", prefix, i)
schema.AddVanishingConstraint(pName, nil, air.NewConst64(1).Sub(&air.Add{Args: pterms}).Mul(pDiff))
// (∀j<i.Bj=0) ∧ Bi=1 ==> C[k]≠C[k-1]
qDiff := Normalise(air.NewColumnAccess(columns[i], 0).Sub(air.NewColumnAccess(columns[i], -1)), schema)
qName := fmt.Sprintf("%s:%d:b", prefix, i)
// bi = 0 || C[k]≠C[k-1]
constraint := air.NewColumnAccess(bits[i], 0).Mul(air.NewConst64(1).Sub(qDiff))
constraint := air.NewColumnAccess(bitIndex+i, 0).Mul(air.NewConst64(1).Sub(qDiff))

if i != 0 {
// (∃j<i.Bj≠0) || bi = 0 || C[k]≠C[k-1]
Expand All @@ -115,25 +117,25 @@ func addLexicographicSelectorBits(prefix string, columns []uint, schema *air.Sch
constraint := sum.Mul(sum.Equate(air.NewConst64(1)))
name := fmt.Sprintf("%s:xor", prefix)
schema.AddVanishingConstraint(name, nil, constraint)

return bits
}

// Construct the lexicographic delta constraint. This states that the delta
// column either holds 0 or the difference Ci[k] - Ci[k-1] (adjusted
// appropriately for the sign) between the ith column whose multiplexor bit is
// set. This is assumes that multiplexor bits are mutually exclusive (i.e. at
// most is one).
func constructLexicographicDeltaConstraint(delta uint, bits []uint, columns []uint, signs []bool) air.Expr {
ncols := len(columns)
func constructLexicographicDeltaConstraint(deltaIndex uint, columns []uint, signs []bool) air.Expr {
ncols := uint(len(columns))
// Calculate column index of first selector bit
bitIndex := deltaIndex + 1
// Construct delta terms
terms := make([]air.Expr, ncols)
Dk := air.NewColumnAccess(delta, 0)
Dk := air.NewColumnAccess(deltaIndex, 0)

for i := 0; i < ncols; i++ {
for i := uint(0); i < ncols; i++ {
var Xdiff air.Expr
// Ith bit column (at row k)
Bk := air.NewColumnAccess(bits[i], 0)
Bk := air.NewColumnAccess(bitIndex+i, 0)
// Ith column (at row k)
Xk := air.NewColumnAccess(columns[i], 0)
// Ith column (at row k-1)
Expand All @@ -150,98 +152,19 @@ func constructLexicographicDeltaConstraint(delta uint, bits []uint, columns []ui
return Dk.Equate(&air.Add{Args: terms})
}

type lexicographicSortExpander struct {
prefix string
columns []uint
signs []bool
bitwidth uint
}

// RequiredSpillage returns the minimum amount of spillage required to ensure
// valid traces are accepted in the presence of arbitrary padding.
func (p *lexicographicSortExpander) RequiredSpillage() uint {
return uint(0)
}

// Accepts checks whether a given trace has the necessary columns
func (p *lexicographicSortExpander) Accepts(tr trace.Trace) error {
//prefix := constructLexicographicSortingPrefix(p.columns, p.signs)
deltaName := fmt.Sprintf("%s:delta", p.prefix)
// Check delta column exists
if !tr.HasColumn(deltaName) {
return fmt.Errorf("Trace missing lexicographic delta column ({%s})", deltaName)
}
// Check selector columns exist
for i := range p.columns {
bitName := fmt.Sprintf("%s:%d", p.prefix, i)
if !tr.HasColumn(bitName) {
return fmt.Errorf("Trace missing lexicographic selector column ({%s})", bitName)
}
// 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 (computed) column
// bits[i] = schema.AddColumn(ith, sc.NewUintType(1))
// Add binarity constraints (i.e. to enfoce that this column is a bit).
ApplyBinaryGadget(bits[i], schema)
}
//
return nil
}

// Add columns as needed to support the LexicographicSortingGadget. That
// includes the delta column, and the bit selectors.
func (p *lexicographicSortExpander) ExpandTrace(tr trace.Trace) error {
zero := fr.NewElement(0)
one := fr.NewElement(1)
// Exact number of columns involved in the sort
ncols := len(p.columns)
// Determine how many rows to be constrained.
nrows := tr.Height()
// Construct a unique prefix for this sort.
deltaName := fmt.Sprintf("%s:delta", p.prefix)
// Initialise new data columns
delta := make([]*fr.Element, nrows)
bit := make([][]*fr.Element, ncols)

for i := 0; i < ncols; i++ {
bit[i] = make([]*fr.Element, nrows)
}

for i := 0; i < int(nrows); i++ {
set := false
// Initialise delta to zero
delta[i] = &zero
// Decide which row is the winner (if any)
for j := 0; j < ncols; j++ {
prev := tr.ColumnByIndex(p.columns[j]).Get(i - 1)
curr := tr.ColumnByIndex(p.columns[j]).Get(i)

if !set && prev != nil && prev.Cmp(curr) != 0 {
var diff fr.Element

bit[j][i] = &one
// Compute curr - prev
if p.signs[j] {
diff.Set(curr)
delta[i] = diff.Sub(&diff, prev)
} else {
diff.Set(prev)
delta[i] = diff.Sub(&diff, curr)
}

set = true
} else {
bit[j][i] = &zero
}
}
}
// Add delta column data
tr.AddColumn(deltaName, delta, &zero)
// Add bit column data
for i := 0; i < ncols; i++ {
bitName := fmt.Sprintf("%s:%d", p.prefix, i)
tr.AddColumn(bitName, bit[i], &zero)
}
// Done.
return nil
}

// String returns a string representation of this constraint. This is primarily
// used for debugging.
func (p *lexicographicSortExpander) String() string {
return fmt.Sprintf("(lexer (%v) (%v) :%d))", any(p.columns), p.signs, p.bitwidth)
return bits
}
10 changes: 5 additions & 5 deletions pkg/air/gadgets/normalisation.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,14 @@ import (
"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
"github.com/consensys/go-corset/pkg/air"
sc "github.com/consensys/go-corset/pkg/schema"
"github.com/consensys/go-corset/pkg/schema/assignment"
tr "github.com/consensys/go-corset/pkg/trace"
"github.com/consensys/go-corset/pkg/util"
)

// Normalise constructs 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.
// This is done by introducing a synthetic column to hold the (pseudo)
// This is done by introducing a computed column to hold the (pseudo)
// mutliplicative inverse of e.
func Normalise(e air.Expr, schema *air.Schema) air.Expr {
// Construct pseudo multiplicative inverse of e.
Expand All @@ -32,12 +33,11 @@ func ApplyPseudoInverseGadget(e air.Expr, schema *air.Schema) air.Expr {
// Determine computed column name
name := ie.String()
// Look up column
index, ok := schema.ColumnIndex(name)
index, ok := sc.ColumnIndexOf(schema, name)
// Add new column (if it does not already exist)
if !ok {
// Add (synthetic) computed column
index = schema.AddColumn(name, true)
schema.AddComputation(sc.NewComputedColumn(name, ie))
// Add computed column
index = schema.AddAssignment(assignment.NewComputedColumn(name, ie))
}

// Construct 1/e
Expand Down
Loading

0 comments on commit 8c0dd5d

Please sign in to comment.