add token ghost library
In the spirit of providing convenient wrapper around own
, this one provides the simplest of all ghost libraries -- a unique, exclusive token.
In particular, this lets us prove a spinlock without directly using the rather complicated own
.