Add history variable to the cluster state machine

[marshtompsxd]

This PR augments the cluster state machine with a history that records all the past global state of the cluster. The history will help us prove some invariants that involve resource version of state objects.

Instead of modifying the cluster state machine's definition (and all its references) to maintain the history, this PR adds a new state machine, called retentive cluster, that wraps up the original state machine's init and next and meanwhile maintains a history of the original state machine. This brings several benefits: (1) it minimizes the changes we need to make to the current spec and lemmas (in fact, no changes are needed) to use the history variable, (2) it allows us to stick with the original state machine (w/o the history) in the cases where we don't need to use the history variable just like what we are doing.

It is obvious that any invariant on the cluster state (not the history) can be transferred between the two state machines because they are identical except the history recording. To transfer invariants, this PR also introduces two lemmas transfer_invariant_to_cluster and transfer_invariant_from_cluster.