Fork-local preview only. Not submitted to circify/circ.
Minimal reproducer
Save as main.zok:
def main(private field i, private field x, private bool c) -> field:
field[2] values = [1, 2]
cond_store(values, i, x, c)
return values[0]
Use this input:
The stage comparison at CirC 271f911 is:
| Stage |
return = 1 |
return = 0 |
| Raw source IR |
accepted |
rejected |
After LinearScan |
rejected |
accepted |
| Final R1CS relation |
rejected |
accepted |
Expected
A false conditional store is a no-op. The array remains [1, 2], so the function returns 1.
Actual
The rewritten relation stores 0 into slot zero and returns 0.
Why it happens
The dynamic-index lowering initializes its fold with an unconditional Update(0, ...), then guards only candidate indices 1..N. If c is 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-store at 62bbb92 starts the fold with the untouched tuple and guards every candidate update—including index zero—with index == candidate && condition.
Self-contained regression:
cargo test false_dynamic_conditional_store_preserves_array
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