Home

What is Corset?

Corset is both a lisp-like language aiming at describing AIR-based constraint systems and the compiler and utility suite for it.

As a language, it provides a typed, high-level, expressive, extensible language to write constraints, that are then compiled down to operations usable on a field backing a R1CS-based constraint proving system providing the following operations: addition, subtraction, negation and multiplication.

As a utility suite, it provides many tools to export these compiled constraints to multiple languages, to inspect and debug constraint system, and to validate constraint systems on real numeric traces.

Installation

Corset only depends on the Rust language compiler. The build Corset, the Rust compiler must be available, installed either through your OS preferred method to install packages, or with Rustup.

Once the Rust compiler is available, Corset can simply be installed with

cargo install --git https://github.com/ConsenSys/corset

When new versions are released, repeating this command will ensure that you are using the latest available version.

Development

If you wish to work on Corset, you should first clone the Corset repo

git clone ssh://github.com/ConsenSys/corset

then build a local copy of Corset

cd corset && cargo build --release

that you can, later on, make available system-wide

cd corset && cargo install --path .

Shared Arguments

Some ancillary corset arguments are shared among all other subcommands, and are desribed here:

-v, --verbose...         More output per occurrence
-q, --quiet...           Less output per occurrence
    --debug              Compile code in debug mode
-t, --threads <THREADS>  number of threads to use [default: 1]
    --no-stdlib
-h, --help               Print help
-V, --version            Print version

What Next?

I want to write constraint systems

The first thing to do should be to take a look at the tutorial to familiarize yourself with the Corset language. Afterwards, you may wish to read the Corset language reference guide, then the compile command. Finally, to see how your constraints are compiled to polynomial expression, see the debug command.

Albeit not required, the command besu is used to generate useful scaffolding files to help generate traces from the linea-besu ethereum client.

I want to debug constraint systems

Debugging constraint systems and their corresponding trace generation is typically a ballet-like operation, where blame is repeatedly pushed on one, then the other.

Thus, the debugging process will imply the check command, to see which constraints are being broken by a given trace, the inspect command to efficiently navigate through the traces.

I want to prove my traces

For now, the only proving format is provided through the wizard-iop command, which export the constraint system to a format readable by the Linea prover.

For the more mathematically inclined users, the latex command will export the constraints as LaTeX snippets, that may then be embedded in any document.