fix: preserve arrays on false conditional stores - #249
Draft
NullWitnessZK wants to merge 1 commit into
Draft
Conversation
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
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.
Fixes #246.
Minimal reproducer
Save as
main.zok:Use this input:
The stage comparison at CirC
271f911is:return = 1return = 0LinearScanExpected
A false conditional store is a no-op. The array remains
[1, 2], so the function returns1.Actual
The rewritten relation stores
0into slot zero and returns0.Why it happens
The dynamic-index lowering initializes its fold with an unconditional
Update(0, ...), then guards only candidate indices1..N. Ifcis false, all guarded arms fall through to that slot-zero update.Impact: an unsound verifier relation for a custom witness, plus disagreement with the bundled witness computation. The stock CLI does not directly produce a false proof here: its source-correct precompute conflicts with the malformed constraints.
Proposed fix
fix/linear-scan-conditional-storeat62bbb92starts the fold with the untouched tuple and guards every candidate update—including index zero—withindex == candidate && condition.Self-contained regression:
cargo test false_dynamic_conditional_store_preserves_array