• Corset Corset is a Lisp-based DSL (Domain-Specific Language), designed to implement constraint systems in the context of zero-knowledge proof systems. It aims at simplifying the writing and understanding of complicated, intricate, commitments by abstracting over cryptographic polynomial primitives while letting users work at their preferred granularity level.

It offers all the tools to:

1. Implement a constraint system in a high-level, dynamically but strongly typed dialect of Lisp;
2. Parse, compile down to polynomial arithmetic, and serialize constraint systems written in Corset Lisp;
3. Export those constraint systems in many formats, from Go to LaTeX;
4. Check & debug traces against a compiled constraint system.
   • Installation The only dependency to run Corset is [[https://www.rust-lang.org/][the Rust compiler]]. Once it is available, Corset can be installed with ~cargo install --git https://github.com/ConsenSys/corset~; or, within a local copy of the repo: ~cargo install --path .~
   • Usage Corset is a simple Lisp dialect, compiling expressions to a representation compatible with a polynomial cryptographic proof system featuring the following operations: ~Add~, ~Mul~, ~Sub~, ~Neg~, and ~Inv~.

** Command Line Interface

+begin_src

Usage: corset [OPTIONS] [SOURCE]...

Commands: go Export columns in a format usable by zkGeth wizard-iop Produce a WizardIOP constraint system besu Export columns in a format usable by zkBesu latex Produce a LaTeX file describing the constraints compute Given a set of constraints and a trace file, fill the computed columns check Given a set of constraints and a filled trace, check the validity of the constraints debug Display the compiled the constraint system compile Given a set of Corset files, compile them into a single file for faster later use help Print this message or the help of the given subcommand(s)

Arguments: [SOURCE]... Either a file or a string containing the Corset code to process

Options: -v, --verbose... More output per occurrence -q, --quiet... Less output per occurrence --debug Compile code in debug mode --allow-dups Whether to allow re-declaration of symbols -t, --threads number of threads to use [default: 1] --no-stdlib -h, --help Print help -V, --version Print version

+end_src

** General Concept A program takes the form of a list of Lisp-like expression written in the Corset dialect of Lisp, that are then parsed as a list of Lisp constraints and compiled as a succession of constraints expressed as composition of the aforementioned base functions.

Once formalized by the Corset compiler, these "programs" can then be exported to any backend – although for now, only Go exporting is implemented.

• Programming in Corset * General Form of a Corset Program A Corset program is defined as a succession of top-level forms. Each of these forms define a piece of the final program, which can be a column, a constant, a function, an alias, or a constraint*. ** Columns Columns are the basic building block of Corset programs, as they represent the values that the constraint system will be checked against. Columns are defined with the ~defcolumns~ keyword, and can be either scalar or composite (/i.e./ array-like). All the elements of a column can be: integer (/i.e./ field elements), bytes (integers in the 0-255 range), nibbles (integers in the 0-32 range) or booleans*.

+begin_src lisp

;; Columns can be defined one at a time... (defcolumns ALPHA) (defcolumns BETA)

;; ...or several at once (defcolumns GAMMA DELTA EPSILON X Y Z)

;; Columns may have a type (defcolumns A (B :bool) (C :nibble))

;; Columns can be scalar... (defcolumns VALUE) (defconstraint () pipo (eq VALUE 3))

;; ...or array-like (defcolumns (VALUES[5]))

;; Array domains can be defined using several syntaxes (defcolumns (EXAMPLE1[2]) ;; array size: EXAMPLE1 is defined over {1, 2} (EXAMPLE2[4:7]) ;; start:end: EXAMPLE2 is defined over {4, 5, 6, 7} (EXAMPLE3[2:10:2]) ;; start:end:step: EXAMPLE3 is defined over {2, 4, 6, 8, 10} (EXAMPLE4{1 6 8})) ;; diescrete domain: EXAMPLE4 is defined over {1, 6, 8}

;; Array columns are indexed using square brackets (defconstraint foo () (eq [EXAMPLE1 2] [EXAMPLE4 6]))

;; Array accesses are checked at compile time (defconstraint will-fail () [EXAMPLE4 2]) ;; 2 ∉ {1, 6, 8}

+end_src

*** Functions Functions can be defined to factorize common operations. This is done using the ~defun~ form, specifying the name of the function and its (optional) parameters.

+begin_src lisp

(defcolumns A B C[3])

;; Checks that X == Y == Z (defun (eq3 X Y Z) (and (eq X Y) (eq Y Z)))

;; A == B == C[2] (defconstraint alpha () (eq3 A B [C 2]))

(defun (large-operation T U V i k) (begin (some-big-constraint T k) (some-other-constraint U V i)))

;; Factorize big constraints (defconstraint () beta (begin (large-operation A [C 1]) (large-operation A [C 3]) (large-operation A [C 2])))

;; Functions can be combined with for (defconstraint () beta-prime (for i [3] (large-operation A [C i])))

+end_src

**** Pure Functions Functions close over their environment, and thus capture or shadow columns accessible from their declaration point, which are available within the body, along the function parameters.

In contrast, pure functions can only operate on their arguments and constants, thus ensuring that no shadowing or other surprising behavior ever happens.

+begin_src lisp

(defconstant W 10) (defcolumns A)

(defpurefun (f X) (eq X W)) ;; OK (defpurefun (f X) (eq X A)) ;; KO: f can not access A

+end_src

*** Constraints Constraints are the parts of a Corset program that will be compiled and featured in the final product, and represent an epxression of the defined columns that should always evaluate to 0. Their definitions follow the syntax ~(defconstraint NAME (LIMITERS) EXPRESSION)~.

The ~LIMITERS~ is a list of conditions limiting where the constraint must hold true. If it is empty, then ~EXPRESSION~ must hold for its whole definition domain. The available limiters are:

• ~:domain RANGE~ :: a range that specifies a finite set of positions where the constraint must hold true; /e.g./ ={0 -1}=;
• ~:guard EXPRESSION~ :: an expression defining the domain of the constraint: it must only hold when ~EXPRESSION~ is non-zero.

Here is a simple example, establishing that columns ~A~ and ~B~ must always be equal:

+begin_src lisp

(defcolumns A B) (defconstraint A-equals-B () (= A B)) ;; this constraint must be verified everywhere (defconstraint A-equals-B-somewhere (:domain {1 3 5}) (= A B)) ;; this constraint only holds at lines 1, 3, & 5 (defconstraint A-equals-B-sometimes (:guard (eq INST 32)) (= A B)) ;; this constraint only holds if INST == 32

+end_src

*** Modules In order to avoid name conflicts, Corset offers an optional module system allowing the use of the same symbol name in different contexts.

+begin_src lisp

(defcolumns A B) (defconstraint foo (eq A B))

(module shabang) ;; we are now in the namespace of shabang (defconstraint foobar (eq A B)) ;; will fail: A & B do not exist here

(defcolumns A B) ;; A & B now exist in shabang, distinct from the previously declared A & B (defconstraint foobar (eq A B)) ;; will now work

+end_src