THIS PROJECT HAS BEEN SUPERSEDED BY CIRC

Note: This project has been superseded by CirC, which is a Rust re-implementation of the compiler infrastructure.

It is archived here for reference purposes.

Compiler to circuit representations

Currently we have frontends for:

• C
• circom

We have backends for:

• R1CS (proofs via libsnark)
• SMT

Install

Install dependencies

• z3
• The Haskell tool Stack

Build project

Once the dependencies are installed, you should be able to build the compiler:

stack build

Test

stack test

To run an individual test (e.g., C value test), use:

stack test --ta '-p C value test'

Format

We use brittany. You can format all files (slow) with make fmt.

You can format all files changed since a git-ref REF in a directory using

./scripts/format.bash REF DIR

You can format all files in a directory using

./scripts/format.bash all DIR

The formatting script will not format files which have unstaged changes.

Run

For usage information:

stack exec compiler-exe -- -h

For example, to run function foo in file bar, use:

stack exec compiler-exe c foo bar.c -- --solve

Configuration

There is a configuration system in src/Util/Cfg.hs. You can add new configuration options there. Configuration options can be set by environmental variables, like so:

C_cfg_with_underscores_instead_of_dashes=value stack run -- ...

One particularly useful configuration options is C_streams, which enables logging streams. You can log to named streams using logIf in src/Util/Log.hs, and the output will only appear if the specified stream is enabled.

Directory structure

├── app -- Compiler executable
├── src
│ ├── AST -- Circom AST and C AST helpers │ ├── Codegen -- Machinery for generating circuits │ │ ├── Circify -- Language-indended machinery (branches, fns, scopes)
│ │ │ └── Memory-- Stack allocations and accesses
│ │ ├── Circom -- Circom
│ │ └── C -- C
│ ├── IR -- The typed SMT intermediate representation
│ │ ├── SMT -- Logging
│ │ │ ├── TySmt -- Sort-typed SMT terms
│ │ │ ├── Assert-- Monad for accumulating SMT assertions
│ │ │ ├── Opt -- Optimizations over SMT
│ │ │ └── ToPf -- Converting SMT to R1cs
│ │ └── R1cs -- R1cs
│ │ └── Opt -- Optimizations over R1cs
│ ├── Parser -- Machinery for parsing source files │ ├── Targets -- TBD: Alex after code changes
│ └── Util -- Utilities (e.g., logging)
│ ├── Log -- Logging
│ └── Cfg -- Configuration
└── test -- Tests