cli

the zheng command-line face of the legacy proof API. drives five commands from a shell and emits results as a tade chunk stream (the crate tade, imported as tape).

the binary builds only with the cargo feature legacy (cargo run -p zheng-cli --features legacy -- <command>): every command drives the retired folded trace API, which is unsound (soundness § retired). run, demo and prove use the legacy trace statement, not the public execution relation; their reports include verification_scope = legacy_trace_statement and execution_output = unverified. Exit status zero means only that the legacy statement check passed. To prove and verify a public program, input and output, use joy prove / joy verify or the library's profiles (zheng::execution::{certify_execution, verify_certificate}, execution::succinct, zheng::envelope); see execution.

invocation

zheng <command> [args]

output convention — one channel (stdout), two renderings of the same data:

• interactive (stdout is a terminal) — styled ANSI: a gradient banner for help, a titled table with colored status for reports. matches the rune / hemera aesthetic. suppressed by NO_COLOR.
• piped (stdout is not a terminal) — a tade chunk stream (TADE — Typed Annotated Data Exchange); every run ends with a render::STATUS chunk carrying the exit code. zheng ... | <tade reader> is always well-formed.
• exit code — 0 proof verified, 1 prover/verifier error, 2 usage error.

commands

run — check a legacy trace statement

zheng run -e '<formula>' [--object N] [--budget B]

evaluates a nox formula and checks a legacy statement derived from its trace — one process, no intermediate files. This does not bind the public result.

• -e '<formula>' — a nox data formula in bracket syntax ([a b c] → right-nested pairs, atoms are u64 decimals). same grammar as the nox CLI. required.
• --object N — the object noun the formula runs against (atom N). default 0.
• --budget B — focus budget for reduction. default 1_000_000.

emits a render::STRUCT report chunk (see report below) and a status chunk.

aux-free patterns (arithmetic, bitwise, trivial) prove with no auxiliary data. formulas whose trace needs opening proofs (hash pattern 15, axis pattern 0, look pattern 17) require auxiliary data the general path does not yet derive; run reports a prover error for those. demo hash exercises the hash pattern with correctly derived auxiliary data.

demo — run a built-in program

zheng demo hash

runs a known-good program that exercises a specific pattern with correct auxiliary data, then proves and verifies it. hash proves [15 [1 s]] with the HashAux rate derived from the subject's structural digest.

eval — legacy polynomial commitment demo

zheng eval

commits a small multilinear polynomial with the legacy lens opening (Brakedown, code distance unproven), opens it at a point, and verifies the opening via the legacy zheng::open / zheng::verify_eval. reports the point, claimed value, and verify result.

pack — serialize a program capsule

zheng pack -e '<formula>' [--object N] [--budget B] -o <file>

writes the program (formula text, object, budget) to <file> as a single tade chunk (see program file format). does not evaluate or prove.

a nox execution trace cannot round-trip on its own — TraceRow columns are crate-private, so a trace has no public reconstruction path. the program is the canonical serializable unit: re-executing it deterministically reproduces the exact trace, so the capsule stores the program and prove re-runs it.

prove — prove a program capsule

zheng prove <file>

reads a program-capsule tade file, re-executes it to reproduce the trace, proves (aux-free), verifies, and reports. a tampered capsule reduces to a different trace (or fails to parse) — reported as an error, not a false pass.

help

zheng help    |    zheng -h    |    zheng --help

report (STRUCT chunk)

honest, cheaply-measurable proof statistics as nested kv pairs:

proof size in bytes is not reported: Proof::pcs_opening (a lens Opening) has no canonical byte encoding yet. structural counts are reported instead. a .proof file format is reserved for the proof-serialization milestone.

program file format

a single tade chunk, (sigil::BAR, render::STRUCT) (code-with-data), whose payload is encode_nested of three kv pairs:

kv "formula" → text     the bracket-syntax formula
kv "object"  → text     object atom, decimal
kv "budget"  → text     focus budget, decimal

canonical: the kv order is fixed (formula, object, budget) and tade's varint framing is deterministic, so one program encodes to one byte sequence.

deferred

the CLI is retired with the legacy API in phase 5 (soft3 proposals/proof-system-repair.md §5); a CLI over the shipped profiles is joy prove / joy verify. the items below are recorded, not planned:

• offline proof serialization (.proof file, standalone verify <file>) — needs a canonical codec for Proof including the lens Opening (cross-repo).
• raw-trace serialization — blocked on a public TraceRow constructor in nox.
• general auxiliary-data derivation for hash / axis / look formulas under run.
• rich render::TABLE output (current report uses render::STRUCT kv pairs).