Port Invariants from AsyncRaft.tla

[lemmy]

The following invariants have been extracted from Will's AsyncRaft.tla specification, and confirmed to hold for ccfraft.

\* The set of servers that agree up through index.
Agree(i, index) == {i} \cup {k \in Servers : matchIndex[i][k] >= index }

\* If matchIndex on a leader has quorum agreement on an index, then this entry must
\* be present on a quorum of Servers.
H_LeaderMatchIndexValid == 
    \A s \in { s \in Servers : state[s] = Leader} :
        \A ind \in DOMAIN log[s] :
            \E Q \in Quorums[CurrentConfiguration(s)] :
                \A t \in Q :
                    (Agree(s, ind) \in Q ) => 
                         /\ ind \in DOMAIN log[t]
                         /\ log[t][ind] = log[s][ind]

H_CommitIndexCoversEntryImpliesExistsOnQuorum == 
    \A s \in Servers :
        (commitIndex[s] > 0) => 
            \E Q \in Quorums[CurrentConfiguration(s)] :
            \A t \in Q :
                /\ Len(log[s]) >= commitIndex[s] 
                /\ Len(log[t]) >= commitIndex[s] 
                /\ log[t][commitIndex[s]] = log[s][commitIndex[s]]

\* Match index records for a leader must always be <= its own log length.
H_LeaderMatchIndexBound == 
    \A s \in Servers : (state[s] = Leader) => 
        \A t \in Servers : matchIndex[s][t] <= Len(log[s])

\* Commit index is no greater than the log length on any node.
H_CommitIndexBoundValid == 
    \A s \in Servers : commitIndex[s] <= Len(log[s])

H_CurrentTermAtLeastAsLargeAsLogTerms == 
    \A s \in Servers : 
        (\A i \in DOMAIN log[s] : currentTerm[s] >= log[s][i].term)

\* If two nodes are in the same term, then their votes granted
\* sets cannot have intersecting voters.
H_CandidateVotesGrantedInTermAreUnique ==
    \A s,t \in Servers :
        (/\ s # t
         /\ state[s] = Candidate
         /\ state[t] = Candidate
         /\ currentTerm[s] = currentTerm[t]) =>
            (votesGranted[s] \cap votesGranted[t]) = {}

\* If a node has garnered votes in a term as candidate, there must
\* be no other leader in that term in existence.
H_CandidateWithVotesGrantedInTermImplyNoOtherLeader ==
    \A s,t \in Servers :
        (/\ s # t
         /\ state[s] = Candidate
         /\ votesGranted[s] \in Quorums[CurrentConfiguration(s)] 
         /\ currentTerm[s] = currentTerm[t]) =>
            state[t] # Leader

----

INVARIANT
    ...
    H_LeaderMatchIndexValid
    H_CommitIndexCoversEntryImpliesExistsOnQuorum
    H_LeaderMatchIndexBound
    H_CommitIndexBoundValid
    H_CurrentTermAtLeastAsLargeAsLogTerms
    H_CandidateVotesGrantedInTermAreUnique
    H_CandidateWithVotesGrantedInTermImplyNoOtherLeader   

This one looks interesting but doesn't hold:

\* If a commit index covers a log entry in some term,
\* then no primary in an earlier term can be enabled to commit any entries
\* in its own log.
H_CommitIndexAtEntryInTermDisabledEarlierCommits == 
    \A s,t \in Servers :
        (/\ s # t 
         /\ commitIndex[s] > 0
         /\ state[t] = Leader
         /\ currentTerm[t] < log[s][commitIndex[s]].term) =>
                \A ind \in DOMAIN log[t] : 
                    Agree(t, ind) \notin Quorums[CurrentConfiguration(s)]