feat(verifier): replace panics with error returns#1321
Merged
Conversation
…de-zero invariant - Convert all assert!/assert_eq!/unwrap/expect/unchecked indexing on proof-derived data in the verifier to ZKVMError returns, so a malformed proof is cleanly rejected instead of crashing the process. Covers verify_proofs_halt, verify_proof_validity, verify_chip_proof, TowerVerify::verify, and EccVerifier::verify_ecc_proof. - Add an unconditional public_values.exit_code == 0 check per shard, making "program exited successfully" an explicit verifier-level invariant. On halting shards it is backed by the halt-ecall chip's binding to the a0 register argument; on non-halting shards the verifier enforces it directly so the field cannot carry forged bytes. - Document the verifier's two-statement semantic contract (start at the verifying-key entry PC, exit with code zero) in CLAUDE.md and in a new "What the verifier guarantees" section at the top of docs/src/technical-overview.md. Flag prefix proofs as a dev/bench affordance, not a production verification surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…t/verifier-crypto-contract # Conflicts: # ceno_zkvm/src/scheme/verifier.rs
kunxian-xia
changed the title
The verifier binds public_values.exit_code to register a0 at the halt site via the halt-ecall chip, but does not require any specific value. Guest programs can legitimately halt with non-zero exit codes; callers that want "exited successfully" compare exit_code == 0 themselves. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Prefix / dev-only modes belong in CLAUDE.md (contributor-facing), not in the user-facing mdbook. Also tightens the Halt bullet to the production semantic. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…t/verifier-crypto-contract Conflict in ceno_zkvm/src/scheme/verifier.rs: master's PR #1223 introduced validate_mem_state covering both heap and hint continuation against the new mem_state_verifier; took master's version since it subsumes this branch's heap-only check and already returns ZKVMError rather than panicking, which matches this branch's verifier-error contract.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
A malformed proof could cause the verifier process to crash — any
unwrap/expect/ unchecked indexing /assert!on proof-derived data is a liveness / DoS risk (a crafted proof kills the process instead of being cleanly rejected).Changes
assert!/assert_eq!/unwrap/expect/ unchecked indexing on proof-derived data toZKVMErrorreturns acrossverify_proofs_halt,verify_proof_validity,verify_chip_proof,TowerVerify::verify, andEccVerifier::verify_ecc_proof. A malformed proof is now rejected cleanly in all paths.CLAUDE.mdanddocs/src/technical-overview.md("What the verifier guarantees") state the two program-level facts a valid Ceno proof attests to: execution starts atvk.entry_pcand the terminal shard invokes the halt ecall. The exit code is deliberately not a verifier guarantee —public_values.exit_codeis bound by the halt-ecall chip to registera0, but the guest program defines its own exit-code semantics, so a non-zero value may be a legitimate application signal. Callers that want "exited successfully" compareexit_code == 0themselves.CLAUDE.mdadditionally flags prefix proofs (expect-halt = false) as a dev/bench affordance, not a production surface. This caveat is contributor-facing and is kept out of the user-facing mdbook.Test plan
cargo check --workspace --all-targetscargo make clippy(workspace,-D warnings)cargo test -p ceno_zkvm --lib(152 passed)cargo test -p ceno_zkvm --lib scheme::(18 passed)