From 87af9ac0129094145d05e15ef4f190d4c0aa7fcf Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 17 Jun 2024 17:34:31 +1200 Subject: [PATCH 1/2] Support Bounds Computation This puts in place a proper notion of a bounded computation, which replaces the previously awkward notion of `MaxShift`. This also requires that every column in a trace is given a `padding` value which is used when padding that column. The value for input columns is always `0` otherwise it is computed during trace expansion. Out-of-bounds accesses on trace columns then return the padding value. --- pkg/air/eval.go | 12 ------ pkg/air/expr.go | 46 ++++++--------------- pkg/air/gadgets/lexicographic_sort.go | 4 +- pkg/air/gadgets/normalisation.go | 4 +- pkg/air/schema.go | 10 ----- pkg/cmd/check.go | 6 +-- pkg/hir/eval.go | 7 ---- pkg/hir/expr.go | 57 +++++++++++++++++++++++++++ pkg/hir/schema.go | 15 +++---- pkg/mir/eval.go | 15 +------ pkg/mir/expr.go | 33 ++++++++++++++++ pkg/mir/schema.go | 10 ----- pkg/table/column.go | 17 +++++--- pkg/table/computation.go | 18 +++------ pkg/table/constraints.go | 14 ++++++- pkg/table/schema.go | 5 --- pkg/table/trace.go | 47 ++++++++++++---------- pkg/test/ir_test.go | 14 +++++-- testdata/norm_02.accepts | 2 +- testdata/norm_03.accepts | 2 +- testdata/norm_04.accepts | 2 +- testdata/spillage_01.accepts | 11 +++++- testdata/spillage_01.lisp | 3 +- testdata/spillage_01.rejects | 8 ++++ testdata/spillage_02.lisp | 2 + testdata/spillage_03.lisp | 2 + testdata/spillage_04.lisp | 3 ++ testdata/spillage_05.lisp | 3 ++ 28 files changed, 215 insertions(+), 157 deletions(-) create mode 100644 testdata/spillage_02.lisp create mode 100644 testdata/spillage_03.lisp create mode 100644 testdata/spillage_04.lisp create mode 100644 testdata/spillage_05.lisp diff --git a/pkg/air/eval.go b/pkg/air/eval.go index 9271ed0..1f14a7f 100644 --- a/pkg/air/eval.go +++ b/pkg/air/eval.go @@ -10,16 +10,8 @@ import ( // out-of-bounds. func (e *ColumnAccess) EvalAt(k int, tbl table.Trace) *fr.Element { val := tbl.GetByName(e.Column, k+e.Shift) - // Sanity check value is not nil - if val == nil { - // Indicates an out-of-bounds access of some kind. Note that this is - // fine and expected under normal conditions. For example, when a - // constraint accesses a row which doesn't exist (e.g. via a shift). - return nil - } var clone fr.Element - // Clone original value return clone.Set(val) } @@ -65,10 +57,6 @@ func evalExprsAt(k int, tbl table.Trace, exprs []Expr, fn func(*fr.Element, *fr. // Continue evaluating the rest for i := 1; i < len(exprs); i++ { ith := exprs[i].EvalAt(k, tbl) - if ith == nil { - return ith - } - fn(val, ith) } diff --git a/pkg/air/expr.go b/pkg/air/expr.go index f6c737c..1f37aa7 100644 --- a/pkg/air/expr.go +++ b/pkg/air/expr.go @@ -13,6 +13,7 @@ import ( // expressed within a polynomial but can be computed externally (e.g. during // trace expansion). type Expr interface { + util.Boundable // EvalAt evaluates this expression in a given tabular context. Observe that // if this expression is *undefined* within this context then it returns // "nil". An expression can be undefined for several reasons: firstly, if @@ -34,10 +35,6 @@ type Expr interface { // Equate one expression with another Equate(Expr) Expr - - // Determine the maximum shift in this expression in either the negative - // (left) or positive direction (right). - MaxShift() util.Pair[uint, uint] } // Add represents the sum over zero or more expressions. @@ -55,9 +52,9 @@ func (p *Add) Mul(other Expr) Expr { return &Mul{Args: []Expr{p, other}} } // Equate one expression with another (equivalent to subtraction). func (p *Add) Equate(other Expr) Expr { return &Sub{Args: []Expr{p, other}} } -// MaxShift returns max shift in either the negative (left) or positive +// Bounds returns max shift in either the negative (left) or positive // direction (right). -func (p *Add) MaxShift() util.Pair[uint, uint] { return maxShiftOfArray(p.Args) } +func (p *Add) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } // Sub represents the subtraction over zero or more expressions. type Sub struct{ Args []Expr } @@ -74,9 +71,9 @@ func (p *Sub) Mul(other Expr) Expr { return &Mul{Args: []Expr{p, other}} } // Equate one expression with another (equivalent to subtraction). func (p *Sub) Equate(other Expr) Expr { return &Sub{Args: []Expr{p, other}} } -// MaxShift returns max shift in either the negative (left) or positive +// Bounds returns max shift in either the negative (left) or positive // direction (right). -func (p *Sub) MaxShift() util.Pair[uint, uint] { return maxShiftOfArray(p.Args) } +func (p *Sub) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } // Mul represents the product over zero or more expressions. type Mul struct{ Args []Expr } @@ -93,9 +90,9 @@ func (p *Mul) Mul(other Expr) Expr { return &Mul{Args: []Expr{p, other}} } // Equate one expression with another (equivalent to subtraction). func (p *Mul) Equate(other Expr) Expr { return &Sub{Args: []Expr{p, other}} } -// MaxShift returns max shift in either the negative (left) or positive +// Bounds returns max shift in either the negative (left) or positive // direction (right). -func (p *Mul) MaxShift() util.Pair[uint, uint] { return maxShiftOfArray(p.Args) } +func (p *Mul) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } // Constant represents a constant value within an expression. type Constant struct{ Value *fr.Element } @@ -135,9 +132,9 @@ func (p *Constant) Mul(other Expr) Expr { return &Mul{Args: []Expr{p, other}} } // Equate one expression with another (equivalent to subtraction). func (p *Constant) Equate(other Expr) Expr { return &Sub{Args: []Expr{p, other}} } -// MaxShift returns max shift in either the negative (left) or positive +// Bounds returns max shift in either the negative (left) or positive // direction (right). A constant has zero shift. -func (p *Constant) MaxShift() util.Pair[uint, uint] { return util.NewPair[uint, uint](0, 0) } +func (p *Constant) Bounds() util.Bounds { return util.EMPTY_BOUND } // ColumnAccess represents reading the value held at a given column in the // tabular context. Furthermore, the current row maybe shifted up (or down) by @@ -168,30 +165,13 @@ func (p *ColumnAccess) Mul(other Expr) Expr { return &Mul{Args: []Expr{p, other} // Equate one expression with another (equivalent to subtraction). func (p *ColumnAccess) Equate(other Expr) Expr { return &Sub{Args: []Expr{p, other}} } -// MaxShift returns max shift in either the negative (left) or positive +// Bounds returns max shift in either the negative (left) or positive // direction (right). -func (p *ColumnAccess) MaxShift() util.Pair[uint, uint] { +func (p *ColumnAccess) Bounds() util.Bounds { if p.Shift >= 0 { // Positive shift - return util.NewPair[uint, uint](0, uint(p.Shift)) + return util.NewBounds(0, uint(p.Shift)) } // Negative shift - return util.NewPair[uint, uint](uint(-p.Shift), 0) -} - -// ========================================================================== -// Helpers -// ========================================================================== - -func maxShiftOfArray(args []Expr) util.Pair[uint, uint] { - neg := uint(0) - pos := uint(0) - - for _, e := range args { - mx := e.MaxShift() - neg = max(neg, mx.Left) - pos = max(pos, mx.Right) - } - // Done - return util.NewPair(neg, pos) + return util.NewBounds(uint(-p.Shift), 0) } diff --git a/pkg/air/gadgets/lexicographic_sort.go b/pkg/air/gadgets/lexicographic_sort.go index eef2040..95c8b53 100644 --- a/pkg/air/gadgets/lexicographic_sort.go +++ b/pkg/air/gadgets/lexicographic_sort.go @@ -230,11 +230,11 @@ func (p *lexicographicSortExpander) ExpandTrace(tr table.Trace) error { } // Add delta column data - tr.AddColumn(deltaName, delta) + tr.AddColumn(deltaName, delta, &zero) // Add bit column data for i := 0; i < ncols; i++ { bitName := fmt.Sprintf("%s:%d", prefix, i) - tr.AddColumn(bitName, bit[i]) + tr.AddColumn(bitName, bit[i], &zero) } // Done. return nil diff --git a/pkg/air/gadgets/normalisation.go b/pkg/air/gadgets/normalisation.go index 1a3875e..70e5e33 100644 --- a/pkg/air/gadgets/normalisation.go +++ b/pkg/air/gadgets/normalisation.go @@ -74,9 +74,9 @@ func (e *Inverse) EvalAt(k int, tbl table.Trace) *fr.Element { return inv.Inverse(val) } -// MaxShift returns max shift in either the negative (left) or positive +// Bounds returns max shift in either the negative (left) or positive // direction (right). -func (e *Inverse) MaxShift() util.Pair[uint, uint] { return e.Expr.MaxShift() } +func (e *Inverse) Bounds() util.Bounds { return e.Expr.Bounds() } func (e *Inverse) String() string { return fmt.Sprintf("(inv %s)", e.Expr) diff --git a/pkg/air/schema.go b/pkg/air/schema.go index 4c2a4c1..e102751 100644 --- a/pkg/air/schema.go +++ b/pkg/air/schema.go @@ -105,16 +105,6 @@ func (p *Schema) RequiredSpillage() uint { return mx } -// ApplyPadding adds n items of padding to each column of the trace. -// Padding values are placed either at the front or the back of a given -// column, depending on their interpretation. -func (p *Schema) ApplyPadding(n uint, tr table.Trace) { - tr.Pad(n, func(j int) *fr.Element { - // Extract front value to use for padding. - return tr.GetByIndex(j, 0) - }) -} - // IsInputTrace determines whether a given input trace is a suitable // input (i.e. non-expanded) trace for this schema. Specifically, the // input trace must contain a matching column for each non-synthetic diff --git a/pkg/cmd/check.go b/pkg/cmd/check.go index f0ba6dc..a834027 100644 --- a/pkg/cmd/check.go +++ b/pkg/cmd/check.go @@ -160,10 +160,10 @@ func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) (tab // Apply spillage if cfg.spillage >= 0 { // Apply user-specified spillage - table.FrontPadWithZeros(uint(cfg.spillage), tr) + tr.Pad(uint(cfg.spillage)) } else { // Apply default inferred spillage - table.FrontPadWithZeros(schema.RequiredSpillage(), tr) + tr.Pad(schema.RequiredSpillage()) } // Expand trace if err := schema.ExpandTrace(tr); err != nil { @@ -180,7 +180,7 @@ func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) (tab // Prevent interference ptr := tr.Clone() // Apply padding - schema.ApplyPadding(n, ptr) + ptr.Pad(n) // Check whether accepted or not. if err := schema.Accepts(ptr); err != nil { return ptr, err diff --git a/pkg/hir/eval.go b/pkg/hir/eval.go index e096c66..55349c1 100644 --- a/pkg/hir/eval.go +++ b/pkg/hir/eval.go @@ -10,13 +10,6 @@ import ( // out-of-bounds. func (e *ColumnAccess) EvalAllAt(k int, tbl table.Trace) []*fr.Element { val := tbl.GetByName(e.Column, k+e.Shift) - // Sanity check value is not nil - if val == nil { - // Indicates an out-of-bounds access of some kind. Note that this is - // fine and expected under normal conditions. For example, when a - // constraint accesses a row which doesn't exist (e.g. via a shift). - return nil - } var clone fr.Element // Clone original value diff --git a/pkg/hir/expr.go b/pkg/hir/expr.go index d5f59fe..7766be9 100644 --- a/pkg/hir/expr.go +++ b/pkg/hir/expr.go @@ -4,6 +4,7 @@ import ( "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" "github.com/consensys/go-corset/pkg/mir" "github.com/consensys/go-corset/pkg/table" + "github.com/consensys/go-corset/pkg/util" ) // ============================================================================ @@ -15,6 +16,7 @@ import ( // in the AIR level. For example, an "if" expression at this level will be // "compiled out" into one or more expressions at the MIR level. type Expr interface { + util.Boundable // LowerTo lowers this expression into the Mid-Level Intermediate // Representation. Observe that a single expression at this // level can expand into *multiple* expressions at the MIR @@ -34,18 +36,38 @@ type Expr interface { // Add represents the sum over zero or more expressions. type Add struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Add) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // Sub represents the subtraction over zero or more expressions. type Sub struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Sub) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // Mul represents the product over zero or more expressions. type Mul struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Mul) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // List represents a block of zero or more expressions. type List struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *List) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // Constant represents a constant value within an expression. type Constant struct{ Val *fr.Element } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). A constant has zero shift. +func (p *Constant) Bounds() util.Bounds { return util.EMPTY_BOUND } + // IfZero returns the (optional) true branch when the condition evaluates to zero, and // the (optional false branch otherwise. type IfZero struct { @@ -57,10 +79,34 @@ type IfZero struct { FalseBranch Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *IfZero) Bounds() util.Bounds { + c := p.Condition.Bounds() + // Get bounds for true branch (if applicable) + if p.TrueBranch != nil { + tbounds := p.TrueBranch.Bounds() + c.Union(&tbounds) + } + // Get bounds for false branch (if applicable) + if p.FalseBranch != nil { + fbounds := p.FalseBranch.Bounds() + c.Union(&fbounds) + } + // Done + return c +} + // Normalise reduces the value of an expression to either zero (if it was zero) // or one (otherwise). type Normalise struct{ Arg Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Normalise) Bounds() util.Bounds { + return p.Arg.Bounds() +} + // ColumnAccess represents reading the value held at a given column in the // tabular context. Furthermore, the current row maybe shifted up (or down) by // a given amount. Suppose we are evaluating a constraint on row k=5 which @@ -71,3 +117,14 @@ type ColumnAccess struct { Column string Shift int } + +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *ColumnAccess) Bounds() util.Bounds { + if p.Shift >= 0 { + // Positive shift + return util.NewBounds(0, uint(p.Shift)) + } + // Negative shift + return util.NewBounds(uint(-p.Shift), 0) +} diff --git a/pkg/hir/schema.go b/pkg/hir/schema.go index 5a177c6..3a2ac34 100644 --- a/pkg/hir/schema.go +++ b/pkg/hir/schema.go @@ -1,7 +1,6 @@ package hir import ( - "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" "github.com/consensys/go-corset/pkg/mir" "github.com/consensys/go-corset/pkg/table" "github.com/consensys/go-corset/pkg/util" @@ -35,6 +34,11 @@ func (p ZeroArrayTest) String() string { return p.Expr.String() } +// Bounds determines the bounds for this zero test. +func (p ZeroArrayTest) Bounds() util.Bounds { + return p.Expr.Bounds() +} + // DataColumn captures the essence of a data column at AIR level. type DataColumn = *table.DataColumn[table.Type] @@ -109,15 +113,6 @@ func (p *Schema) RequiredSpillage() uint { return uint(1) } -// ApplyPadding adds n items of padding to each column of the trace. -// Padding values are placed either at the front or the back of a given -// column, depending on their interpretation. -func (p *Schema) ApplyPadding(n uint, tr table.Trace) { - tr.Pad(n, func(j int) *fr.Element { - return tr.GetByIndex(j, 0) - }) -} - // GetDeclaration returns the ith declaration in this schema. func (p *Schema) GetDeclaration(index int) table.Declaration { ith := util.FlatArrayIndexOf_4(index, p.dataColumns, p.permutations, p.vanishing, p.assertions) diff --git a/pkg/mir/eval.go b/pkg/mir/eval.go index b423790..fca0eb6 100644 --- a/pkg/mir/eval.go +++ b/pkg/mir/eval.go @@ -10,13 +10,6 @@ import ( // out-of-bounds. func (e *ColumnAccess) EvalAt(k int, tbl table.Trace) *fr.Element { val := tbl.GetByName(e.Column, k+e.Shift) - // Sanity check value is not nil - if val == nil { - // Indicates an out-of-bounds access of some kind. Note that this is - // fine and expected under normal conditions. For example, when a - // constraint accesses a row which doesn't exist (e.g. via a shift). - return nil - } var clone fr.Element // Clone original value @@ -52,7 +45,7 @@ func (e *Normalise) EvalAt(k int, tbl table.Trace) *fr.Element { // Check whether argument evaluates to zero or not. val := e.Arg.EvalAt(k, tbl) // Normalise value (if necessary) - if val != nil && !val.IsZero() { + if !val.IsZero() { val.SetOne() } // Done @@ -71,15 +64,9 @@ func (e *Sub) EvalAt(k int, tbl table.Trace) *fr.Element { func evalExprsAt(k int, tbl table.Trace, exprs []Expr, fn func(*fr.Element, *fr.Element)) *fr.Element { // Evaluate first argument val := exprs[0].EvalAt(k, tbl) - if val == nil { - return nil - } // Continue evaluating the rest for i := 1; i < len(exprs); i++ { ith := exprs[i].EvalAt(k, tbl) - if ith == nil { - return ith - } fn(val, ith) } diff --git a/pkg/mir/expr.go b/pkg/mir/expr.go index 1f97a4c..620fb37 100644 --- a/pkg/mir/expr.go +++ b/pkg/mir/expr.go @@ -4,6 +4,7 @@ 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/util" ) // Expr represents an expression in the Mid-Level Intermediate Representation @@ -12,6 +13,7 @@ import ( // exist at the AIR level (e.g. normalise) and are "compiled out" by introducing // appropriate computed columns and constraints. type Expr interface { + util.Boundable // Lower this expression into the Arithmetic Intermediate // Representation. Essentially, this means eliminating // normalising expressions by introducing new columns into the @@ -31,19 +33,39 @@ type Expr interface { // Add represents the sum over zero or more expressions. type Add struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Add) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // Sub represents the subtraction over zero or more expressions. type Sub struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Sub) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // Mul represents the product over zero or more expressions. type Mul struct{ Args []Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Mul) Bounds() util.Bounds { return util.BoundsForArray(p.Args) } + // Constant represents a constant value within an expression. type Constant struct{ Value *fr.Element } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). A constant has zero shift. +func (p *Constant) Bounds() util.Bounds { return util.EMPTY_BOUND } + // Normalise reduces the value of an expression to either zero (if it was zero) // or one (otherwise). type Normalise struct{ Arg Expr } +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *Normalise) Bounds() util.Bounds { return p.Arg.Bounds() } + // ColumnAccess represents reading the value held at a given column in the // tabular context. Furthermore, the current row maybe shifted up (or down) by // a given amount. Suppose we are evaluating a constraint on row k=5 which @@ -54,3 +76,14 @@ type ColumnAccess struct { Column string Shift int } + +// Bounds returns max shift in either the negative (left) or positive +// direction (right). +func (p *ColumnAccess) Bounds() util.Bounds { + if p.Shift >= 0 { + // Positive shift + return util.NewBounds(0, uint(p.Shift)) + } + // Negative shift + return util.NewBounds(uint(-p.Shift), 0) +} diff --git a/pkg/mir/schema.go b/pkg/mir/schema.go index 53cf321..43e3a47 100644 --- a/pkg/mir/schema.go +++ b/pkg/mir/schema.go @@ -3,7 +3,6 @@ package mir import ( "fmt" - "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" "github.com/consensys/go-corset/pkg/air" air_gadgets "github.com/consensys/go-corset/pkg/air/gadgets" "github.com/consensys/go-corset/pkg/table" @@ -76,15 +75,6 @@ func (p *Schema) RequiredSpillage() uint { return uint(1) } -// ApplyPadding adds n items of padding to each column of the trace. -// Padding values are placed either at the front or the back of a given -// column, depending on their interpretation. -func (p *Schema) ApplyPadding(n uint, tr table.Trace) { - tr.Pad(n, func(j int) *fr.Element { - return tr.GetByIndex(j, 0) - }) -} - // GetDeclaration returns the ith declaration in this schema. func (p *Schema) GetDeclaration(index int) table.Declaration { ith := util.FlatArrayIndexOf_4(index, p.dataColumns, p.permutations, p.vanishing, p.assertions) diff --git a/pkg/table/column.go b/pkg/table/column.go index 7c02db0..4158f85 100644 --- a/pkg/table/column.go +++ b/pkg/table/column.go @@ -70,7 +70,7 @@ func (c *DataColumn[T]) String() string { // expectation that this computation is acyclic. Furthermore, computed columns // give rise to "trace expansion". That is where the initial trace provided by // the user is expanded by determining the value of all computed columns. -type ComputedColumn[E Computable] struct { +type ComputedColumn[E Evaluable] struct { Name string // The computation which accepts a given trace and computes // the value of this column at a given row. @@ -80,7 +80,7 @@ type ComputedColumn[E Computable] struct { // NewComputedColumn constructs a new computed column with a given name and // determining expression. More specifically, that expression is used to // compute the values for this column during trace expansion. -func NewComputedColumn[E Computable](name string, expr E) *ComputedColumn[E] { +func NewComputedColumn[E Evaluable](name string, expr E) *ComputedColumn[E] { return &ComputedColumn[E]{ Name: name, Expr: expr, @@ -95,7 +95,7 @@ func (c *ComputedColumn[E]) RequiredSpillage() uint { // (i.e. start) of a trace. This is because padding is always inserted at // the front, never the back. As such, it is the maximum positive shift // which determines how much spillage is required for this comptuation. - return c.Expr.MaxShift().Right + return c.Expr.Bounds().End } // Accepts determines whether or not this column accepts the given trace. For a @@ -132,8 +132,12 @@ func (c *ComputedColumn[E]) ExpandTrace(tr Trace) error { data[i] = &zero } } + // Determine padding value. A negative row index is used here to ensure + // that all columns return their padding value which is then used to compute + // the padding value for *this* column. + padding := c.Expr.EvalAt(-1, tr) // Colunm needs to be expanded. - tr.AddColumn(c.Name, data) + tr.AddColumn(c.Name, data, padding) // Done return nil } @@ -280,8 +284,9 @@ func (p *SortedPermutation) ExpandTrace(tr Trace) error { util.PermutationSort(cols, p.Signs) // Physically add the columns for i := 0; i < len(p.Targets); i++ { - col := p.Targets[i] - tr.AddColumn(col, cols[i]) + dstColName := p.Targets[i] + srcCol := tr.ColumnByName(p.Sources[i]) + tr.AddColumn(dstColName, cols[i], srcCol.Padding()) } // return nil diff --git a/pkg/table/computation.go b/pkg/table/computation.go index 1954b24..9267406 100644 --- a/pkg/table/computation.go +++ b/pkg/table/computation.go @@ -4,7 +4,6 @@ import ( "fmt" "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" - "github.com/consensys/go-corset/pkg/util" ) // TraceComputation represents a computation which is applied to a @@ -25,17 +24,6 @@ type TraceComputation interface { RequiredSpillage() uint } -// Computable is an extension of the Evaluable interface which additionally -// allows one to determine specifics about the computation needed to ensure it -// can be correctly computed on a given trace. -type Computable interface { - Evaluable - - // Determine the maximum shift in this expression in either the negative - // (left) or positive direction (right). - MaxShift() util.Pair[uint, uint] -} - // ByteDecomposition is part of a range constraint for wide columns (e.g. u32) // implemented using a byte decomposition. type ByteDecomposition struct { @@ -76,6 +64,8 @@ func (p *ByteDecomposition) Accepts(tr Trace) error { func (p *ByteDecomposition) ExpandTrace(tr Trace) error { // Calculate how many bytes required. n := int(p.BitWidth / 8) + // Identify target column + target := tr.ColumnByName(p.Target) // Extract column data to decompose data := tr.ColumnByName(p.Target).Data() // Construct byte column data @@ -91,10 +81,12 @@ func (p *ByteDecomposition) ExpandTrace(tr Trace) error { cols[j][i] = ith[j] } } + // Determine padding values + padding := decomposeIntoBytes(target.Padding(), n) // Finally, add byte columns to trace for i := 0; i < n; i++ { col := fmt.Sprintf("%s:%d", p.Target, i) - tr.AddColumn(col, cols[i]) + tr.AddColumn(col, cols[i], padding[i]) } // Done return nil diff --git a/pkg/table/constraints.go b/pkg/table/constraints.go index 6d661fb..89662cb 100644 --- a/pkg/table/constraints.go +++ b/pkg/table/constraints.go @@ -5,6 +5,7 @@ import ( "fmt" "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" + "github.com/consensys/go-corset/pkg/util" ) // Evaluable captures something which can be evaluated on a given table row to @@ -12,6 +13,7 @@ import ( // Mid-Level or Arithmetic-Level IR can all be evaluated at rows of a // table. type Evaluable interface { + util.Boundable // EvalAt evaluates this expression in a given tabular context. // Observe that if this expression is *undefined* within this // context then it returns "nil". An expression can be @@ -28,6 +30,8 @@ type Evaluable interface { // Evaluable (i.e. because they return multiple values, rather than a single // value). However, constraints at the HIR level remain testable. type Testable interface { + util.Boundable + // TestAt evaluates this expression in a given tabular context and checks it // against zero. Observe that if this expression is *undefined* within this // context then it returns "nil". An expression can be undefined for @@ -54,6 +58,11 @@ func (p ZeroTest[E]) TestAt(row int, tr Trace) bool { return val == nil || val.IsZero() } +// Bounds determines the bounds for this zero test. +func (p ZeroTest[E]) Bounds() util.Bounds { + return p.Expr.Bounds() +} + // String generates a human-readble string. // //nolint:revive @@ -106,7 +115,10 @@ func (p *RowConstraint[T]) Accepts(tr Trace) error { // HoldsGlobally checks whether a given expression vanishes (i.e. evaluates to // zero) for all rows of a trace. If not, report an appropriate error. func HoldsGlobally[T Testable](handle string, constraint T, tr Trace) error { - for k := uint(0); k < tr.Height(); k++ { + // Determine well-definedness bounds for this constraint + bounds := constraint.Bounds() + // Check all in-bounds values + for k := bounds.Start; k < (tr.Height() - bounds.End); k++ { if err := HoldsLocally(int(k), handle, constraint, tr); err != nil { return err } diff --git a/pkg/table/schema.go b/pkg/table/schema.go index da04db8..634d824 100644 --- a/pkg/table/schema.go +++ b/pkg/table/schema.go @@ -21,11 +21,6 @@ type Schema interface { // ensure valid traces are accepted in the presence of arbitrary padding. // Note: this is calculated on demand. RequiredSpillage() uint - - // ApplyPadding adds n items of padding to each column of the trace. - // Padding values are placed either at the front or the back of a given - // column, depending on their interpretation. - ApplyPadding(uint, Trace) } // Declaration represents a declared element of a schema. For example, a column diff --git a/pkg/table/trace.go b/pkg/table/trace.go index eed6020..6d2e888 100644 --- a/pkg/table/trace.go +++ b/pkg/table/trace.go @@ -24,13 +24,15 @@ type Column interface { Height() uint // Return the data stored in this column. Data() []*fr.Element + // Return the value to use for padding this column. + Padding() *fr.Element } // Trace describes a set of named columns. Columns are not required to have the // same height and can be either "data" columns or "computed" columns. type Trace interface { // Add a new column of data - AddColumn(name string, data []*fr.Element) + AddColumn(name string, data []*fr.Element, padding *fr.Element) // Get the name of the ith column in this trace. ColumnName(int) string // ColumnByIndex returns the ith column in this trace. @@ -55,7 +57,7 @@ type Trace interface { GetByIndex(col int, row int) *fr.Element // Pad each column in this trace with n items at the front. An iterator over // the padding values to use for each column must be given. - Pad(n uint, signs func(int) *fr.Element) + Pad(n uint) // Determine the height of this table, which is defined as the // height of the largest column. Height() uint @@ -77,13 +79,6 @@ func ConstraintsAcceptTrace[T Acceptable](trace Trace, constraints []T) error { return nil } -// FrontPadWithZeros adds n rows of zeros to the given trace. -func FrontPadWithZeros(n uint, tr Trace) { - var zero fr.Element = fr.NewElement((0)) - // Insert initial padding row - tr.Pad(n, func(index int) *fr.Element { return &zero }) -} - // =================================================================== // Array Trace // =================================================================== @@ -145,13 +140,13 @@ func (p *ArrayTrace) HasColumn(name string) bool { } // AddColumn adds a new column of data to this trace. -func (p *ArrayTrace) AddColumn(name string, data []*fr.Element) { +func (p *ArrayTrace) AddColumn(name string, data []*fr.Element, padding *fr.Element) { // Sanity check the column does not already exist. if p.HasColumn(name) { panic("column already exists") } // Construct new column - column := ArrayTraceColumn{name, data} + column := ArrayTraceColumn{name, data, padding} // Append it p.columns = append(p.columns, &column) // Update maximum height @@ -227,9 +222,9 @@ func (p *ArrayTrace) Height() uint { // Pad each column in this trace with n items at the front. An iterator over // the padding values to use for each column must be given. -func (p *ArrayTrace) Pad(n uint, padding func(int) *fr.Element) { - for i, c := range p.columns { - c.Pad(n, padding(i)) +func (p *ArrayTrace) Pad(n uint) { + for _, c := range p.columns { + c.Pad(n) } // Increment height p.height += n @@ -279,6 +274,8 @@ type ArrayTraceColumn struct { name string // Holds the raw data making up this column data []*fr.Element + // Value to be used when padding this column + padding *fr.Element } // Name returns the name of the given column. @@ -291,6 +288,11 @@ func (p *ArrayTraceColumn) Height() uint { return uint(len(p.data)) } +// Padding returns the value which will be used for padding this column. +func (p *ArrayTraceColumn) Padding() *fr.Element { + return p.padding +} + // Data returns the data for the given column. func (p *ArrayTraceColumn) Data() []*fr.Element { return p.data @@ -301,6 +303,7 @@ func (p *ArrayTraceColumn) Clone() *ArrayTraceColumn { clone := new(ArrayTraceColumn) clone.name = p.name clone.data = make([]*fr.Element, len(p.data)) + clone.padding = p.padding copy(clone.data, p.data) return clone @@ -308,14 +311,14 @@ func (p *ArrayTraceColumn) Clone() *ArrayTraceColumn { // Pad this column with n copies of a given value, either at the front // (sign=true) or the back (sign=false). -func (p *ArrayTraceColumn) Pad(n uint, value *fr.Element) { +func (p *ArrayTraceColumn) Pad(n uint) { // Allocate sufficient memory ndata := make([]*fr.Element, uint(len(p.data))+n) // Copy over the data copy(ndata[n:], p.data) // Go padding! for i := uint(0); i < n; i++ { - ndata[i] = value + ndata[i] = p.padding } // Copy over p.data = ndata @@ -323,11 +326,11 @@ func (p *ArrayTraceColumn) Pad(n uint, value *fr.Element) { // Get the value at the given row of this column. func (p *ArrayTraceColumn) Get(row int) *fr.Element { - if row < 0 || row >= len(p.data) { - return nil + if row >= 0 && row < len(p.data) { + return p.data[row] } - - return p.data[row] + // For out-of-bounds access, return padding value. + return p.padding } // =================================================================== @@ -338,6 +341,8 @@ func (p *ArrayTraceColumn) Get(row int) *fr.Element { // [0], "Y": [1]} is a trace containing one row of data each for two columns "X" // and "Y". func ParseJsonTrace(bytes []byte) (*ArrayTrace, error) { + var zero fr.Element = fr.NewElement((0)) + var rawData map[string][]*big.Int // Unmarshall jsonErr := json.Unmarshal(bytes, &rawData) @@ -351,7 +356,7 @@ func ParseJsonTrace(bytes []byte) (*ArrayTrace, error) { // Translate raw bigints into raw field elements rawElements := util.ToFieldElements(rawInts) // Add new column to the trace - trace.AddColumn(name, rawElements) + trace.AddColumn(name, rawElements, &zero) } // Done. diff --git a/pkg/test/ir_test.go b/pkg/test/ir_test.go index a9961c4..71cb8a7 100644 --- a/pkg/test/ir_test.go +++ b/pkg/test/ir_test.go @@ -129,6 +129,14 @@ func Test_Shift_07(t *testing.T) { Check(t, "shift_07") } +// =================================================================== +// Spillage Tests +// =================================================================== + +func Test_Spillage_01(t *testing.T) { + Check(t, "spillage_01") +} + // =================================================================== // Normalisation Tests // =================================================================== @@ -311,7 +319,7 @@ func TestSlow_Mxp(t *testing.T) { // Determines the maximum amount of padding to use when testing. Specifically, // every trace is tested with varying amounts of padding upto this value. -const MAX_PADDING uint = 0 +const MAX_PADDING uint = 1 // For a given set of constraints, check that all traces which we // expect to be accepted are accepted, and all traces that we expect @@ -381,7 +389,7 @@ func checkInputTrace(t *testing.T, tr *table.ArrayTrace, id traceId, schema tabl // Clone trace (to ensure expansion does not affect subsequent tests) etr := tr.Clone() // Apply spillage - table.FrontPadWithZeros(schema.RequiredSpillage(), etr) + etr.Pad(schema.RequiredSpillage()) // Expand trace err := schema.ExpandTrace(etr) // Check @@ -394,7 +402,7 @@ func checkInputTrace(t *testing.T, tr *table.ArrayTrace, id traceId, schema tabl func checkExpandedTrace(t *testing.T, tr table.Trace, id traceId, schema table.Schema) { // Apply padding - schema.ApplyPadding(id.padding, tr) + tr.Pad(id.padding) // Check err := schema.Accepts(tr) // Determine whether trace accepted or not. diff --git a/testdata/norm_02.accepts b/testdata/norm_02.accepts index 483c5bc..0881160 100644 --- a/testdata/norm_02.accepts +++ b/testdata/norm_02.accepts @@ -1,4 +1,4 @@ -{ "ST": [1], "A": [], "B": [] } +{ "ST": [], "A": [], "B": [] } { "ST": [1], "A": [-1], "B": [-1] } { "ST": [1], "A": [-1], "B": [0] } { "ST": [1], "A": [0], "B": [-1] } diff --git a/testdata/norm_03.accepts b/testdata/norm_03.accepts index 3c2d060..87552c8 100644 --- a/testdata/norm_03.accepts +++ b/testdata/norm_03.accepts @@ -1,4 +1,4 @@ -{ "ST": [1], "A": [], "B": [] } +{ "ST": [], "A": [], "B": [] } { "ST": [1], "A": [-1], "B": [0] } { "ST": [1], "A": [1], "B": [0] } { "ST": [1], "A": [0], "B": [-1] } diff --git a/testdata/norm_04.accepts b/testdata/norm_04.accepts index 00b3460..b1329f5 100644 --- a/testdata/norm_04.accepts +++ b/testdata/norm_04.accepts @@ -1,4 +1,4 @@ -{ "ST": [1], "A": [], "B": [] } +{ "ST": [], "A": [], "B": [] } { "ST": [1], "A": [-2], "B": [-2] } { "ST": [1], "A": [-2], "B": [-1] } { "ST": [1], "A": [-2], "B": [0] } diff --git a/testdata/spillage_01.accepts b/testdata/spillage_01.accepts index 8a3e0a7..9d88959 100644 --- a/testdata/spillage_01.accepts +++ b/testdata/spillage_01.accepts @@ -1 +1,10 @@ -{ "A": {} } +{ "ST": [], "A": [] } +{ "ST": [1], "A": [0] } +{ "ST": [1,1], "A": [0,0] } +{ "ST": [1,1], "A": [0,1] } +{ "ST": [1,1], "A": [1,0] } +{ "ST": [1,1,1], "A": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0] } +{ "ST": [1,1,1], "A": [1,0,1] } diff --git a/testdata/spillage_01.lisp b/testdata/spillage_01.lisp index 73469a7..52948f9 100644 --- a/testdata/spillage_01.lisp +++ b/testdata/spillage_01.lisp @@ -1,2 +1,3 @@ +(column ST) (column A) -(vanish spills (* A (~ (shift A 1)))) +(vanish spills (* ST (* A (~ (shift A 1))))) diff --git a/testdata/spillage_01.rejects b/testdata/spillage_01.rejects index e69de29..b0ed581 100644 --- a/testdata/spillage_01.rejects +++ b/testdata/spillage_01.rejects @@ -0,0 +1,8 @@ +{ "ST": [1,1], "A": [1,1] } +{ "ST": [1,1], "A": [2,1] } +{ "ST": [1,1], "A": [1,2] } +{ "ST": [1,1], "A": [2,2] } +{ "ST": [1,1], "A": [0,1,1] } +{ "ST": [1,1], "A": [0,2,1] } +{ "ST": [1,1], "A": [0,1,2] } +{ "ST": [1,1], "A": [0,2,2] } diff --git a/testdata/spillage_02.lisp b/testdata/spillage_02.lisp new file mode 100644 index 0000000..659f74b --- /dev/null +++ b/testdata/spillage_02.lisp @@ -0,0 +1,2 @@ +(column A) +(vanish spills (~ (shift A 2))) diff --git a/testdata/spillage_03.lisp b/testdata/spillage_03.lisp new file mode 100644 index 0000000..1c421a2 --- /dev/null +++ b/testdata/spillage_03.lisp @@ -0,0 +1,2 @@ +(column A) +(vanish spills (~ (shift A 3))) diff --git a/testdata/spillage_04.lisp b/testdata/spillage_04.lisp new file mode 100644 index 0000000..5aa6837 --- /dev/null +++ b/testdata/spillage_04.lisp @@ -0,0 +1,3 @@ +(column A) +(column B) +(vanish spills (~ (* (shift A 3) (shift B 2)))) diff --git a/testdata/spillage_05.lisp b/testdata/spillage_05.lisp new file mode 100644 index 0000000..4de8730 --- /dev/null +++ b/testdata/spillage_05.lisp @@ -0,0 +1,3 @@ +(column A) +(column B) +(vanish spills (~ (* (shift A 2) (shift B 3)))) From f6cddd890abda3a7a532f8c3d84ed262590a5828 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 17 Jun 2024 19:24:42 +1200 Subject: [PATCH 2/2] Fixing outstanding `spillage` tests This fixes the outstanding spillage tests which were written, but not actually being used. --- .pre-commit-config.yaml | 1 + pkg/table/constraints.go | 11 ++- pkg/test/ir_test.go | 12 +++ pkg/util/bounds.go | 47 ++++++++++++ testdata/spillage_02.accepts | 10 +++ testdata/spillage_02.lisp | 3 +- testdata/spillage_02.rejects | 5 ++ testdata/spillage_03.accepts | 15 ++++ testdata/spillage_03.lisp | 3 +- testdata/spillage_03.rejects | 7 ++ testdata/spillage_04.accepts | 144 +++++++++++++++++++++++++++++++++++ testdata/spillage_04.lisp | 3 +- testdata/spillage_04.rejects | 31 ++++++++ testdata/spillage_05.lisp | 3 - 14 files changed, 285 insertions(+), 10 deletions(-) create mode 100644 pkg/util/bounds.go create mode 100644 testdata/spillage_02.accepts create mode 100644 testdata/spillage_02.rejects create mode 100644 testdata/spillage_03.accepts create mode 100644 testdata/spillage_03.rejects create mode 100644 testdata/spillage_04.accepts create mode 100644 testdata/spillage_04.rejects delete mode 100644 testdata/spillage_05.lisp diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 777db69..064e2aa 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -11,6 +11,7 @@ repos: rev: v1.0.0-rc.1 hooks: - id: go-test-mod + args: [ --run=Test_ ] - repo: https://github.com/golangci/golangci-lint rev: v1.57.1 hooks: diff --git a/pkg/table/constraints.go b/pkg/table/constraints.go index 89662cb..d8bcb9e 100644 --- a/pkg/table/constraints.go +++ b/pkg/table/constraints.go @@ -117,10 +117,13 @@ func (p *RowConstraint[T]) Accepts(tr Trace) error { func HoldsGlobally[T Testable](handle string, constraint T, tr Trace) error { // Determine well-definedness bounds for this constraint bounds := constraint.Bounds() - // Check all in-bounds values - for k := bounds.Start; k < (tr.Height() - bounds.End); k++ { - if err := HoldsLocally(int(k), handle, constraint, tr); err != nil { - return err + // Sanity check enough rows + if bounds.End < tr.Height() { + // Check all in-bounds values + for k := bounds.Start; k < (tr.Height() - bounds.End); k++ { + if err := HoldsLocally(int(k), handle, constraint, tr); err != nil { + return err + } } } // Success diff --git a/pkg/test/ir_test.go b/pkg/test/ir_test.go index 71cb8a7..eef73e0 100644 --- a/pkg/test/ir_test.go +++ b/pkg/test/ir_test.go @@ -137,6 +137,18 @@ func Test_Spillage_01(t *testing.T) { Check(t, "spillage_01") } +func Test_Spillage_02(t *testing.T) { + Check(t, "spillage_02") +} + +func Test_Spillage_03(t *testing.T) { + Check(t, "spillage_03") +} + +func Test_Spillage_04(t *testing.T) { + Check(t, "spillage_04") +} + // =================================================================== // Normalisation Tests // =================================================================== diff --git a/pkg/util/bounds.go b/pkg/util/bounds.go new file mode 100644 index 0000000..d8b19ff --- /dev/null +++ b/pkg/util/bounds.go @@ -0,0 +1,47 @@ +package util + +// EMPTY_BOUND is the bound which overlaps exactly with the original range. It +// represents the maximum possible bound. +var EMPTY_BOUND Bounds = Bounds{0, 0} + +// Bounds captures the subrange of rows for which a computation is well-defined. +type Bounds struct { + // Number of rows from first row where computation starts being defined. + Start uint + // Number of rows before last row where computation is no longer defined. + End uint +} + +// NewBounds constructs a new set of bounds. +func NewBounds(start uint, end uint) Bounds { + return Bounds{start, end} +} + +// Union merges one set of bounds into another. +func (p *Bounds) Union(q *Bounds) { + p.Start = max(p.Start, q.Start) + p.End = max(p.End, q.End) +} + +// Boundable captures computations which are well-defined only for a specific +// subrange of rows (the bounds). +type Boundable interface { + // Determine the well-definedness bounds for this expression for both the + // negative (left) or positive (right) directions. For example, consider an + // expression such as "(shift X -1)". This is technically undefined for the + // first row of any trace and, by association, any constraint evaluating + // this expression on that first row is also undefined (and hence must pass). + Bounds() Bounds +} + +// BoundsForArray determines the bounds for an array of expressions. +func BoundsForArray[E Boundable](args []E) Bounds { + bounds := Bounds{0, 0} + + for _, e := range args { + ith := e.Bounds() + bounds.Union(&ith) + } + // Done + return bounds +} diff --git a/testdata/spillage_02.accepts b/testdata/spillage_02.accepts new file mode 100644 index 0000000..c03607d --- /dev/null +++ b/testdata/spillage_02.accepts @@ -0,0 +1,10 @@ +{ "ST": [], "A": [] } +{ "ST": [1], "A": [0] } +{ "ST": [1,1], "A": [0,0] } +{ "ST": [1,1], "A": [0,1] } +{ "ST": [1,1], "A": [1,0] } +{ "ST": [1,1,1], "A": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1] } diff --git a/testdata/spillage_02.lisp b/testdata/spillage_02.lisp index 659f74b..1fcc586 100644 --- a/testdata/spillage_02.lisp +++ b/testdata/spillage_02.lisp @@ -1,2 +1,3 @@ +(column ST) (column A) -(vanish spills (~ (shift A 2))) +(vanish spills (* ST (* A (~ (shift A 2))))) diff --git a/testdata/spillage_02.rejects b/testdata/spillage_02.rejects new file mode 100644 index 0000000..9efe7e5 --- /dev/null +++ b/testdata/spillage_02.rejects @@ -0,0 +1,5 @@ +{ "ST": [1,1,1], "A": [1,0,1] } +{ "ST": [1,1,1], "A": [1,1,1] } +{ "ST": [1,1,1], "A": [1,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,1] } diff --git a/testdata/spillage_03.accepts b/testdata/spillage_03.accepts new file mode 100644 index 0000000..d647246 --- /dev/null +++ b/testdata/spillage_03.accepts @@ -0,0 +1,15 @@ +{ "ST": [], "A": [] } +{ "ST": [1], "A": [0] } +{ "ST": [1,1], "A": [0,0] } +{ "ST": [1,1], "A": [0,1] } +{ "ST": [1,1], "A": [1,0] } +{ "ST": [1,1,1], "A": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0] } +{ "ST": [1,1,1], "A": [1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,1] } +{ "ST": [1,1,1,1,1], "A": [1,0,1,0,1] } diff --git a/testdata/spillage_03.lisp b/testdata/spillage_03.lisp index 1c421a2..9004671 100644 --- a/testdata/spillage_03.lisp +++ b/testdata/spillage_03.lisp @@ -1,2 +1,3 @@ +(column ST) (column A) -(vanish spills (~ (shift A 3))) +(vanish spills (* ST A (~ (shift A 3)))) diff --git a/testdata/spillage_03.rejects b/testdata/spillage_03.rejects new file mode 100644 index 0000000..069db67 --- /dev/null +++ b/testdata/spillage_03.rejects @@ -0,0 +1,7 @@ +{ "ST": [1,1,1,1], "A": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1] } +{ "ST": [1,1,0,1], "A": [1,0,0,1] } +{ "ST": [1,0,1,1], "A": [1,0,0,1] } +{ "ST": [1,0,0,1], "A": [1,0,0,1] } diff --git a/testdata/spillage_04.accepts b/testdata/spillage_04.accepts new file mode 100644 index 0000000..ebca25a --- /dev/null +++ b/testdata/spillage_04.accepts @@ -0,0 +1,144 @@ +{ "ST": [], "A": [], "B": [] } +{ "ST": [1], "A": [1], "B": [1] } +{ "ST": [1], "A": [0], "B": [1] } +{ "ST": [1], "A": [1], "B": [0] } +{ "ST": [1], "A": [0], "B": [0] } +;; +{ "ST": [1,1], "A": [0,0], "B": [0,0] } +{ "ST": [1,1], "A": [0,1], "B": [0,0] } +{ "ST": [1,1], "A": [1,0], "B": [0,0] } +{ "ST": [1,1], "A": [1,1], "B": [0,0] } +{ "ST": [1,1], "A": [0,0], "B": [1,0] } +{ "ST": [1,1], "A": [0,1], "B": [1,0] } +{ "ST": [1,1], "A": [1,0], "B": [1,0] } +{ "ST": [1,1], "A": [1,1], "B": [1,0] } +{ "ST": [1,1], "A": [0,0], "B": [0,1] } +{ "ST": [1,1], "A": [0,1], "B": [0,1] } +{ "ST": [1,1], "A": [1,0], "B": [0,1] } +{ "ST": [1,1], "A": [1,1], "B": [0,1] } +;; +{ "ST": [1,1,1], "A": [0,0,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,0,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,0,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [0,0,1] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,1,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,0,1] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,1,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,1,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,0,1] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,1,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,0,1] } diff --git a/testdata/spillage_04.lisp b/testdata/spillage_04.lisp index 5aa6837..a16fbb8 100644 --- a/testdata/spillage_04.lisp +++ b/testdata/spillage_04.lisp @@ -1,3 +1,4 @@ +(column ST) (column A) (column B) -(vanish spills (~ (* (shift A 3) (shift B 2)))) +(vanish spills (* ST A (~ (* (shift A 3) (shift B 2))))) diff --git a/testdata/spillage_04.rejects b/testdata/spillage_04.rejects new file mode 100644 index 0000000..0babfaa --- /dev/null +++ b/testdata/spillage_04.rejects @@ -0,0 +1,31 @@ +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,1,1,1] } +;; +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,1,1,1] } +;; +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,1,1,1] } +;; +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,1,1,1] } diff --git a/testdata/spillage_05.lisp b/testdata/spillage_05.lisp deleted file mode 100644 index 4de8730..0000000 --- a/testdata/spillage_05.lisp +++ /dev/null @@ -1,3 +0,0 @@ -(column A) -(column B) -(vanish spills (~ (* (shift A 2) (shift B 3))))