The Paxos-Odin book

Authorship and license. The code is authored by Vikrant Rathore, with assistance from Ronak Rathore. Copyright (c) 2026 Vikrant Rathore and Ronak Rathore. The library, Python SDK, CLI and documentation are released under the MIT License; the repository's LICENSE contains the complete terms.

The public monorepo is insanai/paxos-odin. The project website provides this book and the PODs as HTML, their PDFs, and the generated Python API reference.

This book explains one fundamental algorithm: Leslie Lamport's Paxos consensus protocol. It also explains one concrete, bounded implementation of that algorithm written in the Odin programming language: paxos-odin.

The two tasks are kept together throughout this text. A line of systems code is easier to trust when we understand the mathematical proof obligation that requires it. Conversely, a proof of safety is easier to remember when we can point directly to the struct field that carries its meaning.

The source is written in Typst. The diagrams use Fletcher and CeTZ. The code is idiomatic Odin. The consensus protocol is grounded in Leslie Lamport's seminal papers, "The Part-Time Parliament" (ACM TOCS 1998) and "Paxos Made Simple" (2001); the reconfiguration and epoch-sealing layer is derived from the stop-sign construction described in Lamport, Malkhi, and Zhou's "Reconfiguring a State Machine".

Early in this millennium, the Aegean island of Paxos was a thriving mercantile center. Though its citizens were very busy with their business, they needed a government to lead them and make communal decisions.

Preface

The usual introduction to Paxos starts too late. It begins with "Prepare" and "Accept" messages. Those messages then look like arbitrary rules from a game whose underlying purpose was forgotten.

We shall start much earlier. We shall ask a simple question:

Three machines must write one value on three pieces of paper. A machine may stop at any moment. A network messenger may vanish into thin air. No machine may ever erase ink that was once written. How can the machines guarantee that two different values are never declared final?

We build the answer by testing small examples. Each example exposes a flaw in a tempting solution and gives us a condition the next solution must satisfy. Prepare and Accept then become messages that carry those conditions between machines.

We compute small traces, predict outcomes before seeing answers, and explain each transition in plain language. Then we move a crash or delay a message and ask which facts still hold. The formal argument collects those facts into invariants.

The implementation follows the exact same pedagogical order:

1. First come values, node identities, and ballots.
2. Next come promises, durable ballots, and votes.
3. Then come multi-slot logs, leader elections, log hole filling, and stable storage, and the chapter that proves the whole construction safe.
4. Finally come bounded memory windows, rotating slot ownership, stop signs, and state machine replication.

At each step, we ask two fundamental questions:

• What can go wrong?
• Which invariant prevents it?

0.1 How to read the book

Parts I through III derive the protocol from one safety question, end with a sequence of decisions, and close with the safety argument: axioms, lemmas, and the proof that each departure from the textbook preserves agreement. Part IV is the library: the bounded state machine, the host contract, the advanced features, rotating slot ownership, and the coding rules that keep the code reviewable. Part V builds three systems on it. Part VI is the evidence and its limits. Part VII is the desk reference, with the answers to selected exercises, and Part VIII maps Lamport's paper to the procedures that implement it. Part IX develops the proposed Python SDK, keeping its future interface distinct from the implemented Odin core.

0.2 Audience and prerequisites

You need sets, integer arithmetic, and the willingness to accept that a process can stop between any two instructions. Odin is read, not required: every excerpt is short and explained. If you already know Paxos, start with the checkpoint at the top of Part I and skip forward when it passes.

0.3 Notation

• $𝑁$ voters; a quorum $𝑄$; ${𝑄}_1$ the phase-one (read) quorum and ${𝑄}_2$ the phase-two (write) quorum. Intersection is written ${𝑄}_1\cap {𝑄}_2\ne \varnothing$.
• A ballot is the triple $\left(𝑟,𝑝,𝑛\right)$: round, priority, node, ordered lexicographically. The library packs the triple into one 64-bit integer so that the lexicographic order is integer comparison.
• The owner of slot $𝑠$ under rotating ownership is member $\left(𝑠-1\right)mod𝑁$ in ascending node-id order; its ballot in that slot has round $0$.
• Slots are one-based; $𝑠=0$ means "no slot".
• Code identifiers appear in monospace; Odin types are Ada_Case, procedures are snake_case, error values are written with a leading dot, as in .Not_Leader.

0.4 Commands used in the book

make build                       # library object, simulator, benchmark, CLI into bin/
make test                        # odin test tests
make check                       # style, tests in two builds, contracts, 240 seeded simulations, smoke runs
make example                     # the three-node counter
./bin/paxos-sim --seed=7 --steps=10000 --nodes=5 --verbose
./bin/paxos-sim --seed=7 --steps=10000 --nodes=5 --ownership   # every node proposes
./bin/paxos-bench --durable      # in-memory modes plus journal-and-fsync modes
make bench-matched               # matched CPU workloads across four libraries
make bench-profile               # Callgrind and Massif evidence
make bench-compare               # historical harness, including durable modes
make docs                        # this book and the POD records as PDF

0.5 Accompanying artefacts

• The library in src/: the core in ten files (ballot.odin, bit_set.odin, membership.odin, ledger.odin, messages.odin, effects.odin, node.odin, election.odin, consensus.odin, ownership.odin), then replicated_log.odin (stop signs and configuration-checked envelopes), learner.odin, errors.odin, and paxos.odin (the unified surface).
• examples/counter.odin: the three-node replicated counter walked through in Part V.
• sim/: the seeded fault simulator with its oracles, in single-leader and rotating-ownership modes.
• bench/: the in-memory and durable benchmarks.
• tools/check.py: the complete verification run.

Pedagogical Approach and Structure

Distributed consensus is notoriously difficult because one must simultaneously account for process crashes, network partitions, message loss, arbitrary delays, competing leaders, and non-volatile storage invariants. Verbose descriptions rarely help; rigorous structure and progressive disclosure do. This book builds understanding in deliberate layers, repeatedly anchored to one central question.

Our editorial approach is guided by four core principles, directly reflecting the architectural values articulated in POD 0001:

1. Visualize concrete scenarios first. We begin with three voters, one value, and a single slot before introducing generalized quorums and multi-slot logs. We describe the physical situation in clear language before introducing formal symbols.
2. Make the reasoning inspectable. We state explicit assumptions, precisely define terms such as "chosen", and formulate safety invariants before presenting the state transitions that preserve them. Safety guarantees are kept strictly distinct from liveness conditions.
3. Treat code as executable specification. We place Odin implementation excerpts directly beside the mathematical proof obligations they satisfy. We trace entire message flows whenever distributed interactions become subtle.
4. Exercise mechanical sympathy. We assign each variable a single unambiguous meaning, cleanly distinguish buffer indices from consensus slots, and use targeted counterexamples to demonstrate why tempting shortcuts fail.

Diagrams are designed to perform explanatory work: clarifying which participant witnessed an earlier vote, which event must complete before sending a reply, and when storage may be safely reused. Labels convey essential semantic ordering, while colour serves as a reinforcing cue.

0.6 The Three Levels of Understanding

Every consensus mechanism in this book is examined at three distinct levels:

Placing Odin excerpts directly alongside theoretical invariants is intentional: the code is the proof obligation made concrete, and the invariant provides the exact rationale for why the code is structured as it is.

0.7 Chapter Structure

To ensure concepts are internalized and verifiable, instructional chapters follow a structured progression:

1. Objectives & Prerequisites: Clear statements of concepts and skills introduced in the chapter.
2. Thought Experiment: An initial prediction exercise that highlights subtle failure modes before presenting the solution.
3. Worked Derivation: Step-by-step analysis of messages, state mutations, and underlying justifications.
4. Code Inspection: Concrete Odin procedures and data structures implementing the mechanism.
5. Review & Exercises: Structured questions and failure variations to test understanding.

0.8 Suggested Reading Pathways

0.9 Repository Architecture

The principles and claims in this book correspond directly to runnable software in the repository:

• src/: The pure consensus engine. A bounded Multi-Paxos Node whose state resides in a columnar Ledger; a caller-owned Effects batch; optional rotating slot ownership; a Replicated_Log_Node supporting epoch isolation via stop-sign reconfiguration; a non-voting Learner; and an Error enum with explanatory diagnostic hints for every condition.
• examples/counter.odin: A standalone three-node replicated counter illustrating the complete host integration loop in approximately 130 lines of code.
• tests/: 79 deterministic test suites, including an exhaustive election test matrix, seeded reconfiguration scenarios, and rotating slot ownership tests.
• sim/: A deterministic fault simulator verifying safety invariants (agreement, validity, monotonic commitments, contiguity, and liveness) across single-leader and multi-proposer rotating configurations.
• bench/: Matched CPU benchmarks comparing Odin against Zig, Rust (OmniPaxos), and C (LibPaxos3), accompanied by callgrind and memory profile datasets.
• tools/check.py: Complete verification harness covering code style, multi-build compilation, durability contracts, and extensive simulation runs.

0.10 Prerequisite Self-Assessment

Before proceeding to Part I, test your intuition against these four foundational questions:

1. Three nodes must agree on a single value in an asynchronous network. Why is a policy of "the first proposal to arrive wins" unsafe?
2. What fundamental guarantee does a majority quorum provide, and under what conditions can asymmetric read and write quorums provide the same safety guarantee?
3. What state must an acceptor persist to durable storage across crashes, and what failure occurs if this state is lost?
4. What is the precise distinction between a value being chosen versus being known to be chosen?

Revisit your answers after completing Part III. The conceptual distance between the two marks the core contribution of this book.

1 Foundations of Consensus

1.1 The empty ledger

Three librarians sit in three separate rooms. Each keeps a copy of the same ledger, and the next line of every copy is blank. Two merchants arrive at the front desk at the same moment. One wants the line to read olive_oil = 50; the other wants olive_oil = 80. Each merchant hires runners to carry slips to the librarians.

The librarians cannot leave their rooms; they talk only through runners, and the runners are unreliable. A runner may take an hour or a week, deliver slips out of the order they were written, deliver the same slip twice, or never arrive. The one thing a runner never does is change the words on a slip.

What we want is easy to state. At most one value may ever be marked final on that line. Tentative votes may differ; final decisions must agree. A merchant may be told a value only after it is settled. And if runners deliver, a majority of librarians stay at their desks, and one proposer can finish without repeated interruption, the line should eventually be filled. The first two wishes say what must never happen; the third says what should eventually happen. They are different kinds of promise.

A library where nobody writes anything is perfectly safe. That sounds like a joke, but it lets us design the rules that keep us safe first, with no assumption about time, and add the rules that make progress afterwards. Every rule in this chapter is a safety rule.

1.2 Three tempting answers

Each of these designs is the first thing a careful engineer proposes. Each fails, and each contributes a piece that survives into the final protocol.

First writer wins. Each librarian writes whichever slip reaches her first. Runner A reaches librarian 1 first, runner B reaches librarian 2 first, and now copy 1 says 50 and copy 2 says 80, forever. What survives: every librarian keeps local state and answers from it. What fails: nothing ties the local decisions together.

One master. Appoint librarian 1 as the only writer; the others copy her. This works until she falls asleep. If librarian 2 takes over, she must know whether librarian 1 already wrote something that reached a copy, and she cannot ask a sleeping colleague. What survives: one active proposer at a time keeps the protocol simple. What fails: a takeover has no safe way to learn the past.

Unanimity. Write a value only when all three librarians agree. Nobody can ever disagree, but if one librarian is asleep or one runner is lost, the line stays blank forever. What survives: a value is settled by a set of acceptances, not by one person. What fails: the set is too large to survive a single absence.

The final protocol combines the three survivors: durable local state, ordered attempts by proposers, and quorums that connect each new attempt to earlier decisions. Concurrent proposers can delay progress, but must not break agreement.

1.3 The failure model

A proof is only as good as the world it assumes. This library assumes four rules.

1. Nodes may crash and recover. A node runs the algorithm exactly until it halts, and it may halt between any two instructions. After halting it says nothing. It comes back only if the host rebuilds it from a durable journal, and is then the same member only because it remembers what it wrote.
2. The network is asynchronous. There is no bound on how long a message takes. The core reads no clock; the host feeds it logical ticks, which affect only liveness.
3. Runners lose, duplicate and reorder. Any message may be dropped, delivered twice, or delivered after a message sent later. Every handler in src/election.odin and src/consensus.odin must be harmless under duplicates and correct under reordering.
4. Nobody lies. A delivered message is exactly what its sender wrote, and the sender followed the algorithm: the non-Byzantine assumption. node_step rejects senders outside the membership with .Not_Member but does not authenticate; that is the host transport's job.

1.4 Quorums

We cannot wait for everyone, and we cannot let anyone act alone. A quorum is large enough to matter and small enough to assemble.

With $𝑁$ acceptors and simple majorities, a quorum has at least $\lfloor \frac{𝑁}{2}\rfloor +1$ members. Two majorities of an $𝑁$-element set cannot be disjoint, because together they would hold more than $𝑁$ elements. The overlapping member is the witness who carries the past into the future.

The library does not hard-code majorities. It stores a read quorum size for phase one and a write quorum size for phase two, defaults both to the majority, and validates only the property that matters:

    majority := total / 2 + 1
    read := read_quorum_override if read_quorum_override != 0 else majority
    write := write_quorum_override if write_quorum_override != 0 else majority
    if read <= 0 || read > total do return .Invalid_Read_Quorum
    if write <= 0 || write > total do return .Invalid_Write_Quorum
    if read + write <= total do return .Non_Intersecting_Quorums
    validated.read_quorum_size, validated.write_quorum_size = read, write

Odin's integer division makes 5 / 2 + 1 evaluate to 3: five members with default quorums need three promises and three acceptances. A host may lower the write quorum to two only if it raises the read quorum to four, because the sum must exceed total. The error names the consequence, not the arithmetic: .Non_Intersecting_Quorums.

Why odd counts? Three acceptors need two and survive one crash. Four need three and still survive only one: the fourth member costs a machine, a journal and a link and does not increase the number of crashes tolerated by majority quorums. Five need three and survive two. Voting groups are usually three or five.

1.4.1 Intersection is not memory

Suppose acceptors 1 and 2 accept olive_oil = 50. Later a new leader asks acceptors 2 and 3 what they have accepted. The sets intersect at acceptor 2, so on paper the leader must learn about the 50.

Now suppose acceptor 2 kept its vote only in RAM and lost power in between. It restarts with an empty line and says it has never voted. The new leader proposes 80 to acceptors 2 and 3, they accept, and the ledger has chosen two values. The intersection still exists; the knowledge does not. Overlap is a property of sets; safety also needs a property of memory, the subject of the section on durable storage.

1.5 Ballots

Because proposers fail, we must allow many attempts to fill one line and be able to say which attempt is later. Each attempt is a ballot; ballots are unique and totally ordered.

// A ballot is one 64-bit integer, so B1 (a total order on ballots) is integer
// comparison and every message and record carries eight bytes:
//
//   bits 63..24  round      (40 bits, the campaign counter; round 0 is reserved for
//                            slot owners under rotating ownership)
//   bits 23..16  priority   (8 bits, breaks ties between rounds)
//   bits 15..0   node       (16 bits, the proposer; makes every ballot unique)
Ballot :: distinct u64

BALLOT_ZERO      :: Ballot(0)
BALLOT_ROUND_BITS :: 40
MAX_ROUND        :: u64(1) << BALLOT_ROUND_BITS - 1

ballot_make :: #force_inline proc(round: u64, priority: u8, node: Node_Id) -> Ballot {
    return Ballot(round << 24 | u64(priority) << 16 | u64(node))
}

ballot_round :: #force_inline proc(b: Ballot) -> u64 {
    return u64(b) >> 24
}

ballot_priority :: #force_inline proc(b: Ballot) -> u8 {
    return u8(u64(b) >> 16)
}

ballot_node :: #force_inline proc(b: Ballot) -> Node_Id {
    return Node_Id(u64(b))
}

A ballot is a triple (round, priority, node) packed into one unsigned integer, with the round in the high 40 bits, the priority in the next 8 and the 16-bit Node_Id in the low bits. Because each field sits above the fields that rank below it, the plain integer order < on two ballots is exactly the lexicographic order on the triples. A greater round always wins. Within a round, a greater priority wins; the host sets it through Node_Options.priority to prefer some members as leaders. Within a round and a priority, the greater node id wins, and because node ids are unique inside a membership, two members never produce the same ballot. ballot_make packs the triple and ballot_round, ballot_priority and ballot_node unpack it; everything else in the library compares ballots with < and ==. Forty round bits are enough for MAX_ROUND campaigns before .Ballot_Exhausted; BALLOT_ZERO is Ballot(0), below every ballot a campaign can produce. Round 0 itself is reserved for slot owners under rotating ownership, which a later chapter covers.

1.6 Votes and the meaning of "chosen"

An acceptor votes by accepting a proposal: it records a ballot and a value for the slot, in the vote_ballot and value columns of its Ledger, and holds at most one vote per slot, the latest.

The moment the last acceptor of a write quorum makes its vote durable, the value is chosen, even if that acceptor's reply is lost, even if the leader dies in the next microsecond, even if no learner ever hears. Every later rule exists to make sure a fact nobody knows about is still respected.

1.7 Three invariants

Lamport's proof of the Synod protocol rests on three conditions on ballots, each of which the library keeps in a specific place.

B1 makes "later" well defined. B2 makes sure a later ballot cannot avoid meeting a witness. B3 tells the later ballot what to do with what the witness says, and it is the rule people get wrong. It is not "the value with the most votes" and not "the most recent value you heard". Among the votes reported by your read quorum, find the one with the greatest ballot and propose its value; if nobody reported a vote, propose what you like. Older votes may belong to attempts that never reached a quorum, so counting them counts noise. The proof below shows that the greatest-ballot vote carries the chosen value whenever a choice was made.

1.8 The greatest-vote proof

Here is the proof that B1, B2 and B3 together keep safety. The single-decree chapter uses it to explain why each message field exists, and the safety-argument chapter restates it as formal lemmas, each mapped to the procedure that keeps it.

Claim. Suppose value $𝑣$ is chosen at ballot $𝑏$, so a write quorum $𝑊$ of acceptors each accepted $\left(𝑏,𝑣\right)$. Then every ballot ${𝑏}^{\prime }>𝑏$ whose leader sends an Accept sends the value $𝑣$.

Proof. By strong induction on ${𝑏}^{\prime }$. Fix ${𝑏}^{\prime }>𝑏$ and assume the claim for every ballot strictly between $𝑏$ and ${𝑏}^{\prime }$.

The leader of ${𝑏}^{\prime }$ finished phase one, so a read quorum $𝑅$ promised ${𝑏}^{\prime }$. By B2, $𝑅$ and $𝑊$ share some acceptor $𝑎$. Acceptor $𝑎$ did two things: it accepted $\left(𝑏,𝑣\right)$ and it promised ${𝑏}^{\prime }$. Had it promised ${𝑏}^{\prime }$ first, then when $\left(𝑏,𝑣\right)$ arrived, $𝑏<{𝑏}^{\prime }$ would have been below its promise and it would have refused, contradicting $𝑎\in 𝑊$. So $𝑎$ accepted $\left(𝑏,𝑣\right)$ before promising ${𝑏}^{\prime }$.

When $𝑎$ answered the prepare for ${𝑏}^{\prime }$, its slot therefore held a vote with ballot at least $𝑏$: either $\left(𝑏,𝑣\right)$ itself, or a later vote at some ${𝑏}^{″}$ with $𝑏<{𝑏}^{″}<{𝑏}^{\prime }$ that overwrote it. By the induction hypothesis every such ${𝑏}^{″}$ carried $𝑣$. So the greatest-ballot vote reported by $𝑅$ has ballot at least $𝑏$ and value $𝑣$, and by B3 the leader of ${𝑏}^{\prime }$ proposes $𝑣$. $∎$

Three facts had to hold, and each is a line of code. Acceptors refuse ballots below their promise: on_accept calls send_nack when msg.ballot < l.promised, where l is the acceptor's Ledger. Acceptors report their vote in the promise: on_prepare sends one Promise_Message per used cell. And acceptor $𝑎$ still remembered both when asked, which is where durable storage enters.

1.9 Why durable storage is mandatory

The proof used the phrase "still remembered". An acceptor that votes, replies, and then loses the vote to a power failure has told the leader something no longer true. Worse, an acceptor that promises ${𝑏}^{\prime }$, replies, and then forgets may later accept a ballot below ${𝑏}^{\prime }$, which is exactly the refusal the proof relied on.

Lamport's priests wrote in indelible ink. Here, a promise or a vote is a Write record the host must append to a journal and sync before any message from the same transition leaves the machine. The Ledger that holds the durable state refuses to move backwards:

ledger_apply :: proc(l: ^Ledger($Value, $WINDOW), write: Write(Value)) -> Error {
    switch w in write {
    case Write_Promise:
        if w.ballot < l.promised do return .Promise_Regression
        l.promised = w.ballot
    // ...
    case Write_Vote(Value):
        if w.slot == 0 do return .Invalid_Slot
        if w.ballot < l.promised do return .Promise_Regression
        // ...

.Promise_Regression is not a protocol message. It is a self-check: a Write_Promise or Write_Vote that would lower the promised ballot is refused, because the protocol never produces one. A host that sees it has a journal written out of order or corrupted, and the hint in explain_error says to stop the node. The other half of indelible ink lives in Effects: every transition returns its writes and messages in one batch, and with the default Durability_Gate.Enforced the batch refuses to hand out messages until the host calls confirm_writes_durable. The single-decree chapter walks through that gate at every crash point.

1.10 From rules to messages

We can now derive the messages from their purpose. Read the invariants as obligations on a proposer and ask what evidence it must request and send.

1. B1 says: pick a ballot greater than any you have seen. That needs no message, only a memory of the greatest round observed.
2. B3 needs the votes of a read quorum, and the proof needs those acceptors to refuse everything below your ballot from now on. One message asks for both: Prepare, carrying the ballot. The reply, Promise, carries the acceptor's vote for the slot if it has one.
3. B2 says: count promises until you have a read quorum, then apply B3 and pick.
4. Send the ballot and the value to the acceptors: Accept. An acceptor that has not promised anything greater records the vote durably and replies Accepted.
5. Count Accepted replies until you have a write quorum. The value is chosen. Tell everyone: Commit.

One more message follows from liveness rather than safety. An acceptor that receives a Prepare or an Accept below its promise answers Nack with the ballot it has promised. This lets the proposer react promptly instead of waiting for a timeout. The single-decree chapter shows the exchange.

2 The Single-Decree Protocol

2.1 The four roles

Paxos is described with four roles. Keep them apart in your head even though this library runs all four inside one Node value.

The client wants a command applied; it is outside the library, and the host calls paxos.propose on its behalf. The proposer runs campaigns, picks values under B3, and drives phase two; its bookkeeping is volatile, and a restarted proposer simply campaigns again higher. The acceptor promises and votes, and never says anything it has not first written down. The learner collects commits and hands the application a contiguous prefix of decided slots, never a slot with a hole below it.

One Node(Value, MAX_MEMBERS, WINDOW_SLOTS, CHUNK_SLOTS, GATE) plays all four. Its proposer side is the Role enum: .Follower acts only as acceptor and learner, .Preparing is running phase one, .Leader may run phase two. A node built with paxos.init_learner is the exception: its id lies outside the membership, it never promises or votes, and it answers .Learner_Message_Forbidden to anything but Commit.

2.2 Phase one: earn the right to propose

Phase one has two purposes, both from the foundations chapter. It secures a read quorum's promise to refuse lower ballots, and it collects that quorum's votes so that B3 can be applied.

2.2.1 Prepare

A campaign starts when the host calls paxos.campaign(&node, noop, &effects) or when a follower's election timer expires inside paxos.tick. Both paths reach start_campaign:

    greatest := max(node.highest_observed_round, ballot_round(node.ballot))
    greatest = max(greatest, ballot_round(ledger_highest_ballot(&node.ledger)))
    if greatest >= MAX_ROUND do return .Ballot_Exhausted

    node.ballot = ballot_make(greatest + 1, node.priority, node.id)
    node.role = .Preparing

The new round is one more than the greatest round this node has seen from any source: its own last ballot, any round a peer has mentioned, and the greatest ballot anywhere in its own ledger, which ledger_highest_ballot takes over the promise, every per-slot promise and every vote. That is B1 in one expression. The candidate then promises itself, setting ledger.promised to the new ballot and adding a Write_Promise to the batch, and calls broadcast_all with a Prepare_Message holding ballot, the slot range first..last it wants to hear about, and a scope of .Global, meaning "promise me every slot from first on"; it proposes no value. The order matters: the promise is in the same batch as the Prepare, so it is durable before any peer hears the ballot, and a candidate that crashes can never build the same ballot again. The broadcast includes the node itself, so the candidate's own acceptor answers through the same handler as everyone else's; by then the promise is already recorded and on_prepare writes nothing new.

2.2.2 Promise

An acceptor compares the Prepare ballot with the greatest ballot it has ever promised, which lives in node.ledger.promised:

    l := &node.ledger
    if msg.ballot < l.promised {
        send_nack(node, from, msg.ballot, l.promised, 0, effects)
    return .None
}
    if msg.first == 0 || msg.last < msg.first do return .Invalid_Slot
    switch msg.scope {
    case .Global:
        if msg.ballot != l.promised {
            l.promised = msg.ballot
            effects_add_write(effects, Write_Promise{msg.ballot})
    }
        observe_leader(node, from, msg.ballot)

A ballot below the promise is refused with a Nack. A ballot equal to the promise is a retransmission and needs no new record. A greater ballot becomes the new promise, and Write_Promise enters the effects batch before any reply. (The .Bounded scope, which promises one slot range instead of every slot, belongs to rotating ownership and waits for a later chapter.) The handler then walks the ledger's used bitmap and reports every vote or decision it holds in the requested range, one Promise_Message per cell:

    cell, used := bit_set_next(l.used, 0)
    for used {
        slot := l.slot[cell]
        if slot > l.anchor.chosen_trim_slot && slot >= msg.first {
            if slot > msg.last {
                more = true
        } else {
                reported += 1
                send_to(node, from, effects, Promise_Message(V){
                    ballot = msg.ballot, slot = slot, vote = l.vote_ballot[cell],
                    state = l.state[cell], value = &l.value[cell],
                })
        }
    }
        cell, used = bit_set_next(l.used, cell + 1)
}

The state field is the cell's Cell_State. A cell this node voted in is reported as .Voted with its vote ballot. A cell this node learned through a Commit is reported as .Chosen: it carries a value and no meaningful ballot, and it tells the candidate "this is decided; do not run phase two for it". After the per-slot messages comes one Promise_Range_Message, which names the slot range answered, the reported count of per-slot promises sent, and the acceptor's own decided prefix. The candidate counts an acceptor toward the read quorum only when it holds the range descriptor and that many per-slot promises, so reordered runners cannot make a partial answer look complete.

2.2.3 Value selection

The candidate's on_promise stores each report in the recovered_ballot, recovered_state and recovered_value columns at the chunk-relative index slot - recover_base. This index is distinct from a ledger cell. It replaces a vote only when msg.vote > node.recovered_ballot[cell], so each slot keeps the greatest ballot seen; a report with state = .Chosen dominates every vote. Two reports with equal ballots and different values return .Conflicting_Value: that would mean B1 was broken, and the library stops rather than pick. When maybe_resolve_chunk counts a read quorum of complete answers, resolve_chunk walks the slots and applies B3 to each:

        cell, in_chunk := recovery_index(node, slot)
        assert(in_chunk, "Recovery slot outside chunk. Hint: Report this invariant failure.")
        if chosen, is_chosen := ledger_chosen_at(&node.ledger, slot); is_chosen {
            broadcast_peers(node, effects, Commit_Message(V){slot = slot, value = chosen})
        } else if node.recovered_slot[cell] == slot && node.recovered_state[cell] == .Chosen {
            record_commit(node, slot, node.recovered_value[cell], effects) or_return
            if decided, ok := ledger_chosen_at(&node.ledger, slot); ok {
                broadcast_peers(node, effects, Commit_Message(V){slot = slot, value = decided})
            }
        } else {
            value := node.noop.?
            if node.recovered_slot[cell] == slot && node.recovered_state[cell] == .Voted {
                value = node.recovered_value[cell]
            }
            accept_err := send_accept(node, slot, node.ballot, value, effects)
            if accept_err == .Not_Leader {
                // A higher ballot already holds this decree: this candidate lost. Step down
                // quietly; the winner (or the next timeout) finishes the range.
                node.role = .Follower
                return false, .None
            }
            accept_err or_return
        }

A slot the candidate itself already holds as chosen is re-announced. A candidate whose accept is refused because a higher ballot already promised that decree has lost the election; it steps down rather than report an error. A reported decision is committed outright. A reported vote is re-proposed under the new ballot. A slot nobody voted in, below one somebody did, is filled with the host's no-op. For a fresh single decision none of these fire: become_leader runs, the role becomes .Leader, and next_slot is 1.

2.3 Phase two: write the future

A client value arrives through paxos.propose(&node, value, &effects), which checks node.role == .Leader, takes next_slot, and calls send_accept(node, slot, node.ballot, value, effects).

2.3.1 Accept

    l.promised_at[cell] = max(l.promised_at[cell], ballot)
    ledger_record_vote(l, cell, ballot, value)
    effects_add_write(effects, Write_Vote(V){ballot = ballot, slot = slot, value = &l.value[cell]})

    if bit_set_insert(&node.acknowledgements[cell], node.self_index) do node.acknowledged[cell] += 1
    if membership_write_quorum(&node.membership) == 1 {
        record_commit(node, slot, value, effects) or_return
    }
    broadcast_peers(node, effects, Accept_Message(V){ballot = ballot, slot = slot, value = &l.value[cell]})

The leader is also an acceptor, and it votes for its own proposal without sending itself a message: ledger_record_vote puts the ballot and value into its own ledger, Write_Vote records that vote, and the leader sets its own bit in the cell's acknowledgements and counts it in acknowledged. The proposal is that vote: Accept_Message.value points into the leader's ledger, and the pointer stays valid until the node's next transition, which is why a host serialises the batch before running another. This is the local acceptance optimisation. With three members and a write quorum of two, one remote Accepted completes the quorum. broadcast_peers sends the Accept to everyone except the leader.

2.3.2 Accepted

on_accept checks the promise once more, because another candidate may have campaigned since the leader's phase one; a ballot below the effective promise for the cell, l.promised or the cell's own promised_at, whichever is greater, gets send_nack naming the slot. Otherwise the acceptor raises the cell's promised_at to the accepted ballot (a vote implies the promise, even if no Prepare was ever seen), stores the vote with ledger_record_vote, adds Write_Vote to the batch, and only then sends Accepted_Message with the ballot, the slot, and decided_through, its own contiguous decided prefix. The leader records that prefix per peer and uses it in the Multi-Paxos chapter to decide what to retransmit. A duplicate Accept for a vote already held under the same ballot is answered with Accepted again and no new write. A cell that is already .Chosen never votes again: an Accept for the same value gets Accepted, an Accept for a different value gets the decision back as a Commit_Message. One more guard applies before any of this: an Accept whose ballot has round zero is accepted only from the slot's owner under rotating ownership, and otherwise ignored; a later chapter explains that mode.

2.3.3 Commit

The leader's on_accepted ignores replies for any slot and ballot but the one it is driving in that cell (lead_slot and lead_ballot), adds the sender's bit to acknowledgements[cell], and returns until acknowledged[cell] reaches membership_write_quorum. At that count the value is chosen. record_commit marks the cell .Chosen with ledger_record_chosen, adds Write_Chosen, and calls emit_contiguous, which walks from delivered_through + 1 upward and appends every chosen slot it finds to effects.committed until it reaches a hole. Then broadcast_peers sends Commit_Message{slot, value} to every peer, whose on_commit runs the same record_commit and the same emit_contiguous. A later Accepted for a slot already chosen returns early.

2.4 A complete trace

Members 1, 2 and 3; read and write quorums both 2; every priority 0. The host calls paxos.campaign(&n1, noop, &effects), later paxos.propose(&n1, tea, &effects). The runner to member 3 is slow. Each row lists writes before messages, the host's order, and drops the _Message suffix from message names. Ballots are written as their unpacked (round, priority, node) triples, and the chunk is the default 64 slots.

Look at step 9. Tea was chosen the instant N2's Write_Vote in step 8 became durable, because at that moment two of three acceptors held durable votes under (1, 0, 1). Step 9 is N1 learning that fact. Had N1 crashed between steps 8 and 9, tea would still be chosen, and any future read quorum would meet the choosing quorum {N1, N2}. At least one witness would preserve tea through the highest-vote rule.

2.5 Rejection and competing campaigns

A ballot below an acceptor's promise is answered with a Nack rather than silence, so that a stale leader learns it is stale. Nack_Message carries the rejected ballot, the promised ballot that beat it, the slot whose Accept was refused (zero for a refused Prepare), and the acceptor's decided_through. The receiver's on_nack is short because a Nack changes nothing durable:

    node.highest_observed_round = max(node.highest_observed_round, ballot_round(msg.promised))
    if msg.rejected != node.ballot || msg.promised <= node.ballot do return
    node.role = .Follower
    node.leader_hint = ballot_node(msg.promised)

Every Nack raises highest_observed_round, so the next start_campaign jumps above the rival instead of colliding with it again. A Nack for some other ballot, or whose promised is not actually greater, changes nothing else. A genuine Nack demotes the node to .Follower and points leader_hint at the winner, the node id unpacked from the promised ballot.

Suppose N2 campaigns at (2, 0, 2) while N1 leads at (1, 0, 1). N1's own acceptor sees the greater ballot, writes Write_Promise{(2, 0, 2)}, and observe_leader demotes N1 to .Follower. A later paxos.propose on N1 returns .Not_Leader, and any Accept of N1's still in flight is nacked by every acceptor that promised (2, 0, 2).

2.6 Liveness and the dueling leaders

Two candidates can chase each other upward forever: N1 prepares round 1, N2 prepares round 2 and N1's Accepts are nacked, N1 prepares round 3 and N2's are nacked, and so on. Nothing unsafe happens, and nothing useful either. No safety rule can remove this.

The core reads no clock, so it can be simulated and replayed deterministically. Time enters only through paxos.tick(&node, noop, &effects), called at a cadence the host chooses. A follower that reaches election_timeout_ticks without leader contact campaigns; a leader sends Heartbeat_Messages every heartbeat_interval_ticks and retransmits every resend_interval_ticks. All three are fields of Node_Options, and so are the two tools against duels. priority breaks ties inside a round: if N1 and N2 both reach round 5, the greater priority wins and the other steps aside on its Nack; priority never overrides a greater round, so it cannot affect safety. campaign_disabled removes a member from the contest: it promises and votes like any acceptor, but paxos.campaign returns .Campaign_Disabled and its timer never fires, until the host calls paxos.set_campaign_enabled.

2.7 Crash points and recovery

Every transition returns its writes and messages together in one Effects, and the host must persist the writes before sending the messages. The library does not trust the host to remember:

    when G == .Enforced {
        if e.writes_pending do host_order_violation("messages_slice before confirm_writes_durable")
}
    return small_array.slice(&e.messages)

That is the body of effects_messages_slice, where G is the node's GATE parameter. With the default gate, reading messages while a write is unconfirmed calls host_order_violation, which prints a diagnostic and stops the process; so does effects_reset on a batch with unconfirmed writes. The check is compiled out only for a Node declared with Durability_Gate.Host_Managed, whose comment lists the four obligations such a host takes on.

Not every batch needs the same barrier. effects_requires_power_loss_barrier returns true only when the batch holds a Write_Promise, a Write_Promise_At or a Write_Vote; decisions (Write_Chosen) and trim anchors are derived state a restart can rebuild, so a host may persist them more cheaply. Step 10 of the trace is such a batch. One deliberate overlap exists: effects_pre_durable_messages returns an iterator whose pre_durable_next yields only the Accept_Message envelopes whose ballot has a round above zero, so a host may put a leader's Accepts on the wire while its own vote is still syncing. The batch must still be confirmed before messages_slice is read or the next transition runs.

2.7.1 Where the power can fail

No row says "guess". Every restart sees either the old durable state or the new one, and both are states the protocol could have been in.

2.7.2 What a restart replays

The host feeds every journal record, in journal order, through ledger_replay_fold into an empty Ledger:

ledger_replay_fold :: proc(l: ^Ledger($Value, $WINDOW), write: Write(Value)) -> Error {
    switch w in write {
    case Write_Promise:
        l.promised = max(l.promised, w.ballot)
        return .None
    // ...

Replay folds monotonically: a promise record raises promised only if greater, a vote record claims the slot's cell, raises that cell's promised_at to its ballot and installs the vote unless the cell already holds a decision, and decisions and trim anchors go through ledger_apply. The result is the greatest promise and the latest vote per slot, which is what the acceptor knew at the crash. Then paxos.restore(&node, id, membership, ledger) builds a Node around that ledger. It comes back as a .Follower with no leader hint and no election bookkeeping: none of that was durable and none is needed, because the next Prepare or heartbeat re-establishes it and the next campaign starts above every round the journal holds.

3 Multi-Paxos Log Replication

3.1 Why Multi-Paxos?

The single-decree protocol chooses one value. A replicated log needs a chosen value in slot 1, then slot 2, then slot 3, without end. The obvious construction runs an independent single-decree instance per slot. Each instance costs a Prepare/Promise round trip with a durable promise on every acceptor, then an Accept/Accepted round trip with a durable vote on every acceptor: two round trips and two synchronous writes for every entry, before the commit is even announced.

Multi-Paxos observes that phase one does not depend on the value. A candidate can send one Prepare that covers every slot from some starting point onward. Once a read quorum has promised, the candidate holds a ballot that is valid for every one of those slots, and each later proposal needs only phase two: one round trip and one durable vote per acceptor. The candidate that finishes this phase one is the leader for its ballot until a higher ballot appears.

3.2 One Phase One for Every Slot After first

Slots are 64-bit and one-based. The Prepare names the first slot the candidate wants resolved, the last slot of the chunk it wants reported, and a scope:

// One-based position in the global decree log. Zero means "no slot".
Slot :: u64

Prepare_Scope :: enum u8 {
    Global,
    Bounded,
}

// Phase one: promise `ballot` for the decrees the scope names and report your votes in
// [first, last].
Prepare_Message :: struct {
    ballot: Ballot,
    first:  Slot,
    last:   Slot,
    scope:  Prepare_Scope,
}

campaign(&node, noop, &effects) starts the election. The candidate picks a round above every round it has observed, promised, or used, records the host's noop for later, sets recover_base to delivered_through + 1 and recover_last to the end of the first chunk, and broadcasts Prepare_Message{ballot, first = recover_base, last = recover_last} with the default scope .Global to every member, itself included. The candidate answers its own Prepare as an ordinary acceptor when the host steps that envelope back into it; there is no private shortcut for the local vote. Everything below first is already delivered on this node. Everything at or above it is covered by this one promise: that is what .Global means, and it is the Multi-Paxos takeover this chapter describes. (.Bounded promises only [first, last] and belongs to rotating ownership, a later chapter.) The question is how an acceptor describes an unbounded suffix in a bounded message.

3.3 Combining Phase-One Replies per Slot

3.3.1 A chunk and its manifest

An acceptor answers a Prepare for one chunk of CHUNK_SLOTS slots starting at first. For each used cell in that chunk, it sends one Promise_Message carrying the slot, the cell's state, its vote ballot and its value. A cell that holds a decision (the acceptor learned it from a Commit, whether or not it also voted) is reported with state = .Chosen, so the candidate learns the decided value without a separate message kind. After the per-slot promises the acceptor sends one manifest:

Promise_Range_Message :: struct {
    ballot:         Ballot,
    anchor:         Trim_Anchor,
    chosen_through: Slot,
    first:          Slot,
    last:           Slot,
    reported:       u32,
    more:           bool,
}

reported says how many Promise_Messages the acceptor sent for the range first..last. more says whether it holds used cells above last, so the candidate knows another chunk is needed. chosen_through and anchor are the acceptor's two fences; we return to them below.

3.3.2 Counting a peer as complete

The candidate cannot assume the manifest arrives after the promises it describes, or before them. It keeps one Election_Peer per member:

Election_Peer :: struct {
    anchor:            Trim_Anchor,
    chosen_through:    Slot,
    range_first:       Slot,
    range_last:        Slot,
    expected_in_range: u32,
    received_in_range: u32,
    range_described:   bool,
    more:              bool,
}

Each Promise_Message inside the current chunk increments that peer's received_in_range, but only the first time a given slot is seen from that peer: a per-peer bit set, promise_seen, deduplicates retransmissions. The report goes into the candidate's recovered_slot, recovered_ballot, recovered_state and recovered_value columns, which keep the highest-ballot vote per slot, with a .Chosen report dominating any vote; two different values under one ballot for one slot are .Conflicting_Value. The manifest sets expected_in_range and marks the peer range_described. maybe_resolve_chunk then runs after every promise and every manifest:

    if !node.recovery_ready {
        complete := 0
        any_more := false
        for i in 0..<membership_count(&node.membership) {
            peer := &node.election[i]
            if !peer.range_described || peer.received_in_range < peer.expected_in_range do continue
            complete += 1
            any_more ||= peer.more
        }
        if complete < membership_read_quorum(&node.membership) do return .None
        // Phase two may pause at the window boundary. Freeze the selection before any
        // vote leaves, so a late promise cannot change a value under this same ballot.
        node.recovery_ready = true
        node.recovery_more = any_more
    }

A peer counts only when it is fully described: its manifest arrived and every promise the manifest announced arrived too. The candidate waits until read_quorum_size peers are complete. That answers the prediction: the acceptor counts once its manifest and both promises are in, in whatever order they took. Wire order does not matter, and neither does a duplicate.

3.3.3 One slot, two indexes

The ledger keeps WINDOW_SLOTS cells; recovery scratch keeps only CHUNK_SLOTS reports and one chunk-sized bitmap per peer. They serve different lifetimes. The ledger survives the election; scratch describes just the chunk being recovered.

Take a window of 8 and a chunk of 3 starting at slot 7. Slots 7, 8, and 9 map to ledger cells 6, 7, and 0, but to scratch indexes 0, 1, and 2. Using the ledger mask for scratch would both exceed its bounds and confuse the next chunk with this one. recovery_index checks that the slot belongs to the current range before subtracting recover_base. The chunk need not be a power of two.

3.3.4 Freeze the answer before acting on it

A complete read quorum gives the candidate enough evidence to select values. recovery_ready then freezes that selection, and recovery_more remembers whether another chunk is needed. This matters when the current window cannot hold every selected slot: phase two may begin, pause, and resume after the host advances the memory floor.

Suppose the candidate has already sent X for one slot at ballot 5. A late promise reports an older vote for Y. Replacing X in scratch would make the retry send a second value at the same ballot. The candidate must keep its original selection. Late reports cannot change it; a later campaign selects again under a new ballot.

3.3.5 The next chunk

If any complete peer reported more, the candidate resolves this chunk (below) and calls begin_next_chunk: recover_base moves to the slot after the chunk and recover_last to the end of the next one, every Election_Peer is reset except its two fences, promise_seen is cleared, and a new Prepare with the new first and last goes out under the same ballot. Each reply describes at most CHUNK_SLOTS slots per peer. Delayed replies and retransmissions may remain in the network; the candidate only counts reports for its current ballot and chunk. When no complete peer reports more, the candidate becomes leader.

3.4 The Fences

Two numbers from the manifests tell the new leader where the past is already settled. quorum_fences folds them over the election state into a Fences value, starting from the candidate's own values:

    fences.trim = node.ledger.anchor.chosen_trim_slot
    fences.chosen = node.delivered_through
    for i in 0..<membership_count(&node.membership) {
        peer := &node.election[i]
        fences.trim = max(fences.trim, peer.anchor.chosen_trim_slot)
        if peer.chosen_through > fences.chosen {
            fences.chosen = peer.chosen_through
            fences.chosen_peer = membership_get(&node.membership, i)
        }
    }

The trim fence is the greatest chosen_trim_slot any promising peer has adopted: every slot at or below it was chosen and has been released from that peer's window (the advanced-features chapter covers trim anchors). The chosen fence is the greatest chosen_through any promising peer reported: that peer has delivered a contiguous decided prefix through it. The leader takes the larger of the two and never re-proposes, fills, or accepts a client value at or below it. A missing vote below the fence means the slot was released, not that it is open.

The chosen fence also tells the leader that it is behind. Leadership means holding the highest ballot, not knowing every decision. When the chosen fence is above the leader's own delivered_through, resolve_chunk sends a Learn_Message to chosen_peer, asking for commits from delivered_through + 1 for up to CHUNK_SLOTS slots. The leader learns those slots the same way any lagging follower does.

3.5 Holes and the No-Op

Within the chunk, above the fence, the leader must settle every slot up to the highest one it knows about, from its own cells or from recovered votes. A slot with no recovered vote is a hole: no acceptor in the read quorum voted there, so by quorum intersection nothing can have been chosen there, and the leader may propose anything. (The safety-argument chapter proves this per-slot claim as a lemma.) It must propose something, because entries are released only in contiguous order and a permanent hole would block every later slot forever.

The library does not invent a value. The host passes a noop to campaign and to tick; the node remembers it, and maybe_resolve_chunk refuses to resolve with .Missing_Noop if none was recorded. resolve_chunk then walks the chunk:

        cell, in_chunk := recovery_index(node, slot)
        assert(in_chunk, "Recovery slot outside chunk. Hint: Report this invariant failure.")
        if chosen, is_chosen := ledger_chosen_at(&node.ledger, slot); is_chosen {
            broadcast_peers(node, effects, Commit_Message(V){slot = slot, value = chosen})
        } else if node.recovered_slot[cell] == slot && node.recovered_state[cell] == .Chosen {
            record_commit(node, slot, node.recovered_value[cell], effects) or_return
            if decided, ok := ledger_chosen_at(&node.ledger, slot); ok {
                broadcast_peers(node, effects, Commit_Message(V){slot = slot, value = decided})
            }
        } else {
            value := node.noop.?
            if node.recovered_slot[cell] == slot && node.recovered_state[cell] == .Voted {
                value = node.recovered_value[cell]
            }
            accept_err := send_accept(node, slot, node.ballot, value, effects)
            if accept_err == .Not_Leader {
                // A higher ballot already holds this decree: this candidate lost. Step down
                // quietly; the winner (or the next timeout) finishes the range.
                node.role = .Follower
                return false, .None
            }
            accept_err or_return
        }

Three outcomes per slot, after a slot the leader itself already holds as chosen is simply re-announced with a Commit_Message. A report with state = .Chosen came from a peer's decided cell, so it is recorded and announced as a commit. A report with state = .Voted is re-proposed under the leader's ballot with send_accept: the highest-vote rule applied to that slot. No report at all means the no-op is proposed. Each send_accept records the leader's own vote durably (a Write_Vote) before the Accept_Message leaves.

When the window cannot yet hold the whole chunk because the memory floor is too far behind, resolve_chunk proposes as much as fits and reports the chunk unresolved. The node stays in .Preparing, and tick retries maybe_resolve_chunk until the host advances the floor or the election times out.

3.6 A Worked Recovery: Slots 10, 11, and 12

Three voters, ids 1, 2, and 3; both quorums are majorities of two. Node 1 led under ballot ${𝑏}_1$ and delivered through slot 9. It proposed X in slot 10, and node 2's Accepted gave it a write quorum, so node 1 committed slot 10 and sent a Commit; the Commit reached node 2 but not node 3. Node 1 proposed Z in slot 12, and that Accept reached node 3 only. Nothing was ever sent for slot eleven. Then node 1 crashed. Node 3's election timer fires, and the host calls campaign(&node3, noop, &effects). Its delivered_through is 9.

Notice what did not happen. Slot 10 was never re-proposed: the chosen fence put it out of reach, and the leader learned it instead. Node 2's recovered report for slot 10 sat unused, because resolve_chunk began above the fence. Had node 2 voted for X but never received the Commit, it would have reported chosen_through = 9 and Promise{slot 10, vote b_1, state .Voted, X}, and the leader would have re-proposed X in slot 10 under its own ballot, which is the highest-vote rule at work. The .Chosen branch is for a peer that holds the decision but has not delivered through it, for instance one that received the Commit for slot 10 while slot 9 was still missing. Every path ends the same way: X is the only value slot 10 can ever hold.

3.7 The Stable-Leader Pipeline

After become_leader, propose(&node, value, &effects) assigns next_slot, advances it, and calls send_accept. Nothing waits for the previous slot to commit: the leader may have many slots in flight, and acceptors vote on each independently. propose_batch(&node, values, slots, &effects) does the same for up to CHUNK_SLOTS values in consecutive slots and one effect batch, returning the assigned slots in the caller's slots buffer; more values give .Batch_Too_Large, none give .Empty_Batch.

Pipelining needs a bound, or one slow follower would let the leader's memory grow without limit. The bound is the window:

    if node.next_slot == max(Slot) do return 0, .Global_Slot_Exhausted
    if node.next_slot - node.memory_floor > Slot(W) do return 0, .Window_Full

W is the node's WINDOW_SLOTS parameter. memory_floor is the greatest slot the host has told the node it may forget. It rises only when the host calls advance_memory_floor(&node, through) after durably consuming every released entry through through:

node_advance_memory_floor :: proc(node: ^Node($V, $M, $W, $C, $G), through: Slot) -> Error {
    if through > node.delivered_through do return .Invalid_Slot
    node.memory_floor = max(node.memory_floor, through)
    return .None
}

Asking to advance past delivered_through is .Invalid_Slot, and the floor never moves down. .Window_Full is flow control, not a log limit: the proposal is refused, nothing is written or sent, and the same call succeeds once the floor moves.

Physically, slot s lives in the ledger cell cell_of(s, WINDOW_SLOTS):

// The window index of a slot. WINDOW is a power of two, so this is one mask.
cell_of :: #force_inline proc(slot: Slot, $WINDOW: int) -> int {
    return int((slot - 1) & Slot(WINDOW - 1))
}

node_init asserts at compile time that WINDOW_SLOTS is a power of two, so the ring index is (s - 1) & (WINDOW_SLOTS - 1), one mask rather than a division. The cell is tagged with its slot number in the ledger's slot column. claim_live decides whether a cell may be taken for a new slot. The live window is $($memory_floor,memory_floor+𝑊]: a slot below it has been consumed by the host, and a slot above it would land in the cell of a slot that is still live, so both are refused, and live slots and cells stay in bijection:

    if slot <= node.memory_floor || slot - node.memory_floor > Slot(W) do return 0, false
    l := &node.ledger
    cell := cell_of(slot, W)
    held := l.slot[cell]
    if held == slot do return cell, true
    if held == 0 || (held <= node.memory_floor && l.state[cell] == .Chosen) {
        ledger_open(l, cell, slot)
        return cell, true
    }
    return cell, false

A cell is retagged (ledger_open clears everything but the value storage) only when it is empty or when its old occupant is both at or below the memory floor and .Chosen. A cell holding a .Voted but undecided vote is never evicted, because that vote may be part of a quorum some future leader must discover. The tag makes a stale cell impossible to mistake for the slot that now maps to it.

3.8 Membership Changes: The Stop Sign

A configuration is a fixed voter set with fixed quorum sizes. To change it, the log carries a stop sign: a special entry that names the next configuration and its members. The Replicated_Log_Node in src/replicated_log.odin layers this on the core Node; its entries are an Entry union of the host's Value and a Stop_Sign. From the moment a stop sign is pending on a node, log_propose refuses commands with .Log_Sealed; once the stop is decided in slot $𝑠$, no slot above $𝑠$ is ever released to the application in that configuration, and the next configuration starts at $𝑠+1$ on the same slot line. The full treatment, including how a delayed message from the old configuration is rejected, is in the advanced-features chapter.

3.9 Global Slots on One Line

Application slot numbers form one increasing sequence. Slot :: u64 counts from 1 and never resets: not on a new leader, not on a trim, and not on a configuration change. A decision above a stop sign may be abandoned and its position decided by the next configuration, but that position was never released in the old configuration. What the window bounds is residency, not history: at most WINDOW_SLOTS slots live in protocol memory at a time, and everything below the memory floor survives only in the host's journal and materialized state.

Slot arithmetic saturates rather than wrapping. Chunk limits, batch sizes, and continuation slots go through slot_add, which adds min(offset, max(Slot) - slot), so no calculation can produce slot zero or a small slot from a large one. The only terminal condition is .Global_Slot_Exhausted, returned by propose, propose_batch, campaign, and chunk resolution when the next slot would be max(Slot). It is a stop, not a rollover: restarting the counter in the same log would reuse consensus instances that acceptors may still hold votes for.

4 The Safety Argument

Parts I to III told the story: an empty ledger, a quorum, a ballot, three rules, and a log of decrees. This chapter is the argument in its compact form. It states the model as axioms, defines the words the theorem uses, proves the Synod theorem for one decree in the style of Lamport's Theorem 1, extends it to the multi-decree log, and then walks through every place where paxos-odin does something Lamport's parliament did not. Every lemma names the procedure in src/ that discharges its premise, and the closing table maps each obligation of the package documentation in src/paxos.odin to its lemma, its procedures, and the test or simulator oracle that exercises it. Where the code guarantees less than a sentence in the package documentation suggests, the lemma says exactly what is guaranteed and what the host must add.

4.1 Axioms of the model

• A1 (Processes). A configuration has a fixed, finite set of members. A process runs the library's transitions one at a time and may crash at any instant. A crashed process may restart, and when it does it holds exactly the records it persisted before the crash and nothing else: every field of Node outside the Ledger is volatile and is reset or rebuilt by node_restore, using the ledger and the host's durable consumed floor and configuration.
• A2 (Channels). Envelopes may be lost, duplicated, reordered and delayed without bound, but never forged or corrupted. Every envelope a node processes was sent by envelope.from with the contents it carries; the host authenticates the transport, and node_step refuses an envelope whose from is outside the membership with .Not_Member and one not addressed to the node with .Wrong_Recipient.
• A3 (Quorums). A read quorum ${𝑄}_1$ is any set of read_quorum_size members and a write quorum ${𝑄}_2$ any set of write_quorum_size members, and read_quorum_size + write_quorum_size > count. membership_init refuses any other pair with .Non_Intersecting_Quorums, and replicated_log_init_from_stop builds the next configuration's membership through the same procedure.
• A4 (Durability). The host appends every Write of a transition to stable storage in the order given, syncs, and only then calls confirm_writes_durable; no message of that transition leaves before then, with the single exception of Lemma 10, and no later transition runs before then (effects_reset stops the process otherwise). A confirmed record survives every crash. On restart the host folds its journal in order through ledger_replay_fold (or ledger_apply) and calls node_restore with the slot through which it has durably consumed the log; that consumed floor is itself durable and never decreases. A Committed entry is applied only after the batch that released it is confirmed.
• A5 (No Byzantine behaviour). Every process runs the library's code on its own ledger, never confirms a write that failed, never edits a ledger by hand, and reports its state truthfully in every message.

4.2 Definitions

The words are ordered by strength: applied implies decided on that node, decided implies chosen (Corollary 1), and chosen is the property the theorem is about. Chosen is a fact about durable votes and nothing else; no message, timer or leader is mentioned in D4.

4.3 The Synod theorem for one decree

Fix one decree $𝑠$ throughout this section.

Lemma 1 (quorum intersection). Every read quorum meets every write quorum: ${𝑄}_1\cap {𝑄}_2\ne \varnothing$.

Proof. $|{𝑄}_1\cap {𝑄}_2|\ge \left|{𝑄}_1\right|+\left|{𝑄}_2\right|-𝑁$, and A3 gives $|{𝑄}_1|+\left|{𝑄}_2\right|>𝑁$. The inequality is read + write <= total in membership_init, refused with .Non_Intersecting_Quorums. $∎$

Lemma 2 (a vote respects the promise). If $𝑎$ votes $\left(𝑏,𝑣\right)$ in $𝑠$ then $𝑏\ge {𝑝}_{𝑎}\left(𝑠\right)$ at the moment of the vote, and ${𝑝}_{𝑎}\left(𝑠\right)\ge 𝑏$ ever after. ${𝑝}_{𝑎}\left(𝑠\right)$ never decreases.

Proof. Every vote is recorded by one of two procedures. on_accept replies send_nack and records nothing when msg.ballot < l.promised or msg.ballot < l.promised_at[cell]; when it does record, it first sets l.promised_at[cell] = msg.ballot. send_accept, the proposer's own vote, returns without voting when ballot < ledger_promise_for(l, cell) and otherwise raises promised_at to the ballot. Promises only grow: on_prepare and on_heartbeat nack a ballot below promised and assign only a ballot at or above it; promise_bounded refuses the whole range if any promised_at exceeds the ballot; ledger_apply returns .Promise_Regression for a lower promise or a vote below a promise, and ledger_replay_fold folds with max. Across a restart the ledger is the replayed journal, so the same fields carry the same values (Lemma 9). $∎$

Lemma 3 (one value per ballot). For each ballot $𝑏$ at most one value is ever carried by an Accept_Message for $\left(𝑏,𝑠\right)$, and every vote at $𝑏$ in $𝑠$ is for that value.

Proof. The proposer of $𝑏$ is ballot_node(b), and a node builds ballots carrying only its own id (start_campaign, start_revocation, ownership_ballot). For a campaign ballot, the round is greatest + 1 where greatest covers the node's own ballot, every round it observed, and ledger_highest_ballot (the global promise, every per-decree promise and every vote in the ledger); so each campaign of a node uses a round it never used before (a restart is Lemma 10). Within one campaign, a value enters $𝑠$ only through send_accept, which refuses to re-vote at the same ballot for a different value in a cell it is driving (.Conflicting_Value), and fresh proposals take next_slot, which become_leader sets above every used slot. For the round-zero ballot, on_accept discards any round-zero Accept unless node.ownership holds and ballot_node(msg.ballot) == owner_of(node, msg.slot), and the owner proposes in an own slot once (Lemma 11). On the acceptor's side, on_accept answers a second value at the ballot it already voted with .Conflicting_Value rather than a vote, and ledger_apply does the same on replay. $∎$

Lemma 4 (B3, the max-vote rule). Suppose the proposer of a campaign ballot $𝑏$ issues an Accept for $\left(𝑏,𝑠,𝑣\right)$. Then there is a set ${𝑄}_1$ of at least read_quorum_size acceptors, each of which promised $𝑏$ for $𝑠$ before reporting, such that either (i) a received report supplies a vote $\left({𝑏}^{″},𝑣\right)$ in $𝑠$ whose ballot is at least as high as every vote reported by ${𝑄}_1$, or (ii) no received report supplies a vote in $𝑠$, and $𝑣$ is the no-op or a fresh client value. The selected report in (i) may come from an additional peer whose chunk is not yet complete.

Proof. Every Accept at a campaign ballot is issued by resolve_chunk or, after become_leader, by node_propose and node_propose_batch. resolve_chunk runs only from maybe_resolve_chunk, which returns until complete reaches membership_read_quorum, where a peer is complete when its Promise_Range_Message arrived (range_described) and received_in_range reached the reported count it announced (on_promise_range, on_promise). Each such peer ran on_prepare, which promised the ballot (globally for .Global, per decree through promise_bounded for .Bounded) and then reported every used cell in the chunk above its trim anchor, one Promise_Message per cell, with the cell's vote_ballot, state and value. The candidate's on_promise keeps, per slot, the report with the greatest vote, promotes a .Chosen report over any vote, and returns .Conflicting_Value on two values at one ballot. resolve_chunk then proposes recovered_value[cell] for a slot with a .Voted record and node.noop for a slot with none, which is (i) and (ii) inside the chunk. Reports already received from additional peers can raise the selected ballot, but cannot lower it below the maximum from the complete quorum. recovery_ready freezes this selection before any phase-two vote and keeps it unchanged across a window-limited retry. A fresh value from node_propose lands at next_slot, which become_leader set above ledger_highest_used and both fences; by Lemma 6 no member of the final chunk's ${𝑄}_1$ holds a vote there, which is (ii). $∎$

Theorem 1 (Agreement). If $𝑣$ is chosen in $𝑠$ at $𝑏$ and $𝑤$ is chosen in $𝑠$ at ${𝑏}^{\prime }$, then $𝑣=𝑤$.

Proof. Let ${𝑏}_0$ be the least ballot at which any value is chosen in $𝑠$, and let ${𝑣}_0$ be that value; by Lemma 3 it is unique. It suffices to show that every Accept issued in $𝑠$ at a ballot ${𝑏}^{\prime }>{𝑏}_0$ carries ${𝑣}_0$: then a value chosen at ${𝑏}_0$ is ${𝑣}_0$ by Lemma 3, and a value chosen at ${𝑏}^{\prime }>{𝑏}_0$ is the value of the Accepts its voters answered, again ${𝑣}_0$.

Order Accept events in $𝑠$ by happens-before. Because every execution prefix is finite the order is well founded, and we argue by induction along it. Consider an Accept $𝑒$ for $\left({𝑏}^{\prime },𝑠,𝑢\right)$ with ${𝑏}^{\prime }>{𝑏}_0$ and assume the claim for every Accept in $𝑠$ that happens before $𝑒$.

The round-zero ballot of $𝑠$ is the least integer any acceptor will vote at in $𝑠$ (Lemma 11), so ${𝑏}^{\prime }>{𝑏}_0$ is a campaign ballot, and Lemma 4 gives a read quorum ${𝑄}_1$ whose members promised ${𝑏}^{\prime }$ for $𝑠$ before reporting. ${𝑣}_0$ chosen at ${𝑏}_0$ gives a write quorum ${𝑄}_2$ each of whose members voted $\left({𝑏}_0,{𝑣}_0\right)$ in $𝑠$. By Lemma 1 pick $𝑎\in {𝑄}_1\cap {𝑄}_2$. By Lemma 2, $𝑎$ could not vote at ${𝑏}_0<{𝑏}^{\prime }$ after promising ${𝑏}^{\prime }$ for $𝑠$; so $𝑎$ voted $\left({𝑏}_0,{𝑣}_0\right)$ before it answered the prepare for ${𝑏}^{\prime }$. A cell's vote is replaced only by a vote at a greater ballot (on_accept records only at or above promised_at, which the earlier vote raised, and equality is the same value), and a vote leaves a ledger only for a slot at or below that node's delivered prefix or trim anchor (Lemma 8), in which case $𝑎$'s manifest fences $𝑠$ and $𝑒$ is never issued. So when $𝑎$ answered, it reported a vote $\left({𝑏}_{𝑚},{𝑢}_{𝑚}\right)$ in $𝑠$ with ${𝑏}_{𝑚}\ge {𝑏}_0$, and case (ii) of Lemma 4 is excluded.

By Lemma 4 (i), $𝑢$ is the value of a reported vote $\left({𝑏}_{𝑀},{𝑢}_{𝑀}\right)$ at least as high as every vote reported by ${𝑄}_1$, with ${𝑏}_{𝑀}\ge {𝑏}_{𝑚}\ge {𝑏}_0$. If ${𝑏}_{𝑀}={𝑏}_0$, then ${𝑢}_{𝑀}={𝑣}_0$ by Lemma 3. If ${𝑏}_{𝑀}>{𝑏}_0$, the vote $\left({𝑏}_{𝑀},{𝑢}_{𝑀}\right)$ was cast on receipt of an Accept for $\left({𝑏}_{𝑀},𝑠,{𝑢}_{𝑀}\right)$ that happened before the report, hence before $𝑒$; by the induction hypothesis ${𝑢}_{𝑀}={𝑣}_0$. In both cases $𝑢={𝑣}_0$. If instead some member of ${𝑄}_1$ reported $𝑠$ as .Chosen, resolve_chunk records that decision and issues no Accept in $𝑠$ at all, and the decision is ${𝑣}_0$ by Corollary 1 and the same induction. $∎$

Corollary 1 (decided implies chosen). If any node has decided $𝑠$ with value $𝑣$, then $𝑣$ is chosen in $𝑠$ once the transition's required writes are durable.

Proof. record_commit is reached from four places. on_accepted calls it only when acknowledged[cell] reached membership_write_quorum, counting each member once (bit_set_insert on acknowledgements[cell]), for the ballot and slot the node is driving (lead_slot, lead_ballot), and only when its own cell still holds a vote at that ballot (.Missing_Proposed_Value otherwise); each acknowledgement is an Accepted_Message sent by on_accept after recording a vote at that ballot (or for a cell already holding it), and by Lemma 3 all those votes are for the same value, so they form a ${𝑄}_2$. send_accept calls it directly only when the write quorum is one, where the proposer's own vote is a ${𝑄}_2$. on_commit and node_learn_chosen record a value another node had decided (A2, A5), and resolve_chunk records a value a reporting peer had decided; both carry an earlier decision. Following these reports backward through the finite execution reaches a quorum-backed decision; this induction is over decision events, including repeated reports, rather than over the number of distinct nodes. $∎$

Theorem 1 with Corollary 1 is what the simulator's AGREEMENT oracle checks: it records the first value it sees chosen in each slot, counting durable votes directly in persist_sim_write so that a value chosen by a quorum whose leader then crashes still enters the golden log, and it fails the run if any node ever decides another.

4.4 Extension to the multi-decree log

Lemma 5 (decrees are independent). The ledger state of decree $𝑠$ is the cell cell_of(s, W) while slot[cell] == s, and nothing about $𝑠$ is ever read from a cell tagged with another slot.

Proof. Every read of a cell goes through ledger_cell, ledger_vote_at, ledger_chosen_at or claim_live, each of which compares l.slot[cell] with the slot it was asked about. A cell is retagged only by ledger_open, reached from claim_live (live), ledger_claim (replay) and ledger_clear_cell (restart), and it clears the promise, vote and state as the tag changes. So a vote, promise or decision belongs to one decree, and the Synod argument applies to each decree separately; only the global promised is shared, and sharing a promise can only refuse more votes, never permit one. $∎$

Lemma 6 (one campaign covers every decree above its base). Let a candidate at campaign ballot $𝑏$ become leader. Then for every decree $𝑠\ge$ recover_base there is a set of at least read_quorum_size acceptors that promised $𝑏$ before reporting their votes in $𝑠$, and the reports for $𝑠$ were complete before the candidate proposed in $𝑠$.

Proof. start_campaign sends Prepare_Message{ballot = b, first = recover_base,
last = recover_last} with scope .Global. on_prepare answers only if msg.ballot >= l.promised, sets promised = b, and then reports every used cell with first <= slot <= last above its anchor; it sets more if it holds a used cell above last. A .Global promise covers every decree, so a member that answered the first chunk refuses every lower ballot in every later chunk as well. maybe_resolve_chunk proposes nothing until a read quorum of members is complete for the current chunk; then resolve_chunk drives the chunk and, if any complete member said more, begin_next_chunk resets every Election_Peer except its fences, clears promise_seen, and sends the next Prepare for [last + 1, ...] under the same ballot. Each chunk therefore has its own complete read quorum, and each of its members reported every vote it held in that chunk after promising $𝑏$. When no complete member reports more, no member of that final read quorum holds a vote above last, which is what Lemma 4 (ii) needs for fresh proposals above the last chunk. $∎$

The per-chunk bookkeeping is what lets the candidate tolerate A2: a manifest that overtakes its promises, a duplicated promise, or a chunk answered in two halves changes expected_in_range and received_in_range and nothing else, and the test review_promise_reordering_deduplication_and_validation runs those orders.

Lemma 7 (holes). Filling a hole with the host's no-op is an ordinary proposal and cannot conflict with a chosen value.

Proof. A hole is a slot in the drive range with no recovered vote and no recovered decision; resolve_chunk calls send_accept(node, slot, node.ballot, node.noop.?,
effects), the same procedure as any proposal, and maybe_resolve_chunk refuses to resolve at all with .Missing_Noop if no no-op was recorded. Lemma 4 (ii) holds for the slot, so if any value were chosen there at a lower ballot, its ${𝑄}_2$ would meet the chunk's ${𝑄}_1$ in a member that voted before promising and reported it, a contradiction; and Theorem 1 covers every higher ballot. The no-op is a Value like any other, with no tag, so nothing downstream distinguishes it. $∎$

Lemma 8 (fences and the memory window). A vote or decision leaves an acceptor's ledger only for a slot at or below that acceptor's delivered prefix or trim anchor, and a candidate never proposes at or below the greatest delivered prefix or trim anchor any complete member reported.

Proof. Three procedures drop a slot from a cell. claim_live admits only slots in the live window $($memory_floor,memory_floor+𝑊], so the map from live slots to cells is a bijection and no cell is ever tagged with a slot whose predecessor in that cell is still live; within the window it retags a cell only when held <= node.memory_floor and the cell is .Chosen; node_advance_memory_floor keeps memory_floor <= delivered_through. node_resume_at clears open votes at or below max(floor, anchor.chosen_trim_slot) and sets delivered_through to that value. ledger_claim, on replay, reuses a cell whose slot is .Chosen or at or below the anchor for a later slot, and the later record exists only because the live node had claimed the cell under the first rule. In each case the dropped slot is at or below delivered_through or the anchor of that node, and both travel in every Promise_Range_Message as chosen_through and anchor. quorum_fences takes the maximum over the candidate's own values and every Election_Peer; resolve_chunk starts driving at max(recover_base, fence + 1), and become_leader sets next_slot above both fences. A slot at or below a delivered prefix is decided on that node, hence chosen (Corollary 1), and a slot at or below a trim anchor is chosen by the definition of Trim_Anchor; so fencing forgoes only proposals that Theorem 1 would have forced to carry the chosen value anyway. The leader learns the fenced slots through request_learn instead, and slots below its memory floor come from the host through Serve_Range_Request. $∎$

The fence is not an optimisation. Without it, an acceptor whose vote for a chosen slot had been cleared by node_resume_at could be the only member of ${𝑄}_1\cap {𝑄}_2$, and the candidate would see a hole where a decision lies. review_recovery_preserves_fences_across_chunks and review_snapshot_preserves_votes_above_anchor exercise both fences.

4.5 Durability

Lemma 9 (indelible ink). No promise or vote is observable by another node before it is durable, and a restarted node's ledger contains every promise and vote it ever revealed. Hence Lemma 2 holds across restarts.

Proof. on_prepare, promise_bounded, on_heartbeat, on_accept and send_accept each call effects_add_write before effects_add_message in the same transition, and effects_add_write sets writes_pending. With the default Durability_Gate.Enforced, effects_messages_slice calls host_order_violation, which stops the process, while writes_pending is set, and so does effects_reset, so neither the messages nor the next transition can precede confirm_writes_durable (A4). A restart replays the journal: ledger_replay_fold keeps the greatest promise, every per-decree promise and every vote for a slot still resident, and node_restore installs the result. Volatile bookkeeping is not needed for Lemma 2: the promise and the vote are the ledger. A restart lowers no promise, and the only cells it clears are those Lemma 8 covers. $∎$

The simulator injects a crash at each of Before_Writes, Partial_Writes and Partial_Messages in process_effects, replays the journal into a fresh Ledger through ledger_replay_fold, restores with the consumed floor, and checks PROMISE REGRESSION and VOTE BELOW PROMISE on every record it persists.

Lemma 10 (the pre-durable exception). Let the host transmit, before its barrier, only the envelopes pre_durable_next yields: Accept_Messages whose ballot has round at least one. Theorem 1 continues to hold provided a proposer that crashes with such an Accept in flight campaigns after restart at a round greater than the round of that ballot. start_campaign and start_revocation guarantee this unconditionally: each records the proposer's own promise for the new ballot in the same batch as the Prepare it sends (Write_Promise from start_campaign; the Write_Promise_At records of promise_bounded from start_revocation), and A4 makes that batch durable before any Prepare leaves. The restarted ledger therefore always holds a record at the round of every ballot the proposer ever announced.

Proof. An Accept claims nothing about its sender's durability: it asks acceptors to vote, and each acceptor persists its own vote before answering (Lemma 9). The only record the crash can lose is the proposer's own vote at $\left(𝑏,𝑠\right)$, and a lost vote shrinks the set of votes at $𝑏$; a subset of a ${𝑄}_2$ is not a ${𝑄}_2$, so nothing chosen becomes unchosen. The proposer counts its own vote toward a quorum only in on_accepted, a later transition, which A4 forbids before the vote is confirmed. What Lemma 3 needs is that $𝑏$ is never used again in $𝑠$ for another value. start_campaign and start_revocation compute greatest from ledger_highest_ballot, which scans promised, every promised_at and every vote_ballot; so if any record at the round of $𝑏$ survived, the next ballot has a greater round and the old votes at $𝑏$ are ordinary votes at a lower ballot that Lemma 4 will report. A record always survives: the proposer's own promise for $𝑏$ was written before its Prepare left, and a Prepare precedes every Accept at $𝑏$. $∎$

The exception is unsound at round zero, and pre_durable_next withholds round-zero Accepts for that reason. An owner's ballot is the same integer in every own slot, so after a restart next_usable_own_slot would hand it the same slot again if its vote there were not durable, and it would propose a different value at the same ballot in the same decree. The simulator's vote oracle, which fails a run when one ballot accepts two values in one slot, found exactly that counter-example: an owner reused its ballot for a different value after a crash. With round-zero Accepts behind the barrier, the owner's vote is in ledger_highest_used before any acceptor can see the Accept, and node_resume_at sets own_next above it.

4.6 Rotating ownership

Lemma 11 (ballot partition). Under rotating_ownership, in every decree $𝑠$ the round-zero ballot ownership_ballot(owner_of(node, s)) is the least ballot any acceptor votes at, it belongs to the owner alone, and every other ballot has round at least one; so B1 holds per decree and Lemma 3 applies.

Proof. owner_of is membership_get((s - 1) mod count), a function of $𝑠$ and the fixed membership, so every node computes the same owner. on_accept discards a round-zero Accept unless node.ownership holds and ballot_node(msg.ballot) is that owner. The owner proposes in $𝑠$ through propose_owned, which takes next_usable_own_slot and then moves own_next to own_slot_from(slot + 1), so it proposes once per own slot; after a restart node_resume_at recomputes own_next above ledger_highest_used, which holds the vote (Lemma 10). Every other ballot comes from start_campaign or start_revocation, whose round is greatest + 1 >= 1, and the round occupies the top 40 bits, so any such ballot exceeds any round-zero ballot. $∎$

Lemma 12 (a revocation is a phase one). A revocation at ballot $𝑏$ over the range $\left[𝑓,𝑙\right]$ satisfies the premises of Lemma 4 for every decree in the range, so Theorem 1 holds with round-zero and campaign ballots mixed in one decree.

Proof. start_revocation picks a fresh round and sends Prepare_Message{scope = .Bounded, first = f, last = l} with $𝑙-𝑓<$ CHUNK_SLOTS. on_prepare first nacks a ballot below the global promise, then calls promise_bounded, which walks the range twice: it returns false, and the acceptor sends nothing, if any slot above the memory floor has no live cell or a promised_at above $𝑏$; otherwise it records Write_Promise_At{ballot = b, slot} for every slot in the range before a single Promise_Message leaves. So a member the candidate counts as complete has promised $𝑏$ for every decree of the chunk, which is all Lemma 2 needs in $𝑠$. The reports and maybe_resolve_chunk are unchanged. resolve_chunk runs with drive_all set, so every decree of the range is settled: a recovered round-zero vote is re-proposed at $𝑏$ (B3, the test ownership_revocation_keeps_a_seen_vote), a recovered decision is recorded, a hole takes the no-op. The revoked owner is fenced by promised_at: on_accept nacks its round-zero Accept, and next_usable_own_slot steps over a slot whose effective promise exceeds ownership_ballot(node.id). After the chunk become_leader returns the revoker to .Follower; there is no standing leader to reuse the ballot. $∎$

Lemma 13 (skips). A skip is a proposal of the no-op at the owner's ballot in an own slot.

Proof. skip_idle_slots calls propose_owned(node, noop, effects) for own slots up to highest_seen, at most min(C, SKIP_BURST) per tick; nothing distinguishes the resulting Accept from any other round-zero proposal. $∎$

Lemma 14 (resubmission). A resubmitted suggestion is a new proposal in a new decree and violates nothing.

Proof. queue_resubmit is called from two places, and both key on the ledger alone: on_accept, when a higher ballot's value is about to overwrite the cell's own round-zero vote, and record_commit, when the decided value differs from that vote. The vote's ballot identifies the suggestion, so the check survives a revocation the owner itself started (which clears the lead columns). A suggestion overwritten in on_accept may yet be chosen at the revoker's ballot only if the revoker re-proposed it (Lemma 4), in which case the resubmission decides it twice; that is the at-least-once the host already handles by command id. drain_resubmits proposes it through propose_owned, that is, at the owner's ballot in a later own slot; Lemma 11 applies to that decree. The queue holds one chunk; a burst beyond it is dropped for the host's ordinary retry, so the guarantee is at-least-once only through the host. $∎$

Liveness, informally. A stalled prefix does not stay stalled. tick_ownership counts stall_ticks while delivered_through < highest_seen, asks the owner of the stuck slot for what it knows every heartbeat_interval_ticks, and starts a revocation of the chunk above delivered_through at election_timeout_ticks; a revoker that times out revokes again at a higher round. A live owner either proposes in its slots or skips them (Lemma 13), resend_to retransmits open Accepts and decisions, and emit_contiguous releases the prefix as it fills. None of this is proved here; it is the subject of the simulator's LIVENESS and CONVERGENCE oracles under --ownership.

4.7 Stop signs

Lemma 15 (a decided stop sign seals its configuration). Let stop sign $𝜎$ be chosen at slot $𝑠$ in configuration $𝐾$. Then (i) no node whose ledger holds $𝜎$, voted or decided, admits a new entry into $𝐾$ through replicated_log_propose, replicated_log_propose_batch or replicated_log_propose_stop_sign; (ii) no Replicated_Log_Node of $𝐾$ that has decided $𝑠$ ever releases, reports or reads a slot above $𝑠$, so a value the core nevertheless chooses there is abandoned; (iii) the next configuration continues at $𝑠+1$ on the same slot line, and a message from $𝐾$ cannot act there.

Proof. (i) All three proposal procedures return .Log_Sealed when replicated_log_is_sealed holds, which is stop_pending || stop_sign != nil. replicated_log_recalculate_stop_pending runs after every transition (replicated_log_observe_effects) and after restore (replicated_log_observe_durable); it scans every used cell of the ledger for a Stop_Sign whose configuration_id exceeds the node's own, so a vote for $𝜎$ seals the node as surely as a decision does. (ii) replicated_log_observe_effects first records the earliest decided stop sign and its slot through replicated_log_observe_stop, and then replicated_log_abandon_above_seal cuts effects.committed at the first slot above stop_slot. Releases are contiguous (Lemma 16), so $𝑠$ is released before or together with $𝑠+1$, and the seal is on record before the cut runs in the same call; after a restart replicated_log_observe_durable rediscovers the seal from the .Chosen cells before any transition runs. replicated_log_decided_through reports at most stop_slot, and replicated_log_read and replicated_log_read_decided refuse the first abandoned slot. (iii) replicated_log_init_from_stop builds the membership from $𝜎$ through membership_init and calls replicated_log_continue_at, which starts an empty window with memory_floor = delivered_through = s and next_slot = s + 1, refusing an anchor above $𝑠$ with .Trim_Regression. replicated_log_step_checked compares Log_Envelope.configuration_id with the node's own before the core sees the envelope, and on a mismatch resets the effects and returns .Configuration_Mismatch with no write and no message. $∎$

4.8 Contiguity

Lemma 16 (contiguous delivery). Every Committed entry a node releases is for slot delivered_through + 1 at the moment of release, its value is chosen, and delivered_through then becomes that slot; so the sequence released by one node is $1,2,3,\dots$ from its restart base, with no gap and no repeat.

Proof. emit_contiguous loops from next = delivered_through + 1, stops at the first cell that is not tagged next or not .Chosen, and for each released slot appends Committed{slot = next} and sets delivered_through = next. The one other release is the pass-through in record_commit, taken only when claim_live fails (the slot is just past the live window) and slot == node.delivered_through + 1; it records Write_Chosen, releases exactly that slot, advances delivered_through and then calls emit_contiguous. Record and entry both point at the single pass_through field, so record_commit takes this path at most once per transition: a second such decision in the same batch is dropped and learned again later, never released with the wrong value. Every released value is a .Chosen cell or a value record_commit was about to record, chosen by Corollary 1. After a restart node_resume_at sets delivered_through to the restart base, the host's consumed floor or the trim anchor, whichever is greater, so the host sees the same sequence continue; a slot delivered before the crash but not yet consumed is released again, which is why the host applies idempotently. The standalone Learner gives the same guarantee through released_through in learner_learn_chosen. $∎$

The simulator's CONTIGUITY oracle fails the run if any node releases a slot other than consumed + 1.

4.9 Chunk-local recovery scratch

The volatile recovery arrays and each peer's report bitmap have capacity CHUNK_SLOTS, independently of the durable ledger window. For an active range [recover_base, recover_last], recovery_index first checks range membership, then checks slot - recover_base < CHUNK_SLOTS, and only then converts the offset to an array index. Subtraction is therefore nonnegative and the index is bounded. Distinct slots in the range have distinct offsets. This argument does not require the chunk size to be a power of two or to divide the ledger window.

reset_recovery_chunk invalidates slot tags, states, ballots, and per-peer duplicate bitmaps at a new campaign or chunk. Payload bytes need not be zeroed: they are read only through a valid state and matching absolute slot tag. Delayed reports are rejected by ballot and range before they can access a new chunk's scratch. The cross-chunk trim and chosen-prefix fences are retained separately.

Once enough complete peer manifests constitute a read quorum, recovery_ready freezes the collected selection and recovery_more. This happens before the first phase-two vote. A window-limited retry retains that same selection; a late promise cannot replace a value already issued under this ballot. New chunks clear the freeze. Without this rule, a late higher losing vote could replace a proposal made from an earlier complete read quorum during a partial drive.

Resolution copies selected payloads into ledger-owned storage before emitting borrowed writes and messages. No outgoing effect borrows scratch that will be invalidated by chunk rollover. The refactor changes volatile representation, not journal or wire formats, quorum intersection, or the persistence-before-reply rule.

Tests exercise absolute-slot reference selection, non-power-of-two chunks, ring crossings, stale and duplicate reports, a blocked partial drive, a late promise after that drive, and large payload lifetimes. The simulator additionally exercises small windows with both flexible-quorum extremes and crashes. These are checks of the implementation's correspondence to the argument, not a machine-checked proof.

4.10 Obligations, lemmas, procedures, evidence

5 Bounded Core State Machine

5.1 Design Philosophy: Consensus Without I/O

The library performs no I/O and owns no threads or clocks. Every public transition has the same shape: it mutates the node in place and fills a caller-owned Effects value with what the host must now do. There is no callback, no socket handle, no allocator, and no wall-clock read in src/.

A second host now exists, in another language. The Python package described in Part IX drives exactly this contract across a C boundary: it copies the writes, persists them, confirms, and only then reads the messages and the released entries. Its bridge compiles the core with the host-managed gate and enforces the same order itself, because the enforced gate ends the process and a host inside an interpreter cannot act on that. Nothing about the contract changes; only who is keeping it.

The reason is determinism. Given the same node state and the same event, a transition produces the same mutation and the same batch, whether it runs under odin test, inside the seeded fault simulator in sim/, or behind a real journal and a real socket. A failing simulation prints its seed and can be replayed step for step, because nothing inside a transition depends on time, memory layout, or scheduling. A transition is not a pure function, though, and the in-memory node is not a substitute for the writes it returns: when a call mutates node.ledger, it appends the matching Write record to the batch, and the node's memory is only a cache of what the journal will hold once the host has appended and synced those records.

5.2 Defining the Configuration

Two parametric structs carry the same five parameters. The first is the node.

// One Multi-Paxos participant: proposer, acceptor, and learner in one bounded value.
// Every array is indexed by window cell or by stable member index; there is no
// per-slot struct, so a scan touches only the columns it needs.
//
// The host persists only the ledger, and only through the Write records it receives.
Node :: struct(
    $Value: typeid,
    $MAX_MEMBERS: int = DEFAULT_MAX_MEMBERS,
    $WINDOW_SLOTS: int = DEFAULT_WINDOW_SLOTS,
    $CHUNK_SLOTS: int = DEFAULT_CHUNK_SLOTS,
    $GATE: Durability_Gate = .Enforced,
) where intrinsics.type_is_comparable(Value) {
    id:                                 Node_Id,
    membership:                         Membership(MAX_MEMBERS),
    ledger:                             Ledger(Value, WINDOW_SLOTS),

The defaults live in src/paxos.odin: DEFAULT_MAX_MEMBERS is 7, DEFAULT_WINDOW_SLOTS is 256, and DEFAULT_CHUNK_SLOTS is 64. MAX_MEMBERS bounds the voting membership, WINDOW_SLOTS is the number of slot cells kept in memory, and CHUNK_SLOTS is how many slots one phase-one round recovers at a time (the Multi-Paxos chapter). GATE selects whether the durability contract is checked at runtime; leave it at .Enforced unless you have read the host-managed section.

The second struct is the batch, declared with the same parameters as the node it serves. The compiler rejects a mismatch: the fixture effects_must_match_node in tools/check_contracts.py pairs paxos.Node(u64, 1, 4, 1) with paxos.Effects(u64, 1, 4, 2) and asserts that paxos.campaign(&n, 0, &e) fails to type-check.

// Caller-owned output of one transition. Declare it with the same parameters as the
// Node it serves; the compiler rejects a mismatch. The zero value is ready to use.
//
// Nothing in a batch owns a value: writes, messages, and committed entries point into
// the node's ledger. Capacities are per-transition maxima: one recovery chunk of votes,
// each possibly followed by a local decision, plus one promise; one chunk per peer plus
// prepares, heartbeats, and one catch-up request (an ownership tick proposes at most
// one chunk and retransmits only on a quiet tick); one window plus one pass-through
// entry of decisions.
Effects :: struct(
    $Value: typeid,
    $MAX_MEMBERS: int = DEFAULT_MAX_MEMBERS,
    $WINDOW_SLOTS: int = DEFAULT_WINDOW_SLOTS,
    $CHUNK_SLOTS: int = DEFAULT_CHUNK_SLOTS,
    $GATE: Durability_Gate = .Enforced,
) where intrinsics.type_is_comparable(Value) {
    writes:         small_array.Small_Array(2 * CHUNK_SLOTS + 1, Write(Value)),
    messages:       small_array.Small_Array(
        MAX_MEMBERS * CHUNK_SLOTS + 2 * MAX_MEMBERS + 1, Envelope(Value),
    ),
    committed:      small_array.Small_Array(WINDOW_SLOTS + 1, Committed(Value)),
    requests:       small_array.Small_Array(MAX_MEMBERS, Host_Request),
    // True while this batch holds writes the host has not confirmed durable.
    writes_pending: bool,
}

5.2.1 Compile-time contracts

Capacity mistakes are caught before the program exists. node_init opens with three #assert statements: MAX_MEMBERS must lie in 1..=65535, WINDOW_SLOTS must be a positive power of two, and CHUNK_SLOTS must satisfy 1 <= CHUNK_SLOTS <= WINDOW_SLOTS. Each message carries a Hint: naming the fix, for example "Invalid window. Hint: WINDOW_SLOTS must be a power of two."

The window is a power of two because a slot's cell is one mask, cell_of in src/ballot.odin: (slot - 1) & (WINDOW - 1). MAX_SUPPORTED_MEMBERS is 65535 because a member's index and the node field of a ballot are both 16 bits wide; per-member sets are the library's own Bit_Set(MAX_MEMBERS) from src/bit_set.odin, not a native bit_set, so the member count is not capped at a machine word. The where intrinsics.type_is_comparable(Value) clause on both structs rejects a value type the language cannot compare with ==; the fixture non_comparable_value shows paxos.Node(map[int]int, 1, 4, 1) refused with a diagnostic naming the where clause. tools/check_contracts.py runs nine compile-fail fixtures: a zero window, a zero chunk, a window of 3 slots (window_not_power_of_two), a chunk larger than its window, zero members, a Membership(65536) (too_many_members), a zero learner window, the non-comparable value, and the mismatched batch.

5.2.2 What a Value may be

The where clause on Ledger, Node, and Effects states the rule: Value must be comparable, because it is stored in the ledger's value column and compared with == to detect a conflicting vote or decision. Odin equality compares active union variants and string contents. A fixed-size struct of integers, such as the Command in examples/counter.odin, needs nothing more. Comparability alone does not make a value suitable for replication. A string compares by contents, but a pointer compares by address; that address has no shared meaning on another machine. Prefer self-contained values. If a value refers to external bytes, the host must define consistent equality and encoding, and keep those bytes alive and immutable for every reference held by the protocol.

5.3 The Ledger: Lamport's Variables in Columns

The acceptor state of The Part-Time Parliament is three variables per decree: the greatest ballot promised, the ballot of the last vote, and the value of that vote. The Ledger is those variables laid out as parallel arrays over the window, with a fourth column for the decision and two bitmaps for the scans that phase one and catch-up need:

Ledger :: struct($Value: typeid, $WINDOW: int = DEFAULT_WINDOW_SLOTS)
    where intrinsics.type_is_comparable(Value) {
    promised:    Ballot,
    anchor:      Trim_Anchor,
    slot:        [WINDOW]Slot,
    promised_at: [WINDOW]Ballot,
    vote_ballot: [WINDOW]Ballot,
    state:       [WINDOW]Cell_State,
    value:       [WINDOW]Value,
    // Bitmaps over cells: `used` has a vote or a decision, `chosen` has a decision.
    used:        Bit_Set(WINDOW),
    chosen:      Bit_Set(WINDOW),
}

promised is Lamport's maxBal, one global promise that covers every decree at or above the base of the campaign that made it. promised_at[c] is a per-decree promise, used only by bounded prepares under rotating ownership; the effective promise of a cell is the larger of the two (ledger_promise_for). vote_ballot[c] and value[c] are maxVBal and maxVal. state[c] is a Cell_State: .Empty, .Voted, or .Chosen, and once a cell is .Chosen its value is the decision. slot[c] tags which slot owns cell c, so a reused cell is never mistaken for an older one. The anchor is the chosen-trim record covered in the next chapter:

// The trim anchor: every slot at or below `chosen_trim_slot` is chosen and has been
// folded into a host state image identified by `trim_id`. The core compares anchors
// by identity; the host binds the image's checksum to the id itself.
Trim_Anchor :: struct {
    trim_id:          u64,
    chosen_trim_slot: Slot,
}

Four queries read the ledger without touching the node. ledger_vote_at(l,
slot) returns (Ballot, ^Value, bool) for a cell in state .Voted; ledger_chosen_at(l, slot) returns (^Value, bool) for a .Chosen cell; ledger_highest_used(l) walks the used bitmap for the greatest slot held; and ledger_highest_ballot(l) returns the greatest ballot anywhere in the ledger, which a campaign must exceed. node_ledger(&node) hands the host a ^Ledger(Value, WINDOW_SLOTS) for inspection.

5.4 The Effect Contract

A batch carries four kinds of output. Writes are the durable records:

// The durable records the host journals, in order. Values are referenced, not copied:
// a pointer is valid until the next transition on the node that produced it, and a
// host persists every write before it runs another transition.
Write_Promise :: struct {
    ballot: Ballot,
}

// A promise for one decree only (a revocation under rotating ownership).
Write_Promise_At :: struct {
    ballot: Ballot,
    slot:   Slot,
}

Write_Vote :: struct($Value: typeid) {
    ballot: Ballot,
    slot:   Slot,
    value:  ^Value,
}

Write_Chosen :: struct($Value: typeid) {
    slot:  Slot,
    value: ^Value,
}

Write_Trim :: Trim_Anchor

Write :: union($Value: typeid) {
    Write_Promise,
    Write_Promise_At,
    Write_Vote(Value),
    Write_Chosen(Value),
    Write_Trim,
}

Messages are Envelope(Value) values, each with a from, a to, and a Message(Value) union holding one of the nine wire messages from the protocol chapter. The three that carry a value do so by pointer: Promise_Message(V){ballot, slot, vote, state, value: ^V}, Accept_Message(V){ballot, slot, value: ^V}, and Commit_Message(V){slot, value: ^V}; message_value(message) returns that pointer and whether the kind carries one. Committed entries are Committed(Value){slot, value: ^V}, released in slot order without gaps. Requests are Host_Request values; today the union has one variant, Serve_Range_Request{peer, first, count}, which asks the host to serve history below this node's memory floor from its own journal or state image.

5.4.1 Values travel by pointer

Nothing in a batch owns a value. A Write_Vote, an Accept_Message, and a Committed entry all point at the value column of the ledger cell the transition just wrote. The rule is stated at the top of src/messages.odin:

// Wire messages. Every variant is small and fixed-size; a value travels by pointer.
// Outbound, the pointer refers into the sending node's ledger and stays valid until
// that node's next transition, so a host serialises before then. Inbound, the host
// points it at the decoded value for the duration of the `step` call. An in-process
// transport that queues envelopes copies the value at enqueue time, as a codec would.

A real host serialises each write and each message before it steps the node again, and the copy happens inside its codec. An in-process transport has no codec, so it copies the value itself when it queues an envelope. The counter example names that pair a Packet:

// An envelope in flight. A message points at a value inside the sender's ledger, so a
// transport copies the value when it queues the envelope, exactly as a codec would.
Packet :: struct {
    envelope: paxos.Envelope(Command),
    value:    Command,
}

packet_of :: proc(envelope: paxos.Envelope(Command)) -> (packet: Packet) {
    packet.envelope = envelope
    if value, carries := paxos.message_value(envelope.message); carries do packet.value = value^
    return
}

packet_envelope :: proc(packet: ^Packet) -> paxos.Envelope(Command) {
    envelope := packet.envelope
    #partial switch &m in envelope.message {
    case paxos.Promise_Message(Command): m.value = &packet.value
    case paxos.Accept_Message(Command):  m.value = &packet.value
    case paxos.Commit_Message(Command):  m.value = &packet.value
    }
    return envelope
}

packet_of copies the value out at enqueue time; packet_envelope points the message back at the packet's own copy for the duration of the step call. The same idiom, generic over the value type, is Packet(V) in tests/harness.odin. The one exception to "into the ledger" is a decision for the slot just past the window edge: record_commit releases it through the node's pass_through field, which is why the committed list has room for WINDOW_SLOTS + 1 entries. The pointer rule is the same either way: valid until the node's next transition.

5.4.2 The host commit sequence

The host consumes one batch in a fixed order. The counter's host_commit (the examples chapter) is this sequence with the journal left out:

err := paxos.step(&node, envelope, &effects)
if err != .None { /* see the section on errors */ }

// 1. Append every write, in slice order, copying each referenced value; then sync.
for w in paxos.writes_slice(&effects) do journal_append(&journal, w)
journal_sync(&journal)

// 2. Only now may anything leave the process.
paxos.confirm_writes_durable(&effects)

// 3. Transmit, copying each referenced value into the wire encoding.
for envelope in paxos.messages_slice(&effects) do transport_send(envelope)

// 4. Apply decided entries in slot order.
for entry in paxos.committed_slice(&effects) do apply(&state, entry.slot, entry.value^)

// 5. Serve history a peer asked for from below the memory floor.
for request in paxos.requests_slice(&effects) {
    switch r in request {
    case paxos.Serve_Range_Request: serve_from_journal(&journal, r.peer, r.first, r.count)
    }
}

journal_append, journal_sync, transport_send, apply, and serve_from_journal are the host's own procedures; the library supplies none. Two consequences of the order are easy to miss: a committed entry is applied only after its Write_Chosen record is durable, because step 4 follows step 2; and the next transition on the same batch calls effects_reset, so the whole sequence must finish, and every pointer must have been followed, before the node is stepped again.

Once the host has durably consumed a released prefix, it calls paxos.advance_memory_floor(&node, through), which licenses reuse of the cells at or below through. A host that never advances the floor eventually receives .Window_Full from every proposal; that is backpressure, not a bug in the log.

5.4.3 The runtime gate

With the default .Enforced gate, reading the messages or resetting the batch while writes_pending is still true stops the process:

-- DURABILITY ORDER VIOLATION --------------------------------------------------

messages_slice before confirm_writes_durable.

Hint: Persist and sync the pending writes before calling confirm_writes_durable(),
then transmit messages and reset the batch. Never confirm a failed write.
Recover from the durable journal before restarting this stopped node.

host_order_violation prints this, or the variant reset discarded unconfirmed
writes, and calls os.exit(1); it is declared -> !. The check is a when G == .Enforced branch, not a debug assertion, so it is present in optimised builds; tools/check_contracts.py builds each of its four durability fixtures with -debug and again with -o:speed and requires the named diagnostic and a Hint: line in both. Because every transition begins with effects_reset, a host that forgets confirm_writes_durable is stopped at its next call even if it never reads the messages.

The zero value of Effects is ready to use; the fixture zero_value_is_ready resets and reads a fresh batch with no initialisation call. Two procedures clear a batch. effects_init (paxos.init(&effects)) clears without checking the gate, for fresh memory or for a batch a crashed process can never complete; the simulator calls it after a simulated crash. effects_reset (paxos.reset(&effects)) clears after checking the gate, and every transition calls it on entry.

Two further queries help a host tune its storage. requires_power_loss_barrier is true when the batch carries a Write_Promise, a Write_Promise_At, or a Write_Vote; decision and trim records are derived state a host may persist with a cheaper barrier. pre_durable_messages returns an iterator whose pre_durable_next yields only Accept_Message envelopes whose ballot has a round above zero, the class the library documents as pipelinable before the local sync barrier completes. The comment explains the exclusion:

// Accept requests at a campaign ballot may leave before the local barrier: they ask peers
// to persist a vote and claim nothing about the sender's own durability, and a restarted
// proposer always campaigns at a fresh ballot. An owner's round-zero suggestion is the
// exception: its own vote is the only durable record that the instance was used, so it
// must wait for the barrier or a restart could reuse the ballot for another value.

The gate does not check this iterator, so a host that uses it takes on the reasoning itself.

5.4.4 The host-managed exception

A host that groups several transitions behind one storage barrier may declare its node and batch with GATE = .Host_Managed. That removes the runtime check and transfers the obligation to the host. The rules are written on the type:

// .Host_Managed disables that check for hosts that own the durability boundary
// themselves, for example by grouping several transitions behind one storage barrier.
// Such a host must guarantee, by construction, that:
//   1. every write of a transition is durable before any message of that transition
//      reaches a peer;
//   2. a batch is never discarded while it still holds unconfirmed writes;
//   3. committed entries are applied only after their commit record is durable;
//   4. a crash between the writes and the barrier is recovered from the journal, never by
//      confirming writes that did not complete.
Durability_Gate :: enum {
    Enforced,
    Host_Managed,
}

The spelling is deliberately searchable. For an example, read paxos.Node(u64, 1, 64, 16, .Host_Managed) and its Effects in tests/test_durability.odin. Search for .Host_Managed when auditing callers; each use takes on the same obligations.

5.5 The Public Transition Surface

src/paxos.odin groups each verb over its receiver types, so paxos.propose dispatches on whether the first argument is a ^Node or a ^Replicated_Log_Node. The table gives the Node signatures; parameter order matches the source.

Queries read plain fields and never touch the batch:

5.6 Node_Options and What Zero Means

init takes an optional Node_Options whose zero value selects every default, so paxos.init(&node, id, membership) and paxos.init(&node, id, membership,
paxos.Node_Options{priority = 2}) both read naturally.

Node_Options :: struct {
    // Breaks ballot ties between rounds: higher wins. Zero is the lowest priority.
    priority:                           u8,
    // Follower ticks without leader contact before it campaigns. Zero means the default.
    election_timeout_ticks:             u32,
    // Leader ticks between heartbeat broadcasts. Zero means the default.
    heartbeat_interval_ticks:           u32,
    // Leader ticks between bounded retransmission scans. Zero means the default.
    resend_interval_ticks:              u32,
    // Refuse proposals with .Leader_Catching_Up until every inherited slot is delivered.
    gate_proposals_on_inherited_prefix: bool,
    // Start as an acceptor that promises and votes but never campaigns.
    campaign_disabled:                  bool,
    // Rotating slot ownership: every member proposes in its own slots without phase one.
    // Campaigns are refused; stalls are repaired by bounded revocations.
    rotating_ownership:                 bool,
}

The timer defaults are 10 election ticks, 3 heartbeat ticks, and 10 resend ticks. A tick is whatever interval the host calls tick at; the library never reads a clock. priority is a u8 because it occupies eight bits of the packed ballot; rotating_ownership selects the second way to lead, which has its own chapter.

5.7 Restoring State After a Crash

A restarted process has an empty Node and a journal of Write records. Two procedures fold records into a Ledger. ledger_apply is strict: a promise lower than the current one is .Promise_Regression, two values under one ballot and slot are .Conflicting_Value, a second value for a chosen slot is .Conflicting_Commit, a record addressing a cell still held by an earlier slot is .Window_Overrun, and an anchor that moves backward is .Trim_Regression; use it for one configuration's journal, where each of these is corruption. ledger_replay_fold is for a lifetime journal: promises fold to their maximum, a vote whose cell has since been claimed by a newer slot is skipped as dead history, and decisions and trim records keep the strict rules.

Because a Write_Vote or Write_Chosen carries a pointer, the journal must hold the value alongside the record and point the record back at it during replay. tests/harness.odin is the reference pattern:

// One journaled record with its value copied out of the ledger.
Journal_Record :: struct($Value: typeid) {
    write: paxos.Write(Value),
    value: Value,
}

journal_append :: proc(journal: ^[dynamic]Journal_Record($V), writes: []paxos.Write(V)) {
    for w in writes {
        record := Journal_Record(V){write = w}
        #partial switch x in w {
        case paxos.Write_Vote(V):   record.value = x.value^
        case paxos.Write_Chosen(V): record.value = x.value^
        }
        append(journal, record)
    }
}

// Rebuilds a ledger from a journal with the lifetime fold.
journal_replay :: proc(
    journal: []Journal_Record($V),
    ledger: ^paxos.Ledger(V, $W),
) -> paxos.Error {
    for &record in journal {
        write := record.write
        #partial switch &x in write {
        case paxos.Write_Vote(V):   x.value = &record.value
        case paxos.Write_Chosen(V): x.value = &record.value
        }
        paxos.ledger_replay_fold(ledger, write) or_return
    }
    return .None
}

The simulator's restart path does the same fold inline and then restores every derived frontier:

    // Replay the lifetime journal into fresh durable state, then restore every derived frontier.
    ledger: paxos.Ledger(u64, SIM_WINDOW)
    for &record in small_array.slice(&sim.journals[node_idx]) {
        write := record.write
        #partial switch &w in write {
        case paxos.Write_Vote(u64):   w.value = &record.value
        case paxos.Write_Chosen(u64): w.value = &record.value
        }
        sim_check(paxos.ledger_replay_fold(&ledger, write))
    }
    options := paxos.Node_Options{priority = u8(node_idx), rotating_ownership = sim.config.ownership}
    floor := sim.consumed[node_idx]
    sim_check(paxos.restore(&sim.nodes[node_idx], id, sim.membership, ledger, floor, options))

Four restore procedures differ in what they keep and what they clear:

• restore(node, id, membership, ledger, floor = 0, options = {}) runs init first, so every volatile field starts fresh: role .Follower, zero ballot, no leader hint, no election state. It installs ledger, clears every cell at or below max(floor, ledger.anchor.chosen_trim_slot) that holds only an open vote, and resumes memory_floor and decided_through at that base. floor is the slot through which the host has durably consumed the log; zero for a node that never released anything.
• continue_at(node, id, membership, floor, anchor, options = {}) starts an empty node on the same slot line with an inherited trim anchor, for a configuration handover or a state-image install; .Trim_Regression if the anchor lies above floor.
• begin_recovery(node, anchor) acts on a live node. It applies the anchor through ledger_apply, clears open votes at or below it, and drops the node to .Follower with its election state cleared. It keeps the promised ballot and every vote or decision above the anchor, because such a vote can belong to a chosen quorum this node has not yet learned about. It takes no batch, so the host persists the image and anchor itself before stepping the node again.
• restore_learner(node, id, membership, ledger) rebuilds a non-voting learner from its decision-only journal.

None of these restores application state, client sessions, or transport queues. The host restores its state image and applied slot from its own durable data and replays committed records above that slot idempotently before serving.

5.8 Errors

Every transition returns an Error; .None is zero, so if err != .None is the whole test. The enum in src/errors.odin groups its members as membership, input and addressing, role and capability, liveness and progress, durability and safety, and replicated-log and window errors. Not every error is retryable: .Not_Leader and .Window_Full describe a state the host can wait out, while .Conflicting_Commit and .Promise_Regression are safety incidents whose hints tell the operator to stop and keep the evidence. explain_error returns an operator-facing banner for each; the table EXPLANATIONS is indexed by the enum, so a value without an entry fails the exhaustive test in tests/test_errors.odin. This is the text for .Not_Leader:

-- NOT LEADER ------------------------------------------------------------------

This node has not completed phase one for its current ballot.
Hint: Route to current_leader() or wait for a successful campaign.

The counter example passes that string as the message of an assert; a host logs it and decides on retry or shutdown by the error's group.

6 Advanced Replicated Log Features

6.1 Logical Time

The core owns no clock. Safety never depends on time, but liveness needs a way to suspect a silent leader, remind followers that a leader is alive, and resend what was lost. The host converts elapsed time into calls to tick(&node, noop, &effects) at whatever cadence it chooses, and three intervals in Node_Options are measured in those calls:

    // Follower ticks without leader contact before it campaigns. Zero means the default.
    election_timeout_ticks:             u32,
    // Leader ticks between heartbeat broadcasts. Zero means the default.
    heartbeat_interval_ticks:           u32,
    // Leader ticks between bounded retransmission scans. Zero means the default.
    resend_interval_ticks:              u32,

DEFAULT_ELECTION_TIMEOUT_TICKS   :: 10
DEFAULT_HEARTBEAT_INTERVAL_TICKS :: 3
DEFAULT_RESEND_INTERVAL_TICKS    :: 10

The zero value of Node_Options selects every default, so paxos.init(&node, id, membership) and paxos.init(&node, id, membership, {election_timeout_ticks = 20}) both read naturally. A non-voting node returns from tick at once: it has nothing to suspect and nothing to resend.

For a voter, one tick increments election_ticks, heartbeat_ticks, and resend_ticks (saturating, never wrapping), then acts by role:

1. A leader whose heartbeat_ticks reached heartbeat_interval_ticks broadcasts Heartbeat_Message{ballot, decided_through} to its peers. The heartbeat carries the leader's delivered prefix, so a follower can see that it is behind without any extra message kind.
2. A leader whose resend_ticks reached resend_interval_ticks calls resend_to for every peer. If the peer has reported a decided prefix above the leader's own, resend_to first sends it a Learn_Message, because leadership does not imply knowing every decision. Then it walks the ledger's used bitmap with bit_set_next from a per-peer cursor (resend_cursor), skipping cells at or below what the peer has already decided, resending a Commit_Message for a .Chosen cell and an Accept_Message for a .Voted cell this leader is driving under its current lead_ballot, and stops after CHUNK_SLOTS messages or one complete sweep. It wraps at most once and never visits the same used cell twice in that sweep. The cursor keeps its position, so a quiet peer cannot pin every retry to the first chunk.
3. A candidate still in .Preparing before its timeout retries maybe_resolve_chunk, for the case where the window could not hold the whole chunk the first time.
4. A follower, or a candidate whose election timed out, with election_ticks at or past election_timeout_ticks starts a campaign with the noop passed to this tick, provided campaigning is enabled. The timeout is suspicion, not proof: the old leader may be alive and partitioned.

A node with rotating_ownership set takes a different path, tick_ownership in src/ownership.odin, after the counters advance; the ownership chapter walks it. election_ticks resets whenever the node observes a leader (observe_leader): on a global Prepare, an Accept at a round above zero, a Commit, or a Heartbeat. The heartbeat handler has one more job:

    // A heartbeat above the promise means this node missed the leader's prepare.
    // Promising is always safe, and it stops a needless election.
    if msg.ballot != l.promised {
        l.promised = msg.ballot
        effects_add_write(effects, Write_Promise{msg.ballot})
    }
    observe_leader(node, from, msg.ballot)
    if msg.decided_through > node.delivered_through do request_learn(node, from, effects)

A follower that never saw the winning Prepare, perhaps because it was partitioned during the election, adopts the heartbeat's ballot by promising to it, and the promise is written to ledger.promised and to the batch before anything else happens, exactly as in phase one. A heartbeat below the follower's promise gets a Nack_Message instead, which tells a stale leader to step down. request_learn asks for one chunk from delivered_through + 1.

6.2 Taking Over: The Term Base

Winning phase one does not leave an idle log. The new leader is re-proposing recovered votes, filling holes with the no-op, and possibly learning slots below the chosen fence from a peer. New proposals go above all of that. become_leader records the boundary: it raises next_slot past the greatest used slot and both fences, and leader_base is the first slot this leadership may fill with a fresh value, while next_slot, reported by proposal_frontier, is the slot the next proposal would take. Right after the election they are equal.

A host whose values are independent of each other may pipeline straight through the takeover. A host whose values depend on applied state (a compare-and-swap, a hash chain, a sequence number derived from the last applied entry) cannot: the inherited slots below leader_base will decide ahead of any new proposal, and a value derived before they are applied is derived from the wrong state. Such a host delivers through leader_base - 1 first. The option gate_proposals_on_inherited_prefix makes the core enforce this in propose and propose_batch, through the shared proposal_gate:

@(private)
proposal_gate :: proc(node: ^Node($V, $M, $W, $C, $G)) -> Error {
    if !node.voting_member do return .Not_Voter
    if node.ownership do return .None
    if node.role != .Leader do return .Not_Leader
    if node.gate_proposals_on_inherited_prefix && node.delivered_through < node.leader_base - 1 {
        return .Leader_Catching_Up
    }
    return .None
}

The option is off by default. With or without it, is_leader_caught_up(&node) reports whether delivered_through has reached leader_base - 1. This resolves the prediction: propose returns .Leader_Catching_Up, and it succeeds once the Learn_Message sent during recovery has been answered and slots 10 through 12 are delivered.

6.3 Flexible Quorums

Phase one needs a read quorum of promises; phase two needs a write quorum of votes. The single-decree argument only requires that every read quorum intersect every write quorum, so that a later ballot's phase one sees at least one vote from any earlier ballot's phase two. With uniform sizes over $𝑁$ members, that is

Two write quorums need not intersect: within one ballot the leader proposes one value per slot, and across ballots the read quorum does the intersecting. The library validates the sizes when the membership is built:

// Validates and installs a membership. Zero overrides select majorities.
membership_init :: proc(
    m: ^Membership($MAX_MEMBERS),
    node_ids: []Node_Id,
    read_quorum_override: int = 0,
    write_quorum_override: int = 0,
) -> Error {

Zero means a majority. A size outside 1..=N is .Invalid_Read_Quorum or .Invalid_Write_Quorum; a pair whose sum does not exceed $𝑁$ is .Non_Intersecting_Quorums, and the caller's membership is left untouched. For five voters:

A smaller write quorum buys cheaper commits and pays for them at the next election. Choose the pair for the failure you expect to be common, and let membership_init check it:

m: paxos.Membership(5)
ids := [5]paxos.Node_Id{1, 2, 3, 4, 5}
err := paxos.membership_init(&m, ids[:], 4, 2) // Q1 = 4, Q2 = 2

Every membership_* query takes a ^Membership. Up to LINEAR_LOOKUP_LIMIT (8) members, membership_index_of scans the members in order; above that it binary-searches them, which works because membership_init sorted them, so a membership near the 65535 bound is still one lookup per message.

6.4 Reconfiguration: The Stop-Sign Invariant

A configuration is a voter set, a pair of quorum sizes, and a configuration id. The application must see one sequence across configuration changes. A stop sign fixes which prefix belongs to the old configuration; the next configuration owns the application sequence after that boundary. Replicated_Log_Node wraps the core Node with entries that are either a command or a stop sign:

// One log entry: an application command or a sealing stop sign.
Entry :: union(
    $Value: typeid,
    $MAX_MEMBERS: int = DEFAULT_MAX_MEMBERS,
    $MAX_METADATA_BYTES: int = DEFAULT_MAX_METADATA_BYTES,
) {
    Value,
    Stop_Sign(MAX_MEMBERS, MAX_METADATA_BYTES),
}

Replicated_Log_Node takes Value, MAX_MEMBERS, WINDOW_SLOTS, CHUNK_SLOTS, MAX_METADATA_BYTES, and GATE, and holds a core node over that union plus four seal fields: configuration_id, stop_sign, stop_slot, and stop_pending. Its effects type is Effects(Entry(Value, MAX_MEMBERS, MAX_METADATA_BYTES), MAX_MEMBERS, WINDOW_SLOTS, CHUNK_SLOTS, GATE), and its durable state is the core's Ledger(Entry(Value, MAX_MEMBERS, MAX_METADATA_BYTES), WINDOW_SLOTS), which log_restore takes and replicated_log_ledger (the ledger proc group) returns. A Stop_Sign carries the next configuration_id, the next member list, and up to MAX_METADATA_BYTES of opaque handover metadata, for example the identifier of a state image the new members must install.

6.4.1 Proposing the stop

log_reconfigure(&log, next_configuration_id, next_members, metadata, &effects) is replicated_log_propose_stop_sign under a shorter name. It refuses an id that is not strictly greater than the current one with .Configuration_Id_Regression, validates the member list and metadata size through stop_sign_create, and proposes the stop sign through the ordinary node_propose. To the host it is one more entry in the pipeline; to the log it is the last one.

The seal starts early on purpose. The proposer is sealed the moment log_reconfigure returns, because its proposal is its own vote in the ledger; an acceptor is sealed the moment it votes for the stop. If the stop is later overtaken (a higher ballot re-proposes that slot with a command, as recovery may) the pending flag is recomputed after every transition (replicated_log_observe_effects) and the seal clears. This local gate stops new proposals as soon as the node knows a stop is pending. Other owners may still decide later slots before learning the stop; the release rule below excludes those slots from the application log.

6.4.2 Observing the decision

Once the stop sign commits, log_stop_sign(&log) returns it with true and log_stop_slot(&log) returns its slot. After a crash, log_restore takes the replayed Ledger and rediscovers a committed stop by walking the ledger's chosen bitmap; log_pending_stop_sign(&log) also reports an undecided one held in a used cell, so a host can resume its own handover phase without guessing.

The library decides where the boundary is. It does not move application state, start processes, or stop old traffic. The host waits for the decided stop, delivers every slot through it, transfers whatever the metadata names, and then starts the new configuration:

stop, sealed := paxos.log_stop_sign(&old)
if sealed {
    stop_slot := paxos.log_stop_slot(&old)
    anchor := paxos.Trim_Anchor{trim_id = 1, chosen_trim_slot = stop_slot}
    err := paxos.log_init_from_stop(&next, id, stop, stop_slot, anchor)
}

log_init_from_stop(node, id, stop, stop_slot, anchor, options = {}) builds the membership from the stop sign's members, takes its configuration id, and calls log_continue_at with stop_slot as the floor: the new node's delivered_through and memory_floor are stop_slot, and its next_slot is stop_slot + 1. The slot line does not restart; the first command of ${𝐶}_2$ takes slot $𝑠+1$. An id that is not among the stop sign's members is refused with .Not_Member, which is how a removed voter learns it is no longer one. An anchor above the floor is .Trim_Regression.

6.4.3 Fencing old traffic

A message from ${𝐶}_1$ may still be in flight when ${𝐶}_2$ starts, and a node that has not heard about the stop may keep sending. A bare Envelope carries no configuration, so the log offers Log_Envelope: a configuration_id next to the core envelope. On the way out, log_envelope(&log, message) stamps each outbound envelope with the sender's current configuration id. On the way in, log_step given a Log_Envelope is the checked overload (replicated_log_step_checked): it compares the stamp to the node's own id before the core sees the message, and on a mismatch resets the effects and returns .Configuration_Mismatch with no writes and no messages. The plain Envelope overload is for transports that already keep configurations apart.

for message in paxos.messages_slice(&effects) {
    deliver(paxos.log_envelope(&log, message))
}
// On the receiving node:
err := paxos.log_step(&log, stamped, &effects)
if err == .Configuration_Mismatch {
    // Stale traffic; nothing was written or sent. Drop it.
}

Do not relabel old traffic with the new id to make it pass. A vote cast under ${𝐶}_1$'s quorum rules is not a vote under ${𝐶}_2$'s. Under rotating ownership the member list also fixes which slots each member owns (owner_of deals the slot line in membership order), so a membership change is a stop sign there too. And because another owner may get a suggestion decided above the stop sign before it learns of the seal, the log abandons every decision above a decided stop sign: replicated_log_observe_effects cuts them from the released batch, the read procedures report them undecided, and the next configuration decides those slots afresh. The ownership chapter returns to this.

6.5 Catch-Up and Reconciliation

A node that missed traffic does not enter a special recovery mode. It asks a peer for decisions with Learn_Message{from_slot, count}, and on_learn answers by walking the ledger's chosen bitmap and sending a Commit_Message for every decision in that range that is still in its window. If any part of the range lies at or below the answering node's memory_floor, that part has left protocol memory, and the node emits a Serve_Range_Request{peer, first, count} in effects.requests for exactly that part: the host serves it from its own journal or state image, because the library never reads history it has released. A from_slot of zero, or a count of zero or above CHUNK_SLOTS, is .Invalid_Slot, so one request never asks for more than one chunk. Three entry points send a Learn_Message:

1. request_catch_up(&node, peer, from_slot, &effects) asks peer for one chunk from from_slot. The host calls it when it knows it is behind, and again as its prefix advances.
2. reconnected(&node, peer, &effects) is the host's signal that a link came back. A leader answers by running resend_to for that peer; a follower whose leader_hint is that peer asks it for decisions from delivered_through + 1.
3. The core sends one itself when a heartbeat, an election manifest, or a resend sweep reveals a peer that has decided further than this node.

The last case relies on peer_decided_through, one slot per member, which node_step updates from every message that reports progress:

// The sender's decided prefix, when the message kind reports it.
@(private)
message_decided_through :: #force_inline proc(message: Message($V)) -> (Slot, bool) {
    #partial switch msg in message {
    case Accepted_Message:      return msg.decided_through, true
    case Heartbeat_Message:     return msg.decided_through, true
    case Nack_Message:          return msg.decided_through, true
    case Promise_Range_Message: return msg.chosen_through, true
    case Prepare_Message:       return msg.first - 1, true
    case Learn_Message:         return msg.from_slot - 1, true
    }
    return 0, false
}

The leader uses it to skip resends a peer no longer needs and to notice when a peer is ahead of it. Decisions may arrive out of order; each is recorded in its cell and only the contiguous prefix is released by emit_contiguous.

6.6 Trim Anchors and State Images

The window bounds residency; the host's journal holds the rest. A journal cannot grow forever either, so the cluster periodically agrees that everything through some slot is captured in a state image, and acceptors then answer phase one for that prefix from the anchor instead of from cells:

// The trim anchor: every slot at or below `chosen_trim_slot` is chosen and has been
// folded into a host state image identified by `trim_id`. The core compares anchors
// by identity; the host binds the image's checksum to the id itself.
Trim_Anchor :: struct {
    trim_id:          u64,
    chosen_trim_slot: Slot,
}

The anchor carries no hash. The core compares anchors by identity only: two anchors with the same trim_id must be the same anchor. A host that wants to verify a state image binds a monotonically increasing trim_id to the image's checksum in the durable record that chose the trim. A raw checksum is not a suitable sequence number: a later checksum can be numerically smaller and would fail the trim-regression check. How the anchor is chosen is the host's business; the natural way is to put the trim record in the log as an ordinary command, ordered with everything else. Once the host knows the record is chosen, it calls install_chosen_trim(&node, anchor, &effects). The call refuses an anchor above delivered_through with .Invalid_Slot, and a lower trim_id, a different anchor under the same trim_id, or a lower chosen_trim_slot with .Trim_Regression; the same anchor again is .None with nothing written. Otherwise it emits Write_Trim for the journal, adopts the anchor into ledger.anchor, and raises memory_floor to the anchor slot, never past delivered_through.

From then on the anchor travels with the node. on_prepare skips cells at or below it and reports it in Promise_Range_Message.anchor; on_accept ignores votes for slots at or below it; and a candidate folds every reported anchor into the trim fence (quorum_fences), so no new leader can propose into a trimmed prefix.

A node so far behind that the slots it needs are below the cluster's anchor cannot catch up from decisions. Its host fetches the state image, verifies it against the anchor, persists it, and calls begin_recovery(&node, anchor):

// Installs a certified state image at `anchor`, keeping votes and decisions above it. The
// host must persist the image and the anchor before running further transitions.
node_begin_recovery :: proc(node: ^Node($V, $M, $W, $C, $G), anchor: Trim_Anchor) -> Error {
    node_assert_valid(node)
    ledger_apply(&node.ledger, Write_Trim(anchor)) or_return
    node.leader_hint = nil
    node.election_ticks, node.heartbeat_ticks, node.resend_ticks = 0, 0, 0
    node.peer_decided_through = {}
    node.resend_cursor = {}
    node.role = .Follower
    clear_election(node)
    node_resume_at(node, anchor.chosen_trim_slot)
    return .None
}

node_resume_at clears every open vote at or below the anchor; every vote and decision above it is kept, because a vote above the anchor may already be part of a quorum that a future election must find. The node returns to .Follower with an empty election state and a floor at the anchor. begin_recovery emits no effects: the host must have persisted the image and the anchor before the call, since the node now answers phase one from them.

continue_at(&node, id, membership, floor, anchor) is the same idea for a node that starts empty rather than repairing in place: a fresh voter joining at a known floor, or the next configuration after a stop sign, which is what log_init_from_stop calls. An anchor above the floor is .Trim_Regression there too.

6.7 Non-Voting Learners

Some processes need the decided sequence and nothing else: a read replica, an indexer, an auditor. Two shapes are available.

The first is a core Node initialized with node_init_learner(&node, id, membership). Its id must be non-zero and lie outside the voting membership, otherwise .Invalid_Node_Id or .Learner_Is_Voter. It never promises, votes, or campaigns; node_step accepts only Commit_Message from a member and returns .Learner_Message_Forbidden for every other kind, and tick does nothing. A host that has certified a decision by some other path installs it with learn_chosen(&node, from, slot, value, &effects), which is .Not_Learner on a voter and .Not_Member if from is not a member. The node releases the contiguous prefix through effects.committed exactly as a voter does; Replicated_Log_Node offers the same through log_init_learner, log_restore_learner, and log_learn_chosen.

The second is the standalone Learner in src/learner.odin, a window of MAX_ENTRIES cells with no membership at all:

// Result of recording a certified chosen value in the learner window.
Learn_Result :: enum {
    // Value was buffered in the window; a gap below it prevents immediate release.
    Buffered,
    // Contiguous released prefix advanced past this value.
    Advanced,
    // Duplicate of an already released or buffered value.
    Duplicate,
}

learner_init(&l, configuration_id) binds it to one configuration. learner_learn_chosen(&l, configuration_id, slot, value) returns a Learn_Result and an Error: .Configuration_Mismatch for a foreign configuration, .Window_Full when the slot is more than MAX_ENTRIES above released_through, and .Conflicting_Chosen_Value if the same slot arrives with a different value, which is a safety incident to preserve, not to retry. learner_read_chosen(&l, from_slot, output) copies the released suffix from from_slot, and learner_chosen_at(&l, slot) reads one released value. The learner takes and stores values by copy, not by pointer, because it has no ledger for a pointer to refer into. It trusts its caller: it has no quorum to check against, so the host must feed it only values it has certified as chosen.

6.8 Two Ways to Lead

Everything above assumes one elected leader: a node campaigns, wins a read quorum, and proposes in every slot above its term base until a higher ballot displaces it. Node_Options.rotating_ownership selects a second discipline in which the slot line is dealt round-robin and each member proposes in its own slots with no phase one at all, because round zero of each such slot's ballot space belongs to the owner alone. Under that option campaign returns .Campaign_Disabled, proposal_gate no longer requires the .Leader role, and tick runs tick_ownership: idle owners fill their slots with the no-op, a stalled prefix is repaired by a bounded phase one (Prepare_Scope.Bounded, recorded per decree as Write_Promise_At), and a suggestion that lost to such a revocation is proposed again. The ledger, the effect contract, the trim anchor, the learners, and reconfiguration are the same in both disciplines; tools/check.py runs the fault simulator in both. The next chapter derives the ownership rules from the same Synod proof and reads src/ownership.odin procedure by procedure.

7 Rotating Slot Ownership

7.1 One Leader Is a Bottleneck

The Multi-Paxos chapter made a single stable leader the engine of the log: it runs phase one once, and from then on every proposal is one round trip of Accept and Accepted. The leader coordinates each decision and can become a bottleneck. Every value a client hands to a follower must first cross the network to the leader, so a proposal from a non-leader pays a forwarding hop before its round trip, and the leader's outbound bandwidth, disk, and CPU bound the throughput of the whole group. In a group spread across sites the forwarding hop is a wide-area delay on every proposal that did not happen to originate at the leader.

Mao, Junqueira, and Marzullo's Mencius (OSDI 2008) removes the forwarding hop by dealing the log out round-robin: every member is the coordinator of its own instances, suggests values in them without a prepare, skips them when it has nothing to say, and is revoked when it is suspected. paxos-odin implements the same idea as an option on Node, called rotating slot ownership. Nothing in the acceptor's or learner's proof changes; what changes is who may propose where, and at which ballot.

7.2 The Ownership Rule

The membership is an ordered list: membership_init sorts the ids the host gives it, so every node holds the same list whatever order its host used, and a member's position in that list is its stable index. Ownership is a function of that index and the slot number alone:

// The member that owns `slot`.
owner_of :: #force_inline proc(node: ^Node($V, $M, $W, $C, $G), slot: Slot) -> Node_Id {
    count := Slot(membership_count(&node.membership))
    return membership_get(&node.membership, int((slot - 1) % count))
}

Slot $𝑠$ is owned by the member at index $\left(𝑠-1\right)mod𝑁$. With members {1, 2, 3} in that order, member 1 owns slots 1, 4, 7, …, member 2 owns 2, 5, 8, …, and member 3 owns 3, 6, 9, …. The first test in tests/test_ownership.odin pins this down: owner_of(&node, 1) is 1 and owner_of(&node, 5) is 2. No message ever carries an owner id; every member computes the same answer from the same membership. Hosts may pass the ids in different orders: membership_init sorts them into the same ascending order. They must still agree on the member set and quorum sizes for the configuration.

The private helper own_slot_from(node, from) returns the first slot at or after from that this node owns; node_init seeds own_next with own_slot_from(node, 1), and node_resume_at recomputes it from next_slot after a restore so a restarted owner never re-suggests in a slot its ledger already holds.

7.3 Partitioning the Ballot Space

Phase one exists to make sure no lower ballot can still choose a different value in the same decree. An owner can skip it only if, in its own slots, there is no lower ballot at all. The library arranges exactly that by reserving one round of the 40-bit round field:

//   bits 63..24  round      (40 bits, the campaign counter; round 0 is reserved for
//                            slot owners under rotating ownership)