test: Make the DST more robust (#116)

This commit is contained in:
Marcelo Mendonça Soares 2026-09-14 10:26:56 -03:00 • committed by GitHub
commit 574f8d067a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -10,9 +10,9 @@ generate scenarios nobody wrote down and assert invariants.
## Running
These suites carry the `dst` tag and are skipped by an ordinary `dart test`,
because they are slow and because a randomly seeded search makes a poor
edit-loop signal — a run can fail for a defect unrelated to the change that
The randomized sweeps carry the `dst` tag and are skipped by an ordinary
`dart test`, because they are slow and because a randomly seeded search makes
a poor edit-loop signal — a run can fail for a defect unrelated to the change that
triggered it. The `dst` preset opts back in:
```sh
@ -21,6 +21,9 @@ DST_SEEDS=200 DST_ROUNDS=40 dart test -P dst # soak
DST_SEED_BASE=1781161784 DST_SEEDS=1 dart test -P dst # replay one seed
```
The deterministic oracle, operation-generator, and runner regressions in this
directory are untagged and run with ordinary `dart test`.
| Variable | Default | Meaning |
| --- | --- | --- |
| `DST_SEEDS` | 8 | How many seeds the sweep runs |
@ -52,9 +55,10 @@ the failure and replay it.
| Property | When it is checked |
| --- | --- |
| **Observer independence** - a scope looks identical to every replica holding it, whatever *other* scopes that replica holds | At quiescence |
| **No cross-scope link** - no visible foreign key resolves to a row owned by another scope | After every merge |
| **Foreign-key closure** - every visible foreign key resolves to a visible parent in the same scope | After every merge |
| **Unique closure** - no visible unique index is violated | After every merge |
| **No cross-scope link** - no visible foreign key resolves to a row owned by another scope | After every local commit and merge |
| **Foreign-key closure** - every visible foreign key resolves to a visible parent in the same scope | After every local commit and merge |
| **Unique closure** - no visible unique index is violated | After every local commit and merge |
| **Projection purity** - FK fields and recorded overrides satisfy the oracle's repair rules, including permitted terminal unique releases | After every local commit and merge |
| **Ownership collision is terminal** - a merge claiming another scope's row id fails, records a durable violation, and leaves the owner untouched | `dst_ownership_collision_test.dart` |
Observer independence is the keystone. A synced row may only reference synced
@ -113,12 +117,47 @@ idempotence gets probed.
| File | Role |
| --- | --- |
| `framework/dst_random.dart` | Seeded randomness, identifiers, clock, sweep config |
| `framework/dst_world.dart` | Replicas, the simulated table graph, operation generation |
| `framework/dst_world.dart` | Replicas and operation generation |
| `framework/dst_schema.dart` | Generated model adapters and declared unique indexes |
| `framework/dst_adversary.dart` | Delivery scheduling and quiescence |
| `framework/dst_snapshot.dart` | Canonical snapshots and the property oracle |
| `framework/dst_runner.dart` | One seeded run, and failure reporting |
The simulated world is five tables chosen to cover every foreign-key action and
both unique-index shapes in one small graph: `town.cityId` is cascade,
`town.mayorId` is set-null, `address.inhabitantId` is restrict and carries the
foreign-key-only global unique index, and `unique.name` is unique per scope.
The simulated graph includes nullable and required cascade, no-action,
set-null, and set-default references, the mixed cascade/no-action chains, and
all outbound references of person and organization. Person, company, and town
can form a cycle. Foreign-key actions, nullability, and defaults are read from
the generated schema; every domain FK of a simulated model is included.
The operation generator selects columns from that same schema. Nullable FKs
can be detached explicitly even when a parent is available. New required FK
values are only generated when a visible parent exists. The well-known default
town is inserted in one scope because row IDs are globally unique.
Projection purity checks every FK field, including fields without a sparse
attempted-value record. A hidden child can retain its authored reference to a
physically present parent in the same scope when its action has no legal repair;
it does not block that parent's deletion. Hidden values are recomputed, so an
earlier projected fallback is not frozen in place. Visible non-null references
must still resolve to visible parents in the same scope. FK repair reasons must
match the action and nullability; FK columns in unique indexes may instead carry
a terminal unique-conflict or hidden-row release reason.
These checks validate the resulting fields and reasons against the observed
visibility. They do not independently recompute deletion arbitration or unique
winners. Replica agreement, export round trips, and the integration suites'
exact expected outcomes provide additional checks; a finite seed sweep is not
a proof for every possible merged history.
The unique simulation authors and captures text, non-FK UUID, nullable integer,
composite, fixed-discriminator, overlapping, FK-only composite, and scoped mixed
FK/text claims. The unique oracle reads all declared tuple components and scope.
A null component releases the tuple, as in SQL.
The operation generator can insert, update, delete, restore a retained identity,
upsert, pass a full model back through update, insert/update/delete a batch,
swap unique tuples atomically, and perform predicate updates/deletes. Scripted regressions
use `DstOperations.apply` to select the same paths directly. Reports retain
attempted and committed counts by table/action so a passing run does not hide
which paths it visited. Rejected local transactions remain separate from
committed operations.