From 2f570217d77a1fff3e06420ea1120985e8ca1587 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Mon, 13 Jul 2026 21:33:49 -0400 Subject: [PATCH 01/29] Add ztest example and discovery demo Register a new example `ztest` in Cargo.toml (requires features `smt` and `zokc`) and add two new files: a Rust example `examples/ztest.rs` that scans a ZoKratesCurly .zok file for functions annotated with `@test` and prints their names and input literals (discovery-only, no compilation or execution), and a demo ZoKrates file `examples/ZoKratesCurly/pf/discovery_demo.zok` containing two @test functions and a helper. This provides a small utility to list test cases embedded in ZoKratesCurly source for development and debugging. --- Cargo.toml | 4 ++ examples/ZoKratesCurly/pf/discovery_demo.zok | 16 +++++ examples/ztest.rs | 75 ++++++++++++++++++++ 3 files changed, 95 insertions(+) create mode 100644 examples/ZoKratesCurly/pf/discovery_demo.zok create mode 100644 examples/ztest.rs diff --git a/Cargo.toml b/Cargo.toml index 3910d00c..6188e9b9 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -138,5 +138,9 @@ required-features = ["lp", "aby"] name = "r1cs_inspect" required-features = ["r1cs"] +[[example]] +name = "ztest" +required-features = ["smt", "zokc"] + [profile.release] debug = true diff --git a/examples/ZoKratesCurly/pf/discovery_demo.zok b/examples/ZoKratesCurly/pf/discovery_demo.zok new file mode 100644 index 00000000..ebd1f562 --- /dev/null +++ b/examples/ZoKratesCurly/pf/discovery_demo.zok @@ -0,0 +1,16 @@ +// Demo file for @test discovery (examples/ztest.rs). +// Two functions are marked @test; `helper` is not and should be skipped. + +@test a = 4, b = 5; +def test_mul(private field a, private field b) -> field { + return a * b; +} + +@test x = 2, y = 3 * 3; +def test_add(private field x, private field y) -> field { + return x + y; +} + +def helper(field n) -> field { + return n + 1; +} diff --git a/examples/ztest.rs b/examples/ztest.rs new file mode 100644 index 00000000..b3799b18 --- /dev/null +++ b/examples/ztest.rs @@ -0,0 +1,75 @@ +/// Test discovery for ZoKratesCurly programs. +/// Reads a .zok file, finds every function marked with a @test annotation, +/// and prints each one's name and inputs. It does NOT run, compile, or +/// check anything — discovery and printing only. + +use circ::cfg::{clap, CircOpt}; +use clap::Parser; +use std::path::PathBuf; +use zokrates_curly_pest_ast::SymbolDeclaration; + +#[derive(Debug, Parser)] +#[command(name = "ztest", about = "List @test functions in a ZoKratesCurly program")] +struct Options { + /// Input file + #[arg(name = "PATH")] + path: PathBuf, + + #[command(flatten)] + circ: CircOpt, +} + +fn main() { + env_logger::Builder::from_default_env() + .format_level(false) + .format_timestamp(None) + .init(); + + let options = Options::parse(); + circ::cfg::set(&options.circ); + + // Read the whole source file into a string; the parser borrows from it. + let source = match std::fs::read_to_string(&options.path) { + Ok(s) => s, + Err(e) => { + eprintln!("Error reading {}: {}", options.path.display(), e); + std::process::exit(1); + } + }; + + // Parse the source into an AST. No type checking happens here. + let file = match zokrates_curly_pest_ast::generate_ast(&source) { + Ok(f) => f, + Err(e) => { + eprintln!("Parse error in {}:\n{}", options.path.display(), e); + std::process::exit(1); + } + }; + + // Walk the top-level declarations, keeping only functions marked @test. + for decl in &file.declarations { + // Only function declarations can carry a @test annotation. + let SymbolDeclaration::Function(f) = decl else { + continue; + }; + + // `f.test` is Some(..) only when the function was annotated @test. + let Some(test) = &f.test else { + continue; + }; + + // Print each input as written in the source (no evaluation): + // `span().as_str()` gives the literal text, e.g. `3 * 3`. + let inputs: Vec = test + .inputs + .iter() + .map(|input| format!("{} = {}", input.name.value, input.value.span().as_str())) + .collect(); + + if inputs.is_empty() { + println!("found {} with no inputs", f.id.value); + } else { + println!("found {} with {}", f.id.value, inputs.join(", ")); + } + } +} From dd8b3f72ea4aa60ec1e8f4ca3a6997588e18926f Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Mon, 13 Jul 2026 21:36:07 -0400 Subject: [PATCH 02/29] Update .gitignore --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 0373d521..6f9a50de 100644 --- a/.gitignore +++ b/.gitignore @@ -19,4 +19,4 @@ scripts/aby_tests/tests /flamegraph*.svg /.ccls-cache /.vscode -CLAUDE.md + From 27b3b863e2abd857097fbf2e2e36b645b9a42572 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 15 Jul 2026 22:46:36 -0400 Subject: [PATCH 03/29] Add test runner and eval for @test inputs Introduce an end-to-end test runner and support for evaluating @test annotation inputs. - Add examples/ztest.rs: a ztest runner that finds @test functions, evaluates their inputs, then runs compile -> setup -> prove -> verify (Groth16 / BLS12-381) and prints pass/fail/error results. Includes panic-catching and pretty printing of input values. - Add /ZoKratesCurly/pf/coverage_test.zok: a comprehensive ZoKratesCurly test file exercising language features through the full pipeline. - Frontend changes: add TestCase and TestCaseInput types and ZSharpCurlyFE::eval_test_inputs to validate and evaluate @test inputs (type checking, literal typing by parameter, scalar-only restriction, generic rejection, ordering/visibility rules). Includes eval_test_case helper and const-literal rewriting for parameter typing. - AST visitor updates: visit test annotations and inputs so visitors/rewriters see them. - Add tests/zok_test_inputs.rs: extensive unit tests covering accepted inputs, typing rules, errors, visibility, ordering, and other edge cases. - Update Cargo.toml: mark the ztest example required features and register the new test target for running the annotation-input tests. These changes enable runners to discover and execute ZoKratesCurly @test annotations reliably and provide thorough validation and diagnostics for malformed annotations. NOTE: This only works for scalar inputs. --- Cargo.toml | 4 + examples/ZoKratesCurly/pf/coverage_test.zok | 117 +++++ examples/ztest.rs | 228 +++++++-- src/front/zsharpcurly/mod.rs | 256 ++++++++++ src/front/zsharpcurly/zvisit/walkfns.rs | 28 ++ src/front/zsharpcurly/zvisit/zvmut.rs | 8 + tests/zok_test_inputs.rs | 448 ++++++++++++++++++ .../zokrates_pest_ast/src/lib.rs | 14 - 8 files changed, 1050 insertions(+), 53 deletions(-) create mode 100644 examples/ZoKratesCurly/pf/coverage_test.zok create mode 100644 tests/zok_test_inputs.rs diff --git a/Cargo.toml b/Cargo.toml index 6188e9b9..6ca11235 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -140,6 +140,10 @@ required-features = ["r1cs"] [[example]] name = "ztest" +required-features = ["smt", "zokc", "bellman"] + +[[test]] +name = "zok_test_inputs" required-features = ["smt", "zokc"] [profile.release] diff --git a/examples/ZoKratesCurly/pf/coverage_test.zok b/examples/ZoKratesCurly/pf/coverage_test.zok new file mode 100644 index 00000000..49e025e3 --- /dev/null +++ b/examples/ZoKratesCurly/pf/coverage_test.zok @@ -0,0 +1,117 @@ +// Systematic @test runner coverage: every currently supported feature, +// each through the full compile -> setup -> prove -> verify pipeline. +// All tests here pass; rejection paths are covered in tests/zok_test_inputs.rs. + +// ---- helpers under test ---- + +const field BASE = 40; + +type Word = u32; + +def sq(field x) -> field { + return x * x; +} + +def pick_max(field x, field y) -> field { + return if x > y { x } else { y }; +} + +def sum_to(u32 n) -> u32 { + u32 mut acc = 0; + for u32 i in 0..8 { + acc = if i < n { acc + i } else { acc }; + } + return acc; +} + +// ---- input types: every scalar, each proven end-to-end ---- + +@test b = true; +def test_bool_input(private bool b) { + assert(b); +} + +@test x = 200u8, y = 55u8; +def test_u8_input(private u8 x, private u8 y) { + assert(x + y == 255u8); +} + +@test x = 0xBEEF; +def test_u16_hex_input(private u16 x) { + assert(x == 48879u16); +} + +@test x = 7; +def test_u32_bare_literal(private u32 x) { + // bare 7 is typed u32 by this parameter + assert(x * x == 49u32); +} + +@test x = 4294967296; +def test_u64_input(private u64 x) { + // 2^32 does not fit in u32; only valid because the parameter is u64 + assert(x == 0x0000000100000000); +} + +@test x = 5f; +def test_field_suffixed(private field x) { + assert(x == 5); +} + +@test w = 21; +def test_type_alias_input(private Word w) { + assert(w + w == 42u32); +} + +// ---- input expressions ---- + +@test x = 3 * 3 + 2 * 2; +def test_arithmetic_expr(private field x) { + assert(x == 13); +} + +@test x = BASE + 2; +def test_constant_expr(private field x) { + assert(x == 42); +} + +@test x = sq(sq(2)); +def test_nested_call_expr(private field x) { + assert(x == 16); +} + +@test b = 5 > 3; +def test_bool_expr(private bool b) { + assert(b); +} + +// ---- function shapes ---- + +@test; +def test_no_inputs() { + assert(sq(6) == 36); +} + +@test a = 1, b = 2, c = 3, d = 4; +def test_mixed_visibility(private field a, public field b, field c, private field d) { + assert(a + b + c + d == 10); +} + +@test x = 9, y = 2; +def test_control_flow(private field x, private field y) { + assert(pick_max(x, y) == 9); + assert(pick_max(y, x) == 9); +} + +@test n = 5; +def test_loop_and_mut(private u32 n) { + // 0+1+2+3+4 + assert(sum_to(n) == 10u32); +} + +@test x = 3; +def test_multiple_asserts(private field x) { + assert(x == 3); + assert(sq(x) == 9); + assert(sq(x) + x == 12, "message on an assert works too"); +} diff --git a/examples/ztest.rs b/examples/ztest.rs index b3799b18..49b539da 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -1,15 +1,27 @@ -/// Test discovery for ZoKratesCurly programs. +/// Unit-test runner for ZoKratesCurly programs. /// Reads a .zok file, finds every function marked with a @test annotation, -/// and prints each one's name and inputs. It does NOT run, compile, or -/// check anything — discovery and printing only. - +/// evaluates its annotation inputs to concrete values, then runs each test +/// through the full in-memory proof pipeline: +/// compile (test fn as entry point) -> setup -> prove -> verify +/// and prints ok / FAILED per test. A test passes when its assertions hold, +/// i.e. when a proof can be produced and verifies (backend: Groth16 over +/// BLS12-381, hardcoded for the MVP). +use bls12_381::Bls12; use circ::cfg::{clap, CircOpt}; +use circ::front::zsharpcurly::{Inputs, TestCase, ZSharpCurlyFE}; +use circ::front::{FrontEnd, Mode}; +use circ::ir::term::Value; +use circ::target::r1cs::bellman::Bellman; +use circ::target::r1cs::proof::ProofSystem; use clap::Parser; +use fxhash::FxHashMap; use std::path::PathBuf; -use zokrates_curly_pest_ast::SymbolDeclaration; #[derive(Debug, Parser)] -#[command(name = "ztest", about = "List @test functions in a ZoKratesCurly program")] +#[command( + name = "ztest", + about = "Run @test functions in a ZoKratesCurly program" +)] struct Options { /// Input file #[arg(name = "PATH")] @@ -19,6 +31,104 @@ struct Options { circ: CircOpt, } +/// The outcome of running one test. +enum Outcome { + /// The proof verified: all assertions hold. + Pass, + /// Proving or verifying failed: an assertion does not hold. + Fail(String), + /// The test could not be run at all (e.g. unsupported shape). + Error(String), +} + +/// 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(), + // Anything else (arrays, tuples, ...): fall back to the default form. + other => other.to_string(), + } +} + +/// Run `f`, catching panics and silencing the default panic hook only for +/// the duration of the call (the frontend and the prover report failures by +/// panicking). Returns the panic message on unwind. +fn catch(f: impl FnOnce() -> R) -> Result { + let prev_hook = std::panic::take_hook(); + std::panic::set_hook(Box::new(|_| {})); + let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(f)); + std::panic::set_hook(prev_hook); + result.map_err(|e| { + if let Some(msg) = e.downcast_ref::() { + msg.clone() + } else if let Some(msg) = e.downcast_ref::<&str>() { + (*msg).to_string() + } else { + "unknown panic".to_string() + } + }) +} + +/// Run one test through compile -> setup -> prove -> verify. +fn run_test(path: &std::path::Path, test: &TestCase) -> Outcome { + // MVP supports assert-style tests only: a return-typed test computes a + // value, but the annotation gives no expected output to check it against. + if test.has_return { + return Outcome::Error( + "test functions with a return type are not supported (yet); \ + drop the return type and use assert(...)" + .to_string(), + ); + } + + // Compile the test function as its own entry point and lower it to + // prover/verifier data. Compilation failures are errors, not test + // failures: the test never ran. + let name = test.name.clone(); + let file = path.to_path_buf(); + let setup = catch(move || { + let comps = ZSharpCurlyFE::gen(Inputs { + file, + entry: name.clone(), + mode: Mode::Proof, + }); + let cs = comps.get(&name); + let (p_data, v_data, _stats) = circ::compile::to_proof_data(cs, circ::cfg::cfg()); + Bellman::::setup(p_data, v_data) + }); + let (pk, vk) = match setup { + Ok(keys) => keys, + Err(e) => return Outcome::Error(e), + }; + + // The prover knows every input; the verifier sees only the public ones. + let prover_map: FxHashMap = test + .inputs + .iter() + .map(|i| (i.name.clone(), i.value.clone())) + .collect(); + let verifier_map: FxHashMap = test + .inputs + .iter() + .filter(|i| i.public) + .map(|i| (i.name.clone(), i.value.clone())) + .collect(); + + // Prove and verify. An assertion that does not hold makes the witness + // unsatisfiable, which the prover reports by panicking. + match catch(|| { + let pf = Bellman::::prove(&pk, &prover_map); + Bellman::::verify(&vk, &verifier_map, &pf) + }) { + Ok(true) => Outcome::Pass, + Ok(false) => Outcome::Fail("proof did not verify".to_string()), + Err(e) => Outcome::Fail(e), + } +} + fn main() { env_logger::Builder::from_default_env() .format_level(false) @@ -28,48 +138,88 @@ fn main() { let options = Options::parse(); circ::cfg::set(&options.circ); - // Read the whole source file into a string; the parser borrows from it. - let source = match std::fs::read_to_string(&options.path) { - Ok(s) => s, - Err(e) => { - eprintln!("Error reading {}: {}", options.path.display(), e); - std::process::exit(1); - } - }; + // 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); + } - // Parse the source into an AST. No type checking happens here. - let file = match zokrates_curly_pest_ast::generate_ast(&source) { - Ok(f) => f, - Err(e) => { - eprintln!("Parse error in {}:\n{}", options.path.display(), e); + // 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); } }; - // Walk the top-level declarations, keeping only functions marked @test. - for decl in &file.declarations { - // Only function declarations can carry a @test annotation. - let SymbolDeclaration::Function(f) = decl else { - continue; - }; - - // `f.test` is Some(..) only when the function was annotated @test. - let Some(test) = &f.test else { - continue; - }; - - // Print each input as written in the source (no evaluation): - // `span().as_str()` gives the literal text, e.g. `3 * 3`. - let inputs: Vec = test + 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 = = `, collapsing to + // `name = ` when the source is already just the value. + let inputs: Vec = t .inputs .iter() - .map(|input| format!("{} = {}", input.name.value, input.value.span().as_str())) + .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, 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(); - if inputs.is_empty() { - println!("found {} with no inputs", f.id.value); - } else { - println!("found {} with {}", f.id.value, inputs.join(", ")); + match run_test(&options.path, t) { + Outcome::Pass => { + passed += 1; + println!("ok"); + } + Outcome::Fail(msg) => { + failed += 1; + println!("FAILED"); + // The prover's message spans several lines; indent them all. + for line in msg.lines() { + println!(" {}", line); + } + } + Outcome::Error(msg) => { + errored += 1; + println!("error"); + for line in msg.lines() { + println!(" {}", line); + } + } } } + + 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); + } } diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index 6108aab6..cf4817c4 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -39,6 +39,42 @@ pub struct Inputs { pub mode: Mode, } +/// A function marked `@test`, with its annotation inputs evaluated to +/// concrete values. +/// +/// Contract: a `TestCase` guarantees its *inputs* are validated — names +/// match parameters exactly, types are checked, values are constant. It +/// does not decide whether the function's *shape* is runnable; that is +/// runner policy. In particular, return-typed test functions are +/// discovered (see [Self::has_return]) and it is up to the runner to +/// support or reject them. +#[derive(Debug, Clone)] +pub struct TestCase { + /// The test function's name. + pub name: String, + /// Whether the function declares a return type. Assert-style tests + /// (no return type) are self-checking; a runner may not support + /// return-typed tests, since the annotation gives no expected output. + pub has_return: bool, + /// The function's evaluated annotation inputs, in parameter order. + pub inputs: Vec, +} + +/// One evaluated `@test` annotation input, e.g. `y = 3 * 3`. +#[derive(Debug, Clone)] +pub struct TestCaseInput { + /// The input's name (the `y` in `y = 3 * 3`). + pub name: String, + /// Whether the parameter this input binds to is public (`public` or no + /// visibility keyword) rather than `private`. In a proof, public inputs + /// are shared with the verifier; private inputs stay with the prover. + pub public: bool, + /// The input expression exactly as written in the source (`3 * 3`). + pub source: String, + /// The concrete value the expression evaluates to (`9`). + pub value: Value, +} + #[allow(dead_code)] fn const_value_simple(term: &Term) -> Option { match term.op() { @@ -113,7 +149,227 @@ impl ZSharpCurlyFE { g.file_stack_push(file); g.generics_stack_push(HashMap::new()); g.const_entry_fn(&entry, input_scalar_values) + } + + /// Evaluate the `@test` annotation inputs of every test function in `file`. + /// + /// Each input expression (e.g. the `3 * 3` in `@test y = 3 * 3;`) is run + /// through the same const evaluator used for `const` definitions and + /// array sizes, yielding a concrete [Value]. Functions without `@test` + /// are skipped. Nothing is compiled, proven, or executed. + /// + /// Inputs are validated against the function's signature: + /// * every input must name a parameter, exactly once, and every + /// parameter must receive an input; + /// * only scalar parameters (`field`, `bool`, `u8`..`u64`) are supported; + /// * unsuffixed literals are typed by the parameter they bind to (so + /// `x = 2` for a `u32 x` is a `u32`), and the evaluated type must + /// match the parameter's declared type; + /// * generic test functions are rejected. + /// + /// Known limits and semantics: + /// * The `Err` case covers annotation validation/evaluation only. + /// Loading/parsing failures panic and some semantic failures exit the + /// process, through pre-existing frontend paths — callers that must + /// survive arbitrary files should `catch_unwind`. + /// * Parameter-directed literal typing does not descend into call + /// arguments (`y = id(2)` for a `u32` fails; write `id(2u32)`), a + /// limit of [ZConstLiteralRewriter]. + /// * Annotation expressions have module-wide visibility: they are + /// evaluated after all declarations are processed, so they may + /// reference constants and functions declared later in the file. + pub fn eval_test_inputs(file: PathBuf, mode: Mode) -> Result, String> { + // Load and typecheck the file (and its imports), exactly like `check`. + // visit_files() also evaluates every `const` definition, so annotation + // inputs that name a constant can resolve it below. + let loader = parser::ZLoad::new(); + let asts = loader.load(&file); + let mut g = ZGen::new(asts, mode, loader.stdlib(), cfg().zsharp.isolate_asserts); + g.visit_files(); + + // Enter the entry file's scope, like `interpret` does, so identifier + // lookups during evaluation know which file's constants and imports + // to search. + g.file_stack_push(file.clone()); + g.generics_stack_push(HashMap::new()); + + let mut tests = Vec::new(); + let ast = g + .asts + .get(&file) + .ok_or_else(|| format!("no AST loaded for {}", file.display()))?; + for decl in &ast.declarations { + // Only functions can be tests, and only those marked @test count. + let ast::SymbolDeclaration::Function(f) = decl else { + continue; + }; + let Some(ann) = &f.test else { + continue; + }; + tests.push(eval_test_case(&g, &file, f, ann)?); + } + + g.generics_stack_pop(); + g.file_stack_pop(); + Ok(tests) + } } + +/// Validate one `@test` function's annotation against its signature and +/// evaluate each input to a concrete value. See [ZSharpCurlyFE::eval_test_inputs] +/// for the rules enforced here. +/// +/// Errors are rendered to owned strings (path + offending source line) +/// before returning, because AST spans borrow the loader's source text and +/// cannot outlive `eval_test_inputs`. +fn eval_test_case<'ast>( + g: &ZGen<'ast>, + file: &std::path::Path, + f: &ast::FunctionDefinition<'ast>, + ann: &ast::TestAnnotation<'ast>, +) -> Result { + let diag = |msg: String, span: &ast::Span| { + format!( + "{}\nIn {}:\n {}", + msg, + file.display(), + span_to_string(span) + ) + }; + + // Generic test functions have no way to receive generic arguments from + // an annotation, so reject them outright. + if !f.generics.is_empty() { + return Err(diag( + format!("@test function {} cannot be generic", f.id.value), + &ann.span, + )); + } + + // Index the annotation inputs by name, rejecting duplicates: collecting + // silently would keep only the last value for a repeated name. + let mut inputs_by_name = HashMap::new(); + for input in &ann.inputs { + if inputs_by_name + .insert(input.name.value.as_str(), input) + .is_some() + { + return Err(diag( + format!( + "duplicate @test input {} for {}", + input.name.value, f.id.value + ), + &input.span, + )); + } + } + + // Every input must name one of the function's parameters. + for input in &ann.inputs { + if !f.parameters.iter().any(|p| p.id.value == input.name.value) { + return Err(diag( + format!( + "@test input {} does not match any parameter of {}", + input.name.value, f.id.value + ), + &input.span, + )); + } + } + + // Walk the parameters in signature order; each must be scalar and have + // exactly one input. This also fixes the output order to parameter order. + let mut inputs = Vec::new(); + for p in &f.parameters { + // Resolve the declared type to a canonical Ty *first*, then apply the + // scalar restriction to that. Checking the AST syntax directly would + // wrongly reject scalar aliases (e.g. `type Word = u32`), which parse + // as a named type but resolve to Ty::Uint(32). + let ty = g + .type_impl_::(&p.ty) + .map_err(|e| diag(e, type_span(&p.ty)))?; + + // Scalar-only for now: compound inputs would additionally need to be + // flattened into per-leaf scalars ("x.0", "x.1", ...) to be usable by + // the interpreter (see interp::extract); reject them until then. This + // scalar set matches interp::extract's scalar leaves. + if !matches!(ty, Ty::Uint(_) | Ty::Field | Ty::Bool | Ty::Integer) { + return Err(diag( + format!( + "parameter {} of @test function {} has a non-scalar type; \ + only field, bool, and u8..u64 parameters are supported", + p.id.value, f.id.value + ), + &p.span, + )); + } + + let input = inputs_by_name.remove(p.id.value.as_str()).ok_or_else(|| { + diag( + format!( + "@test on {} is missing a value for parameter {}", + f.id.value, p.id.value + ), + &ann.span, + ) + })?; + + // Type unsuffixed literals by the parameter they bind to, exactly as + // const_decl_ types them by the constant's declared type. Without + // this, `x = 2` would always evaluate as a field element, even for a + // u32 parameter. + let mut expr = input.value.clone(); + let mut rw = ZConstLiteralRewriter::new(Some(ty.clone())); + rw.visit_expression(&mut expr) + .map_err(|e| diag(e.0, &input.span))?; + + // The const evaluator: reduces the expression tree to a single + // constant term, or errors (with source context). + let t = g + .expr_impl_::(&expr) + .map_err(|e| format!("{}\nIn {}", e, file.display()))?; + + // The evaluated type must be exactly the parameter's type; the + // interpreter downstream trusts this and does not re-check. + if t.type_() != &ty { + return Err(diag( + format!( + "@test input {} for {}: expected type {}, but {} evaluates to {}", + input.name.value, + f.id.value, + ty, + input.value.span().as_str(), + t.type_() + ), + &input.span, + )); + } + + // Pull the concrete Value out of the constant term. + let value = const_value_simple(&t.term).ok_or_else(|| { + diag( + format!( + "@test input {} of {} did not evaluate to a constant", + input.name.value, f.id.value + ), + &input.span, + ) + })?; + inputs.push(TestCaseInput { + name: input.name.value.clone(), + // No visibility keyword defaults to public, matching + // interpret_visibility. + public: !matches!(p.visibility, Some(ast::Visibility::Private(_))), + source: input.value.span().as_str().to_string(), + value, + }); + } + + Ok(TestCase { + name: f.id.value.clone(), + has_return: f.return_type.is_some(), + inputs, + }) } struct ZGen<'ast> { diff --git a/src/front/zsharpcurly/zvisit/walkfns.rs b/src/front/zsharpcurly/zvisit/walkfns.rs index 2ecc8bec..a5e64f76 100644 --- a/src/front/zsharpcurly/zvisit/walkfns.rs +++ b/src/front/zsharpcurly/zvisit/walkfns.rs @@ -157,6 +157,14 @@ pub fn walk_function_definition<'ast, Z: ZVisitorMut<'ast>>( visitor: &mut Z, fundef: &mut ast::FunctionDefinition<'ast>, ) -> ZVisitorResult { + // Note: typing annotation inputs requires the function's parameter + // types, which a generic visitor does not know; that is done with a + // per-parameter type hint in eval_test_case (mod.rs). The structural + // walk here still covers the annotation so that visitors (identifier + // collection, rewriting, linting, ...) see every AST child. + if let Some(t) = fundef.test.as_mut() { + visitor.visit_test_annotation(t)?; + } visitor.visit_identifier_expression(&mut fundef.id)?; fundef .generics @@ -176,6 +184,26 @@ pub fn walk_function_definition<'ast, Z: ZVisitorMut<'ast>>( visitor.visit_span(&mut fundef.span) } +pub fn walk_test_annotation<'ast, Z: ZVisitorMut<'ast>>( + visitor: &mut Z, + testann: &mut ast::TestAnnotation<'ast>, +) -> ZVisitorResult { + testann + .inputs + .iter_mut() + .try_for_each(|i| visitor.visit_test_input(i))?; + visitor.visit_span(&mut testann.span) +} + +pub fn walk_test_input<'ast, Z: ZVisitorMut<'ast>>( + visitor: &mut Z, + testinput: &mut ast::TestInput<'ast>, +) -> ZVisitorResult { + visitor.visit_identifier_expression(&mut testinput.name)?; + visitor.visit_expression(&mut testinput.value)?; + visitor.visit_span(&mut testinput.span) +} + pub fn walk_parameter<'ast, Z: ZVisitorMut<'ast>>( visitor: &mut Z, param: &mut ast::Parameter<'ast>, diff --git a/src/front/zsharpcurly/zvisit/zvmut.rs b/src/front/zsharpcurly/zvisit/zvmut.rs index 6ec2a08e..5732a47b 100644 --- a/src/front/zsharpcurly/zvisit/zvmut.rs +++ b/src/front/zsharpcurly/zvisit/zvmut.rs @@ -101,6 +101,14 @@ pub trait ZVisitorMut<'ast>: Sized { walk_function_definition(self, fundef) } + fn visit_test_annotation(&mut self, testann: &mut ast::TestAnnotation<'ast>) -> ZVisitorResult { + walk_test_annotation(self, testann) + } + + fn visit_test_input(&mut self, testinput: &mut ast::TestInput<'ast>) -> ZVisitorResult { + walk_test_input(self, testinput) + } + fn visit_parameter(&mut self, param: &mut ast::Parameter<'ast>) -> ZVisitorResult { walk_parameter(self, param) } diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs new file mode 100644 index 00000000..4633cfb2 --- /dev/null +++ b/tests/zok_test_inputs.rs @@ -0,0 +1,448 @@ +//! The input contract of `ZSharpCurlyFE::eval_test_inputs`: which `@test` +//! annotations are accepted, how their input expressions are typed and +//! evaluated, and which malformed annotations are rejected (and how). +//! +//! Each test writes its program to a uniquely named file in the OS temp dir, +//! so nothing touches the source tree and tests can run in parallel. + +#![cfg(all(feature = "smt", feature = "zokc"))] + +use circ::front::zsharpcurly::{TestCase, ZSharpCurlyFE}; +use circ::front::Mode; +use circ::ir::term::Value; +use std::sync::Once; + +static INIT: Once = Once::new(); + +/// A temp file that is deleted on drop — even when the test panics, so +/// failing tests don't leave files behind. +struct TempZok(std::path::PathBuf); + +impl Drop for TempZok { + fn drop(&mut self) { + let _ = std::fs::remove_file(&self.0); + } +} + +/// Write `src` to a unique temp file and run eval_test_inputs on it. +fn eval(test_name: &str, src: &str) -> Result, String> { + // The CirC config is process-global and can only be set once. + INIT.call_once(circ::cfg::set_default); + // The process id keeps concurrent `cargo test` processes from colliding + // on the same paths; the test name separates threads within a process. + let path = std::env::temp_dir().join(format!( + "zok_test_inputs_{}_{}.zok", + std::process::id(), + test_name + )); + std::fs::write(&path, src).unwrap(); + let guard = TempZok(path); + ZSharpCurlyFE::eval_test_inputs(guard.0.clone(), Mode::Proof) +} + +/// Assert a Value is a field element with the given integer value. +fn assert_field(v: &Value, expected: u64) { + match v { + Value::Field(f) => assert_eq!(f.i(), expected), + other => panic!("expected field {}, got {:?}", expected, other), + } +} + +/// Assert a Value is a bit-vector of the given width and integer value. +fn assert_uint(v: &Value, width: usize, expected: u64) { + match v { + Value::BitVector(b) => { + assert_eq!(b.width(), width); + assert_eq!(*b.uint(), expected); + } + other => panic!("expected u{} {}, got {:?}", width, expected, other), + } +} + +#[test] +fn constant_arithmetic_evaluates() { + let tests = eval( + "constant_arithmetic", + r#"@test y = 3 * 3; +def test_sq(private field y) -> field { + return y; +} +"#, + ) + .unwrap(); + assert_eq!(tests.len(), 1); + assert_eq!(tests[0].name, "test_sq"); + assert_eq!(tests[0].inputs.len(), 1); + assert_eq!(tests[0].inputs[0].name, "y"); + assert_eq!(tests[0].inputs[0].source, "3 * 3"); + assert_field(&tests[0].inputs[0].value, 9); +} + +#[test] +fn named_constant_resolves() { + let tests = eval( + "named_constant", + r#"const field C = 7; + +@test x = C + 1; +def test_c(private field x) -> field { + return x; +} +"#, + ) + .unwrap(); + assert_field(&tests[0].inputs[0].value, 8); +} + +#[test] +fn const_function_call_evaluates() { + // The const evaluator supports calls to (non-generic, constant-input) + // functions; "non-constant" means evaluator-rejected, not "contains a + // call". + let tests = eval( + "const_fn_call", + r#"def sq(field a) -> field { + return a * a; +} + +@test y = sq(3); +def test_sq(private field y) -> field { + return y; +} +"#, + ) + .unwrap(); + assert_field(&tests[0].inputs[0].value, 9); +} + +#[test] +fn all_scalar_types_evaluate() { + let tests = eval( + "all_scalars", + r#"@test b = true, n8 = 4u8, n16 = 4u16, n32 = 4u32, n64 = 4u64, f = 5f; +def test_scalars(private bool b, private u8 n8, private u16 n16, private u32 n32, private u64 n64, private field f) -> bool { + return b; +} +"#, + ) + .unwrap(); + let inputs = &tests[0].inputs; + assert_eq!(inputs.len(), 6); + assert!(matches!(inputs[0].value, Value::Bool(true))); + assert_uint(&inputs[1].value, 8, 4); + assert_uint(&inputs[2].value, 16, 4); + assert_uint(&inputs[3].value, 32, 4); + assert_uint(&inputs[4].value, 64, 4); + assert_field(&inputs[5].value, 5); +} + +#[test] +fn unsuffixed_literal_typed_by_parameter() { + // The key typing rule: a bare `2` binding to a u32 parameter must come + // back as a 32-bit bit-vector, not as a field element. + let tests = eval( + "unsuffixed_u32", + r#"@test x = 2; +def test_u(private u32 x) -> u32 { + return x; +} +"#, + ) + .unwrap(); + assert_uint(&tests[0].inputs[0].value, 32, 2); +} + +#[test] +fn bare_test_zero_params_ok() { + let tests = eval( + "bare_zero_params", + r#"@test; +def test_noargs() -> bool { + return true; +} +"#, + ) + .unwrap(); + assert_eq!(tests[0].name, "test_noargs"); + assert!(tests[0].inputs.is_empty()); +} + +#[test] +fn bare_test_with_params_rejected() { + let err = eval( + "bare_with_params", + r#"@test; +def test_missing(private field x) -> field { + return x; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("missing a value for parameter x"), "{}", err); +} + +#[test] +fn missing_input_rejected() { + let err = eval( + "missing_input", + r#"@test a = 1; +def test_two(private field a, private field b) -> field { + return a; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("missing a value for parameter b"), "{}", err); +} + +#[test] +fn unknown_input_rejected() { + let err = eval( + "unknown_input", + r#"@test a = 1, nope = 2; +def test_one(private field a) -> field { + return a; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("nope does not match any parameter"), "{}", err); +} + +#[test] +fn duplicate_input_rejected() { + let err = eval( + "duplicate_input", + r#"@test a = 1, a = 2; +def test_dup(private field a) -> field { + return a; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("duplicate @test input a"), "{}", err); +} + +#[test] +fn non_constant_expression_rejected() { + let err = eval( + "non_constant", + r#"@test x = undefined_thing; +def test_bad(private field x) -> field { + return x; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("undefined_thing"), "{}", err); +} + +#[test] +fn array_parameter_rejected() { + let err = eval( + "array_param", + r#"@test xs = [1, 2]; +def test_arr(private field[2] xs) -> field { + return xs[0]; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("non-scalar"), "{}", err); +} + +#[test] +fn scalar_type_alias_accepted() { + // A `type` alias for a scalar resolves to a scalar Ty and must be + // accepted, even though it parses as a named (non-Basic) type. + let tests = eval( + "scalar_alias", + r#"type Word = u32; + +@test x = 2; +def test_alias(private Word x) -> Word { + return x; +} +"#, + ) + .unwrap(); + assert_uint(&tests[0].inputs[0].value, 32, 2); +} + +#[test] +fn generic_test_function_rejected() { + let err = eval( + "generic_fn", + r#"@test x = 1; +def test_gen(private field x) -> field { + return x; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("cannot be generic"), "{}", err); +} + +#[test] +fn type_mismatch_rejected() { + // `true` cannot bind to a field parameter; the diagnostic must name + // both the expected and the actual type. + let err = eval( + "type_mismatch", + r#"@test x = true; +def test_ty(private field x) -> field { + return x; +} +"#, + ) + .unwrap_err(); + assert!(err.contains("expected type field"), "{}", err); + assert!(err.contains("bool"), "{}", err); +} + +#[test] +fn annotation_sees_later_declarations() { + // Annotation expressions have module-wide visibility: they are + // evaluated after every declaration is processed, so forward references + // to constants and functions declared later in the file work. + let tests = eval( + "decl_order", + r#"@test x = LATER + double(2); +def test_order(private field x) { + assert(x == 14); +} + +const field LATER = 10; + +def double(field n) -> field { + return n + n; +} +"#, + ) + .unwrap(); + assert_field(&tests[0].inputs[0].value, 14); +} + +#[test] +fn call_arguments_not_typed_by_parameter() { + // Known limit: parameter-directed literal typing does not descend into + // call arguments, so the bare `2` defaults to field and clashes with + // id's u32 parameter... + let err = eval( + "call_arg_bare", + r#"def id(u32 x) -> u32 { + return x; +} + +@test y = id(2); +def test_id(private u32 y) { + assert(y == 2u32); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("mismatch"), "{}", err); + + // ...suffixing the literal is the supported form. + let tests = eval( + "call_arg_suffixed", + r#"def id(u32 x) -> u32 { + return x; +} + +@test y = id(2u32); +def test_id(private u32 y) { + assert(y == 2u32); +} +"#, + ) + .unwrap(); + assert_uint(&tests[0].inputs[0].value, 32, 2); +} + +#[test] +fn inputs_returned_in_parameter_order() { + // Annotation lists b before a; results follow the signature: a, then b. + let tests = eval( + "param_order", + r#"@test b = 2, a = 1; +def test_order(private field a, private field b) -> field { + return a; +} +"#, + ) + .unwrap(); + assert_eq!(tests[0].inputs[0].name, "a"); + assert_field(&tests[0].inputs[0].value, 1); + assert_eq!(tests[0].inputs[1].name, "b"); + assert_field(&tests[0].inputs[1].value, 2); +} + +#[test] +fn visibility_captured_per_parameter() { + // private -> public: false; public -> true; no keyword defaults to + // public, matching the frontend's interpret_visibility. + let tests = eval( + "visibility", + r#"@test a = 1, b = 2, c = 3; +def test_vis(private field a, public field b, field c) { + assert(a + b + c == 6); +} +"#, + ) + .unwrap(); + let inputs = &tests[0].inputs; + assert!(!inputs[0].public, "private a"); + assert!(inputs[1].public, "public b"); + assert!(inputs[2].public, "unannotated c defaults to public"); +} + +#[test] +fn has_return_exposed() { + // Runners use this to tell self-checking assert-style tests (no return + // type) from return-typed ones (unsupported in the MVP). + let tests = eval( + "has_return", + r#"@test x = 1; +def test_assert_style(private field x) { + assert(x == 1); +} + +@test y = 2; +def test_return_style(private field y) -> field { + return y; +} +"#, + ) + .unwrap(); + assert!(!tests[0].has_return, "assert-style test has no return type"); + assert!(tests[1].has_return, "return-typed test is flagged"); +} + +#[test] +fn plain_functions_skipped() { + let tests = eval( + "plain_skipped", + r#"def helper(field n) -> field { + return n + 1; +} + +@test x = 1; +def test_only(private field x) -> field { + return x; +} +"#, + ) + .unwrap(); + assert_eq!(tests.len(), 1); + assert_eq!(tests[0].name, "test_only"); +} + +#[test] +fn malformed_file_panics() { + // Documents current behavior: parse errors are panics inside the + // frontend (via ZLoad), not Errs. Runners must catch_unwind (as + // examples/ztest.rs does) until a fallible loader API exists. + let result = std::panic::catch_unwind(|| eval("malformed", "def broken( {")); + assert!(result.is_err()); +} diff --git a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs index 76ae1a91..9a74701b 100644 --- a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs +++ b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs @@ -1628,18 +1628,4 @@ mod tests { assert_eq!(ann.inputs[0].name.value, "a"); assert_eq!(ann.inputs[1].name.value, "b"); } - - #[test] - fn bare_marker_still_parses() { - let source = r#"@test; - def t() -> bool { return true; } -"#; - let ast = generate_ast(source).unwrap(); - let f = match &ast.declarations[0] { - SymbolDeclaration::Function(f) => f, - _ => panic!("expected a function"), - }; - let ann = f.test.as_ref().expect("should carry @test"); - assert_eq!(ann.inputs.len(), 0); - } } From d396732c4be3b96ab1e18e2878949973e3933932 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Fri, 17 Jul 2026 14:02:18 -0400 Subject: [PATCH 04/29] Add end-to-end test runner and array support Introduce a reusable test runner (src/test_runner) that orchestrates @test functions end-to-end: compile -> assert-check -> setup -> prove -> verify. Add compile::opt_for_proof to centralize the proof-mode IR optimization pipeline and use it from the CLI driver (examples/circ.rs) and the runner. Refactor ZoKratesCurly frontend types: make TestCase and TestCaseInput fields private and expose read-only accessors; add TestCaseInput::flat_entries and interp::flatten to expand array inputs into per-leaf scalar input entries. Validate and accept arrays-of-scalars (including nested arrays), reject zero-length arrays, and improve error diagnostics. Update examples/ztest.rs to use the new test_runner API and choose the proof backend there. Add many new/updated unit tests exercising array handling and input flattening, and register the ztest_e2e test in Cargo.toml. Misc: small formatting/brace fixes in examples/circ.rs and reorder modules in lib.rs to expose the new test_runner under the appropriate feature gates. --- Cargo.toml | 4 + examples/circ.rs | 44 +- examples/ztest.rs | 159 ++---- src/compile.rs | 47 +- src/front/zsharpcurly/interp.rs | 37 ++ src/front/zsharpcurly/mod.rs | 145 +++++- src/lib.rs | 14 +- src/test_runner/mod.rs | 215 ++++++++ tests/zok_test_inputs.rs | 462 ++++++++++++++++-- tests/ztest_e2e.rs | 269 ++++++++++ .../zokrates_pest_ast/src/lib.rs | 26 + 11 files changed, 1216 insertions(+), 206 deletions(-) create mode 100644 src/test_runner/mod.rs create mode 100644 tests/ztest_e2e.rs diff --git a/Cargo.toml b/Cargo.toml index 6ca11235..1da16315 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -146,5 +146,9 @@ required-features = ["smt", "zokc", "bellman"] name = "zok_test_inputs" required-features = ["smt", "zokc"] +[[test]] +name = "ztest_e2e" +required-features = ["smt", "zokc", "bellman"] + [profile.release] debug = true diff --git a/examples/circ.rs b/examples/circ.rs index 30a4d7d1..da848970 100644 --- a/examples/circ.rs +++ b/examples/circ.rs @@ -326,37 +326,7 @@ fn main() { // vec![Opt::Sha, Opt::ConstantFold, Opt::Mem, Opt::ConstantFold], ) } - Mode::Proof | Mode::ProofOfHighValue(_) => { - let mut opts = Vec::new(); - - opts.push(Opt::ConstantFold(Box::new([]))); - opts.push(Opt::DeskolemizeWitnesses); - opts.push(Opt::ScalarizeVars); - opts.push(Opt::Flatten); - opts.push(Opt::Sha); - opts.push(Opt::ConstantFold(Box::new([]))); - opts.push(Opt::ParseCondStores); - // Tuples must be eliminated before oblivious array elim - opts.push(Opt::ConstantFold(Box::new([]))); - opts.push(Opt::Obliv); - // The obliv elim pass produces more tuples, that must be eliminated - opts.push(Opt::SetMembership); - opts.push(Opt::PersistentRam); - opts.push(Opt::VolatileRam); - if options.circ.ir.fits_in_bits_ip { - opts.push(Opt::FitsInBitsIp); - } - opts.push(Opt::SkolemizeChallenges); - opts.push(Opt::ScalarizeVars); - opts.push(Opt::ConstantFold(Box::new([]))); - opts.push(Opt::Obliv); - opts.push(Opt::LinearScan); - // The linear scan pass produces more tuples, that must be eliminated - opts.push(Opt::Tuple); - opts.push(Opt::Flatten); - opts.push(Opt::ConstantFold(Box::new([]))); - opt(cs, opts) - } + Mode::Proof | Mode::ProofOfHighValue(_) => circ::compile::opt_for_proof(cs, cfg()), }; println!("Running backend"); match options.backend { @@ -427,9 +397,13 @@ fn main() { ) .unwrap(), #[cfg(not(feature = "spartan"))] - ProofImpl::Spartan | ProofImpl::Dorian => panic!("Missing feature: spartan"), + ProofImpl::Spartan | ProofImpl::Dorian => { + panic!("Missing feature: spartan") + } #[cfg(not(feature = "bellman"))] - ProofImpl::Groth16 | ProofImpl::Mirage => panic!("Missing feature: bellman"), + ProofImpl::Groth16 | ProofImpl::Mirage => { + panic!("Missing feature: bellman") + } }; } #[cfg(feature = "bellman")] @@ -444,7 +418,9 @@ fn main() { verifier_key, ) .unwrap(), - ProofImpl::Spartan | ProofImpl::Dorian => panic!("Spartan/Dorian is not CP"), + ProofImpl::Spartan | ProofImpl::Dorian => { + panic!("Spartan/Dorian is not CP") + } }; } #[cfg(not(feature = "bellman"))] diff --git a/examples/ztest.rs b/examples/ztest.rs index 49b539da..f1dd2f9f 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -2,19 +2,30 @@ /// 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) -> setup -> prove -> verify -/// and prints ok / FAILED per test. A test passes when its assertions hold, -/// i.e. when a proof can be produced and verifies (backend: Groth16 over -/// BLS12-381, hardcoded for the MVP). +/// compile (test fn as entry point) -> assert check -> setup -> prove -> verify +/// and prints ok / FAILED per test. A test passes when its assertions +/// evaluate to true on the given inputs (checked by direct IR evaluation — +/// the proof pipeline alone can pass vacuously when optimization eliminates +/// a private variable) AND a proof can be produced and verifies (backend: +/// Groth16 over BLS12-381, hardcoded for the MVP). +/// +/// Performance note: every array leaf is a distinct circuit input. For a +/// *public* array all of its leaves are public inputs, so verification cost +/// and verifying-key size grow linearly with the leaf count under Groth16; +/// prefer testing large arrays as `private` witnesses and keeping `public` +/// arrays to small expected values. (Visibility itself is a protocol choice, +/// not a performance knob — this is just what it costs with this backend.) +/// +/// 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::{Inputs, TestCase, ZSharpCurlyFE}; -use circ::front::{FrontEnd, Mode}; +use circ::front::zsharpcurly::ZSharpCurlyFE; +use circ::front::Mode; use circ::ir::term::Value; use circ::target::r1cs::bellman::Bellman; -use circ::target::r1cs::proof::ProofSystem; +use circ::test_runner::{catch, run_test, Outcome}; use clap::Parser; -use fxhash::FxHashMap; use std::path::PathBuf; #[derive(Debug, Parser)] @@ -31,16 +42,6 @@ struct Options { circ: CircOpt, } -/// The outcome of running one test. -enum Outcome { - /// The proof verified: all assertions hold. - Pass, - /// Proving or verifying failed: an assertion does not hold. - Fail(String), - /// The test could not be run at all (e.g. unsupported shape). - Error(String), -} - /// 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 { @@ -48,87 +49,19 @@ fn pretty_value(v: &Value) -> String { Value::Field(f) => f.i().to_string(), Value::BitVector(b) => b.uint().to_string(), Value::Bool(b) => b.to_string(), - // Anything else (arrays, tuples, ...): fall back to the default form. + Value::Array(a) => format!( + "[{}]", + a.values() + .iter() + .map(pretty_value) + .collect::>() + .join(", ") + ), + // Anything else (tuples, ...): fall back to the default form. other => other.to_string(), } } -/// Run `f`, catching panics and silencing the default panic hook only for -/// the duration of the call (the frontend and the prover report failures by -/// panicking). Returns the panic message on unwind. -fn catch(f: impl FnOnce() -> R) -> Result { - let prev_hook = std::panic::take_hook(); - std::panic::set_hook(Box::new(|_| {})); - let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(f)); - std::panic::set_hook(prev_hook); - result.map_err(|e| { - if let Some(msg) = e.downcast_ref::() { - msg.clone() - } else if let Some(msg) = e.downcast_ref::<&str>() { - (*msg).to_string() - } else { - "unknown panic".to_string() - } - }) -} - -/// Run one test through compile -> setup -> prove -> verify. -fn run_test(path: &std::path::Path, test: &TestCase) -> Outcome { - // MVP supports assert-style tests only: a return-typed test computes a - // value, but the annotation gives no expected output to check it against. - if test.has_return { - return Outcome::Error( - "test functions with a return type are not supported (yet); \ - drop the return type and use assert(...)" - .to_string(), - ); - } - - // Compile the test function as its own entry point and lower it to - // prover/verifier data. Compilation failures are errors, not test - // failures: the test never ran. - let name = test.name.clone(); - let file = path.to_path_buf(); - let setup = catch(move || { - let comps = ZSharpCurlyFE::gen(Inputs { - file, - entry: name.clone(), - mode: Mode::Proof, - }); - let cs = comps.get(&name); - let (p_data, v_data, _stats) = circ::compile::to_proof_data(cs, circ::cfg::cfg()); - Bellman::::setup(p_data, v_data) - }); - let (pk, vk) = match setup { - Ok(keys) => keys, - Err(e) => return Outcome::Error(e), - }; - - // The prover knows every input; the verifier sees only the public ones. - let prover_map: FxHashMap = test - .inputs - .iter() - .map(|i| (i.name.clone(), i.value.clone())) - .collect(); - let verifier_map: FxHashMap = test - .inputs - .iter() - .filter(|i| i.public) - .map(|i| (i.name.clone(), i.value.clone())) - .collect(); - - // Prove and verify. An assertion that does not hold makes the witness - // unsatisfiable, which the prover reports by panicking. - match catch(|| { - let pf = Bellman::::prove(&pk, &prover_map); - Bellman::::verify(&vk, &verifier_map, &pf) - }) { - Ok(true) => Outcome::Pass, - Ok(false) => Outcome::Fail("proof did not verify".to_string()), - Err(e) => Outcome::Fail(e), - } -} - fn main() { env_logger::Builder::from_default_env() .format_level(false) @@ -168,42 +101,46 @@ fn main() { // Show each input as `name = = `, collapsing to // `name = ` when the source is already just the value. let inputs: Vec = t - .inputs + .inputs() .iter() .map(|input| { - let value = pretty_value(&input.value); - if input.source == value { - format!("{} = {}", input.name, value) + let value = pretty_value(input.value()); + if input.source() == value { + format!("{} = {}", input.name(), value) } else { - format!("{} = {} = {}", input.name, input.source, value) + format!("{} = {} = {}", input.name(), input.source(), value) } }) .collect(); - print!("test {} ({}) ... ", t.name, inputs.join(", ")); + print!("test {} ({}) ... ", t.name(), 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(); - match run_test(&options.path, t) { + // Groth16 over BLS12-381 is hardcoded for the MVP; run_test is + // generic over the proof system, so this is the one place the backend + // is chosen. + let indent = |msg: String| { + // The prover's message spans several lines; indent them all. + for line in msg.lines() { + println!(" {}", line); + } + }; + match run_test::>(t) { Outcome::Pass => { passed += 1; println!("ok"); } - Outcome::Fail(msg) => { + Outcome::AssertionFailed(msg) => { failed += 1; println!("FAILED"); - // The prover's message spans several lines; indent them all. - for line in msg.lines() { - println!(" {}", line); - } + indent(msg); } - Outcome::Error(msg) => { + Outcome::Unsupported(msg) | Outcome::CompileError(msg) | Outcome::BackendError(msg) => { errored += 1; println!("error"); - for line in msg.lines() { - println!(" {}", line); - } + indent(msg); } } } diff --git a/src/compile.rs b/src/compile.rs index 3a77e1bb..c68798ba 100644 --- a/src/compile.rs +++ b/src/compile.rs @@ -4,11 +4,56 @@ //! [`Computation`] into the data a proof system needs — without writing files. use crate::cfg::CircCfg; -use crate::ir::term::Computation; +use crate::ir::opt::{opt, Opt}; +use crate::ir::term::{Computation, Computations}; use crate::target::r1cs::opt::reduce_linearities; use crate::target::r1cs::trans::to_r1cs; use crate::target::r1cs::{ProverData, R1csStats, VerifierData}; +/// Run the canonical proof-mode IR optimization pipeline on a set of +/// [`Computations`]. +/// +/// This is the single owner of the pass list the CLI driver (`examples/circ.rs` +/// `Mode::Proof`) and the unit-test runner both use, so they cannot drift. The +/// passes are backend-independent (Groth16, Mirage, and Spartan all consume the +/// same optimized IR); the only configurable input is +/// [`cfg.ir.fits_in_bits_ip`](crate::cfg). This must run before [`to_proof_data`]: +/// R1CS lowering embeds scalar sorts only, so array/tuple terms have to be +/// scalarized and eliminated here first. +pub fn opt_for_proof(cs: Computations, cfg: &CircCfg) -> Computations { + let mut opts = vec![ + Opt::ConstantFold(Box::new([])), + Opt::DeskolemizeWitnesses, + Opt::ScalarizeVars, + Opt::Flatten, + Opt::Sha, + Opt::ConstantFold(Box::new([])), + Opt::ParseCondStores, + // Tuples must be eliminated before oblivious array elim + Opt::ConstantFold(Box::new([])), + Opt::Obliv, + // The obliv elim pass produces more tuples, that must be eliminated + Opt::SetMembership, + Opt::PersistentRam, + Opt::VolatileRam, + ]; + if cfg.ir.fits_in_bits_ip { + opts.push(Opt::FitsInBitsIp); + } + opts.extend([ + Opt::SkolemizeChallenges, + Opt::ScalarizeVars, + Opt::ConstantFold(Box::new([])), + Opt::Obliv, + Opt::LinearScan, + // The linear scan pass produces more tuples, that must be eliminated + Opt::Tuple, + Opt::Flatten, + Opt::ConstantFold(Box::new([])), + ]); + opt(cs, opts) +} + /// Lower a compiled [`Computation`] to R1CS, run the standard R1CS /// optimizations, and produce the prover and verifier data used by a proof /// system's `setup`, `prove`, and `verify`. diff --git a/src/front/zsharpcurly/interp.rs b/src/front/zsharpcurly/interp.rs index 7c2011bf..6a0313a6 100644 --- a/src/front/zsharpcurly/interp.rs +++ b/src/front/zsharpcurly/interp.rs @@ -53,3 +53,40 @@ pub fn extract( )), } } + +/// Inverse of [extract] for the value shapes `@test` supports: break a +/// constant [Value] into the flattened per-leaf scalar entries the proof +/// pipeline uses in input maps. A scalar yields a single (`name`, value) +/// entry; an array yields one entry per element under `name.0`, `name.1`, +/// ..., recursively (a `field[2][2]` named `A` yields `A.0.0` .. `A.1.1`). +/// Ordering and naming mirror [extract] and `declare_input`. +/// +/// This is deliberately *value-only* and limited to indexed arrays: +/// [Array::values] handles sparse arrays (e.g. from `[0; 4]`, whose backing +/// map is empty) by falling back to the array's default. Tuples and structs +/// are not handled — a struct lowers to a [Value::Tuple], which no longer +/// carries the field names `name.field` flattening would need; supporting +/// them will need the resolved [Ty], not just the value. `eval_test_case` +/// rejects those parameter types (and every non-scalar leaf kind) before one +/// can reach here, so the leaf arms below are exhaustive for validated +/// inputs; anything else is an internal invariant violation. +pub fn flatten(name: &str, value: &Value) -> Vec<(String, Value)> { + match value { + Value::Array(arr) => arr + .values() + .into_iter() + .enumerate() + .flat_map(|(i, v)| flatten(&format!("{name}.{i}"), &v)) + .collect(), + // The scalar leaf kinds a validated @test input can hold — the same + // set interp::extract accepts. + Value::Field(_) | Value::BitVector(_) | Value::Bool(_) | Value::Int(_) => { + vec![(name.to_string(), value.clone())] + } + other => unreachable!( + "non-scalar leaf {:?} in @test input {}; \ + eval_test_inputs rejects non-scalar parameter types", + other, name + ), + } +} diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index cf4817c4..39f603d1 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -18,7 +18,7 @@ use rug::Integer; use std::cell::{Cell, RefCell}; use std::collections::HashMap; use std::fmt::Display; -use std::path::PathBuf; +use std::path::{Path, PathBuf}; use std::str::FromStr; use std::time; use zokrates_curly_pest_ast as ast; @@ -48,31 +48,90 @@ pub struct Inputs { /// runner policy. In particular, return-typed test functions are /// discovered (see [Self::has_return]) and it is up to the runner to /// support or reject them. +/// +/// Fields are private with read-only accessors: only +/// [`ZSharpCurlyFE::eval_test_inputs`] (in-crate) constructs these, and +/// external code cannot construct *or mutate* one, so downstream consumers +/// (e.g. [`TestCaseInput::flat_entries`]) can trust the invariant holds. #[derive(Debug, Clone)] +#[non_exhaustive] pub struct TestCase { + name: String, + has_return: bool, + inputs: Vec, + /// The source file this test was discovered in — used to recompile it as + /// an entry point, keeping the case bound to its origin. + file: PathBuf, +} + +impl TestCase { /// The test function's name. - pub name: String, + pub fn name(&self) -> &str { + &self.name + } /// Whether the function declares a return type. Assert-style tests /// (no return type) are self-checking; a runner may not support /// return-typed tests, since the annotation gives no expected output. - pub has_return: bool, + pub fn has_return(&self) -> bool { + self.has_return + } /// The function's evaluated annotation inputs, in parameter order. - pub inputs: Vec, + pub fn inputs(&self) -> &[TestCaseInput] { + &self.inputs + } + /// The source file this test was discovered in. + pub fn file(&self) -> &Path { + &self.file + } } /// One evaluated `@test` annotation input, e.g. `y = 3 * 3`. +/// +/// Fields are private with read-only accessors; constructed only by the +/// validated door ([`ZSharpCurlyFE::eval_test_inputs`]). External code can +/// neither build nor mutate one, so [`Self::flat_entries`] can trust that +/// [`Self::value`] is a scalar or an array of scalars. #[derive(Debug, Clone)] +#[non_exhaustive] pub struct TestCaseInput { + name: String, + public: bool, + source: String, + value: Value, +} + +impl TestCaseInput { /// The input's name (the `y` in `y = 3 * 3`). - pub name: String, + pub fn name(&self) -> &str { + &self.name + } /// Whether the parameter this input binds to is public (`public` or no /// visibility keyword) rather than `private`. In a proof, public inputs /// are shared with the verifier; private inputs stay with the prover. - pub public: bool, + pub fn public(&self) -> bool { + self.public + } /// The input expression exactly as written in the source (`3 * 3`). - pub source: String, - /// The concrete value the expression evaluates to (`9`). - pub value: Value, + pub fn source(&self) -> &str { + &self.source + } + /// The concrete value the expression evaluates to (`9`). Arrays are + /// stored whole, as a [Value::Array]; use [Self::flat_entries] to get + /// the per-leaf scalar entries the proof pipeline consumes. + pub fn value(&self) -> &Value { + &self.value + } + + /// The flattened `(input-name, scalar-value)` entries this input + /// contributes to a proof-pipeline input map. A scalar maps to itself + /// under the bare parameter name; an array yields one entry per leaf + /// under dotted index names (`field[2][2] A` yields `A.0.0` .. + /// `A.1.1`), matching the circuit variables `declare_input` creates. + /// Each leaf becomes one circuit input; the parameter's visibility + /// (`public`) applies to all of its leaves. + pub fn flat_entries(&self) -> Vec<(String, Value)> { + interp::flatten(&self.name, &self.value) + } } #[allow(dead_code)] @@ -161,10 +220,14 @@ impl ZSharpCurlyFE { /// Inputs are validated against the function's signature: /// * every input must name a parameter, exactly once, and every /// parameter must receive an input; - /// * only scalar parameters (`field`, `bool`, `u8`..`u64`) are supported; + /// * parameters may be scalars (`field`, `bool`, `u8`..`u64`) or + /// (possibly nested) arrays of scalars; structs, tuples, and + /// zero-length arrays are rejected; /// * unsuffixed literals are typed by the parameter they bind to (so - /// `x = 2` for a `u32 x` is a `u32`), and the evaluated type must - /// match the parameter's declared type; + /// `x = 2` for a `u32 x` is a `u32`, and `xs = [1, 2]` for a + /// `u32[2] xs` types each element), and the evaluated type must + /// match the parameter's declared type — for arrays this also checks + /// length and element type; /// * generic test functions are rejected. /// /// Known limits and semantics: @@ -215,6 +278,36 @@ impl ZSharpCurlyFE { } } +/// Is `ty` a scalar, or a (possibly nested) array whose base element is a +/// scalar? These are the parameter types `@test` supports: their values +/// flatten to the per-leaf scalar inputs the proof pipeline expects (see +/// [TestCaseInput::flat_entries]). Exhaustive on purpose: a new `Ty` +/// variant must decide whether it is supported. +fn is_scalar_or_scalar_array(ty: &Ty) -> bool { + match ty { + Ty::Uint(_) | Ty::Field | Ty::Bool | Ty::Integer => true, + Ty::Array(_, elem) => is_scalar_or_scalar_array(elem), + Ty::MutArray(_) | Ty::Struct(..) | Ty::Tuple(..) => false, + } +} + +/// Does `ty` contain a zero-length array dimension? Such an input would +/// flatten to no circuit inputs at all — a silent no-op — so the door +/// rejects it. `[]` values already fail const evaluation ("Empty array"), +/// but `[0; 0]` would evaluate cleanly without this type-level guard. +fn has_zero_length_array(ty: &Ty) -> bool { + match ty { + Ty::Array(n, elem) => *n == 0 || has_zero_length_array(elem), + Ty::Uint(_) + | Ty::Field + | Ty::Bool + | Ty::Integer + | Ty::MutArray(_) + | Ty::Struct(..) + | Ty::Tuple(..) => false, + } +} + /// Validate one `@test` function's annotation against its signature and /// evaluate each input to a concrete value. See [ZSharpCurlyFE::eval_test_inputs] /// for the rules enforced here. @@ -289,16 +382,27 @@ fn eval_test_case<'ast>( .type_impl_::(&p.ty) .map_err(|e| diag(e, type_span(&p.ty)))?; - // Scalar-only for now: compound inputs would additionally need to be - // flattened into per-leaf scalars ("x.0", "x.1", ...) to be usable by - // the interpreter (see interp::extract); reject them until then. This - // scalar set matches interp::extract's scalar leaves. - if !matches!(ty, Ty::Uint(_) | Ty::Field | Ty::Bool | Ty::Integer) { + // Scalars and arrays of scalars: array values are flattened into + // per-leaf scalar inputs ("A.0", "A.1.0", ...) by flat_entries — the + // same names declare_input and interp::extract use. Structs and + // tuples are not supported yet. + if !is_scalar_or_scalar_array(&ty) { + return Err(diag( + format!( + "parameter {} of @test function {} has unsupported type {}; \ + only scalars (field, bool, u8..u64) and arrays of scalars \ + are supported", + p.id.value, f.id.value, ty + ), + &p.span, + )); + } + if has_zero_length_array(&ty) { return Err(diag( format!( - "parameter {} of @test function {} has a non-scalar type; \ - only field, bool, and u8..u64 parameters are supported", - p.id.value, f.id.value + "parameter {} of @test function {} has a zero-length array \ + type {}; zero-length test inputs are not supported", + p.id.value, f.id.value, ty ), &p.span, )); @@ -369,6 +473,7 @@ fn eval_test_case<'ast>( name: f.id.value.clone(), has_return: f.return_type.is_some(), inputs, + file: file.to_path_buf(), }) } diff --git a/src/lib.rs b/src/lib.rs index 56dcb2a4..5affa783 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -12,12 +12,18 @@ static GLOBAL: jemallocator::Jemalloc = jemallocator::Jemalloc; #[macro_use] pub mod ir; -pub mod compile; pub mod cfg; pub mod circify; -pub mod front; -pub mod target; -pub mod util; +pub mod compile; pub mod create_input; +pub mod front; #[cfg(feature = "spartan")] pub mod right_field_arithmetic; +pub mod target; +pub mod util; +// Orchestrates the ZoKratesCurly @test pipeline (frontend -> compile -> +// proof backend), so it needs the frontend's features plus R1CS. It sits +// above `front` on purpose: the frontend produces validated test metadata, +// this module consumes it — never the other way around. +#[cfg(all(feature = "smt", feature = "zokc", feature = "r1cs"))] +pub mod test_runner; diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs new file mode 100644 index 00000000..3d732bd9 --- /dev/null +++ b/src/test_runner/mod.rs @@ -0,0 +1,215 @@ +//! Executes one `@test` function end-to-end through the proof pipeline. +//! +//! This is the reusable core behind the `ztest` example: compile the test +//! function as its own entry point, check its assertions against the resolved +//! inputs, then run the full `setup -> prove -> verify` cycle in memory. +//! +//! It sits *above* the frontend on purpose: the ZoKrates frontend produces +//! validated test metadata ([`TestCase`]) and CirC IR; this module consumes +//! that read-only API and orchestrates compilation ([`crate::compile`]) and +//! the proof backend ([`crate::target::r1cs`]). The frontend does not depend +//! back on it. It is generic over the proof system ([`ProofSystem`]) so the +//! backend is chosen by the caller (the example instantiates Groth16 over +//! BLS12-381). That generic covers the [`ProofSystem`] implementors — Bellman +//! (Groth16) and Mirage — and is where their selection will plug in; Spartan +//! uses a separate `SpartanProofSystem` interface (and a different field), so +//! supporting it will take an adapter, not just a type argument. Presentation +//! — printing, exit codes, input formatting — stays in the caller, not here. + +use crate::cfg::cfg; +use crate::compile::{opt_for_proof, to_proof_data}; +use crate::front::zsharpcurly::{Inputs, TestCase, ZSharpCurlyFE}; +use crate::front::{FrontEnd, Mode}; +use crate::ir::term::{eval, Value}; +use crate::target::r1cs::proof::ProofSystem; +use fxhash::FxHashMap; +use std::cell::Cell; +use std::sync::Once; + +/// The outcome of running one test. +/// +/// Semantic outcomes (the test's assertions were accepted or rejected) are +/// kept distinct from infrastructure outcomes (the test could not be run, or a +/// backend step failed). A future `expect = accept|reject` setting keys off +/// [`Outcome::Pass`] / [`Outcome::AssertionFailed`] only — it must never treat +/// a [`Outcome::CompileError`] or [`Outcome::BackendError`] as a rejection. +#[derive(Debug)] +pub enum Outcome { + /// Assertions held for the given inputs and the proof verified. + Pass, + /// An assertion does not hold for the given inputs. This is the semantic + /// "the test rejected these inputs" signal. + AssertionFailed(String), + /// The test's shape is not runnable (e.g. it declares a return type, which + /// carries no expected output to check). + Unsupported(String), + /// The frontend, IR optimization, or R1CS lowering failed — the test could + /// not be turned into a circuit. + CompileError(String), + /// The backend failed to set up, prove, or verify a test whose assertions + /// already held. This is an infrastructure failure, NOT a rejection. + BackendError(String), +} + +thread_local! { + /// Set while a [catch] call is running on this thread, so the shared panic + /// hook stays quiet for *this thread's* panics only. + static SUPPRESS_PANIC: Cell = const { Cell::new(false) }; +} + +static HOOK_INIT: Once = Once::new(); + +/// Install, once per process, a panic hook that defers to the previous hook +/// except while the current thread is inside [catch]. Swapping the global hook +/// per call (take/quiet/restore) races under concurrency — two overlapping +/// calls can restore in the wrong order and leave the quiet hook installed for +/// good, or suppress an unrelated thread's panic. A thread-local flag consulted +/// by one installed-once hook avoids both: suppression is per-thread and the +/// global hook is never swapped after startup. +fn install_quiet_hook() { + HOOK_INIT.call_once(|| { + let prev = std::panic::take_hook(); + std::panic::set_hook(Box::new(move |info| { + if !SUPPRESS_PANIC.with(|s| s.get()) { + prev(info); + } + })); + }); +} + +/// Run `f`, converting a panic on the current thread into `Err(message)`. +/// +/// The frontend and the prover report failures by panicking, so callers must +/// unwind them into a value. Panic-hook noise is suppressed for the duration — +/// but only for this thread (see [install_quiet_hook]), so concurrent code and +/// later panics keep the normal hook. Cannot contain `process::exit` paths +/// (some frontend semantic errors exit rather than unwind). +/// +/// Exposed for callers that must also survive panics from the discovery phase +/// (e.g. [`ZSharpCurlyFE::eval_test_inputs`] panics on a parse/load failure). +pub fn catch(f: impl FnOnce() -> R) -> Result { + install_quiet_hook(); + let was = SUPPRESS_PANIC.with(|s| s.replace(true)); + let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(f)); + SUPPRESS_PANIC.with(|s| s.set(was)); + result.map_err(|e| { + if let Some(msg) = e.downcast_ref::() { + msg.clone() + } else if let Some(msg) = e.downcast_ref::<&str>() { + (*msg).to_string() + } else { + "unknown panic".to_string() + } + }) +} + +/// Run one `@test` function through compile -> assert check -> setup -> prove +/// -> verify, using the proof system `PS`. +/// +/// The test is recompiled from its own source file ([`TestCase::file`]), so the +/// case stays bound to the file it was discovered in — the caller cannot pair a +/// case with an unrelated path. The config is read from the process-global +/// [`cfg`]; the caller must have set it (via `circ::cfg::set` or `set_default`) +/// and it fixes the field/backend for the process. +pub fn run_test(test: &TestCase) -> Outcome { + // Assert-style tests only: a return-typed test computes a value, but the + // annotation gives no expected output to check it against. + if test.has_return() { + return Outcome::Unsupported( + "test functions with a return type are not supported (yet); \ + drop the return type and use assert(...)" + .to_string(), + ); + } + + // Compile the test function as its own entry point, from the file it was + // discovered in. A failure here means the test never became a circuit. + let name = test.name().to_string(); + let file = test.file().to_path_buf(); + let comps = match catch(move || { + ZSharpCurlyFE::gen(Inputs { + file, + entry: name, + mode: Mode::Proof, + }) + }) { + Ok(c) => c, + Err(e) => return Outcome::CompileError(e), + }; + + // Build the prover and verifier input maps in a single pass over the + // inputs — one flatten per input, not one per map. The prover knows every + // input; the verifier sees only the public ones. Arrays flatten to one + // entry per leaf ("A.0.0", ...), the names the compiled circuit declares + // its input variables under; scalars are a single bare-named entry. + let mut prover_map: FxHashMap = FxHashMap::default(); + let mut verifier_map: FxHashMap = FxHashMap::default(); + for input in test.inputs() { + let entries = input.flat_entries(); + if input.public() { + verifier_map.extend(entries.iter().cloned()); + } + prover_map.extend(entries); + } + + // Ground truth: evaluate every assertion directly against the prover's + // inputs on the un-optimized IR. This is the authoritative pass/fail + // verdict. The proof pipeline alone is not sufficient — it proves "a + // satisfying witness exists", and when an optimization eliminates a private + // variable (e.g. reduce_linearities substituting away a purely linear + // assert like `x == 99`), the input-map value is never enforced and an + // untrue test would pass vacuously. + let held = catch(|| { + comps + .get(test.name()) + .outputs + .iter() + .all(|a| matches!(eval(a, &prover_map), Value::Bool(true))) + }); + match held { + Ok(true) => {} + Ok(false) => { + return Outcome::AssertionFailed( + "an assertion does not hold for the given inputs".to_string(), + ) + } + // A panic while evaluating the compiled IR is an internal/compile-side + // failure, not an assertion rejection. + Err(e) => return Outcome::CompileError(e), + } + + // Lower to prover/verifier data: the canonical proof-mode IR optimization + // pipeline (shared with the CLI driver via opt_for_proof — required so + // array/tuple terms are scalarized before R1CS lowering) followed by + // R1CS lowering. + let name = test.name().to_string(); + let lowered = catch(move || { + let comps = opt_for_proof(comps, cfg()); + let cs = comps.get(&name); + let (p_data, v_data, _stats) = to_proof_data(cs, cfg()); + (p_data, v_data) + }); + let (p_data, v_data) = match lowered { + Ok(d) => d, + Err(e) => return Outcome::CompileError(e), + }; + + // Backend setup, then prove + verify. The assertions already held under + // direct evaluation, so any failure from here on is a backend/infrastructure + // failure — reported as BackendError, never as an assertion rejection. + let setup = catch(move || PS::setup(p_data, v_data)); + let (pk, vk) = match setup { + Ok(keys) => keys, + Err(e) => return Outcome::BackendError(e), + }; + match catch(|| { + let pf = PS::prove(&pk, &prover_map); + PS::verify(&vk, &verifier_map, &pf) + }) { + Ok(true) => Outcome::Pass, + Ok(false) => Outcome::BackendError( + "proof did not verify though assertions held for the given inputs".to_string(), + ), + Err(e) => Outcome::BackendError(e), + } +} diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs index 4633cfb2..04bb0d6a 100644 --- a/tests/zok_test_inputs.rs +++ b/tests/zok_test_inputs.rs @@ -59,6 +59,50 @@ fn assert_uint(v: &Value, width: usize, expected: u64) { } } +/// Unwrap a Value::Array into its element Values, in index order. +fn array_values(v: &Value) -> Vec { + match v { + Value::Array(a) => a.values(), + other => panic!("expected array, got {:?}", other), + } +} + +/// Assert a Value is an array of field elements with the given values. +fn assert_field_array(v: &Value, expected: &[u64]) { + let vals = array_values(v); + assert_eq!(vals.len(), expected.len(), "array length"); + for (v, e) in vals.iter().zip(expected) { + assert_field(v, *e); + } +} + +/// A temp directory that is deleted on drop, with everything in it. +struct TempDir(std::path::PathBuf); + +impl Drop for TempDir { + fn drop(&mut self) { + let _ = std::fs::remove_dir_all(&self.0); + } +} + +/// Write several files into a unique temp directory — so sibling imports +/// resolve by bare name, like the examples import "xor" — and run +/// eval_test_inputs on the first one. +fn eval_files(test_name: &str, files: &[(&str, &str)]) -> Result, String> { + INIT.call_once(circ::cfg::set_default); + let dir = std::env::temp_dir().join(format!( + "zok_test_inputs_{}_{}", + std::process::id(), + test_name + )); + std::fs::create_dir_all(&dir).unwrap(); + let guard = TempDir(dir); + for (name, src) in files { + std::fs::write(guard.0.join(name), src).unwrap(); + } + ZSharpCurlyFE::eval_test_inputs(guard.0.join(files[0].0), Mode::Proof) +} + #[test] fn constant_arithmetic_evaluates() { let tests = eval( @@ -71,11 +115,11 @@ def test_sq(private field y) -> field { ) .unwrap(); assert_eq!(tests.len(), 1); - assert_eq!(tests[0].name, "test_sq"); - assert_eq!(tests[0].inputs.len(), 1); - assert_eq!(tests[0].inputs[0].name, "y"); - assert_eq!(tests[0].inputs[0].source, "3 * 3"); - assert_field(&tests[0].inputs[0].value, 9); + assert_eq!(tests[0].name(), "test_sq"); + assert_eq!(tests[0].inputs().len(), 1); + assert_eq!(tests[0].inputs()[0].name(), "y"); + assert_eq!(tests[0].inputs()[0].source(), "3 * 3"); + assert_field(tests[0].inputs()[0].value(), 9); } #[test] @@ -91,7 +135,7 @@ def test_c(private field x) -> field { "#, ) .unwrap(); - assert_field(&tests[0].inputs[0].value, 8); + assert_field(tests[0].inputs()[0].value(), 8); } #[test] @@ -112,7 +156,7 @@ def test_sq(private field y) -> field { "#, ) .unwrap(); - assert_field(&tests[0].inputs[0].value, 9); + assert_field(tests[0].inputs()[0].value(), 9); } #[test] @@ -126,14 +170,14 @@ def test_scalars(private bool b, private u8 n8, private u16 n16, private u32 n32 "#, ) .unwrap(); - let inputs = &tests[0].inputs; + let inputs = tests[0].inputs(); assert_eq!(inputs.len(), 6); - assert!(matches!(inputs[0].value, Value::Bool(true))); - assert_uint(&inputs[1].value, 8, 4); - assert_uint(&inputs[2].value, 16, 4); - assert_uint(&inputs[3].value, 32, 4); - assert_uint(&inputs[4].value, 64, 4); - assert_field(&inputs[5].value, 5); + assert!(matches!(inputs[0].value(), Value::Bool(true))); + assert_uint(inputs[1].value(), 8, 4); + assert_uint(inputs[2].value(), 16, 4); + assert_uint(inputs[3].value(), 32, 4); + assert_uint(inputs[4].value(), 64, 4); + assert_field(inputs[5].value(), 5); } #[test] @@ -149,7 +193,7 @@ def test_u(private u32 x) -> u32 { "#, ) .unwrap(); - assert_uint(&tests[0].inputs[0].value, 32, 2); + assert_uint(tests[0].inputs()[0].value(), 32, 2); } #[test] @@ -163,8 +207,8 @@ def test_noargs() -> bool { "#, ) .unwrap(); - assert_eq!(tests[0].name, "test_noargs"); - assert!(tests[0].inputs.is_empty()); + assert_eq!(tests[0].name(), "test_noargs"); + assert!(tests[0].inputs().is_empty()); } #[test] @@ -238,17 +282,360 @@ def test_bad(private field x) -> field { } #[test] -fn array_parameter_rejected() { - let err = eval( +fn array_parameter_accepted() { + let tests = eval( "array_param", r#"@test xs = [1, 2]; -def test_arr(private field[2] xs) -> field { - return xs[0]; +def test_arr(private field[2] xs) { + assert(xs[0] + xs[1] == 3); +} +"#, + ) + .unwrap(); + assert_eq!(tests[0].inputs()[0].source(), "[1, 2]"); + assert_field_array(tests[0].inputs()[0].value(), &[1, 2]); +} + +#[test] +fn nested_array_accepted() { + let tests = eval( + "nested_array", + r#"@test A = [[1, 2], [3, 4]]; +def test_mat(private field[2][2] A) { + assert(A[0][0] == 1); +} +"#, + ) + .unwrap(); + let rows = array_values(tests[0].inputs()[0].value()); + assert_field_array(&rows[0], &[1, 2]); + assert_field_array(&rows[1], &[3, 4]); +} + +#[test] +fn array_input_flattens_to_leaf_names() { + // The naming contract the proof pipeline relies on: one entry per leaf, + // dotted indices, outermost dimension first, in index order — the same + // names declare_input gives the circuit's input variables (on-disk + // ground truth: examples/ZoKratesCurly/pf/mm.zok.pin). + let tests = eval( + "flatten_names", + r#"@test A = [[1, 2], [3, 4]], y = 5; +def test_flat(private field[2][2] A, public field y) { + assert(A[0][0] + y == 6); +} +"#, + ) + .unwrap(); + let entries = tests[0].inputs()[0].flat_entries(); + let names: Vec<&str> = entries.iter().map(|(n, _)| n.as_str()).collect(); + assert_eq!(names, ["A.0.0", "A.0.1", "A.1.0", "A.1.1"]); + for ((_, v), e) in entries.iter().zip([1u64, 2, 3, 4]) { + assert_field(v, e); + } + // A scalar flattens to a single entry under the bare parameter name. + assert_eq!( + tests[0].inputs()[1].flat_entries(), + vec![("y".to_string(), tests[0].inputs()[1].value().clone())] + ); +} + +#[test] +fn non_square_array_flattens_row_major() { + // A non-square field[2][3] pins the dimension order: a transposition bug + // (column-major) would relabel M.0.2 as M.2.0 (out of range) — a square + // matrix can't expose that. Leaves are row-major: M.0.0 .. M.1.2. + let tests = eval( + "flatten_non_square", + r#"@test M = [[1, 2, 3], [4, 5, 6]]; +def test_ns(private field[2][3] M) { + assert(M[0][0] == 1); +} +"#, + ) + .unwrap(); + let entries = tests[0].inputs()[0].flat_entries(); + let names: Vec<&str> = entries.iter().map(|(n, _)| n.as_str()).collect(); + assert_eq!( + names, + ["M.0.0", "M.0.1", "M.0.2", "M.1.0", "M.1.1", "M.1.2"] + ); + for ((_, v), e) in entries.iter().zip([1u64, 2, 3, 4, 5, 6]) { + assert_field(v, e); + } +} + +#[test] +fn three_dimensional_array_flattens() { + // Three dimensions: one dotted index per level, outermost first. + let tests = eval( + "flatten_3d", + r#"@test T = [[[1, 2], [3, 4]], [[5, 6], [7, 8]]]; +def test_3d(private field[2][2][2] T) { + assert(T[0][0][0] == 1); +} +"#, + ) + .unwrap(); + let entries = tests[0].inputs()[0].flat_entries(); + let names: Vec<&str> = entries.iter().map(|(n, _)| n.as_str()).collect(); + assert_eq!( + names, + ["T.0.0.0", "T.0.0.1", "T.0.1.0", "T.0.1.1", "T.1.0.0", "T.1.0.1", "T.1.1.0", "T.1.1.1"] + ); + for ((_, v), e) in entries.iter().zip([1u64, 2, 3, 4, 5, 6, 7, 8]) { + assert_field(v, e); + } +} + +#[test] +fn array_initializer_accepted() { + // [0; 4] const-folds to a sparse Value::Array (empty backing map, every + // leaf comes from the default); flattening must still yield all leaves. + let tests = eval( + "array_fill", + r#"@test xs = [0; 4]; +def test_fill(private field[4] xs) { + assert(xs[3] == 0); +} +"#, + ) + .unwrap(); + assert_field_array(tests[0].inputs()[0].value(), &[0, 0, 0, 0]); + assert_eq!(tests[0].inputs()[0].flat_entries().len(), 4); +} + +#[test] +fn spread_in_array_accepted() { + let tests = eval( + "array_spread", + r#"@test xs = [...[1, 2], 3]; +def test_spread(private field[3] xs) { + assert(xs[2] == 3); +} +"#, + ) + .unwrap(); + assert_field_array(tests[0].inputs()[0].value(), &[1, 2, 3]); +} + +#[test] +fn named_const_array_resolves() { + // "Large inputs pointed at by name", same-file half: the annotation + // names a constant instead of spelling the array out. + let tests = eval( + "const_array", + r#"const field[2][2] IMG = [[1, 0], [0, 1]]; + +@test A = IMG; +def test_img(private field[2][2] A) { + assert(A[0][0] == 1); +} +"#, + ) + .unwrap(); + let rows = array_values(tests[0].inputs()[0].value()); + assert_field_array(&rows[0], &[1, 0]); + assert_field_array(&rows[1], &[0, 1]); +} + +#[test] +fn imported_const_array_resolves() { + // "Large inputs pointed at by name", imported half: the const lives in + // a sibling file, imported by bare name. + let tests = eval_files( + "imported_const_array", + &[ + ( + "main.zok", + r#"from "helper" import IMG; + +@test A = IMG; +def test_img(private field[2][2] A) { + assert(A[0][0] == 1); +} +"#, + ), + ("helper.zok", "const field[2][2] IMG = [[1, 0], [0, 1]];\n"), + ], + ) + .unwrap(); + let rows = array_values(tests[0].inputs()[0].value()); + assert_field_array(&rows[0], &[1, 0]); + assert_field_array(&rows[1], &[0, 1]); +} + +#[test] +fn array_elements_typed_by_parameter() { + // Literal typing descends into inline arrays: bare 1/2/3 binding to a + // u32[3] parameter come back as 32-bit bit-vectors. + let tests = eval( + "uint_array", + r#"@test xs = [1, 2, 3]; +def test_u32s(private u32[3] xs) { + assert(xs[0] == 1u32); +} +"#, + ) + .unwrap(); + let vals = array_values(tests[0].inputs()[0].value()); + for (i, v) in vals.iter().enumerate() { + assert_uint(v, 32, (i + 1) as u64); + } +} + +#[test] +fn bool_array_accepted() { + let tests = eval( + "bool_array", + r#"@test bs = [true, false]; +def test_bools(private bool[2] bs) { + assert(bs[0]); +} +"#, + ) + .unwrap(); + let vals = array_values(tests[0].inputs()[0].value()); + assert!(matches!(vals[0], Value::Bool(true))); + assert!(matches!(vals[1], Value::Bool(false))); +} + +#[test] +fn array_wrong_length_rejected() { + // The type-equality check works structurally on arrays: a 2-element + // value cannot bind to a field[3] parameter, and the diagnostic names + // both types. + let err = eval( + "array_len", + r#"@test xs = [1, 2]; +def test_len(private field[3] xs) { + assert(xs[0] == 1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("expected type field[3]"), "{}", err); + assert!(err.contains("field[2]"), "{}", err); +} + +#[test] +fn array_wrong_element_type_rejected() { + let err = eval( + "array_elem_ty", + r#"@test xs = [true, false]; +def test_elem_ty(private field[2] xs) { + assert(xs[0] == 1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("expected type field[2]"), "{}", err); + assert!(err.contains("bool"), "{}", err); +} + +#[test] +fn struct_parameter_rejected() { + let err = eval( + "struct_param", + r#"struct Point { + field x; + field y; +} + +@test p = Point { x: 1, y: 2 }; +def test_pt(private Point p) { + assert(p.x == 1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("unsupported type"), "{}", err); + assert!(err.contains("arrays of scalars"), "{}", err); +} + +#[test] +fn tuple_parameter_rejected() { + let err = eval( + "tuple_param", + r#"@test t = (1, true); +def test_tup(private (field, bool) t) { + assert(t.1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("unsupported type"), "{}", err); +} + +#[test] +fn array_of_struct_rejected() { + // The support check recurses to the array's base element: an array is + // only accepted if that base is a scalar. + let err = eval( + "arr_of_struct", + r#"struct Point { + field x; + field y; +} + +@test ps = [Point { x: 1, y: 2 }, Point { x: 3, y: 4 }]; +def test_pts(private Point[2] ps) { + assert(ps[0].x == 1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("unsupported type"), "{}", err); +} + +#[test] +fn array_type_alias_accepted() { + // The resolved-Ty rule extends to arrays: an alias for field[2][2] + // resolves to an array of scalars and must be accepted. + let tests = eval( + "array_alias", + r#"type Mat = field[2][2]; + +@test A = [[1, 2], [3, 4]]; +def test_alias(private Mat A) { + assert(A[0][0] == 1); +} +"#, + ) + .unwrap(); + let rows = array_values(tests[0].inputs()[0].value()); + assert_field_array(&rows[0], &[1, 2]); +} + +#[test] +fn zero_length_array_rejected() { + // A zero-length input would flatten to no circuit inputs at all — a + // silent no-op — so the door rejects the type outright. + let err = eval( + "zero_len_param", + r#"@test xs = [0; 0]; +def test_zero(private field[0] xs) { + assert(true); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("zero-length"), "{}", err); +} + +#[test] +fn empty_array_value_rejected() { + // `[]` fails const evaluation ("Empty array") before the type check. + let err = eval( + "empty_array_value", + r#"@test xs = []; +def test_empty(private field[2] xs) { + assert(xs[0] == 0); } "#, ) .unwrap_err(); - assert!(err.contains("non-scalar"), "{}", err); + assert!(err.contains("Empty array"), "{}", err); } #[test] @@ -266,7 +653,7 @@ def test_alias(private Word x) -> Word { "#, ) .unwrap(); - assert_uint(&tests[0].inputs[0].value, 32, 2); + assert_uint(tests[0].inputs()[0].value(), 32, 2); } #[test] @@ -320,7 +707,7 @@ def double(field n) -> field { "#, ) .unwrap(); - assert_field(&tests[0].inputs[0].value, 14); + assert_field(tests[0].inputs()[0].value(), 14); } #[test] @@ -357,7 +744,7 @@ def test_id(private u32 y) { "#, ) .unwrap(); - assert_uint(&tests[0].inputs[0].value, 32, 2); + assert_uint(tests[0].inputs()[0].value(), 32, 2); } #[test] @@ -372,10 +759,10 @@ def test_order(private field a, private field b) -> field { "#, ) .unwrap(); - assert_eq!(tests[0].inputs[0].name, "a"); - assert_field(&tests[0].inputs[0].value, 1); - assert_eq!(tests[0].inputs[1].name, "b"); - assert_field(&tests[0].inputs[1].value, 2); + assert_eq!(tests[0].inputs()[0].name(), "a"); + assert_field(tests[0].inputs()[0].value(), 1); + assert_eq!(tests[0].inputs()[1].name(), "b"); + assert_field(tests[0].inputs()[1].value(), 2); } #[test] @@ -391,10 +778,10 @@ def test_vis(private field a, public field b, field c) { "#, ) .unwrap(); - let inputs = &tests[0].inputs; - assert!(!inputs[0].public, "private a"); - assert!(inputs[1].public, "public b"); - assert!(inputs[2].public, "unannotated c defaults to public"); + let inputs = tests[0].inputs(); + assert!(!inputs[0].public(), "private a"); + assert!(inputs[1].public(), "public b"); + assert!(inputs[2].public(), "unannotated c defaults to public"); } #[test] @@ -415,8 +802,11 @@ def test_return_style(private field y) -> field { "#, ) .unwrap(); - assert!(!tests[0].has_return, "assert-style test has no return type"); - assert!(tests[1].has_return, "return-typed test is flagged"); + assert!( + !tests[0].has_return(), + "assert-style test has no return type" + ); + assert!(tests[1].has_return(), "return-typed test is flagged"); } #[test] @@ -435,7 +825,7 @@ def test_only(private field x) -> field { ) .unwrap(); assert_eq!(tests.len(), 1); - assert_eq!(tests[0].name, "test_only"); + assert_eq!(tests[0].name(), "test_only"); } #[test] diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs new file mode 100644 index 00000000..60e94f28 --- /dev/null +++ b/tests/ztest_e2e.rs @@ -0,0 +1,269 @@ +//! End-to-end coverage of the `@test` runner: `eval_test_inputs` (discovery + +//! input evaluation) followed by `circ::test_runner::run_test` (compile -> +//! assert check -> setup -> prove -> verify through Groth16/BLS12-381). This is the +//! path the `ztest` example exercises; `tests/zok_test_inputs.rs` stops at +//! input evaluation, so without this file a regression in flattening, the IR +//! optimization pipeline, R1CS lowering, or the outcome semantics could merge +//! with every registered test green. +//! +//! Assertions are on the structured `Outcome`, not on printed text. + +#![cfg(all(feature = "smt", feature = "zokc", feature = "bellman"))] + +use bls12_381::Bls12; +use circ::front::zsharpcurly::{TestCase, ZSharpCurlyFE}; +use circ::front::Mode; +use circ::target::r1cs::bellman::Bellman; +use circ::test_runner::{run_test, Outcome}; +use std::path::{Path, PathBuf}; +use std::sync::Once; + +static INIT: Once = Once::new(); + +/// A temp directory (with its contents) removed on drop, even on panic. +struct TempDir(PathBuf); + +impl Drop for TempDir { + fn drop(&mut self) { + let _ = std::fs::remove_dir_all(&self.0); + } +} + +/// Write `files` into a unique temp directory (so sibling imports resolve by +/// bare name) and return the guard plus the path to the first file (the entry). +fn write_files(test_name: &str, files: &[(&str, &str)]) -> (TempDir, PathBuf) { + INIT.call_once(circ::cfg::set_default); + let dir = std::env::temp_dir().join(format!("ztest_e2e_{}_{}", std::process::id(), test_name)); + std::fs::create_dir_all(&dir).unwrap(); + let guard = TempDir(dir); + for (name, src) in files { + std::fs::write(guard.0.join(name), src).unwrap(); + } + let entry = guard.0.join(files[0].0); + (guard, entry) +} + +/// Single-file convenience wrapper over [`write_files`]. +fn write_file(test_name: &str, src: &str) -> (TempDir, PathBuf) { + write_files(test_name, &[("main.zok", src)]) +} + +/// Discover the `@test` functions in `path`. +fn discover(path: &Path) -> Vec { + ZSharpCurlyFE::eval_test_inputs(path.to_path_buf(), Mode::Proof).unwrap() +} + +/// Discover and run every test in a single-test file; return its outcome. +fn run_only(test_name: &str, src: &str) -> Outcome { + let (_guard, path) = write_file(test_name, src); + let tests = discover(&path); + assert_eq!(tests.len(), 1, "expected exactly one @test function"); + run_test::>(&tests[0]) +} + +#[test] +fn nested_array_passes_full_pipeline() { + let outcome = run_only( + "nested_array", + r#"@test A = [[1, 2], [3, 4]]; +def test_mat(private field[2][2] A) { + assert(A[0][0] == 1); + assert(A[1][1] == 4); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn array_initializer_passes() { + // Sparse [0; 4]: the flatten path must still emit all four leaves. + let outcome = run_only( + "array_fill", + r#"@test xs = [0; 4]; +def test_fill(private field[4] xs) { + assert(xs[0] + xs[1] + xs[2] + xs[3] == 0); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn public_and_private_array_leaves_pass() { + // Matrix multiply with private inputs and a PUBLIC expected array C: C's + // leaves must reach the verifier map. Product independently confirmed via + // zcxi against mm.zok: [[1,2],[3,4]] x [[5,6],[7,8]] = [[19,22],[43,50]]. + let outcome = run_only( + "public_private", + r#"@test A = [[1, 2], [3, 4]], B = [[5, 6], [7, 8]], C = [[19, 22], [43, 50]]; +def test_mm(private field[2][2] A, private field[2][2] B, public field[2][2] C) { + field[2][2] P = [[0; 2]; 2]; + for field i in 0..2 { + for field j in 0..2 { + for field k in 0..2 { + P[i][j] = P[i][j] + A[i][k] * B[k][j]; + } + } + } + for field i in 0..2 { + for field j in 0..2 { + assert(P[i][j] == C[i][j]); + } + } +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn same_file_named_const_array_passes() { + let outcome = run_only( + "same_file_const", + r#"const field[2][2] IMG = [[1, 0], [0, 1]]; + +@test A = IMG; +def test_img(private field[2][2] A) { + assert(A[0][0] == 1); + assert(A[1][1] == 1); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn imported_const_array_passes() { + let (_guard, path) = write_files( + "imported_const", + &[ + ( + "main.zok", + r#"from "helper" import IMG; + +@test A = IMG; +def test_img(private field[2][2] A) { + assert(A[0][0] == 1); + assert(A[1][1] == 1); +} +"#, + ), + ("helper.zok", "const field[2][2] IMG = [[1, 0], [0, 1]];\n"), + ], + ); + let tests = discover(&path); + assert_eq!(tests.len(), 1); + let outcome = run_test::>(&tests[0]); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn non_square_array_passes() { + // A non-square field[2][3]: the shape itself (2 rows of 3, not 3 of 2) + // would break if flattening reversed dimension order — a square matrix + // could hide that. Distinct values pin the row/column mapping. + let outcome = run_only( + "non_square", + r#"@test M = [[1, 2, 3], [4, 5, 6]]; +def test_ns(private field[2][3] M) { + assert(M[0][0] == 1); + assert(M[0][2] == 3); + assert(M[1][0] == 4); + assert(M[1][2] == 6); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn three_dimensional_array_passes() { + let outcome = run_only( + "three_dim", + r#"@test T = [[[1, 2], [3, 4]], [[5, 6], [7, 8]]]; +def test_3d(private field[2][2][2] T) { + assert(T[0][0][0] == 1); + assert(T[1][0][1] == 6); + assert(T[1][1][1] == 8); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn uint_array_passes() { + let outcome = run_only( + "uint_array", + r#"@test ws = [1, 2, 3, 4]; +def test_u32s(private u32[4] ws) { + assert(ws[0] + ws[1] == ws[2]); + assert(ws[3] == 4u32); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn wrong_nested_array_value_is_assertion_failure() { + // A false assertion is a SEMANTIC rejection (AssertionFailed), never a + // backend error. This is the signal a future `expect = reject` keys off. + let outcome = run_only( + "wrong_nested", + r#"@test A = [[1, 2], [3, 4]]; +def test_mat(private field[2][2] A) { + assert(A[1][1] == 99); +} +"#, + ); + assert!( + matches!(outcome, Outcome::AssertionFailed(_)), + "got {:?}", + outcome + ); +} + +#[test] +fn linear_all_private_false_assertion_is_assertion_failure() { + // The vacuous-pass class: a purely linear assert on a private scalar. The + // proof pipeline alone would pass this vacuously (the private var gets + // optimized away); the ground-truth check must still classify it as + // AssertionFailed. + let outcome = run_only( + "linear_private", + r#"@test x = 4; +def test_linear(private field x) { + assert(x == 99); +} +"#, + ); + assert!( + matches!(outcome, Outcome::AssertionFailed(_)), + "got {:?}", + outcome + ); +} + +#[test] +fn return_typed_test_is_unsupported() { + // A return-typed test is not runnable (no expected output to check); it is + // an infrastructure "Unsupported", not an assertion failure. + let (_guard, path) = write_file( + "return_typed", + r#"@test x = 3; +def test_ret(private field x) -> field { + return x; +} +"#, + ); + let tests = discover(&path); + assert_eq!(tests.len(), 1); + let outcome = run_test::>(&tests[0]); + assert!( + matches!(outcome, Outcome::Unsupported(_)), + "got {:?}", + outcome + ); +} diff --git a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs index 9a74701b..83b2b489 100644 --- a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs +++ b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs @@ -1626,6 +1626,32 @@ mod tests { let ann = f.test.as_ref().expect("should carry @test"); assert_eq!(ann.inputs.len(), 2); assert_eq!(ann.inputs[0].name.value, "a"); + assert_eq!(ann.inputs[0].value.span().as_str(), "3"); + assert_eq!(ann.inputs[1].name.value, "b"); + assert_eq!(ann.inputs[1].value.span().as_str(), "3 * 3"); + } + #[test] + fn parses_array_test_inputs() { + // The value slot is a full expression, so every array form parses: + // nested inline arrays, initializers, and spreads. + let source = r#"@test A = [[1, 0], [0, 1]], xs = [0; 4], ys = [...[1, 2], 3]; + def test_arrays(private field[2][2] A, private field[4] xs, private field[3] ys) -> bool { + return true; + } +"#; + let ast = generate_ast(source).unwrap(); + let f = match &ast.declarations[0] { + SymbolDeclaration::Function(f) => f, + _ => panic!("expected a function"), + }; + let ann = f.test.as_ref().expect("should carry @test"); + assert_eq!(ann.inputs.len(), 3); + assert!(matches!(ann.inputs[0].value, Expression::InlineArray(_))); + assert!(matches!( + ann.inputs[1].value, + Expression::ArrayInitializer(_) + )); + assert!(matches!(ann.inputs[2].value, Expression::InlineArray(_))); } } From 5e3f639700f07121e52a39ae1fa42d6c36537001 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Fri, 17 Jul 2026 14:31:03 -0400 Subject: [PATCH 05/29] Update coverage_test.zok --- examples/ZoKratesCurly/pf/coverage_test.zok | 128 ++++++-------------- 1 file changed, 37 insertions(+), 91 deletions(-) diff --git a/examples/ZoKratesCurly/pf/coverage_test.zok b/examples/ZoKratesCurly/pf/coverage_test.zok index 49e025e3..d6d89d21 100644 --- a/examples/ZoKratesCurly/pf/coverage_test.zok +++ b/examples/ZoKratesCurly/pf/coverage_test.zok @@ -1,117 +1,63 @@ -// Systematic @test runner coverage: every currently supported feature, -// each through the full compile -> setup -> prove -> verify pipeline. -// All tests here pass; rejection paths are covered in tests/zok_test_inputs.rs. +// Simple @test coverage: scalar and array inputs, private/public visibility. +// All tests pass. Run: +// cargo run --example ztest --features zokc -- examples/ZoKratesCurly/pf/coverage_test.zok -// ---- helpers under test ---- +// ---- scalar inputs ---- -const field BASE = 40; - -type Word = u32; - -def sq(field x) -> field { - return x * x; -} - -def pick_max(field x, field y) -> field { - return if x > y { x } else { y }; +@test x = 5; +def test_field(private field x) { + assert(x == 5); } -def sum_to(u32 n) -> u32 { - u32 mut acc = 0; - for u32 i in 0..8 { - acc = if i < n { acc + i } else { acc }; - } - return acc; +@test a = 4, b = 6; +def test_add(private field a, private field b) { + assert(a + b == 10); } -// ---- input types: every scalar, each proven end-to-end ---- - @test b = true; -def test_bool_input(private bool b) { +def test_bool(private bool b) { assert(b); } -@test x = 200u8, y = 55u8; -def test_u8_input(private u8 x, private u8 y) { - assert(x + y == 255u8); +@test x = 7u32; +def test_u32(private u32 x) { + assert(x * 2 == 14u32); } -@test x = 0xBEEF; -def test_u16_hex_input(private u16 x) { - assert(x == 48879u16); -} - -@test x = 7; -def test_u32_bare_literal(private u32 x) { - // bare 7 is typed u32 by this parameter - assert(x * x == 49u32); -} +// ---- scalar visibility corners ---- -@test x = 4294967296; -def test_u64_input(private u64 x) { - // 2^32 does not fit in u32; only valid because the parameter is u64 - assert(x == 0x0000000100000000); -} - -@test x = 5f; -def test_field_suffixed(private field x) { - assert(x == 5); +@test a = 3, b = 4; +def test_all_public(public field a, public field b) { + assert(a + b == 7); } -@test w = 21; -def test_type_alias_input(private Word w) { - assert(w + w == 42u32); +@test a = 3, b = 4; +def test_mixed_visibility(private field a, public field b) { + assert(a + b == 7); } -// ---- input expressions ---- +// ---- array inputs ---- -@test x = 3 * 3 + 2 * 2; -def test_arithmetic_expr(private field x) { - assert(x == 13); +@test xs = [1, 2, 3]; +def test_array(private field[3] xs) { + assert(xs[0] + xs[1] == xs[2]); } -@test x = BASE + 2; -def test_constant_expr(private field x) { - assert(x == 42); +@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 x = sq(sq(2)); -def test_nested_call_expr(private field x) { - assert(x == 16); +@test xs = [1, 2]; +def test_public_array(public field[2] xs) { + assert(xs[0] + xs[1] == 3); } -@test b = 5 > 3; -def test_bool_expr(private bool b) { - assert(b); -} - -// ---- function shapes ---- - -@test; -def test_no_inputs() { - assert(sq(6) == 36); -} - -@test a = 1, b = 2, c = 3, d = 4; -def test_mixed_visibility(private field a, public field b, field c, private field d) { - assert(a + b + c + d == 10); -} - -@test x = 9, y = 2; -def test_control_flow(private field x, private field y) { - assert(pick_max(x, y) == 9); - assert(pick_max(y, x) == 9); -} - -@test n = 5; -def test_loop_and_mut(private u32 n) { - // 0+1+2+3+4 - assert(sum_to(n) == 10u32); -} +// ---- array + scalar together ---- -@test x = 3; -def test_multiple_asserts(private field x) { - assert(x == 3); - assert(sq(x) == 9); - assert(sq(x) + x == 12, "message on an assert works too"); +@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); } From 3ba60f864e44ded666c8e3bf34a0af17573865b6 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Fri, 17 Jul 2026 14:54:58 -0400 Subject: [PATCH 06/29] Remove duplicate assertion in test case Removed duplicate assertion for the second input value. --- third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs index 6bfdbf9f..83b2b489 100644 --- a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs +++ b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs @@ -1630,7 +1630,6 @@ mod tests { assert_eq!(ann.inputs[1].name.value, "b"); assert_eq!(ann.inputs[1].value.span().as_str(), "3 * 3"); - assert_eq!(ann.inputs[1].value.span().as_str(), "3 * 3"); } #[test] fn parses_array_test_inputs() { From 08236ecbaa15fe56207e2108b233b14821224863 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Fri, 17 Jul 2026 15:00:34 -0400 Subject: [PATCH 07/29] Refactor comments to use Rust doc comments format Updated documentation comments to use the new style. --- examples/ztest.rs | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/examples/ztest.rs b/examples/ztest.rs index f1dd2f9f..9ef8954f 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -1,23 +1,22 @@ -/// 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 -/// evaluate to true on the given inputs (checked by direct IR evaluation — -/// the proof pipeline alone can pass vacuously when optimization eliminates -/// a private variable) AND a proof can be produced and verifies (backend: -/// Groth16 over BLS12-381, hardcoded for the MVP). -/// -/// Performance note: every array leaf is a distinct circuit input. For a -/// *public* array all of its leaves are public inputs, so verification cost -/// and verifying-key size grow linearly with the leaf count under Groth16; -/// prefer testing large arrays as `private` witnesses and keeping `public` -/// arrays to small expected values. (Visibility itself is a protocol choice, -/// not a performance knob — this is just what it costs with this backend.) -/// -/// The per-test execution logic lives in [`circ::test_runner`]; this file is -/// the CLI wrapper. +//! 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 +//! evaluate to true on the given inputs (checked by direct IR evaluation — +//! the proof pipeline alone can pass vacuously when optimization eliminates +//! a private variable) AND a proof can be produced and verifies (backend: +//! Groth16 over BLS12-381, hardcoded for the MVP). +//! +//! Performance note: every array leaf is a distinct circuit input. For a +//! *public* array all of its leaves are public inputs, so verification cost +//! and verifying-key size grow linearly with the leaf count under Groth16; +//! prefer testing large arrays as `private` witnesses and keeping `public` +//! arrays to small expected values. +//! +//! 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::ZSharpCurlyFE; From 49ca19b4d7ac3c7e8e30483282b9a63b04d245c6 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:41:51 -0400 Subject: [PATCH 08/29] Clarify documentation on value-only array handling Updated documentation to clarify that the function is limited to arrays instead of just indexed arrays. --- src/front/zsharpcurly/interp.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/front/zsharpcurly/interp.rs b/src/front/zsharpcurly/interp.rs index 6a0313a6..2fabe03a 100644 --- a/src/front/zsharpcurly/interp.rs +++ b/src/front/zsharpcurly/interp.rs @@ -61,7 +61,7 @@ pub fn extract( /// ..., recursively (a `field[2][2]` named `A` yields `A.0.0` .. `A.1.1`). /// Ordering and naming mirror [extract] and `declare_input`. /// -/// This is deliberately *value-only* and limited to indexed arrays: +/// This is deliberately *value-only* and limited to arrays: /// [Array::values] handles sparse arrays (e.g. from `[0; 4]`, whose backing /// map is empty) by falling back to the array's default. Tuples and structs /// are not handled — a struct lowers to a [Value::Tuple], which no longer From ae9cbc210db83599ccb1fb3affb97989c7109208 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:43:18 -0400 Subject: [PATCH 09/29] Fix formatting in documentation comment --- src/front/zsharpcurly/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index 39f603d1..02e84635 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -42,7 +42,7 @@ pub struct Inputs { /// A function marked `@test`, with its annotation inputs evaluated to /// concrete values. /// -/// Contract: a `TestCase` guarantees its *inputs* are validated — names +/// a `TestCase` guarantees its *inputs* are validated — names /// match parameters exactly, types are checked, values are constant. It /// does not decide whether the function's *shape* is runnable; that is /// runner policy. In particular, return-typed test functions are From 020f58f29158820b3062bae43f316444ecc9b4e0 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 14:08:03 -0400 Subject: [PATCH 10/29] Update comments for zero-length array check Clarify comments regarding zero-length array handling. --- src/front/zsharpcurly/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index 02e84635..c5910212 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -292,8 +292,8 @@ fn is_scalar_or_scalar_array(ty: &Ty) -> bool { } /// Does `ty` contain a zero-length array dimension? Such an input would -/// flatten to no circuit inputs at all — a silent no-op — so the door -/// rejects it. `[]` values already fail const evaluation ("Empty array"), +/// flatten to no circuit inputs at all, so it is rejected. +///`[]` values already fail const evaluation ("Empty array"), /// but `[0; 0]` would evaluate cleanly without this type-level guard. fn has_zero_length_array(ty: &Ty) -> bool { match ty { From 0ab8cbf977e0dcb7e55578331f9e0951a7bd3a75 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 14:51:19 -0400 Subject: [PATCH 11/29] Refactor comments and update outcome descriptions --- src/test_runner/mod.rs | 68 +++++++++++++++--------------------------- 1 file changed, 24 insertions(+), 44 deletions(-) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index 3d732bd9..af3f4213 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -1,20 +1,11 @@ -//! Executes one `@test` function end-to-end through the proof pipeline. +//! Runs a ZoKrates `@test` through compilation and the proof pipeline. //! -//! This is the reusable core behind the `ztest` example: compile the test -//! function as its own entry point, check its assertions against the resolved -//! inputs, then run the full `setup -> prove -> verify` cycle in memory. -//! -//! It sits *above* the frontend on purpose: the ZoKrates frontend produces -//! validated test metadata ([`TestCase`]) and CirC IR; this module consumes -//! that read-only API and orchestrates compilation ([`crate::compile`]) and -//! the proof backend ([`crate::target::r1cs`]). The frontend does not depend -//! back on it. It is generic over the proof system ([`ProofSystem`]) so the -//! backend is chosen by the caller (the example instantiates Groth16 over -//! BLS12-381). That generic covers the [`ProofSystem`] implementors — Bellman -//! (Groth16) and Mirage — and is where their selection will plug in; Spartan -//! uses a separate `SpartanProofSystem` interface (and a different field), so -//! supporting it will take an adapter, not just a type argument. Presentation -//! — printing, exit codes, input formatting — stays in the caller, not here. +//! This module sits above the frontend, which provides validated [`TestCase`] +//! metadata and CirC IR without depending on the runner. The runner pre-checks +//! assertions and runs `setup -> prove -> verify` using a caller-selected +//! [`ProofSystem`]. Bellman and Mirage implement this interface; `ztest` uses +//! Bellman Groth16 over BLS12-381. Spartan uses a separate interface and is not +//! supported here. CLI output remains in `ztest`. use crate::cfg::cfg; use crate::compile::{opt_for_proof, to_proof_data}; @@ -26,28 +17,22 @@ use fxhash::FxHashMap; use std::cell::Cell; use std::sync::Once; -/// The outcome of running one test. +/// Result of running one test. /// -/// Semantic outcomes (the test's assertions were accepted or rejected) are -/// kept distinct from infrastructure outcomes (the test could not be run, or a -/// backend step failed). A future `expect = accept|reject` setting keys off -/// [`Outcome::Pass`] / [`Outcome::AssertionFailed`] only — it must never treat -/// a [`Outcome::CompileError`] or [`Outcome::BackendError`] as a rejection. +/// Assertion failures are kept separate from unsupported tests and +/// compile/backend errors, so execution failures are not treated as expected +/// test rejections. #[derive(Debug)] pub enum Outcome { - /// Assertions held for the given inputs and the proof verified. + /// The assertion pre-check passed and the proof verified. Pass, - /// An assertion does not hold for the given inputs. This is the semantic - /// "the test rejected these inputs" signal. + /// The assertion pre-check failed. AssertionFailed(String), - /// The test's shape is not runnable (e.g. it declares a return type, which - /// carries no expected output to check). + /// The runner does not support this test shape. Unsupported(String), - /// The frontend, IR optimization, or R1CS lowering failed — the test could - /// not be turned into a circuit. + /// Frontend compilation, optimization, or R1CS lowering failed. CompileError(String), - /// The backend failed to set up, prove, or verify a test whose assertions - /// already held. This is an infrastructure failure, NOT a rejection. + /// Proof setup, proving, or verification failed. BackendError(String), } @@ -152,13 +137,11 @@ pub fn run_test(test: &TestCase) -> Outcome { prover_map.extend(entries); } - // Ground truth: evaluate every assertion directly against the prover's - // inputs on the un-optimized IR. This is the authoritative pass/fail - // verdict. The proof pipeline alone is not sufficient — it proves "a - // satisfying witness exists", and when an optimization eliminates a private - // variable (e.g. reduce_linearities substituting away a purely linear - // assert like `x == 99`), the input-map value is never enforced and an - // untrue test would pass vacuously. + // Evaluate assertions against the supplied prover inputs on the unoptimized IR. + // Checking before optimization catches failures that could otherwise be hidden + // if an optimization removes a private input from the circuit. This is only a + // pre-check; challenge-dependent assertions must still be checked during + // proving. let held = catch(|| { comps .get(test.name()) @@ -194,9 +177,8 @@ pub fn run_test(test: &TestCase) -> Outcome { Err(e) => return Outcome::CompileError(e), }; - // Backend setup, then prove + verify. The assertions already held under - // direct evaluation, so any failure from here on is a backend/infrastructure - // failure — reported as BackendError, never as an assertion rejection. + // Run backend setup, proving, and verification. Failures in this phase are + // reported as `BackendError`. let setup = catch(move || PS::setup(p_data, v_data)); let (pk, vk) = match setup { Ok(keys) => keys, @@ -207,9 +189,7 @@ pub fn run_test(test: &TestCase) -> Outcome { PS::verify(&vk, &verifier_map, &pf) }) { Ok(true) => Outcome::Pass, - Ok(false) => Outcome::BackendError( - "proof did not verify though assertions held for the given inputs".to_string(), - ), + Ok(false) => Outcome::BackendError("proof did not verify".to_string()), Err(e) => Outcome::BackendError(e), } } From 9cd54fef708cadace2aebe87a4db391799fbfebb Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 14:58:14 -0400 Subject: [PATCH 12/29] Update comment on generic test functions rejection --- src/front/zsharpcurly/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index c5910212..599fef61 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -228,7 +228,7 @@ impl ZSharpCurlyFE { /// `u32[2] xs` types each element), and the evaluated type must /// match the parameter's declared type — for arrays this also checks /// length and element type; - /// * generic test functions are rejected. + /// * test functions parameterized with generics are rejected /// /// Known limits and semantics: /// * The `Err` case covers annotation validation/evaluation only. From bf16d69c81efa17b13db9cfd7bce81ec37cd907f Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 18:31:58 -0400 Subject: [PATCH 13/29] Remove performance notes from ztest.rs Removed performance notes regarding array leaves and verification costs. --- examples/ztest.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/examples/ztest.rs b/examples/ztest.rs index 9ef8954f..9819c46a 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -9,12 +9,6 @@ //! a private variable) AND a proof can be produced and verifies (backend: //! Groth16 over BLS12-381, hardcoded for the MVP). //! -//! Performance note: every array leaf is a distinct circuit input. For a -//! *public* array all of its leaves are public inputs, so verification cost -//! and verifying-key size grow linearly with the leaf count under Groth16; -//! prefer testing large arrays as `private` witnesses and keeping `public` -//! arrays to small expected values. -//! //! The per-test execution logic lives in [`circ::test_runner`]; this file is //! the CLI wrapper. use bls12_381::Bls12; From d2bcd53afba9a53b4a5ad6463059de29cf78494d Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 21 Jul 2026 18:48:27 -0400 Subject: [PATCH 14/29] Add TODO for error handling refactor in catch function Added TODO comments regarding future error handling improvements. --- src/test_runner/mod.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index af3f4213..74e747bd 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -70,6 +70,10 @@ fn install_quiet_hook() { /// later panics keep the normal hook. Cannot contain `process::exit` paths /// (some frontend semantic errors exit rather than unwind). /// +/// TODO: Replace this panic-catching boundary with normal `Result` propagation +/// once the frontend and prover return structured errors. This requires a +/// broader error-handling refactor outside the current test-runner scope. +/// /// Exposed for callers that must also survive panics from the discovery phase /// (e.g. [`ZSharpCurlyFE::eval_test_inputs`] panics on a parse/load failure). pub fn catch(f: impl FnOnce() -> R) -> Result { From f66c1d93f433a5167213e1dfc1208f300435c05c Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 14:59:41 -0400 Subject: [PATCH 15/29] Refactor comments in walk_function_definition --- src/front/zsharpcurly/zvisit/walkfns.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/front/zsharpcurly/zvisit/walkfns.rs b/src/front/zsharpcurly/zvisit/walkfns.rs index a5e64f76..fd2c861d 100644 --- a/src/front/zsharpcurly/zvisit/walkfns.rs +++ b/src/front/zsharpcurly/zvisit/walkfns.rs @@ -157,11 +157,7 @@ pub fn walk_function_definition<'ast, Z: ZVisitorMut<'ast>>( visitor: &mut Z, fundef: &mut ast::FunctionDefinition<'ast>, ) -> ZVisitorResult { - // Note: typing annotation inputs requires the function's parameter - // types, which a generic visitor does not know; that is done with a - // per-parameter type hint in eval_test_case (mod.rs). The structural - // walk here still covers the annotation so that visitors (identifier - // collection, rewriting, linting, ...) see every AST child. + // Visit the @test annotation when the function has one. if let Some(t) = fundef.test.as_mut() { visitor.visit_test_annotation(t)?; } From 9700b47165a435d31337842a48f9db1e998a154a Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 15:05:32 -0400 Subject: [PATCH 16/29] Revise flatten function documentation Updated documentation for the flatten function to clarify its behavior and limitations regarding scalar and array inputs. --- src/front/zsharpcurly/interp.rs | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/src/front/zsharpcurly/interp.rs b/src/front/zsharpcurly/interp.rs index 2fabe03a..88d70025 100644 --- a/src/front/zsharpcurly/interp.rs +++ b/src/front/zsharpcurly/interp.rs @@ -54,22 +54,17 @@ pub fn extract( } } -/// Inverse of [extract] for the value shapes `@test` supports: break a -/// constant [Value] into the flattened per-leaf scalar entries the proof -/// pipeline uses in input maps. A scalar yields a single (`name`, value) -/// entry; an array yields one entry per element under `name.0`, `name.1`, -/// ..., recursively (a `field[2][2]` named `A` yields `A.0.0` .. `A.1.1`). -/// Ordering and naming mirror [extract] and `declare_input`. +/// Converts a scalar or array test input into the named scalar values expected +/// by the proof pipeline. /// -/// This is deliberately *value-only* and limited to arrays: -/// [Array::values] handles sparse arrays (e.g. from `[0; 4]`, whose backing -/// map is empty) by falling back to the array's default. Tuples and structs -/// are not handled — a struct lowers to a [Value::Tuple], which no longer -/// carries the field names `name.field` flattening would need; supporting -/// them will need the resolved [Ty], not just the value. `eval_test_case` -/// rejects those parameter types (and every non-scalar leaf kind) before one -/// can reach here, so the leaf arms below are exhaustive for validated -/// inputs; anything else is an internal invariant violation. +/// This reverses [`extract`]. Scalars keep their names, while array elements +/// use dotted indices. For example, a `field[2][2]` named `A` becomes +/// `A.0.0`, `A.0.1`, `A.1.0`, and `A.1.1`. +/// +/// [`Array::values`] expands repeated arrays such as `[0; 4]`. +/// +/// Tuples and structs are not supported. `eval_test_case` rejects them before +/// the inputs reach this function. pub fn flatten(name: &str, value: &Value) -> Vec<(String, Value)> { match value { Value::Array(arr) => arr From 85cd72e713b45356e64109e3fe2a01638cf766f2 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 15:28:59 -0400 Subject: [PATCH 17/29] Remove return type restriction in run_test function Removed unsupported return type check for tests. --- src/test_runner/mod.rs | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index 74e747bd..7cf57bcd 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -101,16 +101,6 @@ pub fn catch(f: impl FnOnce() -> R) -> Result { /// [`cfg`]; the caller must have set it (via `circ::cfg::set` or `set_default`) /// and it fixes the field/backend for the process. pub fn run_test(test: &TestCase) -> Outcome { - // Assert-style tests only: a return-typed test computes a value, but the - // annotation gives no expected output to check it against. - if test.has_return() { - return Outcome::Unsupported( - "test functions with a return type are not supported (yet); \ - drop the return type and use assert(...)" - .to_string(), - ); - } - // Compile the test function as its own entry point, from the file it was // discovered in. A failure here means the test never became a circuit. let name = test.name().to_string(); From 8029862bd4983ca9bcb67fc14cc991c69b330b9d Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 15:29:09 -0400 Subject: [PATCH 18/29] Refactor TestCase struct and improve documentation Updated documentation for TestCase struct and removed has_return field. --- src/front/zsharpcurly/mod.rs | 35 +++++++++++++++-------------------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index 599fef61..5b15ad54 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -39,25 +39,18 @@ pub struct Inputs { pub mode: Mode, } -/// A function marked `@test`, with its annotation inputs evaluated to -/// concrete values. +/// A function marked `@test` with validated, evaluated inputs. /// -/// a `TestCase` guarantees its *inputs* are validated — names -/// match parameters exactly, types are checked, values are constant. It -/// does not decide whether the function's *shape* is runnable; that is -/// runner policy. In particular, return-typed test functions are -/// discovered (see [Self::has_return]) and it is up to the runner to -/// support or reject them. +/// Input names and types must match the function parameters, and each input +/// must evaluate to a constant. Return-typed tests are rejected before a +/// `TestCase` is created. /// -/// Fields are private with read-only accessors: only -/// [`ZSharpCurlyFE::eval_test_inputs`] (in-crate) constructs these, and -/// external code cannot construct *or mutate* one, so downstream consumers -/// (e.g. [`TestCaseInput::flat_entries`]) can trust the invariant holds. +/// Only [`ZSharpCurlyFE::eval_test_inputs`] creates `TestCase` values. Its +/// private fields prevent callers from changing inputs after validation. #[derive(Debug, Clone)] #[non_exhaustive] pub struct TestCase { name: String, - has_return: bool, inputs: Vec, /// The source file this test was discovered in — used to recompile it as /// an entry point, keeping the case bound to its origin. @@ -69,12 +62,6 @@ impl TestCase { pub fn name(&self) -> &str { &self.name } - /// Whether the function declares a return type. Assert-style tests - /// (no return type) are self-checking; a runner may not support - /// return-typed tests, since the annotation gives no expected output. - pub fn has_return(&self) -> bool { - self.has_return - } /// The function's evaluated annotation inputs, in parameter order. pub fn inputs(&self) -> &[TestCaseInput] { &self.inputs @@ -338,6 +325,15 @@ fn eval_test_case<'ast>( &ann.span, )); } + if f.return_type.is_some() { + return Err(diag( + format!( + "@test function {} cannot declare a return type; use assert(...) instead", + f.id.value + ), + &ann.span, + )); + } // Index the annotation inputs by name, rejecting duplicates: collecting // silently would keep only the last value for a repeated name. @@ -471,7 +467,6 @@ fn eval_test_case<'ast>( Ok(TestCase { name: f.id.value.clone(), - has_return: f.return_type.is_some(), inputs, file: file.to_path_buf(), }) From 51d9b3acdbd3ad47bb2ac48ef3db02999c039063 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 15:37:14 -0400 Subject: [PATCH 19/29] Reject return-typed test functions during discovery --- examples/ztest.rs | 2 +- src/front/zsharpcurly/mod.rs | 14 +++--- src/test_runner/mod.rs | 7 +-- tests/zok_test_inputs.rs | 87 ++++++++++++++++-------------------- tests/ztest_e2e.rs | 22 --------- 5 files changed, 48 insertions(+), 84 deletions(-) diff --git a/examples/ztest.rs b/examples/ztest.rs index 9819c46a..753ea018 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -130,7 +130,7 @@ fn main() { println!("FAILED"); indent(msg); } - Outcome::Unsupported(msg) | Outcome::CompileError(msg) | Outcome::BackendError(msg) => { + Outcome::CompileError(msg) | Outcome::BackendError(msg) => { errored += 1; println!("error"); indent(msg); diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index 5b15ad54..cf119a88 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -326,13 +326,13 @@ fn eval_test_case<'ast>( )); } if f.return_type.is_some() { - return Err(diag( - format!( - "@test function {} cannot declare a return type; use assert(...) instead", - f.id.value - ), - &ann.span, - )); + return Err(diag( + format!( + "@test function {} cannot declare a return type; use assert(...) instead", + f.id.value + ), + &ann.span, + )); } // Index the annotation inputs by name, rejecting duplicates: collecting diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index 7cf57bcd..91278b24 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -19,17 +19,14 @@ use std::sync::Once; /// Result of running one test. /// -/// Assertion failures are kept separate from unsupported tests and -/// compile/backend errors, so execution failures are not treated as expected -/// test rejections. +/// Assertion failures are kept separate from compile/backend errors, so +/// execution failures are not treated as expected test rejections. #[derive(Debug)] pub enum Outcome { /// The assertion pre-check passed and the proof verified. Pass, /// The assertion pre-check failed. AssertionFailed(String), - /// The runner does not support this test shape. - Unsupported(String), /// Frontend compilation, optimization, or R1CS lowering failed. CompileError(String), /// Proof setup, proving, or verification failed. diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs index 04bb0d6a..a6df4146 100644 --- a/tests/zok_test_inputs.rs +++ b/tests/zok_test_inputs.rs @@ -108,8 +108,8 @@ fn constant_arithmetic_evaluates() { let tests = eval( "constant_arithmetic", r#"@test y = 3 * 3; -def test_sq(private field y) -> field { - return y; +def test_sq(private field y) { + assert(y == 9); } "#, ) @@ -129,8 +129,8 @@ fn named_constant_resolves() { r#"const field C = 7; @test x = C + 1; -def test_c(private field x) -> field { - return x; +def test_c(private field x) { + assert(x == 8); } "#, ) @@ -150,8 +150,8 @@ fn const_function_call_evaluates() { } @test y = sq(3); -def test_sq(private field y) -> field { - return y; +def test_sq(private field y) { + assert(y == 9); } "#, ) @@ -164,8 +164,8 @@ fn all_scalar_types_evaluate() { let tests = eval( "all_scalars", r#"@test b = true, n8 = 4u8, n16 = 4u16, n32 = 4u32, n64 = 4u64, f = 5f; -def test_scalars(private bool b, private u8 n8, private u16 n16, private u32 n32, private u64 n64, private field f) -> bool { - return b; +def test_scalars(private bool b, private u8 n8, private u16 n16, private u32 n32, private u64 n64, private field f) { + assert(b); } "#, ) @@ -187,8 +187,8 @@ fn unsuffixed_literal_typed_by_parameter() { let tests = eval( "unsuffixed_u32", r#"@test x = 2; -def test_u(private u32 x) -> u32 { - return x; +def test_u(private u32 x) { + assert(x == 2u32); } "#, ) @@ -201,8 +201,8 @@ fn bare_test_zero_params_ok() { let tests = eval( "bare_zero_params", r#"@test; -def test_noargs() -> bool { - return true; +def test_noargs() { + assert(true); } "#, ) @@ -216,8 +216,8 @@ fn bare_test_with_params_rejected() { let err = eval( "bare_with_params", r#"@test; -def test_missing(private field x) -> field { - return x; +def test_missing(private field x) { + assert(x == x); } "#, ) @@ -230,8 +230,8 @@ fn missing_input_rejected() { let err = eval( "missing_input", r#"@test a = 1; -def test_two(private field a, private field b) -> field { - return a; +def test_two(private field a, private field b) { + assert(a == a); } "#, ) @@ -244,8 +244,8 @@ fn unknown_input_rejected() { let err = eval( "unknown_input", r#"@test a = 1, nope = 2; -def test_one(private field a) -> field { - return a; +def test_one(private field a) { + assert(a == a); } "#, ) @@ -258,8 +258,8 @@ fn duplicate_input_rejected() { let err = eval( "duplicate_input", r#"@test a = 1, a = 2; -def test_dup(private field a) -> field { - return a; +def test_dup(private field a) { + assert(a == a); } "#, ) @@ -272,8 +272,8 @@ fn non_constant_expression_rejected() { let err = eval( "non_constant", r#"@test x = undefined_thing; -def test_bad(private field x) -> field { - return x; +def test_bad(private field x) { + assert(x == x); } "#, ) @@ -647,8 +647,8 @@ fn scalar_type_alias_accepted() { r#"type Word = u32; @test x = 2; -def test_alias(private Word x) -> Word { - return x; +def test_alias(private Word x) { + assert(x == 2u32); } "#, ) @@ -661,8 +661,8 @@ fn generic_test_function_rejected() { let err = eval( "generic_fn", r#"@test x = 1; -def test_gen(private field x) -> field { - return x; +def test_gen(private field x) { + assert(x == x); } "#, ) @@ -677,8 +677,8 @@ fn type_mismatch_rejected() { let err = eval( "type_mismatch", r#"@test x = true; -def test_ty(private field x) -> field { - return x; +def test_ty(private field x) { + assert(x == x); } "#, ) @@ -753,8 +753,8 @@ fn inputs_returned_in_parameter_order() { let tests = eval( "param_order", r#"@test b = 2, a = 1; -def test_order(private field a, private field b) -> field { - return a; +def test_order(private field a, private field b) { + assert(a == 1); } "#, ) @@ -785,28 +785,17 @@ def test_vis(private field a, public field b, field c) { } #[test] -fn has_return_exposed() { - // Runners use this to tell self-checking assert-style tests (no return - // type) from return-typed ones (unsupported in the MVP). - let tests = eval( - "has_return", - r#"@test x = 1; -def test_assert_style(private field x) { - assert(x == 1); -} - -@test y = 2; +fn return_typed_test_rejected() { + let err = eval( + "return_typed", + r#"@test y = 2; def test_return_style(private field y) -> field { return y; } "#, ) - .unwrap(); - assert!( - !tests[0].has_return(), - "assert-style test has no return type" - ); - assert!(tests[1].has_return(), "return-typed test is flagged"); + .unwrap_err(); + assert!(err.contains("cannot declare a return type"), "{}", err); } #[test] @@ -818,8 +807,8 @@ fn plain_functions_skipped() { } @test x = 1; -def test_only(private field x) -> field { - return x; +def test_only(private field x) { + assert(x == 1); } "#, ) diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs index 60e94f28..d54e49dd 100644 --- a/tests/ztest_e2e.rs +++ b/tests/ztest_e2e.rs @@ -245,25 +245,3 @@ def test_linear(private field x) { outcome ); } - -#[test] -fn return_typed_test_is_unsupported() { - // A return-typed test is not runnable (no expected output to check); it is - // an infrastructure "Unsupported", not an assertion failure. - let (_guard, path) = write_file( - "return_typed", - r#"@test x = 3; -def test_ret(private field x) -> field { - return x; -} -"#, - ); - let tests = discover(&path); - assert_eq!(tests.len(), 1); - let outcome = run_test::>(&tests[0]); - assert!( - matches!(outcome, Outcome::Unsupported(_)), - "got {:?}", - outcome - ); -} From 1e0fe839b22d9b293b4c8c45fe6d7f9cd5d6363f Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 16:15:02 -0400 Subject: [PATCH 20/29] Refine documentation for public inputs and tests Updated documentation for public input and test input evaluation methods to clarify behavior and expectations. --- src/front/zsharpcurly/mod.rs | 67 ++++++++++-------------------------- 1 file changed, 19 insertions(+), 48 deletions(-) diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index cf119a88..c43d9aea 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -92,9 +92,8 @@ impl TestCaseInput { pub fn name(&self) -> &str { &self.name } - /// Whether the parameter this input binds to is public (`public` or no - /// visibility keyword) rather than `private`. In a proof, public inputs - /// are shared with the verifier; private inputs stay with the prover. + /// Whether the input is public. Parameters without a visibility keyword + /// are public by default. pub fn public(&self) -> bool { self.public } @@ -109,13 +108,11 @@ impl TestCaseInput { &self.value } - /// The flattened `(input-name, scalar-value)` entries this input - /// contributes to a proof-pipeline input map. A scalar maps to itself - /// under the bare parameter name; an array yields one entry per leaf - /// under dotted index names (`field[2][2] A` yields `A.0.0` .. - /// `A.1.1`), matching the circuit variables `declare_input` creates. - /// Each leaf becomes one circuit input; the parameter's visibility - /// (`public`) applies to all of its leaves. + /// Returns the scalar entries used by the proof pipeline. + /// + /// Scalars keep their parameter name. Array elements use dotted names, so + /// `field[2][2] A` becomes `A.0.0` through `A.1.1`. The parameter's + /// visibility applies to every array element. pub fn flat_entries(&self) -> Vec<(String, Value)> { interp::flatten(&self.name, &self.value) } @@ -197,37 +194,15 @@ impl ZSharpCurlyFE { g.const_entry_fn(&entry, input_scalar_values) } - /// Evaluate the `@test` annotation inputs of every test function in `file`. - /// - /// Each input expression (e.g. the `3 * 3` in `@test y = 3 * 3;`) is run - /// through the same const evaluator used for `const` definitions and - /// array sizes, yielding a concrete [Value]. Functions without `@test` - /// are skipped. Nothing is compiled, proven, or executed. + /// Finds every `@test` function in `file` and evaluates its inputs. /// - /// Inputs are validated against the function's signature: - /// * every input must name a parameter, exactly once, and every - /// parameter must receive an input; - /// * parameters may be scalars (`field`, `bool`, `u8`..`u64`) or - /// (possibly nested) arrays of scalars; structs, tuples, and - /// zero-length arrays are rejected; - /// * unsuffixed literals are typed by the parameter they bind to (so - /// `x = 2` for a `u32 x` is a `u32`, and `xs = [1, 2]` for a - /// `u32[2] xs` types each element), and the evaluated type must - /// match the parameter's declared type — for arrays this also checks - /// length and element type; - /// * test functions parameterized with generics are rejected + /// Inputs must match the function parameters by name and type and evaluate to + /// constants. Scalars and nested scalar arrays are supported. Generic and + /// return-typed test functions are rejected. Functions without `@test` are + /// ignored. This method discovers tests but does not run them. /// - /// Known limits and semantics: - /// * The `Err` case covers annotation validation/evaluation only. - /// Loading/parsing failures panic and some semantic failures exit the - /// process, through pre-existing frontend paths — callers that must - /// survive arbitrary files should `catch_unwind`. - /// * Parameter-directed literal typing does not descend into call - /// arguments (`y = id(2)` for a `u32` fails; write `id(2u32)`), a - /// limit of [ZConstLiteralRewriter]. - /// * Annotation expressions have module-wide visibility: they are - /// evaluated after all declarations are processed, so they may - /// reference constants and functions declared later in the file. + /// `Err` only represents annotation errors; existing parser/frontend errors + /// may still panic or exit. pub fn eval_test_inputs(file: PathBuf, mode: Mode) -> Result, String> { // Load and typecheck the file (and its imports), exactly like `check`. // visit_files() also evaluates every `const` definition, so annotation @@ -265,11 +240,7 @@ impl ZSharpCurlyFE { } } -/// Is `ty` a scalar, or a (possibly nested) array whose base element is a -/// scalar? These are the parameter types `@test` supports: their values -/// flatten to the per-leaf scalar inputs the proof pipeline expects (see -/// [TestCaseInput::flat_entries]). Exhaustive on purpose: a new `Ty` -/// variant must decide whether it is supported. +/// Returns true for scalars and nested arrays of scalars supported by `@test`. fn is_scalar_or_scalar_array(ty: &Ty) -> bool { match ty { Ty::Uint(_) | Ty::Field | Ty::Bool | Ty::Integer => true, @@ -278,10 +249,10 @@ fn is_scalar_or_scalar_array(ty: &Ty) -> bool { } } -/// Does `ty` contain a zero-length array dimension? Such an input would -/// flatten to no circuit inputs at all, so it is rejected. -///`[]` values already fail const evaluation ("Empty array"), -/// but `[0; 0]` would evaluate cleanly without this type-level guard. +/// Returns true if any array dimension is zero. +/// +/// `[0; 0]` evaluates successfully but produces no circuit inputs, so it must +/// be rejected separately. fn has_zero_length_array(ty: &Ty) -> bool { match ty { Ty::Array(n, elem) => *n == 0 || has_zero_length_array(elem), From 88aa167945a6780c1d3111fa86b2cf10b891d656 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 16:33:16 -0400 Subject: [PATCH 21/29] Refactor comments in test runner module Updated comments for clarity and conciseness in the test runner module. --- src/test_runner/mod.rs | 36 ++++++++++-------------------------- 1 file changed, 10 insertions(+), 26 deletions(-) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index 91278b24..56ba1138 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -1,8 +1,5 @@ -//! Runs a ZoKrates `@test` through compilation and the proof pipeline. -//! -//! This module sits above the frontend, which provides validated [`TestCase`] -//! metadata and CirC IR without depending on the runner. The runner pre-checks -//! assertions and runs `setup -> prove -> verify` using a caller-selected +//! Runs a ZoKrates `@test` through compilation, assertion checking, setup, +//! proving, and verification. //! [`ProofSystem`]. Bellman and Mirage implement this interface; `ztest` uses //! Bellman Groth16 over BLS12-381. Spartan uses a separate interface and is not //! supported here. CLI output remains in `ztest`. @@ -41,13 +38,9 @@ thread_local! { static HOOK_INIT: Once = Once::new(); -/// Install, once per process, a panic hook that defers to the previous hook -/// except while the current thread is inside [catch]. Swapping the global hook -/// per call (take/quiet/restore) races under concurrency — two overlapping -/// calls can restore in the wrong order and leave the quiet hook installed for -/// good, or suppress an unrelated thread's panic. A thread-local flag consulted -/// by one installed-once hook avoids both: suppression is per-thread and the -/// global hook is never swapped after startup. +/// Installs one panic hook that uses a thread-local flag to silence panics +/// caught by [`catch`]. Installing it once avoids races from replacing the +/// global hook on every call. fn install_quiet_hook() { HOOK_INIT.call_once(|| { let prev = std::panic::take_hook(); @@ -89,12 +82,10 @@ pub fn catch(f: impl FnOnce() -> R) -> Result { }) } -/// Run one `@test` function through compile -> assert check -> setup -> prove -/// -> verify, using the proof system `PS`. +/// Runs one `@test` using the proof system `PS`. /// /// The test is recompiled from its own source file ([`TestCase::file`]), so the -/// case stays bound to the file it was discovered in — the caller cannot pair a -/// case with an unrelated path. The config is read from the process-global +/// case stays bound to the file it was discovered in. The config is read from the process-global /// [`cfg`]; the caller must have set it (via `circ::cfg::set` or `set_default`) /// and it fixes the field/backend for the process. pub fn run_test(test: &TestCase) -> Outcome { @@ -113,11 +104,7 @@ pub fn run_test(test: &TestCase) -> Outcome { Err(e) => return Outcome::CompileError(e), }; - // Build the prover and verifier input maps in a single pass over the - // inputs — one flatten per input, not one per map. The prover knows every - // input; the verifier sees only the public ones. Arrays flatten to one - // entry per leaf ("A.0.0", ...), the names the compiled circuit declares - // its input variables under; scalars are a single bare-named entry. + /// Give the prover all inputs and the verifier only public inputs. let mut prover_map: FxHashMap = FxHashMap::default(); let mut verifier_map: FxHashMap = FxHashMap::default(); for input in test.inputs() { @@ -128,11 +115,8 @@ pub fn run_test(test: &TestCase) -> Outcome { prover_map.extend(entries); } - // Evaluate assertions against the supplied prover inputs on the unoptimized IR. - // Checking before optimization catches failures that could otherwise be hidden - // if an optimization removes a private input from the circuit. This is only a - // pre-check; challenge-dependent assertions must still be checked during - // proving. + // Check assertions before optimization so removing a private input cannot hide + // a failure. Challenge-dependent assertions are still checked during proving. let held = catch(|| { comps .get(test.name()) From 4995d41c6101ffe21ec909bdc0fff6007d5dac81 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 16:36:42 -0400 Subject: [PATCH 22/29] Refine documentation for proof-mode optimization Updated documentation for the proof-mode optimizations to clarify the purpose and requirements of the optimization pipeline. --- src/compile.rs | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/compile.rs b/src/compile.rs index c68798ba..3266d1a6 100644 --- a/src/compile.rs +++ b/src/compile.rs @@ -10,16 +10,10 @@ use crate::target::r1cs::opt::reduce_linearities; use crate::target::r1cs::trans::to_r1cs; use crate::target::r1cs::{ProverData, R1csStats, VerifierData}; -/// Run the canonical proof-mode IR optimization pipeline on a set of -/// [`Computations`]. +/// Runs the proof-mode optimizations shared by the CLI and test runner. /// -/// This is the single owner of the pass list the CLI driver (`examples/circ.rs` -/// `Mode::Proof`) and the unit-test runner both use, so they cannot drift. The -/// passes are backend-independent (Groth16, Mirage, and Spartan all consume the -/// same optimized IR); the only configurable input is -/// [`cfg.ir.fits_in_bits_ip`](crate::cfg). This must run before [`to_proof_data`]: -/// R1CS lowering embeds scalar sorts only, so array/tuple terms have to be -/// scalarized and eliminated here first. +/// This must run before [`to_proof_data`] to remove arrays and tuples because +/// the R1CS lowering step accepts only scalar values. pub fn opt_for_proof(cs: Computations, cfg: &CircCfg) -> Computations { let mut opts = vec![ Opt::ConstantFold(Box::new([])), From 2f56252e5570b5cb73db2a912fef43950ed2f9ca Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 16:47:55 -0400 Subject: [PATCH 23/29] Refine comments in ztest_e2e.rs for clarity Updated comments to clarify the purpose and scope of end-to-end tests. --- tests/ztest_e2e.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs index d54e49dd..93bb9ba1 100644 --- a/tests/ztest_e2e.rs +++ b/tests/ztest_e2e.rs @@ -1,12 +1,9 @@ -//! End-to-end coverage of the `@test` runner: `eval_test_inputs` (discovery + -//! input evaluation) followed by `circ::test_runner::run_test` (compile -> -//! assert check -> setup -> prove -> verify through Groth16/BLS12-381). This is the -//! path the `ztest` example exercises; `tests/zok_test_inputs.rs` stops at -//! input evaluation, so without this file a regression in flattening, the IR -//! optimization pipeline, R1CS lowering, or the outcome semantics could merge -//! with every registered test green. +//! End-to-end tests for the `@test` runner using Groth16/BLS12-381. //! -//! Assertions are on the structured `Outcome`, not on printed text. +//! `zok_test_inputs.rs` stops after discovery and input evaluation. These tests +//! continue through array flattening, compilation, assertion checking, IR +//! optimization, R1CS lowering, setup, proving, and verification. They check +//! the structured [`Outcome`] rather than CLI output. #![cfg(all(feature = "smt", feature = "zokc", feature = "bellman"))] From 97c586ef2c4c9039a4608b179f438845f368cc5f Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Wed, 22 Jul 2026 20:26:55 -0400 Subject: [PATCH 24/29] Support tuple test inputs Add support for tuples in @test inputs across the frontend, literal rewriting, flattening, and tests. Key changes: - interp.flatten: handle Value::Tuple so tuple elements are flattened into dotted names (e.g. t.0, t.1). - Frontend validation: expand supported input types to include tuples (is_supported_test_input_type) and update empty-input check (has_empty_test_input). Update messages and docs to mention arrays and tuples. - ZConstLiteralRewriter: validate tuple literal types, add visit_inline_tuple_expression to type-check tuple elements, and improve error text for postfix accesses on tuple literals. - examples/ztest.rs: pretty-print singleton tuples as `(x,)` and format tuple printing. - tests: add many unit and e2e tests covering mixed-type tuples, nested tuples/arrays, array-of-tuples, singleton tuples, constant tuples, error cases (empty tuple, wrong length/type, postfix-on-literal), and ensure flattening names are correct. - Example Zokrates test file updated with tuple test cases; small comment/formatting tweaks in test_runner. These changes enable tuple-typed @test inputs (including nested and array-of-tuple combinations), improve diagnostics, and add comprehensive tests. --- examples/ZoKratesCurly/pf/coverage_test.zok | 40 +++- examples/ztest.rs | 9 +- src/front/zsharpcurly/interp.rs | 23 ++- src/front/zsharpcurly/mod.rs | 65 +++--- src/front/zsharpcurly/zvisit/zconstlitrw.rs | 68 +++++- src/test_runner/mod.rs | 9 +- tests/zok_test_inputs.rs | 216 +++++++++++++++++++- tests/ztest_e2e.rs | 55 ++++- 8 files changed, 420 insertions(+), 65 deletions(-) diff --git a/examples/ZoKratesCurly/pf/coverage_test.zok b/examples/ZoKratesCurly/pf/coverage_test.zok index d6d89d21..44af7bd4 100644 --- a/examples/ZoKratesCurly/pf/coverage_test.zok +++ b/examples/ZoKratesCurly/pf/coverage_test.zok @@ -1,5 +1,5 @@ -// Simple @test coverage: scalar and array inputs, private/public visibility. -// All tests pass. Run: +// Simple @test coverage: scalar, array, and tuple inputs, private/public +// visibility. All tests pass. Run: // cargo run --example ztest --features zokc -- examples/ZoKratesCurly/pf/coverage_test.zok // ---- scalar inputs ---- @@ -61,3 +61,39 @@ 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); +} diff --git a/examples/ztest.rs b/examples/ztest.rs index 753ea018..5dd6a0ee 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -50,7 +50,14 @@ fn pretty_value(v: &Value) -> String { .collect::>() .join(", ") ), - // Anything else (tuples, ...): fall back to the default form. + // 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::>().join(", ") + ), + // Anything else (structs, ...): fall back to the default form. other => other.to_string(), } } diff --git a/src/front/zsharpcurly/interp.rs b/src/front/zsharpcurly/interp.rs index 88d70025..06d2462f 100644 --- a/src/front/zsharpcurly/interp.rs +++ b/src/front/zsharpcurly/interp.rs @@ -54,17 +54,17 @@ pub fn extract( } } -/// Converts a scalar or array test input into the named scalar values expected -/// by the proof pipeline. +/// Converts a scalar, array, or tuple test input into the named scalar values +/// expected by the proof pipeline. /// -/// This reverses [`extract`]. Scalars keep their names, while array elements -/// use dotted indices. For example, a `field[2][2]` named `A` becomes -/// `A.0.0`, `A.0.1`, `A.1.0`, and `A.1.1`. +/// This reverses [`extract`]. Scalars keep their names, while array and tuple +/// elements use dotted indices. For example, a tuple named `t` becomes `t.0`, +/// `t.1`, and so on. /// /// [`Array::values`] expands repeated arrays such as `[0; 4]`. /// -/// Tuples and structs are not supported. `eval_test_case` rejects them before -/// the inputs reach this function. +/// Structs are not supported. `eval_test_case` rejects them before the inputs +/// reach this function. pub fn flatten(name: &str, value: &Value) -> Vec<(String, Value)> { match value { Value::Array(arr) => arr @@ -73,14 +73,19 @@ pub fn flatten(name: &str, value: &Value) -> Vec<(String, Value)> { .enumerate() .flat_map(|(i, v)| flatten(&format!("{name}.{i}"), &v)) .collect(), + Value::Tuple(values) => values + .iter() + .enumerate() + .flat_map(|(i, value)| flatten(&format!("{name}.{i}"), value)) + .collect(), // The scalar leaf kinds a validated @test input can hold — the same // set interp::extract accepts. Value::Field(_) | Value::BitVector(_) | Value::Bool(_) | Value::Int(_) => { vec![(name.to_string(), value.clone())] } other => unreachable!( - "non-scalar leaf {:?} in @test input {}; \ - eval_test_inputs rejects non-scalar parameter types", + "unsupported value {:?} in @test input {}; \ + eval_test_inputs rejects unsupported parameter types", other, name ), } diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index c43d9aea..e018657b 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -77,7 +77,7 @@ impl TestCase { /// Fields are private with read-only accessors; constructed only by the /// validated door ([`ZSharpCurlyFE::eval_test_inputs`]). External code can /// neither build nor mutate one, so [`Self::flat_entries`] can trust that -/// [`Self::value`] is a scalar or an array of scalars. +/// [`Self::value`] is a supported scalar, array, or tuple. #[derive(Debug, Clone)] #[non_exhaustive] pub struct TestCaseInput { @@ -101,18 +101,17 @@ impl TestCaseInput { pub fn source(&self) -> &str { &self.source } - /// The concrete value the expression evaluates to (`9`). Arrays are - /// stored whole, as a [Value::Array]; use [Self::flat_entries] to get - /// the per-leaf scalar entries the proof pipeline consumes. + /// The concrete value the expression evaluates to (`9`). Arrays and tuples + /// are stored whole; use [`Self::flat_entries`] to get their scalar entries. pub fn value(&self) -> &Value { &self.value } /// Returns the scalar entries used by the proof pipeline. /// - /// Scalars keep their parameter name. Array elements use dotted names, so - /// `field[2][2] A` becomes `A.0.0` through `A.1.1`. The parameter's - /// visibility applies to every array element. + /// Scalars keep their parameter name. Array and tuple elements use dotted + /// indices, such as `A.0.0` or `t.1`. The parameter's visibility applies + /// to every element. pub fn flat_entries(&self) -> Vec<(String, Value)> { interp::flatten(&self.name, &self.value) } @@ -197,9 +196,10 @@ impl ZSharpCurlyFE { /// Finds every `@test` function in `file` and evaluates its inputs. /// /// Inputs must match the function parameters by name and type and evaluate to - /// constants. Scalars and nested scalar arrays are supported. Generic and - /// return-typed test functions are rejected. Functions without `@test` are - /// ignored. This method discovers tests but does not run them. + /// constants. Scalars, nested arrays, and tuples composed of those types are + /// supported. Generic and return-typed test functions are rejected. Functions + /// without `@test` are ignored. This method discovers tests but does not run + /// them. /// /// `Err` only represents annotation errors; existing parser/frontend errors /// may still panic or exit. @@ -240,29 +240,26 @@ impl ZSharpCurlyFE { } } -/// Returns true for scalars and nested arrays of scalars supported by `@test`. -fn is_scalar_or_scalar_array(ty: &Ty) -> bool { +/// Returns true for scalar, array, and tuple inputs supported by `@test`. +fn is_supported_test_input_type(ty: &Ty) -> bool { match ty { Ty::Uint(_) | Ty::Field | Ty::Bool | Ty::Integer => true, - Ty::Array(_, elem) => is_scalar_or_scalar_array(elem), - Ty::MutArray(_) | Ty::Struct(..) | Ty::Tuple(..) => false, + Ty::Array(_, elem) => is_supported_test_input_type(elem), + Ty::Tuple(elements) => elements.iter().all(is_supported_test_input_type), + Ty::MutArray(_) | Ty::Struct(..) => false, } } -/// Returns true if any array dimension is zero. +/// Returns true if an array or tuple input contains no values. /// -/// `[0; 0]` evaluates successfully but produces no circuit inputs, so it must -/// be rejected separately. -fn has_zero_length_array(ty: &Ty) -> bool { +/// Empty inputs produce no circuit inputs, so they are rejected separately. +fn has_empty_test_input(ty: &Ty) -> bool { match ty { - Ty::Array(n, elem) => *n == 0 || has_zero_length_array(elem), - Ty::Uint(_) - | Ty::Field - | Ty::Bool - | Ty::Integer - | Ty::MutArray(_) - | Ty::Struct(..) - | Ty::Tuple(..) => false, + Ty::Array(n, elem) => *n == 0 || has_empty_test_input(elem), + Ty::Tuple(elements) => elements.is_empty() || elements.iter().any(has_empty_test_input), + Ty::Uint(_) | Ty::Field | Ty::Bool | Ty::Integer | Ty::MutArray(_) | Ty::Struct(..) => { + false + } } } @@ -349,26 +346,22 @@ fn eval_test_case<'ast>( .type_impl_::(&p.ty) .map_err(|e| diag(e, type_span(&p.ty)))?; - // Scalars and arrays of scalars: array values are flattened into - // per-leaf scalar inputs ("A.0", "A.1.0", ...) by flat_entries — the - // same names declare_input and interp::extract use. Structs and - // tuples are not supported yet. - if !is_scalar_or_scalar_array(&ty) { + if !is_supported_test_input_type(&ty) { return Err(diag( format!( "parameter {} of @test function {} has unsupported type {}; \ - only scalars (field, bool, u8..u64) and arrays of scalars \ - are supported", + only scalars (field, bool, u8..u64), arrays, and tuples \ + composed of those types are supported", p.id.value, f.id.value, ty ), &p.span, )); } - if has_zero_length_array(&ty) { + if has_empty_test_input(&ty) { return Err(diag( format!( - "parameter {} of @test function {} has a zero-length array \ - type {}; zero-length test inputs are not supported", + "parameter {} of @test function {} has an empty array or tuple \ + in type {}; empty test inputs are not supported", p.id.value, f.id.value, ty ), &p.span, diff --git a/src/front/zsharpcurly/zvisit/zconstlitrw.rs b/src/front/zsharpcurly/zvisit/zconstlitrw.rs index 332b62a7..97321688 100644 --- a/src/front/zsharpcurly/zvisit/zconstlitrw.rs +++ b/src/front/zsharpcurly/zvisit/zconstlitrw.rs @@ -135,6 +135,17 @@ impl<'ast> ZVisitorMut<'ast> for ZConstLiteralRewriter { Ty::Field => Ok(ast::DecimalSuffix::Field(ast::FieldSuffix { span: dle.span, })), + t @ Ty::Tuple(types) => { + let mut msg = + format!("ZConstLiteralRewriter: a literal cannot have tuple type {t}"); + if types.len() == 1 { + msg.push_str( + "; a single-element tuple is written (x,) with a trailing \ + comma; (x) is a parenthesized expression", + ); + } + Err(msg) + } _ => Err( "ZConstLiteralRewriter: rewriting DecimalLiteralExpression to incompatible type" .to_string(), @@ -266,6 +277,52 @@ impl<'ast> ZVisitorMut<'ast> for ZConstLiteralRewriter { self.visit_span(&mut iae.span) } + fn visit_inline_tuple_expression( + &mut self, + ite: &mut ast::InlineTupleExpression<'ast>, + ) -> ZVisitorResult { + // Validate against self.to_ty by reference so the error returns below + // leave the hint in place for the caller. + let element_types = match self.to_ty.as_ref() { + Some(Ty::Tuple(types)) if types.len() == ite.elements.len() => Some(types.clone()), + Some(Ty::Tuple(types)) => { + let n = ite.elements.len(); + return Err(format!( + "ZConstLiteralRewriter: tuple has {} element{}, expected {}", + n, + if n == 1 { "" } else { "s" }, + types.len() + ) + .into()); + } + Some(ty) => { + return Err(format!( + "ZConstLiteralRewriter: tuple expression used where {ty} is expected" + ) + .into()) + } + None => None, + }; + + let previous_ty = self.replace(None); + let result = (|| { + if let Some(types) = element_types { + for (element, ty) in ite.elements.iter_mut().zip(types) { + self.to_ty = Some(ty); + self.visit_expression(element)?; + } + } else { + for element in &mut ite.elements { + self.visit_expression(element)?; + } + } + self.visit_span(&mut ite.span) + })(); + + self.to_ty = previous_ty; + result + } + fn visit_postfix_expression( &mut self, pe: &mut ast::PostfixExpression<'ast>, @@ -273,9 +330,16 @@ impl<'ast> ZVisitorMut<'ast> for ZConstLiteralRewriter { use ast::Expression; match *pe.base { Expression::Identifier(ref mut id) => self.visit_identifier_expression(id)?, - _ => panic!("Expected identifier in postfix expression base"), + _ => { + return Err( + "ZConstLiteralRewriter: postfix expression base must be a named \ + identifier; accessing a literal such as (1, 2).0 is not supported \ + here; bind the value to a constant and access that instead" + .to_string() + .into(), + ) + } } - //self.visit_identifier_expression(&mut pe.base.id)?; // descend into accesses. we do not know expected type for these expressions // (but we may end up descending into an ArrayAccess, which would get typed) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index 56ba1138..e093bb1f 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -1,8 +1,9 @@ //! Runs a ZoKrates `@test` through compilation, assertion checking, setup, //! proving, and verification. -//! [`ProofSystem`]. Bellman and Mirage implement this interface; `ztest` uses -//! Bellman Groth16 over BLS12-381. Spartan uses a separate interface and is not -//! supported here. CLI output remains in `ztest`. +//! +//! The runner is generic over [`ProofSystem`]. Bellman and Mirage implement +//! this interface. `ztest` uses Bellman Groth16 over BLS12-381. Spartan uses a +//! separate interface and is not supported here. CLI output remains in `ztest`. use crate::cfg::cfg; use crate::compile::{opt_for_proof, to_proof_data}; @@ -104,7 +105,7 @@ pub fn run_test(test: &TestCase) -> Outcome { Err(e) => return Outcome::CompileError(e), }; - /// Give the prover all inputs and the verifier only public inputs. + // Give the prover all inputs and the verifier only public inputs. let mut prover_map: FxHashMap = FxHashMap::default(); let mut verifier_map: FxHashMap = FxHashMap::default(); for input in test.inputs() { diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs index a6df4146..a4f34d4a 100644 --- a/tests/zok_test_inputs.rs +++ b/tests/zok_test_inputs.rs @@ -67,6 +67,13 @@ fn array_values(v: &Value) -> Vec { } } +fn tuple_values(v: &Value) -> &[Value] { + match v { + Value::Tuple(values) => values, + other => panic!("expected tuple, got {:?}", other), + } +} + /// Assert a Value is an array of field elements with the given values. fn assert_field_array(v: &Value, expected: &[u64]) { let vals = array_values(v); @@ -550,27 +557,216 @@ def test_pt(private Point p) { ) .unwrap_err(); assert!(err.contains("unsupported type"), "{}", err); - assert!(err.contains("arrays of scalars"), "{}", err); + assert!(err.contains("arrays, and tuples"), "{}", err); } #[test] -fn tuple_parameter_rejected() { - let err = eval( +fn mixed_scalar_tuple_accepted() { + let tests = eval( "tuple_param", - r#"@test t = (1, true); -def test_tup(private (field, bool) t) { - assert(t.1); + r#"@test t = (1, 2, true); +def test_tup(private (field, u32, bool) t) { + assert(t.0 == 1); + assert(t.1 == 2u32); + assert(t.2); +} +"#, + ) + .unwrap(); + + let input = &tests[0].inputs()[0]; + let values = tuple_values(input.value()); + assert_field(&values[0], 1); + assert_uint(&values[1], 32, 2); + assert!(matches!(values[2], Value::Bool(true))); + + let entries = input.flat_entries(); + let names: Vec<&str> = entries.iter().map(|(name, _)| name.as_str()).collect(); + assert_eq!(names, ["t.0", "t.1", "t.2"]); +} + +#[test] +fn nested_tuple_and_array_accepted() { + let tests = eval( + "nested_tuple", + r#"@test t = ([1, 2], (true, 3)); +def test_nested(private (field[2], (bool, u32)) t) { + assert(t.0[1] == 2); + assert(t.1.0); + assert(t.1.1 == 3u32); +} +"#, + ) + .unwrap(); + + let entries = tests[0].inputs()[0].flat_entries(); + let names: Vec<&str> = entries.iter().map(|(name, _)| name.as_str()).collect(); + assert_eq!(names, ["t.0.0", "t.0.1", "t.1.0", "t.1.1"]); +} + +#[test] +fn array_of_tuples_accepted() { + let tests = eval( + "array_of_tuples", + r#"@test pairs = [(1, 2), (3, 4)]; +def test_pairs(private (field, u32)[2] pairs) { + assert(pairs[0].0 == 1); + assert(pairs[1].1 == 4u32); +} +"#, + ) + .unwrap(); + + let entries = tests[0].inputs()[0].flat_entries(); + let names: Vec<&str> = entries.iter().map(|(name, _)| name.as_str()).collect(); + assert_eq!(names, ["pairs.0.0", "pairs.0.1", "pairs.1.0", "pairs.1.1"]); +} + +#[test] +fn empty_tuple_rejected() { + let err = eval( + "empty_tuple", + r#"@test t = (); +def test_empty(private () t) { + assert(true); } "#, ) .unwrap_err(); - assert!(err.contains("unsupported type"), "{}", err); + assert!(err.contains("empty array or tuple"), "{}", err); +} + +#[test] +fn wrong_tuple_length_rejected() { + let err = eval( + "tuple_length", + r#"@test t = (1,); +def test_length(private (field, u32) t) { + assert(t.0 == 1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("tuple has 1 element, expected 2"), "{}", err); +} + +#[test] +fn wrong_tuple_element_type_rejected() { + let err = eval( + "tuple_element_type", + r#"@test t = (true, 2); +def test_type(private (field, u32) t) { + assert(t.0 == 1); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("expected type (field, u32)"), "{}", err); + assert!(err.contains("(bool, u32)"), "{}", err); +} + +#[test] +fn singleton_tuple_accepted() { + let tests = eval( + "singleton_tuple", + r#"@test t = (5,); +def test_single(private (field,) t) { + assert(t.0 == 5); +} +"#, + ) + .unwrap(); + + let input = &tests[0].inputs()[0]; + let values = tuple_values(input.value()); + assert_eq!(values.len(), 1); + assert_field(&values[0], 5); + + let entries = input.flat_entries(); + let names: Vec<&str> = entries.iter().map(|(name, _)| name.as_str()).collect(); + assert_eq!(names, ["t.0"]); +} + +#[test] +fn named_tuple_constant_accepted() { + let tests = eval( + "named_tuple_const", + r#"const (field, u32) T = (7, 9); + +@test t = T; +def test_const(private (field, u32) t) { + assert(t.0 == 7); + assert(t.1 == 9u32); +} +"#, + ) + .unwrap(); + + let input = &tests[0].inputs()[0]; + let values = tuple_values(input.value()); + assert_field(&values[0], 7); + assert_uint(&values[1], 32, 9); + + let entries = input.flat_entries(); + let names: Vec<&str> = entries.iter().map(|(name, _)| name.as_str()).collect(); + assert_eq!(names, ["t.0", "t.1"]); +} + +#[test] +fn postfix_on_tuple_literal_rejected() { + // Must be a contextual Err, not a panic. + let err = eval( + "postfix_tuple_literal", + r#"@test x = (1, 2).0; +def test_access(private field x) { + assert(x == 1); +} +"#, + ) + .unwrap_err(); + assert!( + err.contains("postfix expression base must be a named identifier"), + "{}", + err + ); +} + +#[test] +fn tuple_literal_for_scalar_rejected() { + let err = eval( + "tuple_for_scalar", + r#"@test x = (1, 2); +def test_scalar(private field x) { + assert(x == 1); +} +"#, + ) + .unwrap_err(); + assert!( + err.contains("tuple expression used where field is expected"), + "{}", + err + ); +} + +#[test] +fn paren_literal_for_singleton_tuple_hinted() { + // `(4)` is a parenthesized expression, not a 1-tuple; the error must + // point at the trailing-comma rule. + let err = eval( + "paren_singleton", + r#"@test t = (4); +def test_paren(private (field,) t) { + assert(t.0 == 4); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("trailing"), "{}", err); } #[test] fn array_of_struct_rejected() { - // The support check recurses to the array's base element: an array is - // only accepted if that base is a scalar. let err = eval( "arr_of_struct", r#"struct Point { @@ -620,7 +816,7 @@ def test_zero(private field[0] xs) { "#, ) .unwrap_err(); - assert!(err.contains("zero-length"), "{}", err); + assert!(err.contains("empty array or tuple"), "{}", err); } #[test] diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs index 93bb9ba1..a8de48d0 100644 --- a/tests/ztest_e2e.rs +++ b/tests/ztest_e2e.rs @@ -1,7 +1,7 @@ //! End-to-end tests for the `@test` runner using Groth16/BLS12-381. //! //! `zok_test_inputs.rs` stops after discovery and input evaluation. These tests -//! continue through array flattening, compilation, assertion checking, IR +//! continue through input flattening, compilation, assertion checking, IR //! optimization, R1CS lowering, setup, proving, and verification. They check //! the structured [`Outcome`] rather than CLI output. @@ -72,6 +72,59 @@ def test_mat(private field[2][2] A) { assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); } +#[test] +fn nested_tuple_passes_full_pipeline() { + let outcome = run_only( + "nested_tuple", + r#"@test t = ([1, 2], (true, 3)); +def test_tuple(private (field[2], (bool, u32)) t) { + assert(t.0[0] == 1); + assert(t.0[1] == 2); + assert(t.1.0); + assert(t.1.1 == 3u32); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn false_private_tuple_assertion_is_assertion_failure() { + // Linear, all-private: the class of assert that optimization can + // eliminate (the vacuous-pass hazard) — must FAIL, not pass, for tuple + // inputs just as for scalars and arrays. + let outcome = run_only( + "false_private_tuple", + r#"@test t = (4, true); +def test_tuple(private (field, bool) t) { + assert(t.0 == 99); + assert(t.1); +} +"#, + ); + assert!( + matches!(outcome, Outcome::AssertionFailed(_)), + "got {:?}", + outcome + ); +} + +#[test] +fn public_tuple_passes() { + // No visibility keyword = public: every tuple leaf goes into the + // verifier map too. + let outcome = run_only( + "public_tuple", + r#"@test t = (7, 9); +def test_tuple((field, u32) t) { + assert(t.0 == 7); + assert(t.1 == 9u32); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + #[test] fn array_initializer_passes() { // Sparse [0; 4]: the flatten path must still emit all four leaves. From 0e83e7887880a2cf56fe4e56514b9df9d3e0709f Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Thu, 23 Jul 2026 10:27:13 -0400 Subject: [PATCH 25/29] Support per-test backend selection (mirage/groth16) Add per-@test backend selection and plumbing to run tests with either Groth16 (Bellman) or Mirage. Introduces TestBackend and TestSettings in the zsharpcurly front end, parses test settings in the ZoKrates grammar, and exposes TestSetting/TestSettingName/TestSettingValue in the pest AST. Visitor traits and walkers were extended to visit test settings. eval_test_case now reads and validates the backend setting (rejecting duplicates, unknown names, and unsupported backends) and attaches settings to TestCase. Wire the backend into the CLI and test runner: examples/ztest prints the selected backend and selects either Bellman::Groth16 or Mirage when running a test; end-to-end tests were updated and a helper to run the selected backend was added. New unit tests cover parsing, discovery, and error cases for backend settings. Also updated an example test to demonstrate backend annotation and adjusted a mirage module docstring. Error messages include guidance on supported backends (groth16, mirage). --- examples/ZoKratesCurly/pf/coverage_test.zok | 6 +- examples/ztest.rs | 24 +++-- src/front/zsharpcurly/mod.rs | 76 +++++++++++++++ src/front/zsharpcurly/zvisit/walkfns.rs | 13 +++ src/front/zsharpcurly/zvisit/zvmut.rs | 4 + src/target/r1cs/mirage.rs | 2 +- src/test_runner/mod.rs | 10 +- tests/zok_test_inputs.rs | 97 ++++++++++++++++++- tests/ztest_e2e.rs | 47 ++++++++- .../zokrates_parser/src/zokrates.pest | 6 +- .../zokrates_pest_ast/src/lib.rs | 61 +++++++++++- 11 files changed, 317 insertions(+), 29 deletions(-) diff --git a/examples/ZoKratesCurly/pf/coverage_test.zok b/examples/ZoKratesCurly/pf/coverage_test.zok index 44af7bd4..cae4e21f 100644 --- a/examples/ZoKratesCurly/pf/coverage_test.zok +++ b/examples/ZoKratesCurly/pf/coverage_test.zok @@ -1,5 +1,5 @@ -// Simple @test coverage: scalar, array, and tuple inputs, private/public -// visibility. All tests pass. Run: +// Simple @test coverage: backend selection, scalar, array, and tuple inputs, +// and private/public visibility. All tests pass. Run: // cargo run --example ztest --features zokc -- examples/ZoKratesCurly/pf/coverage_test.zok // ---- scalar inputs ---- @@ -9,7 +9,7 @@ def test_field(private field x) { assert(x == 5); } -@test a = 4, b = 6; +@test(backend = mirage) a = 4, b = 6; def test_add(private field a, private field b) { assert(a + b == 10); } diff --git a/examples/ztest.rs b/examples/ztest.rs index 5dd6a0ee..81e7a144 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -6,17 +6,17 @@ //! and prints ok / FAILED per test. A test passes when its assertions //! evaluate to true on the given inputs (checked by direct IR evaluation — //! the proof pipeline alone can pass vacuously when optimization eliminates -//! a private variable) AND a proof can be produced and verifies (backend: -//! Groth16 over BLS12-381, hardcoded for the MVP). +//! a private variable) AND a proof can be produced and verifies. 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::ZSharpCurlyFE; +use circ::front::zsharpcurly::{TestBackend, ZSharpCurlyFE}; use circ::front::Mode; use circ::ir::term::Value; -use circ::target::r1cs::bellman::Bellman; +use circ::target::r1cs::{bellman::Bellman, mirage::Mirage}; use circ::test_runner::{catch, run_test, Outcome}; use clap::Parser; use std::path::PathBuf; @@ -112,22 +112,28 @@ fn main() { } }) .collect(); - print!("test {} ({}) ... ", t.name(), inputs.join(", ")); + 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(); - // Groth16 over BLS12-381 is hardcoded for the MVP; run_test is - // generic over the proof system, so this is the one place the backend - // is chosen. let indent = |msg: String| { // The prover's message spans several lines; indent them all. for line in msg.lines() { println!(" {}", line); } }; - match run_test::>(t) { + let outcome = match t.settings().backend() { + TestBackend::Groth16 => run_test::>(t), + TestBackend::Mirage => run_test::>(t), + }; + match outcome { Outcome::Pass => { passed += 1; println!("ok"); diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index e018657b..f54a5a69 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -39,6 +39,38 @@ pub struct Inputs { pub mode: Mode, } +/// Proof backend selected for an `@test` function. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +pub enum TestBackend { + /// Groth16 through Bellman. + #[default] + Groth16, + /// Mirage over BLS12-381. + Mirage, +} + +impl Display for TestBackend { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Self::Groth16 => f.write_str("groth16"), + Self::Mirage => f.write_str("mirage"), + } + } +} + +/// Settings attached to an `@test` function. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +pub struct TestSettings { + backend: TestBackend, +} + +impl TestSettings { + /// The proof backend used to run the test. + pub fn backend(&self) -> TestBackend { + self.backend + } +} + /// A function marked `@test` with validated, evaluated inputs. /// /// Input names and types must match the function parameters, and each input @@ -51,6 +83,7 @@ pub struct Inputs { #[non_exhaustive] pub struct TestCase { name: String, + settings: TestSettings, inputs: Vec, /// The source file this test was discovered in — used to recompile it as /// an entry point, keeping the case bound to its origin. @@ -62,6 +95,10 @@ impl TestCase { pub fn name(&self) -> &str { &self.name } + /// The settings from the test annotation. + pub fn settings(&self) -> &TestSettings { + &self.settings + } /// The function's evaluated annotation inputs, in parameter order. pub fn inputs(&self) -> &[TestCaseInput] { &self.inputs @@ -285,6 +322,44 @@ fn eval_test_case<'ast>( ) }; + let mut settings = TestSettings::default(); + let mut backend_seen = false; + for setting in &ann.settings { + match setting.name.value.as_str() { + "backend" if backend_seen => { + return Err(diag( + format!("duplicate @test setting backend for {}", f.id.value), + &setting.span, + )); + } + "backend" => { + backend_seen = true; + settings.backend = match setting.value.value.as_str() { + "groth16" => TestBackend::Groth16, + "mirage" => TestBackend::Mirage, + backend => { + return Err(diag( + format!( + "unsupported @test backend {} for {}; supported backends: groth16, mirage", + backend, f.id.value + ), + &setting.value.span, + )); + } + }; + } + name => { + return Err(diag( + format!( + "unknown @test setting {} for {}; supported settings: backend", + name, f.id.value + ), + &setting.name.span, + )); + } + } + } + // Generic test functions have no way to receive generic arguments from // an annotation, so reject them outright. if !f.generics.is_empty() { @@ -431,6 +506,7 @@ fn eval_test_case<'ast>( Ok(TestCase { name: f.id.value.clone(), + settings, inputs, file: file.to_path_buf(), }) diff --git a/src/front/zsharpcurly/zvisit/walkfns.rs b/src/front/zsharpcurly/zvisit/walkfns.rs index fd2c861d..c514c102 100644 --- a/src/front/zsharpcurly/zvisit/walkfns.rs +++ b/src/front/zsharpcurly/zvisit/walkfns.rs @@ -184,6 +184,10 @@ pub fn walk_test_annotation<'ast, Z: ZVisitorMut<'ast>>( visitor: &mut Z, testann: &mut ast::TestAnnotation<'ast>, ) -> ZVisitorResult { + testann + .settings + .iter_mut() + .try_for_each(|s| visitor.visit_test_setting(s))?; testann .inputs .iter_mut() @@ -191,6 +195,15 @@ pub fn walk_test_annotation<'ast, Z: ZVisitorMut<'ast>>( visitor.visit_span(&mut testann.span) } +pub fn walk_test_setting<'ast, Z: ZVisitorMut<'ast>>( + visitor: &mut Z, + setting: &mut ast::TestSetting<'ast>, +) -> ZVisitorResult { + visitor.visit_span(&mut setting.name.span)?; + visitor.visit_span(&mut setting.value.span)?; + visitor.visit_span(&mut setting.span) +} + pub fn walk_test_input<'ast, Z: ZVisitorMut<'ast>>( visitor: &mut Z, testinput: &mut ast::TestInput<'ast>, diff --git a/src/front/zsharpcurly/zvisit/zvmut.rs b/src/front/zsharpcurly/zvisit/zvmut.rs index 5732a47b..4bb33085 100644 --- a/src/front/zsharpcurly/zvisit/zvmut.rs +++ b/src/front/zsharpcurly/zvisit/zvmut.rs @@ -105,6 +105,10 @@ pub trait ZVisitorMut<'ast>: Sized { walk_test_annotation(self, testann) } + fn visit_test_setting(&mut self, setting: &mut ast::TestSetting<'ast>) -> ZVisitorResult { + walk_test_setting(self, setting) + } + fn visit_test_input(&mut self, testinput: &mut ast::TestInput<'ast>) -> ZVisitorResult { walk_test_input(self, testinput) } diff --git a/src/target/r1cs/mirage.rs b/src/target/r1cs/mirage.rs index 7dd81835..d741e3b6 100644 --- a/src/target/r1cs/mirage.rs +++ b/src/target/r1cs/mirage.rs @@ -355,7 +355,7 @@ mod serde_field { } } -/// The [::bellman] implementation of Groth16. +/// The Mirage proof system implemented by the Bellman fork. pub struct Mirage(PhantomData); /// The pk for [mirage] diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index e093bb1f..d12d7847 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -2,8 +2,8 @@ //! proving, and verification. //! //! The runner is generic over [`ProofSystem`]. Bellman and Mirage implement -//! this interface. `ztest` uses Bellman Groth16 over BLS12-381. Spartan uses a -//! separate interface and is not supported here. CLI output remains in `ztest`. +//! this interface, and `ztest` selects between them for each test. Spartan uses +//! a separate interface and is not supported here. CLI output remains in `ztest`. use crate::cfg::cfg; use crate::compile::{opt_for_proof, to_proof_data}; @@ -86,9 +86,9 @@ pub fn catch(f: impl FnOnce() -> R) -> Result { /// Runs one `@test` using the proof system `PS`. /// /// The test is recompiled from its own source file ([`TestCase::file`]), so the -/// case stays bound to the file it was discovered in. The config is read from the process-global -/// [`cfg`]; the caller must have set it (via `circ::cfg::set` or `set_default`) -/// and it fixes the field/backend for the process. +/// case stays bound to the file it was discovered in. The config is read from +/// the process-global [`cfg`]; the caller must have set it (via `circ::cfg::set` +/// or `set_default`) and it fixes the field and compiler options for the process. pub fn run_test(test: &TestCase) -> Outcome { // Compile the test function as its own entry point, from the file it was // discovered in. A failure here means the test never became a circuit. diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs index a4f34d4a..76973d65 100644 --- a/tests/zok_test_inputs.rs +++ b/tests/zok_test_inputs.rs @@ -7,7 +7,7 @@ #![cfg(all(feature = "smt", feature = "zokc"))] -use circ::front::zsharpcurly::{TestCase, ZSharpCurlyFE}; +use circ::front::zsharpcurly::{TestBackend, TestCase, ZSharpCurlyFE}; use circ::front::Mode; use circ::ir::term::Value; use std::sync::Once; @@ -994,6 +994,101 @@ def test_return_style(private field y) -> field { assert!(err.contains("cannot declare a return type"), "{}", err); } +#[test] +fn backend_settings_are_discovered() { + let tests = eval( + "backend_settings", + r#"@test; +def test_default() { + assert(true); +} + +@test(); +def test_empty_settings() { + assert(true); +} + +@test(backend = groth16); +def test_groth16() { + assert(true); +} + +@test(backend = mirage) x = 4; +def test_mirage(private field x) { + assert(x == 4); +} +"#, + ) + .unwrap(); + + assert_eq!(tests.len(), 4); + assert_eq!(tests[0].settings().backend(), TestBackend::Groth16); + assert_eq!(tests[1].settings().backend(), TestBackend::Groth16); + assert_eq!(tests[2].settings().backend(), TestBackend::Groth16); + assert_eq!(tests[3].settings().backend(), TestBackend::Mirage); + assert_eq!(tests[3].inputs()[0].name(), "x"); + assert_field(tests[3].inputs()[0].value(), 4); +} + +#[test] +fn backend_can_still_be_an_input_name() { + let tests = eval( + "backend_input", + r#"@test backend = 3; +def test_backend_input(private field backend) { + assert(backend == 3); +} +"#, + ) + .unwrap(); + + assert_eq!(tests[0].settings().backend(), TestBackend::Groth16); + assert_eq!(tests[0].inputs()[0].name(), "backend"); +} + +#[test] +fn duplicate_backend_setting_rejected() { + let err = eval( + "duplicate_backend", + r#"@test(backend = groth16, backend = mirage); +def test_duplicate() { + assert(true); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("duplicate @test setting backend"), "{}", err); +} + +#[test] +fn unknown_test_setting_rejected() { + let err = eval( + "unknown_setting", + r#"@test(backnd = groth16); +def test_unknown() { + assert(true); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("unknown @test setting backnd"), "{}", err); +} + +#[test] +fn unsupported_backend_rejected() { + let err = eval( + "unsupported_backend", + r#"@test(backend = spartan); +def test_spartan() { + assert(true); +} +"#, + ) + .unwrap_err(); + assert!(err.contains("unsupported @test backend spartan"), "{}", err); + assert!(err.contains("groth16, mirage"), "{}", err); +} + #[test] fn plain_functions_skipped() { let tests = eval( diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs index a8de48d0..242e3a76 100644 --- a/tests/ztest_e2e.rs +++ b/tests/ztest_e2e.rs @@ -1,4 +1,4 @@ -//! End-to-end tests for the `@test` runner using Groth16/BLS12-381. +//! End-to-end tests for the `@test` runner using Groth16 and Mirage over BLS12-381. //! //! `zok_test_inputs.rs` stops after discovery and input evaluation. These tests //! continue through input flattening, compilation, assertion checking, IR @@ -8,9 +8,9 @@ #![cfg(all(feature = "smt", feature = "zokc", feature = "bellman"))] use bls12_381::Bls12; -use circ::front::zsharpcurly::{TestCase, ZSharpCurlyFE}; +use circ::front::zsharpcurly::{TestBackend, TestCase, ZSharpCurlyFE}; use circ::front::Mode; -use circ::target::r1cs::bellman::Bellman; +use circ::target::r1cs::{bellman::Bellman, mirage::Mirage}; use circ::test_runner::{run_test, Outcome}; use std::path::{Path, PathBuf}; use std::sync::Once; @@ -50,12 +50,19 @@ fn discover(path: &Path) -> Vec { ZSharpCurlyFE::eval_test_inputs(path.to_path_buf(), Mode::Proof).unwrap() } +fn run_selected(test: &TestCase) -> Outcome { + match test.settings().backend() { + TestBackend::Groth16 => run_test::>(test), + TestBackend::Mirage => run_test::>(test), + } +} + /// Discover and run every test in a single-test file; return its outcome. fn run_only(test_name: &str, src: &str) -> Outcome { let (_guard, path) = write_file(test_name, src); let tests = discover(&path); assert_eq!(tests.len(), 1, "expected exactly one @test function"); - run_test::>(&tests[0]) + run_selected(&tests[0]) } #[test] @@ -72,6 +79,38 @@ def test_mat(private field[2][2] A) { assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); } +#[test] +fn mixed_backends_pass_in_one_file() { + let (_guard, path) = write_file( + "mixed_backends", + r#"@test(backend = groth16) x = 3; +def test_groth16(private field x) { + assert(x * x == 9); +} + +@test(backend = mirage) x = 4; +def test_mirage(private field x) { + assert(x * x == 16); +} +"#, + ); + let tests = discover(&path); + assert_eq!(tests.len(), 2); + assert_eq!(tests[0].settings().backend(), TestBackend::Groth16); + assert_eq!(tests[1].settings().backend(), TestBackend::Mirage); + + for test in &tests { + let outcome = run_selected(test); + assert!( + matches!(outcome, Outcome::Pass), + "{} with {} returned {:?}", + test.name(), + test.settings().backend(), + outcome + ); + } +} + #[test] fn nested_tuple_passes_full_pipeline() { let outcome = run_only( diff --git a/third_party/ZoKratesCurly/zokrates_parser/src/zokrates.pest b/third_party/ZoKratesCurly/zokrates_parser/src/zokrates.pest index 01444fc2..d23fd67e 100644 --- a/third_party/ZoKratesCurly/zokrates_parser/src/zokrates.pest +++ b/third_party/ZoKratesCurly/zokrates_parser/src/zokrates.pest @@ -14,7 +14,11 @@ main_import_directive = { "import" ~ quoted_string ~ ("as" ~ identifier)? } import_symbol = { identifier ~ ("as" ~ identifier)? } import_symbol_list = _{ import_symbol ~ ("," ~ import_symbol)* } function_definition = { test_annotation? ~ "def" ~ identifier ~ constant_generics_declaration? ~ "(" ~ parameter_list ~ ")" ~ ("->" ~ ty)? ~ block_statement } -test_annotation = { "@test" ~ test_inputs? ~ ";" } +test_annotation = { "@test" ~ ("(" ~ test_settings? ~ ")")? ~ test_inputs? ~ ";" } +test_settings = _{ test_setting ~ ("," ~ test_setting)* } +test_setting = { test_setting_name ~ "=" ~ test_setting_value } +test_setting_name = @{ identifier } +test_setting_value = @{ identifier } test_inputs = _{ test_input ~ ("," ~ test_input)* } test_input = { identifier ~ "=" ~ expression } const_definition = {"const" ~ typed_identifier ~ "=" ~ expression } diff --git a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs index 83b2b489..7e5a25b4 100644 --- a/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs +++ b/third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs @@ -25,11 +25,11 @@ pub use ast::{ NotOperator, Parameter, PosOperator, PostfixExpression, Pragma, PrivateVisibility, PublicVisibility, Range, RangeOrExpression, RawString, ReturnStatement, Span, Spread, SpreadOrExpression, Statement, StructDefinition, StructField, StructType, SymbolDeclaration, - TernaryExpression, TestAnnotation, TestInput, ToExpression, TupleType, Type, TypeDefinition, - TypedIdentifier, TypedIdentifierOrAssignee, U16NumberExpression, U16Suffix, U16Type, - U32NumberExpression, U32Suffix, U32Type, U64NumberExpression, U64Suffix, U64Type, - U8NumberExpression, U8Suffix, U8Type, UnaryExpression, UnaryOperator, Underscore, Visibility, - EOI, + TernaryExpression, TestAnnotation, TestInput, TestSetting, TestSettingName, TestSettingValue, + ToExpression, TupleType, Type, TypeDefinition, TypedIdentifier, TypedIdentifierOrAssignee, + U16NumberExpression, U16Suffix, U16Type, U32NumberExpression, U32Suffix, U32Type, + U64NumberExpression, U64Suffix, U64Type, U8NumberExpression, U8Suffix, U8Type, UnaryExpression, + UnaryOperator, Underscore, Visibility, EOI, }; mod ast { @@ -196,11 +196,39 @@ mod ast { #[derive(Debug, FromPest, PartialEq, Clone)] #[pest_ast(rule(Rule::test_annotation))] pub struct TestAnnotation<'ast> { + pub settings: Vec>, pub inputs: Vec>, #[pest_ast(outer())] pub span: Span<'ast>, } + #[derive(Debug, FromPest, PartialEq, Eq, Clone)] + #[pest_ast(rule(Rule::test_setting))] + pub struct TestSetting<'ast> { + pub name: TestSettingName<'ast>, + pub value: TestSettingValue<'ast>, + #[pest_ast(outer())] + pub span: Span<'ast>, + } + + #[derive(Debug, FromPest, PartialEq, Eq, Clone)] + #[pest_ast(rule(Rule::test_setting_name))] + pub struct TestSettingName<'ast> { + #[pest_ast(outer(with(span_into_str)))] + pub value: String, + #[pest_ast(outer())] + pub span: Span<'ast>, + } + + #[derive(Debug, FromPest, PartialEq, Eq, Clone)] + #[pest_ast(rule(Rule::test_setting_value))] + pub struct TestSettingValue<'ast> { + #[pest_ast(outer(with(span_into_str)))] + pub value: String, + #[pest_ast(outer())] + pub span: Span<'ast>, + } + #[derive(Debug, FromPest, PartialEq, Clone)] #[pest_ast(rule(Rule::test_input))] pub struct TestInput<'ast> { @@ -1631,6 +1659,29 @@ mod tests { assert_eq!(ann.inputs[1].name.value, "b"); assert_eq!(ann.inputs[1].value.span().as_str(), "3 * 3"); } + + #[test] + fn parses_test_settings_and_inputs() { + let source = r#"@test(backend = mirage) a = 3, b = 4; + def test_backend(private field a, private field b) { + assert(a + b == 7); + } +"#; + let ast = generate_ast(source).unwrap(); + let f = match &ast.declarations[0] { + SymbolDeclaration::Function(f) => f, + _ => panic!("expected a function"), + }; + let ann = f.test.as_ref().expect("should carry @test"); + + assert_eq!(ann.settings.len(), 1); + assert_eq!(ann.settings[0].name.value, "backend"); + assert_eq!(ann.settings[0].value.value, "mirage"); + assert_eq!(ann.inputs.len(), 2); + assert_eq!(ann.inputs[0].name.value, "a"); + assert_eq!(ann.inputs[1].name.value, "b"); + } + #[test] fn parses_array_test_inputs() { // The value slot is a full expression, so every array form parses: From 883ff16c72e0ad117a987cf3a685e9efb0c0e55e Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Mon, 27 Jul 2026 19:49:15 -0400 Subject: [PATCH 26/29] Remove singleton-tuple special-case and update tests Drop the special-case error for single-element tuple literal types in the const-literal rewriter, letting the generic "incompatible type" message surface instead. Update the corresponding test (rename and assert on the new message) and adjust related wording in examples and test-runner comments. Also add a TODO about additional proof backends in the front module and tidy several docstrings/comments for clarity. --- examples/ztest.rs | 7 +++--- src/front/zsharpcurly/mod.rs | 1 + src/front/zsharpcurly/zvisit/zconstlitrw.rs | 15 ++----------- src/test_runner/mod.rs | 24 ++++++++++----------- tests/zok_test_inputs.rs | 8 +++---- 5 files changed, 21 insertions(+), 34 deletions(-) diff --git a/examples/ztest.rs b/examples/ztest.rs index 81e7a144..6ed198b0 100644 --- a/examples/ztest.rs +++ b/examples/ztest.rs @@ -3,10 +3,9 @@ //! 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 -//! evaluate to true on the given inputs (checked by direct IR evaluation — -//! the proof pipeline alone can pass vacuously when optimization eliminates -//! a private variable) AND a proof can be produced and verifies. Tests use +//! 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 diff --git a/src/front/zsharpcurly/mod.rs b/src/front/zsharpcurly/mod.rs index f54a5a69..034b5407 100644 --- a/src/front/zsharpcurly/mod.rs +++ b/src/front/zsharpcurly/mod.rs @@ -39,6 +39,7 @@ pub struct Inputs { pub mode: Mode, } +//TODO: Add support for Spartan and Dorian Proof Backend. /// Proof backend selected for an `@test` function. #[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] pub enum TestBackend { diff --git a/src/front/zsharpcurly/zvisit/zconstlitrw.rs b/src/front/zsharpcurly/zvisit/zconstlitrw.rs index 97321688..dcfb95a9 100644 --- a/src/front/zsharpcurly/zvisit/zconstlitrw.rs +++ b/src/front/zsharpcurly/zvisit/zconstlitrw.rs @@ -135,17 +135,6 @@ impl<'ast> ZVisitorMut<'ast> for ZConstLiteralRewriter { Ty::Field => Ok(ast::DecimalSuffix::Field(ast::FieldSuffix { span: dle.span, })), - t @ Ty::Tuple(types) => { - let mut msg = - format!("ZConstLiteralRewriter: a literal cannot have tuple type {t}"); - if types.len() == 1 { - msg.push_str( - "; a single-element tuple is written (x,) with a trailing \ - comma; (x) is a parenthesized expression", - ); - } - Err(msg) - } _ => Err( "ZConstLiteralRewriter: rewriting DecimalLiteralExpression to incompatible type" .to_string(), @@ -333,8 +322,8 @@ impl<'ast> ZVisitorMut<'ast> for ZConstLiteralRewriter { _ => { return Err( "ZConstLiteralRewriter: postfix expression base must be a named \ - identifier; accessing a literal such as (1, 2).0 is not supported \ - here; bind the value to a constant and access that instead" + identifier; the CirC ZoKrates frontend does not support accessing \ + a literal such as (1, 2).0; bind the value to a constant first" .to_string() .into(), ) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index d12d7847..63b7f7da 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -54,19 +54,16 @@ fn install_quiet_hook() { } /// Run `f`, converting a panic on the current thread into `Err(message)`. +/// The frontend and the prover report failures by panicking. Panic-hook noise +/// is suppressed for this thread only (see [install_quiet_hook]). Cannot +/// contain `process::exit` paths (some frontend semantic errors exit rather +/// than unwind). /// -/// The frontend and the prover report failures by panicking, so callers must -/// unwind them into a value. Panic-hook noise is suppressed for the duration — -/// but only for this thread (see [install_quiet_hook]), so concurrent code and -/// later panics keep the normal hook. Cannot contain `process::exit` paths -/// (some frontend semantic errors exit rather than unwind). +/// Public because discovery can panic too ([`ZSharpCurlyFE::eval_test_inputs`] +/// panics on a parse/load failure). /// -/// TODO: Replace this panic-catching boundary with normal `Result` propagation -/// once the frontend and prover return structured errors. This requires a -/// broader error-handling refactor outside the current test-runner scope. -/// -/// Exposed for callers that must also survive panics from the discovery phase -/// (e.g. [`ZSharpCurlyFE::eval_test_inputs`] panics on a parse/load failure). +/// TODO: replace with `Result` propagation once the frontend and prover +/// return structured errors. pub fn catch(f: impl FnOnce() -> R) -> Result { install_quiet_hook(); let was = SUPPRESS_PANIC.with(|s| s.replace(true)); @@ -116,8 +113,9 @@ pub fn run_test(test: &TestCase) -> Outcome { prover_map.extend(entries); } - // Check assertions before optimization so removing a private input cannot hide - // a failure. Challenge-dependent assertions are still checked during proving. + // Evaluate assertions against the annotation inputs before optimization. + // Proof verification does not bind private inputs to the particular values + // supplied by the test runner, so check those values directly here. let held = catch(|| { comps .get(test.name()) diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs index 76973d65..d076b556 100644 --- a/tests/zok_test_inputs.rs +++ b/tests/zok_test_inputs.rs @@ -750,9 +750,9 @@ def test_scalar(private field x) { } #[test] -fn paren_literal_for_singleton_tuple_hinted() { - // `(4)` is a parenthesized expression, not a 1-tuple; the error must - // point at the trailing-comma rule. +fn paren_literal_for_singleton_tuple_rejected() { + // `(4)` is a parenthesized expression, not a 1-tuple, so the literal + // cannot satisfy the tuple hint. let err = eval( "paren_singleton", r#"@test t = (4); @@ -762,7 +762,7 @@ def test_paren(private (field,) t) { "#, ) .unwrap_err(); - assert!(err.contains("trailing"), "{}", err); + assert!(err.contains("incompatible type"), "{}", err); } #[test] From a80c190074d4a696279351703332507bec7d75f7 Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Mon, 27 Jul 2026 21:11:18 -0400 Subject: [PATCH 27/29] Add Mirage and Groth16 challenge e2e tests Add two end-to-end tests to tests/ztest_e2e.rs: one (chall_lookup_mirage_passes_full_pipeline) exercises sample_challenge and value_in_array through the Mirage backend, verifying a small binarization/range-lookup pipeline and the polynomial identity check over a flattened bit matrix; builtin lengths are made explicit to avoid generic inference. The second (chall_circuit_on_groth16_is_backend_error) is a control asserting that a challenge-style circuit under the Groth16 backend yields a BackendError (Bellman rejects the round structure at setup) rather than passing or producing a semantic assertion failure. --- tests/ztest_e2e.rs | 69 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs index 242e3a76..678efc9a 100644 --- a/tests/ztest_e2e.rs +++ b/tests/ztest_e2e.rs @@ -334,3 +334,72 @@ def test_linear(private field x) { outcome ); } + +#[test] +fn chall_lookup_mirage_passes_full_pipeline() { + // Exercises sample_challenge and value_in_array through the Mirage + // proof pipeline. Builtin lengths are explicit to avoid generic inference. + let outcome = run_only( + "chall_lookup", + r#"from "EMBED" import value_in_array, sample_challenge; + +const field[5] TABLE = [0, 1, 2, 3, 4]; + +@test(backend = mirage) image = [[1, 6], [7, 2]], bin = [[1, 0], [0, 1]], flat = [1, 0, 0, 1]; +def test_binarize(private field[2][2] image, private field[2][2] bin, private field[4] flat) { + for u32 r in 0..2 { + for u32 c in 0..2 { + // each claimed-binary pixel is a bit + assert(bin[r][c] * (1 - bin[r][c]) == 0); + // range lookup: bin = 1 -> image in [0,4]; bin = 0 -> image in [4,8] + field to_lookup = image[r][c] - 4 * (1 - bin[r][c]); + assert(value_in_array::<5>(to_lookup, TABLE)); + } + } + // flat == row-major(bin), checked as a polynomial identity at a + // verifier challenge; holds for every gamma when consistent + field gamma = sample_challenge::<8>([...flat, ...bin[0], ...bin[1]]); + field mut lhs = 0; + field mut rhs = 0; + field mut power = 1; + for u32 i in 0..4 { + lhs = lhs + flat[i] * power; + power = power * gamma; + } + field mut power2 = 1; + for u32 r in 0..2 { + for u32 c in 0..2 { + rhs = rhs + bin[r][c] * power2; + power2 = power2 * gamma; + } + } + assert(lhs == rhs); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn chall_circuit_on_groth16_is_backend_error() { + // Control: a challenge circuit under Groth16 is a BackendError (Bellman + // rejects round structure at setup) — never Pass, and never a semantic + // AssertionFailed. x = y makes the identity hold for every challenge, so + // the pre-check passes and the failure is pinned to the backend. + let outcome = run_only( + "chall_groth16", + r#"from "EMBED" import sample_challenge; + +@test(backend = groth16) x = 3, y = 3; +def test_chall(private field x, private field y) { + field a = sample_challenge::<2>([x, y]); + assert(a * x == a * y); +} +"#, + ); + assert!( + matches!(outcome, Outcome::BackendError(_)), + "got {:?}", + outcome + ); +} From 93b84cc6d9b4fe6c66d35a3376490dded2a611ce Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Tue, 28 Jul 2026 21:22:28 -0400 Subject: [PATCH 28/29] Refactor challenge tests for Mirage backend Split and simplify the previous challenge lookup test into two focused tests: chall_sample_challenge_mirage_passes_full_pipeline (verifies sample_challenge with equal inputs and explicit generics) and chall_value_in_array_mirage_passes_full_pipeline (verifies value_in_array with a compile-time TABLE lookup). Updated embedded test snippets, made lookup table constant. Also refined the Groth16 test comment. --- tests/ztest_e2e.rs | 71 ++++++++++++++++++++-------------------------- 1 file changed, 31 insertions(+), 40 deletions(-) diff --git a/tests/ztest_e2e.rs b/tests/ztest_e2e.rs index 678efc9a..2862441a 100644 --- a/tests/ztest_e2e.rs +++ b/tests/ztest_e2e.rs @@ -336,44 +336,36 @@ def test_linear(private field x) { } #[test] -fn chall_lookup_mirage_passes_full_pipeline() { - // Exercises sample_challenge and value_in_array through the Mirage - // proof pipeline. Builtin lengths are explicit to avoid generic inference. +fn chall_sample_challenge_mirage_passes_full_pipeline() { + // Equal inputs make the identity hold for any challenge value. + // Generics are explicit because inference invokes an external SMT solver. + let outcome = run_only( + "chall_sample", + r#"from "EMBED" import sample_challenge; + +@test(backend = mirage) x = 3, y = 3; +def test_chall(private field x, private field y) { + field a = sample_challenge::<2>([x, y]); + assert(a * x == a * y); +} +"#, + ); + assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome); +} + +#[test] +fn chall_value_in_array_mirage_passes_full_pipeline() { + // The lookup table must be a compile-time constant, and the lookup's + // lowering creates a verifier challenge, so this also needs mirage. let outcome = run_only( "chall_lookup", - r#"from "EMBED" import value_in_array, sample_challenge; - -const field[5] TABLE = [0, 1, 2, 3, 4]; - -@test(backend = mirage) image = [[1, 6], [7, 2]], bin = [[1, 0], [0, 1]], flat = [1, 0, 0, 1]; -def test_binarize(private field[2][2] image, private field[2][2] bin, private field[4] flat) { - for u32 r in 0..2 { - for u32 c in 0..2 { - // each claimed-binary pixel is a bit - assert(bin[r][c] * (1 - bin[r][c]) == 0); - // range lookup: bin = 1 -> image in [0,4]; bin = 0 -> image in [4,8] - field to_lookup = image[r][c] - 4 * (1 - bin[r][c]); - assert(value_in_array::<5>(to_lookup, TABLE)); - } - } - // flat == row-major(bin), checked as a polynomial identity at a - // verifier challenge; holds for every gamma when consistent - field gamma = sample_challenge::<8>([...flat, ...bin[0], ...bin[1]]); - field mut lhs = 0; - field mut rhs = 0; - field mut power = 1; - for u32 i in 0..4 { - lhs = lhs + flat[i] * power; - power = power * gamma; - } - field mut power2 = 1; - for u32 r in 0..2 { - for u32 c in 0..2 { - rhs = rhs + bin[r][c] * power2; - power2 = power2 * gamma; - } - } - assert(lhs == rhs); + r#"from "EMBED" import value_in_array; + +const field[4] TABLE = [3, 5, 7, 9]; + +@test(backend = mirage) x = 7; +def test_lookup(private field x) { + assert(value_in_array::<4>(x, TABLE)); } "#, ); @@ -382,10 +374,9 @@ def test_binarize(private field[2][2] image, private field[2][2] bin, private fi #[test] fn chall_circuit_on_groth16_is_backend_error() { - // Control: a challenge circuit under Groth16 is a BackendError (Bellman - // rejects round structure at setup) — never Pass, and never a semantic - // AssertionFailed. x = y makes the identity hold for every challenge, so - // the pre-check passes and the failure is pinned to the backend. + // Groth16 cannot run verifier-challenge circuits. + // Using equal inputs lets the assertion pre-check pass, + // so the failure comes from backend setup. let outcome = run_only( "chall_groth16", r#"from "EMBED" import sample_challenge; From c8bcfc79d581c5640c88822e54ee29b96c196d9d Mon Sep 17 00:00:00 2001 From: Karan Pratap Singh <144534418+karandeol-26@users.noreply.github.com> Date: Thu, 30 Jul 2026 14:12:43 -0400 Subject: [PATCH 29/29] Clarify assertion checks before optimization Expand comment in test runner to explain that optimization can replace private inputs with constants, allowing failing inputs to still pass proof verification. --- src/test_runner/mod.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs index 63b7f7da..89d6bfa4 100644 --- a/src/test_runner/mod.rs +++ b/src/test_runner/mod.rs @@ -113,9 +113,12 @@ pub fn run_test(test: &TestCase) -> Outcome { prover_map.extend(entries); } - // Evaluate assertions against the annotation inputs before optimization. - // Proof verification does not bind private inputs to the particular values - // supplied by the test runner, so check those values directly here. + //Optimization replaces private values with constants when required by the circuit, + //allowing some private inputs that would fail assertions to actually pass proof verification. + //We check these asserts separately, before optimization, and fail on these inputs. + //Note: this differs from what the real prove/verify pipeline does! + //TODO: Make this a warning instead of a failure. + let held = catch(|| { comps .get(test.name())