Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -105,5 +105,21 @@ required-features = ["smt", "zok", "r1cs"]
name = "opa_bench"
required-features = ["lp", "aby"]

[[example]]
name = "ztest"
required-features = ["smt", "zokc", "bellman"]

[profile.release]
debug = true

[[test]]
name = "inmem"
required-features = ["smt", "zokc", "bellman"]

[[test]]
name = "ztest_e2e"
required-features = ["smt", "zokc", "bellman"]

[[test]]
name = "zok_test_inputs"
required-features = ["smt", "zokc"]
35 changes: 35 additions & 0 deletions examples/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
# CirC examples

## `ztest.rs` — Unit-test circuits written in ZoKratesCurly

`ztest` discovers and runs `@test` functions in a ZoKratesCurly (`.zok`) program.
Each test is compiled to R1CS on its own and its assertions are checked with a
proof backend, so a test passes only if the circuit is satisfiable for the given
inputs.

**Step 1: Write tests**

Annotate test functions with:

```
@test(backend = {groth16, mirage}) <input1> = <val1>, <input2> = <val2>, ...;
```

See [ZoKratesCurly/pf/ztest/coverage_test.zok](ZoKratesCurly/pf/ztest/coverage_test.zok)
for a worked example covering backend selection, scalar/array/tuple inputs, and
public/private visibility.

Rules for an annotated function:

- The backend defaults to `groth16` and may be omitted.
- It behaves like `main`: it must have no generics and no return value.
- It must make assertions (that is what the test verifies).

**Step 2: Run tests**

Build with the features the backends need, then point `ztest` at a file:

```
cargo run --example ztest --features smt,zokc,bellman -- \
examples/ZoKratesCurly/pf/ztest/coverage_test.zok
```
7 changes: 7 additions & 0 deletions examples/ZoKratesCurly/pf/no_main.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
def add(private field a, public field b) -> field {
return a + b;
}

def square(private field x) -> field {
return x * x;
}
99 changes: 99 additions & 0 deletions examples/ZoKratesCurly/pf/ztest/coverage_test.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
// Simple @test coverage: backend selection, scalar, array, and tuple inputs,
// and private/public visibility. All tests pass. Run:
// cargo run --example ztest --features smt,zokc,bellman -- examples/ZoKratesCurly/pf/ztest/coverage_test.zok

// ---- scalar inputs ----

@test x = 5;
def test_field(private field x) {
assert(x == 5);
}

@test(backend = mirage) a = 4, b = 6;
def test_add(private field a, private field b) {
assert(a + b == 10);
}

@test b = true;
def test_bool(private bool b) {
assert(b);
}

@test x = 7u32;
def test_u32(private u32 x) {
assert(x * 2 == 14u32);
}

// ---- scalar visibility corners ----

@test a = 3, b = 4;
def test_all_public(public field a, public field b) {
assert(a + b == 7);
}

@test a = 3, b = 4;
def test_mixed_visibility(private field a, public field b) {
assert(a + b == 7);
}

// ---- array inputs ----

@test xs = [1, 2, 3];
def test_array(private field[3] xs) {
assert(xs[0] + xs[1] == xs[2]);
}

@test A = [[1, 2], [3, 4]];
def test_nested_array(private field[2][2] A) {
assert(A[0][0] == 1);
assert(A[1][1] == 4);
}

@test xs = [1, 2];
def test_public_array(public field[2] xs) {
assert(xs[0] + xs[1] == 3);
}

// ---- array + scalar together ----

@test k = 10, xs = [1, 2];
def test_array_and_scalar(private field k, public field[2] xs) {
assert(k + xs[0] == 11);
assert(k + xs[1] == 12);
}

// ---- tuple inputs ----

@test t = (4, true);
def test_tuple(private (field, bool) t) {
assert(t.0 == 4);
assert(t.1);
}

// A singleton tuple needs the trailing comma: (5,) is a 1-tuple, (5) is
// just a parenthesized expression.
@test t = (5,);
def test_singleton_tuple(private (field,) t) {
assert(t.0 == 5);
}

@test t = ([1, 2], (true, 3));
def test_nested_tuple(private (field[2], (bool, u32)) t) {
assert(t.0[0] + t.0[1] == 3);
assert(t.1.0);
assert(t.1.1 == 3u32);
}

@test pairs = [(1, 2), (3, 4)];
def test_array_of_tuples(private (field, u32)[2] pairs) {
assert(pairs[0].0 == 1);
assert(pairs[0].1 == 2u32);
assert(pairs[1].0 == 3);
assert(pairs[1].1 == 4u32);
}

@test t = (7, 9);
def test_public_tuple(public (field, u32) t) {
assert(t.0 == 7);
assert(t.1 == 9u32);
}
1 change: 1 addition & 0 deletions examples/circ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -215,6 +215,7 @@ fn main() {
DeterminedLanguage::ZsharpCurly => {
let inputs = zsharpcurly::Inputs {
file: options.path,
entry: "main".to_string(),
mode,
};
ZSharpCurlyFE::gen(inputs)
Expand Down
1 change: 1 addition & 0 deletions examples/zcxi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ fn main() {
circ::cfg::set(&options.circ);
let inputs = Inputs {
file: options.zsharp_path,
entry: "main".to_string(),
mode: Mode::Proof,
};
let scalar_input_values = match options.inputs_path.as_ref() {
Expand Down
167 changes: 167 additions & 0 deletions examples/ztest.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,167 @@
//! Unit-test runner for ZoKratesCurly programs.
//! Reads a .zok file, finds every function marked with a @test annotation,
//! evaluates its annotation inputs to concrete values, then runs each test
//! through the full in-memory proof pipeline:
//! compile (test fn as entry point) -> assert check -> setup -> prove -> verify
//! and prints ok / FAILED per test. A test passes when its assertions hold for
//! the supplied inputs and its proof verifies. Assertions are evaluated
//! directly on the unoptimized IR before proof generation. Tests use
//! Groth16 by default and may select Mirage in the annotation.
//!
//! The per-test execution logic lives in [`circ::test_runner`]; this file is
//! the CLI wrapper.
use bls12_381::Bls12;
use circ::cfg::{clap, CircOpt};
use circ::front::zsharpcurly::{TestBackend, ZSharpCurlyFE};
use circ::front::Mode;
use circ::ir::term::Value;
use circ::target::r1cs::{bellman::Bellman, mirage::Mirage};
use circ::test_runner::{catch, run_test, Outcome};
use clap::Parser;
use std::path::PathBuf;

#[derive(Debug, Parser)]
#[command(
name = "ztest",
about = "Run @test functions in a ZoKratesCurly program"
)]
struct Options {
/// Input file
#[arg(name = "PATH")]
path: PathBuf,

#[command(flatten)]
circ: CircOpt,
}

/// Render a concrete Value as a plain number/bool, without the field
/// modulus that Value's own Display appends (e.g. `9` instead of `#f9m524...`).
fn pretty_value(v: &Value) -> String {
match v {
Value::Field(f) => f.i().to_string(),
Value::BitVector(b) => b.uint().to_string(),
Value::Bool(b) => b.to_string(),
Value::Array(a) => format!(
"[{}]",
a.values()
.iter()
.map(pretty_value)
.collect::<Vec<_>>()
.join(", ")
),
// Singletons print as `(5,)` — the trailing comma matches how they
// must be written in source.
Value::Tuple(vs) if vs.len() == 1 => format!("({},)", pretty_value(&vs[0])),
Value::Tuple(vs) => format!(
"({})",
vs.iter().map(pretty_value).collect::<Vec<_>>().join(", ")
),
// Anything else (structs, ...): fall back to the default form.
other => other.to_string(),
}
}

fn main() {
env_logger::Builder::from_default_env()
.format_level(false)
.format_timestamp(None)
.init();

let options = Options::parse();
circ::cfg::set(&options.circ);

// The frontend panics on a missing file with an unhelpful unwrap
// message; check up front so the user gets a plain answer.
if !options.path.exists() {
eprintln!("Error: file not found: {}", options.path.display());
std::process::exit(1);
}

// Find every @test function and evaluate its annotation inputs to
// concrete values. Parse errors surface as panics, evaluation errors
// through the Result.
let tests = match catch(|| ZSharpCurlyFE::eval_test_inputs(options.path.clone(), Mode::Proof)) {
Ok(Ok(tests)) => tests,
Ok(Err(e)) | Err(e) => {
eprintln!("Error: {}", e);
std::process::exit(1);
}
};

println!(
"running {} test{} from {}",
tests.len(),
if tests.len() == 1 { "" } else { "s" },
options.path.display()
);

let (mut passed, mut failed, mut errored) = (0, 0, 0);
for t in &tests {
// Show each input as `name = <source> = <value>`, collapsing to
// `name = <value>` when the source is already just the value.
let inputs: Vec<String> = t
.inputs()
.iter()
.map(|input| {
let value = pretty_value(input.value());
if input.source() == value {
format!("{} = {}", input.name(), value)
} else {
format!("{} = {} = {}", input.name(), input.source(), value)
}
})
.collect();
print!(
"test {} [{}] ({}) ... ",
t.name(),
t.settings().backend(),
inputs.join(", ")
);
// Flush so the prover's own stderr diagnostics (printed when a
// constraint fails) appear under this test's line, not before it.
use std::io::Write;
let _ = std::io::stdout().flush();

let indent = |msg: String| {
// The prover's message spans several lines; indent them all.
for line in msg.lines() {
println!(" {}", line);
}
};
let outcome = match t.settings().backend() {
TestBackend::Groth16 => run_test::<Bellman<Bls12>>(t),
TestBackend::Mirage => run_test::<Mirage<Bls12>>(t),
};
match outcome {
Outcome::Pass => {
passed += 1;
println!("ok");
}
Outcome::AssertionFailed(msg) => {
failed += 1;
println!("FAILED");
indent(msg);
}
Outcome::CompileError(msg) | Outcome::BackendError(msg) => {
errored += 1;
println!("error");
indent(msg);
}
}
}

println!(
"\ntest result: {}. {} passed; {} failed; {} errored",
if failed == 0 && errored == 0 {
"ok"
} else {
"FAILED"
},
passed,
failed,
errored
);
if failed > 0 || errored > 0 {
std::process::exit(1);
}
}
Loading
Loading