From 953de6b6f40229b2aff83d327c0be9dedf79fb03 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 17 Jun 2024 14:46:17 +1200 Subject: [PATCH] Resolve issues around negative permutation sorts There are some genuinely hard problems with negative permutation sorts. The current solution is simply to prohibit permutation sorts whose "index column" (i.e. leftmost column) is negatively sorted. There is an additional issue that traces which have a `0` for this column prior to expansion will (most likely) be rejected. --- pkg/air/gadgets/bits.go | 3 +- pkg/air/schema.go | 10 +++--- pkg/cmd/check.go | 45 +++++++++++++---------- pkg/hir/parser.go | 4 +++ pkg/hir/schema.go | 5 ++- pkg/mir/schema.go | 5 ++- pkg/table/printer.go | 71 ++++++++++++++++++++++++++++++++++++ pkg/table/trace.go | 41 ++++++--------------- pkg/test/ir_test.go | 72 +++---------------------------------- testdata/permute_04.accepts | 24 ++++++------- testdata/permute_04.lisp | 5 +-- testdata/permute_04.rejects | 10 +++--- testdata/permute_07.accepts | 30 ++++++++-------- testdata/permute_07.lisp | 5 +-- testdata/permute_07.rejects | 14 ++++---- testdata/permute_09.accepts | 29 ++++++++------- testdata/permute_09.lisp | 5 +-- testdata/permute_09.rejects | 12 +++---- testdata/shift_07.accepts | 5 +++ testdata/shift_07.lisp | 8 +++++ testdata/shift_07.rejects | 2 ++ 21 files changed, 213 insertions(+), 192 deletions(-) create mode 100644 pkg/table/printer.go create mode 100644 testdata/shift_07.accepts create mode 100644 testdata/shift_07.lisp create mode 100644 testdata/shift_07.rejects diff --git a/pkg/air/gadgets/bits.go b/pkg/air/gadgets/bits.go index 0b961c0..8e8c131 100644 --- a/pkg/air/gadgets/bits.go +++ b/pkg/air/gadgets/bits.go @@ -52,7 +52,8 @@ func ApplyBitwidthGadget(col string, nbits uint, schema *air.Schema) { // Construct X == (X:0 * 1) + ... + (X:n * 2^n) X := air.NewColumnAccess(col, 0) eq := X.Equate(sum) - schema.AddVanishingConstraint(col, nil, eq) + // Construct column name + schema.AddVanishingConstraint(fmt.Sprintf("%s:u%d", col, nbits), nil, eq) // Finally, add the necessary byte decomposition computation. schema.AddComputation(table.NewByteDecomposition(col, nbits)) } diff --git a/pkg/air/schema.go b/pkg/air/schema.go index 2580d83..4c2a4c1 100644 --- a/pkg/air/schema.go +++ b/pkg/air/schema.go @@ -109,9 +109,9 @@ func (p *Schema) RequiredSpillage() uint { // 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) (bool, *fr.Element) { - value := tr.GetByIndex(j, 0) - return true, value + tr.Pad(n, func(j int) *fr.Element { + // Extract front value to use for padding. + return tr.GetByIndex(j, 0) }) } @@ -179,7 +179,9 @@ func (p *Schema) IsOutputTrace(tr table.Trace) error { // AddColumn appends a new data column which is either synthetic or // not. A synthetic column is one which has been introduced by the // process of lowering from HIR / MIR to AIR. That is, it is not a -// column which was original specified by the user. +// column which was original specified by the user. Columns also support a +// "padding sign", which indicates whether padding should occur at the front +// (positive sign) or the back (negative sign). func (p *Schema) AddColumn(name string, synthetic bool) { // NOTE: the air level has no ability to enforce the type specified for a // given column. diff --git a/pkg/cmd/check.go b/pkg/cmd/check.go index 2bedcd5..f0ba6dc 100644 --- a/pkg/cmd/check.go +++ b/pkg/cmd/check.go @@ -30,6 +30,7 @@ var checkCmd = &cobra.Command{ cfg.mir = getFlag(cmd, "mir") cfg.hir = getFlag(cmd, "hir") cfg.expand = !getFlag(cmd, "raw") + cfg.report = getFlag(cmd, "report") cfg.spillage = getInt(cmd, "spillage") cfg.padding.Right = getUint(cmd, "padding") // TODO: support true ranges @@ -62,6 +63,9 @@ type checkConfig struct { // not required when a "raw" trace is given which already includes all // implied columns. expand bool + // Specifies whether or not to report details of the failure (e.g. for + // debugging purposes). + report bool } // Check a given trace is consistently accepted (or rejected) at the different @@ -87,10 +91,10 @@ func checkTraceWithLowering(tr *table.ArrayTrace, schema *hir.Schema, cfg checkC } func checkTraceWithLoweringHir(tr *table.ArrayTrace, hirSchema *hir.Schema, cfg checkConfig) { - errHIR := checkTrace(tr, hirSchema, cfg) + trHIR, errHIR := checkTrace(tr, hirSchema, cfg) // if errHIR != nil { - reportError(errHIR, "HIR") + reportError("HIR", trHIR, errHIR, cfg) os.Exit(1) } } @@ -99,10 +103,10 @@ func checkTraceWithLoweringMir(tr *table.ArrayTrace, hirSchema *hir.Schema, cfg // Lower HIR => MIR mirSchema := hirSchema.LowerToMir() // Check trace - errMIR := checkTrace(tr, mirSchema, cfg) + trMIR, errMIR := checkTrace(tr, mirSchema, cfg) // if errMIR != nil { - reportError(errMIR, "MIR") + reportError("MIR", trMIR, errMIR, cfg) os.Exit(1) } } @@ -112,10 +116,10 @@ func checkTraceWithLoweringAir(tr *table.ArrayTrace, hirSchema *hir.Schema, cfg mirSchema := hirSchema.LowerToMir() // Lower MIR => AIR airSchema := mirSchema.LowerToAir() - errAIR := checkTrace(tr, airSchema, cfg) + trAIR, errAIR := checkTrace(tr, airSchema, cfg) // if errAIR != nil { - reportError(errAIR, "AIR") + reportError("AIR", trAIR, errAIR, cfg) os.Exit(1) } } @@ -128,9 +132,9 @@ func checkTraceWithLoweringDefault(tr *table.ArrayTrace, hirSchema *hir.Schema, // Lower MIR => AIR airSchema := mirSchema.LowerToAir() // - errHIR := checkTrace(tr, hirSchema, cfg) - errMIR := checkTrace(tr, mirSchema, cfg) - errAIR := checkTrace(tr, airSchema, cfg) + trHIR, errHIR := checkTrace(tr, hirSchema, cfg) + trMIR, errMIR := checkTrace(tr, mirSchema, cfg) + trAIR, errAIR := checkTrace(tr, airSchema, cfg) // if errHIR != nil || errMIR != nil || errAIR != nil { strHIR := toErrorString(errHIR) @@ -140,16 +144,16 @@ func checkTraceWithLoweringDefault(tr *table.ArrayTrace, hirSchema *hir.Schema, if strHIR == strMIR && strMIR == strAIR { fmt.Println(errHIR) } else { - reportError(errHIR, "HIR") - reportError(errMIR, "MIR") - reportError(errAIR, "AIR") + reportError("HIR", trHIR, errHIR, cfg) + reportError("MIR", trMIR, errMIR, cfg) + reportError("AIR", trAIR, errAIR, cfg) } os.Exit(1) } } -func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) error { +func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) (table.Trace, error) { if cfg.expand { // Clone to prevent interefence with subsequent checks tr = tr.Clone() @@ -163,13 +167,13 @@ func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) erro } // Expand trace if err := schema.ExpandTrace(tr); err != nil { - return err + return tr, err } } // Check whether padding requested if cfg.padding.Left == 0 && cfg.padding.Right == 0 { // No padding requested. Therefore, we can avoid a clone in this case. - return schema.Accepts(tr) + return tr, schema.Accepts(tr) } // Apply padding for n := cfg.padding.Left; n <= cfg.padding.Right; n++ { @@ -179,11 +183,11 @@ func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) erro schema.ApplyPadding(n, ptr) // Check whether accepted or not. if err := schema.Accepts(ptr); err != nil { - return err + return ptr, err } } // Done - return nil + return nil, nil } func toErrorString(err error) string { @@ -194,7 +198,11 @@ func toErrorString(err error) string { return err.Error() } -func reportError(err error, ir string) { +func reportError(ir string, tr table.Trace, err error, cfg checkConfig) { + if cfg.report { + table.PrintTrace(tr) + } + if err != nil { fmt.Printf("%s: %s\n", ir, err) } else { @@ -204,6 +212,7 @@ func reportError(err error, ir string) { func init() { rootCmd.AddCommand(checkCmd) + checkCmd.Flags().Bool("report", false, "report details of failure for debugging") checkCmd.Flags().Bool("raw", false, "assume input trace already expanded") checkCmd.Flags().Bool("hir", false, "check at HIR level") checkCmd.Flags().Bool("mir", false, "check at MIR level") diff --git a/pkg/hir/parser.go b/pkg/hir/parser.go index f7dd869..292d08d 100644 --- a/pkg/hir/parser.go +++ b/pkg/hir/parser.go @@ -150,6 +150,10 @@ func (p *hirParser) parseSortedPermutationDeclaration(elements []sexp.SExp) erro if strings.HasPrefix(sortName, "+") { signs[i] = true } else if strings.HasPrefix(sortName, "-") { + if i == 0 { + return p.translator.SyntaxError(source, "sorted permutation requires ascending first column") + } + signs[i] = false } else { return p.translator.SyntaxError(source, "malformed sort direction") diff --git a/pkg/hir/schema.go b/pkg/hir/schema.go index 481e592..5a177c6 100644 --- a/pkg/hir/schema.go +++ b/pkg/hir/schema.go @@ -113,9 +113,8 @@ func (p *Schema) RequiredSpillage() uint { // 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) (bool, *fr.Element) { - value := tr.GetByIndex(j, 0) - return true, value + tr.Pad(n, func(j int) *fr.Element { + return tr.GetByIndex(j, 0) }) } diff --git a/pkg/mir/schema.go b/pkg/mir/schema.go index 831d340..53cf321 100644 --- a/pkg/mir/schema.go +++ b/pkg/mir/schema.go @@ -80,9 +80,8 @@ func (p *Schema) RequiredSpillage() uint { // 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) (bool, *fr.Element) { - value := tr.GetByIndex(j, 0) - return true, value + tr.Pad(n, func(j int) *fr.Element { + return tr.GetByIndex(j, 0) }) } diff --git a/pkg/table/printer.go b/pkg/table/printer.go new file mode 100644 index 0000000..22775d8 --- /dev/null +++ b/pkg/table/printer.go @@ -0,0 +1,71 @@ +package table + +import ( + "fmt" + "unicode/utf8" +) + +// PrintTrace prints a trace in a more human-friendly fashion. +func PrintTrace(tr Trace) { + n := tr.Width() + // + rows := make([][]string, n) + for i := uint(0); i < n; i++ { + rows[i] = traceColumnData(tr, i) + } + // + widths := traceRowWidths(tr.Height(), rows) + // + printHorizontalRule(widths) + // + for _, r := range rows { + printTraceRow(r, widths) + printHorizontalRule(widths) + } +} + +func traceColumnData(tr Trace, col uint) []string { + n := tr.Height() + data := make([]string, n+1) + data[0] = tr.ColumnName(int(col)) + + for row := uint(0); row < n; row++ { + data[row+1] = tr.GetByIndex(int(col), int(row)).String() + } + + return data +} + +func traceRowWidths(height uint, rows [][]string) []int { + widths := make([]int, height+1) + + for _, row := range rows { + for i, col := range row { + w := utf8.RuneCountInString(col) + widths[i] = max(w, widths[i]) + } + } + + return widths +} + +func printTraceRow(row []string, widths []int) { + for i, col := range row { + fmt.Printf(" %*s |", widths[i], col) + } + + fmt.Println() +} + +func printHorizontalRule(widths []int) { + for _, w := range widths { + fmt.Print("-") + + for i := 0; i < w; i++ { + fmt.Print("-") + } + fmt.Print("-+") + } + + fmt.Println() +} diff --git a/pkg/table/trace.go b/pkg/table/trace.go index dbd170e..eed6020 100644 --- a/pkg/table/trace.go +++ b/pkg/table/trace.go @@ -53,11 +53,9 @@ type Trace interface { // does not exist or if the index is out-of-bounds then an // error is returned. GetByIndex(col int, row int) *fr.Element - // Pad each column in this trace with n rows of a given value, either at - // the front (sign=true) or the back (sign=false). An iterator over the - // column signs is provided.Padding is done by duplicating either the first - // (sign=true) or last (sign=false) item of the trace n times. - Pad(n uint, signs func(int) (bool, *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) // Determine the height of this table, which is defined as the // height of the largest column. Height() uint @@ -83,7 +81,7 @@ func ConstraintsAcceptTrace[T Acceptable](trace Trace, constraints []T) error { func FrontPadWithZeros(n uint, tr Trace) { var zero fr.Element = fr.NewElement((0)) // Insert initial padding row - tr.Pad(n, func(index int) (bool, *fr.Element) { return true, &zero }) + tr.Pad(n, func(index int) *fr.Element { return &zero }) } // =================================================================== @@ -227,14 +225,11 @@ func (p *ArrayTrace) Height() uint { return p.height } -// Pad each column in this trace with n items, either at the front -// (sign=true) or the back (sign=false). An iterator over the column signs -// is provided.Padding is done by duplicating either the first (sign=true) -// or last (sign=false) item of the trace n times. -func (p *ArrayTrace) Pad(n uint, signs func(int) (bool, *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. +func (p *ArrayTrace) Pad(n uint, padding func(int) *fr.Element) { for i, c := range p.columns { - sign, value := signs(i) - c.Pad(n, sign, value) + c.Pad(n, padding(i)) } // Increment height p.height += n @@ -313,27 +308,13 @@ 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, sign bool, value *fr.Element) { - // Offset where original data should start - var copy_offset uint - // Offset where padding values should start - var padding_offset uint +func (p *ArrayTraceColumn) Pad(n uint, value *fr.Element) { // Allocate sufficient memory ndata := make([]*fr.Element, uint(len(p.data))+n) - // Check direction of padding - if sign { - // Pad at the front - copy_offset = n - padding_offset = 0 - } else { - // Pad at the back - copy_offset = 0 - padding_offset = uint(len(p.data)) - } // Copy over the data - copy(ndata[copy_offset:], p.data) + copy(ndata[n:], p.data) // Go padding! - for i := padding_offset; i < (n + padding_offset); i++ { + for i := uint(0); i < n; i++ { ndata[i] = value } // Copy over diff --git a/pkg/test/ir_test.go b/pkg/test/ir_test.go index c10e1df..8456427 100644 --- a/pkg/test/ir_test.go +++ b/pkg/test/ir_test.go @@ -7,7 +7,6 @@ import ( "os" "strings" "testing" - "unicode/utf8" "github.com/consensys/go-corset/pkg/hir" "github.com/consensys/go-corset/pkg/table" @@ -126,6 +125,10 @@ func Test_Shift_06(t *testing.T) { Check(t, "shift_06") } +func Test_Shift_07(t *testing.T) { + Check(t, "shift_07") +} + // =================================================================== // Normalisation Tests // =================================================================== @@ -308,7 +311,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 = 1 +const MAX_PADDING uint = 0 // For a given set of constraints, check that all traces which we // expect to be accepted are accepted, and all traces that we expect @@ -508,68 +511,3 @@ func readLine(reader *bufio.Reader) *string { // Done return &str } - -// Prints a trace in a more human-friendly fashion. -func printTrace(tr table.Trace) { - n := tr.Width() - // - rows := make([][]string, n) - for i := uint(0); i < n; i++ { - rows[i] = traceColumnData(tr, i) - } - // - widths := traceRowWidths(tr.Height(), rows) - // - printHorizontalRule(widths) - // - for _, r := range rows { - printTraceRow(r, widths) - printHorizontalRule(widths) - } -} - -func traceColumnData(tr table.Trace, col uint) []string { - n := tr.Height() - data := make([]string, n+1) - data[0] = tr.ColumnName(int(col)) - - for row := uint(0); row < n; row++ { - data[row+1] = tr.GetByIndex(int(col), int(row)).String() - } - - return data -} - -func traceRowWidths(height uint, rows [][]string) []int { - widths := make([]int, height+1) - - for _, row := range rows { - for i, col := range row { - w := utf8.RuneCountInString(col) - widths[i] = max(w, widths[i]) - } - } - - return widths -} - -func printTraceRow(row []string, widths []int) { - for i, col := range row { - fmt.Printf(" %*s |", widths[i], col) - } - - fmt.Println() -} - -func printHorizontalRule(widths []int) { - for _, w := range widths { - fmt.Print("-") - - for i := 0; i < w; i++ { - fmt.Print("-") - } - fmt.Print("-+") - } - - fmt.Println() -} diff --git a/testdata/permute_04.accepts b/testdata/permute_04.accepts index 9306be6..ce04e1e 100644 --- a/testdata/permute_04.accepts +++ b/testdata/permute_04.accepts @@ -1,12 +1,12 @@ -{"X": [5]} -{"X": [0,5]} -{"X": [5,0]} -{"X": [0,1,5]} -{"X": [0,5,1]} -{"X": [5,1,0]} -{"X": [1,0,5]} -{"X": [1,2,3,4,5]} -{"X": [1,2,3,5,4]} -{"X": [1,2,5,4,3]} -{"X": [1,5,3,4,2]} -{"X": [5,2,3,4,1]} +{"ST": [1], "X": [5]} +{"ST": [1,1], "X": [6,5]} +{"ST": [1,1], "X": [5,6]} +{"ST": [1,1,1], "X": [6,7,5]} +{"ST": [1,1,1], "X": [6,5,7]} +{"ST": [1,1,1], "X": [5,7,6]} +{"ST": [1,1,1], "X": [7,6,5]} +{"ST": [1,1,1,1,1], "X": [6,7,8,9,5]} +{"ST": [1,1,1,1,1], "X": [6,7,8,5,9]} +{"ST": [1,1,1,1,1], "X": [6,7,5,9,8]} +{"ST": [1,1,1,1,1], "X": [6,5,8,9,7]} +{"ST": [1,1,1,1,1], "X": [5,7,8,9,6]} diff --git a/testdata/permute_04.lisp b/testdata/permute_04.lisp index 35f92dd..f84c48c 100644 --- a/testdata/permute_04.lisp +++ b/testdata/permute_04.lisp @@ -1,3 +1,4 @@ +(column ST :u16) (column X :u16) -(permute (Y) (-X)) -(vanish:first last-row (- Y 5)) +(permute (ST' Y) (+ST -X)) +(vanish:last first-row (- Y 5)) diff --git a/testdata/permute_04.rejects b/testdata/permute_04.rejects index e5cc1eb..74fda2a 100644 --- a/testdata/permute_04.rejects +++ b/testdata/permute_04.rejects @@ -1,5 +1,5 @@ -{"X": [-1]} -{"X": [255]} -{"X": [1234987]} -{"X": [1,2,3]} -{"X": [3,44,235,623,1,35]} +{"ST": [1], "X": [-1]} +{"ST": [1], "X": [255]} +{"ST": [1], "X": [1234987]} +{"ST": [1,1,1], "X": [1,2,3]} +{"ST": [1,1,1,1,1,1], "X": [3,44,235,623,1,35]} diff --git a/testdata/permute_07.accepts b/testdata/permute_07.accepts index 9b9d829..9474bf1 100644 --- a/testdata/permute_07.accepts +++ b/testdata/permute_07.accepts @@ -1,16 +1,16 @@ -{"X": [], "Y": []} -{"X": [0], "Y": [0]} -{"X": [1], "Y": [0]} -{"X": [0], "Y": [1]} -{"X": [2], "Y": [0]} -;; n=2 -{"X": [0,0], "Y": [0,0]} -{"X": [1,0], "Y": [0,1]} -{"X": [2,1], "Y": [1,0]} -{"X": [2,0], "Y": [0,1]} +{"ST": [], "X": [], "Y": []} +{"ST": [1], "X": [1], "Y": [1]} +{"ST": [1], "X": [2], "Y": [1]} +{"ST": [1], "X": [1], "Y": [2]} +{"ST": [1], "X": [3], "Y": [1]} ;; n=3 -{"X": [0,0,0], "Y": [0,0,0]} -{"X": [3,1,4], "Y": [1,0,3]} -{"X": [3,0,1], "Y": [1,1,0]} -{"X": [3,0,1], "Y": [1,1,0]} -{"X": [5,2,3], "Y": [3,0,2]} +{"ST": [1,1], "X": [1,1], "Y": [1,1]} +{"ST": [1,1], "X": [2,1], "Y": [1,2]} +{"ST": [1,1], "X": [3,2], "Y": [2,1]} +{"ST": [1,1], "X": [3,1], "Y": [1,2]} +;; n=3 +{"ST": [1,1,1], "X": [1,1,1], "Y": [1,1,1]} +{"ST": [1,1,1], "X": [4,2,5], "Y": [2,1,4]} +{"ST": [1,1,1], "X": [4,1,2], "Y": [2,2,1]} +{"ST": [1,1,1], "X": [4,1,2], "Y": [2,2,1]} +{"ST": [1,1,1], "X": [6,3,4], "Y": [4,1,3]} diff --git a/testdata/permute_07.lisp b/testdata/permute_07.lisp index 02e693c..cd8c231 100644 --- a/testdata/permute_07.lisp +++ b/testdata/permute_07.lisp @@ -1,4 +1,5 @@ +(column ST :u16) (column X :u16) (column Y :u16) -(permute (A B) (-X +Y)) -(vanish diag_ab (- (shift A 1) B)) +(permute (ST' A B) (+ST -X +Y)) +(vanish diag_ab (* ST' (- (shift A 1) B))) diff --git a/testdata/permute_07.rejects b/testdata/permute_07.rejects index 42eb25a..b1b72c5 100644 --- a/testdata/permute_07.rejects +++ b/testdata/permute_07.rejects @@ -1,7 +1,7 @@ -{"X": [0,0], "Y": [1,1]} -{"X": [1,2], "Y": [1,0]} -{"X": [1,1], "Y": [1,0]} -{"X": [0,3,2], "Y": [0,0,0]} -{"X": [0,3,2], "Y": [3,0,2]} -{"X": [0,3,2], "Y": [3,1,2]} -{"X": [0,3,2], "Y": [3,2,2]} +{"ST": [1,1], "X": [0,0], "Y": [1,1]} +{"ST": [1,1], "X": [1,2], "Y": [1,0]} +{"ST": [1,1], "X": [1,1], "Y": [1,0]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [0,0,0]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [3,0,2]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [3,1,2]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [3,2,2]} diff --git a/testdata/permute_09.accepts b/testdata/permute_09.accepts index 5b3ae2b..394cd0a 100644 --- a/testdata/permute_09.accepts +++ b/testdata/permute_09.accepts @@ -1,17 +1,16 @@ -{"X": [], "Y": []} -{"X": [0], "Y": [0]} -{"X": [1], "Y": [0]} +{"ST": [], "X": [], "Y": []} +{"ST": [1], "X": [0], "Y": [0]} +{"ST": [1], "X": [1], "Y": [0]} ;; n=2 -{"X": [0,0], "Y": [0,0]} -{"X": [2,1], "Y": [1,0]} -{"X": [3,2], "Y": [2,0]} -{"X": [2,3], "Y": [0,2]} -{"X": [2,2], "Y": [0,2]} -{"X": [2,1], "Y": [1,0]} -{"X": [2,2], "Y": [2,0]} +{"ST": [1,1], "X": [0,0], "Y": [0,0]} +{"ST": [1,1], "X": [2,1], "Y": [1,0]} +{"ST": [1,1], "X": [3,2], "Y": [2,0]} +{"ST": [1,1], "X": [2,3], "Y": [0,2]} +{"ST": [1,1], "X": [2,2], "Y": [0,2]} +{"ST": [1,1], "X": [2,1], "Y": [1,0]} +{"ST": [1,1], "X": [2,2], "Y": [2,0]} ;; n=3 -{"X": [0,0,0], "Y": [0,0,0]} -;; -{"X": [3,1,2], "Y": [2,0,1]} -{"X": [3,1,2], "Y": [2,0,1]} -{"X": [2,2,1], "Y": [1,2,0]} +{"ST": [1,1,1], "X": [0,0,0], "Y": [0,0,0]} +{"ST": [1,1,1], "X": [3,1,2], "Y": [2,0,1]} +{"ST": [1,1,1], "X": [3,1,2], "Y": [2,0,1]} +{"ST": [1,1,1], "X": [2,2,1], "Y": [1,2,0]} diff --git a/testdata/permute_09.lisp b/testdata/permute_09.lisp index 0b4df1d..330a4f5 100644 --- a/testdata/permute_09.lisp +++ b/testdata/permute_09.lisp @@ -1,4 +1,5 @@ +(column ST :u16) (column X :u16) (column Y :u16) -(permute (A B) (-X -Y)) -(vanish diag_ab (- (shift A 1) B)) +(permute (ST' A B) (+ST -X -Y)) +(vanish diag_ab (* ST' (- (shift A 1) B))) diff --git a/testdata/permute_09.rejects b/testdata/permute_09.rejects index 9ff18f5..adb6824 100644 --- a/testdata/permute_09.rejects +++ b/testdata/permute_09.rejects @@ -1,6 +1,6 @@ -{"X": [0,0], "Y": [1,1]} -{"X": [1,2], "Y": [1,0]} -{"X": [0,3,2], "Y": [0,0,0]} -{"X": [0,3,2], "Y": [3,0,2]} -{"X": [0,3,2], "Y": [3,1,2]} -{"X": [0,3,2], "Y": [3,2,2]} +{"ST": [1,1], "X": [0,0], "Y": [1,1]} +{"ST": [1,1], "X": [1,2], "Y": [1,0]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [0,0,0]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [3,0,2]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [3,1,2]} +{"ST": [1,1,1], "X": [0,3,2], "Y": [3,2,2]} diff --git a/testdata/shift_07.accepts b/testdata/shift_07.accepts new file mode 100644 index 0000000..2a86f0c --- /dev/null +++ b/testdata/shift_07.accepts @@ -0,0 +1,5 @@ +{"BIT_1": [], "ARG": []} +{"BIT_1": [0], "ARG": [0]} +{"BIT_1": [0], "ARG": [1]} +{"BIT_1": [0], "ARG": [2]} +{"BIT_1": [0,1], "ARG": [2,0]} diff --git a/testdata/shift_07.lisp b/testdata/shift_07.lisp new file mode 100644 index 0000000..6e4bf8d --- /dev/null +++ b/testdata/shift_07.lisp @@ -0,0 +1,8 @@ +(column BIT_1 :u1) +(column ARG) + +(vanish pivot + ;; If BIT_1[k-1]=0 and BIT_1[k]=1 + (if (+ (shift BIT_1 -1) (- 1 BIT_1)) + ;; Then ARG = 0 + ARG)) diff --git a/testdata/shift_07.rejects b/testdata/shift_07.rejects new file mode 100644 index 0000000..4e7d29f --- /dev/null +++ b/testdata/shift_07.rejects @@ -0,0 +1,2 @@ +{"BIT_1": [1], "ARG": [1]} +{"BIT_1": [0,1], "ARG": [2,1]}