Zok unit test runner by karandeol-26 · Pull Request #9 · sschefflab/circ

karandeol-26 · 2026-07-17T18:04:19Z

Adds a unit-test framework for ZoKratesCurly: @test-annotated functions in .zok files that a runner discovers, evaluates inputs for, and runs through the full in-memory ZK pipeline (compile → assert-check → prove → verify), printing cargo test–style pass/fail with an exit code. Supports scalar and array inputs and all private/public visibility combinations. Run with cargo run --example ztest --features zokc -- filepath/myfile.zok

Runner core (src/test_runner/, generic over the proof system).

I left generous comments throughout, so anyone building on top can understand what's going on without reverse-engineering it.

@test

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.

…circ into zok_unit_test_runner

@test

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.

@test

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.

…circ into zok_unit_test_runner

Copilot

Pull request overview

Adds an in-repo unit-test runner for ZoKratesCurly @test-annotated functions, including frontend discovery + constant input evaluation, plus an end-to-end “compile → assert-check → prove → verify” execution path (with examples and Rust integration tests) to prevent regressions across the full proof pipeline.

Changes:

Introduces ZSharpCurlyFE::eval_test_inputs and associated TestCase/TestCaseInput API to discover and const-evaluate @test inputs (including arrays and visibility).
Adds reusable runner core circ::test_runner::run_test (generic over proof system) and a CLI wrapper example examples/ztest.rs.
Centralizes the proof-mode optimization pass list into compile::opt_for_proof and adds comprehensive integration tests (input-contract + E2E Groth16).

Reviewed changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs	Extends AST parser tests to cover array-shaped `@test` inputs.
tests/ztest_e2e.rs	New end-to-end integration tests covering full proof pipeline outcomes.
tests/zok_test_inputs.rs	New integration tests specifying the input/typing/validation contract of `eval_test_inputs`.
src/test_runner/mod.rs	New reusable runner core (`catch`, `run_test`, `Outcome`) orchestrating compile + assert-check + prove/verify.
src/lib.rs	Exposes `test_runner` behind feature gates.
src/front/zsharpcurly/zvisit/zvmut.rs	Adds visitor hooks for `TestAnnotation` and `TestInput`.
src/front/zsharpcurly/zvisit/walkfns.rs	Ensures AST walking traverses `@test` annotations and inputs.
src/front/zsharpcurly/mod.rs	Adds `TestCase`/`TestCaseInput` types and implements `ZSharpCurlyFE::eval_test_inputs` + validation/eval logic.
src/front/zsharpcurly/interp.rs	Adds `interp::flatten` to convert validated scalar/array `Value`s into per-leaf input map entries.
src/compile.rs	Adds `opt_for_proof` to centralize proof-mode IR optimization pipeline used by CLI + runner.
examples/ztest.rs	New CLI example runner for `@test` functions (Groth16/BLS12-381 MVP).
examples/ZoKratesCurly/pf/discovery_demo.zok	Demo program for `@test` discovery behavior.
examples/ZoKratesCurly/pf/coverage_test.zok	Example program exercising scalar/array inputs and visibility combinations.
examples/circ.rs	Refactors proof-mode compilation path to use `compile::opt_for_proof`.
Cargo.toml	Registers the new example and integration tests with required feature sets.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Removed duplicate assertion for the second input value.

Updated documentation comments to use the new style.

kmerrill18

Most, if not all, of my comments and requested changes are about documentation instead of the code itself. :)

Overall, I think a lot of the docstring comments are quite AI-y and verbose. I'm actually less bothered by the AI-ness (it's pretty expected that they are written by AI these days I think), but the verbose-ness does bother me. I left a few notes, but it might be worth a pass to see if you can shorten the long comment blocks in any spots.

kmerrill18 · 2026-07-17T20:50:30Z

+//! 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`


This doesn't make sense to me. Why are private arrays more efficient to compile than public ones?

They aren’t cheaper to compile, the note is about verification. Public leaves increase the Groth16 verifying key and verifier work; private leaves remain witness values. I’ll clarify the wording.

But prover work should increase with the size of the witness, and moving large arrays into the witness will increase that size. And also, visibility in tests should match the expected "real world" use case and not whatever is most efficient to test. Unless I am still misunderstanding something, I would remove this note.

I’ll remove the note. You are right tests should use the same public/private visibility expected in production.

kmerrill18 · 2026-07-17T21:27:31Z

+        Err(e) => return Outcome::CompileError(e),
+    };
+
+    // Backend setup, then prove + verify. The assertions already held under


Again, not necessarily true - see above. I still think we should separate these error types, but just the documentation here is not accurate.

kmerrill18 · 2026-07-17T21:31:13Z

@@ -0,0 +1,838 @@
+//! The input contract of `ZSharpCurlyFE::eval_test_inputs`: which `@test`


I didn't look at the path of this file and just started reading, and I was very confused! Perhaps this top level comment should say "Tests the input contracts of ..." to make sure everyone knows this file is just for tests and not real infra. :)

Updated documentation to clarify that the function is limited to arrays instead of just indexed arrays.

Clarify comments regarding zero-length array handling.

Removed performance notes regarding array leaves and verification costs.

kmerrill18

Thank you! Documentation is looking a lot better. Just a few more small things.

kmerrill18 · 2026-07-21T22:32:28Z

+#[non_exhaustive]
+pub struct TestCase {
+    name: String,
+    has_return: bool,


Why do we gather up malformed tests into this struct? Can we error out right where we see the return type?

kmerrill18 · 2026-07-21T22:32:51Z

 /// concrete values.
 ///
-/// Contract: a `TestCase` guarantees its *inputs* are validated — names
+/// a `TestCase` guarantees its *inputs* are validated — names


I'm sorry, so annoying, but please capitalize the sentence :)

kmerrill18 · 2026-07-21T22:35:20Z

+/// 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.


Ah, so it's just the "exhaustive match" feature of the rust compiler. Yeah I don't think you need to say that.

Added TODO comments regarding future error handling improvements.

Updated documentation for the flatten function to clarify its behavior and limitations regarding scalar and array inputs.

Removed unsupported return type check for tests.

Updated documentation for TestCase struct and removed has_return field.

Updated documentation for public input and test input evaluation methods to clarify behavior and expectations.

Updated comments for clarity and conciseness in the test runner module.

Updated documentation for the proof-mode optimizations to clarify the purpose and requirements of the optimization pipeline.

Updated comments to clarify the purpose and scope of end-to-end tests.

@test

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.

@test

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).

kmerrill18 · 2026-07-23T19:57:08Z

+//!   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


I'm not convinced that this is true. If the CirC compiler is sound, shouldn't it not compile away inputs that actually get used in assertions that aren't trivially true?
I think it doesn't really matter if this is the case or not, but we just shouldn't be making statements in the comments that we aren't sure are true.

kmerrill18 · 2026-07-23T20:00:50Z

                Ty::Field => Ok(ast::DecimalSuffix::Field(ast::FieldSuffix {
                    span: dle.span,
                })),
+                t @ Ty::Tuple(types) => {


What's going on here? From the code, this looks like an "illegal representable state." ie, we can represent a tuple as a literal, but apparently it's not??? If that is indeed what is happening, that is bad, and we should remove Tuple from the type we are matching on here. Otherwise, please explain.

From discussion irl: tuples are never constant literals, so remove this match case, and let it fall into the generic error case below.

kmerrill18 · 2026-07-23T20:04:09Z

+                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"


When you say "not supported here", do you mean "not supported by ZoKrates" or "not supported here specifically"? If the former, remove the "here," if the latter, why?

I meant that this is a limitation of CirC’s ZoKrates frontend, not ZoKrates itself. The existing postfix typing and evaluation paths require the base to be an identifier. I’ll make that explicit in the error message.

kmerrill18 · 2026-07-23T20:14:46Z

+        prover_map.extend(entries);
+    }
+
+    // Check assertions before optimization so removing a private input cannot hide


Related to another comment about how the soundness of the CirC compiler should mean that optimization does not convert any failures into successes. Figure out what the truth is there and fix comments accordingly.

Optimization is sound. The pre-check is needed to evaluate assertions against the exact private values provided by the @test annotation. I updated the comments to describe the pre-check in those terms.

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.

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.

kmerrill18 · 2026-07-28T17:11:48Z

-    // 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


what does this last sentence mean?

basically the proof verifies only means some private values satisfy the constraints. The verifier never sees private inputs, so it can't check they were the values from the @test annotation. e.g. @test x = 4 with assert(x == 99) still gives a valid proof, because the optimizer substitutes x = 99 and the 4 never gets used. So this eval is the only place the supplied values actually get checked.

Hmmm, that shouldn't be the case by the soundness of the proof system. The assertion checker can't check it, sure, but if the prover provides 4 as the witness when generating the proof, that proof should fail to verify.

I agree that the proof should fail if 4 reaches the prover as the witness. What I found is that optimization removes x first, so the supplied 4 is never used and the proof proceeds with x = 99.

I reproduced this with the pre-check removed and the proof still verified.

Ok, I investigated for myself and you are right. It seems that CirC does optimize away relating private inputs to constants, which sure, I guess there is nothing to actually prove there. Sorry for leading you astray there!

I'm a little torn as to whether having the test behavior deviate from the real proof/verify system is actually desirable. On the one hand, passing in an input that fails an assert you wrote is probably an accident/mistake, but on the other hand, the point of these tests is to see what the prover and the verifier actually do.

Let's leave it as is for now, but clarify this comment and leave a note to address this in the future. Perhaps something like "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 behavior differs from the real pipeline! In the future, it may be more desirable to make this a warning instead of a failure."

kmerrill18 · 2026-07-28T17:14:09Z

 }
+
+#[test]
+fn chall_lookup_mirage_passes_full_pipeline() {


Sure, we don't need to spend a ton of cycles spinning on this, but these tests could be a lot simpler. The goal is just to demonstrate that value_in_array and sample_challenge work, not test the specific examples I linked. So you could write much simpler contrived examples using those functions that would be more readable. Does that make sense?

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.

kmerrill18 · 2026-07-29T18:39:54Z

-    // 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


Ok, I investigated for myself and you are right. It seems that CirC does optimize away relating private inputs to constants, which sure, I guess there is nothing to actually prove there. Sorry for leading you astray there!

I'm a little torn as to whether having the test behavior deviate from the real proof/verify system is actually desirable. On the one hand, passing in an input that fails an assert you wrote is probably an accident/mistake, but on the other hand, the point of these tests is to see what the prover and the verifier actually do.

Let's leave it as is for now, but clarify this comment and leave a note to address this in the future. Perhaps something like "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 behavior differs from the real pipeline! In the future, it may be more desirable to make this a warning instead of a failure."

Expand comment in test runner to explain that optimization can replace private inputs with constants, allowing failing inputs to still pass proof verification.

karandeol-26 added 8 commits July 13, 2026 21:33

Update .gitignore

dd8b3f7

Merge branch 'zok_unit_test_runner' of https://github.com/sschefflab/…

332040c

…circ into zok_unit_test_runner

Merge branch 'master' into zok_unit_test_runner

e84472f

Merge branch 'zok_unit_test_runner' of https://github.com/sschefflab/…

6c83f30

…circ into zok_unit_test_runner

Update coverage_test.zok

5e3f639

karandeol-26 requested a review from Copilot July 17, 2026 18:46

Copilot started reviewing on behalf of karandeol-26 July 17, 2026 18:46 View session

Copilot AI reviewed Jul 17, 2026

View reviewed changes

Comment thread third_party/ZoKratesCurly/zokrates_pest_ast/src/lib.rs Outdated

Comment thread examples/ztest.rs Outdated

karandeol-26 added 2 commits July 17, 2026 14:54

Remove duplicate assertion in test case

3ba60f8

Removed duplicate assertion for the second input value.

Refactor comments to use Rust doc comments format

08236ec

Updated documentation comments to use the new style.

karandeol-26 marked this pull request as ready for review July 17, 2026 19:02

karandeol-26 requested a review from kmerrill18 July 17, 2026 19:02

karandeol-26 marked this pull request as draft July 17, 2026 19:03

karandeol-26 marked this pull request as ready for review July 17, 2026 19:03

kmerrill18 requested changes Jul 17, 2026

View reviewed changes

karandeol-26 added 5 commits July 21, 2026 13:41

Clarify documentation on value-only array handling

49ca19b

Updated documentation to clarify that the function is limited to arrays instead of just indexed arrays.

Fix formatting in documentation comment

ae9cbc2

Update comments for zero-length array check

020f58f

Clarify comments regarding zero-length array handling.

Refactor comments and update outcome descriptions

0ab8cbf

Update comment on generic test functions rejection

9cd54fe

kmerrill18 self-requested a review July 21, 2026 22:30

Remove performance notes from ztest.rs

bf16d69

Removed performance notes regarding array leaves and verification costs.

kmerrill18 requested changes Jul 21, 2026

View reviewed changes

karandeol-26 added 4 commits July 21, 2026 18:48

Add TODO for error handling refactor in catch function

d2bcd53

Added TODO comments regarding future error handling improvements.

Refactor comments in walk_function_definition

f66c1d9

Revise flatten function documentation

9700b47

Updated documentation for the flatten function to clarify its behavior and limitations regarding scalar and array inputs.

Remove return type restriction in run_test function

85cd72e

Removed unsupported return type check for tests.

karandeol-26 added 8 commits July 22, 2026 15:29

Refactor TestCase struct and improve documentation

8029862

Updated documentation for TestCase struct and removed has_return field.

Reject return-typed test functions during discovery

51d9b3a

Refine documentation for public inputs and tests

1e0fe83

Updated documentation for public input and test input evaluation methods to clarify behavior and expectations.

Refactor comments in test runner module

88aa167

Updated comments for clarity and conciseness in the test runner module.

Refine documentation for proof-mode optimization

4995d41

Updated documentation for the proof-mode optimizations to clarify the purpose and requirements of the optimization pipeline.

Refine comments in ztest_e2e.rs for clarity

2f56252

Updated comments to clarify the purpose and scope of end-to-end tests.

kmerrill18 self-requested a review July 23, 2026 19:53

kmerrill18 requested changes Jul 23, 2026

View reviewed changes

karandeol-26 added 2 commits July 27, 2026 19:49

kmerrill18 self-requested a review July 28, 2026 17:10

kmerrill18 reviewed Jul 28, 2026

View reviewed changes

kmerrill18 requested changes Jul 29, 2026

View reviewed changes

Clarify assertion checks before optimization

c8bcfc7

Expand comment in test runner to explain that optimization can replace private inputs with constants, allowing failing inputs to still pass proof verification.

kmerrill18 approved these changes Jul 30, 2026

View reviewed changes

kmerrill18 merged commit 3071bb8 into master Jul 30, 2026

		@@ -0,0 +1,838 @@
		//! The input contract of `ZSharpCurlyFE::eval_test_inputs`: which `@test`

Uh oh!

Conversation

karandeol-26 commented Jul 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

kmerrill18 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kmerrill18 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

karandeol-26 commented Jul 17, 2026 •

edited

Loading