From aac6849d218f7cd8318cff02638db2b61c7f6952 Mon Sep 17 00:00:00 2001
From: David Pearce <david.pearce@consensys.net>
Date: Tue, 10 Dec 2024 15:04:19 +1300
Subject: [PATCH] Update Syntax for Counter Example (#425)

This updates the syntax for the counter example to reflect how it
originally was written in Corset.  Thus, it is now demonstrating some of
the new features supported in `go-corset`.
---
 pkg/corset/parser.go  |  2 +-
 testdata/counter.lisp | 42 ++++++++++++++++++++++++++++--------------
 2 files changed, 29 insertions(+), 15 deletions(-)

diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go
index db510445..a8b40633 100644
--- a/pkg/corset/parser.go
+++ b/pkg/corset/parser.go
@@ -917,5 +917,5 @@ func isIdentifierStart(c rune) bool {
 }
 
 func isIdentifierMiddle(c rune) bool {
-	return unicode.IsDigit(c) || isIdentifierStart(c) || c == '-'
+	return unicode.IsDigit(c) || isIdentifierStart(c) || c == '-' || c == '!'
 }
diff --git a/testdata/counter.lisp b/testdata/counter.lisp
index 3573b2d8..44c364f7 100644
--- a/testdata/counter.lisp
+++ b/testdata/counter.lisp
@@ -1,3 +1,19 @@
+(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
@@ -6,30 +22,28 @@
 
 ;; In the last row of a valid frame, the counter must have its max
 ;; value.  This ensures that all non-padding frames are complete.
-(defconstraint last (:domain {-1}) (* STAMP (- 3 CT)))
+(defconstraint last (:domain {-1} :guard STAMP) (eq! CT 3))
 
 ;; STAMP either remains constant, or increments by one.
 (defconstraint increment () (*
                       ;; STAMP[k] == STAMP[k+1]
-                      (- STAMP (shift STAMP 1))
+                      (will-inc! STAMP 0)
                       ;; Or, STAMP[k]+1 == STAMP[k+1]
-                      (- (+ 1 STAMP) (shift STAMP 1))))
+                      (will-inc! STAMP 1)))
 
 ;; If STAMP changes, counter resets to zero.
 (defconstraint reset () (*
                   ;; STAMP[k] == STAMP[k+1]
-                  (- STAMP (shift STAMP 1))
+                  (will-remain-constant! STAMP)
                   ;; Or, CT[k+1] == 0
-                  (shift CT 1)))
+                  (vanishes! (next CT))))
 
 ;; If STAMP non-zero and reaches end-of-cycle, then stamp increments;
 ;; otherwise, counter increments.
-(defconstraint heartbeat ()
-  (if STAMP
-      0
-      ;; If CT == 3
-      (if (- 3 CT)
-          ;; Then, STAMP[k]+1 == STAMP[k]
-          (- (+ 1 STAMP) (shift STAMP 1))
-          ;; Else, CT[k]+1 == CT[k]
-          (- (+ 1 CT) (shift CT 1)))))
+(defconstraint heartbeat (:guard STAMP)
+  ;; If CT == 3
+  (if-eq-else CT 3
+      ;; Then, STAMP[k]+1 == STAMP[k]
+      (will-inc! STAMP 1)
+      ;; Else, CT[k]+1 == CT[k]
+      (will-inc! CT 1)))