diff --git a/pkg/air/gadgets/bits.go b/pkg/air/gadgets/bits.go
index 0b961c0a..8e8c131a 100644
--- a/pkg/air/gadgets/bits.go
+++ b/pkg/air/gadgets/bits.go
@@ -52,7 +52,8 @@ func ApplyBitwidthGadget(col string, nbits uint, schema *air.Schema) {
 	// Construct X == (X:0 * 1) + ... + (X:n * 2^n)
 	X := air.NewColumnAccess(col, 0)
 	eq := X.Equate(sum)
-	schema.AddVanishingConstraint(col, nil, eq)
+	// Construct column name
+	schema.AddVanishingConstraint(fmt.Sprintf("%s:u%d", col, nbits), nil, eq)
 	// Finally, add the necessary byte decomposition computation.
 	schema.AddComputation(table.NewByteDecomposition(col, nbits))
 }
diff --git a/pkg/air/schema.go b/pkg/air/schema.go
index 2580d834..4c2a4c19 100644
--- a/pkg/air/schema.go
+++ b/pkg/air/schema.go
@@ -109,9 +109,9 @@ func (p *Schema) RequiredSpillage() uint {
 // Padding values are placed either at the front or the back of a given
 // column, depending on their interpretation.
 func (p *Schema) ApplyPadding(n uint, tr table.Trace) {
-	tr.Pad(n, func(j int) (bool, *fr.Element) {
-		value := tr.GetByIndex(j, 0)
-		return true, value
+	tr.Pad(n, func(j int) *fr.Element {
+		// Extract front value to use for padding.
+		return tr.GetByIndex(j, 0)
 	})
 }
 
@@ -179,7 +179,9 @@ func (p *Schema) IsOutputTrace(tr table.Trace) error {
 // AddColumn appends a new data column which is either synthetic or
 // not.  A synthetic column is one which has been introduced by the
 // process of lowering from HIR / MIR to AIR.  That is, it is not a
-// column which was original specified by the user.
+// column which was original specified by the user.  Columns also support a
+// "padding sign", which indicates whether padding should occur at the front
+// (positive sign) or the back (negative sign).
 func (p *Schema) AddColumn(name string, synthetic bool) {
 	// NOTE: the air level has no ability to enforce the type specified for a
 	// given column.
diff --git a/pkg/cmd/check.go b/pkg/cmd/check.go
index 2bedcd56..f0ba6dc2 100644
--- a/pkg/cmd/check.go
+++ b/pkg/cmd/check.go
@@ -30,6 +30,7 @@ var checkCmd = &cobra.Command{
 		cfg.mir = getFlag(cmd, "mir")
 		cfg.hir = getFlag(cmd, "hir")
 		cfg.expand = !getFlag(cmd, "raw")
+		cfg.report = getFlag(cmd, "report")
 		cfg.spillage = getInt(cmd, "spillage")
 		cfg.padding.Right = getUint(cmd, "padding")
 		// TODO: support true ranges
@@ -62,6 +63,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 report details of the failure (e.g. for
+	// debugging purposes).
+	report bool
 }
 
 // Check a given trace is consistently accepted (or rejected) at the different
@@ -87,10 +91,10 @@ func checkTraceWithLowering(tr *table.ArrayTrace, schema *hir.Schema, cfg checkC
 }
 
 func checkTraceWithLoweringHir(tr *table.ArrayTrace, hirSchema *hir.Schema, cfg checkConfig) {
-	errHIR := checkTrace(tr, hirSchema, cfg)
+	trHIR, errHIR := checkTrace(tr, hirSchema, cfg)
 	//
 	if errHIR != nil {
-		reportError(errHIR, "HIR")
+		reportError("HIR", trHIR, errHIR, cfg)
 		os.Exit(1)
 	}
 }
@@ -99,10 +103,10 @@ func checkTraceWithLoweringMir(tr *table.ArrayTrace, hirSchema *hir.Schema, cfg
 	// Lower HIR => MIR
 	mirSchema := hirSchema.LowerToMir()
 	// Check trace
-	errMIR := checkTrace(tr, mirSchema, cfg)
+	trMIR, errMIR := checkTrace(tr, mirSchema, cfg)
 	//
 	if errMIR != nil {
-		reportError(errMIR, "MIR")
+		reportError("MIR", trMIR, errMIR, cfg)
 		os.Exit(1)
 	}
 }
@@ -112,10 +116,10 @@ func checkTraceWithLoweringAir(tr *table.ArrayTrace, hirSchema *hir.Schema, cfg
 	mirSchema := hirSchema.LowerToMir()
 	// Lower MIR => AIR
 	airSchema := mirSchema.LowerToAir()
-	errAIR := checkTrace(tr, airSchema, cfg)
+	trAIR, errAIR := checkTrace(tr, airSchema, cfg)
 	//
 	if errAIR != nil {
-		reportError(errAIR, "AIR")
+		reportError("AIR", trAIR, errAIR, cfg)
 		os.Exit(1)
 	}
 }
@@ -128,9 +132,9 @@ func checkTraceWithLoweringDefault(tr *table.ArrayTrace, hirSchema *hir.Schema,
 	// Lower MIR => AIR
 	airSchema := mirSchema.LowerToAir()
 	//
-	errHIR := checkTrace(tr, hirSchema, cfg)
-	errMIR := checkTrace(tr, mirSchema, cfg)
-	errAIR := checkTrace(tr, airSchema, cfg)
+	trHIR, errHIR := checkTrace(tr, hirSchema, cfg)
+	trMIR, errMIR := checkTrace(tr, mirSchema, cfg)
+	trAIR, errAIR := checkTrace(tr, airSchema, cfg)
 	//
 	if errHIR != nil || errMIR != nil || errAIR != nil {
 		strHIR := toErrorString(errHIR)
@@ -140,16 +144,16 @@ func checkTraceWithLoweringDefault(tr *table.ArrayTrace, hirSchema *hir.Schema,
 		if strHIR == strMIR && strMIR == strAIR {
 			fmt.Println(errHIR)
 		} else {
-			reportError(errHIR, "HIR")
-			reportError(errMIR, "MIR")
-			reportError(errAIR, "AIR")
+			reportError("HIR", trHIR, errHIR, cfg)
+			reportError("MIR", trMIR, errMIR, cfg)
+			reportError("AIR", trAIR, errAIR, cfg)
 		}
 
 		os.Exit(1)
 	}
 }
 
-func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) error {
+func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) (table.Trace, error) {
 	if cfg.expand {
 		// Clone to prevent interefence with subsequent checks
 		tr = tr.Clone()
@@ -163,13 +167,13 @@ func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) erro
 		}
 		// Expand trace
 		if err := schema.ExpandTrace(tr); err != nil {
-			return err
+			return tr, err
 		}
 	}
 	// Check whether padding requested
 	if cfg.padding.Left == 0 && cfg.padding.Right == 0 {
 		// No padding requested.  Therefore, we can avoid a clone in this case.
-		return schema.Accepts(tr)
+		return tr, schema.Accepts(tr)
 	}
 	// Apply padding
 	for n := cfg.padding.Left; n <= cfg.padding.Right; n++ {
@@ -179,11 +183,11 @@ func checkTrace(tr *table.ArrayTrace, schema table.Schema, cfg checkConfig) erro
 		schema.ApplyPadding(n, ptr)
 		// Check whether accepted or not.
 		if err := schema.Accepts(ptr); err != nil {
-			return err
+			return ptr, err
 		}
 	}
 	// Done
-	return nil
+	return nil, nil
 }
 
 func toErrorString(err error) string {
@@ -194,7 +198,11 @@ func toErrorString(err error) string {
 	return err.Error()
 }
 
-func reportError(err error, ir string) {
+func reportError(ir string, tr table.Trace, err error, cfg checkConfig) {
+	if cfg.report {
+		table.PrintTrace(tr)
+	}
+
 	if err != nil {
 		fmt.Printf("%s: %s\n", ir, err)
 	} else {
@@ -204,6 +212,7 @@ func reportError(err error, ir string) {
 
 func init() {
 	rootCmd.AddCommand(checkCmd)
+	checkCmd.Flags().Bool("report", false, "report details of failure for debugging")
 	checkCmd.Flags().Bool("raw", false, "assume input trace already expanded")
 	checkCmd.Flags().Bool("hir", false, "check at HIR level")
 	checkCmd.Flags().Bool("mir", false, "check at MIR level")
diff --git a/pkg/hir/parser.go b/pkg/hir/parser.go
index f7dd869d..292d08d2 100644
--- a/pkg/hir/parser.go
+++ b/pkg/hir/parser.go
@@ -150,6 +150,10 @@ func (p *hirParser) parseSortedPermutationDeclaration(elements []sexp.SExp) erro
 		if strings.HasPrefix(sortName, "+") {
 			signs[i] = true
 		} else if strings.HasPrefix(sortName, "-") {
+			if i == 0 {
+				return p.translator.SyntaxError(source, "sorted permutation requires ascending first column")
+			}
+
 			signs[i] = false
 		} else {
 			return p.translator.SyntaxError(source, "malformed sort direction")
diff --git a/pkg/hir/schema.go b/pkg/hir/schema.go
index 481e5922..5a177c6a 100644
--- a/pkg/hir/schema.go
+++ b/pkg/hir/schema.go
@@ -113,9 +113,8 @@ func (p *Schema) RequiredSpillage() uint {
 // Padding values are placed either at the front or the back of a given
 // column, depending on their interpretation.
 func (p *Schema) ApplyPadding(n uint, tr table.Trace) {
-	tr.Pad(n, func(j int) (bool, *fr.Element) {
-		value := tr.GetByIndex(j, 0)
-		return true, value
+	tr.Pad(n, func(j int) *fr.Element {
+		return tr.GetByIndex(j, 0)
 	})
 }
 
diff --git a/pkg/mir/schema.go b/pkg/mir/schema.go
index 831d340f..53cf3211 100644
--- a/pkg/mir/schema.go
+++ b/pkg/mir/schema.go
@@ -80,9 +80,8 @@ func (p *Schema) RequiredSpillage() uint {
 // Padding values are placed either at the front or the back of a given
 // column, depending on their interpretation.
 func (p *Schema) ApplyPadding(n uint, tr table.Trace) {
-	tr.Pad(n, func(j int) (bool, *fr.Element) {
-		value := tr.GetByIndex(j, 0)
-		return true, value
+	tr.Pad(n, func(j int) *fr.Element {
+		return tr.GetByIndex(j, 0)
 	})
 }
 
diff --git a/pkg/table/printer.go b/pkg/table/printer.go
new file mode 100644
index 00000000..22775d89
--- /dev/null
+++ b/pkg/table/printer.go
@@ -0,0 +1,71 @@
+package table
+
+import (
+	"fmt"
+	"unicode/utf8"
+)
+
+// PrintTrace prints a trace in a more human-friendly fashion.
+func PrintTrace(tr Trace) {
+	n := tr.Width()
+	//
+	rows := make([][]string, n)
+	for i := uint(0); i < n; i++ {
+		rows[i] = traceColumnData(tr, i)
+	}
+	//
+	widths := traceRowWidths(tr.Height(), rows)
+	//
+	printHorizontalRule(widths)
+	//
+	for _, r := range rows {
+		printTraceRow(r, widths)
+		printHorizontalRule(widths)
+	}
+}
+
+func traceColumnData(tr Trace, col uint) []string {
+	n := tr.Height()
+	data := make([]string, n+1)
+	data[0] = tr.ColumnName(int(col))
+
+	for row := uint(0); row < n; row++ {
+		data[row+1] = tr.GetByIndex(int(col), int(row)).String()
+	}
+
+	return data
+}
+
+func traceRowWidths(height uint, rows [][]string) []int {
+	widths := make([]int, height+1)
+
+	for _, row := range rows {
+		for i, col := range row {
+			w := utf8.RuneCountInString(col)
+			widths[i] = max(w, widths[i])
+		}
+	}
+
+	return widths
+}
+
+func printTraceRow(row []string, widths []int) {
+	for i, col := range row {
+		fmt.Printf(" %*s |", widths[i], col)
+	}
+
+	fmt.Println()
+}
+
+func printHorizontalRule(widths []int) {
+	for _, w := range widths {
+		fmt.Print("-")
+
+		for i := 0; i < w; i++ {
+			fmt.Print("-")
+		}
+		fmt.Print("-+")
+	}
+
+	fmt.Println()
+}
diff --git a/pkg/table/trace.go b/pkg/table/trace.go
index dbd170e7..eed60205 100644
--- a/pkg/table/trace.go
+++ b/pkg/table/trace.go
@@ -53,11 +53,9 @@ type Trace interface {
 	// does not exist or if the index is out-of-bounds then an
 	// error is returned.
 	GetByIndex(col int, row int) *fr.Element
-	// Pad each column in this trace with n rows of a given value, either at
-	// the front (sign=true) or the back (sign=false).  An iterator over the
-	// column signs is provided.Padding is done by duplicating either the first
-	// (sign=true) or last (sign=false) item of the trace n times.
-	Pad(n uint, signs func(int) (bool, *fr.Element))
+	// Pad each column in this trace with n items at the front.  An iterator over
+	// the padding values to use for each column must be given.
+	Pad(n uint, signs func(int) *fr.Element)
 	// Determine the height of this table, which is defined as the
 	// height of the largest column.
 	Height() uint
@@ -83,7 +81,7 @@ func ConstraintsAcceptTrace[T Acceptable](trace Trace, constraints []T) error {
 func FrontPadWithZeros(n uint, tr Trace) {
 	var zero fr.Element = fr.NewElement((0))
 	// Insert initial padding row
-	tr.Pad(n, func(index int) (bool, *fr.Element) { return true, &zero })
+	tr.Pad(n, func(index int) *fr.Element { return &zero })
 }
 
 // ===================================================================
@@ -227,14 +225,11 @@ func (p *ArrayTrace) Height() uint {
 	return p.height
 }
 
-// Pad each column in this trace with n items, either at the front
-// (sign=true) or the back (sign=false).  An iterator over the column signs
-// is provided.Padding is done by duplicating either the first (sign=true)
-// or last (sign=false) item of the trace n times.
-func (p *ArrayTrace) Pad(n uint, signs func(int) (bool, *fr.Element)) {
+// Pad each column in this trace with n items at the front.  An iterator over
+// the padding values to use for each column must be given.
+func (p *ArrayTrace) Pad(n uint, padding func(int) *fr.Element) {
 	for i, c := range p.columns {
-		sign, value := signs(i)
-		c.Pad(n, sign, value)
+		c.Pad(n, padding(i))
 	}
 	// Increment height
 	p.height += n
@@ -313,27 +308,13 @@ func (p *ArrayTraceColumn) Clone() *ArrayTraceColumn {
 
 // Pad this column with n copies of a given value, either at the front
 // (sign=true) or the back (sign=false).
-func (p *ArrayTraceColumn) Pad(n uint, sign bool, value *fr.Element) {
-	// Offset where original data should start
-	var copy_offset uint
-	// Offset where padding values should start
-	var padding_offset uint
+func (p *ArrayTraceColumn) Pad(n uint, value *fr.Element) {
 	// Allocate sufficient memory
 	ndata := make([]*fr.Element, uint(len(p.data))+n)
-	// Check direction of padding
-	if sign {
-		// Pad at the front
-		copy_offset = n
-		padding_offset = 0
-	} else {
-		// Pad at the back
-		copy_offset = 0
-		padding_offset = uint(len(p.data))
-	}
 	// Copy over the data
-	copy(ndata[copy_offset:], p.data)
+	copy(ndata[n:], p.data)
 	// Go padding!
-	for i := padding_offset; i < (n + padding_offset); i++ {
+	for i := uint(0); i < n; i++ {
 		ndata[i] = value
 	}
 	// Copy over
diff --git a/pkg/test/ir_test.go b/pkg/test/ir_test.go
index c10e1df9..8456427b 100644
--- a/pkg/test/ir_test.go
+++ b/pkg/test/ir_test.go
@@ -7,7 +7,6 @@ import (
 	"os"
 	"strings"
 	"testing"
-	"unicode/utf8"
 
 	"github.com/consensys/go-corset/pkg/hir"
 	"github.com/consensys/go-corset/pkg/table"
@@ -126,6 +125,10 @@ func Test_Shift_06(t *testing.T) {
 	Check(t, "shift_06")
 }
 
+func Test_Shift_07(t *testing.T) {
+	Check(t, "shift_07")
+}
+
 // ===================================================================
 // Normalisation Tests
 // ===================================================================
@@ -308,7 +311,7 @@ func TestSlow_Mxp(t *testing.T) {
 
 // Determines the maximum amount of padding to use when testing.  Specifically,
 // every trace is tested with varying amounts of padding upto this value.
-const MAX_PADDING uint = 1
+const MAX_PADDING uint = 0
 
 // For a given set of constraints, check that all traces which we
 // expect to be accepted are accepted, and all traces that we expect
@@ -508,68 +511,3 @@ func readLine(reader *bufio.Reader) *string {
 	// Done
 	return &str
 }
-
-// Prints a trace in a more human-friendly fashion.
-func printTrace(tr table.Trace) {
-	n := tr.Width()
-	//
-	rows := make([][]string, n)
-	for i := uint(0); i < n; i++ {
-		rows[i] = traceColumnData(tr, i)
-	}
-	//
-	widths := traceRowWidths(tr.Height(), rows)
-	//
-	printHorizontalRule(widths)
-	//
-	for _, r := range rows {
-		printTraceRow(r, widths)
-		printHorizontalRule(widths)
-	}
-}
-
-func traceColumnData(tr table.Trace, col uint) []string {
-	n := tr.Height()
-	data := make([]string, n+1)
-	data[0] = tr.ColumnName(int(col))
-
-	for row := uint(0); row < n; row++ {
-		data[row+1] = tr.GetByIndex(int(col), int(row)).String()
-	}
-
-	return data
-}
-
-func traceRowWidths(height uint, rows [][]string) []int {
-	widths := make([]int, height+1)
-
-	for _, row := range rows {
-		for i, col := range row {
-			w := utf8.RuneCountInString(col)
-			widths[i] = max(w, widths[i])
-		}
-	}
-
-	return widths
-}
-
-func printTraceRow(row []string, widths []int) {
-	for i, col := range row {
-		fmt.Printf(" %*s |", widths[i], col)
-	}
-
-	fmt.Println()
-}
-
-func printHorizontalRule(widths []int) {
-	for _, w := range widths {
-		fmt.Print("-")
-
-		for i := 0; i < w; i++ {
-			fmt.Print("-")
-		}
-		fmt.Print("-+")
-	}
-
-	fmt.Println()
-}
diff --git a/testdata/permute_04.accepts b/testdata/permute_04.accepts
index 9306be64..ce04e1e7 100644
--- a/testdata/permute_04.accepts
+++ b/testdata/permute_04.accepts
@@ -1,12 +1,12 @@
-{"X": [5]}
-{"X": [0,5]}
-{"X": [5,0]}
-{"X": [0,1,5]}
-{"X": [0,5,1]}
-{"X": [5,1,0]}
-{"X": [1,0,5]}
-{"X": [1,2,3,4,5]}
-{"X": [1,2,3,5,4]}
-{"X": [1,2,5,4,3]}
-{"X": [1,5,3,4,2]}
-{"X": [5,2,3,4,1]}
+{"ST": [1], "X": [5]}
+{"ST": [1,1], "X": [6,5]}
+{"ST": [1,1], "X": [5,6]}
+{"ST": [1,1,1], "X": [6,7,5]}
+{"ST": [1,1,1], "X": [6,5,7]}
+{"ST": [1,1,1], "X": [5,7,6]}
+{"ST": [1,1,1], "X": [7,6,5]}
+{"ST": [1,1,1,1,1], "X": [6,7,8,9,5]}
+{"ST": [1,1,1,1,1], "X": [6,7,8,5,9]}
+{"ST": [1,1,1,1,1], "X": [6,7,5,9,8]}
+{"ST": [1,1,1,1,1], "X": [6,5,8,9,7]}
+{"ST": [1,1,1,1,1], "X": [5,7,8,9,6]}
diff --git a/testdata/permute_04.lisp b/testdata/permute_04.lisp
index 35f92dd8..f84c48cc 100644
--- a/testdata/permute_04.lisp
+++ b/testdata/permute_04.lisp
@@ -1,3 +1,4 @@
+(column ST :u16)
 (column X :u16)
-(permute (Y) (-X))
-(vanish:first last-row (- Y 5))
+(permute (ST' Y) (+ST -X))
+(vanish:last first-row (- Y 5))
diff --git a/testdata/permute_04.rejects b/testdata/permute_04.rejects
index e5cc1eb7..74fda2a8 100644
--- a/testdata/permute_04.rejects
+++ b/testdata/permute_04.rejects
@@ -1,5 +1,5 @@
-{"X": [-1]}
-{"X": [255]}
-{"X": [1234987]}
-{"X": [1,2,3]}
-{"X": [3,44,235,623,1,35]}
+{"ST": [1], "X": [-1]}
+{"ST": [1], "X": [255]}
+{"ST": [1], "X": [1234987]}
+{"ST": [1,1,1], "X": [1,2,3]}
+{"ST": [1,1,1,1,1,1], "X": [3,44,235,623,1,35]}
diff --git a/testdata/permute_07.accepts b/testdata/permute_07.accepts
index 9b9d829a..9474bf13 100644
--- a/testdata/permute_07.accepts
+++ b/testdata/permute_07.accepts
@@ -1,16 +1,16 @@
-{"X": [], "Y": []}
-{"X": [0], "Y": [0]}
-{"X": [1], "Y": [0]}
-{"X": [0], "Y": [1]}
-{"X": [2], "Y": [0]}
-;; n=2
-{"X": [0,0], "Y": [0,0]}
-{"X": [1,0], "Y": [0,1]}
-{"X": [2,1], "Y": [1,0]}
-{"X": [2,0], "Y": [0,1]}
+{"ST": [], "X": [], "Y": []}
+{"ST": [1], "X": [1], "Y": [1]}
+{"ST": [1], "X": [2], "Y": [1]}
+{"ST": [1], "X": [1], "Y": [2]}
+{"ST": [1], "X": [3], "Y": [1]}
 ;; n=3
-{"X": [0,0,0], "Y": [0,0,0]}
-{"X": [3,1,4], "Y": [1,0,3]}
-{"X": [3,0,1], "Y": [1,1,0]}
-{"X": [3,0,1], "Y": [1,1,0]}
-{"X": [5,2,3], "Y": [3,0,2]}
+{"ST": [1,1], "X": [1,1], "Y": [1,1]}
+{"ST": [1,1], "X": [2,1], "Y": [1,2]}
+{"ST": [1,1], "X": [3,2], "Y": [2,1]}
+{"ST": [1,1], "X": [3,1], "Y": [1,2]}
+;; n=3
+{"ST": [1,1,1], "X": [1,1,1], "Y": [1,1,1]}
+{"ST": [1,1,1], "X": [4,2,5], "Y": [2,1,4]}
+{"ST": [1,1,1], "X": [4,1,2], "Y": [2,2,1]}
+{"ST": [1,1,1], "X": [4,1,2], "Y": [2,2,1]}
+{"ST": [1,1,1], "X": [6,3,4], "Y": [4,1,3]}
diff --git a/testdata/permute_07.lisp b/testdata/permute_07.lisp
index 02e693c7..cd8c231e 100644
--- a/testdata/permute_07.lisp
+++ b/testdata/permute_07.lisp
@@ -1,4 +1,5 @@
+(column ST :u16)
 (column X :u16)
 (column Y :u16)
-(permute (A B) (-X +Y))
-(vanish diag_ab (- (shift A 1) B))
+(permute (ST' A B) (+ST -X +Y))
+(vanish diag_ab (* ST' (- (shift A 1) B)))
diff --git a/testdata/permute_07.rejects b/testdata/permute_07.rejects
index 42eb25a5..b1b72c52 100644
--- a/testdata/permute_07.rejects
+++ b/testdata/permute_07.rejects
@@ -1,7 +1,7 @@
-{"X": [0,0], "Y": [1,1]}
-{"X": [1,2], "Y": [1,0]}
-{"X": [1,1], "Y": [1,0]}
-{"X": [0,3,2], "Y": [0,0,0]}
-{"X": [0,3,2], "Y": [3,0,2]}
-{"X": [0,3,2], "Y": [3,1,2]}
-{"X": [0,3,2], "Y": [3,2,2]}
+{"ST": [1,1], "X": [0,0], "Y": [1,1]}
+{"ST": [1,1], "X": [1,2], "Y": [1,0]}
+{"ST": [1,1], "X": [1,1], "Y": [1,0]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [0,0,0]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [3,0,2]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [3,1,2]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [3,2,2]}
diff --git a/testdata/permute_09.accepts b/testdata/permute_09.accepts
index 5b3ae2bb..394cd0ab 100644
--- a/testdata/permute_09.accepts
+++ b/testdata/permute_09.accepts
@@ -1,17 +1,16 @@
-{"X": [], "Y": []}
-{"X": [0], "Y": [0]}
-{"X": [1], "Y": [0]}
+{"ST": [], "X": [], "Y": []}
+{"ST": [1], "X": [0], "Y": [0]}
+{"ST": [1], "X": [1], "Y": [0]}
 ;; n=2
-{"X": [0,0], "Y": [0,0]}
-{"X": [2,1], "Y": [1,0]}
-{"X": [3,2], "Y": [2,0]}
-{"X": [2,3], "Y": [0,2]}
-{"X": [2,2], "Y": [0,2]}
-{"X": [2,1], "Y": [1,0]}
-{"X": [2,2], "Y": [2,0]}
+{"ST": [1,1], "X": [0,0], "Y": [0,0]}
+{"ST": [1,1], "X": [2,1], "Y": [1,0]}
+{"ST": [1,1], "X": [3,2], "Y": [2,0]}
+{"ST": [1,1], "X": [2,3], "Y": [0,2]}
+{"ST": [1,1], "X": [2,2], "Y": [0,2]}
+{"ST": [1,1], "X": [2,1], "Y": [1,0]}
+{"ST": [1,1], "X": [2,2], "Y": [2,0]}
 ;; n=3
-{"X": [0,0,0], "Y": [0,0,0]}
-;;
-{"X": [3,1,2], "Y": [2,0,1]}
-{"X": [3,1,2], "Y": [2,0,1]}
-{"X": [2,2,1], "Y": [1,2,0]}
+{"ST": [1,1,1], "X": [0,0,0], "Y": [0,0,0]}
+{"ST": [1,1,1], "X": [3,1,2], "Y": [2,0,1]}
+{"ST": [1,1,1], "X": [3,1,2], "Y": [2,0,1]}
+{"ST": [1,1,1], "X": [2,2,1], "Y": [1,2,0]}
diff --git a/testdata/permute_09.lisp b/testdata/permute_09.lisp
index 0b4df1dd..330a4f57 100644
--- a/testdata/permute_09.lisp
+++ b/testdata/permute_09.lisp
@@ -1,4 +1,5 @@
+(column ST :u16)
 (column X :u16)
 (column Y :u16)
-(permute (A B) (-X -Y))
-(vanish diag_ab (- (shift A 1) B))
+(permute (ST' A B) (+ST -X -Y))
+(vanish diag_ab (* ST' (- (shift A 1) B)))
diff --git a/testdata/permute_09.rejects b/testdata/permute_09.rejects
index 9ff18f59..adb68240 100644
--- a/testdata/permute_09.rejects
+++ b/testdata/permute_09.rejects
@@ -1,6 +1,6 @@
-{"X": [0,0], "Y": [1,1]}
-{"X": [1,2], "Y": [1,0]}
-{"X": [0,3,2], "Y": [0,0,0]}
-{"X": [0,3,2], "Y": [3,0,2]}
-{"X": [0,3,2], "Y": [3,1,2]}
-{"X": [0,3,2], "Y": [3,2,2]}
+{"ST": [1,1], "X": [0,0], "Y": [1,1]}
+{"ST": [1,1], "X": [1,2], "Y": [1,0]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [0,0,0]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [3,0,2]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [3,1,2]}
+{"ST": [1,1,1], "X": [0,3,2], "Y": [3,2,2]}
diff --git a/testdata/shift_07.accepts b/testdata/shift_07.accepts
new file mode 100644
index 00000000..2a86f0c8
--- /dev/null
+++ b/testdata/shift_07.accepts
@@ -0,0 +1,5 @@
+{"BIT_1": [], "ARG": []}
+{"BIT_1": [0], "ARG": [0]}
+{"BIT_1": [0], "ARG": [1]}
+{"BIT_1": [0], "ARG": [2]}
+{"BIT_1": [0,1], "ARG": [2,0]}
diff --git a/testdata/shift_07.lisp b/testdata/shift_07.lisp
new file mode 100644
index 00000000..6e4bf8d8
--- /dev/null
+++ b/testdata/shift_07.lisp
@@ -0,0 +1,8 @@
+(column BIT_1 :u1)
+(column ARG)
+
+(vanish pivot
+        ;; If BIT_1[k-1]=0 and BIT_1[k]=1
+        (if (+ (shift BIT_1 -1) (- 1 BIT_1))
+            ;; Then ARG = 0
+            ARG))
diff --git a/testdata/shift_07.rejects b/testdata/shift_07.rejects
new file mode 100644
index 00000000..4e7d29f8
--- /dev/null
+++ b/testdata/shift_07.rejects
@@ -0,0 +1,2 @@
+{"BIT_1": [1], "ARG": [1]}
+{"BIT_1": [0,1], "ARG": [2,1]}