feat: support debug constraints (#448)

Support debug constraints

This adds support for debug constraints, including a CLI option to
enable them.  However, the implementation is fairly conservative at this
stage to avoid any wierd behaviour.

cmd/testgen/main.go

@@ -190,7 +190,7 @@ func readSchemaFile(filename string) *hir.Schema {
 	// Package up as source file
 	srcfile := sexp.NewSourceFile(filename, bytes)
 	// Attempt to parse schema
-	schema, err2 := corset.CompileSourceFile(false, srcfile)
+	schema, err2 := corset.CompileSourceFile(false, false, srcfile)
 	// Check whether parsed successfully or not
 	if err2 == nil {
 		// Ok

pkg/binfile/constraint.go

@@ -62,16 +62,8 @@ func (e jsonConstraint) addToSchema(colmap map[uint]uint, schema *hir.Schema) {
 		domain := e.Vanishes.Domain.toHir()
 		// Determine enclosing module
 		ctx := expr.Context(schema)
-		// Check for vacuous constraint (i.e. one which evaluates to a constant)
-		if constant := expr.AsConstant(); constant != nil {
-			// Constraint outcome known at compile time.
-			if !constant.IsZero() {
-				panic(fmt.Sprintf("constraint %s always fails (i.e. evaluates to constant value %s)", e.Vanishes.Handle, constant))
-			}
-		} else {
-			// Construct the vanishing constraint
-			schema.AddVanishingConstraint(e.Vanishes.Handle, ctx, domain, expr)
-		}
+		// Construct the vanishing constraint
+		schema.AddVanishingConstraint(e.Vanishes.Handle, ctx, domain, expr)
 	} else if e.Lookup != nil {
 		sources := jsonExprsToHirUnit(e.Lookup.From, colmap, schema)
 		targets := jsonExprsToHirUnit(e.Lookup.To, colmap, schema)

pkg/cmd/check.go

@@ -31,7 +31,7 @@ var checkCmd = &cobra.Command{
 			os.Exit(1)
 		}
 		// Configure log level
-		if GetFlag(cmd, "debug") {
+		if GetFlag(cmd, "verbose") {
 			log.SetLevel(log.DebugLevel)
 		}
 		//
@@ -45,6 +45,7 @@ var checkCmd = &cobra.Command{
 		cfg.spillage = GetInt(cmd, "spillage")
 		cfg.strict = !GetFlag(cmd, "warn")
 		cfg.stdlib = !GetFlag(cmd, "no-stdlib")
+		cfg.debug = GetFlag(cmd, "debug")
 		cfg.quiet = GetFlag(cmd, "quiet")
 		cfg.padding.Right = GetUint(cmd, "padding")
 		cfg.parallelExpansion = !GetFlag(cmd, "sequential")
@@ -59,7 +60,7 @@ var checkCmd = &cobra.Command{
 		//
 		stats := util.NewPerfStats()
 		// Parse constraints
-		hirSchema = readSchema(cfg.stdlib, args[1:])
+		hirSchema = readSchema(cfg.stdlib, cfg.debug, args[1:])
 		//
 		stats.Log("Reading constraints file")
 		// Parse trace file
@@ -88,6 +89,8 @@ type checkConfig struct {
 	spillage int
 	// Determines how much padding to use
 	padding util.Pair[uint, uint]
+	// Determines whether or not to enable debugging constraints
+	debug bool
 	// Suppress output (e.g. warnings)
 	quiet bool
 	// Specified whether strict checking is performed or not.  This is enabled
@@ -317,7 +320,8 @@ func init() {
 	checkCmd.Flags().BoolP("warn", "w", false, "report warnings instead of failing for certain errors"+
 		"(e.g. unknown columns in the trace)")
 	checkCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included")
-	checkCmd.Flags().BoolP("debug", "d", false, "report debug logs")
+	checkCmd.Flags().Bool("debug", false, "enable debugging constraints")
+	checkCmd.Flags().BoolP("verbose", "v", false, "increase logging verbosity")
 	checkCmd.Flags().BoolP("quiet", "q", false, "suppress output (e.g. warnings)")
 	checkCmd.Flags().Bool("sequential", false, "perform sequential trace expansion")
 	checkCmd.Flags().Uint("padding", 0, "specify amount of (front) padding to apply")

pkg/cmd/debug.go

@@ -29,8 +29,9 @@ var debugCmd = &cobra.Command{
 		air := GetFlag(cmd, "air")
 		stats := GetFlag(cmd, "stats")
 		stdlib := !GetFlag(cmd, "no-stdlib")
+		debug := GetFlag(cmd, "debug")
 		// Parse constraints
-		hirSchema := readSchema(stdlib, args)
+		hirSchema := readSchema(stdlib, debug, args)
 		// Print constraints
 		if stats {
 			printStats(hirSchema, hir, mir, air)
@@ -47,6 +48,7 @@ func init() {
 	debugCmd.Flags().Bool("air", false, "Print constraints at AIR level")
 	debugCmd.Flags().Bool("stats", false, "Print summary information")
 	debugCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included")
+	debugCmd.Flags().Bool("debug", false, "enable debugging constraints")
 }
 
 func printSchemas(hirSchema *hir.Schema, hir bool, mir bool, air bool) {

pkg/cmd/test.go

@@ -57,7 +57,7 @@ var testCmd = &cobra.Command{
 		//
 		stats := util.NewPerfStats()
 		// Parse constraints
-		hirSchema = readSchema(cfg.stdlib, args)
+		hirSchema = readSchema(cfg.stdlib, false, args)
 		//
 		stats.Log("Reading constraints file")
 		//

pkg/cmd/util.go

@@ -135,7 +135,7 @@ func readTraceFile(filename string) []trace.RawColumn {
 }
 
 // Read the constraints file, whilst optionally including the standard library.
-func readSchema(stdlib bool, filenames []string) *hir.Schema {
+func readSchema(stdlib bool, debug bool, filenames []string) *hir.Schema {
 	if len(filenames) == 0 {
 		fmt.Println("source or binary constraint(s) file required.")
 		os.Exit(5)
@@ -144,7 +144,7 @@ func readSchema(stdlib bool, filenames []string) *hir.Schema {
 		return readBinaryFile(filenames[0])
 	}
 	// Must be source files
-	return readSourceFiles(stdlib, filenames)
+	return readSourceFiles(stdlib, debug, filenames)
 }
 
 // Read a "bin" file.
@@ -169,7 +169,7 @@ func readBinaryFile(filename string) *hir.Schema {
 
 // Parse a set of source files and compile them into a single schema.  This can
 // result, for example, in a syntax error, etc.
-func readSourceFiles(stdlib bool, filenames []string) *hir.Schema {
+func readSourceFiles(stdlib bool, debug bool, filenames []string) *hir.Schema {
 	srcfiles := make([]*sexp.SourceFile, len(filenames))
 	// Read each file
 	for i, n := range filenames {
@@ -184,7 +184,7 @@ func readSourceFiles(stdlib bool, filenames []string) *hir.Schema {
 		srcfiles[i] = sexp.NewSourceFile(n, bytes)
 	}
 	// Parse and compile source files
-	schema, errs := corset.CompileSourceFiles(stdlib, srcfiles)
+	schema, errs := corset.CompileSourceFiles(stdlib, debug, srcfiles)
 	// Check for any errors
 	if len(errs) == 0 {
 		return schema

pkg/corset/compiler.go

@@ -21,7 +21,7 @@ type SyntaxError = sexp.SyntaxError
 // CompileSourceFiles compiles one or more source files into a schema.  This
 // process can fail if the source files are mal-formed, or contain syntax errors
 // or other forms of error (e.g. type errors).
-func CompileSourceFiles(stdlib bool, srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError) {
+func CompileSourceFiles(stdlib bool, debug bool, srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError) {
 	// Include the standard library (if requested)
 	srcfiles = includeStdlib(stdlib, srcfiles)
 	// Parse all source files (inc stdblib if applicable).
@@ -31,15 +31,15 @@ func CompileSourceFiles(stdlib bool, srcfiles []*sexp.SourceFile) (*hir.Schema,
 		return nil, errs
 	}
 	// Compile each module into the schema
-	return NewCompiler(circuit, srcmap).Compile()
+	return NewCompiler(circuit, srcmap).SetDebug(debug).Compile()
 }
 
 // CompileSourceFile compiles exactly one source file into a schema.  This is
 // really helper function for e.g. the testing environment.   This process can
 // fail if the source file is mal-formed, or contains syntax errors or other
 // forms of error (e.g. type errors).
-func CompileSourceFile(stdlib bool, srcfile *sexp.SourceFile) (*hir.Schema, []SyntaxError) {
-	schema, errs := CompileSourceFiles(stdlib, []*sexp.SourceFile{srcfile})
+func CompileSourceFile(stdlib bool, debug bool, srcfile *sexp.SourceFile) (*hir.Schema, []SyntaxError) {
+	schema, errs := CompileSourceFiles(stdlib, debug, []*sexp.SourceFile{srcfile})
 	// Check for errors
 	if errs != nil {
 		return nil, errs
@@ -54,6 +54,8 @@ func CompileSourceFile(stdlib bool, srcfile *sexp.SourceFile) (*hir.Schema, []Sy
 type Compiler struct {
 	// A high-level definition of a Corset circuit.
 	circuit Circuit
+	// Determines whether debug
+	debug bool
 	// Source maps nodes in the circuit back to the spans in their original
 	// source files.  This is needed when reporting syntax errors to generate
 	// highlights of the relevant source line(s) in question.
@@ -62,7 +64,14 @@ type Compiler struct {
 
 // NewCompiler constructs a new compiler for a given set of modules.
 func NewCompiler(circuit Circuit, srcmaps *sexp.SourceMaps[Node]) *Compiler {
-	return &Compiler{circuit, srcmaps}
+	return &Compiler{circuit, false, srcmaps}
+}
+
+// SetDebug enables or disables debug mode.  In debug mode, debug constraints
+// will be compiled in.
+func (p *Compiler) SetDebug(flag bool) *Compiler {
+	p.debug = flag
+	return p
 }
 
 // Compile is the top-level function for the corset compiler which actually
@@ -81,7 +90,7 @@ func (p *Compiler) Compile() (*hir.Schema, []SyntaxError) {
 	// Convert global scope into an environment by allocating all columns.
 	environment := scope.ToEnvironment()
 	// Finally, translate everything and add it to the schema.
-	return TranslateCircuit(environment, p.srcmap, &p.circuit)
+	return TranslateCircuit(environment, p.debug, p.srcmap, &p.circuit)
 }
 
 func includeStdlib(stdlib bool, srcfiles []*sexp.SourceFile) []*sexp.SourceFile {

pkg/corset/expression.go

@@ -233,6 +233,55 @@ func (e *Constant) Dependencies() []Symbol {
 	return nil
 }
 
+// ============================================================================
+// Normalise
+// ============================================================================
+
+// Debug is an optional constraint which can be specifically enabled via the
+// debug setting.  The intention of debug constraints is that they capture
+// things which are implied by other constraints.  The ability to enable them
+// can simply help with debugging, should it arise that they are not actually
+// implied.
+type Debug struct{ Arg Expr }
+
+// AsConstant attempts to evaluate this expression as a constant (signed) value.
+// If this expression is not constant, then nil is returned.
+func (e *Debug) AsConstant() *big.Int {
+	return nil
+}
+
+// Multiplicity determines the number of values that evaluating this expression
+// can generate.
+func (e *Debug) Multiplicity() uint {
+	return determineMultiplicity([]Expr{e.Arg})
+}
+
+// Context returns the context for this expression.  Observe that the
+// expression must have been resolved for this to be defined (i.e. it may
+// panic if it has not been resolved yet).
+func (e *Debug) Context() Context {
+	return ContextOfExpressions([]Expr{e.Arg})
+}
+
+// Lisp converts this schema element into a simple S-Expression, for example
+// so it can be printed.
+func (e *Debug) Lisp() sexp.SExp {
+	return sexp.NewList([]sexp.SExp{
+		sexp.NewSymbol("debug"),
+		e.Arg.Lisp()})
+}
+
+// Substitute all variables (such as for function parameters) arising in
+// this expression.
+func (e *Debug) Substitute(mapping map[uint]Expr) Expr {
+	return &Debug{e.Arg.Substitute(mapping)}
+}
+
+// Dependencies needed to signal declaration.
+func (e *Debug) Dependencies() []Symbol {
+	return e.Arg.Dependencies()
+}
+
 // ============================================================================
 // Exponentiation
 // ============================================================================

pkg/corset/parser.go

@@ -152,6 +152,7 @@ func NewParser(srcfile *sexp.SourceFile, srcmap *sexp.SourceMap[sexp.SExp]) *Par
 	p.AddRecursiveListRule("~", normParserRule)
 	p.AddRecursiveListRule("^", powParserRule)
 	p.AddRecursiveListRule("begin", beginParserRule)
+	p.AddRecursiveListRule("debug", debugParserRule)
 	p.AddListRule("for", forParserRule(parser))
 	p.AddListRule("reduce", reduceParserRule(parser))
 	p.AddRecursiveListRule("if", ifParserRule)
@@ -943,6 +944,14 @@ func beginParserRule(_ string, args []Expr) (Expr, error) {
 	return &List{args}, nil
 }
 
+func debugParserRule(_ string, args []Expr) (Expr, error) {
+	if len(args) == 1 {
+		return &Debug{args[0]}, nil
+	}
+	//
+	return nil, errors.New("incorrect number of arguments")
+}
+
 func forParserRule(p *Parser) sexp.ListRule[Expr] {
 	return func(list *sexp.List) (Expr, []SyntaxError) {
 		var (

pkg/corset/resolver.go

@@ -502,12 +502,14 @@ func (r *resolver) finaliseExpressionsInModule(scope LocalScope, args []Expr) ([
 func (r *resolver) finaliseExpressionInModule(scope LocalScope, expr Expr) (Type, []SyntaxError) {
 	if v, ok := expr.(*ArrayAccess); ok {
 		return r.finaliseArrayAccessInModule(scope, v)
-	} else if v, ok := expr.(*Constant); ok {
-		nbits := v.Val.BitLen()
-		return NewUintType(uint(nbits)), nil
 	} else if v, ok := expr.(*Add); ok {
 		types, errs := r.finaliseExpressionsInModule(scope, v.Args)
 		return LeastUpperBoundAll(types), errs
+	} else if v, ok := expr.(*Constant); ok {
+		nbits := v.Val.BitLen()
+		return NewUintType(uint(nbits)), nil
+	} else if v, ok := expr.(*Debug); ok {
+		return r.finaliseExpressionInModule(scope, v.Arg)
 	} else if v, ok := expr.(*Exp); ok {
 		purescope := scope.NestedPureScope()
 		arg_types, arg_errs := r.finaliseExpressionInModule(scope, v.Arg)