feat: Support Summary Information for debug Command

pkg/air/expr.go

@@ -185,7 +185,7 @@ type ColumnAccess struct {
 
 // NewColumnAccess constructs an AIR expression representing the value of a given
 // column on the current row.
-func NewColumnAccess(column uint, shift int) Expr {
+func NewColumnAccess(column uint, shift int) *ColumnAccess {
 	return &ColumnAccess{column, shift}
 }
 

pkg/air/schema.go

@@ -14,11 +14,14 @@ import (
 // DataColumn captures the essence of a data column at AIR level.
 type DataColumn = *assignment.DataColumn
 
-// LookupConstraint captures the essence of a lookup constraint at the HIR
+// LookupConstraint captures the essence of a lookup constraint at the AIR
 // level.  At the AIR level, lookup constraints are only permitted between
 // columns (i.e. not arbitrary expressions).
 type LookupConstraint = *constraint.LookupConstraint[*ColumnAccess]
 
+// VanishingConstraint captures the essence of a vanishing constraint at the AIR level.
+type VanishingConstraint = *constraint.VanishingConstraint[constraint.ZeroTest[Expr]]
+
 // PropertyAssertion captures the notion of an arbitrary property which should
 // hold for all acceptable traces.  However, such a property is not enforced by
 // the prover.
@@ -95,16 +98,17 @@ func (p *Schema) AddLookupConstraint(handle string, source trace.Context,
 	}
 	// TODO: sanity source columns are in the same module, and likewise target
 	// columns (though they don't have to be in the same column together).
-	from := make([]Expr, len(sources))
-	into := make([]Expr, len(targets))
+	from := make([]*ColumnAccess, len(sources))
+	into := make([]*ColumnAccess, len(targets))
 	// Construct column accesses from column indices.
 	for i := 0; i < len(from); i++ {
 		from[i] = NewColumnAccess(sources[i], 0)
 		into[i] = NewColumnAccess(targets[i], 0)
 	}
-	//
-	p.constraints = append(p.constraints,
-		constraint.NewLookupConstraint(handle, source, target, from, into))
+	// Construct lookup constraint
+	var lookup LookupConstraint = constraint.NewLookupConstraint(handle, source, target, from, into)
+	// Add
+	p.constraints = append(p.constraints, lookup)
 }
 
 // AddPermutationConstraint appends a new permutation constraint which

pkg/cmd/debug.go

@@ -4,7 +4,13 @@ import (
 	"fmt"
 	"os"
 
+	"github.com/consensys/go-corset/pkg/air"
+	"github.com/consensys/go-corset/pkg/hir"
+	"github.com/consensys/go-corset/pkg/mir"
 	"github.com/consensys/go-corset/pkg/schema"
+	"github.com/consensys/go-corset/pkg/schema/assignment"
+	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/util"
 	"github.com/spf13/cobra"
 )
 
@@ -22,23 +28,44 @@ var debugCmd = &cobra.Command{
 		hir := getFlag(cmd, "hir")
 		mir := getFlag(cmd, "mir")
 		air := getFlag(cmd, "air")
+		stats := getFlag(cmd, "stats")
 		// Parse constraints
 		hirSchema := readSchemaFile(args[0])
-		mirSchema := hirSchema.LowerToMir()
-		airSchema := mirSchema.LowerToAir()
+
 		// Print constraints
-		if hir {
-			printSchema(hirSchema)
-		}
-		if mir {
-			printSchema(mirSchema)
-		}
-		if air {
-			printSchema(airSchema)
+		if stats {
+			printStats(hirSchema, hir, mir, air)
+		} else {
+			printSchemas(hirSchema, hir, mir, air)
 		}
 	},
 }
 
+func init() {
+	rootCmd.AddCommand(debugCmd)
+	debugCmd.Flags().Bool("hir", false, "Print constraints at HIR level")
+	debugCmd.Flags().Bool("mir", false, "Print constraints at MIR level")
+	debugCmd.Flags().Bool("air", false, "Print constraints at AIR level")
+	debugCmd.Flags().Bool("stats", false, "Print summary information")
+}
+
+func printSchemas(hirSchema *hir.Schema, hir bool, mir bool, air bool) {
+	mirSchema := hirSchema.LowerToMir()
+	airSchema := mirSchema.LowerToAir()
+
+	if hir {
+		printSchema(airSchema)
+	}
+
+	if mir {
+		printSchema(airSchema)
+	}
+
+	if air {
+		printSchema(airSchema)
+	}
+}
+
 // Print out all declarations included in a given
 func printSchema(schema schema.Schema) {
 	for i := schema.Declarations(); i.HasNext(); {
@@ -50,9 +77,149 @@ func printSchema(schema schema.Schema) {
 	}
 }
 
-func init() {
-	rootCmd.AddCommand(debugCmd)
-	debugCmd.Flags().Bool("hir", false, "Print constraints at HIR level")
-	debugCmd.Flags().Bool("mir", false, "Print constraints at MIR level")
-	debugCmd.Flags().Bool("air", false, "Print constraints at AIR level")
+func printStats(hirSchema *hir.Schema, hir bool, mir bool, air bool) {
+	schemas := make([]schema.Schema, 0)
+	mirSchema := hirSchema.LowerToMir()
+	airSchema := mirSchema.LowerToAir()
+	// Construct columns
+	if hir {
+		schemas = append(schemas, hirSchema)
+	}
+
+	if mir {
+		schemas = append(schemas, mirSchema)
+	}
+
+	if air {
+		schemas = append(schemas, airSchema)
+	}
+	//
+	n := 1 + uint(len(schemas))
+	m := uint(len(schemaSummarisers))
+	tbl := util.NewTablePrinter(n, m)
+	// Go!
+	for i := uint(0); i < m; i++ {
+		ith := schemaSummarisers[i]
+		row := make([]string, n)
+		row[0] = ith.name
+
+		for j := 0; j < len(schemas); j++ {
+			row[j+1] = ith.summary(schemas[j])
+		}
+		tbl.SetRow(i, row...)
+	}
+	//
+	tbl.SetMaxWidth(64)
+	tbl.Print()
+}
+
+// ============================================================================
+// Schema Summarisers
+// ============================================================================
+
+type schemaSummariser struct {
+	name    string
+	summary func(schema.Schema) string
+}
+
+var schemaSummarisers []schemaSummariser = []schemaSummariser{
+	// Constraints
+	{"Constraints", vanishingSummariser},
+	{"Lookups", lookupSummariser},
+	{"Permutations", constraintSummariser[*constraint.PermutationConstraint]},
+	{"Types", constraintSummariser[*constraint.TypeConstraint]},
+	{"Ranges", constraintSummariser[*constraint.RangeConstraint]},
+	// Assignments
+	{"Decomposition", assignmentSummariser[*assignment.ByteDecomposition]},
+	{"Computed Columns", computedColumnSummariser},
+	{"Committed Columns", assignmentSummariser[*assignment.DataColumn]},
+	{"Sorted Permutations", assignmentSummariser[*assignment.SortedPermutation]},
+	{"Interleave", assignmentSummariser[*assignment.Interleaving]},
+	{"Lexicographic Sort", assignmentSummariser[*assignment.LexicographicSort]},
+	// Column Width
+	columnWidthSummariser(1, 1),
+	columnWidthSummariser(2, 4),
+	columnWidthSummariser(5, 8),
+	columnWidthSummariser(9, 16),
+	columnWidthSummariser(17, 32),
+	columnWidthSummariser(33, 64),
+	columnWidthSummariser(65, 128),
+	columnWidthSummariser(129, 256),
+}
+
+func vanishingSummariser(sc schema.Schema) string {
+	count := constraintCounter[air.VanishingConstraint](sc)
+	count += constraintCounter[mir.VanishingConstraint](sc)
+	count += constraintCounter[hir.VanishingConstraint](sc)
+
+	return fmt.Sprintf("%d", count)
+}
+
+func lookupSummariser(sc schema.Schema) string {
+	count := constraintCounter[air.LookupConstraint](sc)
+	count += constraintCounter[mir.LookupConstraint](sc)
+	count += constraintCounter[hir.LookupConstraint](sc)
+
+	return fmt.Sprintf("%d", count)
+}
+
+func constraintSummariser[T any](sc schema.Schema) string {
+	count := constraintCounter[T](sc)
+	return fmt.Sprintf("%d", count)
+}
+
+func constraintCounter[T any](sc schema.Schema) int {
+	count := 0
+
+	for c := sc.Constraints(); c.HasNext(); {
+		ith := c.Next()
+		if _, ok := ith.(T); ok {
+			count++
+		}
+	}
+
+	return count
+}
+
+func computedColumnSummariser(sc schema.Schema) string {
+	count := assignmentCounter[*assignment.ComputedColumn[air.Expr]](sc)
+	count += assignmentCounter[*assignment.ComputedColumn[mir.Expr]](sc)
+	count += assignmentCounter[*assignment.ComputedColumn[mir.Expr]](sc)
+
+	return fmt.Sprintf("%d", count)
+}
+
+func assignmentSummariser[T any](sc schema.Schema) string {
+	count := assignmentCounter[T](sc)
+	return fmt.Sprintf("%d", count)
+}
+
+func assignmentCounter[T any](sc schema.Schema) int {
+	count := 0
+
+	for c := sc.Declarations(); c.HasNext(); {
+		ith := c.Next()
+		if _, ok := ith.(T); ok {
+			count++
+		}
+	}
+
+	return count
+}
+
+func columnWidthSummariser(lowWidth uint, highWidth uint) schemaSummariser {
+	return schemaSummariser{
+		name: fmt.Sprintf("Columns (%d..%d bits)", lowWidth, highWidth),
+		summary: func(sc schema.Schema) string {
+			count := 0
+			for i := sc.Columns(); i.HasNext(); {
+				ith := i.Next()
+				ithWidth := ith.Type().BitWidth()
+				if ithWidth >= lowWidth && ithWidth <= highWidth {
+					count++
+				}
+			}
+			return fmt.Sprintf("%d", count)
+		},
+	}
 }

pkg/cmd/trace.go

@@ -134,7 +134,7 @@ func printTrace(start uint, end uint, max_width uint, tr trace.Trace) {
 
 func listColumns(tr trace.Trace) {
 	// Determine number of columns
-	m := 1 + uint(len(summarisers))
+	m := 1 + uint(len(colSummarisers))
 	// Determine number of rows
 	n := tr.Columns().Len()
 	// Go!
@@ -145,8 +145,8 @@ func listColumns(tr trace.Trace) {
 		row := make([]string, m)
 		row[0] = QualifiedColumnName(i, tr)
 		// Add summarises
-		for j := 0; j < len(summarisers); j++ {
-			row[j+1] = summarisers[j].summary(ith)
+		for j := 0; j < len(colSummarisers); j++ {
+			row[j+1] = colSummarisers[j].summary(ith)
 		}
 		tbl.SetRow(i, row...)
 	}
@@ -180,7 +180,7 @@ type ColSummariser struct {
 	summary func(trace.Column) string
 }
 
-var summarisers []ColSummariser = []ColSummariser{
+var colSummarisers []ColSummariser = []ColSummariser{
 	{"count", rowSummariser},
 	{"width", widthSummariser},
 	{"bytes", bytesSummariser},

pkg/schema/type.go

@@ -14,17 +14,15 @@ type Type interface {
 	// AsUint accesses this type as an unsigned integer.  If this type is not an
 	// unsigned integer, then this returns nil.
 	AsUint() *UintType
-
 	// AsField accesses this type as a field element.  If this type is not a
 	// field element, then this returns nil.
 	AsField() *FieldType
-
 	// Accept checks whether a specific value is accepted by this type
 	Accept(*fr.Element) bool
-
 	// Return the number of bytes required represent any element of this type.
 	ByteWidth() uint
-
+	// Return the minimum number of bits required represent any element of this type.
+	BitWidth() uint
 	// Produce a string representation of this type.
 	String() string
 }
@@ -126,6 +124,12 @@ func (p *FieldType) ByteWidth() uint {
 	return 32
 }
 
+// BitWidth returns the bitwidth of this type.  For example, the
+// bitwidth of the type u8 is 8.
+func (p *FieldType) BitWidth() uint {
+	return p.ByteWidth() * 8
+}
+
 // Accept determines whether a given value is an element of this type.  In
 // fact, all field elements are members of this type.
 func (p *FieldType) Accept(val *fr.Element) bool {