docs(specs): pilot a Quint model of statement routing

.claude/skills/proxy-quint/SKILL.md

@@ -13,7 +13,7 @@ This skill holds only what is specific to Proxy, and wins where it differs from
 ## Running the checks
 
 - Iterate with `./check.sh` from `specs/quint`: typecheck, scenario tests, and simulation with every witness required to be reached.
-- Before pushing a model change, run `./check.sh all` in the background (about 11 minutes) and wait for exit 0. TLC is part of Proxy's checks, unlike the kit's sampled-only workflow.
+- Before pushing a model change, run `./check.sh all` in the background (about 6 minutes) and wait for exit 0. TLC is part of Proxy's checks, unlike the kit's sampled-only workflow.
 - Record the new state counts, timings and witness counts in `verification.md` in the same change.
 - When you run `quint` yourself, use the pinned CLI (`npx --no-install quint` in `specs/quint`, or bare `quint` under mise) and pass `--backend typescript` to `run` and `test`: the default Rust backend downloads through the GitHub API, which cloud sessions block.
 

.github/workflows/quint.yml

@@ -0,0 +1,51 @@
+name: Quint specifications
+# Design-level model of statement routing; see specs/quint/README.md.
+# Not a required check: it is a pilot.
+on:
+  pull_request:
+    paths:
+      - 'specs/quint/**'
+      - '.github/workflows/quint.yml'
+  push:
+    branches:
+      - main
+    paths:
+      - 'specs/quint/**'
+      - '.github/workflows/quint.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  model-check:
+    name: Quint model check
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    defaults:
+      run:
+        working-directory: specs/quint
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v4
+        with:
+          node-version: '22'
+          cache: npm
+          cache-dependency-path: specs/quint/package-lock.json
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: '21'
+      - name: Cache Apalache (bundles TLC)
+        uses: actions/cache@v4
+        with:
+          path: ~/.quint
+          key: quint-apalache-${{ hashFiles('specs/quint/package-lock.json') }}
+      - name: Install the pinned Quint CLI
+        run: npm ci --ignore-scripts
+      - name: Typecheck, scenario tests and simulation
+        run: ./check.sh basic
+      - name: TLC model checking
+        run: ./check.sh tlc
+      - name: Mutation tests
+        run: ./check.sh mutations

AGENTS.md

@@ -12,9 +12,10 @@ architecture, domain boundaries, request flow, and vocabulary.
 ## Formal models
 
 Before changing `specs/quint/`, or Proxy's statement routing, Parse/Bind
-lifecycle, settings protocol or schema reload (`frontend.rs`,
-`context/{lifecycle,mod,settings_protocol}.rs` and
-`schema/{middleware,manager}.rs` in `packages/cipherstash-proxy/src/`, and
+lifecycle, settings protocol or schema reload (`frontend.rs`, `error.rs`,
+`context/{lifecycle,mod,settings,settings_protocol}.rs`,
+`schema/{middleware,manager}.rs` and `sql/select_table_schemas.sql` in
+`packages/cipherstash-proxy/src/`, and
 `packages/eql-mapper/src/eql_mapper.rs`), use the `proxy-quint` skill.
 
 ## Development workflow

DEVELOPMENT.md

@@ -491,7 +491,7 @@ mise run quint:install
 # typecheck, scenario tests and simulation (about 20 s)
 mise run quint:check
 
-# everything, including exhaustive TLC checks (about 10 min)
+# everything, including exhaustive TLC checks (about 6 min)
 mise run quint:check all
 ```
 

specs/quint/.gitignore

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

specs/quint/README.md

@@ -0,0 +1,48 @@
+# Quint specifications
+
+Design-level models of CipherStash Proxy behaviour, written in [Quint](https://quint.sh) and checked with its simulator and with TLC.
+They are a pilot: the CI job is not a required check, and no Rust code is tested against them yet.
+
+| Model | What it checks |
+|---|---|
+| [`routing/`](routing/requirements.md) | Statement routing: can a client's plaintext reach an encrypted column? |
+
+Start with a model's `requirements.md`, which lists its sources, scope, assumptions, properties, findings and open decisions, then read its `verification.md` for the exact results.
+
+## Running the checks
+
+Needs Node 22 and Java 21.
+The Quint CLI is pinned in `package-lock.json`; install it here rather than globally.
+
+```bash
+cd specs/quint
+npm ci --ignore-scripts
+./check.sh            # typecheck, scenario tests, simulation (about 20 s)
+./check.sh tlc        # exhaustive TLC checks, including expected findings (about 4 min)
+./check.sh mutations  # injected faults must each be caught (about 2 min)
+```
+
+The first `quint verify` downloads the Apalache distribution, which bundles TLC, into `~/.quint`.
+`check.sh` uses the simulator's TypeScript backend, because the default Rust backend downloads a binary through the GitHub API at first use.
+
+## What each stage means
+
+- `quint typecheck`: the model is well formed. Nothing more.
+- `quint test`: the named scenarios behave as written.
+- `quint run`: no violation in the sampled traces, and every named witness is reached in at least one trace. Not a proof.
+- `quint verify --backend=tlc`: the property holds in every reachable state of that finite instance. Not a proof for larger instances.
+- Mutations: each injected fault produces a counterexample, so the properties are not vacuous.
+
+## Changing a model
+
+Decide first whether a change is a requirements change or an implementation change.
+A requirements change updates `requirements.md` and the model together, and needs review of the property it changes.
+Never weaken a property to make a check pass.
+Nothing connects these checks to Proxy's Rust code yet, so changing Proxy alone never changes their results.
+When Proxy's behaviour changes, update the model by hand to match.
+If that model change means a recorded finding no longer reproduces, `check.sh tlc` fails until the finding is moved out of the expected violations.
+
+## Tooling notes
+
+- `npm audit` reports two high-severity advisories in `adm-zip`, which Quint uses to unpack the Apalache download. They concern extracting untrusted archives; Quint only extracts its own release download.
+- Agent skills for these models are in `.claude/skills/`: `proxy-quint`, plus `quint-lang` and `quint-modeling` vendored from the Quint LLM Kit (see `.claude/skills/VENDORED.md`).

specs/quint/check.sh

@@ -0,0 +1,167 @@
+#!/usr/bin/env bash
+# Runs the Quint checks for the routing model. See README.md for what each
+# stage does and does not show.
+#
+#   ./check.sh            typecheck, scenario tests, simulation
+#   ./check.sh tlc        exhaustive TLC checks, expected findings included
+#   ./check.sh mutations  each injected fault must be caught by TLC
+#   ./check.sh all        everything
+set -euo pipefail
+
+cd "$(dirname "$0")"
+
+QUINT=(npx --no-install quint)
+MODEL=routing/routing.qnt
+TESTS=routing/routing_test.qnt
+SEED=42
+
+fail() {
+  echo "FAIL: $*" >&2
+  exit 1
+}
+
+# verify_holds INSTANCE INVARIANT [FILE]: TLC must explore every state and find
+# no violation.
+verify_holds() {
+  local main=$1 invariant=$2 file=${3:-$MODEL} out
+  echo "== TLC: $main satisfies $invariant"
+  if ! out=$("${QUINT[@]}" verify "$file" --main "$main" --backend=tlc --invariant "$invariant" 2>&1); then
+    echo "$out" >&2
+    fail "$main should satisfy $invariant"
+  fi
+  # The summary is informational: a change in Quint's wording must not fail
+  # a check that passed.
+  grep -E "distinct states found|No violation found" <<<"$out" || true
+}
+
+# verify_violated INSTANCE INVARIANT [FILE]: TLC must report a counterexample,
+# not an error of any other kind.
+verify_violated() {
+  local main=$1 invariant=$2 file=${3:-$MODEL} out
+  echo "== TLC: $main violates $invariant"
+  if out=$("${QUINT[@]}" verify "$file" --main "$main" --backend=tlc --invariant "$invariant" 2>&1); then
+    echo "$out" >&2
+    fail "$main should violate $invariant"
+  fi
+  grep -q "\[violation\]" <<<"$out" || {
+    echo "$out" >&2
+    fail "$main did not report a violation of $invariant"
+  }
+  echo "counterexample found, as expected"
+}
+
+# simulate INSTANCE WITNESS...: sample traces, require no violation of safety,
+# and require every witness to be reached in at least one trace. A witness
+# reached in 0 traces means the state is dead, so the model is over-constrained.
+simulate() {
+  local main=$1 out
+  shift
+  echo "== simulation: $main"
+  if ! out=$("${QUINT[@]}" run "$MODEL" --main "$main" --backend typescript \
+    --max-samples=2000 --max-steps=12 --seed="$SEED" --invariant safety \
+    --witnesses "$@" 2>&1); then
+    echo "$out" >&2
+    fail "$main should satisfy safety in simulation"
+  fi
+  grep -E "was witnessed in" <<<"$out"
+  if grep -qE "was witnessed in 0 trace" <<<"$out"; then
+    fail "$main: a witness was never reached"
+  fi
+}
+
+basic() {
+  echo "== typecheck"
+  "${QUINT[@]}" typecheck "$MODEL"
+  "${QUINT[@]}" typecheck "$TESTS"
+
+  echo "== scenario tests"
+  for main in routingScenarioTest routingDomainCheckTest; do
+    "${QUINT[@]}" test "$TESTS" --main "$main" --backend typescript --seed "$SEED"
+  done
+
+  echo "== simulation"
+  simulate asBuilt ciphertextStored fellBack statementRefused batchRuleFired \
+    unknownBindRefused settingsChangedRefused unsafePlaintextStored \
+    statementPrepared inTransaction boundExecuted statementClosed \
+    transactionEnded mappingDisabled
+  simulate concurrentDdl ciphertextStored dbRejected txSnapshotStale \
+    preparedRouteStale
+}
+
+tlc() {
+  # Properties that must hold.
+  verify_holds asBuilt safety
+  verify_holds concurrentDdl safety
+
+  # Findings: each counterexample must still exist. When one stops existing,
+  # the behaviour changed; update requirements.md and this list together.
+  verify_violated concurrentDdl noPlaintextToCurrentlyEncrypted       # F1
+  verify_violated concurrentDdlNoDomainCheck noPlaintextAtRest        # F1
+  verify_violated uncheckedWrites noPlaintextToKnownEncrypted         # F2
+}
+
+# mutate NAME FROM TO INVARIANT: replace FROM with TO in a copy of the model
+# and require TLC to find a violation of INVARIANT in the asBuilt
+# instance.
+mutate() {
+  local name=$1 from=$2 to=$3 invariant=$4 dir file
+  dir=$(mktemp -d)
+  file="$dir/routing.qnt"
+  cp "$MODEL" "$file"
+  grep -qF -- "$from" "$file" || fail "mutation $name: pattern not found"
+  FROM=$from TO=$to perl -0pi -e 's/\Q$ENV{FROM}\E/$ENV{TO}/' "$file"
+  echo "== mutation $name"
+  verify_violated asBuilt "$invariant" "$file"
+  rm -rf "$dir"
+}
+
+mutations() {
+  # M1: a write may fall back while encrypted columns are configured.
+  mutate M1-write-falls-back \
+    "not(mapErrs) and not(writesEncrypted)" \
+    "not(mapErrs)" \
+    noPlaintextToKnownEncrypted
+  # M2: a table Proxy cannot resolve type checks as native (#486).
+  mutate M2-unresolvable-is-native \
+    "val typeCheckFails = s.kind == Gap or v == VUnknown" \
+    "val typeCheckFails = s.kind == Gap" \
+    noPlaintextToUnresolvable
+  # M3: no batch rule, so a fallback carries a mapped statement as written.
+  mutate M3-no-batch-rule \
+    "else if (batchRefused(routes))" \
+    "else if (false)" \
+    noPlaintextToKnownEncrypted
+  # M4: Bind ignores a change to the mapping setting since Parse.
+  mutate M4-no-bind-settings-check \
+    "val settingsChanged = requiresSchema(p.stmt.kind) and conn.unsafe != p.unsafeAtParse" \
+    "val settingsChanged = false" \
+    noPlaintextToKnownEncrypted
+  # M5: a refused statement in a simple Query is forwarded anyway.
+  mutate M5-refusal-ignored \
+    "if (routeSet.contains(Refuse))" \
+    "if (false)" \
+    noPlaintextToKnownEncrypted
+  # M6: COPY ... FROM into an encrypted column is forwarded (#488).
+  mutate M6-copy-into-encrypted \
+    "encConfigured and v != VNative" \
+    "encConfigured and v == VUnknown" \
+    noPlaintextToKnownEncrypted
+  # M7: a write nested in a statement Proxy does not type check is forwarded.
+  mutate M7-nested-write-forwarded \
+    "if (snap.encConfigured) Refuse else Forward(NotTypeChecked)" \
+    "Forward(NotTypeChecked)" \
+    noPlaintextToKnownEncrypted
+  # M8: the Bind settings check leaves out COPY ... FROM (requires_schema).
+  mutate M8-settings-check-skips-copy \
+    "k == Checked or k == Gap or k == CopyFrom" \
+    "k == Checked or k == Gap" \
+    noPlaintextToKnownEncrypted
+}
+
+case "${1:-basic}" in
+  basic) basic ;;
+  tlc) tlc ;;
+  mutations) mutations ;;
+  all) basic; tlc; mutations ;;
+  *) fail "unknown stage: $1" ;;
+esac