Expand-errors blames incorrect conjunct

[jaylorch]

In the attached recording, the "expand errors" report blames two failing quantified conjuncts, below. But only the second one is a problem; there's nothing wrong with the first conjunct. And indeed if you restore the commented-out part of the proof at the end of kv::lemma_volatile_matches_durable_after_create, you find that fixing the second conjunct is sufficient to fix the verification.

          |   forall |k|
          |       new_volatile_index.contains_key(k) ==>
          |           let indexed_offset = new_volatile_index.spec_index(k).0.header_addr;
          |               new_durable_state.contains_key(indexed_offset) ✘
          |               |   new_durable_state.spec_index(indexed_offset) is Some 
          |               +---
          |               new_durable_state.spec_index(indexed_offset).0.key == k ✘
          |   forall |i|
          |       new_durable_state.contains_key(i) ==>
          |           new_volatile_index.contains_key(new_durable_state.spec_index(i).0.key) ✘
          |           |   new_volatile_index.spec_index(new_durable_state.spec_index(i).0.key) is Some 
          |           +---
          |           new_volatile_index.spec_index(new_durable_state.spec_index(i).0.key).0.header_addr == i ✘

2024-07-11-11-44-44.zip

[tjhance]

this may have been fixed by d56fd23