explain how the ghost state for the counter example can be implemented

program_logic/counter_examples.v

@@ -87,6 +87,12 @@ Module inv. Section inv.
   (* We have tokens for a little "two-state STS": [start] -> [finish].
      state. [start] also asserts the exact state; it is only ever owned by the
      invariant.  [finished] is duplicable. *)
+  (* Posssible implementations of these axioms:
+     * Using the STS monoid of a two-state STS, where [start] is the
+       authoritative saying the state is exactly [start], and [finish]
+       is the "we are at least in state [finish]" typically owned by threads.
+     * Ex () +_⊥ ()
+  *)
   Context (gname : Type).
   Context (start finished : gname → iProp).