#1084 follow up: verifier check on dynamic init table#1223
#1084 follow up: verifier check on dynamic init table#1223kunxian-xia merged 16 commits intomasterfrom
Conversation
…/ceno into feat/dynamic_heap_hint_check
| "HeapTable" | ||
| } | ||
|
|
||
| fn max_len(params: &ProgramParams) -> usize { |
There was a problem hiding this comment.
no logic change, just make function impl order follow trait
| "HintsTable" | ||
| } | ||
|
|
||
| fn max_len(params: &ProgramParams) -> usize { |
There was a problem hiding this comment.
no logic change, just make function impl order follow trait
| name_fn: N, | ||
| assert_zero_expr: Expression<E>, | ||
| ) -> Result<(), CircuitBuilderError> { | ||
| assert!( |
There was a problem hiding this comment.
To check assert_eq(public_value[i], public_value[j]) within constrain, both are scalar thus degree is 0
| let chip_proofs = | ||
| builder.get(&zkvm_proof_input.chip_proofs, num_chips_verified.get_var()); | ||
|
|
||
| let chip_proofs_len = chip_proofs.len(); |
There was a problem hiding this comment.
Soundness fix: this logic present in rust verifier but not in recursion verifier
| .then(|builder| { | ||
| builder.assert_usize_eq(chip_proofs_len.clone(), Usize::from(1)); | ||
| }); | ||
| } else if circuit_vk.get_cs().with_omc_init_dyn() { |
There was a problem hiding this comment.
dynamic init table only allow 1 chip proof per shard
97f5680 to
d87ea19
Compare
Resolve the merge by combining PR 1223's memory-layout swap with master's removal of the PUBLIC I/O linker term. Keep the PR's dynamic heap/hint init and shard continuation verification semantics, preserve the ISA-extensible mem-state verifier generic with an RV32 default, and align benches with the current e2e API.
Bring in master changes from PR 1318 for single-shard e2e verification, keep the shard mem-state verification work on this branch, and fix the debug single-shard verifier to derive halt expectation from the selected shard proof rather than the full program exit code. Also take master's ceno-gpu dependency update.
|
Update on the two merge follow-ups now on this PR head (7da2e88):
Net result: this PR is rebased onto current master semantics, keeps the shard continuation / dynamic-init verification work, and now also retains the newer single-shard debug verification flow. |
…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.
Problem
Dynamic heap/hint init tables need verifier-side checks so shard continuation and dynamic-length constraints cannot be bypassed. This PR also needs to stay compatible with current master after the linker/public-io cleanup and the later single-shard debug verification support.
Design Rationale
Keep the memory-state verifier ISA-extensible by carrying RV32-specific heap/hint bounds in RV32imMemStateConfig, while enforcing continuation and dynamic-init checks in the native and recursion verifier paths. Merge on top of master instead of reverting master-only changes.
Change Highlights
Benchmark / Performance Impact
No intended performance change beyond verifier-side checks. Previous measurements on this work showed negligible overhead; no new benchmark run was needed for the merge-only follow-ups.
Benchmark command(s): not rerun for the merge-only follow-ups.
Environment (CPU/GPU, core count, rust toolchain, commit hash): validated on local dev environment at head 7da2e88.
raw data:
Testing
Risks and Rollout
Main risk is verifier semantic drift between full-trace verification and single-shard debug verification. This branch keeps them separate: full-trace verification still owns entry/continuation checks, while single-shard debug verification checks only the selected shard segment.
Follow-ups (optional)
Copilot Reviewer Directive (keep this section)
When Copilot reviews this PR, apply .github/copilot-instructions.md strictly.