Read-back: OpenSearchSafety.commit_reachable

Notions used

Sources and conventions. Rendered from Definitions/Def_OpenSearchCoordination.lean, Definitions/Def_OpenSearchSafety.lean and the stub Theorems/Thm_OpenSearchSafety_commit_reachable.lean; Java line numbers refer to OpenSearch b2a54ba5c0defba3d1d20423e911d4bf920bab19 (CS = CoordinationState.java, CM = CoordinationMetadata.java, ES = ElectionStrategy.java, CO = Coordinator.java, CBS = ClusterBootstrapService.java), checked against the local checkout. Throughout, $V$ is an arbitrary payload type, $P$ a parameter record and $W$ a cluster; $cs_n$ abbreviates $W.\mathrm{node}(n)$, the coordination state of node $n$ in $W$, and "$m \in \mathrm{sent}$" means $W.\mathrm{sent}(m)$. Booleans are read as truth values: "$\mathrm{won}(cs)$" means electionWon = true, "$\neg\mathrm{won}(cs)$" means electionWon = false.

Nodes, configurations, quorums. Node ids are natural numbers. A discovery node $d$ is a pair $(d.\mathrm{id}, d.\mathrm{cm})$ of an id and a Boolean (isClusterManagerNode). A voting configuration $c$ is a strictly increasing list of node ids, hence duplicate-free; two configurations are equal exactly when they have the same members. $\emptyset$ denotes the empty configuration EMPTY_CONFIG; "$c$ is empty" means its list is empty. For a configuration $c$ and any list $q$ of ids,

$$\mathrm{hasQuorum}(c, q) \iff 2\cdot\big|\{x \in c : x \in q\}\big| > |c| ,$$

so the empty configuration has no quorum, and ids of $q$ outside $c$ as well as repetitions in $q$ are irrelevant. Transcription check: matches VotingConfiguration.hasQuorum (CM:405-409).

A vote collection is a list of node ids; the empty collection is $[\,]$; $\mathrm{isQuorum}(v, c) := \mathrm{hasQuorum}(c, v)$; $\mathrm{addVote}(v, d)$ is $(d.\mathrm{id} :: v,\ \text{added})$ if $d.\mathrm{cm}$ is true and $d.\mathrm{id} \notin v$, and $(v,\ \text{not added})$ otherwise. Transcription check: VoteCollection (CS:750-814) keys a map by node id; addVote (CS:755-757) changes the key set exactly in the same cases.

Cluster states. A cluster state $s$ has a term $s.\mathrm{term} \in \mathbb{N}$, a version $s.\mathrm{version} \in \mathbb{Z}$, a metadata version $s.\mathrm{mv} \in \mathbb{Z}$, a last committed and a last accepted configuration $s.\mathrm{lcc}$ and $s.\mathrm{lac}$, an optional natural number $s.\mathrm{cmNode}$ (the cluster-manager node), two Booleans $s.\mathrm{uuidKnown}$ and $s.\mathrm{uuidCommitted}$, and a payload $s.\mathrm{value} \in V$. Two cluster states are equal when all nine fields are. $\mathrm{vomv}(s)$ (versionOrMetadataVersion) is $s.\mathrm{mv}$ if $s.\mathrm{term} = 0$ and $s.\mathrm{version}$ otherwise. $\mathrm{markCommitted}(s)$ is $s$ with $\mathrm{lcc}$ replaced by $s.\mathrm{lac}$ and with $\mathrm{uuidCommitted}$ set to true when $s.\mathrm{uuidKnown}$ is true; nothing else changes (transcribes CS:703-740; the Java assertion at CS:708-710 is not checked).

Message contents. A join $j$ has a source and a target discovery node $j.\mathrm{src}$, $j.\mathrm{tgt}$, a term $j.\mathrm{term} \in \mathbb{N}$, a last accepted term $j.\mathrm{lat} \in \mathbb{N}$ and a last accepted version $j.\mathrm{lav} \in \mathbb{Z}$; two joins are equal when all five fields are. A publish response is a pair $\langle t, v\rangle \in \mathbb{N}\times\mathbb{Z}$. An apply-commit request is a triple $\langle d, t, v\rangle$ of a discovery node, a term and a version. A start-join request is a pair of a discovery node and a term; it is not a cluster message (see the steps).

Coordination states. A coordination state $cs$ has a local node $cs.\mathrm{localNode}$ (a discovery node), a current term $\mathrm{ct}(cs) \in \mathbb{N}$, a last accepted state $cs.\mathrm{las}$ (a cluster state), two vote collections $\mathrm{joinVotes}(cs)$ and $\mathrm{pubVotes}(cs)$, Booleans $\mathrm{started}(cs)$ (startedJoinSinceLastReboot) and $\mathrm{won}(cs)$ (electionWon), a last published version $\mathrm{lpv}(cs) \in \mathbb{Z}$ and a last published configuration $\mathrm{lpc}(cs)$. $\mathrm{lat}(cs)$, $\mathrm{lav}(cs)$, $\mathrm{lcc}(cs)$, $\mathrm{lac}(cs)$ are the term, version, last committed and last accepted configuration of $cs.\mathrm{las}$. $\mathrm{init}(d, t, s)$ is the coordination state with local node $d$, current term $t$, last accepted state $s$, both vote collections empty, $\mathrm{started}$ and $\mathrm{won}$ false, $\mathrm{lpv} = 0$ and $\mathrm{lpc} = s.\mathrm{lac}$ (the constructor, CS:84-106).

Election strategies. An election strategy is a Boolean function $\sigma(d, t, at, av, c_1, c_2, v)$ of a discovery node, two naturals, an integer, two configurations and a vote collection; DEFAULT_INSTANCE is the constant-true function. $\mathrm{isElectionQuorum}_\sigma(cs, v) := \mathrm{isQuorum}(v, \mathrm{lcc}(cs)) \wedge \mathrm{isQuorum}(v, \mathrm{lac}(cs)) \wedge \sigma(cs.\mathrm{localNode}, \mathrm{ct}(cs), \mathrm{lat}(cs), \mathrm{lav}(cs), \mathrm{lcc}(cs), \mathrm{lac}(cs), v)$; for the default strategy the third conjunct is true. $\mathrm{isPublishQuorum}(cs, v) := \mathrm{isQuorum}(v, \mathrm{lcc}(cs)) \wedge \mathrm{isQuorum}(v, \mathrm{lpc}(cs))$. Transcription check: ES:68-88 with CS:144-154, and CS:156-158.

Parameters. A parameter record $P$ consists of $\mathrm{elig} : \mathbb{N} \to \mathrm{Bool}$ (eligible: whether a node is cluster-manager-eligible), a predicate $\mathrm{initConfs}$ on configurations (an arbitrary set of "bootstrap configurations": possibly empty, possibly containing $\emptyset$, possibly infinite), and an election strategy $\sigma_P$ (strategy). $\mathrm{dn}(n) := (n, \mathrm{elig}(n))$; "$x$ is eligible" means $\mathrm{elig}(x) =$ true. $\mathrm{InitCompatible}(P)$ holds when for all configurations $X, Y$ with $\mathrm{initConfs}(X)$ and $\mathrm{initConfs}(Y)$ and all lists $q_1, q_2$ of eligible ids,

$$\mathrm{hasQuorum}(X, q_1) \wedge \mathrm{hasQuorum}(Y, q_2) \implies \exists x,\ x \in q_1 \wedge x \in q_2$$

(for $X = Y$ this is automatic: two majorities of one configuration meet).

Messages and clusters. A cluster message is one of: $\mathsf{join}(j)$; $\mathsf{pubReq}(a, s, pt, pv)$, a publish request from node $a$ carrying a cluster state $s$ and a ghost parent $(pt, pv) \in \mathbb{N}\times\mathbb{Z}$; $\mathsf{pubResp}(a, d, r)$, a publish response $r$ from node $a$ to node $d$; $\mathsf{commit}(c)$, an apply-commit request $c$. A cluster $W$ is a function $W.\mathrm{node}$ from node ids to coordination states together with a predicate $W.\mathrm{sent}$ on messages (the messages sent so far). $W.\mathrm{set}(n, cs)$ replaces node $n$'s state by $cs$ and changes nothing else; $W.\mathrm{send}(m)$ adds $m$ to the sent set and changes nothing else. A key is a pair $(t, v) \in \mathbb{N}\times\mathbb{Z}$; the key of a publication $\mathsf{pubReq}(a, s, pt, pv)$ is $(s.\mathrm{term}, s.\mathrm{version})$.

The handlers. Each handler returns either an error (the corresponding step is then impossible) or a result. Guards are tested in the order listed; the first that applies gives the error.

• $\mathrm{setInitialState}(cs, s)$: error if $\mathrm{lac}(cs)$ is non-empty; otherwise $cs$ with $cs.\mathrm{las} := s$ (nothing else changes). Its contract $\mathrm{initialStateContract}(cs, s)$ is the conjunction: $\mathrm{lat}(cs) = 0$; $\mathrm{lcc}(cs)$ empty; $\mathrm{lpv}(cs) = 0$; $\mathrm{lpc}(cs)$ empty; $\neg\mathrm{won}(cs)$; $\mathrm{joinVotes}(cs)$ and $\mathrm{pubVotes}(cs)$ empty; $s.\mathrm{term} = 0$; $s.\mathrm{version} = \mathrm{lav}(cs)$; $s.\mathrm{lac}$ and $s.\mathrm{lcc}$ non-empty. Transcription check: CS:180-204; the contract is the eleven assertions CS:190-201.
• $\mathrm{handleStartJoin}(cs, (d, t))$: error if $t \le \mathrm{ct}(cs)$; otherwise the pair of $cs$ with $\mathrm{ct} := t$, $\mathrm{lpv} := 0$, $\mathrm{lpc} := \mathrm{lac}(cs)$, $\mathrm{started} :=$ true, $\mathrm{won} :=$ false and both vote collections emptied (last accepted state unchanged), and the join $\langle cs.\mathrm{localNode}, d, t, \mathrm{lat}(cs), \mathrm{vomv}(cs.\mathrm{las})\rangle$ (source, target, term, last accepted term, last accepted version — the metadata version when $\mathrm{lat}(cs) = 0$). Transcription check: CS:213-255.
• $\mathrm{handleJoin}_\sigma(cs, j)$: errors, in order, if $j.\mathrm{term} \ne \mathrm{ct}(cs)$; if $\neg\mathrm{started}(cs)$; if $j.\mathrm{lat} > \mathrm{lat}(cs)$; if $j.\mathrm{lat} = \mathrm{lat}(cs)$ and $j.\mathrm{lav} > \mathrm{vomv}(cs.\mathrm{las})$; if $\mathrm{lac}(cs)$ is empty. Otherwise, with $(v', b) = \mathrm{addVote}(\mathrm{joinVotes}(cs), j.\mathrm{src})$ and $w = \mathrm{isElectionQuorum}_\sigma(cs, v')$, the result is $cs$ with $\mathrm{joinVotes} := v'$ and $\mathrm{won} := w$, and moreover $\mathrm{lpv} := \mathrm{lav}(cs)$ if $w$ holds and $\mathrm{won}(cs)$ did not; together with the Boolean $b$ ("vote added"). The target $j.\mathrm{tgt}$ is not examined. Transcription check: CS:264-339; the Java assertions CS:265 (target is the local node) and CS:323-324 (a won election is not lost) are not checked by the handler.
• $\mathrm{handleClientValue}(cs, s)$: errors, in order, if $\neg\mathrm{won}(cs)$; if $\mathrm{lpv}(cs) \ne \mathrm{lav}(cs)$; if $s.\mathrm{term} \ne \mathrm{ct}(cs)$; if $s.\mathrm{version} \le \mathrm{lpv}(cs)$; if $s.\mathrm{lac} \ne \mathrm{lac}(cs)$ and $\mathrm{lcc}(cs) \ne \mathrm{lac}(cs)$; if $\neg\mathrm{isQuorum}(\mathrm{joinVotes}(cs), s.\mathrm{lac})$. Otherwise $cs$ with $\mathrm{lpv} := s.\mathrm{version}$, $\mathrm{lpc} := s.\mathrm{lac}$, $\mathrm{pubVotes} := [\,]$, together with the publish request carrying $s$. Its contract $\mathrm{clientValueContract}(cs, s)$ is $s.\mathrm{lcc} = \mathrm{lcc}(cs)$. Transcription check: CS:348-407; the contract is the assertion CS:397-398.
• $\mathrm{handlePublishRequest}(cs, s)$: error if $s.\mathrm{term} \ne \mathrm{ct}(cs)$. Otherwise, if $s.\mathrm{term} = \mathrm{lat}(cs)$ and $s.\mathrm{version} \le \mathrm{lav}(cs)$: when $s.\mathrm{term} \ne 0$, error; when $s.\mathrm{term} = 0$ (the "Zen1" branch), error if $s.\mathrm{cmNode}$ is none, accept if $s.\mathrm{cmNode} = \mathrm{some}\ m$ with $\mathrm{some}\ m \ne cs.\mathrm{las}.\mathrm{cmNode}$, error otherwise. In all remaining cases, accept. To accept is to return $cs$ with $cs.\mathrm{las} := s$ and the response $\langle s.\mathrm{term}, s.\mathrm{version}\rangle$. Transcription check: CS:416-460 (a null incoming cluster-manager in the Zen1 branch throws in Java).
• $\mathrm{handlePublishResponse}(cs, d, r)$: errors, in order, if $\neg\mathrm{won}(cs)$; if $r.\mathrm{term} \ne \mathrm{ct}(cs)$; if $r.\mathrm{version} \ne \mathrm{lpv}(cs)$. Otherwise let $v'$ be the collection returned by $\mathrm{addVote}(\mathrm{pubVotes}(cs), d)$; the result is $cs$ with $\mathrm{pubVotes} := v'$, together with the optional apply-commit request $\mathrm{some}\ \langle cs.\mathrm{localNode}, r.\mathrm{term}, r.\mathrm{version}\rangle$ if $\mathrm{isQuorum}(v', \mathrm{lcc}(cs)) \wedge \mathrm{isQuorum}(v', \mathrm{lpc}(cs))$, and $\mathrm{none}$ otherwise. Transcription check: CS:471-515.
• $\mathrm{handleCommit}(cs, \langle d, t, v\rangle)$: errors, in order, if $t \ne \mathrm{ct}(cs)$; if $t \ne \mathrm{lat}(cs)$; if $v \ne \mathrm{lav}(cs)$. Otherwise $cs$ with $cs.\mathrm{las} := \mathrm{markCommitted}(cs.\mathrm{las})$. The source $d$ is not examined. Transcription check: CS:523-573.

Restart states. $\mathrm{RestartState}(s, s')$ holds when either (i) $s'$ agrees with $s$ on term, version, $\mathrm{lcc}$, $\mathrm{lac}$, $\mathrm{uuidKnown}$ and $\mathrm{uuidCommitted}$ (its metadata version, cluster-manager node and payload are free); or (ii) $s.\mathrm{term} = 0$, $s.\mathrm{lcc} = s.\mathrm{lac} = \emptyset$, $s.\mathrm{uuidKnown} =$ false, and $s'.\mathrm{term} = 0$, $s'.\mathrm{lcc} = s'.\mathrm{lac} = \emptyset$ (every other field of $s'$, including its version, is free). Citation check: in GatewayMetaState.java (141-207) an eligible node reloads its persisted current term, version and metadata (the metadata includes the coordination metadata and the cluster-UUID flags). The remote-store path (169-186) is taken by an eligible node with remote cluster state enabled when its local cluster UUID is unknown and the remote store knows one; the restored state is built on Metadata.EMPTY_METADATA (line 296), to which RemoteStoreRestoreService.restore adds index metadata, global settings, templates, customs and the remote version, but no coordination metadata and no cluster UUID — so its term is 0 and its configurations are empty, as in (ii). Java also persists the rest of the metadata (payload, metadata version), which (i) leaves free: more behaviours than Java.

Initial clusters. $\mathrm{Initial}(P, W)$ holds when every node $n$ has $cs_n = \mathrm{init}(\mathrm{dn}(n), 0, s_n)$ for some cluster state $s_n$ with $s_n.\mathrm{term} = 0$ and $s_n.\mathrm{lcc} = s_n.\mathrm{lac} = \emptyset$ (the version, metadata version, cluster-manager node, cluster-UUID flags and payload of $s_n$ are arbitrary and may differ from node to node), and no message is sent.

Steps. $\mathrm{Step}_P(W, W')$ holds exactly in the following nine cases (all objects arbitrary unless constrained):

1. bootstrap: a node $n$, a configuration $X$ with $\mathrm{initConfs}(X)$, a cluster state $s$ with $\mathrm{initialStateContract}(cs_n, s)$ and $s.\mathrm{lcc} = s.\mathrm{lac} = X$, and $\mathrm{setInitialState}(cs_n, s) = \mathrm{ok}\ cs'$; then $W' = W.\mathrm{set}(n, cs')$. Node $n$ need not be eligible (the Coordinator rejects non-eligible nodes and imposes further guards, CO:1110-1141; omitting them only adds behaviours).
2. startJoin: nodes $n$, $src$ with $src$ eligible, a term $t$, and $\mathrm{handleStartJoin}(cs_n, (\mathrm{dn}(src), t)) = \mathrm{ok}\ (cs', j)$; then $W' = W.\mathrm{set}(n, cs').\mathrm{send}(\mathsf{join}(j))$. No message from $src$ is required.
3. join: a node $n$ and a join $j$ with $\mathsf{join}(j) \in \mathrm{sent}$, $j.\mathrm{tgt}.\mathrm{id} = n$ and $\mathrm{handleJoin}_{\sigma_P}(cs_n, j) = \mathrm{ok}\ (cs', b)$; then $W' = W.\mathrm{set}(n, cs')$.
4. clientValue: a node $n$ and a cluster state $s$ with $\mathrm{clientValueContract}(cs_n, s)$ and $\mathrm{handleClientValue}(cs_n, s) = \mathrm{ok}\ (cs', p)$; then $W' = W.\mathrm{set}(n, cs').\mathrm{send}(\mathsf{pubReq}(n, s, \mathrm{lat}(cs_n), \mathrm{lav}(cs_n)))$: the request carries the state of $p$, which is $s$, and as ghost parent the key of $n$'s last accepted state (unchanged by the handler).
5. publish: nodes $n$, $src$ and $\mathsf{pubReq}(src, s, pt, pv) \in \mathrm{sent}$ with $\mathrm{handlePublishRequest}(cs_n, s) = \mathrm{ok}\ (cs', r)$; then $W' = W.\mathrm{set}(n, cs').\mathrm{send}(\mathsf{pubResp}(n, src, r))$. Any node may handle any sent publish request.
6. respond: nodes $n$, $src$ and $\mathsf{pubResp}(src, n, r) \in \mathrm{sent}$ with $\mathrm{handlePublishResponse}(cs_n, \mathrm{dn}(src), r) = \mathrm{ok}\ (cs', o)$; then $W' = W.\mathrm{set}(n, cs')$ if $o = \mathrm{none}$ and $W' = W.\mathrm{set}(n, cs').\mathrm{send}(\mathsf{commit}(c))$ if $o = \mathrm{some}\ c$.
7. commit: a node $n$ and $\mathsf{commit}(c) \in \mathrm{sent}$ with $\mathrm{handleCommit}(cs_n, c) = \mathrm{ok}\ cs'$; then $W' = W.\mathrm{set}(n, cs')$. Any node may handle any sent commit.
8. restart: an eligible node $n$ and a cluster state $s'$ with $\mathrm{RestartState}(cs_n.\mathrm{las}, s')$; then $W' = W.\mathrm{set}(n, \mathrm{init}(cs_n.\mathrm{localNode}, \mathrm{ct}(cs_n), s'))$.
9. restartAny: a node $n$ that is not eligible, any term $t$ and any cluster state $s'$; then $W' = W.\mathrm{set}(n, \mathrm{init}(cs_n.\mathrm{localNode}, t, s'))$.

Messages are never removed from the sent set; a sent message may be handled any number of times, or never.

Reachability. $\mathrm{Reachable}_P$ is the least predicate on clusters that holds of every $W$ with $\mathrm{Initial}(P, W)$ and holds of $W'$ whenever it holds of $W$ and $\mathrm{Step}_P(W, W')$.

Commits. $\mathrm{Committed}(W, t, v)$ holds when $\mathsf{commit}(\langle d, t, v\rangle) \in \mathrm{sent}$ for some discovery node $d$ (the source is irrelevant).

1. Declaration

Binders and hypotheses. None.

Conclusion. There exist a parameter record $P$ and a cluster $W$ with payload type Unit (a one-element type) such that $\mathrm{InitCompatible}(P)$, $\sigma_P =$ DEFAULT_INSTANCE, $\mathrm{Reachable}_P(W)$ and $\mathrm{Committed}(W, 1, 1)$: a commit message for version 1 of term 1 has been sent in some reachable cluster.

2. What is not constrained

• $P$ and $W$ are chosen by the prover. The theorem shows that the hypotheses hP, hes, hW of the cluster theorems can hold together with one $\mathrm{Committed}$ hypothesis — a non-vacuity witness for, e.g., committed_published and the reflexive case of committed_linear.
• It does not exhibit two distinct committed keys, a publication of a later term after a commit, more than one eligible node, or a reconfiguration; so it does not witness the non-trivial cases of committed_linear, committed_versions or leader_completeness.
• A witness of this shape exists (one-node scenario, my reconstruction from the definitions): $\mathrm{elig}(n) \iff n = 0$, $\mathrm{initConfs} = \{\{0\}\}$, default strategy; start from the initial cluster with every node $\mathrm{init}(\mathrm{dn}(n), 0, s_0)$, $s_0$ of term 0, version 0, empty configurations; then node 0 bootstraps with $s_b$ (term 0, version 0, both configurations $\{0\}$), handles the start-join $(\mathrm{dn}(0), 1)$ and sends $j = \langle \mathrm{dn}(0), \mathrm{dn}(0), 1, 0, s_b.\mathrm{mv}\rangle$, handles $j$ and wins with votes $[0]$, publishes $s_1$ (term 1, version 1, both configurations $\{0\}$) with ghost parent $(0, 0)$, accepts $s_1$ and responds $\langle 1, 1\rangle$ to itself, and on that response (a publish quorum of $\{0\}$ and $\{0\}$) sends $\mathsf{commit}(\langle \mathrm{dn}(0), 1, 1\rangle)$.

3. Plain-language summary

There is a reachable cluster, under compatible bootstrap configurations and the default election strategy, in which version 1 of term 1 has been committed. It is a sanity check that the safety theorems' hypotheses can hold together, for a single committed key.