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

@@ -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))
 }

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.

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")

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")

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)
 	})
 }
 

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)
 	})
 }
 

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()
+}

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