Refactor abstract consensus specification

[lemmy]

• Refactor (simplify) TypeOK to use (more concise) Sequences!Seq operator.
• Define InitialLogs less explicitly.
• Add assumptions about abs.tla's constants (TLAPS will likely need those assumptions should we attempt writing a proof).
• Mitigate state-space explosion during explicit-state model checking by declaring constant Servers to be symmetric.

[achamayou]

@lemmy could you add a short description to the PR capture its goal(s)? The overall impression I get from the commit is that this is trying to simplify things, but it adds a net 34 lines.

[lemmy]

@lemmy could you add a short description to the PR capture its goal(s)? The overall impression I get from the commit is that this is trying to simplify things, but it adds a net 34 lines.

• Align spec with CCF by replacing global upper bound MaxLogLength with MaxUncommittedCount (see max_uncommitted_tx_count in raft.h) that restricts the length by which a log may be extended in each step.

• Move refinement mapping from TLC-specific module into ccfraft. Clearly, refinement mapping belongs in ccfraft, but we couldn't do that up until recently because of a limitation in TLC)

• Refactor (simplify) TypeOK to use (more concise) Sequences!Seq operator.

• Define InitialLogs less explicitly.

• Add assumptions about abs.tla's constants (TLAPS will likely need those assumptions should we attempt writing a proof).

• Mitigate state-space explosion during explicit-state model checking by declaring constant Servers to be symmetric.

• Limit the global length of all logs to 7 during model checking (maintains the checked state space).

I propose not to squash the commits.

[heidihoward]

I'm good for this to be merged once the ci is green.

I would suggest double checking the impact of refinement checking on the ci times for consensus with reconfiguration once its finishing properly

[lemmy]

I'm good for this to be merged once the ci is green.

I would suggest double checking the impact of refinement checking on the ci times for consensus with reconfiguration once its finishing properly

I removed all commits with semantic changes from this PR. Will continue with those in a separate PR, after this has moved through the merge queue.