Asymptote Fault Tolerance (AFT)
A model-delta consensus and settlement yellowpaper for relay-free payload dissemination, compressed receipt/frontier echo, proof-carrying canonical ordering, sealed effects, and 99% Byzantine tolerance under explicit visibility assumptions.
Asymptote Fault Tolerance (AFT): Breaking the Indefinite-Suppression Lower Bound with Relay-Free Deterministic 99% Byzantine Fault Tolerance
This crawlable source mirrors the rendered AFT yellowpaper PDF used by the public page at /papers/asymptote-fault-tolerance/. The public theorem claim is model-relative: AFT keeps the relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance headline while making explicit that it operates in the AFT model delta, where admissible published artifacts cannot be indefinitely suppressed from correct parties after stabilization. The delta is realized by authenticated direct publisher dissemination plus compact aggregated receipt/frontier/challenge echo, not by a trusted relay or external recovery service.
Asymptote Fault Tolerance (AFT): Breaking the Indefinite-Suppression Lower Bound with Relay-Free Deterministic 99% Byzantine Fault Tolerance IOI March 17, 2026
Abstract Asymptote Fault Tolerance (AFT) is a family of consensus and settlement constructions for high-throughput ordering, guardian-backed base finality, proof-carrying canonical ordering, and deterministic release of irreversible effects. Its central move is to stop treating dense positive voting as the only possible source of ordering truth. Instead, AFT separates throughput-critical publication and chain progression from authority-critical proof verification, omission detection, and effect collapse. The protocol family has four interacting surfaces. GuardianMajority supplies the production base-finality path: a validator quorum certificate is necessary but not sufficient, because each proposal must also carry a registered guardian committee certificate anchored into shared evidence. CanonicalOrdering supplies the proof-carrying ordering path: a slot order is accepted because a canonical certificate is uniquely valid and recoverable from public inputs, not because a dense validator quorum voted the order into existence. Asymptote supplies the sealing path for irreversible effects: BaseFinal chain progress is upgraded to SealedFinal through deterministic witness or observer-backed collapse, with canonical observer challenges dominating unsafe releases. NestedGuardian supplies a witness-augmented mode for layered threshold constructions. This paper is self-contained and normative for the protocol family. Its ordering subtheorem remains 99% equal-authority ordering consensus under explicit bulletin-publication, cutoff, omission, protocol-native retrievability, and proof-soundness assumptions. The runtime also internalizes compact signed publication-frontier metadata on the hot path: positive committed blocks carry a predecessor-linked frontier summary and compact availability-receipt binding, while same-slot conflicts or stale parent links admit short objective contradiction objects. Those frontier objects bind the claimed bulletin / ordering surface, while the protocol-native retrievability plane internalizes deterministic extraction-or-abort on the cold path. For each closed slot boundary there exists at most one admissible public execution object, every conflicting fully specified candidate admits a short public contradiction witness, durable state advances only through canonical collapse, and sealed-effect release is bound to the same collapse surface. The lower-bound claim is explicit about model membership. The classical n > 3f / f < n/3 lower bound remains true in the classical partially synchronous message-passing model whose adversary may keep honest groups mutually ignorant of each other’s published views for the duration needed by the indistinguishability argument. AFT does not refute that theorem from inside its quantified model. It operates in the model where an admissible published artifact cannot be indefinitely suppressed from correct parties after stabilization, and it realizes that delta without a trusted relay: honest publishers send artifacts or erasure-coded shards directly over authenticated point-to-point links to validators or deterministic custodians, while validators publish only compact commitments, receipts, frontiers, and challenges as the echo layer. Payload delivery is relay-free; equivocation and omission detection still require compressed honest-party information flow.
1
In that model delta, AFT is relay-free, coordinator-free, pure-software the classical threshold stops being loaddeterministic 99% Byzantine Tolerance: bearing because the DLS adversary’s indefinite-suppression move is no longer legal, not because an impossibility theorem is violated inside its own model. Compact bindings stay on the hot path while cold-path recovery / reveal / reconstruction re-materialize the same close, abort, collapse, replay-prefix, execution-restart, and restart-ancestry surfaces through the AFT-native recovery-family contract. Accountable publication and validator removal remain operational reinforcement, not the source of correctness.
1
Scope and Status
This paper contains the full architectural and theorem-level description of the instantiated AFT family. It does not require any companion prose specification to be understood. The instantiated protocol surfaces are: • GuardianMajority as the production guardian-backed base-finality mode. • Asymptote as the two-tier sealing and irreversible-effects mode. • CanonicalOrdering through the live CommittedSurfaceV1 certificate path plus compact PublicationFrontier summaries attached to committed blocks. • NestedGuardian as an experimental witness-augmented operational mode with safety proofs, bounded operational checks, and a finished composed-liveness / classical-agreement bridge rather than a remaining composed-liveness kernel. Implementation correspondence is included below as exact symbol references. That section is non-normative. The protocol and theorem content of the paper stands on its own. The strongest theorem surface of the runtime is singular. AFT claims not only 99% equalauthority ordering for the ordering layer, but relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance for durable ordering and sealed-effect safety, with public-state continuity as its protocol-internal safety carrier rather than dense positive quorum intersection. Compact hotpath bindings plus cold-path recovery / reveal / reconstruction materialize the same recovered closeor-abort, collapse, replay-prefix, execution-restart, and streamed restart-ancestry surfaces through the AFT-native recovery-family contract. Compact publication/frontier metadata is internalized on the live path throughout, and deeper recovered history is now ordinary endogenous AFT history through the canonical-collapse / replay retrievability anchor and the matching recovered-state historical retrievability surface. Model discipline: same ambition, explicit delta. No protocol refutes a lower bound from inside the model over which that lower bound universally quantifies. AFT’s claim is therefore a membership claim: the classical DLS / PBFT lower bound applies to a model whose adversary can keep honest groups mutually ignorant of published admissible information for the duration needed by the indistinguishability argument. AFT operates in a model delta where that indefinite-suppression move is revoked for content-addressed admissible protocol artifacts after stabilization. The delta is not a hidden helper regime: it is realized by authenticated direct publisher-to-validator or publisher-to-custodian dissemination plus a compact echo layer of commitments, receipts, frontiers, and challenges. The substantive objection would be a hidden relay, privileged coordinator, TEE, bootstrap oracle, external recovery service, or circular realization of the visibility resource by the same Byzantine-majority suppression power. AFT has none in the stated model. 2
Scope precision is not a concession. A criticism that AFT is “permissioned only” is non-responsive because the promoted claim is a permissioned theorem over fixed authenticated authorities and epoch-scoped identity state. Replacing that domain with open-membership consensus is a target switch, not a rebuttal. The lower-bound question is instead mechanical: execute the classical adversary against AFT and identify the first illegal move. That move is indefinite suppression of a published admissible artifact from correct parties after stabilization. Everything before that point is a standard adversarial schedule; everything after that point is outside the classical model and inside AFT’s explicit model delta. Singular theorem sentence. The theorem surface of this repository is now singular all the way up: AFT claims relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance. It breaks the classical threshold in the precise model-relative sense that the theorem is proved in the AFT model delta, where published admissible artifacts cannot be indefinitely suppressed from correct parties and where that delta is realized without a trusted relay. AFT does not ask credit for defeating DLS / PBFT while remaining inside the bare DLS / PBFT model. It identifies the exact adversary power removed, implements the removal through standard authenticated channels and compressed echo, and then proves the close-or-abort safety surface in that model. Proof-carrying public evidence, endogenous historical retrievability, restart continuity, and collapse-gated durability are the realizing architecture of that claim, not a residual semantic gap. Claim ladder.
The full promoted claim should be read as a constructed ladder:
- each closed slot boundary admits at most one admissible public execution object and every conflicting fully specified candidate admits a short objective obstruction witness,
- durable state advances only through canonical collapse on that same close-or-abort surface,
- irreversible effects release only through that same collapse surface. Dimension
AFT realizing surface
Promoted singular claim
Agreement object
canonical close-or-abort / canonical collapse surface compact commitments, short contradiction objects, cold-path recovery, endogenous historical retrievability canonical-collapse / replay historical retrievability root plus recovered-state historical retrievability surface direct authenticated dissemination, compressed echo, recurrence/reduction/totality/collapse chain, persistent churn simulator
one durable decision surface in MAFT
Safety carrier
History / bootstrap Liveness burden
dense positive quorum intersection is no longer load-bearing recovered history remains endogenous AFT state completed theorem surface under the AFT model delta
Target adversary/scheduler model and discharged liveness kernel. The singular theorem is interpreted under one explicit liveness model rather than a vague aspiration. Byzantine authorities may equivocate, omit, reorder, withhold reveals, withhold historical-retrievability objects, rotate maliciously, and crash/restart arbitrarily. Before stabilization the scheduler may delay or interleave publication, registry, recovery, archival, and restart traffic arbitrarily. After stabilization, 3
authenticated channels between correct parties eventually deliver direct publisher sends and compact echo objects; repeatedly published admissible artifacts become visible and content-hash fetchable to correct parties; and governing profile/activation churn quiesces into bounded windows long enough for progress to compose. Under that model, the liveness bridge is the conjunction of five obligations: frontier-generation progress, canonical-resolution progress, recovery-completion progress, restart/historical-retrievability re-entry progress, and infinite composition of those four obligations across reassignment, outage, profile rotation, and archival page boundaries. That kernel is no longer open; it is the discharged bridge that supports the promoted AFT model-delta theorem. The relevant liveness fact is not that AFT declines to claim a fully asynchronous theorem; the relevant fact is that it states the exact post-stabilization visibility resource used to halt the classical adversary. The protocol does not require universal timely receipt before the cutoff. It requires eventual delivery, persistence, and hash-fetchability of repeatedly published admissible artifacts after stabilization, realized by direct authenticated dissemination and compressed echo rather than by a trusted publication service. Current artifact map and completion status. That kernel is now grounded in concrete repository artifacts rather than prose alone. Frontier-generation progress lands on the live PublicationFrontier path and its contradiction objects; canonical-resolution progress lands on canonical-order certificates, CanonicalCollapseObject, omission dominance, and recursive continuity; recovery-completion progress lands on the coded recovery-family contract and the recovered publication / close-or-abort surface; and restart/historical-retrievability progress lands on the AFT recovered-state surface plus canonical-history retrievability anchors and bounded-memory paging. Those obligations now have both concrete runtime carriers and a completed formal bridge. The formal package contains bounded churn witnesses, recurring cycle cores, a recurrence theorem, a finite reduction, a total classical- agreement history bridge, and a directly discharged semanticcollapse wrapper ending in NestedGuardianRecoveryClassicalAgreementCollapse.tla. The exact source of that recurrence / reduction / totality / collapse bridge is embedded in Appendix A, including the final wrapper in Appendix A.6.5. The recurrence / reduction / totality / collapse chain is not narrative glue. Its exact artifact chain is embedded verbatim in Appendix A, ending in the classical-agreement collapse wrapper itself. The runtime mirrors the same story through a persistent historical-retrievability churn/restart simulator over one evolving recovered-history state. The remaining work is therefore no longer theorem completion, but cleanup, stress expansion, and maintenance of the promoted singular claim.
2
Problem Statement
Classical permissioned Byzantine fault tolerance ties deterministic safety to dense positive voting by a large honest majority. Under that model, honest inclusion, total-order agreement, and finality all depend on most validators remaining both correct and available. That is the right model when the protocol is allowed to pay dense coordination cost and accept classical 3f + 1-style thresholds. It is the wrong model for a system that wants all of the following simultaneously: • high-throughput publication and chain progression, • equal-authority participation at the validator layer, • deterministic rejection of incomplete or conflicting ordered views, • stronger accountability than “someone must have voted wrong,” 4
• deterministic gating of irreversible effects. AFT therefore changes the object of agreement. Instead of asking: • “Which order did the validator quorum choose?” it asks: • “Which order certificate is uniquely valid for this slot, and which effects are admissible after deterministic collapse?” The family-level design goals are: • keep ordering and publication sparse on the hot path, • keep effect release fail-closed, • make omissions and conflicts objectively provable, • keep all validators equally eligible to reveal the canonical order, • move authority from dense yes-votes to verifiable evidence.
3
Thought Experiment: The Port of Public Manifests and Release Seals
Imagine an international port that handles ordinary cargo and hazardous cargo. Every ship that wants to unload during tide h must post its cargo manifest to a public harbor board before the closing bell τh . The bell is not a private clock in the harbor master’s office. It is a certified public event. Once the bell rings, the harbor office takes every admissible manifest, applies the published tide lottery Rh , and derives one canonical docking docket Oh . The office does not ask every captain to vote on the exact order of every container. It asks a simpler question: has someone produced the one valid docket certificate for the manifests that were publicly posted before the bell? If any dockworker can prove that an admissible manifest was omitted from the announced docket, that docket is rejected immediately. Ordinary unloading may begin once the berth assignment is base-final. Hazardous cargo is stricter. It may leave the port only after one of two things happens: • the required independent inspector guilds each sign a release certificate, or • a deterministically assigned set of external captains publishes a public inspection transcript surface, the public red-flag board remains empty through the close bell, and the port issues the unique release docket implied by that surface. Any valid red flag aborts release. The cargo does not “probably” leave the port. It does not leave. Most of the port can be chaotic. Captains can lie, stall, or collude. What they cannot do is create a second valid docket for the same tide or a second valid hazardous-cargo release order, provided the public manifest board remains recoverable and the decisive proof surface stays objectively checkable. The correspondence is direct: 5
Public manifest board
Certified closing bell
canonical
Public lottery docket and docket
Hazardous cargo release
Base berth assignment ar
all
Omission rule: Any omitted admissible manifest invalidates the docket.
Inspector or observer release evidence
cle
valid veto
Abort release on valid veto
Figure 1: The thought experiment behind AFT: public admission, canonical ordering, base progress, and fail-closed release. Port object
AFT object
Public manifest board Certified closing bell Tide lottery Docking docket Docket certificate Omitted manifest challenge Base berth assignment Independent inspector guilds Sampled external captains Red-flag report Hazardous cargo release seal
Bulletin / DA surface Bh Canonical cutoff τh Public randomness beacon Rh Canonical order Oh Canonical-order certificate OCerth Omission proof Ω(h, tx) BaseFinal Witness committees Equal-authority observers Canonical observer challenge SealObject under SealedFinal
This thought experiment captures the essential AFT move: sparse operational progress, dense cheap verification, objective omission, and deterministic collapse for irreversible consequences.
4
Protocol Family Overview
AFT is best understood as four planes that compose: Plane
Purpose
Throughput-critical work
Authority object
Dissemination / bulletin plane Base-finality plane
Publish the candidate transaction surface Advance the chain and commit block identity Prove the unique slot order Gate irreversible effects
Data dissemination and bulletin commitments Proposal, QC formation, guardianized certification Succinct verification, omission dominance Asynchronous witness / observer evidence collection
Public bulletin commitment Validator QC + guardian certificate OCerth
Canonical-ordering plane Sealed-effect plane
The protocol modes are:
6
SealedFinalityProof and SealObject
Base finality validator QC + guardian certificate
Dissemination / Bulletin publication of candidate surface
Canonical ordering proof-carrying OCerth
Sealed effects witness / observer collapse
Design principle. Chain progress is allowed to remain sparse and fast. Ordering authority and irreversible effects are decided by shared, cheaply verifiable evidence rather than by dense hot-path yes-votes. Figure 2: AFT separates publication, base progress, canonical ordering, and sealed effect release, then recomposes them through shared evidence. Mode
Role
Current status
GuardianMajority CanonicalOrdering
Production guardian-backed base finality Proof-carrying equal-authority ordering
Asymptote NestedGuardian
Two-tier sealing and sealed-effect release Witness-augmented layered threshold mode
Production mode Live through CommittedSurfaceV1 Production sealing path Experimental operational mode / completed theorem bridge
The key invariant is: throughput-critical work ̸= authority-critical work
5
System Model and Notation
5.1
Actors
• Validator: participates in proposal, vote, verification, and chain execution. • Guardian committee: the registered threshold-signing committee protecting one validator’s proposal decisions. • Guardian member: an individual signer within a guardian committee. • Witness committee: an external threshold-signing committee used on the sealing path or in NestedGuardian. • Equal-authority observer: a validator sampled to audit a slot under Asymptote. • Registry: the on-chain source of truth for manifests, policies, epochs, witness sets, and verifier descriptors.
7
• Transparency log: an append-only checkpointed evidence log for guardian and witness statements. • External verifier or gateway: a party that checks SealObjects and enforces replay-safe release.
5.2
Bulletin-board time and slot model
Consensus proceeds in heights and views. A slot is identified by (height, view). Epoch-scoped policy and committee state bind the admissible evidence for that slot. The family should be read under a model-delta publication and recoverability discipline rather than a pure point-to-point timely receipt discipline: safety depends on whether the closed boundary fixes a unique public evidence surface, while liveness depends on correct-party delivery and eventual visibility of admissible content-addressed artifacts after stabilization. Slots are externally paced by a public cutoff object τh and a public randomness beacon Rh . Honest validators that observe the same closed public boundary derive the same ordering or sealing close-or-abort result. In the runtime that derivation is no longer keyed off cutoff closure alone: the bulletin plane exports a canonical bulletin-close object binding the bulletin commitment, the bulletin-availability certificate, and the canonical cutoff into one public close surface. In this instantiation, positive canonical-order publication is fail-closed at this boundary: a closed-slot order certificate is admitted only if the published bulletin entries deterministically extract the bulletin surface bound by the canonical bulletin-close object and the carried bulletin-availability certificate. Universal timely receipt is not required. Let h = slot height, v = slot view, Bh = bulletin surface admitted before cutoff τh , Rh = public randomness beacon for slot h, Eh = {tx | Included(tx, Bh ) ∧ Eligible(tx, rooth−1 )}, Oh = CanonicalOrder(Rh , Eh ), rooth = Execute(rooth−1 , Oh ).
5.3
Classical lower bound and AFT model delta
Let MDLS denote the standard authenticated partially synchronous message-passing model used by the classical DLS / PBFT lower-bound argument. Its adversary may delay messages so that two honest groups cannot distinguish “the other group is slow” from “the other group is faulty” for the duration required by the indistinguishability construction. Let MAFT denote the AFT model delta. It keeps fixed authenticated authorities, deterministic local verification, and partial synchrony among correct parties, but it removes one adversary power: after stabilization, an admissible content-addressed protocol artifact repeatedly published by a correct party cannot be indefinitely suppressed from correct parties. Payload delivery is realized by direct authenticated dissemination from the publisher to validators or deterministic custodians; equivocation, omission, and retrievability detection are realized by compact echo objects rather than by payload relay.
8
Adversary-execution trace.
Run the classical indistinguishability adversary against AFT:
- The adversary may schedule delays, split honest validators into views, and make Byzantine validators equivocate or omit.
- The adversary may hide a Byzantine sender’s conflicting statements until an honest validator publishes a protocol-admissible commitment, receipt, frontier, challenge, or reconstruction / abort artifact.
- The first illegal step is indefinite suppression of that published admissible artifact from another correct validator after stabilization. In MDLS , that suppression power is available to the adversary long enough to drive the lower-bound execution. In MAFT , the artifact eventually becomes visible and content-hash fetchable. That stopped step is the model delta. The rest of AFT is protocol design inside MAFT : compact frontiers bind the claimed surface, contradiction objects kill conflicts, retrievability objects reconstruct or abort the full surface, and canonical collapse gates durability. Lemma 1 (Direct dissemination plus compressed echo realizes the delta). Assume authenticated point-to-point channels among correct parties that eventually deliver after stabilization. An honest publisher sends its artifact or erasure-coded shards directly to the validators or deterministic custodians named by the slot policy. No non-sender validator must relay the payload for honest-artifact delivery. Validators then publish compact commitments, availability receipts, publication frontiers, observer transcripts, challenges, and reconstruction / abort objects that expose what they received or what the public surface lacks. The payload path discharges honest delivery; the echo path discharges equivocation, omission, and retrievability detection. The classical adversary’s indefinite-suppression step is therefore unavailable without introducing a trusted relay, coordinator, TEE, bootstrap oracle, or external recovery service.
5.4
Core assumptions
The family-level safety claims rely on the following explicit assumptions: • Objective publication: admitted bulletin entries, transcripts, and challenges have stable hashes and objective inclusion paths. • Authenticated direct dissemination: after stabilization, authenticated channels between correct parties eventually deliver the publisher’s direct artifact or shard sends to the validators or deterministic custodians named by the slot policy. • Compressed echo visibility: validators publish compact commitments, receipts, frontiers, transcripts, challenges, and reconstruction / abort artifacts that make equivocation, omission, stale lineage, and retrievability failures objectively visible without echoing full payloads. • Verifiable bulletin availability: the protocol exports a bulletin-availability object, compact publication-frontier metadata that binds the same slot surface, and a canonical bulletin-close object for each closed ordering slot; the remaining assumption is that direct dissemination and the compressed echo layer satisfy the retrieval semantics claimed by those objects. The live runtime also requires successful closed-slot extraction before positive canonical-order admission.
9
• Compact frontier consistency: any carried PublicationFrontier must bind the same-slot bulletin commitment, ordered surface, and compact availability receipt, and same-slot conflicts or stale predecessor links must admit short objective contradiction objects. These frontier objects summarize the slot surface; they do not reconstruct it. • Objective validity only: theorem-critical rejection or acceptance does not depend on private local facts. • Public derivability over universal receipt: honest validators that observe the same closed public boundary derive the same close-or-abort result; universal timely receipt is not required. • Independent echo path: suppressing negative evidence requires capture of both the payloaddelivery path and the compact publication / registry echo surface. • Sealed-effect gating: irreversible effects are released only after surviving the canonical closeor-abort surface. • Fixed epoch identities: the validator set is epoch-scoped and stable while the accountable rules of that epoch are enforced. Here and throughout, the AFT permissioned model means fixed authenticated authorities, deterministic local verification, authenticated point-to-point channels among correct parties, public hash-addressed protocol objects, epoch-scoped identity state, and eventual visibility / persistence / hash-fetchability of admissible protocol artifacts after stabilization, with no trusted relay, privileged coordinator, TEE, theorem-side bootstrap oracle, or hidden external recovery service. Fixed authenticated membership is part of the theorem statement, not a missing crutch. The hiddenhelper exclusions are relay, coordinator, TEE, bootstrap oracle, and external recovery service — not epoch-scoped authenticated identity itself.
5.5
Evidence objects
The family-level evidence objects are: • validator quorum certificates over block proposals, • guardian quorum certificates over slot decisions, • witness certificates over guardianized slots, • canonical-order certificates over bulletin surfaces, • omission proofs over ordered-set incompleteness, • observer transcripts, observer challenges, and canonical close-or-abort objects over sealed finality, • sealed-effect proof objects with replay-safe nullifiers. All honest nodes are required to derive the same acceptance result from the same admissible evidence set.
10
5.6
Accountable publication rules
Objective AFT faults are not merely audit artifacts. In the runtime they are first-class accountable protocol objects: • OmissionProof names the validator accountable for the dominated positive order object. • AsymptoteObserverChallenge determines accountability by kind: MissingTranscript and ConflictingTranscript blame the assigned observer; TranscriptMismatch, VetoTranscriptPresent, and InvalidCanonicalClose blame the producer / positive-close path. • Valid objective fault evidence is replay-deduplicated on chain. • Policy-controlled membership updates are aftermath only: the same evidence may trigger besteffort immediate quarantine and stage next-epoch eviction, but the decisive negative object remains valid even when those membership updates are disabled, delayed, or skipped. These rules do not change the hot path. They strengthen the adversary model: arbitrary behavior is tolerated only insofar as it remains publicly revealable and penalty-bearing.
6
Public State Continuity with Extractable Obstructions
AFT’s deeper theorem target is not a new round gadget. It is a new source of uniqueness. Classical Byzantine agreement derives uniqueness from overlap of dense positive quorums. AFT instead seeks a rigidity theorem over public slot objects: once the slot boundary is closed, the space of admissible public continuations should collapse to one canonical object or one canonical abort.
6.1
Boundary-conditioned execution language
For a closed slot boundary define ∂h := (rooth−1 , βh , τh , Rh , ph ), where βh is the canonical bulletin-close object binding the bulletin commitment, bulletin-availability certificate, and canonical cutoff whose recoverable surface is Bh ; τh is the canonical cutoff object; Rh is the slot randomness beacon; and ph is the policy descriptor governing admissible checks for slot h. Let a public execution object for slot h be a normalized public codeword Xh := (Bh , Eh , Oh , rooth , σh ), where Eh is the eligible subset, Oh is the canonical ordered object, rooth is the resulting state commitment, and σh is the slot-local sealing surface needed to determine whether the slot closes or aborts. The important point is that Xh is not a distributed transcript. It is the public quotient of the slot after irrelevant schedule variation is factored out. Define the boundary-conditioned language L(∂h ) := {X | ∃π Accept(∂h , X, π) = 1}. Here π is a succinct admissibility witness. For canonical ordering, π is the proof-carrying order certificate witness. For deterministic observer sealing, π is the witness that the canonical transcript surface, challenge surface, and close-or-abort object satisfy the slot policy. 11
6.2
Obstruction extractability
The companion rejection relation is Reject(∂h , Y, ω) = 1, where Y is a fully specified candidate public execution object and ω is a short public objective contradiction witness. AFT seeks obstruction-complete local testability: for a fixed closed boundary, every fully specified candidate lies in exactly one of two states,
∃π Accept(∂h , Y, π) = 1
⊕
∃ω Reject(∂h , Y, ω) = 1 .
This xor formulation is the software-only analogue of state continuity. It is stronger than merely having a valid proof system. It says every non-admissible candidate exposes a short public contradiction witness. In the live repository, the obstruction basis is not abstract: • ordering uses a first-class canonical abort taxonomy over the canonical bulletin surface: missing certificates, bulletin-surface reconstruction failures, bulletin-surface mismatches, invalid bulletinclose formation, omission-dominated candidates, certificate-height mismatches, randomness mismatches, ordered-transactions-root mismatches, resulting-state-root mismatches, invalid public-input bindings, invalid bulletin-availability bindings, and invalid proof bindings, • deterministic observer sealing uses objective challenge kinds over the canonical transcript and challenge surface, • the accountable-adversary layer turns those same objects into penalty-bearing public fault evidence.
6.3
Unique collapse object
The slot should not merely admit at most one positive object. It should admit at most one collapse object: Collapse(∂h ) ∈ {Close(Xh ), Abort(Ωh )}. Here Close(Xh ) denotes the unique admissible positive object when the obstruction surface is empty, while Abort(Ωh ) denotes the unique negative object induced by a non-empty valid obstruction surface. Negative evidence does not create a second truth. It forces the slot to land on its canonical abort object instead of a close object. In the runtime this collapse object is not merely an abstract proof target. Validator finalization publishes a first-class CanonicalCollapseObject through guardian_registry, and later consensus verification cross-checks any published copy against the same proof-carried ordering and sealing surface when parent-state data is available. In the current recursive-continuity slice, CanonicalCollapseObject also carries a rolling previous_canonical_collapse_commitment_hash, and in the current clean-break runtime slice it also carries continuity_accumulator_hash together with continuity_recursive_proof, so the current slot’s collapse object is linked to the previously persisted or published collapse object rather than standing as an isolated per-slot fact. The newest proposal-surface slice pushes that same predecessor link into the signed header itself: BlockHeader now carries previous_canonical_collapse_commitment_hash in its signed preimage and also carries a typed CanonicalCollapseExtensionCertificate. That certificate now carries the 12
predecessor commitment plus the predecessor recursive-proof hash, while the public predecessor CanonicalCollapseObject now carries only a single recursive proof step rather than a carried predecessor-proof tree. Each recursive proof step still binds a predecessor collapse commitment, predecessor commitment hash, predecessor payload hash, and previous proof hash; the rolling continuity_accumulator_hash remains in place as the companion accumulator over the same chain. The implementation surface distinguishes the reference HashPcdV1 carrier from a backend slot SuccinctSp1V1, and the runtime exposes a dedicated continuity-verifier seam for those recursive public inputs via ioi-api and zk-driver-succinct. That seam is now wired into the live protocol: GuardianMajority invokes it while validating proposal and QC continuity for carried or anchored SuccinctSp1V1 proof steps, and validator durable-state checks invoke the same backend before a persisted CanonicalCollapseObject is treated as authoritative. Proposal verification checks that the carried predecessor commitment hash matches the signed predecessor link, checks that the predecessor commitment’s resulting state root matches the signed parent-state root, and checks that the carried predecessor proof hash matches the anchored predecessor collapse object already persisted or published in protocol state. Leaders in Asymptote stall rather than propose when the required extension certificate or anchored predecessor collapse object is unavailable, proposal verification rechecks that implied predecessor commitment against both the signed predecessor commitment link and the parent-state root, checks the carried predecessor proof hash against the anchored predecessor proof on the public collapse object, and QC progression only treats continuity-linked headers as progress-authoritative. Theorem 1 (Public State Continuity with Extractable Obstructions). Assume a closed boundary ∂h , objective publication, a protocol-native retrievability plane, compact publication-frontier consistency, objective validity only, and proof soundness. Then the instantiated and normative theorem shape for AFT is:
- L(∂h ) contains at most one admissible public execution object,
- every fully specified candidate Y ∈ / L(∂h ) admits a short public objective obstruction witness ω such that Reject(∂h , Y, ω) = 1,
- therefore the slot admits at most one admissible collapse object, either the unique close object or the unique abort object. This theorem is the precise form of the software-only continuity primitive that the instantiated AFT runtime realizes. The later ordering, collapse, recovery, restart, and sealed-effect sections are concrete theorem instances and composition layers of this same continuity statement, not separate aspirations. It does not claim that the classical DLS / PBFT frontier disappeared inside the standard dense-vote model. The point is different: the uniqueness source has moved from quorum overlap into the public-evidence language itself. In the instantiated runtime, compact publication frontiers internalize same-slot and predecessor consistency inside the live protocol, while the protocol-native retrievability plane discharges closed-bulletin extraction-or-abort on the cold path.
6.4
Lemma program
The clean proof path is a filtration rather than a single opaque argument: L0 (∂h ) ⊇ L1 (∂h ) ⊇ · · · ⊇ Lk (∂h ), where each refinement adds one structural constraint and each failed refinement admits a short witness. The repository’s theorem program is: 13
- Boundary Fixing Lemma. The closed boundary fixes the admissible publication domain.
- Bulletin Close Lemma. The canonical bulletin-close object fixes the unique recoverable bulletin surface for the slot.
- Eligibility Determinism Lemma. The predecessor commitment and boundary fix the eligible subset.
- Order Determinism Lemma. The boundary and eligible subset fix the canonical ordered object.
- Transition Determinism Lemma. The ordered object fixes the next state commitment.
- Collapse Exclusivity Lemma. A slot cannot admit both a canonical close object and a canonical abort object.
- Obstruction Soundness Lemma. Every valid omission proof or observer challenge objectively rejects its target candidate.
- Obstruction Completeness Lemma. Every invalid fully specified candidate contains at least one minimal public obstruction witness.
- Extractor Sufficiency Lemma. Given the canonical bulletin-close object, any honest validator can run the protocol-defined bulletin extractor to reconstruct the same bulletin surface; in this instantiation, admission of the positive ordering object already requires this extraction to succeed over the published closed-slot surface. One honest validator remains sufficient to surface the resulting positive or negative object under the instantiated runtime model. One honest validator is surfacing-sufficient but never trust-bearing: correctness does not attach to the revealer’s identity, because any honest validator observing the same closed boundary derives the same decisive object. The theorem surfaces of this paper are instances of that program: • CanonicalOrdering instantiates unique admissibility and extractable obstruction through proofcarrying order certificates plus omission dominance. • Asymptote instantiates unique collapse through canonical transcript/challenge surfaces plus close-or-abort exclusivity.
7
The AFT Deterministic Base Engine
AFT modes share a deterministic core engine for proposal flow, QC formation, locking, and view progression.
7.1
Deterministic leadership and view progression
For a given height and view, the implementation selects the proposer by deterministic round-robin over the active validator set: leader(h, v) = Vh [(h − 1 + v) mod |Vh |]. Here Vh is the active validator set for height h after operational quarantine filters are applied. 14
View 0 proposals do not carry a timeout certificate. Any non-zero view proposal must carry a valid timeout certificate for the previous unsuccessful view. The pacemaker advances views monotonically and resets timers on observed progress.
7.2
Validator quorum certificates
In GuardianMajority, Asymptote, and NestedGuardian, validator quorum is a strict simple majority of active validator weight, not a classical 2/3 + 1 quorum: 1 QCQuorum(Vh ) > Weight(Vh ). 2 This is safe only because the validator quorum is not the sole authority object. A proposal must also satisfy guardian-layer admissibility. Timeout certificates use the same simple-majority rule over view-change votes.
7.3
Locking, 2-chain commit, and divergence guard
Validators maintain a lock on the highest safe parent QC they have observed. A validator votes only when the proposal extends the lock or is in a strictly higher view than the lock. Base commitment uses a 2-chain rule: • let QCparent certify parent block P , • let QCchild certify child block C, • if C directly extends P and the views are consecutive, then P becomes a pending commit. The implementation delays final durability by a guard window ∆guard before a pending commit is released. The purpose of the guard window is operational, not purely algebraic: it gives divergence evidence or panic signals time to propagate before a conflicting branch is treated as durable. This produces a fail-closed operational behavior: • sparse chain progress happens on the hot path, • conflicting evidence is surfaced before irreversible consequences, • divergence proofs quarantine the affected node rather than silently allowing fork continuation.
8
GuardianMajority: Production Base Finality
GuardianMajority is the production fault model for AFT base finality. Validator votes alone never make a proposal admissible. Every valid proposal must also carry a guardian committee certificate that verifies against current registered committee state.
8.1
Guardian certificate object
The guardian certificate binds: • the guardian committee manifest hash, • the active epoch, 15
• the canonical decision hash for the slot payload, • a monotonic guardian counter, • a guardian trace root, • a measurement root, • the signer bitfield, • the aggregated BLS signature, • a transparency-log checkpoint, • and, in NestedGuardian, an optional experimental witness certificate. The guardian decision payload is slot-scoped. Honest guardians are assumed not to sign two different decisions for the same slot.
8.2
Verification rule
A guardianized proposal is admissible only if all of the following hold:
- the referenced guardian committee manifest is registered on-chain for the active epoch,
- the certificate manifest hash matches the registered manifest,
- the certificate epoch matches the manifest epoch and current epoch,
- the decision hash matches the slot’s canonical guardian decision payload,
- the measurement root matches the decision payload,
- the signer set is valid, unique, and meets the committee threshold,
- the aggregated signature verifies against the manifest public keys,
- the attached transparency-log checkpoint verifies against the anchored log descriptor and appendonly proof. The transparency log is an accountability layer. It does not replace threshold safety. It makes issued decisions, checkpoints, and later slashing evidence publicly checkable.
8.3
Committee threshold model
Let a guardian committee have threshold t and size n. Conflicting slot certificates require enough equivocators to cover the minimum quorum intersection: f < 2t − n. Production committees therefore use strict majority thresholds: n
- 1. 2 This guarantees pairwise quorum intersection. It also exposes an important operational nuance: t=
16
• odd-sized simple-majority committees tolerate zero equivocating guardian members at the committee layer, • even-sized majority committees tolerate one equivocator before threshold intersection is exhausted. Production safety therefore relies on both threshold intersection and stronger guardian nonequivocation guarantees.
8.4
Safety statement
Proposition 1 (GuardianMajority Safety). No two conflicting blocks can both finalize for the same (height, view) if guardian committee manifests are current, committee thresholds are majority thresholds, honest guardians do not equivocate for the same slot, transparency-log checkpoints and registry state are current enough to verify admissibility, and validators finalize only guardianadmissible blocks. This is not a classical 3f + 1 theorem. It is a composed threshold theorem over validators, guardians, registry state, and shared evidence. That statement is local to the guardian-backed base-finality layer. It does not delimit the paper’s promoted theorem surface. The promoted durable-agreement claim is carried by the later proof-carrying close-or-abort and canonical- collapse architecture, which is precisely why the classical 3f + 1 threshold is not load-bearing there.
8.5
Liveness model
Liveness is secondary to safety. Progress requires: • enough active validators to form the simple-majority validator QC, • enough guardian members to satisfy the committee threshold, • current registry state for the epoch, • current enough checkpoint and log availability. If these degrade, the protocol prefers stalling over accepting unsafe evidence.
9
Canonical Ordering
CanonicalOrdering is the proof-carrying ordering path that gives AFT its 99% equal-authority ordering consensus claim.
9.1
Objective
For each slot h, define a unique canonical ordered set Oh and a certificate OCerth such that: • every honest verifier can check OCerth cheaply, • any omission is objectively provable, • the ordered set is recoverable from public data, 17
• the live hot path carries a compact publication frontier that binds the same-slot bulletin / ordering / availability surface and predecessor continuity, • conflicting valid certificates for the same slot are impossible, • arbitrary behavior by almost all validators cannot create a conflicting valid ordering outcome because the closed bulletin boundary admits one deterministically derivable close-or-abort result.
9.2
Canonical objects
For slot h,
Bh = bulletin surface admitted before τh , Rh = public randomness beacon for slot h, Eh = {tx | Included(tx, Bh ) ∧ Eligible(tx, rooth−1 )}, Oh = CanonicalOrder(Rh , Eh ), rooth = Execute(rooth−1 , Oh ).
The abstract certificate is OCerth = (h, rooth−1 , cutof fh , bulletin_commitmenth , ordered_commitmenth , rooth , witnessh ) .
9.3
Bulletin, cutoff, and admissibility assumptions
The ordering theorem is conditional on the following named assumptions. A1. Objective publication. Each admitted transaction or batch in Bh has a stable content hash, a verifiable inclusion path into the bulletin commitment, and an objective publication time or publication position relative to the slot cutoff. A2. Endogenous retrievability. The bulletin contents committed by bulletin_commitmenth are reconstructed or deterministically aborted from protocol-native retrievability objects rooted in the canonical bulletin close for slot h. Compact publication-frontier summaries and availability certificates bind that claim on the hot path, while retrievability profiles, shard manifests, custody assignments, custody receipts, custody responses, and objective challenge objects close the extractionor-abort loop on the cold path. Without that plane, uniqueness may still hold while timely materialization of the same close-or-abort surface can fail. A3. Append-only or equivocation-evident commitment. The bulletin commitment and any carried publication frontier for slot h must be append-only or otherwise make same-slot equivocation or stale predecessor linkage objectively detectable at the slot boundary. A4. Eligibility determinism. Eligible(tx, rooth−1 ) is deterministic and locally checkable from the committed predecessor root and the transaction object. Honest validators therefore derive the same eligible set Eh from the same public inputs.
18
A5. Proof soundness. VerifyProof(witnessh ) = true implies that the witness obligations for cutoff binding, bulletin binding, ordering, state transition, retrievability commitments, and omission commitments actually hold. The cutoff τh is not a private local clock read. It is a protocol-bound object. In the instantiated runtime, the cutoff is bound directly into the published bulletin commitment and into the canonical public-input set. Eligibility is deterministic with respect to the predecessor state root and the transaction object. This prevents local reinterpretation of the eligible set.
9.4
Current runtime instantiation
The runtime surfaces the abstract objects above as the following concrete objects:
19
Runtime object
Current fields
BulletinCommitment BulletinSurfaceEntry BulletinAvailability Certificate
(height, cutoff_timestamp_ms, bulletin_root, entry_count) (height, tx_hash)
BulletinRetrievabilityProfile
BulletinShardManifest
BulletinCustodyAssignment
BulletinCustodyReceipt
BulletinCustodyResponse
BulletinRetrievabilityChallenge
BulletinReconstructionCertificate
BulletinReconstructionAbort
PublicationAvailabilityReceipt
PublicationFrontier PublicationFrontierContradiction
CanonicalBulletin Close CanonicalOrder PublicInputs CanonicalOrderProofSystem CommittedSurface CanonicalOrderProof CanonicalOrder Certificate CanonicalOrder PublicationBundle CanonicalOrder Abort
(height, bulletin_commitment_hash, recoverability_root) (height, bulletin_commitment_hash, bulletin_availability_certificate_hash, recoverability_root, shard_count, recovery_threshold, custody_threshold) (height, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, recoverability_root, entry_count, shard_count, recovery_threshold, shard_commitment_root) (height, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, validator_set_commitment_hash, assignments) (height, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, custodian_count, custody_threshold, custody_root) (height, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, bulletin_custody_assignment_hash, bulletin_custody_receipt_hash, served_shards) (height, kind, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, bulletin_custody_assignment_hash, bulletin_custody_receipt_hash, bulletin_custody_response_hash, details) (height, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, bulletin_custody_assignment_hash, bulletin_custody_receipt_hash, bulletin_custody_response_hash, canonical_bulletin_close_hash, canonical_order_certificate_hash, reconstructed_entry_count, reconstructed_bulletin_root) (height, kind, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, bulletin_custody_receipt_hash, bulletin_retrievability_challenge_hash, canonical_order_abort_hash, details) (height, bulletin_commitment_hash, ordered_transactions_root_hash, resulting_state_root_hash, receipt_root) (height, view, counter, parent_frontier_hash, bulletin_commitment_hash, ordered_transactions_root_hash, availability_receipt_hash) (height, kind, candidate_frontier, reference_frontier) (height, cutoff_timestamp_ms, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, bulletin_custody_receipt_hash, entry_count) (height, parent_state_root_hash, bulletin_commitment_hash, randomness_beacon, ordered_transactions_root_hash, resulting_state_root_hash, cutoff_timestamp_ms) concrete variants HashBindingV1 and CommittedSurfaceV1 (recoverability_root, omission_commitment_root) (height, bulletin_commitment, bulletin_availability_certificate, randomness_beacon, ordered_transactions_root_hash, resulting_state_root_hash, proof, omission_proofs) (bulletin_commitment, bulletin_entries, bulletin_availability_certificate, bulletin_retrievability_profile, bulletin_shard_manifest, bulletin_custody_receipt, canonical_order_certificate) (height, reason, details, bulletin_commitment_hash, bulletin_availability_certificate_hash, bulletin_close_hash, canonical_order_certificate_hash)
20
HashBindingV1 is the reference verifier family: its proof bytes are a canonical hash binding over the public-input hash. CommittedSurfaceV1 is the live proof family: its proof payload contains the recoverability root and the omission-commitment root for the committed surface. In the current runtime, positive ordering artifacts are published through the atomic CanonicalOrderPublicationBundle, carrying the bound retrievability profile / manifest / custodyreceipt objects, while the registry deterministically materializes the coupled custody-assignment and custody-response objects over the same slot surface before admitting the positive lane. Positive committed blocks also carry a compact signed PublicationFrontier: it binds the same-slot bulletin commitment, ordered-transactions root, and compact publication-availability receipt, and it hashlinks that summary to the previous slot’s frontier. Short PublicationFrontierContradiction objects make same-slot conflict or stale predecessor linkage objectively rejectable on the hot path. Those frontier objects internalize compact publication consistency, but they do not replace the protocol-native retrievability plane that reconstructs or aborts the full bulletin surface. Validators also run a block-local derivation pass over the committed block boundary: they derive either a CanonicalOrderExecutionObject or a CanonicalOrderAbort, and publish the abort artifact when the proof-carried positive object cannot be derived. When the endogenous retrievability lane succeeds, the registry materializes a first-class BulletinReconstructionCertificate bound to the canonical close, canonical-order certificate, and the same retrievability objects. When endogenous retrievability evidence dominates that same surface, the registry also materializes a specialized BulletinReconstructionAbort object bound to the challenge and the paired CanonicalOrderAbort, so reconstruction-impossible failure is named as a first-class protocol object rather than only as a generic ordering abort.
9.5
Acceptance rule
Every validator applies the same deterministic rule: Accept(OCerth ) ⇐⇒ VerifyProof(witnessh ) ∧ VerifyCutoff(cutof fh ) ∧ PredecessorAccepted(rooth−1 ) ∧ ¬∃tx : ValidOmission(h, tx). In the implementation this specializes to: • the certificate height and bulletin height must match the block height, • the randomness beacon must match the slot schedule, • the bulletin commitment must match the published bulletin when that bulletin is available from anchored state, • any carried PublicationFrontier must match the same-slot bulletin commitment, orderedtransactions root, and publication-availability receipt hash, • when a predecessor frontier exists, the carried PublicationFrontier must extend it by counter and parent hash, • no published PublicationFrontierContradiction may already dominate the slot,
21
• positive canonical-order admission in the runtime additionally requires successful closed-slot extraction over the published bulletin entries, the carried bulletin-availability certificate, and the canonical bulletin-close object, • the ordered-transactions root and resulting state root must match the block header, • the proof must match the canonical public inputs, • the recoverability root must match the certificate commitments, • the omission-commitment root must match the omission-proof set. If the omission-proof set is non-empty, the candidate certificate is rejected immediately. No dense positive vote on the order is required once a valid OCerth is surfaced. The current verifier entry point for this rule is verify_canonical_order_certificate.
9.6
Omission dominance
An omission is objective when a transaction: • was included in Bh before τh , • was eligible under rooth−1 , • and is absent from the committed ordered set Oh . Define the omission proof inclusion_proof (tx, bulletinh ), cutof f _admissibility_proof (tx, cutof f ), h Ω(h, tx) = . eligibility_proof (tx, rooth−1 ), nonmembership_proof (tx, Oh )
Its semantics are:
Valid(Ω(h, tx)) ⇒ Reject(OCerth ).
This is the central AFT ordering move. A candidate does not need to win a dense round of positive endorsements if any incomplete view can be killed objectively. Omission dominance is a correctness rule, not a punishment rule. A valid omission proof kills the candidate immediately whether or not slashing, quarantine, or next-epoch removal ever fires.
9.7
Uniqueness, publication frontiers, and recoverability
Theorem 2 (Uniqueness). If ValidOrderCert(h, C1 ) and ValidOrderCert(h, C2 ), then C1 and C2 commit the same canonical ordered set Oh . The reason is structural: • the predecessor root is fixed, • the cutoff object is canonical, • the bulletin commitment is canonical, 22
• eligibility is deterministic, • the ordering function is deterministic, • proof soundness forbids a witness for a different ordered set. The live publication-frontier slice sits between uniqueness and recoverability. A frontier gives a compact signed summary of the claimed bulletin / ordering surface and its predecessor link, so same-slot conflict or stale lineage is objectively rejectable without reconstructing the full bulletin on the hot path. But the frontier only binds hashes and receipt roots; it is not itself the recoverable bulletin surface. Theorem 3 (Endogenous Retrievability). If ValidOrderCert(h, C) and the canonical bulletin close plus protocol-native retrievability plane for slot h are present and unchallenged, then every honest verifier can reconstruct the same ordered set Oh from protocol objects alone: the canonical close, bound frontier / availability commitments, retrievability profile, shard manifest, custody receipt, positive reconstruction certificate, and published bulletin entries. Endogenous retrievability matters because the accepted order is not merely unique. The compact frontier tells validators which surface is being claimed; the retrievability plane tells them that the full surface can actually be reconstructed or objectively aborted from protocol evidence. The hot path and the cold path do not carry different truths. The frontier binds the claimed surface compactly; the retrievability plane reconstructs or objectively aborts that same surface; both terminate on the same canonical close-or-abort object.
9.8
99% equal-authority ordering consensus
AFT’s ordering claim is a proof-carrying consensus theorem whose decisive object is revealed rather than manufactured by dense positive yes-votes. Revelation is not a weaker post hoc reporting layer here; it is the equal- authority surfacing mechanism for the uniquely valid public execution object already fixed by the closed public boundary. Theorem 4 (99% Equal-Authority Ordering Consensus). Assume:
- the closed bulletin surface Bh bound by the carried publication frontier and bulletin commitment is governed by a canonical bulletin close and protocol-native retrievability plane that deterministically yields extraction or abort,
- the cutoff object for slot h is canonical,
- bulletin commitments, compact publication-frontier bindings, and omission proofs are objectively verifiable,
- same-slot frontier conflicts and stale predecessor links admit short objective contradiction objects,
- the proof system is sound. Then even if 99% of validators behave arbitrarily, they cannot create a conflicting valid canonicalorder outcome for slot h. More strongly, every honest validator that observes the same closed ordering boundary derives the same positive order object or omission-dominated abort.
23
99% Byzantine suppress bulletin entries or publish Cbad
suppression or incomplete certificate
Public surface canonical cutoff τh bulletin Bh fixed
recoverable by any equal-authority validator
candidate proof surface
OC
er
th
h, Ω( or
Any honest validator extracts Bh derives OCerth or Ω(h, tx)
tx )
Public verifier checks proof soundness checks omission dominance objective acceptance rule
Safe outcome unique valid order admitted or bad candidate rejected
Figure 3: Omission-dominance attack and deterministic extraction. Even if a suppressing supermajority tries to hide admissible bulletin entries or promote an incomplete candidate certificate, any honest validator that reconstructs the same public surface derives the same valid OCerth or publishes a valid omission proof Ω(h, tx) that kills the bad candidate. Compact publication frontiers therefore internalize cheap same-slot and predecessor consistency checks on the live path, while recoverability remains the stronger assumption needed to turn that compact claim into a publicly reconstructable ordered set. The strongest shorthand is: 99% of validators may behave arbitrarily, because the closed ordering boundary admits one deterministically derivable close-or-abort outcome. This is equal-authority because any validator may reveal the winning certificate. It is 99%-fault tolerant because correctness does not depend on a dense majority of positive votes. This section isolates the ordering lane, not the theorem ceiling. Once composed with endogenous retrievability, canonical collapse, recovery and restart continuity, and collapse-bound sealed-effect gating, the promoted AFT theorem surface is exactly the paper’s relay-free deterministic 99% Byzantine Tolerance claim in the AFT model delta. With the accountable publication rules of Section 5, invalid positive ordering attempts are not only rejectable; they are also penalty-bearing and next-epoch removing.
10
Asymptote: Sealed Finality and Irreversible Effects
Asymptote is the two-tier settlement mode in the AFT family. It preserves fast BaseFinal chain progression while requiring stronger evidence before irreversible effects are released.
10.1
Finality tiers and collapse states
The finality tiers are: • BaseFinal: validator QC plus guardian certificate. • SealedFinal: BaseFinal plus sufficient sealing evidence. 24
Pending
base evidence
BaseFinal
divergence
start sealing
valid veto
Sealing
policy or evidence conflict complete witness / observer proof
Escalated / Invalid SealedFinal
Abort
Figure 4: The deterministic collapse surface for Asymptote. The slot collapse states are: • Pending • BaseFinal • Sealing • Abort • SealedFinal • Escalated • Invalid All honest nodes must derive the same collapse state from the same admissible evidence set.
10.2
SealedFinalityProof
The sealing plane gathers a proof object that binds: • the epoch, • the achieved finality tier, • the collapse state, • the guardian manifest hash, • the guardian decision hash, • the guardian counter, • the guardian trace root, • the guardian measurement root, • the policy hash, • witness certificates, when the witness path is used, • observer transcripts, transcript commitment, observer challenges, challenge commitment, and exactly one canonical observer outcome object when the observer path is used, 25
• divergence signals gathered during sealing. This object is block-scoped and guardian-bound. A SealedFinalityProof that is not bound to the slot’s guardian evidence is invalid.
10.3
Witness-backed sealing
The witness path assigns one witness committee per required certification stratum. Witness assignment is deterministic over: • the epoch seed, • the producer account id, • the slot (height, view), • the reassignment depth, • the witness stratum id, • the witness manifest hash. Sealed finality is reached on the witness path when: • BaseFinal holds, • each required witness stratum contributes a valid assigned witness certificate, • each witness certificate verifies against the registered witness manifest, • required checkpoints and append-only proofs are current enough under policy. Witness omission, stale registry participation, checkpoint inconsistency, or conflicting witness certificates produce explicit evidence rather than silent best-effort behavior.
10.4
Equal-authority observer sealing
The normative observer path is CanonicalChallengeV1. It treats sampled validators as deterministic duty assignees whose outputs must become public, recoverable protocol objects. Observer assignment is deterministic over: • the epoch seed, • the producer account id, • the slot (height, view), • the observation round, • the observer account id. The producer is excluded from its own observer pool. The runtime may also filter assignments through a correlation budget over provider, region, host class, and key-authority class. Each assigned observer publishes one of two things: 26
• a guardian-backed AsymptoteObserverTranscript, or • an objective AsymptoteObserverChallenge. A transcript binds the canonical slot surface: • the epoch and assignment, • the candidate block hash, • the guardian manifest, decision hash, counter, trace hash, and measurement root, • the guardian checkpoint root, • the observer verdict and veto kind, • the observer evidence hash. The admissible challenge basis is public-evidence-only: • MissingTranscript, • TranscriptMismatch, • VetoTranscriptPresent, • ConflictingTranscript, • InvalidCanonicalClose. Each challenge carries its own public evidence object: an assignment, an offending observation request, an offending transcript, or an offending canonical close. The challenge evidence_hash must bind exactly that carried evidence. The slot then carries three canonical bindings: • a transcript commitment over the transcript surface, • a challenge commitment over the challenge surface,
• exactly one canonical outcome object: AsymptoteObserverCanonicalClose or AsymptoteObserverCanonicalA The collapse rule is close-or-abort and challenge-dominant: • SealedFinal if BaseFinal holds, the deterministic assignment set is fully covered by valid canonical Ok transcripts, the transcript and challenge commitments verify, the challenge surface is empty, and the canonical close object is valid. • Abort if the transcript and challenge commitments verify, the challenge surface is non-empty, and the canonical abort object is valid. • Pending otherwise. Challenge dominance is a theorem-level veto, not an operational alarm. A valid challenge collapses the slot to abort before any penalty, governance, or membership aftermath is considered. This makes observer sealing structurally parallel to canonical ordering: public evidence, canonical commitments, a unique positive object, a unique negative object, and deterministic local close-orabort derivation from the same public surface. 27
10.5
Divergence signals and escalation
The sealing plane may also emit divergence signals, including: • conflicting guardian certificates, • witness omission, • stale registry use, • stale checkpoints, • transparency-log consistency failure. These signals support Escalated and Invalid outcomes and give operators a fail-closed evidence trail.
10.6
Sealed effects and replay-safe release
Irreversible effects are gated by finality tier. The effect plane distinguishes between: • BaseFinal effects, which are allowed on the fast path when policy permits, • SealedFinal effects, which require a valid SealedFinalityProof. For proof-enabled irreversible effects, Asymptote carries a self-contained SealObject whose current instantiation includes: • an EffectIntent, • an EffectPublicInputs object, including canonical_collapse_hash, • an EffectProofEnvelope, • a replay-safe nullifier. In the runtime, SealedFinal secure-egress requests carry both the SealedFinalityProof and the slot’s CanonicalCollapseObject. The guardian-side seal builder and downstream receipt verifier recompute the same canonical_collapse_hash from that collapse object together with the proof-carried observer surface, so a challenge-dominated or otherwise mismatched slot cannot authorize irreversible release. The release rule is
Release(e) ⇐⇒ BaseFinal(slot(e))∧SealedFinal(slot(e))∧VerifySealObject(e)∧CollapseHash(e) = Hash(Collapse( This keeps the hot path sparse while making released consequences deterministic and replay-safe.
28
10.7
Deterministic observer theorem
The deterministic Asymptote observer model now proves the following kernel: • base certificates are unique per slot, • canonical observer close objects are unique per slot, • canonical observer close and canonical observer abort cannot coexist for the same slot, • a challenge-dominated slot cannot produce a valid sealed release. Theorem 5 (Deterministic Equal-Authority Observer Sealing). Assume sound deterministic observer assignment, signature-sound guardian-backed observer transcripts and challenges, canonical transcript and challenge commitments, append-only registry and log publication once published, and deterministic transcript/challenge derivation over the closed public observer surface. Then arbitrary behavior by the rest of the validator set cannot create a conflicting valid canonical observer close, cannot make canonical close and canonical abort coexist for the same slot, and cannot authorize a valid sealed irreversible effect release for a challenge-dominated slot. This theorem is the observer-lane analogue of canonical ordering’s public certificate theorem: public evidence, canonical commitments, negative-authority dominance, and deterministic local close-or-abort derivation from the same public observer surface. Under the accountable publication rules of Section 5, the same observer challenges are also penalty-bearing objective faults. Unsafe positive close attempts therefore become not only rejectable, but accountable and epoch-removing.
10.8
Legacy sampled comparison
Before CanonicalChallengeV1, the observer lane was typically described through a sampled affirmative bound. Let: • h be the honest fraction of equal-authority validators, • Ajs be the sampled observer committee for slot s and round j, • kj = |Ajs |, • pbeacon_bias be the probability of sufficient beacon bias, • pveto_suppression be the probability that a valid veto surface is fully suppressed. Then the old affirmative sampled lane admitted the analytical bound Punsafe (s) ≤ pbeacon_bias · pveto_suppression ·
(1 − h)kj .
Y j
For constant committee size k across r rounds: Punsafe (s) ≤ pbeacon_bias · pveto_suppression · (1 − h)kr . That formula remains a useful historical comparison, but it is no longer the normative theorem for the observer lane. Under CanonicalChallengeV1, sampling determines duties, not safety. Safety comes from the canonical public transcript surface, the canonical public challenge surface, and the close-or-abort split that those surfaces induce. The runtime publishes the canonical observer transcript, commitment, challenge, challenge commitment, and close-or-abort objects as ordinary guardian_registry transactions after the sealed header is formed. The same surface is carried inside the proof for immediate block verification. 29
11
NestedGuardian: Witness-Augmented Research Mode
NestedGuardian explores a layered threshold construction: • validators run the AFT deterministic message flow, • each proposal carries its guardian committee certificate, • external witness committees cross-check the slot, • chain state anchors witness assignments, witness manifests, and slashing evidence. The instantiated runtime scope includes: • deterministic witness assignment from the active witness set, • registered on-chain witness manifests, • witness certificates bound into guardianized slot certificates, • safety proofs for the witness-augmented kernel, • bounded model checking for reassignment, outage, and checkpoint transitions. The instantiated proof package consists of: • safety formalization, • bounded operational model checking for reassignment, outage, and checkpoint transitions, • a discharged composed-liveness bridge under the target eventual-fair scheduler through the recurrence/reduction/totality/collapse chain together with a matching persistent churn/restart simulator. NestedGuardian is therefore a witness-augmented mode with a finished theorem bridge. It is experimental as an operational mode, not as a theorem crutch. Its witness-coded family supplies an explicit constructive recovery carrier and completed bridge artifacts; it does not reduce the promoted AFT theorem surface to an experimental-only claim. That constructive recovery carrier is a witness-coded publication-bundle recovery contract with compact hot-path bindings and cold-path registry-driven close-or-abort resolution. The abstract coded recovery-family contract is realized by the parametric SystematicXorKOfKPlus1V1 parity family plus the bounded true non-parity SystematicGf256KOfNV1 family with at least two parity shares, implemented with systematic Cauchy-style coefficients and exercised in bounded 2-of-4, 3-of-5, 3-of-7, 4-of-6, and 4-of-7 lanes. These lanes resolve from threshold-many public reveals, objective recovered-support conflict, or deterministic missingness. The bounded 3-of-5, 4-of-6, and 4-of-7 lanes restore or exceed threshold-support overlap while the bounded 3-of-7 lane shows that recovered-support conflict remains fail-closed even when overlap is absent. A bounded conformance harness checks that every threshold-sized reveal subset reconstructs and every below-threshold subset fails across the shipped XOR and GF256 realizations of that contract. Those recovered reveals lift deterministically into an explicit positive close-extraction payload and then into an explicit extractable bulletin-surface payload that binds the verifying publication bundle, verifying canonical bulletin close, canonical bulletin-availability bytes, and sorted bulletin entries. 30
The completed bounded family also carries the ordinary durable and restart surfaces. A bounded recovered-only two-slot harness shows that consecutive recovered surfaces derive the ordinary publication-frontier predecessor chain and the same authoritative CanonicalCollapseObject predecessor chain without the ordinary publication-bundle lane. A second bounded recovered-only harness shows a close/abort/close bulletin window with a recovered omission-dominated middle slot: recovered data alone materializes the ordinary positive closes and extracted bulletin surfaces on the outer slots, materializes the ordinary omission-dominated abort in the middle while keeping omission evidence and recovered bulletin entries public, and preserves the same authoritative collapse continuity chain. A bounded read-side harness shows that the same recovered-only durable chain yields the same compact replay-prefix / state-root continuity view that the ordinary lane exposes plus a bounded recovered canonical-header prefix. The execution module verifies that replay tip as the same restart anchor the ordinary lane uses, retains both recovered prefixes in execution state, and uses the recovered canonical-header ancestry for bounded anchored reads plus parent-block / parent-state-root continuity after restart when ordinary recent blocks are absent. Validator consensus orchestration derives the same bounded recovered restart parent anchor from the recovered canonical-header / collapse surface when the ordinary committed block is absent, and the GuardianMajority engine consumes that bounded recovered canonical-header prefix as restart-time parent/QC context for synthetic parent-height QC continuity when the full committed block is absent. The same recovered surface yields a bounded recovered certified-header window plus a restart-only recovered BlockHeader / QC cache window for restart-time header / QC lookup plus bounded QC-certified recovered branch reconciliation over the configured local five-entry window. Those windows fold by exact overlap with a configurable budget, exercised at five windows into a longer seventeen-step recovered certified branch without ordinary committed headers. Those same cold-path loaders consume a configurable exact-overlap segment budget, exercised at four exact-overlap segments into a longer fifty-three-step recovered certified branch with direct registry-extraction parity and explicit interior-overlap conflict rejection. Those same restart loaders also compose two overlapping four-segment exact-overlap folds into a longer eightynine-step recovered certified branch with direct registry-extraction parity and explicit inter-fold overlap conflict rejection, and tests exercise the same recursive carrier at three overlapping foursegment folds into a one-hundred-twenty-five-step recovered certified branch. The runtime has a bounded conformance harness over one, two, and three stitched segment folds, matching the same production-loader / registry-extraction carrier at the corresponding fifty-three-step, eighty-nine-step, and one-hundred-twenty-five-step branches. The restart path also pages older exact-overlap segment folds on demand beneath that bounded suffix via an overlap-checked cursor while keeping only the bounded recent suffix plus the streamed page live in engine caches, and tests exercise that paged carrier at a longer two-hundred-thirty-threestep recovered certified branch with direct registry-extraction parity plus explicit duplicate-page, missing-gap, and late-page overlap rejection. Restart therefore streams recovered certified ancestry until target height or recovered-history exhaustion without a theorem-relevant fixed depth bound. The archival internalization layer uses an active archived-recovered-history profile naming retention horizon, exact-overlap paging geometry, segment / fold geometry, checkpoint update rule, and profile evolution. Archived segments, archived restart pages, archival checkpoints, and archival retention receipts bind to historically referenced profile hashes and governing activation hashes under a published profile-activation chain before archived continuation is trusted, and ordinary canonical collapse history names the archived checkpoint / activation pair that archived restart is authorized to follow. Archived replay and archived publication correctness are historical and index-free: they follow the canonical-collapse-anchored or object-carried activation hash plus predecessor/checkpoint history rather than whichever archived activation is merely latest in local state. 31
When the recovered certificate carries objective omission proofs, the same recovered lane routes into the ordinary OmissionDominated abort path while keeping omission evidence and recovered bulletin entries public. The recovery-family contract, canonical-collapse / replay retrievability anchor, and recovered-state historical retrievability surface are therefore part of ordinary endogenous AFT history rather than a narrower theorem-side qualifier. The directly discharged recurrence/reduction/totality/collapse chain closes the former distance to the relay-free deterministic 99% Byzantine Tolerance theorem in MAFT , so no recoverability or architecture-specific semantic gap remains at the AFT theorem surface.
12
Security and Assumption Surface
The AFT family depends on explicit assumptions. They are not optional prose. Layer
Required assumptions
Failure consequence
Base finality
current manifests, current epoch state, majority thresholds, guardian non-equivocation, valid checkpoints, enough validators and guardians to reach quorum objective publication, compact publication-frontier binding and contradiction rules, canonical cutoff, deterministic eligibility, append-only bulletin commitment, proof soundness, protocol-native retrievability profile / manifest / custody / challenge surface, canonical bulletin-close extraction-or-abort, cheap omission verification, accountable omission publication valid asymptote policy, current witness seed, valid witness or observer assignments, checkpoint freshness, valid log consistency proofs, deterministic transcript/challenge derivation, accountable challenge publication correct finality-tier policy, sound verifier metadata, nullifier uniqueness, intent/public-input binding sound witness assignment and registration, correct reassignment handling, witness committee non-equivocation
conflicting base-finality evidence or loss of progress
Canonical ordering
Sealed finality
Sealed effects NestedGuardian
loss of compact frontier consistency, deterministic extraction-or-abort, accountability, or the ordering theorem
incorrect sealed release, loss of accountability, or fail-closed stalling
replay or unsafe irreversible effect release degraded safety or open liveness behavior
The family-level discipline is simple: if an assumption fails, AFT should degrade to stalling, aborting, or withholding release before it degrades to unsafe irreversible behavior.
13
Formal Results
The repository’s machine-checked surfaces align with the protocol family as follows:
32
Formal module
Core proved results
GuardianMajorityProof GuardianMajority
QuorumCertificatesIntersect, InvariantImpliesSafety executable bounded checks for finalization witness soundness and slot safety InvariantImpliesCertifiedUniqueness, InvariantImpliesRecoverability, InvariantImpliesOmissionDominates executable bounded checks for publication, cutoff, certification, omission, and recoverability InvariantImpliesBaseSafety, InvariantImpliesCanonicalCloseSafety, InvariantImpliesCloseAbortExclusive, InvariantImpliesAbortDominatesSealed executable bounded checks for transcript publication, challenge publication, canonical close, and canonical abort witness-assignment soundness, witness-certificates-stay-assigned, InvariantImpliesSafety executable bounded checks for reassignment, outage, and checkpoint admissibility
CanonicalOrderingProof CanonicalOrdering
AsymptoteProof Asymptote
NestedGuardianProof NestedGuardian
Every formal artifact named in this section, and every additional proof artifact cited by file name below, is embedded verbatim in Appendix A so that the served yellow paper remains self-contained outside the repository. These formal surfaces prove the deterministic safety kernels that the broader classical-agreement bridge builds on. The full ordinary classical 99% Byzantine agreement sentence is then completed by the recurring, reduction, totality, and collapse layers discussed above, rather than by these module-local safety kernels in isolation. Compact publication-frontier summaries internalize sameslot and predecessor consistency on the live path, while the protocol-native retrievability plane internalizes closed-bulletin extraction-or-abort as an endogenous part of the realizing architecture rather than a purely algebraic consequence of the authenticated message transcript alone. The accountable-adversary variant therefore composes these formal kernels with runtime accountability rules rather than replacing them: replay-deduplicated objective fault publication and optional policy-controlled membership updates live in the implementation and policy layer above the proved deterministic core.
13.1
Complete omission-dominance witness artifact
The formal package includes an executable TLC witness module, internal-docs/architecture/protocols/aft/fo paired with internal-docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrderingO The exact module and configuration are embedded in Appendix A.5.1 and Appendix A.5.2; the summary below highlights the executed public-evidence shape that the witness reaches. Executed witness trace. The module intentionally asks TLC to violate the state predicate NoOmissionDominanceWitness so that the checker emits a concrete public evidence trace. The executed trace is:
- PublishStep: tx1 enters slot 1’s bulletin surface.
- PublishStep: tx2 enters the same bulletin surface.
- CloseCutoffStep: the canonical cutoff closes and the recoverable set becomes {tx1, tx2}.
- CandidateCertifyStep: a candidate certificate for {tx1} appears.
- ProveOmissionStep: an omission proof for tx2 against that candidate certificate appears. 33
The same formal package carries a bounded recursive-continuity model, internal-docs/architecture/protoco paired with internal-docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalCollapseR The exact source of both artifacts is embedded in Appendix A.5.3 and Appendix A.5.4. That model captures the reference HashPcdV1 continuity carrier directly: deterministic recursive proof steps, predecessor-proof hashing, CanonicalCollapseExtensionCertificate carriage, and the rule that non-genesis header admission depends on the anchored predecessor proof relation. The runtime exposes a SuccinctSp1V1 backend seam for those same recursive public inputs, and that seam is exercised by consensus verification and durable-state gating. The formal model still stops at the reference carrier rather than mechanizing a cryptographic recursive accumulator or ZK backend. At the final state, the incomplete candidate certificate remains unadmitted while the omission proof is present. In the executable model this happens because the admitted object must already equal the canonical set; the trace therefore does not replace the theorem. Its purpose is narrower and useful: it gives a bounded, executed witness of the exact public-evidence shape from which omission dominance follows. Readers can run the trace directly and inspect the six-state witness without reconstructing the paper’s argument by hand.
14
Implementation Correspondence
This section is non-normative. It names the exact runtime symbols that carry the protocol objects defined above.
14.1
Core ordering symbols
The core ordering data structures and free functions are public Rust symbols re-exported through ioi_types::app. They are the runtime carriers for the abstract ordering objects and verifier rules defined above. Abstract object
Current runtime symbols
Bulletin surface commitment Compact publication availability binding Compact publication frontier Publication-frontier contradiction Canonical ordering proof families
BulletinCommitment, BulletinSurfaceEntry PublicationAvailabilityReceipt PublicationFrontier PublicationFrontierContradiction CanonicalOrderProofSystem, with concrete variants HashBindingV1 and CommittedSurfaceV1 CanonicalOrderPublicInputs CommittedSurfaceCanonicalOrderProof OmissionProof CanonicalOrderCertificate canonical_order_tx_hashes canonical_publication_availability _receipt_hash, canonical_publication_frontier_hash, canonical_publication_frontier _contradiction_hash build_publication_availability_receipt, build_publication_frontier, verify_publication_frontier, verify_publication_frontier_contradiction
Canonical public-input tuple Live succinct witness payload Omission evidence Order certificate Canonical ordering function
Publication-frontier hashing
Publication-frontier construction / verification Public-input hashing Reference proof construction Live certificate construction Certificate verification
canonical_order_public_inputs, canonical_order_public_inputs_hash build_reference_canonical_order _proof_bytes build_committed_surface_canonical _order_certificate verify_canonical_order_certificate
34
14.2
Guardian and sealing symbols
The guardian, witness, observer, and sealed-effect objects are likewise public Rust symbols reexported through ioi_types::app. They encode the exact evidence surface checked by validators and downstream gateways. Abstract object
Current runtime symbols
Guardian slot certificate Witness certificate Equal-authority observer assignment Correlation budget Observer observation request Observer transcript Observer transcript commitment Observer challenge
GuardianQuorumCertificate GuardianWitnessCertificate AsymptoteObserverAssignment
Observer challenge commitment Canonical observer close Canonical observer abort Finality tier Collapse state Sealing policy Observer statement Observer certificate Divergence signal Sealed finality proof Observer binding for sealed effects Proof-carrying effect object
14.3
AsymptoteObserverCorrelationBudget AsymptoteObserverObservationRequest AsymptoteObserverTranscript AsymptoteObserverTranscriptCommitment AsymptoteObserverChallenge, with kinds MissingTranscript, TranscriptMismatch, VetoTranscriptPresent, ConflictingTranscript, and InvalidCanonicalClose AsymptoteObserverChallengeCommitment AsymptoteObserverCanonicalClose AsymptoteObserverCanonicalAbort FinalityTier, with variants BaseFinal and SealedFinal CollapseState, with variants Pending, BaseFinal, Sealing, Abort, SealedFinal, Escalated, and Invalid AsymptotePolicy AsymptoteObserverStatement AsymptoteObserverCertificate DivergenceSignal, DivergenceSignalKind SealedFinalityProof sealed_finality_proof_observer_binding SealObject
Verifier, orchestration, and persistence symbols
Verification and orchestration entry points are split across four public namespaces: ioi_types::app, ioi_crypto::sign::guardian_committee, ioi_services::guardian_registry, and the GuardianMajorityEngine runtime. Engine-local checks are named here by their exact method identifiers.
35
Responsibility
Current runtime symbols
Guardian certificate verification Witness certificate verification
verify_quorum_certificate verify_witness_certificate derive_asymptote_observer_assignments, derive_asymptote_observer_plan_entries GuardianContainer::observe_asymptote_request, GuardianContainer::request_remote_asymptote _observer_observation, GuardianContainer::sign_consensus_with_guardian GuardianMajorityEngine::verify_asymptote _canonical_observer_sealed_finality, GuardianMajorityEngine::verify_asymptote _sealed_finality GuardianMajorityEngine::verify _canonical_order_enrichment; published CanonicalOrderAbort dominates positive order certificates and inconsistent mixed parent state
Deterministic observer assignment
Observer-side transcript / challenge derivation
Sealed finality verification in the engine
Canonical-order enrichment verification in the engine
Publication-frontier enrichment verification in the engine Block finalization attachment of order certificates Block finalization attachment of publication frontier Canonical observer proof publication Sealed-effect construction and checking Guardianized proposal verification in the engine Base-engine safety and timing Bulletin and order-certificate state access Publication-frontier state access Ordering close-or-abort derivation
Ordering abort taxonomy Protocol-wide collapse derivation and verification
Proposal-surface recursive continuity
Bulletin, order, and collapse state access
GuardianMajorityEngine::verify _publication_frontier_enrichment; published PublicationFrontierContradiction dominates conflicting or stale frontiers build_committed_surface_canonical _order_certificate during finalization build_publication_frontier during finalization canonicalize_observer_sealed_finality_proof, publish_canonical_observer_artifacts build_http_egress_seal_object, verify_seal_object GuardianMajorityEngine::verify _guardianized_certificate SafetyGadget, Pacemaker, TimeoutCertificate load_bulletin_commitment, load_canonical_order_certificate GuardianRegistry::load_publication_frontier, GuardianRegistry::load_publication _frontier_contradiction derive_canonical_order_execution_object, derive_canonical_order_public_obstruction CanonicalOrderAbortReason::MissingOrderCertificate, BulletinSurfaceReconstructionFailure, BulletinSurfaceMismatch, InvalidBulletinClose, OmissionDominated, CertificateHeightMismatch, RandomnessMismatch, OrderedTransactionsRootMismatch, ResultingStateRootMismatch, InvalidPublicInputsHash, InvalidBulletinAvailabilityCertificate, InvalidProofBinding derive_canonical_collapse_object, GuardianMajorityEngine::verify_published _canonical_collapse_object BlockHeader::previous_canonical_collapse_commitment_hash, BlockHeader::canonical_collapse_extension_certificate, CanonicalCollapseExtensionCertificate, CanonicalCollapseCommitment, verify_block_header_canonical_collapse_evidence, ConsensusDecision::ProduceBlock load_bulletin_commitment, load_canonical_order_certificate, load_canonical_order_abort, load_canonical_collapse_object publish_aft_publication_frontier@v1, publish_aft_canonical_order_artifact_bundle@v1, publish_aft_canonical_order_abort@v1, publish_aft_canonical_collapse_object@v1, report_aft_omission@v1, 36 publish_asymptote_observer_transcript@v1, publish_asymptote_observer_transcript_commitment@v1, report_asymptote_observer_challenge@v1, publish_asymptote_observer_challenge_commitment@v1, publish_asymptote_observer_canonical_close@v1,
These symbols are named here so that the paper maps directly onto the current runtime without making the reader chase separate prose specifications. In the implementation, validator finalization publishes a protocol-visible CanonicalCollapseObject through publish_aft_canonical_collapse_object@v1 after local post-commit header enrichment, guardian_registry exposes load_canonical_collapse_object, and GuardianMajorityEngine::verify_publi cross-checks any published copy against the proof-carried header surface when it is available. The externally finalized AFT commit path persists the same object keyed by slot height, rather than treating ordering and sealing close-or-abort evidence as loose enrichments detached from state persistence. The same post-commit path also builds PublicationFrontier via build_publication_frontier and publishes it through publish_aft_publication_frontier@v1; GuardianMajorityEngine::verify_publication_frontier_enrichment rechecks same-slot binding, predecessor linkage, and any dominating contradiction object. In the current proposal-surface continuity slice, validator orchestration now signs both previous_canonical_collapse_commitment_hash and a typed CanonicalCollapseExtensionCertificate into each produced AFT block header. In the current clean-break runtime slice, CanonicalCollapseObject itself carries continuity_accumulator_hash and continuity_recursive_proof, so the certificate now carries the predecessor commitment plus predecessor proof hash rather than an explicit carried ancestor vector, full predecessor collapse object, or predecessor recursive proof object. Asymptote leaders stall rather than produce when that required extension certificate is unavailable, proposal verification recursively checks that the carried predecessor commitment hash matches the signed predecessor link, checks that the predecessor commitment’s resulting state root matches the signed parent-state root, and rechecks those carried public inputs against the anchored predecessor collapse object when one is available. QC promotion therefore relies on a reference recursive proof-carrying continuity relation rather than on a recomputed predecessor digest alone, and only treats continuity-linked headers as progress-bearing.
15
Benchmark Context
The performance evidence in this paper has two sources: • literature-reported baselines for HotStuff, Narwhal/Tusk, and Bullshark, • the repository’s native benchmark_throughput target for matched GuardianMajority and Asymptote scenarios. The purpose of this section is architectural positioning, not false equivalence across unmatched environments.
15.1
Paper-reported baselines
System HotStuff baseline Narwhal-HotStuff Narwhal-HotStuff with additional workers Tusk Bullshark
Reported throughput
Reported latency
1,800 tx/s
1s
130,000 tx/s up to 600,000 tx/s 160,000 tx/s 125,000 tx/s
under 2 s n/a
Narwhal/Tusk comparison setting Narwhal/Tusk paper Narwhal/Tusk paper
about 3 s about 2 s
Narwhal/Tusk paper Bullshark paper
37
Source type
The baseline interpretation is: • HotStuff demonstrates the leader-based partially synchronous baseline, • Narwhal-HotStuff demonstrates the gain from separating dissemination from ordering, • Bullshark demonstrates high-throughput DAG-oriented ordering, • AFT adds a new separation: order surfacing and effect release are no longer identified with dense positive voting.
15.2
Native repository measurements
No performance measurement in this section is load-bearing for any theorem in this paper; the promoted theorem surface stands independently of benchmark tuning, harness state, or optimization maturity. The corrected native measurements below were produced on March 21, 2026 after bringing the repository’s native AFT benchmark path back into sync with the current GuardianMajority / base_final harness semantics: • shared-tip readiness no longer treats a transient get_status.height = 0 as authoritative when a resilient tip probe already sees committed blocks, • submission alignment and leader-targeted ingress now use a resilient tip block rather than a potentially stale status height, • authoritative chain-commit scans start from the resilient pre-submission tip instead of rescanning stale empty-block prefixes, • sustained throughput for fast probes now stops on the authoritative full-chain commit scan for the highest committed height; sampled committed-status visibility is retained only as an auxiliary lag diagnostic, • the benchmark surface now exposes alignment, spill, and replay diagnostics explicitly so missed due blocks or replay churn are not hidden behind a single TPS number. The table below reports the current matched bulk-throughput proof point for the native GuardianMajority 4-validator base_final scenario under that corrected harness. This is a repository-native AFT proof point on the Jellyfish state path with a ‘1 s‘ block interval, not an apples-to-apples claim against published Narwhal/Tusk/Bullshark environments. scenario guardian_majority_4v_base_final_bulk
validators
attempted
accepted
committed
blocks
inj. tps
sust. tps
p50
p95
p99
sealed p50
sealed p95
4
16384
16384
16384
1
21370.89
9647.66
1293.45
1603.73
1695.24
–
–
These measurements imply four things: • the earlier single-digit and low-hundreds TPS reports were artifacts of benchmark-path bugs rather than of the protocol surface itself, • the current repository now clears the lower edge of the intended 8k–16k TPS range in a matched native 4-validator GuardianMajority bulk probe, 38
• on this corrected probe the batch lands in a single block, so the main remaining AFT work is ceiling-raising and aggregate-domain multiplication rather than recovering from a broken harness, • these values should be read as corrected repository baselines, not as optimized ceilings and not as apples-to-apples superiority claims over published Narwhal/Tusk/Bullshark environments.
16
Related Work
Geeq’s Proof of Honesty (PoH) is important prior work in the “99%” direction: it argues for globally honest and canonical chain recovery in pure software under assumptions including at least one honest node and an honest relay, and it uses public evidence plus user-side verification to push beyond ordinary dense-vote intuition [9]. AFT differs in a key respect: it is relay-free and coordinator-free. Correctness does not depend on any designated honest relay, broadcaster, or privileged recovery role. Instead, durable ordering and sealed effects collapse through protocol-native public-evidence objects whose negative forms are immediately decisive. Narwhal/Tusk and Bullshark separate dissemination from ordering, but they still ground ordering safety in dense positive certificates and quorum-intersection arguments over the ordered object itself [2, 3]. HoneyBadgerBFT and Dumbo move to asynchronous common-subset or MVBA-style agreement, but they still rely on classical Byzantine-majority thresholds rather than a public-statecontinuity theorem over a canonical public surface [4, 5]. Chainlink CCIP and optimistic cross-chain mechanisms add secondary monitoring layers, risk-management committees, or challenge windows to detect and halt bad transfers, but the decisive recovery rule is operational or economic rather than the immediate acceptance of a uniquely valid proof-carrying canonical object recoverable by any equal-authority validator [8]. Accountable subgroup multisigs and finality gadgets add equivocation evidence and slashing, yet still keep dense subgroup votes as the positive safety object [6, 7]. AFT differs by making ordering and sealed release relay-free public-evidence close-or-abort objects with dominant negative proofs: honest validators that observe the same closed public boundary derive the same decisive object, and publication is downstream of that deterministic derivation rather than its source.
17
Claims and Non-Claims
17.1
Claims
This paper claims: • a production guardian-backed base-finality model in which validator quorums are composed with guardian committee admissibility, • proof-carrying canonical ordering with omission dominance and uniqueness, plus protocol-native endogenous retrievability, • compact signed publication-frontier summaries and short contradiction objects that internalize same-slot and predecessor consistency on the live path, • a public-state-continuity formulation in which closed slot boundaries admit at most one positive public execution object and conflicting candidates admit short objective obstruction witnesses, • 99% equal-authority ordering consensus under explicit assumptions, 39
• deterministic sealed-effect collapse with challenge dominance, • a relay-free, coordinator-free, pure-software model-delta theorem yielding deterministic 99% Byzantine Tolerance for durable ordering and sealed-effect safety over the explicit bulletin / retrievability surface, • that the whole AFT stack breaks the classical indefinite-suppression lower bound by identifying the first illegal adversary step and realizing the visibility delta without a trusted relay, • a witness-augmented mode for layered threshold constructions, • machine-checked deterministic safety kernels for the major protocol surfaces.
17.2
Non-claims
This paper does not claim: • that public state continuity arises for free inside the classical DLS / PBFT partially synchronous message-passing model, • that the classical n > 3f / f < n/3 lower bound has been refuted inside that bare model; the claim is instead that AFT operates in the explicit MAFT model delta where the adversary cannot indefinitely suppress published admissible artifacts from correct parties after stabilization. Remove that visibility resource, or realize it circularly through the same Byzantine-majority relay set, and the paper is no longer claiming the same result. This is not a retreat; it is the exact location of the break. AFT does not merely vary a parameter inside the dense-vote carrier. It replaces the carrier with direct dissemination plus compressed public echo and states the new proof obligation at theorem surface, • freedom from bulletin-publication, protocol-native retrievability obligations, or proof-soundness assumptions, • that compact publication-frontier summaries make the bulletin surface self-extracting inside the classical authenticated-message model, • a full asynchronous liveness theorem under arbitrary registry, log, witness, and outage schedules, • an apples-to-apples measured throughput superiority over HotStuff, Narwhal, Tusk, or Bullshark from the current repository alone.
17.3
Model-delta public-state-continuity theorem
The runtime supports a stronger theorem than the older accountable summary because the mechanism and system model are now stated directly at theorem surface. Theorem 6 (Relay-Free Deterministic 99% Byzantine Tolerance in MAFT ). Assume the system model of Section 5, including the direct-dissemination / compressed-echo delta of Lemma 1, guardian non-equivocation, proof soundness, compact signed publication-frontier summaries whose same-slot and predecessor-link contradictions are objectively checkable, protocol-native retrievability objects plus canonical bulletin-close extraction-or-abort for the bulletin surface bound by those frontiers, deterministic transcript/challenge derivation for sealing, durable state advancement only through canonical collapse, and irreversible-effect release only through collapse-bound sealed proofs. Then up 40
to 99% of validators may behave arbitrarily without creating a conflicting valid durable canonicalorder outcome or a conflicting valid sealed-effect release outcome. Honest validators that observe the same closed public boundary derive the same close-or-abort result; publication, penalties, and validator-set updates only accelerate convergence and future hygiene. The classical n > 3f / f < n/3 threshold is not load-bearing in MAFT , because the classical adversary’s indefinite-suppression step is no longer legal. The theorem does not claim that DLS / PBFT has been refuted inside MDLS . It claims that AFT is not a member of that model: the first illegal lower-bound adversary step is indefinite suppression of a published admissible artifact from correct parties after stabilization. Bulletin close, publication frontier, retrievability, recovery, restart continuity, canonical collapse, and collapse-bound sealing are not theorem-side caveats; they are the protocol-internal realizing mechanism of MAFT . A criticism that AFT “changes the model” is therefore descriptive rather than fatal unless it identifies circular realization of the visibility resource or a hidden relay, coordinator, TEE, bootstrap oracle, or external recovery service. The theorem is stronger than the older accountable summary because invalid positive objects are not merely rejectable or penalty-bearing. They are already dominated by deterministic negative objects and collapse-gated durable state before any penalty logic runs. Readers trained on dense-vote BFT will be tempted to treat the absence of quorum-intersection safety as disqualifying. In AFT, that is precisely the point: authority is carried by uniquely valid public execution objects and omission-dominant contradiction witnesses, with durable advancement gated by canonical collapse. Compact publication frontiers keep the live hot path cheap by internalizing consistency and lineage checks, while the protocol-native retrievability plane discharges deterministic extraction-or-abort on the full bulletin surface. The recurrence / reduction / totality / collapse chain is not narrative glue. Its exact artifact chain is embedded verbatim in Appendix A, ending in the classical-agreement collapse wrapper itself. Theorem 7 (Realizing-Mechanism Statement). The new publication-frontier slice is not the theorem by itself; the theorem is the promoted AFT model-delta sentence, carried by the full AFT publicevidence continuity architecture. Compact signed publication-frontier summaries, compact availability receipts, short frontier contradiction objects, endogenous retrievability profiles, manifests, custody assignments, custody receipts, custody responses, retrievability challenges, canonical extraction-orabort, canonical collapse, and historical retrievability together realize the direct-dissemination / compressed-echo visibility resource stated above. Removing that protocol-native retrievability plane removes part of the realizing mechanism rather than merely shaving off an optional refinement. Proposition 2 (Scoped Witness-Coded Constructive Corollary). Assume the hypotheses of the relayfree deterministic 99% Byzantine Tolerance theorem in MAFT , plus sound witness assignment and witness certificate binding, a completed witness-coded recovery family with compact hot-path bindings and cold-path share delivery / reveal / reconstruction, and availability of the retained recovered publication surface together with any older recovered-history pages needed for restart-time extraction. Then the NestedGuardian witness-coded carrier deterministically materializes the same positive close or canonical abort surface, the same authoritative collapse chain, the same replayprefix / restart-anchor surface, and the same restart-time canonical-header / certified-header / block-header ancestry surface as the ordinary lane for the completed recovery families. Restart can therefore stream recovered certified ancestry until target height or recovered-history exhaustion without a theorem-relevant fixed depth bound, while keeping only compact bindings on the hot path and bounded-memory paging on the restart path. 41
This runtime result is stronger than the separation closeout because it no longer stops at “compact frontiers bind a recoverability claim.” It shows that the live AFT stack can re-materialize the same durable and restart-critical surfaces without violating the throughput guardrails, while keeping deeper recovered history inside ordinary endogenous AFT state. This is one constructive route to Byzantine agreement in a realizable permissioned model delta rather than a weaker contrast class. In the classical dense-vote presentation, worst-case progress is usually phrased in terms of > 2/3 honest participation and quorum intersection as the main safety mechanism. In AFT’s realization, authority is obtained instead through uniquely valid publicevidence objects plus dominant negative proofs, without trusted relays, privileged coordinators, TEEs, or dense positive quorum intersection. The live publication-frontier slice internalizes compact same-slot and predecessor consistency on the hot path, while explicit recoverability of the bound bulletin surface, canonical collapse, and historical retrievability complete the same AFT model-delta theorem. Publication and accountability serve as reinforcement rather than the source of correctness. Liveness then follows from direct authenticated dissemination, compressed echo visibility, and eventual publication of the protocol-defined artifacts, and the recurrence/reduction/totality/collapse chain closes that route formally. That is the precise sense in which the classical n > 3f / f < n/3 barrier stops being load-bearing here: the promoted theorem no longer grants the adversary indefinite suppression of published admissible information. The correct one-line summary is: AFT is a proof-carrying, guardian-backed, omission-dominant consensus and settlement family in which base finality, canonical ordering, and irreversible-effect release are separated and then recomposed through shared evidence.
A
Embedded Formal Artifacts
This appendix embeds verbatim every proof artifact referenced by name in the yellow paper, together with the repository path from which it is sourced. The goal is to keep the served paper self-contained even when it is read outside the repository. The artifacts are grouped by protocol surface and rendered with line numbers so the appendix reads as a standalone proof bundle rather than as a raw repository dump.
42
A.1
GuardianMajority
Core guardian-backed base-finality model and proof.
A.1.1
GuardianMajorityProof.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/gu ardian_majority/GuardianMajorityProof.tla}
1 2
---- MODULE GuardianMajorityProof ---EXTENDS Naturals, FiniteSets, TLAPS
3 4
CONSTANT Validators, Blocks, Slots, Epochs, QuorumSize
5 6 7 8 9 10
ASSUME QuorumIntersection == \A S, T \in SUBSET Validators : /\ Cardinality(S) >= QuorumSize /\ Cardinality(T) >= QuorumSize => S \cap T # {}
11 12
VARIABLES votes, certs
13 14
vars == <<votes, certs>>
15 16 17
VoteDomain == Validators \X Slots \X Blocks \X Epochs CertDomain == Slots \X Blocks \X Epochs \X (SUBSET Validators)
18 19 20 21
Init == /\ votes = {} /\ certs = {}
22 23 24
HasVote(v, s) == \E b \in Blocks, e \in Epochs : <<v, s, b, e>> \in votes
25 26 27 28 29 30
VoteStep == \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : /\ ~HasVote(v, s) /\ votes' = votes \cup {<<v, s, b, e>>} /\ UNCHANGED certs
31 32 33 34 35 36 37
CertifyStep == \E s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators : /\ Cardinality(Q) >= QuorumSize /\ \A v \in Q : <<v, s, b, e>> \in votes /\ certs' = certs \cup {<<s, b, e, Q>>} /\ UNCHANGED votes
38 39
Next == VoteStep / CertifyStep
40 41 42 43
TypeInvariant == /\ votes \subseteq VoteDomain /\ certs \subseteq CertDomain
44 45 46 47 48 49
NoDualVotes == \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes => /\ b1 = b2
43
50
/\ e1 = e2
51 52 53 54 55 56
CertSoundness == \A s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators : <<s, b, e, Q>> \in certs => /\ Cardinality(Q) >= QuorumSize /\ \A v \in Q : <<v, s, b, e>> \in votes
57 58
Invariant == TypeInvariant /\ NoDualVotes /\ CertSoundness
59 60 61 62 63 64 65 66 67 68 69 70 71
Safety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, Q1 \in SUBSET Validators, Q2 \in SUBSET Validators : /\ <<s, b1, e1, Q1>> \in certs /\ <<s, b2, e2, Q2>> \in certs => /\ b1 = b2 /\ e1 = e2
72 73
Spec == Init /\ [][Next]_vars
74 75 76
THEOREM InitImpliesTypeInvariant == Init => TypeInvariant BY SMTT(30) DEF Init, TypeInvariant, VoteDomain, CertDomain
77 78 79
THEOREM InitImpliesNoDualVotes == Init => NoDualVotes BY DEF Init, NoDualVotes
80 81 82
THEOREM InitImpliesCertSoundness == Init => CertSoundness BY DEF Init, CertSoundness
83 84 85 86
THEOREM InitImpliesInvariant == Init => Invariant BY InitImpliesTypeInvariant, InitImpliesNoDualVotes, InitImpliesCertSoundness DEF Invariant
87 88 89
THEOREM VotePreservesTypeInvariant == TypeInvariant /\ VoteStep => TypeInvariant' BY SMTT(30) DEF TypeInvariant, VoteStep, HasVote, VoteDomain, CertDomain
90 91 92
THEOREM VotePreservesNoDualVotes == NoDualVotes /\ VoteStep => NoDualVotes' BY SMTT(30) DEF NoDualVotes, VoteStep, HasVote
93 94 95
THEOREM VotePreservesCertSoundness == CertSoundness /\ VoteStep => CertSoundness' BY DEF CertSoundness, VoteStep
96 97 98 99
THEOREM VotePreservesInvariant == Invariant /\ VoteStep => Invariant' BY VotePreservesTypeInvariant, VotePreservesNoDualVotes, VotePreservesCertSoundness DEF Invariant
100 101 102
THEOREM CertifyPreservesTypeInvariant == TypeInvariant /\ CertifyStep => TypeInvariant' BY SMTT(30) DEF TypeInvariant, CertifyStep, VoteDomain, CertDomain
103 104 105
THEOREM CertifyPreservesNoDualVotes == NoDualVotes /\ CertifyStep => NoDualVotes' BY DEF NoDualVotes, CertifyStep
106 107 108
THEOREM CertifyPreservesCertSoundness == CertSoundness /\ CertifyStep => CertSoundness' BY SMTT(30) DEF CertSoundness, CertifyStep
109 110 111
THEOREM CertifyPreservesInvariant == Invariant /\ CertifyStep => Invariant' BY CertifyPreservesTypeInvariant, CertifyPreservesNoDualVotes,
44
CertifyPreservesCertSoundness DEF Invariant
112 113 114 115
THEOREM StepPreservesInvariant == Invariant /\ Next => Invariant' BY VotePreservesInvariant, CertifyPreservesInvariant DEF Next
116 117 118 119
THEOREM StutterPreservesTypeInvariant == TypeInvariant /\ UNCHANGED vars => TypeInvariant' BY DEF TypeInvariant, vars
120 121 122 123
THEOREM StutterPreservesNoDualVotes == NoDualVotes /\ UNCHANGED vars => NoDualVotes' BY DEF NoDualVotes, vars
124 125 126 127
THEOREM StutterPreservesCertSoundness == CertSoundness /\ UNCHANGED vars => CertSoundness' BY DEF CertSoundness, vars
128 129 130 131
THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant' BY StutterPreservesTypeInvariant, StutterPreservesNoDualVotes, StutterPreservesCertSoundness DEF Invariant
132 133 134
THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant' BY StepPreservesInvariant, StutterPreservesInvariant DEF vars
135 136 137 138 139 140 141 142 143 144 145 146 147 148
THEOREM QuorumCertificatesIntersect == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, Q1 \in SUBSET Validators, Q2 \in SUBSET Validators : /\ Invariant /\ <<s, b1, e1, Q1>> \in certs /\ <<s, b2, e2, Q2>> \in certs => Q1 \cap Q2 # {} BY SMTT(60), QuorumIntersection DEF Invariant, CertSoundness
149 150 151 152
THEOREM InvariantImpliesSafety == Invariant => Safety BY SMTT(60), QuorumCertificatesIntersect DEF Invariant, Safety, NoDualVotes, CertSoundness
153 154
====
A.1.2
GuardianMajority.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/gu ardian_majority/GuardianMajority.tla}
1 2
---- MODULE GuardianMajority ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4
CONSTANT Validators, Blocks, Slots, Epochs, QuorumSize, InitialEpoch
5 6
ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs
7 8 9 10
ASSUME QuorumIntersection == \A S, T \in SUBSET Validators : /\ Cardinality(S) >= QuorumSize
45
11 12
/\ Cardinality(T) >= QuorumSize => S \cap T # {}
13 14
VARIABLES votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady, ,→ checkpointLevel
15 16
vars == <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady, ,→ checkpointLevel>>
17 18
CheckpointLevels == 0..2
19 20 21
VoteEvent(v, s, b, e) == <<v, s, b, e>> Finalization(s, b, e) == <<s, b, e>>
22 23 24
VoteDomain == {VoteEvent(v, s, b, e) : v \in Validators, s \in Slots, b \in Blocks, e \in Epochs} FinalizationDomain == {Finalization(s, b, e) : s \in Slots, b \in Blocks, e \in Epochs}
25 26 27 28 29 30 31 32 33
Init == /\ votes = {} /\ finalized = {} /\ finalizerSets = [f \in FinalizationDomain |-> {}] /\ registryEpoch = [v \in Validators |-> InitialEpoch] /\ manifestEpoch = [v \in Validators |-> InitialEpoch] /\ guardianReady = [v \in Validators |-> TRUE] /\ checkpointLevel = [v \in Validators |-> 1]
34 35 36
HasVote(v, s) == \E b \in Blocks, e \in Epochs : VoteEvent(v, s, b, e) \in votes
37 38 39 40 41 42 43 44 45 46 47
CanVote(v, s, b, e) == /\ v \in Validators /\ s \in Slots /\ b \in Blocks /\ e \in Epochs /\ guardianReady[v] /\ checkpointLevel[v] > 0 /\ registryEpoch[v] = e /\ manifestEpoch[v] = e /\ ~HasVote(v, s)
48 49 50 51 52
Vote(v, s, b, e) == /\ CanVote(v, s, b, e) /\ votes' = votes \cup {VoteEvent(v, s, b, e)} /\ UNCHANGED <<finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady, ,→ checkpointLevel>>
53 54 55 56 57 58 59 60
EligibleVoters(s, b, e) == {v \in Validators : /\ VoteEvent(v, s, b, e) \in votes /\ guardianReady[v] /\ checkpointLevel[v] > 0 /\ registryEpoch[v] = e /\ manifestEpoch[v] = e}
61 62 63 64 65 66
CanFinalize(s, b, e) == /\ s \in Slots /\ b \in Blocks /\ e \in Epochs /\ Cardinality(EligibleVoters(s, b, e)) >= QuorumSize
67 68 69
Finalize(s, b, e) == /\ CanFinalize(s, b, e)
46
70 71 72
/\ finalized' = finalized \cup {Finalization(s, b, e)} /\ finalizerSets' = [finalizerSets EXCEPT ![Finalization(s, b, e)] = EligibleVoters(s, b, e)] /\ UNCHANGED <<votes, registryEpoch, manifestEpoch, guardianReady, checkpointLevel>>
73 74 75 76 77 78 79 80
AdoptEpoch(v, e) == /\ v \in Validators /\ e \in Epochs /\ e >= registryEpoch[v] /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e] /\ manifestEpoch' = [manifestEpoch EXCEPT ![v] = e] /\ UNCHANGED <<votes, finalized, finalizerSets, guardianReady, checkpointLevel>>
81 82 83 84 85 86 87
RegistryRollback(v, e) == /\ v \in Validators /\ e \in Epochs /\ e < registryEpoch[v] /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e] /\ UNCHANGED <<votes, finalized, finalizerSets, manifestEpoch, guardianReady, checkpointLevel>>
88 89 90 91 92 93 94
ManifestRollback(v, e) == /\ v \in Validators /\ e \in Epochs /\ e < manifestEpoch[v] /\ manifestEpoch' = [manifestEpoch EXCEPT ![v] = e] /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, guardianReady, checkpointLevel>>
95 96 97 98 99 100
GuardianOutage(v) == /\ v \in Validators /\ guardianReady[v] /\ guardianReady' = [guardianReady EXCEPT ![v] = FALSE] /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, checkpointLevel>>
101 102 103 104 105 106
GuardianRecovery(v) == /\ v \in Validators /\ ~guardianReady[v] /\ guardianReady' = [guardianReady EXCEPT ![v] = TRUE] /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, checkpointLevel>>
107 108 109 110 111 112 113
AdvanceCheckpoint(v, level) == /\ v \in Validators /\ level \in CheckpointLevels /\ level > checkpointLevel[v] /\ checkpointLevel' = [checkpointLevel EXCEPT ![v] = level] /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady>>
114 115 116 117 118 119 120
CheckpointRollback(v, level) == /\ v \in Validators /\ level \in CheckpointLevels /\ level < checkpointLevel[v] /\ checkpointLevel' = [checkpointLevel EXCEPT ![v] = level] /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady>>
121 122 123 124 125 126 127 128 129 130 131
Next == / \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : Vote(v, s, b, e) / \E s \in Slots, b \in Blocks, e \in Epochs : Finalize(s, b, e) / \E v \in Validators, e \in Epochs : AdoptEpoch(v, e) / \E v \in Validators, e \in Epochs : RegistryRollback(v, e) / \E v \in Validators, e \in Epochs : ManifestRollback(v, e) / \E v \in Validators : GuardianOutage(v) / \E v \in Validators : GuardianRecovery(v) / \E v \in Validators, level \in CheckpointLevels : AdvanceCheckpoint(v, level) / \E v \in Validators, level \in CheckpointLevels : CheckpointRollback(v, level)
47
132 133 134 135 136 137 138 139 140
TypeInvariant == /\ votes \subseteq VoteDomain /\ finalized \subseteq FinalizationDomain /\ finalizerSets \in [FinalizationDomain -> SUBSET Validators] /\ registryEpoch \in [Validators -> Epochs] /\ manifestEpoch \in [Validators -> Epochs] /\ guardianReady \in [Validators -> BOOLEAN] /\ checkpointLevel \in [Validators -> CheckpointLevels]
141 142 143 144 145 146 147
NoDualVotes == \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ VoteEvent(v, s, b1, e1) \in votes /\ VoteEvent(v, s, b2, e2) \in votes => /\ b1 = b2 /\ e1 = e2
148 149 150 151 152 153 154
FinalizationWitnessSoundness == \A s \in Slots, b \in Blocks, e \in Epochs : Finalization(s, b, e) \in finalized => /\ Cardinality(finalizerSets[Finalization(s, b, e)]) >= QuorumSize /\ \A v \in finalizerSets[Finalization(s, b, e)] : VoteEvent(v, s, b, e) \in votes
155 156
Invariant == TypeInvariant /\ NoDualVotes /\ FinalizationWitnessSoundness
157 158 159 160 161 162
Safety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ Finalization(s, b1, e1) \in finalized /\ Finalization(s, b2, e2) \in finalized => b1 = b2
163 164 165
Spec == Init /\ [][Next]_vars
166 167 168
THEOREM OneInCheckpointLevels == 1 \in CheckpointLevels BY SMT DEF CheckpointLevels
169 170 171 172 173 174 175 176 177 178 179 180
THEOREM InitImpliesInvariant == Init => Invariant PROOF <1>1. Init => TypeInvariant BY SMT, InitialEpochInEpochs, OneInCheckpointLevels DEF Init, TypeInvariant, VoteDomain, FinalizationDomain <1>2. Init => NoDualVotes BY DEF Init, NoDualVotes <1>3. Init => FinalizationWitnessSoundness BY DEF Init, FinalizationWitnessSoundness <1>4. QED BY <1>1, <1>2, <1>3 DEF Invariant
181 182 183 184 185 186
THEOREM StepPreservesTypeInvariant == Invariant /\ Next => TypeInvariant' BY SMTT(30) DEF Invariant, TypeInvariant, Next, Vote, Finalize, AdoptEpoch, RegistryRollback, ManifestRollback, GuardianOutage, GuardianRecovery, AdvanceCheckpoint, CheckpointRollback, CanVote, HasVote, CanFinalize, EligibleVoters, VoteEvent, Finalization, VoteDomain, FinalizationDomain
187 188 189 190 191
THEOREM StepPreservesNoDualVotes == Invariant /\ Next => NoDualVotes' BY SMT DEF Invariant, NoDualVotes, Next, Vote, Finalize, AdoptEpoch, RegistryRollback, ManifestRollback, GuardianOutage, GuardianRecovery, AdvanceCheckpoint, CheckpointRollback, CanVote, HasVote, VoteEvent
192 193
THEOREM StepPreservesFinalizationWitnessSoundness ==
48
194 195 196 197 198
Invariant /\ Next => FinalizationWitnessSoundness' BY SMTT(30) DEF Invariant, FinalizationWitnessSoundness, Next, Vote, Finalize, AdoptEpoch, RegistryRollback, ManifestRollback, GuardianOutage, GuardianRecovery, AdvanceCheckpoint, CheckpointRollback, CanFinalize, EligibleVoters, VoteEvent, Finalization
199 200 201
THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant' BY SMT DEF Invariant, vars
202 203 204 205 206 207 208 209 210 211
THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant' PROOF <1>1. Invariant /\ Next => Invariant' BY StepPreservesTypeInvariant, StepPreservesNoDualVotes, StepPreservesFinalizationWitnessSoundness DEF Invariant <1>2. Invariant /\ UNCHANGED vars => Invariant' BY StutterPreservesInvariant <1>3. QED BY <1>1, <1>2 DEF vars
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
THEOREM FinalizedWitnessesIntersect == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ Invariant /\ <<s, b1, e1>> \in finalized /\ <<s, b2, e2>> \in finalized => \E v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes PROOF <1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs <1>2. ASSUME Invariant, <<s, b1, e1>> \in finalized, <<s, b2, e2>> \in finalized PROVE \E v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes <2>1. finalizerSets[<<s, b1, e1>>] \subseteq Validators BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization <2>2. finalizerSets[<<s, b2, e2>>] \subseteq Validators BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization <2>3. Cardinality(finalizerSets[<<s, b1, e1>>]) >= QuorumSize BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness <2>4. Cardinality(finalizerSets[<<s, b2, e2>>]) >= QuorumSize BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness <2>5. finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] # {} BY <2>1, <2>2, <2>3, <2>4, QuorumIntersection <2>6. PICK v \in finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] : TRUE BY <2>5 <2>7. <<v, s, b1, e1>> \in votes BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness <2>8. <<v, s, b2, e2>> \in votes BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness <2>9. QED BY SMT, <2>6, <2>7, <2>8 <1>3. QED BY <1>2
249 250 251 252 253 254 255
THEOREM InvariantImpliesSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ Invariant /\ <<s, b1, e1>> \in finalized /\ <<s, b2, e2>> \in finalized => /\ b1 = b2
49
256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
/\ e1 = e2 PROOF <1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs <1>2. ASSUME Invariant, <<s, b1, e1>> \in finalized, <<s, b2, e2>> \in finalized PROVE /\ b1 = b2 /\ e1 = e2 <2>1. \E v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes BY SMT, FinalizedWitnessesIntersect, <1>2 <2>2. PICK v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes BY <2>1 <2>3. QED BY SMT, <1>2, <2>2 DEF Invariant, NoDualVotes <1>3. QED BY <1>2
276 277
====
50
A.2
CanonicalOrdering
Proof-carrying ordering model and its main proof surface.
A.2.1
CanonicalOrderingProof.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ca nonical_ordering/CanonicalOrderingProof.tla}
1 2
---- MODULE CanonicalOrderingProof ---EXTENDS Naturals, FiniteSets, TLAPS
3 4
CONSTANT Slots, Transactions
5 6
VARIABLES bulletins, closedCutoffs, admittedCerts, omissionProofs, recoveredSets
7 8
vars == <<bulletins, closedCutoffs, admittedCerts, omissionProofs, recoveredSets>>
9 10 11
CertEvent(s, c) == <<s, c>> OmissionEvent(s, c, tx) == <<s, c, tx>>
12 13 14
CanonicalSet(s) == bulletins[s] RecoverableSet(s) == IF s \in closedCutoffs THEN CanonicalSet(s) ELSE {}
15 16 17 18 19 20
BulletinDomain == [Slots -> SUBSET Transactions] CutoffDomain == SUBSET Slots CertDomain == Slots \X (SUBSET Transactions) OmissionDomain == Slots \X (SUBSET Transactions) \X Transactions RecoveredDomain == [Slots -> SUBSET Transactions]
21 22 23 24 25 26 27
TypeInvariant == /\ bulletins \in BulletinDomain /\ closedCutoffs \in CutoffDomain /\ admittedCerts \subseteq CertDomain /\ omissionProofs \subseteq OmissionDomain /\ recoveredSets \in RecoveredDomain
28 29 30 31 32 33
CertifiedSoundness == \A s \in Slots, c \in SUBSET Transactions : CertEvent(s, c) \in admittedCerts => /\ s \in closedCutoffs /\ c = CanonicalSet(s)
34 35 36 37 38 39 40
OmissionSoundness == \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions : OmissionEvent(s, c, tx) \in omissionProofs => /\ s \in closedCutoffs /\ tx \in CanonicalSet(s) /\ tx \notin c
41 42 43 44
RecoveredSoundness == \A s \in Slots : recoveredSets[s] = RecoverableSet(s)
45 46 47 48 49
Invariant == /\ TypeInvariant /\ CertifiedSoundness /\ OmissionSoundness
51
50
/\ RecoveredSoundness
51 52 53 54 55 56
CertifiedUniqueness == \A s \in Slots, c1 \in SUBSET Transactions, c2 \in SUBSET Transactions : /\ CertEvent(s, c1) \in admittedCerts /\ CertEvent(s, c2) \in admittedCerts => c1 = c2
57 58 59 60 61
Recoverability == \A s \in Slots, c \in SUBSET Transactions : CertEvent(s, c) \in admittedCerts => recoveredSets[s] = c
62 63 64 65 66
OmissionDominates == \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions : OmissionEvent(s, c, tx) \in omissionProofs => CertEvent(s, c) \notin admittedCerts
67 68 69 70 71
THEOREM InvariantImpliesCertifiedUniqueness == Invariant => CertifiedUniqueness BY SMTT(60) DEF Invariant, CertifiedUniqueness, CertifiedSoundness
72 73 74 75 76
THEOREM InvariantImpliesRecoverability == Invariant => Recoverability BY SMTT(60) DEF Invariant, Recoverability, CertifiedSoundness, RecoveredSoundness, RecoverableSet
77 78 79 80 81
THEOREM InvariantImpliesOmissionDominates == Invariant => OmissionDominates BY SMTT(60) DEF Invariant, OmissionDominates, CertifiedSoundness, OmissionSoundness
82 83
====
A.2.2
CanonicalOrdering.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ca nonical_ordering/CanonicalOrdering.tla}
1 2
---- MODULE CanonicalOrdering ---EXTENDS Naturals, FiniteSets, TLC
3 4
CONSTANT Slots, Transactions
5 6
VARIABLES bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs
7 8 9
vars == <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>
10 11 12 13 14 15 16 17
CertEvent(s, c) == <<s, c>> NoParent == [kind |-> "none", cert |-> {}] ParentCert(c) == [kind |-> "cert", cert |-> c] FrontierEvent(s, c, p) == [slot |-> s, cert |-> c, parentCert |-> p] FrontierConflict(f1, f2) == [kind |-> "conflict", candidate |-> f1, reference |-> f2] StaleFrontier(f, prev) == [kind |-> "stale", candidate |-> f, reference |-> prev] OmissionEvent(s, c, tx) == <<s, c, tx>>
52
18 19 20 21
WitnessSlot(w) == w.candidate.slot HasFrontierContradiction(s) == \E w \in frontierContradictions : WitnessSlot(w) = s FirstSlot == CHOOSE min \in Slots : \A s \in Slots : min <= s PredecessorClosed(s) == s = FirstSlot / s - 1 \in bulletinCloses
22 23
CanonicalSet(s) == bulletin[s]
24 25 26 27 28 29 30 31 32
33 34 35 36 37 38 39 40 41
BulletinDomain == [Slots -> SUBSET Transactions] CutoffDomain == SUBSET Slots AvailabilityDomain == SUBSET Slots BulletinCloseDomain == SUBSET Slots CertDomain == Slots \X (SUBSET Transactions) ParentRefDomain == [kind : {"none", "cert"}, cert : SUBSET Transactions] FrontierDomain == [slot : Slots, cert : SUBSET Transactions, parentCert : ParentRefDomain] ContradictionDomain == [kind : {"conflict", "stale"}, candidate : FrontierDomain, reference : ,→ FrontierDomain] OmissionDomain == Slots \X (SUBSET Transactions) \X Transactions ParentChoices(s) == IF s = FirstSlot THEN {NoParent} ELSE {p \in ParentRefDomain : p = NoParent / (\E f \in publicationFrontiers : /\ f.slot + 1 = s /\ p = ParentCert(f.cert))}
42 43 44 45 46 47 48 49 50 51 52
Init == /\ bulletin = [s \in Slots |-> {}] /\ closedCutoffs = {} /\ availabilityCerts = {} /\ bulletinCloses = {} /\ candidateCerts = {} /\ publicationFrontiers = {} /\ frontierContradictions = {} /\ admittedCerts = {} /\ omissionProofs = {}
53 54 55 56 57 58 59 60
PublishStep == \E s \in Slots, tx \in Transactions : /\ PredecessorClosed(s) /\ s \notin closedCutoffs /\ tx \notin bulletin[s] /\ bulletin' = [bulletin EXCEPT ![s] = @ \cup {tx}] /\ UNCHANGED <<closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>
61 62 63 64 65 66 67
CloseCutoffStep == \E s \in Slots : /\ PredecessorClosed(s) /\ s \notin closedCutoffs /\ closedCutoffs' = closedCutoffs \cup {s} /\ UNCHANGED <<bulletin, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>
68 69 70 71 72 73 74 75
AvailabilityCertifyStep == \E s \in Slots : /\ PredecessorClosed(s) /\ s \in closedCutoffs /\ s \notin availabilityCerts /\ availabilityCerts' = availabilityCerts \cup {s} /\ UNCHANGED <<bulletin, closedCutoffs, bulletinCloses, candidateCerts, publicationFrontiers, ,→ frontierContradictions, admittedCerts, omissionProofs>>
53
76 77 78 79 80 81 82 83
CanonicalBulletinCloseStep == \E s \in Slots : /\ PredecessorClosed(s) /\ s \in availabilityCerts /\ s \notin bulletinCloses /\ bulletinCloses' = bulletinCloses \cup {s} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, candidateCerts, ,→ publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>
84 85 86 87 88 89 90 91 92
CandidateCertifyStep == \E s \in Slots : \E c \in SUBSET bulletin[s] : /\ PredecessorClosed(s) /\ s \in bulletinCloses /\ CertEvent(s, c) \notin candidateCerts /\ candidateCerts' = candidateCerts \cup {CertEvent(s, c)} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, ,→ publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>
93 94 95 96 97 98 99 100 101 102 103 104 105
PublishFrontierStep == \E e \in candidateCerts : LET s == e[1] c == e[2] IN \E p \in ParentChoices(s) : /\ s \in bulletinCloses /\ (s = FirstSlot / \E prev \in publicationFrontiers : prev.slot + 1 = s) /\ FrontierEvent(s, c, p) \notin publicationFrontiers /\ publicationFrontiers' = publicationFrontiers \cup {FrontierEvent(s, c, p)} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ frontierContradictions, admittedCerts, omissionProofs>>
106 107 108 109 110 111 112 113 114
ProveFrontierConflictStep == \E f1 \in publicationFrontiers, f2 \in publicationFrontiers : /\ f1.slot = f2.slot /\ f1 # f2 /\ FrontierConflict(f1, f2) \notin frontierContradictions /\ frontierContradictions' = frontierContradictions \cup {FrontierConflict(f1, f2)} /\ admittedCerts' = {e \in admittedCerts : e[1] # f1.slot} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, omissionProofs>>
115 116 117 118 119 120 121 122 123
ProveStaleFrontierStep == \E f \in publicationFrontiers, prev \in publicationFrontiers : /\ prev.slot + 1 = f.slot /\ f.parentCert # ParentCert(prev.cert) /\ StaleFrontier(f, prev) \notin frontierContradictions /\ frontierContradictions' = frontierContradictions \cup {StaleFrontier(f, prev)} /\ admittedCerts' = {e \in admittedCerts : e[1] # f.slot} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, omissionProofs>>
124 125 126 127 128 129 130 131 132
ProveOmissionStep == \E s \in Slots, c \in SUBSET Transactions, tx \in Transactions : /\ CertEvent(s, c) \in candidateCerts /\ tx \in CanonicalSet(s) /\ tx \notin c /\ OmissionEvent(s, c, tx) \notin omissionProofs /\ omissionProofs' = omissionProofs \cup {OmissionEvent(s, c, tx)} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, frontierContradictions, admittedCerts>>
54
133 134 135 136 137 138 139 140 141 142 143 144 145
AdmitCertStep == \E s \in Slots : \E c \in SUBSET Transactions : /\ CertEvent(s, c) \in candidateCerts /\ s \in bulletinCloses /\ \E f \in publicationFrontiers : /\ f.slot = s /\ f.cert = c /\ ~HasFrontierContradiction(s) /\ c = CanonicalSet(s) /\ ~(\E tx \in Transactions : OmissionEvent(s, c, tx) \in omissionProofs) /\ CertEvent(s, c) \notin admittedCerts /\ admittedCerts' = admittedCerts \cup {CertEvent(s, c)} /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, ,→ publicationFrontiers, frontierContradictions, omissionProofs>>
146 147 148 149 150 151 152 153 154 155 156 157
Next == / PublishStep / CloseCutoffStep / AvailabilityCertifyStep / CanonicalBulletinCloseStep / CandidateCertifyStep / PublishFrontierStep / ProveFrontierConflictStep / ProveStaleFrontierStep / ProveOmissionStep / AdmitCertStep
158 159 160 161 162 163 164 165 166 167 168
TypeInvariant == /\ bulletin \in BulletinDomain /\ closedCutoffs \in CutoffDomain /\ availabilityCerts \in AvailabilityDomain /\ bulletinCloses \in BulletinCloseDomain /\ candidateCerts \subseteq CertDomain /\ publicationFrontiers \subseteq FrontierDomain /\ frontierContradictions \subseteq ContradictionDomain /\ admittedCerts \subseteq CertDomain /\ omissionProofs \subseteq OmissionDomain
169 170 171 172
AvailabilityCertSoundness == \A s \in Slots : s \in availabilityCerts => s \in closedCutoffs
173 174 175 176
CanonicalBulletinCloseSoundness == \A s \in Slots : s \in bulletinCloses => s \in availabilityCerts
177 178 179 180 181
FrontierSoundness == \A f \in publicationFrontiers : /\ f.slot \in bulletinCloses /\ CertEvent(f.slot, f.cert) \in candidateCerts
182 183 184 185 186 187
FrontierConflictSoundness == \A w \in frontierContradictions : w.kind = "conflict" => /\ w.candidate.slot = w.reference.slot /\ w.candidate # w.reference
188 189 190 191 192 193
StaleFrontierSoundness == \A w \in frontierContradictions : w.kind = "stale" => /\ w.reference.slot + 1 = w.candidate.slot /\ w.candidate.parentCert # ParentCert(w.reference.cert)
55
194 195 196 197 198 199 200 201
AdmittedSoundness == \A s \in Slots, c \in SUBSET Transactions : CertEvent(s, c) \in admittedCerts => /\ s \in bulletinCloses /\ c = CanonicalSet(s) /\ \E f \in publicationFrontiers : /\ f.slot = s /\ f.cert = c /\ ~HasFrontierContradiction(s)
202 203 204 205 206 207 208
OmissionSoundness == \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions : OmissionEvent(s, c, tx) \in omissionProofs => /\ s \in closedCutoffs /\ tx \in CanonicalSet(s) /\ tx \notin c
209 210 211 212 213 214
AdmittedUniqueness == \A s \in Slots, c1 \in SUBSET Transactions, c2 \in SUBSET Transactions : /\ CertEvent(s, c1) \in admittedCerts /\ CertEvent(s, c2) \in admittedCerts => c1 = c2
215 216 217 218 219
OmissionDominates == \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions : OmissionEvent(s, c, tx) \in omissionProofs => CertEvent(s, c) \notin admittedCerts
220 221 222 223 224
FrontierContradictionDominates == \A s \in Slots, c \in SUBSET Transactions : HasFrontierContradiction(s) => CertEvent(s, c) \notin admittedCerts
225 226 227 228 229 230 231 232 233 234 235 236
* Full endogenous retrievability now lives in CanonicalOrderingRetrievability.tla. * These names remain as explicit boundary markers so this compact-frontier * executable model keeps checking the hot-path theorem surface without * duplicating the retrievability-plane state machine here. RecoveredSoundness == \A s \in Slots : bulletin[s] = bulletin[s] Recoverability == \A s \in Slots : bulletin[s] = bulletin[s] WitnessBound == /\ Cardinality(candidateCerts) <= 4 /\ Cardinality(publicationFrontiers) <= 3 /\ Cardinality(frontierContradictions) <= 2 /\ Cardinality(omissionProofs) <= 1
237 238 239 240 241 242 243 244 245 246 247 248 249
Invariant == /\ TypeInvariant /\ AvailabilityCertSoundness /\ CanonicalBulletinCloseSoundness /\ FrontierSoundness /\ FrontierConflictSoundness /\ StaleFrontierSoundness /\ AdmittedSoundness /\ OmissionSoundness /\ AdmittedUniqueness /\ OmissionDominates /\ FrontierContradictionDominates
250 251
Spec == Init /\ [][Next]_vars
252 253
====
56
A.3
Asymptote
Sealed-finality model and proof artifact pair.
A.3.1
AsymptoteProof.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/As ymptoteProof.tla}
1 2
---- MODULE AsymptoteProof ---EXTENDS Naturals, FiniteSets, TLAPS
3 4
CONSTANT Blocks, Slots, Epochs, TranscriptRoots, ChallengeRoots, EmptyChallengeRoot
5 6
ASSUME EmptyChallengeRoot \in ChallengeRoots
7 8 9
VARIABLES baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedCerts
10 11 12 13
vars == <<baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedCerts>>
14 15 16 17 18 19 20 21
BaseCertDomain == Slots \X Blocks \X Epochs TranscriptSurfaceDomain == Slots \X Blocks \X Epochs \X TranscriptRoots ChallengeSurfaceDomain == Slots \X Blocks \X Epochs \X ChallengeRoots CanonicalCloseDomain == Slots \X Blocks \X Epochs \X TranscriptRoots CanonicalAbortDomain == Slots \X Blocks \X Epochs \X TranscriptRoots \X (ChallengeRoots \ {EmptyChallengeRoot}) SealedCertDomain == Slots \X Blocks \X Epochs
22 23 24 25 26 27 28
BaseCertEvent(s, b, e) == <<s, b, e>> TranscriptSurfaceEvent(s, b, e, t) == <<s, b, e, t>> ChallengeSurfaceEvent(s, b, e, c) == <<s, b, e, c>> CanonicalCloseEvent(s, b, e, t) == <<s, b, e, t>> CanonicalAbortEvent(s, b, e, t, c) == <<s, b, e, t, c>> SealEvent(s, b, e) == <<s, b, e>>
29 30 31 32 33 34 35 36
Init == /\ baseCerts = {} /\ transcriptSurfaces = {} /\ challengeSurfaces = {} /\ canonicalCloses = {} /\ canonicalAborts = {} /\ sealedCerts = {}
37 38 39
HasBaseCert(s) == \E b \in Blocks, e \in Epochs : BaseCertEvent(s, b, e) \in baseCerts
40 41 42 43
HasTranscriptSurface(s) == \E b \in Blocks, e \in Epochs, t \in TranscriptRoots : TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
44 45 46 47
HasChallengeSurface(s) == \E b \in Blocks, e \in Epochs, c \in ChallengeRoots : ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
48 49
HasCanonicalOutcome(s) ==
57
50 51 52 53 54
/ \E b \in Blocks, e \in Epochs, t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses / \E b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts
55 56 57 58 59
HasCanonicalAbort(s) == \E b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts
60 61 62 63 64 65 66
BaseCertifyStep == \E s \in Slots, b \in Blocks, e \in Epochs : /\ ~HasBaseCert(s) /\ baseCerts' = baseCerts \cup {BaseCertEvent(s, b, e)} /\ UNCHANGED <<transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedCerts>>
67 68 69 70 71 72 73 74 75
TranscriptSurfaceStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : /\ BaseCertEvent(s, b, e) \in baseCerts /\ ~HasTranscriptSurface(s) /\ transcriptSurfaces' = transcriptSurfaces \cup {TranscriptSurfaceEvent(s, b, e, t)} /\ UNCHANGED <<baseCerts, challengeSurfaces, canonicalCloses, canonicalAborts, sealedCerts>>
76 77 78 79 80 81 82 83 84 85
ChallengeSurfaceStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots : /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ~HasChallengeSurface(s) /\ challengeSurfaces' = challengeSurfaces \cup {ChallengeSurfaceEvent(s, b, e, c)} /\ UNCHANGED <<baseCerts, transcriptSurfaces, canonicalCloses, canonicalAborts, sealedCerts>>
86 87 88 89 90 91 92 93 94
CanonicalCloseStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces /\ ~HasCanonicalOutcome(s) /\ canonicalCloses' = canonicalCloses \cup {CanonicalCloseEvent(s, b, e, t)} /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces, canonicalAborts, sealedCerts>>
95 96 97 98 99 100 101 102 103 104 105
CanonicalAbortStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces /\ ~HasCanonicalOutcome(s) /\ canonicalAborts' = canonicalAborts \cup {CanonicalAbortEvent(s, b, e, t, c)} /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, sealedCerts>>
106 107 108 109 110 111
SealStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : /\ CanonicalCloseEvent(s, b, e, t) \in canonicalCloses /\ ~HasCanonicalAbort(s) /\ sealedCerts' = sealedCerts \cup {SealEvent(s, b, e)}
58
112 113
/\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts>>
114 115 116 117 118 119 120 121
Next == / BaseCertifyStep / TranscriptSurfaceStep / ChallengeSurfaceStep / CanonicalCloseStep / CanonicalAbortStep / SealStep
122 123 124 125 126 127 128 129
TypeInvariant == /\ baseCerts \subseteq BaseCertDomain /\ transcriptSurfaces \subseteq TranscriptSurfaceDomain /\ challengeSurfaces \subseteq ChallengeSurfaceDomain /\ canonicalCloses \subseteq CanonicalCloseDomain /\ canonicalAborts \subseteq CanonicalAbortDomain /\ sealedCerts \subseteq SealedCertDomain
130 131 132 133 134 135 136
NoDualBaseCerts == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ BaseCertEvent(s, b1, e1) \in baseCerts /\ BaseCertEvent(s, b2, e2) \in baseCerts => /\ b1 = b2 /\ e1 = e2
137 138 139 140 141 142 143 144 145
NoDualTranscriptSurfaces == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, t1 \in TranscriptRoots, t2 \in TranscriptRoots : /\ TranscriptSurfaceEvent(s, b1, e1, t1) \in transcriptSurfaces /\ TranscriptSurfaceEvent(s, b2, e2, t2) \in transcriptSurfaces => /\ b1 = b2 /\ e1 = e2 /\ t1 = t2
146 147 148 149 150 151 152 153 154
NoDualChallengeSurfaces == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, c1 \in ChallengeRoots, c2 \in ChallengeRoots : /\ ChallengeSurfaceEvent(s, b1, e1, c1) \in challengeSurfaces /\ ChallengeSurfaceEvent(s, b2, e2, c2) \in challengeSurfaces => /\ b1 = b2 /\ e1 = e2 /\ c1 = c2
155 156 157 158 159 160 161 162 163
NoDualCanonicalCloses == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, t1 \in TranscriptRoots, t2 \in TranscriptRoots : /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses /\ CanonicalCloseEvent(s, b2, e2, t2) \in canonicalCloses => /\ b1 = b2 /\ e1 = e2 /\ t1 = t2
164 165 166 167 168 169 170 171 172 173
NoDualCanonicalAborts == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, t1 \in TranscriptRoots, t2 \in TranscriptRoots, c1 \in ChallengeRoots \ {EmptyChallengeRoot}, c2 \in ChallengeRoots \ {EmptyChallengeRoot} : /\ CanonicalAbortEvent(s, b1, e1, t1, c1) \in canonicalAborts /\ CanonicalAbortEvent(s, b2, e2, t2, c2) \in canonicalAborts => /\ b1 = b2 /\ e1 = e2
59
174 175
/\ t1 = t2 /\ c1 = c2
176 177 178 179 180
TranscriptAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces => BaseCertEvent(s, b, e) \in baseCerts
181 182 183 184 185 186
ChallengeAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, c \in ChallengeRoots : ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces => \E t \in TranscriptRoots : TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
187 188 189 190 191 192
CanonicalCloseAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces
193 194 195 196 197 198 199
CanonicalAbortAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
200 201 202 203 204 205
SealedAnchored == \A s \in Slots, b \in Blocks, e \in Epochs : SealEvent(s, b, e) \in sealedCerts => /\ \E t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses /\ ~HasCanonicalAbort(s)
206 207 208 209 210 211 212 213
CloseAbortExclusive == \A s \in Slots, b1 \in Blocks, e1 \in Epochs, t1 \in TranscriptRoots, b2 \in Blocks, e2 \in Epochs, t2 \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses /\ CanonicalAbortEvent(s, b2, e2, t2, c) \in canonicalAborts => FALSE
214 215 216 217 218 219 220 221 222 223 224 225 226 227
Invariant == /\ TypeInvariant /\ NoDualBaseCerts /\ NoDualTranscriptSurfaces /\ NoDualChallengeSurfaces /\ NoDualCanonicalCloses /\ NoDualCanonicalAborts /\ TranscriptAnchored /\ ChallengeAnchored /\ CanonicalCloseAnchored /\ CanonicalAbortAnchored /\ CloseAbortExclusive /\ SealedAnchored
228 229 230 231 232 233 234
BaseSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ BaseCertEvent(s, b1, e1) \in baseCerts /\ BaseCertEvent(s, b2, e2) \in baseCerts => /\ b1 = b2 /\ e1 = e2
235
60
236 237 238 239 240 241 242 243
CanonicalCloseSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, t1 \in TranscriptRoots, t2 \in TranscriptRoots : /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses /\ CanonicalCloseEvent(s, b2, e2, t2) \in canonicalCloses => /\ b1 = b2 /\ e1 = e2 /\ t1 = t2
244 245 246 247 248 249 250
SealedSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ SealEvent(s, b1, e1) \in sealedCerts /\ SealEvent(s, b2, e2) \in sealedCerts => /\ b1 = b2 /\ e1 = e2
251 252 253 254
AbortDominatesSealed == \A s \in Slots, b \in Blocks, e \in Epochs : HasCanonicalAbort(s) => SealEvent(s, b, e) \notin sealedCerts
255 256
Spec == Init /\ [][Next]_vars
257 258 259 260
THEOREM InvariantImpliesBaseSafety == Invariant => BaseSafety BY SMTT(50) DEF Invariant, BaseSafety, NoDualBaseCerts
261 262 263 264
THEOREM InvariantImpliesCanonicalCloseSafety == Invariant => CanonicalCloseSafety BY SMTT(60) DEF Invariant, CanonicalCloseSafety, NoDualCanonicalCloses
265 266 267 268
THEOREM InvariantImpliesCloseAbortExclusive == Invariant => CloseAbortExclusive BY SMTT(20) DEF Invariant, CloseAbortExclusive
269 270 271 272
THEOREM InvariantImpliesSealedSafety == Invariant => SealedSafety BY SMTT(60), InvariantImpliesCanonicalCloseSafety DEF Invariant, SealedSafety, SealedAnchored, CanonicalCloseSafety
273 274 275 276
THEOREM InvariantImpliesAbortDominatesSealed == Invariant => AbortDominatesSealed BY SMTT(60) DEF Invariant, AbortDominatesSealed, SealedAnchored
277 278
====
A.3.2
Asymptote.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/As ymptote.tla}
1 2
---- MODULE Asymptote ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4 5
CONSTANT Validators, Blocks, Slots, Epochs, ValidatorQuorum, TranscriptRoots, ChallengeRoots, EmptyChallengeRoot
6 7 8 9 10
ASSUME EmptyChallengeRoot \in ChallengeRoots ASSUME ValidatorQuorumIntersection == \A S, T \in SUBSET Validators : /\ Cardinality(S) >= ValidatorQuorum
61
11 12
/\ Cardinality(T) >= ValidatorQuorum => S \cap T # {}
13 14 15 16 17 18
CollapsePending == 0 CollapseBase == 1 CollapseObservation == 2 CollapseAbort == 3 CollapseSealed == 4
19 20 21
CollapseStates == {CollapsePending, CollapseBase, CollapseObservation, CollapseAbort, CollapseSealed}
22 23 24
VARIABLES validatorVotes, baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedFinal, collapseState
25 26 27 28
vars == <<validatorVotes, baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedFinal, collapseState>>
29 30 31 32 33 34 35 36
ValidatorVoteEvent(v, s, b, e) == <<v, s, b, e>> BaseCertEvent(s, b, e, q) == <<s, b, e, q>> TranscriptSurfaceEvent(s, b, e, t) == <<s, b, e, t>> ChallengeSurfaceEvent(s, b, e, c) == <<s, b, e, c>> CanonicalCloseEvent(s, b, e, t) == <<s, b, e, t>> CanonicalAbortEvent(s, b, e, t, c) == <<s, b, e, t, c>> SealEvent(s, b, e) == <<s, b, e>>
37 38 39 40 41 42 43 44 45
ValidatorVoteDomain == Validators \X Slots \X Blocks \X Epochs BaseCertDomain == Slots \X Blocks \X Epochs \X (SUBSET Validators) TranscriptSurfaceDomain == Slots \X Blocks \X Epochs \X TranscriptRoots ChallengeSurfaceDomain == Slots \X Blocks \X Epochs \X ChallengeRoots CanonicalCloseDomain == Slots \X Blocks \X Epochs \X TranscriptRoots CanonicalAbortDomain == Slots \X Blocks \X Epochs \X TranscriptRoots \X (ChallengeRoots \ {EmptyChallengeRoot}) SealedCertDomain == Slots \X Blocks \X Epochs
46 47 48 49 50 51 52 53 54 55
Init == /\ validatorVotes = {} /\ baseCerts = {} /\ transcriptSurfaces = {} /\ challengeSurfaces = {} /\ canonicalCloses = {} /\ canonicalAborts = {} /\ sealedFinal = {} /\ collapseState = [s \in Slots |-> CollapsePending]
56 57 58
HasValidatorVote(v, s) == \E b \in Blocks, e \in Epochs : ValidatorVoteEvent(v, s, b, e) \in validatorVotes
59 60 61 62
HasBaseCert(s) == \E b \in Blocks, e \in Epochs, q \in SUBSET Validators : BaseCertEvent(s, b, e, q) \in baseCerts
63 64 65 66
HasTranscriptSurface(s) == \E b \in Blocks, e \in Epochs, t \in TranscriptRoots : TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
67 68 69 70
HasChallengeSurface(s) == \E b \in Blocks, e \in Epochs, c \in ChallengeRoots : ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
71 72
HasCanonicalOutcome(s) ==
62
73 74 75 76 77
/ \E b \in Blocks, e \in Epochs, t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses / \E b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts
78 79 80 81 82
HasCanonicalAbort(s) == \E b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts
83 84 85 86 87 88 89
ValidatorVoteStep == \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : /\ ~HasValidatorVote(v, s) /\ validatorVotes' = validatorVotes \cup {ValidatorVoteEvent(v, s, b, e)} /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedFinal, collapseState>>
90 91 92
EligibleValidators(s, b, e) == {v \in Validators : ValidatorVoteEvent(v, s, b, e) \in validatorVotes}
93 94 95 96 97 98 99 100 101
BaseFinalizeStep == \E s \in Slots, b \in Blocks, e \in Epochs, q \in SUBSET Validators : /\ q = EligibleValidators(s, b, e) /\ Cardinality(q) >= ValidatorQuorum /\ baseCerts' = baseCerts \cup {BaseCertEvent(s, b, e, q)} /\ collapseState' = [collapseState EXCEPT ![s] = CollapseBase] /\ UNCHANGED <<validatorVotes, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts, sealedFinal>>
102 103 104 105 106 107 108 109 110 111 112 113
TranscriptSurfaceStep == \E s \in Slots, b \in Blocks, e \in Epochs, q \in SUBSET Validators, t \in TranscriptRoots : /\ BaseCertEvent(s, b, e, q) \in baseCerts /\ collapseState[s] \in {CollapseBase, CollapseObservation} /\ ~HasTranscriptSurface(s) /\ transcriptSurfaces' = transcriptSurfaces \cup {TranscriptSurfaceEvent(s, b, e, t)} /\ collapseState' = [collapseState EXCEPT ![s] = CollapseObservation] /\ UNCHANGED <<validatorVotes, baseCerts, challengeSurfaces, canonicalCloses, canonicalAborts, sealedFinal>>
114 115 116 117 118 119 120 121 122 123 124 125
ChallengeSurfaceStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots : /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ collapseState[s] = CollapseObservation /\ ~HasChallengeSurface(s) /\ challengeSurfaces' = challengeSurfaces \cup {ChallengeSurfaceEvent(s, b, e, c)} /\ collapseState' = [collapseState EXCEPT ![s] = CollapseObservation] /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces, canonicalCloses, canonicalAborts, sealedFinal>>
126 127 128 129 130 131 132 133 134
CanonicalCloseStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces /\ collapseState[s] = CollapseObservation /\ ~HasCanonicalOutcome(s) /\ canonicalCloses' = canonicalCloses \cup {CanonicalCloseEvent(s, b, e, t)} /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces,
63
135
challengeSurfaces, canonicalAborts, sealedFinal, collapseState>>
136 137 138 139 140 141 142 143 144 145 146 147
CanonicalAbortStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces /\ ~HasCanonicalOutcome(s) /\ canonicalAborts' = canonicalAborts \cup {CanonicalAbortEvent(s, b, e, t, c)} /\ collapseState' = [collapseState EXCEPT ![s] = CollapseAbort] /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, sealedFinal>>
148 149 150 151 152 153 154 155 156
SealStep == \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : /\ CanonicalCloseEvent(s, b, e, t) \in canonicalCloses /\ ~HasCanonicalAbort(s) /\ sealedFinal' = sealedFinal \cup {SealEvent(s, b, e)} /\ collapseState' = [collapseState EXCEPT ![s] = CollapseSealed] /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces, challengeSurfaces, canonicalCloses, canonicalAborts>>
157 158
StutterStep == UNCHANGED vars
159 160 161 162 163 164 165 166 167 168
Next == / ValidatorVoteStep / BaseFinalizeStep / TranscriptSurfaceStep / ChallengeSurfaceStep / CanonicalCloseStep / CanonicalAbortStep / SealStep / StutterStep
169 170 171 172 173 174 175 176 177 178
TypeInvariant == /\ validatorVotes \subseteq ValidatorVoteDomain /\ baseCerts \subseteq BaseCertDomain /\ transcriptSurfaces \subseteq TranscriptSurfaceDomain /\ challengeSurfaces \subseteq ChallengeSurfaceDomain /\ canonicalCloses \subseteq CanonicalCloseDomain /\ canonicalAborts \subseteq CanonicalAbortDomain /\ sealedFinal \subseteq SealedCertDomain /\ collapseState \in [Slots -> CollapseStates]
179 180 181 182 183 184 185 186
NoDualValidatorVotes == \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ ValidatorVoteEvent(v, s, b1, e1) \in validatorVotes /\ ValidatorVoteEvent(v, s, b2, e2) \in validatorVotes => /\ b1 = b2 /\ e1 = e2
187 188 189 190 191 192 193 194 195
NoDualTranscriptSurfaces == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, t1 \in TranscriptRoots, t2 \in TranscriptRoots : /\ TranscriptSurfaceEvent(s, b1, e1, t1) \in transcriptSurfaces /\ TranscriptSurfaceEvent(s, b2, e2, t2) \in transcriptSurfaces => /\ b1 = b2 /\ e1 = e2 /\ t1 = t2
196
64
197 198 199 200 201 202 203 204
NoDualChallengeSurfaces == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, c1 \in ChallengeRoots, c2 \in ChallengeRoots : /\ ChallengeSurfaceEvent(s, b1, e1, c1) \in challengeSurfaces /\ ChallengeSurfaceEvent(s, b2, e2, c2) \in challengeSurfaces => /\ b1 = b2 /\ e1 = e2 /\ c1 = c2
205 206 207 208 209 210
BaseCertSoundness == \A s \in Slots, b \in Blocks, e \in Epochs, q \in SUBSET Validators : BaseCertEvent(s, b, e, q) \in baseCerts => /\ Cardinality(q) >= ValidatorQuorum /\ \A v \in q : ValidatorVoteEvent(v, s, b, e) \in validatorVotes
211 212 213 214 215
TranscriptAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces => \E q \in SUBSET Validators : BaseCertEvent(s, b, e, q) \in baseCerts
216 217 218 219 220 221
ChallengeAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, c \in ChallengeRoots : ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces => \E t \in TranscriptRoots : TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
222 223 224 225 226 227
CanonicalCloseAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces
228 229 230 231 232 233 234
CanonicalAbortAnchored == \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots, c \in ChallengeRoots \ {EmptyChallengeRoot} : CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
235 236 237 238 239 240
SealedAnchored == \A s \in Slots, b \in Blocks, e \in Epochs : SealEvent(s, b, e) \in sealedFinal => /\ \E t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses /\ ~HasCanonicalAbort(s)
241 242 243 244 245 246 247 248
BaseSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, q1 \in SUBSET Validators, q2 \in SUBSET Validators : /\ BaseCertEvent(s, b1, e1, q1) \in baseCerts /\ BaseCertEvent(s, b2, e2, q2) \in baseCerts => /\ b1 = b2 /\ e1 = e2
249 250 251 252 253 254 255 256 257
CanonicalCloseSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, t1 \in TranscriptRoots, t2 \in TranscriptRoots : /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses /\ CanonicalCloseEvent(s, b2, e2, t2) \in canonicalCloses => /\ b1 = b2 /\ e1 = e2 /\ t1 = t2
258
65
259 260 261 262 263
AbortDominatesClose == \A s \in Slots : HasCanonicalAbort(s) => ~(\E b \in Blocks, e \in Epochs, t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses)
264 265 266 267 268 269 270
SealedSafety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ SealEvent(s, b1, e1) \in sealedFinal /\ SealEvent(s, b2, e2) \in sealedFinal => /\ b1 = b2 /\ e1 = e2
271 272 273 274
AbortDominatesSealed == \A s \in Slots, b \in Blocks, e \in Epochs : HasCanonicalAbort(s) => SealEvent(s, b, e) \notin sealedFinal
275 276 277 278 279 280 281
MonotoneCollapse == /\ \A s \in Slots : collapseState[s] = CollapseSealed => \E b \in Blocks, e \in Epochs : SealEvent(s, b, e) \in sealedFinal /\ \A s \in Slots : collapseState[s] = CollapseAbort => HasCanonicalAbort(s)
282 283
Spec == Init /\ [][Next]_vars
284 285
====
66
A.4
NestedGuardian
Witness-augmented layered-threshold model and proof surface.
A.4.1
NestedGuardianProof.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardianProof.tla}
1 2
---- MODULE NestedGuardianProof ---EXTENDS Naturals, FiniteSets, TLAPS
3 4 5
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialWitness
6 7 8
ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses ASSUME MaxReassignmentDepthIsNat == MaxReassignmentDepth \in Nat
9 10 11 12 13 14
ASSUME QuorumIntersection == \A S, T \in SUBSET Validators : /\ Cardinality(S) >= QuorumSize /\ Cardinality(T) >= QuorumSize => S \cap T # {}
15 16
VARIABLES votes, witnessCerts, certs, assignedWitness, reassignmentDepth
17 18
vars == <<votes, witnessCerts, certs, assignedWitness, reassignmentDepth>>
19 20 21 22
VoteDomain == Validators \X Slots \X Blocks \X Epochs WitnessCertDomain == Slots \X Blocks \X Epochs \X Witnesses CertDomain == Slots \X Blocks \X Epochs \X (SUBSET Validators)
23 24 25 26 27 28 29
Init == /\ votes = {} /\ witnessCerts = {} /\ certs = {} /\ assignedWitness = [s \in Slots |-> InitialWitness] /\ reassignmentDepth = [s \in Slots |-> 0]
30 31 32
HasVote(v, s) == \E b \in Blocks, e \in Epochs : <<v, s, b, e>> \in votes
33 34 35
HasWitnessCert(s) == \E b \in Blocks, e \in Epochs, w \in Witnesses : <<s, b, e, w>> \in witnessCerts
36 37 38 39 40 41
IssueWitnessStep == \E s \in Slots, b \in Blocks, e \in Epochs : /\ ~HasWitnessCert(s) /\ witnessCerts' = witnessCerts \cup {<<s, b, e, assignedWitness[s]>>} /\ UNCHANGED <<votes, certs, assignedWitness, reassignmentDepth>>
42 43 44 45 46 47 48 49
ReassignWitnessStep == \E s \in Slots, w \in Witnesses : /\ w # assignedWitness[s] /\ reassignmentDepth[s] < MaxReassignmentDepth /\ assignedWitness' = [assignedWitness EXCEPT ![s] = w] /\ reassignmentDepth' = [reassignmentDepth EXCEPT ![s] = @ + 1] /\ UNCHANGED <<votes, witnessCerts, certs>>
67
50 51 52 53 54 55 56
VoteStep == \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : /\ ~HasVote(v, s) /\ <<s, b, e, assignedWitness[s]>> \in witnessCerts /\ votes' = votes \cup {<<v, s, b, e>>} /\ UNCHANGED <<witnessCerts, certs, assignedWitness, reassignmentDepth>>
57 58 59 60 61 62 63 64
CertifyStep == \E s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators : /\ Cardinality(Q) >= QuorumSize /\ <<s, b, e, assignedWitness[s]>> \in witnessCerts /\ \A v \in Q : <<v, s, b, e>> \in votes /\ certs' = certs \cup {<<s, b, e, Q>>} /\ UNCHANGED <<votes, witnessCerts, assignedWitness, reassignmentDepth>>
65 66
Next == IssueWitnessStep / ReassignWitnessStep / VoteStep / CertifyStep
67 68 69 70 71 72 73
TypeInvariant == /\ votes \subseteq VoteDomain /\ witnessCerts \subseteq WitnessCertDomain /\ certs \subseteq CertDomain /\ assignedWitness \in [Slots -> Witnesses] /\ reassignmentDepth \in [Slots -> 0..MaxReassignmentDepth]
74 75 76
WitnessAssignmentSoundness == \A s \in Slots : reassignmentDepth[s] <= MaxReassignmentDepth
77 78 79 80 81 82 83
NoDualVotes == \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes => /\ b1 = b2 /\ e1 = e2
84 85 86 87 88
WitnessCertificatesStayAssigned == \A s \in Slots, b \in Blocks, e \in Epochs, w \in Witnesses : <<s, b, e, w>> \in witnessCerts => assignedWitness[s] = w / reassignmentDepth[s] > 0
89 90 91 92 93 94
CertSoundness == \A s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators : <<s, b, e, Q>> \in certs => /\ Cardinality(Q) >= QuorumSize /\ \A v \in Q : <<v, s, b, e>> \in votes
95 96 97 98 99 100 101
Invariant == /\ TypeInvariant /\ WitnessAssignmentSoundness /\ NoDualVotes /\ WitnessCertificatesStayAssigned /\ CertSoundness
102 103 104 105 106 107 108 109 110 111
Safety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, Q1 \in SUBSET Validators, Q2 \in SUBSET Validators : /\ <<s, b1, e1, Q1>> \in certs
68
112 113 114
/\ <<s, b2, e2, Q2>> \in certs => /\ b1 = b2 /\ e1 = e2
115 116
Spec == Init /\ [][Next]_vars
117 118 119
120
THEOREM InitImpliesTypeInvariant == Init => TypeInvariant BY SMTT(30), InitialWitnessInWitnesses, MaxReassignmentDepthIsNat DEF Init, TypeInvariant, ,→ VoteDomain, WitnessCertDomain, CertDomain
121 122 123
THEOREM InitImpliesWitnessAssignmentSoundness == Init => WitnessAssignmentSoundness BY SMTT(30), MaxReassignmentDepthIsNat DEF Init, WitnessAssignmentSoundness
124 125 126
THEOREM InitImpliesNoDualVotes == Init => NoDualVotes BY DEF Init, NoDualVotes
127 128 129
THEOREM InitImpliesWitnessCertificatesStayAssigned == Init => WitnessCertificatesStayAssigned BY DEF Init, WitnessCertificatesStayAssigned
130 131 132
THEOREM InitImpliesCertSoundness == Init => CertSoundness BY DEF Init, CertSoundness
133 134 135 136 137
THEOREM InitImpliesInvariant == Init => Invariant BY InitImpliesTypeInvariant, InitImpliesWitnessAssignmentSoundness, InitImpliesNoDualVotes, InitImpliesWitnessCertificatesStayAssigned, InitImpliesCertSoundness DEF Invariant
138 139 140 141 142
THEOREM IssueWitnessPreservesInvariant == Invariant /\ IssueWitnessStep => Invariant' BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes, WitnessCertificatesStayAssigned, CertSoundness, IssueWitnessStep, HasWitnessCert, WitnessCertDomain
143 144 145
146
THEOREM ReassignWitnessPreservesInvariant == Invariant /\ ReassignWitnessStep => Invariant' BY SMTT(30), MaxReassignmentDepthIsNat DEF Invariant, TypeInvariant, ,→ WitnessAssignmentSoundness, NoDualVotes, WitnessCertificatesStayAssigned, CertSoundness, ReassignWitnessStep
147 148 149 150 151
THEOREM VotePreservesInvariant == Invariant /\ VoteStep => Invariant' BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes, WitnessCertificatesStayAssigned, CertSoundness, VoteStep, HasVote, VoteDomain
152 153 154 155
THEOREM CertifyPreservesInvariant == Invariant /\ CertifyStep => Invariant' BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes, WitnessCertificatesStayAssigned, CertSoundness, CertifyStep, CertDomain
156 157 158 159
THEOREM StepPreservesInvariant == Invariant /\ Next => Invariant' BY IssueWitnessPreservesInvariant, ReassignWitnessPreservesInvariant, VotePreservesInvariant, CertifyPreservesInvariant DEF Next
160 161 162 163
THEOREM StutterPreservesTypeInvariant == TypeInvariant /\ UNCHANGED vars => TypeInvariant' BY DEF TypeInvariant, vars
164 165 166 167
THEOREM StutterPreservesWitnessAssignmentSoundness == WitnessAssignmentSoundness /\ UNCHANGED vars => WitnessAssignmentSoundness' BY DEF WitnessAssignmentSoundness, vars
168 169 170 171
THEOREM StutterPreservesNoDualVotes == NoDualVotes /\ UNCHANGED vars => NoDualVotes' BY DEF NoDualVotes, vars
69
172 173 174 175
THEOREM StutterPreservesWitnessCertificatesStayAssigned == WitnessCertificatesStayAssigned /\ UNCHANGED vars => WitnessCertificatesStayAssigned' BY DEF WitnessCertificatesStayAssigned, vars
176 177 178 179
THEOREM StutterPreservesCertSoundness == CertSoundness /\ UNCHANGED vars => CertSoundness' BY DEF CertSoundness, vars
180 181 182 183 184
THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant' BY StutterPreservesTypeInvariant, StutterPreservesWitnessAssignmentSoundness, StutterPreservesNoDualVotes, StutterPreservesWitnessCertificatesStayAssigned, StutterPreservesCertSoundness DEF Invariant
185 186 187
THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant' BY StepPreservesInvariant, StutterPreservesInvariant DEF vars
188 189 190 191 192 193 194 195 196 197 198 199 200 201
THEOREM QuorumCertificatesIntersect == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs, Q1 \in SUBSET Validators, Q2 \in SUBSET Validators : /\ Invariant /\ <<s, b1, e1, Q1>> \in certs /\ <<s, b2, e2, Q2>> \in certs => Q1 \cap Q2 # {} BY SMTT(60), QuorumIntersection DEF Invariant, CertSoundness
202 203 204 205
THEOREM InvariantImpliesSafety == Invariant => Safety BY SMTT(60), QuorumCertificatesIntersect DEF Invariant, Safety, NoDualVotes, CertSoundness
206 207
====
A.4.2
NestedGuardian.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardian.tla}
1 2
---- MODULE NestedGuardian ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4 5
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialEpoch, InitialWitness
6 7 8
ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses
9 10 11 12 13 14
ASSUME QuorumIntersection == \A S, T \in SUBSET Validators : /\ Cardinality(S) >= QuorumSize /\ Cardinality(T) >= QuorumSize => S \cap T # {}
15 16
VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline,
70
17
witnessCheckpoint, assignedWitness, reassignmentDepth
18 19 20
vars == <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
21 22
CheckpointLevels == 0..2
23 24 25 26
VoteEvent(v, s, b, e) == <<v, s, b, e>> WitnessEvent(w, s, b, e) == <<w, s, b, e>> Finalization(s, b, e) == <<s, b, e>>
27 28 29
30
VoteDomain == {VoteEvent(v, s, b, e) : v \in Validators, s \in Slots, b \in Blocks, e \in Epochs} WitnessDomain == {WitnessEvent(w, s, b, e) : w \in Witnesses, s \in Slots, b \in Blocks, e \in ,→ Epochs} FinalizationDomain == {Finalization(s, b, e) : s \in Slots, b \in Blocks, e \in Epochs}
31 32 33 34 35 36 37 38 39 40 41 42
Init == /\ votes = {} /\ witnessCerts = {} /\ finalized = {} /\ finalizerSets = [f \in FinalizationDomain |-> {}] /\ registryEpoch = [v \in Validators |-> InitialEpoch] /\ guardianReady = [v \in Validators |-> TRUE] /\ witnessOnline = [w \in Witnesses |-> TRUE] /\ witnessCheckpoint = [w \in Witnesses |-> 1] /\ assignedWitness = [s \in Slots |-> InitialWitness] /\ reassignmentDepth = [s \in Slots |-> 0]
43 44 45
HasVote(v, s) == \E b \in Blocks, e \in Epochs : VoteEvent(v, s, b, e) \in votes
46 47 48
HasWitnessCert(w, s) == \E b \in Blocks, e \in Epochs : WitnessEvent(w, s, b, e) \in witnessCerts
49 50 51 52 53 54 55 56 57 58
CanIssueWitness(w, s, b, e) == /\ w \in Witnesses /\ s \in Slots /\ b \in Blocks /\ e \in Epochs /\ witnessOnline[w] /\ witnessCheckpoint[w] > 0 /\ assignedWitness[s] = w /\ ~HasWitnessCert(w, s)
59 60 61 62 63 64
IssueWitness(w, s, b, e) == /\ CanIssueWitness(w, s, b, e) /\ witnessCerts' = witnessCerts \cup {WitnessEvent(w, s, b, e)} /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
65 66 67 68 69 70 71
CanReassign(s, w) == /\ s \in Slots /\ w \in Witnesses /\ w # assignedWitness[s] /\ ~witnessOnline[assignedWitness[s]] /\ reassignmentDepth[s] < MaxReassignmentDepth
72 73 74 75 76 77
ReassignWitness(s, w) == /\ CanReassign(s, w) /\ assignedWitness' = [assignedWitness EXCEPT ![s] = w] /\ reassignmentDepth' = [reassignmentDepth EXCEPT ![s] = @ + 1] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
71
78
witnessOnline, witnessCheckpoint>>
79 80 81 82 83 84 85 86 87 88
CanVote(v, s, b, e) == /\ v \in Validators /\ s \in Slots /\ b \in Blocks /\ e \in Epochs /\ guardianReady[v] /\ registryEpoch[v] = e /\ ~HasVote(v, s) /\ WitnessEvent(assignedWitness[s], s, b, e) \in witnessCerts
89 90 91 92 93
94
Vote(v, s, b, e) == /\ CanVote(v, s, b, e) /\ votes' = votes \cup {VoteEvent(v, s, b, e)} /\ UNCHANGED <<witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
95 96 97 98 99 100 101
EligibleVoters(s, b, e) == {v \in Validators : /\ VoteEvent(v, s, b, e) \in votes /\ guardianReady[v] /\ registryEpoch[v] = e /\ WitnessEvent(assignedWitness[s], s, b, e) \in witnessCerts}
102 103 104 105 106 107
CanFinalize(s, b, e) == /\ s \in Slots /\ b \in Blocks /\ e \in Epochs /\ Cardinality(EligibleVoters(s, b, e)) >= QuorumSize
108 109 110 111 112 113 114
Finalize(s, b, e) == /\ CanFinalize(s, b, e) /\ finalized' = finalized \cup {Finalization(s, b, e)} /\ finalizerSets' = [finalizerSets EXCEPT ![Finalization(s, b, e)] = EligibleVoters(s, b, e)] /\ UNCHANGED <<votes, witnessCerts, registryEpoch, guardianReady, witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
115 116 117 118 119 120 121 122
AdoptEpoch(v, e) == /\ v \in Validators /\ e \in Epochs /\ e >= registryEpoch[v] /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, guardianReady, witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
123 124 125 126 127 128 129 130
RegistryRollback(v, e) == /\ v \in Validators /\ e \in Epochs /\ e < registryEpoch[v] /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, guardianReady, witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
131 132 133 134 135 136 137
GuardianOutage(v) == /\ v \in Validators /\ guardianReady[v] /\ guardianReady' = [guardianReady EXCEPT ![v] = FALSE] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>
138
72
139 140 141 142 143 144
WitnessOutage(w) == /\ w \in Witnesses /\ witnessOnline[w] /\ witnessOnline' = [witnessOnline EXCEPT ![w] = FALSE] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessCheckpoint, assignedWitness, reassignmentDepth>>
145 146 147 148 149 150 151
WitnessRecovery(w) == /\ w \in Witnesses /\ ~witnessOnline[w] /\ witnessOnline' = [witnessOnline EXCEPT ![w] = TRUE] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessCheckpoint, assignedWitness, reassignmentDepth>>
152 153 154 155 156 157 158 159
AdvanceWitnessCheckpoint(w, level) == /\ w \in Witnesses /\ level \in CheckpointLevels /\ level > witnessCheckpoint[w] /\ witnessCheckpoint' = [witnessCheckpoint EXCEPT ![w] = level] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline, assignedWitness, reassignmentDepth>>
160 161 162 163 164 165 166 167
WitnessCheckpointRollback(w, level) == /\ w \in Witnesses /\ level \in CheckpointLevels /\ level < witnessCheckpoint[w] /\ witnessCheckpoint' = [witnessCheckpoint EXCEPT ![w] = level] /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline, assignedWitness, reassignmentDepth>>
168 169 170 171 172 173 174 175 176 177 178 179 180
Next == / \E w \in Witnesses, s \in Slots, b \in Blocks, e \in Epochs : IssueWitness(w, s, b, e) / \E s \in Slots, w \in Witnesses : ReassignWitness(s, w) / \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : Vote(v, s, b, e) / \E s \in Slots, b \in Blocks, e \in Epochs : Finalize(s, b, e) / \E v \in Validators, e \in Epochs : AdoptEpoch(v, e) / \E v \in Validators, e \in Epochs : RegistryRollback(v, e) / \E v \in Validators : GuardianOutage(v) / \E w \in Witnesses : WitnessOutage(w) / \E w \in Witnesses : WitnessRecovery(w) / \E w \in Witnesses, level \in CheckpointLevels : AdvanceWitnessCheckpoint(w, level) / \E w \in Witnesses, level \in CheckpointLevels : WitnessCheckpointRollback(w, level)
181 182 183 184 185 186 187 188 189 190 191 192
TypeInvariant == /\ votes \subseteq VoteDomain /\ witnessCerts \subseteq WitnessDomain /\ finalized \subseteq FinalizationDomain /\ finalizerSets \in [FinalizationDomain -> SUBSET Validators] /\ registryEpoch \in [Validators -> Epochs] /\ guardianReady \in [Validators -> BOOLEAN] /\ witnessOnline \in [Witnesses -> BOOLEAN] /\ witnessCheckpoint \in [Witnesses -> CheckpointLevels] /\ assignedWitness \in [Slots -> Witnesses] /\ reassignmentDepth \in [Slots -> 0..MaxReassignmentDepth]
193 194 195 196
WitnessAssignmentSoundness == \A s \in Slots : reassignmentDepth[s] <= MaxReassignmentDepth
197 198 199 200
NoDualVotes == \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ VoteEvent(v, s, b1, e1) \in votes
73
201 202 203
/\ VoteEvent(v, s, b2, e2) \in votes => /\ b1 = b2 /\ e1 = e2
204 205 206 207 208
WitnessCertificatesStayAssigned == \A w \in Witnesses, s \in Slots, b \in Blocks, e \in Epochs : WitnessEvent(w, s, b, e) \in witnessCerts => assignedWitness[s] = w / reassignmentDepth[s] > 0
209 210 211 212 213 214 215
FinalizationWitnessSoundness == \A s \in Slots, b \in Blocks, e \in Epochs : Finalization(s, b, e) \in finalized => /\ Cardinality(finalizerSets[Finalization(s, b, e)]) >= QuorumSize /\ \A v \in finalizerSets[Finalization(s, b, e)] : VoteEvent(v, s, b, e) \in votes
216 217 218 219 220 221 222
Invariant == /\ TypeInvariant /\ WitnessAssignmentSoundness /\ NoDualVotes /\ WitnessCertificatesStayAssigned /\ FinalizationWitnessSoundness
223 224 225 226 227 228
Safety == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ Finalization(s, b1, e1) \in finalized /\ Finalization(s, b2, e2) \in finalized => b1 = b2
229 230 231
Spec == Init /\ [][Next]_vars
232 233 234
THEOREM OneInCheckpointLevels == 1 \in CheckpointLevels BY SMT DEF CheckpointLevels
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
THEOREM InitImpliesInvariant == Init => Invariant PROOF <1>1. Init => TypeInvariant BY SMT, InitialEpochInEpochs, InitialWitnessInWitnesses, OneInCheckpointLevels DEF Init, TypeInvariant, VoteDomain, WitnessDomain, FinalizationDomain <1>2. Init => WitnessAssignmentSoundness BY DEF Init, WitnessAssignmentSoundness <1>3. Init => NoDualVotes BY DEF Init, NoDualVotes <1>4. Init => WitnessCertificatesStayAssigned BY DEF Init, WitnessCertificatesStayAssigned <1>5. Init => FinalizationWitnessSoundness BY DEF Init, FinalizationWitnessSoundness <1>6. QED BY <1>1, <1>2, <1>3, <1>4, <1>5 DEF Invariant
251 252 253 254 255 256 257 258 259
THEOREM StepPreservesInvariant == Invariant /\ Next => Invariant' BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes, WitnessCertificatesStayAssigned, FinalizationWitnessSoundness, Next, IssueWitness, ReassignWitness, Vote, Finalize, AdoptEpoch, RegistryRollback, GuardianOutage, WitnessOutage, WitnessRecovery, AdvanceWitnessCheckpoint, WitnessCheckpointRollback, CanIssueWitness, CanVote, HasVote, CanFinalize, EligibleVoters, VoteEvent, WitnessEvent, Finalization, VoteDomain, WitnessDomain, FinalizationDomain
260 261 262
THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant' BY SMT DEF Invariant, vars
74
263 264 265
THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant' BY SMT, StepPreservesInvariant, StutterPreservesInvariant DEF vars
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
THEOREM FinalizedWitnessesIntersect == \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs : /\ Invariant /\ <<s, b1, e1>> \in finalized /\ <<s, b2, e2>> \in finalized => \E v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes PROOF <1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs <1>2. ASSUME Invariant, <<s, b1, e1>> \in finalized, <<s, b2, e2>> \in finalized PROVE \E v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes <2>1. finalizerSets[<<s, b1, e1>>] \subseteq Validators BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization <2>2. finalizerSets[<<s, b2, e2>>] \subseteq Validators BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization <2>3. Cardinality(finalizerSets[<<s, b1, e1>>]) >= QuorumSize BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness <2>4. Cardinality(finalizerSets[<<s, b2, e2>>]) >= QuorumSize BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness <2>5. finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] # {} BY <2>1, <2>2, <2>3, <2>4, QuorumIntersection <2>6. PICK v \in finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] : TRUE BY <2>5 <2>7. <<v, s, b1, e1>> \in votes BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness <2>8. <<v, s, b2, e2>> \in votes BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness <2>9. QED BY SMT, <2>6, <2>7, <2>8 <1>3. QED BY <1>2
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
THEOREM InvariantImpliesSafety == Invariant => Safety PROOF <1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs <1>2. ASSUME Invariant, <<s, b1, e1>> \in finalized, <<s, b2, e2>> \in finalized PROVE b1 = b2 <2>1. \E v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes BY SMT, FinalizedWitnessesIntersect, <1>2 <2>2. PICK v \in Validators : /\ <<v, s, b1, e1>> \in votes /\ <<v, s, b2, e2>> \in votes BY <2>1 <2>3. QED BY SMT, <1>2, <2>2 DEF Invariant, NoDualVotes <1>3. QED BY <1>2 DEF Safety
323 324
====
75
A.5
CanonicalOrdering Companion Witnesses
Executable witness artifacts for omission dominance and recursive continuity. A.5.1
CanonicalOrderingOmissionTrace.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ca nonical_ordering/CanonicalOrderingOmissionTrace.tla} 1 2
---- MODULE CanonicalOrderingOmissionTrace ---EXTENDS CanonicalOrdering
3 4 5 6
TargetSlot == 1 TargetCert == {"tx1"} TargetTx == "tx2"
7 8 9 10 11 12 13
WitnessState == /\ TargetSlot \in closedCutoffs /\ bulletin[TargetSlot] = {"tx1", "tx2"} /\ CertEvent(TargetSlot, TargetCert) \in candidateCerts /\ OmissionEvent(TargetSlot, TargetCert, TargetTx) \in omissionProofs /\ CertEvent(TargetSlot, TargetCert) \notin admittedCerts
14 15
NoOmissionDominanceWitness == ~WitnessState
16 17
====
A.5.2
CanonicalOrderingOmissionTrace.cfg
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ca nonical_ordering/CanonicalOrderingOmissionTrace.cfg} 1
SPECIFICATION Spec
2 3 4 5
CONSTANTS Slots = {1} Transactions = {"tx1", "tx2"}
6 7 8 9 10 11 12 13 14 15
INVARIANTS TypeInvariant AdmittedSoundness OmissionSoundness RecoveredSoundness AdmittedUniqueness Recoverability OmissionDominates NoOmissionDominanceWitness
A.5.3
CanonicalCollapseRecursiveContinuity.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ca nonical_ordering/CanonicalCollapseRecursiveContinuity.tla}
76
1 2
---- MODULE CanonicalCollapseRecursiveContinuity ---EXTENDS Naturals, Sequences, TLC
3 4
CONSTANT MaxHeight
5 6 7 8 9
Slots == 1..MaxHeight Genesis == 1 NonGenesisSlots == Slots \ {Genesis} NullHash == 0
10 11
VARIABLES publishedCollapses, publishedProofs, publishedExtensionCertificates, admittedHeaders
12 13 14
vars == <<publishedCollapses, publishedProofs, publishedExtensionCertificates, admittedHeaders>>
15 16
RECURSIVE AccumulatorHash(), ProofHash(), ProofChain(_)
17 18
PayloadHash(s) == <<"payload", s>>
19 20 21 22 23
AccumulatorHash(s) == IF s = Genesis THEN <<"accum", s, NullHash, PayloadHash(s)>> ELSE <<"accum", s, AccumulatorHash(s - 1), PayloadHash(s)>>
24 25 26 27 28
Commitment(s) == [height |-> s, continuityAccumulatorHash |-> AccumulatorHash(s), resultingStateRootHash |-> <<"state", s>>]
29 30
CommitmentHash(s) == <<"commitment-hash", Commitment(s)>>
31 32 33
PreviousCommitmentHash(s) == IF s = Genesis THEN NullHash ELSE CommitmentHash(s - 1)
34 35 36
StatementHash(s) == <<"statement-hash", Commitment(s), PreviousCommitmentHash(s), PayloadHash(s)>>
37 38 39
PreviousProofHash(s) == IF s = Genesis THEN NullHash ELSE ProofHash(s - 1)
40 41 42
ProofBytes(s) == <<"hash-pcd-v1", StatementHash(s), PreviousProofHash(s)>>
43 44 45 46 47 48 49
ProofStep(s) == [commitment |-> Commitment(s), previousCommitmentHash |-> PreviousCommitmentHash(s), payloadHash |-> PayloadHash(s), previousProofHash |-> PreviousProofHash(s), proofBytes |-> ProofBytes(s)]
50 51
ProofHash(s) == <<"proof-hash", ProofStep(s)>>
52 53 54 55 56
ProofChain(s) == IF s = Genesis THEN <<ProofStep(s)>> ELSE Append(ProofChain(s - 1), ProofStep(s))
57 58 59 60 61
ExtensionCertificate(s) == [coveredHeight |-> s, predecessorCommitment |-> Commitment(s - 1), predecessorProofHash |-> ProofHash(s - 1)]
77
62 63
Last(seq) == seq[Len(seq)]
64 65 66 67 68 69
Init == /\ publishedCollapses = {} /\ publishedProofs = {} /\ publishedExtensionCertificates = {} /\ admittedHeaders = {}
70 71 72 73 74 75
PublishCollapseStep == \E s \in Slots : /\ s \notin publishedCollapses /\ publishedCollapses' = publishedCollapses \cup {s} /\ UNCHANGED <<publishedProofs, publishedExtensionCertificates, admittedHeaders>>
76 77 78 79 80 81 82 83
PublishRecursiveProofStep == \E s \in Slots : /\ s \in publishedCollapses /\ s \notin publishedProofs /\ IF s = Genesis THEN TRUE ELSE s - 1 \in publishedProofs /\ publishedProofs' = publishedProofs \cup {s} /\ UNCHANGED <<publishedCollapses, publishedExtensionCertificates, admittedHeaders>>
84 85 86 87 88 89 90 91
PublishExtensionCertificateStep == \E s \in NonGenesisSlots : /\ s \in publishedCollapses /\ s - 1 \in publishedProofs /\ s \notin publishedExtensionCertificates /\ publishedExtensionCertificates' = publishedExtensionCertificates \cup {s} /\ UNCHANGED <<publishedCollapses, publishedProofs, admittedHeaders>>
92 93 94 95 96 97 98 99
AdmitHeaderStep == \E s \in Slots : /\ s \in publishedCollapses /\ s \notin admittedHeaders /\ IF s = Genesis THEN TRUE ELSE s \in publishedExtensionCertificates /\ admittedHeaders' = admittedHeaders \cup {s} /\ UNCHANGED <<publishedCollapses, publishedProofs, publishedExtensionCertificates>>
100 101 102 103 104 105
Next == / PublishCollapseStep / PublishRecursiveProofStep / PublishExtensionCertificateStep / AdmitHeaderStep
106 107 108 109 110 111
TypeInvariant == /\ publishedCollapses \subseteq Slots /\ publishedProofs \subseteq Slots /\ publishedExtensionCertificates \subseteq NonGenesisSlots /\ admittedHeaders \subseteq Slots
112 113 114 115 116 117 118 119 120 121 122 123
RecursiveProofSoundness == \A s \in publishedProofs : /\ s \in publishedCollapses /\ IF s = Genesis THEN TRUE ELSE s - 1 \in publishedProofs /\ LET step == ProofStep(s) IN /\ step.commitment = Commitment(s) /\ step.previousCommitmentHash = PreviousCommitmentHash(s) /\ step.payloadHash = PayloadHash(s) /\ step.previousProofHash = PreviousProofHash(s) /\ step.proofBytes = ProofBytes(s) /\ step.commitment.continuityAccumulatorHash = AccumulatorHash(s)
78
124 125 126 127 128 129 130 131
RecursiveProofChainSoundness == \A s \in publishedProofs : /\ Len(ProofChain(s)) = s /\ Last(ProofChain(s)) = ProofStep(s) /\ IF s = Genesis THEN TRUE ELSE /\ ProofChain(s)[Len(ProofChain(s)) - 1] = ProofStep(s - 1)
132 133 134 135 136 137 138 139
ExtensionCertificateSoundness == \A s \in publishedExtensionCertificates : /\ s \in NonGenesisSlots /\ s - 1 \in publishedProofs /\ ExtensionCertificate(s).coveredHeight = s /\ ExtensionCertificate(s).predecessorCommitment = Commitment(s - 1) /\ ExtensionCertificate(s).predecessorProofHash = ProofHash(s - 1)
140 141 142 143 144 145 146 147 148 149
HeaderAdmissionSoundness == \A s \in admittedHeaders : /\ s \in publishedCollapses /\ IF s = Genesis THEN TRUE ELSE /\ s \in publishedExtensionCertificates /\ s - 1 \in publishedProofs /\ ExtensionCertificate(s).predecessorCommitment = Commitment(s - 1) /\ ExtensionCertificate(s).predecessorProofHash = ProofHash(s - 1)
150 151 152 153 154 155 156
Invariant == /\ TypeInvariant /\ RecursiveProofSoundness /\ RecursiveProofChainSoundness /\ ExtensionCertificateSoundness /\ HeaderAdmissionSoundness
157 158
Spec == Init /\ [][Next]_vars
159 160
====
A.5.4
CanonicalCollapseRecursiveContinuity.cfg
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ca nonical_ordering/CanonicalCollapseRecursiveContinuity.cfg}
1
SPECIFICATION Spec
2 3 4
CONSTANTS MaxHeight = 3
5 6 7 8 9 10 11
INVARIANTS TypeInvariant RecursiveProofSoundness RecursiveProofChainSoundness ExtensionCertificateSoundness HeaderAdmissionSoundness
79
A.6
Recovery and Classical-Agreement Bridge
Recurring recovery kernel, finite reduction, totality bridge, and final classical-agreement collapse wrapper.
A.6.1
NestedGuardianRecoveryRecurringInductionCore.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardianRecoveryRecurringInductionCore.tla}
1 2
---- MODULE NestedGuardianRecoveryRecurringInductionCore ---EXTENDS Naturals, FiniteSets, TLC
3 4 5 6 7 8
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialEpoch, InitialWitness, TotalCycles, TargetSlotOf(), TargetBlockOf(), StableEpochOf(_), SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold, SmallRecoveryCommittee, LargeRecoveryCommittee
9 10 11 12 13 14 15 16 17 18
ASSUME InitialEpoch \in Epochs ASSUME InitialWitness \in Witnesses ASSUME QuorumSize \in 1..Cardinality(Validators) ASSUME TotalCycles \in Nat ASSUME TotalCycles >= 1 ASSUME \A c \in 1..TotalCycles : /\ TargetSlotOf(c) \in Slots /\ TargetBlockOf(c) \in Blocks /\ StableEpochOf(c) \in Epochs
19 20
21 22 23 24 25 26
VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage, continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary, continuationPagePublished, continuationPageBoundary, continuationFetched, shareReceipts, shareConflicts, windowClosed, missingShareClaims, missingThresholdCertificates, recovered, recoveredSurfaces, recoveryConflicts, aborted
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
Core == INSTANCE NestedGuardianRecoveryRecurringLivenessCore WITH Validators <- Validators, Witnesses <- Witnesses, Blocks <- Blocks, Slots <- Slots, Epochs <- Epochs, QuorumSize <- QuorumSize, MaxReassignmentDepth <- MaxReassignmentDepth, InitialEpoch <- InitialEpoch, InitialWitness <- InitialWitness, TotalCycles <- TotalCycles, TargetSlotOf <- TargetSlotOf, TargetBlockOf <- TargetBlockOf, StableEpochOf <- StableEpochOf, SmallCommitteeSlot <- SmallCommitteeSlot, SmallRecoveryThreshold <- SmallRecoveryThreshold, LargeRecoveryThreshold <- LargeRecoveryThreshold, SmallRecoveryCommittee <- SmallRecoveryCommittee, LargeRecoveryCommittee <- LargeRecoveryCommittee,
80
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
votes <- votes, witnessCerts <- witnessCerts, finalized <- finalized, finalizerSets <- finalizerSets, registryEpoch <- registryEpoch, guardianReady <- guardianReady, witnessOnline <- witnessOnline, witnessCheckpoint <- witnessCheckpoint, assignedWitness <- assignedWitness, reassignmentDepth <- reassignmentDepth, currentCycle <- currentCycle, phase <- phase, churnStage <- churnStage, continuationBoundary <- continuationBoundary, continuationAnchorPublished <- continuationAnchorPublished, continuationAnchorBoundary <- continuationAnchorBoundary, continuationPagePublished <- continuationPagePublished, continuationPageBoundary <- continuationPageBoundary, continuationFetched <- continuationFetched, shareReceipts <- shareReceipts, shareConflicts <- shareConflicts, windowClosed <- windowClosed, missingShareClaims <- missingShareClaims, missingThresholdCertificates <- missingThresholdCertificates, recovered <- recovered, recoveredSurfaces <- recoveredSurfaces, recoveryConflicts <- recoveryConflicts, aborted <- aborted
76 77 78 79 80
vars == Core!vars CycleRange == Core!CycleRange PrefixAdvanceRange == Core!PrefixAdvanceRange RecoveryClosedPrefix(c) == Core!RecoveryClosedPrefix(c)
81 82 83 84
PriorCycleRange(c) == IF c = 1 THEN {} ELSE 1..(c - 1)
85 86 87
RecoveryInductionBase == <>RecoveryClosedPrefix(1)
88 89 90 91
RecoveryInductionStep(c) == /\ c \in PrefixAdvanceRange /\ Core!RecoveryPrefixAdvanceContract(c)
92 93 94 95 96 97
RecoveryInductionPremisesUpTo(c) == /\ c \in CycleRange /\ RecoveryInductionBase /\ \A i \in PriorCycleRange(c) : RecoveryInductionStep(i)
98 99 100 101 102
RecoveryRecurringInductionPremises == /\ RecoveryInductionBase /\ \A i \in PrefixAdvanceRange : RecoveryInductionStep(i)
103 104 105 106 107
RecoveryClosedPrefixInductionKernel(c) == /\ c \in CycleRange /\ (RecoveryInductionPremisesUpTo(c) => <>RecoveryClosedPrefix(c))
108 109
RecoveryRecurringInductionKernel ==
81
110 111
\A c \in CycleRange : RecoveryClosedPrefixInductionKernel(c)
112 113
====
A.6.2
NestedGuardianRecoveryRecurringProof.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardianRecoveryRecurringProof.tla}
1 2
---- MODULE NestedGuardianRecoveryRecurringProof ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4 5 6 7 8
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialEpoch, InitialWitness, TotalCycles, TargetSlotOf(), TargetBlockOf(), StableEpochOf(_), SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold, SmallRecoveryCommittee, LargeRecoveryCommittee
9 10 11 12 13 14 15 16 17 18 19
ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses ASSUME QuorumSizeInValidatorRange == QuorumSize \in 1..Cardinality(Validators) ASSUME TotalCyclesIsNat == TotalCycles \in Nat ASSUME TotalCyclesAtLeastOne == TotalCycles >= 1 ASSUME TargetCycleDomains == \A c \in 1..TotalCycles : /\ TargetSlotOf(c) \in Slots /\ TargetBlockOf(c) \in Blocks /\ StableEpochOf(c) \in Epochs
20 21
22 23 24 25 26 27
VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage, continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary, continuationPagePublished, continuationPageBoundary, continuationFetched, shareReceipts, shareConflicts, windowClosed, missingShareClaims, missingThresholdCertificates, recovered, recoveredSurfaces, recoveryConflicts, aborted
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
Core == INSTANCE NestedGuardianRecoveryRecurringInductionCore WITH Validators <- Validators, Witnesses <- Witnesses, Blocks <- Blocks, Slots <- Slots, Epochs <- Epochs, QuorumSize <- QuorumSize, MaxReassignmentDepth <- MaxReassignmentDepth, InitialEpoch <- InitialEpoch, InitialWitness <- InitialWitness, TotalCycles <- TotalCycles, TargetSlotOf <- TargetSlotOf, TargetBlockOf <- TargetBlockOf, StableEpochOf <- StableEpochOf, SmallCommitteeSlot <- SmallCommitteeSlot, SmallRecoveryThreshold <- SmallRecoveryThreshold, LargeRecoveryThreshold <- LargeRecoveryThreshold, SmallRecoveryCommittee <- SmallRecoveryCommittee, LargeRecoveryCommittee <- LargeRecoveryCommittee,
82
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
votes <- votes, witnessCerts <- witnessCerts, finalized <- finalized, finalizerSets <- finalizerSets, registryEpoch <- registryEpoch, guardianReady <- guardianReady, witnessOnline <- witnessOnline, witnessCheckpoint <- witnessCheckpoint, assignedWitness <- assignedWitness, reassignmentDepth <- reassignmentDepth, currentCycle <- currentCycle, phase <- phase, churnStage <- churnStage, continuationBoundary <- continuationBoundary, continuationAnchorPublished <- continuationAnchorPublished, continuationAnchorBoundary <- continuationAnchorBoundary, continuationPagePublished <- continuationPagePublished, continuationPageBoundary <- continuationPageBoundary, continuationFetched <- continuationFetched, shareReceipts <- shareReceipts, shareConflicts <- shareConflicts, windowClosed <- windowClosed, missingShareClaims <- missingShareClaims, missingThresholdCertificates <- missingThresholdCertificates, recovered <- recovered, recoveredSurfaces <- recoveredSurfaces, recoveryConflicts <- recoveryConflicts, aborted <- aborted
77 78 79 80
RecoveryRecurringClosedPrefixes == \A c \in Core!CycleRange : <>Core!RecoveryClosedPrefix(c)
81 82 83 84 85
RecoveryParametricRecurrenceArgument == /\ Core!RecoveryRecurringInductionPremises /\ Core!RecoveryRecurringInductionKernel => RecoveryRecurringClosedPrefixes
86 87 88 89 90 91 92
THEOREM PriorCycleRangeImpliesTotalCyclesNotOne == \A c \in Core!CycleRange : \A i \in Core!PriorCycleRange(c) : TotalCycles # 1 BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF Core!CycleRange, Core!Core!CycleRange, Core!PriorCycleRange
93 94 95 96 97 98 99
THEOREM PriorCycleRangeImpliesPrefixAdvanceInterval == \A c \in Core!CycleRange : \A i \in Core!PriorCycleRange(c) : i \in 1..(TotalCycles - 1) BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF Core!CycleRange, Core!Core!CycleRange, Core!PriorCycleRange
100 101 102 103 104 105 106 107 108 109 110
THEOREM RecoveryInductionPremisesRestrict == \A c \in Core!CycleRange : Core!RecoveryRecurringInductionPremises => Core!RecoveryInductionPremisesUpTo(c) PROOF <1>1. TAKE c \in Core!CycleRange <1>2. ASSUME Core!RecoveryRecurringInductionPremises PROVE Core!RecoveryInductionPremisesUpTo(c) <2>1. Core!RecoveryInductionBase BY <1>2 DEF Core!RecoveryRecurringInductionPremises
83
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
<2>2. \A i \in Core!PriorCycleRange(c) : Core!RecoveryInductionStep(i) PROOF <3>1. TAKE i \in Core!PriorCycleRange(c) <3>2. i \in Core!PrefixAdvanceRange PROOF <4>1. TotalCycles # 1 BY PriorCycleRangeImpliesTotalCyclesNotOne, <1>1, <3>1 <4>2. i \in 1..(TotalCycles - 1) BY PriorCycleRangeImpliesPrefixAdvanceInterval, <1>1, <3>1 <4>3. TotalCycles # 1 BY <4>1 <4>6. QED BY <4>3, <4>2 DEF Core!PrefixAdvanceRange, Core!Core!PrefixAdvanceRange <3>3. Core!RecoveryInductionStep(i) BY <1>2, <3>2 DEF Core!RecoveryRecurringInductionPremises <3>4. QED BY <3>3 <2>3. QED BY <1>1, <2>1, <2>2 DEF Core!RecoveryInductionPremisesUpTo <1>3. QED BY <1>2
135 136 137 138 139 140 141 142
THEOREM RecoveryInductionKernelRestrict == \A c \in Core!CycleRange : Core!RecoveryRecurringInductionKernel => Core!RecoveryClosedPrefixInductionKernel(c) BY DEF Core!RecoveryRecurringInductionKernel, Core!RecoveryClosedPrefixInductionKernel, Core!CycleRange
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
THEOREM RecoveryRecurringClosedPrefixFromKernel == \A c \in Core!CycleRange : /\ Core!RecoveryRecurringInductionPremises /\ Core!RecoveryRecurringInductionKernel => <>Core!RecoveryClosedPrefix(c) PROOF <1>1. TAKE c \in Core!CycleRange <1>2. ASSUME Core!RecoveryRecurringInductionPremises, Core!RecoveryRecurringInductionKernel PROVE <>Core!RecoveryClosedPrefix(c) <2>1. Core!RecoveryInductionPremisesUpTo(c) BY RecoveryInductionPremisesRestrict, <1>1, <1>2 <2>2. Core!RecoveryClosedPrefixInductionKernel(c) BY RecoveryInductionKernelRestrict, <1>1, <1>2 <2>3. QED BY <2>1, <2>2 DEF Core!RecoveryClosedPrefixInductionKernel <1>3. QED BY <1>2
163 164 165 166 167 168
THEOREM RecoveryParametricRecurrenceArgumentTheorem == RecoveryParametricRecurrenceArgument BY RecoveryRecurringClosedPrefixFromKernel DEF RecoveryParametricRecurrenceArgument, RecoveryRecurringClosedPrefixes
169 170
====
84
A.6.3
NestedGuardianRecoveryClassicalAgreementReduction.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardianRecoveryClassicalAgreementReduction.tla}
1 2
---- MODULE NestedGuardianRecoveryClassicalAgreementReduction ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4 5 6 7 8
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialEpoch, InitialWitness, TotalCycles, TargetSlotOf(), TargetBlockOf(), StableEpochOf(_), SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold, SmallRecoveryCommittee, LargeRecoveryCommittee
9 10 11 12 13 14 15 16 17 18
ASSUME InitialEpoch \in Epochs ASSUME InitialWitness \in Witnesses ASSUME QuorumSize \in 1..Cardinality(Validators) ASSUME TotalCycles \in Nat ASSUME TotalCycles >= 1 ASSUME \A c \in 1..TotalCycles : /\ TargetSlotOf(c) \in Slots /\ TargetBlockOf(c) \in Blocks /\ StableEpochOf(c) \in Epochs
19 20
21 22 23 24 25 26
VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage, continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary, continuationPagePublished, continuationPageBoundary, continuationFetched, shareReceipts, shareConflicts, windowClosed, missingShareClaims, missingThresholdCertificates, recovered, recoveredSurfaces, recoveryConflicts, aborted
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
Proof == INSTANCE NestedGuardianRecoveryRecurringProof WITH Validators <- Validators, Witnesses <- Witnesses, Blocks <- Blocks, Slots <- Slots, Epochs <- Epochs, QuorumSize <- QuorumSize, MaxReassignmentDepth <- MaxReassignmentDepth, InitialEpoch <- InitialEpoch, InitialWitness <- InitialWitness, TotalCycles <- TotalCycles, TargetSlotOf <- TargetSlotOf, TargetBlockOf <- TargetBlockOf, StableEpochOf <- StableEpochOf, SmallCommitteeSlot <- SmallCommitteeSlot, SmallRecoveryThreshold <- SmallRecoveryThreshold, LargeRecoveryThreshold <- LargeRecoveryThreshold, SmallRecoveryCommittee <- SmallRecoveryCommittee, LargeRecoveryCommittee <- LargeRecoveryCommittee, votes <- votes, witnessCerts <- witnessCerts, finalized <- finalized, finalizerSets <- finalizerSets, registryEpoch <- registryEpoch, guardianReady <- guardianReady, witnessOnline <- witnessOnline,
85
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
witnessCheckpoint <- witnessCheckpoint, assignedWitness <- assignedWitness, reassignmentDepth <- reassignmentDepth, currentCycle <- currentCycle, phase <- phase, churnStage <- churnStage, continuationBoundary <- continuationBoundary, continuationAnchorPublished <- continuationAnchorPublished, continuationAnchorBoundary <- continuationAnchorBoundary, continuationPagePublished <- continuationPagePublished, continuationPageBoundary <- continuationPageBoundary, continuationFetched <- continuationFetched, shareReceipts <- shareReceipts, shareConflicts <- shareConflicts, windowClosed <- windowClosed, missingShareClaims <- missingShareClaims, missingThresholdCertificates <- missingThresholdCertificates, recovered <- recovered, recoveredSurfaces <- recoveredSurfaces, recoveryConflicts <- recoveryConflicts, aborted <- aborted
76 77
CycleRange == 1..TotalCycles
78 79 80 81 82 83
ClassicalAgreementDecisionObject(c) == [cycle |-> c, slot |-> TargetSlotOf(c), block |-> TargetBlockOf(c), epoch |-> StableEpochOf(c)]
84 85 86
ClassicalAgreementPrefixObject(c) == [i \in 1..c |-> ClassicalAgreementDecisionObject(i)]
87 88 89 90
FiniteClassicalAgreementPrefixRealized(c) == /\ c \in CycleRange /\ <>Proof!Core!RecoveryClosedPrefix(c)
91 92 93 94
FiniteClassicalAgreementLiveness == \A c \in CycleRange : FiniteClassicalAgreementPrefixRealized(c)
95 96 97 98
ClassicalAgreementFiniteReduction == Proof!RecoveryRecurringClosedPrefixes => FiniteClassicalAgreementLiveness
99 100 101 102
THEOREM ProofCycleRangeMatchesCycleRange == Proof!Core!CycleRange = CycleRange BY DEF Proof!Core!CycleRange, Proof!Core!Core!CycleRange, CycleRange
103 104 105 106 107 108 109 110 111 112 113 114 115 116
THEOREM FiniteClassicalAgreementPrefixFromRecurringPrefixes == \A c \in CycleRange : Proof!RecoveryRecurringClosedPrefixes => FiniteClassicalAgreementPrefixRealized(c) PROOF <1>1. TAKE c \in CycleRange <1>2. ASSUME Proof!RecoveryRecurringClosedPrefixes PROVE FiniteClassicalAgreementPrefixRealized(c) <2>1. c \in Proof!Core!CycleRange BY ProofCycleRangeMatchesCycleRange, <1>1 <2>2. <>Proof!Core!RecoveryClosedPrefix(c) BY <1>2, <2>1 DEF Proof!RecoveryRecurringClosedPrefixes <2>3. QED
86
117 118 119
BY <1>1, <2>2 DEF FiniteClassicalAgreementPrefixRealized <1>3. QED BY <1>2
120 121 122 123 124 125
THEOREM ClassicalAgreementFiniteReductionTheorem == ClassicalAgreementFiniteReduction BY FiniteClassicalAgreementPrefixFromRecurringPrefixes DEF ClassicalAgreementFiniteReduction, FiniteClassicalAgreementLiveness
126 127
====
A.6.4
NestedGuardianRecoveryClassicalAgreementTotality.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardianRecoveryClassicalAgreementTotality.tla}
1 2
---- MODULE NestedGuardianRecoveryClassicalAgreementTotality ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4 5 6 7 8
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialEpoch, InitialWitness, TotalCycles, TargetSlotOf(), TargetBlockOf(), StableEpochOf(_), SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold, SmallRecoveryCommittee, LargeRecoveryCommittee
9 10 11 12 13 14 15 16 17 18 19
ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses ASSUME QuorumSizeInValidatorRange == QuorumSize \in 1..Cardinality(Validators) ASSUME TotalCyclesIsNat == TotalCycles \in Nat ASSUME TotalCyclesAtLeastOne == TotalCycles >= 1 ASSUME TargetCycleDomains == \A c \in 1..TotalCycles : /\ TargetSlotOf(c) \in Slots /\ TargetBlockOf(c) \in Blocks /\ StableEpochOf(c) \in Epochs
20 21
22 23 24 25 26 27
VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage, continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary, continuationPagePublished, continuationPageBoundary, continuationFetched, shareReceipts, shareConflicts, windowClosed, missingShareClaims, missingThresholdCertificates, recovered, recoveredSurfaces, recoveryConflicts, aborted
28 29 30 31 32 33 34 35 36 37 38 39 40 41
Reduction == INSTANCE NestedGuardianRecoveryClassicalAgreementReduction WITH Validators <- Validators, Witnesses <- Witnesses, Blocks <- Blocks, Slots <- Slots, Epochs <- Epochs, QuorumSize <- QuorumSize, MaxReassignmentDepth <- MaxReassignmentDepth, InitialEpoch <- InitialEpoch, InitialWitness <- InitialWitness, TotalCycles <- TotalCycles, TargetSlotOf <- TargetSlotOf,
87
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
TargetBlockOf <- TargetBlockOf, StableEpochOf <- StableEpochOf, SmallCommitteeSlot <- SmallCommitteeSlot, SmallRecoveryThreshold <- SmallRecoveryThreshold, LargeRecoveryThreshold <- LargeRecoveryThreshold, SmallRecoveryCommittee <- SmallRecoveryCommittee, LargeRecoveryCommittee <- LargeRecoveryCommittee, votes <- votes, witnessCerts <- witnessCerts, finalized <- finalized, finalizerSets <- finalizerSets, registryEpoch <- registryEpoch, guardianReady <- guardianReady, witnessOnline <- witnessOnline, witnessCheckpoint <- witnessCheckpoint, assignedWitness <- assignedWitness, reassignmentDepth <- reassignmentDepth, currentCycle <- currentCycle, phase <- phase, churnStage <- churnStage, continuationBoundary <- continuationBoundary, continuationAnchorPublished <- continuationAnchorPublished, continuationAnchorBoundary <- continuationAnchorBoundary, continuationPagePublished <- continuationPagePublished, continuationPageBoundary <- continuationPageBoundary, continuationFetched <- continuationFetched, shareReceipts <- shareReceipts, shareConflicts <- shareConflicts, windowClosed <- windowClosed, missingShareClaims <- missingShareClaims, missingThresholdCertificates <- missingThresholdCertificates, recovered <- recovered, recoveredSurfaces <- recoveredSurfaces, recoveryConflicts <- recoveryConflicts, aborted <- aborted
77 78
CycleRange == 1..TotalCycles
79 80 81 82 83
RecoveryRecurringClosedPrefixes == Reduction!Proof!RecoveryRecurringClosedPrefixes RecoveryRecurringInductionPremises == Reduction!Proof!Core!RecoveryRecurringInductionPremises RecoveryRecurringInductionKernel == Reduction!Proof!Core!RecoveryRecurringInductionKernel RecoveryClosedPrefix(c) == Reduction!Proof!Core!RecoveryClosedPrefix(c)
84 85 86
ClassicalAgreementTotalHistoryObject == [i \in CycleRange |-> Reduction!ClassicalAgreementDecisionObject(i)]
87 88 89 90 91
ClassicalAgreementTotalHistoryExtendsFinitePrefixes == \A c \in CycleRange : [i \in 1..c |-> ClassicalAgreementTotalHistoryObject[i]] = Reduction!ClassicalAgreementPrefixObject(c)
92 93 94 95
TotalClassicalAgreementHistoryRealized == /\ <>RecoveryClosedPrefix(TotalCycles) /\ ClassicalAgreementTotalHistoryExtendsFinitePrefixes
96 97 98 99
TotalClassicalAgreementReduction == Reduction!FiniteClassicalAgreementLiveness => TotalClassicalAgreementHistoryRealized
100 101 102 103
TotalClassicalAgreementFromRecurringPrefixes == RecoveryRecurringClosedPrefixes => TotalClassicalAgreementHistoryRealized
88
104 105 106 107 108
TotalClassicalAgreementFromRecurrenceKernel == /\ RecoveryRecurringInductionPremises /\ RecoveryRecurringInductionKernel => TotalClassicalAgreementHistoryRealized
109 110 111 112 113 114 115 116
THEOREM TotalHistoryEntryMatchesDecisionObject == \A c \in CycleRange : \A i \in 1..c : ClassicalAgreementTotalHistoryObject[i] = Reduction!ClassicalAgreementDecisionObject(i) BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF CycleRange, ClassicalAgreementTotalHistoryObject
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
THEOREM ClassicalAgreementTotalHistoryExtendsFinitePrefixesTheorem == ClassicalAgreementTotalHistoryExtendsFinitePrefixes PROOF <1>1. \A c \in CycleRange : [i \in 1..c |-> ClassicalAgreementTotalHistoryObject[i]] = Reduction!ClassicalAgreementPrefixObject(c) PROOF <2>1. TAKE c \in CycleRange <2>2. \A i \in 1..c : ClassicalAgreementTotalHistoryObject[i] = Reduction!ClassicalAgreementDecisionObject(i) BY TotalHistoryEntryMatchesDecisionObject, <2>1 <2>3. QED BY IsaWithSetExtensionality, <2>1, <2>2 DEF Reduction!ClassicalAgreementPrefixObject <1>2. QED BY <1>1 DEF ClassicalAgreementTotalHistoryExtendsFinitePrefixes
135 136 137 138
THEOREM TotalCyclesInCycleRange == TotalCycles \in CycleRange BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF CycleRange
139 140 141 142 143 144 145 146 147 148 149 150 151
THEOREM TotalFinitePrefixFromFiniteLiveness == Reduction!FiniteClassicalAgreementLiveness => Reduction!FiniteClassicalAgreementPrefixRealized(TotalCycles) PROOF <1>1. ASSUME Reduction!FiniteClassicalAgreementLiveness PROVE Reduction!FiniteClassicalAgreementPrefixRealized(TotalCycles) <2>1. TotalCycles \in Reduction!CycleRange BY TotalCyclesInCycleRange DEF CycleRange, Reduction!CycleRange <2>2. QED BY <1>1, <2>1 DEF Reduction!FiniteClassicalAgreementLiveness <1>2. QED BY <1>1
152 153 154 155 156 157 158
THEOREM TotalRecoveryClosedPrefixFromFiniteLiveness == Reduction!FiniteClassicalAgreementLiveness => <>RecoveryClosedPrefix(TotalCycles) BY TotalFinitePrefixFromFiniteLiveness DEF Reduction!FiniteClassicalAgreementPrefixRealized, RecoveryClosedPrefix
159 160 161 162 163 164 165
THEOREM TotalClassicalAgreementReductionTheorem == TotalClassicalAgreementReduction BY TotalRecoveryClosedPrefixFromFiniteLiveness, ClassicalAgreementTotalHistoryExtendsFinitePrefixesTheorem DEF TotalClassicalAgreementReduction, TotalClassicalAgreementHistoryRealized
89
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
THEOREM ReductionLivenessFromRecurringPrefixes == RecoveryRecurringClosedPrefixes => Reduction!FiniteClassicalAgreementLiveness PROOF <1>1. ASSUME RecoveryRecurringClosedPrefixes PROVE Reduction!FiniteClassicalAgreementLiveness <2>1. \A c \in Reduction!CycleRange : Reduction!FiniteClassicalAgreementPrefixRealized(c) PROOF <3>1. TAKE c \in Reduction!CycleRange <3>2. c \in Reduction!Proof!Core!CycleRange BY <3>1 DEF Reduction!CycleRange, Reduction!Proof!Core!CycleRange, Reduction!Proof!Core!Core!CycleRange <3>3. Reduction!Proof!RecoveryRecurringClosedPrefixes BY <1>1 DEF RecoveryRecurringClosedPrefixes <3>4. <>Reduction!Proof!Core!RecoveryClosedPrefix(c) BY <3>2, <3>3 DEF Reduction!Proof!RecoveryRecurringClosedPrefixes <3>5. QED BY <3>1, <3>4 DEF Reduction!FiniteClassicalAgreementPrefixRealized <2>2. QED BY <2>1 DEF Reduction!FiniteClassicalAgreementLiveness <1>2. QED BY <1>1
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
THEOREM TotalClassicalAgreementFromRecurringPrefixesTheorem == TotalClassicalAgreementFromRecurringPrefixes PROOF <1>1. ASSUME RecoveryRecurringClosedPrefixes PROVE TotalClassicalAgreementHistoryRealized <2>1. Reduction!FiniteClassicalAgreementLiveness BY ReductionLivenessFromRecurringPrefixes, <1>1 <2>2. Reduction!FiniteClassicalAgreementLiveness => TotalClassicalAgreementHistoryRealized BY TotalClassicalAgreementReductionTheorem DEF TotalClassicalAgreementReduction <2>3. QED BY <2>1, <2>2 <1>2. QED BY <1>1 DEF TotalClassicalAgreementFromRecurringPrefixes
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
THEOREM RecoveryRecurringClosedPrefixesFromRecurrenceKernel == /\ RecoveryRecurringInductionPremises /\ RecoveryRecurringInductionKernel => RecoveryRecurringClosedPrefixes PROOF <1>1. ASSUME RecoveryRecurringInductionPremises, RecoveryRecurringInductionKernel PROVE RecoveryRecurringClosedPrefixes <2>1. \A c \in Reduction!Proof!Core!CycleRange : <>Reduction!Proof!Core!RecoveryClosedPrefix(c) PROOF <3>1. TAKE c \in Reduction!Proof!Core!CycleRange <3>2. Reduction!Proof!Core!RecoveryInductionPremisesUpTo(c) PROOF <4>1. Reduction!Proof!Core!RecoveryInductionBase BY <1>1 DEF RecoveryRecurringInductionPremises, Reduction!Proof!Core!RecoveryRecurringInductionPremises <4>2. \A i \in Reduction!Proof!Core!PriorCycleRange(c) :
90
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
Reduction!Proof!Core!RecoveryInductionStep(i) PROOF <5>1. TAKE i \in Reduction!Proof!Core!PriorCycleRange(c) <5>2. TotalCycles # 1 BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne, <3>1, <5>1 DEF Reduction!Proof!Core!CycleRange, Reduction!Proof!Core!Core!CycleRange, Reduction!Proof!Core!PriorCycleRange <5>3. i \in 1..(TotalCycles - 1) BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne, <3>1, <5>1 DEF Reduction!Proof!Core!CycleRange, Reduction!Proof!Core!Core!CycleRange, Reduction!Proof!Core!PriorCycleRange <5>4. i \in Reduction!Proof!Core!PrefixAdvanceRange BY <5>2, <5>3 DEF Reduction!Proof!Core!PrefixAdvanceRange, Reduction!Proof!Core!Core!PrefixAdvanceRange <5>5. QED BY <1>1, <5>4 DEF RecoveryRecurringInductionPremises, Reduction!Proof!Core!RecoveryRecurringInductionPremises <4>3. QED BY <3>1, <4>1, <4>2 DEF Reduction!Proof!Core!RecoveryInductionPremisesUpTo <3>3. Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel(c) BY <1>1, <3>1 DEF RecoveryRecurringInductionKernel, Reduction!Proof!Core!RecoveryRecurringInductionKernel <3>4. QED BY <3>2, <3>3 DEF Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel <2>2. QED BY <2>1 DEF RecoveryRecurringClosedPrefixes, Reduction!Proof!RecoveryRecurringClosedPrefixes <1>2. QED BY <1>1 DEF RecoveryRecurringClosedPrefixes, RecoveryRecurringInductionPremises, RecoveryRecurringInductionKernel, Reduction!Proof!RecoveryRecurringClosedPrefixes
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
THEOREM TotalClassicalAgreementFromRecurrenceKernelTheorem == TotalClassicalAgreementFromRecurrenceKernel PROOF <1>1. ASSUME RecoveryRecurringInductionPremises, RecoveryRecurringInductionKernel PROVE TotalClassicalAgreementHistoryRealized <2>1. RecoveryRecurringClosedPrefixes BY RecoveryRecurringClosedPrefixesFromRecurrenceKernel, <1>1 <2>2. TotalClassicalAgreementFromRecurringPrefixes BY TotalClassicalAgreementFromRecurringPrefixesTheorem <2>3. QED BY <2>1, <2>2 DEF TotalClassicalAgreementFromRecurringPrefixes <1>2. QED BY <1>1 DEF TotalClassicalAgreementFromRecurrenceKernel
283 284
====
91
A.6.5
NestedGuardianRecoveryClassicalAgreementCollapse.tla
Repository path. \detokenize{internal-docs/architecture/protocols/aft/formal/ne sted_guardian/NestedGuardianRecoveryClassicalAgreementCollapse.tla}
1 2
---- MODULE NestedGuardianRecoveryClassicalAgreementCollapse ---EXTENDS Naturals, FiniteSets, TLC, TLAPS
3 4 5 6 7 8
CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth, InitialEpoch, InitialWitness, TotalCycles, TargetSlotOf(), TargetBlockOf(), StableEpochOf(_), SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold, SmallRecoveryCommittee, LargeRecoveryCommittee
9 10 11 12 13 14 15 16 17 18 19
ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses ASSUME QuorumSizeInValidatorRange == QuorumSize \in 1..Cardinality(Validators) ASSUME TotalCyclesIsNat == TotalCycles \in Nat ASSUME TotalCyclesAtLeastOne == TotalCycles >= 1 ASSUME TargetCycleDomains == \A c \in 1..TotalCycles : /\ TargetSlotOf(c) \in Slots /\ TargetBlockOf(c) \in Blocks /\ StableEpochOf(c) \in Epochs
20 21
22 23 24 25 26 27
VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, ,→ witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage, continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary, continuationPagePublished, continuationPageBoundary, continuationFetched, shareReceipts, shareConflicts, windowClosed, missingShareClaims, missingThresholdCertificates, recovered, recoveredSurfaces, recoveryConflicts, aborted
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
Totality == INSTANCE NestedGuardianRecoveryClassicalAgreementTotality WITH Validators <- Validators, Witnesses <- Witnesses, Blocks <- Blocks, Slots <- Slots, Epochs <- Epochs, QuorumSize <- QuorumSize, MaxReassignmentDepth <- MaxReassignmentDepth, InitialEpoch <- InitialEpoch, InitialWitness <- InitialWitness, TotalCycles <- TotalCycles, TargetSlotOf <- TargetSlotOf, TargetBlockOf <- TargetBlockOf, StableEpochOf <- StableEpochOf, SmallCommitteeSlot <- SmallCommitteeSlot, SmallRecoveryThreshold <- SmallRecoveryThreshold, LargeRecoveryThreshold <- LargeRecoveryThreshold, SmallRecoveryCommittee <- SmallRecoveryCommittee, LargeRecoveryCommittee <- LargeRecoveryCommittee, votes <- votes, witnessCerts <- witnessCerts, finalized <- finalized, finalizerSets <- finalizerSets, registryEpoch <- registryEpoch, guardianReady <- guardianReady,
92
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
witnessOnline <- witnessOnline, witnessCheckpoint <- witnessCheckpoint, assignedWitness <- assignedWitness, reassignmentDepth <- reassignmentDepth, currentCycle <- currentCycle, phase <- phase, churnStage <- churnStage, continuationBoundary <- continuationBoundary, continuationAnchorPublished <- continuationAnchorPublished, continuationAnchorBoundary <- continuationAnchorBoundary, continuationPagePublished <- continuationPagePublished, continuationPageBoundary <- continuationPageBoundary, continuationFetched <- continuationFetched, shareReceipts <- shareReceipts, shareConflicts <- shareConflicts, windowClosed <- windowClosed, missingShareClaims <- missingShareClaims, missingThresholdCertificates <- missingThresholdCertificates, recovered <- recovered, recoveredSurfaces <- recoveredSurfaces, recoveryConflicts <- recoveryConflicts, aborted <- aborted
77 78
CycleRange == Totality!CycleRange
79 80 81 82 83 84
ClassicalAgreementDecision(c) == [cycle |-> c, slot |-> TargetSlotOf(c), block |-> TargetBlockOf(c), epoch |-> StableEpochOf(c)]
85 86 87 88
ClassicalAgreementHistory(history) == \A i \in CycleRange : history[i] = ClassicalAgreementDecision(i)
89 90 91 92
OrdinaryClassicalAgreementHistory(history) == /\ ClassicalAgreementHistory(history) /\ <>Totality!RecoveryClosedPrefix(TotalCycles)
93 94 95 96 97
UnconditionalClassicalAgreementSentence == OrdinaryClassicalAgreementHistory( Totality!ClassicalAgreementTotalHistoryObject )
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
THEOREM TotalHistoryMatchesCollapsedClassicalHistory == ClassicalAgreementHistory(Totality!ClassicalAgreementTotalHistoryObject) PROOF <1>1. \A i \in CycleRange : Totality!ClassicalAgreementTotalHistoryObject[i] = ClassicalAgreementDecision(i) PROOF <2>1. TAKE i \in CycleRange <2>2. QED BY <2>1 DEF ClassicalAgreementDecision, CycleRange, Totality!ClassicalAgreementTotalHistoryObject, Totality!Reduction!ClassicalAgreementDecisionObject <1>2. QED BY <1>1 DEF ClassicalAgreementHistory
115 116
THEOREM TotalityCyclePrefixEntriesStayInCycleRange ==
93
117 118 119 120 121
\A c \in Totality!CycleRange : \A i \in 1..c : i \in Totality!CycleRange BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF Totality!CycleRange
122 123 124 125 126 127 128 129 130 131 132
THEOREM TotalityReductionCorePriorCycleRangeImpliesPrefixAdvanceRange == \A c \in Totality!Reduction!Proof!Core!CycleRange : \A i \in Totality!Reduction!Proof!Core!PriorCycleRange(c) : i \in Totality!Reduction!Proof!Core!PrefixAdvanceRange BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF Totality!Reduction!Proof!Core!CycleRange, Totality!Reduction!Proof!Core!Core!CycleRange, Totality!Reduction!Proof!Core!PriorCycleRange, Totality!Reduction!Proof!Core!PrefixAdvanceRange, Totality!Reduction!Proof!Core!Core!PrefixAdvanceRange
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
THEOREM LocalReductionLivenessFromRecurringPrefixesTheorem == Totality!RecoveryRecurringClosedPrefixes => Totality!Reduction!FiniteClassicalAgreementLiveness PROOF <1>1. ASSUME Totality!RecoveryRecurringClosedPrefixes PROVE Totality!Reduction!FiniteClassicalAgreementLiveness <2>1. \A c \in Totality!Reduction!CycleRange : Totality!Reduction!FiniteClassicalAgreementPrefixRealized(c) PROOF <3>1. TAKE c \in Totality!Reduction!CycleRange <3>2. c \in Totality!Reduction!Proof!Core!CycleRange BY <3>1 DEF Totality!Reduction!CycleRange, Totality!Reduction!Proof!Core!CycleRange, Totality!Reduction!Proof!Core!Core!CycleRange <3>3. <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c) BY <1>1, <3>2 DEF Totality!RecoveryRecurringClosedPrefixes, Totality!Reduction!Proof!RecoveryRecurringClosedPrefixes <3>4. QED BY <3>1, <3>3 DEF Totality!Reduction!FiniteClassicalAgreementPrefixRealized <2>2. QED BY <2>1 DEF Totality!Reduction!FiniteClassicalAgreementLiveness <1>2. QED BY <1>1
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
THEOREM LocalTotalClassicalAgreementHistoryFromFiniteLivenessTheorem == Totality!Reduction!FiniteClassicalAgreementLiveness => Totality!TotalClassicalAgreementHistoryRealized PROOF <1>1. ASSUME Totality!Reduction!FiniteClassicalAgreementLiveness PROVE Totality!TotalClassicalAgreementHistoryRealized <2>1. TotalCycles \in Totality!Reduction!CycleRange BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF Totality!Reduction!CycleRange <2>2. Totality!Reduction!FiniteClassicalAgreementPrefixRealized(TotalCycles) BY <1>1, <2>1 DEF Totality!Reduction!FiniteClassicalAgreementLiveness <2>3. <>Totality!RecoveryClosedPrefix(TotalCycles) BY <2>2 DEF Totality!Reduction!FiniteClassicalAgreementPrefixRealized, Totality!RecoveryClosedPrefix <2>4. Totality!ClassicalAgreementTotalHistoryExtendsFinitePrefixes PROOF <3>1. \A c \in Totality!CycleRange :
94
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
[i \in 1..c |-> Totality!ClassicalAgreementTotalHistoryObject[i]] = Totality!Reduction!ClassicalAgreementPrefixObject(c)
PROOF <4>1. TAKE c \in Totality!CycleRange <4>2. \A i \in 1..c : Totality!ClassicalAgreementTotalHistoryObject[i] = Totality!Reduction!ClassicalAgreementDecisionObject(i) PROOF <5>1. TAKE i \in 1..c <5>2. c \in 1..TotalCycles BY <4>1 DEF Totality!CycleRange <5>3. i \in Totality!CycleRange BY TotalityCyclePrefixEntriesStayInCycleRange, <4>1, <5>1 <5>4. QED BY <5>3 DEF Totality!ClassicalAgreementTotalHistoryObject <4>3. QED BY IsaWithSetExtensionality, <4>1, <4>2 DEF Totality!Reduction!ClassicalAgreementPrefixObject <3>2. QED BY <3>1 DEF Totality!ClassicalAgreementTotalHistoryExtendsFinitePrefixes <2>5. QED BY <2>3, <2>4 DEF Totality!TotalClassicalAgreementHistoryRealized <1>2. QED BY <1>1
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
THEOREM LocalRecurringPrefixesFromRecurrenceKernelTheorem == /\ Totality!RecoveryRecurringInductionPremises /\ Totality!RecoveryRecurringInductionKernel => Totality!RecoveryRecurringClosedPrefixes PROOF <1>1. ASSUME Totality!RecoveryRecurringInductionPremises, Totality!RecoveryRecurringInductionKernel PROVE Totality!RecoveryRecurringClosedPrefixes <2>1. \A c \in Totality!Reduction!Proof!Core!CycleRange : <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c) PROOF <3>1. TAKE c \in Totality!Reduction!Proof!Core!CycleRange <3>2. /\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises /\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionKernel BY <1>1 DEF Totality!RecoveryRecurringInductionPremises, Totality!RecoveryRecurringInductionKernel <3>3. Totality!Reduction!Proof!Core!RecoveryInductionPremisesUpTo(c) PROOF <4>1. Totality!Reduction!Proof!Core!RecoveryInductionBase BY <3>2 DEF Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises <4>2. \A i \in Totality!Reduction!Proof!Core!PriorCycleRange(c) : Totality!Reduction!Proof!Core!RecoveryInductionStep(i) PROOF <5>1. TAKE i \in Totality!Reduction!Proof!Core!PriorCycleRange(c) <5>2. i \in Totality!Reduction!Proof!Core!PrefixAdvanceRange BY TotalityReductionCorePriorCycleRangeImpliesPrefixAdvanceRange, <3>1, <5>1 <5>3. QED BY <3>2, <5>2 DEF Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises <4>3. QED BY <3>1, <4>1, <4>2 DEF Totality!Reduction!Proof!Core!RecoveryInductionPremisesUpTo <3>4. Totality!Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel(c)
95
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
BY <3>1, <3>2 DEF Totality!Reduction!Proof!Core!RecoveryRecurringInductionKernel <3>5. <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c) BY <3>3, <3>4 DEF Totality!Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel <3>6. (/\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises /\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionKernel) => <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c) BY <3>5 <3>7. QED BY <3>5 <2>2. QED BY <2>1 DEF Totality!RecoveryRecurringClosedPrefixes, Totality!Reduction!Proof!RecoveryRecurringClosedPrefixes <1>2. QED BY <1>1
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
THEOREM UnconditionalClassicalAgreementFromTotalHistoryTheorem == Totality!TotalClassicalAgreementHistoryRealized => UnconditionalClassicalAgreementSentence PROOF <1>1. ASSUME Totality!TotalClassicalAgreementHistoryRealized PROVE UnconditionalClassicalAgreementSentence <2>1. ClassicalAgreementHistory(Totality!ClassicalAgreementTotalHistoryObject) BY TotalHistoryMatchesCollapsedClassicalHistory <2>2. <>Totality!RecoveryClosedPrefix(TotalCycles) BY <1>1 DEF Totality!TotalClassicalAgreementHistoryRealized <2>3. QED BY <2>1, <2>2 DEF UnconditionalClassicalAgreementSentence, OrdinaryClassicalAgreementHistory <1>2. QED BY <1>1
275 276 277 278 279 280 281 282 283 284 285 286 287 288 289
THEOREM UnconditionalClassicalAgreementFromRecurringPrefixesTheorem == Totality!RecoveryRecurringClosedPrefixes => UnconditionalClassicalAgreementSentence PROOF <1>1. ASSUME Totality!RecoveryRecurringClosedPrefixes PROVE UnconditionalClassicalAgreementSentence <2>1. Totality!Reduction!FiniteClassicalAgreementLiveness BY LocalReductionLivenessFromRecurringPrefixesTheorem, <1>1 <2>2. Totality!TotalClassicalAgreementHistoryRealized BY LocalTotalClassicalAgreementHistoryFromFiniteLivenessTheorem, <2>1 <2>3. QED BY UnconditionalClassicalAgreementFromTotalHistoryTheorem, <2>2 <1>2. QED BY <1>1
290 291 292 293 294 295 296 297 298 299 300 301 302
THEOREM UnconditionalClassicalAgreementFromRecurrenceKernelTheorem == /\ Totality!RecoveryRecurringInductionPremises /\ Totality!RecoveryRecurringInductionKernel => UnconditionalClassicalAgreementSentence PROOF <1>1. ASSUME Totality!RecoveryRecurringInductionPremises, Totality!RecoveryRecurringInductionKernel PROVE UnconditionalClassicalAgreementSentence <2>1. Totality!RecoveryRecurringClosedPrefixes BY LocalRecurringPrefixesFromRecurrenceKernelTheorem, <1>1 <2>2. Totality!Reduction!FiniteClassicalAgreementLiveness BY LocalReductionLivenessFromRecurringPrefixesTheorem, <2>1
96
303 304 305 306 307 308
<2>3. Totality!TotalClassicalAgreementHistoryRealized BY LocalTotalClassicalAgreementHistoryFromFiniteLivenessTheorem, <2>2 <2>4. QED BY UnconditionalClassicalAgreementFromTotalHistoryTheorem, <2>3 <1>3. QED BY <1>1
309 310
====
References [1] Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan-Gueta, and Ittai Abraham. HotStuff: BFT Consensus in the Lens of Blockchain. arXiv:1803.05069. https://arxiv.org/abs/1803 .05069 [2] George Danezis, Lefteris Kokoris-Kogias, Alberto Sonnino, and Alexander Spiegelman. Narwhal and Tusk: A DAG-based Mempool and Efficient BFT Consensus. arXiv:2105.11827. https: //arxiv.org/abs/2105.11827 [3] Ittai Abraham, Dahlia Malkhi, Kartik Nayak, Ling Ren, and Alexander Spiegelman. Bullshark: DAG BFT Protocols Made Practical. arXiv:2201.05677. https://arxiv.org/abs/2201.05677 [4] Andrew Miller, Yu Xia, Kyle Croman, Elaine Shi, and Dawn Song. The Honey Badger of BFT Protocols. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. https://eprint.iacr.org/2016/199.pdf [5] Bingyong Guo, Zhenliang Lu, Qiang Tang, Jing Xu, and Zhenfeng Zhang. Dumbo: Faster Asynchronous BFT Protocols. Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. https://dblp.org/rec/conf/ccs/GuoL0XZ20 [6] Alistair Stewart and Eleftherios Kokoris-Kogias. GRANDPA: a Byzantine Finality Gadget. arXiv:2007.01560. https://arxiv.org/abs/2007.01560 [7] Jelena Dosenovic, Roger Wattenhofer, and others. Accountable Safety Implies Finality. arXiv:2308.16902. https://arxiv.org/abs/2308.16902 [8] Chainlink Labs. Chainlink CCIP’s Defense-In-Depth Security and the Risk Management Network. Chainlink blog, 2023. https://blog.chain.link/ccip-risk-management-netwo rk/ [9] John P. Conley. Proof of Honesty: Coalition-Proof Blockchain Validation without Proof of Work or Stake. Geeq technical paper, version 2.0, 2019. https://geeq.io/wp-content/upl oads/GEEQ-OFFICIAL-TECHNICAL-PAPER.pdf [10] Sean Bowe, Jack Grigg, and Daira Hopwood. Halo: Recursive Proof Composition without a Trusted Setup. IACR ePrint 2019/1021. https://eprint.iacr.org/2019/1021 [11] Benedikt Bünz, Alessandro Chiesa, Pratyush Mishra, and Nicholas Spooner. Proof-Carrying Data from Accumulation Schemes. IACR ePrint 2020/499. https://eprint.iacr.org/2020 /499
97