Design notes

The port that
audited the original

Rewriting etcd's raft in MoonBit was not transcription. Where Go uses a struct field and a convention, MoonBit uses a sum type and an exhaustive match - and the compiler refuses to let a case go unhandled. Three times, filling in a case the Go code left implicit turned up a real latent bug. Two of them were safety violations.

Method: we fixed the implementation, never the assertion. Every bug below is pinned by a ported etcd test that fails before the fix and passes after.

Bug 1 · Election & State-Machine Safety

B1Two leaders in one term

Raft's whole promise is that a committed entry is permanent. That rests on Election Safety: at most one leader per term. The reference step path, ported faithfully, had a gap - it never dropped a response stamped with a term below the receiver's own.

The failure

A VoteResp from an old term, reordered late by the network, was counted into the current tally - enough to manufacture a false majority and elect a second leader in a term that already had one. A stale AppendResp could likewise inflate a follower's progress and over-commit. Both break the guarantee the log rests on.

The regression test

b1_stale_term_wbtest.mbt replays the reordered stale response. Before the fix it observes is_leader() true on a second node and a commit index of 3 where 0 is correct; after the fix, both hold.

The fix makes "how does this message's term compare to mine?" a value you must destructure - so "it's older" cannot be silently skipped:

priv enum TermRel {
  Stale      // msg.term < ours - ignore requests, DROP responses
  Aligned    // msg.term == ours
  Ahead      // msg.term > ours - step down first
}

fn step(self : RaftNode, m : Message) -> Array[Message] {
  match self.term_rel(m) {
    Stale   => match m.payload {
                 // a response from a dead term proves nothing
                 VoteResp(_) | AppendResp(_) | HeartbeatResp(_) => return []
                 _ => /* reply with our term so the sender updates */
               }
    Ahead   => self.become_follower(m.term())
    Aligned => ()
  }
  // … only messages that passed the classifier reach the handlers
}

In Go the term comparison is a chain of ifs; forgetting the response case compiles cleanly and ships. In MoonBit the match on TermRel and the nested match on Payload are both exhaustive: leave the stale-response case out and it does not build. The bug becomes unrepresentable.

Bug 2 · Storage contract

S2Compacted or just unavailable?

When a leader asks storage for an entry the follower needs, the answer decides the next move: if the index was compacted away, send a snapshot; if it is simply past the end, wait. The old storage returned the same empty answer for both - a None that conflated two states needing opposite responses.

Before - one None for two worlds

fn term(i : UInt64) -> UInt64? {
  // compacted? out of range? caller
  // cannot tell - and guesses wrong
  ...
}

After - the states are distinct by type

suberror StorageError {
  Compacted
  Unavailable
  SnapOutOfDate
  SnapshotTemporarilyUnavailable
}

The read path now raises the precise variant; storage_bridge.mbt catches it and either ships a snapshot or backs off - no guessing. TestStorageTerm, TestStorageEntries and TestStorageCompact assert the distinction that the boolean answer used to erase. (A third fix, S1, corrected apply_snapshot wrongly advancing the HardState commit index - etcd leaves it untouched.)

The through-line

Types that erase whole classes of bug

Both fixes share a shape: a place where Go collapses several distinct situations into one under-specified value - a bare term integer, a None - and MoonBit forces them apart into a sum type the compiler makes you handle. The bug is not caught at test time; it is made impossible to write.

Messages are one enum

Every request is paired with its response in a single Payload. A transport moves them without knowing what any means; a handler cannot receive a shape the type forbids.

Roles are a closed set

Follower / Candidate / Leader - every transition is a match over three cases. A new state can't be bolted on without the compiler pointing at every site that must account for it.

Errors carry their reason

StorageError replaced a boolean that discarded exactly the information the caller needed. The recovery decision reads off the variant.

Provenance

What is derived, what is new

This is a faithful port of etcd-io/raft (Apache-2.0): the protocol core, the storage model, and the test suite are carried over - the tests especially, because a port you can't check against the original is just a rewrite. What the MoonBit version adds is the algebraic data model above, a deterministic simulation harness with built-in safety-invariant checks, and the WebAssembly demo where each node runs in its own Web Worker.

▶ Watch the invariants hold Full porting log ↗

The port thataudited the original