feat: support tests for invalid syntax (#388)

This adds support for tests which ensure certain forms of invalid syntax are identified. For example, attempting to use a column which doesn't exist, or combining columns from different modules in the same constraint, etc.

pkg/corset/ast.go

@@ -175,15 +175,15 @@ type DefInterleaved struct {
 	// The target column being defined
 	Target string
 	// The source columns used to define the interleaved target column.
-	Sources []string
+	Sources []*DefSourceColumn
 }
 
 // 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) {
+		if !env.IsColumnFinalised(module, col.Name) {
 			return false
 		}
 	}
@@ -200,6 +200,19 @@ func (p *DefInterleaved) Lisp() sexp.SExp {
 	panic("got here")
 }
 
+// DefSourceColumn provides information about a column being permuted by a
+// sorted permutation.
+type DefSourceColumn struct {
+	// Name of the column to be permuted
+	Name string
+}
+
+// Lisp converts this node into its lisp representation.  This is primarily used
+// for debugging purposes.
+func (p *DefSourceColumn) Lisp() sexp.SExp {
+	panic("got here")
+}
+
 // DefLookup represents a lookup constraint between a set N of source
 // expressions and a set of N target expressions.  The source expressions must
 // have a single context (i.e. all be in the same module) and likewise for the

pkg/corset/parser.go

@@ -302,6 +302,10 @@ func (p *Parser) parseColumnDeclaration(e sexp.SExp) (*DefColumn, *SyntaxError)
 
 // Parse a vanishing declaration
 func (p *Parser) parseDefConstraint(elements []sexp.SExp) (*DefConstraint, *SyntaxError) {
+	// Initial sanity checks
+	if elements[1].AsSymbol() == nil {
+		return nil, p.translator.SyntaxError(elements[1], "expected constraint handle")
+	}
 	//
 	handle := elements[1].AsSymbol().Value
 	// Vanishing constraints do not have global scope, hence qualified column
@@ -331,15 +335,15 @@ func (p *Parser) parseDefInterleaved(elements []sexp.SExp) (*DefInterleaved, *Sy
 	// Extract target and source columns
 	target := elements[1].AsSymbol().Value
 	sexpSources := elements[2].AsList()
-	sources := make([]string, sexpSources.Len())
+	sources := make([]*DefSourceColumn, sexpSources.Len())
 	//
 	for i := 0; i != sexpSources.Len(); i++ {
 		ith := sexpSources.Get(i)
 		if ith.AsSymbol() == nil {
 			return nil, p.translator.SyntaxError(ith, "malformed source column")
 		}
 		// Extract column name
-		sources[i] = ith.AsSymbol().Value
+		sources[i] = &DefSourceColumn{ith.AsSymbol().Value}
 	}
 	// Done
 	return &DefInterleaved{target, sources}, nil
@@ -408,15 +412,15 @@ func (p *Parser) parseDefPermutation(elements []sexp.SExp) (*DefPermutation, *Sy
 			return nil, err
 		}
 		// Parse source column
-		if sources[i], err = p.parsePermutedColumnDeclaration(sexpSources.Get(i)); err != nil {
+		if sources[i], err = p.parsePermutedColumnDeclaration(i == 0, sexpSources.Get(i)); err != nil {
 			return nil, err
 		}
 	}
 	//
 	return &DefPermutation{targets, sources}, nil
 }
 
-func (p *Parser) parsePermutedColumnDeclaration(e sexp.SExp) (*DefPermutedColumn, *SyntaxError) {
+func (p *Parser) parsePermutedColumnDeclaration(signRequired bool, e sexp.SExp) (*DefPermutedColumn, *SyntaxError) {
 	var err *SyntaxError
 	//
 	defcolumn := &DefPermutedColumn{"", false}
@@ -436,6 +440,8 @@ func (p *Parser) parsePermutedColumnDeclaration(e sexp.SExp) (*DefPermutedColumn
 		}
 		// Parse column name
 		defcolumn.Name = l.Get(1).AsSymbol().Value
+	} else if signRequired {
+		return nil, p.translator.SyntaxError(e, "missing sort direction")
 	} else {
 		defcolumn.Name = e.String(false)
 	}
@@ -458,6 +464,10 @@ func (p *Parser) parsePermutedColumnSign(sign *sexp.Symbol) (bool, *SyntaxError)
 
 // Parse a property assertion
 func (p *Parser) parseDefProperty(elements []sexp.SExp) (*DefProperty, *SyntaxError) {
+	// Initial sanity checks
+	if elements[1].AsSymbol() == nil {
+		return nil, p.translator.SyntaxError(elements[1], "expected constraint handle")
+	}
 	//
 	handle := elements[1].AsSymbol().Value
 	// Translate expression

pkg/corset/resolver.go

@@ -125,11 +125,11 @@ func (r *resolver) resolveAssignments(circuit *Circuit) []SyntaxError {
 // to process all columns before we can sure that they are all declared
 // correctly.
 func (r *resolver) resolveAssignmentsInModule(module string, decls []Declaration) []SyntaxError {
-	// FIXME: the following is actually broken since we must allocate all input
-	// columns in all modules before any assignments are preregistered.
-	errors := r.initialiseAssignmentsInModule(module, decls)
-	// Check for any errors
-	if len(errors) > 0 {
+	if errors := r.initialiseAssignmentsInModule(module, decls); len(errors) > 0 {
+		return errors
+	}
+	// Check assignments
+	if errors := r.checkAssignmentsInModule(module, decls); len(errors) > 0 {
 		return errors
 	}
 	// Iterate until all columns finalised
@@ -170,6 +170,29 @@ func (r *resolver) initialiseAssignmentsInModule(module string, decls []Declarat
 	return errors
 }
 
+func (r *resolver) checkAssignmentsInModule(module string, decls []Declaration) []SyntaxError {
+	errors := make([]SyntaxError, 0)
+	mid := r.env.Module(module)
+	//
+	for _, d := range decls {
+		if col, ok := d.(*DefInterleaved); ok {
+			for _, c := range col.Sources {
+				if !r.env.HasColumn(mid, c.Name) {
+					errors = append(errors, *r.srcmap.SyntaxError(c, "unknown source column"))
+				}
+			}
+		} else if col, ok := d.(*DefPermutation); ok {
+			for _, c := range col.Sources {
+				if !r.env.HasColumn(mid, c.Name) {
+					errors = append(errors, *r.srcmap.SyntaxError(c, "unknown source column"))
+				}
+			}
+		}
+	}
+	// Done
+	return errors
+}
+
 // Iterate the column allocation to a fix point by iteratively fleshing out column information.
 func (r *resolver) finaliseAssignmentsInModule(module string, decls []Declaration) []SyntaxError {
 	mid := r.env.Module(module)
@@ -253,7 +276,7 @@ func (r *resolver) finaliseInterleavedAssignment(module uint, decl *DefInterleav
 	// Determine type and length multiplier
 	for i, source := range decl.Sources {
 		// Lookup info of column being interleaved.
-		info := r.env.Column(module, source)
+		info := r.env.Column(module, source.Name)
 		if i == 0 {
 			length_multiplier = info.multiplier
 			datatype = info.datatype
@@ -290,7 +313,9 @@ func (r *resolver) finalisePermutationAssignment(module uint, decl *DefPermutati
 		ith := decl.Sources[i]
 		src := r.env.Column(module, ith.Name)
 		// Sanity check length multiplier
-		if i == 0 {
+		if i == 0 && src.datatype.AsUint() == nil {
+			errors = append(errors, *r.srcmap.SyntaxError(ith, "fixed-width type required"))
+		} else if i == 0 {
 			multiplier = src.multiplier
 		} else if multiplier != src.multiplier {
 			// Problem
@@ -357,53 +382,69 @@ func (r *resolver) resolveConstraintsInModule(module string, decls []Declaration
 
 // Resolve those variables appearing in either the guard or the body of this constraint.
 func (r *resolver) resolveDefConstraintInModule(module string, decl *DefConstraint) []SyntaxError {
-	var errors []SyntaxError
+	var (
+		errors  []SyntaxError
+		context = tr.VoidContext()
+	)
+	// Resolve guard
 	if decl.Guard != nil {
-		errors = r.resolveExpressionInModule(module, false, decl.Guard)
+		errors = r.resolveExpressionInModule(module, false, &context, decl.Guard)
 	}
 	// Resolve constraint body
-	errors = append(errors, r.resolveExpressionInModule(module, false, decl.Constraint)...)
+	errors = append(errors, r.resolveExpressionInModule(module, false, &context, decl.Constraint)...)
 	// Done
 	return errors
 }
 
 // Resolve those variables appearing in the body of this range constraint.
 func (r *resolver) resolveDefInRangeInModule(module string, decl *DefInRange) []SyntaxError {
-	var errors []SyntaxError
+	var (
+		errors  []SyntaxError
+		context = tr.VoidContext()
+	)
 	// Resolve property body
-	errors = append(errors, r.resolveExpressionInModule(module, false, decl.Expr)...)
+	errors = append(errors, r.resolveExpressionInModule(module, false, &context, decl.Expr)...)
 	// Done
 	return errors
 }
 
 // Resolve those variables appearing in the body of this lookup constraint.
 func (r *resolver) resolveDefLookupInModule(module string, decl *DefLookup) []SyntaxError {
-	var errors []SyntaxError
+	var (
+		errors        []SyntaxError
+		sourceContext = tr.VoidContext()
+		targetContext = tr.VoidContext()
+	)
+
 	// Resolve source expressions
-	errors = append(errors, r.resolveExpressionsInModule(module, true, decl.Sources)...)
+	errors = append(errors, r.resolveExpressionsInModule(module, true, &sourceContext, decl.Sources)...)
 	// Resolve target expressions
-	errors = append(errors, r.resolveExpressionsInModule(module, true, decl.Targets)...)
+	errors = append(errors, r.resolveExpressionsInModule(module, true, &targetContext, decl.Targets)...)
 	// Done
 	return errors
 }
 
 // Resolve those variables appearing in the body of this property assertion.
 func (r *resolver) resolveDefPropertyInModule(module string, decl *DefProperty) []SyntaxError {
-	var errors []SyntaxError
+	var (
+		errors  []SyntaxError
+		context = tr.VoidContext()
+	)
 	// Resolve property body
-	errors = append(errors, r.resolveExpressionInModule(module, false, decl.Assertion)...)
+	errors = append(errors, r.resolveExpressionInModule(module, false, &context, decl.Assertion)...)
 	// Done
 	return errors
 }
 
 // Resolve a sequence of zero or more expressions within a given module.  This
 // simply resolves each of the arguments in turn, collecting any errors arising.
-func (r *resolver) resolveExpressionsInModule(module string, global bool, args []Expr) []SyntaxError {
+func (r *resolver) resolveExpressionsInModule(module string, global bool,
+	context *tr.Context, args []Expr) []SyntaxError {
 	var errors []SyntaxError
 	// Visit each argument
 	for _, arg := range args {
 		if arg != nil {
-			errs := r.resolveExpressionInModule(module, global, arg)
+			errs := r.resolveExpressionInModule(module, global, context, arg)
 			errors = append(errors, errs...)
 		}
 	}
@@ -416,25 +457,25 @@ func (r *resolver) resolveExpressionsInModule(module string, global bool, args [
 // variable accesses.  As above, the goal is ensure variable refers to something
 // that was declared and, more specifically, what kind of access it is (e.g.
 // column access, constant access, etc).
-func (r *resolver) resolveExpressionInModule(module string, global bool, expr Expr) []SyntaxError {
+func (r *resolver) resolveExpressionInModule(module string, global bool, context *tr.Context, expr Expr) []SyntaxError {
 	if _, ok := expr.(*Constant); ok {
 		return nil
 	} else if v, ok := expr.(*Add); ok {
-		return r.resolveExpressionsInModule(module, global, v.Args)
+		return r.resolveExpressionsInModule(module, global, context, v.Args)
 	} else if v, ok := expr.(*Exp); ok {
-		return r.resolveExpressionInModule(module, global, v.Arg)
+		return r.resolveExpressionInModule(module, global, context, v.Arg)
 	} else if v, ok := expr.(*IfZero); ok {
-		return r.resolveExpressionsInModule(module, global, []Expr{v.Condition, v.TrueBranch, v.FalseBranch})
+		return r.resolveExpressionsInModule(module, global, context, []Expr{v.Condition, v.TrueBranch, v.FalseBranch})
 	} else if v, ok := expr.(*List); ok {
-		return r.resolveExpressionsInModule(module, global, v.Args)
+		return r.resolveExpressionsInModule(module, global, context, v.Args)
 	} else if v, ok := expr.(*Mul); ok {
-		return r.resolveExpressionsInModule(module, global, v.Args)
+		return r.resolveExpressionsInModule(module, global, context, v.Args)
 	} else if v, ok := expr.(*Normalise); ok {
-		return r.resolveExpressionInModule(module, global, v.Arg)
+		return r.resolveExpressionInModule(module, global, context, v.Arg)
 	} else if v, ok := expr.(*Sub); ok {
-		return r.resolveExpressionsInModule(module, global, v.Args)
+		return r.resolveExpressionsInModule(module, global, context, v.Args)
 	} else if v, ok := expr.(*VariableAccess); ok {
-		return r.resolveVariableInModule(module, global, v)
+		return r.resolveVariableInModule(module, global, context, v)
 	} else {
 		return r.srcmap.SyntaxErrors(expr, "unknown expression")
 	}
@@ -443,18 +484,25 @@ func (r *resolver) resolveExpressionInModule(module string, global bool, expr Ex
 // Resolve a specific variable access contained within some expression which, in
 // turn, is contained within some module.  Note, qualified accesses are only
 // permitted in a global context.
-func (r *resolver) resolveVariableInModule(module string, global bool, expr *VariableAccess) []SyntaxError {
+func (r *resolver) resolveVariableInModule(module string, global bool, context *tr.Context,
+	expr *VariableAccess) []SyntaxError {
 	// Check whether this is a qualified access, or not.
-	if global && expr.Module != nil {
-		module = *expr.Module
-	} else if expr.Module != nil {
+	if !global && expr.Module != nil {
 		return r.srcmap.SyntaxErrors(expr, "qualified access not permitted here")
+	} else if expr.Module != nil && !r.env.HasModule(*expr.Module) {
+		return r.srcmap.SyntaxErrors(expr, fmt.Sprintf("unknown module %s", *expr.Module))
+	} else if expr.Module != nil {
+		module = *expr.Module
 	}
-	// FIXME: handle qualified variable accesses
+	//
 	mid := r.env.Module(module)
 	// Attempt resolve as a column access in enclosing module
 	if cinfo, ok := r.env.LookupColumn(mid, expr.Name); ok {
 		ctx := tr.NewContext(mid, cinfo.multiplier)
+		// Update context
+		if *context = context.Join(ctx); context.IsConflicted() {
+			return r.srcmap.SyntaxErrors(expr, "conflicting context")
+		}
 		// Register the binding to complete resolution.
 		expr.Binding = &Binder{true, ctx, cinfo.cid}
 		// Done

pkg/corset/translator.go

@@ -230,7 +230,7 @@ func (t *translator) translateDefInterleaved(decl *DefInterleaved, module uint)
 	info := t.env.Column(module, decl.Target)
 	// Determine source column identifiers
 	for i, source := range decl.Sources {
-		sources[i] = t.env.Column(module, source).cid
+		sources[i] = t.env.Column(module, source.Name).cid
 	}
 	// Construct context for this assignment
 	context := tr.NewContext(module, info.multiplier)