diff --git a/pkg/corset/stdlib.lisp b/pkg/corset/stdlib.lisp
index 1d26ec07..d9966e69 100644
--- a/pkg/corset/stdlib.lisp
+++ b/pkg/corset/stdlib.lisp
@@ -1,12 +1,14 @@
 (defpurefun ((vanishes! :@loob) x) x)
 
+;; =============================================================================
+;; Logical
+;; =============================================================================
 (defpurefun ((or! :@loob) x y) (* x y))
 (defpurefun ((eq! :@loob) x y) (- x y))
 
-(defpurefun (prev x) (shift x -1))
-(defpurefun (next x) (shift x 1))
-
-;;
+;; =============================================================================
+;; Control Flow
+;; =============================================================================
 (defpurefun (if-not-eq lhs rhs then)
     (if
      (eq! lhs rhs)
@@ -28,3 +30,12 @@
      then
      ;; False branch
      else))
+
+;; =============================================================================
+;; Temporal
+;; =============================================================================
+(defpurefun (prev x) (shift x -1))
+(defpurefun (next x) (shift x 1))
+(defpurefun (will-eq! e0 e1) (eq! (next e0) e1))
+(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset)))
+(defpurefun (will-remain-constant! e0) (will-eq! e0 e0))
diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go
index efdfb446..c284acd5 100644
--- a/pkg/test/valid_corset_test.go
+++ b/pkg/test/valid_corset_test.go
@@ -625,23 +625,23 @@ func Test_PureFun_04(t *testing.T) {
 // ===================================================================
 
 func Test_Counter(t *testing.T) {
-	Check(t, false, "counter")
+	Check(t, true, "counter")
 }
 
 func Test_ByteDecomp(t *testing.T) {
-	Check(t, false, "byte_decomposition")
+	Check(t, true, "byte_decomposition")
 }
 
 func Test_BitDecomp(t *testing.T) {
-	Check(t, false, "bit_decomposition")
+	Check(t, true, "bit_decomposition")
 }
 
 func Test_ByteSorting(t *testing.T) {
-	Check(t, false, "byte_sorting")
+	Check(t, true, "byte_sorting")
 }
 
 func Test_WordSorting(t *testing.T) {
-	Check(t, false, "word_sorting")
+	Check(t, true, "word_sorting")
 }
 
 func Test_Memory(t *testing.T) {
@@ -649,23 +649,23 @@ func Test_Memory(t *testing.T) {
 }
 
 func TestSlow_Add(t *testing.T) {
-	Check(t, false, "add")
+	Check(t, true, "add")
 }
 
 func TestSlow_BinStatic(t *testing.T) {
-	Check(t, false, "bin-static")
+	Check(t, true, "bin-static")
 }
 
 func TestSlow_BinDynamic(t *testing.T) {
-	Check(t, false, "bin-dynamic")
+	Check(t, true, "bin-dynamic")
 }
 
 func TestSlow_Wcp(t *testing.T) {
-	Check(t, false, "wcp")
+	Check(t, true, "wcp")
 }
 
 func TestSlow_Mxp(t *testing.T) {
-	Check(t, false, "mxp")
+	Check(t, true, "mxp")
 }
 
 // ===================================================================
diff --git a/testdata/bit_decomposition.lisp b/testdata/bit_decomposition.lisp
index f5a33ce5..4cfdb8bd 100644
--- a/testdata/bit_decomposition.lisp
+++ b/testdata/bit_decomposition.lisp
@@ -6,4 +6,4 @@
   (BIT_3 :i1@prove))
 
 ;; NIBBLE = 8*BIT_3 + 4*BIT_2 + 2*BIT_1 + BIT_0
-(defconstraint decomp () (- NIBBLE (+ BIT_0 (* 2 BIT_1) (* 4 BIT_2) (* 8 BIT_3))))
+(defconstraint decomp () (eq! NIBBLE (+ BIT_0 (* 2 BIT_1) (* 4 BIT_2) (* 8 BIT_3))))
diff --git a/testdata/byte_decomposition.lisp b/testdata/byte_decomposition.lisp
index 12bc1785..84042838 100644
--- a/testdata/byte_decomposition.lisp
+++ b/testdata/byte_decomposition.lisp
@@ -35,9 +35,9 @@
   ;; If CT[k] == 3
   (if-eq-else CT 3
               ;; Then, CT[k+1] == 0
-              (shift CT 1)
+              (eq! (next CT) 0)
               ;; Else, CT[k]+1 == CT[k+1]
-              (- (+ 1 CT) (next CT))))
+              (eq! (+ 1 CT) (next CT))))
 
 ;; Argument accumulates byte values.
 (defconstraint accumulator (:guard ST)
diff --git a/testdata/byte_sorting.lisp b/testdata/byte_sorting.lisp
index 2e0624ea..1a114f20 100644
--- a/testdata/byte_sorting.lisp
+++ b/testdata/byte_sorting.lisp
@@ -8,4 +8,4 @@
 (defcolumns (Delta :i8@prove))
 
 ;; Delta == X - X[i-1]
-(defconstraint sort () (- Delta (- X (shift X -1))))
+(defconstraint sort () (eq! Delta (- X (shift X -1))))
diff --git a/testdata/counter.lisp b/testdata/counter.lisp
index 44c364f7..b52b0e07 100644
--- a/testdata/counter.lisp
+++ b/testdata/counter.lisp
@@ -1,16 +1,3 @@
-(defpurefun (vanishes! e0) e0)
-;;
-(defpurefun (next X) (shift X 1))
-(defpurefun (prev X) (shift X -1))
-;;
-(defpurefun (eq! x y) (- x y))
-;;
-(defpurefun (will-eq! e0 e1) (eq! (next e0) e1))
-(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset)))
-(defpurefun (will-remain-constant! e0) (will-eq! e0 e0))
-;;
-(defpurefun (if-eq-else x val then else) (if (eq! x val) then else))
-
 ;; ===================================================
 ;; Constraints
 ;; ===================================================
@@ -18,7 +5,7 @@
 
 ;; In the first row, STAMP is always zero.  This allows for an
 ;; arbitrary amount of padding at the beginning which has no function.
-(defconstraint first (:domain {0}) STAMP)
+(defconstraint first (:domain {0}) (eq! STAMP 0))
 
 ;; In the last row of a valid frame, the counter must have its max
 ;; value.  This ensures that all non-padding frames are complete.
diff --git a/testdata/type_invalid_05.lisp b/testdata/type_invalid_05.lisp
index 4ee1f8d8..6b8e0f38 100644
--- a/testdata/type_invalid_05.lisp
+++ b/testdata/type_invalid_05.lisp
@@ -1,5 +1,5 @@
 (defcolumns
-    (BIT :binary@loob)
+    (BIT :binary)
     (X :binary@loob))
 
 (defconstraint c1 () (if (+ 2 BIT) X))
diff --git a/testdata/word_sorting.lisp b/testdata/word_sorting.lisp
index 81ec278c..920f138f 100644
--- a/testdata/word_sorting.lisp
+++ b/testdata/word_sorting.lisp
@@ -9,7 +9,7 @@
 (defcolumns (Byte_0 :i8@prove) (Byte_1 :i8@prove))
 
 ;; Ensure Delta is a u16
-(defconstraint delta_type () (- Delta (+ (* 256 Byte_1) Byte_0)))
+(defconstraint delta_type () (eq! Delta (+ (* 256 Byte_1) Byte_0)))
 
 ;; Delta == X - X[i-1]
-(defconstraint sort () (- Delta (- X (shift X -1))))
+(defconstraint sort () (eq! Delta (- X (shift X -1))))