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 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

Usage: corset [OPTIONS] [SOURCE]... <COMMAND>

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 <THREADS>  number of threads to use [default: 1]
      --no-stdlib
  -h, --help               Print help
  -V, --version            Print version

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.

;; 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}

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.

(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])))

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.

(defconstant W 10)
(defcolumns A)

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

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:

(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

Modules

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

(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