Fidelity¶

Every invariant DST proves is proven against the in-memory mock — so the honest question is always "and does the mock behave like the real engine?". This page is the measured answer, in two layers: the anomaly matrix (does the mock agree with real Postgres and Mongo on classic isolation phenomena, per level?) and the bug transfer (do the mock's verdicts on known bugs hold on the real engine?). Both are regenerated artifacts, never prose claims — just dst-fidelity and just dst-transfer re-run the differentials and rewrite the tables below.

DST fidelity matrix¶

Mock↔real verdict agreement for the isolation anomaly battery, per backend and IsolationLevel. ✓ = both backends produce the same verdict; ▲ = mock stricter (mock prevents, real permits — the false-confidence direction: simulation green, production bleeds); △ = mock weaker (mock permits, real prevents — the false-alarm direction: simulated violations reality cannot produce). A divergence is admissible only when a reviewed engine-scoped catalog entry explains it; an unexplained divergence fails the differential. There is deliberately no single agreement score.

Generated by just dst-fidelity — do not edit by hand.

mock ↔ postgres¶

Divergences — mock-stricter (▲): 0 · mock-weaker (△): 0 · unexplained: 0

mock ↔ mongo¶

Divergences — mock-stricter (▲): 0 · mock-weaker (△): 4 · unexplained: 0

Contract strengthenings (reviewed)¶

A Forze adapter prevents an anomaly the textbook contract permits — the only sanctioned way an observed verdict may deviate from the textbook, and the only thing that may explain a mock↔real divergence above.

Mechanism divergences (normalized, never verdict-level)¶

Surface differences between correct engines that the differential normalizes away before a verdict exists — listed for completeness; they can never explain a verdict divergence.

Corpus bug transfer¶

Mock↔real verdict pairs for every transferable misuse-corpus instance: the same hand-authored provocation (a forced port-level interleaving, a re-invocation, or a documented crash analog) runs on both backends, and the same final-state predicate — read back through the ports — decides detected/clean on each. ✓ = the verdicts agree; ▲ = mock artifact (mock detects, real clean — everything DST catches via that mutant is noise); △ = mock blind spot (real bleeds, mock clean — the dangerous direction: DST would green-light a real bug). There is no allowed-divergence catalog on this plane — any divergence is a finding.

Generated by just dst-transfer — do not edit by hand.

mock ↔ postgres¶

Instances: 19 mutants + 18 controls · mock artifacts (▲): 0 · mock blind spots (△): 0

Controls (expected clean on both backends)¶

Not transferable — 1/20 mutants¶

Defects whose trigger or observable needs simulation-only machinery; their ground_truth stays undetermined by design, and the fraction is stated so a capped denominator never reads as full coverage.

Does anomaly divergence predict bug divergence?¶

The pre-registered predictor question: are matrix cells where the mock disagrees with the real engine on an isolation phenomenon also where corpus bugs fail to transfer? Protocol fixed before the data existed — each transferable mutant is mapped to the battery phenomenon its defect manifests through, its postgres cell is read at READ_COMMITTED (the level the corpus workloads run under), and the 2×2 is tested with the exact Fisher test. Both outcomes were committed to in advance: a predictive proxy (run the battery, trust the corpus) or a non-predictive one (the corpus-on-real run stays load-bearing).

Generated by just dst-transfer — do not edit by hand.

Mapped mutants¶

The contingency table¶

Fisher exact (two-sided): p = 1.

Verdict¶

The data lands in the degenerate branch: the postgres matrix has zero divergent cells and the corpus run had zero transfer divergences, so both margins of the table are empty on one side and the test carries no evidence either way (p = 1 by construction). What the run does establish: every mutant in a battery-clean cell transferred — the hypothesis's clean-cell branch is consistent with all observed data — but the divergent-cell branch is unexercised, so the proxy's predictive power is untested, not confirmed. Per the pre-registered commitment, the conservative conclusion stands: the corpus-on-real run stays load-bearing; the battery is not certified as its substitute.

Outside the proxy's domain — 10/19 transferable mutants¶

These defects do not manifest through any isolation phenomenon, so anomaly conformance could never predict their transfer even in principle — for this part of the corpus the battery is not a proxy at all, only the transfer run speaks. This bound on the proxy's domain is itself a finding of the analysis.

With a corpus this size the test is underpowered for subtle effects; the association worth acting on is the strong kind — a divergent cell with multiple diverging mutants — and none was observed.

Bugs the harness found in Forze itself¶

The strongest evidence is provenance. A git-history audit found three confirmed harness-found bugs — all surfaced by the conformance differential, which is exactly the component this page measures:

• The mock's write-through dirty read. The default mock transaction manager let a concurrent transaction read another's uncommitted, later-rolled-back write — weaker than real read-committed. Found by the dirty_read battery case; fixed by buffering every write through the MVCC overlay. Pinned forever by the battery.
• The revision-conflict kind divergence. On a stale-revision write the mock raised a different exception contract than every real adapter — an app's optimistic-concurrency handling would behave differently on the mock than in production. Found by the real-Postgres differential doing precisely its job; the mock (the outlier) was fixed to match.
• The rev-guarded double charge. Making read-committed faithful exposed that two concurrent rev-guarded updates could both commit — a double charge. Fixed with first-committer-wins write-write rejection; the payments example's oracle keeps it caught.

The framing matters: these are differential catches, not seed-search catches — which is exactly what the tables above are for. Claiming more would be the overreach this page exists to prevent.

Which planes have a leg¶

A differential is only evidence for the plane it runs on, so the next question after "does the mock agree?" is "agree about what?". That answer is a manifest rather than a paragraph: [tool.conformance_manifest] in pyproject.toml names every plane, the scenario it runs, the contract ports it covers and the engines it must run against. just conformance-check (part of just quality) enforces it, and just conformance runs the legs themselves.

The manifest exists because the previous answer was prose, and prose does not fail a build. A plane could gain a backend whose only test ran against that backend alone, with nothing comparing it to anything, and CI stayed green. So the checker derives which packages actually register each plane's ports — from the integration packages, not from a list somebody maintains — and fails when one of them runs no leg. Adding a backend now means adding its leg or writing down, in the manifest, why there isn't one.

That check runs before the suite does, so it can only prove a leg exists. Existing is not running: a leg whose engine never starts, whose optional extra is missing, or whose suite is absent from CI's matrix skips quietly, and a skipped test looks exactly like a passing one in a green pipeline. So each CI shard also records what it actually ran, per leg, and a final job unions those records and fails on any manifested leg that passed nothing anywhere. That gate earned its place immediately: it found that two of the four inference legs, and the whole portability suite, had never run in CI at all. Individual skips inside a leg stay allowed — a check that cannot apply to an engine should skip with a reason naming it — but they are reported, so a leg quietly hollowing out one check at a time stays visible.

Uncovered planes are declared rather than omitted, which is the part worth reading:

Read that table as the honest complement to the green matrices above: those planes are tested, they are simply not compared.

Deriving the requirement from the code is what keeps that table honest, and one plane needed help to manage it. Field encryption's ports are resolved by the adapters that seal values rather than registered by a backend, so the census sees no providers for them — and a derivation that finds nothing requires nothing, which is a ratchet that cannot fail. The manifest lets such a plane name a proxy instead (derive_from), and here the proxy is exact rather than approximate: the battery is document-plane specific, so "which backends need a field-encryption leg" is "which backends provide a document port". A misspelled proxy key is a hard error for the same reason — it would derive from nothing and look like success.

Known differences that are real and expected live in forze_dst.conformance.catalog as data, not prose. Each row records what each engine did, what was done about it (unified, normalized, or declared), and a probe naming the test that asserts it — a link the checker resolves against real pytest collection, so a catalog entry cannot outlive the test behind it.

One row is worth reading for a different reason: it records a case where the oracle could not be wrong, because it could not model the outcome at all. The storage port lets a caller ask list(missing_ok=False) so a vanished bucket can be told from an emptied one — the distinction the re-encryption sweep is built on. The mock reached its bucket through setdefault, so the bucket existed the instant anything looked at it and the parameter was documented as a no-op. That is a stronger failure than "untested": no test written against that oracle could have failed, so every mock-backed test of the contract was green without exercising anything. Closing it meant giving the mock the concept first — reads never provision, the documented write paths do — and the sweep's own test then had to say which state it meant, having asserted "empty" while exercising "absent". The leg then went a step past the raise: missing_ok=True still reports container_missing on the page it returns, because tolerating an absent bucket should not mean being unable to see one. With per-tenant buckets that is the difference between a tenant nobody provisioned and a tenant that has uploaded nothing, and every backend in the leg — MinIO, floci, GCS, the mock — is held to it.

A third row records the one interaction none of this page's other machinery can reach. The offline mailbox bounds a reconnect replay by a retention cap, and clients ack cumulatively — "I have everything up to this id". Each is fine alone; together, a replay that delivered an incomplete window plus an ack on a live frame lets the cursor jump the gap, and the trim floor then deletes signals that were never sent. Nothing raises. Simulation cannot find it either, because the race lives in document-port code rather than stream code, so no schedule the explorer drives will interleave it. The leg drives that interleaving directly against the mock, Postgres and Mongo, and its controls reconstruct the fault by truncating the replay — so the check is known to fail when the guarantee does, rather than merely passing today.

One divergence there is worth reading as a pattern rather than an entry. The inference port is declarative: each adapter publishes an InferenceCapabilities and the shared validators gate requests against it, so "does this call get through?" is a property of the declaration, not of the model behind it. A mock told nothing advertises the full surface — unbounded batches, streaming, async jobs — which is true of the mock and truer than any backend it stands in for, so a capability gate that passes against the oracle can still refuse in production. The fix is a wiring obligation (MockInferenceRegistry.on(..., capabilities=…)) and it cannot be defaulted away, because the mock is also used where no backend is being mirrored at all. So the differential carries it instead: the battery compares a backend's gates against a mock built from that backend's own declaration, and asserts that an untold oracle disagrees — which is what makes forgetting the wiring fail at authoring time rather than in production.

What these numbers license — and what they don't¶

• A green matrix licenses trusting the mock for the phenomena, levels, and backends tested — the isolation family on Postgres and Mongo. It says nothing about untested planes, and the gap table is where those are named.
• The transfer table is the direct evidence, at found-bug granularity — and its N is what it is: every transferable corpus instance, currently against Postgres.
• The transfer leg's zero is not a sampling result, and no interval will ever be attached to it. Elsewhere in DST a zero comes with a bound, because it is a zero out of repeated independent draws: detection statistics can say "0 violations in 1000 seeds licenses < 0.30%" precisely because there were 1000 chances. Here each transferable mutant runs once per backend under a deterministic verdict predicate. There is no repetition, no rate, and — because the corpus is hand-authored rather than sampled from the population of real defects — nothing a frequentist interval could be an interval over. "Does the mock's verdict hold on the real engine?" is an epistemic question, and a binomial bound on "0 divergences in K mutants" would be a category error dressed as rigour. The honest artifact is the list of what has been checked and the gap table naming what has not: untested, not confirmed.
• The pre-registered predictor analysis is currently uninformative by construction (zero divergence on either plane), so the battery is not certified as a substitute for the transfer run — and for the corpus's non-isolation half it could never be one.
• Logic below the port — triggers, generated columns, database views — is outside every oracle here. An invariant maintained by a trigger must be covered by an integration test, not by simulation — and that exclusion is now checkable, not just prose: declare it with a HorizonDeclaration naming the covering test, and per-invariant accounting keeps the clean verdict scoped to invariants the harness has been shown able to catch (see what a green run doesn't say).
• A divergence is admissible only through the reviewed catalogs above; an unexplained one fails the build. There is deliberately no single "fidelity score" anywhere on this page — the two divergence directions have opposite costs, and averaging them would hide exactly the one that ships bugs.