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

PrincetonUniversity / VST

Verified Software Toolchain

https://vst.cs.princeton.edu

Other

424 stars 91 forks source link

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

Open andrew-appel opened 2 months ago

andrew-appel commented 2 months ago

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 commented 2 months ago

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.