From f737b77bfefa4559693393c758026eabccfd799b Mon Sep 17 00:00:00 2001 From: DavePearce Date: Fri, 13 Dec 2024 14:16:29 +1300 Subject: [PATCH] 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. --- pkg/corset/parser.go | 83 ++++++++++++++-------- pkg/corset/stdlib.lisp | 158 +++++++++++++++++++++++++++++++---------- pkg/sexp/parser.go | 2 + testdata/add.lisp | 99 +++++++++++++++++++++----- 4 files changed, 260 insertions(+), 82 deletions(-) diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go index 37690a7..085ae27 100644 --- 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 index d9966e6..3080ef5 100644 --- 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 index 617eef6..276455c 100644 --- 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 index 0f056cb..d676898 100644 --- 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)))))))))