Fork-local preview only. Not submitted to circify/circ.
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
Minimal reproducer
Save as
main.zok:Use
i = 1andv = 99.Expected
The store guard is the literal
false, so the store is dead anda[1]must equal11. A public claimreturn = 99must be rejected.Actual
The finalized relation accepts both:
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_romadmits 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-storeata1a5504rejects 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