diff --git a/Cargo.toml b/Cargo.toml
index 3910d00c..1da16315 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -138,5 +138,17 @@ required-features = ["lp", "aby"]
 name = "r1cs_inspect"
 required-features = ["r1cs"]
 
+[[example]]
+name = "ztest"
+required-features = ["smt", "zokc", "bellman"]
+
+[[test]]
+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/ZoKratesCurly/pf/coverage_test.zok b/examples/ZoKratesCurly/pf/coverage_test.zok
new file mode 100644
index 00000000..cae4e21f
--- /dev/null
+++ b/examples/ZoKratesCurly/pf/coverage_test.zok
@@ -0,0 +1,99 @@
+// Simple @test coverage: backend selection, scalar, array, and tuple inputs,
+// and private/public visibility. All tests pass. Run:
+//   cargo run --example ztest --features zokc -- examples/ZoKratesCurly/pf/coverage_test.zok
+
+// ---- scalar inputs ----
+
+@test x = 5;
+def test_field(private field x) {
+    assert(x == 5);
+}
+
+@test(backend = mirage) a = 4, b = 6;
+def test_add(private field a, private field b) {
+    assert(a + b == 10);
+}
+
+@test b = true;
+def test_bool(private bool b) {
+    assert(b);
+}
+
+@test x = 7u32;
+def test_u32(private u32 x) {
+    assert(x * 2 == 14u32);
+}
+
+// ---- scalar visibility corners ----
+
+@test a = 3, b = 4;
+def test_all_public(public field a, public field b) {
+    assert(a + b == 7);
+}
+
+@test a = 3, b = 4;
+def test_mixed_visibility(private field a, public field b) {
+    assert(a + b == 7);
+}
+
+// ---- array inputs ----
+
+@test xs = [1, 2, 3];
+def test_array(private field[3] xs) {
+    assert(xs[0] + xs[1] == xs[2]);
+}
+
+@test A = [[1, 2], [3, 4]];
+def test_nested_array(private field[2][2] A) {
+    assert(A[0][0] == 1);
+    assert(A[1][1] == 4);
+}
+
+@test xs = [1, 2];
+def test_public_array(public field[2] xs) {
+    assert(xs[0] + xs[1] == 3);
+}
+
+// ---- array + scalar together ----
+
+@test k = 10, xs = [1, 2];
+def test_array_and_scalar(private field k, public field[2] xs) {
+    assert(k + xs[0] == 11);
+    assert(k + xs[1] == 12);
+}
+
+// ---- tuple inputs ----
+
+@test t = (4, true);
+def test_tuple(private (field, bool) t) {
+    assert(t.0 == 4);
+    assert(t.1);
+}
+
+// A singleton tuple needs the trailing comma: (5,) is a 1-tuple, (5) is
+// just a parenthesized expression.
+@test t = (5,);
+def test_singleton_tuple(private (field,) t) {
+    assert(t.0 == 5);
+}
+
+@test t = ([1, 2], (true, 3));
+def test_nested_tuple(private (field[2], (bool, u32)) t) {
+    assert(t.0[0] + t.0[1] == 3);
+    assert(t.1.0);
+    assert(t.1.1 == 3u32);
+}
+
+@test pairs = [(1, 2), (3, 4)];
+def test_array_of_tuples(private (field, u32)[2] pairs) {
+    assert(pairs[0].0 == 1);
+    assert(pairs[0].1 == 2u32);
+    assert(pairs[1].0 == 3);
+    assert(pairs[1].1 == 4u32);
+}
+
+@test t = (7, 9);
+def test_public_tuple(public (field, u32) t) {
+    assert(t.0 == 7);
+    assert(t.1 == 9u32);
+}
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/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
new file mode 100644
index 00000000..6ed198b0
--- /dev/null
+++ b/examples/ztest.rs
@@ -0,0 +1,167 @@
+//! Unit-test runner for ZoKratesCurly programs.
+//! Reads a .zok file, finds every function marked with a @test annotation,
+//! evaluates its annotation inputs to concrete values, then runs each test
+//! through the full in-memory proof pipeline:
+//!   compile (test fn as entry point) -> assert check -> setup -> prove -> verify
+//! and prints ok / FAILED per test. A test passes when its assertions hold for
+//! the supplied inputs and its proof verifies. Assertions are evaluated
+//! directly on the unoptimized IR before proof generation. Tests use
+//! Groth16 by default and may select Mirage in the annotation.
+//!
+//! The per-test execution logic lives in [`circ::test_runner`]; this file is
+//! the CLI wrapper.
+use bls12_381::Bls12;
+use circ::cfg::{clap, CircOpt};
+use circ::front::zsharpcurly::{TestBackend, ZSharpCurlyFE};
+use circ::front::Mode;
+use circ::ir::term::Value;
+use circ::target::r1cs::{bellman::Bellman, mirage::Mirage};
+use circ::test_runner::{catch, run_test, Outcome};
+use clap::Parser;
+use std::path::PathBuf;
+
+#[derive(Debug, Parser)]
+#[command(
+    name = "ztest",
+    about = "Run @test functions in a ZoKratesCurly program"
+)]
+struct Options {
+    /// Input file
+    #[arg(name = "PATH")]
+    path: PathBuf,
+
+    #[command(flatten)]
+    circ: CircOpt,
+}
+
+/// Render a concrete Value as a plain number/bool, without the field
+/// modulus that Value's own Display appends (e.g. `9` instead of `#f9m524...`).
+fn pretty_value(v: &Value) -> String {
+    match v {
+        Value::Field(f) => f.i().to_string(),
+        Value::BitVector(b) => b.uint().to_string(),
+        Value::Bool(b) => b.to_string(),
+        Value::Array(a) => format!(
+            "[{}]",
+            a.values()
+                .iter()
+                .map(pretty_value)
+                .collect::<Vec<_>>()
+                .join(", ")
+        ),
+        // Singletons print as `(5,)` — the trailing comma matches how they
+        // must be written in source.
+        Value::Tuple(vs) if vs.len() == 1 => format!("({},)", pretty_value(&vs[0])),
+        Value::Tuple(vs) => format!(
+            "({})",
+            vs.iter().map(pretty_value).collect::<Vec<_>>().join(", ")
+        ),
+        // Anything else (structs, ...): fall back to the default form.
+        other => other.to_string(),
+    }
+}
+
+fn main() {
+    env_logger::Builder::from_default_env()
+        .format_level(false)
+        .format_timestamp(None)
+        .init();
+
+    let options = Options::parse();
+    circ::cfg::set(&options.circ);
+
+    // The frontend panics on a missing file with an unhelpful unwrap
+    // message; check up front so the user gets a plain answer.
+    if !options.path.exists() {
+        eprintln!("Error: file not found: {}", options.path.display());
+        std::process::exit(1);
+    }
+
+    // Find every @test function and evaluate its annotation inputs to
+    // concrete values. Parse errors surface as panics, evaluation errors
+    // through the Result.
+    let tests = match catch(|| ZSharpCurlyFE::eval_test_inputs(options.path.clone(), Mode::Proof)) {
+        Ok(Ok(tests)) => tests,
+        Ok(Err(e)) | Err(e) => {
+            eprintln!("Error: {}", e);
+            std::process::exit(1);
+        }
+    };
+
+    println!(
+        "running {} test{} from {}",
+        tests.len(),
+        if tests.len() == 1 { "" } else { "s" },
+        options.path.display()
+    );
+
+    let (mut passed, mut failed, mut errored) = (0, 0, 0);
+    for t in &tests {
+        // Show each input as `name = <source> = <value>`, collapsing to
+        // `name = <value>` when the source is already just the value.
+        let inputs: Vec<String> = t
+            .inputs()
+            .iter()
+            .map(|input| {
+                let value = pretty_value(input.value());
+                if input.source() == value {
+                    format!("{} = {}", input.name(), value)
+                } else {
+                    format!("{} = {} = {}", input.name(), input.source(), value)
+                }
+            })
+            .collect();
+        print!(
+            "test {} [{}] ({}) ... ",
+            t.name(),
+            t.settings().backend(),
+            inputs.join(", ")
+        );
+        // Flush so the prover's own stderr diagnostics (printed when a
+        // constraint fails) appear under this test's line, not before it.
+        use std::io::Write;
+        let _ = std::io::stdout().flush();
+
+        let indent = |msg: String| {
+            // The prover's message spans several lines; indent them all.
+            for line in msg.lines() {
+                println!("    {}", line);
+            }
+        };
+        let outcome = match t.settings().backend() {
+            TestBackend::Groth16 => run_test::<Bellman<Bls12>>(t),
+            TestBackend::Mirage => run_test::<Mirage<Bls12>>(t),
+        };
+        match outcome {
+            Outcome::Pass => {
+                passed += 1;
+                println!("ok");
+            }
+            Outcome::AssertionFailed(msg) => {
+                failed += 1;
+                println!("FAILED");
+                indent(msg);
+            }
+            Outcome::CompileError(msg) | Outcome::BackendError(msg) => {
+                errored += 1;
+                println!("error");
+                indent(msg);
+            }
+        }
+    }
+
+    println!(
+        "\ntest result: {}. {} passed; {} failed; {} errored",
+        if failed == 0 && errored == 0 {
+            "ok"
+        } else {
+            "FAILED"
+        },
+        passed,
+        failed,
+        errored
+    );
+    if failed > 0 || errored > 0 {
+        std::process::exit(1);
+    }
+}
diff --git a/src/compile.rs b/src/compile.rs
index 3a77e1bb..3266d1a6 100644
--- a/src/compile.rs
+++ b/src/compile.rs
@@ -4,11 +4,50 @@
 //! [`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};
 
+/// Runs the proof-mode optimizations shared by the CLI and test runner.
+///
+/// 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([])),
+        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..06d2462f 100644
--- a/src/front/zsharpcurly/interp.rs
+++ b/src/front/zsharpcurly/interp.rs
@@ -53,3 +53,40 @@ pub fn extract(
         )),
     }
 }
+
+/// 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 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]`.
+///
+/// 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
+            .values()
+            .into_iter()
+            .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!(
+            "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 6108aab6..034b5407 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;
@@ -39,6 +39,122 @@ 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 {
+    /// 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
+/// must evaluate to a constant. Return-typed tests are rejected before a
+/// `TestCase` is created.
+///
+/// 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,
+    settings: TestSettings,
+    inputs: Vec<TestCaseInput>,
+    /// 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 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
+    }
+    /// 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 supported scalar, array, or tuple.
+#[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 fn name(&self) -> &str {
+        &self.name
+    }
+    /// Whether the input is public. Parameters without a visibility keyword
+    /// are public by default.
+    pub fn public(&self) -> bool {
+        self.public
+    }
+    /// The input expression exactly as written in the source (`3 * 3`).
+    pub fn source(&self) -> &str {
+        &self.source
+    }
+    /// 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 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)
+    }
+}
+
 #[allow(dead_code)]
 fn const_value_simple(term: &Term) -> Option<Value> {
     match term.op() {
@@ -113,7 +229,288 @@ impl ZSharpCurlyFE {
         g.file_stack_push(file);
         g.generics_stack_push(HashMap::new());
         g.const_entry_fn(&entry, input_scalar_values)
+    }
+
+    /// 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, 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.
+    pub fn eval_test_inputs(file: PathBuf, mode: Mode) -> Result<Vec<TestCase>, 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)
+    }
+}
+
+/// 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_supported_test_input_type(elem),
+        Ty::Tuple(elements) => elements.iter().all(is_supported_test_input_type),
+        Ty::MutArray(_) | Ty::Struct(..) => false,
+    }
+}
+
+/// Returns true if an array or tuple input contains no values.
+///
+/// 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_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
+        }
+    }
 }
+
+/// 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<TestCase, String> {
+    let diag = |msg: String, span: &ast::Span| {
+        format!(
+            "{}\nIn {}:\n  {}",
+            msg,
+            file.display(),
+            span_to_string(span)
+        )
+    };
+
+    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() {
+        return Err(diag(
+            format!("@test function {} cannot be generic", f.id.value),
+            &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.
+    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_::<true>(&p.ty)
+            .map_err(|e| diag(e, type_span(&p.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), arrays, and tuples \
+                     composed of those types are supported",
+                    p.id.value, f.id.value, ty
+                ),
+                &p.span,
+            ));
+        }
+        if has_empty_test_input(&ty) {
+            return Err(diag(
+                format!(
+                    "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,
+            ));
+        }
+
+        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_::<true>(&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(),
+        settings,
+        inputs,
+        file: file.to_path_buf(),
+    })
 }
 
 struct ZGen<'ast> {
diff --git a/src/front/zsharpcurly/zvisit/walkfns.rs b/src/front/zsharpcurly/zvisit/walkfns.rs
index 2ecc8bec..c514c102 100644
--- a/src/front/zsharpcurly/zvisit/walkfns.rs
+++ b/src/front/zsharpcurly/zvisit/walkfns.rs
@@ -157,6 +157,10 @@ pub fn walk_function_definition<'ast, Z: ZVisitorMut<'ast>>(
     visitor: &mut Z,
     fundef: &mut ast::FunctionDefinition<'ast>,
 ) -> ZVisitorResult {
+    // Visit the @test annotation when the function has one.
+    if let Some(t) = fundef.test.as_mut() {
+        visitor.visit_test_annotation(t)?;
+    }
     visitor.visit_identifier_expression(&mut fundef.id)?;
     fundef
         .generics
@@ -176,6 +180,39 @@ 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
+        .settings
+        .iter_mut()
+        .try_for_each(|s| visitor.visit_test_setting(s))?;
+    testann
+        .inputs
+        .iter_mut()
+        .try_for_each(|i| visitor.visit_test_input(i))?;
+    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>,
+) -> 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/zconstlitrw.rs b/src/front/zsharpcurly/zvisit/zconstlitrw.rs
index 332b62a7..dcfb95a9 100644
--- a/src/front/zsharpcurly/zvisit/zconstlitrw.rs
+++ b/src/front/zsharpcurly/zvisit/zconstlitrw.rs
@@ -266,6 +266,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 +319,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; 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(),
+                )
+            }
         }
-        //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/front/zsharpcurly/zvisit/zvmut.rs b/src/front/zsharpcurly/zvisit/zvmut.rs
index 6ec2a08e..4bb33085 100644
--- a/src/front/zsharpcurly/zvisit/zvmut.rs
+++ b/src/front/zsharpcurly/zvisit/zvmut.rs
@@ -101,6 +101,18 @@ 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_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)
+    }
+
     fn visit_parameter(&mut self, param: &mut ast::Parameter<'ast>) -> ZVisitorResult {
         walk_parameter(self, param)
     }
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/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<E: Engine>(PhantomData<E>);
 
 /// The pk for [mirage]
diff --git a/src/test_runner/mod.rs b/src/test_runner/mod.rs
new file mode 100644
index 00000000..89d6bfa4
--- /dev/null
+++ b/src/test_runner/mod.rs
@@ -0,0 +1,172 @@
+//! Runs a ZoKrates `@test` through compilation, assertion checking, setup,
+//! proving, and verification.
+//!
+//! The runner is generic over [`ProofSystem`]. Bellman and Mirage implement
+//! 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};
+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;
+
+/// Result of running one test.
+///
+/// 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),
+    /// Frontend compilation, optimization, or R1CS lowering failed.
+    CompileError(String),
+    /// Proof setup, proving, or verification failed.
+    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<bool> = const { Cell::new(false) };
+}
+
+static HOOK_INIT: Once = Once::new();
+
+/// 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();
+        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. 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).
+///
+/// Public because discovery can panic too ([`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<R>(f: impl FnOnce() -> R) -> Result<R, String> {
+    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::<String>() {
+            msg.clone()
+        } else if let Some(msg) = e.downcast_ref::<&str>() {
+            (*msg).to_string()
+        } else {
+            "unknown panic".to_string()
+        }
+    })
+}
+
+/// 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 and compiler options for the process.
+pub fn run_test<PS: ProofSystem>(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.
+    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),
+    };
+
+    // Give the prover all inputs and the verifier only public inputs.
+    let mut prover_map: FxHashMap<String, Value> = FxHashMap::default();
+    let mut verifier_map: FxHashMap<String, Value> = 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);
+    }
+
+    //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())
+            .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),
+    };
+
+    // 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,
+        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".to_string()),
+        Err(e) => Outcome::BackendError(e),
+    }
+}
diff --git a/tests/zok_test_inputs.rs b/tests/zok_test_inputs.rs
new file mode 100644
index 00000000..d076b556
--- /dev/null
+++ b/tests/zok_test_inputs.rs
@@ -0,0 +1,1118 @@
+//! 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::{TestBackend, 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<Vec<TestCase>, 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),
+    }
+}
+
+/// Unwrap a Value::Array into its element Values, in index order.
+fn array_values(v: &Value) -> Vec<Value> {
+    match v {
+        Value::Array(a) => a.values(),
+        other => panic!("expected array, got {:?}", other),
+    }
+}
+
+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);
+    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<Vec<TestCase>, 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(
+        "constant_arithmetic",
+        r#"@test y = 3 * 3;
+def test_sq(private field y) {
+    assert(y == 9);
+}
+"#,
+    )
+    .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) {
+    assert(x == 8);
+}
+"#,
+    )
+    .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) {
+    assert(y == 9);
+}
+"#,
+    )
+    .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) {
+    assert(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) {
+    assert(x == 2u32);
+}
+"#,
+    )
+    .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() {
+    assert(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) {
+    assert(x == 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) {
+    assert(a == 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) {
+    assert(a == 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) {
+    assert(a == 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) {
+    assert(x == x);
+}
+"#,
+    )
+    .unwrap_err();
+    assert!(err.contains("undefined_thing"), "{}", err);
+}
+
+#[test]
+fn array_parameter_accepted() {
+    let tests = eval(
+        "array_param",
+        r#"@test xs = [1, 2];
+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, and tuples"), "{}", err);
+}
+
+#[test]
+fn mixed_scalar_tuple_accepted() {
+    let tests = eval(
+        "tuple_param",
+        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("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_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);
+def test_paren(private (field,) t) {
+    assert(t.0 == 4);
+}
+"#,
+    )
+    .unwrap_err();
+    assert!(err.contains("incompatible type"), "{}", err);
+}
+
+#[test]
+fn array_of_struct_rejected() {
+    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("empty array or tuple"), "{}", 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("Empty array"), "{}", 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) {
+    assert(x == 2u32);
+}
+"#,
+    )
+    .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<N>(private field x) {
+    assert(x == 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) {
+    assert(x == 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) {
+    assert(a == 1);
+}
+"#,
+    )
+    .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 return_typed_test_rejected() {
+    let err = eval(
+        "return_typed",
+        r#"@test y = 2;
+def test_return_style(private field y) -> field {
+    return y;
+}
+"#,
+    )
+    .unwrap_err();
+    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(
+        "plain_skipped",
+        r#"def helper(field n) -> field {
+    return n + 1;
+}
+
+@test x = 1;
+def test_only(private field x) {
+    assert(x == 1);
+}
+"#,
+    )
+    .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/tests/ztest_e2e.rs b/tests/ztest_e2e.rs
new file mode 100644
index 00000000..2862441a
--- /dev/null
+++ b/tests/ztest_e2e.rs
@@ -0,0 +1,396 @@
+//! 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
+//! optimization, R1CS lowering, setup, proving, and verification. They check
+//! the structured [`Outcome`] rather than CLI output.
+
+#![cfg(all(feature = "smt", feature = "zokc", feature = "bellman"))]
+
+use bls12_381::Bls12;
+use circ::front::zsharpcurly::{TestBackend, TestCase, ZSharpCurlyFE};
+use circ::front::Mode;
+use circ::target::r1cs::{bellman::Bellman, mirage::Mirage};
+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<TestCase> {
+    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::<Bellman<Bls12>>(test),
+        TestBackend::Mirage => run_test::<Mirage<Bls12>>(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_selected(&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 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(
+        "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.
+    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::<Bellman<Bls12>>(&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 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;
+
+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));
+}
+"#,
+    );
+    assert!(matches!(outcome, Outcome::Pass), "got {:?}", outcome);
+}
+
+#[test]
+fn chall_circuit_on_groth16_is_backend_error() {
+    // 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;
+
+@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
+    );
+}
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 df5339f4..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<TestSetting<'ast>>,
         pub inputs: Vec<TestInput<'ast>>,
         #[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,4 +1659,50 @@ 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:
+        // 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(_)));
+    }
 }