From 0fb958ad541548aedad1aab06e7a838aa2832f4c Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 22 Jul 2024 17:47:00 +1200 Subject: [PATCH] Support summary information for `debug` command This implements a relatively general mechanism for producing summary information about a given set of constraints. There is still quite a lot of tidying up which could be done, but its a useful start. --- pkg/air/expr.go | 2 +- pkg/air/schema.go | 16 ++-- pkg/cmd/debug.go | 197 +++++++++++++++++++++++++++++++++++++++++---- pkg/cmd/trace.go | 8 +- pkg/schema/type.go | 12 ++- 5 files changed, 205 insertions(+), 30 deletions(-) diff --git a/pkg/air/expr.go b/pkg/air/expr.go index 8eab2b59..7b4ea635 100644 --- a/pkg/air/expr.go +++ b/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} } diff --git a/pkg/air/schema.go b/pkg/air/schema.go index b0763ee5..2f2fcea9 100644 --- a/pkg/air/schema.go +++ b/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 diff --git a/pkg/cmd/debug.go b/pkg/cmd/debug.go index 86bd102d..728e788f 100644 --- a/pkg/cmd/debug.go +++ b/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) + }, + } } diff --git a/pkg/cmd/trace.go b/pkg/cmd/trace.go index 7e66194c..86c3641d 100644 --- a/pkg/cmd/trace.go +++ b/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}, diff --git a/pkg/schema/type.go b/pkg/schema/type.go index 446e5aaa..d0945132 100644 --- a/pkg/schema/type.go +++ b/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 {