Covering-ROM classification admits an inactive late write

[NullWitnessZK]

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