I have made a start of attacking this challenge with VeriFast. So far, I have written (safety) specs for intrinsics::{atomic_store_relaxed, atomic_store_release, atomic_store_seqcst} and verified atomic_store, AtomicBool::from_ptr, and AtomicBool::store, using this type interpretation for AtomicBool. As far as I can tell, the other atomic types will be extremely similar. (In fact, they will be simpler because AtomicBool is the only type that involves a nontrivial invariant (saying that the internal u8 is either 0 or 1).) The main difficulty that I see is dealing with the fact that the atomic integer types are generated using a macro.

But maybe I'm missing something. A few things in the challenge confused me:

The challenge asks to "verify" the intrinsics. What do you mean by that?
The challenge asks to verify that atomic_store does not panic. But this seems to contradict the statement at the top that "The goal of this challenge is to verify that these methods are safe. [1]", where [1] says that "safe" means absence of UB. Panicking is not UB. VeriFast does not verify absence of panics, and adding a precondition to AtomicBool::store would run counter to the goal of verifying semantic well-typedness, i.e. safety in the presence of arbitrary non-unsafe client code.

Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics #83

Description