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.