IPM proof fails in lib/proof body_release, succeeds in atomics body_release

[andrew-appel]

In vst_on_iris branch, in lib/proof/verif_locks.v, in Lemma body_release, there is a Iris Proof Mode proof that fails:

iInv i as "((% & >p & ?) & Hown)" "Hclose".

The same exact proof succeeds, with apparently the same context, in atomics/verif_lock.v (also in the vst_on_iris branch).

Can someone familiar with IPM fix this one?

[mansky1]

There were two problems here: 1) the definition that was being destructed was declared Opaque, and 2) the Timeless instance for atomic_int_at wasn't declared as an instance. It should work now.