§31 Loam Router and Verification: Sharded Loam SQL and Loam Postgres, Specified, Simulated and Tested

Status: Proposed · 2026-10-01. This document folds the chat-dump plan "Loam SQL, Loam Postgres, and Loam Router: Build and Verification Plan" (chatdump.md, lines 54–322, owner request of 2026-10-01) into Loam's design, and reconciles it with what has been decided since that plan was written: D260 (no TiDB), D236 (PgDog, unmodified), §28 (Loam Postgres, Arm A) and the pending §29 (WeSQL as the MySQL OLTP engine, PR #172, D273–D280). Decisions are D300–D322 and open questions Q300–Q314, all proposals. It changes no code; the work is track RT (RT0–RT5, §17), with plans RT0, RT1 and RT2.

The chat dump's own milestones M0–M5 are renamed RT0–RT5, so they do not clash with Loam's M0–M6 (D319).

Markers, as in §28 and §29:

• (verify) means not checked against a primary source, or checked only by reading code that was not run. The task that depends on it checks it first.
• (estimate) means computed or reasoned, not measured.
• (source) means read in the source on 2026-10-01, at the revisions below.
• Paths of the form pgdog/… point into pgdogdev/pgdog at 80d6059d (v0.1.60-30, 2026-10-01), read as a reference only (AGPL-3.0, D236). vitess/… points into vitessio/vitess main read through the GitHub API on 2026-10-01 (latest release v24.0.4, 2026-10-01). neon/… points into neondatabase/neon at fa504217c, the base of dina-kar/neon (§28). wesql/… points into ostrium-labs/wesql branch 8.0 at eef34f452 (§29).

1. SummaryCopy Anchor Link

2. Goals and non-goalsCopy Anchor Link

2.1 GoalsCopy Anchor Link

1. Sharded MySQL and Postgres for apps that outgrow one primary, on engines Loam already runs: Loam Postgres (§28) and WeSQL (§29).
2. One shard map and one control plane for both engines: placement, routing generations, cutover, failover and in-doubt monitoring, driven from Loam's metastore and Resonate sagas.
3. Buy the routers. PgDog and Vitess already parse, plan, route, scatter, merge, aggregate, pool, reshard and (with conditions) commit atomically. Loam builds what neither gives it: multi-instance coordination, a fence in the backend, and evidence.
4. Evidence, not only tests, as the chat dump asked: TLA+ for the protocols, Lean 4 for pure kernels, deterministic simulation for Loam's control plane, and fault tests on the real systems.

2.2 Non-goalsCopy Anchor Link

• A new MySQL engine (D301), a new SQL router (D300) or a Vitess tablet re-implementation (D302), unless D317's triggers fire.
• Transactions across engines (kept from the chat dump).
• Cross-shard joins beyond what the bought routers do (kept, and now defined by them).
• Proving PgDog or Vitess correct. Loam proves its own kernels and protocols, and tests the routers' behaviour.
• Modifying PgDog (D236), or TiKV/PD (D126).
• Upstream contributions without the owner's go-ahead (as §28 and §29).

3. Reconciling the chat dumpCopy Anchor Link

Each claim of the chat dump that the current design or the sources change, checked on 2026-10-01.

4. ArchitectureCopy Anchor Link

 MySQL clients                                   Postgres clients
     │ mysql://<keyspace>                            │ postgres://…/<db>[__<branch>]
     ▼                                               ▼
 ┌─────────────────────────────┐            ┌─────────────────────────────────┐
 │ vtgate ×N (Vitess v24,      │            │ PgDog ×N (AGPL-3.0, unmodified, │
 │ Apache-2.0, unmodified)     │            │ StatefulSet when 2PC is on)     │
 │ VSchema, vindexes, scatter, │            │ hash/range/list sharding,       │
 │ merge, buffering            │            │ scatter, merge, partial aggs,   │
 └──────────┬──────────────────┘            │ 2PC (opt-in), RESHARD           │
            │ gRPC                          └──────────┬──────────────────────┘
            ▼                                          │ Postgres protocol (TLS)
 ┌─────────────────────────────┐                       ▼
 │ vttablet ×shard (unmanaged) │            ┌─────────────────────────────────┐
 │ query service, VReplication │            │ Loam Postgres computes per shard│
 └──────────┬──────────────────┘            │ (§28: pageserver, Arm A WAL)    │
            ▼                               │ Postgres 17.11 shards in CI     │
 ┌─────────────────────────────┐            └─────────────────────────────────┘
 │ WeSQL primaries + replicas  │
 │ (§29: W2 quorum, W3 HA)     │                 ▲ config + RELOAD, PAUSE/RESUME,
 └─────────────────────────────┘                 │ CUTOVER; fence via SQL
            ▲ vtctld gRPC: VSchema, Reshard,     │
            │ TabletExternallyReparented         │
 ┌──────────┴──────────────────────────────────────────────────────────────────┐
 │ Loam router control plane (in `operon`, D300)                                │
 │ operon-sqlrouter (sans-I/O machines: shard map, config push, cutover,        │
 │   in-doubt monitor; kernels: ranges, hashing, merge reference) ── traces ──► │
 │ operon-sqlrouter-io (adapters: TiKV records, PgDog admin, Postgres and       │
 │   WeSQL backends, vtctld, Kubernetes ConfigMaps); sagas on Resonate (§21)    │
 └──────────┬───────────────────────────────────────────────────────────────────┘
            ▼
 TiKV metastore: shard map record (D304), §23 `x/` records, §29 W3 primary record

 Verification: spec/tla/router (TLC, Apalache) ◄── trace validation ── operon-detsim
               spec/lean (LoamRouter oracle)  ◄── differential tests ── routers' results
               operon-nemesis (RT5) on real processes, same workloads and checkers

4.1 ComponentsCopy Anchor Link

5. The ADRs of the chat dump's §2, decidedCopy Anchor Link

The chat dump asked for one ADR per row of its §2 before any code. Each is decided here, with the evidence of §3, and two are added.

ADR-1. Router language: Go fork of vtgate, or a Rust rewrite. Decision: neither. Loam runs vtgate (Go) and PgDog (Rust) unmodified and writes its control plane in Rust (D300). Why: both routers exist, are maintained (Vitess releases monthly; PgDog weekly) and carry years of compatibility work Loam would otherwise repeat. DST, the chat dump's argument for Rust, applies to the code Loam writes (D313), and Loam writes the coordination code. Consequences: Loam's evidence about routing correctness is black-box (differential tests, D308); a router bug is fixed upstream or worked around in config. Revisit when any trigger of D317 fires.

ADR-2. Vitess compatibility level: real vttablet in front of the engine, or the tablet contract natively. Decision: real vttablet, unmanaged, v24 (D302). Why: the engine is WeSQL, a real mysqld with binlog commands, GTIDs and performance_schema. Consequences: WeSQL's gaps surface as inventory rows (§9.2), not as Loam code; Vitess's MySQL 8.0 support ends after v24, so WeSQL's rebase to 8.4 becomes a dependency (Q302).

ADR-3. Router license. Decision: Apache-2.0 for everything Loam links (D11, D318). Consequences: no PgDog code anywhere; Vitess code may be ported only into an Apache-2.0 fallback with its notices (D317).

ADR-4. Postgres router path: fork PgDog, or a clean implementation. Decision: neither: PgDog unmodified (D236), with Loam's multi-instance cutover and fence (D305). Why: forking PgDog makes Loam's fork AGPL and a network service, which triggers AGPL §13 (§28 §8); a clean implementation duplicates what PgDog does. Consequences: PgDog's v0.1.x maturity is a product risk (Q305, risk 1 in this document's §18).

ADR-5. Shard-key hashing. Decision: native per router (D303). Why: Vitess tooling and docs transfer only for Vitess keyspaces; for Postgres, PgDog's choice is Postgres's own hash partitioning, so a sharded table matches a hash-partitioned one. Consequences: the shard map has two hash families (§6.1), and the Lean kernel covers both through the same partition lemma (§12).

ADR-6 (new). The MySQL engine. Decision: WeSQL (D301). Why: §3 row 1. Consequences: §29's W1–W4 become RT3's dependencies for anything beyond single-node durability (§17).

ADR-7 (new). Simulation scope. Decision: bit-exact DST for sans-I/O control-plane machines; seeded simulation (D28) for the engine; real-process nemesis tests for engines and routers (D313, D315). Why: §3 row "deterministic async runtime". Consequences: the control plane's machines must not do I/O; the lints of §7.1 enforce it.

6. The shard map and the control planeCopy Anchor Link

6.1 The record (D304)Copy Anchor Link

One record per mapped database, in the TiKV metastore beside §23's x/<ns>/<db> record (the prefix is fixed in RT1 Task 0 against the as-built key layout; proposed xs/<ns>/<db>), postcard-encoded, changed only by compare-and-set on version:

pub struct ShardMapRecord {
    pub version: u64,            // CAS version: every write increments it
    pub generation: u64,         // routing generation: increments when routing changes
    pub engine: Engine,          // Postgres | MySql
    pub router: RouterKind,      // PgDog { database: String } | Vitess { keyspace: String }
    pub scheme: Scheme,
    pub shards: Vec<ShardEntry>, // ordered; index = PgDog `shard` number
    pub state: MapState,         // Serving | Resharding { to: u64 } | CuttingOver { step: CutoverStep } | Fenced
}
pub enum Scheme {
    PgHash { column: String, data_type: PgKeyType, shards: u32 },          // hashint8extended / hash_bytes_extended, mod n
    PgRange { column: String, ranges: Vec<(Bound, Bound, u32)> },          // PgDog [[sharded_mappings]] kind = range
    PgList { column: String, lists: Vec<(Vec<Value>, u32)> },
    Vindex { vindex: VindexKind, ranges: Vec<KeyRange> },                  // hash (DES) | xxhash; keyspace-ID ranges
}
pub struct KeyRange { pub lo: [u8; 8], pub hi: Option<[u8; 8]> }           // [lo, hi), hi = None means the end; Vitess "-80", "80-"
pub struct ShardEntry { pub name: String, pub backend: BackendRef, pub fence: FenceState }

• Generation semantics. A router instance that has applied generation g routes by g's shard list. A backend accepts router writes only while its fence state allows them (§6.4). Generations are never reused.
• Vitess mirror. For a Vitess keyspace the record mirrors SrvKeyspace (read through vtctld) after every Vitess workflow step, so Loam's checkers and the oracle know the current partition. Loam does not write Vitess's topology except through vtctld's API (VSchema apply, workflow commands).

6.2 RenderingCopy Anchor Link

• PgDog (pgdog.toml, users.toml): one [[databases]] entry per shard (name = <db>, shard = i, host, port, database_name, role), [[sharded_tables]] with column and data_type, and [[sharded_mappings]] for range and list schemes. The output is byte-deterministic (golden-file tests), carries the generation in a ConfigMap annotation loam.dev/router-generation, and keeps §28 §8's rules (TLS both hops, SCRAM terminated in PgDog, <db>__<branch> names). cutover_save_config = false: Loam's record, not PgDog's disk, is the truth.
• Vitess: VSchema JSON per keyspace (vindexes, tables, sequences), and vtgate's static auth file (mysql_auth_server_static_file) rendered from the auth plan's credentials (Q30), as users.toml is for PgDog.

6.3 Pushing a generationCopy Anchor Link

The ConfigPush machine (§7.1) moves every router instance to the record's generation: write the ConfigMap (or the compose file in dev), then RELOAD each PgDog instance's admin database, and record each instance's observed generation from the reply and from SHOW CONFIG (verify which admin command reports the loaded file). An instance that restarts reads the ConfigMap, so the ConfigMap is written only when it is safe for any instance to route by it (§6.4). That rule is the main thing ShardMap.tla checks (§11.2).

6.4 Cutover with a backend fence (D305)Copy Anchor Link

PgDog's open-source RESHARD runs schema sync, parallel binary COPY, replication catch-up and a traffic swap on one instance (pgdog/docs/RESHARDING.md, "Traffic cutover via RESHARD is supported on single-node PgDog only"). Loam's orchestration for N instances, as a Resonate saga with deterministic step ids:

1. Copy and catch up on a designated instance d: RESHARD <source> <destination> <publication> against d's admin database; poll SHOW TASKS and SHOW REPLICATION until lag is under the stop threshold. The destination is a second database entry (<db>__reshard_<g>) rendered into every instance at generation g but unused by clients.
2. Pause <db> on every instance (PAUSE <db>), so new queries queue (PgDog's own barrier).
3. Fence the source in Postgres, which is what makes the cutover safe when an instance is unreachable: on every source shard, ALTER ROLE <app_role> NOLOGIN, then pg_terminate_backend for that role's sessions. Any PgDog instance that still routes to a source shard can no longer connect (SQLSTATE 28000) and its in-flight sessions end (57P01), so a write fails instead of being lost, and a stale read fails instead of returning old data. default_transaction_read_only is not a fence: a client's BEGIN READ WRITE or SET overrides it. The replication role PgDog uses for the reverse stream is a different role and is not fenced (Q307).
4. Cut over on d (CUTOVER <task>), which drains and swaps the two databases' identity in d's routing table and starts the reverse stream (pgdog/pgdog/src/admin/cutover.rs, RESHARDING.md "Point of no return").
5. Publish generation g+1 in the record (the destination is now <db>), write the ConfigMap, and RELOAD every other instance.
6. Resume <db> on every instance.
7. Finalize or reverse. Until finalize, the reverse stream keeps the old shards current; a rollback is steps 2–6 in the other direction. Finalize stops the reverse task (STOP_TASK), drops the old computes after a grace period, and clears the fence.

An instance unreachable at step 2 or 5 cannot write to the source (step 3) and, if it restarts, reads the ConfigMap that step 5 wrote. Whether CUTOVER on d plus RELOAD elsewhere gives every instance the same routing is the first thing RT4 verifies on a real PgDog (Q306). Vitess keyspaces use Vitess's own Reshard and SwitchTraffic, which buffer in vtgate and use tablet controls; Loam drives them and mirrors the result (§6.1).

6.5 The in-doubt monitorCopy Anchor Link

PgDog names prepared transactions __pgdog_2pc_[<DEPLOYMENT_ID>_]<instance>_<random> (pgdog/pgdog/src/frontend/client/query_engine/two_pc/transaction.rs), where the instance id is NODE_ID or, without it, 8 random hex digits per process (pgdog/pgdog/src/util.rs). Its coordinator log is a local WAL directory with no checksums ("We didn't add checksums", two_pc/wal/README.md), and without PGDOG_TWO_PHASE_COMMIT_WAL_DIR there is no log at all (verify that no default directory applies). So:

• Deployment rule (D306): a database with 2PC on runs PgDog as a StatefulSet with NODE_ID = the pod ordinal, DEPLOYMENT_ID = <cluster>-<db> and the WAL directory on the pod's persistent volume.
• The monitor (a sans-I/O machine with a Postgres adapter) lists pg_prepared_xacts on every shard every 30 s, groups __pgdog_2pc_ transactions by instance, and raises an alert for any older than 2pc_in_doubt_alert (default 5 min) whose instance is gone or restarted. It never commits or rolls back a transaction: without the coordinator's log it cannot know the decision, and CrossShardCommit.tla shows that guessing violates atomicity (§11.2). An operator resolves with the shard data in view, through a documented runbook.

7. Trait seamsCopy Anchor Link

7.1 Sans-I/O machines (operon-sqlrouter)Copy Anchor Link

The kernel crate has no dependency on tokio, sockets, files or clocks. Its clippy.toml (read from the crate directory) adds disallowed-methods for std::time::{Instant, SystemTime}::now, rand::rng, rand::thread_rng, std::thread::spawn and std::env::var, and the crate has no tokio in its Cargo.toml. Every protocol is a machine:

pub struct Ctx<'a> {
    pub now: Millis,                      // supplied by the driver: real clock or simulated clock
    pub rng: &'a mut dyn rand::RngCore,   // supplied by the driver: seeded in simulation
    pub trace: &'a mut dyn TraceSink,     // spec events (D311)
}
pub trait Machine {
    type Input;
    type Output;
    /// Consume one input and return the commands to execute. Never blocks, never does I/O.
    fn on(&mut self, ctx: &mut Ctx<'_>, input: Self::Input) -> Vec<Self::Output>;
}
pub trait TraceSink { fn emit(&mut self, event: SpecEvent); }
pub struct SpecEvent { pub spec: &'static str, pub action: &'static str, pub fields: Vec<(&'static str, SpecValue)> }

Machines in RT1–RT2: ConfigPush (§6.3), InDoubtMonitor (§6.5), and the kernels ranges (partition, split, merge, lookup), hash (Postgres hashint8extended/hash_bytes_extended ported from PostgreSQL's src/common/hashfn.c under the PostgreSQL License with its notice, never from PgDog's copy; Vitess hash through the des crate; xxhash through xxhash-rust), render (PgDog and Vitess files) and reference (k-way merge, LIMIT/OFFSET, aggregate decomposition: the Rust mirror of the Lean oracle, used by checkers and differential tests, never on a routing path). RT4 adds Cutover (§6.4) and FailoverRepoint.

The chat dump's simulation seams map onto this: Clock and Rng are Ctx fields; Network, Disk and Spawn do not exist inside a machine, because outputs are commands that the driver executes (tokio adapters in production, the scheduler in simulation).

7.2 I/O seams (operon-sqlrouter-io)Copy Anchor Link

#[async_trait]
pub trait ShardMapStore: Send + Sync {
    async fn read(&self, db: &DbRef) -> Result<Option<ShardMapRecord>, StoreError>;
    async fn cas(&self, db: &DbRef, expect: Option<u64>, next: &ShardMapRecord) -> Result<u64, StoreError>; // Conflict { current }
    async fn watch(&self, db: &DbRef, after: u64) -> Result<ShardMapRecord, StoreError>;                    // long poll
}
#[async_trait]
pub trait RouterInstance: Send + Sync {
    fn id(&self) -> &InstanceId;
    async fn apply(&self, generation: u64, files: &RenderedFiles) -> Result<Applied, RouterError>;
    async fn pause(&self, database: &str) -> Result<(), RouterError>;
    async fn resume(&self, database: &str) -> Result<(), RouterError>;
    async fn observe(&self) -> Result<Observed, RouterError>; // version, generation, peers, tasks
}
#[async_trait]
pub trait ShardBackend: Send + Sync {
    async fn status(&self) -> Result<BackendStatus, BackendError>;          // role, read-only, lag, LSN/GTID
    async fn fence_writes(&self, role: &str) -> Result<(), BackendError>;   // §6.4 step 3
    async fn unfence_writes(&self, role: &str) -> Result<(), BackendError>;
    async fn prepared(&self) -> Result<Vec<PreparedXact>, BackendError>;    // pg_prepared_xacts
    async fn checksum(&self, table: &str, by: &ShardFn) -> Result<TableDigest, BackendError>; // split verification
}

Implementations: ShardMapStore for memory and TiKV (operon-tikv's TxnRunner); RouterInstance for PgDog's admin database (tokio-postgres, simple query protocol) and, in RT3, vtgate/vtctld; ShardBackend for Postgres (Loam Postgres computes and CNPG) and, in RT3, WeSQL. Each has a simulation model in operon-detsim and a contract suite (D316).

7.3 Fallback seams (D317), specified and not builtCopy Anchor Link

If D317's triggers fire, the chat dump's router architecture applies, behind these traits, sharing §7.1's kernels and §7.2's ShardMapStore and ShardBackend:

pub trait Frontend { type Conn; fn accept(&mut self, ctx: &mut Ctx<'_>, bytes: &[u8]) -> Vec<FrontendEvent>; }   // MySQL or Postgres wire, sans-I/O
pub trait Dialect  { fn parse(&self, sql: &str) -> Result<Statement, ParseError>; fn shard_keys(&self, stmt: &Statement, map: &ShardMapRecord) -> Route; }
pub trait Planner  { fn plan(&self, stmt: &Statement, route: &Route) -> Result<PlanIr, PlanError>; }
pub trait Executor: Machine<Input = ExecInput, Output = ExecCommand> {}   // route, scatter, merge, 2PC
pub trait BackendPool { fn checkout(&mut self, ctx: &mut Ctx<'_>, shard: u32, read: bool) -> PoolCommand; }

They exist on paper so that RT1's seams do not paint the fallback into a corner.

8. Loam Postgres as a shard (D307)Copy Anchor Link

9. WeSQL as a shard behind Vitess (D301, D302)Copy Anchor Link

9.1 ShapeCopy Anchor Link

• One unmanaged vttablet per WeSQL primary (and per replica, as replica tablets, once W3 exists), with --unmanaged, --db-host, --db-port, the app and DBA users, --init-keyspace, --init-shard. Vitess does not manage WeSQL's process, backups or replication; Loam (§29) does.
• Binlog requirements that VReplication needs, which §29 already sets: binlog_format = ROW, binlog_row_image = FULL, and gtid_mode = ON with enforce_gtid_consistency (W2 requires it, §29 §6.2). The §23 spike ran with gtid_mode = OFF, so the default changes for Vitess-fronted WeSQL.
• Failover: W3 promotes a replica (§29 §7.3). Step 5, "repoint", becomes vtctldclient TabletExternallyReparented <new-primary-tablet> for the shard, plus the x/ record change (D320 amends §29 §7.2's "router follows the record").
• Front end: vtgate, also for unsharded keyspaces (D320). Database name = keyspace.

9.2 What is already known to need checkingCopy Anchor Link

10. Cross-shard semantics (D306, D322)Copy Anchor Link

The DST and nemesis checkers check exactly this table: snapshot isolation per shard for the list-append workload, conservation only for 2PC-enabled bank transfers, and fractured reads allowed across shards.

11. Formal specifications (TLA+)Copy Anchor Link

11.1 Tools and layout (D310)Copy Anchor Link

• spec/tla/router/<Spec>.tla, a model file MC<Spec>.tla and one or more MC<Spec>_<variant>.cfg per spec, as Neon's safekeeper/spec/ is laid out (Apache-2.0, used as the reference layout and, for the Postgres half of PrimaryFailover, as the model of walproposer's Paxos, cited and not copied).
• scripts/spec/check.sh <Spec> [<variant>] runs TLC (v1.7.4 by default, the jar pinned by SHA-256 in the script) with -workers 2 -deadlock, and Apalache v0.62.3 check --inv=<Inv> --length=<k> for the invariants marked inductive. Bounds and the time each run takes are recorded in the spec's header.
• CI job tla (path-filtered on spec/tla/**): every spec at its PR bounds; nightly at larger bounds. A variant marked EXPECT_VIOLATION must fail with the named invariant, which keeps known-unsafe configurations documented and tested.

11.2 The specsCopy Anchor Link

11.3 Trace validation and the action-to-code map (D311)Copy Anchor Link

• Emitting. Every machine reports each transition it takes as a SpecEvent through Ctx::trace. Drivers write them as JSON lines ({"spec":"ShardMap","action":"Reload","instance":"pgdog-1","gen":4,"ok":true,"t":1234}): operon-detsim to its run directory, the production driver to tracing target loam::spec (off unless LOAM_SPEC_TRACE=<path>).
• Checking. spec/tla/router/<Spec>Trace.tla reads the file with the CommunityModules Json module and constrains the spec's Next so each step matches the next event (the trace-validation method of Cirstea, Kuppe, Loillier, Merz and others, "Validating Traces of Distributed Programs Against TLA+ Specifications", 2024). TLC either finds a behaviour of the spec that explains the trace or reports the first event it cannot explain. Fields the code cannot observe (another instance's state) are left unconstrained.
• Coverage. A test in operon-sqlrouter parses each spec's action list from its header and fails if an action has no SpecEvent emitter in code, or an emitter names an action the spec does not have.

The map for ShardMap (the others follow the same form in their headers):

12. Lean 4 kernels and the differential oracle (D312)Copy Anchor Link

12.1 ScopeCopy Anchor Link

Hash functions (DES, Postgres's Jenkins hash, xxhash) are not modelled in Lean: they are checked by reference vectors in Rust (§7.1), generated from a real Postgres (SELECT hashint8extended(k, seed)) and from Vitess's own tests (vitess/go/vt/vtgate/vindexes/hash_test.go, Apache-2.0, vectors copied with the notice).

12.2 The oracleCopy Anchor Link

• lake build oracle builds loam-router-oracle, which reads JSON lines on stdin ({"op":"merge","order":[…],"shards":[[…],…]}, {"op":"aggregate",…}, {"op":"partition_check",…}) and writes one result per line.
• Rust side. operon_sqlrouter::reference implements the same functions; proptest properties mirror the Lean theorems for fast CI; a differential test (reference_matches_lean_oracle, 10 000 cases on PRs that touch either side, 100 000 nightly) feeds both the same random inputs. Without the oracle binary on PATH the test prints skipped: needs loam-router-oracle (the cluster-test convention of R1).
• Against the routers (RT2): a query runs on unsharded Postgres, through PgDog over 2 and 4 shards, and its per-shard results go through the oracle; three answers are compared. Deviations a router documents are listed in conformance/router/pgdog-cross-shard-allowlist.toml with the source of the documentation.
• The gap, stated as the chat dump asked. Lean proves the model; the differential tests are what connect the model to Loam's Rust reference and to the routers' behaviour. Neither router's code is proved.

12.3 CICopy Anchor Link

Job lean (path-filtered on spec/lean/** and crates/operon-sqlrouter/src/reference/**): elan with the pinned lean-toolchain, lake build, lake exe plausible-check, then the differential test. Lake's build directory is cached by lean-toolchain and lake-manifest.json (Q308).

13. Deterministic simulation (D313, D314)Copy Anchor Link

13.1 TiersCopy Anchor Link

operon-detsim is its own small crate (rand_chacha, serde_json, operon-meta-conformance for the linearizability checker) so the router's tests do not build operon-sim's Lance and DataFusion dependencies. operon-sim re-exports its checkers.

13.2 The schedulerCopy Anchor Link

• One RNG (ChaCha8Rng from the seed) decides every choice: the next event among the ready ones, message delays, drops, duplicates, reorders, fault firings, workload operations.
• Simulated time advances only by events. Machines see it through Ctx::now.
• Network model: per directed link a queue with delay distribution, drop and duplicate probabilities, and partition state (symmetric and asymmetric); a "slow link" multiplies delays; a reset fails in-flight requests with an indeterminate outcome.
• Fault points (buggify): detsim::fault_point!("pgdog.reload.after_parse") in model code; each run enables a random subset of named points (swarm testing) and each enabled point fires with its own probability.
• Trace hash: SHA-256 over the canonical JSON of every scheduled event. CI runs each corpus seed twice and fails if the hashes differ.
• Shrinking: a failing run's schedule (the list of chosen events and fault firings) is minimized by delta debugging over fault firings and workload operations, replayed with the same seed, until no smaller schedule fails. The report prints the seed, the enabled faults and the shrunk schedule, in SimReport's format (D28).

13.3 Fault catalogCopy Anchor Link

The chat dump's catalog (§7.2), each fault mapped to where it is injected and when it arrives.

13.4 Workloads and checkersCopy Anchor Link

Every run asserts that no acknowledged commit is lost and no committed transaction is partially visible where atomicity is promised (§10).

13.5 CI policyCopy Anchor Link

• Pull requests (job router-sim, path-filtered on crates/operon-sqlrouter*/** and crates/operon-detsim/**): the regression corpus (crates/operon-sqlrouter/tests/sim/corpus/*.seed) twice each with trace-hash equality, plus 2 000 fresh seeds per scenario (ROUTER_SIM_SEEDS), within 10 minutes (estimate: a pure machine step costs microseconds; a 500-step run, a few milliseconds).
• Nightly: 1 000 000 seeds across scenarios with swarm configuration, split over the matrix (Q310); 100 sampled traces through trace validation; the Lean differential at 100 000 cases; Apalache at nightly bounds.
• A failing nightly seed files an issue (gh issue create, label sim-failure) with the seed, the enabled faults and the shrunk schedule. The fix's PR adds the seed to the corpus; a seed is never removed.

14. Real-system testsCopy Anchor Link

14.1 Contract suites (D316)Copy Anchor Link

shard_backend_conformance!(Backend) and router_fleet_conformance!(Fleet) expand the same cases against the model and the real thing: role and read-only reporting, fence then write fails with the documented error, unfence restores, prepared transactions listed with their gids, checksums equal for equal data, RELOAD applies a generation, PAUSE queues and RESUME releases. Real backends: Postgres 17.11 in CI, Loam Postgres computes from deploy/neon once P2b is merged, WeSQL in RT3.

14.2 Differential testsCopy Anchor Link

The same seeded SQL stream against an unsharded engine and the sharded stack, results compared (row multiset, or order when ORDER BY is total), with the oracle as the third opinion for merges and aggregates (§12.2). Postgres in RT1 (single-shard) and RT2 (scatter, merge, aggregate); MySQL in RT3.

14.3 Nemesis runs (RT5)Copy Anchor Link

operon-nemesis composes the stack (compose for the PR-sized run, k3d nightly), runs Tier 1's workloads through real clients (tokio-postgres, mysql_async), injects Tier 3 faults, and runs the same checkers on the recorded history. Online resharding under load checks table checksums at each step. Performance baselines (routing overhead, scatter latency, cutover duration, commit latency on the bucket-backed logs) are recorded, not gated, at first.

15. The compatibility inventory method (D309)Copy Anchor Link

The inventory is the spec of what an engine must answer for a router. It is built the same way for both halves:

1. Static extraction. List every statement and command the router or its tablet sends to the backend, from its source: string constants and query builders, flavor files, sidecar DDL, health checks, replication and schema-engine queries. For Vitess: go/mysql/flavor_mysql*.go, go/vt/vttablet/tabletserver/schema/, go/vt/vttablet/tabletmanager/, go/vt/vttablet/tabletserver/vstreamer/, go/vt/vttablet/tabletmanager/vreplication/, go/vt/sidecardb/schema/**. For PgDog: pgdog/src/backend/{replication,schema,pool}/ and the 2PC module (read as a reference; the inventory records statements and source paths, never PgDog code).
2. Dynamic capture. Run the router's own suites against the reference engine with statement logging: Vitess's examples/local and selected go/test/endtoend/ packages against MySQL 8.0.46 with performance_schema.events_statements_summary_by_digest; PgDog's integration/ suites (resharding, logical, failover, pgbench, rewrite) against Postgres 17.11 with log_statement = 'all' and pg_stat_statements. Normalize to digests.
3. Merge the static and dynamic lists into one table keyed by digest, with the component that issues each statement.
4. Replay and classify each digest (with its captured example and session state) against the target engine (WeSQL; Loam Postgres) and the reference: same (identical result, warnings and errors), differs (result or metadata differs), error (target errors), unsupported (target refuses by design, with the reason). Results compare by a canonical hash.
5. Suite pass rates. Run the selected suites through the router against the target; record pass, fail and skip per test, and link each failure to inventory rows.
6. Bless the tables as TSV files (conformance/router/{vitess-wesql,pgdog-loampg}-statements.tsv with columns digest, component, source, example, class, ref_hash, target_hash, note, issue, where the two hashes are the canonical result hashes of step 4; …-suites.tsv with suite, test, result, rows). A PR that changes a pinned version re-runs the inventory and shows the diff.
7. Gate. RT3's gate for D302 (proposed): no error or differs row in the components Loam uses (query service, health, schema engine, VReplication for MoveTables and Reshard), and the suite pass rates in §17's RT3 row. Rows in components Loam does not use are recorded, not gating.

16. Licenses (D318)Copy Anchor Link

17. Roadmap: track RT (D319)Copy Anchor Link

Each phase is small stacked PRs. RT adds crates and CI jobs and changes no M-track code path.

18. RisksCopy Anchor Link

19. Open questionsCopy Anchor Link

20. Contradictions with earlier decisions, and how they are resolvedCopy Anchor Link

21. SourcesCopy Anchor Link

Read on 2026-10-01.

• Chat dump: chatdump.md lines 54–322.
• PgDog (pgdogdev/pgdog at 80d6059d, AGPL-3.0, read as a reference): docs/{SHARDING.md,RESHARDING.md,REPLICATION.md}; pgdog/src/admin/{cutover.rs,pause.rs,reload.rs,show_peers.rs}; pgdog/src/frontend/client/query_engine/two_pc/{mod.rs,manager.rs,transaction.rs,wal/README.md}; pgdog/src/util.rs (instance_id, deployment_id); pgdog-config/src/general.rs (two_phase_commit*); integration/ directory list. GitHub API: license AGPL-3.0, release v0.1.60 (2026-09-24).
• Vitess (vitessio/vitess, Apache-2.0, through the GitHub API): go/vt/sidecardb/schema/{twopc,vreplication}/*.sql; go/vt/sidecardb/sidecardb.go; go/vt/vttablet/tabletserver/{dt_executor.go,tx_engine.go}; go/vt/vtgate/vindexes/hash.go; doc/design-docs/AtomicDistributedTransaction.md; releases v22.0.0 (2025-04-29), v23.0.0 (2025-11-04), v24.0.0 (2026-04-30), v24.0.4 (2026-10-01). vitess.io/docs/24.0: "Supported databases", "Distributed transactions", "Unmanaged tablet".
• Neon (neondatabase/neon, Apache-2.0): pageserver/src/pgdatadir_mapping.rs; test_runner/regress/{test_twophase.py,test_logical_replication.py}; safekeeper/spec/{ProposerAcceptorStatic.tla,ProposerAcceptorReconfig.tla,readme.md}.
• WeSQL (ostrium-labs/wesql at eef34f452): mysql-test/suite/smartengine_consistent_snapshot/t/default_storage_engine.test; semi-sync tests under mysql-test/suite/smartengine_rpl_*.
• Tools: GitHub API for tlaplus/tlaplus (MIT; v1.7.4 stable, v1.8.0 rolling pre-release), apalache-mc/apalache (Apache-2.0; v0.62.3), leanprover/lean4 (v4.34.1), leanprover-community/plausible (Apache-2.0), madsim-rs/madsim (Apache-2.0), tokio-rs/turmoil (MIT), jepsen-io/elle (EPL-2.0); crates.io for madsim 0.2.34, turmoil 0.7.2, proptest 1.11.0, des 0.9.0, xxhash-rust 0.8.19. Trace validation: H. Cirstea, M. A. Kuppe, B. Loillier, S. Merz et al., "Validating Traces of Distributed Programs Against TLA+ Specifications" (2024).
• Loam: §12 §2; §18 §5; §20 §10, §14; §21; §23 §6.3, §6.4, §9; §28 §4, §5, §7.2, §8, §11; §29 (PR #172) §4, §6, §7, §9; D11, D28, D148, D153, D154, D236, D260, D264, D273–D280; Q260, Q274.