Closed mjp41 closed 1 year ago
FYI @septract, @mattwindsor91, @bensimner, I have updated the starling proof of the Verona reference counting mechanism. I think it is slightly clearer now.
I pushed a second version that uses an auxiliary variable to enforce that destruction happens before deallocation: docs/internal/verona_rc_wrc_aux.cvf
Added explicit state for destruction and deallocation of the underlying object. This simplified a few of the structures to make it clearer when things happen.
It still has some deficiencies around not being able to guarantee the destructor was called before it was deallocated.