diff --git a/pkg/corset/ast.go b/pkg/corset/ast.go
index 040884c..4ce3e9f 100644
--- a/pkg/corset/ast.go
+++ b/pkg/corset/ast.go
@@ -175,7 +175,7 @@ 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.
@@ -183,7 +183,7 @@ type DefInterleaved struct {
 // 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
diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go
index 843e4d5..0996d96 100644
--- a/pkg/corset/parser.go
+++ b/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,7 +335,7 @@ 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)
@@ -339,7 +343,7 @@ func (p *Parser) parseDefInterleaved(elements []sexp.SExp) (*DefInterleaved, *Sy
 			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,7 +412,7 @@ 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
 		}
 	}
@@ -416,7 +420,7 @@ func (p *Parser) parseDefPermutation(elements []sexp.SExp) (*DefPermutation, *Sy
 	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
diff --git a/pkg/corset/resolver.go b/pkg/corset/resolver.go
index 070db2c..9a58236 100644
--- a/pkg/corset/resolver.go
+++ b/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
diff --git a/pkg/corset/translator.go b/pkg/corset/translator.go
index b8a16b6..fd62800 100644
--- a/pkg/corset/translator.go
+++ b/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)
diff --git a/pkg/test/invalid_corset_test.go b/pkg/test/invalid_corset_test.go
new file mode 100644
index 0000000..9622bd2
--- /dev/null
+++ b/pkg/test/invalid_corset_test.go
@@ -0,0 +1,269 @@
+package test
+
+import (
+	"fmt"
+	"os"
+	"testing"
+
+	"github.com/consensys/go-corset/pkg/corset"
+	"github.com/consensys/go-corset/pkg/sexp"
+)
+
+// Determines the (relative) location of the test directory.  That is
+// where the corset test files (lisp) and the corresponding traces
+// (accepts/rejects) are found.
+const InvalidTestDir = "../../testdata"
+
+// ===================================================================
+// Basic Tests
+// ===================================================================
+
+func Test_Invalid_Basic_01(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_01")
+}
+
+func Test_Invalid_Basic_02(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_02")
+}
+
+func Test_Invalid_Basic_03(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_03")
+}
+
+func Test_Invalid_Basic_04(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_04")
+}
+
+func Test_Invalid_Basic_05(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_05")
+}
+
+func Test_Invalid_Basic_06(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_06")
+}
+
+func Test_Invalid_Basic_07(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_07")
+}
+
+func Test_Invalid_Basic_08(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_08")
+}
+
+func Test_Invalid_Basic_09(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_09")
+}
+
+func Test_Invalid_Basic_10(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_10")
+}
+
+func Test_Invalid_Basic_11(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_11")
+}
+
+func Test_Invalid_Basic_12(t *testing.T) {
+	CheckInvalid(t, "basic_invalid_12")
+}
+
+// ===================================================================
+// Property Tests
+// ===================================================================
+func Test_Invalid_Property_01(t *testing.T) {
+	CheckInvalid(t, "property_invalid_01")
+}
+
+func Test_Invalid_Property_02(t *testing.T) {
+	CheckInvalid(t, "property_invalid_02")
+}
+
+// ===================================================================
+// Shift Tests
+// ===================================================================
+
+func Test_Invalid_Shift_01(t *testing.T) {
+	CheckInvalid(t, "shift_invalid_01")
+}
+
+func Test_Invalid_Shift_02(t *testing.T) {
+	CheckInvalid(t, "shift_invalid_02")
+}
+
+// ===================================================================
+// Normalisation Tests
+// ===================================================================
+
+func Test_Invalid_Norm_01(t *testing.T) {
+	CheckInvalid(t, "norm_invalid_01")
+}
+
+// ===================================================================
+// If-Zero
+// ===================================================================
+
+func Test_Invalid_If_01(t *testing.T) {
+	CheckInvalid(t, "if_invalid_01")
+}
+
+func Test_Invalid_If_02(t *testing.T) {
+	CheckInvalid(t, "if_invalid_02")
+}
+
+// ===================================================================
+// Range Constraints
+// ===================================================================
+
+func Test_Invalid_Range_01(t *testing.T) {
+	CheckInvalid(t, "range_invalid_01")
+}
+
+func Test_Invalid_Range_02(t *testing.T) {
+	CheckInvalid(t, "range_invalid_02")
+}
+
+func Test_Invalid_Range_03(t *testing.T) {
+	CheckInvalid(t, "range_invalid_03")
+}
+
+func Test_Invalid_Range_04(t *testing.T) {
+	CheckInvalid(t, "range_invalid_04")
+}
+
+// ===================================================================
+// Modules
+// ===================================================================
+
+func Test_Invalid_Module_01(t *testing.T) {
+	CheckInvalid(t, "module_invalid_01")
+}
+
+// ===================================================================
+// Permutations
+// ===================================================================
+
+func Test_Invalid_Permute_01(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_01")
+}
+
+func Test_Invalid_Permute_02(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_02")
+}
+
+func Test_Invalid_Permute_03(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_03")
+}
+
+func Test_Invalid_Permute_04(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_04")
+}
+
+func Test_Invalid_Permute_05(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_05")
+}
+
+func Test_Invalid_Permute_06(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_06")
+}
+func Test_Invalid_Permute_07(t *testing.T) {
+	CheckInvalid(t, "permute_invalid_07")
+}
+
+// ===================================================================
+// Lookups
+// ===================================================================
+
+func Test_Invalid_Lookup_01(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_01")
+}
+
+func Test_Invalid_Lookup_02(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_02")
+}
+func Test_Invalid_Lookup_03(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_03")
+}
+
+func Test_Invalid_Lookup_04(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_04")
+}
+
+func Test_Invalid_Lookup_05(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_05")
+}
+func Test_Invalid_Lookup_06(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_06")
+}
+func Test_Invalid_Lookup_07(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_07")
+}
+func Test_Invalid_Lookup_08(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_08")
+}
+func Test_Invalid_Lookup_09(t *testing.T) {
+	CheckInvalid(t, "lookup_invalid_09")
+}
+
+// ===================================================================
+// Interleavings
+// ===================================================================
+
+func Test_Invalid_Interleave_01(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_01")
+}
+
+func Test_Invalid_Interleave_02(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_02")
+}
+
+func Test_Invalid_Interleave_03(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_03")
+}
+
+func Test_Invalid_Interleave_04(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_04")
+}
+
+func Test_Invalid_Interleave_05(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_05")
+}
+
+func Test_Invalid_Interleave_06(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_06")
+}
+
+func Test_Invalid_Interleave_07(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_07")
+}
+
+func Test_Invalid_Interleave_08(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_08")
+}
+
+func Test_Invalid_Interleave_09(t *testing.T) {
+	CheckInvalid(t, "interleave_invalid_09")
+}
+
+// ===================================================================
+// Test Helpers
+// ===================================================================
+
+// Check that a given source file fails to compiler.
+func CheckInvalid(t *testing.T, test string) {
+	filename := fmt.Sprintf("%s.lisp", test)
+	// Enable testing each trace in parallel
+	t.Parallel()
+	// Read constraints file
+	bytes, err := os.ReadFile(fmt.Sprintf("%s/%s", InvalidTestDir, filename))
+	// Check test file read ok
+	if err != nil {
+		t.Fatal(err)
+	}
+	// Package up as source file
+	srcfile := sexp.NewSourceFile(filename, bytes)
+	// Parse terms into an HIR schema
+	_, errs := corset.CompileSourceFile(srcfile)
+	// Check program did not compile!
+	if len(errs) == 0 {
+		t.Fatalf("Error %s should not have compiled\n", filename)
+	}
+}
diff --git a/pkg/test/ir_test.go b/pkg/test/valid_corset_test.go
similarity index 100%
rename from pkg/test/ir_test.go
rename to pkg/test/valid_corset_test.go
diff --git a/testdata/basic_invalid_01.lisp b/testdata/basic_invalid_01.lisp
new file mode 100644
index 0000000..7530ad0
--- /dev/null
+++ b/testdata/basic_invalid_01.lisp
@@ -0,0 +1 @@
+(defcolumns X ())
diff --git a/testdata/basic_invalid_02.lisp b/testdata/basic_invalid_02.lisp
new file mode 100644
index 0000000..8e36c81
--- /dev/null
+++ b/testdata/basic_invalid_02.lisp
@@ -0,0 +1 @@
+(defcolumns (X :odd))
diff --git a/testdata/basic_invalid_03.lisp b/testdata/basic_invalid_03.lisp
new file mode 100644
index 0000000..e339e63
--- /dev/null
+++ b/testdata/basic_invalid_03.lisp
@@ -0,0 +1 @@
+(defcolumns (X :i32 :odd))
diff --git a/testdata/basic_invalid_04.lisp b/testdata/basic_invalid_04.lisp
new file mode 100644
index 0000000..26192a8
--- /dev/null
+++ b/testdata/basic_invalid_04.lisp
@@ -0,0 +1 @@
+(defcolumns X X)
diff --git a/testdata/basic_invalid_05.lisp b/testdata/basic_invalid_05.lisp
new file mode 100644
index 0000000..6205d70
--- /dev/null
+++ b/testdata/basic_invalid_05.lisp
@@ -0,0 +1,2 @@
+(defcolumns X)
+(defcolumns X)
diff --git a/testdata/basic_invalid_06.lisp b/testdata/basic_invalid_06.lisp
new file mode 100644
index 0000000..3afd6d4
--- /dev/null
+++ b/testdata/basic_invalid_06.lisp
@@ -0,0 +1,3 @@
+(defcolumns X)
+
+(defconstraint c () Y)
diff --git a/testdata/basic_invalid_07.lisp b/testdata/basic_invalid_07.lisp
new file mode 100644
index 0000000..a058f51
--- /dev/null
+++ b/testdata/basic_invalid_07.lisp
@@ -0,0 +1,3 @@
+(defcolumns X)
+
+(defconstraint c () (+ X Y))
diff --git a/testdata/basic_invalid_08.lisp b/testdata/basic_invalid_08.lisp
new file mode 100644
index 0000000..81bc9c4
--- /dev/null
+++ b/testdata/basic_invalid_08.lisp
@@ -0,0 +1,3 @@
+(defcolumns X)
+
+(defconstraint c (:guard Y) X)
diff --git a/testdata/basic_invalid_09.lisp b/testdata/basic_invalid_09.lisp
new file mode 100644
index 0000000..9f05e4a
--- /dev/null
+++ b/testdata/basic_invalid_09.lisp
@@ -0,0 +1,4 @@
+(module m1)
+(defcolumns X)
+
+(defconstraint c () m1.X)
diff --git a/testdata/basic_invalid_10.lisp b/testdata/basic_invalid_10.lisp
new file mode 100644
index 0000000..536bb6b
--- /dev/null
+++ b/testdata/basic_invalid_10.lisp
@@ -0,0 +1,4 @@
+(module m1)
+(defcolumns X)
+
+(defconstraint c (:guard m1.X) X)
diff --git a/testdata/basic_invalid_11.lisp b/testdata/basic_invalid_11.lisp
new file mode 100644
index 0000000..e00982f
--- /dev/null
+++ b/testdata/basic_invalid_11.lisp
@@ -0,0 +1,2 @@
+(defcolumns X)
+(defconstraint (c) () X)
diff --git a/testdata/basic_invalid_12.lisp b/testdata/basic_invalid_12.lisp
new file mode 100644
index 0000000..3af8f25
--- /dev/null
+++ b/testdata/basic_invalid_12.lisp
@@ -0,0 +1 @@
+(module)
diff --git a/testdata/if_invalid_01.lisp b/testdata/if_invalid_01.lisp
new file mode 100644
index 0000000..ab17409
--- /dev/null
+++ b/testdata/if_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns A)
+(defconstraint c1 () (if A))
diff --git a/testdata/if_invalid_02.lisp b/testdata/if_invalid_02.lisp
new file mode 100644
index 0000000..16bc840
--- /dev/null
+++ b/testdata/if_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns A B C D)
+(defconstraint c1 () (if A B C D))
diff --git a/testdata/interleave_invalid_01.lisp b/testdata/interleave_invalid_01.lisp
new file mode 100644
index 0000000..8032982
--- /dev/null
+++ b/testdata/interleave_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y Z)
+(definterleaved Z (X Y))
diff --git a/testdata/interleave_invalid_02.lisp b/testdata/interleave_invalid_02.lisp
new file mode 100644
index 0000000..e12b5aa
--- /dev/null
+++ b/testdata/interleave_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(definterleaved () (X Y))
diff --git a/testdata/interleave_invalid_03.lisp b/testdata/interleave_invalid_03.lisp
new file mode 100644
index 0000000..169140b
--- /dev/null
+++ b/testdata/interleave_invalid_03.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(definterleaved Z ((X) Y))
diff --git a/testdata/interleave_invalid_04.lisp b/testdata/interleave_invalid_04.lisp
new file mode 100644
index 0000000..549e683
--- /dev/null
+++ b/testdata/interleave_invalid_04.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved A (X Y))
+(definterleaved B (A Y))
diff --git a/testdata/interleave_invalid_05.lisp b/testdata/interleave_invalid_05.lisp
new file mode 100644
index 0000000..8a045a7
--- /dev/null
+++ b/testdata/interleave_invalid_05.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved A (X Y))
+(definterleaved B (X A))
diff --git a/testdata/interleave_invalid_06.lisp b/testdata/interleave_invalid_06.lisp
new file mode 100644
index 0000000..9d21176
--- /dev/null
+++ b/testdata/interleave_invalid_06.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved A (X Y))
+(defconstraint c1 () (+ A X))
diff --git a/testdata/interleave_invalid_07.lisp b/testdata/interleave_invalid_07.lisp
new file mode 100644
index 0000000..4fcf933
--- /dev/null
+++ b/testdata/interleave_invalid_07.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved A (X Y))
+(defproperty p1 (+ A X))
diff --git a/testdata/interleave_invalid_08.lisp b/testdata/interleave_invalid_08.lisp
new file mode 100644
index 0000000..ca86f65
--- /dev/null
+++ b/testdata/interleave_invalid_08.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved A (X Y))
+(deflookup l1 (A X) (Y Y))
diff --git a/testdata/interleave_invalid_09.lisp b/testdata/interleave_invalid_09.lisp
new file mode 100644
index 0000000..8dd29cb
--- /dev/null
+++ b/testdata/interleave_invalid_09.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved Z (X Y))
+(defpermutation (A B) ((+ Z) (+ Y)))
diff --git a/testdata/interleave_invalid_10.lisp b/testdata/interleave_invalid_10.lisp
new file mode 100644
index 0000000..1362992
--- /dev/null
+++ b/testdata/interleave_invalid_10.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+(definterleaved Z (X Y))
+(defpermutation (A B) ((+ X) (+ Z)))
diff --git a/testdata/lookup_invalid_01.lisp b/testdata/lookup_invalid_01.lisp
new file mode 100644
index 0000000..5ef5098
--- /dev/null
+++ b/testdata/lookup_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(deflookup test (Y) (X X))
diff --git a/testdata/lookup_invalid_02.lisp b/testdata/lookup_invalid_02.lisp
new file mode 100644
index 0000000..2ca809d
--- /dev/null
+++ b/testdata/lookup_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(deflookup test (Y Y) (X))
diff --git a/testdata/lookup_invalid_03.lisp b/testdata/lookup_invalid_03.lisp
new file mode 100644
index 0000000..38e1c64
--- /dev/null
+++ b/testdata/lookup_invalid_03.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(deflookup () (Y) (X))
diff --git a/testdata/lookup_invalid_04.lisp b/testdata/lookup_invalid_04.lisp
new file mode 100644
index 0000000..a3ebf08
--- /dev/null
+++ b/testdata/lookup_invalid_04.lisp
@@ -0,0 +1,5 @@
+(defcolumns X)
+(deflookup test (X) (Y))
+
+(module m1)
+(defcolumns Y)
diff --git a/testdata/lookup_invalid_05.lisp b/testdata/lookup_invalid_05.lisp
new file mode 100644
index 0000000..9064102
--- /dev/null
+++ b/testdata/lookup_invalid_05.lisp
@@ -0,0 +1,5 @@
+(defcolumns X)
+(deflookup test (Y) (X))
+
+(module m1)
+(defcolumns Y)
diff --git a/testdata/lookup_invalid_06.lisp b/testdata/lookup_invalid_06.lisp
new file mode 100644
index 0000000..a9c2d4c
--- /dev/null
+++ b/testdata/lookup_invalid_06.lisp
@@ -0,0 +1,8 @@
+(defcolumns X Y)
+(deflookup test (m1.A m2.B) (X Y))
+
+(module m1)
+(defcolumns A)
+
+(module m2)
+(defcolumns B)
diff --git a/testdata/lookup_invalid_07.lisp b/testdata/lookup_invalid_07.lisp
new file mode 100644
index 0000000..2f498ee
--- /dev/null
+++ b/testdata/lookup_invalid_07.lisp
@@ -0,0 +1,8 @@
+(defcolumns X)
+(deflookup test ((+ m1.A m2.B)) (X))
+
+(module m1)
+(defcolumns A)
+
+(module m2)
+(defcolumns B)
diff --git a/testdata/lookup_invalid_08.lisp b/testdata/lookup_invalid_08.lisp
new file mode 100644
index 0000000..6c7529d
--- /dev/null
+++ b/testdata/lookup_invalid_08.lisp
@@ -0,0 +1,5 @@
+(defcolumns X)
+(deflookup test ((+ m2.A 1)) (X))
+
+(module m1)
+(defcolumns A)
diff --git a/testdata/lookup_invalid_09.lisp b/testdata/lookup_invalid_09.lisp
new file mode 100644
index 0000000..12d932f
--- /dev/null
+++ b/testdata/lookup_invalid_09.lisp
@@ -0,0 +1,5 @@
+(defcolumns X)
+(deflookup test (X) ((+ m2.A 1)))
+
+(module m1)
+(defcolumns A)
diff --git a/testdata/module_invalid_01.lisp b/testdata/module_invalid_01.lisp
new file mode 100644
index 0000000..900cf2d
--- /dev/null
+++ b/testdata/module_invalid_01.lisp
@@ -0,0 +1,5 @@
+(module m1)
+(defcolumns X)
+
+(module m2)
+(definrange X 2)
diff --git a/testdata/norm_invalid_01.lisp b/testdata/norm_invalid_01.lisp
new file mode 100644
index 0000000..24add0c
--- /dev/null
+++ b/testdata/norm_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns ST A)
+(defconstraint c1 () (* ST (- 1 (~ A 0))))
diff --git a/testdata/permute_invalid_01.lisp b/testdata/permute_invalid_01.lisp
new file mode 100644
index 0000000..b486f28
--- /dev/null
+++ b/testdata/permute_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns (X :i16@prove))
+(defpermutation (Z) ())
diff --git a/testdata/permute_invalid_02.lisp b/testdata/permute_invalid_02.lisp
new file mode 100644
index 0000000..cba2d28
--- /dev/null
+++ b/testdata/permute_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns (X :i16@prove))
+(defpermutation (Z) (X X))
diff --git a/testdata/permute_invalid_03.lisp b/testdata/permute_invalid_03.lisp
new file mode 100644
index 0000000..74cf7e5
--- /dev/null
+++ b/testdata/permute_invalid_03.lisp
@@ -0,0 +1,2 @@
+(defcolumns (X :i16@prove))
+(defpermutation (Z) ((X)))
diff --git a/testdata/permute_invalid_04.lisp b/testdata/permute_invalid_04.lisp
new file mode 100644
index 0000000..0284c87
--- /dev/null
+++ b/testdata/permute_invalid_04.lisp
@@ -0,0 +1,2 @@
+(defcolumns (X :i16@prove))
+(defpermutation (Z) ((? X)))
diff --git a/testdata/permute_invalid_05.lisp b/testdata/permute_invalid_05.lisp
new file mode 100644
index 0000000..70dcc8e
--- /dev/null
+++ b/testdata/permute_invalid_05.lisp
@@ -0,0 +1,3 @@
+(module m1)
+(defcolumns (X :i16@prove))
+(defpermutation (Z) ((+ m1.X)))
diff --git a/testdata/permute_invalid_06.lisp b/testdata/permute_invalid_06.lisp
new file mode 100644
index 0000000..4f3d0a0
--- /dev/null
+++ b/testdata/permute_invalid_06.lisp
@@ -0,0 +1,2 @@
+(defcolumns X)
+(defpermutation (Z) ((+ X)))
diff --git a/testdata/permute_invalid_07.lisp b/testdata/permute_invalid_07.lisp
new file mode 100644
index 0000000..fb1d06f
--- /dev/null
+++ b/testdata/permute_invalid_07.lisp
@@ -0,0 +1,3 @@
+(module m1)
+(defcolumns (X :i16))
+(defpermutation (Z) (X))
diff --git a/testdata/property_invalid_01.lisp b/testdata/property_invalid_01.lisp
new file mode 100644
index 0000000..7dd0672
--- /dev/null
+++ b/testdata/property_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns X)
+(defproperty (c) X)
diff --git a/testdata/property_invalid_02.lisp b/testdata/property_invalid_02.lisp
new file mode 100644
index 0000000..ae733bd
--- /dev/null
+++ b/testdata/property_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns X)
+(defproperty p1 X X)
diff --git a/testdata/range_invalid_01.lisp b/testdata/range_invalid_01.lisp
new file mode 100644
index 0000000..c93036f
--- /dev/null
+++ b/testdata/range_invalid_01.lisp
@@ -0,0 +1,3 @@
+(defcolumns X Y)
+
+(definrange X)
diff --git a/testdata/range_invalid_02.lisp b/testdata/range_invalid_02.lisp
new file mode 100644
index 0000000..c994a0f
--- /dev/null
+++ b/testdata/range_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(definrange X Y)
diff --git a/testdata/range_invalid_03.lisp b/testdata/range_invalid_03.lisp
new file mode 100644
index 0000000..145cf8d
--- /dev/null
+++ b/testdata/range_invalid_03.lisp
@@ -0,0 +1,2 @@
+(defcolumns X Y)
+(definrange X 2 Y)
diff --git a/testdata/range_invalid_04.lisp b/testdata/range_invalid_04.lisp
new file mode 100644
index 0000000..f8f667e
--- /dev/null
+++ b/testdata/range_invalid_04.lisp
@@ -0,0 +1,2 @@
+(defcolumns X)
+(definrange Y 2)
diff --git a/testdata/shift_invalid_01.lisp b/testdata/shift_invalid_01.lisp
new file mode 100644
index 0000000..9c19c4b
--- /dev/null
+++ b/testdata/shift_invalid_01.lisp
@@ -0,0 +1,2 @@
+(defcolumns X ST)
+(defconstraint c1 () (* ST (shift X X)))
diff --git a/testdata/shift_invalid_02.lisp b/testdata/shift_invalid_02.lisp
new file mode 100644
index 0000000..e9eb289
--- /dev/null
+++ b/testdata/shift_invalid_02.lisp
@@ -0,0 +1,2 @@
+(defcolumns X ST)
+(defconstraint c1 () (* ST (shift X)))