CoBBl: SNARK over Basic Blocks

CoBBl is an end-to-end SNARK system that divides a computation into blocks and verify their correctness in parallel. CoBBl is divided into two components:

CirC Blocks

A front-end SNARK compiler based on CirC that divides a program into blocks and generates all constraints related to verification.

Spartan Parallel

A modified Spartan proof system that supports data-parallelism and additional properties. Currently does not support Goldilocks and cannot verify ceno!!!

Running the recursive verifier for ceno

• Requires rustc 1.74.0-nightly
• First set up all compilers: bash setup.sh
• Then run the ceno verifier: bash encode_ceno.sh
• Note that spartan_parallel currently does not support Goldilocks fields and cannot verify the circuit generated by circ_blocks
• Finally run bash verify_ceno.sh, which emits size & number of execution for each block before throwing out a verifier error due to wrong field size.

File Structure

CirC Blocks generates constraints from customized Zokrates codes (see zok_format.md) located in zok_tests/benchmarks.

Ceno Demo

This is a verbose encoding of ceno into Zokrates, aiming for as much resemblance to the Rust code as possible. This produces inefficient constraints, but is useful for debugging purposes. Currently implements functions up to TowerVerify::verify, which is located in zok_tests/benchmarks/ceno_demo/tower_verifier.zok.

Ceno Compact

Work in progress

Producing alternative inputs for Tower Verifier

• Please review zok_format.md first, especially the .input and .witness section.
• Clone or switch to the custom branch https://github.com/scroll-tech/ceno/tree/kunming/recursive_verifier.
• Navigate to ceno/ceno_zkvm and run the benchmark: RAYON_NUM_THREADS=1 cargo run --example riscv_opcodes (might not work with multicore)
• For every benchmark, copy lines below INPUT: to zok_tests/benchmarks/ceno_demo/tower_verifier.input and lines below WITNESS: to zok_tests/benchmarks/ceno_demo/tower_verifier.witness, don't forget the END at the end of each file
• Run the ceno verifier: bash encode_ceno.sh
• I know this is looks stupid, I'm trying to come up with a better solution.

Other compilation flags and functionalities

Many flags are WIP. For temporary hacks, alter the code directly and recompile through bash setup.sh

Verbose outputs for

Working with a different field

Verify circuit using spartan_parallel (only supported in Curve25519)

Continuous Integration

At the moment we only have a simple CI that checks formatting and cargo check and runs setup.sh and encode_ceno.sh.

TODO:

• run tests in CI, too. (That means we need to fix our tests.)
• reorganise the code, so that we only need a single carge check or cargo test instead of having to run that in a dozen different directories.