diff --git a/.github/workflows/zeronym-guards.yml b/.github/workflows/zeronym-guards.yml
index 200c33db..d46c2547 100644
--- a/.github/workflows/zeronym-guards.yml
+++ b/.github/workflows/zeronym-guards.yml
@@ -40,6 +40,51 @@ jobs:
- name: Repository claim guards
run: sh zeronym/guards.sh
+ # The Quint specification of the protocol: typecheck, tests
+ # and bounded random simulation. About 2 minutes on a 16-core machine.
+ spec-protocol:
+ runs-on: ubuntu-latest
+ timeout-minutes: 15
+ # It runs code fetched at run time (npx, Quint's evaluator), so it gets a
+ # read-only token and a pinned checkout.
+ permissions:
+ contents: read
+ steps:
+ - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+ with:
+ persist-credentials: false
+ - name: Protocol specification, tiers 1 to 3b
+ run: sh zeronym/spec/quint/check.sh
+ env:
+ CHECK_TIERS: simulation
+
+ # The hub specification checked exhaustively with TLC, which needs Java. The
+ # Apalache distribution that carries TLC is fetched by Quint on first use.
+ # About 8.5 minutes on a 16-core machine with four rows at a time. Rows that
+ # expect a violation run TLC on one worker, so the trace lengths are
+ # shortest; two rows at a time with 6 GB each fit a 4-core, 16 GB runner.
+ spec-protocol-tlc:
+ runs-on: ubuntu-latest
+ timeout-minutes: 45
+ # Same reasoning as `spec-protocol`: it runs code fetched at run time.
+ permissions:
+ contents: read
+ steps:
+ - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+ with:
+ persist-credentials: false
+ - uses: actions/setup-java@de7274f081f381c8f8158605e0321c36c376e2e6 # v6.0.1
+ with:
+ distribution: temurin
+ java-version: '21'
+ - name: Hub specification, tier 4
+ run: sh zeronym/spec/quint/check.sh
+ env:
+ CHECK_TIERS: tlc
+ QUINT_JOBS: '2'
+ TLC_HEAP: 6g
+ TLC_TIMEOUT: '900'
+
tests:
runs-on: blacksmith-8vcpu-ubuntu-2404
timeout-minutes: 30
diff --git a/zeronym/spec/.gitignore b/zeronym/spec/.gitignore
new file mode 100644
index 00000000..a4074725
--- /dev/null
+++ b/zeronym/spec/.gitignore
@@ -0,0 +1 @@
+_apalache-out/
diff --git a/zeronym/spec/quint/.gitignore b/zeronym/spec/quint/.gitignore
new file mode 100644
index 00000000..4eba4666
--- /dev/null
+++ b/zeronym/spec/quint/.gitignore
@@ -0,0 +1,2 @@
+*.itf.json
+_apalache-out/
diff --git a/zeronym/spec/quint/README.md b/zeronym/spec/quint/README.md
new file mode 100644
index 00000000..73fb34b2
--- /dev/null
+++ b/zeronym/spec/quint/README.md
@@ -0,0 +1,447 @@
+# The zeronym protocol, specified in Quint
+
+A [Quint](https://quint-lang.org) specification of zeronym: the protocol between a wallet, the shim in front of an operator's indexer, the hub that batches diverted transactions, and the chain.
+
+- [System](#system)
+- [Assumptions](#assumptions)
+- [Threat model](#threat-model)
+- [Guarantees](#guarantees)
+- [Trust matrix](#trust-matrix)
+- [Known gaps](#known-gaps)
+- [Out of scope](#out-of-scope)
+- [Findings](#findings)
+- [How it is checked](#how-it-is-checked)
+- [Future work](#future-work)
+
+## System
+
+> Who the actors are, what each one does, and where each lives in the specification.
+
+The architecture diagram and the prose description of the deployment are in [`zeronym/README.md`](../../README.md).
+
+Only the mixnet transport is modelled; the HTTP transport is out of scope (see [Out of scope](#out-of-scope)).
+
+There are two specifications, sharing one hub function:
+
+- **The protocol specification** (`protocol.qnt`): wallet, shim, network, hub, indexer and an outside third party. Its hub is abstract: a queue and the entries out with a flush, with no tip, schedule or phases. It is checked by random simulation and scripted runs.
+- **The hub specification** (`hubMachine.qnt`): one hub, the chain, and the two things the hub asks its indexer (the tip, and a verdict on each broadcast). It owns the schedule, expiry, requeue, crash and drain. TLC visits every reachable state of each of its configurations.
+
+Each component is one total function from its state and one input to its next state and one output. An input that is invalid in the current state returns an error output and leaves the state alone. The state machines hold no protocol logic: a step picks an input, calls the function, and puts the output where it goes. `hub.qnt` and `shim.qnt` are the precise statement of what each does.
+
+| Component | Inputs | Outputs | Seam in the implementation |
+|---|---|---|---|
+| `hub` | `SubmitHInput`, `LookupHInput` (with the indexer's answer), `TipHInput(height)`, `StaleHInput(estimate)`, `FlushDueHInput`, `VerdictHInput`, `FlushDoneHInput`, `DrainHInput`, `CrashHInput`, `RestartHInput` | `AckOutput`, `LookupReplyOutput`, `BroadcastOutput`, `RequeuedOutput`, `NoHubOutput`, `HubErrorOutput` | `Hub::admit`, `Hub::lookup` (`hub/src/server.rs`), `run_listener` (`hub/src/nym.rs`), `TipTracker::observe`, `cadence_height`, `flush` (`hub/src/batcher.rs`), `Queue::requeue`, `Queue::begin_draining` (`hub/src/queue.rs`) |
+| `shim` | `SendTxSInput` (with whether the transport took the frame), `GetTxSInput`, `FrameSInput`, `LookupTimeoutSInput` | `ForwardOutput`, `DivertedOutput`, `SendDoneOutput`, `LookupSentOutput`, `LookupDoneOutput`, `NoShimOutput`, `ShimErrorOutput` | `send_transaction`, `divert`, `get_transaction` (`shim/src/intercept.rs`), `NymHandle::submit`, `get_transaction`, `deliver` (`shim/src/nym.rs`) |
+| indexer | `BroadcastIInput`, `LookupIInput`, `AdvanceIInput`, `MineIInput` | `VerdictOutput`, `AnswerOutput`, `NoIndexerOutput` | the mock indexer in `hub/tests/common/mod.rs` |
+
+
+Shim: routing a send, and one lookup
+
+Routing one `SendTransaction` (`shim.qnt`):
+
+```mermaid
+stateDiagram-v2
+ [*] --> Inspect
+ Inspect --> Forwarded: Clean and class PassThrough
+ Inspect --> FailClosed: Unreadable or EmptyBody
+ Inspect --> Framing: Clean and class OrchardTouching or Unparseable
+ Framing --> FailClosed: oversize
+ Framing --> Dispatched: one frame to the hub, fresh nonce
+ Framing --> FailClosed: no frame handed over
+ Dispatched --> ToldOk
+ Forwarded --> [*]
+ ToldOk --> [*]
+ FailClosed --> [*]
+```
+
+One `GetTransaction` lookup:
+
+```mermaid
+stateDiagram-v2
+ [*] --> Awaiting: send Lookup to the hub, fresh nonce
+ Awaiting --> Awaiting: wrong-kind or unknown-nonce frame ignored
+ Awaiting --> Pending: reply found, height 0, no body
+ Awaiting --> Tx: reply found, body txid equals query
+ Awaiting --> NotFound: reply not_found, or found that fails L4
+ Awaiting --> Unavailable: reply error, or timeout
+ Pending --> [*]
+ Tx --> [*]
+ NotFound --> [*]
+ Unavailable --> [*]
+```
+
+
+
+
+Hub: phases, the flush cycle, and one payload's entry
+
+The hub's phases (`hub.qnt`). `Starting` and `Stale` restate what the tip fields already say (no tip yet; the clock is free-running) and are phases for readability:
+
+```mermaid
+stateDiagram-v2
+ [*] --> Down
+ Down --> Starting: restart, queue empty, no tip, no epoch
+ Starting --> Running: first tip observed, epoch adopted without a flush
+ Running --> Stale: no forward tip progress
+ Stale --> Running: tip advances
+ Running --> Draining: shutdown signal
+ Stale --> Draining: shutdown signal
+ Draining --> Stopped: final flush done, leftovers lost
+ Starting --> Down: crash
+ Running --> Down: crash, queue and in-flight batch lost
+ Stale --> Down: crash, queue and in-flight batch lost
+ Draining --> Down: crash
+ Stopped --> Down
+```
+
+The flush cycle:
+
+```mermaid
+stateDiagram-v2
+ [*] --> Idle
+ Idle --> Broadcasting: tip epoch exceeds last flushed epoch, or draining; whole queue moves in flight
+ Idle --> Idle: nothing queued, epoch recorded
+ Broadcasting --> Broadcasting: indexer returns one entry's verdict
+ Broadcasting --> Idle: all verdicts in; requeue retryable entries; record epoch
+```
+
+One payload's entry. `Absent --> Queued` is reachable again after `Published`: bytes that were published are admitted again if resubmitted.
+
+```mermaid
+stateDiagram-v2
+ [*] --> Absent
+ Absent --> Refused: admit fails (TipStale, Draining, ExpiryTooTight)
+ Refused --> Absent
+ Absent --> Queued: admit
+ Queued --> Queued: same bytes again (duplicate)
+ Queued --> InFlight: flush begins
+ InFlight --> Published: verdict Accepted or AlreadyKnown
+ InFlight --> Rejected: verdict Rejected
+ InFlight --> Queued: Retryable, still survives next flush, attempts within bound, no resident copy
+ InFlight --> DroppedExpired: Retryable, no longer survives next flush
+ InFlight --> DroppedExhausted: Retryable, attempts over bound
+ Queued --> Lost: crash
+ InFlight --> Lost: crash
+ Published --> Absent
+ Rejected --> Absent
+ DroppedExpired --> Absent
+ DroppedExhausted --> Absent
+ Lost --> Absent
+```
+
+
+
+
+Indexer, network and third party
+
+- **Chain and indexer** (`indexer.qnt`). A transaction's status only moves forward: absent, in the mempool, mined. The indexer answers lookups and gives a verdict on each broadcast.
+- **Network** (`spells/soup.qnt`). A message is added to the soup and never removed. It may be delivered any number of times, in any order, or never.
+- **Third party.** A client of the hub's public, unauthenticated address. It may learn a txid out of band, look it up, and resubmit any payload the chain has published.
+
+
+
+### Wire encoding
+
+A hub answers a lookup with one of three wire replies, and the shim turns that into what the wallet sees (`wire.qnt`).
+
+| The hub's situation | Reply on the wire | What the wallet sees |
+|---|---|---|
+| The transaction is queued here | found, height 0, no body | Pending |
+| Its indexer has the transaction | found, with the height and the body | The transaction, if the body's txid is the one asked for; otherwise not found |
+| Its indexer says not found | not found | Not found |
+| Its indexer cannot be reached | error | Unavailable |
+| Its indexer says "found, height 0, no body" (a fault) | found, height 0, no body | Pending |
+
+"Pending" has no reply of its own: it is a found reply with nothing in it. So the first and last rows are the same bytes, and neither the shim nor the wallet can tell "queued at the hub" from "an indexer said found and returned nothing". One misbehaving indexer endpoint is enough to produce the last row (finding 8).
+
+## Assumptions
+
+> What must be true of the world for the claims to apply.
+
+- **Roles.** The shim and the hub both run attested. The shim is modelled as honest in every configuration: it sees every migration in plaintext and controls everything the wallet observes, so no wallet-facing guarantee could survive its compromise. The hub is modelled as honest or Byzantine, not because it is trusted less, but to measure how much each guarantee depends on the hub's enclave. The indexer runs outside any enclave, so a Byzantine indexer is the realistic adversary. One component is Byzantine at a time.
+- **Honest and Byzantine.** An honest component takes exactly the transition its function gives. A Byzantine one takes any member of a finite set that contains the honest transition (`byzantineContainsHonestTest`). No message or state field records which it took.
+- **Byzantine hub.** It admits or refuses a submission whatever the admission rules say, and may send any reply to a lookup. Its ack is modelled as truthful: a real one could ack anything, but nothing reads an ack. Every other move is the honest one: it cannot evict or withhold a queued entry, flush off schedule, or send a frame nobody asked for.
+- **Byzantine indexer.** Any verdict, with the transaction relayed or not. Any lookup answer built from a payload it was offered, one the chain published, or a twin of either. In the hub specification it also reports any tip.
+- **Network.** May lose, duplicate, delay and reorder frames. Cannot forge or read them.
+- **Third party.** Looks up txids it knows and submits payloads it has learned or the chain has published. It cannot read or forge frames, so it does not know a nonce and cannot answer the shim.
+- **Nonces** are unique. A counter stands for an unguessable value.
+- **Chain.** No reorg of an included transaction and no mempool eviction. The operator's indexer publishes nothing.
+- **Wallets.** A supported ("conforming") wallet sets an expiry at least `MIN_WALLET_EXPIRY` after the height it builds at, and its frame reaches the hub within `DELIVERY_LAG` blocks. A wallet asks only about transactions it has sent.
+- **Hub schedule** (hub specification only). How promptly the hub learns the tip depends on the configuration: at every block, up to the reorg allowance behind, or not at all for a while. Fewer blocks arrive while a flush is in flight than the mining margin reserves. The code enforces neither; see [Configurations](#configurations) and findings 1, 2 and 4.
+- **Time.** There is no clock. A timeout may happen at any moment; the staleness window is counted in blocks.
+
+Each configuration's assumptions are the guard of its named `init`. A guard that is false leaves no initial state, and the gate fails on that.
+
+## Threat model
+
+> What the specification is afraid of, who could cause it, and whether a property answers it.
+
+The deployment targets the server-side and network-metadata adversaries of Taylor Hornby's [wallet app threat model](https://zcash.readthedocs.io/en/latest/rtd_pages/wallet_threat_model.html); the Security section of [`zeronym/README.md`](../../README.md) says what is and is not protected. This specification covers the part of that which is a property of protocol runs. Which guarantee answers a threat is the "Answers" column under [Guarantees](#guarantees), and which gap records one that is not prevented is the "Threat" column under [Known gaps](#known-gaps).
+
+| # | Threat | Adversary | Status |
+|---|---|---|---|
+| T1 | The operator sees a migration's contents | Operator behind the shim | Answered |
+| T2 | Someone obtains a queued migration's bytes and publishes it early, breaking the batch | Unauthenticated third party; Byzantine hub or indexer | Answered, if the hub and the indexer are honest |
+| T3 | The wallet is served a different transaction than the one it asked for | Byzantine hub or indexer | Answered for the txid; not for the bytes or the height |
+| T4 | The wallet is told something false about its transaction's status | Byzantine hub or indexer; network reordering | Answered for each answer, if the hub and the indexer are honest; not across answers (T8) |
+| T5 | A supported wallet's migration expires while the hub holds it | Chain timing; a flaky tip; Byzantine hub or indexer | Answered in part: under a timely or regressing tip, not under a stale one |
+| T6 | The hub silently drops or admits entries outside its rules | Hub implementation error | Answered |
+| T7 | The wallet is told "sent" but the hub never admits it | Network; the hub's own refusals | Not prevented |
+| T8 | The wallet sees its transaction's status go backwards | Network reordering; resubmission; the flush window | Not prevented |
+| T9 | An acknowledged migration is lost to a crash, a failed final flush, or a requeue drop | None needed | Not prevented |
+| T10 | A third party who knows a txid learns it is queued | Unauthenticated third party | Accepted |
+| T11 | A lying indexer makes the hub flush early, shrinking the batch, or stop admitting | Byzantine indexer; one endpoint suffices | Not prevented; recorded |
+| T12 | Any admitted transaction, including a late arrival or one from an unsupported wallet, is offered too late | As T5 | Not checked |
+| T13 | The hub acknowledges a migration it never queued | Byzantine hub | Not modelled: nothing reads an ack |
+| T14 | Linking a wallet to its migration by source IP | Network observer; operator | Not modelled. Claimed protected in `zeronym/README.md` |
+| T15 | Linking by submission size and arrival time | Operator | Not modelled. Listed as not protected in `zeronym/README.md` |
+| T16 | The operator recovering txid and value through transparent-pool queries | Operator | Not modelled. Listed as not protected in `zeronym/README.md` |
+| T17 | Batch-size and timing anonymity; partitioning the anonymity set across hubs | Network observer | Out of scope: timing and anonymity are not trace properties here, and there is one hub |
+| T18 | A compromised shim or enclave host | Host; a malicious build | Assumed away. A compromised host is delegated to AWS in `zeronym/README.md`; a malicious shim build is excluded by attestation and is not discussed there |
+
+## Guarantees
+
+> Promises about whole runs of the system: this bad thing never happens.
+
+| Id | Name | What it says | Answers | Checked by |
+|---|---|---|---|---|
+| G1 | `operatorBlind` | Everything the shim hands the operator is a pass-through transaction | T1 | Simulation |
+| G2 | `queuedBytesConfidential` | Everything the third party has learned is on the chain, or was a pass-through transaction given to the operator. Its knowledge is derived from the replies sent to it and the operator's view | T2 | Simulation |
+| G3 | `txidAuthenticity` | A transaction served to the wallet has the txid asked for. It need not be the bytes the wallet sent, and its height is whatever the hub said | T3 | Simulation; `servedOnlyOnMatchingTxidTest` exhaustively |
+| G4 | `lookupValidityPerHub` | Every lookup answer other than "unavailable" was true at the hub that gave it at some point between request and answer. Not-found during the flush window counts as true, as the implementation intends (`Hub::lookup`, `zeronym/hub/src/server.rs`). It does not say that successive answers agree | T4 | Simulation |
+| G6b | `conformingFirstOfferBeforeExpiry` | A supported wallet's transaction is offered with the mining margin to spare, the first time a hub offers it. About the margin left when the flush begins, not about acceptance; nothing about a later offer of a requeued entry | T5 | TLC, exhaustive |
+| G6c | `conformingFirstOfferJudgedBeforeExpiry` | End to end: when a node judges the first offer of a supported wallet's transaction, it has not expired. Needs G6b and the flight-time assumption | T5 | TLC, exhaustive |
+| G7 | `wellFormedTest` | Structural sanity of the hub: a queued entry is within its attempts and a down hub holds nothing | T6 | Exhaustive test over every reachable hub state |
+| A2 | `neverEvictTest` | An entry leaves the hub's queue only into a flush, or because the hub went down or exited after its final flush | T6 | Exhaustive test over every reachable hub state and input |
+| A3 | `drainIsFinalTest` | A draining honest hub's queue gains only what a flush hands back | T6 | Exhaustive test over every reachable hub state and input |
+
+A2 and A3 constrain a single hub step, not a state; the rest are state invariants.
+
+Each pure function also has exhaustive tests over small inputs, in `tests/*Test.qnt`.
+
+## Trust matrix
+
+> For each guarantee, whose honesty it depends on.
+
+Single-fault. "holds" is a checked row on the named configuration. "required" is a scripted run in which the component is Byzantine and the guarantee fails; the run asserts the guarantee in the state just before the Byzantine step, so the lie is what breaks it.
+
+| | All honest | Byzantine hub | Byzantine indexer |
+|---|---|---|---|
+| G1 | holds (`baseline`) | holds (`byzHub`) | holds (`byzIndexer`) |
+| G2 | holds (`baseline`) | **required**: `hubServesQueuedBodyTest` | **required**: `indexerServesUnpublishedBodyTest`. One endpoint suffices |
+| G3 | holds (`baseline`) | holds (`byzHub`); a twin and a false height are both served | holds (`byzIndexer`) |
+| G4 | holds (`baseline`) | **required**: `hubDeniesQueuedTest`, `hubServesFalseHeightTest` | **required**: `indexerForgesPendingTest`. One endpoint suffices |
+| G6b | holds (`timely`, `flakyTip`, `flakyTipSlowFlight`) | **required**: `hubAdmitsBeforeFirstTipTest` | **required**: `indexerWithholdsTipFromConformingTest`. Needs every endpoint |
+| G6c | holds (`timely`, `flakyTip`) | **required**: `hubAdmitsBeforeFirstTipTest` | **required**: `indexerWithholdsTipFromConformingTest`. Needs every endpoint |
+| A3 | holds | **required**: `hubAdmitsWhileDrainingTest` | holds |
+
+- A hub folds several indexer endpoints into one answer: the tip is the maximum, a lookup takes the first "found", a broadcast takes the best verdict. So one misbehaving endpoint can raise the tip, inject a lookup answer or change a verdict, while lowering or freezing the tip takes every endpoint. The model has one abstract indexer and does not enforce that difference; the indexer cells say which each needs.
+- There is no shim column: every wallet-facing guarantee assumes an honest, attested shim.
+- G3 is the only wallet-facing guarantee that survives a Byzantine hub or indexer, and it authenticates the txid only.
+- G1 depends on the shim alone.
+- A Byzantine hub breaks G6b by admitting while it has no tip, when an honest hub refuses everything. Admitting past the expiry rule cannot break it, because that rule never refuses a supported wallet's timely transaction (`conformingTimelyPayloadIsAdmissibleTest`).
+
+## Known gaps
+
+> Things you might expect to hold that don't, each with a concrete example run. Every component is honest in all of them.
+
+"By design" means the implementation says so itself. "Found here" means this specification showed it and nobody has yet decided whether it is acceptable.
+
+| Id | Threat | What is lost | Status | Where | Checked by | Scripted run |
+|---|---|---|---|---|---|---|
+| K1 | T7 | Told ok does not mean the hub ever admits it: it may refuse the frame, or never receive it | By design: the hub's verdict "is deliberately not waited for" (`zeronym/shim/src/hub.rs:289-295`) | `baseline` | scripted runs | `toldOkThenRefusedTest`, `toldOkAndNeverDeliveredTest` |
+| K2 | T8 | `statusNeverRegresses`: what a wallet sees of one transaction never goes backwards | By design for the flush window, which the code accepts in a comment on `Hub::lookup` (`zeronym/hub/src/server.rs`); resubmission of a published transaction is finding 10, not triaged | `baseline` | simulation, violated | `repliesReorderedTest`, `walletResendsPublishedTest`, `thirdPartyResubmitsPublishedTest`, `flushWindowTest`, `rejectedAtFlushTest` |
+| K3' | T5 | G6b and G6c when the expiry floor leaves no slack for the reorg allowance | Found here (finding 3); not triaged | `flakyTipNoSlack` | TLC, violated | `conformingMissesMarginWithoutSlackTest` |
+| K4 | T5 | G6b and G6c on the shipped relation between the constants, across a tip silence shorter than the staleness window | Found here (finding 1); not triaged | `staleLag` | TLC, violated | `silenceAcrossBoundaryMissesMarginTest`; contrast `sameSilenceWithSlackKeepsMarginTest` |
+| K5 | T9 | `ackedIsHeldOrSettled`: an acknowledged payload is still held by the hub, or is on the chain, or a node judged it | By design: the queue is in memory only, and the code logs what it loses (`zeronym/hub/src/batcher.rs:337-347`, `:467-478`). How much one unjudged flush drops is not triaged (finding 5) | `timely` | TLC, violated three ways | `ackedThenCrashedTest`, `ackedThenLostAtDrainTest`, `requeueDropsAckedAsExpiredTest` |
+| K6 | T5 | `conformingEveryOfferBeforeExpiry`: G6b for every offer, not only the first | Found here (finding 7); not triaged | `staleLag` | TLC, violated | `requeuedPastExpiryTest` |
+| K7 | T5 | G6c when a flush may stay in flight for as many blocks as the mining margin | Found here (finding 4); not triaged | `flakyTipSlowFlight` | TLC, violated; G6b holds there | `slowFlightSpendsTheMarginTest` |
+| K8 | T5 | A supported wallet's transaction, acknowledged on time, lost to a crash and resent, is first offered by the restarted hub with less than the mining margin. To the restarted hub the resend is a late first arrival, so G6b and G6c do not cover it | Found here (finding 6); not triaged | `flakyTip` | scripted run | `crashThenLateDuplicateTest`; control `lateDuplicateWithoutCrashTest` |
+| K9 | T5 | G6b and G6c even when the expiry floor is wide enough to cover a tip silence: a stale hub's free-running clock flushes an empty queue early and spends the next epoch, so a transaction admitted after the tip returns waits a full interval | Found here (finding 2); not triaged | `staleLagWithSlack` | TLC, violated | `earlyFlushSpendsTheNextEpochTest` |
+
+K1 is not an invariant because it would be false on the ordinary success path too: the wallet is told ok before the hub has the frame.
+
+Behaviours that are accepted or only recorded:
+
+| Behaviour | Threat | Shown by |
+|---|---|---|
+| **Accepted disclosure.** A third party that knows a txid learns that it is queued. The hub withholds the bytes, not the fact. The implementation leaves this open deliberately (`Hub::lookup`, `zeronym/hub/src/server.rs`): "the 200-versus-NotFound distinction still discloses that a given txid is queued here. Closing that too means answering NotFound, which costs a wallet the ability to tell "pending" from "never seen"" | T10 | `thirdPartyLearnsItIsQueuedTest`; witness `wQueuedDisclosed` on `baseline` |
+| **Twin and false height served.** The wallet can be served a twin of what it sent, and a transaction at a height the hub made up. G3 holds throughout | T3 | `wTwinServed`, `wFalseHeightServed` on `byzHub` |
+| **Premature flush.** A Byzantine indexer reports a tip ahead of the chain and the hub flushes before the true boundary: a batching harm, not an expiry one. What a report far ahead of the chain does is finding 11 | T11 | `tipAheadOfChainFlushesEarlyTest` |
+| **Early flush by the free-running clock.** A stale hub's clock is ahead of the chain and it flushes before the true boundary, with every component honest | T11, with no liar | `freeRunningClockFlushesEarlyTest` |
+| **Unparseable and queued.** A payload the hub cannot parse has no txid, so a lookup misses it while it is queued | none | `unparseableIsQueuedAndMissedTest` |
+
+## Out of scope
+
+> What the specification deliberately does not cover, and why.
+
+### One hub
+
+The specification checks one hub; production runs one or more, replicated: every shim sends every submission to every hub, and each hub that receives a migration queues and broadcasts it (`zeronym/shim/src/nym.rs:602-647`). The single hub is a scope choice, not a claim about production.
+
+Not checked as a result: two hubs disagreeing about one transaction; duplicate publication, and a second enclave holding the plaintext, both accepted deliberately in production; told ok after a partial send, and its anonymity cost; a lookup moving to the next address on a timeout (finding 9); that one Byzantine replica is enough to break G2 and G4.
+
+Argued, not checked, on the assumption that hubs share nothing but the chain and the indexer:
+
+- **Compose per hub:** G1, G3, G4 (which is why its name says "per hub"), G6b and G6c, and gap K5.
+- **Compose only if every hub is honest:** G2. One Byzantine replica holds the same bytes and can give them away.
+- **Do not compose:** K1 and K2 each gain a cause with a second hub.
+
+### Not modelled
+
+| Item | Reason |
+|---|---|
+| Attestation, PCRs, TLS, STEVE, keymaker quorum | No in-protocol messages exist. Represented by the roles |
+| Mixnet internals: SURBs, Sphinx, cover traffic, gateways, throttling; the shim's client rotation; both `nym_driver.rs` | Their protocol-visible effect is loss and delay |
+| The hub's lookup concurrency bound, reply deadline and dropped acks | Refinements of "the network lost the message" |
+| Wall-clock time | There is no clock: the staleness window is counted in blocks, and a timeout may happen at any moment |
+| Multiple indexer endpoints | One abstract indexer stands for all of a hub's endpoints. The trust matrix says, for each Byzantine-indexer cell, whether one lying endpoint suffices |
+| Wire codecs, byte layout, malformed frames | Pinned by the Rust tests and golden vectors in both crates. The specification works at the level of what a reply means, and does not bind the codec |
+| Reorgs of included transactions, mempool eviction | Assumed away: a transaction's chain status only moves forward |
+| Anonymity-set size, shuffle, simultaneity, timing and length side channels | Not properties of a single run |
+| The forward-only shim, transparent-pool RPCs, health, address and attestation endpoints, logging | Not part of the divert protocol |
+| The HTTP transport, where the shim waits for the hub's verdict before answering the wallet (`HubTransport::Http`, `--hub`) | The production deployment is the mixnet (`HTTP_SUBMIT=0`). So there is no configuration here in which the shim's ok means the hub has the transaction |
+| A Byzantine shim | The shim runs attested, sees every migration in plaintext and controls what the wallet observes. Every wallet-facing guarantee assumes it honest |
+| What the hub's ack says | Nothing reads an ack: the shim tells the wallet ok without waiting for it. That an accepted ack is only for a queued payload is not a checked property, and a Byzantine hub's ack is modelled as truthful |
+| The hub's capacity and size refusals, and denial of service generally | Not claimed properties. The shim's own too-large refusal is modelled |
+| A third party submitting payloads of its own making | Possible, since the hub's address is public and unauthenticated. The model's third party submits only what it has learned or the chain has published |
+| Wallets whose expiry is below the supported floor, and submissions that arrive later than the delivery lag | No schedule guarantee is made for them (but see finding 6). Admission's own claim that every admitted entry "provably survives" its scheduled flush (`zeronym/hub/src/queue.rs:497-519`) is not checked, and is known not to hold under a tip reported behind the chain |
+| More than one Byzantine component at once | The trust matrix is single-fault |
+| Liveness: that anything eventually happens, such as a submitted migration being published | The network may lose everything, and nobody waits for an ack |
+
+## Findings
+
+> Where the model disagrees with what the code or its comments assume.
+
+Nothing here has been fixed. "Code read" means the cited lines were read and match the model; nothing was run against the Rust. The severity beside a code bug is a judgement from that reading, not from a reproduction: HIGH, one in-scope adversary degrades batching or availability for every user of the hub; MEDIUM, one wallet loses a transaction or is misled about one; LOW, a transient wrong status or a wrong operator signal. Only code bugs carry a severity, so a row without one is not thereby minor: finding 5 is by design and may matter more than any MEDIUM bug.
+
+| # | Finding | Kind | Shown by | Against the Rust |
+|---|---|---|---|---|
+| 1 | **A short tip silence costs a supported wallet its mining margin.** The cadence follows the last tip seen, so a silence across a flush boundary delays the flush until the hub goes stale. The staleness window is 12 blocks and the slack is 10, so on the shipped constants the first offer is at `created + 37` against an expiry of `created + 40`: three blocks of margin where four are reserved. It needs the hub not to hear the tip while a broadcast would still succeed, and the tip not to return before the hub goes stale; the tip and the broadcast use the same endpoints, so an unreachable indexer delays both | Latent: a real gap between the constants, in a narrow environment | K4, `silenceAcrossBoundaryMissesMarginTest`; TLC on `staleLag` | Code read: `batcher.rs:40-71`, `:227-247`. The one-block shortfall reads 15 minutes as exactly 12 blocks |
+| 2 | **An early free-running flush spends the next epoch.** A stale hub's clock runs ahead, flushes an empty queue and records that epoch. When the tip returns, admission counts on a flush that has already happened, and the transaction waits a full interval. A wider expiry floor does not fix it. The supported-wallet witness also needs a second, shorter silence | Code bug (MEDIUM), one root cause with finding 6: the loop records the epoch from the cadence height, and admission estimates the next flush from the observed height | K9, `earlyFlushSpendsTheNextEpochTest`; TLC on `staleLagWithSlack` | Code read: `batcher.rs:236-247`, `:316-326`. The comment there calls a clock that runs ahead "the safe direction" |
+| 3 | **The reorg slack holds by coincidence of constants.** The expiry floor minus the three-term budget is 10 blocks, exactly the reorg allowance, and startup validation checks only the three-term sum. Without the slack a supported wallet's transaction misses its margin | Latent: no failure on the shipped constants | K3', `conformingMissesMarginWithoutSlackTest`; TLC on `flakyTipNoSlack` | Code read: `batcher.rs:40-59`, `:101-113` |
+| 4 | **A flush's flight is bounded in time, not in blocks.** The budget leaves exactly the mining margin at the offer, so blocks that arrive while the batch is in flight come out of it. Each call is bounded at 10 s with 64 in flight, about 160 s at the 1,024-entry cap, which is about two nominal blocks against a margin of four. Block arrival is not bounded by the clock, and requeue does not enforce the entry cap | Bounded in time, not in blocks; reachable only with a slow or selectively hanging indexer | K7, `slowFlightSpendsTheMarginTest`; TLC on `flakyTipSlowFlight` | Code read: `chain.rs:49`, `:59`. Estimate, not measured: with exponential block times at a 75 s mean, a flight of that length sees four or more blocks about one time in six |
+| 5 | **An acknowledged payload can be lost three ways with every component honest:** a crash; a draining hub's final flush that finds the indexer unreachable; a requeue that gives the entry up as expired. On the shipped constants a requeue keeps an entry only if it was created at most 16 blocks before the flush (`40 - 20 - 4`). For wallets at the 40-block floor, one unjudged flush therefore drops between 20% and 50% of a batch, depending on delivery lag, each entry with 14 to 23 blocks of life left | By design; the magnitude is not triaged | K5 and its three runs; TLC on `timely` | Code read: the loss is logged at error level (`batcher.rs:337-347`, `:467-478`) and unit-tested (`queue.rs`, `a_requeue_gives_up_on_an_entry_that_can_no_longer_be_mined`); the rule is `queue.rs:507-520`. The percentages are arithmetic on the constants, assuming arrivals uniform over the interval |
+| 6 | **An entry admitted while the tip is reported below a boundary already flushed waits a full interval.** Admission counts on the flush at that boundary, which will not happen again. Any late arrival meets it; the supported-wallet case is a resend after a crash, which a restarted hub offers with less than the mining margin | Code bug (MEDIUM), one root cause with finding 2 | K8, `crashThenLateDuplicateTest` | Code read: `batcher.rs:177-186`, `:316-327`; `queue.rs:294`, `:507-520` |
+| 7 | **On a stale hub a requeued entry is offered again past its expiry, and only the attempt bound stops it.** Each requeue judges the entry against the same stale tip, as admission does, so the expiry rule never gives it up. A supported wallet's transaction is offered a third time after its expiry, and is finally dropped as exhausted. The late offers normally reach no node: a stale hub whose flushes come back unjudged almost always has an unreachable indexer | Real behaviour that contradicts a comment; low harm | K6, `requeuedPastExpiryTest`; TLC on `staleLag`; `expiringEntryDroppedAsExhaustedTest` | Code read: `batcher.rs:417-422`; `queue.rs:197` says "Only reachable for a payload with no expiry". The shipped bound is 8 requeues |
+| 8 | **One indexer endpoint can make a wallet see "pending" for a transaction nobody holds.** "Found, height 0, no body" from an indexer is byte-identical to the hub's own queue-hit reply, and the hub forwards it unchanged | Code bug (MEDIUM): an ambiguous wire reply, and no check on an untrusted answer | `sentinelCollisionTest`, `indexerForgesPendingTest` | Code read: `server.rs:445-451`, `chain.rs:284-290`, `:305-319` |
+| 9 | **Lookups choose a hub by apparent liveness.** A lookup starts at a rotating cursor and moves to the next address only on a timeout, the pattern the submit path forbids. Whoever can make one hub time out decides which hub answers | Undecided: deliberate and tested, and in conflict with a rule written for submits. The `PRODUCTION.md` that rule cites is not in the repository | Not modelled: needs more than one hub | Code read: `shim/src/nym.rs:746-797`, against the rule at `:628-633`; `shim/tests/nym.rs` asserts the behaviour today |
+| 10 | **Anyone can make the hub answer "pending" for a published transaction, and pad its batch-size signal.** The queue deduplicates against resident entries only, so published bytes are admitted again if resubmitted, and a lookup answers from the queue first. The wallet reads "pending" for a transaction it has already been served, until the next flush. The flush also counts an already-known verdict toward the achieved batch size, which the code calls "the honest measure of the privacy", so free, public bytes can raise that figure and suppress the warning for a batch of one | Code bug (LOW): the comment on `Hub::lookup` calls a resubmit harmless. The batch-size figure is logged and returned but drives no decision | K2, `thirdPartyResubmitsPublishedTest`, `walletResendsPublishedTest` | Code read: `queue.rs:308-310`, `:358-359`; `Hub::lookup` in `server.rs`; `batcher.rs:352`, `:389`, `:480`. Not checked: that a node answers already-known for a transaction that is already mined |
+| 11 | **One high tip report pins the hub's tip.** `observe` adopts any higher height and ignores a later drop larger than the reorg allowance. So one endpoint reporting a height P makes every real height look like an oversized regression until the chain reaches P minus the allowance, which for a large P is until restart. The epoch jumps, so the hub flushes once off cadence; after that admission refuses every expiring transaction, because the observed height is P | Code bug (HIGH): the code says taking the maximum over endpoints defends the clock against being advanced, and it defends only against slowing it | Found by reading; not modelled, because the model's heights are bounded. `tipAheadOfChainFlushesEarlyTest` shows the one early flush | Code read: `batcher.rs:19-22`, `:171-203`, `:316-326`; `chain.rs:176-201` |
+
+On finding 2, the model lets the free-running clock be at most one flush interval ahead, so it can spend one epoch. `cadence_height` has no such cap. Reading that code, a clock further ahead would skip more than one boundary; the model does not exhibit that.
+
+## How it is checked
+
+> How much to trust a green row, and how to produce one.
+
+```sh
+sh zeronym/spec/quint/check.sh
+```
+
+"Holds" means one of three things, and the "Checked by" column says which:
+
+- **TLC, exhaustive.** The hub specification. TLC visits every reachable state of the named configuration. The configurations are small (two or three payloads, a schedule scaled down from the shipped one, heights up to 12), so this is exhaustive for those parameters and not beyond them.
+- **Exhaustive test.** `quint test` over a small finite universe: every input of a function, or every reachable hub state.
+- **Simulation.** The protocol specification. `quint run`: at most 40 or 80 steps per trace, 2000 random traces, one seed. Not a proof and not exhaustive to any depth; a property that holds is one no sampled trace violated.
+
+`quint verify` has not been run on any part of this. TLC is run through `tlc.sh`, because the compiled specification is larger than the Apalache server accepts.
+
+| Tier | What | Expectation |
+|---|---|---|
+| 1 | `quint typecheck` on every file | ok |
+| 2 | `quint test` on every test file | all pass, and each file reports at least the count `check.sh` gives it |
+| 3 | `quint run`, invariants | "holds" rows hold; K2 is violated |
+| 3b | `quint run`, witnesses | every listed state is reached at least once; no invariant is violated on the way |
+| 4 | `tlc.sh`, one row per invariant and configuration | "holds" rows hold over every reachable state; "violated" rows are violated by a counterexample no longer than the recorded one |
+
+Quint 0.33.0 is pinned (`npx --yes @informalsystems/quint@0.33.0` by default; set `QUINT=quint` to use an installed one). Tier 4 needs Java and Apalache 0.62.1, whose jar carries TLC; without either the tier fails, it never skips. `CHECK_TIERS=simulation` runs tiers 1 to 3b and `CHECK_TIERS=tlc` tiers 1 and 4; CI runs them as two jobs. All four tiers take about six minutes on a 16-core machine. It has not been timed on a CI runner.
+
+### Configurations
+
+A configuration is a value held in the state and selected by a named init.
+
+#### Protocol specification
+
+At most 3 sends and 3 lookups by the wallet, 3 requests by the third party.
+
+| Configuration | Hub | Indexer |
+|---|---|---|
+| `baseline` | honest | honest |
+| `byzHub` | **Byzantine** | honest |
+| `byzIndexer` | honest | **Byzantine** |
+
+#### Hub specification
+
+The schedule flushes every 3 blocks with a mining margin of 2, a delivery lag of 1, a reorg allowance of 1, a staleness window of 3 and an expiry floor of 7. It is the shipped schedule scaled down (interval 20, margin 4, lag 6, reorg allowance 10, staleness window 12 blocks, expiry floor 40), keeping the relations between the constants that the findings turn on.
+
+| Configuration | Differs from `timely` by | For |
+|---|---|---|
+| `timely` | | G6b, G6c, K5 |
+| `flakyTip` | the tip may be reported up to the reorg allowance behind | G6b, G6c under regression; K8 |
+| `flakyTipNoSlack` | and the expiry floor is 6, leaving no reorg slack | K3' |
+| `flakyTipSlowFlight` | and a flush may be in flight for 2 blocks | K7 |
+| `staleLag` | the hub may hear no tip, and goes stale | K4, K6 |
+| `staleLagWithSlack` | and the expiry floor is 8, enough to cover the silence | finding 2 |
+| `byzHub`, `byzIndexer` | one Byzantine component, and a tight-expiry payload | the trust matrix |
+| `unknownUpgrade` | an unparseable payload; scripted runs only | the attempt bound |
+
+In every configuration a due flush begins before the next block, and at most one block arrives while a flush is in flight (two in `flakyTipSlowFlight`). Under `staleLag` a hub is stale once it has heard no tip for the staleness window; its free-running clock is then assumed never behind the chain and at most one flush interval ahead of it. The implementation relies on "never behind" and does not enforce it (`zeronym/hub/src/batcher.rs:64-67`).
+
+
+What TLC visits
+
+With 8 workers, on the machine this was written on:
+
+| Configuration | Invariant | Verdict |
+|---|---|---|
+| `timely` | G6b and G6c | holds, 20 030 states, depth 40 |
+| `timely` | K6's predicate | holds, 20 030 states, depth 40 |
+| `flakyTip` | G6b and G6c | holds, 113 496 states, depth 38 |
+| `flakyTipSlowFlight` | G6b | holds, 156 352 states, depth 39 |
+| `flakyTipNoSlack` | G6b (K3') | violated, 12 states |
+| `flakyTipSlowFlight` | G6c (K7) | violated, 14 states |
+| `staleLag` | G6b; G6c; K6 | violated, 13; 14; 13 states |
+| `staleLagWithSlack` | G6b; G6c (finding 2) | violated, 19; 20 states |
+| `timely` | K5 | violated: 5 states; 8 without a crash; 12 without a shutdown either |
+| `byzHub` | G6b; G6c | violated, 12; 13 states |
+| `byzIndexer` | G6b; G6c | violated, 16; 17 states |
+
+TLC runs with deadlock checking off, so a machine whose steps had died would hold everything. The gate therefore also requires one reachable state per family of steps, and the antecedents of G6b and G6c, each as a violated `not(..)` row.
+
+
+
+
+The abstraction lemma
+
+The protocol specification's hub is the abstract one in `abstractHub.qnt`. `hubTest` checks, over every reachable state of the real hub function and every input, that each real step is a step of the abstract hub (`abstractionTest`, `byzantineAbstractionTest`), and that each abstract move has a real step behind it (`realisesTest`). So an invariant that holds over the abstract hub, and reads only queue membership and wire replies, holds over the real one: that covers G2, G3 and G4. It does not transfer reachability: the abstract hub answers where the real one is down or stale, so a violation shown over it is a state of the abstract hub. The reachable set is computed at a smaller schedule than the hub specification's and carried over by argument.
+
+
+
+### Layout
+
+Only `protocol.qnt` and `hubMachine.qnt` declare variables, and no module declares a constant. Every other module is pure.
+
+| File | Owns |
+|---|---|
+| `spells/basicSpells.qnt`, `spells/soup.qnt` | `Option` and set and map helpers; the message soup |
+| `types.qnt` | The vocabulary: payloads, verdicts, refusals, roles, observations |
+| `wire.qnt` | The four frames; `render`, `meaning`, `interpretReply` |
+| `indexer.qnt` | The chain and indexer as a relation, honest and Byzantine |
+| `hub.qnt` | `hub(state, input)`: admission, the tip rule, the flush cycle, requeue; the Byzantine relation |
+| `shim.qnt` | `shim(state, input)`: routing and reply correlation |
+| `hubMachine.qnt` | The hub specification: one hub, the chain, its configurations and invariants |
+| `abstractHub.qnt` | The hub as the protocol sees it |
+| `protocol.qnt` | The protocol specification: state, steps, guarantees, gaps, witnesses, configurations |
+| `tests/wireTest.qnt`, `indexerTest.qnt`, `shimTest.qnt`, `hubTest.qnt` | The functional properties; in `hubTest.qnt` also G7, A2, A3 and the abstraction lemma |
+| `tests/hubScenariosTest.qnt` | Scripted runs of the hub specification: one per gap and per trust-matrix cell |
+| `tests/scenariosTest.qnt`, `tests/trustTest.qnt` | Scripted runs of the protocol specification: gaps and witnesses; trust-matrix cells |
+| `check.sh`, `tlc.sh` | The gate; one TLC check of one invariant on one configuration |
+
+## Future work
+
+> What would make these results bind the code.
+
+1. **Failing Rust tests for the findings.** Each finding is shown on the model and matched to the code by reading; no test has been written. A reading of the existing harnesses suggests most need no production change: finding 8 fits the hub's integration tests with its mock indexer, and the cadence findings (1, 2 and 6) fit `batcher.rs`'s own unit tests, where the loop and the cadence clock are visible. Missing today: a fixture with a non-zero expiry, and a way to know the cadence loop has completed a poll. Finding 4 is impractical to reproduce.
+2. **Model-based testing with `quint-connect`.** Depends on 1, and needs driver code in Rust. The specification is shaped for it: every branch of a step is a named action with its choices as named picks; each step gives one input to one component function and applies one output; and those functions map onto the seams in the table under [System](#system).
+3. **`quint verify` with Apalache for a subset of the claims.** The compiled specification is too large for the Apalache server today. A subset small enough to pass would give bounded symbolic checking of the protocol guarantees, which are simulated only.
diff --git a/zeronym/spec/quint/abstractHub.qnt b/zeronym/spec/quint/abstractHub.qnt
new file mode 100644
index 00000000..6e6fe026
--- /dev/null
+++ b/zeronym/spec/quint/abstractHub.qnt
@@ -0,0 +1,76 @@
+// -*- mode: Bluespec; -*-
+
+/// The hub as the protocol sees it: which payloads it has queued, which are
+/// out with a flush, and what it puts on the wire. No phase, no tip, no
+/// schedule.
+///
+/// `hubTest` checks that every step of the real hub from a reachable state is
+/// a step of this one (the abstraction lemma), so a protocol invariant that
+/// holds over this hub, and reads only queue membership and wire replies,
+/// holds over the real one. The converse does not hold: this hub answers
+/// where the real one would refuse or error, so a reachable state here need
+/// not be reachable there.
+module abstractHub {
+ import basicSpells.* from "./spells/basicSpells"
+ import types.* from "./types"
+ import wire.* from "./wire"
+
+ type AHub = { queue: Set[Payload], held: Set[Payload] }
+
+ /// A client's request, with the indexer's answer for a lookup.
+ type ARequest =
+ | ASubmit(Payload)
+ | ALookup({ txid: TxId, answer: IndexerAnswer })
+
+ type AReply = AAck(WireAck) | AWire(WireReply)
+
+ /// A request's effect: the hub after it, and its reply.
+ type AAnswer = { hub: AHub, reply: AReply }
+
+ pure val emptyAHub: AHub = { queue: Set(), held: Set() }
+
+ pure val WIRE_ACKS: Set[WireAck] =
+ Set(WAccepted, WRefused(WExpiryTooTight), WRefused(WQueueFull), WRefused(WTipStale))
+
+ /// An honest hub accepts a submission into its queue or refuses it under any
+ /// code, and answers a lookup from its queue first and its indexer second.
+ pure def honestAnswers(h: AHub, request: ARequest): Set[AAnswer] =
+ match request {
+ | ASubmit(payload) =>
+ WIRE_ACKS.map(ack =>
+ { hub: if (ack == WAccepted) { ...h, queue: h.queue.union(Set(payload)) } else h, reply: AAck(ack) })
+ | ALookup(lookup) =>
+ val hit = h.queue.exists(payload => payload.txid == Some(lookup.txid))
+ val outcome = if (hit) QueueHit else FromIndexer(lookup.answer)
+ Set({ hub: h, reply: AWire(render(outcome)) })
+ }
+
+ /// A Byzantine hub answers a lookup with anything: a body from `universe` or
+ /// none, at any height, or not found, or an error. A submission it accepts
+ /// or refuses as it likes, which the honest relation already allows; its ack
+ /// says which.
+ pure def byzantineAnswers(h: AHub, request: ARequest, universe: Set[Payload]): Set[AAnswer] =
+ match request {
+ | ASubmit(_) => honestAnswers(h, request)
+ | ALookup(_) =>
+ tuples(Set(None).union(universe.map(payload => Some(payload))), WIRE_HEIGHTS)
+ .map(((body, claimed)) => WFound({ body: body, height: claimed }))
+ .union(Set(WNotFound, WError))
+ .map(reply => { hub: h, reply: AWire(reply) })
+ }
+
+ /// The moves no client asks for: the queue goes out with a flush; an entry
+ /// out with it is settled; what is kept comes back; everything is lost.
+ pure def take(h: AHub): AHub = { queue: Set(), held: h.held.union(h.queue) }
+ pure def settle(h: AHub, payload: Payload): AHub = { ...h, held: h.held.exclude(Set(payload)) }
+ pure def giveBack(h: AHub, kept: Set[Payload]): AHub = { queue: h.queue.union(kept), held: Set() }
+
+ pure def isInternal(h: AHub, after: AHub): bool =
+ or {
+ after == h,
+ after == h.take(),
+ h.held.exists(payload => after == h.settle(payload)),
+ after.held == Set() and after.queue.subseteq(h.queue.union(h.held)) and h.queue.subseteq(after.queue),
+ after == emptyAHub,
+ }
+}
diff --git a/zeronym/spec/quint/check.sh b/zeronym/spec/quint/check.sh
new file mode 100755
index 00000000..36b8a47d
--- /dev/null
+++ b/zeronym/spec/quint/check.sh
@@ -0,0 +1,416 @@
+#!/bin/sh
+# Check the zeronym protocol specification and assert every expected outcome.
+#
+# "Holds" here means bounded random simulation: fixed constants, a fixed step
+# bound, a fixed number of traces and one seed. It is not a proof and it is
+# not exhaustive to any depth. The exception is tier 4, the hub specification,
+# where TLC visits every reachable state of each configuration.
+#
+# Tiers:
+# 1 typecheck every file.
+# 2 quint test: the functional layer and the scripted runs, among them
+# `liveInitsTest`, which starts from every named init.
+# 3 quint run: invariants. "holds" rows are the guarantees, on the
+# configurations where they are claimed. The "fails" row is K2, a known
+# gap; it shows polarity only, and the scripted runs in tier 2 carry the
+# causes. A guarantee under the Byzantine component it depends on has a
+# scripted run and its control, and no row here.
+# 3b quint run: witnesses. Every listed state must be reached in at least
+# one trace. These runs also re-check the configuration's guarantees, on
+# longer traces and under the narrower step relations, which get deeper
+# into the protocol than `step` does.
+# 4 tlc.sh: the hub specification, exhaustively. "holds" rows are the
+# schedule guarantees; "violated" rows are the known gaps, the guarantees
+# under a Byzantine hub or indexer, and the states that must be reachable
+# (each as `not(..)`). Needs Java; fails, never skips, without it.
+#
+# A row that starts holding where it is expected to fail, or the reverse,
+# means the specification or the prediction changed: read README.md before
+# changing the row.
+#
+# QUINT defaults to `npx @informalsystems/quint@0.33.0`. QUINT_BACKEND=typescript
+# skips the Rust evaluator, which is downloaded from GitHub on first use; the
+# sample counts and seeds below were settled on the Rust evaluator.
+# QUINT_JOBS is how many rows run at once. CHECK_TIERS picks what runs after
+# tier 1: `simulation` (2 to 3b), `tlc` (4) or `all`, the default.
+set -u
+
+cd "$(dirname "$0")"
+QUINT=${QUINT:-"npx --yes @informalsystems/quint@0.33.0"}
+BACKEND=${QUINT_BACKEND:-rust}
+SAMPLES=${QUINT_SAMPLES:-2000}
+JOBS=${QUINT_JOBS:-4}
+TIERS=${CHECK_TIERS:-all}
+case $TIERS in
+ all | simulation | tlc) ;;
+ *) echo "CHECK_TIERS is '$TIERS', not all, simulation or tlc" >&2; exit 2 ;;
+esac
+SEED=7
+failures=0
+
+# Rows run JOBS at a time, each writing its result lines to a file of its own
+# and, once it has run to the end, its exit status to a second file; `finish`
+# prints them in the order the rows were written and counts the failures. A
+# row with no status was killed before it finished, and is a failure whatever
+# it printed.
+results=$(mktemp -d)
+trap 'rm -rf "$results"' EXIT
+queued=0
+running=0
+
+job() {
+ queued=$((queued + 1))
+ row_file="$results/$(printf '%04d' "$queued")"
+ ( "$@"; echo $? >"$row_file.status" ) >"$row_file" 2>&1 &
+ running=$((running + 1))
+ if [ "$running" -ge "$JOBS" ]; then
+ wait
+ running=0
+ fi
+}
+
+finish() {
+ wait
+ running=0
+ for file in "$results"/[0-9][0-9][0-9][0-9]; do
+ [ -f "$file" ] || continue
+ cat "$file"
+ failures=$((failures + $(grep -c '^FAIL' "$file")))
+ if [ ! -s "$file.status" ]; then
+ echo "FAIL row $(basename "$file"): killed before it finished"
+ failures=$((failures + 1))
+ fi
+ rm -f "$file" "$file.status"
+ done
+}
+
+# Each file with tests carries the fewest it may report, so a test that stops
+# being found (renamed so it no longer ends in `Test`, say) fails the gate.
+SPELLS="spells/basicSpells.qnt:6 spells/soup.qnt:4"
+MODULES="types.qnt wire.qnt indexer.qnt hub.qnt abstractHub.qnt hubMachine.qnt shim.qnt protocol.qnt"
+FUNCTIONAL="tests/wireTest.qnt:11 tests/indexerTest.qnt:14 tests/hubTest.qnt:27 tests/shimTest.qnt:13
+ tests/hubScenariosTest.qnt:28 tests/scenariosTest.qnt:21 tests/trustTest.qnt:12"
+
+fail() {
+ echo "FAIL $1"
+}
+
+# run_tests FILE:MIN: every test passes, and there are at least MIN.
+run_tests() {
+ file=${1%:*} least=${1##*:}
+ out=$($QUINT test "$file" --backend="$BACKEND" 2>&1)
+ status=$?
+ passing=$(echo "$out" | sed -n 's/^ *\([0-9][0-9]*\) passing.*/\1/p')
+ if [ "$status" -eq 0 ] && [ -n "$passing" ] && [ "$passing" -ge "$least" ]; then
+ echo "ok test $file: $passing passing"
+ elif [ "$status" -eq 0 ] && [ -n "$passing" ]; then
+ fail "test $file: $passing passing, expected at least $least"
+ else
+ echo "$out" | tail -25
+ fail "test $file"
+ fi
+}
+
+# simulate CONFIG STEP MAX_STEPS ARGS...: one simulation of $samples traces
+# from CONFIG's named init; the output is left in $out.
+samples=$SAMPLES
+simulate() {
+ main=$1 step=$2 steps=$3
+ shift 3
+ case $main in
+ baseline) init=initBaseline ;;
+ byzHub) init=initByzHub ;;
+ byzIndexer) init=initByzIndexer ;;
+ *) init=none ;;
+ esac
+ out=$($QUINT run protocol.qnt --backend="$BACKEND" --main=protocol --init="$init" --step="$step" \
+ --max-samples="$samples" --max-steps="$steps" --seed="$SEED" "$@" 2>&1)
+}
+
+# Classified by Quint's verdict line, so a crash, a download failure or a
+# misspelt name fails the gate instead of passing as a counterexample.
+verdict() {
+ case $out in
+ *"[ok] No violation found"*) got=holds ;;
+ *"[violation] Found an issue"*) got=fails ;;
+ *) got=none ;;
+ esac
+}
+
+# holds CONFIG INVARIANT...: all of them, together, under `step`.
+holds() {
+ main=$1
+ shift
+ simulate "$main" step 40 --invariants "$@"
+ verdict
+ case $got in
+ holds) echo "ok $main: holds: $*" ;;
+ fails)
+ echo "$out" | grep -a -E '^ *❌' | sed 's/^/ /'
+ fail "$main: expected to hold, violated (among: $*)"
+ ;;
+ *)
+ echo "$out" | tail -20
+ fail "$main: quint gave no verdict"
+ ;;
+ esac
+}
+
+# fails CONFIG STEP MAX_STEPS INVARIANT [TRACES]: violated in some trace of STEP.
+fails() {
+ samples=${5:-$SAMPLES}
+ simulate "$1" "$2" "$3" --invariant="$4"
+ verdict
+ case $got in
+ fails) echo "ok $1: fails: $4 ($2, $3 steps)" ;;
+ holds) fail "$1: $4 expected to fail under $2, no violation in $samples traces" ;;
+ *)
+ echo "$out" | tail -20
+ fail "$1: $4: quint gave no verdict"
+ ;;
+ esac
+}
+
+# The names after `--` in "$@", and the names before it.
+after_dashes() {
+ seen=0
+ for arg in "$@"; do
+ if [ "$seen" -eq 1 ]; then printf '%s ' "$arg"; fi
+ if [ "$arg" = "--" ]; then seen=1; fi
+ done
+}
+
+before_dashes() {
+ for arg in "$@"; do
+ if [ "$arg" = "--" ]; then break; fi
+ printf '%s ' "$arg"
+ done
+}
+
+# reaches CONFIG STEP MAX_STEPS WITNESS... -- INVARIANT...: every witness is
+# reached in at least one trace of STEP, and no invariant is violated on the
+# way.
+reaches() {
+ main=$1 step=$2 steps=$3
+ shift 3
+ witnesses=$(before_dashes "$@")
+ invariants=$(after_dashes "$@")
+ # shellcheck disable=SC2086
+ simulate "$main" "$step" "$steps" --witnesses $witnesses --invariants $invariants
+ verdict
+ case $got in
+ holds) ;;
+ fails)
+ echo "$out" | grep -a -E '^ *❌' | sed 's/^/ /'
+ fail "$main: an invariant was violated under $step (among: $invariants)"
+ return
+ ;;
+ *)
+ echo "$out" | tail -20
+ fail "$main: witnesses under $step: quint gave no verdict"
+ return
+ ;;
+ esac
+ for witness in $witnesses; do
+ count=$(echo "$out" | sed -n "s/^$witness was witnessed in \([0-9][0-9]*\) trace.*/\1/p")
+ if [ -z "$count" ]; then
+ fail "$main: witness $witness: no count reported"
+ elif [ "$count" -eq 0 ]; then
+ fail "$main: witness $witness never reached under $step in $samples traces"
+ else
+ echo "ok $main: reached: $witness ($count of $samples, $step, $steps steps)"
+ fi
+ done
+}
+
+# tlc_holds INIT STEP INVARIANT: TLC exhausts the configuration and finds
+# every reachable state satisfies the invariant.
+tlc_holds() {
+ out=$(QUINT=$QUINT sh ./tlc.sh hubMachine.qnt hubMachine "$1" "$2" "$3" 2>&1)
+ case $out in
+ "holds "*) echo "ok $1: holds, exhaustively: $3 ($2; states and depth: ${out#holds })" ;;
+ "violated "*) fail "$1: $3 expected to hold under $2, TLC found a counterexample of ${out#violated } states" ;;
+ *)
+ echo "$out" | tail -20
+ fail "$1: $3: tlc.sh gave no verdict"
+ ;;
+ esac
+}
+
+# tlc_violated INIT STEP INVARIANT LENGTH: TLC finds a counterexample, and it
+# is no longer than the recorded one. With one worker TLC searches breadth
+# first and its counterexample is a shortest one, so a longer one means the
+# recorded counterexample is gone.
+tlc_violated() {
+ out=$(QUINT=$QUINT TLC_WORKERS=1 sh ./tlc.sh hubMachine.qnt hubMachine "$1" "$2" "$3" 2>&1)
+ case $out in
+ "violated "*)
+ length=${out#violated }
+ if [ "$length" -le "$4" ]; then
+ echo "ok $1: violated: $3 ($2, $length states)"
+ else
+ fail "$1: $3 violated under $2 in $length states, recorded as $4"
+ fi
+ ;;
+ "holds "*) fail "$1: $3 expected to be violated under $2, TLC found it holds" ;;
+ *)
+ echo "$out" | tail -20
+ fail "$1: $3: tlc.sh gave no verdict"
+ ;;
+ esac
+}
+
+typecheck() {
+ if out=$($QUINT typecheck "$1" 2>&1); then
+ echo "ok typecheck $1"
+ else
+ echo "$out" | tail -20
+ fail "typecheck $1"
+ fi
+}
+
+# Quint, through npx, and its Rust evaluator are fetched on first use, into
+# caches that rows run in parallel would fill at the same time. One run here
+# fetches both before any row starts.
+echo "---- 0 toolchain"
+mkdir "$results/warm"
+printf 'module warm {\n var x: int\n action init = x'"'"' = 0\n action step = x'"'"' = x\n}\n' \
+ >"$results/warm/warm.qnt"
+if out=$($QUINT run "$results/warm/warm.qnt" --max-samples=1 --max-steps=1 --backend="$BACKEND" 2>&1); then
+ echo "ok quint $($QUINT --version 2>/dev/null), $BACKEND evaluator"
+else
+ echo "$out" | tail -25
+ fail "toolchain: quint run failed"
+ exit 1
+fi
+rm -rf "$results/warm"
+
+echo "---- 1 typecheck"
+for file in $SPELLS $MODULES $FUNCTIONAL; do
+ job typecheck "${file%:*}"
+done
+finish
+if [ "$failures" -ne 0 ]; then
+ exit "$failures"
+fi
+
+if [ "$TIERS" != tlc ]; then
+echo "---- 2 tests"
+for file in $SPELLS $FUNCTIONAL; do
+ job run_tests "$file"
+done
+finish
+
+echo "---- 3 invariants ($SAMPLES traces, seed $SEED)"
+
+# The guarantees, where they are claimed.
+job holds baseline operatorBlind queuedBytesConfidential txidAuthenticity lookupValidityPerHub
+job holds byzHub operatorBlind txidAuthenticity
+job holds byzIndexer operatorBlind txidAuthenticity
+
+# The known gaps, with every component honest.
+job fails baseline quietStep 40 statusNeverRegresses # K2
+
+finish
+
+echo "---- 3b witnesses ($SAMPLES traces, seed $SEED)"
+
+BASELINE_HOLDS="operatorBlind queuedBytesConfidential txidAuthenticity lookupValidityPerHub"
+
+# The accepted disclosure, a third party served a published body, and the
+# antecedents of G1 and G2. The served body is G2's reply-body branch, which
+# `vQueuedBytesConfidential` does not reach on its own.
+job reaches baseline step 40 \
+ wQueuedDisclosed wThirdPartyServedBody \
+ vOperatorBlind vQueuedBytesConfidential \
+ -- $BASELINE_HOLDS
+# The antecedent of G3, and G4's under a step that keeps to one migration.
+job reaches baseline quietStep 80 \
+ vTxidAuthenticity \
+ -- $BASELINE_HOLDS
+job reaches baseline earlyLookupStep 40 \
+ vLookupValidityPerHub \
+ -- $BASELINE_HOLDS
+
+# A twin served, and a transaction served at a false height.
+job reaches byzHub quietStep 40 \
+ vOperatorBlind vTxidAuthenticity wTwinServed wFalseHeightServed \
+ -- operatorBlind txidAuthenticity
+job reaches byzIndexer quietStep 40 \
+ vOperatorBlind vTxidAuthenticity \
+ -- operatorBlind txidAuthenticity
+finish
+fi
+
+if [ "$TIERS" != simulation ]; then
+echo "---- 4 hub specification (TLC, exhaustive)"
+
+# Fetched once here, not by the first rows: rows run in parallel would unpack
+# it into ~/.quint at the same time.
+if ! QUINT=$QUINT sh ./tlc.sh --fetch; then
+ exit 1
+fi
+
+G6B=conformingFirstOfferBeforeExpiry
+G6C=conformingFirstOfferJudgedBeforeExpiry
+K5=ackedIsHeldOrSettled
+K6=conformingEveryOfferBeforeExpiry
+
+# The schedule guarantees with every component honest: under a timely tip;
+# under a tip that may be reported behind the chain; and with a slow flight as
+# well, the one about the offer.
+job tlc_holds initTimely step "$G6B and $G6C"
+job tlc_holds initTimely step $K6
+job tlc_holds initFlakyTip step "$G6B and $G6C"
+job tlc_holds initFlakyTipSlowFlight step $G6B
+
+# The known gaps, each on the configuration that isolates its cause. The last
+# argument is the length of TLC's counterexample.
+job tlc_violated initFlakyTipNoSlack step $G6B 12 # K3'
+job tlc_violated initFlakyTipSlowFlight step $G6C 14 # K7
+job tlc_violated initStaleLag step $G6B 13 # K4
+job tlc_violated initStaleLag step $G6C 14 # K4
+job tlc_violated initStaleLag step $K6 13 # K6
+job tlc_violated initStaleLagWithSlack step $G6B 19 # finding 2
+job tlc_violated initStaleLagWithSlack step $G6C 20 # finding 2
+# K5, three causes: a crash; without one, a final flush nothing judged; with
+# no shutdown either, a requeue that gives the entry up as expired.
+job tlc_violated initTimely step $K5 5
+job tlc_violated initTimely noCrashStep $K5 8
+job tlc_violated initTimely quietStep $K5 12
+
+# The trust matrix: each schedule guarantee is violated once the component it
+# depends on is Byzantine.
+job tlc_violated initByzHub step $G6B 12
+job tlc_violated initByzHub step $G6C 13
+job tlc_violated initByzIndexer step $G6B 16
+job tlc_violated initByzIndexer step $G6C 17
+
+# Reachability. The antecedents of G6b and G6c, so that a "holds" is not
+# vacuous; and one state per family of steps, because TLC runs with deadlock
+# checking off and a machine whose steps died would hold everything.
+job tlc_violated initTimely step "not(wConformingFirstOffer)" 6
+job tlc_violated initTimely step "not(wConformingFirstOfferInFlightABlock)" 7
+job tlc_violated initTimely step "not(wOffered)" 7
+job tlc_violated initTimely step "not(wRequeued)" 9
+job tlc_violated initTimely step "not(wDown)" 2
+job tlc_violated initTimely step "not(wRestartedOwing)" 6
+job tlc_violated initTimely step "not(wBlockInFlight)" 7
+job tlc_violated initTimely step "not(wStopped)" 4
+job tlc_violated initFlakyTip step "not(wConformingFirstOffer)" 6
+job tlc_violated initFlakyTip step "not(wConformingFirstOfferInFlightABlock)" 7
+job tlc_violated initFlakyTip step "not(wOffered)" 7
+job tlc_violated initFlakyTip step "not(wRequeued)" 9
+job tlc_violated initFlakyTip step "not(wDown)" 2
+job tlc_violated initFlakyTip step "not(wRestartedOwing)" 6
+job tlc_violated initFlakyTip step "not(wBlockInFlight)" 7
+job tlc_violated initFlakyTip step "not(wStopped)" 4
+job tlc_violated initFlakyTip step "not(wTimelyQueuedBehindEpoch)" 6
+job tlc_violated initFlakyTipSlowFlight step "not(wConformingFirstOffer)" 6
+job tlc_violated initFlakyTipSlowFlight step "not(wBlockInFlight)" 7
+job tlc_violated initStaleLag step "not(wStale)" 6
+job tlc_violated initStaleLagWithSlack step "not(wStale)" 6
+finish
+fi
+
+exit "$failures"
diff --git a/zeronym/spec/quint/hub.qnt b/zeronym/spec/quint/hub.qnt
new file mode 100644
index 00000000..2884f93b
--- /dev/null
+++ b/zeronym/spec/quint/hub.qnt
@@ -0,0 +1,447 @@
+// -*- mode: Bluespec; -*-
+
+/// The hub: it admits diverted transactions into a queue held in memory,
+/// answers lookups, and publishes the whole queue at once on a block cadence.
+///
+/// The hub is one total function, `hub(state, input)`, from its state and one
+/// input to its next state and one output. Each input is one thing that can
+/// happen to a hub (a frame arrives, a tip is observed, a flush becomes due, a
+/// verdict comes back) and corresponds to one seam in the implementation. An
+/// input that makes no sense in the current state returns `HubErrorOutput` and
+/// leaves the state alone.
+///
+/// `byzHubResults` is the wider relation a Byzantine hub draws from.
+module hub {
+ import basicSpells.* from "./spells/basicSpells"
+ import types.* from "./types"
+
+ // ------------------------------------------------------------------------
+ // State
+ // ------------------------------------------------------------------------
+
+ /// The schedule a hub is started with.
+ ///
+ /// `deliveryLag` and `minWalletExpiry` are not read by any transition. They
+ /// are the wallet-side budget the schedule is validated against at startup
+ /// (`scheduleFitsBudget`), and the properties read them from here.
+ type HubParams = {
+ flushInterval: int, // blocks between scheduled flushes
+ miningMargin: int, // blocks a published transaction needs to be mined
+ deliveryLag: int, // blocks a submission may take to arrive
+ minWalletExpiry: int, // the smallest expiry delta a supported wallet sets
+ reorgAllowance: int, // how far back a tip report is followed
+ maxAttempts: int, // requeues an entry is allowed
+ }
+
+ /// The startup check: a transaction that takes `deliveryLag` blocks to
+ /// arrive, waits a full interval and needs `miningMargin` blocks to be mined
+ /// still fits inside the smallest supported expiry.
+ pure def scheduleFitsBudget(params: HubParams): bool =
+ params.flushInterval + params.miningMargin + params.deliveryLag <= params.minWalletExpiry
+
+ /// Where the process is in its life. `Starting` has not seen a tip yet;
+ /// `Stale` has seen no forward tip progress for the staleness window;
+ /// `Draining` has had its shutdown signal and owes one final flush;
+ /// `Stopped` has done it.
+ type Phase = Down | Starting | Running | Stale | Draining | Stopped
+
+ /// The clock the flush schedule runs on. It follows the observed tip until
+ /// the hub is stale, and then free-runs from an estimate of elapsed time.
+ /// Admission and requeue never use it: they read the observed tip.
+ type Cadence = Tracking | FreeRunning(Height)
+
+ /// The flush cycle. While broadcasting, `batch` holds the entries still
+ /// waiting for a verdict and `unplaced` those nothing judged; both map a
+ /// payload to the requeues it has had. `final` marks the shutdown flush.
+ type Flush =
+ | Idle
+ | Broadcasting({ batch: Payload -> int, unplaced: Payload -> int, final: bool })
+
+ /// - `tip`: the last tip observed, absent until the first observation.
+ /// - `queue`: the admitted entries, keyed by their bytes, each with the
+ /// number of requeues it has had.
+ /// - `lastEpoch`: the flush epoch last acted on, absent until adopted.
+ type HubState = {
+ params: HubParams,
+ phase: Phase,
+ tip: Option[Height],
+ cadence: Cadence,
+ queue: Payload -> int,
+ flush: Flush,
+ lastEpoch: Option[int],
+ }
+
+ /// A hub that is not running. It holds nothing: the queue lives in memory.
+ pure def downHub(params: HubParams): HubState = {
+ params: params,
+ phase: Down,
+ tip: None,
+ cadence: Tracking,
+ queue: Map(),
+ flush: Idle,
+ lastEpoch: None,
+ }
+
+ /// A hub that has just started and has not yet seen a tip.
+ pure def startingHub(params: HubParams): HubState =
+ { ...downHub(params), phase: Starting }
+
+ // ------------------------------------------------------------------------
+ // Inputs and outputs
+ // ------------------------------------------------------------------------
+
+ type HubInput =
+ | SubmitHInput({ nonce: Nonce, payload: Payload })
+ // A lookup, together with what the hub's indexer would answer. The answer
+ // is used only when the queue misses.
+ | LookupHInput({ nonce: Nonce, txid: TxId, answer: IndexerAnswer })
+ | TipHInput(Height) // the cadence loop observes a tip
+ // No forward tip progress for the staleness window. The height is what
+ // the free-running cadence clock now reads.
+ | StaleHInput(Height)
+ | FlushDueHInput // the cadence loop finds a flush due
+ | VerdictHInput({ payload: Payload, verdict: Verdict })
+ | FlushDoneHInput // every entry of the batch has a verdict
+ | DrainHInput // shutdown signal
+ | CrashHInput
+ | RestartHInput
+
+ type HubOutput =
+ | AckOutput({ nonce: Nonce, kind: AckKind })
+ | LookupReplyOutput({ nonce: Nonce, outcome: HubOutcome })
+ | BroadcastOutput(Set[Payload])
+ | RequeuedOutput({ held: int, droppedExpired: int, droppedExhausted: int })
+ | NoHubOutput
+ | HubErrorOutput(str)
+
+ type HubResult = Result[HubState, HubOutput]
+
+ pure def toAckOutput(state: HubState, nonce: Nonce, kind: AckKind): HubResult =
+ { state: state, out: AckOutput({ nonce: nonce, kind: kind }) }
+
+ pure def toLookupReplyOutput(state: HubState, nonce: Nonce, outcome: HubOutcome): HubResult =
+ { state: state, out: LookupReplyOutput({ nonce: nonce, outcome: outcome }) }
+
+ pure def toBroadcastOutput(state: HubState, batch: Set[Payload]): HubResult =
+ { state: state, out: BroadcastOutput(batch) }
+
+ pure def toRequeuedOutput(state: HubState, held: int, droppedExpired: int, droppedExhausted: int): HubResult = {
+ state: state,
+ out: RequeuedOutput({ held: held, droppedExpired: droppedExpired, droppedExhausted: droppedExhausted }),
+ }
+
+ pure def toNoHubOutput(state: HubState): HubResult =
+ { state: state, out: NoHubOutput }
+
+ pure def toHubErrorOutput(state: HubState, reason: str): HubResult =
+ { state: state, out: HubErrorOutput(reason) }
+
+ // ------------------------------------------------------------------------
+ // Views
+ // ------------------------------------------------------------------------
+
+ /// Whether the hub answers frames at all.
+ pure def isServing(state: HubState): bool =
+ state.phase != Down and state.phase != Stopped
+
+ /// Whether the tip cannot be trusted: none has been observed, or the hub is
+ /// stale and its cadence is free-running.
+ pure def isTipStale(state: HubState): bool =
+ state.tip == None or state.cadence != Tracking
+
+ /// The last observed tip. Read only where a tip has been observed.
+ pure def observedTip(state: HubState): Height =
+ state.tip.unwrapOr(0)
+
+ /// The height the flush schedule runs on.
+ pure def cadenceHeight(state: HubState): Height =
+ match state.cadence {
+ | Tracking => state.observedTip()
+ | FreeRunning(height) => height
+ }
+
+ /// The flush epoch the cadence clock is in.
+ pure def cadenceEpoch(state: HubState): int =
+ state.cadenceHeight() / state.params.flushInterval
+
+ /// The payloads waiting in the queue.
+ pure def queued(state: HubState): Set[Payload] =
+ state.queue.keys()
+
+ /// The payloads out with a flush: awaiting a verdict, or awaiting requeue.
+ pure def inFlight(state: HubState): Set[Payload] =
+ match state.flush {
+ | Idle => Set()
+ | Broadcasting(flush) => flush.batch.keys().union(flush.unplaced.keys())
+ }
+
+ /// Whether a lookup for `txid` hits the queue. An entry whose bytes do not
+ /// parse has no txid and is never hit.
+ pure def isQueuedTxid(state: HubState, txid: TxId): bool =
+ state.queued().exists(payload => payload.txid == Some(txid))
+
+ /// Whether the cadence loop would start a flush now: the cadence clock has
+ /// crossed into a new epoch, or the hub is draining and owes its final one.
+ pure def isFlushDue(state: HubState): bool =
+ and {
+ state.flush == Idle,
+ or {
+ state.phase == Draining,
+ and {
+ state.phase == Running or state.phase == Stale,
+ match state.lastEpoch {
+ | Some(epoch) => state.cadenceEpoch() > epoch
+ | None => false
+ },
+ },
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Admission
+ // ------------------------------------------------------------------------
+
+ /// The next height at which a flush is scheduled, strictly after `height`.
+ pure def nextFlushHeight(height: Height, flushInterval: int): Height =
+ (height / flushInterval + 1) * flushInterval
+
+ /// Whether an entry with `expiry`, judged at `tip`, provably survives the
+ /// flush that would publish it with `miningMargin` blocks to spare. A
+ /// transaction with no expiry always does.
+ pure def survivesNextFlush(expiry: Option[Height], tip: Height, flushInterval: int, miningMargin: int): bool =
+ match expiry {
+ | None => true
+ | Some(height) => height >= nextFlushHeight(tip, flushInterval) + miningMargin
+ }
+
+ /// The hub's decision on a submission, in the order the checks are made. No
+ /// check asks a node anything: admission must not leak a transaction's
+ /// arrival.
+ pure def admission(state: HubState, payload: Payload): AckKind =
+ if (state.isTipStale())
+ Refused(TipStale)
+ else if (state.phase == Draining)
+ Refused(HubDraining)
+ else if (not(survivesNextFlush(payload.expiry, state.observedTip(), state.params.flushInterval, state.params.miningMargin)))
+ Refused(ExpiryTooTight)
+ else if (state.queued().contains(payload))
+ Duplicate
+ else
+ Admitted
+
+ // ------------------------------------------------------------------------
+ // Tip
+ // ------------------------------------------------------------------------
+
+ /// The cadence loop observes `height`. The first observation is adopted,
+ /// with its epoch, and nothing is flushed. After that a forward move is
+ /// followed and ends staleness; a move back within the reorg allowance is
+ /// followed and does not; a larger move back is ignored.
+ pure def observeTip(state: HubState, height: Height): HubResult =
+ match state.tip {
+ | None =>
+ if (state.phase == Starting)
+ { ...state,
+ phase: Running,
+ tip: Some(height),
+ lastEpoch: Some(height / state.params.flushInterval),
+ }.toNoHubOutput()
+ else state.toHubErrorOutput("no cadence loop is running")
+ | Some(tip) =>
+ if (state.phase != Running and state.phase != Stale)
+ state.toHubErrorOutput("no cadence loop is running")
+ else if (state.flush != Idle)
+ state.toHubErrorOutput("the tip is not observed during a flush")
+ else if (height > tip)
+ { ...state, phase: Running, tip: Some(height), cadence: Tracking }.toNoHubOutput()
+ else if (tip - height <= state.params.reorgAllowance)
+ { ...state, tip: Some(height) }.toNoHubOutput()
+ else
+ state.toNoHubOutput()
+ }
+
+ /// The staleness window passes with no forward progress, or passes further:
+ /// the cadence clock free-runs and now reads `height`. The estimate starts at
+ /// or above the observed tip and never runs backwards.
+ pure def freeRun(state: HubState, height: Height): HubResult =
+ if (state.flush != Idle)
+ state.toHubErrorOutput("the cadence clock is not read during a flush")
+ else
+ match state.cadence {
+ | Tracking =>
+ if (state.phase == Running and height >= state.observedTip())
+ { ...state, phase: Stale, cadence: FreeRunning(height) }.toNoHubOutput()
+ else state.toHubErrorOutput("not a running hub, or an estimate below the observed tip")
+ | FreeRunning(estimate) =>
+ if (state.phase == Stale and height >= estimate)
+ { ...state, cadence: FreeRunning(height) }.toNoHubOutput()
+ else state.toHubErrorOutput("not a stale hub, or an estimate that runs backwards")
+ }
+
+ // ------------------------------------------------------------------------
+ // Flush
+ // ------------------------------------------------------------------------
+
+ /// A flush begins: the whole queue moves out at once. An empty queue is
+ /// still a flush event, and the epoch is recorded. The final flush of a
+ /// draining hub with nothing to publish stops it.
+ pure def beginFlush(state: HubState): HubResult =
+ if (not(state.isFlushDue()))
+ state.toHubErrorOutput("no flush is due")
+ else if (state.queue == Map())
+ if (state.phase == Draining)
+ { ...state, phase: Stopped }.toNoHubOutput()
+ else
+ { ...state, lastEpoch: Some(state.cadenceEpoch()) }.toNoHubOutput()
+ else
+ { ...state,
+ queue: Map(),
+ flush: Broadcasting({ batch: state.queue, unplaced: Map(), final: state.phase == Draining }),
+ }.toBroadcastOutput(state.queued())
+
+ /// The indexer's verdict on one entry. Accepted and already-known entries
+ /// are published and leave; a rejected entry is dropped; a retryable one is
+ /// set aside for requeue.
+ pure def takeVerdict(state: HubState, payload: Payload, verdict: Verdict): HubResult =
+ match state.flush {
+ | Idle => state.toHubErrorOutput("no flush is in flight")
+ | Broadcasting(flush) =>
+ if (not(flush.batch.keys().contains(payload)))
+ state.toHubErrorOutput("the payload is not awaiting a verdict")
+ else
+ val attempts = flush.batch.get(payload)
+ { ...state,
+ flush: Broadcasting({ ...flush,
+ batch: flush.batch.mapRemove(payload),
+ unplaced: if (verdict == Retryable) flush.unplaced.put(payload, attempts) else flush.unplaced,
+ }),
+ }.toNoHubOutput()
+ }
+
+ /// A flush ends: the entries nothing judged go back into the queue, each
+ /// decided on its own.
+ ///
+ /// - The same bytes already resident (resubmitted during the flush) win, and
+ /// the returning copy is dropped without being counted.
+ /// - An entry that no longer survives the next flush, judged at the observed
+ /// tip exactly as admission judges it, is dropped as expired.
+ /// - An entry out of attempts is dropped as exhausted. Only an entry with no
+ /// expiry gets that far.
+ /// - The rest are held.
+ ///
+ /// After the final flush the process exits and whatever was held is lost.
+ pure def endFlush(state: HubState): HubResult =
+ match state.flush {
+ | Idle => state.toHubErrorOutput("no flush is in flight")
+ | Broadcasting(flush) =>
+ if (flush.batch != Map())
+ state.toHubErrorOutput("entries are still awaiting a verdict")
+ else
+ val params = state.params
+ val returning = flush.unplaced.keys().exclude(state.queued())
+ val expired = returning.filter(payload =>
+ not(survivesNextFlush(payload.expiry, state.observedTip(), params.flushInterval, params.miningMargin)))
+ val exhausted = returning.exclude(expired).filter(payload =>
+ flush.unplaced.get(payload) + 1 > params.maxAttempts)
+ val held = returning.exclude(expired).exclude(exhausted)
+ val queue = state.queued().union(held).mapBy(payload =>
+ if (held.contains(payload)) flush.unplaced.get(payload) + 1 else state.queue.get(payload))
+ val idle =
+ if (flush.final) { ...state, phase: Stopped, queue: Map(), flush: Idle }
+ else { ...state, queue: queue, flush: Idle, lastEpoch: Some(state.cadenceEpoch()) }
+ idle.toRequeuedOutput(held.size(), expired.size(), exhausted.size())
+ }
+
+ // ------------------------------------------------------------------------
+ // The hub function
+ // ------------------------------------------------------------------------
+
+ pure def hub(state: HubState, input: HubInput): HubResult =
+ match input {
+ | SubmitHInput(submit) =>
+ if (not(state.isServing()))
+ state.toHubErrorOutput("the hub is not serving")
+ else
+ val kind = admission(state, submit.payload)
+ // The entry is resident before the ack exists: an accepted ack is a
+ // promise that the hub holds the bytes.
+ val admitted =
+ if (kind == Admitted) { ...state, queue: state.queue.put(submit.payload, 0) } else state
+ admitted.toAckOutput(submit.nonce, kind)
+
+ | LookupHInput(lookup) =>
+ if (not(state.isServing()))
+ state.toHubErrorOutput("the hub is not serving")
+ // The queue first: a diverted transaction that has not been flushed
+ // exists nowhere else. Then the indexer, whose answer is forwarded.
+ else if (state.isQueuedTxid(lookup.txid))
+ state.toLookupReplyOutput(lookup.nonce, QueueHit)
+ else
+ state.toLookupReplyOutput(lookup.nonce, FromIndexer(lookup.answer))
+
+ | TipHInput(height) => observeTip(state, height)
+
+ | StaleHInput(height) => freeRun(state, height)
+
+ | FlushDueHInput => beginFlush(state)
+
+ | VerdictHInput(judged) => takeVerdict(state, judged.payload, judged.verdict)
+
+ | FlushDoneHInput => endFlush(state)
+
+ | DrainHInput =>
+ // Admission closes first; a flush already in flight finishes, and then
+ // the final one runs.
+ if (state.phase == Running or state.phase == Stale)
+ { ...state, phase: Draining }.toNoHubOutput()
+ else state.toHubErrorOutput("only a running hub can be drained")
+
+ | CrashHInput =>
+ if (state.phase == Down) state.toHubErrorOutput("the hub is already down")
+ else downHub(state.params).toNoHubOutput()
+
+ | RestartHInput =>
+ if (state.phase == Down) startingHub(state.params).toNoHubOutput()
+ else state.toHubErrorOutput("the hub is already up")
+ }
+
+ // ------------------------------------------------------------------------
+ // Byzantine relation
+ // ------------------------------------------------------------------------
+
+ /// The transitions of a Byzantine hub. It keeps the honest schedule, and is
+ /// free in what it tells its clients and in what it admits:
+ ///
+ /// - a submission is admitted or refused whatever the admission rules say,
+ /// and the ack says which;
+ /// - a lookup is answered with any outcome: a queue hit, or anything an
+ /// indexer could say, with a body drawn from `universe` or none, at any
+ /// height.
+ ///
+ /// The honest transition is always a member.
+ pure def byzHubResults(
+ state: HubState,
+ input: HubInput,
+ universe: Set[Payload],
+ ): Set[HubResult] =
+ val honest = Set(hub(state, input))
+ if (not(state.isServing())) honest
+ else
+ match input {
+ | SubmitHInput(submit) =>
+ val admitted =
+ if (state.queued().contains(submit.payload)) state.toAckOutput(submit.nonce, Duplicate)
+ else { ...state, queue: state.queue.put(submit.payload, 0) }.toAckOutput(submit.nonce, Admitted)
+ val refused = Set(TipStale, HubDraining, ExpiryTooTight).map(refusal =>
+ state.toAckOutput(submit.nonce, Refused(refusal)))
+ honest.union(Set(admitted)).union(refused)
+ | LookupHInput(lookup) =>
+ val bodies = Set(None).union(universe.map(payload => Some(payload)))
+ val answers = tuples(bodies, WIRE_HEIGHTS)
+ .map(((body, claimed)) => IFound({ body: body, height: claimed }))
+ .union(Set(INotFound, IUnavailable))
+ val outcomes = Set(QueueHit).union(answers.map(answer => FromIndexer(answer)))
+ honest.union(outcomes.map(outcome => state.toLookupReplyOutput(lookup.nonce, outcome)))
+ | _ => honest
+ }
+}
diff --git a/zeronym/spec/quint/hubMachine.qnt b/zeronym/spec/quint/hubMachine.qnt
new file mode 100644
index 00000000..7725eb56
--- /dev/null
+++ b/zeronym/spec/quint/hubMachine.qnt
@@ -0,0 +1,748 @@
+// -*- mode: Bluespec; -*-
+
+/// The hub specification: one hub, the chain it publishes to, and the two
+/// things it asks its indexer (what the tip is, and what became of a
+/// broadcast). Submissions are inputs: who sent one, and over what network,
+/// is the protocol specification's business.
+///
+/// This is where the schedule is checked: whether a transaction a hub admits
+/// is offered to the chain, and judged by a node, before it expires. The
+/// state is small enough for TLC to visit every reachable state of every
+/// configuration, so "holds" here means exactly that.
+///
+/// How it is built. The module holds no hub logic. Every step picks an input,
+/// hands it to `hub(state, input)` and records what an observer needs. A step
+/// exists in two forms: `xWith(..)`, which takes every choice as a parameter
+/// and is what a scripted run is made of, and `x`, which picks the choices and
+/// is what `step` is made of.
+///
+/// A configuration is a value, held in the state and set once by `initWith`.
+/// One named init per configuration (`initTimely`, ...) selects it, guarded by
+/// the assumptions that configuration is checked under.
+///
+/// The observer's memory is four sets of payloads and one height. It is never
+/// read by a step: only the properties read it.
+module hubMachine {
+ import basicSpells.* from "./spells/basicSpells"
+ import types.* from "./types"
+ import indexer.* from "./indexer"
+ import hub.* from "./hub"
+
+ // ------------------------------------------------------------------------
+ // Configuration
+ // ------------------------------------------------------------------------
+
+ /// - `payloads`: the transactions that may be submitted.
+ /// - `params`: the schedule the hub is started with.
+ /// - `staleWindow`: blocks without a forward tip observation after which a
+ /// hub is stale.
+ /// - `maxFlightBlocks`: blocks that may arrive while one flush is in flight.
+ /// - `maxHeight`: where the chain stops growing; a bound of the model.
+ /// - `tip`: how the hub's view of the tip relates to the true height.
+ type HubConfig = {
+ payloads: Set[Payload],
+ params: HubParams,
+ staleWindow: int,
+ maxFlightBlocks: int,
+ maxHeight: Height,
+ tip: TipModel,
+ hubRole: Role,
+ indexerRole: Role,
+ }
+
+ /// The height the chain starts at. Height 0 is kept for "in the mempool".
+ pure val GENESIS_HEIGHT = 1
+
+ /// Every height a tip report or a free-running clock may carry, in any
+ /// configuration. Picks are drawn from this fixed range and filtered by the
+ /// configuration, so no range has a bound that depends on the state.
+ pure val CLOCK_HEIGHTS = 0.to(16)
+
+ // ------------------------------------------------------------------------
+ // Assumptions
+ // ------------------------------------------------------------------------
+ //
+ // Each is a predicate over a configuration. A named init asserts the ones
+ // its configuration is checked under, so a configuration that does not meet
+ // them has no initial state and every check of it fails.
+
+ /// The hub's startup check: delivery, one full interval and the mining
+ /// margin fit inside the smallest supported expiry.
+ pure def budgetFits(c: HubConfig): bool =
+ scheduleFitsBudget(c.params)
+
+ /// The same budget with the reorg allowance added. A hub that follows a tip
+ /// report up to the allowance behind the chain can flush that much late.
+ /// Nothing in the implementation checks this; its shipped constants meet it
+ /// with equality.
+ pure def reorgSlackFits(c: HubConfig): bool =
+ c.params.flushInterval + c.params.miningMargin + c.params.deliveryLag + c.params.reorgAllowance
+ <= c.params.minWalletExpiry
+
+ /// Fewer blocks arrive while a flush is in flight than the mining margin
+ /// reserves. The margin is measured from the height at which a flush begins;
+ /// every block that arrives before the node judges a transaction is taken
+ /// out of it. The implementation bounds each call to the indexer
+ /// (`RPC_TIMEOUT`, `zeronym/hub/src/chain.rs`) and not the batch as a whole,
+ /// and bounds neither in blocks, so this is an assumption about the
+ /// environment that the code does not enforce.
+ pure def flightWithinMargin(c: HubConfig): bool =
+ c.maxFlightBlocks < c.params.miningMargin
+
+ /// The same budget with the longest silence that does not yet make a hub
+ /// stale. The shipped constants do not meet it.
+ pure def staleSlackFits(c: HubConfig): bool =
+ c.params.flushInterval + c.params.miningMargin + c.params.deliveryLag + (c.staleWindow - 1)
+ <= c.params.minWalletExpiry
+
+ /// The relations between the shipped constants that the scaled-down schedule
+ /// keeps: the slack left by the startup budget equals the reorg allowance;
+ /// the staleness window exceeds both the margin and that slack; the budget
+ /// with the longest non-stale silence added exceeds the expiry floor by
+ /// exactly one block, and without the margin it fits.
+ pure def shippedRelationsKept(c: HubConfig): bool =
+ val budget = c.params.flushInterval + c.params.miningMargin + c.params.deliveryLag
+ and {
+ c.params.minWalletExpiry - budget == c.params.reorgAllowance,
+ c.staleWindow > c.params.miningMargin,
+ c.staleWindow > c.params.reorgAllowance,
+ budget + (c.staleWindow - 1) == c.params.minWalletExpiry + 1,
+ budget - c.params.miningMargin + (c.staleWindow - 1) <= c.params.minWalletExpiry,
+ }
+
+ /// What every configuration meets: the startup budget; a schedule that
+ /// moves; payloads told apart by their bytes and, where they parse, by their
+ /// txid, none built before the chain starts; and a clock range wide enough
+ /// for a free-running clock one interval past the last block.
+ pure def standingAssumptions(c: HubConfig): bool = and {
+ budgetFits(c),
+ c.params.flushInterval > 0,
+ c.payloads.size() == c.payloads.map(payload => payload.id).size(),
+ c.payloads.filter(payload => isSome(payload.txid)).size() == txidsOf(c.payloads).size(),
+ c.payloads.forall(payload => payload.created >= GENESIS_HEIGHT),
+ CLOCK_HEIGHTS.contains(c.maxHeight + c.params.flushInterval),
+ }
+
+ /// The shipped relations, with the slack and the flight bound they give.
+ pure def shippedAssumptions(c: HubConfig): bool = and {
+ standingAssumptions(c),
+ shippedRelationsKept(c),
+ reorgSlackFits(c),
+ flightWithinMargin(c),
+ not(staleSlackFits(c)),
+ }
+
+ // ------------------------------------------------------------------------
+ // State
+ // ------------------------------------------------------------------------
+
+ /// The configuration. Written by `initWith` and by nothing else.
+ var cfg: HubConfig
+ /// The hub. Only ever the state of a result of `hub`.
+ var h: HubState
+ /// The true chain height.
+ var height: Height
+ /// The payloads a node has taken.
+ var onChain: Set[Payload]
+ /// Whether the cadence loop has asked for the tip since the last block.
+ var polled: bool
+ /// The true height at which the flush in flight began; 0 while none is.
+ var flightStart: Height
+
+ // The observer's memory.
+
+ /// The payloads that have entered this hub's queue since it last came up.
+ var seen: Set[Payload]
+ /// Those that first did so within the delivery lag of the height they were
+ /// built at.
+ var onTime: Set[Payload]
+ /// The payloads a flight of this run of the process has carried, once that
+ /// flight has had a node's answer for them or has ended. `seen`, `onTime`
+ /// and `offered` are forgotten together when the hub goes down, as its
+ /// queue is: a hub cannot be held to an arrival it no longer knows of, and
+ /// a restarted hub's entries start again at no attempts
+ /// (`zeronym/hub/src/queue.rs:334`).
+ var offered: Set[Payload]
+ /// The payloads acknowledged as accepted that no node has judged since.
+ var owed: Set[Payload]
+
+ action initWith(c: HubConfig): bool = all {
+ cfg' = c,
+ h' = startingHub(c.params),
+ height' = GENESIS_HEIGHT,
+ onChain' = Set(),
+ polled' = false,
+ flightStart' = 0,
+ seen' = Set(),
+ onTime' = Set(),
+ offered' = Set(),
+ owed' = Set(),
+ }
+
+ // ------------------------------------------------------------------------
+ // Views
+ // ------------------------------------------------------------------------
+
+ /// The chain as the indexer relations read it. Every transaction a node has
+ /// taken is in the mempool: nothing here depends on its being mined.
+ def chain: IndexerState = {
+ height: height,
+ txs: onChain.fold(Map(), (txs, payload) =>
+ match payload.txid {
+ | Some(txid) => txs.put(txid, { payload: payload, at: InMempool })
+ | None => txs
+ }),
+ offered: Set(),
+ }
+
+ /// How far behind the chain the hub's observed tip is.
+ def lag: int = height - h.observedTip()
+
+ /// The entries of the batch still waiting for a verdict.
+ def awaiting: Set[Payload] =
+ match h.flush {
+ | Broadcasting(flush) => flush.batch.keys()
+ | Idle => Set()
+ }
+
+ pure def isError(output: HubOutput): bool =
+ match output {
+ | HubErrorOutput(_) => true
+ | _ => false
+ }
+
+ /// Whether `output` is an ack that promises the hub holds the payload.
+ pure def isAcceptedAck(output: HubOutput): bool =
+ match output {
+ | AckOutput(ack) => isAccepted(ack.kind)
+ | _ => false
+ }
+
+ // ------------------------------------------------------------------------
+ // The oracles
+ // ------------------------------------------------------------------------
+ //
+ // The hub asks its indexer two things. Both answers are the relations of
+ // `indexer.qnt`, not a second model of them: the honest one, or, for a
+ // Byzantine indexer, the wider one.
+
+ /// The tips the indexer may report now.
+ def tips: Set[Height] =
+ match cfg.indexerRole {
+ | Honest =>
+ honestTips(chain, if (cfg.tip == TipMayRegress) cfg.params.reorgAllowance else 0, CLOCK_HEIGHTS)
+ | Byzantine => byzTips(CLOCK_HEIGHTS)
+ }
+
+ /// What a broadcast of `payload` may come to: the verdict the hub is given,
+ /// and whether the network took the transaction.
+ def broadcastResults(payload: Payload): Set[IndexerResult] =
+ match cfg.indexerRole {
+ | Honest => honestIndexerResults(chain, BroadcastIInput(payload))
+ | Byzantine => byzIndexerResults(chain, BroadcastIInput(payload), cfg.payloads)
+ }
+
+ /// The indexer's transition that gives `given` on `payload` and relays the
+ /// transaction to the network, or does not.
+ def broadcastResult(payload: Payload, given: Verdict, relayed: bool): IndexerResult = {
+ state: indexerApply(chain, BroadcastIInput(payload), VerdictOutput(if (relayed) Accepted else Retryable)),
+ out: VerdictOutput(given),
+ }
+
+ /// The verdicts on `payload`, each with whether the network took it.
+ def verdictsOn(payload: Payload): Set[(Verdict, bool)] =
+ tuples(Set(Accepted, AlreadyKnown, Rejected, Retryable), Set(true, false)).filter(((given, relayed)) =>
+ broadcastResults(payload).contains(broadcastResult(payload, given, relayed)))
+
+ /// The heights a stale hub's free-running clock may read now: not behind
+ /// the chain, and at most one flush interval ahead of it. The
+ /// implementation relies on the first ("during a real stall blocks arrive
+ /// slower than this", `zeronym/hub/src/batcher.rs:64-67`) and enforces
+ /// neither.
+ def freeRunEstimates: Set[Height] =
+ CLOCK_HEIGHTS.filter(estimate => height <= estimate and estimate <= height + cfg.params.flushInterval)
+
+ /// The transitions the hub may take on a submission of `payload`: the one
+ /// the protocol prescribes, or, for a Byzantine hub, any decision with the
+ /// payload queued or not. A Byzantine hub keeps the honest schedule.
+ def submitResults(payload: Payload): Set[HubResult] =
+ val input = SubmitHInput({ nonce: 0, payload: payload })
+ match cfg.hubRole {
+ | Honest => Set(hub(h, input))
+ | Byzantine => byzHubResults(h, input, cfg.payloads)
+ }
+
+ // ------------------------------------------------------------------------
+ // Frames
+ // ------------------------------------------------------------------------
+
+ action chainKept = all { height' = height, onChain' = onChain, polled' = polled }
+ action admissionsKept = all { seen' = seen, onTime' = onTime }
+ /// The hub went down. `owed` is kept: an acknowledged payload lost with the
+ /// process is K5.
+ action runForgotten = all { seen' = Set(), onTime' = Set(), offered' = Set() }
+ action memoryKept = all { admissionsKept, offered' = offered, owed' = owed }
+
+ /// The hub takes `input` on its own schedule. A step that would change
+ /// nothing is not taken.
+ action hubTakes(input: HubInput): bool =
+ val result = hub(h, input)
+ all {
+ not(isError(result.out)),
+ result.state != h,
+ h' = result.state,
+ cfg' = cfg,
+ }
+
+ // ------------------------------------------------------------------------
+ // Steps
+ // ------------------------------------------------------------------------
+
+ /// The cadence loop observes the tip its indexer reports.
+ ///
+ /// The poll is recorded whether or not the answer moves the hub's tip: a hub
+ /// that asked and was told nothing new has still asked. A second poll in the
+ /// same block that changes nothing is not taken.
+ action observeWith(tip: Height): bool =
+ val result = hub(h, TipHInput(tip))
+ all {
+ tips.contains(tip),
+ not(isError(result.out)),
+ result.state != h or not(polled),
+ h' = result.state,
+ polled' = true,
+ height' = height,
+ onChain' = onChain,
+ flightStart' = flightStart,
+ memoryKept,
+ cfg' = cfg,
+ }
+
+ action observe = {
+ nondet tip = oneOf(tips)
+ observeWith(tip)
+ }
+
+ /// A hub that has seen no tip progress for the staleness window goes stale,
+ /// or, already stale, reads its free-running clock again.
+ action staleWith(estimate: Height): bool = all {
+ cfg.tip == TipMayLag,
+ h.phase == Stale or lag >= cfg.staleWindow,
+ freeRunEstimates.contains(estimate),
+ hubTakes(StaleHInput(estimate)),
+ flightStart' = flightStart,
+ chainKept,
+ memoryKept,
+ }
+
+ action stale = {
+ nondet estimate = oneOf(freeRunEstimates)
+ staleWith(estimate)
+ }
+
+ /// A submission of `payload` reaches the hub, which takes `result`. A
+ /// payload does not exist before it is built, whoever submits it; after
+ /// that it may arrive at any time and any number of times.
+ action submitWith(payload: Payload, result: HubResult): bool =
+ val entered = result.state.queued().contains(payload) and not(seen.contains(payload))
+ all {
+ cfg.payloads.contains(payload),
+ height >= payload.created,
+ h.isServing(),
+ submitResults(payload).contains(result),
+ not(isError(result.out)),
+ h' = result.state,
+ seen' = if (entered) seen.union(Set(payload)) else seen,
+ onTime' =
+ if (entered and height <= payload.created + cfg.params.deliveryLag) onTime.union(Set(payload))
+ else onTime,
+ owed' = if (isAcceptedAck(result.out)) owed.union(Set(payload)) else owed,
+ offered' = offered,
+ flightStart' = flightStart,
+ chainKept,
+ cfg' = cfg,
+ }
+
+ action submit = all {
+ h.isServing(),
+ {
+ nondet payload = oneOf(cfg.payloads)
+ nondet result = oneOf(submitResults(payload))
+ submitWith(payload, result)
+ },
+ }
+
+ /// A flush begins: the hub's whole queue goes out at once. With nothing
+ /// queued the epoch is recorded, or a draining hub stops, and no flight
+ /// starts.
+ action flushBegin =
+ val result = hub(h, FlushDueHInput)
+ all {
+ hubTakes(FlushDueHInput),
+ flightStart' = if (result.state.flush == Idle) 0 else height,
+ if (result.state.phase == Stopped) runForgotten else all { admissionsKept, offered' = offered },
+ owed' = owed,
+ chainKept,
+ }
+
+ /// The indexer returns `given` on one entry of the batch, and the network
+ /// has taken the transaction or has not. A verdict other than `Retryable`
+ /// is a node's judgement: it settles the entry.
+ action verdictWith(payload: Payload, given: Verdict, relayed: bool): bool =
+ val judged = given != Retryable
+ all {
+ awaiting.contains(payload),
+ verdictsOn(payload).contains((given, relayed)),
+ hubTakes(VerdictHInput({ payload: payload, verdict: given })),
+ onChain' = if (relayed) onChain.union(Set(payload)) else onChain,
+ offered' = if (judged) offered.union(Set(payload)) else offered,
+ owed' = if (judged) owed.exclude(Set(payload)) else owed,
+ height' = height,
+ polled' = polled,
+ flightStart' = flightStart,
+ admissionsKept,
+ }
+
+ action verdict = all {
+ awaiting != Set(),
+ {
+ nondet payload = oneOf(awaiting)
+ nondet outcome = oneOf(verdictsOn(payload))
+ verdictWith(payload, outcome._1, outcome._2)
+ },
+ }
+
+ /// A flush ends: what nothing judged is requeued or dropped. The flight is
+ /// over for every entry it carried. The final flush stops the hub.
+ action flushEnd =
+ val result = hub(h, FlushDoneHInput)
+ all {
+ hubTakes(FlushDoneHInput),
+ flightStart' = 0,
+ owed' = owed,
+ if (result.state.phase == Stopped) runForgotten
+ else all { admissionsKept, offered' = offered.union(h.inFlight()) },
+ chainKept,
+ }
+
+ /// The hub gets its shutdown signal.
+ action drain = all {
+ hubTakes(DrainHInput),
+ flightStart' = flightStart,
+ chainKept,
+ memoryKept,
+ }
+
+ /// The hub's process dies, or exits after its final flush. A flight it had
+ /// out is over.
+ action crash = all {
+ hubTakes(CrashHInput),
+ flightStart' = 0,
+ owed' = owed,
+ runForgotten,
+ chainKept,
+ }
+
+ action restart = all {
+ hubTakes(RestartHInput),
+ flightStart' = flightStart,
+ chainKept,
+ memoryKept,
+ }
+
+ /// Whether the next block may arrive. This is where the timing assumptions
+ /// live: a block is held back until the hub has done what the tip model says
+ /// it does within a block.
+ ///
+ /// In every model, a flush that is due has begun, and no flush has been in
+ /// flight for `maxFlightBlocks` blocks already. A hub whose flush is in
+ /// flight is not looking at the tip, so the clauses below bind it only while
+ /// it is idle.
+ ///
+ /// - `TipTimely`: a running hub has asked for the tip since the last block.
+ /// An honest indexer answers with the true height, so the hub's lag is
+ /// zero at every block. A Byzantine one is asked just as often; what it
+ /// controls is the answer.
+ /// - `TipMayRegress`: a running hub is no further behind than the allowance.
+ /// - `TipMayLag`: a hub whose silence has reached the staleness window has
+ /// become stale, and a stale hub's free-running clock has caught up with
+ /// the current block.
+ def mayAdvance: bool = and {
+ height < cfg.maxHeight,
+ not(h.isFlushDue()),
+ h.flush == Idle or height - flightStart < cfg.maxFlightBlocks,
+ h.flush == Idle implies
+ match cfg.tip {
+ | TipTimely => h.phase == Running implies polled
+ | TipMayRegress => h.phase == Running implies lag <= cfg.params.reorgAllowance
+ | TipMayLag =>
+ and {
+ h.phase == Running implies lag < cfg.staleWindow,
+ h.phase == Stale implies h.cadenceHeight() >= height,
+ }
+ },
+ }
+
+ /// The chain grows by one block.
+ action advance = all {
+ mayAdvance,
+ height' = height + 1,
+ polled' = false,
+ onChain' = onChain,
+ h' = h,
+ flightStart' = flightStart,
+ memoryKept,
+ cfg' = cfg,
+ }
+
+ /// One step of the hub and its environment.
+ action step = any {
+ observe, stale, submit, flushBegin, verdict, flushEnd, advance,
+ drain, crash, restart,
+ }
+
+ // The relations below are parts of `step`. A property that holds under
+ // `step` holds under each; one that fails under a part fails under `step`,
+ // and the part says which faults the failure does not need.
+
+ /// No crash: the hub may still be shut down and started again.
+ action noCrashStep = any {
+ observe, stale, submit, flushBegin, verdict, flushEnd, advance,
+ drain, restart,
+ }
+
+ /// No shutdown, no crash, no restart.
+ action quietStep = any {
+ observe, stale, submit, flushBegin, verdict, flushEnd, advance,
+ }
+
+ // ------------------------------------------------------------------------
+ // Guarantees
+ // ------------------------------------------------------------------------
+ //
+ // G6b is about the moment a flush begins: how much of the mining margin is
+ // left when the hub hands the batch over. It does not say a node accepts the
+ // transaction, because the chain may move while the batch is in flight. G6c
+ // is about the moment a node judges it.
+ //
+ // Each is a predicate on the current state. That is enough: the whole batch
+ // is in flight in the state `flushBegin` produces, with `flightStart` the
+ // height it began at; and an entry awaiting a verdict can be given one, a
+ // rejection at least, at whatever height the chain has reached.
+
+ /// Whether `payload`, published at height `at`, can still be mined
+ /// `miningMargin` blocks later.
+ def marginLeft(payload: Payload, at: Height): bool =
+ match payload.expiry {
+ | Some(expiry) => expiry >= at + cfg.params.miningMargin
+ | None => true
+ }
+
+ /// Whether `payload` reached this hub as a supported wallet's would: it
+ /// honours the expiry floor, and it first entered the queue of this run of
+ /// the hub within the delivery lag of the height it was built at. A copy
+ /// that arrives late at a hub that has been down since the first one is not
+ /// timely, whatever happened before (K8).
+ def isConformingAndOnTime(payload: Payload): bool =
+ conforming(payload, cfg.params.minWalletExpiry) and onTime.contains(payload)
+
+ /// Whether the flight `payload` is on, if any, is its first since the hub
+ /// last came up.
+ def isFirstOffer(payload: Payload): bool =
+ not(offered.contains(payload))
+
+ /// G6b. A supported wallet's transaction is offered with the mining margin
+ /// to spare, the first time the hub offers it. A claim about the margin left
+ /// at the offer, not about acceptance. It says nothing about a later offer of
+ /// an entry that was requeued; see `conformingEveryOfferBeforeExpiry`.
+ val conformingFirstOfferBeforeExpiry =
+ h.inFlight().forall(payload =>
+ isConformingAndOnTime(payload) and isFirstOffer(payload) implies marginLeft(payload, flightStart))
+
+ /// G6c. The end-to-end claim: when a node judges the first offer of a
+ /// supported wallet's transaction, the transaction has not expired. It can
+ /// still be mined in the next block, so the node does not turn it away for
+ /// its expiry.
+ ///
+ /// The margin is what pays for the blocks that arrive while the batch is in
+ /// flight. G6c therefore needs G6b and one thing more: that fewer blocks
+ /// than the mining margin arrive during a flush (`flightWithinMargin`).
+ val conformingFirstOfferJudgedBeforeExpiry =
+ awaiting.forall(payload =>
+ isConformingAndOnTime(payload) and isFirstOffer(payload) implies
+ match payload.expiry {
+ | Some(expiry) => expiry > height
+ | None => true
+ })
+
+ // ------------------------------------------------------------------------
+ // Known gaps: invariants that do not hold
+ // ------------------------------------------------------------------------
+
+ /// K6. G6b without its restriction to the first offer. This does not hold
+ /// once a hub is stale: requeue judges an entry at the observed tip, which
+ /// has stopped, while the flush schedule runs on.
+ val conformingEveryOfferBeforeExpiry =
+ h.inFlight().forall(payload => isConformingAndOnTime(payload) implies marginLeft(payload, flightStart))
+
+ /// K5. A payload the hub has acknowledged is accounted for: the hub still
+ /// holds it, queued or in flight; or the chain has it; or a node has judged
+ /// it since the ack. Being offered is not enough: an offer nothing judged
+ /// settles nothing.
+ ///
+ /// This does not hold. The queue lives in memory: a crash after the ack
+ /// loses it; so does a final flush that finds the indexer unreachable; and
+ /// so does a requeue that gives the entry up as expired.
+ val ackedIsHeldOrSettled =
+ owed.subseteq(h.queued().union(h.inFlight()).union(onChain))
+
+ // ------------------------------------------------------------------------
+ // Reachability
+ // ------------------------------------------------------------------------
+ //
+ // States that must be reachable, each checked as `not(..)` expected to be
+ // violated. The first two are the antecedents of G6b and G6c: without
+ // them a "holds" could be vacuous. The rest are one per family of steps: TLC
+ // is run with deadlock checking off, so a configuration whose steps died
+ // after `init` would otherwise hold everything on a handful of states.
+
+ /// A supported wallet's transaction, with an expiry, is on its first flight.
+ val wConformingFirstOffer =
+ h.inFlight().exists(payload =>
+ isSome(payload.expiry) and isConformingAndOnTime(payload) and isFirstOffer(payload))
+
+ /// The same entry is still unjudged after a block has arrived.
+ val wConformingFirstOfferInFlightABlock =
+ height > flightStart and awaiting.exists(payload =>
+ isSome(payload.expiry) and isConformingAndOnTime(payload) and isFirstOffer(payload))
+
+ /// A flight has been answered or has ended.
+ val wOffered = offered != Set()
+ /// An entry nothing judged is back in the queue.
+ val wRequeued = h.queued().exists(payload => h.queue.get(payload) > 0)
+ val wDown = h.phase == Down
+ /// The hub has been started again, owing a payload from before.
+ val wRestartedOwing = h.phase == Starting and owed != Set()
+ /// A block has arrived while a flush is in flight.
+ val wBlockInFlight = flightStart > 0 and height > flightStart
+ val wStopped = h.phase == Stopped
+ val wStale = h.phase == Stale
+ /// A timely payload is queued while the cadence clock is in an epoch before
+ /// the one the hub last recorded: the tip went back across a boundary the
+ /// hub has already acted on.
+ val wTimelyQueuedBehindEpoch =
+ h.queued().exists(payload => onTime.contains(payload)) and
+ match h.lastEpoch {
+ | Some(epoch) => h.cadenceEpoch() < epoch
+ | None => false
+ }
+
+ // ------------------------------------------------------------------------
+ // Configurations
+ // ------------------------------------------------------------------------
+ //
+ // The schedule flushes every 3 blocks with a mining margin of 2 and a
+ // delivery lag of 1, and supports wallets that set an expiry 7 blocks out.
+ // It is the shipped one scaled down (shipped: interval 20, margin 4, lag 6,
+ // reorg allowance 10, staleness window 12 blocks, expiry floor 40), keeping
+ // the relations `shippedRelationsKept` names. The margin is 2, the smallest
+ // that leaves room for a block to arrive while a flush is in flight.
+
+ pure def orchard(id: str, created: Height, expiry: Height): Payload =
+ { id: id, txid: Some(id), created: created, expiry: Some(expiry), class: OrchardTouching, oversize: false }
+
+ /// Two migrations from supported wallets, built at heights 2 and 4.
+ pure val early = orchard("early", 2, 9)
+ pure val late = orchard("late", 4, 11)
+ /// A migration whose wallet set its expiry tighter than the supported floor.
+ pure val tight = orchard("tight", 2, 5)
+
+ /// Every component honest, and a hub that sees each block before the next.
+ pure val timely: HubConfig = {
+ payloads: Set(early, late),
+ params: {
+ flushInterval: 3,
+ miningMargin: 2,
+ deliveryLag: 1,
+ minWalletExpiry: 7,
+ reorgAllowance: 1,
+ maxAttempts: 2,
+ },
+ staleWindow: 3,
+ maxFlightBlocks: 1,
+ maxHeight: 12,
+ tip: TipTimely,
+ hubRole: Honest,
+ indexerRole: Honest,
+ }
+
+ // A tip that may be reported up to the reorg allowance behind the chain:
+ // with the slack that covers it, and without. In the second the expiry
+ // floor is the three-term budget exactly.
+ pure val flakyTip: HubConfig = { ...timely, tip: TipMayRegress }
+ pure val flakyTipNoSlack: HubConfig = {
+ ...flakyTip,
+ params: { ...flakyTip.params, minWalletExpiry: 6 },
+ payloads: Set(orchard("early", 2, 8), late),
+ }
+
+ // The same tip, and a flush that may stay in flight for as many blocks as
+ // the mining margin reserves.
+ pure val flakyTipSlowFlight: HubConfig = { ...flakyTip, maxFlightBlocks: 2 }
+
+ // A hub that may go without a tip for a while: on the shipped relation
+ // between the staleness window and the expiry floor, and on the relation
+ // that would cover the silence.
+ pure val staleLag: HubConfig = { ...timely, tip: TipMayLag }
+ pure val staleLagWithSlack: HubConfig = {
+ ...staleLag,
+ params: { ...staleLag.params, minWalletExpiry: 8 },
+ payloads: Set(orchard("early", 2, 10), orchard("late", 4, 12)),
+ }
+
+ // One Byzantine component at a time, on the schedule of `timely`, each
+ // with `tight` as well: a Byzantine hub admits what the expiry rule refuses.
+ // The Byzantine indexer gets one supported migration and `tight`: with three
+ // payloads TLC does not reach its G6c counterexample in five minutes.
+ pure val byzHub: HubConfig = { ...timely, hubRole: Byzantine, payloads: Set(early, late, tight) }
+ pure val byzIndexer: HubConfig = { ...timely, indexerRole: Byzantine, payloads: Set(early, tight) }
+
+ /// Bytes neither the shim nor the hub can parse: no txid, no expiry. After
+ /// a network upgrade a build does not know, every transaction looks like
+ /// this to it.
+ pure val junk: Payload =
+ { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, oversize: false }
+ pure val unknownUpgrade: HubConfig = { ...timely, payloads: Set(early, tight, junk) }
+
+ // One named init per configuration. A configuration built to show what a
+ // relation buys asserts that the relation is false of it, so that its known
+ // gap stays pinned on the missing relation.
+
+ action initTimely = all { shippedAssumptions(timely), initWith(timely) }
+ action initFlakyTip = all { shippedAssumptions(flakyTip), initWith(flakyTip) }
+ action initFlakyTipNoSlack = all {
+ standingAssumptions(flakyTipNoSlack),
+ flightWithinMargin(flakyTipNoSlack),
+ not(reorgSlackFits(flakyTipNoSlack)),
+ initWith(flakyTipNoSlack),
+ }
+ action initFlakyTipSlowFlight = all {
+ standingAssumptions(flakyTipSlowFlight),
+ shippedRelationsKept(flakyTipSlowFlight),
+ reorgSlackFits(flakyTipSlowFlight),
+ not(flightWithinMargin(flakyTipSlowFlight)),
+ initWith(flakyTipSlowFlight),
+ }
+ action initStaleLag = all { shippedAssumptions(staleLag), initWith(staleLag) }
+ action initByzHub = all { shippedAssumptions(byzHub), initWith(byzHub) }
+ action initByzIndexer = all { shippedAssumptions(byzIndexer), initWith(byzIndexer) }
+ action initUnknownUpgrade = all { shippedAssumptions(unknownUpgrade), initWith(unknownUpgrade) }
+ action initStaleLagWithSlack = all {
+ standingAssumptions(staleLagWithSlack),
+ reorgSlackFits(staleLagWithSlack),
+ flightWithinMargin(staleLagWithSlack),
+ staleSlackFits(staleLagWithSlack),
+ not(shippedRelationsKept(staleLagWithSlack)),
+ initWith(staleLagWithSlack),
+ }
+}
diff --git a/zeronym/spec/quint/indexer.qnt b/zeronym/spec/quint/indexer.qnt
new file mode 100644
index 00000000..c7f3abfb
--- /dev/null
+++ b/zeronym/spec/quint/indexer.qnt
@@ -0,0 +1,218 @@
+// -*- mode: Bluespec; -*-
+
+/// The chain as a hub sees it: one abstract indexer standing for all of a
+/// hub's indexer endpoints and the network behind them.
+///
+/// It is the environment, written in the same shape as the components: an
+/// input, a set of possible outputs, and the effect of each on the state. The
+/// honest relation is already nondeterministic, because a hub cannot tell in
+/// advance whether a broadcast will be taken. The Byzantine relation is a
+/// superset of it.
+///
+/// A hub folds several endpoints into one answer, and the folds are not
+/// symmetric. The tip is the maximum over the endpoints that answer; a lookup
+/// returns the first `found`; a broadcast takes the best verdict. So a single
+/// misbehaving endpoint is enough to raise the tip, inject a lookup answer or
+/// change a verdict, while lowering or freezing the tip takes every endpoint.
+/// "Byzantine indexer" in this specification covers both cases.
+module indexer {
+ import basicSpells.* from "./spells/basicSpells"
+ import types.* from "./types"
+
+ /// A transaction the chain has, with the bytes it was accepted as.
+ type ChainTx = { payload: Payload, at: Inclusion }
+
+ /// - `height`: the true chain height.
+ /// - `txs`: the transactions in the mempool or in a block, by txid.
+ /// - `offered`: every payload a hub has broadcast, whatever came of it. It
+ /// is what an indexer has seen, and so what a Byzantine one could reveal.
+ type IndexerState = {
+ height: Height,
+ txs: TxId -> ChainTx,
+ offered: Set[Payload],
+ }
+
+ type IndexerInput =
+ | BroadcastIInput(Payload) // a hub publishes one entry of a batch
+ | LookupIInput(TxId) // a hub's lookup missed its queue
+ | AdvanceIInput // the chain grows by one block
+ | MineIInput(TxId) // a mempool transaction is included
+
+ type IndexerOutput =
+ | VerdictOutput(Verdict)
+ | AnswerOutput(IndexerAnswer)
+ | NoIndexerOutput
+
+ type IndexerResult = Result[IndexerState, IndexerOutput]
+
+ pure def initialIndexer(height: Height): IndexerState =
+ { height: height, txs: Map(), offered: Set() }
+
+ // ------------------------------------------------------------------------
+ // Views
+ // ------------------------------------------------------------------------
+
+ /// Where `txid` stands on the chain.
+ pure def inclusion(state: IndexerState, txid: TxId): Inclusion =
+ if (state.txs.keys().contains(txid)) state.txs.get(txid).at else Absent
+
+ /// The payloads the chain has made public.
+ pure def published(state: IndexerState): Set[Payload] =
+ state.txs.keys().map(txid => state.txs.get(txid).payload)
+
+ /// Whether the chain already has a transaction with `payload`'s txid.
+ pure def isKnown(state: IndexerState, payload: Payload): bool =
+ match payload.txid {
+ | Some(txid) => state.txs.keys().contains(txid)
+ | None => false
+ }
+
+ /// Whether a node would take `payload` into its mempool now: it parses, it
+ /// can still be mined in the next block, and it is not there already.
+ pure def isAcceptable(state: IndexerState, payload: Payload): bool =
+ and {
+ isSome(payload.txid),
+ not(state.isKnown(payload)),
+ match payload.expiry {
+ | Some(expiry) => expiry > state.height
+ | None => true
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Effect
+ // ------------------------------------------------------------------------
+
+ /// The state after `input` was answered with `output`. A broadcast is always
+ /// remembered as offered; it reaches the mempool only on `Accepted`.
+ pure def indexerApply(state: IndexerState, input: IndexerInput, output: IndexerOutput): IndexerState =
+ match input {
+ | BroadcastIInput(payload) =>
+ val noted = { ...state, offered: state.offered.union(Set(payload)) }
+ match payload.txid {
+ | Some(txid) =>
+ if (output == VerdictOutput(Accepted))
+ { ...noted, txs: noted.txs.put(txid, { payload: payload, at: InMempool }) }
+ else noted
+ | None => noted
+ }
+ | LookupIInput(_) => state
+ | AdvanceIInput => { ...state, height: state.height + 1 }
+ | MineIInput(txid) =>
+ if (state.inclusion(txid) == InMempool)
+ { ...state, txs: state.txs.setBy(txid, tx => { ...tx, at: Mined }) }
+ else state
+ }
+
+ // ------------------------------------------------------------------------
+ // Honest relation
+ // ------------------------------------------------------------------------
+
+ /// The outputs an honest indexer may give. An empty set means the input is
+ /// not enabled.
+ ///
+ /// - Broadcast: `Rejected` and `Retryable` are always possible (the node has
+ /// reasons this model does not see, and the indexer may be unreachable);
+ /// `Accepted` only for a transaction a node would take; `AlreadyKnown`
+ /// only for one the chain has.
+ /// - Lookup: the chain's answer, or unavailable.
+ pure def honestIndexerOutputs(state: IndexerState, input: IndexerInput): Set[IndexerOutput] =
+ match input {
+ | BroadcastIInput(payload) =>
+ Set(Rejected, Retryable)
+ .union(if (state.isAcceptable(payload)) Set(Accepted) else Set())
+ .union(if (state.isKnown(payload)) Set(AlreadyKnown) else Set())
+ .map(verdict => VerdictOutput(verdict))
+ | LookupIInput(txid) =>
+ if (state.txs.keys().contains(txid))
+ val tx = state.txs.get(txid)
+ Set(
+ AnswerOutput(IFound({ body: Some(tx.payload), height: answerHeight(tx.at) })),
+ AnswerOutput(IUnavailable),
+ )
+ else Set(AnswerOutput(INotFound), AnswerOutput(IUnavailable))
+ | AdvanceIInput => Set(NoIndexerOutput)
+ | MineIInput(txid) =>
+ if (state.inclusion(txid) == InMempool) Set(NoIndexerOutput) else Set()
+ }
+
+ pure def honestIndexerResults(state: IndexerState, input: IndexerInput): Set[IndexerResult] =
+ honestIndexerOutputs(state, input).map(output =>
+ { state: indexerApply(state, input, output), out: output })
+
+ /// The honest relation as the protocol specification uses it, which has no
+ /// chain height: a broadcast that parses and is new may be accepted whatever
+ /// its expiry. It contains the honest relation (`heightlessCoversTest`).
+ pure def heightlessIndexerResults(state: IndexerState, input: IndexerInput): Set[IndexerResult] =
+ val accepted = match input {
+ | BroadcastIInput(payload) =>
+ if (isSome(payload.txid) and not(state.isKnown(payload)))
+ Set({ state: indexerApply(state, input, VerdictOutput(Accepted)), out: VerdictOutput(Accepted) })
+ else Set()
+ | _ => Set()
+ }
+ honestIndexerResults(state, input).union(accepted)
+
+ /// The truthful, available answer to a lookup: the one member of the honest
+ /// relation that is not `IUnavailable`.
+ pure def chainAnswer(state: IndexerState, txid: TxId): IndexerAnswer =
+ if (state.txs.keys().contains(txid))
+ val tx = state.txs.get(txid)
+ IFound({ body: Some(tx.payload), height: answerHeight(tx.at) })
+ else INotFound
+
+ /// The tips an honest indexer may report when reports can trail the true
+ /// height by up to `slack` blocks. `heights` is every height there is: the
+ /// answer is a part of a fixed range, never a range with a moving bound.
+ pure def honestTips(state: IndexerState, slack: int, heights: Set[Height]): Set[Height] =
+ heights.filter(height => state.height - slack <= height and height <= state.height)
+
+ // ------------------------------------------------------------------------
+ // Byzantine relation
+ // ------------------------------------------------------------------------
+
+ /// The payloads a Byzantine indexer can put in a lookup answer: those it was
+ /// offered, those the chain made public, and any twin of either that exists
+ /// in `universe`.
+ pure def servable(state: IndexerState, universe: Set[Payload]): Set[Payload] =
+ val known = state.offered.union(state.published())
+ universe.filter(candidate =>
+ known.exists(payload => candidate == payload or areTwins(candidate, payload)))
+
+ /// The outputs a Byzantine indexer may give: any verdict, and any lookup
+ /// answer built from a payload it can serve, at any height, with or without
+ /// a body.
+ pure def byzIndexerOutputs(state: IndexerState, input: IndexerInput, universe: Set[Payload]): Set[IndexerOutput] =
+ match input {
+ | BroadcastIInput(_) =>
+ Set(Accepted, AlreadyKnown, Rejected, Retryable).map(verdict => VerdictOutput(verdict))
+ | LookupIInput(_) =>
+ val bodies = Set(None).union(state.servable(universe).map(payload => Some(payload)))
+ tuples(bodies, WIRE_HEIGHTS)
+ .map(((body, claimed)) => AnswerOutput(IFound({ body: body, height: claimed })))
+ .union(Set(AnswerOutput(INotFound), AnswerOutput(IUnavailable)))
+ .union(honestIndexerOutputs(state, input))
+ | AdvanceIInput => honestIndexerOutputs(state, input)
+ | MineIInput(_) => honestIndexerOutputs(state, input)
+ }
+
+ /// The transitions of a Byzantine indexer. On a broadcast the verdict it
+ /// reports and what it does with the transaction are independent: it may
+ /// relay a transaction it claims to have rejected, or sit on one it claims to
+ /// have accepted. It cannot make the network take a transaction a node would
+ /// refuse: the chain itself stays honest.
+ pure def byzIndexerResults(state: IndexerState, input: IndexerInput, universe: Set[Payload]): Set[IndexerResult] =
+ val outputs = byzIndexerOutputs(state, input, universe)
+ match input {
+ | BroadcastIInput(payload) =>
+ val withheld = indexerApply(state, input, VerdictOutput(Retryable))
+ val relayed = indexerApply(state, input, VerdictOutput(Accepted))
+ val effects = if (state.isAcceptable(payload)) Set(withheld, relayed) else Set(withheld)
+ tuples(effects, outputs).map(((effect, output)) => { state: effect, out: output })
+ | _ => outputs.map(output => { state: indexerApply(state, input, output), out: output })
+ }
+
+ /// The tips a Byzantine indexer may report: any height there is.
+ pure def byzTips(heights: Set[Height]): Set[Height] =
+ heights
+}
diff --git a/zeronym/spec/quint/protocol.qnt b/zeronym/spec/quint/protocol.qnt
new file mode 100644
index 00000000..398fd22d
--- /dev/null
+++ b/zeronym/spec/quint/protocol.qnt
@@ -0,0 +1,1153 @@
+// -*- mode: Bluespec; -*-
+
+/// The zeronym protocol as a state machine: a wallet, a shim, one hub, the
+/// chain behind the hub's indexer, an unreliable network between them, and a
+/// third party that can reach the hub.
+///
+/// The spec checks one hub; production runs one or more, replicated: every
+/// shim sends every submission to every hub, and each hub that receives a
+/// migration queues and broadcasts it.
+///
+/// What is assumed:
+///
+/// - Roles. The shim and the hub run in enclaves and are honest in the
+/// baseline. The shim is honest in every configuration; the hub and its
+/// indexer can each be made Byzantine through `cfg.roles`. A Byzantine
+/// component draws its transitions from a wider relation and is not marked
+/// in any other way.
+/// - Network. Frames may be lost, duplicated, delayed and reordered. They
+/// cannot be forged or read in transit.
+/// - Third party. A client of the hub's public address. It looks up txids it
+/// knows and submits payloads it has learned or the chain has published. It cannot read or
+/// forge frames, so it does not know a nonce and cannot answer the shim.
+/// - Nonces are unique. A counter stands for an unguessable random value.
+/// - Chain. A transaction's status only moves forward: no reorg of an
+/// included transaction, no mempool eviction.
+/// - Hub. The hub is abstract (`abstractHub.qnt`): a queue, the entries out
+/// with a flush, and its replies, with no schedule. `hubTest` checks that
+/// the real hub function refines it. Its timing is the hub specification's.
+/// - Time. There is no clock. A timeout is an event that may happen at any
+/// moment.
+///
+/// How it is built. This module holds no protocol logic. Every step picks an
+/// input, hands it to one component (`shim`, the abstract hub, or the indexer
+/// relation) and puts the output where it goes. Each step exists in two
+/// forms: `xWith(..)`, which takes every choice as a parameter and is what a
+/// scripted run is made of, and `x`, which picks the choices and is what
+/// `step` is made of. All state is written by `commit`, so no action has a
+/// frame condition.
+module protocol {
+ import basicSpells.* from "./spells/basicSpells"
+ import soup.* from "./spells/soup"
+ import types.* from "./types"
+ import wire.* from "./wire"
+ import indexer.* from "./indexer"
+ import abstractHub.* from "./abstractHub"
+ import shim.* from "./shim"
+
+ // ========================================================================
+ // Transactions and configurations
+ // ========================================================================
+
+ // ------------------------------------------------------------------------
+ // Transactions
+ // ------------------------------------------------------------------------
+ //
+ // The expiries are set against the hub specification's schedule; the
+ // protocol does not read them.
+
+ pure def orchard(id: str, created: Height, expiry: Height): Payload =
+ { id: id, txid: Some(id), created: created, expiry: Some(expiry), class: OrchardTouching, oversize: false }
+
+ /// Two migrations from supported wallets, built at heights 2 and 4.
+ pure val early = orchard("early", 2, 9)
+ pure val late = orchard("late", 4, 11)
+ /// A migration whose wallet set its expiry tighter than the supported floor.
+ pure val tight = orchard("tight", 2, 5)
+ /// Bytes the shim cannot parse and neither can a hub: no txid, no expiry.
+ pure val junk: Payload =
+ { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, oversize: false }
+ /// A transaction that is not a migration.
+ pure val plain: Payload =
+ { id: "plain", txid: Some("plain"), created: 1, expiry: Some(9), class: PassThrough, oversize: false }
+ /// Other bytes with the txid of `early`.
+ pure val earlyTwin = { ...early, id: "early-twin" }
+
+ // ------------------------------------------------------------------------
+ // Configurations
+ // ------------------------------------------------------------------------
+
+ pure val allHonest: Roles = { hub: Honest, indexer: Honest }
+
+ /// One hub, the mixnet transport, every component honest.
+ pure val baseline: Config = {
+ payloads: Set(early, late, tight, junk, plain),
+ twins: Set(earlyTwin),
+ maxRequests: 3,
+ roles: allHonest,
+ }
+
+ // One Byzantine component at a time.
+ pure val byzHub = { ...baseline, roles: { ...allHonest, hub: Byzantine } }
+ pure val byzIndexer = { ...baseline, roles: { ...allHonest, indexer: Byzantine } }
+
+ // ========================================================================
+ // The system
+ //
+ // The whole system as one value: the components' states, the network
+ // between them, and what each outside party has seen. Nothing here decides
+ // anything: these functions put a component's output where it goes and
+ // derive the views the properties are stated over.
+ // ========================================================================
+
+ // ------------------------------------------------------------------------
+ // The system
+ // ------------------------------------------------------------------------
+
+ type Mail = Envelope[Addr, Msg]
+ type Net = Soup[Addr, Msg]
+
+ /// The wallet: the answers it has been given, in the order it got them, and
+ /// how many requests of each kind it has made.
+ type Wallet = { log: List[WalletEvent], sends: int, gets: int }
+
+ /// The third party: a client of the hub's public address that is not the
+ /// shim. `txids` are the transaction ids it has learned out of band.
+ type ThirdParty = { txids: Set[TxId], nextNonce: Nonce, requests: int }
+
+ /// - `hub`: the hub as the protocol sees it (`abstractHub.qnt`).
+ /// - `operator`: every transaction the shim has handed the operator's
+ /// indexer. The operator is assumed to publish nothing itself.
+ type System = {
+ indexer: IndexerState,
+ hub: AHub,
+ shim: ShimState,
+ net: Net,
+ wallet: Wallet,
+ operator: Set[Payload],
+ thirdParty: ThirdParty,
+ }
+
+ /// The system at rest: the chain and the hub empty, nothing sent. The
+ /// protocol has no chain height, and the indexer's stays at 0.
+ pure def initialSystem(config: Config): System = {
+ indexer: initialIndexer(0),
+ hub: emptyAHub,
+ shim: initialShim,
+ net: Set(),
+ wallet: { log: [], sends: 0, gets: 0 },
+ operator: Set(),
+ thirdParty: { txids: Set(), nextNonce: 0, requests: 0 },
+ }
+
+ /// What an observer of the run has recorded. It is not protocol state: no
+ /// component reads it, and it is derived at every step from the states
+ /// before and after, never from what a component reports about itself.
+ ///
+ /// - `windows`: for each lookup the shim has sent, the answers that were
+ /// true at the hub at some point while it waited.
+ type Audit = {
+ windows: Nonce -> Set[LookupObs],
+ }
+
+ // ------------------------------------------------------------------------
+ // Views
+ // ------------------------------------------------------------------------
+
+ /// Where `txid` stands on the chain.
+ pure def onChain(s: System, txid: TxId): Inclusion =
+ s.indexer.inclusion(txid)
+
+ /// The answers the wallet has been given, without their order.
+ pure def events(s: System): Set[WalletEvent] =
+ s.wallet.log.indices().map(i => s.wallet.log[i])
+
+ /// The payloads the wallet has been told were diverted.
+ pure def toldOk(s: System): Set[Payload] =
+ s.events().filterMap(event =>
+ match event {
+ | Sent(sent) =>
+ match sent.input {
+ | Clean(payload) => if (sent.obs == SentOk) Some(payload) else None
+ | _ => None
+ }
+ | _ => None
+ })
+
+ /// The frames `client` has addressed to the hub.
+ pure def toHub(s: System, client: Addr): Set[Msg] =
+ s.net.filter(mail => mail.src == client and mail.dst == HubAddr).map(mail => mail.msg)
+
+ /// The frames the hub has addressed to `client`.
+ pure def fromHub(s: System, client: Addr): Set[Msg] =
+ s.net.filter(mail => mail.src == HubAddr and mail.dst == client).map(mail => mail.msg)
+
+ /// The acks the hub has sent `client`.
+ pure def acks(s: System, client: Addr): Set[{ nonce: Nonce, ack: WireAck }] =
+ s.fromHub(client).filterMap(msg => match msg { | Ack(ack) => Some(ack) | _ => None })
+
+ /// The lookups `client` has addressed to the hub.
+ pure def lookups(s: System, client: Addr): Set[{ nonce: Nonce, txid: TxId }] =
+ s.toHub(client).filterMap(msg => match msg { | Lookup(lookup) => Some(lookup) | _ => None })
+
+ /// The lookup replies the hub has addressed to `client`.
+ pure def replies(s: System, client: Addr): Set[{ nonce: Nonce, reply: WireReply }] =
+ s.fromHub(client).filterMap(msg => match msg { | LookupReply(reply) => Some(reply) | _ => None })
+
+ /// The transaction bodies in lookup replies addressed to `client`.
+ pure def repliedBodies(s: System, client: Addr): Set[Payload] =
+ s.replies(client).filterMap(reply =>
+ match reply.reply {
+ | WFound(found) => found.body
+ | _ => None
+ })
+
+ // ------------------------------------------------------------------------
+ // What each party knows
+ // ------------------------------------------------------------------------
+
+ /// The transaction ids the third party knows: those it learned out of band
+ /// and everything the chain has made public.
+ pure def tpTxids(s: System): Set[TxId] =
+ s.thirdParty.txids.union(s.indexer.txs.keys())
+
+ /// The payloads the third party did not make and yet has: the bodies of
+ /// replies sent to it, and whatever reached the operator. The chain is left
+ /// out on purpose: what is published is public. A Byzantine hub or indexer
+ /// leaks through a lookup reply; there is no other disclosure.
+ ///
+ /// This is derived from what the third party can observe. Nothing updates it
+ /// when a transaction is published, so a property over it constrains what
+ /// the hub puts in its replies.
+ pure def tpLearned(s: System): Set[Payload] =
+ s.repliedBodies(ThirdPartyAddr).union(s.operator)
+
+ /// Every payload the third party has: what it learned and what the chain
+ /// published.
+ pure def tpPayloads(s: System): Set[Payload] =
+ s.tpLearned().union(s.indexer.published())
+
+ /// The payloads the wallet has handed the shim: every send is answered at
+ /// once.
+ pure def sentByWallet(s: System): Set[Payload] =
+ s.events().filterMap(event =>
+ match event {
+ | Sent(done) =>
+ match done.input {
+ | Clean(payload) => Some(payload)
+ | _ => None
+ }
+ | _ => None
+ })
+
+ // ------------------------------------------------------------------------
+ // Putting outputs where they go
+ // ------------------------------------------------------------------------
+
+ pure def logged(s: System, event: WalletEvent): System =
+ { ...s, wallet: { ...s.wallet, log: s.wallet.log.append(event) } }
+
+ pure def posted(s: System, mails: Set[Mail]): System =
+ { ...s, net: s.net.sendAll(mails) }
+
+ /// The system after the shim took `result`. `via` is the nonce of the frame
+ /// that was delivered to it, if the step was a delivery: it is recorded with
+ /// a lookup answer so the answer can be traced to the reply that gave it.
+ pure def shimStepped(s: System, result: ShimResult, via: Option[Nonce]): System =
+ val stepped = { ...s, shim: result.state }
+ match result.out {
+ | ForwardOutput(payload) =>
+ { ...stepped, operator: stepped.operator.union(Set(payload)) }
+ .logged(Sent({ input: Clean(payload), obs: SentToOperator }))
+ | DivertedOutput(diverted) =>
+ stepped.posted(Set({ src: ShimAddr, dst: HubAddr, msg: diverted.frame }))
+ .logged(Sent({ input: Clean(diverted.payload), obs: diverted.told }))
+ | SendDoneOutput(done) => stepped.logged(Sent(done))
+ | LookupSentOutput(frame) => stepped.posted(Set({ src: ShimAddr, dst: HubAddr, msg: frame }))
+ | LookupDoneOutput(done) =>
+ stepped.logged(Got({ query: done.query, obs: done.result, via: via }))
+ | NoShimOutput => stepped
+ | ShimErrorOutput(_) => stepped
+ }
+
+ /// The system after the hub answered `answer` to the request `mail`. The
+ /// reply goes back to its sender under its nonce.
+ pure def hubReplied(s: System, mail: Mail, answer: AAnswer): System =
+ val nonce = match mail.msg {
+ | Submit(submit) => submit.nonce
+ | Lookup(lookup) => lookup.nonce
+ | _ => 0
+ }
+ val msg = match answer.reply {
+ | AAck(ack) => Ack({ nonce: nonce, ack: ack })
+ | AWire(reply) => LookupReply({ nonce: nonce, reply: reply })
+ }
+ { ...s, hub: answer.hub }.posted(Set({ src: HubAddr, dst: mail.src, msg: msg }))
+
+ /// The request a frame carries. `answer` is what the hub's indexer would say
+ /// to a lookup. Reply frames are not requests and give nothing.
+ pure def requestOf(msg: Msg, answer: IndexerAnswer): Set[ARequest] =
+ match msg {
+ | Submit(submit) => Set(ASubmit(submit.payload))
+ | Lookup(lookup) => Set(ALookup({ txid: lookup.txid, answer: answer }))
+ | _ => Set()
+ }
+
+ /// The wallet makes one more request of a kind.
+ pure def countSend(s: System): System =
+ { ...s, wallet: { ...s.wallet, sends: s.wallet.sends + 1 } }
+
+ pure def countGet(s: System): System =
+ { ...s, wallet: { ...s.wallet, gets: s.wallet.gets + 1 } }
+
+ /// The third party sends `msg` to the hub, under a nonce of its own.
+ pure def thirdPartySent(s: System, msg: Msg): System =
+ { ...s,
+ thirdParty: { ...s.thirdParty,
+ nextNonce: s.thirdParty.nextNonce + 1,
+ requests: s.thirdParty.requests + 1,
+ },
+ }.posted(Set({ src: ThirdPartyAddr, dst: HubAddr, msg: msg }))
+
+ // ========================================================================
+ // Properties
+ //
+ // What a wallet can rely on, what it cannot, and what must be reachable.
+ // Every definition is a pure predicate over the system and the audit
+ // record. Three classes, kept apart: guarantees, invariants claimed under
+ // stated trust assumptions; known gaps, invariants a wallet might hope for
+ // that fail even when every component is honest; witnesses, states that
+ // must be reachable. A predicate reads the system and the audit record, and
+ // the audit record is derived from consecutive states by `advance`, never
+ // from what a component says about itself.
+ // ========================================================================
+
+ // ------------------------------------------------------------------------
+ // The audit record
+ // ------------------------------------------------------------------------
+
+ /// The true answer to a lookup for `query` at the hub, read off its
+ /// queue and the chain. The queue comes first, as it does in the hub.
+ ///
+ /// `NotFound` is the true answer for a transaction that is with a flush and
+ /// not yet on the chain. That window is part of the lookup contract. The
+ /// implementation says so (`zeronym/hub/src/server.rs`, on `Hub::lookup`):
+ ///
+ /// > Note the flush-in-flight gap: `flush()` drains the queue before
+ /// > `broadcast_batch` has reached the indexer, so a lookup in that window
+ /// > gets a queue miss then an indexer NOT_FOUND for a transaction it was
+ /// > told height-0 about seconds earlier. Wallets poll on multi-second
+ /// > intervals and tolerate a transient NOT_FOUND; a resubmit is harmless
+ /// > (deduped pre-flush, already-known post-flush). Holding entries until
+ /// > broadcast returns would extend how long the hub remembers a txid, which
+ /// > is the wrong trade.
+ ///
+ /// It is also the true answer for a queued payload that does not parse.
+ pure def truth(s: System, query: TxId): LookupObs =
+ if (s.hub.queue.exists(payload => payload.txid == Some(query)))
+ Pending
+ else if (s.indexer.txs.keys().contains(query))
+ val tx = s.indexer.txs.get(query)
+ Tx({ payload: tx.payload, height: answerHeight(tx.at) })
+ else
+ NotFound
+
+ pure val initialAudit: Audit = { windows: Map() }
+
+ /// The audit record after one step, from the states before and after it.
+ pure def advance(audit: Audit, pre: System, post: System): Audit =
+ // The lookups the shim is waiting on, or was until this step, each widen
+ // their window by what is true at the hub.
+ val waiting = pre.shim.waiters.keys().union(post.shim.waiters.keys())
+ val windows = post.lookups(ShimAddr)
+ .filter(lookup => waiting.contains(lookup.nonce))
+ .fold(audit.windows, (acc, lookup) =>
+ val seen = if (acc.keys().contains(lookup.nonce)) acc.get(lookup.nonce) else Set()
+ acc.put(lookup.nonce, seen.union(Set(truth(post, lookup.txid)))))
+ { windows: windows }
+
+ // ------------------------------------------------------------------------
+ // Guarantees
+ // ------------------------------------------------------------------------
+
+ /// G1. The operator sees no migration: everything the shim hands it is a
+ /// pass-through transaction.
+ pure def operatorBlindIn(s: System): bool =
+ s.operator.forall(payload => payload.class == PassThrough)
+
+ /// G2. A transaction's bytes do not reach a third party before the chain has
+ /// published them. Everything the third party has learned is on the chain,
+ /// or was a pass-through transaction the operator was given.
+ pure def queuedBytesConfidentialIn(s: System): bool =
+ s.tpLearned().forall(payload =>
+ or {
+ s.indexer.published().contains(payload),
+ s.operator.contains(payload) and payload.class == PassThrough,
+ })
+
+ /// G3. A transaction served to the wallet has the txid the wallet asked for.
+ /// That is all: it need not be the bytes the wallet sent (a twin passes),
+ /// and its height is whatever the hub said.
+ pure def txidAuthenticityIn(s: System): bool =
+ s.events().forall(event =>
+ match event {
+ | Got(got) =>
+ match got.obs {
+ | Tx(tx) => tx.payload.txid == Some(got.query)
+ | _ => true
+ }
+ | _ => true
+ })
+
+ /// G4. Every lookup answer other than `Unavailable` was true, at the hub
+ /// that gave it, at some point between the request and the answer.
+ ///
+ /// It is a statement about one request. It does not say that successive
+ /// answers agree; see `statusNeverRegresses`.
+ pure def lookupValidityPerHubIn(s: System, audit: Audit): bool =
+ s.events().forall(event =>
+ match event {
+ | Got(got) =>
+ or {
+ got.obs == Unavailable,
+ match got.via {
+ | Some(nonce) =>
+ audit.windows.keys().contains(nonce) and audit.windows.get(nonce).contains(got.obs)
+ | None => false
+ },
+ }
+ | _ => true
+ })
+
+ // ------------------------------------------------------------------------
+ // Known gaps
+ // ------------------------------------------------------------------------
+
+ /// K2. What a wallet sees of one transaction never goes backwards: once
+ /// served, it is not later pending or missing; once pending, it is not later
+ /// missing. This does not hold. Replies are reordered; a published
+ /// transaction can be queued again; a flush empties the queue before the
+ /// chain has the batch; and the node can reject at flush.
+ pure def statusNeverRegressesIn(s: System): bool =
+ val log = s.wallet.log
+ tuples(log.indices(), log.indices()).forall(((i, j)) =>
+ i < j implies
+ match log[i] {
+ | Got(earlier) =>
+ match log[j] {
+ | Got(later) =>
+ earlier.query != later.query or
+ match earlier.obs {
+ | Tx(_) =>
+ match later.obs {
+ | Tx(_) => true
+ | Unavailable => true
+ | _ => false
+ }
+ | Pending => later.obs != NotFound
+ | _ => true
+ }
+ | _ => true
+ }
+ | _ => true
+ })
+
+ // ------------------------------------------------------------------------
+ // Witnesses
+ // ------------------------------------------------------------------------
+
+ pure def wasGiven(s: System, isIt: LookupObs => bool): bool =
+ s.events().exists(event =>
+ match event {
+ | Got(got) => isIt(got.obs)
+ | _ => false
+ })
+
+ /// The wallet is told its transaction is pending.
+ pure def wPendingIn(s: System): bool =
+ s.wasGiven(obs => obs == Pending)
+
+ /// The wallet is served its transaction from the mempool.
+ pure def wTxInMempoolIn(s: System): bool =
+ s.wasGiven(obs =>
+ match obs {
+ | Tx(tx) => tx.height == AtZero
+ | _ => false
+ })
+
+ /// The wallet is served its transaction from a block.
+ pure def wTxMinedIn(s: System): bool =
+ s.wasGiven(obs =>
+ match obs {
+ | Tx(tx) => tx.height == AtMined
+ | _ => false
+ })
+
+ /// The accepted disclosure: a third party that knows a txid learns that
+ /// it is queued at the hub. The hub withholds the bytes; it does not withhold
+ /// the fact. The implementation leaves this open on purpose
+ /// (`zeronym/hub/src/server.rs`, in `Hub::lookup`):
+ ///
+ /// > What this does NOT close: the 200-versus-NotFound distinction still
+ /// > discloses that a given txid is queued here. Closing that too means
+ /// > answering NotFound, which costs a wallet the ability to tell "pending"
+ /// > from "never seen". That is a product decision, not a code one, and it
+ /// > is left open deliberately.
+ pure def wQueuedDisclosedIn(s: System): bool =
+ tuples(s.lookups(ThirdPartyAddr), s.replies(ThirdPartyAddr)).exists(((lookup, reply)) =>
+ lookup.nonce == reply.nonce and reply.reply == WFound({ body: None, height: AtZero }))
+
+ /// The hub holds a payload it cannot parse; the wallet that sent it asks
+ /// for it and is told not found. An entry without a txid can never
+ /// be hit.
+ pure def wUnparseableMissedIn(s: System): bool =
+ tuples(s.events(), s.lookups(ShimAddr)).exists(((event, lookup)) =>
+ match event {
+ | Got(got) =>
+ and {
+ got.obs == NotFound,
+ got.via == Some(lookup.nonce),
+ s.hub.queue.exists(payload => payload.txid == None and walletTxid(payload) == got.query),
+ }
+ | _ => false
+ })
+
+ /// A third party is given a transaction's bytes in a lookup reply.
+ /// With every component honest these are published bytes, served from the
+ /// indexer: the branch of G2 that `vQueuedBytesConfidential` alone does not
+ /// reach, since `plain` at the operator satisfies it.
+ pure def wThirdPartyServedBodyIn(s: System): bool =
+ s.repliedBodies(ThirdPartyAddr) != Set()
+
+ /// W16a. The wallet is served a twin of what it sent: other bytes, same txid.
+ pure def wTwinServedIn(s: System): bool =
+ s.wasGiven(obs =>
+ match obs {
+ | Tx(tx) => s.toldOk().exists(sent => areTwins(sent, tx.payload))
+ | _ => false
+ })
+
+ /// W16b. The wallet is served a transaction at a height that cannot be
+ /// true: the chain does not have it, or has it in the mempool and the
+ /// height says mined, or the height is not where it was mined.
+ pure def wFalseHeightServedIn(s: System): bool =
+ s.wasGiven(obs =>
+ match obs {
+ | Tx(tx) =>
+ val at = match tx.payload.txid {
+ | Some(txid) => s.onChain(txid)
+ | None => Absent
+ }
+ or { at == Absent, tx.height == AtOther, tx.height == AtMined and at != Mined }
+ | _ => false
+ })
+
+ // ------------------------------------------------------------------------
+ // Non-vacuity: the antecedent of each guarantee is reachable
+ // ------------------------------------------------------------------------
+
+ pure def vOperatorBlindIn(s: System): bool =
+ s.operator != Set()
+
+ pure def vQueuedBytesConfidentialIn(s: System): bool =
+ s.tpLearned() != Set()
+
+ pure def vTxidAuthenticityIn(s: System): bool =
+ s.wasGiven(obs =>
+ match obs {
+ | Tx(_) => true
+ | _ => false
+ })
+
+ pure def vLookupValidityPerHubIn(s: System): bool =
+ and {
+ s.wPendingIn(),
+ s.vTxidAuthenticityIn(),
+ s.wasGiven(obs => obs == NotFound),
+ }
+
+ // ========================================================================
+ // The machine
+ // ========================================================================
+
+
+ // ------------------------------------------------------------------------
+ // Configuration
+ // ------------------------------------------------------------------------
+
+ /// The configuration. Written by `initWith` and by nothing else. The names
+ /// below are its fields, and are what the rest of the module uses.
+ var cfg: Config
+
+ /// The transactions a wallet may send.
+ def PAYLOADS = cfg.payloads
+ /// Twins of wallet transactions: other bytes with the same txid. No honest
+ /// party sends one.
+ def TWINS = cfg.twins
+
+ /// The bound of the model: the wallet makes at most `MAX_REQUESTS` sends
+ /// and as many lookups, as does the third party.
+ def MAX_REQUESTS = cfg.maxRequests
+
+ def ROLES = cfg.roles
+
+ /// Every payload that exists. A Byzantine component builds its lies from it.
+ pure def universeOf(c: Config): Set[Payload] = c.payloads.union(c.twins)
+ def UNIVERSE = universeOf(cfg)
+ /// What a wallet may send.
+ def SEND_INPUTS = PAYLOADS.map(payload => Clean(payload)).union(Set(Unreadable, EmptyBody))
+ /// Every transaction id there is.
+ def TXIDS = txidsOf(UNIVERSE)
+
+ /// The standing assumption, checked by every named init: payloads are told
+ /// apart by their bytes, and a twin is a twin of something a wallet sends.
+ pure def payloadsWellFormed(c: Config): bool =
+ val universe = universeOf(c)
+ and {
+ universe.size() == universe.map(payload => payload.id).size(),
+ c.twins.forall(twin => c.payloads.exists(payload => areTwins(twin, payload))),
+ }
+
+ /// Checked by the Byzantine inits: the universe holds a wallet payload, its
+ /// twin, and a payload with another txid, so a lie can be the twin or a
+ /// foreign transaction.
+ pure def universeCoversLies(c: Config): bool =
+ c.payloads.exists(payload => and {
+ c.twins.exists(twin => areTwins(twin, payload)),
+ c.payloads.exists(other => other.txid != None and other.txid != payload.txid),
+ })
+
+ // ------------------------------------------------------------------------
+ // State
+ // ------------------------------------------------------------------------
+
+ /// The protocol state.
+ var s: System
+ /// The observer's record of the run. No step reads it.
+ var audit: Audit
+
+ /// The only writer of the variables after `initWith`.
+ action commit(post: System): bool = all {
+ cfg' = cfg,
+ s' = post,
+ audit' = advance(audit, s, post),
+ }
+
+ action initWith(c: Config): bool = all {
+ cfg' = c,
+ s' = initialSystem(c),
+ audit' = initialAudit,
+ }
+
+ action initBaseline = all { payloadsWellFormed(baseline), initWith(baseline) }
+ action initByzHub = all { payloadsWellFormed(byzHub), universeCoversLies(byzHub), initWith(byzHub) }
+ action initByzIndexer = all { payloadsWellFormed(byzIndexer), universeCoversLies(byzIndexer), initWith(byzIndexer) }
+
+ // ------------------------------------------------------------------------
+ // Roles
+ // ------------------------------------------------------------------------
+
+ def hubAnswers(h: AHub, request: ARequest): Set[AAnswer] =
+ match ROLES.hub {
+ | Honest => honestAnswers(h, request)
+ | Byzantine => byzantineAnswers(h, request, UNIVERSE)
+ }
+
+ def indexerResults(state: IndexerState, input: IndexerInput): Set[IndexerResult] =
+ match ROLES.indexer {
+ | Honest => heightlessIndexerResults(state, input)
+ | Byzantine => byzIndexerResults(state, input, UNIVERSE)
+ }
+
+ /// What the indexer may answer a hub's lookup for the transaction `msg`
+ /// asks about. A frame that is not a lookup needs no answer.
+ def lookupAnswers(state: IndexerState, msg: Msg): Set[IndexerAnswer] =
+ match msg {
+ | Lookup(lookup) =>
+ indexerResults(state, LookupIInput(lookup.txid)).filterMap(result =>
+ match result.out {
+ | AnswerOutput(answer) => Some(answer)
+ | _ => None
+ })
+ | _ => Set(INotFound)
+ }
+
+ pure def isShimError(output: ShimOutput): bool =
+ match output {
+ | ShimErrorOutput(_) => true
+ | _ => false
+ }
+
+ // ------------------------------------------------------------------------
+ // Wallet
+ // ------------------------------------------------------------------------
+
+ /// The wallet sends a transaction, and the shim routes it and answers.
+ /// `handedOver` is whether the transport takes the frame for the hub.
+ action walletSendWith(input: SendInput, handedOver: bool): bool = all {
+ s.wallet.sends < MAX_REQUESTS,
+ SEND_INPUTS.contains(input),
+ val result = shim(s.shim, SendTxSInput({ input: input, handedOver: handedOver }))
+ all {
+ not(isShimError(result.out)),
+ commit(s.countSend().shimStepped(result, None)),
+ },
+ }
+
+ action walletSend = all {
+ s.wallet.sends < MAX_REQUESTS,
+ {
+ nondet input = oneOf(SEND_INPUTS)
+ nondet handedOver = oneOf(Set(true, false))
+ walletSendWith(input, handedOver)
+ },
+ }
+
+ /// The txids of the transactions the wallet has handed the shim. A wallet
+ /// asks only about its own transactions.
+ def walletTxids: Set[TxId] =
+ s.sentByWallet().map(payload => walletTxid(payload))
+
+ /// The wallet asks for a transaction it has sent. The shim asks the hub.
+ action walletGetWith(query: TxId): bool = all {
+ s.wallet.gets < MAX_REQUESTS,
+ walletTxids.contains(query),
+ val result = shim(s.shim, GetTxSInput(query))
+ all {
+ not(isShimError(result.out)),
+ commit(s.countGet().shimStepped(result, None)),
+ },
+ }
+
+ action walletGet = all {
+ s.wallet.gets < MAX_REQUESTS,
+ walletTxids != Set(),
+ {
+ nondet query = oneOf(walletTxids)
+ walletGetWith(query)
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Shim
+ // ------------------------------------------------------------------------
+
+ /// The frames whose delivery to the shim would do something: replies under
+ /// a nonce it is waiting on. Any other frame is dropped without effect.
+ def shimDeliverable: Set[Mail] =
+ s.net.inbox(ShimAddr).filter(mail =>
+ match nonceOf(FrameSInput(mail.msg)) {
+ | Some(nonce) => s.shim.hasWaiter(nonce)
+ | None => false
+ })
+
+ /// The network delivers a frame to the shim.
+ action shimReceiveWith(mail: Mail): bool = all {
+ shimDeliverable.contains(mail),
+ val result = shim(s.shim, FrameSInput(mail.msg))
+ all {
+ not(isShimError(result.out)),
+ commit(s.shimStepped(result, nonceOf(FrameSInput(mail.msg)))),
+ },
+ }
+
+ action shimReceive = all {
+ shimDeliverable != Set(),
+ {
+ nondet mail = oneOf(shimDeliverable)
+ shimReceiveWith(mail)
+ },
+ }
+
+ /// The shim gives up waiting for a lookup reply.
+ action shimLookupTimeoutWith(nonce: Nonce): bool = all {
+ s.shim.hasWaiter(nonce),
+ val result = shim(s.shim, LookupTimeoutSInput(nonce))
+ all {
+ not(isShimError(result.out)),
+ commit(s.shimStepped(result, None)),
+ },
+ }
+
+ action shimLookupTimeout = all {
+ s.shim.waiters.keys() != Set(),
+ {
+ nondet nonce = oneOf(s.shim.waiters.keys())
+ shimLookupTimeoutWith(nonce)
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Hub
+ // ------------------------------------------------------------------------
+
+ /// The request frames that may be delivered to the hub: all of them, as
+ /// often as the network likes.
+ def hubDeliverable: Set[Mail] =
+ s.net.inbox(HubAddr).filter(mail => requestOf(mail.msg, INotFound) != Set())
+
+ /// What the hub may answer when `mail` is delivered and its indexer would
+ /// answer a lookup with `answer`.
+ def hubReceipts(mail: Mail, answer: IndexerAnswer): Set[AAnswer] =
+ requestOf(mail.msg, answer).map(request => hubAnswers(s.hub, request)).flatten()
+
+ /// The network delivers a request to the hub, which answers its sender. For
+ /// a lookup, `answer` is what the hub's indexer says if the queue misses.
+ action hubReceiveWith(mail: Mail, answer: IndexerAnswer, result: AAnswer): bool = all {
+ hubDeliverable.contains(mail),
+ lookupAnswers(s.indexer, mail.msg).contains(answer),
+ hubReceipts(mail, answer).contains(result),
+ commit(s.hubReplied(mail, result)),
+ }
+
+ action hubReceive = all {
+ hubDeliverable != Set(),
+ {
+ nondet mail = oneOf(hubDeliverable)
+ nondet answer = oneOf(lookupAnswers(s.indexer, mail.msg))
+ nondet result = oneOf(hubReceipts(mail, answer))
+ hubReceiveWith(mail, answer, result)
+ },
+ }
+
+ /// A flush begins: the whole queue goes out at once. A Byzantine hub keeps
+ /// the schedule, so these steps are the same whatever its role.
+ action hubTake = all {
+ s.hub.queue != Set(),
+ commit({ ...s, hub: s.hub.take() }),
+ }
+
+ /// The verdict an indexer output carries. Read only where it carries one.
+ pure def verdictIn(output: IndexerOutput): Verdict =
+ match output {
+ | VerdictOutput(verdict) => verdict
+ | _ => Retryable
+ }
+
+ /// The indexer returns its verdict on one entry out with a flush. `result`
+ /// is the indexer's transition: the verdict, and what became of the
+ /// transaction. A node's verdict settles the entry; a retryable one leaves it
+ /// out with the flush.
+ action indexerVerdictWith(payload: Payload, result: IndexerResult): bool = all {
+ s.hub.held.contains(payload),
+ indexerResults(s.indexer, BroadcastIInput(payload)).contains(result),
+ result.out == VerdictOutput(verdictIn(result.out)),
+ val hub = if (verdictIn(result.out) == Retryable) s.hub else s.hub.settle(payload)
+ commit({ ...s, indexer: result.state, hub: hub }),
+ }
+
+ action indexerVerdict = all {
+ s.hub.held != Set(),
+ {
+ nondet payload = oneOf(s.hub.held)
+ nondet result = oneOf(indexerResults(s.indexer, BroadcastIInput(payload)))
+ indexerVerdictWith(payload, result)
+ },
+ }
+
+ /// A flush ends: of what nothing judged, `kept` goes back into the queue and
+ /// the rest is dropped.
+ action hubReturnWith(kept: Set[Payload]): bool = all {
+ s.hub.held != Set(),
+ kept.subseteq(s.hub.held),
+ commit({ ...s, hub: s.hub.giveBack(kept) }),
+ }
+
+ action hubReturn = all {
+ s.hub.held != Set(),
+ {
+ nondet kept = oneOf(s.hub.held.powerset())
+ hubReturnWith(kept)
+ },
+ }
+
+ /// The hub loses everything: its process dies, or exits after its final
+ /// flush.
+ action hubLose = all {
+ s.hub != emptyAHub,
+ commit({ ...s, hub: emptyAHub }),
+ }
+
+ // ------------------------------------------------------------------------
+ // Chain
+ // ------------------------------------------------------------------------
+
+ /// The transactions waiting in the mempool.
+ def mempool: Set[TxId] =
+ s.indexer.txs.keys().filter(txid => s.onChain(txid) == InMempool)
+
+ /// A mempool transaction is included in the current block.
+ action chainMineWith(txid: TxId): bool = all {
+ mempool.contains(txid),
+ commit({ ...s, indexer: indexerApply(s.indexer, MineIInput(txid), NoIndexerOutput) }),
+ }
+
+ action chainMine = all {
+ mempool != Set(),
+ {
+ nondet txid = oneOf(mempool)
+ chainMineWith(txid)
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Third party
+ // ------------------------------------------------------------------------
+
+ /// The txids of wallet transactions the third party has yet to learn.
+ def unknownTxids: Set[TxId] =
+ txidsOf(PAYLOADS).exclude(s.tpTxids())
+
+ /// The third party learns a txid out of band, before the transaction is
+ /// published. An operator can recover one from a wallet's transparent-pool
+ /// queries.
+ action thirdPartyLearnsTxidWith(txid: TxId): bool = all {
+ unknownTxids.contains(txid),
+ commit({ ...s, thirdParty: { ...s.thirdParty, txids: s.thirdParty.txids.union(Set(txid)) } }),
+ }
+
+ action thirdPartyLearnsTxid = all {
+ unknownTxids != Set(),
+ {
+ nondet txid = oneOf(unknownTxids)
+ thirdPartyLearnsTxidWith(txid)
+ },
+ }
+
+ /// The third party asks the hub about a txid it knows. The lookup is not
+ /// authenticated.
+ action thirdPartyLookupWith(txid: TxId): bool = all {
+ s.thirdParty.requests < MAX_REQUESTS,
+ s.tpTxids().contains(txid),
+ commit(s.thirdPartySent(Lookup({ nonce: s.thirdParty.nextNonce, txid: txid }))),
+ }
+
+ action thirdPartyLookup = all {
+ s.thirdParty.requests < MAX_REQUESTS,
+ s.tpTxids() != Set(),
+ {
+ nondet txid = oneOf(s.tpTxids())
+ thirdPartyLookupWith(txid)
+ },
+ }
+
+ /// The third party submits a payload it has learned or the chain has
+ /// published. Submission is not authenticated either.
+ action thirdPartySubmitWith(payload: Payload): bool = all {
+ s.thirdParty.requests < MAX_REQUESTS,
+ s.tpPayloads().contains(payload),
+ commit(s.thirdPartySent(Submit({ nonce: s.thirdParty.nextNonce, payload: payload }))),
+ }
+
+ action thirdPartySubmit = all {
+ s.thirdParty.requests < MAX_REQUESTS,
+ s.tpPayloads() != Set(),
+ {
+ nondet payload = oneOf(s.tpPayloads())
+ thirdPartySubmitWith(payload)
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Step
+ // ------------------------------------------------------------------------
+
+ /// A fault: a timeout, or the hub losing what it holds.
+ action faultStep = any {
+ shimLookupTimeout, hubLose,
+ }
+
+ /// A step by someone outside the protocol: the third party.
+ action outsiderStep = any {
+ thirdPartyLearnsTxid, thirdPartyLookup, thirdPartySubmit,
+ }
+
+ /// One step of the system.
+ ///
+ /// Faults and outsiders are grouped so that the simulator, which chooses
+ /// uniformly among the alternatives it is given, takes one of each about as
+ /// often as it takes any single step of the protocol.
+ action step = any {
+ walletSend, walletGet,
+ shimReceive,
+ hubReceive, hubTake, indexerVerdict, hubReturn,
+ chainMine,
+ faultStep,
+ outsiderStep,
+ }
+
+ // The relations below are parts of `step`. Everything one of them reaches,
+ // `step` reaches, so they are sound for showing that a state is reachable
+ // and for nothing else. They keep a simulation on one part of the behaviour
+ // long enough to get deep into it.
+
+ /// The protocol with no faults and no outsiders.
+ action quietStep = any {
+ walletSend, walletGet,
+ shimReceive,
+ hubReceive, hubTake, indexerVerdict, hubReturn,
+ chainMine,
+ }
+
+ /// One migration, `early`, sent and asked about, with no faults and no
+ /// outsiders. Its three lookups can be answered pending (queued), not found
+ /// (the flush window) and served (accepted): G4's antecedent.
+ action earlyLookupStep = any {
+ walletSendWith(Clean(early), true), walletGetWith("early"),
+ shimReceive, hubReceive, hubTake, indexerVerdict,
+ }
+
+ // ------------------------------------------------------------------------
+ // Guarantees
+ // ------------------------------------------------------------------------
+ //
+ // The predicates are defined, and documented, above, each as
+ // `In(..)`: a predicate over a system and an audit record. These are
+ // their values in the current state, under the names the gate checks.
+
+ val operatorBlind = operatorBlindIn(s)
+ val queuedBytesConfidential = queuedBytesConfidentialIn(s)
+ val txidAuthenticity = txidAuthenticityIn(s)
+ val lookupValidityPerHub = lookupValidityPerHubIn(s, audit)
+
+ // ------------------------------------------------------------------------
+ // Known gaps: invariants that do not hold
+ // ------------------------------------------------------------------------
+
+ val statusNeverRegresses = statusNeverRegressesIn(s)
+
+ // ------------------------------------------------------------------------
+ // Witnesses
+ // ------------------------------------------------------------------------
+
+ val wPending = wPendingIn(s)
+ val wTxInMempool = wTxInMempoolIn(s)
+ val wTxMined = wTxMinedIn(s)
+ val wQueuedDisclosed = wQueuedDisclosedIn(s)
+ val wUnparseableMissed = wUnparseableMissedIn(s)
+ val wThirdPartyServedBody = wThirdPartyServedBodyIn(s)
+ val wTwinServed = wTwinServedIn(s)
+ val wFalseHeightServed = wFalseHeightServedIn(s)
+
+ // Non-vacuity: the antecedent of each guarantee is reachable.
+ val vOperatorBlind = vOperatorBlindIn(s)
+ val vQueuedBytesConfidential = vQueuedBytesConfidentialIn(s)
+ val vTxidAuthenticity = vTxidAuthenticityIn(s)
+ val vLookupValidityPerHub = vLookupValidityPerHubIn(s)
+
+ // ------------------------------------------------------------------------
+ // Run vocabulary
+ // ------------------------------------------------------------------------
+ //
+ // Shorthands for scripted runs. Each is a `...With` step with the choices an
+ // honest component and a truthful, reachable indexer would make, or a short
+ // sequence of such steps. A run that needs another choice (a Byzantine
+ // transition, an indexer that is down) uses the `...With` step itself.
+
+ /// A submission of `payload` from the shim to the hub under `nonce`.
+ pure def submitMail(nonce: Nonce, payload: Payload): Mail =
+ { src: ShimAddr, dst: HubAddr, msg: Submit({ nonce: nonce, payload: payload }) }
+
+ /// A lookup of `txid` from the shim to the hub under `nonce`.
+ pure def lookupMail(nonce: Nonce, txid: TxId): Mail =
+ { src: ShimAddr, dst: HubAddr, msg: Lookup({ nonce: nonce, txid: txid }) }
+
+ /// The same frame, sent by the third party instead.
+ pure def fromThirdParty(mail: Mail): Mail =
+ { ...mail, src: ThirdPartyAddr }
+
+ /// The hub's ack to the shim under `nonce`.
+ pure def ackMail(nonce: Nonce, ack: WireAck): Mail =
+ { src: HubAddr, dst: ShimAddr, msg: Ack({ nonce: nonce, ack: ack }) }
+
+ /// The hub's lookup reply to the shim under `nonce`.
+ pure def replyMail(nonce: Nonce, reply: WireReply): Mail =
+ { src: HubAddr, dst: ShimAddr, msg: LookupReply({ nonce: nonce, reply: reply }) }
+
+ /// The wallet sends, and the shim routes the transaction as it should.
+ action sends(input: SendInput, handedOver: bool): bool =
+ walletSendWith(input, handedOver)
+
+ /// The wallet sends a transaction and the transport takes the frame.
+ action sendToHub(payload: Payload): bool =
+ sends(Clean(payload), true)
+
+ /// The wallet asks, and the shim asks the hub.
+ action ask(query: TxId): bool =
+ walletGetWith(query)
+
+ /// `client`'s submission of `payload` under `nonce` reaches the hub, which
+ /// answers `ack`, and queues the payload if it accepts it.
+ action answerSubmitFrom(client: Addr, nonce: Nonce, payload: Payload, ack: WireAck): bool =
+ hubReceiveWith(
+ { src: client, dst: HubAddr, msg: Submit({ nonce: nonce, payload: payload }) },
+ INotFound,
+ { hub: if (ack == WAccepted) { ...s.hub, queue: s.hub.queue.union(Set(payload)) } else s.hub, reply: AAck(ack) },
+ )
+
+ /// The same, accepted.
+ action deliverSubmitFrom(client: Addr, nonce: Nonce, payload: Payload): bool =
+ answerSubmitFrom(client, nonce, payload, WAccepted)
+
+ /// The shim's submission of `payload` under `nonce` reaches the hub.
+ action deliverSubmit(nonce: Nonce, payload: Payload): bool =
+ deliverSubmitFrom(ShimAddr, nonce, payload)
+
+ /// `client`'s lookup of `txid` under `nonce` reaches the hub, which acts as
+ /// it should on the answer `answer` from its indexer.
+ action deliverLookupFrom(client: Addr, nonce: Nonce, txid: TxId, answer: IndexerAnswer): bool =
+ hubReceiveWith(
+ { src: client, dst: HubAddr, msg: Lookup({ nonce: nonce, txid: txid }) },
+ answer,
+ { hub: s.hub, reply: AWire(honestReplyOn(txid, answer)) },
+ )
+
+ /// The shim's lookup of `txid` under `nonce` reaches the hub, whose indexer
+ /// is reachable and truthful.
+ action deliverLookup(nonce: Nonce, txid: TxId): bool =
+ deliverLookupFrom(ShimAddr, nonce, txid, chainAnswer(s.indexer, txid))
+
+ /// `mail` reaches the shim, which acts as it should.
+ action deliverToShim(mail: Mail): bool =
+ shimReceiveWith(mail)
+
+ /// The reply an honest hub gives, in the current state, to a lookup of
+ /// `txid` on which its indexer would answer `answer`.
+ def honestReplyOn(txid: TxId, answer: IndexerAnswer): WireReply =
+ render(if (s.hub.queue.exists(payload => payload.txid == Some(txid))) QueueHit else FromIndexer(answer))
+
+ /// The same, with a truthful indexer.
+ def honestReply(txid: TxId): WireReply =
+ honestReplyOn(txid, chainAnswer(s.indexer, txid))
+
+ /// The shim's wait under `nonce` times out.
+ action timeOutLookup(nonce: Nonce): bool =
+ shimLookupTimeoutWith(nonce)
+
+ /// An honest indexer gives `verdict` on `payload`, with the effect that
+ /// verdict has.
+ action judge(payload: Payload, verdict: Verdict): bool =
+ indexerVerdictWith(payload, {
+ state: indexerApply(s.indexer, BroadcastIInput(payload), VerdictOutput(verdict)),
+ out: VerdictOutput(verdict),
+ })
+
+ /// The wallet sends `payload`, and the frame under `nonce` reaches the hub.
+ run submitTo(nonce: Nonce, payload: Payload): bool =
+ sendToHub(payload).then(deliverSubmit(nonce, payload))
+
+ /// The wallet asks for `query`; the lookup under `nonce` reaches the hub;
+ /// the reply reaches the shim. The hub's state does not change in between.
+ run lookUp(nonce: Nonce, query: TxId): bool =
+ ask(query)
+ .then(deliverLookup(nonce, query))
+ .then(deliverToShim(replyMail(nonce, honestReply(query))))
+
+ /// The hub flushes `batch`, and the indexer gives every entry `verdict`.
+ run flush(batch: List[Payload], verdict: Verdict): bool =
+ hubTake.then(batch.length().reps(i => judge(batch[i], verdict)))
+
+ /// The wallet's most recent answer.
+ def lastEvent: WalletEvent =
+ s.wallet.log[s.wallet.log.length() - 1]
+}
diff --git a/zeronym/spec/quint/shim.qnt b/zeronym/spec/quint/shim.qnt
new file mode 100644
index 00000000..4d5cefb7
--- /dev/null
+++ b/zeronym/spec/quint/shim.qnt
@@ -0,0 +1,180 @@
+// -*- mode: Bluespec; -*-
+
+/// The shim: it sits in front of an operator's indexer, forwards what is not
+/// a migration, and diverts every migration, and every transaction lookup, to
+/// the hub.
+///
+/// Like the hub it is one total function, `shim(state, input)`. Its state is
+/// only the lookups it is waiting on: it keeps no record of a migration once
+/// the wallet has its answer, which is why every lookup has to go to the hub.
+///
+/// The shim is honest in every configuration: it sees every migration in the
+/// clear and controls everything the wallet observes, so a Byzantine shim
+/// would void every wallet-facing guarantee and nothing else.
+module shim {
+ import basicSpells.* from "./spells/basicSpells"
+ import types.* from "./types"
+ import wire.* from "./wire"
+
+ // ------------------------------------------------------------------------
+ // State
+ // ------------------------------------------------------------------------
+
+ /// - `waiters`: the outstanding lookups, by nonce, with the txid each asks
+ /// about. A submission leaves nothing behind: the wallet has its answer
+ /// when the frame is handed over, and an ack, if one comes, is discarded.
+ /// - `nextNonce`: the source of fresh nonces. A counter stands for a random
+ /// value nobody else can guess.
+ type ShimState = { waiters: Nonce -> TxId, nextNonce: Nonce }
+
+ pure val initialShim: ShimState = { waiters: Map(), nextNonce: 0 }
+
+ // ------------------------------------------------------------------------
+ // Inputs and outputs
+ // ------------------------------------------------------------------------
+
+ type ShimInput =
+ // A wallet's `SendTransaction`. `handedOver` is whether the transport took
+ // the frame for the hub.
+ | SendTxSInput({ input: SendInput, handedOver: bool })
+ | GetTxSInput(TxId) // a wallet's `GetTransaction`
+ | FrameSInput(Msg) // a frame arrives from the network
+ | LookupTimeoutSInput(Nonce) // no reply to a lookup in time
+
+ type ShimOutput =
+ | ForwardOutput(Payload) // to the operator's indexer
+ // `payload` is what the wallet sent; `frame` goes to the hub; `told` is
+ // the wallet's answer.
+ | DivertedOutput({ payload: Payload, frame: Msg, told: SendObs })
+ | SendDoneOutput({ input: SendInput, obs: SendObs })
+ | LookupSentOutput(Msg) // to the hub
+ | LookupDoneOutput({ query: TxId, result: LookupObs })
+ | NoShimOutput
+ | ShimErrorOutput(str)
+
+ type ShimResult = Result[ShimState, ShimOutput]
+
+ pure def toForwardOutput(state: ShimState, payload: Payload): ShimResult =
+ { state: state, out: ForwardOutput(payload) }
+
+ pure def toDivertedOutput(state: ShimState, payload: Payload, frame: Msg, told: SendObs): ShimResult =
+ { state: state, out: DivertedOutput({ payload: payload, frame: frame, told: told }) }
+
+ pure def toSendDoneOutput(state: ShimState, input: SendInput, obs: SendObs): ShimResult =
+ { state: state, out: SendDoneOutput({ input: input, obs: obs }) }
+
+ pure def toLookupSentOutput(state: ShimState, frame: Msg): ShimResult =
+ { state: state, out: LookupSentOutput(frame) }
+
+ pure def toLookupDoneOutput(state: ShimState, query: TxId, result: LookupObs): ShimResult =
+ { state: state, out: LookupDoneOutput({ query: query, result: result }) }
+
+ pure def toNoShimOutput(state: ShimState): ShimResult =
+ { state: state, out: NoShimOutput }
+
+ pure def toShimErrorOutput(state: ShimState, reason: str): ShimResult =
+ { state: state, out: ShimErrorOutput(reason) }
+
+ // ------------------------------------------------------------------------
+ // Views
+ // ------------------------------------------------------------------------
+
+ /// Whether a transaction of this class is diverted. A body the shim cannot
+ /// parse is treated as a migration: forwarding it is the one outcome the
+ /// shim exists to prevent.
+ pure def treatAsMigration(class: Class): bool =
+ class != PassThrough
+
+ pure def hasWaiter(state: ShimState, nonce: Nonce): bool =
+ state.waiters.keys().contains(nonce)
+
+ /// The nonce a reply frame or a timeout refers to, if any.
+ pure def nonceOf(input: ShimInput): Option[Nonce] =
+ match input {
+ | FrameSInput(msg) =>
+ match msg {
+ | Ack(ack) => Some(ack.nonce)
+ | LookupReply(reply) => Some(reply.nonce)
+ | _ => None
+ }
+ | LookupTimeoutSInput(nonce) => Some(nonce)
+ | _ => None
+ }
+
+ // ------------------------------------------------------------------------
+ // SendTransaction
+ // ------------------------------------------------------------------------
+
+ /// Divert a migration: one frame to the hub, under a fresh nonce. The wallet
+ /// is told ok as soon as the frame has been handed over, and no ack is
+ /// waited for.
+ pure def divert(state: ShimState, payload: Payload, handedOver: bool): ShimResult =
+ if (not(handedOver))
+ state.toSendDoneOutput(Clean(payload), SendUnavailable)
+ else
+ { ...state, nextNonce: state.nextNonce + 1 }
+ .toDivertedOutput(payload, Submit({ nonce: state.nextNonce, payload: payload }), SentOk)
+
+ /// Route a `SendTransaction`. Nothing but a cleanly read pass-through
+ /// transaction ever reaches the operator; everything else is diverted or
+ /// fails closed.
+ pure def sendTransaction(state: ShimState, input: SendInput, handedOver: bool): ShimResult =
+ match input {
+ | Unreadable => state.toSendDoneOutput(input, SendUnavailable)
+ | EmptyBody => state.toSendDoneOutput(input, SendInvalid)
+ | Clean(payload) =>
+ if (not(treatAsMigration(payload.class))) state.toForwardOutput(payload)
+ else if (payload.oversize) state.toSendDoneOutput(input, SendTooLarge)
+ else divert(state, payload, handedOver)
+ }
+
+ // ------------------------------------------------------------------------
+ // GetTransaction
+ // ------------------------------------------------------------------------
+
+ /// Every lookup goes to the hub, under a fresh nonce.
+ pure def getTransaction(state: ShimState, query: TxId): ShimResult =
+ val nonce = state.nextNonce
+ { waiters: state.waiters.put(nonce, query), nextNonce: nonce + 1 }
+ .toLookupSentOutput(Lookup({ nonce: nonce, txid: query }))
+
+ /// A lookup got no reply in time. It fails closed.
+ pure def lookupTimeout(state: ShimState, nonce: Nonce): ShimResult =
+ if (not(state.hasWaiter(nonce)))
+ state.toShimErrorOutput("no request is waiting under this nonce")
+ else
+ { ...state, waiters: state.waiters.mapRemove(nonce) }
+ .toLookupDoneOutput(state.waiters.get(nonce), Unavailable)
+
+ // ------------------------------------------------------------------------
+ // Frames from the network
+ // ------------------------------------------------------------------------
+
+ /// A frame arrives. A lookup reply is matched to its lookup by its nonce
+ /// alone; under an unknown nonce it is dropped. An ack is dropped: nobody
+ /// waits for one.
+ pure def receive(state: ShimState, msg: Msg): ShimResult =
+ match msg {
+ | Ack(_) => state.toNoShimOutput()
+ | LookupReply(reply) =>
+ if (not(state.hasWaiter(reply.nonce))) state.toNoShimOutput()
+ else
+ val query = state.waiters.get(reply.nonce)
+ { ...state, waiters: state.waiters.mapRemove(reply.nonce) }
+ .toLookupDoneOutput(query, interpretReply(reply.reply, query))
+ | Submit(_) => state.toShimErrorOutput("not a reply frame")
+ | Lookup(_) => state.toShimErrorOutput("not a reply frame")
+ }
+
+ // ------------------------------------------------------------------------
+ // The shim function
+ // ------------------------------------------------------------------------
+
+ pure def shim(state: ShimState, input: ShimInput): ShimResult =
+ match input {
+ | SendTxSInput(send) => sendTransaction(state, send.input, send.handedOver)
+ | GetTxSInput(query) => getTransaction(state, query)
+ | FrameSInput(msg) => receive(state, msg)
+ | LookupTimeoutSInput(nonce) => lookupTimeout(state, nonce)
+ }
+}
diff --git a/zeronym/spec/quint/spells/basicSpells.qnt b/zeronym/spec/quint/spells/basicSpells.qnt
new file mode 100644
index 00000000..522f2c1d
--- /dev/null
+++ b/zeronym/spec/quint/spells/basicSpells.qnt
@@ -0,0 +1,72 @@
+// -*- mode: Bluespec; -*-
+
+/// Small, protocol-free helpers. A spell lives here only while something in the
+/// specification calls it, and each one carries its own test.
+module basicSpells {
+ /// A value that may be absent.
+ type Option[a] = Some(a) | None
+
+ /// Whether the option holds a value.
+ pure def isSome(opt: Option[a]): bool =
+ match opt {
+ | Some(_) => true
+ | None => false
+ }
+
+ run isSomeTest = all {
+ assert(isSome(Some(1))),
+ assert(not(isSome(None))),
+ }
+
+ /// The held value, or `default` when there is none.
+ pure def unwrapOr(opt: Option[a], default: a): a =
+ match opt {
+ | Some(value) => value
+ | None => default
+ }
+
+ run unwrapOrTest = all {
+ assert(unwrapOr(Some(1), 7) == 1),
+ assert(unwrapOr(None, 7) == 7),
+ }
+
+ /// What `f` keeps of `items`.
+ pure def filterMap(items: Set[a], f: a => Option[b]): Set[b] =
+ items.fold(Set(), (acc, elem) =>
+ match f(elem) {
+ | Some(kept) => acc.union(Set(kept))
+ | None => acc
+ })
+
+ run filterMapTest = all {
+ assert(Set(1, 2, 3).filterMap(n => if (n > 1) Some(n * 10) else None) == Set(20, 30)),
+ assert(Set(1).filterMap(n => if (n > 1) Some(n) else None) == Set()),
+ }
+
+ /// `items` without `elem`.
+ pure def setRemove(items: Set[a], elem: a): Set[a] =
+ items.exclude(Set(elem))
+
+ run setRemoveTest = all {
+ assert(Set(1, 2, 3).setRemove(2) == Set(1, 3)),
+ assert(Set(1, 2).setRemove(5) == Set(1, 2)),
+ }
+
+ /// `entries` without the keys in `dropped`.
+ pure def mapRemoveSet(entries: a -> b, dropped: Set[a]): a -> b =
+ entries.keys().exclude(dropped).mapBy(key => entries.get(key))
+
+ run mapRemoveSetTest = all {
+ assert(Map(1 -> "a", 2 -> "b", 3 -> "c").mapRemoveSet(Set(1, 3)) == Map(2 -> "b")),
+ assert(Map(1 -> "a").mapRemoveSet(Set()) == Map(1 -> "a")),
+ }
+
+ /// `entries` without `key`.
+ pure def mapRemove(entries: a -> b, key: a): a -> b =
+ entries.mapRemoveSet(Set(key))
+
+ run mapRemoveTest = all {
+ assert(Map(1 -> "a", 2 -> "b").mapRemove(1) == Map(2 -> "b")),
+ assert(Map(1 -> "a").mapRemove(9) == Map(1 -> "a")),
+ }
+}
diff --git a/zeronym/spec/quint/spells/soup.qnt b/zeronym/spec/quint/spells/soup.qnt
new file mode 100644
index 00000000..7044b986
--- /dev/null
+++ b/zeronym/spec/quint/spells/soup.qnt
@@ -0,0 +1,67 @@
+// -*- mode: Bluespec; -*-
+
+/// A message soup: the standard abstraction of an unreliable network.
+///
+/// The soup only grows. A message, once sent, stays available for delivery
+/// forever, and delivering it does not remove it. That one rule gives every
+/// fault an asynchronous network can show without a separate action for each:
+///
+/// - loss: a message is never chosen for delivery;
+/// - duplication: a message is chosen more than once;
+/// - delay and reordering: messages are chosen in any order, at any time.
+///
+/// What the soup does not give is forgery. A message is in it only because some
+/// participant's transition put it there.
+///
+/// The module is generic in the address type `p` and the message type `m`.
+module soup {
+ /// A message in transit, with the addresses it travels between.
+ type Envelope[p, m] = { src: p, dst: p, msg: m }
+
+ /// Everything ever sent.
+ type Soup[p, m] = Set[Envelope[p, m]]
+
+ /// `soup` after one more message is sent.
+ pure def send(soup: Soup[p, m], envelope: Envelope[p, m]): Soup[p, m] =
+ soup.union(Set(envelope))
+
+ /// `soup` after a set of messages is sent.
+ pure def sendAll(soup: Soup[p, m], envelopes: Set[Envelope[p, m]]): Soup[p, m] =
+ soup.union(envelopes)
+
+ /// The messages that may be delivered to `addr`.
+ pure def inbox(soup: Soup[p, m], addr: p): Soup[p, m] =
+ soup.filter(envelope => envelope.dst == addr)
+
+ /// The messages `addr` has sent.
+ pure def outbox(soup: Soup[p, m], addr: p): Soup[p, m] =
+ soup.filter(envelope => envelope.src == addr)
+
+ // Tested at two instantiations, (str, int) and (int, bool), to show the
+ // definitions do not depend on either type.
+
+ pure val ab = { src: "a", dst: "b", msg: 1 }
+ pure val ba = { src: "b", dst: "a", msg: 2 }
+
+ run sendTest = all {
+ assert(Set().send(ab) == Set(ab)),
+ assert(Set(ab).send(ab) == Set(ab)),
+ assert(Set().send({ src: 1, dst: 2, msg: true }).size() == 1),
+ }
+
+ run sendAllTest = all {
+ assert(Set(ab).sendAll(Set(ab, ba)) == Set(ab, ba)),
+ assert(Set({ src: 1, dst: 2, msg: true }).sendAll(Set()).size() == 1),
+ }
+
+ run inboxTest = all {
+ assert(Set(ab, ba).inbox("b") == Set(ab)),
+ assert(Set(ab, ba).inbox("c") == Set()),
+ assert(Set({ src: 1, dst: 2, msg: true }).inbox(2).size() == 1),
+ }
+
+ run outboxTest = all {
+ assert(Set(ab, ba).outbox("b") == Set(ba)),
+ assert(Set({ src: 1, dst: 2, msg: true }).outbox(2) == Set()),
+ }
+}
diff --git a/zeronym/spec/quint/tests/hubScenariosTest.qnt b/zeronym/spec/quint/tests/hubScenariosTest.qnt
new file mode 100644
index 00000000..b6c3ae9d
--- /dev/null
+++ b/zeronym/spec/quint/tests/hubScenariosTest.qnt
@@ -0,0 +1,547 @@
+// -*- mode: Bluespec; -*-
+
+/// Scripted runs of the hub specification.
+///
+/// A run is a sequence of the machine's own steps from `initWith(c)`. Where a
+/// run says a property fails, it also says what in the state makes it fail.
+/// Where a Byzantine choice breaks a property, the run asserts the property
+/// just before that choice.
+///
+/// The schedule in every configuration: the chain starts at height 1, a flush
+/// is scheduled at heights 3, 6, 9 and 12, and the mining margin is 2 blocks.
+module hubScenariosTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import indexer.* from "../indexer"
+ import hub.* from "../hub"
+ import hubMachine.* from "../hubMachine"
+
+ // ------------------------------------------------------------------------
+ // Run vocabulary
+ // ------------------------------------------------------------------------
+ //
+ // Each is a `...With` step with the choice an honest hub and a truthful,
+ // reachable indexer would make, or a short sequence of such steps. A run
+ // that needs another choice uses the `...With` step itself.
+
+ /// What an honest hub does with a submission of `payload` now.
+ def honestly(payload: Payload): HubResult =
+ hub(h, SubmitHInput({ nonce: 0, payload: payload }))
+
+ /// The decision an honest hub would give `payload` now.
+ def decision(payload: Payload): AckKind =
+ admission(h, payload)
+
+ /// A submission of `payload` reaches the hub, which acts as it should.
+ action deliver(payload: Payload): bool =
+ submitWith(payload, honestly(payload))
+
+ /// The hub observes the true height.
+ action see = observeWith(height)
+
+ /// The hub of configuration `c`, running at the genesis height.
+ run started(c: HubConfig): bool = initWith(c).then(see)
+
+ /// One block arrives and the hub sees it.
+ run block = advance.then(see)
+
+ /// `count` blocks arrive, each seen by the hub. No flush may fall due on the
+ /// way.
+ run blocks(count: int): bool = count.reps(_ => block)
+
+ /// `count` blocks arrive and the hub hears of none.
+ run unseenBlocks(count: int): bool = count.reps(_ => advance)
+
+ /// An honest indexer gives `given` on `payload`, with the effect that
+ /// verdict has.
+ action judge(payload: Payload, given: Verdict): bool =
+ verdictWith(payload, given, given == Accepted)
+
+ /// The hub flushes `batch`, and the indexer gives every entry `given`.
+ run flush(batch: List[Payload], given: Verdict): bool =
+ flushBegin
+ .then(batch.length().reps(i => judge(batch[i], given)))
+ .then(flushEnd)
+
+ /// What the requeue at the end of the flush in flight would report.
+ def requeueReport: HubOutput =
+ hub(h, FlushDoneHInput).out
+
+ /// The hub is publishing a scheduled batch for an epoch the chain has not
+ /// reached: its cadence clock is ahead of the true height.
+ def flushesAheadOfChain: bool =
+ h.flush != Idle and h.cadenceEpoch() > height / cfg.params.flushInterval
+
+ /// Whether a node would take `payload` now.
+ def nodeWouldTake(payload: Payload): bool =
+ verdictsOn(payload).contains((Accepted, true))
+
+ /// What a Byzantine hub answers when it takes `payload` into its queue
+ /// whatever the admission rules say.
+ def admitting(payload: Payload): HubResult =
+ { ...h, queue: h.queue.put(payload, 0) }.toAckOutput(0, Admitted)
+
+ pure def requeued(held: int, droppedExpired: int, droppedExhausted: int): HubOutput =
+ RequeuedOutput({ held: held, droppedExpired: droppedExpired, droppedExhausted: droppedExhausted })
+
+ // ------------------------------------------------------------------------
+ // Configurations
+ // ------------------------------------------------------------------------
+
+ /// Every named init has an initial state. A configuration that does not
+ /// meet the assumptions in its guard stops this run.
+ run liveInitsTest =
+ initTimely
+ .then(initFlakyTip)
+ .then(initFlakyTipNoSlack)
+ .then(initFlakyTipSlowFlight)
+ .then(initStaleLag)
+ .then(initStaleLagWithSlack)
+ .then(initByzHub)
+ .then(initByzIndexer)
+ .then(initUnknownUpgrade)
+ .expect(cfg == unknownUpgrade and h == startingHub(unknownUpgrade.params) and height == GENESIS_HEIGHT)
+
+ // ------------------------------------------------------------------------
+ // The schedule under a timely tip
+ // ------------------------------------------------------------------------
+
+ /// A supported wallet's transaction, from admission to the mempool: offered
+ /// at the first boundary after it arrived, and accepted after a block in
+ /// flight.
+ run admittedThenPublishedTest =
+ started(timely)
+ .then(block)
+ .then(deliver(early))
+ .expect(h.queued() == Set(early) and seen == Set(early) and onTime == Set(early) and owed == Set(early))
+ .then(block)
+ .then(flushBegin)
+ .expect(h.inFlight() == Set(early) and flightStart == 3)
+ .expect(wConformingFirstOffer)
+ .then(advance)
+ .expect(height == 4 and not(mayAdvance) and wConformingFirstOfferInFlightABlock and wBlockInFlight)
+ .then(judge(early, Accepted))
+ .then(flushEnd)
+ .expect(onChain == Set(early) and offered == Set(early) and owed == Set() and flightStart == 0)
+ .expect(conformingFirstOfferBeforeExpiry and conformingFirstOfferJudgedBeforeExpiry)
+ .expect(conformingEveryOfferBeforeExpiry and ackedIsHeldOrSettled)
+
+ // ------------------------------------------------------------------------
+ // K5. Acknowledged, then lost
+ // ------------------------------------------------------------------------
+
+ /// K5a. The hub crashes after the ack. The queue was in memory.
+ run ackedThenCrashedTest =
+ started(timely)
+ .then(block)
+ .then(deliver(early))
+ .expect(owed == Set(early) and ackedIsHeldOrSettled)
+ .then(crash)
+ .expect(h == downHub(timely.params) and onChain == Set() and offered == Set())
+ .expect(not(ackedIsHeldOrSettled))
+
+ /// K5b. The final flush of a draining hub finds the indexer unreachable.
+ /// The entry was offered and nothing judged it; the hub stops, forgetting
+ /// the offer with the rest of its run, and the transaction is held nowhere.
+ run ackedThenLostAtDrainTest =
+ started(timely)
+ .then(block)
+ .then(deliver(early))
+ .then(drain)
+ .then(flush([early], Retryable))
+ .expect(h.phase == Stopped and h.queued() == Set() and h.inFlight() == Set() and onChain == Set())
+ .expect(offered == Set() and owed == Set(early))
+ .expect(not(ackedIsHeldOrSettled))
+
+ /// K5c. A requeue gives an acknowledged entry up as expired. No crash and
+ /// no shutdown: the flushes at 3 and at 6 both come back unjudged, and an
+ /// expiry of 9 does not survive the flush at 9.
+ run requeueDropsAckedAsExpiredTest =
+ started(timely)
+ .then(block)
+ .then(deliver(early))
+ .then(block)
+ .then(flushBegin)
+ .then(judge(early, Retryable))
+ .expect(requeueReport == requeued(1, 0, 0))
+ .then(flushEnd)
+ .then(blocks(3))
+ .then(flushBegin)
+ .then(judge(early, Retryable))
+ .expect(requeueReport == requeued(0, 1, 0))
+ .then(flushEnd)
+ .expect(h.phase == Running and h.queue == Map())
+ .expect(owed == Set(early) and not(ackedIsHeldOrSettled))
+
+ // ------------------------------------------------------------------------
+ // The unknown upgrade
+ // ------------------------------------------------------------------------
+
+ /// A payload the hub cannot parse has no txid and no expiry. The expiry
+ /// rule never refuses it and never gives it up, so the attempt bound is the
+ /// only limit on its requeue: after the third unjudged flush it is dropped
+ /// as exhausted. On the way `tight`, acknowledged, is dropped as expired.
+ run requeueAndDropTest =
+ started(unknownUpgrade)
+ .then(deliver(junk))
+ .then(block)
+ .then(deliver(tight))
+ .then(block)
+ .then(flushBegin)
+ // A fresh admission while the batch is out.
+ .then(deliver(early))
+ .expect(h.queued() == Set(early) and h.inFlight() == Set(junk, tight))
+ .then(judge(junk, Retryable))
+ .then(judge(tight, Retryable))
+ .expect(requeueReport == requeued(1, 1, 0))
+ .then(flushEnd)
+ .expect(h.queue == Map(early -> 0, junk -> 1) and wRequeued)
+ .expect(owed.contains(tight) and not(ackedIsHeldOrSettled))
+ .then(blocks(3))
+ .then(flushBegin)
+ .then(judge(early, Accepted))
+ .then(judge(junk, Retryable))
+ .then(flushEnd)
+ .expect(h.queue == Map(junk -> 2))
+ // The third failure is one more than the attempts allowed.
+ .then(blocks(3))
+ .then(flushBegin)
+ .then(judge(junk, Retryable))
+ .expect(requeueReport == requeued(0, 0, 1))
+ .then(flushEnd)
+ .expect(h.queue == Map() and owed.contains(junk))
+
+ // ------------------------------------------------------------------------
+ // A tip reported behind the chain
+ // ------------------------------------------------------------------------
+
+ /// A supported wallet's transaction is admitted against a tip reported one
+ /// block back, below a boundary the hub has already flushed, and so flushed
+ /// one block late.
+ run regressedTipDelaysFlush(c: HubConfig, payload: Payload): bool =
+ started(c)
+ .then(blocks(2))
+ .then(flushBegin)
+ .then(observeWith(2))
+ .then(deliver(payload))
+ .expect(height == 3 and onTime == Set(payload))
+ .then(blocks(2))
+ .then(unseenBlocks(2))
+ .then(observeWith(6))
+ .then(flushBegin)
+ .expect(flightStart == 7 and h.inFlight() == Set(payload))
+ .expect(conforming(payload, cfg.params.minWalletExpiry))
+
+ /// K3'. The expiry floor equals the three-term budget, with no slack for
+ /// the reorg allowance. The flush is one block late and the transaction
+ /// misses the mining margin by that block. With the slack, G6b and G6c hold
+ /// on `flakyTip` in every reachable state.
+ run conformingMissesMarginWithoutSlackTest =
+ regressedTipDelaysFlush(flakyTipNoSlack, orchard("early", 2, 8))
+ .expect(not(reorgSlackFits(cfg)))
+ .expect(not(conformingFirstOfferBeforeExpiry))
+
+ /// K7. With the slack, and the batch in flight for two blocks, as many as
+ /// the margin reserves. The offer left the whole margin, and G6b holds. By
+ /// the time the node looks, the transaction can no longer be mined: the
+ /// budget had already spent the slack, and the flight spent the margin.
+ run slowFlightSpendsTheMarginTest =
+ regressedTipDelaysFlush(flakyTipSlowFlight, early)
+ .then(unseenBlocks(2))
+ .expect(height == 9 and early.expiry == Some(9) and not(flightWithinMargin(cfg)))
+ .expect(not(nodeWouldTake(early)))
+ .expect(conformingFirstOfferBeforeExpiry and not(conformingFirstOfferJudgedBeforeExpiry))
+ .then(judge(early, Rejected))
+
+ /// A supported wallet's transaction is admitted on time at height 2. At
+ /// height 6 the hub, having adopted that epoch without flushing, is told
+ /// the tip is 5, and a duplicate of the submission arrives. The hub is shut
+ /// down at 8.
+ run duplicateBehindTheBoundary(lost: bool): bool =
+ started(flakyTip)
+ .then(block)
+ .then(deliver(early))
+ .expect(onTime == Set(early))
+ .then(
+ if (lost) crash.then(unseenBlocks(4)).then(restart).then(see)
+ else block.then(flush([early], Accepted)).then(blocks(3)).then(flushBegin)
+ )
+ .expect(height == 6 and h.lastEpoch == Some(2))
+ .then(observeWith(5))
+ .then(deliver(early))
+ .expect(h.queued() == Set(early))
+ .then(see)
+ .then(blocks(2))
+ .then(drain)
+ .then(flushBegin)
+ .expect(flightStart == 8 and h.inFlight() == Set(early) and not(marginLeft(early, flightStart)))
+
+ /// K8 (finding 6). The hub crashed in between and lost its queue. To it the
+ /// duplicate is a first arrival, four blocks late, and admission counts on
+ /// the flush at 6, which will not happen. The wallet's transaction was on
+ /// time, was acknowledged, and is first offered with one block of margin
+ /// where two are reserved. G6b and G6c hold: they are about arrivals this
+ /// run of the hub knows to be timely.
+ run crashThenLateDuplicateTest =
+ duplicateBehindTheBoundary(true)
+ .expect(reorgSlackFits(cfg) and onTime == Set() and offered == Set())
+ .expect(conformingFirstOfferBeforeExpiry)
+ .then(advance)
+ .expect(not(nodeWouldTake(early)) and conformingFirstOfferJudgedBeforeExpiry)
+
+ /// K8, control. No crash: the transaction is published by the flush at 3.
+ /// The late offer at 8 is a second offer of an entry whose first was in
+ /// time.
+ run lateDuplicateWithoutCrashTest =
+ duplicateBehindTheBoundary(false)
+ .expect(onTime == Set(early) and offered == Set(early))
+ .expect(conformingFirstOfferBeforeExpiry and not(conformingEveryOfferBeforeExpiry))
+
+ /// A hub that comes back up owes a fresh arrival the whole margin, even
+ /// with the tip reported one block behind throughout. The hub restarts at
+ /// height 3 and is told the tip is 2; `early` arrives then, on time. The
+ /// flush falls due when the hub hears of height 6, which is at 7, and the
+ /// offer leaves exactly the margin.
+ run freshAfterRestartMeetsMarginTest =
+ initWith(flakyTip)
+ .then(crash)
+ .then(unseenBlocks(2))
+ .then(restart)
+ .then(see)
+ .then(observeWith(2))
+ .then(deliver(early))
+ .expect(height == 3 and onTime == Set(early))
+ .then(4.reps(i => advance.then(observeWith(3 + i))))
+ .expect(height == 7 and h.tip == Some(6) and not(mayAdvance))
+ .then(flushBegin)
+ .expect(flightStart == 7 and wConformingFirstOffer and conformingFirstOfferBeforeExpiry)
+ .then(advance)
+ .expect(height == 8 and not(mayAdvance))
+ .expect(wConformingFirstOfferInFlightABlock and conformingFirstOfferJudgedBeforeExpiry)
+ .then(judge(early, Accepted))
+
+ // ------------------------------------------------------------------------
+ // A hub that hears nothing for a while
+ // ------------------------------------------------------------------------
+
+ /// The hub hears nothing after height 5, one block short of the flush at 6,
+ /// while the chain goes on. Its cadence still follows the tip it last saw,
+ /// so nothing is flushed until it goes stale at height 8.
+ run silenceAcrossBoundary(c: HubConfig, payload: Payload): bool =
+ started(c)
+ .then(blocks(2))
+ .then(flushBegin)
+ .then(deliver(payload))
+ .expect(height == 3 and onTime == Set(payload))
+ .then(blocks(2))
+ .then(unseenBlocks(3))
+ .expect(height == 8 and h.tip == Some(5) and not(h.isFlushDue()))
+ .then(staleWith(8))
+ .then(flushBegin)
+ .expect(flightStart == 8 and h.inFlight() == Set(payload))
+ .expect(conforming(payload, cfg.params.minWalletExpiry))
+
+ /// K4. A supported wallet's transaction, expiring at 9, is offered at 8:
+ /// not yet expired, with one block of margin where two are reserved. One
+ /// block arrives while the batch is in flight, as the margin allows for,
+ /// and the node can no longer take it.
+ run silenceAcrossBoundaryMissesMarginTest =
+ silenceAcrossBoundary(staleLag, early)
+ .expect(not(conformingFirstOfferBeforeExpiry))
+ .then(advance)
+ .expect(height == 9 and not(mayAdvance) and flightWithinMargin(cfg))
+ .expect(not(nodeWouldTake(early)) and not(conformingFirstOfferJudgedBeforeExpiry))
+ .then(judge(early, Rejected))
+
+ /// K4, contrast. The same steps with an expiry floor one block higher,
+ /// which is the relation `staleSlackFits` asks for. The same late flush
+ /// leaves the margin, and after a block in flight the node accepts.
+ run sameSilenceWithSlackKeepsMarginTest =
+ silenceAcrossBoundary(staleLagWithSlack, orchard("early", 2, 10))
+ .expect(staleSlackFits(cfg) and wConformingFirstOffer and conformingFirstOfferBeforeExpiry)
+ .then(advance)
+ .expect(height == 9 and conformingFirstOfferJudgedBeforeExpiry)
+ .then(judge(orchard("early", 2, 10), Accepted))
+ .expect(onChain == Set(orchard("early", 2, 10)))
+
+ /// A stale hub's flush finds the indexer unreachable, twice. Requeue judges
+ /// the entry at the observed tip, which stopped at 5: the next flush it
+ /// knows of is the one at 6, so an expiry of 11 looks safe both times. The
+ /// free-running schedule offers it again at 12.
+ run requeuedTwiceWhileStale: bool =
+ started(staleLag)
+ .then(blocks(2))
+ .then(flushBegin)
+ .then(blocks(2))
+ .then(deliver(late))
+ .then(unseenBlocks(3))
+ .then(staleWith(8))
+ .then(flush([late], Retryable))
+ .expect(h.queue == Map(late -> 1))
+ .then(advance)
+ .then(staleWith(9))
+ .then(flush([late], Retryable))
+ .expect(h.queue == Map(late -> 2) and h.tip == Some(5))
+ .then(3.reps(i => advance.then(staleWith(10 + i))))
+ .then(flushBegin)
+ .expect(flightStart == 12 and late.expiry == Some(11))
+
+ /// K6. The third offer is past the expiry. The first was in time, which is
+ /// all G6b covers.
+ run requeuedPastExpiryTest =
+ requeuedTwiceWhileStale
+ .expect(not(conformingEveryOfferBeforeExpiry) and conformingFirstOfferBeforeExpiry)
+
+ /// Finding 7. The third flush comes back unjudged as well, and the entry,
+ /// which has an expiry, is dropped as exhausted: the expiry rule, reading a
+ /// tip that stopped at 5, still does not give it up.
+ run expiringEntryDroppedAsExhaustedTest =
+ requeuedTwiceWhileStale
+ .then(judge(late, Retryable))
+ .expect(isSome(late.expiry) and requeueReport == requeued(0, 0, 1))
+ .then(flushEnd)
+ .expect(h.queue == Map())
+
+ /// A stale hub's free-running clock reads 6 at true height 5, and the flush
+ /// scheduled for 6 runs a block early.
+ run freeRunningClockFlushesEarlyTest =
+ started(staleLag)
+ .then(block)
+ .then(deliver(early))
+ .then(unseenBlocks(3))
+ .then(staleWith(6))
+ .then(flushBegin)
+ .expect(height == 5 and h.cadence == FreeRunning(6) and h.inFlight() == Set(early))
+ .expect(flushesAheadOfChain and conformingFirstOfferBeforeExpiry)
+
+ /// A stale hub refuses submissions until it sees the tip move again.
+ run staleHubRefusesTest =
+ started(staleLag)
+ .then(unseenBlocks(3))
+ .then(staleWith(4))
+ .expect(wStale and decision(early) == Refused(TipStale))
+ .then(deliver(early))
+ .expect(h.queued() == Set())
+ .then(see)
+ .expect(h.phase == Running and h.cadence == Tracking)
+ .then(deliver(early))
+ .expect(h.queued() == Set(early))
+
+ /// Finding 2; the slack does not cover it. A stale hub's free-running clock
+ /// reads 6 at true height 4, and the flush scheduled for 6 runs then, with
+ /// nothing to publish. When the hub sees the tip again the chain is at 5,
+ /// and admission, which knows the tip and not the schedule's history,
+ /// counts on the flush at 6. That flush has already happened. The
+ /// transaction waits for the one at 9, and a second, shorter silence makes
+ /// that one late too: it is offered at 11 with expiry 12, one block of
+ /// margin where two are reserved, and a block in flight uses that up.
+ ///
+ /// Neither half is enough alone at these numbers. Without the early flush
+ /// the transaction goes out at 6; without the second silence, at 9.
+ run earlyFlushSpendsTheNextEpochTest =
+ val lateAtFloor = orchard("late", 4, 12)
+ started(staleLagWithSlack)
+ .then(unseenBlocks(3))
+ .then(staleWith(6))
+ .then(flushBegin)
+ .expect(height == 4 and h.lastEpoch == Some(2))
+ .then(block)
+ .expect(h.cadence == Tracking and h.tip == Some(5))
+ .then(deliver(lateAtFloor))
+ .expect(onTime == Set(lateAtFloor))
+ .then(blocks(3))
+ // Height 8. The boundary at 6 has passed and nothing was flushed.
+ .expect(offered == Set() and h.queued() == Set(lateAtFloor))
+ .then(unseenBlocks(3))
+ .then(staleWith(11))
+ .then(flushBegin)
+ .expect(conforming(lateAtFloor, cfg.params.minWalletExpiry) and staleSlackFits(cfg))
+ .expect(flightStart == 11 and not(conformingFirstOfferBeforeExpiry))
+ .then(advance)
+ .expect(height == 12 and not(nodeWouldTake(lateAtFloor)))
+ .expect(not(conformingFirstOfferJudgedBeforeExpiry))
+ .then(judge(lateAtFloor, Rejected))
+
+ // ------------------------------------------------------------------------
+ // A Byzantine hub
+ // ------------------------------------------------------------------------
+
+ /// G6b and G6c need the hub. A supported wallet's transaction is refused by
+ /// an honest hub only for reasons that are not about the transaction. This
+ /// hub takes one while it has not yet seen a tip, when an honest hub
+ /// refuses everything. It first sees the chain at height 7, adopts that
+ /// epoch without flushing, and offers the transaction at 9, its expiry,
+ /// when no node can take it.
+ run hubAdmitsBeforeFirstTipTest =
+ initWith(byzHub)
+ .then(unseenBlocks(2))
+ .expect(decision(early) == Refused(TipStale))
+ .expect(conformingFirstOfferBeforeExpiry and conformingFirstOfferJudgedBeforeExpiry)
+ .then(submitWith(early, admitting(early)))
+ .expect(h.phase == Starting and height == 3 and onTime == Set(early))
+ .then(unseenBlocks(4))
+ .then(see)
+ .then(blocks(2))
+ .then(flushBegin)
+ .expect(conforming(early, cfg.params.minWalletExpiry) and flightStart == 9)
+ .expect(not(conformingFirstOfferBeforeExpiry))
+ .expect(not(nodeWouldTake(early)) and not(conformingFirstOfferJudgedBeforeExpiry))
+ .then(judge(early, Rejected))
+
+ /// A3 needs the hub. Once its drain has begun, it takes a submission into
+ /// the queue: draining before and after, nothing in flight, and the queue
+ /// grown by a payload no flush handed back.
+ run hubAdmitsWhileDrainingTest =
+ started(byzHub)
+ .then(block)
+ .then(deliver(early))
+ .then(drain)
+ .expect(h.phase == Draining and h.queued() == Set(early) and h.inFlight() == Set())
+ .expect(decision(tight) == Refused(HubDraining))
+ .then(submitWith(tight, admitting(tight)))
+ .expect(h.phase == Draining and h.queued() == Set(early, tight))
+
+ // ------------------------------------------------------------------------
+ // A Byzantine indexer
+ // ------------------------------------------------------------------------
+
+ /// Premature flush. The indexer reports tip 3 at true height 2; the hub
+ /// believes the boundary has come and publishes what it holds. One lying
+ /// endpoint is enough for this: the tip is the maximum over endpoints. The
+ /// transaction is published early, which costs it nothing.
+ run tipAheadOfChainFlushesEarlyTest =
+ started(byzIndexer)
+ .then(block)
+ .then(deliver(early))
+ .then(observeWith(3))
+ .then(flushBegin)
+ .expect(height == 2 and h.tip == Some(3) and h.inFlight() == Set(early))
+ .expect(flushesAheadOfChain)
+ .expect(conformingFirstOfferBeforeExpiry)
+
+ /// The hub asks for the tip at every block. The indexer goes on answering 2
+ /// while `silence` more blocks arrive, and then answers truthfully. The
+ /// flush scheduled for 3 runs then.
+ run tipWithheld(payload: Payload, silence: int): bool =
+ started(byzIndexer)
+ .then(block)
+ .then(deliver(payload))
+ .expect(conformingFirstOfferBeforeExpiry and conformingFirstOfferJudgedBeforeExpiry)
+ .then((silence - 1).reps(_ => advance.then(observeWith(2))))
+ .then(advance)
+ .expect(height == 2 + silence and h.tip == Some(2) and not(mayAdvance))
+ .then(see)
+ .then(flushBegin)
+ .expect(flightStart == 2 + silence and h.inFlight() == Set(payload))
+
+ /// G6b and G6c need the indexer. With the tip withheld up to height 8, a
+ /// supported wallet's transaction is offered at 8 with expiry 9, and after
+ /// one block in flight the node cannot take it.
+ run indexerWithholdsTipFromConformingTest =
+ tipWithheld(early, 6)
+ .expect(conforming(early, cfg.params.minWalletExpiry) and onTime == Set(early))
+ .expect(not(conformingFirstOfferBeforeExpiry))
+ .then(advance)
+ .expect(not(nodeWouldTake(early)) and not(conformingFirstOfferJudgedBeforeExpiry))
+ .then(judge(early, Rejected))
+}
diff --git a/zeronym/spec/quint/tests/hubTest.qnt b/zeronym/spec/quint/tests/hubTest.qnt
new file mode 100644
index 00000000..9a899f30
--- /dev/null
+++ b/zeronym/spec/quint/tests/hubTest.qnt
@@ -0,0 +1,470 @@
+// -*- mode: Bluespec; -*-
+
+/// The hub function, checked on a small schedule: a flush every 3 blocks, a
+/// mining margin of 1, at most 2 requeues.
+module hubTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import hub.* from "../hub"
+ import wire.* from "../wire"
+ import abstractHub.* from "../abstractHub"
+
+ pure val PARAMS: HubParams = {
+ flushInterval: 3,
+ miningMargin: 1,
+ deliveryLag: 1,
+ minWalletExpiry: 6,
+ reorgAllowance: 1,
+ maxAttempts: 2,
+ }
+
+ pure def orchard(id: str, expiry: Option[Height]): Payload =
+ { id: id, txid: Some(id), created: 1, expiry: expiry, class: OrchardTouching, oversize: false }
+
+ pure val pA = orchard("a", Some(9))
+ pure val pB = orchard("b", Some(9))
+ pure val pC = orchard("c", None)
+ pure val pTight = orchard("tight", Some(6))
+ pure val pJunk = { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, oversize: false }
+
+ pure val PAYLOADS = Set(pA, pB, pC, pTight, pJunk)
+ pure val REFUSALS = Set(TipStale, HubDraining, ExpiryTooTight)
+
+ /// The state after `input`.
+ pure def after(state: HubState, input: HubInput): HubState =
+ hub(state, input).state
+
+ /// The output of `input`.
+ pure def outputOf(state: HubState, input: HubInput): HubOutput =
+ hub(state, input).out
+
+ pure def isError(output: HubOutput): bool =
+ match output {
+ | HubErrorOutput(_) => true
+ | _ => false
+ }
+
+ pure def submit(payload: Payload): HubInput =
+ SubmitHInput({ nonce: 0, payload: payload })
+
+ pure def verdict(payload: Payload, given: Verdict): HubInput =
+ VerdictHInput({ payload: payload, verdict: given })
+
+ pure val down = downHub(PARAMS)
+ pure val starting = startingHub(PARAMS)
+ pure def running(tip: Height): HubState = starting.after(TipHInput(tip))
+
+ /// Running at tip 5 with `pA` and `pJunk` queued.
+ pure val holding = running(5).after(submit(pA)).after(submit(pJunk))
+ /// The same hub one block later, with its flush in flight.
+ pure val flushing = holding.after(TipHInput(6)).after(FlushDueHInput)
+ pure val stale = running(5).after(StaleHInput(8))
+ pure val draining = holding.after(DrainHInput)
+ pure val stopped = draining.after(FlushDueHInput).after(verdict(pA, Accepted))
+ .after(verdict(pJunk, Rejected)).after(FlushDoneHInput)
+
+ pure val STATES = Set(down, starting, running(2), running(5), holding, flushing, stale, draining, stopped,
+ stale.after(DrainHInput), flushing.after(verdict(pA, Retryable)))
+
+ pure val INPUTS: Set[HubInput] =
+ PAYLOADS.map(payload => submit(payload))
+ .union(Set(
+ LookupHInput({ nonce: 1, txid: "a", answer: INotFound }),
+ LookupHInput({ nonce: 1, txid: "zz", answer: IFound({ body: Some(pB), height: AtMined }) }),
+ TipHInput(0), TipHInput(4), TipHInput(5), TipHInput(6), TipHInput(9),
+ StaleHInput(4), StaleHInput(8), StaleHInput(9),
+ FlushDueHInput, FlushDoneHInput, DrainHInput, CrashHInput, RestartHInput,
+ ))
+ .union(tuples(Set(pA, pB, pJunk), Set(Accepted, AlreadyKnown, Rejected, Retryable))
+ .map(((payload, given)) => verdict(payload, given)))
+
+ // ------------------------------------------------------------------------
+ // Admission
+ // ------------------------------------------------------------------------
+
+ /// Under the startup budget, a conforming payload that arrives within
+ /// the delivery lag passes the expiry check. The lemma is about admission at
+ /// one tip. It does not say at what height the flush later happens.
+ run conformingTimelyPayloadIsAdmissibleTest = all {
+ assert(scheduleFitsBudget(PARAMS)),
+ assert(tuples(0.to(9), 0.to(PARAMS.deliveryLag), 0.to(2)).forall(((created, lag, extra)) =>
+ survivesNextFlush(
+ Some(created + PARAMS.minWalletExpiry + extra), created + lag,
+ PARAMS.flushInterval, PARAMS.miningMargin))),
+ // The budget is what makes it true: one block less and a payload built
+ // one block before a boundary, arriving on it, is refused.
+ assert(not(scheduleFitsBudget({ ...PARAMS, minWalletExpiry: 4 }))),
+ assert(not(survivesNextFlush(Some(2 + 4), 2 + 1, PARAMS.flushInterval, PARAMS.miningMargin))),
+ }
+
+ run nextFlushHeightTest = all {
+ assert(nextFlushHeight(0, 3) == 3),
+ assert(nextFlushHeight(2, 3) == 3),
+ // Strictly after: a tip on a boundary waits a whole interval.
+ assert(nextFlushHeight(3, 3) == 6),
+ assert(survivesNextFlush(None, 100, 3, 1)),
+ assert(survivesNextFlush(Some(7), 5, 3, 1)),
+ assert(not(survivesNextFlush(Some(6), 5, 3, 1))),
+ }
+
+ /// Each refusal, and the order the checks are made in.
+ run admissionDecisionTableTest = all {
+ // No tip yet, or a stale one: nothing else is looked at.
+ assert(PAYLOADS.forall(payload => admission(starting, payload) == Refused(TipStale))),
+ assert(PAYLOADS.forall(payload => admission(stale, payload) == Refused(TipStale))),
+ assert(PAYLOADS.forall(payload => admission(stale.after(DrainHInput), payload) == Refused(TipStale))),
+ // Draining comes before anything about the payload.
+ assert(PAYLOADS.forall(payload => admission(draining, payload) == Refused(HubDraining))),
+ // Expiry before the queue is looked at. At tip 5 the next flush is at 6.
+ assert(admission(running(5), pTight) == Refused(ExpiryTooTight)),
+ assert(admission(holding, pTight) == Refused(ExpiryTooTight)),
+ assert(admission(running(2), pTight) == Admitted),
+ // A duplicate is recognised; anything else that passes is admitted.
+ assert(admission(holding, pA) == Duplicate),
+ assert(admission(holding, pB) == Admitted),
+ assert(admission(running(5), pA) == Admitted),
+ // An unparseable payload has no expiry and is admitted like any other.
+ assert(admission(running(5), pJunk) == Admitted),
+ // Every refusal is produced, and a refusal changes nothing.
+ assert(REFUSALS.forall(refusal =>
+ tuples(STATES, PAYLOADS).exists(((state, payload)) =>
+ state.isServing() and outputOf(state, submit(payload)) == AckOutput({ nonce: 0, kind: Refused(refusal) })))),
+ assert(tuples(STATES, PAYLOADS).forall(((state, payload)) =>
+ match outputOf(state, submit(payload)) {
+ | AckOutput(ack) => ack.kind == Admitted or state.after(submit(payload)) == state
+ | _ => true
+ })),
+ }
+
+ // ------------------------------------------------------------------------
+ // Lookup
+ // ------------------------------------------------------------------------
+
+ run lookupTest = all {
+ // A queue hit, whatever the indexer would have said.
+ assert(outputOf(holding, LookupHInput({ nonce: 7, txid: "a", answer: IFound({ body: Some(pA), height: AtMined }) }))
+ == LookupReplyOutput({ nonce: 7, outcome: QueueHit })),
+ // A miss forwards the indexer's answer as it came.
+ assert(Set(INotFound, IUnavailable, IFound({ body: Some(pB), height: AtMined }), IFound({ body: None, height: AtZero }))
+ .forall(answer =>
+ outputOf(holding, LookupHInput({ nonce: 7, txid: "b", answer: answer }))
+ == LookupReplyOutput({ nonce: 7, outcome: FromIndexer(answer) }))),
+ // A queued payload that does not parse is never hit.
+ assert(holding.queued().contains(pJunk) and not(holding.isQueuedTxid("junk"))),
+ // Once the flush has taken the queue, the same lookup misses.
+ assert(outputOf(flushing, LookupHInput({ nonce: 7, txid: "a", answer: INotFound }))
+ == LookupReplyOutput({ nonce: 7, outcome: FromIndexer(INotFound) })),
+ assert(STATES.forall(state =>
+ after(state, LookupHInput({ nonce: 7, txid: "a", answer: INotFound })) == state)),
+ }
+
+ /// Bytes the shim rejects for their trailing junk and the hub's parser
+ /// accepts: the shim diverts them, and the hub queues them under the txid it
+ /// computes, so a lookup by that txid is a queue hit.
+ pure val pTrailing = { ...pJunk, id: "trailing", txid: Some("tt") }
+
+ run trailingBytesAreQueuedAndHitTest =
+ val queued = running(5).after(submit(pTrailing))
+ all {
+ assert(admission(running(5), pTrailing) == Admitted),
+ assert(queued.isQueuedTxid("tt")),
+ assert(outputOf(queued, LookupHInput({ nonce: 7, txid: "tt", answer: INotFound }))
+ == LookupReplyOutput({ nonce: 7, outcome: QueueHit })),
+ }
+
+ // ------------------------------------------------------------------------
+ // Tip
+ // ------------------------------------------------------------------------
+
+ /// The tip rule.
+ run tipRuleTest = all {
+ // The first observation is adopted with its epoch, and nothing is due.
+ assert(running(5).tip == Some(5) and running(5).phase == Running),
+ assert(running(5).lastEpoch == Some(1) and not(running(5).isFlushDue())),
+ // Forward: followed.
+ assert(running(5).after(TipHInput(6)).tip == Some(6)),
+ // Back within the allowance: followed.
+ assert(running(5).after(TipHInput(4)).tip == Some(4)),
+ // Back beyond it: ignored.
+ assert(running(5).after(TipHInput(3)) == running(5)),
+ assert(outputOf(running(5), TipHInput(3)) == NoHubOutput),
+ // A forward move ends staleness; a move back does not.
+ assert(stale.after(TipHInput(6)).phase == Running and stale.after(TipHInput(6)).cadence == Tracking),
+ assert(stale.after(TipHInput(4)).phase == Stale and stale.after(TipHInput(4)).cadence == FreeRunning(8)),
+ // Never during a flush, and never without a cadence loop.
+ assert(isError(outputOf(flushing, TipHInput(7)))),
+ assert(isError(outputOf(down, TipHInput(7)))),
+ assert(isError(outputOf(draining, TipHInput(7)))),
+ }
+
+ run staleCadenceTest = all {
+ assert(stale.phase == Stale and stale.cadence == FreeRunning(8)),
+ // The observed tip is untouched; only the schedule moves.
+ assert(stale.observedTip() == 5 and stale.cadenceHeight() == 8 and stale.cadenceEpoch() == 2),
+ assert(stale.isFlushDue()),
+ assert(stale.after(StaleHInput(9)).cadence == FreeRunning(9)),
+ assert(isError(outputOf(stale, StaleHInput(7)))),
+ assert(isError(outputOf(running(5), StaleHInput(4)))),
+ assert(isError(outputOf(starting, StaleHInput(4)))),
+ assert(isError(outputOf(flushing, StaleHInput(9)))),
+ }
+
+ // ------------------------------------------------------------------------
+ // Flush and requeue
+ // ------------------------------------------------------------------------
+
+ run flushCycleTest = all {
+ assert(not(holding.isFlushDue()) and isError(outputOf(holding, FlushDueHInput))),
+ assert(holding.after(TipHInput(6)).isFlushDue()),
+ // The whole queue moves out at once.
+ assert(outputOf(holding.after(TipHInput(6)), FlushDueHInput) == BroadcastOutput(Set(pA, pJunk))),
+ assert(flushing.queue == Map() and flushing.inFlight() == Set(pA, pJunk)),
+ // Published, already known and rejected entries leave.
+ assert(Set(Accepted, AlreadyKnown, Rejected).forall(given =>
+ flushing.after(verdict(pA, given)).inFlight() == Set(pJunk))),
+ // A retryable entry stays out until the flush ends.
+ assert(flushing.after(verdict(pA, Retryable)).inFlight() == Set(pA, pJunk)),
+ assert(isError(outputOf(flushing, verdict(pB, Accepted)))),
+ assert(isError(outputOf(flushing.after(verdict(pA, Accepted)), verdict(pA, Accepted)))),
+ assert(isError(outputOf(holding, verdict(pA, Accepted)))),
+ // The flush cannot end while a verdict is outstanding.
+ assert(isError(outputOf(flushing, FlushDoneHInput))),
+ assert(isError(outputOf(holding, FlushDoneHInput))),
+ // An empty queue is still a flush event: the epoch is recorded.
+ assert(running(5).after(TipHInput(6)).after(FlushDueHInput).lastEpoch == Some(2)),
+ assert(outputOf(running(5).after(TipHInput(6)), FlushDueHInput) == NoHubOutput),
+ }
+
+ /// A flush at tip 5 that left four entries unjudged, with three resident.
+ pure val pExpired = orchard("expired", Some(6))
+ pure val pResident = orchard("resident", Some(9))
+ pure val pWornOut = { ...pJunk, id: "worn-out" }
+ pure val pWornOutTight = { ...pExpired, id: "worn-out-tight" }
+ pure val returning: HubState = {
+ ...running(5),
+ queue: Map(pResident -> 0, pB -> 0, pC -> 0),
+ flush: Broadcasting({
+ batch: Map(),
+ unplaced: Map(pA -> 0, pExpired -> 0, pWornOut -> 2, pResident -> 1, pJunk -> 1, pWornOutTight -> 2),
+ final: false,
+ }),
+ }
+
+ /// Requeue, entry by entry, and the counts it reports.
+ run requeueTest = all {
+ assert(outputOf(returning, FlushDoneHInput)
+ == RequeuedOutput({ held: 2, droppedExpired: 2, droppedExhausted: 1 })),
+ // Held entries come back with one more attempt. The resident copy of the
+ // same bytes wins and keeps its own count.
+ assert(returning.after(FlushDoneHInput).queue
+ == Map(pResident -> 0, pB -> 0, pC -> 0, pA -> 1, pJunk -> 2)),
+ assert(returning.after(FlushDoneHInput).flush == Idle),
+ assert(returning.after(FlushDoneHInput).lastEpoch == Some(1)),
+ // Expiry is judged at the observed tip, not at the cadence height.
+ assert({ ...returning, phase: Stale, cadence: FreeRunning(11) }.after(FlushDoneHInput).queued().contains(pA)),
+ assert({ ...returning, phase: Stale, cadence: FreeRunning(11) }.after(FlushDoneHInput).lastEpoch == Some(3)),
+ assert(not({ ...returning, tip: Some(8) }.after(FlushDoneHInput).queued().contains(pA))),
+ }
+
+ run drainTest = all {
+ assert(draining.phase == Draining and draining.isFlushDue()),
+ assert(isError(outputOf(starting, DrainHInput))),
+ assert(isError(outputOf(draining, DrainHInput))),
+ assert(stale.after(DrainHInput).phase == Draining),
+ // The final flush publishes what is held; what it cannot place is lost.
+ assert(stopped.phase == Stopped and stopped.queue == Map()),
+ assert(draining.after(FlushDueHInput).after(verdict(pA, Retryable)).after(verdict(pJunk, Retryable))
+ .after(FlushDoneHInput).queue == Map()),
+ assert(outputOf(
+ draining.after(FlushDueHInput).after(verdict(pA, Retryable)).after(verdict(pJunk, Retryable)),
+ FlushDoneHInput) == RequeuedOutput({ held: 2, droppedExpired: 0, droppedExhausted: 0 })),
+ // With nothing held, the final flush stops the hub at once.
+ assert(running(5).after(DrainHInput).after(FlushDueHInput).phase == Stopped),
+ // A flush already in flight finishes first, and the final one follows.
+ assert(flushing.after(DrainHInput).after(verdict(pA, Accepted)).after(verdict(pJunk, Retryable))
+ .after(FlushDoneHInput).phase == Draining),
+ assert(flushing.after(DrainHInput).after(verdict(pA, Accepted)).after(verdict(pJunk, Retryable))
+ .after(FlushDoneHInput).isFlushDue()),
+ }
+
+ run crashAndRestartTest = all {
+ assert(STATES.exclude(Set(down)).forall(state => state.after(CrashHInput) == down)),
+ assert(isError(outputOf(down, CrashHInput))),
+ assert(down.after(RestartHInput) == starting),
+ assert(STATES.exclude(Set(down)).forall(state => isError(outputOf(state, RestartHInput)))),
+ // A hub that is not serving answers nothing.
+ assert(Set(down, stopped).forall(state =>
+ isError(outputOf(state, submit(pA)))
+ and isError(outputOf(state, LookupHInput({ nonce: 1, txid: "a", answer: INotFound }))))),
+ }
+
+ // ------------------------------------------------------------------------
+ // Totality and the Byzantine relation
+ // ------------------------------------------------------------------------
+
+ /// The function answers every input in every state, and an input that
+ /// is invalid in a state leaves that state unchanged.
+ run totalityTest =
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ val result = hub(state, input)
+ and {
+ result.state.params == state.params,
+ isError(result.out) implies result.state == state,
+ }))
+
+ /// The Byzantine relation contains the honest transition.
+ run byzantineContainsHonestTest =
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ byzHubResults(state, input, PAYLOADS).contains(hub(state, input))))
+
+ /// A Byzantine hub can hold a payload admission would refuse, and can
+ /// answer a lookup with a queued body.
+ run byzantineHubTest = all {
+ assert(byzHubResults(running(5), submit(pTight), PAYLOADS).exists(result =>
+ result.state.queued().contains(pTight))),
+ assert(byzHubResults(holding, LookupHInput({ nonce: 1, txid: "a", answer: INotFound }), PAYLOADS)
+ .contains(holding.toLookupReplyOutput(1, FromIndexer(IFound({ body: Some(pA), height: AtZero }))))),
+ // It still cannot act while it is not running.
+ assert(byzHubResults(down, submit(pA), PAYLOADS) == Set(hub(down, submit(pA)))),
+ }
+
+ // ------------------------------------------------------------------------
+ // Every reachable state
+ // ------------------------------------------------------------------------
+ //
+ // `REACH` is every hub state reachable from a starting hub under
+ // `REACH_INPUTS`, honest or through the Byzantine submit relation. The
+ // properties below are exhaustive over it, for these parameters: two
+ // payloads, one with no txid and no expiry; tips 0, 4, 5, 6 and 9; free-run
+ // estimates 4, 8 and 9; every verdict on either payload.
+
+ pure val REACH_PAYLOADS = Set(pA, pJunk)
+ pure val REACH_INPUTS: Set[HubInput] =
+ REACH_PAYLOADS.map(payload => submit(payload))
+ .union(Set(
+ TipHInput(0), TipHInput(4), TipHInput(5), TipHInput(6), TipHInput(9),
+ StaleHInput(4), StaleHInput(8), StaleHInput(9),
+ FlushDueHInput, FlushDoneHInput, DrainHInput, CrashHInput, RestartHInput,
+ ))
+ .union(tuples(REACH_PAYLOADS, Set(Accepted, AlreadyKnown, Rejected, Retryable))
+ .map(((payload, given)) => verdict(payload, given)))
+
+ /// The states a Byzantine hub may move to on a submission.
+ pure def byzantineSteps(state: HubState): Set[HubState] =
+ REACH_PAYLOADS.map(payload => byzHubResults(state, submit(payload), REACH_PAYLOADS)
+ .map(result => result.state)).flatten()
+
+ pure def successors(state: HubState): Set[HubState] =
+ REACH_INPUTS.map(input => hub(state, input).state).union(byzantineSteps(state))
+
+ /// The closure, breadth first. The bound on rounds is a budget, not a
+ /// depth bound: `reachTest` fails unless the result is closed.
+ pure val REACH: Set[HubState] =
+ 1.to(60).fold({ reached: Set(starting), frontier: Set(starting) }, (acc, _) =>
+ val fresh = acc.frontier.map(state => successors(state)).flatten().exclude(acc.reached)
+ { reached: acc.reached.union(fresh), frontier: fresh }).reached
+
+ /// `REACH` is a fixpoint: no input, honest or Byzantine, leaves it.
+ run reachTest = assert(REACH.forall(state => successors(state).subseteq(REACH)))
+
+ /// A2. An entry leaves the queue only into a flush, or because the hub went
+ /// down or exited after its final flush. Nothing evicts it, whatever the
+ /// hub's role: the Byzantine submit relation only ever adds to the queue.
+ /// The exit matters only to a Byzantine hub, which can admit while
+ /// draining; an honest one has nothing queued by then.
+ run neverEvictTest =
+ assert(REACH.forall(state =>
+ successors(state).forall(stepped =>
+ stepped.phase == Down or stepped.phase == Stopped
+ or state.queued().subseteq(stepped.queued().union(stepped.inFlight())))))
+
+ /// A3. A draining honest hub admits nothing: its queue gains only what a
+ /// flush hands back. A Byzantine hub is not bound by it
+ /// (`hubAdmitsWhileDrainingTest`).
+ run drainIsFinalTest =
+ assert(REACH.forall(state =>
+ state.phase == Draining implies REACH_INPUTS.forall(input =>
+ hub(state, input).state.queued().subseteq(state.queued().union(state.inFlight())))))
+
+ /// G7's hub half: a queued entry is within its attempts, and a hub that is
+ /// down holds nothing and knows nothing.
+ run wellFormedTest =
+ assert(REACH.forall(state => and {
+ state.queued().forall(payload => state.queue.get(payload) >= 0 and state.queue.get(payload) <= PARAMS.maxAttempts),
+ state.phase == Down implies state == down,
+ }))
+
+ // ------------------------------------------------------------------------
+ // The abstraction lemma
+ // ------------------------------------------------------------------------
+
+ pure def project(state: HubState): AHub =
+ { queue: state.queued(), held: state.inFlight() }
+
+ pure def requestOf(input: HubInput): Option[ARequest] =
+ match input {
+ | SubmitHInput(submitted) => Some(ASubmit(submitted.payload))
+ | LookupHInput(lookup) => Some(ALookup({ txid: lookup.txid, answer: lookup.answer }))
+ | _ => None
+ }
+
+ pure def replyOf(output: HubOutput): Option[AReply] =
+ match output {
+ | AckOutput(ack) => Some(AAck(renderAck(ack.kind)))
+ | LookupReplyOutput(reply) => Some(AWire(render(reply.outcome)))
+ | _ => None
+ }
+
+ pure val LOOKUPS: Set[HubInput] =
+ Set(INotFound, IUnavailable, IFound({ body: Some(pA), height: AtMined }))
+ .map(answer => LookupHInput({ nonce: 1, txid: "a", answer: answer }))
+ .union(Set(LookupHInput({ nonce: 1, txid: "zz", answer: IFound({ body: Some(pB), height: AtMined }) })))
+
+ /// An error changes nothing. A request is one of `answers`; anything else
+ /// is an internal move with no reply.
+ pure def isAbstracted(state: HubState, input: HubInput, result: HubResult, answers: (AHub, ARequest) => Set[AAnswer]): bool =
+ val before = state.project()
+ val after = result.state.project()
+ if (result.out.isError()) result.state == state
+ else match input.requestOf() {
+ | Some(request) =>
+ match result.out.replyOf() {
+ | Some(reply) => answers(before, request).contains({ hub: after, reply: reply })
+ | None => false
+ }
+ | None => result.out.replyOf() == None and isInternal(before, after)
+ }
+
+ /// Every step of the real hub from a reachable state is a step of the
+ /// abstract one, honest against honest and Byzantine against Byzantine.
+ run abstractionTest =
+ assert(REACH.forall(state =>
+ REACH_INPUTS.union(LOOKUPS).forall(input =>
+ isAbstracted(state, input, hub(state, input), honestAnswers))))
+
+ run byzantineAbstractionTest =
+ assert(REACH.forall(state =>
+ REACH_PAYLOADS.map(payload => submit(payload)).union(LOOKUPS).forall(input =>
+ byzHubResults(state, input, PAYLOADS).forall(result =>
+ isAbstracted(state, input, result, (h, request) => byzantineAnswers(h, request, PAYLOADS))))))
+
+ /// Each abstract move has a concrete step that projects onto it.
+ pure def realises(state: HubState, input: HubInput, move: AHub, reply: Option[AReply]): bool =
+ val result = hub(state, input)
+ and { not(result.out.isError()), result.state.project() == move, result.out.replyOf() == reply }
+
+ run realisesTest = all {
+ // accept, refuse
+ assert(realises(running(5), submit(pA), { queue: Set(pA), held: Set() }, Some(AAck(WAccepted)))),
+ assert(realises(draining, submit(pB), draining.project(), Some(AAck(WRefused(WQueueFull))))),
+ // take, settle, a retryable verdict that moves nothing
+ assert(realises(holding.after(TipHInput(6)), FlushDueHInput, holding.project().take(), None)),
+ assert(realises(flushing, verdict(pA, Accepted), flushing.project().settle(pA), None)),
+ assert(realises(flushing, verdict(pA, Retryable), flushing.project(), None)),
+ // give back what is kept: `pJunk` is held, `pA` was settled
+ val ending = flushing.after(verdict(pA, Accepted)).after(verdict(pJunk, Retryable))
+ assert(realises(ending, FlushDoneHInput, ending.project().giveBack(Set(pJunk)), None)),
+ // lose
+ assert(realises(holding, CrashHInput, emptyAHub, None)),
+ }
+}
diff --git a/zeronym/spec/quint/tests/indexerTest.qnt b/zeronym/spec/quint/tests/indexerTest.qnt
new file mode 100644
index 00000000..292061a0
--- /dev/null
+++ b/zeronym/spec/quint/tests/indexerTest.qnt
@@ -0,0 +1,151 @@
+// -*- mode: Bluespec; -*-
+
+/// The indexer relations, checked over a small universe.
+module indexerTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import indexer.* from "../indexer"
+
+ pure def orchard(id: str, txid: TxId, expiry: Option[Height]): Payload =
+ { id: id, txid: Some(txid), created: 1, expiry: expiry, class: OrchardTouching, oversize: false }
+
+ pure val pA = orchard("a", "ta", Some(9))
+ pure val pATwin = orchard("a-twin", "ta", Some(9))
+ pure val pB = orchard("b", "tb", None)
+ pure val pOld = orchard("old", "told", Some(4))
+ pure val pJunk = { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, oversize: false }
+
+ pure val UNIVERSE = Set(pA, pATwin, pB, pOld, pJunk)
+
+ pure def verdictOn(given: Verdict): IndexerOutput = VerdictOutput(given)
+
+ pure val empty = initialIndexer(4)
+ /// `pA` accepted at height 4.
+ pure val withA = indexerApply(empty, BroadcastIInput(pA), verdictOn(Accepted))
+ /// `pA` mined at height 5.
+ pure val minedA = indexerApply(indexerApply(withA, AdvanceIInput, NoIndexerOutput), MineIInput("ta"), NoIndexerOutput)
+ /// `pB` offered and not taken.
+ pure val offeredB = indexerApply(empty, BroadcastIInput(pB), verdictOn(Retryable))
+
+ pure val STATES = Set(empty, withA, minedA, offeredB)
+ pure val INPUTS: Set[IndexerInput] =
+ UNIVERSE.map(payload => BroadcastIInput(payload))
+ .union(Set(LookupIInput("ta"), LookupIInput("tb"), AdvanceIInput, MineIInput("ta"), MineIInput("tb")))
+
+ run broadcastVerdictsTest = all {
+ // A valid, unexpired, unknown transaction may be accepted.
+ assert(honestIndexerOutputs(empty, BroadcastIInput(pA))
+ == Set(Accepted, Rejected, Retryable).map(verdictOn)),
+ // One that can no longer be mined may not.
+ assert(honestIndexerOutputs(empty, BroadcastIInput(pOld))
+ == Set(Rejected, Retryable).map(verdictOn)),
+ // Nor one that does not parse.
+ assert(honestIndexerOutputs(empty, BroadcastIInput(pJunk))
+ == Set(Rejected, Retryable).map(verdictOn)),
+ // The chain has it: already known, under these bytes or a twin's.
+ assert(honestIndexerOutputs(withA, BroadcastIInput(pA))
+ == Set(AlreadyKnown, Rejected, Retryable).map(verdictOn)),
+ assert(honestIndexerOutputs(withA, BroadcastIInput(pATwin))
+ == Set(AlreadyKnown, Rejected, Retryable).map(verdictOn)),
+ }
+
+ run broadcastEffectTest = all {
+ assert(withA.inclusion("ta") == InMempool and withA.published() == Set(pA)),
+ assert(withA.offered == Set(pA)),
+ // Offered is remembered whatever the verdict; the chain is untouched.
+ assert(offeredB.offered == Set(pB) and offeredB.txs == Map()),
+ assert(Set(AlreadyKnown, Rejected, Retryable).forall(given =>
+ indexerApply(empty, BroadcastIInput(pA), verdictOn(given)).txs == Map())),
+ // The chain keeps the bytes it accepted first.
+ assert(indexerApply(withA, BroadcastIInput(pATwin), verdictOn(AlreadyKnown)).published() == Set(pA)),
+ }
+
+ run lookupTest = all {
+ assert(honestIndexerOutputs(empty, LookupIInput("ta"))
+ == Set(AnswerOutput(INotFound), AnswerOutput(IUnavailable))),
+ // A mempool transaction is found at height 0, with its bytes.
+ assert(honestIndexerOutputs(withA, LookupIInput("ta"))
+ == Set(AnswerOutput(IFound({ body: Some(pA), height: AtZero })), AnswerOutput(IUnavailable))),
+ assert(honestIndexerOutputs(minedA, LookupIInput("ta"))
+ == Set(AnswerOutput(IFound({ body: Some(pA), height: AtMined })), AnswerOutput(IUnavailable))),
+ assert(chainAnswer(empty, "ta") == INotFound),
+ assert(chainAnswer(minedA, "ta") == IFound({ body: Some(pA), height: AtMined })),
+ // A lookup changes nothing.
+ assert(STATES.forall(state =>
+ honestIndexerResults(state, LookupIInput("ta")).forall(result => result.state == state))),
+ // An honest indexer never reports a transaction without its bytes.
+ assert(tuples(STATES, Set("ta", "tb")).forall(((state, txid)) =>
+ honestIndexerOutputs(state, LookupIInput(txid)).forall(output =>
+ match output {
+ | AnswerOutput(answer) =>
+ match answer {
+ | IFound(found) => isSome(found.body)
+ | _ => true
+ }
+ | _ => true
+ }))),
+ }
+
+ run chainTest = all {
+ assert(indexerApply(empty, AdvanceIInput, NoIndexerOutput).height == 5),
+ assert(minedA.inclusion("ta") == Mined),
+ // Only a mempool transaction can be mined: not an absent one, not twice.
+ assert(honestIndexerOutputs(withA, MineIInput("ta")) == Set(NoIndexerOutput)),
+ assert(honestIndexerOutputs(empty, MineIInput("ta")) == Set()),
+ assert(honestIndexerOutputs(minedA, MineIInput("ta")) == Set()),
+ assert(indexerApply(minedA, MineIInput("ta"), NoIndexerOutput) == minedA),
+ }
+
+ run tipReportsTest = all {
+ assert(honestTips(empty, 0, 0.to(7)) == Set(4)),
+ assert(honestTips(empty, 1, 0.to(7)) == Set(3, 4)),
+ assert(honestTips(initialIndexer(1), 3, 0.to(7)) == Set(0, 1)),
+ }
+
+ /// The Byzantine relation contains every honest transition, and every
+ /// honest tip report is one a Byzantine indexer could make.
+ run byzantineContainsHonestTest = all {
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ honestIndexerResults(state, input).subseteq(byzIndexerResults(state, input, UNIVERSE)))),
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ honestIndexerOutputs(state, input).subseteq(byzIndexerOutputs(state, input, UNIVERSE)))),
+ assert(tuples(STATES, 0.to(3)).forall(((state, slack)) =>
+ honestTips(state, slack, 0.to(7)).subseteq(byzTips(0.to(7))))),
+ }
+
+ /// The protocol's relation, which has no chain height, contains the honest
+ /// relation, and is wider by the expiry clause only: it may accept an
+ /// expired transaction.
+ run heightlessCoversTest = all {
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ honestIndexerResults(state, input).subseteq(heightlessIndexerResults(state, input)))),
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ heightlessIndexerResults(state, input).exclude(honestIndexerResults(state, input)).forall(result =>
+ input == BroadcastIInput(pOld) and result.out == VerdictOutput(Accepted)))),
+ assert(heightlessIndexerResults(empty, BroadcastIInput(pOld)).exists(result => result.out == VerdictOutput(Accepted))),
+ }
+
+ run byzantineIndexerTest = all {
+ // It may serve what it was offered and the chain has not published.
+ assert(offeredB.servable(UNIVERSE) == Set(pB)),
+ assert(byzIndexerOutputs(offeredB, LookupIInput("tb"), UNIVERSE)
+ .contains(AnswerOutput(IFound({ body: Some(pB), height: AtOther })))),
+ // A twin of what it knows, too. Nothing else.
+ assert(withA.servable(UNIVERSE) == Set(pA, pATwin)),
+ assert(empty.servable(UNIVERSE) == Set()),
+ // "Found, height 0, no body" for a transaction that does not exist.
+ assert(byzIndexerOutputs(empty, LookupIInput("ta"), UNIVERSE)
+ .contains(AnswerOutput(IFound({ body: None, height: AtZero })))),
+ // The verdict and the effect are independent.
+ assert(byzIndexerResults(empty, BroadcastIInput(pA), UNIVERSE)
+ .contains({ state: offeredB.with("offered", Set(pA)), out: verdictOn(Accepted) })),
+ assert(byzIndexerResults(empty, BroadcastIInput(pA), UNIVERSE)
+ .contains({ state: withA, out: verdictOn(Rejected) })),
+ // It cannot put an expired transaction on the chain.
+ assert(byzIndexerResults(empty, BroadcastIInput(pOld), UNIVERSE)
+ .forall(result => result.state.txs == Map())),
+ // The chain's own steps are not the indexer's to change.
+ assert(byzIndexerResults(withA, AdvanceIInput, UNIVERSE) == honestIndexerResults(withA, AdvanceIInput)),
+ assert(byzIndexerResults(withA, MineIInput("ta"), UNIVERSE) == honestIndexerResults(withA, MineIInput("ta"))),
+ }
+}
diff --git a/zeronym/spec/quint/tests/scenariosTest.qnt b/zeronym/spec/quint/tests/scenariosTest.qnt
new file mode 100644
index 00000000..c59a4c5a
--- /dev/null
+++ b/zeronym/spec/quint/tests/scenariosTest.qnt
@@ -0,0 +1,235 @@
+// -*- mode: Bluespec; -*-
+
+/// Scripted runs against the honest configurations, and the two witnesses that
+/// need a Byzantine component: one run for each behaviour that must be
+/// reachable, and one for each cause of each known gap.
+///
+/// A run is a sequence of the machine's own steps. Where a run says a property
+/// fails, it also says what is in the wallet's log, the soup or the audit
+/// record that makes it fail.
+///
+/// Shim nonces count up from 0, one per frame.
+
+module scenariosTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import wire.* from "../wire"
+ import indexer.* from "../indexer"
+ import abstractHub.* from "../abstractHub"
+ import shim.* from "../shim"
+ import protocol.* from "../protocol"
+
+ /// Every named init is live: its guard holds and it starts a run.
+ run liveInitsTest =
+ initBaseline
+ .then(initByzHub)
+ .then(initByzIndexer)
+
+ // ------------------------------------------------------------------------
+ // Every component honest (`baseline`)
+ // ------------------------------------------------------------------------
+
+ // ------------------------------------------------------------------------
+ // Witnesses
+ // ------------------------------------------------------------------------
+
+ /// A migration from send to mined, with the wallet polling.
+ run pendingThenMempoolThenMinedTest =
+ initBaseline
+ // The shim diverts and answers at once; the operator sees nothing.
+ .then(submitTo(0, early))
+ .expect(lastEvent == Sent({ input: Clean(early), obs: SentOk }))
+ .expect(s.hub.queue == Set(early) and s.operator == Set())
+ .then(lookUp(1, "early"))
+ .expect(lastEvent == Got({ query: "early", obs: Pending, via: Some(1) }))
+ .then(flush([early], Accepted))
+ .expect(s.hub.queue == Set() and s.onChain("early") == InMempool)
+ .then(lookUp(2, "early"))
+ .expect(lastEvent == Got({ query: "early", obs: Tx({ payload: early, height: AtZero }), via: Some(2) }))
+ .then(chainMineWith("early"))
+ .then(lookUp(3, "early"))
+ .expect(lastEvent == Got({ query: "early", obs: Tx({ payload: early, height: AtMined }), via: Some(3) }))
+ .expect(wPending and wTxInMempool and wTxMined)
+ .expect(operatorBlind and queuedBytesConfidential and txidAuthenticity and lookupValidityPerHub)
+ .expect(statusNeverRegresses)
+
+ /// A pass-through transaction goes to the operator and nowhere else.
+ run passThroughIsForwardedTest =
+ initBaseline
+ .then(sendToHub(plain))
+ .expect(lastEvent == Sent({ input: Clean(plain), obs: SentToOperator }))
+ .expect(s.operator == Set(plain) and s.net == Set())
+ .expect(vOperatorBlind and operatorBlind and vQueuedBytesConfidential and queuedBytesConfidential)
+
+ /// The accepted disclosure: a third party that knows a txid is told it
+ /// is queued, and is not given the bytes.
+ run thirdPartyLearnsItIsQueuedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(thirdPartyLearnsTxidWith("early"))
+ .then(thirdPartyLookupWith("early"))
+ .then(deliverLookupFrom(ThirdPartyAddr, 0, "early", INotFound))
+ .expect(s.replies(ThirdPartyAddr) == Set({ nonce: 0, reply: WFound({ body: None, height: AtZero }) }))
+ .expect(wQueuedDisclosed)
+ .expect(s.tpLearned() == Set() and queuedBytesConfidential)
+
+ /// Once `early` is published its txid is public, and a third party
+ /// that asks is served its bytes from the indexer. G2 holds: they are
+ /// public.
+ run thirdPartyIsServedPublishedBodyTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(thirdPartyLookupWith("early"))
+ .then(deliverLookupFrom(ThirdPartyAddr, 0, "early", chainAnswer(s.indexer, "early")))
+ .expect(s.replies(ThirdPartyAddr) == Set({ nonce: 0, reply: WFound({ body: Some(early), height: AtZero }) }))
+ .expect(s.repliedBodies(ThirdPartyAddr) == Set(early) and s.operator == Set())
+ .expect(wThirdPartyServedBody and vQueuedBytesConfidential and queuedBytesConfidential)
+
+ /// A lookup that gets no reply in time fails closed, and G4 holds of it.
+ run lookupTimesOutTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(ask("early"))
+ .then(timeOutLookup(1))
+ .expect(lastEvent == Got({ query: "early", obs: Unavailable, via: None }))
+ .expect(s.shim.waiters == Map() and lookupValidityPerHub)
+
+ /// A queued payload the hub cannot parse has no txid to be found by.
+ run unparseableIsQueuedAndMissedTest =
+ initBaseline
+ .then(submitTo(0, junk))
+ .expect(lastEvent == Sent({ input: Clean(junk), obs: SentOk }) and s.hub.queue == Set(junk))
+ .then(lookUp(1, "junk"))
+ .expect(lastEvent == Got({ query: "junk", obs: NotFound, via: Some(1) }))
+ .expect(wUnparseableMissed and lookupValidityPerHub)
+
+ // ------------------------------------------------------------------------
+ // K1. Told ok, and no hub ever has it
+ // ------------------------------------------------------------------------
+
+ /// K1a. The hub refuses the frame after the wallet was told ok.
+ run toldOkThenRefusedTest =
+ initBaseline
+ .then(sendToHub(tight))
+ .then(answerSubmitFrom(ShimAddr, 0, tight, WRefused(WExpiryTooTight)))
+ .expect(s.wallet.log == [Sent({ input: Clean(tight), obs: SentOk })])
+ .expect(s.acks(ShimAddr) == Set({ nonce: 0, ack: WRefused(WExpiryTooTight) }))
+ .expect(s.hub == emptyAHub)
+
+ /// K1b. The frame is never delivered. Nothing obliges the network to.
+ run toldOkAndNeverDeliveredTest =
+ initBaseline
+ .then(sendToHub(early))
+ .expect(s.wallet.log == [Sent({ input: Clean(early), obs: SentOk })])
+ .expect(s.net == Set(submitMail(0, early)))
+ .expect(s.hub == emptyAHub)
+
+ // ------------------------------------------------------------------------
+ // K2. The status a wallet sees goes backwards
+ // ------------------------------------------------------------------------
+
+ /// K2a. Two polls, answered in order, delivered out of order.
+ run repliesReorderedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(ask("early"))
+ .then(deliverLookup(1, "early"))
+ .then(flush([early], Accepted))
+ .then(ask("early"))
+ .then(deliverLookup(2, "early"))
+ .then(deliverToShim(replyMail(2, WFound({ body: Some(early), height: AtZero }))))
+ .then(deliverToShim(replyMail(1, WFound({ body: None, height: AtZero }))))
+ .expect(s.wallet.log == [
+ Sent({ input: Clean(early), obs: SentOk }),
+ Got({ query: "early", obs: Tx({ payload: early, height: AtZero }), via: Some(2) }),
+ Got({ query: "early", obs: Pending, via: Some(1) }),
+ ])
+ // Each answer was true when it was given.
+ .expect(not(statusNeverRegresses) and lookupValidityPerHub)
+
+ /// K2b. The wallet sends published bytes again. The hub's memory of them
+ /// went with the flush, so they are admitted and pending once more.
+ run walletResendsPublishedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(lookUp(1, "early"))
+ .then(submitTo(2, early))
+ .expect(s.hub.queue == Set(early) and s.onChain("early") == InMempool)
+ .then(lookUp(3, "early"))
+ .expect(s.wallet.log.slice(1, 4) == [
+ Got({ query: "early", obs: Tx({ payload: early, height: AtZero }), via: Some(1) }),
+ Sent({ input: Clean(early), obs: SentOk }),
+ Got({ query: "early", obs: Pending, via: Some(3) }),
+ ])
+ .expect(not(statusNeverRegresses) and lookupValidityPerHub)
+
+ /// K2c. The same, done by a third party: the bytes are public once
+ /// published, and submission is open to anyone.
+ run thirdPartyResubmitsPublishedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(lookUp(1, "early"))
+ .expect(s.tpPayloads().contains(early))
+ .then(thirdPartySubmitWith(early))
+ .then(deliverSubmitFrom(ThirdPartyAddr, 0, early))
+ .then(lookUp(2, "early"))
+ .expect(s.wallet.log.slice(1, 3) == [
+ Got({ query: "early", obs: Tx({ payload: early, height: AtZero }), via: Some(1) }),
+ Got({ query: "early", obs: Pending, via: Some(2) }),
+ ])
+ .expect(not(statusNeverRegresses) and lookupValidityPerHub)
+
+ /// K2d. The flush window: the queue is empty and the chain does not have
+ /// the batch yet.
+ run flushWindowTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(lookUp(1, "early"))
+ .then(hubTake)
+ .expect(s.hub.held == Set(early) and s.onChain("early") == Absent)
+ .then(lookUp(2, "early"))
+ .expect(s.wallet.log.slice(1, 3) == [
+ Got({ query: "early", obs: Pending, via: Some(1) }),
+ Got({ query: "early", obs: NotFound, via: Some(2) }),
+ ])
+ .expect(not(statusNeverRegresses) and lookupValidityPerHub)
+
+ /// K2e. The node rejects the transaction at flush. It was pending; now it
+ /// is nowhere.
+ run rejectedAtFlushTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(lookUp(1, "early"))
+ .then(flush([early], Rejected))
+ .expect(s.hub.queue == Set() and s.hub.held == Set() and s.onChain("early") == Absent)
+ .then(lookUp(2, "early"))
+ .expect(s.wallet.log.slice(1, 3) == [
+ Got({ query: "early", obs: Pending, via: Some(1) }),
+ Got({ query: "early", obs: NotFound, via: Some(2) }),
+ ])
+ .expect(not(statusNeverRegresses) and lookupValidityPerHub)
+
+ // ------------------------------------------------------------------------
+ // A Byzantine hub (`byzHub`)
+ // ------------------------------------------------------------------------
+
+ /// A Byzantine hub serves a twin of the wallet's transaction at a
+ /// height the chain has not reached. The shim checks the txid, which a twin
+ /// shares, and nothing else: it serves both.
+ run twinAtFalseHeightIsServedTest =
+ initByzHub
+ .then(submitTo(0, early))
+ .then(ask("early"))
+ .then(hubReceiveWith(
+ lookupMail(1, "early"), INotFound,
+ { hub: s.hub, reply: AWire(render(FromIndexer(IFound({ body: Some(earlyTwin), height: AtOther })))) },
+ ))
+ .then(deliverToShim(replyMail(1, WFound({ body: Some(earlyTwin), height: AtOther }))))
+ .expect(lastEvent == Got({ query: "early", obs: Tx({ payload: earlyTwin, height: AtOther }), via: Some(1) }))
+ .expect(s.onChain("early") == Absent)
+ .expect(wTwinServed and wFalseHeightServed)
+ .expect(txidAuthenticity and not(lookupValidityPerHub))
+}
diff --git a/zeronym/spec/quint/tests/shimTest.qnt b/zeronym/spec/quint/tests/shimTest.qnt
new file mode 100644
index 00000000..03de158a
--- /dev/null
+++ b/zeronym/spec/quint/tests/shimTest.qnt
@@ -0,0 +1,166 @@
+// -*- mode: Bluespec; -*-
+
+/// The shim function.
+module shimTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import wire.* from "../wire"
+ import shim.* from "../shim"
+
+ pure def payload(id: str, class: Class): Payload =
+ { id: id, txid: Some(id), created: 1, expiry: Some(9), class: class, oversize: false }
+
+ pure val pOrchard = payload("orchard", OrchardTouching)
+ pure val pPlain = payload("plain", PassThrough)
+ pure val pJunk = { ...payload("junk", Unparseable), txid: None, expiry: None }
+ /// Trailing bytes: the shim's parser gives up, the hub's computes a txid.
+ pure val pTrailing = { ...payload("trailing", Unparseable), expiry: None }
+ pure val pBig = { ...payload("big", OrchardTouching), oversize: true }
+ pure val pBigPlain = { ...payload("big-plain", PassThrough), oversize: true }
+
+ pure val PAYLOADS = Set(pOrchard, pPlain, pJunk, pBig, pBigPlain)
+ pure val SEND_INPUTS = PAYLOADS.map(p => Clean(p)).union(Set(Unreadable, EmptyBody))
+
+ pure def after(state: ShimState, input: ShimInput): ShimState = shim(state, input).state
+ pure def outputOf(state: ShimState, input: ShimInput): ShimOutput = shim(state, input).out
+
+ pure def isError(output: ShimOutput): bool =
+ match output {
+ | ShimErrorOutput(_) => true
+ | _ => false
+ }
+
+ pure def send(input: SendInput, handedOver: bool): ShimInput =
+ SendTxSInput({ input: input, handedOver: handedOver })
+
+ pure def ack(nonce: Nonce, given: WireAck): ShimInput =
+ FrameSInput(Ack({ nonce: nonce, ack: given }))
+
+ pure def reply(nonce: Nonce, given: WireReply): ShimInput =
+ FrameSInput(LookupReply({ nonce: nonce, reply: given }))
+
+ /// Nonce 0 went out with a submission; nonce 1 is a lookup.
+ pure val busy = initialShim.after(send(Clean(pOrchard), true)).after(GetTxSInput("orchard"))
+
+ pure val STATES = Set(initialShim, busy, initialShim.after(GetTxSInput("orchard")))
+
+ pure val INPUTS: Set[ShimInput] =
+ tuples(SEND_INPUTS, Set(true, false)).map(((input, handedOver)) => send(input, handedOver))
+ .union(Set("orchard", "zz").map(query => GetTxSInput(query)))
+ .union(0.to(2).map(nonce => ack(nonce, WAccepted)))
+ .union(0.to(2).map(nonce => ack(nonce, WRefused(WQueueFull))))
+ .union(0.to(2).map(nonce => reply(nonce, WNotFound)))
+ .union(0.to(2).map(nonce => reply(nonce, WFound({ body: Some(pOrchard), height: AtMined }))))
+ .union(0.to(2).map(nonce => LookupTimeoutSInput(nonce)))
+ .union(Set(
+ FrameSInput(Submit({ nonce: 0, payload: pOrchard })),
+ FrameSInput(Lookup({ nonce: 0, txid: "orchard" })),
+ ))
+
+ // ------------------------------------------------------------------------
+ // SendTransaction
+ // ------------------------------------------------------------------------
+
+ /// Only a cleanly read pass-through transaction is forwarded. Every
+ /// other input is diverted or fails closed, in every state.
+ run onlyPassThroughIsForwardedTest = all {
+ assert(tuples(STATES, SEND_INPUTS, Set(true, false)).forall(((state, input, handedOver)) =>
+ match outputOf(state, send(input, handedOver)) {
+ | ForwardOutput(forwarded) => input == Clean(forwarded) and forwarded.class == PassThrough
+ | _ => true
+ })),
+ assert(outputOf(initialShim, send(Clean(pPlain), true)) == ForwardOutput(pPlain)),
+ // Forwarding does not depend on the hub, or on the hub frame's size.
+ assert(outputOf(initialShim, send(Clean(pPlain), false)) == ForwardOutput(pPlain)),
+ assert(outputOf(initialShim, send(Clean(pBigPlain), true)) == ForwardOutput(pBigPlain)),
+ assert(initialShim.after(send(Clean(pPlain), true)) == initialShim),
+ // A body the shim cannot parse is diverted, never forwarded.
+ assert(outputOf(initialShim, send(Clean(pJunk), true))
+ == DivertedOutput({ payload: pJunk, frame: Submit({ nonce: 0, payload: pJunk }), told: SentOk })),
+ // So is one the hub's parser accepts: the shim's classification alone
+ // decides.
+ assert(outputOf(initialShim, send(Clean(pTrailing), true))
+ == DivertedOutput({ payload: pTrailing, frame: Submit({ nonce: 0, payload: pTrailing }), told: SentOk })),
+ }
+
+ run failClosedTest = all {
+ assert(outputOf(initialShim, send(Unreadable, true)) == SendDoneOutput({ input: Unreadable, obs: SendUnavailable })),
+ assert(outputOf(initialShim, send(EmptyBody, true)) == SendDoneOutput({ input: EmptyBody, obs: SendInvalid })),
+ assert(outputOf(initialShim, send(Clean(pBig), true)) == SendDoneOutput({ input: Clean(pBig), obs: SendTooLarge })),
+ // The frame not handed over: the hub is unreachable.
+ assert(outputOf(initialShim, send(Clean(pOrchard), false))
+ == SendDoneOutput({ input: Clean(pOrchard), obs: SendUnavailable })),
+ // None of these leaves anything behind.
+ assert(Set(send(Unreadable, true), send(EmptyBody, true), send(Clean(pBig), true), send(Clean(pOrchard), false))
+ .forall(input => initialShim.after(input) == initialShim)),
+ }
+
+ run dispatchOnlyTest = all {
+ // One frame, under a fresh nonce, and the wallet is told ok at once.
+ assert(outputOf(initialShim, send(Clean(pOrchard), true))
+ == DivertedOutput({ payload: pOrchard, frame: Submit({ nonce: 0, payload: pOrchard }), told: SentOk })),
+ assert(initialShim.after(send(Clean(pOrchard), true)).nextNonce == 1),
+ // A submission leaves nothing to wait on, and an ack tells nobody.
+ assert(initialShim.after(send(Clean(pOrchard), true)).waiters == Map()),
+ assert(outputOf(busy, ack(0, WRefused(WQueueFull))) == NoShimOutput),
+ assert(busy.after(ack(0, WRefused(WQueueFull))) == busy),
+ }
+
+ // ------------------------------------------------------------------------
+ // GetTransaction
+ // ------------------------------------------------------------------------
+
+ run lookupTest = all {
+ // The lookup goes to the hub under a fresh nonce.
+ assert(outputOf(initialShim, GetTxSInput("orchard")) == LookupSentOutput(Lookup({ nonce: 0, txid: "orchard" }))),
+ assert(busy.waiters == Map(1 -> "orchard")),
+ // Each reply arm.
+ assert(outputOf(busy, reply(1, WFound({ body: None, height: AtZero })))
+ == LookupDoneOutput({ query: "orchard", result: Pending })),
+ assert(outputOf(busy, reply(1, WFound({ body: Some(pOrchard), height: AtMined })))
+ == LookupDoneOutput({ query: "orchard", result: Tx({ payload: pOrchard, height: AtMined }) })),
+ assert(outputOf(busy, reply(1, WFound({ body: Some(pPlain), height: AtMined })))
+ == LookupDoneOutput({ query: "orchard", result: NotFound })),
+ assert(outputOf(busy, reply(1, WNotFound)) == LookupDoneOutput({ query: "orchard", result: NotFound })),
+ assert(outputOf(busy, reply(1, WError)) == LookupDoneOutput({ query: "orchard", result: Unavailable })),
+ // Any reply is final: the waiter is gone.
+ assert(Set(WNotFound, WError).forall(given => not(busy.after(reply(1, given)).hasWaiter(1)))),
+ }
+
+ run lookupTimeoutTest = all {
+ // A timeout fails the lookup closed.
+ assert(outputOf(busy, LookupTimeoutSInput(1)) == LookupDoneOutput({ query: "orchard", result: Unavailable })),
+ assert(not(busy.after(LookupTimeoutSInput(1)).hasWaiter(1))),
+ // A late reply to the abandoned lookup is dropped.
+ assert(outputOf(busy.after(LookupTimeoutSInput(1)), reply(1, WNotFound)) == NoShimOutput),
+ assert(isError(outputOf(busy, LookupTimeoutSInput(0)))),
+ assert(isError(outputOf(busy, LookupTimeoutSInput(9)))),
+ }
+
+ run correlationTest = all {
+ // An unknown nonce is dropped.
+ assert(outputOf(busy, ack(9, WAccepted)) == NoShimOutput and busy.after(ack(9, WAccepted)) == busy),
+ assert(outputOf(busy, reply(9, WNotFound)) == NoShimOutput and busy.after(reply(9, WNotFound)) == busy),
+ // An ack under a lookup's nonce is ignored, and the lookup keeps waiting.
+ // A reply under a submission's nonce is dropped.
+ assert(outputOf(busy, ack(1, WAccepted)) == NoShimOutput and busy.after(ack(1, WAccepted)) == busy),
+ assert(outputOf(busy, reply(0, WNotFound)) == NoShimOutput and busy.after(reply(0, WNotFound)) == busy),
+ // Request frames are not replies.
+ assert(isError(outputOf(busy, FrameSInput(Submit({ nonce: 0, payload: pOrchard }))))),
+ assert(isError(outputOf(busy, FrameSInput(Lookup({ nonce: 1, txid: "orchard" }))))),
+ }
+
+ // ------------------------------------------------------------------------
+ // Totality
+ // ------------------------------------------------------------------------
+
+ /// The function answers every input in every state, and an invalid
+ /// input leaves the state unchanged.
+ run totalityTest =
+ assert(tuples(STATES, INPUTS).forall(((state, input)) =>
+ val result = shim(state, input)
+ and {
+ result.state.nextNonce >= state.nextNonce,
+ isError(result.out) implies result.state == state,
+ }))
+}
diff --git a/zeronym/spec/quint/tests/trustTest.qnt b/zeronym/spec/quint/tests/trustTest.qnt
new file mode 100644
index 00000000..1af164e9
--- /dev/null
+++ b/zeronym/spec/quint/tests/trustTest.qnt
@@ -0,0 +1,135 @@
+// -*- mode: Bluespec; -*-
+
+/// The trust matrix, cell by cell: for every guarantee that needs a component
+/// to be honest, a run in which that component is Byzantine and the guarantee
+/// fails.
+///
+/// Each run is built from the machine's own steps. It names the one Byzantine
+/// transition it relies on, written out as a `...With` step, and ends by
+/// stating what in the wallet's log, the soup or the audit record constitutes
+/// the failure. The guarantee is asserted in the state just before that
+/// transition, so the run shows the lie is what breaks it.
+
+module trustTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import wire.* from "../wire"
+ import indexer.* from "../indexer"
+ import abstractHub.* from "../abstractHub"
+ import shim.* from "../shim"
+ import protocol.* from "../protocol"
+
+ // ------------------------------------------------------------------------
+ // A Byzantine hub (`byzHub`)
+ // ------------------------------------------------------------------------
+
+ /// G2 needs the hub. Asked by a third party about a queued txid, it answers
+ /// with the queued bytes.
+ run hubServesQueuedBodyTest =
+ initByzHub
+ .then(submitTo(0, early))
+ .then(thirdPartyLearnsTxidWith("early"))
+ .then(thirdPartyLookupWith("early"))
+ .expect(queuedBytesConfidential)
+ .then(hubReceiveWith(
+ fromThirdParty(lookupMail(0, "early")), INotFound,
+ { hub: s.hub, reply: AWire(render(FromIndexer(IFound({ body: Some(early), height: AtZero })))) },
+ ))
+ .expect(s.replies(ThirdPartyAddr) == Set({ nonce: 0, reply: WFound({ body: Some(early), height: AtZero }) }))
+ .expect(s.tpLearned() == Set(early) and s.onChain("early") == Absent)
+ // What it learned came in the body of a reply addressed to it.
+ .expect(s.repliedBodies(ThirdPartyAddr) == Set(early) and s.operator == Set())
+ .expect(not(queuedBytesConfidential))
+
+ /// G4 needs the hub. It answers not found for a transaction it has queued.
+ run hubDeniesQueuedTest =
+ initByzHub
+ .then(submitTo(0, early))
+ .then(ask("early"))
+ .expect(lookupValidityPerHub)
+ .then(hubReceiveWith(
+ lookupMail(1, "early"), INotFound,
+ { hub: s.hub, reply: AWire(render(FromIndexer(INotFound))) },
+ ))
+ .then(deliverToShim(replyMail(1, WNotFound)))
+ .expect(lastEvent == Got({ query: "early", obs: NotFound, via: Some(1) }))
+ .expect(s.hub.queue == Set(early) and audit.windows.get(1) == Set(Pending))
+ .expect(not(lookupValidityPerHub))
+
+ /// G4 needs the hub, second run. It serves a mempool transaction as mined,
+ /// at a height it made up. The txid is right, so the shim passes it on.
+ run hubServesFalseHeightTest =
+ initByzHub
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(ask("early"))
+ .expect(lookupValidityPerHub)
+ .then(hubReceiveWith(
+ lookupMail(1, "early"), chainAnswer(s.indexer, "early"),
+ { hub: s.hub, reply: AWire(render(FromIndexer(IFound({ body: Some(early), height: AtOther })))) },
+ ))
+ .then(deliverToShim(replyMail(1, WFound({ body: Some(early), height: AtOther }))))
+ .expect(lastEvent == Got({ query: "early", obs: Tx({ payload: early, height: AtOther }), via: Some(1) }))
+ .expect(s.onChain("early") == InMempool)
+ .expect(audit.windows.get(1) == Set(Tx({ payload: early, height: AtZero })))
+ .expect(not(lookupValidityPerHub) and txidAuthenticity)
+
+ /// G3 survives. The hub answers with another transaction; the shim compares
+ /// txids and refuses it.
+ run wrongTransactionIsRefusedTest =
+ initByzHub
+ .then(sendToHub(early))
+ .then(ask("early"))
+ .then(hubReceiveWith(
+ lookupMail(1, "early"), INotFound,
+ { hub: s.hub, reply: AWire(render(FromIndexer(IFound({ body: Some(tight), height: AtMined })))) },
+ ))
+ .then(deliverToShim(replyMail(1, WFound({ body: Some(tight), height: AtMined }))))
+ .expect(lastEvent == Got({ query: "early", obs: NotFound, via: Some(1) }))
+ .expect(txidAuthenticity)
+
+ // ------------------------------------------------------------------------
+ // A Byzantine indexer (`byzIndexer`)
+ // ------------------------------------------------------------------------
+
+ // A hub folds several indexer endpoints into one answer. A lookup answer
+ // comes from the first endpoint that says found, so one misbehaving endpoint
+ // is enough for the first two runs. The tip is the maximum over endpoints,
+ // so holding it back, as the last two do, takes every endpoint. The model
+ // has one abstract indexer and does not enforce that difference.
+
+ /// G2 needs the indexer. It is offered a batch, reports nothing judged, and
+ /// then serves the unpublished bytes in a lookup answer, which the honest
+ /// hub forwards to whoever asked.
+ run indexerServesUnpublishedBodyTest =
+ initByzIndexer
+ .then(submitTo(0, early))
+ .then(hubTake)
+ .then(judge(early, Retryable))
+ .expect(s.indexer.offered == Set(early) and s.onChain("early") == Absent)
+ .then(thirdPartyLearnsTxidWith("early"))
+ .then(thirdPartyLookupWith("early"))
+ .expect(queuedBytesConfidential)
+ .then(deliverLookupFrom(
+ ThirdPartyAddr, 0, "early", IFound({ body: Some(early), height: AtZero }),
+ ))
+ .expect(s.replies(ThirdPartyAddr) == Set({ nonce: 0, reply: WFound({ body: Some(early), height: AtZero }) }))
+ .expect(s.tpLearned() == Set(early) and s.onChain("early") == Absent)
+ // What it learned came in the body of a reply addressed to it.
+ .expect(s.repliedBodies(ThirdPartyAddr) == Set(early) and s.operator == Set())
+ .expect(not(queuedBytesConfidential))
+
+ /// G4 needs the indexer. For a transaction that exists nowhere it answers
+ /// "found, height 0, no body". The hub forwards it unchanged, and on the
+ /// wire it is the hub's own "queued here": the wallet sees pending.
+ run indexerForgesPendingTest =
+ initByzIndexer
+ .then(sends(Clean(early), true))
+ .then(ask("early"))
+ .expect(lookupValidityPerHub)
+ .then(deliverLookupFrom(ShimAddr, 1, "early", IFound({ body: None, height: AtZero })))
+ .then(deliverToShim(replyMail(1, WFound({ body: None, height: AtZero }))))
+ .expect(lastEvent == Got({ query: "early", obs: Pending, via: Some(1) }))
+ .expect(s.hub.queue == Set() and audit.windows.get(1) == Set(NotFound))
+ .expect(not(lookupValidityPerHub))
+}
diff --git a/zeronym/spec/quint/tests/wireTest.qnt b/zeronym/spec/quint/tests/wireTest.qnt
new file mode 100644
index 00000000..54792ca0
--- /dev/null
+++ b/zeronym/spec/quint/tests/wireTest.qnt
@@ -0,0 +1,109 @@
+// -*- mode: Bluespec; -*-
+
+/// The wire layer, checked exhaustively over a small universe of payloads,
+/// heights and queries.
+module wireTest {
+ import basicSpells.* from "../spells/basicSpells"
+ import types.* from "../types"
+ import wire.* from "../wire"
+
+ pure val pA = { id: "a", txid: Some("ta"), created: 1, expiry: Some(9), class: OrchardTouching, oversize: false }
+ pure val pATwin = { ...pA, id: "a-twin" }
+ pure val pB = { id: "b", txid: Some("tb"), created: 1, expiry: None, class: PassThrough, oversize: false }
+ pure val pJunk = { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, oversize: false }
+
+ pure val PAYLOADS = Set(pA, pATwin, pB, pJunk)
+ pure val HEIGHTS = WIRE_HEIGHTS
+ pure val QUERIES = Set("ta", "tb", "unknown")
+ pure val BODIES = Set(None).union(PAYLOADS.map(payload => Some(payload)))
+
+ /// Every indexer answer the type admits.
+ pure val ANSWERS =
+ tuples(BODIES, HEIGHTS).map(((body, height)) => IFound({ body: body, height: height }))
+ .union(Set(INotFound, IUnavailable))
+
+ /// The answers an honest indexer gives: a found transaction has a body, and
+ /// the body parses.
+ pure val HONEST_ANSWERS = ANSWERS.filter(answer =>
+ match answer {
+ | IFound(found) =>
+ match found.body {
+ | Some(payload) => isSome(payload.txid)
+ | None => false
+ }
+ | INotFound => true
+ | IUnavailable => true
+ })
+
+ pure val HONEST_OUTCOMES = Set(QueueHit).union(HONEST_ANSWERS.map(answer => FromIndexer(answer)))
+
+ pure val REPLIES =
+ tuples(BODIES, HEIGHTS).map(((body, height)) => WFound({ body: body, height: height }))
+ .union(Set(WNotFound, WError))
+
+ pure val REFUSALS = Set(TipStale, HubDraining, ExpiryTooTight)
+
+ /// Rendering an honest outcome and reading it back gives what the
+ /// outcome means.
+ run renderThenInterpretIsMeaningTest =
+ assert(tuples(HONEST_OUTCOMES, QUERIES).forall(((outcome, query)) =>
+ interpretReply(render(outcome), query) == meaning(outcome, query)))
+
+ /// The documented collision: a queue hit and an indexer answer of
+ /// "found, height 0, no body" are the same reply, though they mean different
+ /// things. The wallet cannot tell them apart: it is told pending for both,
+ /// so an indexer that answers that way for a transaction nobody holds makes
+ /// the wallet see pending (`indexerForgesPendingTest` is that run). No two
+ /// honest outcomes collide.
+ run sentinelCollisionTest = all {
+ assert(render(QueueHit) == render(FromIndexer(IFound({ body: None, height: AtZero })))),
+ assert(QUERIES.forall(query =>
+ and {
+ interpretReply(render(QueueHit), query) == Pending,
+ interpretReply(render(FromIndexer(IFound({ body: None, height: AtZero }))), query) == Pending,
+ })),
+ assert(QUERIES.forall(query =>
+ meaning(QueueHit, query)
+ != meaning(FromIndexer(IFound({ body: None, height: AtZero })), query))),
+ assert(tuples(HONEST_OUTCOMES, HONEST_OUTCOMES).forall(((left, right)) =>
+ left != right implies render(left) != render(right))),
+ }
+
+ /// The shim serves a transaction only when its txid is the one asked
+ /// for, and compares nothing else.
+ run servedOnlyOnMatchingTxidTest = all {
+ assert(tuples(REPLIES, QUERIES).forall(((reply, query)) =>
+ match interpretReply(reply, query) {
+ | Tx(tx) => tx.payload.txid == Some(query)
+ | _ => true
+ })),
+ // Found with no body at a mined height is not a transaction and not the
+ // pending sentinel.
+ assert(interpretReply(WFound({ body: None, height: AtMined }), "ta") == NotFound),
+ // A twin of the transaction asked for is served.
+ assert(interpretReply(WFound({ body: Some(pATwin), height: AtMined }), "ta")
+ == Tx({ payload: pATwin, height: AtMined })),
+ // The height is passed through as given.
+ assert(HEIGHTS.forall(height =>
+ interpretReply(WFound({ body: Some(pA), height: height }), "ta")
+ == Tx({ payload: pA, height: height }))),
+ // Bytes that do not parse are never served, at any height.
+ assert(tuples(HEIGHTS, QUERIES).forall(((height, query)) =>
+ interpretReply(WFound({ body: Some(pJunk), height: height }), query) == NotFound)),
+ }
+
+ /// A hub error fails closed. It is never reported as not found.
+ run errorIsNeverNotFoundTest =
+ assert(QUERIES.forall(query => interpretReply(WError, query) == Unavailable))
+
+ /// A draining hub refuses under the queue-full code; a fresh admission
+ /// and a duplicate are one acceptance. Every refusal has its own code.
+ run ackRenderingTest = all {
+ assert(renderAck(Refused(HubDraining)) == WRefused(WQueueFull)),
+ assert(renderAck(Admitted) == WAccepted),
+ assert(renderAck(Duplicate) == WAccepted),
+ assert(REFUSALS.forall(refusal => renderAck(Refused(refusal)) != WAccepted)),
+ assert(tuples(REFUSALS, REFUSALS).forall(((left, right)) =>
+ renderAck(Refused(left)) == renderAck(Refused(right)) implies left == right)),
+ }
+}
diff --git a/zeronym/spec/quint/tlc.sh b/zeronym/spec/quint/tlc.sh
new file mode 100755
index 00000000..7e6cf91e
--- /dev/null
+++ b/zeronym/spec/quint/tlc.sh
@@ -0,0 +1,186 @@
+#!/bin/sh
+# Check one invariant of one configuration exhaustively, with TLC.
+#
+# tlc.sh FILE MAIN INIT STEP INVARIANT
+# tlc.sh --fetch only fetch Apalache, if it is missing
+#
+# FILE is a Quint file, MAIN the module in it, INIT a named init action built
+# on `initWith`, STEP a step relation and INVARIANT a state predicate. On
+# success exactly one line is printed:
+#
+# holds every reachable state satisfies it
+# violated TLC found a counterexample that long
+#
+# Anything else is a failure: a line `FAIL : ` on stderr, no
+# verdict line, and a non-zero exit status. Nothing skips a stage.
+#
+# The route, and why it is not `quint verify`: the Apalache server behind
+# `quint verify` refuses a specification larger than 20 MB, and these compile
+# to more. So the three stages are run by hand:
+#
+# 1. quint compile --target=json (stdout; `--out` writes another format)
+# 2. apalache-mc typecheck (exports TLA+, named after the output file)
+# 3. tlc2.TLC from the Apalache jar
+#
+# Between 2 and 3 a filter removes the primes that the export leaves on the
+# assignments of the init operator, which TLC rejects. That is a workaround
+# for the export, tied to the pinned versions below.
+#
+# TLC_WORKERS and TLC_HEAP size the run, and TLC_TIMEOUT (seconds) bounds it: a
+# run that TLC has not finished by then is a failure, never a verdict. QUINT is
+# the Quint command. TLC_TRACE, if set, names a file that receives TLC's output
+# when it finds a violation.
+set -u
+
+QUINT=${QUINT:-"npx --yes @informalsystems/quint@0.33.0"}
+QUINT_VERSION=0.33.0
+APALACHE_VERSION=0.62.1
+APALACHE=$HOME/.quint/apalache-dist-$APALACHE_VERSION/apalache
+JAR=$APALACHE/lib/apalache.jar
+WORKERS=${TLC_WORKERS:-2}
+HEAP=${TLC_HEAP:-4g}
+TIMEOUT=${TLC_TIMEOUT:-300}
+
+die() {
+ echo "FAIL $1" >&2
+ exit 1
+}
+
+# The Apalache distribution is fetched by Quint the first time it verifies
+# anything. The verdict of that run is irrelevant.
+fetch() {
+ [ -f "$JAR" ] && return 0
+ dir=$(mktemp -d)
+ cat >"$dir/fetch.qnt" <<'EOF'
+module fetch {
+ var x: int
+ action init = x' = 0
+ action step = x' = x
+}
+EOF
+ (cd "$dir" && $QUINT verify fetch.qnt --max-steps=1 >fetch.log 2>&1)
+ if [ ! -f "$JAR" ]; then
+ tail -5 "$dir/fetch.log" >&2
+ rm -rf "$dir"
+ die "toolchain: no Apalache $APALACHE_VERSION at $JAR"
+ fi
+ rm -rf "$dir"
+}
+
+# `tlc.sh --fetch` only fetches. A caller that runs several checks at once
+# fetches first: two first runs would unpack it into ~/.quint together.
+if [ "${1:-}" = --fetch ]; then
+ fetch
+ exit 0
+fi
+
+[ $# -eq 5 ] || die "usage: tlc.sh FILE MAIN INIT STEP INVARIANT"
+case $1 in
+ /*) file=$1 ;;
+ *) file=$PWD/$1 ;;
+esac
+main=$2 init=$3 step=$4 invariant=$5
+[ -f "$file" ] || die "compile: no such file: $file"
+
+command -v java >/dev/null 2>&1 || die "toolchain: java not found"
+java -version >/dev/null 2>&1 || die "toolchain: java does not run"
+version=$($QUINT --version 2>/dev/null)
+[ "$version" = "$QUINT_VERSION" ] || die "toolchain: quint is '$version', not $QUINT_VERSION"
+
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+cd "$work" || die "toolchain: cannot enter $work"
+
+fetch
+
+# 1. Compile. A misspelt name leaves stdout empty and exits non-zero.
+if ! $QUINT compile --target=json --main="$main" --init="$init" --step="$step" \
+ --invariant="$invariant" "$file" >"$main.qnt.json" 2>compile.log; then
+ tail -5 compile.log >&2
+ die "compile: quint compile failed ($main $init $step $invariant)"
+fi
+[ -s "$main.qnt.json" ] || die "compile: quint compile wrote nothing"
+
+# 2. Export. TLC wants the module named after its file.
+if ! "$APALACHE/bin/apalache-mc" typecheck --out-dir="$work/apalache" \
+ --output="$work/export.tla" "$main.qnt.json" >export.log 2>&1; then
+ tail -5 export.log >&2
+ die "export: apalache-mc typecheck failed"
+fi
+grep -q "^-* MODULE export -*\$" export.tla 2>/dev/null || die "export: no TLA+ module was written"
+
+# The filter. It rewrites `x' := e` to `x := e` (the export may break the line
+# after the prime) in the definitions named
+# `initWith` and INIT and in no other, so a step action whose name merely
+# contains "init" keeps its assignments. Exactly one of the two holds
+# assignments (`initWith`); any other count means the export is not shaped as
+# expected, and a verdict from it would be about another machine.
+if ! awk -v names="initWith $init" -v expected=1 '
+ BEGIN { count = split(names, list, " "); for (i = 1; i <= count; i++) wanted[list[i]] = 1 }
+ /^[A-Za-z_][A-Za-z0-9_]*(\(.*\))? ==/ {
+ name = $0
+ sub(/[( ].*/, "", name)
+ inside = (name in wanted)
+ fresh = 1
+ }
+ /^$/ { inside = 0 }
+ inside {
+ if (gsub(/\047 :=/, " :=") + sub(/\047$/, "") > 0 && fresh) { changed++; fresh = 0 }
+ if ($0 ~ /[A-Za-z0-9_]\047/) { left++ }
+ }
+ { sub(/ MODULE export /, " MODULE " module " ") ; print }
+ END {
+ if (left > 0) { print "a primed variable is left in an init operator" > "/dev/stderr"; exit 4 }
+ if (changed != expected) {
+ print changed + 0 " init definitions rewritten, expected " expected > "/dev/stderr"
+ exit 3
+ }
+ }' module="$main" export.tla >"$main.tla" 2>filter.log; then
+ cat filter.log >&2
+ die "filter: the init operator is not as expected"
+fi
+
+# 3. TLC. `-deadlock` switches deadlock checking off: every machine here stops
+# at its height bound.
+printf 'INIT q_init\nNEXT q_step\nINVARIANT q_inv\n' >"$main.cfg"
+java "-Xmx$HEAP" -XX:+UseParallelGC -cp "$JAR" tlc2.TLC -deadlock -workers "$WORKERS" \
+ -metadir "$work/states" -config "$main.cfg" "$main.tla" >tlc.log 2>&1 &
+tlc=$!
+(sleep "$TIMEOUT" && touch "$work/timed-out" && kill "$tlc") >/dev/null 2>&1 &
+watchdog=$!
+wait "$tlc"
+status=$?
+kill "$watchdog" 2>/dev/null
+wait "$watchdog" 2>/dev/null
+
+# Out of time. How far TLC got is reported, as its last progress line has it.
+if [ -f "$work/timed-out" ]; then
+ reached=$(sed -n 's/^Progress(\([0-9]*\)).*, \([0-9,]*\) distinct states found.*, \([0-9,]*\) states left on queue.*/\2 distinct states, depth \1, \3 on queue/p' tlc.log | tail -1)
+ die "tlc: not exhausted in $TIMEOUT s (${reached:-no progress reported})"
+fi
+
+# A dead init (a guard that is false) leaves TLC with nothing to explore, and
+# it reports "No error has been found".
+if grep -q "Finished computing initial states: 0 distinct states generated" tlc.log; then
+ die "tlc: no initial state: the guard of $init is false"
+fi
+if [ "$status" -eq 0 ] \
+ && grep -q "Finished computing initial states: [1-9]" tlc.log \
+ && grep -q "Model checking completed. No error has been found." tlc.log \
+ && grep -q " 0 states left on queue" tlc.log; then
+ states=$(sed -n 's/^[0-9][0-9]* states generated, \([0-9][0-9]*\) distinct states found, 0 states left on queue.*/\1/p' tlc.log | tail -1)
+ depth=$(sed -n 's/^The depth of the complete state graph search is \([0-9][0-9]*\).*/\1/p' tlc.log | tail -1)
+ [ -n "$states" ] && [ -n "$depth" ] || { tail -15 tlc.log >&2; die "tlc: no state count or depth reported"; }
+ echo "holds $states $depth"
+elif [ "$status" -eq 12 ] && grep -q "Error: Invariant q_inv is violated by the initial state" tlc.log; then
+ [ -n "${TLC_TRACE:-}" ] && cp tlc.log "$TLC_TRACE"
+ echo "violated 1"
+elif [ "$status" -eq 12 ] && grep -q "Error: Invariant q_inv is violated." tlc.log; then
+ length=$(grep -c '^State [0-9][0-9]*:' tlc.log)
+ [ "$length" -gt 0 ] || { tail -15 tlc.log >&2; die "tlc: a violation with no trace"; }
+ [ -n "${TLC_TRACE:-}" ] && cp tlc.log "$TLC_TRACE"
+ echo "violated $length"
+else
+ tail -15 tlc.log >&2
+ die "tlc: no verdict (exit status $status)"
+fi
diff --git a/zeronym/spec/quint/types.qnt b/zeronym/spec/quint/types.qnt
new file mode 100644
index 00000000..aed53c38
--- /dev/null
+++ b/zeronym/spec/quint/types.qnt
@@ -0,0 +1,202 @@
+// -*- mode: Bluespec; -*-
+
+/// The vocabulary of the zeronym protocol: every domain the components, the
+/// wire and the properties talk about, and nothing that computes.
+///
+/// Domains are sum types. A value that the protocol cannot produce (a refusal
+/// carrying a transaction, a lookup answer that is both found and not found)
+/// has no representation here, so no definition downstream has to rule it out.
+module types {
+ import basicSpells.* from "./spells/basicSpells"
+
+ type TxId = str
+ type Height = int
+ type Nonce = int
+
+ // ------------------------------------------------------------------------
+ // Transactions
+ // ------------------------------------------------------------------------
+
+ /// How the shim classifies a `SendTransaction` body. `Unparseable` is the
+ /// shim's own parser giving up; it is treated as a migration, never forwarded.
+ type Class = OrchardTouching | PassThrough | Unparseable
+
+ /// A transaction's bytes, abstracted to what a party can compute from them.
+ ///
+ /// - `id` stands for the bytes themselves, and so for their SHA-256, the key
+ /// a hub's queue uses.
+ /// - `txid` is what the hub's and the node's parser compute, absent when the
+ /// bytes do not deserialise. Two payloads with different `id` and the same
+ /// `txid` are twins: the txid does not commit to every byte (ZIP 244).
+ /// - `created` is the chain height the wallet built the transaction at.
+ /// - `expiry` is `nExpiryHeight`, absent when the transaction never expires
+ /// or does not parse.
+ /// - `class` is the shim's classification. It is independent of `txid`: the
+ /// shim rejects trailing bytes that the hub's parser accepts.
+ /// - `oversize`: the bytes do not fit the fixed hub frame.
+ type Payload = {
+ id: str,
+ txid: Option[TxId],
+ created: Height,
+ expiry: Option[Height],
+ class: Class,
+ oversize: bool,
+ }
+
+ /// Whether `payload` was built by a wallet that honours the supported expiry
+ /// floor: it never expires, or expires at least `minWalletExpiry` blocks
+ /// after the height it was built at.
+ pure def conforming(payload: Payload, minWalletExpiry: int): bool =
+ match payload.expiry {
+ | None => true
+ | Some(expiry) => expiry >= payload.created + minWalletExpiry
+ }
+
+ /// Whether two payloads are different bytes with the same transaction id.
+ pure def areTwins(left: Payload, right: Payload): bool =
+ and {
+ left.id != right.id,
+ isSome(left.txid),
+ left.txid == right.txid,
+ }
+
+ /// The transaction ids a set of payloads carries.
+ pure def txidsOf(payloads: Set[Payload]): Set[TxId] =
+ payloads.fold(Set(), (acc, payload) =>
+ match payload.txid {
+ | Some(txid) => acc.union(Set(txid))
+ | None => acc
+ })
+
+ /// The id a wallet knows its transaction by, and asks for. For bytes no
+ /// parser accepts it is a name that no hub or node will ever compute.
+ pure def walletTxid(payload: Payload): TxId =
+ payload.txid.unwrapOr(payload.id)
+
+ /// What the wallet hands the shim in a `SendTransaction`: a body the shim
+ /// read in full, a body it could not read, or an empty one.
+ type SendInput = Clean(Payload) | Unreadable | EmptyBody
+
+ // ------------------------------------------------------------------------
+ // Chain and indexer
+ // ------------------------------------------------------------------------
+
+ /// Where a transaction stands on the chain. It only ever moves forward.
+ type Inclusion = Absent | InMempool | Mined
+
+ /// The height a lookup answer carries, relative to the transaction it names:
+ /// 0, meaning the mempool; the height it was mined at; or any other height.
+ /// No answer is compared against the chain height except through this.
+ type WireHeight = AtZero | AtMined | AtOther
+
+ pure val WIRE_HEIGHTS = Set(AtZero, AtMined, AtOther)
+
+ /// The height a lookup answer carries for `inclusion`.
+ pure def answerHeight(inclusion: Inclusion): WireHeight =
+ match inclusion {
+ | Mined => AtMined
+ | InMempool => AtZero
+ | Absent => AtZero
+ }
+
+ /// An indexer's answer to a transaction lookup. An honest indexer always
+ /// returns a body with `IFound`; the type admits a missing one because the
+ /// hub forwards whatever it is given.
+ type IndexerAnswer =
+ | IFound({ body: Option[Payload], height: WireHeight })
+ | INotFound
+ | IUnavailable
+
+ /// An indexer's verdict on one broadcast transaction. `Retryable` means
+ /// nothing judged it: the indexer could not be reached or could not be read.
+ type Verdict = Accepted | AlreadyKnown | Rejected | Retryable
+
+ // ------------------------------------------------------------------------
+ // Hub
+ // ------------------------------------------------------------------------
+
+ /// Why a hub refuses a submission, in the order admission checks them.
+ type Refusal = TipStale | HubDraining | ExpiryTooTight
+
+ /// A hub's decision on a submission. `Duplicate` is a success: the bytes are
+ /// already queued here.
+ type AckKind = Admitted | Duplicate | Refused(Refusal)
+
+ /// Whether a decision promises the hub holds the payload.
+ pure def isAccepted(kind: AckKind): bool =
+ match kind {
+ | Admitted => true
+ | Duplicate => true
+ | Refused(_) => false
+ }
+
+ /// What a hub found for a lookup: its own queue, or its indexer's answer.
+ type HubOutcome = QueueHit | FromIndexer(IndexerAnswer)
+
+ // ------------------------------------------------------------------------
+ // Participants
+ // ------------------------------------------------------------------------
+
+ /// A network address. The third party is any client of the hub's public,
+ /// unauthenticated address other than the shim.
+ type Addr = ShimAddr | HubAddr | ThirdPartyAddr
+
+ /// Whether a component follows the protocol. A Byzantine component is not
+ /// marked in any message or state: it simply draws its transitions from a
+ /// wider relation than the honest one.
+ type Role = Honest | Byzantine
+
+ /// The role of each component.
+ type Roles = { hub: Role, indexer: Role }
+
+ /// How a hub's view of the chain tip relates to the true height.
+ ///
+ /// - `TipTimely`: every running hub sees each block before the next one.
+ /// - `TipMayRegress`: a report may be up to the reorg allowance behind.
+ /// - `TipMayLag`: a hub may go without a report for a while, and is stale
+ /// once the silence reaches the staleness window.
+ type TipModel = TipTimely | TipMayRegress | TipMayLag
+
+ // ------------------------------------------------------------------------
+ // What the wallet observes
+ // ------------------------------------------------------------------------
+
+ /// The answer to a `SendTransaction`.
+ type SendObs =
+ | SentOk // diverted; error code 0
+ | SentToOperator // not a migration; the operator's indexer has it
+ | SendUnavailable // failed closed: unreadable body, or no hub reachable
+ | SendInvalid // empty body
+ | SendTooLarge // does not fit the hub frame
+
+ /// The answer to a `GetTransaction`.
+ type LookupObs =
+ | Pending // found, height 0, no body
+ | Tx({ payload: Payload, height: WireHeight }) // the transaction, as served
+ | NotFound
+ | Unavailable // failed closed
+
+ /// One completed wallet request. For a lookup, `via` is the nonce of the hub
+ /// request whose reply produced the answer, absent when no reply did.
+ type WalletEvent =
+ | Sent({ input: SendInput, obs: SendObs })
+ | Got({ query: TxId, obs: LookupObs, via: Option[Nonce] })
+
+ // ------------------------------------------------------------------------
+ // Shapes shared by the components
+ // ------------------------------------------------------------------------
+
+ /// What a component's transition function returns: its next state and the
+ /// one output the step produced.
+ type Result[s, o] = { state: s, out: o }
+
+ /// One configuration of the protocol: the transactions in play, the bound
+ /// of the model, and the roles. Field by field it is the list of constants
+ /// in `protocol.qnt`.
+ type Config = {
+ payloads: Set[Payload],
+ twins: Set[Payload],
+ maxRequests: int,
+ roles: Roles,
+ }
+}
diff --git a/zeronym/spec/quint/wire.qnt b/zeronym/spec/quint/wire.qnt
new file mode 100644
index 00000000..8c655437
--- /dev/null
+++ b/zeronym/spec/quint/wire.qnt
@@ -0,0 +1,111 @@
+// -*- mode: Bluespec; -*-
+
+/// The shim-to-hub wire, at the level of what a frame can say.
+///
+/// Four frames exist: a submission and its ack, a lookup and its reply. Byte
+/// layout, padding and malformed frames are below this level. What is modelled
+/// is the part with protocol consequences: which distinctions a hub's answer
+/// keeps when it is put on the wire, and how the shim reads it back.
+module wire {
+ import basicSpells.* from "./spells/basicSpells"
+ import types.* from "./types"
+
+ /// The refusal codes an ack can carry, one per refusal.
+ type WireRefusal = WExpiryTooTight | WQueueFull | WTipStale
+
+ /// An ack's disposition. A fresh admission and a duplicate are the same ack.
+ type WireAck = WAccepted | WRefused(WireRefusal)
+
+ /// A lookup reply's disposition. Only `WFound` has room for a height and a
+ /// body; a `not_found` or an `error` that carries either does not decode.
+ type WireReply =
+ | WFound({ body: Option[Payload], height: WireHeight })
+ | WNotFound
+ | WError
+
+ /// A frame. Requests and replies are matched by `nonce` and by nothing else.
+ type Msg =
+ | Submit({ nonce: Nonce, payload: Payload })
+ | Ack({ nonce: Nonce, ack: WireAck })
+ | Lookup({ nonce: Nonce, txid: TxId })
+ | LookupReply({ nonce: Nonce, reply: WireReply })
+
+ /// A hub's decision as an ack. A draining hub answers under the queue-full
+ /// code, as the implementation does.
+ pure def renderAck(kind: AckKind): WireAck =
+ match kind {
+ | Admitted => WAccepted
+ | Duplicate => WAccepted
+ | Refused(refusal) =>
+ match refusal {
+ | TipStale => WRefused(WTipStale)
+ | HubDraining => WRefused(WQueueFull)
+ | ExpiryTooTight => WRefused(WExpiryTooTight)
+ }
+ }
+
+ /// A hub's lookup outcome as a reply. A queue hit is "found, height 0, no
+ /// body": the hub confirms the transaction is pending without handing its
+ /// bytes to whoever asked. An indexer answer is forwarded as it came.
+ pure def render(outcome: HubOutcome): WireReply =
+ match outcome {
+ | QueueHit => WFound({ body: None, height: AtZero })
+ | FromIndexer(answer) =>
+ match answer {
+ | IFound(found) => WFound(found)
+ | INotFound => WNotFound
+ | IUnavailable => WError
+ }
+ }
+
+ /// What a hub outcome is meant to tell a wallet asking for `query`. This is
+ /// the intent, written without reference to the wire; `interpretReply` after
+ /// `render` is the mechanism, and the two agree on every outcome a queue or
+ /// an honest indexer produces.
+ ///
+ /// They disagree on one outcome an honest indexer never produces: an indexer
+ /// answer of "found, height 0, no body". It means nothing was returned, and
+ /// on the wire it is the hub's own "queued here", so the wallet is told
+ /// pending. The encoding is not injective there, and the shim cannot tell.
+ pure def meaning(outcome: HubOutcome, query: TxId): LookupObs =
+ match outcome {
+ | QueueHit => Pending
+ | FromIndexer(answer) =>
+ match answer {
+ | IFound(found) =>
+ match found.body {
+ | Some(payload) =>
+ if (payload.txid == Some(query))
+ Tx({ payload: payload, height: found.height })
+ else NotFound
+ // An indexer that reports a transaction and returns none has
+ // told the wallet nothing.
+ | None => NotFound
+ }
+ | INotFound => NotFound
+ | IUnavailable => Unavailable
+ }
+ }
+
+ /// How the shim reads a lookup reply for `query`. The arms, in order:
+ ///
+ /// 1. found, height 0, no body: relayed as pending;
+ /// 2. found otherwise: served only if the returned bytes parse and their
+ /// txid is the one asked for, else not found. Nothing else is compared:
+ /// not the bytes, so a twin passes, and not the height;
+ /// 3. not found;
+ /// 4. error: the lookup fails closed, and is never reported as not found.
+ pure def interpretReply(reply: WireReply, query: TxId): LookupObs =
+ match reply {
+ | WFound(found) =>
+ match found.body {
+ | None => if (found.height == AtZero) Pending else NotFound
+ | Some(payload) =>
+ if (payload.txid == Some(query))
+ Tx({ payload: payload, height: found.height })
+ else NotFound
+ }
+ | WNotFound => NotFound
+ | WError => Unavailable
+ }
+}