diff --git a/.github/workflows/zeronym-guards.yml b/.github/workflows/zeronym-guards.yml
index 815d2b18..671eae7e 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'
+
# Formatting drift, on the cheap runner and without waiting for a compile.
# `hub` and `shim` are separate workspaces, so each gets its own step.
fmt:
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..19bf227d
--- /dev/null
+++ b/zeronym/spec/quint/README.md
@@ -0,0 +1,361 @@
+# The zeronym protocol, specified in Quint
+
+A [Quint][quint] 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.
+
+> [!NOTE]
+> Checked against: `main` at `2bae0a6`, except the hub's tip rule, which is checked against the open #92 at `b767ac9`, the shim's classifier, which is checked against the open #94 at `59b602a`, and the hub's burn set and nullifier check, which are checked against `main` at `6c2227c` (#104, #106). Citations marked "at #92" or "at #94" are line numbers there.
+
+- [System][system]
+- [Assumptions][assumptions]
+- [Out of scope][out-of-scope]
+- [Threat model][threat-model]
+- [Guarantees][guarantees]
+- [Trust matrix][trust-matrix]
+- [Known gaps][known-gaps]
+- [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`][zeronym-readme].
+
+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 spec][protocol-spec] has every actor, but its hub is abstract: a queue that can flush at any time. Random simulation and scripted runs check this spec.
+- The [hub spec][hub-spec] models one hub concretely along with the chain, and the two things the hub asks its indexer: the tip, and a verdict on each broadcast. It owns everything the abstract hub leaves out: 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.
+
+
+Indexer, network and observer
+
+- **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.
+- **Observer.** 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: the three lookup replies and what the wallet sees
+
+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" with no body, at any height (a fault) | error | Unavailable |
+
+
+
+## Assumptions
+
+> What must be true of the world for the claims to apply.
+
+- **Roles.** 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`), and no message or state field records which it took. The set holds protocol moves only, so a component that leaks what it sees (by logging it, or through extra bytes, sizes or timing) falls outside it; see [Out of scope][out-of-scope]. The shim and the hub both run attested. An honest shim or hub runs a binary built from the commit under *Checked against*, which reproduces to the hash in its `deploy/EXPECTED_SHA256` and passes the auditor procedure in `zeronym/README.md` (`caution verify` is its step 2). 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 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.
+- **Byzantine hub** (protocol specification only). 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 answer from its nullifier view. Any lookup answer built from a payload it was offered or one the chain published. In the hub specification it also reports any tip in the model's range. On mainnet #92 drops a tip outside a band or above the plausible climb rate (`tip_guard.rs`), so this over-approximates the guard.
+- **Network.** May lose, duplicate, delay and reorder frames. Cannot forge or read them.
+- **Observer.** 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 `MAX_DELIVERY_LAG` blocks. A wallet asks only about transactions it has sent. The model also has wallets below the floor and submissions later than the delivery lag.
+- **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 (findings 1, 2 and 4).
+- **Time.** There is no clock. A timeout may happen at any moment; the staleness window is counted in blocks.
+
+## Out of scope
+
+> What the specification deliberately does not cover, and why.
+
+### Not modelled
+
+| Item | Reason |
+|---|---|
+| Several hubs | Production replicates: every shim sends every submission to every hub (`zeronym/shim/src/nym.rs:602-647`). Not checked as a result: two hubs disagreeing about one transaction; duplicate publication and a second enclave holding the plaintext, both accepted in production; told ok after a partial send; a lookup moving to the next address on a timeout (finding 9); one Byzantine replica breaking G2 and G4 |
+| Attestation, PCRs, TLS, STEVE | No in-protocol messages exist. Represented by the roles |
+| Mixnet internals; 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" |
+| 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 |
+| Anonymity-set size, shuffle, simultaneity | Not properties of a single run |
+| Covert channels: extra bytes on the real wire, sizes and timing | Messages are strictly typed. A message can carry only its type's fields, so one with extra data is unrepresentable in the model |
+| A transaction's inputs and outputs beyond the txids it spends from: output indices, values, scripts, addresses | A payload carries the txids its transparent inputs spend (`spends`) and what the shim's parser reads of its pools (`class`). Sprout, Sapling and Ironwood are one class, `OtherShielded`, because the classifier treats them alike |
+| Transaction dependencies at the node | The indexer judges each transaction on its own. #94 queues both legs of a TEX payment at the hub, and one flush may offer the second leg before the first; what a node answers then is outside the model |
+| What the hub's verdict and ack say, and the HTTP transport that waits for the verdict (`HubTransport::Http`, `--hub`) | The deployment is the mixnet (`HTTP_SUBMIT=0`): the shim tells the wallet ok without waiting, and nothing reads an ack. So in every configuration the shim's ok says only that the frame left the shim. That an accepted ack is only for a queued payload is unchecked, and a Byzantine hub's ack is modelled as truthful |
+| The hub's capacity and size refusals, the burn set's bound, and denial of service generally | Not claimed properties. The shim's own too-large refusal is modelled. A free burst of junk fills the entry cap for a flush window: finding 13 |
+| An observer submitting payloads of its own making | Possible, since the hub's address is public and unauthenticated. The model's observer submits only what it has learned or the chain has published. Finding 13 is what junk of its own making buys |
+| A different transaction with the same txid (a twin) | No configuration contains one. The pure wire test shows the shim would serve it (`servedOnlyOnMatchingTxidTest`): the shim compares the txid and nothing else |
+| 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 |
+
+## 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][wallet-threat-model]; the Security section of [`zeronym/README.md`][zeronym-readme] 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 observer; 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 | An admitted migration expires while the hub holds it | Chain timing; a flaky tip; Byzantine hub or indexer | Answered in part for supported wallets: under a timely or regressing tip, not under a stale one. Not checked for late arrivals and unsupported wallets |
+| 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; an observer's burst of junk (finding 13) | Not prevented |
+| T8 | The wallet sees its transaction's status go backwards | Network reordering; resubmission; the flush window (after a flush empties the queue, before the indexer has the batch) | Not prevented |
+| T9 | An acknowledged migration is lost to a crash, a failed final flush, or a requeue drop | None needed | Not prevented |
+| T10 | An observer who knows a txid learns it is queued | Unauthenticated observer | Accepted. A Nym hub answers on the mixnet only; a clearnet hub also answers on `POST /transaction` (#99) |
+| T11 | A lying indexer makes the hub flush early, shrinking the batch, or stop admitting | Byzantine indexer; one endpoint suffices | Bounded on mainnet by #92 (finding 11); possible inside the bound; recorded |
+| 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 | Observer; operator | Not modelled, except the route through a forwarded transaction (T19). `zeronym/README.md` claims it against the hub and the peer-to-peer network at any volume, and lists the operator's and the wallet's ISP's link at batch size one as not protected (T17) |
+| 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: the queries are outside the divert protocol. Listed as not protected in `zeronym/README.md`. The same txid reaching the operator in a forwarded `SendTransaction` is T19 |
+| T17 | Batch-size and timing anonymity; partitioning the anonymity set across hubs | Observer; operator | 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 and Caution in `zeronym/README.md`; a malicious shim build is excluded by the auditor procedure there and is not discussed further |
+| T19 | The operator learns a diverted transaction's txid on the wallet's connection, from a forwarded transaction that spends its output | Operator | Answered for a transparent-only spend, the second leg of a TEX payment (G9, by #94). Not prevented for a spend with a shielded bundle (K10) |
+| T20 | A substitute hub reads migrations on the clearnet hop: the shim checks only the certificate name for the hub address in its config | A network position on the shim-to-hub path plus a certificate for the hub's name: Caution or AWS on a managed app, a parent-host operator in BYOC, with whoever holds the hub's DNS zone | Assumed away by the honest-hub role. Listed as not protected in `zeronym/README.md`, whose auditor step 4 ties the address to an attested hub. Nym mode encrypts each frame to the hub's in-enclave key (#98) |
+| T21 | A second valid certificate for the wallet-facing name serves wallets while auditors reach the enclave | The operator, who holds the wallet-facing DNS zone, from a network position on the wallet's path | Assumed away by the honest-shim role. `zeronym/README.md` scopes the attestation to the auditor's own connection (#98) |
+| T22 | The operator sees the txids wallets look up, through the hub's lookup fall-through to an indexer it runs | Operator, when it also runs the hub's indexers | Not modelled: the indexer here is one party, distinct from the operator. `zeronym/README.md` states the condition; guard M14 and auditor step 4 check it (#98) |
+
+## Guarantees
+
+> Promises about whole runs of the system: this bad thing never happens.
+
+| Id | Name | What it says | Answers | Checked by |
+|---|---|---|---|---|
+| G1 | `operatorBlind` | Every transaction the shim forwards to the operator's indexer is one the classifier passes: a Sprout, Sapling or Ironwood transaction, or a coinbase | T1 | Simulation |
+| G2 | `queuedBytesConfidential` | Everything the observer has learned is on the chain, or was a transaction the classifier passes, given to the operator's indexer. 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 |
+| G5 | `pendingOnlyFromQueue` | Every "pending" the wallet is told was true at the hub that gave it: the transaction was queued there. G4 restricted to pending | T4 | Simulation |
+| G9 | `forwardedSpendsNoDiverted` | No transaction the shim forwards to the operator's indexer spends an output of one the shim diverted, in either order and before or after publication. Holds while every such spend has transparent parts only; a spend with a shielded bundle is K10 | T19 | Simulation; `texSecondLegIsDivertedTest` |
+| 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 |
+| G8 | `admissionMatchesCadence` | Every entry admitted, and not requeued, survives the first flush the cadence has not spent, with the mining margin to spare | 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, because a node judged an entry with its txid and the hub burned that txid, 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 |
+
+An unchecked corollary of G6b: if fewer blocks arrive while a flush is in flight than the mining margin reserves, a node that judges a supported wallet's first offer finds it unexpired. Nothing in the code bounds a flight in blocks (finding 4).
+
+A2 and A3 constrain a single hub step, not a state; the rest are state invariants. What each entry under "Checked by" is worth is under [How it is checked][how-it-is-checked].
+
+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][configurations]. "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`) | holds (`byzIndexer`) |
+| G4 | holds (`baseline`) | **required**: `hubDeniesQueuedTest`, `hubServesFalseHeightTest` | **required**: `indexerServesFalseHeightTest`. One endpoint suffices |
+| G5 | holds (`baseline`) | **required**: `hubForgesPendingTest` | holds (`byzIndexer`); `indexerEmptyAnswerIsUnavailableTest` |
+| G9 | holds (`baseline`) | holds (`byzHub`) | holds (`byzIndexer`) |
+| G6b | holds (`timely`, `flakyTip`) | argued, not checked: a hub that admits while it has no tip breaks it | **required**: `indexerWithholdsTipFromConformingTest`. Needs every endpoint |
+| G8 | holds (`timely`, `flakyTip`, `staleLagWithSlack`) | argued, not checked | argued, not checked: admission never judges below the recorded boundary, whatever the tip |
+| A3 | holds | argued, not checked: draining is an admission rule | holds |
+
+- A hub folds several indexer endpoints into one answer: the tip is the maximum of the answers the tip guard keeps (`batcher.rs:245-282`, `chain.rs:176-208` at #92), a lookup takes the first "found", a broadcast takes the best verdict. So one misbehaving endpoint can raise the tip (on mainnet, only inside the guard's band and climb rate), 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 and G9 depend on the shim alone.
+- The hub specification has no Byzantine hub, so the hub column of G6b and A3 is an argument. 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`). The protocol specification's Byzantine hub backs the other rows.
+
+## 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. "Where" names a [configuration][configurations].
+
+| 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`). An observer can make every refusal in one flush window `Full` at no cost (finding 13) | `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`, `observerResubmitsPublishedTest`, `flushWindowTest`, `rejectedAtFlushTest` |
+| K3' | T5 | G6b when the expiry floor leaves no slack for the reorg allowance | Found here (finding 3); not triaged | `flakyTipNoSlack` | TLC, violated | `conformingMissesMarginWithoutSlackTest` |
+| K4 | T5 | G6b on the shipped relation between the constants, across a tip silence shorter than the staleness window | Found here (finding 1); accepted: one block of margin in a narrow environment, and each fix costs more | `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:382-392`, `:513-524`). 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` |
+| K9 | T5 | G6b 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). #85 fixed admission's half (G8); the spent epoch remains, and this counterexample is unchanged | `staleLagWithSlack` | TLC, violated | `earlyFlushSpendsTheNextEpochTest` |
+| K10 | T19 | G9 for a spend that carries a shielded bundle. A wallet deshields Orchard to its own address, then auto-shields that output into Ironwood: the second transaction forwards, and its prevout names the diverted first | By design in #94: catching it needs a record of what was diverted, and the shim keeps none (`zeronym/shim/ENDPOINTS.md:208-214` at #94) | `shieldedSpend` | simulation, violated | `shieldedSpendOfDivertedIsForwardedTest` |
+
+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.** An observer 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 | `observerLearnsItIsQueuedTest`; witness `wQueuedDisclosed` on `baseline` |
+| **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. A report far ahead of the chain is finding 11, which #92 bounds on mainnet | 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` |
+
+## Findings
+
+> Where the model disagrees with what the code or its comments assume.
+
+Findings 6 and 8 are fixed by #85, and finding 2 in part. Finding 11 is fixed by #92, and finding 12 by #94. Finding 10 is fixed in part by #104 and #106, and finding 13 by #100 and #104. Nothing else 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`, `:233-237`, `:274-287`. 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), partly fixed by #85; 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:276-287`, `:355-374`. 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 (flush interval, mining margin, delivery lag) 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 | Not a checked property: the corollary of G6b under [Guarantees][guarantees] assumes it away | 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:382-392`, `:513-524`) and unit-tested (`queue.rs`, `a_requeue_gives_up_on_an_entry_that_can_no_longer_be_mined`); the rule is `queue.rs:509-522`. 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.** Before #85 admission counted on the flush at that boundary, which will not happen again. Any late arrival met it, and one that expired before that next flush was first offered after its expiry; the supported-wallet case was a resend after a crash, which a restarted hub offered with less than the mining margin. Since #85 admission counts on the next unspent flush, and that resend is refused | Code bug (MEDIUM), fixed by #85; one root cause with finding 2 | G8 on `flakyTip`; `crashThenLateDuplicateTest` | Code read before #85, at `ee910d6`: `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 observed tip, 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:463-468`; `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), fixed by #85: an ambiguous wire reply, and no check on an indexer's answer | `sentinelCollisionTest`, `indexerEmptyAnswerIsUnavailableTest` | Code read before #85, at `ee910d6`: `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), fixed in part by #104 and #106: a copy of an Orchard transaction a node rejected or mined is refused `SpentProof`. The comment on `Hub::lookup` calls a resubmit harmless. The batch-size figure is logged and returned but drives no decision | K2, `observerResubmitsPublishedTest`, `walletResendsPublishedTest`; the refusal in `admissionDecisionTableTest` | Code read: `queue.rs:310-312`, `:360-361`; `Hub::lookup` in `server.rs`; `batcher.rs:397`, `:434`, `:526`. Not checked: that a node answers already-known for a transaction that is already mined |
+| 11 | **One high tip report pinned the hub's tip.** Before #92, `observe` adopted any higher height and ignored a later drop larger than the reorg allowance. So one endpoint reporting a height P made every real height look like an oversized regression until the chain reached P minus the allowance, which for a large P is until restart. The epoch jumped, so the hub flushed once off cadence; after that admission refused every expiring transaction, because the observed height was P. The same rule could freeze the cadence: every step up refreshed liveness, so a tip that oscillated inside the allowance never went stale. #92 judges each answer before the maximum: on mainnet it drops a height outside a band around a compiled anchor, which also refuses a height near `u32::MAX`, and a new high faster than the chain can climb. Only a new high refreshes liveness, reorg depth is measured from the best height seen, and the free-running clock starts from that height | Code bug (HIGH), fixed by #92. On mainnet the guard bounds the lie: inside the band and rate one endpoint can still shift flush timing, hold a lead of about 16 blocks, or choose the boot height. Testnet and regtest are unguarded | `observeTip` follows #92: `tipRuleTest`, `staleCadenceTest`, `tipNearBestTest`. The Byzantine indexer still reports any tip in a bounded range, which over-approximates the guard. The freeze was invisible to the model before #92: staleness here is counted from the chain height alone, and the one configuration that goes stale reports the true height, which only climbs. `tipAheadOfChainFlushesEarlyTest` shows the one early flush | Code read at #92: `batcher.rs:19-45`, `:164-202`, `:240-349`, `:416-431`; `tip_guard.rs:40-65`; `chain.rs:176-208`. Before #92, at `2bae0a6`: `batcher.rs:19-22`, `:177-209`, `:355-374`; `chain.rs:176-201` |
+| 12 | **The second leg of a TEX payment named a diverted transaction.** A ZIP 320 (TEX) payment from shielded funds is two transactions, and the second spends the first's single-use transparent output. When the first touched Orchard, the shim diverted it. The second has transparent parts only, so the shim forwarded it, and its one prevout handed the operator the txid the hub held, on the wallet's connection. An external report found it; this specification missed it. A payload carried a class label and nothing about its inputs, so G1 held by construction and every property read one send at a time. A payload now carries the txids it spends and its pool shape, the shim applies #94's rule to them, and G9 states the link | Code bug (privacy), fixed by #94. The severity scale grades batching and availability harms, so this row is ungraded | G9, `texSecondLegIsDivertedTest`; K10 for what #94 leaves. A one-off mutation run with the transparent-only arm removed: the `baseline` simulation violates G9, and `texSecondLegIsDivertedTest` fails at its second send | Code read at #94: `classify.rs:274-295`, `:333-338` |
+| 13 | **A free burst of junk shuts admission for a flush window, and before #100 for nine.** Unparseable bytes are admitted with no expiry, and 1,024 entries fill the cap, so 64 KiB of junk refuses every later submission `Full` until the next flush. Forged parseable bytes fill it as well, because the node is the only judge of validity. Over the mixnet each refusal is K1: the wallet was already told ok, and the SDK keeps a ZIP 318 migration's notes locked until its expiry, 30 to 60 days out. Before #100 a node's parse-failure answer (`-22`) came back retryable through lightwalletd and zaino both, so the flush requeued every junk entry up to the attempt bound: one burst held the cap for 8 more flushes and reached every indexer 9 times. An external report found it; this specification could not, since it has no capacity and its observer submits only what it has learned | Code bug (HIGH), fixed in part by #100 and #104: the requeue loop is gone, and an Orchard entry costs a proof in a lane of its own. The free lanes remain, documented in the hub's `OPERATORS.md` (#102) | Not modelled: capacity and payloads of the observer's own making, under [Not modelled][not-modelled]. Rust tests in #100: `tests/junk_flood.rs` fails on `main` with every junk entry held | Code read at #100: `queue.rs:83`, `:283-291`, `:324`; `chain.rs`, `classify_send_response` and `classify_publish_failure`. zaino's relay: `zaino-source-zebra-rpc/src/adapter.rs`, `submission_rejection` |
+
+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 rely on 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 and K10 are 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, whose guard is that configuration's assumptions. A false guard leaves no initial state, and the gate fails.
+
+#### Protocol specification
+
+At most 3 sends and 3 lookups by the wallet, 3 requests by the observer. The `baseline` transactions are three Orchard migrations (one with an expiry below the supported floor), bytes nobody can parse, a Sapling payment, and the second leg of a TEX payment that one migration starts.
+
+| Configuration | Hub | Indexer | Transactions |
+|---|---|---|---|
+| `baseline` | honest | honest | |
+| `byzHub` | **Byzantine** | honest | |
+| `byzIndexer` | honest | **Byzantine** | |
+| `shieldedSpend` | honest | honest | and an auto-shield of a migration's output into Ironwood: K10 |
+
+#### 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, K5 |
+| `flakyTip` | the tip may be reported up to the reorg allowance behind | G6b under regression; G8, finding 6 |
+| `flakyTipNoSlack` | and the expiry floor is 6, leaving no reorg slack | K3' |
+| `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 |
+| `byzIndexer` | a Byzantine indexer, 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. Under `staleLag` a hub is stale once it has seen no new high 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 | holds, 22 947 states, depth 40 |
+| `timely` | K6's predicate | holds, 22 947 states, depth 40 |
+| `flakyTip` | G6b | holds, 117 501 states, depth 36 |
+| `timely`; `flakyTip`; `staleLagWithSlack` | G8 | holds: 22 947; 117 501; 895 083 states |
+| `flakyTipNoSlack` | G6b (K3') | violated, 12 states |
+| `staleLag` | G6b; K6 | violated, 13; 13 states |
+| `staleLagWithSlack` | G6b (finding 2) | violated, 19 states |
+| `timely` | K5 | violated: 5 states; 8 without a crash; 12 without a shutdown either |
+| `byzIndexer` | G6b | violated, 16 states |
+
+`flakyTip` had 81 518 states before the tip rule followed #92. The hub's best height is now part of its state, so a tip one below the best and the same tip as the best are distinct states. Every verdict and counterexample length stayed the same.
+
+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 antecedent of G6b, 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`), 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 with their pool shape and parents, 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)`: the classifier, 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.** Findings 2, 6 and 8 have Rust tests, written with their fixes in #85; the part of finding 2 that #85 leaves has none. The other findings are shown on the model and matched to the code by reading. Finding 1 fits `batcher.rs`'s unit tests as 2 and 6 did. 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 each function maps onto one seam in the Rust code.
+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.
+4. **A Byzantine and a leaky shim.** Privacy properties are __hyperproperties__ and Quint doesn't support them (see the [discussion on the Quint Telegram channel][quint-tg]).
+
+[protocol-spec]: ./protocol.qnt
+[hub-spec]: ./hubMachine.qnt
+[quint]: https://quint-lang.org
+[system]: #system
+[assumptions]: #assumptions
+[out-of-scope]: #out-of-scope
+[threat-model]: #threat-model
+[guarantees]: #guarantees
+[trust-matrix]: #trust-matrix
+[known-gaps]: #known-gaps
+[findings]: #findings
+[how-it-is-checked]: #how-it-is-checked
+[future-work]: #future-work
+[zeronym-readme]: ../../README.md
+[configurations]: #configurations
+[wallet-threat-model]: https://zcash.readthedocs.io/en/latest/rtd_pages/wallet_threat_model.html
+[not-modelled]: #not-modelled
+[quint-tg]: https://t.me/quint_lang/1311
diff --git a/zeronym/spec/quint/abstractHub.qnt b/zeronym/spec/quint/abstractHub.qnt
new file mode 100644
index 00000000..3bac7c38
--- /dev/null
+++ b/zeronym/spec/quint/abstractHub.qnt
@@ -0,0 +1,81 @@
+// -*- 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, with every queued entry of its txid; 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 settleWithCopy(h: AHub, payload: Payload): AHub = {
+ queue: h.queue.filter(other => not(sharesTxid(payload, other))),
+ 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) or after == h.settleWithCopy(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..28374cc0
--- /dev/null
+++ b/zeronym/spec/quint/check.sh
@@ -0,0 +1,415 @@
+#!/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" rows are K2 and
+# K10, known gaps; they show 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 one with a nonzero
+# status failed; either 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))
+ elif [ "$(cat "$file.status")" != 0 ]; then
+ echo "FAIL row $(basename "$file"): exited $(cat "$file.status")"
+ 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:25 tests/shimTest.qnt:14
+ tests/hubScenariosTest.qnt:25 tests/scenariosTest.qnt:22 tests/trustTest.qnt:14"
+
+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 ;;
+ shieldedSpend) init=initShieldedSpend ;;
+ *) 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 pendingOnlyFromQueue forwardedSpendsNoDiverted
+job holds byzHub operatorBlind txidAuthenticity forwardedSpendsNoDiverted
+job holds byzIndexer operatorBlind txidAuthenticity pendingOnlyFromQueue forwardedSpendsNoDiverted
+
+# The known gaps, with every component honest.
+job fails baseline quietStep 40 statusNeverRegresses # K2
+job fails shieldedSpend quietStep 40 forwardedSpendsNoDiverted # K10
+
+finish
+
+echo "---- 3b witnesses ($SAMPLES traces, seed $SEED)"
+
+BASELINE_HOLDS="operatorBlind queuedBytesConfidential txidAuthenticity lookupValidityPerHub pendingOnlyFromQueue forwardedSpendsNoDiverted"
+
+# The accepted disclosure, an observer served a published body, and the
+# antecedents of G1, G2 and G9. The served body is G2's reply-body branch, which
+# `vQueuedBytesConfidential` does not reach on its own.
+job reaches baseline step 40 \
+ wQueuedDisclosed wObserverServedBody \
+ vOperatorBlind vQueuedBytesConfidential vForwardedSpendsNoDiverted \
+ -- $BASELINE_HOLDS
+# G3's antecedent, and the wallet observations a quiet run reaches: pending,
+# served from the mempool, served from a block, and an unparseable payload
+# missed while it is still queued.
+job reaches baseline quietStep 80 \
+ wPending wTxInMempool wTxMined wUnparseableMissed \
+ vTxidAuthenticity \
+ -- $BASELINE_HOLDS
+# G4's antecedent, under a step that keeps to one migration.
+job reaches baseline earlyLookupStep 40 \
+ vLookupValidityPerHub \
+ -- $BASELINE_HOLDS
+
+job reaches byzHub quietStep 40 \
+ vOperatorBlind vTxidAuthenticity vForwardedSpendsNoDiverted \
+ -- operatorBlind txidAuthenticity forwardedSpendsNoDiverted
+job reaches byzIndexer quietStep 40 \
+ vOperatorBlind vTxidAuthenticity vForwardedSpendsNoDiverted \
+ -- operatorBlind txidAuthenticity pendingOnlyFromQueue forwardedSpendsNoDiverted
+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
+K5=ackedIsHeldOrSettled
+K6=conformingEveryOfferBeforeExpiry
+G8=admissionMatchesCadence
+
+# The schedule guarantee with every component honest: under a timely tip, and
+# under a tip that may be reported behind the chain.
+job tlc_holds initTimely step $G6B
+job tlc_holds initTimely step $K6
+job tlc_holds initFlakyTip step $G6B
+job tlc_holds initTimely step $G8
+job tlc_holds initFlakyTip step $G8 # finding 6, fixed by #85
+job tlc_holds initStaleLagWithSlack step $G8 # finding 2's admission half, fixed by #85
+
+# 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 initStaleLag step $G6B 13 # K4
+job tlc_violated initStaleLag step $K6 13 # K6
+job tlc_violated initStaleLagWithSlack step $G6B 19 # finding 2's spent epoch, not fixed by #85
+# 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: the schedule guarantee is violated once the indexer is
+# Byzantine.
+job tlc_violated initByzIndexer step $G6B 16
+
+# Reachability. The antecedent of G6b, 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(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(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 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..ef443866
--- /dev/null
+++ b/zeronym/spec/quint/hub.qnt
@@ -0,0 +1,473 @@
+// -*- 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.
+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 new high 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 the best height seen, on an
+ /// estimate of elapsed time.
+ /// Admission and requeue never read it directly: requeue reads the observed
+ /// tip, admission `admissionHeight`.
+ 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.
+ /// - `best`: the highest tip observed, 0 until the first observation. Only
+ /// a tip above it is progress, and a tip is judged against it.
+ /// - `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. A
+ /// flush records it when it begins.
+ /// - `burned`: the txids whose proofs this hub published to a rejection or a
+ /// mined verdict. Admission refuses a payload carrying one, and the burn
+ /// drops every queued entry carrying it. It lives in memory, like the
+ /// queue. The code keys this on bundle keys; the txid is what a re-signing
+ /// keeps.
+ type HubState = {
+ params: HubParams,
+ phase: Phase,
+ tip: Option[Height],
+ best: Height,
+ cadence: Cadence,
+ queue: Payload -> int,
+ flush: Flush,
+ lastEpoch: Option[int],
+ burned: Set[TxId],
+ }
+
+ /// 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,
+ best: 0,
+ cadence: Tracking,
+ queue: Map(),
+ flush: Idle,
+ lastEpoch: None,
+ burned: Set(),
+ }
+
+ /// 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 =
+ // A submission, together with whether every indexer's current nullifier
+ // view reports its Orchard nullifiers mined (`ChainNullifiers::any_revealed`).
+ | SubmitHInput({ nonce: Nonce, payload: Payload, revealed: bool })
+ // A lookup, together with what the hub's indexer would answer, as its
+ // client returns it (`hubReads`). 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 new high 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 is unreliable: 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()
+
+ /// Whether `payload`'s txid is in `burned`. A payload with no txid is not.
+ pure def isBurned(burned: Set[TxId], payload: Payload): bool =
+ match payload.txid {
+ | Some(txid) => burned.contains(txid)
+ | None => false
+ }
+
+ /// The queue without every entry that carries `txid`.
+ pure def dropTxid(entries: Payload -> int, txid: TxId): Payload -> int =
+ entries.keys().filter(payload => payload.txid != Some(txid)).mapBy(payload => entries.get(payload))
+
+ /// 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
+
+ /// The height admission judges expiry at: the observed tip, or the boundary
+ /// of the last flush epoch if that is higher, because the flush at that
+ /// boundary is spent (`TipTracker::admission_height`).
+ pure def admissionHeight(state: HubState): Height =
+ match state.lastEpoch {
+ | Some(epoch) =>
+ val boundary = epoch * state.params.flushInterval
+ if (boundary > state.observedTip()) boundary else state.observedTip()
+ | None => state.observedTip()
+ }
+
+ /// 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.
+ /// `revealed` is the nullifier views' answer, which the hub reads on its own
+ /// clock. No check asks a node anything: admission must not leak a
+ /// transaction's arrival.
+ pure def admission(state: HubState, payload: Payload, revealed: bool): AckKind =
+ if (state.isTipStale())
+ Refused(TipStale)
+ else if (state.phase == Draining)
+ Refused(HubDraining)
+ else if (not(survivesNextFlush(payload.expiry, state.admissionHeight(), state.params.flushInterval, state.params.miningMargin)))
+ Refused(ExpiryTooTight)
+ else if (revealed and hasProof(payload))
+ Refused(SpentProof)
+ else if (state.queued().contains(payload))
+ Duplicate
+ else if (isBurned(state.burned, payload))
+ Refused(SpentProof)
+ else
+ Admitted
+
+ // ------------------------------------------------------------------------
+ // Tip
+ // ------------------------------------------------------------------------
+
+ /// The cadence loop observes `height`. The first observation is adopted as
+ /// the best height, with its epoch, and nothing is flushed. After that only
+ /// a new high, above the best, is progress: it is followed, becomes the best
+ /// and ends staleness. A height within the reorg allowance below the best is
+ /// followed and leaves the phase and the cadence alone, so a tip that dips
+ /// and climbs back is not progress. A height further below the best is
+ /// ignored, so a reorg cannot be walked down one allowance at a time.
+ pure def observeTip(state: HubState, height: Height): HubResult =
+ match state.tip {
+ | None =>
+ if (state.phase == Starting)
+ { ...state,
+ phase: Running,
+ tip: Some(height),
+ best: height,
+ lastEpoch: Some(height / state.params.flushInterval),
+ }.toNoHubOutput()
+ else state.toHubErrorOutput("no cadence loop is running")
+ | Some(_) =>
+ 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 > state.best)
+ { ...state, phase: Running, tip: Some(height), best: height, cadence: Tracking }.toNoHubOutput()
+ else if (state.best - height <= state.params.reorgAllowance)
+ { ...state, tip: Some(height) }.toNoHubOutput()
+ else
+ state.toNoHubOutput()
+ }
+
+ /// The staleness window passes with no new high, or passes further: the
+ /// cadence clock free-runs and now reads `height`. The estimate starts at or
+ /// above the best height, where the implementation's clock starts, 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.best)
+ { ...state, phase: Stale, cadence: FreeRunning(height) }.toNoHubOutput()
+ else state.toHubErrorOutput("not a running hub, or an estimate below the best height")
+ | 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. The epoch is recorded here, before the batch goes
+ /// out. 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 }),
+ lastEpoch: if (state.phase == Draining) state.lastEpoch else Some(state.cadenceEpoch()),
+ }.toBroadcastOutput(state.queued())
+
+ /// The indexer's verdict on one entry. Accepted, already-known and mined
+ /// entries are published and leave; a rejected entry is dropped; a retryable
+ /// one is set aside for requeue. A rejected or mined entry's proofs are
+ /// burned, and every queued entry with its txid is dropped with them
+ /// (`Queue::burn`).
+ 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)
+ val burns = (verdict == Rejected or verdict == AlreadyMined) and hasProof(payload)
+ val base =
+ if (burns)
+ match payload.txid {
+ | Some(txid) =>
+ { ...state,
+ queue: dropTxid(state.queue, txid),
+ burned: state.burned.union(Set(txid)),
+ }
+ | None => state
+ }
+ else state
+ { ...base,
+ 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. So is one whose
+ /// txid was burned.
+ /// - An entry that no longer survives the next flush, judged at the observed
+ /// tip, is dropped as expired. Admission judges at `admissionHeight`,
+ /// which can be higher; requeue does not, so as not to drop an
+ /// acknowledged entry that may still be mined.
+ /// - 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()).filter(payload =>
+ not(isBurned(state.burned, payload)))
+ 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 }
+ 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, submit.revealed)
+ // 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")
+ }
+}
diff --git a/zeronym/spec/quint/hubMachine.qnt b/zeronym/spec/quint/hubMachine.qnt
new file mode 100644
index 00000000..bee873ee
--- /dev/null
+++ b/zeronym/spec/quint/hubMachine.qnt
@@ -0,0 +1,714 @@
+// -*- 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 with its mining margin to spare. 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 the properties need. 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 audit record 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 new high 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,
+ 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
+
+ /// 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 they give.
+ pure def shippedAssumptions(c: HubConfig): bool = and {
+ standingAssumptions(c),
+ shippedRelationsKept(c),
+ reorgSlackFits(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 audit record.
+
+ /// 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:336`).
+ 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()
+
+ /// How far the chain is past the best height the hub has seen. Staleness is
+ /// counted on this, as the implementation times it from the last new high.
+ /// Under `TipMayLag` every report is the true height, so it equals `lag`.
+ def silence: int = height - h.best
+
+ /// 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, AlreadyMined, 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)
+
+ /// What the hub's nullifier views may report for `payload` now.
+ def revealedOn(payload: Payload): Set[bool] =
+ match cfg.indexerRole {
+ | Honest => honestRevealed(chain, payload)
+ | Byzantine => byzRevealed
+ }
+
+ /// The transitions the hub may take on a submission of `payload`.
+ def submitResults(payload: Payload): Set[HubResult] =
+ revealedOn(payload).map(revealed => hub(h, SubmitHInput({ nonce: 0, payload: payload, revealed: revealed })))
+
+ // ------------------------------------------------------------------------
+ // 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 new high 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 silence >= 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 that has gone the staleness window without a new
+ /// high 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 silence < 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.
+ //
+ // 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.
+
+ /// 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 (finding 6).
+ 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))
+
+ /// G8. Every entry the hub has admitted, and not requeued, survives the
+ /// first flush the cadence has not spent, with the mining margin to spare:
+ /// admission's "provably survives". A requeued entry is judged at the
+ /// observed tip on purpose, so it is not covered.
+ val admissionMatchesCadence =
+ match h.lastEpoch {
+ | Some(epoch) =>
+ h.queued().forall(payload =>
+ h.queue.get(payload) == 0 implies
+ survivesNextFlush(payload.expiry, epoch * cfg.params.flushInterval,
+ cfg.params.flushInterval, cfg.params.miningMargin))
+ | 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 is the antecedent of G6b: without
+ // it 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))
+
+ /// 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, spends: Set(), 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,
+ 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),
+ }
+
+ // 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)),
+ }
+
+ // A Byzantine indexer, on the schedule of `timely`, with one supported
+ // migration and `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, spends: Set(), 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),
+ not(reorgSlackFits(flakyTipNoSlack)),
+ initWith(flakyTipNoSlack),
+ }
+ action initStaleLag = all { shippedAssumptions(staleLag), initWith(staleLag) }
+ action initByzIndexer = all { shippedAssumptions(byzIndexer), initWith(byzIndexer) }
+ action initUnknownUpgrade = all { shippedAssumptions(unknownUpgrade), initWith(unknownUpgrade) }
+ action initStaleLagWithSlack = all {
+ standingAssumptions(staleLagWithSlack),
+ reorgSlackFits(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..53fdd6ec
--- /dev/null
+++ b/zeronym/spec/quint/indexer.qnt
@@ -0,0 +1,234 @@
+// -*- 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 the chain has a transaction with `payload`'s txid in a block.
+ pure def isMined(state: IndexerState, payload: Payload): bool =
+ match payload.txid {
+ | Some(txid) => state.inclusion(txid) == Mined
+ | None => false
+ }
+
+ /// What the hub's nullifier views may report for `payload`: mined only if
+ /// it is, and nothing while a view is not current.
+ pure def honestRevealed(state: IndexerState, payload: Payload): Set[bool] =
+ Set(false).union(if (state.isMined(payload)) Set(true) else Set())
+
+ /// 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; `AlreadyMined` only for one in a block.
+ /// - 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())
+ .union(if (state.isMined(payload)) Set(AlreadyMined) 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, AlreadyMined, 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 })
+ }
+
+ /// What a Byzantine indexer's nullifier view may report: anything.
+ pure val byzRevealed: Set[bool] = Set(false, true)
+
+ /// 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..fb5ac42a
--- /dev/null
+++ b/zeronym/spec/quint/protocol.qnt
@@ -0,0 +1,1179 @@
+// -*- 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 an
+/// observer 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.
+/// - Observer. 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, spends: Set(), oversize: false }
+
+ /// Two migrations from supported wallets, built at heights 2 and 4. Each
+ /// pays a single-use transparent output: `early` is the first leg of a TEX
+ /// payment, and `late` deshields to the wallet's own address.
+ 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, spends: Set(), oversize: false }
+ /// A Sapling payment with no transparent inputs. The shim forwards it.
+ pure val plain: Payload =
+ { id: "plain", txid: Some("plain"), created: 1, expiry: Some(9), class: OtherShielded, spends: Set(), oversize: false }
+ /// The second leg of the TEX payment `early` starts: transparent parts only,
+ /// and its one prevout is `early`'s single-use output. The shim diverts it
+ /// by its shape (#94).
+ pure val tex: Payload =
+ { id: "tex", txid: Some("tex"), created: 2, expiry: Some(9), class: TransparentOnly, spends: Set("early"), oversize: false }
+ /// An auto-shield of `late`'s output into Ironwood: a transparent spend
+ /// with a shielded bundle. The shim forwards it, and its prevout names
+ /// `late` (K10).
+ pure val autoShield: Payload =
+ { id: "autoShield", txid: Some("autoShield"), created: 4, expiry: Some(11), class: OtherShielded, spends: Set("late"), oversize: false }
+
+ // ------------------------------------------------------------------------
+ // 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, tex),
+ 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 baseline, and a shielded spend of a diverted transaction's output:
+ /// the residual #94 leaves (K10).
+ pure val shieldedSpend = { ...baseline, payloads: baseline.payloads.union(Set(autoShield)) }
+
+ // ========================================================================
+ // 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 observer: 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 Observer = { 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],
+ observer: Observer,
+ }
+
+ /// 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(),
+ observer: { txids: Set(), nextNonce: 0, requests: 0 },
+ }
+
+ /// The audit record: what the checker records of the run. 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 observer knows: those it learned out of band
+ /// and everything the chain has made public.
+ pure def tpTxids(s: System): Set[TxId] =
+ s.observer.txids.union(s.indexer.txs.keys())
+
+ /// The payloads the observer 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 observer sees. 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(ObserverAddr).union(s.operator)
+
+ /// Every payload the observer 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
+ })
+
+ /// The payloads the shim has diverted: the bodies of its submissions to the
+ /// hub. The network keeps every frame, so this set only grows.
+ pure def diverted(s: System): Set[Payload] =
+ s.toHub(ShimAddr).filterMap(msg => match msg { | Submit(submit) => Some(submit.payload) | _ => 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 observer sends `msg` to the hub, under a nonce of its own.
+ pure def observerSent(s: System, msg: Msg): System =
+ { ...s,
+ observer: { ...s.observer,
+ nextNonce: s.observer.nextNonce + 1,
+ requests: s.observer.requests + 1,
+ },
+ }.posted(Set({ src: ObserverAddr, 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 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
+ /// transaction `treatAsMigration` passes, a Sprout, Sapling or Ironwood
+ /// transaction or a coinbase.
+ pure def operatorBlindIn(s: System): bool =
+ s.operator.forall(payload => not(treatAsMigration(payload)))
+
+ /// G2. A transaction's bytes do not reach an observer before the chain has
+ /// published them. Everything the observer has learned is on the chain,
+ /// or was a transaction the classifier passes and 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 not(treatAsMigration(payload)),
+ })
+
+ /// 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
+ })
+
+ /// G5. Every "pending" the wallet is told was true at the hub that gave
+ /// it: the transaction was queued there at some point between the request
+ /// and the answer. G4 restricted to pending; unlike G4 it survives a
+ /// Byzantine indexer, whose empty "found" the hub reads as a failure.
+ pure def pendingOnlyFromQueueIn(s: System, audit: Audit): bool =
+ s.events().forall(event =>
+ match event {
+ | Got(got) =>
+ got.obs != Pending or
+ match got.via {
+ | Some(nonce) => audit.windows.keys().contains(nonce) and audit.windows.get(nonce).contains(Pending)
+ | None => false
+ }
+ | _ => true
+ })
+
+ /// G9. The operator is handed no transaction that spends an output of one
+ /// the shim diverted. Such a transaction names the diverted txid in its
+ /// prevout, and the operator sees it arrive on the wallet's connection.
+ /// The parent may be diverted before or after the child is forwarded, and
+ /// may be published already: each order links the wallet to the parent.
+ ///
+ /// It holds while every transaction that spends a diverted one has
+ /// transparent parts only. A spend with a shielded bundle forwards (K10).
+ pure def forwardedSpendsNoDivertedIn(s: System): bool =
+ val hidden = txidsOf(s.diverted())
+ s.operator.forall(payload => payload.spends.intersect(hidden) == Set())
+
+ // ------------------------------------------------------------------------
+ // 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: an observer 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(ObserverAddr), s.replies(ObserverAddr)).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
+ })
+
+ /// An observer 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 wObserverServedBodyIn(s: System): bool =
+ s.repliedBodies(ObserverAddr) != Set()
+
+ // ------------------------------------------------------------------------
+ // 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 wallet has handed the shim a transaction that spends one the shim
+ /// diverted.
+ pure def vForwardedSpendsNoDivertedIn(s: System): bool =
+ val hidden = txidsOf(s.diverted())
+ s.sentByWallet().exists(payload => payload.spends.intersect(hidden) != Set())
+
+ // ========================================================================
+ // 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
+ /// The bound of the model: the wallet makes at most `MAX_REQUESTS` sends
+ /// and as many lookups, as does the observer.
+ def MAX_REQUESTS = cfg.maxRequests
+
+ def ROLES = cfg.roles
+
+ /// 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(PAYLOADS)
+
+ /// The standing assumption, checked by every named init: payloads are told
+ /// apart by their bytes.
+ pure def payloadsWellFormed(c: Config): bool =
+ c.payloads.size() == c.payloads.map(payload => payload.id).size()
+
+ /// Checked by the Byzantine inits: two payloads have different txids, so a
+ /// lie can be a transaction other than the one asked for.
+ pure def aForeignTransactionExists(c: Config): bool =
+ tuples(c.payloads, c.payloads).exists(((one, other)) =>
+ one.txid != None and other.txid != None and one.txid != other.txid)
+
+ // ------------------------------------------------------------------------
+ // State
+ // ------------------------------------------------------------------------
+
+ /// The protocol state.
+ var s: System
+ /// The audit 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), aForeignTransactionExists(byzHub), initWith(byzHub) }
+ action initByzIndexer = all { payloadsWellFormed(byzIndexer), aForeignTransactionExists(byzIndexer), initWith(byzIndexer) }
+ action initShieldedSpend = all { payloadsWellFormed(shieldedSpend), initWith(shieldedSpend) }
+
+ // ------------------------------------------------------------------------
+ // Roles
+ // ------------------------------------------------------------------------
+
+ def hubAnswers(h: AHub, request: ARequest): Set[AAnswer] =
+ match ROLES.hub {
+ | Honest => honestAnswers(h, request)
+ | Byzantine => byzantineAnswers(h, request, PAYLOADS)
+ }
+
+ def indexerResults(state: IndexerState, input: IndexerInput): Set[IndexerResult] =
+ match ROLES.indexer {
+ | Honest => heightlessIndexerResults(state, input)
+ | Byzantine => byzIndexerResults(state, input, PAYLOADS)
+ }
+
+ /// 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, hubReads(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, once the last flush has
+ /// ended, as the real hub's `flush == Idle` requires. A Byzantine hub keeps
+ /// the schedule, so these steps are the same whatever its role.
+ action hubTake = all {
+ s.hub.held == Set(),
+ 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. A rejected or mined verdict burns its proofs, and
+ /// every queued entry with its txid goes with them.
+ 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 verdict = verdictIn(result.out)
+ val burns = (verdict == Rejected or verdict == AlreadyMined) and hasProof(payload)
+ val hub =
+ if (verdict == Retryable) s.hub
+ else if (burns) s.hub.settleWithCopy(payload)
+ 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)
+ },
+ }
+
+ // ------------------------------------------------------------------------
+ // Observer
+ // ------------------------------------------------------------------------
+
+ /// The txids of wallet transactions the observer has yet to learn.
+ def unknownTxids: Set[TxId] =
+ txidsOf(PAYLOADS).exclude(s.tpTxids())
+
+ /// The observer learns a txid out of band, before the transaction is
+ /// published. An operator can recover one from a wallet's transparent-pool
+ /// queries.
+ action observerLearnsTxidWith(txid: TxId): bool = all {
+ unknownTxids.contains(txid),
+ commit({ ...s, observer: { ...s.observer, txids: s.observer.txids.union(Set(txid)) } }),
+ }
+
+ action observerLearnsTxid = all {
+ unknownTxids != Set(),
+ {
+ nondet txid = oneOf(unknownTxids)
+ observerLearnsTxidWith(txid)
+ },
+ }
+
+ /// The observer asks the hub about a txid it knows. The lookup is not
+ /// authenticated.
+ action observerLookupWith(txid: TxId): bool = all {
+ s.observer.requests < MAX_REQUESTS,
+ s.tpTxids().contains(txid),
+ commit(s.observerSent(Lookup({ nonce: s.observer.nextNonce, txid: txid }))),
+ }
+
+ action observerLookup = all {
+ s.observer.requests < MAX_REQUESTS,
+ s.tpTxids() != Set(),
+ {
+ nondet txid = oneOf(s.tpTxids())
+ observerLookupWith(txid)
+ },
+ }
+
+ /// The observer submits a payload it has learned or the chain has
+ /// published. Submission is not authenticated either.
+ action observerSubmitWith(payload: Payload): bool = all {
+ s.observer.requests < MAX_REQUESTS,
+ s.tpPayloads().contains(payload),
+ commit(s.observerSent(Submit({ nonce: s.observer.nextNonce, payload: payload }))),
+ }
+
+ action observerSubmit = all {
+ s.observer.requests < MAX_REQUESTS,
+ s.tpPayloads() != Set(),
+ {
+ nondet payload = oneOf(s.tpPayloads())
+ observerSubmitWith(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 observer.
+ action outsiderStep = any {
+ observerLearnsTxid, observerLookup, observerSubmit,
+ }
+
+ /// 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)
+ val pendingOnlyFromQueue = pendingOnlyFromQueueIn(s, audit)
+ val forwardedSpendsNoDiverted = forwardedSpendsNoDivertedIn(s)
+
+ // ------------------------------------------------------------------------
+ // 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 wObserverServedBody = wObserverServedBodyIn(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)
+ val vForwardedSpendsNoDiverted = vForwardedSpendsNoDivertedIn(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 observer instead.
+ pure def fromObserver(mail: Mail): Mail =
+ { ...mail, src: ObserverAddr }
+
+ /// 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(hubReads(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..81dee7e1
--- /dev/null
+++ b/zeronym/spec/quint/shim.qnt
@@ -0,0 +1,195 @@
+// -*- 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 is diverted (`classify`, `shim/src/classify.rs`
+ /// at #94). Two arms divert:
+ ///
+ /// - It touches Orchard.
+ /// - It spends a transparent output and has transparent parts only. The
+ /// second leg of a ZIP 320 (TEX) payment has this shape, and its one
+ /// prevout names the first leg. The shim keeps no record of what it
+ /// diverted, so the arm reads the shape alone.
+ ///
+ /// A body the shim cannot parse is treated as a migration: forwarding it is
+ /// the one outcome the shim exists to prevent. Everything else forwards: a
+ /// Sprout, Sapling or Ironwood bundle, with or without transparent parts,
+ /// and a coinbase.
+ pure def treatAsMigration(payload: Payload): bool =
+ match payload.class {
+ | OrchardTouching => true
+ | Unparseable => true
+ | TransparentOnly => payload.spends != Set()
+ | OtherShielded => false
+ }
+
+ 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 transaction that
+ /// `treatAsMigration` passes 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))) 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..9e833c7e
--- /dev/null
+++ b/zeronym/spec/quint/tests/hubScenariosTest.qnt
@@ -0,0 +1,482 @@
+// -*- 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, revealed: false }))
+
+ /// The decision an honest hub would give `payload` now.
+ def decision(payload: Payload): AckKind =
+ admission(h, payload, false)
+
+ /// 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))
+
+ 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(initStaleLag)
+ .then(initStaleLagWithSlack)
+ .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 wBlockInFlight)
+ .then(judge(early, Accepted))
+ .then(flushEnd)
+ .expect(onChain == Set(early) and offered == Set(early) and owed == Set() and flightStart == 0)
+ .expect(conformingFirstOfferBeforeExpiry)
+ .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 holds
+ /// on `flakyTip` in every reachable state.
+ run conformingMissesMarginWithoutSlackTest =
+ regressedTipDelaysFlush(flakyTipNoSlack, orchard("early", 2, 8))
+ .expect(not(reorgSlackFits(cfg)))
+ .expect(not(conformingFirstOfferBeforeExpiry))
+
+ /// 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. Admission judges
+ /// at the recorded boundary 6, not 5: the next flush is at 9, which an
+ /// expiry of 9 does not survive, so the duplicate is refused. At 8 nothing
+ /// is waiting to be offered late.
+ 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))
+ .expect(h.admissionHeight() == 6 and decision(early) == Refused(ExpiryTooTight))
+ .then(deliver(early))
+ .expect(h.queued() == Set())
+ .then(see)
+ .then(blocks(2))
+ .expect(height == 8 and h.queued() == Set() and h.inFlight() == Set())
+
+ /// Finding 6, fixed by #85. The hub crashed in between and lost its queue,
+ /// as K5 says. The resend is refused, not offered with one block of margin
+ /// where two are reserved, as it was before #85.
+ run crashThenLateDuplicateTest =
+ duplicateBehindTheBoundary(true)
+ .expect(onTime == Set() and offered == Set())
+ .expect(admissionMatchesCadence and conformingEveryOfferBeforeExpiry)
+
+ /// Control. No crash: the transaction is published by the flush at 3, and
+ /// the duplicate is refused rather than offered a second time.
+ run lateDuplicateWithoutCrashTest =
+ duplicateBehindTheBoundary(false)
+ .expect(onTime == Set(early) and offered == Set(early))
+ .expect(admissionMatchesCadence and 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))
+ .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))
+ .expect(not(nodeWouldTake(early)))
+ .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)
+ .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)))
+ .then(judge(lateAtFloor, Rejected))
+
+ // ------------------------------------------------------------------------
+ // 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)
+ .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 needs 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)))
+ .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..aec4b491
--- /dev/null
+++ b/zeronym/spec/quint/tests/hubTest.qnt
@@ -0,0 +1,504 @@
+// -*- 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, spends: Set(), oversize: false }
+
+ pure val pA = orchard("a", Some(9))
+ pure val pB = orchard("b", Some(9))
+ pure val pC = orchard("c", None)
+ /// A second signing of `pC`: different bytes, the same txid.
+ pure val pCSigned = { ...pC, id: "c-signed" }
+ pure val pTight = orchard("tight", Some(6))
+ pure val pJunk = { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, spends: Set(), oversize: false }
+
+ pure val PAYLOADS = Set(pA, pB, pC, pTight, pJunk)
+ pure val REFUSALS = Set(TipStale, HubDraining, ExpiryTooTight, SpentProof)
+
+ /// 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, revealed: false })
+
+ /// A submission whose nullifiers every current view reports mined.
+ pure def submitRevealed(payload: Payload): HubInput =
+ SubmitHInput({ nonce: 0, payload: payload, revealed: true })
+
+ 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)
+
+ /// `pC`, which never expires, out with a flush at tip 6, and resent while
+ /// it is out.
+ pure val flushingC = running(5).after(submit(pC)).after(TipHInput(6)).after(FlushDueHInput)
+ pure val resent = flushingC.after(submit(pC))
+ /// After a node rejected `pC`: its proofs are burned.
+ pure val burnedC = flushingC.after(verdict(pC, Rejected))
+
+ pure val STATES = Set(down, starting, running(2), running(5), holding, flushing, stale, draining, stopped,
+ stale.after(DrainHInput), flushing.after(verdict(pA, Retryable)), burnedC)
+
+ pure val INPUTS: Set[HubInput] =
+ PAYLOADS.map(payload => submit(payload))
+ .union(PAYLOADS.map(payload => submitRevealed(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, AlreadyMined, 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, false) == Refused(TipStale))),
+ assert(PAYLOADS.forall(payload => admission(stale, payload, false) == Refused(TipStale))),
+ assert(PAYLOADS.forall(payload => admission(stale.after(DrainHInput), payload, false) == Refused(TipStale))),
+ // Draining comes before anything about the payload.
+ assert(PAYLOADS.forall(payload => admission(draining, payload, false) == Refused(HubDraining))),
+ // Expiry before the queue is looked at. At tip 5 the next flush is at 6.
+ assert(admission(running(5), pTight, false) == Refused(ExpiryTooTight)),
+ assert(admission(holding, pTight, false) == Refused(ExpiryTooTight)),
+ assert(admission(running(2), pTight, false) == Admitted),
+ // A duplicate is recognised; anything else that passes is admitted.
+ assert(admission(holding, pA, false) == Duplicate),
+ assert(admission(holding, pB, false) == Admitted),
+ assert(admission(running(5), pA, false) == Admitted),
+ // An unparseable payload has no expiry and is admitted like any other.
+ assert(admission(running(5), pJunk, false) == Admitted),
+ // Mined nullifiers refuse a payload with proofs, after expiry and before
+ // the queue; a payload with no proofs to read is not refused for them.
+ assert(admission(holding, pA, true) == Refused(SpentProof)),
+ assert(admission(holding, pTight, true) == Refused(ExpiryTooTight)),
+ assert(admission(running(5), pJunk, true) == Admitted),
+ // Burned proofs are refused after the duplicate check, including a second
+ // signing of the same txid.
+ assert(admission(burnedC, pC, false) == Refused(SpentProof)),
+ assert(admission(burnedC, pCSigned, false) == Refused(SpentProof)),
+ assert(admission(burnedC, pJunk, false) == 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, false) == 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, and the best is kept.
+ assert(running(5).after(TipHInput(4)).tip == Some(4) and running(5).after(TipHInput(4)).best == 5),
+ // Back beyond it: ignored.
+ assert(running(5).after(TipHInput(3)) == running(5)),
+ assert(outputOf(running(5), TipHInput(3)) == NoHubOutput),
+ // Depth is measured from the best, so a reorg is not walked down one
+ // allowance at a time.
+ assert(running(5).after(TipHInput(4)).after(TipHInput(3)) == running(5).after(TipHInput(4))),
+ // A new high ends staleness; a move back does not, and neither does a
+ // climb back to the best.
+ 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)),
+ assert(stale.after(TipHInput(4)).after(TipHInput(5)).phase == Stale),
+ assert(stale.after(TipHInput(5)).phase == Stale and stale.after(TipHInput(5)).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)))),
+ // The clock starts from the best height, not from a tip that dipped.
+ assert(isError(outputOf(running(5).after(TipHInput(4)), StaleHInput(4)))),
+ assert(running(5).after(TipHInput(4)).after(StaleHInput(5)).cadence == FreeRunning(5)),
+ }
+
+ // ------------------------------------------------------------------------
+ // 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, mined and rejected entries leave.
+ assert(Set(Accepted, AlreadyKnown, AlreadyMined, 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))),
+ // A rejected or mined entry with proofs burns its txid, and every queued
+ // entry with that txid leaves with it: the same bytes, or a second
+ // signing. Without proofs nothing is burned.
+ assert(Set(Rejected, AlreadyMined).forall(given =>
+ val judged = resent.after(verdict(pC, given))
+ val signed = flushingC.after(submit(pCSigned)).after(verdict(pC, given))
+ and {
+ judged.burned == Set("c") and judged.queue == Map(),
+ signed.burned == Set("c") and signed.queue == Map(),
+ })),
+ assert(Set(Accepted, AlreadyKnown).forall(given =>
+ val judged = resent.after(verdict(pC, given))
+ judged.burned == Set() and judged.queued() == Set(pC))),
+ assert(flushing.after(verdict(pJunk, Rejected)).burned == Set()),
+ // A restart forgets the burn set with the queue.
+ assert(burnedC.after(CrashHInput) == down),
+ // 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)),
+ // The epoch was recorded when the flush began; its end leaves it alone.
+ assert({ ...returning, phase: Stale, cadence: FreeRunning(11) }.after(FlushDoneHInput).lastEpoch == Some(1)),
+ assert(not({ ...returning, tip: Some(8), best: 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
+ // ------------------------------------------------------------------------
+
+ /// 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,
+ }))
+
+ // ------------------------------------------------------------------------
+ // Every reachable state
+ // ------------------------------------------------------------------------
+ //
+ // `REACH` is every hub state reachable from a starting hub under
+ // `REACH_INPUTS`. 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(REACH_PAYLOADS.map(payload => submitRevealed(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, AlreadyMined, Rejected, Retryable))
+ .map(((payload, given)) => verdict(payload, given)))
+
+ pure def successors(state: HubState): Set[HubState] =
+ REACH_INPUTS.map(input => hub(state, input).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 leaves it.
+ run reachTest = assert(REACH.forall(state => successors(state).subseteq(REACH)))
+
+ /// A2. An entry leaves the queue only into a flush, because a node judged an
+ /// entry with its txid and the hub burned that txid, or because the hub went
+ /// down or exited after its final flush.
+ 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()).union(
+ state.queued().filter(payload => isBurned(stepped.burned, payload)))))))
+
+ /// A3. A draining hub admits nothing: its queue gains only what a flush
+ /// hands back.
+ 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 observed tip is the best, or within the reorg allowance below it.
+ run tipNearBestTest =
+ assert(REACH.forall(state =>
+ match state.tip {
+ | Some(tip) => tip <= state.best and state.best - tip <= PARAMS.reorgAllowance
+ | None => state.best == 0
+ }))
+
+ // ------------------------------------------------------------------------
+ // 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.
+ run abstractionTest =
+ assert(REACH.forall(state =>
+ REACH_INPUTS.union(LOOKUPS).forall(input =>
+ isAbstracted(state, input, hub(state, input), honestAnswers))))
+
+ /// 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)),
+ // settle with the copy resent meanwhile, and with a second signing of it
+ assert(realises(resent, verdict(pC, Rejected), resent.project().settleWithCopy(pC), None)),
+ val signed = flushingC.after(submit(pCSigned))
+ assert(realises(signed, verdict(pC, Rejected), signed.project().settleWithCopy(pC), 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..95341dba
--- /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, spends: Set(), 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, spends: Set(), 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: AtMined })))),
+ // 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..2e316eb2
--- /dev/null
+++ b/zeronym/spec/quint/tests/scenariosTest.qnt
@@ -0,0 +1,248 @@
+// -*- mode: Bluespec; -*-
+
+/// Scripted runs against the honest configuration: 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)
+ .then(initShieldedSpend)
+
+ // ------------------------------------------------------------------------
+ // 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 TEX payment from Orchard funds: both legs go to the hub and are
+ /// published together. The second leg's prevout names the first, and the
+ /// operator sees neither (#94).
+ run texSecondLegIsDivertedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(submitTo(1, tex))
+ .expect(lastEvent == Sent({ input: Clean(tex), obs: SentOk }))
+ .expect(s.hub.queue == Set(early, tex) and s.operator == Set())
+ .expect(vForwardedSpendsNoDiverted and forwardedSpendsNoDiverted)
+ .then(flush([early, tex], Accepted))
+ .expect(s.onChain("early") == InMempool and s.onChain("tex") == InMempool)
+ .expect(operatorBlind and forwardedSpendsNoDiverted)
+
+ /// 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: an observer that knows a txid is told it
+ /// is queued, and is not given the bytes.
+ run observerLearnsItIsQueuedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(observerLearnsTxidWith("early"))
+ .then(observerLookupWith("early"))
+ .then(deliverLookupFrom(ObserverAddr, 0, "early", INotFound))
+ .expect(s.replies(ObserverAddr) == 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 an observer
+ /// that asks is served its bytes from the indexer. G2 holds: they are
+ /// public.
+ run observerIsServedPublishedBodyTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(observerLookupWith("early"))
+ .then(deliverLookupFrom(ObserverAddr, 0, "early", chainAnswer(s.indexer, "early")))
+ .expect(s.replies(ObserverAddr) == Set({ nonce: 0, reply: WFound({ body: Some(early), height: AtZero }) }))
+ .expect(s.repliedBodies(ObserverAddr) == Set(early) and s.operator == Set())
+ .expect(wObserverServedBody 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 an observer: the bytes are public once
+ /// published, and submission is open to anyone.
+ run observerResubmitsPublishedTest =
+ initBaseline
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(lookUp(1, "early"))
+ .expect(s.tpPayloads().contains(early))
+ .then(observerSubmitWith(early))
+ .then(deliverSubmitFrom(ObserverAddr, 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)
+
+ // ------------------------------------------------------------------------
+ // K10. A shielded spend of a diverted transaction is forwarded
+ // ------------------------------------------------------------------------
+
+ /// K10. The wallet deshields `late` to its own address, then auto-shields
+ /// that output into Ironwood. The second transaction carries a shielded
+ /// bundle, so neither arm diverts it. The operator gets it, and its prevout
+ /// names `late`, which the hub holds. G1 holds throughout: the operator
+ /// sees no migration's contents, only its txid.
+ run shieldedSpendOfDivertedIsForwardedTest =
+ initShieldedSpend
+ .then(submitTo(0, late))
+ .then(sendToHub(autoShield))
+ .expect(lastEvent == Sent({ input: Clean(autoShield), obs: SentToOperator }))
+ .expect(s.operator == Set(autoShield) and s.hub.queue == Set(late))
+ .expect(not(forwardedSpendsNoDiverted) and operatorBlind)
+ // Publishing `late` changes nothing: the link is already made.
+ .then(flush([late], Accepted))
+ .expect(s.onChain("late") == InMempool and not(forwardedSpendsNoDiverted))
+}
diff --git a/zeronym/spec/quint/tests/shimTest.qnt b/zeronym/spec/quint/tests/shimTest.qnt
new file mode 100644
index 00000000..5db3d04e
--- /dev/null
+++ b/zeronym/spec/quint/tests/shimTest.qnt
@@ -0,0 +1,196 @@
+// -*- 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, spends: Set(), oversize: false }
+
+ pure val pOrchard = payload("orchard", OrchardTouching)
+ pure val pPlain = payload("plain", OtherShielded)
+ 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", OtherShielded), oversize: true }
+ /// The second leg of a TEX payment: transparent parts only, spending an
+ /// output of `pOrchard`.
+ pure val pTex = { ...payload("tex", TransparentOnly), spends: Set("orchard") }
+ /// Transparent parts only, spending nothing: a coinbase.
+ pure val pCoinbase = payload("coinbase", TransparentOnly)
+ /// A shielded transaction that spends an output of `pOrchard`.
+ pure val pShieldedSpend = { ...payload("shielded-spend", OtherShielded), spends: Set("orchard") }
+
+ pure val PAYLOADS = Set(pOrchard, pPlain, pJunk, pBig, pBigPlain, pTex, pCoinbase, pShieldedSpend)
+ 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 transaction with a Sprout, Sapling or Ironwood
+ /// bundle, or a coinbase, 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) =>
+ and {
+ input == Clean(forwarded),
+ or {
+ forwarded.class == OtherShielded,
+ forwarded.class == TransparentOnly and forwarded.spends == Set(),
+ },
+ }
+ | _ => 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 })),
+ }
+
+ /// The two arms of the classifier (#94), and what each leaves forwarded.
+ run classifierArmsTest = all {
+ // The transparent-only arm: the second leg of a TEX payment is diverted.
+ assert(outputOf(initialShim, send(Clean(pTex), true))
+ == DivertedOutput({ payload: pTex, frame: Submit({ nonce: 0, payload: pTex }), told: SentOk })),
+ // The arm needs a spend: a coinbase is forwarded.
+ assert(outputOf(initialShim, send(Clean(pCoinbase), true)) == ForwardOutput(pCoinbase)),
+ // A spend that carries a shielded bundle is forwarded, whatever it
+ // spends. The shim reads the shape alone (K10).
+ assert(outputOf(initialShim, send(Clean(pShieldedSpend), true)) == ForwardOutput(pShieldedSpend)),
+ // Diverted: either arm, or bytes the shim cannot parse.
+ assert(Set(pOrchard, pTex, pJunk).forall(p => treatAsMigration(p))),
+ assert(Set(pPlain, pCoinbase, pShieldedSpend).forall(p => not(treatAsMigration(p)))),
+ }
+
+ 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..79a11b0a
--- /dev/null
+++ b/zeronym/spec/quint/tests/trustTest.qnt
@@ -0,0 +1,164 @@
+// -*- 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 an observer about a queued txid, it answers
+ /// with the queued bytes.
+ run hubServesQueuedBodyTest =
+ initByzHub
+ .then(submitTo(0, early))
+ .then(observerLearnsTxidWith("early"))
+ .then(observerLookupWith("early"))
+ .expect(queuedBytesConfidential)
+ .then(hubReceiveWith(
+ fromObserver(lookupMail(0, "early")), INotFound,
+ { hub: s.hub, reply: AWire(render(FromIndexer(IFound({ body: Some(early), height: AtZero })))) },
+ ))
+ .expect(s.replies(ObserverAddr) == 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(ObserverAddr) == 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.
+ /// 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: AtMined })))) },
+ ))
+ .then(deliverToShim(replyMail(1, WFound({ body: Some(early), height: AtMined }))))
+ .expect(lastEvent == Got({ query: "early", obs: Tx({ payload: early, height: AtMined }), via: Some(1) }))
+ .expect(s.onChain("early") == InMempool)
+ .expect(audit.windows.get(1) == Set(Tx({ payload: early, height: AtZero })))
+ .expect(not(lookupValidityPerHub) and txidAuthenticity)
+
+ /// G5 needs the hub. It answers pending for a transaction it does not hold.
+ run hubForgesPendingTest =
+ initByzHub
+ .then(sends(Clean(early), true))
+ .then(ask("early"))
+ .expect(pendingOnlyFromQueue)
+ .then(hubReceiveWith(
+ lookupMail(1, "early"), INotFound,
+ { hub: s.hub, reply: AWire(WFound({ 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(pendingOnlyFromQueue))
+
+ /// 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(observerLearnsTxidWith("early"))
+ .then(observerLookupWith("early"))
+ .expect(queuedBytesConfidential)
+ .then(deliverLookupFrom(
+ ObserverAddr, 0, "early", IFound({ body: Some(early), height: AtZero }),
+ ))
+ .expect(s.replies(ObserverAddr) == 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(ObserverAddr) == Set(early) and s.operator == Set())
+ .expect(not(queuedBytesConfidential))
+
+ /// Finding 8, fixed by #85. For a transaction that exists nowhere the
+ /// indexer answers "found, height 0, no body". Before #85 the hub forwarded
+ /// it and the wallet saw pending. The hub's client now reads it as the
+ /// endpoint failing, and the wallet sees the lookup as unavailable.
+ run indexerEmptyAnswerIsUnavailableTest =
+ initByzIndexer
+ .then(sends(Clean(early), true))
+ .then(ask("early"))
+ .then(deliverLookupFrom(ShimAddr, 1, "early", IFound({ body: None, height: AtZero })))
+ .then(deliverToShim(replyMail(1, WError)))
+ .expect(lastEvent == Got({ query: "early", obs: Unavailable, via: Some(1) }))
+ .expect(lookupValidityPerHub and pendingOnlyFromQueue)
+
+ /// G4 needs the indexer. It serves a published mempool transaction as
+ /// mined. The txid is right, so the shim passes it on.
+ run indexerServesFalseHeightTest =
+ initByzIndexer
+ .then(submitTo(0, early))
+ .then(flush([early], Accepted))
+ .then(ask("early"))
+ .expect(lookupValidityPerHub)
+ .then(deliverLookupFrom(ShimAddr, 1, "early", IFound({ body: Some(early), height: AtMined })))
+ .then(deliverToShim(replyMail(1, WFound({ body: Some(early), height: AtMined }))))
+ .expect(lastEvent == Got({ query: "early", obs: Tx({ payload: early, height: AtMined }), via: Some(1) }))
+ .expect(s.onChain("early") == InMempool)
+ .expect(audit.windows.get(1) == Set(Tx({ payload: early, height: AtZero })))
+ .expect(not(lookupValidityPerHub) and txidAuthenticity)
+}
diff --git a/zeronym/spec/quint/tests/wireTest.qnt b/zeronym/spec/quint/tests/wireTest.qnt
new file mode 100644
index 00000000..448377d1
--- /dev/null
+++ b/zeronym/spec/quint/tests/wireTest.qnt
@@ -0,0 +1,112 @@
+// -*- 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, spends: Set(), oversize: false }
+ pure val pATwin = { ...pA, id: "a-twin" }
+ pure val pB = { id: "b", txid: Some("tb"), created: 1, expiry: None, class: OtherShielded, spends: Set(), oversize: false }
+ pure val pJunk = { id: "junk", txid: None, created: 1, expiry: None, class: Unparseable, spends: Set(), 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, SpentProof)
+
+ /// 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,
+ /// The hub reads that indexer answer as a failure, so it never reaches the
+ /// wire (`indexerEmptyAnswerIsUnavailableTest`). 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 and a spent proof refuse under the queue-full code; a
+ /// fresh admission and a duplicate are one acceptance. Every other refusal
+ /// has its own code.
+ run ackRenderingTest = all {
+ assert(renderAck(Refused(HubDraining)) == WRefused(WQueueFull)),
+ assert(renderAck(Refused(SpentProof)) == 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)) =>
+ and { renderAck(Refused(left)) == renderAck(Refused(right)), renderAck(Refused(left)) != WRefused(WQueueFull) }
+ 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..e17923fb
--- /dev/null
+++ b/zeronym/spec/quint/types.qnt
@@ -0,0 +1,241 @@
+// -*- 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
+ // ------------------------------------------------------------------------
+
+ /// What the shim's parser reads of a `SendTransaction` body's pools. The
+ /// shim's routing rule over it is `treatAsMigration` in `shim.qnt`.
+ ///
+ /// - `OrchardTouching`: at least one Orchard action.
+ /// - `TransparentOnly`: transparent parts only, with no Sprout, Sapling,
+ /// Orchard or Ironwood data.
+ /// - `OtherShielded`: a Sprout, Sapling or Ironwood bundle, and no Orchard
+ /// action.
+ /// - `Unparseable`: the shim's own parser gives up. It is treated as a
+ /// migration, never forwarded.
+ type Class = OrchardTouching | TransparentOnly | OtherShielded | 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 what the shim's parser reads of the pools. It is independent
+ /// of `txid`: the shim rejects trailing bytes that the hub's parser
+ /// accepts.
+ /// - `spends` holds the txids whose transparent outputs the transaction
+ /// spends: its prevouts, without the output index. It is empty for a
+ /// coinbase and for a transaction with no transparent inputs. A node
+ /// that accepts the bytes reads it, and so does the operator.
+ /// - `oversize`: the bytes do not fit the fixed hub frame.
+ type Payload = {
+ id: str,
+ txid: Option[TxId],
+ created: Height,
+ expiry: Option[Height],
+ class: Class,
+ spends: Set[TxId],
+ 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 the hub can read Orchard proofs in `payload`, and so can burn
+ /// them: it parses and touches Orchard. Only such a payload has bundle keys.
+ pure def hasProof(payload: Payload): bool =
+ payload.class == OrchardTouching and isSome(payload.txid)
+
+ /// 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,
+ }
+
+ /// Whether both payloads carry one txid. A payload with none shares nothing,
+ /// so a burn has no key to spread to it. A re-signing keeps the txid.
+ pure def sharesTxid(left: Payload, right: Payload): bool =
+ and {
+ 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
+
+ pure val WIRE_HEIGHTS = Set(AtZero, AtMined)
+
+ /// 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 lookup answer as the hub's client returns it
+ /// (`ChainClient::get_transaction`). A found answer with no body, at any
+ /// height, is that endpoint failing: "found, height 0, no body" is the hub's
+ /// own queue-hit reply. With the model's one endpoint that is unavailable.
+ pure def hubReads(answer: IndexerAnswer): IndexerAnswer =
+ match answer {
+ | IFound(found) => if (found.body == None) IUnavailable else answer
+ | _ => answer
+ }
+
+ /// An indexer's verdict on one broadcast transaction. `AlreadyKnown` is a
+ /// mempool's, `AlreadyMined` names a block. `Retryable` means nothing judged
+ /// it: the indexer could not be reached or could not be read.
+ type Verdict = Accepted | AlreadyKnown | AlreadyMined | Rejected | Retryable
+
+ // ------------------------------------------------------------------------
+ // Hub
+ // ------------------------------------------------------------------------
+
+ /// Why a hub refuses a submission, in the order admission checks them.
+ /// `SpentProof`: the payload's proofs are mined, or this hub published them
+ /// to a rejection or a mined verdict (`Refusal::Rejected`).
+ type Refusal = TipStale | HubDraining | ExpiryTooTight | SpentProof
+
+ /// 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 observer is any client of the hub's public,
+ /// unauthenticated address other than the shim.
+ type Addr = ShimAddr | HubAddr | ObserverAddr
+
+ /// 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],
+ maxRequests: int,
+ roles: Roles,
+ }
+}
diff --git a/zeronym/spec/quint/wire.qnt b/zeronym/spec/quint/wire.qnt
new file mode 100644
index 00000000..ed9a77a0
--- /dev/null
+++ b/zeronym/spec/quint/wire.qnt
@@ -0,0 +1,113 @@
+// -*- 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.
+ 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 and a spent proof answer 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)
+ | SpentProof => WRefused(WQueueFull)
+ }
+ }
+
+ /// 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.
+ /// The hub's client never lets that answer through (`hubReads`).
+ 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
+ }
+}