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

.github/workflows/zeronym-guards.yml

@@ -40,6 +40,23 @@ jobs:
       - name: Repository claim guards
         run: sh zeronym/guards.sh
 
+  # The Quint model of the shim <-> hub divert protocol. Simulation only, so it
+  # stays in the cheap tier.
+  spec:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    # 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
+      # The runner image's Node is enough for Quint.
+      - name: Divert protocol model
+        run: sh zeronym/spec/check.sh
+
   tests:
     runs-on: blacksmith-8vcpu-ubuntu-2404
     timeout-minutes: 30

zeronym/spec/check.sh

@@ -0,0 +1,67 @@
+#!/bin/sh
+# Simulate the divert model and assert every invariant's expected outcome.
+#
+# "holds" rows are the protocol's safety claims against an honest hub. "fails" rows are the two fixed
+# bugs, reproduced with their fix switched off, and the known gaps: if
+# one starts holding, the code or the model changed and divert.qnt needs a
+# look.
+#
+# QUINT defaults to `npx @informalsystems/quint@0.32.0`. QUINT_BACKEND=typescript
+# skips the Rust evaluator, which is downloaded from GitHub on first use.
+set -u
+
+cd "$(dirname "$0")"
+QUINT=${QUINT:-"npx --yes @informalsystems/quint@0.32.0"}
+BACKEND=${QUINT_BACKEND:-rust}
+SAMPLES=${QUINT_SAMPLES:-20000}
+failures=0
+
+# Classified by Quint's verdict line, so a crash, a download failure or a
+# misspelt invariant fails the gate instead of passing as a counterexample.
+check() {
+  main=$1 invariant=$2 expect=$3
+  out=$($QUINT run divert.qnt --backend="$BACKEND" --main="$main" --invariant="$invariant" \
+      --max-samples="$SAMPLES" --max-steps=30 --seed=7 2>&1)
+  case $out in
+    *"[ok] No violation found"*) got=holds ;;
+    *"[violation] Found an issue"*) got=fails ;;
+    *)
+      echo "ERROR $main.$invariant: quint gave no verdict"
+      echo "$out" | tail -20
+      failures=$((failures + 1))
+      return
+      ;;
+  esac
+  if [ "$got" = "$expect" ]; then
+    echo "ok    $main.$invariant $got"
+  else
+    echo "FAIL  $main.$invariant expected $expect, got $got"
+    failures=$((failures + 1))
+  fi
+}
+
+$QUINT typecheck divert.qnt || exit 1
+
+echo "---- runs"
+for main in badIndexer honest current; do
+  if $QUINT test divert.qnt --main "$main"; then
+    :
+  else
+    failures=$((failures + 1))
+  fi
+done
+
+check honest         pendingVisible  holds
+check honest         safety          holds
+check honest         pendingIsTrue   holds
+check badIndexer     pendingIsTrue   fails
+check before_ecb4641 pendingVisible  fails
+check before_45e408f noQueuedBytes   fails
+check current        noQueuedBytes   fails
+check current        noEarlyBytes    fails
+check current        noSilentRefusal fails
+check current        pendingIsTrue   fails
+check current        queuedNotSuppressed fails
+check honest         pendingMonotone fails
+
+exit "$failures"