Fixes for Quick Tests

This puts through various minor fixes for the quick tests.  What remains
now is to update the larger tests.  At this stage, performance may be
starting to become an issue.

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))

pkg/test/valid_corset_test.go

@@ -625,47 +625,47 @@ 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) {
 	Check(t, true, "memory")
 }
 
 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")
 }
 
 // ===================================================================

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))))

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)

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))))

testdata/counter.lisp

@@ -1,24 +1,11 @@
-(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
 ;; ===================================================
 (defcolumns STAMP CT)
 
 ;; 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.

testdata/type_invalid_05.lisp

@@ -1,5 +1,5 @@
 (defcolumns
-    (BIT :binary@loob)
+    (BIT :binary)
     (X :binary@loob))
 
 (defconstraint c1 () (if (+ 2 BIT) X))

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))))