Minor fixes

This adds another test case, and fixes a minor issue with the memory example.
Consensys · Dec 13, 2024 · 858a490 · 858a490
1 parent 404a7eb
commit 858a490
Show file tree

Hide file tree

Showing 5 changed files with 100 additions and 0 deletions.
diff --git a/pkg/corset/stdlib.lisp b/pkg/corset/stdlib.lisp
@@ -125,3 +125,13 @@
 (defpurefun (stamp-constancy STAMP C)
             (if (will-remain-constant! STAMP)
                 (will-remain-constant! C)))
+
+;; =============================================================================
+;; Add
+;; =============================================================================
+(defpurefun (if-not-eq X Y then)
+    (if (eq! X Y)
+        ;; True branch
+        (vanishes! 0)
+        ;; False branch
+        then))
diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go
@@ -322,6 +322,10 @@ func Test_If_09(t *testing.T) {
 	Check(t, false, "if_09")
 }
 
+func Test_If_10(t *testing.T) {
+	Check(t, false, "if_10")
+}
+
 // ===================================================================
 // Guards
 // ===================================================================

diff --git a/testdata/if_10.accepts b/testdata/if_10.accepts
@@ -0,0 +1,36 @@
+{ "X": [], "Y": [], "A": [] }
+;;
+{ "X": [0], "Y": [0], "A": [0] }
+{ "X": [0], "Y": [1], "A": [0] }
+{ "X": [1], "Y": [0], "A": [0] }
+{ "X": [1], "Y": [1], "A": [0] }
+{ "X": [1], "Y": [0], "A": [1] }
+;;
+{ "X": [0,0], "Y": [0,0], "A": [0,0] }
+{ "X": [0,0], "Y": [0,1], "A": [0,0] }
+{ "X": [0,1], "Y": [0,0], "A": [0,0] }
+{ "X": [0,1], "Y": [0,1], "A": [0,0] }
+{ "X": [1,0], "Y": [0,0], "A": [0,0] }
+{ "X": [1,0], "Y": [0,1], "A": [0,0] }
+{ "X": [1,1], "Y": [0,0], "A": [0,0] }
+{ "X": [1,1], "Y": [0,1], "A": [0,0] }
+{ "X": [0,0], "Y": [1,0], "A": [0,0] }
+{ "X": [0,0], "Y": [1,1], "A": [0,0] }
+{ "X": [0,1], "Y": [1,0], "A": [0,0] }
+{ "X": [0,1], "Y": [1,1], "A": [0,0] }
+{ "X": [1,0], "Y": [1,0], "A": [0,0] }
+{ "X": [1,0], "Y": [1,1], "A": [0,0] }
+{ "X": [1,1], "Y": [1,0], "A": [0,0] }
+{ "X": [1,1], "Y": [1,1], "A": [0,0] }
+;;
+{ "X": [0,1], "Y": [0,0], "A": [0,1] }
+{ "X": [1,1], "Y": [0,0], "A": [0,1] }
+{ "X": [0,1], "Y": [1,0], "A": [0,1] }
+{ "X": [1,1], "Y": [1,0], "A": [0,1] }
+;;
+{ "X": [1,0], "Y": [0,0], "A": [1,0] }
+{ "X": [1,0], "Y": [0,1], "A": [1,0] }
+{ "X": [1,1], "Y": [0,0], "A": [1,0] }
+{ "X": [1,1], "Y": [0,1], "A": [1,0] }
+;;
+{ "X": [1,1], "Y": [0,0], "A": [1,1] }
diff --git a/testdata/if_10.lisp b/testdata/if_10.lisp
@@ -0,0 +1,5 @@
+(defpurefun ((vanishes! :@loob) x) x)
+
+(defcolumns (X :binary@loob) (Y :binary@bool) A)
+(defconstraint c1 () (if X (vanishes! A)))
+(defconstraint c2 () (if Y (vanishes! A)))
diff --git a/testdata/if_10.rejects b/testdata/if_10.rejects
@@ -0,0 +1,45 @@
+{ "X": [0], "Y": [0], "A": [1] }
+{ "X": [0], "Y": [1], "A": [1] }
+{ "X": [1], "Y": [1], "A": [1] }
+;;
+{ "X": [0,0], "Y": [0,0], "A": [0,1] }
+{ "X": [0,0], "Y": [0,1], "A": [0,1] }
+{ "X": [0,1], "Y": [0,1], "A": [0,1] }
+{ "X": [1,0], "Y": [0,0], "A": [0,1] }
+{ "X": [1,0], "Y": [0,1], "A": [0,1] }
+{ "X": [1,1], "Y": [0,1], "A": [0,1] }
+{ "X": [0,0], "Y": [1,0], "A": [0,1] }
+{ "X": [0,0], "Y": [1,1], "A": [0,1] }
+{ "X": [0,1], "Y": [1,1], "A": [0,1] }
+{ "X": [1,0], "Y": [1,0], "A": [0,1] }
+{ "X": [1,0], "Y": [1,1], "A": [0,1] }
+{ "X": [1,1], "Y": [1,1], "A": [0,1] }
+;;
+{ "X": [0,0], "Y": [0,0], "A": [1,0] }
+{ "X": [0,0], "Y": [0,1], "A": [1,0] }
+{ "X": [0,1], "Y": [0,0], "A": [1,0] }
+{ "X": [0,1], "Y": [0,1], "A": [1,0] }
+{ "X": [0,0], "Y": [1,0], "A": [1,0] }
+{ "X": [0,0], "Y": [1,1], "A": [1,0] }
+{ "X": [0,1], "Y": [1,0], "A": [1,0] }
+{ "X": [0,1], "Y": [1,1], "A": [1,0] }
+{ "X": [1,0], "Y": [1,0], "A": [1,0] }
+{ "X": [1,0], "Y": [1,1], "A": [1,0] }
+{ "X": [1,1], "Y": [1,0], "A": [1,0] }
+{ "X": [1,1], "Y": [1,1], "A": [1,0] }
+;;
+{ "X": [0,0], "Y": [0,0], "A": [1,1] }
+{ "X": [0,0], "Y": [0,1], "A": [1,1] }
+{ "X": [0,1], "Y": [0,0], "A": [1,1] }
+{ "X": [0,1], "Y": [0,1], "A": [1,1] }
+{ "X": [1,0], "Y": [0,0], "A": [1,1] }
+{ "X": [1,0], "Y": [0,1], "A": [1,1] }
+{ "X": [1,1], "Y": [0,1], "A": [1,1] }
+{ "X": [0,0], "Y": [1,0], "A": [1,1] }
+{ "X": [0,0], "Y": [1,1], "A": [1,1] }
+{ "X": [0,1], "Y": [1,0], "A": [1,1] }
+{ "X": [0,1], "Y": [1,1], "A": [1,1] }
+{ "X": [1,0], "Y": [1,0], "A": [1,1] }
+{ "X": [1,0], "Y": [1,1], "A": [1,1] }
+{ "X": [1,1], "Y": [1,0], "A": [1,1] }
+{ "X": [1,1], "Y": [1,1], "A": [1,1] }