Report generation for vanishing constraints

This puts in place report generation for vanishing constraints.

pkg/cmd/check.go

@@ -8,7 +8,8 @@ import (
 
 	"github.com/consensys/go-corset/pkg/hir"
 	sc "github.com/consensys/go-corset/pkg/schema"
-	"github.com/consensys/go-corset/pkg/trace"
+	"github.com/consensys/go-corset/pkg/schema/constraint"
+	tr "github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 	log "github.com/sirupsen/logrus"
 	"github.com/spf13/cobra"
@@ -45,6 +46,7 @@ var checkCmd = &cobra.Command{
 		cfg.padding.Right = getUint(cmd, "padding")
 		cfg.parallelExpansion = !getFlag(cmd, "sequential")
 		cfg.batchSize = getUint(cmd, "batch")
+		cfg.ansiEscapes = getFlag(cmd, "ansi-escapes")
 		//
 		stats := util.NewPerfStats()
 		// TODO: support true ranges
@@ -94,11 +96,13 @@ type checkConfig struct {
 	parallelExpansion bool
 	// Size of constraint batches to execute in parallel
 	batchSize uint
+	// Enable ansi escape codes in reports
+	ansiEscapes bool
 }
 
 // Check a given trace is consistently accepted (or rejected) at the different
 // IR levels.
-func checkTraceWithLowering(cols []trace.RawColumn, schema *hir.Schema, cfg checkConfig) bool {
+func checkTraceWithLowering(cols []tr.RawColumn, schema *hir.Schema, cfg checkConfig) bool {
 	hir := cfg.hir
 	mir := cfg.mir
 	air := cfg.air
@@ -117,43 +121,43 @@ func checkTraceWithLowering(cols []trace.RawColumn, schema *hir.Schema, cfg chec
 	}
 
 	if mir {
-		res = res && checkTrace("MIR", cols, schema.LowerToMir(), cfg)
+		res = checkTrace("MIR", cols, schema.LowerToMir(), cfg) && res
 	}
 
 	if air {
-		res = res && checkTrace("AIR", cols, schema.LowerToMir().LowerToAir(), cfg)
+		res = checkTrace("AIR", cols, schema.LowerToMir().LowerToAir(), cfg) && res
 	}
 
 	return res
 }
 
-func checkTrace(ir string, cols []trace.RawColumn, schema sc.Schema, cfg checkConfig) bool {
+func checkTrace(ir string, cols []tr.RawColumn, schema sc.Schema, cfg checkConfig) bool {
 	builder := sc.NewTraceBuilder(schema).Expand(cfg.expand).Parallel(cfg.parallelExpansion)
 	//
 	for n := cfg.padding.Left; n <= cfg.padding.Right; n++ {
 		stats := util.NewPerfStats()
-		tr, errs := builder.Padding(n).Build(cols)
+		trace, errs := builder.Padding(n).Build(cols)
 
 		stats.Log("Expanding trace columns")
 		// Report any errors
 		reportErrors(cfg.strict, ir, errs)
 		// Check whether considered unrecoverable
-		if tr == nil || (cfg.strict && len(errs) > 0) {
+		if trace == nil || (cfg.strict && len(errs) > 0) {
 			return false
 		}
-		// Validate trace.
+		// Validate trace
 		stats = util.NewPerfStats()
 		//
-		if err := validationCheck(tr, schema); err != nil {
+		if err := validationCheck(trace, schema); err != nil {
 			reportErrors(true, ir, []error{err})
 			return false
 		}
-		// Check trace.
+		// Check trace
 		stats.Log("Validating trace")
 		stats = util.NewPerfStats()
 		//
-		if errs := sc.Accepts(cfg.batchSize, schema, tr); len(errs) > 0 {
-			reportFailures(ir, errs)
+		if errs := sc.Accepts(cfg.batchSize, schema, trace); len(errs) > 0 {
+			reportFailures(ir, errs, trace, cfg)
 			return false
 		}
 
@@ -165,7 +169,7 @@ func checkTrace(ir string, cols []trace.RawColumn, schema sc.Schema, cfg checkCo
 
 // Validate that values held in trace columns match the expected type.  This is
 // really a sanity check that the trace is not malformed.
-func validationCheck(tr trace.Trace, schema sc.Schema) error {
+func validationCheck(tr tr.Trace, schema sc.Schema) error {
 	var err error
 
 	schemaCols := schema.Columns()
@@ -199,11 +203,11 @@ func validationCheck(tr trace.Trace, schema sc.Schema) error {
 }
 
 // Validate that all elements of a given column are within the given type.
-func validateColumn(colType sc.Type, col trace.Column, mod sc.Module) error {
+func validateColumn(colType sc.Type, col tr.Column, mod sc.Module) error {
 	for j := 0; j < int(col.Data().Len()); j++ {
 		jth := col.Get(j)
 		if !colType.Accept(jth) {
-			qualColName := trace.QualifiedColumnName(mod.Name(), col.Name())
+			qualColName := tr.QualifiedColumnName(mod.Name(), col.Name())
 			return fmt.Errorf("row %d of column %s is out-of-bounds (%s)", j, qualColName, jth.String())
 		}
 	}
@@ -212,13 +216,60 @@ func validateColumn(colType sc.Type, col trace.Column, mod sc.Module) error {
 }
 
 // Report constraint failures, whilst providing contextual information (when requested).
-func reportFailures(ir string, failures []sc.Failure) {
+func reportFailures(ir string, failures []sc.Failure, trace tr.Trace, cfg checkConfig) {
 	errs := make([]error, len(failures))
 	for i, f := range failures {
 		errs[i] = errors.New(f.Message())
 	}
-
+	// First, log errors
 	reportErrors(true, ir, errs)
+	// Second, produce report (if requested)
+	if cfg.report {
+		for _, f := range failures {
+			reportFailure(f, trace, cfg)
+		}
+	}
+}
+
+// Print a human-readable report detailing the given failure
+func reportFailure(failure sc.Failure, trace tr.Trace, cfg checkConfig) {
+	if f, ok := failure.(*constraint.VanishingFailure); ok {
+		reportVanishingFailure(f, trace, cfg)
+	}
+}
+
+// Print a human-readable report detailing the given failure with a vanishing constraint.
+func reportVanishingFailure(failure *constraint.VanishingFailure, trace tr.Trace, cfg checkConfig) {
+	var start uint = math.MaxUint
+	// Determine all (input) cells involved in evaluating the given constraint
+	cells := failure.RequiredCells(trace)
+	end := uint(0)
+	// Determine row bounds
+	for _, c := range cells.ToArray() {
+		start = min(start, uint(c.Row))
+		end = max(end, uint(c.Row))
+	}
+	// Determine columns to show
+	cols := util.NewSortedSet[uint]()
+	for _, c := range cells.ToArray() {
+		cols.Insert(c.Column)
+	}
+	// Construct & configure printer
+	tp := tr.NewPrinter().Start(start).End(end).MaxCellWidth(16)
+	// Determine whether to enable ANSI escapes (e.g. for colour in the terminal)
+	tp = tp.AnsiEscapes(cfg.ansiEscapes)
+	// Filter out columns not used in evaluating the constraint.
+	tp = tp.Columns(func(col uint, trace tr.Trace) bool {
+		return cols.Contains(col)
+	})
+	// Highlight failing cells
+	tp = tp.Highlight(func(cell tr.CellRef, trace tr.Trace) bool {
+		return cells.Contains(cell)
+	})
+	// Print out report
+	fmt.Printf("failing constraint %s:\n", failure.Handle())
+	tp.Print(trace)
+	fmt.Println()
 }
 
 func reportErrors(error bool, ir string, errs []error) {
@@ -255,4 +306,5 @@ func init() {
 	checkCmd.Flags().UintP("batch", "b", math.MaxUint, "specify batch size for constraint checking")
 	checkCmd.Flags().Int("spillage", -1,
 		"specify amount of splillage to account for (where -1 indicates this should be inferred)")
+	checkCmd.Flags().Bool("ansi-escapes", true, "specify whether to allow ANSI escapes or not (e.g. for colour reports)")
 }

pkg/cmd/debug.go

@@ -109,7 +109,7 @@ func printStats(hirSchema *hir.Schema, hir bool, mir bool, air bool) {
 		tbl.SetRow(i, row...)
 	}
 	//
-	tbl.SetMaxWidth(64)
+	tbl.SetMaxWidths(64)
 	tbl.Print()
 }
 

pkg/cmd/trace.go

@@ -102,7 +102,7 @@ func printTrace(start uint, end uint, max_width uint, cols []trace.RawColumn) {
 		}
 	}
 	//
-	tbl.SetMaxWidth(max_width)
+	tbl.SetMaxWidths(max_width)
 	tbl.Print()
 }
 
@@ -122,7 +122,7 @@ func listColumns(tr []trace.RawColumn) {
 		tbl.SetRow(i, row...)
 	}
 	//
-	tbl.SetMaxWidth(64)
+	tbl.SetMaxWidths(64)
 	tbl.Print()
 }
 
@@ -136,7 +136,7 @@ func summaryStats(tr []trace.RawColumn) {
 		tbl.SetRow(i, ith.name, summary)
 	}
 	//
-	tbl.SetMaxWidth(64)
+	tbl.SetMaxWidths(64)
 	tbl.Print()
 }
 

pkg/schema/constraint/vanishing.go

@@ -5,7 +5,7 @@ import (
 
 	"github.com/consensys/go-corset/pkg/schema"
 	sc "github.com/consensys/go-corset/pkg/schema"
-	"github.com/consensys/go-corset/pkg/trace"
+	tr "github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 )
 
@@ -18,7 +18,7 @@ type ZeroTest[E sc.Evaluable] struct {
 
 // TestAt determines whether or not a given expression evaluates to zero.
 // Observe that if the expression is undefined, then it is assumed not to hold.
-func (p ZeroTest[E]) TestAt(row int, tr trace.Trace) bool {
+func (p ZeroTest[E]) TestAt(row int, tr tr.Trace) bool {
 	val := p.Expr.EvalAt(row, tr)
 	return val.IsZero()
 }
@@ -30,7 +30,7 @@ func (p ZeroTest[E]) Bounds() util.Bounds {
 
 // Context determines the evaluation context (i.e. enclosing module) for this
 // expression.
-func (p ZeroTest[E]) Context(schema sc.Schema) trace.Context {
+func (p ZeroTest[E]) Context(schema sc.Schema) tr.Context {
 	return p.Expr.Context(schema)
 }
 
@@ -43,7 +43,7 @@ func (p ZeroTest[E]) RequiredColumns() *util.SortedSet[uint] {
 
 // RequiredCells returns the set of trace cells on which evaluation of this
 // constraint element depends.
-func (p ZeroTest[E]) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace.CellRef] {
+func (p ZeroTest[E]) RequiredCells(row int, tr tr.Trace) *util.AnySortedSet[tr.CellRef] {
 	return p.Expr.RequiredCells(row, tr)
 }
 
@@ -58,11 +58,16 @@ func (p ZeroTest[E]) String() string {
 type VanishingFailure struct {
 	// Handle of the failing constraint
 	handle string
+	// Constraint expression
+	constraint sc.Testable
 	// Row on which the constraint failed
 	row uint
-	// Cells used by the failing constraint.  This is useful for providing a
-	// detailed report including the values of relevant cells.
-	cells []trace.CellRef
+}
+
+// Handle returns the handle of this constraint
+func (p *VanishingFailure) Handle() string {
+	// Construct useful error message
+	return p.handle
 }
 
 // Message provides a suitable error message
@@ -71,6 +76,21 @@ func (p *VanishingFailure) Message() string {
 	return fmt.Sprintf("constraint \"%s\" does not hold (row %d)", p.handle, p.row)
 }
 
+// Constraint returns the constraint expression itself.
+func (p *VanishingFailure) Constraint() sc.Testable {
+	return p.constraint
+}
+
+// Row identifies the row on which this constraint failed.
+func (p *VanishingFailure) Row() uint {
+	return p.row
+}
+
+// RequiredCells identifies the cells required to evaluate the failing constraint at the failing row.
+func (p *VanishingFailure) RequiredCells(trace tr.Trace) *util.AnySortedSet[tr.CellRef] {
+	return p.constraint.RequiredCells(int(p.row), trace)
+}
+
 func (p *VanishingFailure) String() string {
 	return p.Message()
 }
@@ -87,7 +107,7 @@ type VanishingConstraint[T sc.Testable] struct {
 	handle string
 	// Evaluation context for this constraint which must match that of the
 	// constrained expression itself.
-	context trace.Context
+	context tr.Context
 	// Indicates (when nil) a global constraint that applies to all rows.
 	// Otherwise, indicates a local constraint which applies to the specific row
 	// given here.
@@ -98,7 +118,7 @@ type VanishingConstraint[T sc.Testable] struct {
 }
 
 // NewVanishingConstraint constructs a new vanishing constraint!
-func NewVanishingConstraint[T sc.Testable](handle string, context trace.Context,
+func NewVanishingConstraint[T sc.Testable](handle string, context tr.Context,
 	domain *int, constraint T) *VanishingConstraint[T] {
 	return &VanishingConstraint[T]{handle, context, domain, constraint}
 }
@@ -124,15 +144,15 @@ func (p *VanishingConstraint[T]) Domain() *int {
 
 // Context returns the evaluation context for this constraint.  Every constraint
 // must be situated within exactly one module in order to be well-formed.
-func (p *VanishingConstraint[T]) Context() trace.Context {
+func (p *VanishingConstraint[T]) Context() tr.Context {
 	return p.context
 }
 
 // Accepts checks whether a vanishing constraint evaluates to zero on every row
 // of a table.  If so, return nil otherwise return an error.
 //
 //nolint:revive
-func (p *VanishingConstraint[T]) Accepts(tr trace.Trace) schema.Failure {
+func (p *VanishingConstraint[T]) Accepts(tr tr.Trace) schema.Failure {
 	if p.domain == nil {
 		// Global Constraint
 		return HoldsGlobally(p.handle, p.context, p.constraint, tr)
@@ -154,7 +174,7 @@ func (p *VanishingConstraint[T]) Accepts(tr trace.Trace) schema.Failure {
 
 // 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 sc.Testable](handle string, ctx trace.Context, constraint T, tr trace.Trace) schema.Failure {
+func HoldsGlobally[T sc.Testable](handle string, ctx tr.Context, constraint T, tr tr.Trace) schema.Failure {
 	// Determine height of enclosing module
 	height := tr.Height(ctx)
 	// Determine well-definedness bounds for this constraint
@@ -174,13 +194,11 @@ func HoldsGlobally[T sc.Testable](handle string, ctx trace.Context, constraint T
 
 // HoldsLocally checks whether a given constraint holds (e.g. vanishes) on a
 // specific row of a trace. If not, report an appropriate error.
-func HoldsLocally[T sc.Testable](k uint, handle string, constraint T, tr trace.Trace) schema.Failure {
+func HoldsLocally[T sc.Testable](k uint, handle string, constraint T, tr tr.Trace) schema.Failure {
 	// Check whether it holds or not
 	if !constraint.TestAt(int(k), tr) {
-		//cells := constraint.RequiredCells(int(k), tr).ToArray()
-		cells := make([]trace.CellRef, 0)
 		// Evaluation failure
-		return &VanishingFailure{handle, k, cells}
+		return &VanishingFailure{handle, constraint, k}
 	}
 	// Success
 	return nil