From 61d1f95a26538b5e626eab35b3758501597d1669 Mon Sep 17 00:00:00 2001
From: Jakob Homan <jakob@posthog.com>
Date: Thu, 23 Jul 2026 21:32:14 +0100
Subject: [PATCH] ci: on-demand TLA+ model check workflow + fast profile
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Not a default PR gate — the full model is ~85M distinct states (~18 min
on 12 perf cores, 60-90 min on a standard runner):

- workflow_dispatch (full by default, fast selectable) — the receipt
  for spec changes
- pull_request touching tla/**: fast profile automatically (~3M
  states, minutes) as a non-required smoke signal
- nightly full run on main for spec/code drift

Viaduck.fast.cfg = MaxOps 3 (~28x smaller; 55s locally, all 7
invariants). tla2tools pinned + cached; log uploaded as artifact with
a step summary. just tlc-fast mirrors the profile locally.
---
 .github/workflows/tla.yml | 93 +++++++++++++++++++++++++++++++++++++++
 justfile                  |  5 +++
 tla/Viaduck.fast.cfg      | 26 +++++++++++
 3 files changed, 124 insertions(+)
 create mode 100644 .github/workflows/tla.yml
 create mode 100644 tla/Viaduck.fast.cfg

diff --git a/.github/workflows/tla.yml b/.github/workflows/tla.yml
new file mode 100644
index 0000000..25dfc43
--- /dev/null
+++ b/.github/workflows/tla.yml
@@ -0,0 +1,93 @@
+name: TLA+ Model Check
+
+# On-demand + spec-change verification of tla/Viaduck.tla — NOT a default
+# PR gate. The full profile explores ~85M distinct states (~18 min on 12
+# perf cores; expect 60-90 min on a standard 4-vCPU runner), so:
+#   - workflow_dispatch: full by default (the receipt for spec changes)
+#   - pull_request touching tla/**: fast profile (~3M states, minutes) as
+#     an automatic smoke signal, non-required
+#   - nightly on main: full, catches spec/code drift for free
+# The local `just tlc` run stays authoritative for the edit-check loop.
+
+on:
+  workflow_dispatch:
+    inputs:
+      profile:
+        description: "Model size"
+        type: choice
+        options: [full, fast]
+        default: full
+  pull_request:
+    paths:
+      - "tla/**"
+      - ".github/workflows/tla.yml"
+  schedule:
+    - cron: "17 3 * * *" # nightly, off the top-of-hour stampede
+
+permissions:
+  contents: read
+
+env:
+  TLA_TOOLS_VERSION: v1.7.4
+
+jobs:
+  tlc:
+    runs-on: ubuntu-latest
+    # Full profile on 4 vCPUs needs generous headroom; fast finishes in
+    # minutes. Cap well below the 6h job limit so a pathological spec
+    # change fails loudly instead of burning hours.
+    timeout-minutes: 150
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: "21"
+
+      - name: Cache tla2tools.jar
+        id: cache-tla
+        uses: actions/cache@v4
+        with:
+          path: tla2tools.jar
+          key: tla2tools-${{ env.TLA_TOOLS_VERSION }}
+
+      - name: Fetch tla2tools.jar
+        if: steps.cache-tla.outputs.cache-hit != 'true'
+        run: |
+          curl -fsSL -o tla2tools.jar \
+            "https://github.com/tlaplus/tlaplus/releases/download/${TLA_TOOLS_VERSION}/tla2tools.jar"
+
+      - name: Resolve profile
+        id: profile
+        run: |
+          # dispatch: the chosen input; PR path-trigger: fast; schedule: full
+          case "${{ github.event_name }}" in
+            workflow_dispatch) echo "cfg=${{ inputs.profile == 'fast' && 'Viaduck.fast.cfg' || 'Viaduck.cfg' }}" >> "$GITHUB_OUTPUT" ;;
+            pull_request)      echo "cfg=Viaduck.fast.cfg" >> "$GITHUB_OUTPUT" ;;
+            *)                 echo "cfg=Viaduck.cfg" >> "$GITHUB_OUTPUT" ;;
+          esac
+
+      - name: Run TLC
+        working-directory: tla
+        run: |
+          java -XX:+UseParallelGC -Xmx12g \
+            -cp "${GITHUB_WORKSPACE}/tla2tools.jar" tlc2.TLC \
+            Viaduck.tla -config "${{ steps.profile.outputs.cfg }}" \
+            -workers auto 2>&1 | tee "${GITHUB_WORKSPACE}/tlc.log"
+
+      - name: Summarize
+        if: always()
+        run: |
+          {
+            echo "### TLC (${{ steps.profile.outputs.cfg }})"
+            grep -E "distinct states|No error|violated|Error" tlc.log | tail -5 | sed 's/^/    /'
+          } >> "$GITHUB_STEP_SUMMARY"
+
+      - name: Upload log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: tlc-log-${{ github.run_id }}
+          path: tlc.log
+          retention-days: 30
diff --git a/justfile b/justfile
index de3f76a..1464062 100644
--- a/justfile
+++ b/justfile
@@ -217,3 +217,8 @@ build:
 [group('build')]
 clean:
     rm -rf .venv dist *.egg-info __pycache__ viaduck/__pycache__
+
+# Fast-profile model check (~3M states, under a minute locally) — the
+# smoke pass; `just tlc` (full, ~85M states) is authoritative.
+tlc-fast:
+    cd tla && tlc Viaduck.tla -config Viaduck.fast.cfg -workers auto
diff --git a/tla/Viaduck.fast.cfg b/tla/Viaduck.fast.cfg
new file mode 100644
index 0000000..c9c2a36
--- /dev/null
+++ b/tla/Viaduck.fast.cfg
@@ -0,0 +1,26 @@
+\* FAST PROFILE: MaxOps=3 shrinks the state space ~30x (minutes, not
+\* tens of minutes) at the cost of shallower interleavings. The full
+\* Viaduck.cfg (MaxOps=4, ~85M distinct states) remains the
+\* authoritative check for spec changes; this profile exists so CI can
+\* afford a smoke pass. Keep the two files in sync except MaxOps.
+SPECIFICATION Spec
+
+CONSTANTS
+    Keys = {1, 2}
+    Dests = {"d1", "d2"}
+    Instances = {"i1"}
+    MaxOps = 3
+    BufferCap = 3
+    RoutingMap <- RoutingMapDef
+    DestOwner <- DestOwnerDef
+    ValProj <- ValProjDef
+
+CHECK_DEADLOCK FALSE
+
+INVARIANT EventualConsistency
+INVARIANT NoPhantomWhenCurrent
+INVARIANT NoDataLossWhenCurrent
+INVARIANT CursorMonotonicity
+INVARIANT PartitionCorrectness
+INVARIANT BufferPositionBound
+INVARIANT FlushStateConsistency