Update standard library

This pulls over as much of the original corset standard library as possible at the moment (which is actually most of it). There are a couple of outstanding issues to be resolved around overloading, etc.
Consensys · Dec 13, 2024 · f737b77 · f737b77
1 parent 65a1a9a
commit f737b77
Show file tree

Hide file tree

Showing 4 changed files with 260 additions and 82 deletions.
diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go
@@ -334,7 +334,10 @@ func (p *Parser) parseDefColumns(module string, l *sexp.List) (Declaration, []Sy
 }
 
 func (p *Parser) parseColumnDeclaration(e sexp.SExp, binding *ColumnBinding) (*DefColumn, *SyntaxError) {
-	var name string
+	var (
+		name  string
+		error *SyntaxError
+	)
 	// Check whether extended declaration or not.
 	if l := e.AsList(); l != nil {
 		// Check at least the name provided.
@@ -346,14 +349,8 @@ func (p *Parser) parseColumnDeclaration(e sexp.SExp, binding *ColumnBinding) (*D
 		// Column name is always first
 		name = l.Elements[0].String(false)
 		//	Parse type (if applicable)
-		if len(l.Elements) == 2 {
-			var err *SyntaxError
-			if binding.dataType, binding.mustProve, err = p.parseType(l.Elements[1]); err != nil {
-				return nil, err
-			}
-		} else if len(l.Elements) > 2 {
-			// For now.
-			return nil, p.translator.SyntaxError(l, "unknown column declaration attributes")
+		if binding.dataType, binding.mustProve, error = p.parseColumnDeclarationAttributes(l.Elements[1:]); error != nil {
+			return nil, error
 		}
 	} else {
 		name = e.String(false)
@@ -366,6 +363,33 @@ func (p *Parser) parseColumnDeclaration(e sexp.SExp, binding *ColumnBinding) (*D
 	return def, nil
 }
 
+func (p *Parser) parseColumnDeclarationAttributes(attrs []sexp.SExp) (Type, bool, *SyntaxError) {
+	var (
+		dataType  Type = NewFieldType()
+		mustProve bool = false
+		err       *SyntaxError
+	)
+
+	for _, attr := range attrs {
+		symbol := attr.AsSymbol()
+		// Sanity check
+		if symbol == nil {
+			return nil, false, p.translator.SyntaxError(attr, "unknown column attribute")
+		}
+		//
+		switch symbol.Value {
+		case ":display", ":opcode":
+			// skip these for now, as they are only relevant to the inspector.
+		default:
+			if dataType, mustProve, err = p.parseType(attr); err != nil {
+				return nil, false, err
+			}
+		}
+	}
+	// Done
+	return dataType, mustProve, nil
+}
+
 // Parse a constant declaration
 func (p *Parser) parseDefConst(elements []sexp.SExp) (Declaration, []SyntaxError) {
 	var (
@@ -668,28 +692,27 @@ func (p *Parser) parseFunctionNameReturn(element sexp.SExp) (string, Type, bool,
 	//
 	if symbol != nil {
 		name = symbol
-	} else if list.Len() == 2 {
-		name = list.Get(0)
-		// Extract type (and check for errors)
-		if ret, _, err = p.parseType(list.Get(1)); err != nil {
-			return "", nil, false, []SyntaxError{*err}
-		}
-	} else if list.Len() >= 3 {
-		name = list.Get(0)
-		modifier := list.Get(2).AsSymbol()
-		// Check have ":forced" as expected.
-		if modifier == nil || modifier.Value != ":force" {
-			err := p.translator.SyntaxError(list.Get(2), "unexpected modifier")
-			return "", nil, false, []SyntaxError{*err}
-		} else if list.Len() > 3 {
-			err := p.translator.SyntaxError(list.Get(3), "unexpected modifier")
-			return "", nil, false, []SyntaxError{*err}
-		}
-		// Make this as forcing the outcome
-		forced = true
 	} else {
-		err := p.translator.SyntaxError(element, "invalid function declaration")
-		return "", nil, false, []SyntaxError{*err}
+		// Check all modifiers
+		for i, element := range list.Elements {
+			symbol := element.AsSymbol()
+			// Check what we have
+			if symbol == nil {
+				err := p.translator.SyntaxError(element, "modifier expected")
+				return "", nil, false, []SyntaxError{*err}
+			} else if i == 0 {
+				name = symbol
+			} else {
+				switch symbol.Value {
+				case ":force":
+					forced = true
+				default:
+					if ret, _, err = p.parseType(element); err != nil {
+						return "", nil, false, []SyntaxError{*err}
+					}
+				}
+			}
+		}
 	}
 	//
 	if isIdentifier(name) {

diff --git a/pkg/corset/stdlib.lisp b/pkg/corset/stdlib.lisp
@@ -1,41 +1,127 @@
-(defpurefun ((vanishes! :@loob) x) x)
+;; [TODO] (defunalias debug-assert debug)
+
+(defpurefun (if-zero cond then) (if (vanishes! cond) then))
+;; [TODO] (defpurefun (if-zero cond then else) (if (vanishes! cond) then else))
+(defpurefun (if-zero-else cond then else) (if (vanishes! cond) then else))
+
+(defpurefun (if-not-zero cond then) (if (force-bool cond) then))
+;; [TODO] (defpurefun (if-not-zero cond then else) (if (force-bool cond) then else))
+
+(defpurefun ((force-bool :@bool :force) x) x)
+(defpurefun ((is-binary :@loob :force) e0) (* e0 (- 1 e0)))
+
+(defpurefun ((force-bin :binary :force) x) x)
+
+;;
+;; Boolean functions
+;;
+;; !-suffix denotes loobean algebra (i.e. 0 == true)
+;; ~-prefix denotes normalized-functions (i.e. output is 0/1)
+(defpurefun (and a b) (* a b))
+;; [TODO] (defpurefun ((~and :binary@bool) a b) (~ (and a b)))
+(defpurefun ((or! :@loob) a b) (* a b))
+;; [TODO] (defpurefun ((~or! :binary@loob) a b) (~ (or! a b)))
+
+;; [TODO] (defpurefun ((not :binary@bool :force) (x :binary)) (- 1 x))
 
-;; =============================================================================
-;; Logical
-;; =============================================================================
-(defpurefun ((or! :@loob) x y) (* x y))
 (defpurefun ((eq! :@loob) x y) (- x y))
+;; [TODO] (defpurefun ((neq! :binary@loob :force) x y) (not (~ (eq! x y))))
+;; [TODO] (defunalias = eq!)
 
-;; =============================================================================
-;; Control Flow
-;; =============================================================================
-(defpurefun (if-not-eq lhs rhs then)
-    (if
-     (eq! lhs rhs)
-     ;; True branch
-     (vanishes! 0)
-     ;; False branch
-     then))
-
-(defpurefun (if-eq lhs rhs then)
-    (if
-     (eq! lhs rhs)
-     ;; True branch
-     then))
-
-(defpurefun (if-eq-else lhs rhs then else)
-    (if
-     (eq! lhs rhs)
-     ;; True branch
-     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))
+;; [TODO] (defpurefun ((eq :binary@bool :force) (x :binary) (y :binary)) (^ (- x y) 2))
+(defpurefun ((eq :binary@bool :force) x y) (- 1 (~ (eq! x y))))
+(defpurefun ((neq :binary@bool :force) x y) (eq! x y))
+
+;; Variadic variations on and/or
+;; [TODO] (defunalias any! *)
+;; [TODO] (defunalias all *)
+
+;; Boolean functions
+(defpurefun ((is-not-zero :binary@bool) x) (~ x))
+(defpurefun ((is-not-zero! :binary@loob :force) x) (- 1 (is-not-zero x)))
+(defpurefun ((is-zero :binary@bool :force) x) (- 1 (~ x)))
+
+;; Chronological functions
+(defpurefun (next X) (shift X 1))
+(defpurefun (prev X) (shift X -1))
+
+;; Ensure that e0 has (resp. will) increase (resp. decrease) of offset
+;; w.r.t. the previous (resp. next) row.
+(defpurefun (did-inc! e0 offset) (eq! e0 (+ (prev e0) offset)))
+(defpurefun (did-dec! e0 offset) (eq!  e0 (- (prev e0) offset)))
 (defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset)))
+(defpurefun (will-dec! e0 offset) (eq! (next e0) (- e0 offset)))
+
+(defpurefun (did-inc e0 offset) (eq e0 (+ (prev e0) offset)))
+(defpurefun (did-dec e0 offset) (eq  e0 (- (prev e0) offset)))
+(defpurefun (will-inc e0 offset) (will-eq e0 (+ e0 offset)))
+(defpurefun (will-dec e0 offset) (eq (next e0) (- e0 offset)))
+
+;; Ensure that e0 remained (resp. will be) constant
+;; with regards to the previous (resp. next) row.
+(defpurefun (remained-constant! e0) (eq! e0 (prev e0)))
 (defpurefun (will-remain-constant! e0) (will-eq! e0 e0))
+
+(defpurefun (remained-constant e0) (eq e0 (prev e0)))
+(defpurefun (will-remain-constant e0) (will-eq e0 e0))
+
+;; Ensure (in loobean logic) that e0 has changed (resp. will change) its value
+;; with regards to the previous (resp. next) row.
+;; [TODO] (defpurefun (did-change! e0) (neq! e0 (prev e0)))
+;; [TODO] (defpurefun (will-change! e0) (neq! e0 (next e0)))
+
+(defpurefun (did-change e0) (neq e0 (prev e0)))
+(defpurefun (will-change e0) (neq e0 (next e0)))
+
+;; Ensure (in loobean logic) that e0 was (resp. will be) equal to e1 in the
+;; previous (resp. next) row.
+(defpurefun (was-eq! e0 e1) (eq! (prev e0) e1))
+(defpurefun (will-eq! e0 e1) (eq! (next e0) e1))
+
+(defpurefun (was-eq e0 e1) (eq (prev e0) e1))
+(defpurefun (will-eq e0 e1) (eq (next e0) e1))
+
+
+;; Helpers
+(defpurefun ((vanishes! :@loob :force) e0) e0)
+(defpurefun (if-eq x val then) (if (eq! x val) then))
+(defpurefun (if-eq-else x val then else) (if (eq! x val) then else))
+
+;; counter constancy constraint
+(defpurefun ((counter-constancy :@loob) ct X)
+  (if-not-zero ct
+               (remained-constant! X)))
+
+;; perspective constancy constraint
+(defpurefun ((perspective-constancy :@loob) PERSPECTIVE_SELECTOR X)
+            (if-not-zero (* PERSPECTIVE_SELECTOR (prev PERSPECTIVE_SELECTOR))
+                         (remained-constant! X)))
+
+;; base-X decomposition constraints
+(defpurefun (base-X-decomposition ct base acc digits)
+  (if-zero-else ct
+           (eq! acc digits)
+           (eq! acc (+ (* base (prev acc)) digits))))
+
+;; byte decomposition constraint
+(defpurefun (byte-decomposition ct acc bytes) (base-X-decomposition ct 256 acc bytes))
+
+;; bit decomposition constraint
+(defpurefun (bit-decomposition ct acc bits) (base-X-decomposition ct 2 acc bits))
+
+;; plateau constraints
+;; [TODO] (defpurefun (plateau-constraint CT (X :binary) C)
+;;             (begin (debug-assert (stamp-constancy CT C))
+;;                    (if-zero C
+;;                             (eq! X 1)
+;;                             (if (eq! CT 0)
+;;                                 (vanishes! X)
+;;                               (if (eq!  CT C)
+;;                                   (did-inc! X 1)
+;;                                 (remained-constant! X))))))
+
+;; stamp constancy imposes that the column C may only
+;; change at rows where the STAMP column changes.
+(defpurefun (stamp-constancy STAMP C)
+            (if (will-remain-constant! STAMP)
+                (will-remain-constant! C)))
diff --git a/pkg/sexp/parser.go b/pkg/sexp/parser.go
@@ -173,6 +173,8 @@ func (p *Parser) parseSequence(terminator rune) ([]SExp, *SyntaxError) {
 		}
 		// Continue around!
 		elements = append(elements, element)
+		// Skip whitespace
+		p.SkipWhiteSpace()
 	}
 	// Consume terminator
 	p.Next()

diff --git a/testdata/add.lisp b/testdata/add.lisp
@@ -1,30 +1,97 @@
 (module add)
 
 (defcolumns
-  (ACC_2 :i128)
-  (RES_LO :i128)
+  (STAMP :i32)
+  (CT_MAX :byte)
+  (CT :byte)
+  (INST :byte :display :opcode)
+  (ARG_1_HI :i128)
   (ARG_1_LO :i128)
-  (OVERFLOW :binary@prove)
+  (ARG_2_HI :i128)
+  (ARG_2_LO :i128)
   (RES_HI :i128)
-  (INST :i8)
+  (RES_LO :i128)
   (BYTE_1 :byte@prove)
   (BYTE_2 :byte@prove)
   (ACC_1 :i128)
-  (STAMP :i32)
-  (ARG_1_HI :i128)
-  (ARG_2_LO :i128)
-  (ARG_2_HI :i128)
-  (CT_MAX :i8)
-  (CT :i8))
+  (ACC_2 :i128)
+  (OVERFLOW :binary@prove))
+
+(defconst
+  EVM_INST_STOP                          0x00
+  EVM_INST_ADD                           0x01
+  EVM_INST_MUL                           0x02
+  EVM_INST_SUB                           0x03
+  LLARGEMO 15
+  LLARGE   16
+  THETA 340282366920938463463374607431768211456) ;; note that 340282366920938463463374607431768211456 = 256^16
 
-(defconstraint adder-constraints () (if STAMP 0 (if (- CT CT_MAX) (begin (- RES_HI ACC_1) (- RES_LO ACC_2) (if (- INST 3) 0 (begin (- (+ ARG_1_LO ARG_2_LO) (+ RES_LO (* 340282366920938463463374607431768211456 OVERFLOW))) (- (+ ARG_1_HI ARG_2_HI OVERFLOW) (+ RES_HI (* 340282366920938463463374607431768211456 (shift OVERFLOW -1)))))) (if (- INST 1) 0 (begin (- (+ RES_LO ARG_2_LO) (+ ARG_1_LO (* 340282366920938463463374607431768211456 OVERFLOW))) (- (+ RES_HI ARG_2_HI OVERFLOW) (+ ARG_1_HI (* 340282366920938463463374607431768211456 (shift OVERFLOW -1))))))))))
+(defconstraint stamp-constancies ()
+  (begin (stamp-constancy STAMP ARG_1_HI)
+         (stamp-constancy STAMP ARG_1_LO)
+         (stamp-constancy STAMP ARG_2_HI)
+         (stamp-constancy STAMP ARG_2_LO)
+         (stamp-constancy STAMP RES_HI)
+         (stamp-constancy STAMP RES_LO)
+         (stamp-constancy STAMP INST)
+         (stamp-constancy STAMP CT_MAX)))
 
-(defconstraint stamp-constancies () (begin (if (- (shift STAMP 1) STAMP) (- (shift ARG_1_HI 1) ARG_1_HI)) (if (- (shift STAMP 1) STAMP) (- (shift ARG_1_LO 1) ARG_1_LO)) (if (- (shift STAMP 1) STAMP) (- (shift ARG_2_HI 1) ARG_2_HI)) (if (- (shift STAMP 1) STAMP) (- (shift ARG_2_LO 1) ARG_2_LO)) (if (- (shift STAMP 1) STAMP) (- (shift RES_HI 1) RES_HI)) (if (- (shift STAMP 1) STAMP) (- (shift RES_LO 1) RES_LO)) (if (- (shift STAMP 1) STAMP) (- (shift INST 1) INST)) (if (- (shift STAMP 1) STAMP) (- (shift CT_MAX 1) CT_MAX))))
+;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                     ;;
+;;    1.3 heartbeat    ;;
+;;                     ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;
+(defconstraint first-row (:domain {0})
+  (vanishes! STAMP))
 
-(defconstraint heartbeat () (begin (if STAMP (begin INST)) (* (- (shift STAMP 1) STAMP) (- (shift STAMP 1) (+ STAMP 1))) (if (- (shift STAMP 1) STAMP) 0 (shift CT 1)) (if STAMP 0 (begin (* (- INST 1) (- INST 3)) (if (- 1 (~ (- CT CT_MAX))) (- (shift CT 1) (+ CT 1)) (- (shift STAMP 1) (+ STAMP 1))) (- (~ (* (- CT 16) CT_MAX)) 1)))))
+(defconstraint heartbeat ()
+  (begin (if-zero STAMP
+                  (begin (vanishes! INST)
+                         ;; (debug (vanishes! CT))
+                         ;; (debug (vanishes! CT_MAX))
+                         ))
+         (vanishes! (* (will-remain-constant! STAMP) (will-inc! STAMP 1)))
+         (if-not-zero (will-remain-constant! STAMP)
+                      (vanishes! (next CT)))
+         (if-not-zero STAMP
+                      (begin (vanishes! (* (eq! INST EVM_INST_ADD) (eq! INST EVM_INST_SUB)))
+                             (if (eq CT CT_MAX)
+                                 (will-inc! STAMP 1)
+                                 (will-inc! CT 1))
+                             (eq! (~ (* (- CT LLARGE) CT_MAX))
+                                  1)))))
 
-(defconstraint binary-and-byte-decompositions () (begin (if CT (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if CT (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2)))))
+(defconstraint last-row (:domain {-1})
+  (eq! CT CT_MAX))
 
-(defconstraint last-row (:domain {-1}) (- CT CT_MAX))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                   ;;
+;;    1.4 binary, bytehood and byte decompositions   ;;
+;;                                                   ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defconstraint binary-and-byte-decompositions ()
+  (begin (byte-decomposition CT ACC_1 BYTE_1)
+         (byte-decomposition CT ACC_2 BYTE_2)))
 
-(defconstraint first-row (:domain {0}) STAMP)
+;; TODO: bytehood constraints
+;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                       ;;
+;;    1.5 constraints    ;;
+;;                       ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defconstraint adder-constraints (:guard STAMP)
+  (if-eq CT CT_MAX
+         (begin (eq! RES_HI ACC_1)
+                (eq! RES_LO ACC_2)
+                (if-not-zero (- INST EVM_INST_SUB)
+                             (begin (eq! (+ ARG_1_LO ARG_2_LO)
+                                         (+ RES_LO (* THETA OVERFLOW)))
+                                    (eq! (+ ARG_1_HI ARG_2_HI OVERFLOW)
+                                         (+ RES_HI
+                                            (* THETA (prev OVERFLOW))))))
+                (if-not-zero (- INST EVM_INST_ADD)
+                             (begin (eq! (+ RES_LO ARG_2_LO)
+                                         (+ ARG_1_LO (* THETA OVERFLOW)))
+                                    (eq! (+ RES_HI ARG_2_HI OVERFLOW)
+                                         (+ ARG_1_HI
+                                            (* THETA (prev OVERFLOW)))))))))