# dgen_registry Formal Model

A TLA+ model of the replication protocol in
[`src/dgen_registry/dgen_registry_member.erl`](../src/dgen_registry/dgen_registry_member.erl)
(design: [`docs/design/dgen_registry_design.md`](../docs/design/dgen_registry_design.md)
§4.5, §5). TLC checks its safety properties against every interleaving of a
small bounded cluster. Tests can only sample interleavings; the
[simulation harness](../test/support/sim/dgen_registry_simulation.md) covers the
other side: it checks that the real code implements this protocol.

## What it models

One module, `DgenRegistryReplication.tla`:

- **Fenced commit**: the leader is the only writer. A commit succeeds only if
  the durable leader key and epoch still match.
- **Version-stamped broadcasts**: one per commit version, carrying `{Epoch,
  PrevVersion, Version}`. Followers apply only contiguous broadcasts.
- **Resync**: a follower with a gap requests a snapshot from its stream's
  sender.
- **Forwarded registrations, version-guarded acks**: a follower answers its
  caller only after its replica has applied the batch, in the epoch that
  committed it (`EpochFencedAck`).
- **Direct registrations, replicate-before-ack**: the leader waits for a
  follower to confirm before answering `yes`. The degrade-open timeout is a
  constant.
- **Leadership handoff** (§5.7): the new leader gathers the freshest live
  replica and fans out a snapshot. Two separate constants guard it: the
  durable-version-key fence on the gather (`SafeAssumeGather`) and the
  version-monotonic snapshot apply (`SafeAssumeSnap`).
- **Replication heartbeat**: the leader's periodic empty batch stamped
  `{Applied, Applied}`, which reveals a gap even when there is no traffic. At
  most one is in flight per leader. A deposed leader that hasn't been told yet
  can still send one, and that case is checked.
- **Failures**: member crash (bounded by `MaxCrashes`) and message loss with
  Erlang's signal ordering (per-pair FIFO, arbitrary loss).

**Deliberately out of scope**: unregister, retract and `DOWN` cleanup; the
§5.6 conflict trail and kill budget; metadata, queries and presence; membership
joins and partial gathers, including the continuing-leader join fast path
(`assume_leadership_fast_path/6` / `cast_data_to_new_member` / `{peer_joined}`); `register_replicas
> 1` (`RecvAck` resolves on the first follower ack); Erlang-distribution-only
partitions. The simulation harness covers register/unregister concurrency. The
module header in the `.tla` has the full scope note.

## Checked properties

| Invariant | Meaning | Design doc |
|---|---|---|
| `TypeOK` | state stays within declared shapes | — |
| `PrefixConsistency` | every live member's replica equals the committed history at its applied version | §4.5, §5.7 |
| `LeaderEpochUnique` | two members may both believe they lead only under different epochs | §4.2, §5.1 |
| `UniqueBinding` | at most one pid is ever acked `yes` per name | Guarantee 1 |
| `DurableAcked` | every acked registration has enough version-visible holders to survive `MaxCrashes` | Guarantee 4, §5.5 |
| `DegradedFlagSound` | an assume that did not flag itself `degraded` (gathered max version reached the durable version key) adopted exactly the committed map | §5.6, §8 `reject_when_degraded` |

"All invariants hold" is a claim about the fail-closed setting
(`strict_replication = true`). The default is degrade-open. See
DegradeOpenSafety below for what it still guarantees.

## Configs

Each config is `formal/<Name>.cfg`. Passing configs take minutes. Failing ones
take seconds.

| Config | Expect | What it shows |
|---|---|---|
| `DgenRegistryReplication` | pass | all six invariants, full depth, heartbeat off |
| `DgenRegistryReplicationHeartbeat` | pass | the first five with the heartbeat on (`MaxVersion = 2`) |
| `DgenRegistryReplicationDegradeOpenSafety` | pass | the default degrade-open mode keeps everything except `DurableAcked` |
| `DgenRegistryReplicationDegradedAssume` | pass | with the gather deadline modeled, `DegradedFlagSound` holds: the flag never misses an incomplete reconstruction |
| `DgenRegistryReplicationLeaderGoneAssume` | pass | the gather stops waiting once every live member has handled its old leader's DOWN. All six invariants hold. The plain deadline can't keep `DurableAcked`, but this exit only fires once nothing more can arrive from the old leader |
| `DgenRegistryReplicationHandoffRace` | fail | the pre-§5.7 handoff (both `SafeAssume*` off): one crash loses an acked registration (`DurableAcked`) |
| `DgenRegistryReplicationHandoffRaceUnique` | fail | the same race checked against `UniqueBinding` alone: the freed name is re-issued to a second pid |
| `DgenRegistryReplicationHandoffGatherOnly` | fail | the gather fence alone off: it is needed on its own |
| `DgenRegistryReplicationSnapMonotonicOnly` | fail | the snapshot guard alone off, with `EpochFencedAck` also off: it was needed on its own. The epoch fence alone also closes this race (see the `.cfg`) |
| `DgenRegistryReplicationNoGuard` | fail | optimistic follower acks (`VersionGuardedAck = FALSE`) lose `DurableAcked` |
| `DgenRegistryReplicationDegradeOpen` | fail | degrade-open (`strict_replication = false`) loses `DurableAcked` |
| `DgenRegistryReplicationAckReachable` | fail | vacuity canary: `NoAcks` fails, so acks are actually reachable |
| `DgenRegistryReplicationDegradedReachable` | fail | vacuity canary: `NoDegradedAssume` fails, so degraded assumes are actually reachable |
| `DgenRegistryReplicationLeaderGoneReachable` | fail | vacuity canary: with the deadline off, `NoDegradedAssume` fails, so the leader-gone exit is actually taken |
| `DgenRegistryReplicationNoEpochFence` | fail | `EpochFencedAck = FALSE`: a follower releases a held ack when a later leader's batch passes its version, though that leader took over without the commit (`DurableAcked`) |

If a vacuity canary ever passes, the model has stopped exercising its
behaviour, and a green run on the other configs means much less.

## Spec ↔ code map

| Spec | Code |
|---|---|
| `Elect` | `dgen_registry_elector` committing a membership/leadership change (abstracted to one durable write) |
| `AssumeGather` (incl. the `SafeAssumeGather` version-key fence) | the `assuming` statem state: `prepare_to_assume_leadership/6` → `spawn_leadership_gather` → `gather_until_caught_up/7` → the `{assume_gathered}` continuation, valid only in `assuming` for its arming ref. The continuing-leader join fast path (`assume_leadership_fast_path/6` / `cast_data_to_new_member` / `{peer_joined}`) dispatches in the `leader` state and is out of scope |
| `HeartbeatBcast` / `RecvHeartbeat` | `handle_event(info, replica_heartbeat, leader, …)` → `broadcast_heartbeat/1` (`{names_batch, [], E, V, V, Self}`) / the empty batch through `dgen_registry_replica:offer_batch/5` |
| `CanCommit`'s `dbLeader/dbEpoch` conjuncts | the fenced version-key bump in `dgen_registry_names:start_commit/4` (§5.1) |
| `RegisterForward` | follower `route_register` forward → leader `{register_req}` → group commit → `broadcast_batch/5` + `{register_reply, Ref, yes, Version}` |
| `RegisterDirect` + `RecvSync`/`RecvAck` | leader-local `route_register` → `dgen_registry_pipeline:await_acks/5` / `{replicate_sync}` / `{replicate_ack}` → `dgen_registry_pipeline:record_ack/3` |
| `DegradeTimeout` | `handle_info({replicate_timeout, _})` with `strict_replication = false` |
| `RecvBcastApply/Drop/Gap` | `dgen_registry_replica:offer_batch/5` → `applied` / `stale_epoch`+`duplicate` / `gap` (one `{names_batch, …}` per commit version). A batch from a later epoch is a `gap` (`Later`). The member's `{names_batch}` handler reacts to the verdict |
| `RecvReply` | `dgen_registry_intents:on_reply/5` incl. the `awaiting_version` phase. The reply carries the leader's epoch, and a held ack keeps it. Flushes are `dgen_registry_intents:on_version/2`, called from the `{names_batch}` handler's `applied` branch and on an accepted snapshot. Both release only in the held ack's epoch. On a leadership change, or once our replica passes that epoch, the code re-drives a deferred ack as a fresh forward (`redrive/5`) where the spec drops it: a fresh `RegisterForward` in spec terms |
| `RecvSnap` (incl. the `SafeAssumeSnap` version-monotonic guard) | `dgen_registry_replica:offer_snapshot/4` (the `Epoch >= CurEpoch andalso V >= Applied` guard), called from `handle_cast({apply_names_snapshot, ...})` |
| `ServeResync` / `resyncReq` | `{resync_req}` handler / `request_resync/2` |
| `Crash` | member/node death; the ETS replica dies with the process |
| `ObserveDown` / `leaderDown` (with `LeaderGoneAssume`) | the peer-monitor `'DOWN'` handler setting `leader_down` when the dead member is our `leader`. `get_names_snapshot` reports it, and `gather_until_caught_up/7` stops waiting once our own flag and every peer's are set |
| `DropMsg` | casts lost on an Erlang-distribution disconnect (signal-ordering semantics) |

The member's `gen_statem` states (`searching`/`assuming`/`leader`/`follower`)
correspond to what `leaderView[m]`/`epoch[m]`/mid-assume encode in the spec.
Gap/resync, leader reachability and the commit pipeline are per-member
variables on both sides.

Keep this table in sync whenever either side changes. If the two drift, TLC
keeps passing and the tests keep passing, but they no longer describe the same
protocol.

## Running

```sh
formal/check.sh DgenRegistryReplication            # expect pass
formal/check.sh DgenRegistryReplicationNoGuard fail  # expect fail
```

`check.sh <Config> [pass|fail]` runs TLC and checks the result against the
expectation. It needs Java 11+ and nothing else. It uses the TLC jar checked in
at `formal/vendor/tla2tools-v1.8.0.jar`. To use a different TLC, set
`TLA2TOOLS_JAR` or put the jar at `formal/tla2tools.jar` (gitignored). Each run
gets its own temporary metadir, so concurrent runs are safe.

CI (`.github/workflows/formal.yml`) runs every config in the table above with
its expected result on every push and PR.