feat: implement corset type checker

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(srcfile)
+	schema, err2 := corset.CompileSourceFile(false, srcfile)
 	// Check whether parsed successfully or not
 	if err2 == nil {
 		// Ok

pkg/cmd/check.go

@@ -44,6 +44,7 @@ var checkCmd = &cobra.Command{
 		cfg.reportCellWidth = GetUint(cmd, "report-cellwidth")
 		cfg.spillage = GetInt(cmd, "spillage")
 		cfg.strict = !GetFlag(cmd, "warn")
+		cfg.stdlib = !GetFlag(cmd, "no-stdlib")
 		cfg.quiet = GetFlag(cmd, "quiet")
 		cfg.padding.Right = GetUint(cmd, "padding")
 		cfg.parallelExpansion = !GetFlag(cmd, "sequential")
@@ -58,7 +59,7 @@ var checkCmd = &cobra.Command{
 		//
 		stats := util.NewPerfStats()
 		// Parse constraints
-		hirSchema = readSchema(args[1:])
+		hirSchema = readSchema(cfg.stdlib, args[1:])
 		//
 		stats.Log("Reading constraints file")
 		// Parse trace file
@@ -97,6 +98,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 include the standard library.  The default is
+	// to include it.
+	stdlib bool
 	// Specifies whether or not to report details of the failure (e.g. for
 	// debugging purposes).
 	report bool
@@ -312,6 +316,7 @@ func init() {
 	checkCmd.Flags().Bool("air", false, "check at AIR level")
 	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().BoolP("quiet", "q", false, "suppress output (e.g. warnings)")
 	checkCmd.Flags().Bool("sequential", false, "perform sequential trace expansion")

pkg/cmd/debug.go

@@ -28,8 +28,9 @@ var debugCmd = &cobra.Command{
 		mir := GetFlag(cmd, "mir")
 		air := GetFlag(cmd, "air")
 		stats := GetFlag(cmd, "stats")
+		stdlib := !GetFlag(cmd, "no-stdlib")
 		// Parse constraints
-		hirSchema := readSchema(args)
+		hirSchema := readSchema(stdlib, args)
 		// Print constraints
 		if stats {
 			printStats(hirSchema, hir, mir, air)
@@ -45,6 +46,7 @@ func init() {
 	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")
+	debugCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included")
 }
 
 func printSchemas(hirSchema *hir.Schema, hir bool, mir bool, air bool) {

pkg/cmd/test.go

@@ -38,6 +38,7 @@ var testCmd = &cobra.Command{
 		cfg.mir = GetFlag(cmd, "mir")
 		cfg.hir = GetFlag(cmd, "hir")
 		cfg.expand = !GetFlag(cmd, "raw")
+		cfg.stdlib = !GetFlag(cmd, "no-stdlib")
 		cfg.report = GetFlag(cmd, "report")
 		cfg.reportPadding = GetUint(cmd, "report-context")
 		// cfg.strict = !GetFlag(cmd, "warn")
@@ -56,7 +57,7 @@ var testCmd = &cobra.Command{
 		//
 		stats := util.NewPerfStats()
 		// Parse constraints
-		hirSchema = readSchema(args)
+		hirSchema = readSchema(cfg.stdlib, args)
 		//
 		stats.Log("Reading constraints file")
 		//
@@ -140,6 +141,7 @@ func init() {
 	// testCmd.Flags().BoolP("warn", "w", false, "report warnings instead of failing for certain errors"+
 	// 	"(e.g. unknown columns in the trace)")
 	testCmd.Flags().BoolP("debug", "d", false, "report debug logs")
+	testCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included")
 	//testCmd.Flags().BoolP("quiet", "q", false, "suppress output (e.g. warnings)")
 	testCmd.Flags().Bool("sequential", false, "perform sequential trace expansion")
 	testCmd.Flags().Uint("padding", 0, "specify amount of (front) padding to apply")

pkg/cmd/util.go

@@ -134,7 +134,8 @@ func readTraceFile(filename string) []trace.RawColumn {
 	return nil
 }
 
-func readSchema(filenames []string) *hir.Schema {
+// Read the constraints file, whilst optionally including the standard library.
+func readSchema(stdlib bool, filenames []string) *hir.Schema {
 	if len(filenames) == 0 {
 		fmt.Println("source or binary constraint(s) file required.")
 		os.Exit(5)
@@ -143,7 +144,7 @@ func readSchema(filenames []string) *hir.Schema {
 		return readBinaryFile(filenames[0])
 	}
 	// Must be source files
-	return readSourceFiles(filenames)
+	return readSourceFiles(stdlib, filenames)
 }
 
 // Read a "bin" file.
@@ -168,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(filenames []string) *hir.Schema {
+func readSourceFiles(stdlib bool, filenames []string) *hir.Schema {
 	srcfiles := make([]*sexp.SourceFile, len(filenames))
 	// Read each file
 	for i, n := range filenames {
@@ -183,7 +184,7 @@ func readSourceFiles(filenames []string) *hir.Schema {
 		srcfiles[i] = sexp.NewSourceFile(n, bytes)
 	}
 	// Parse and compile source files
-	schema, errs := corset.CompileSourceFiles(srcfiles)
+	schema, errs := corset.CompileSourceFiles(stdlib, srcfiles)
 	// Check for any errors
 	if len(errs) == 0 {
 		return schema

pkg/corset/binding.go

@@ -3,7 +3,6 @@ package corset
 import (
 	"math"
 
-	sc "github.com/consensys/go-corset/pkg/schema"
 	tr "github.com/consensys/go-corset/pkg/trace"
 )
 
@@ -42,19 +41,37 @@ type ColumnBinding struct {
 	// Column's length multiplier
 	multiplier uint
 	// Column's datatype
-	dataType sc.Type
+	dataType Type
 }
 
-// NewColumnBinding constructs a new column binding in a given module.
-func NewColumnBinding(module string, computed bool, mustProve bool, multiplier uint, datatype sc.Type) *ColumnBinding {
-	return &ColumnBinding{math.MaxUint, module, computed, mustProve, multiplier, datatype}
+// NewInputColumnBinding constructs a new column binding in a given module.
+// This is for the case where all information about the column is already known,
+// and will not be inferred from elsewhere.
+func NewInputColumnBinding(module string, mustProve bool, multiplier uint, datatype Type) *ColumnBinding {
+	return &ColumnBinding{math.MaxUint, module, false, mustProve, multiplier, datatype}
+}
+
+// NewComputedColumnBinding constructs a new column binding in a given
+// module.  This is for the case where not all information is yet known about
+// the column and, hence, it must be finalised later on.  For example, in a
+// definterleaved constraint the target column information (e.g. its type) is
+// not immediately available and must be determined from those columns from
+// which it is constructed.
+func NewComputedColumnBinding(module string) *ColumnBinding {
+	return &ColumnBinding{math.MaxUint, module, true, false, 0, nil}
 }
 
 // IsFinalised checks whether this binding has been finalised yet or not.
 func (p *ColumnBinding) IsFinalised() bool {
 	return p.multiplier != 0
 }
 
+// Finalise this binding by providing the necessary missing information.
+func (p *ColumnBinding) Finalise(multiplier uint, datatype Type) {
+	p.multiplier = multiplier
+	p.dataType = datatype
+}
+
 // Context returns the of this column.  That is, the module in which this colunm
 // was declared and also the length multiplier of that module it requires.
 func (p *ColumnBinding) Context() Context {
@@ -84,11 +101,24 @@ func (p *ColumnBinding) ColumnId() uint {
 type ConstantBinding struct {
 	// Constant expression which, when evaluated, produces a constant value.
 	value Expr
+	// Inferred type of the given expression
+	datatype Type
+}
+
+// NewConstantBinding creates a new constant binding (which is initially not
+// finalised).
+func NewConstantBinding(value Expr) ConstantBinding {
+	return ConstantBinding{value, nil}
 }
 
 // IsFinalised checks whether this binding has been finalised yet or not.
 func (p *ConstantBinding) IsFinalised() bool {
-	return true
+	return p.datatype != nil
+}
+
+// Finalise this binding by providing the necessary missing information.
+func (p *ConstantBinding) Finalise(datatype Type) {
+	p.datatype = datatype
 }
 
 // Context returns the of this constant, noting that constants (by definition)
@@ -105,33 +135,38 @@ func (p *ConstantBinding) Context() Context {
 type ParameterBinding struct {
 	// Identifies the variable or column index (as appropriate).
 	index uint
+	// Type to use for this parameter.
+	datatype Type
 }
 
-// ============================================================================
-// FunctionBinding
-// ============================================================================
-
 // IsFinalised checks whether this binding has been finalised yet or not.
 func (p *ParameterBinding) IsFinalised() bool {
-	panic("")
+	panic("should be unreachable?")
 }
 
+// ============================================================================
+// FunctionBinding
+// ============================================================================
+
 // FunctionBinding represents the binding of a function application to its
 // physical definition.
 type FunctionBinding struct {
 	// Flag whether or not is pure function
 	pure bool
-	// Types of parameters
-	paramTypes []sc.Type
-	// Type of return
-	returnType sc.Type
+	// Types of parameters (optional)
+	paramTypes []Type
+	// Type of return (optional)
+	returnType Type
+	// Inferred type of the body.  This is used to compare against the declared
+	// type (if there is one) to check for any descrepencies.
+	bodyType Type
 	// body of the function in question.
 	body Expr
 }
 
 // NewFunctionBinding constructs a new function binding.
-func NewFunctionBinding(pure bool, paramTypes []sc.Type, returnType sc.Type, body Expr) FunctionBinding {
-	return FunctionBinding{pure, paramTypes, returnType, body}
+func NewFunctionBinding(pure bool, paramTypes []Type, returnType Type, body Expr) FunctionBinding {
+	return FunctionBinding{pure, paramTypes, returnType, nil, body}
 }
 
 // IsPure checks whether this is a defpurefun or not
@@ -141,14 +176,19 @@ func (p *FunctionBinding) IsPure() bool {
 
 // IsFinalised checks whether this binding has been finalised yet or not.
 func (p *FunctionBinding) IsFinalised() bool {
-	return p.returnType != nil
+	return p.bodyType != nil
 }
 
 // Arity returns the number of parameters that this function accepts.
 func (p *FunctionBinding) Arity() uint {
 	return uint(len(p.paramTypes))
 }
 
+// Finalise this binding by providing the necessary missing information.
+func (p *FunctionBinding) Finalise(bodyType Type) {
+	p.bodyType = bodyType
+}
+
 // Apply a given set of arguments to this function binding.
 func (p *FunctionBinding) Apply(args []Expr) Expr {
 	return p.body.Substitute(args)

pkg/corset/compiler.go

@@ -1,10 +1,17 @@
 package corset
 
 import (
+	_ "embed"
+
 	"github.com/consensys/go-corset/pkg/hir"
 	"github.com/consensys/go-corset/pkg/sexp"
 )
 
+// STDLIB is an import of the standard library.
+//
+//go:embed stdlib.lisp
+var STDLIB []byte
+
 // SyntaxError defines the kind of errors that can be reported by this compiler.
 // Syntax errors are always associated with some line in one of the original
 // source files.  For simplicity, we reuse existing notion of syntax error from
@@ -14,7 +21,10 @@ 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(srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError) {
+func CompileSourceFiles(stdlib 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).
 	circuit, srcmap, errs := ParseSourceFiles(srcfiles)
 	// Check for parsing errors
 	if errs != nil {
@@ -28,8 +38,8 @@ func CompileSourceFiles(srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError
 // 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(srcfile *sexp.SourceFile) (*hir.Schema, []SyntaxError) {
-	schema, errs := CompileSourceFiles([]*sexp.SourceFile{srcfile})
+func CompileSourceFile(stdlib bool, srcfile *sexp.SourceFile) (*hir.Schema, []SyntaxError) {
+	schema, errs := CompileSourceFiles(stdlib, []*sexp.SourceFile{srcfile})
 	// Check for errors
 	if errs != nil {
 		return nil, errs
@@ -73,3 +83,14 @@ func (p *Compiler) Compile() (*hir.Schema, []SyntaxError) {
 	// Finally, translate everything and add it to the schema.
 	return TranslateCircuit(environment, p.srcmap, &p.circuit)
 }
+
+func includeStdlib(stdlib bool, srcfiles []*sexp.SourceFile) []*sexp.SourceFile {
+	if stdlib {
+		// Include stdlib file
+		srcfile := sexp.NewSourceFile("stdlib.lisp", STDLIB)
+		// Append to srcfile list
+		srcfiles = append(srcfiles, srcfile)
+	}
+	// Not included
+	return srcfiles
+}