feat: function call declaration (#1329)

This adds support for parsing defcall declarations, along with an
appropriate AST node.

This adds support for the resolution, processing and typing stages for
the DefCall construct.  An initial implementation of translation is also
included, but this does not yet actually translate the call.

This adds support for checking arguments and returns.  In particular,
check that there are enough arguments and returns, and also that their
bitwidths follow the expected subtyping pattern.

Condition function calls are supported where a (logical) selector is 
provided.  Function calls are encoded / decoded at the HIR level.

Author: DavePearce

pkg/asm/propagate.go

@@ -19,12 +19,13 @@ import (
 
 	"github.com/consensys/go-corset/pkg/asm/io"
 	"github.com/consensys/go-corset/pkg/ir"
+	"github.com/consensys/go-corset/pkg/ir/hir"
 	sc "github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/module"
 	"github.com/consensys/go-corset/pkg/schema/register"
+	"github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/trace/lt"
 	"github.com/consensys/go-corset/pkg/util/collection/array"
-	"github.com/consensys/go-corset/pkg/util/field"
 	"github.com/consensys/go-corset/pkg/util/word"
 )
 
@@ -38,8 +39,8 @@ type RawModule = lt.Module[word.BigEndian]
 // Validation?
 // Batch size?
 // Recursion limit (to prevent infinite loops)
-func PropagateAll[F field.Element[F], T io.Instruction[T], M sc.Module[F]](p MixedProgram[F, T, M], ts []lt.TraceFile,
-	expanding bool) ([]lt.TraceFile, []error) {
+func PropagateAll[T io.Instruction[T], M sc.Module[word.BigEndian]](p MixedProgram[word.BigEndian, T, M],
+	ts []lt.TraceFile, expanding bool) ([]lt.TraceFile, []error) {
 	//
 	var (
 		errors  []error
@@ -76,12 +77,12 @@ func PropagateAll[F field.Element[F], T io.Instruction[T], M sc.Module[F]](p Mix
 // Validation?
 // Batch size?
 // Recursion limit (to prevent infinite loops)
-func Propagate[F field.Element[F], T io.Instruction[T], M sc.Module[F]](p MixedProgram[F, T, M], trace lt.TraceFile,
-	expanding bool) (lt.TraceFile, []error) {
+func Propagate[T io.Instruction[T], M sc.Module[word.BigEndian]](p MixedProgram[word.BigEndian, T, M],
+	trace lt.TraceFile, expanding bool) (lt.TraceFile, []error) {
 	// Construct suitable executior for the given program
 	var (
 		errors []error
-		n      = len(p.program.Functions())
+		n      = uint(len(p.program.Functions()))
 		//
 		executor = io.NewExecutor(p.program)
 		// Clone heap in trace file, since will mutate this.
@@ -94,7 +95,7 @@ func Propagate[F field.Element[F], T io.Instruction[T], M sc.Module[F]](p MixedP
 		return lt.TraceFile{}, errors
 	}
 	// Write seed instances
-	errors = writeInstances(p.program, trace.Modules[:n], executor)
+	errors = writeInstances(p, n, trace.Modules, executor)
 	// Read out generated instances
 	modules := readInstances(&heap, p.program, executor)
 	// Append external modules (which are unaffected by propagation).
@@ -106,15 +107,24 @@ func Propagate[F field.Element[F], T io.Instruction[T], M sc.Module[F]](p MixedP
 // WriteInstances writes all of the instances defined in the given trace columns
 // into the executor which, in turn, forces it to execute the relevant
 // functions, and functions they call, etc.
-func writeInstances[T io.Instruction[T]](p io.Program[T], trace []lt.Module[word.BigEndian],
-	executor *io.Executor[T]) []error {
+func writeInstances[T io.Instruction[T], M sc.Module[word.BigEndian]](p MixedProgram[word.BigEndian, T, M], n uint,
+	trace []lt.Module[word.BigEndian], executor *io.Executor[T]) []error {
 	//
 	var errors []error
-	//
-	for i, m := range trace {
-		errs := writeFunctionInstances(uint(i), p, m, executor)
+	// Write all from assembly modules
+	for i, m := range trace[:n] {
+		errs := writeFunctionInstances(uint(i), p.program, m, executor)
 		errors = append(errors, errs...)
 	}
+	// Write all from non-assembly modules
+	for i, m := range trace[n:] {
+		var extern = p.externs[i]
+		// Write instances from any external calls
+		for _, call := range extractExternalCalls(extern) {
+			errs := writeExternCall(call, p.program, m, executor)
+			errors = append(errors, errs...)
+		}
+	}
 	//
 	return errors
 }
@@ -145,6 +155,68 @@ func writeFunctionInstances[T io.Instruction[T]](fid uint, p io.Program[T], mod
 	return errors
 }
 
+// Extract any external function calls found within the given module, returning
+// them as an array.
+func extractExternalCalls[M sc.Module[word.BigEndian]](extern M) []hir.FunctionCall {
+	var calls []hir.FunctionCall
+	//
+	for iter := extern.Constraints(); iter.HasNext(); {
+		c := iter.Next()
+		// This should always hold
+		if hc, ok := c.(hir.Constraint); ok {
+			// Check whether its a call or not
+			if call, ok := hc.Unwrap().(hir.FunctionCall); ok {
+				// Yes, so record it
+				calls = append(calls, call)
+			}
+		}
+	}
+	//
+	return calls
+}
+
+// Write any function instances arising from the given call.
+func writeExternCall[T io.Instruction[T]](call hir.FunctionCall, p io.Program[T], mod RawModule,
+	executor *io.Executor[T]) []error {
+	//
+	var (
+		trMod   = &ltModuleAdaptor{mod}
+		height  = mod.Height()
+		fn      = p.Function(call.Callee)
+		inputs  = make([]big.Int, fn.NumInputs())
+		outputs = make([]big.Int, fn.NumOutputs())
+		errors  []error
+	)
+	//
+	if call.Selector.HasValue() {
+		var selector = call.Selector.Unwrap()
+		// Invoke each user-defined instance in turn
+		for i := range height {
+			// execute if selector enabled
+			if enabled, _, err := selector.TestAt(int(i), trMod, nil); enabled {
+				// Extract external columns
+				extractExternColumns(int(i), call, trMod, inputs, outputs)
+				// Execute function call to produce outputs
+				errs := executeAndCheck(call.Callee, fn.Name(), inputs, outputs, executor)
+				errors = append(errors, errs...)
+			} else if err != nil {
+				errors = append(errors, err)
+			}
+		}
+	} else {
+		// Invoke each user-defined instance in turn
+		for i := range height {
+			// Extract external columns
+			extractExternColumns(int(i), call, trMod, inputs, outputs)
+			// Execute function call to produce outputs
+			errs := executeAndCheck(call.Callee, fn.Name(), inputs, outputs, executor)
+			errors = append(errors, errs...)
+		}
+	}
+	//
+	return errors
+}
+
 func executeAndCheck[T io.Instruction[T]](fid uint, name module.Name, inputs, outputs []big.Int,
 	executor *io.Executor[T]) []error {
 	var (
@@ -198,6 +270,34 @@ func extractFunctionColumns(row uint, mod RawModule, inputs, outputs []big.Int)
 	}
 }
 
+func extractExternColumns(row int, call hir.FunctionCall, mod trace.Module[word.BigEndian],
+	inputs, outputs []big.Int) []error {
+	//
+	// Extract function arguments
+	errs1 := extractExternTerms(row, call.Arguments, mod, inputs)
+	// Extract function returns
+	errs2 := extractExternTerms(row, call.Returns, mod, outputs)
+	//
+	return append(errs1, errs2...)
+}
+
+func extractExternTerms(row int, terms []hir.Term, mod trace.Module[word.BigEndian], values []big.Int) []error {
+	var errors []error
+	//
+	for i, arg := range terms {
+		var (
+			ith      big.Int
+			val, err = arg.EvalAt(row, mod, nil)
+		)
+		ith.SetBytes(val.Bytes())
+		values[i] = ith
+		//
+		errors = append(errors, err)
+	}
+	//
+	return errors
+}
+
 func extractFunctionPadding(registers []register.Register, inputs, outputs []big.Int) {
 	var numInputs = len(inputs)
 	//
@@ -282,3 +382,50 @@ func toArgumentString(args []big.Int) string {
 	//
 	return builder.String()
 }
+
+// The purpose of the lt adaptor is to make an lt.TraceFile look like a Trace.
+// In general, this is not safe.  However, we use this once we already know that
+// the trace has been aligned.  Also, it is only used in a specific context.
+type ltModuleAdaptor struct {
+	module lt.Module[word.BigEndian]
+}
+
+func (p *ltModuleAdaptor) Name() trace.ModuleName {
+	return p.module.Name
+}
+
+func (p *ltModuleAdaptor) Width() uint {
+	return uint(len(p.module.Columns))
+}
+
+func (p *ltModuleAdaptor) Height() uint {
+	return p.module.Height()
+}
+
+func (p *ltModuleAdaptor) Column(cid uint) trace.Column[word.BigEndian] {
+	return &ltColumnAdaptor{p.module.Columns[cid]}
+}
+
+func (p *ltModuleAdaptor) ColumnOf(col string) trace.Column[word.BigEndian] {
+	panic("unsupported operation")
+}
+
+type ltColumnAdaptor struct {
+	column lt.Column[word.BigEndian]
+}
+
+func (p *ltColumnAdaptor) Name() string {
+	return p.column.Name
+}
+
+func (p *ltColumnAdaptor) Get(row int) word.BigEndian {
+	return p.column.Data.Get(uint(row))
+}
+
+func (p *ltColumnAdaptor) Data() array.Array[word.BigEndian] {
+	return p.column.Data
+}
+
+func (p *ltColumnAdaptor) Padding() word.BigEndian {
+	panic("unsupported operation")
+}

pkg/corset/ast/declaration.go

@@ -147,6 +147,97 @@ func (p *DefAlias) Lisp() sexp.SExp {
 	return sexp.NewSymbol(p.Name)
 }
 
+// ============================================================================
+// defcall
+// ============================================================================
+
+// DefCall captures a function call between a lisp module and an assembly
+// function.  A key feature of this is that it triggers trace propagation.
+type DefCall struct {
+	// Returns for the call
+	Returns []Expr
+	// Function being called
+	Function string
+	// Arguments for the call
+	Arguments []Expr
+	// Optional source selector
+	Selector util.Option[Expr]
+	// determines whether or not this has been finalised.
+	finalised bool
+}
+
+// NewDefCall creates a new (unfinalised) function call.
+func NewDefCall(returns []Expr, fun string, args []Expr, selector util.Option[Expr]) *DefCall {
+	//
+	return &DefCall{returns, fun, args, selector, false}
+}
+
+// Definitions returns the set of symbols defined by this declaration.  Observe
+// that these may not yet have been finalised.
+func (p *DefCall) Definitions() iter.Iterator[SymbolDefinition] {
+	return iter.NewArrayIterator[SymbolDefinition](nil)
+}
+
+// Dependencies needed to signal declaration.
+func (p *DefCall) Dependencies() iter.Iterator[Symbol] {
+	var deps []Symbol
+	//
+	deps = append(deps, DependenciesOfExpressions(p.Arguments)...)
+	deps = append(deps, DependenciesOfExpressions(p.Returns)...)
+	// Include selector dependencies (if applicable)
+	if p.Selector.HasValue() {
+		deps = append(deps, p.Selector.Unwrap().Dependencies()...)
+	}
+	// Combine deps
+	return iter.NewArrayIterator(deps)
+}
+
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefCall) Defines(symbol Symbol) bool {
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefCall) IsFinalised() bool {
+	return p.finalised
+}
+
+// Finalise this declaration, which means that all source and target expressions
+// have been resolved.
+func (p *DefCall) Finalise() {
+	p.finalised = true
+}
+
+// Lisp converts this node into its lisp representation.  This is primarily used
+// for debugging purposes.
+func (p *DefCall) Lisp() sexp.SExp {
+	returns := make([]sexp.SExp, len(p.Returns))
+	args := make([]sexp.SExp, len(p.Arguments))
+	// Returns
+	for i, t := range p.Returns {
+		returns[i] = t.Lisp()
+	}
+	// Arguments
+	for i, t := range p.Arguments {
+		args[i] = t.Lisp()
+	}
+	//
+	list := sexp.NewList([]sexp.SExp{
+		sexp.NewSymbol("defcall"),
+		sexp.NewList(returns),
+		sexp.NewSymbol(p.Function),
+		sexp.NewList(args),
+	})
+	// Include selector (if applicable)
+	if p.Selector.HasValue() {
+		list.Append(p.Selector.Unwrap().Lisp())
+	}
+	//
+	return list
+}
+
 // ============================================================================
 // defcolumns
 // ============================================================================

pkg/corset/ast/expression.go

@@ -524,7 +524,7 @@ type For struct {
 // NewFor constructs a new for-expression given a variable name, a static index
 // range and a body.
 func NewFor(name string, start uint, end uint, body Expr) *For {
-	binding := NewLocalVariableBinding(name, INT_TYPE)
+	binding := NewLocalVariableBinding(name, UINT_TYPE)
 	return &For{binding, start, end, body}
 }
 
@@ -714,7 +714,7 @@ func NewLet(bindings []util.Pair[string, Expr], body Expr) *Let {
 	exprs := make([]Expr, len(bindings))
 	//
 	for i, p := range bindings {
-		vars[i] = NewLocalVariableBinding(p.Left, INT_TYPE)
+		vars[i] = NewLocalVariableBinding(p.Left, UINT_TYPE)
 		exprs[i] = p.Right
 	}
 	//

pkg/corset/ast/type.go

@@ -136,10 +136,10 @@ func (p *AnyType) String() string {
 // IntType
 // ============================================================================
 
-// INT_TYPE represents the infinite integer range.  This cannot be translated
+// UINT_TYPE represents the infinite integer range.  This cannot be translated
 // into a concrete type at the lower level, and therefore can only be used
 // internally (e.g. for type checking).
-var INT_TYPE = &IntType{math.INFINITY}
+var UINT_TYPE = &IntType{math.INFINITY}
 
 // IntType represents a set of signed integer values.
 type IntType struct {

pkg/corset/compiler/intrinsics.go

@@ -91,7 +91,7 @@ func (p *IntrinsicDefinition) Signature() *ast.FunctionSignature {
 	types := make([]ast.Type, p.arity)
 	//
 	for i := 0; i < len(types); i++ {
-		types[i] = ast.INT_TYPE
+		types[i] = ast.UINT_TYPE
 	}
 	// Allow return type to be inferred.
 	return ast.NewFunctionSignature(true, types, nil, body)