Rework scope resolution

This reworks the way in which scopes are resolved to avoid using the
Environment until the very last moment in the compilation process.  This
just means we don't have to get too concerned about specific column
identifiers until it really matters.  It also means we can retain more
detailed meta-information, allowing better analysis.

pkg/air/expr.go

@@ -213,7 +213,7 @@ func NewConst64(val uint64) Expr {
 // Context determines the evaluation context (i.e. enclosing module) for this
 // expression.
 func (p *Constant) Context(schema sc.Schema) trace.Context {
-	return trace.VoidContext()
+	return trace.VoidContext[uint]()
 }
 
 // RequiredColumns returns the set of columns on which this term depends.

pkg/binfile/computation.go

@@ -127,7 +127,7 @@ func sourceColumnsFromHandles(handles []string, columns []column,
 	// Convert source refs into column indexes
 	sources := make([]uint, len(sourceIDs))
 	//
-	ctx := trace.VoidContext()
+	ctx := trace.VoidContext[uint]()
 	//
 	for i, source_id := range sourceIDs {
 		// Determine schema column index for ith source column.

pkg/corset/ast.go

@@ -177,19 +177,6 @@ type DefInterleaved struct {
 	Sources []*DefName
 }
 
-// CanFinalise checks whether or not this interleaving is ready to be finalised.
-// Specifically, it checks whether or not the source columns of this
-// interleaving are themselves finalised.
-func (p *DefInterleaved) CanFinalise(module uint, env *Environment) bool {
-	for _, col := range p.Sources {
-		if !env.IsColumnFinalised(module, col.Name) {
-			return false
-		}
-	}
-	//
-	return true
-}
-
 // IsDeclaration needed to signal declaration.
 func (p *DefInterleaved) IsDeclaration() {}
 
@@ -238,46 +225,19 @@ func (p *DefLookup) Lisp() sexp.SExp {
 // source columns can be specified as increasing or decreasing.
 type DefPermutation struct {
 	Targets []*DefColumn
-	Sources []*DefPermutedColumn
+	Sources []*DefName
+	Signs   []bool
 }
 
 // IsDeclaration needed to signal declaration.
 func (p *DefPermutation) IsDeclaration() {}
 
-// CanFinalise checks whether or not this permutation is ready to be finalised.
-// Specifically, it checks whether or not the source columns of this permutation
-// are themselves finalised.
-func (p *DefPermutation) CanFinalise(module uint, env *Environment) bool {
-	for _, col := range p.Sources {
-		if !env.IsColumnFinalised(module, col.Name) {
-			return false
-		}
-	}
-	//
-	return true
-}
-
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefPermutation) Lisp() sexp.SExp {
 	panic("got here")
 }
 
-// DefPermutedColumn provides information about a column being permuted by a
-// sorted permutation.
-type DefPermutedColumn struct {
-	// Name of the column to be permuted
-	Name string
-	// Sign of the column
-	Sign bool
-}
-
-// Lisp converts this node into its lisp representation.  This is primarily used
-// for debugging purposes.
-func (p *DefPermutedColumn) Lisp() sexp.SExp {
-	panic("got here")
-}
-
 // DefProperty represents an assertion to be used only for debugging / testing /
 // verification.  Unlike vanishing constraints, property assertions do not
 // represent something that the prover can enforce.  Rather, they represent
@@ -370,21 +330,24 @@ type Expr interface {
 	Node
 	// Multiplicity defines the number of values which will be returned when
 	// evaluating this expression.  Due to the nature of expressions in Corset,
-	// they can (perhaps) surprisingly return multiple values.  For example,
+	// they can (perhaps surprisingly) return multiple values.  For example,
 	// lists return one value for each element in the list.  Note, every
 	// expression must return at least one value.
 	Multiplicity() uint
 
 	// 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).
-	Context() tr.Context
+	Context() Context
 
 	// Substitute all variables (such as for function parameters) arising in
 	// this expression.
 	Substitute(args []Expr) Expr
 }
 
+// Context represents the evaluation context for a given expression.
+type Context = tr.RawContext[string]
+
 // ============================================================================
 // Addition
 // ============================================================================
@@ -401,7 +364,7 @@ func (e *Add) Multiplicity() uint {
 // 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 *Add) Context() tr.Context {
+func (e *Add) Context() Context {
 	return ContextOfExpressions(e.Args)
 }
 
@@ -433,8 +396,8 @@ func (e *Constant) Multiplicity() uint {
 // 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 *Constant) Context() tr.Context {
-	return tr.VoidContext()
+func (e *Constant) Context() Context {
+	return tr.VoidContext[string]()
 }
 
 // Lisp converts this schema element into a simple S-Expression, for example
@@ -468,7 +431,7 @@ func (e *Exp) Multiplicity() uint {
 // 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 *Exp) Context() tr.Context {
+func (e *Exp) Context() Context {
 	return ContextOfExpressions([]Expr{e.Arg})
 }
 
@@ -508,7 +471,7 @@ func (e *IfZero) Multiplicity() uint {
 // 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 *IfZero) Context() tr.Context {
+func (e *IfZero) Context() Context {
 	return ContextOfExpressions([]Expr{e.Condition, e.TrueBranch, e.FalseBranch})
 }
 
@@ -543,7 +506,7 @@ func (e *List) Multiplicity() uint {
 // 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 *List) Context() tr.Context {
+func (e *List) Context() Context {
 	return ContextOfExpressions(e.Args)
 }
 
@@ -575,7 +538,7 @@ func (e *Mul) Multiplicity() uint {
 // 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 *Mul) Context() tr.Context {
+func (e *Mul) Context() Context {
 	return ContextOfExpressions(e.Args)
 }
 
@@ -608,7 +571,7 @@ func (e *Normalise) Multiplicity() uint {
 // 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 *Normalise) Context() tr.Context {
+func (e *Normalise) Context() Context {
 	return ContextOfExpressions([]Expr{e.Arg})
 }
 
@@ -640,7 +603,7 @@ func (e *Sub) Multiplicity() uint {
 // 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 *Sub) Context() tr.Context {
+func (e *Sub) Context() Context {
 	return ContextOfExpressions(e.Args)
 }
 
@@ -671,7 +634,7 @@ type Invoke struct {
 // 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 *Invoke) Context() tr.Context {
+func (e *Invoke) Context() Context {
 	if e.Binding == nil {
 		panic("unresolved expressions encountered whilst resolving context")
 	}
@@ -720,12 +683,16 @@ func (e *VariableAccess) Multiplicity() uint {
 // 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 *VariableAccess) Context() tr.Context {
-	if e.Binding == nil {
-		panic("unresolved expressions encountered whilst resolving context")
+func (e *VariableAccess) Context() Context {
+	binding, ok := e.Binding.(*ColumnBinding)
+	//
+	if ok {
+		return binding.Context()
+	} else if binding == nil {
+		panic("unresolved column access")
 	}
-	// Extract saved context
-	return e.Binding.Context()
+	//
+	panic("invalid column access")
 }
 
 // Lisp converts this schema element into a simple S-Expression, for example
@@ -758,8 +725,8 @@ func (e *VariableAccess) Substitute(args []Expr) Expr {
 // they are all constants) then the void context is returned.  Likewise, if
 // there are expressions with different contexts then the conflicted context
 // will be returned.  Otherwise, the one consistent context will be returned.
-func ContextOfExpressions(exprs []Expr) tr.Context {
-	context := tr.VoidContext()
+func ContextOfExpressions(exprs []Expr) Context {
+	context := tr.VoidContext[string]()
 	//
 	for _, e := range exprs {
 		context = context.Join(e.Context())

pkg/corset/binding.go

@@ -1,32 +1,71 @@
 package corset
 
 import (
+	"math"
+
+	sc "github.com/consensys/go-corset/pkg/schema"
 	tr "github.com/consensys/go-corset/pkg/trace"
 )
 
+// BindingId is an identifier is used to distinguish different forms of binding,
+// as some forms are known from their use.  Specifically, at the current time,
+// only functions are distinguished from other categories (e.g. columns,
+// parameters, etc).
+type BindingId struct {
+	// Name of the binding
+	name string
+	// Indicates whether function binding or other.
+	fn bool
+}
+
 // Binding represents an association between a name, as found in a source file,
 // and concrete item (e.g. a column, function, etc).
 type Binding interface {
 	// Returns the context associated with this binding.
-	Context() tr.Context
+	IsBinding()
 }
 
 // ColumnBinding represents something bound to a given column.
 type ColumnBinding struct {
-	// For a column access, this identifies the enclosing context.
-	context tr.Context
-	// Identifies the variable or column index (as appropriate).
-	index uint
+	// Column's allocated identifier
+	cid uint
+	// Column's enclosing module
+	module string
+	// Determines whether this is a computed column, or not.
+	computed bool
+	// Column's length multiplier
+	multiplier uint
+	// Column's datatype
+	datatype sc.Type
+}
+
+// NewColumnBinding constructs a new column binding in a given module.
+func NewColumnBinding(module string, computed bool, multiplier uint, datatype sc.Type) *ColumnBinding {
+	return &ColumnBinding{math.MaxUint, module, computed, multiplier, datatype}
+}
+
+// IsBinding ensures this is an instance of Binding.
+func (p *ColumnBinding) IsBinding() {}
+
+// 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 {
+	return tr.NewContext(p.module, p.multiplier)
 }
 
-// Context returns the enclosing context for this column access.
-func (p *ColumnBinding) Context() tr.Context {
-	return p.context
+// AllocateId allocates the column identifier for this column
+func (p *ColumnBinding) AllocateId(cid uint) {
+	p.cid = cid
 }
 
-// ColumnID returns the column identifier that this column access refers to.
-func (p *ColumnBinding) ColumnID() uint {
-	return p.index
+// ColumnId returns the allocated identifier for this column.  NOTE: this will
+// panic if this column has not yet been allocated an identifier.
+func (p *ColumnBinding) ColumnId() uint {
+	if p.cid == math.MaxUint {
+		panic("column id not yet allocated")
+	}
+	//
+	return p.cid
 }
 
 // ParameterBinding represents something bound to a given column.
@@ -35,11 +74,8 @@ type ParameterBinding struct {
 	index uint
 }
 
-// Context for a parameter is always void, as it does not correspond to a column
-// in given module.
-func (p *ParameterBinding) Context() tr.Context {
-	return tr.VoidContext()
-}
+// IsBinding ensures this is an instance of Binding.
+func (p *ParameterBinding) IsBinding() {}
 
 // FunctionBinding represents the binding of a function application to its
 // physical definition.
@@ -50,11 +86,8 @@ type FunctionBinding struct {
 	body Expr
 }
 
-// Context for a parameter is always void, as it does not correspond to a column
-// in given module.
-func (p *FunctionBinding) Context() tr.Context {
-	return tr.VoidContext()
-}
+// IsBinding ensures this is an instance of Binding.
+func (p *FunctionBinding) IsBinding() {}
 
 // Apply a given set of arguments to this function binding.
 func (p *FunctionBinding) Apply(args []Expr) Expr {

pkg/corset/compiler.go

@@ -64,15 +64,17 @@ func NewCompiler(circuit Circuit, srcmaps *sexp.SourceMaps[Node]) *Compiler {
 // etc.
 func (p *Compiler) Compile() (*hir.Schema, []SyntaxError) {
 	// Resolve variables (via nested scopes)
-	env, errs := ResolveCircuit(p.srcmap, &p.circuit)
+	scope, errs := ResolveCircuit(p.srcmap, &p.circuit)
 	// Check whether any errors were encountered.  If so, terminate since we
 	// cannot proceed with translation.
 	if len(errs) != 0 {
 		return nil, errs
 	}
+	// Convert global scope into an environment by allocating all columns.
+	environment := scope.ToEnvironment()
 	// Check constraint contexts (e.g. for constraints, lookups, etc)
 	// Type check constraints
 	fmt.Println("Translating Circuit...")
 	// Finally, translate everything and add it to the schema.
-	return TranslateCircuit(env, p.srcmap, &p.circuit)
+	return TranslateCircuit(environment, p.srcmap, &p.circuit)
 }