Quorum Protocols & BFT

Tools

`quorum_size`

Compute quorum requirements for a distributed system. Returns minimum quorum size, fault tolerance f, and read/write quorum intersection guarantee.

`bft_analysis`

Analyze Byzantine fault tolerance for a given protocol configuration. Returns safety, liveness, and complexity metrics.

`consistency_check`

Check consistency properties (linearizability, sequential, causal) for a set of operations, reporting any violations.

`quorum_visibility`

Analyze quorum visibility and ordering. Checks whether two quorums have sufficient intersection for consistency guarantees.

`async_network`

Model an asynchronous network with quorum protocols. Returns expected consensus time, partition probability, and CAP position.

`reynolds_regime_sandwich`

Compute the theorem-backed Reynolds-BFT fold regime: mergeAll when 3*chunks > 2*stages, quorumFold when 2*chunks > stages but quorum safety fails, syncRequired otherwise. Returns BFT-derived schedulin...

`thm_quorum_visibility`

In the bounded asynchronous single-key quorum protocol, write and read quorums intersect, acknowledged versions remain covered under bounded crashes/recovery, and every legal quorum read returns the a...

`thm_quorum_boundary`

The quorum-visibility claim fails exactly where the assumptions say it should: weak quorums admit disjoint read/write sets, contagious regression can make an intersecting read quorum miss the acknowle...

`thm_quorum_connected`

In the bounded asynchronous single-key quorum model with explicit connectivity, quorum availability is exactly the presence of a live connected quorum, minority connected splits are unavailable, and a...

`thm_quorum_consistency`

In the bounded single-session quorum model, once reads are restricted to committed states (`pendingVersion = 0`), each observed read equals the acknowledged version, therefore satisfies read-your-writ...

`thm_quorum_consistency_boundary`

The session-consistency claim is scoped, not universal: if reads are allowed during in-flight writes, monotonicity can fail; if the client does not carry a session floor, read-your-writes can fail eve...

`thm_quorum_ordering`

In the bounded multi-writer quorum register, globally ordered ballots plus committed-state reads force each observed read to return the latest acknowledged ballot and its writer, so a later committed ...

`thm_quorum_ordering_boundary`

The multi-writer ordering claim is scoped, not universal: if a read loses quorum connectivity under partition it can return a stale ballot, and if ballots are not globally unique then writer identity ...

`thm_quorum_history_refinement`

In the bounded committed-state multi-writer quorum register, observed reads refine the latest completed-write prefix, operation-history indices stay monotone, and the latest committed read linearizes ...

`thm_quorum_async_network`

Quorum async network: minority connected set cannot host quorum. Connected quorum read is exact under coverage. Minority split read is stale if weak reads are allowed [LEDGER: THM-QUORUM-ASYNC-NETWORK...

`thm_quorum_visibility_base`

Base quorum results: read value is supremum of stored versions. Write-read quorums intersect (critical W+R > N property). Strict majority failure budget is less than quorum size [LEDGER: THM-QUORUM-VI...

`thm_reynolds_bft`

Reynolds-BFT correspondence: Reynolds number Re = N/C (stages/chunks). Idle fraction = max(0, 1 - 1/Re). BFT thresholds derived from fork/race/fold framework: Re < 3/2 (quorum-safe), Re < 2 (majority-...

`thm_reynolds_bft_partition`

Exact BFT regime partition: `mergeAll` iff `3 * C > 2 * N` (equiv. `Re < 3/2`), `quorumFold` iff `2 * C > N` and not `3 * C > 2 * N` (equiv. `3/2 ≤ Re < 2`), and `syncRequired` iff not `2 * C > N` (eq...