Add library for monotonic nat ghost state

Implemented as an algebra for rules about auth max_natUR and a logic-level wrapper for the auth element (a nat) and fragment (a persistent lower-bound).

Fixes #327 (closed).