#1084 follow up: verifier check on dynamic init table#1223
Open
#1084 follow up: verifier check on dynamic init table#1223
Conversation
…/ceno into feat/dynamic_heap_hint_check
hero78119
commented
Jan 13, 2026
| "HeapTable" | ||
| } | ||
|
|
||
| fn max_len(params: &ProgramParams) -> usize { |
Collaborator
Author
There was a problem hiding this comment.
no logic change, just make function impl order follow trait
| "HintsTable" | ||
| } | ||
|
|
||
| fn max_len(params: &ProgramParams) -> usize { |
Collaborator
Author
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!( |
Collaborator
Author
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
hero78119
commented
Jan 13, 2026
| let chip_proofs = | ||
| builder.get(&zkvm_proof_input.chip_proofs, num_chips_verified.get_var()); | ||
|
|
||
| let chip_proofs_len = chip_proofs.len(); |
Collaborator
Author
There was a problem hiding this comment.
Soundness fix: this logic present in rust verifier but not in recursion verifier
hero78119
commented
Jan 13, 2026
| .then(|builder| { | ||
| builder.assert_usize_eq(chip_proofs_len.clone(), Usize::from(1)); | ||
| }); | ||
| } else if circuit_vk.get_cs().with_omc_init_dyn() { |
Collaborator
Author
There was a problem hiding this comment.
dynamic init table only allow 1 chip proof per shard
hero78119
force-pushed
the
feat/dynamic_heap_hint_check
branch
from
97f5680 to
d87ea19
Compare
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.
To address #1212 (Follow up on #1084)
change highlights
assert_eq(pi[num_instances], pi[mem_length]). Also makenum_instancecould be query from public_values.heap,hintwithinRV32imMemStateConfig, for those terms are tightly couple with riv32im. This design keep the door open to support other ISA.sum_num_instances,log_num_instancefromnum_instances, avoid hint mismatched for malicious manipulationassert_eq!(chip_proofs.len(), 1)assert_eq!(chip_proofs.len(), 0)assert_eq!(chip_proofs.len(), 0 or 1)heapto lower address space to assure "2 * heap.end < Babybear Prime"benchmark
it shows a negligible overhead in
23817600e2e