Skip to content

fix: reject late writes from covering ROMs - #248

Draft
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/covering-rom-dead-store
Draft

fix: reject late writes from covering ROMs#248
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/covering-rom-dead-store

Conversation

@NullWitnessZK

Copy link
Copy Markdown

Fixes #244.

Minimal reproducer

Save as main.zok:

def main(private field i, private field v) -> field:
    transcript field[4] a = [10, 11, 12, 13]
    cond_store(a, i, v, false)
    return a[i]

Use i = 1 and v = 99.

Expected

The store guard is the literal false, so the store is dead and a[1] must equal 11. A public claim return = 99 must be rejected.

Actual

The finalized relation accepts both:

return = 11  # correct
return = 99  # incorrect, accepted with a custom witness

Debug output identifies a covering ROM with a lookup haystack of five entries: four real initialization writes plus the one dead conditional write.

Why it happens

Ram::is_covering_rom admits a late write when its active flag is false, but the covering-ROM checker does not encode that active flag. It places the dead write's private (i, v) pair into the lookup haystack, allowing it to justify an arbitrary read value.

Impact: transcript-array underconstraint/soundness.

Proposed fix

fix/covering-rom-dead-store at a1a5504 rejects every late access whose write flag is not statically false, regardless of its active flag.

Self-contained regression:

cargo test covering_rom_rejects_inactive_late_write

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Covering-ROM classification admits an inactive late write

1 participant