Struct SpinLockGuard Copy item path

A guard that provides exclusive access to the data protected by a SpinLock.

§Verified Properties

§Verification Design

The guard is extended with a ghost permission field v_perm that holds the ghost permission (PointsTo<T>) This permission grants exclusive ownership of the protected data and enables verified access to the PCell<T>.

§Invariant

The guard maintains a type invariant ensuring that its ghost permission’s ID matches the lock’s internal cell ID. This guarantees that the permission corresponds to the correct protected data.

#[verifier::type_invariant]
   spec fn type_inv(self) -> bool{
       self.lock.cell_id() == self.v_perm@.id()
   }

Note: The invariant is encapsulated using the #[verifier::type_invariant] mechanism. It internally holds at all steps during the method executions and is NOT exposed in the public APIs’ pre- and post-conditions.