Add Extended System-Level TLA+ Specification for Raft Core Module

tla/extended_spec/MCetcdraft.cfg

@@ -0,0 +1,240 @@
+SPECIFICATION mc_etcdSpec
+
+CONSTANTS
+    s1 = s1
+    s2 = s2
+    s3 = s3
+    s4 = s4
+    s5 = s5
+    s6 = s6
+
+    InitServer  = {s1, s2}
+    Server      = {s1, s2, s3, s4}
+
+    v1 = v1
+    v2 = v2
+    v3 = v3
+    Value       = {v1, v2}
+
+    \* Constraint limits - tuned for tractable state space
+    ReconfigurationLimit    = 2
+    MaxTermLimit            = 4
+    MaxTimeoutLimit         = 6
+    RequestLimit            = 6
+
+    \* Fault injection limits
+    RestartLimit            = 1
+    DropLimit               = 4
+    DuplicateLimit          = 0
+    StepDownLimit           = 2
+    HeartbeatLimit          = 8
+
+    \* Snapshot limits
+    SnapshotLimit           = 2
+    CompactLimit            = 2
+
+    \* Config change limits
+    ConfChangeLimit         = 2
+
+    \* ReportUnreachable limit
+    ReportUnreachableLimit  = 1
+
+    \* Flow control
+    MaxInflightMsgs         = 4
+
+    \* FIFO message ordering - when TRUE, enforces FIFO delivery per (source, dest) pair
+    MsgNoReorder            = FALSE
+
+    \* Network partition configuration
+    MaxPartitions           = 2     \* Maximum number of partition groups (2 = split into 2 groups)
+    RestartDropsMessages    = FALSE \* When TRUE, Restart drops all messages to/from the node
+    PartitionLimit          = 0     \* Maximum number of partition/heal cycles
+
+    \* DisableConfChangeValidation - when TRUE, allows proposing LeaveJoint before
+    \* EnterJoint is applied. This is dangerous and can violate QuorumLogInv.
+    \* Reference: raft.go:258-278
+    DisableConfChangeValidation = FALSE
+
+    \* Message buffer limit for state space pruning
+    MaxMsgBufferLimit       = 12
+
+    \* Pending messages buffer limit for state space pruning
+    MaxPendingMsgLimit      = 12
+
+    \* Action overrides
+    Timeout             <- MCTimeout
+    Send                <- MCSend
+    ClientRequest       <- MCClientRequest
+    ClientRequestAndSend <- MCClientRequestAndSend
+    AddNewServer        <- MCAddNewServer
+    DeleteServer        <- MCDeleteServer
+    AddLearner          <- MCAddLearner
+    Restart             <- MCRestart
+    DropMessage         <- MCDropMessage
+    DuplicateMessage    <- MCDuplicateMessage
+    StepDownToFollower  <- MCStepDown
+    Heartbeat           <- MCHeartbeat
+    SendSnapshot        <- MCSendSnapshot
+    CompactLog          <- MCCompactLog
+    ChangeConf          <- MCChangeConf
+    ChangeConfAndSend   <- MCChangeConfAndSend
+    ManualSendSnapshot  <- MCManualSendSnapshot
+    SendSnapshotWithCompaction <- MCSendSnapshotWithCompaction
+    ReportUnreachable   <- MCReportUnreachable
+
+    \* Initialization overrides
+    InitServerVars  <- etcdInitServerVars
+    InitLogVars     <- etcdInitLogVars
+    InitConfigVars  <- etcdInitConfigVars
+    InitDurableState <- etcdInitDurableState
+
+    \* Type constants
+    Nil = Nil
+
+    ValueEntry  = ValueEntry
+    ConfigEntry = ConfigEntry
+
+    Follower    = Follower
+    Candidate   = Candidate
+    Leader      = Leader
+
+    RequestVoteRequest      = RequestVoteRequest
+    RequestVoteResponse     = RequestVoteResponse
+    AppendEntriesRequest    = AppendEntriesRequest
+    AppendEntriesResponse   = AppendEntriesResponse
+    SnapshotRequest         = SnapshotRequest
+    SnapshotResponse        = SnapshotResponse
+
+    StateProbe      = StateProbe
+    StateReplicate  = StateReplicate
+    StateSnapshot   = StateSnapshot
+
+SYMMETRY Symmetry
+\* VIEW ModelView
+
+CHECK_DEADLOCK
+    FALSE
+
+\* Constraints
+CONSTRAINT
+    MsgBufferConstraint
+    PendingMsgBufferConstraint
+
+\* Core Raft Safety
+INVARIANTS
+    LogInv
+    MoreThanOneLeaderInv
+    LogMatchingInv
+    QuorumLogInv
+    MoreUpToDateCorrectInv
+    LeaderCompletenessInv
+    CommittedIsDurableInv
+    AppliedBoundInv
+    MessageDestinationValidInv
+
+\* Progress and Inflights
+INVARIANTS
+    ProbeLimitInv
+    ProbeNetworkMessageLimitInv
+    ReplicatePauseInv
+    SnapshotInflightsInv
+    InflightsLogIndexInv
+    InflightsMatchIndexInv
+    InflightsMonotonicInv
+    ProgressStateTypeInv
+    InflightsInv
+    SnapshotPendingInv
+    NoPendingSnapshotInv
+    LeaderSelfReplicateInv
+    SnapshotStateInv
+    MatchIndexLessThanLogInv
+    MatchIndexNonNegativeInv
+    InflightsAboveMatchInv
+    MatchIndexLessThanNextInv
+    MsgAppFlowPausedConsistencyInv
+    ProbeOneInflightMaxInv
+    SnapshotNoInflightsStrictInv
+    NextIndexPositiveInv
+    NextIndexBoundInv
+    MatchIndexBoundInv
+    PendingSnapshotBoundInv
+    InflightsOnlyInReplicateInv
+    InflightsBelowNextInv
+
+\* Log Structure
+INVARIANTS
+    LogOffsetMinInv
+    SnapshotOffsetConsistencyInv
+    SnapshotTermValidInv
+    SnapshotTermBoundInv
+    HistoryLogLengthInv
+    SnapshotCommitConsistencyInv
+
+\* Configuration
+INVARIANTS
+    JointConfigNonEmptyInv
+    SingleConfigOutgoingEmptyInv
+    LearnersVotersDisjointInv
+    ConfigNonEmptyInv
+    PendingConfIndexValidInv
+    AppliedConfigBoundInv
+
+\* Message Content
+INVARIANTS
+    SnapshotMsgIndexValidInv
+    SnapshotMsgTermValidInv
+    AppendEntriesPrevIndexNonNegInv
+    AppendEntriesCommitBoundInv
+    VoteRequestLogIndexNonNegInv
+    VoteRequestLogTermNonNegInv
+    AppendEntriesTermConsistentInv
+    SnapshotMsgIndexPositiveInv
+    ResponseTermPositiveInv
+
+\* Additional Safety
+INVARIANTS
+    AllMessageTermsValid
+    MessageIndexValidInv
+    StateMachineConsistency
+    CommitIndexBoundInv
+    LogTermMonotonic
+    CommittedEntriesTermInv
+    PendingConfigBoundInv
+    LeaderLogLengthInv
+    CurrentTermAtLeastLogTerm
+    CandidateVotedForSelfInv
+    DurableStateConsistency
+    MessageEndpointsValidInv
+    LeaderDurableTermInv
+
+\* Term and Vote
+INVARIANTS
+    TermPositiveInv
+    LeaderTermPositiveInv
+    CandidateTermPositiveInv
+    \*VotesRespondedSubsetInv
+    VotesGrantedSubsetInv
+
+\* Bug Detection
+INVARIANTS
+    AppendEntriesPrevLogTermValidInv
+    SinglePendingLeaveJointInv
+    PendingConfIndexAutoLeaveInv
+    TermNeverZeroInLogInv
+
+\* Verdi-Raft Inspired
+INVARIANTS
+    VotedForConsistencyInv
+    LeaderCurrentTermEntriesInv
+    RequestVoteTermBoundInv
+    AppendEntriesResponseTermInv
+    SnapshotResponseTermValidInv
+
+\* Temporal Properties
+PROPERTIES
+    MonotonicCommitIndexProp
+    MonotonicTermProp
+    MonotonicMatchIndexProp
+    LeaderCommitCurrentTermLogsProp
+    LeaderAppendOnlyProp
+    CommittedEntriesPersistProp