[tobyhede]

Requested by Toby

A proof-of-concept formal model, in Quint, of how Proxy decides to map, forward or refuse each statement.
The property it checks is that plaintext never reaches an encrypted column, except when the client uses UNSAFE_DISABLE_MAPPING.
It's a design-level model only: it changes no production code, and no Rust code is tested against it yet.

Start with specs/quint/routing/requirements.md, which has the scope, assumptions, properties, findings and open decisions.
verification.md has the exact results.

What it models

• The refuse-by-default Frontend::route from refactor(proxy): route each statement through one refuse-by-default decision #484, including may_fall_back, the unresolvable-table refusal (fix(proxy): refuse writes to a table Proxy cannot resolve #486) and the simple Query batch rule.
• One connection running simple Query batches, Parse, Bind/Execute, Close, transactions and UNSAFE_DISABLE_MAPPING.
• Both values of mapping_errors_enabled.
• Optionally, another connection committing DDL that changes whether a column is encrypted.

Results (Quint 0.33.0, TLC, exhaustive for each finite instance)

• S1–S3 hold as built, including UNSAFE_DISABLE_MAPPING and concurrent DDL.
  With a stable schema they hold on Proxy's routing alone, even with PostgreSQL's domain check switched off.
• TLC catches each of four injected faults: write fallback, no unresolvable-table refusal, no batch rule (main's pre-refactor(proxy): route each statement through one refuse-by-default decision #484 behaviour), and no Bind settings check.

Findings to confirm against real Proxy before acting

These are recorded as expected counterexamples, so CI fails if one stops reproducing.

• F3 (retracted): the first version of the model left out the Bind settings check (PreparedSettingsChanged), so it reported a plaintext path that Proxy does not have. The model now includes the check, and mutation M4 covers it.
• F1: routes go stale under concurrent DDL. Prepared statements are routed once, at Parse, and transactions pin the schema. Only PostgreSQL's type and domain checks stop the plaintext write.
• F2: COPY FROM STDIN, DO and CALL are never type checked, so nothing in routing stops them writing plaintext.

PostgreSQL's domain check should reject the value in every case, so none of these is a confirmed leak. Each would need a failing test first.

Tooling

• specs/quint has a pinned package-lock.json, and check.sh covers typecheck, scenario tests, simulation, TLC and mutations.
• .github/workflows/quint.yml runs on changes under specs/quint only. It isn't a required check, and the full run takes about 8 minutes.
• npm audit flags adm-zip, which Quint uses only to unpack its own Apalache download (noted in the README).

Acknowledgment

By submitting this pull request, I confirm that CipherStash can use, modify, copy, and redistribute this contribution, under the terms of CipherStash's choice.

---

Generated by Claude Code