trailofbits/sv_circuit

Compile processor circuit to ZK-statement

sv_circuit

SIEVE circuit compositor.

Dependencies

sv_circuit is built using nix. It is recommended to use the Determinate Systems installer:

$ curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install

Running

Running without installing,

$ nix run github:trailofbits/sv_circuit

Building

$ nix build

Development Environment

To enter a shell with all dependencies,

$ nix develop

Phases are defined as Cargo hooks. Running a build phase manually,

$ cargoBuildHook
$ cargoCheckHook

However standard cargo commands apply, for compiling a release build and testing:

$ cargo build --release
$ cargo test

Distribution and Licensing

This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR001120C0084.

The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

DISTRIBUTION STATEMENT A: Approved for public release, distribution unlimited.

sv_circuit is licensed under the GNU AGPLv3 License. A copy of the terms can be found in the LICENSE file.

sv_circuit's Issues

Bring `clap` dependency up-to-date, fixing any deprecated API calls.

See #32 failing build: we're (as of writing) 2 major versions out of sync and as a result are calling some seemingly deprecated APIs.

Add Phase 2 IR0+ backend

Updated terminology:

• IR0 relation .rel -> IR0+ circuit
• IR0 instance .ins -> IR0+ public_input
• IR0 short witness .wit -> IR0+ private_input

Since we're not using any of the looping constructs or plugins yet, we're able to transform the Tiny86 NOP IR0 .rel into an IR0+-conformant circuit with string substitution. sed commands that accomplish this are below. NB: our NOP circuit does not use initial register file state, so we didn't need to substitute instance with public():

sed -i 's/short_witness/private()/g' ~/tiny86.rel
sed -i 's/@and/@mul/g' ~/tiny86.rel
sed -i 's/@xor/@add/g' ~/tiny86.rel
sed -i 's/@not(\(\$[0-9]\+\))/@addc(\1, <1>)/g' ~/tiny86.rel

Other changes:

• For the first line of all the files, change version-1.0.0 to version-2.0.0-beta
• The second line of the file is the resource type (circuit, public_input, private_input) followed by ;
• Fields used by the circuit (zero-indexed) start in the third line of the file. For our purposes, IR0 field characteristic 2 degree 1 -> IR0+ @type field 2.
  • Right now, we only emit field-switching gates when targeting the reverie backend, so we can omit indices from private([field_index]) and public([field_index]), but if we were to transform circuits including multiple fields, we'd need to calculate {characteristic}^{degree} to perform the substitution correctly.

Configure dependabot to update only on new major/minor versions

refactor to unpin nightly version regression to allow nightly versions newer than ~2022-11-01

rust nightly versions newer than approx. 2022-11-01 fail to compile;

error[E0310]: the parameter type `T` may not live long enough
   --> src/generic/circuit.rs:795:21
    |
795 |     type IntoIter = impl Iterator<Item = Operation<T>>;
    |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ...so that the type `mcircuit::Operation<T>` will meet its required lifetime bounds
    |
help: consider adding an explicit lifetime bound...
    |
790 | impl<'a, T: 'a + WireValue + 'static> IntoIterator for &'a GenericCircuit<T>
    |                            +++++++++

For more information about this error, try `rustc --explain E0310`.
error: could not compile `sv_circuit` due to 3 previous errors

for now pinning rust compiler to a known good nightly in default.nix and using nix-shell --pure --run "cargo build". however, this annoying and likely to confuse anyone reasonably using 'bare' cargo build.

Use `yosys` for circuit flattening

For targets that require a fully inlined circuit, yosys itself can perform complete inlining. See: https://yosyshq.readthedocs.io/projects/yosys/en/latest/cmd/flatten.html

For targets with function calls (like the primary IR0+), a non-flattened circuit with @functions at module boundaries could yield more efficient circuits at verification time.

include utility functions from SIEVE repo (e.g. `sv-stat`)