Fixing outstanding spillage tests

This fixes the outstanding spillage tests which were written, but not actually being used.
Consensys · Jun 17, 2024 · f6cddd8 · f6cddd8
1 parent 87af9ac
commit f6cddd8
Show file tree

Hide file tree

Showing 14 changed files with 285 additions and 10 deletions.
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -11,6 +11,7 @@ repos:
     rev: v1.0.0-rc.1
     hooks:
       - id: go-test-mod
+        args: [ --run=Test_ ]
   - repo: https://github.com/golangci/golangci-lint
     rev: v1.57.1
     hooks:

diff --git a/pkg/table/constraints.go b/pkg/table/constraints.go
@@ -117,10 +117,13 @@ func (p *RowConstraint[T]) Accepts(tr Trace) error {
 func HoldsGlobally[T Testable](handle string, constraint T, tr Trace) error {
 	// Determine well-definedness bounds for this constraint
 	bounds := constraint.Bounds()
-	// Check all in-bounds values
-	for k := bounds.Start; k < (tr.Height() - bounds.End); k++ {
-		if err := HoldsLocally(int(k), handle, constraint, tr); err != nil {
-			return err
+	// Sanity check enough rows
+	if bounds.End < tr.Height() {
+		// Check all in-bounds values
+		for k := bounds.Start; k < (tr.Height() - bounds.End); k++ {
+			if err := HoldsLocally(int(k), handle, constraint, tr); err != nil {
+				return err
+			}
 		}
 	}
 	// Success

diff --git a/pkg/test/ir_test.go b/pkg/test/ir_test.go
@@ -137,6 +137,18 @@ func Test_Spillage_01(t *testing.T) {
 	Check(t, "spillage_01")
 }
 
+func Test_Spillage_02(t *testing.T) {
+	Check(t, "spillage_02")
+}
+
+func Test_Spillage_03(t *testing.T) {
+	Check(t, "spillage_03")
+}
+
+func Test_Spillage_04(t *testing.T) {
+	Check(t, "spillage_04")
+}
+
 // ===================================================================
 // Normalisation Tests
 // ===================================================================

diff --git a/pkg/util/bounds.go b/pkg/util/bounds.go
@@ -0,0 +1,47 @@
+package util
+
+// EMPTY_BOUND is the bound which overlaps exactly with the original range.  It
+// represents the maximum possible bound.
+var EMPTY_BOUND Bounds = Bounds{0, 0}
+
+// Bounds captures the subrange of rows for which a computation is well-defined.
+type Bounds struct {
+	// Number of rows from first row where computation starts being defined.
+	Start uint
+	// Number of rows before last row where computation is no longer defined.
+	End uint
+}
+
+// NewBounds constructs a new set of bounds.
+func NewBounds(start uint, end uint) Bounds {
+	return Bounds{start, end}
+}
+
+// Union merges one set of bounds into another.
+func (p *Bounds) Union(q *Bounds) {
+	p.Start = max(p.Start, q.Start)
+	p.End = max(p.End, q.End)
+}
+
+// Boundable captures computations which are well-defined only for a specific
+// subrange of rows (the bounds).
+type Boundable interface {
+	// Determine the well-definedness bounds for this expression for both the
+	// negative (left) or positive (right) directions.  For example, consider an
+	// expression such as "(shift X -1)".  This is technically undefined for the
+	// first row of any trace and, by association, any constraint evaluating
+	// this expression on that first row is also undefined (and hence must pass).
+	Bounds() Bounds
+}
+
+// BoundsForArray determines the bounds for an array of expressions.
+func BoundsForArray[E Boundable](args []E) Bounds {
+	bounds := Bounds{0, 0}
+
+	for _, e := range args {
+		ith := e.Bounds()
+		bounds.Union(&ith)
+	}
+	// Done
+	return bounds
+}
diff --git a/testdata/spillage_02.accepts b/testdata/spillage_02.accepts
@@ -0,0 +1,10 @@
+{ "ST": [], "A": [] }
+{ "ST": [1], "A": [0] }
+{ "ST": [1,1], "A": [0,0] }
+{ "ST": [1,1], "A": [0,1] }
+{ "ST": [1,1], "A": [1,0] }
+{ "ST": [1,1,1], "A": [0,0,0] }
+{ "ST": [1,1,1], "A": [0,0,1] }
+{ "ST": [1,1,1], "A": [0,1,0] }
+{ "ST": [1,1,1], "A": [1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1] }
diff --git a/testdata/spillage_02.lisp b/testdata/spillage_02.lisp
@@ -1,2 +1,3 @@
+(column ST)
 (column A)
-(vanish spills (~ (shift A 2)))
+(vanish spills (* ST (* A (~ (shift A 2)))))
diff --git a/testdata/spillage_02.rejects b/testdata/spillage_02.rejects
@@ -0,0 +1,5 @@
+{ "ST": [1,1,1], "A": [1,0,1] }
+{ "ST": [1,1,1], "A": [1,1,1] }
+{ "ST": [1,1,1], "A": [1,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,1] }
diff --git a/testdata/spillage_03.accepts b/testdata/spillage_03.accepts
@@ -0,0 +1,15 @@
+{ "ST": [], "A": [] }
+{ "ST": [1], "A": [0] }
+{ "ST": [1,1], "A": [0,0] }
+{ "ST": [1,1], "A": [0,1] }
+{ "ST": [1,1], "A": [1,0] }
+{ "ST": [1,1,1], "A": [0,0,0] }
+{ "ST": [1,1,1], "A": [0,0,1] }
+{ "ST": [1,1,1], "A": [0,1,0] }
+{ "ST": [1,1,1], "A": [1,0,0] }
+{ "ST": [1,1,1], "A": [1,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [1,1,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,1] }
+{ "ST": [1,1,1,1,1], "A": [1,0,1,0,1] }
diff --git a/testdata/spillage_03.lisp b/testdata/spillage_03.lisp
@@ -1,2 +1,3 @@
+(column ST)
 (column A)
-(vanish spills (~ (shift A 3)))
+(vanish spills (* ST A (~ (shift A 3))))
diff --git a/testdata/spillage_03.rejects b/testdata/spillage_03.rejects
@@ -0,0 +1,7 @@
+{ "ST": [1,1,1,1], "A": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1] }
+{ "ST": [1,1,0,1], "A": [1,0,0,1] }
+{ "ST": [1,0,1,1], "A": [1,0,0,1] }
+{ "ST": [1,0,0,1], "A": [1,0,0,1] }
diff --git a/testdata/spillage_04.accepts b/testdata/spillage_04.accepts
@@ -0,0 +1,144 @@
+{ "ST": [], "A": [], "B": [] }
+{ "ST": [1], "A": [1], "B": [1] }
+{ "ST": [1], "A": [0], "B": [1] }
+{ "ST": [1], "A": [1], "B": [0] }
+{ "ST": [1], "A": [0], "B": [0] }
+;;
+{ "ST": [1,1], "A": [0,0], "B": [0,0] }
+{ "ST": [1,1], "A": [0,1], "B": [0,0] }
+{ "ST": [1,1], "A": [1,0], "B": [0,0] }
+{ "ST": [1,1], "A": [1,1], "B": [0,0] }
+{ "ST": [1,1], "A": [0,0], "B": [1,0] }
+{ "ST": [1,1], "A": [0,1], "B": [1,0] }
+{ "ST": [1,1], "A": [1,0], "B": [1,0] }
+{ "ST": [1,1], "A": [1,1], "B": [1,0] }
+{ "ST": [1,1], "A": [0,0], "B": [0,1] }
+{ "ST": [1,1], "A": [0,1], "B": [0,1] }
+{ "ST": [1,1], "A": [1,0], "B": [0,1] }
+{ "ST": [1,1], "A": [1,1], "B": [0,1] }
+;;
+{ "ST": [1,1,1], "A": [0,0,0], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [1,0,0], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [0,1,0], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [0,0,1], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [1,1,0], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [0,1,1], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [1,1,1], "B": [0,0,0] }
+{ "ST": [1,1,1], "A": [0,0,0], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [1,0,0], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [0,1,0], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [0,0,1], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [1,1,0], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [0,1,1], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [1,1,1], "B": [1,0,0] }
+{ "ST": [1,1,1], "A": [0,0,0], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [1,0,0], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [0,1,0], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [0,0,1], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [1,1,0], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [0,1,1], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [1,1,1], "B": [0,1,0] }
+{ "ST": [1,1,1], "A": [0,0,0], "B": [0,0,1] }
+{ "ST": [1,1,1], "A": [1,0,0], "B": [0,0,1] }
+{ "ST": [1,1,1], "A": [0,1,0], "B": [0,0,1] }
+{ "ST": [1,1,1], "A": [0,0,1], "B": [0,0,1] }
+{ "ST": [1,1,1], "A": [1,1,0], "B": [0,0,1] }
+{ "ST": [1,1,1], "A": [0,1,1], "B": [0,0,1] }
+{ "ST": [1,1,1], "A": [1,1,1], "B": [0,0,1] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,0,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,0,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,0,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,1,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,0,1] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,1,0,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,1,0,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,1,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,0,1] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,1,0] }
+;;
+{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,0,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,0,1] }
diff --git a/testdata/spillage_04.lisp b/testdata/spillage_04.lisp
@@ -1,3 +1,4 @@
+(column ST)
 (column A)
 (column B)
-(vanish spills (~ (* (shift A 3) (shift B 2))))
+(vanish spills (* ST A (~ (* (shift A 3) (shift B 2)))))
diff --git a/testdata/spillage_04.rejects b/testdata/spillage_04.rejects
@@ -0,0 +1,31 @@
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,1,1,1] }
+;;
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,1,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,1,1,1] }
+;;
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,1,1,1] }
+{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,1,1,1] }
+;;
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,0,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,1,1,0] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,0,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,1,1,1] }
+{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,1,1,1] }
diff --git a/testdata/spillage_05.lisp b/testdata/spillage_05.lisp