Update consensus protocol spec (#9607)

The spec was written for the buggy protocol which we had before the one
more similar to Raft was implemented. Update the spec with what we
currently have.

ref #8699

safekeeper/spec/.gitignore

@@ -0,0 +1,3 @@
+*TTrace*
+*.toolbox/
+states/

safekeeper/spec/MCProposerAcceptorStatic.tla

@@ -0,0 +1,31 @@
+---- MODULE MCProposerAcceptorStatic ----
+EXTENDS TLC, ProposerAcceptorStatic
+
+\* Augments the spec with model checking constraints.
+
+\* For model checking.
+CONSTANTS
+  max_entries, \* model constraint: max log entries acceptor/proposer can hold
+  max_term \* model constraint: max allowed term
+
+ASSUME max_entries \in Nat /\ max_term \in Nat
+
+\* Model space constraint.
+StateConstraint == \A p \in proposers:
+                    /\ prop_state[p].term <= max_term
+                    /\ Len(prop_state[p].wal) <= max_entries
+\* Sets of proposers and acceptors are symmetric because we don't take any
+\* actions depending on some concrete proposer/acceptor (like IF p = p1 THEN
+\* ...)
+ProposerAcceptorSymmetry == Permutations(proposers) \union Permutations(acceptors)
+
+\* enforce order of the vars in the error trace with ALIAS
+\* Note that ALIAS is supported only since version 1.8.0 which is pre-release
+\* as of writing this.
+Alias == [
+           prop_state |-> prop_state,
+           acc_state |-> acc_state,
+           committed |-> committed
+         ]
+
+====