test(zeronym): model the protocol in Quint and check it in CI

.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:

zeronym/spec/.gitignore

@@ -0,0 +1 @@
+_apalache-out/

zeronym/spec/quint/.gitignore

@@ -0,0 +1,2 @@
+*.itf.json
+_apalache-out/

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,
+    }
+}