feat: implement corset type checker (#431)

* Add Tests for Typing

This adds a small number of valid and invalid tests for checking typing.

* Distinguish loobean / boolean semantics

Whilst this is a fairly esoteric part of the corset language, it is
nevertheless necessary to implement in order to faithly recreate the
language's semantics.

* Support primitive type inference

This puts in place a fairly primitive form of type inference, which
doesn't really do anything at this time.  However, most of the machinery
is now in place...

* Enable Resolution of If

This puts in place the ability to resolve an if as either an if-zero or
an if-notzero depending on whether the condition is loobean or boolean.
In the case that it is neither, then an error is reported.  At this
stage, however, the mechanism for infering the type of an arbitrary
expression remains somewhat limited.

* Enable checking guards are boolean

This adds support for checking that guards have boolean semantics.  For
now, checking constraints have loobean semantics is implemented but not
enabled.  The problem is that it breaks a lot of the existing tests!

* Fix (now broken) tests

This fixes a number of tests which have been broken as a result of the
introduced type checking process.  The biggest issue here is that we
really need the ability to put return types on functions in order to
resolve some situations.

* Support Function Return Types

This adds support for function return types, and updates a larger number
of tests to use "vanishes!" to meet the loobean requirements for a
constraint.  This also relaxes the rules for combining types for
addition and subtraction, following what corset does.

In addition, this introduces a very minimal standard library which (at
this time) includes only the "vanishes" declaration.

* Rework Memory Example

This reworks the memory example so that it now: (a) compiles; (b) makes
use of the stdlib (what there is of it) to improve the overall look.
There is an outstanding issue related to the return types of functions.
Specifically, it seems that corset infers the return type when it is not
specified.

* Implement type inference

This puts in place a naive algorithm for type inference of function
invocations.  Its somewhat awkward, but it reflects the original corset
language.

* Support type inference through invocations

The corset language supports an interesting notion of type inference in
the case that a function is declared without an explicit return type
being given.  Specifically, it types it polymorphically at the call site
based on the types of the given arguments.

* Fix Declaration Finalisation

This fixes some problems with the existing finalisation algorithm.
Firstly, it was sometimes finalising things more than once (which is
wasteful).  Secondly, it was not finalising at a fine-enough granularity
(which caused problems for constant definitions which referred to
themself).  Finally, there were still some gremlins related to binding.

* Fixes for Quick Tests

This puts through various minor fixes for the quick tests.  What remains
now is to update the larger tests.  At this stage, performance may be
starting to become an issue.

* Update standard library

This pulls over as much of the original corset standard library as
possible at the moment (which is actually most of it).  There are a
couple of outstanding issues to be resolved around overloading, etc.

* Update Slow Tests

This updates the slow test to be almost exactly as they were original
defined (i.e. using the full corset syntax).  At this stage, there are
a number of outstanding issues which remain, and some of the tests have
parts commented out.

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
+}