Skip to content

False dynamic conditional store overwrites slot zero #246

Description

@NullWitnessZK

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:

i = 1
x = 0
c = false

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions