# pg_lease — Invariant → Test Mapping

Stage-09 regression suite (`test/sql/pg_lease.sql`). Test IDs are the
comment banners in the test file. Regression tests are single-session;
multi-session races belong to the stage-10 isolation suite, restart/crash
to the stage-11 failure suite — noted below where that is the authoritative
test.

## SEMANTICS.md operations

| Spec item                                                   | Test                   |
| ----------------------------------------------------------- | ---------------------- |
| §4.1 Acquire fresh key (epoch 1, expiry)                    | OPS-02                 |
| §4.1 Acquire denied while HELD (`not_acquirable`)           | OPS-04                 |
| §4.1 Blocking mode wait bound exhausted = `timeout` (57014) | OPS-11                 |
| §4.1 Same-owner idempotent re-acquire (Issue 3)             | OPS-03                 |
| §4.2 Renew ok / non-holder / wrong epoch / unknown key      | OPS-06                 |
| §4.3 Release wrong owner / wrong epoch / ok / duplicate     | OPS-07, OPS-08         |
| §4.3 Release after lapse = `lapsed` (review finding 2)      | OPS-10                 |
| §4.4 Inspect held / unleased / lapsed (lazy model, Issue 1) | OPS-02, OPS-05, OPS-09 |
| §5 Input constraints, §7 `invalid_input`                    | OPS-01                 |
| §7 `lapsed` vs `not_owner` distinguishability               | OPS-06, OPS-09, OPS-10 |
| §7 `timeout` vs non-blocking denial distinguishability      | OPS-04, OPS-11         |
| §8 Transaction semantics: commit persists                   | TXN-01                 |
| §8 Rollback undoes acquire / renew / release                | TXN-02, TXN-03, TXN-04 |
| §9 Takeover of lapsed lease                                 | OPS-09                 |
| §10 Lapsed holder: renew and release fail; must re-acquire  | OPS-09, OPS-10         |

## INVARIANTS.md

| Invariant                               | Regression test                                                                                                                     | Authoritative stage                                                                    |
| --------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------- |
| I1 Mutual exclusion                     | OPS-04 (denied acquire while held); OPS-09 (post-lapse only)                                                                        | **Stage 10** (simultaneous-acquire races)                                              |
| I2 Epoch monotonicity                   | INV-I2 chain 3→4→5; OPS-08 duplicate release leaves epoch; INV-I2/I9 7→8→9; OPS-09 takeover epoch 2                                 | regression                                                                             |
| I3 Fencing effectiveness                | epoch_mismatch on renew/release with stale epoch (OPS-06, OPS-07); consumer-side rejection is a caller convention, specified S4/S10 | regression (spec-level)                                                                |
| I4 Ambiguity window bounded             | OPS-09 (lapse observable immediately after expiry; inspect reports unowned)                                                         | regression; window bound A1/A2 stated at stage 16                                      |
| I5 Takeover liveness                    | OPS-09 (takeover succeeds after TTL without holder action)                                                                          | regression                                                                             |
| I6 Atomicity of transitions             | TXN-02/03/04 (all-or-nothing under rollback)                                                                                        | regression; race-level in stage 10                                                     |
| I7 No client clock trust                | INV-I7 (no operation accepts a timestamp; lapse governed by server clock)                                                           | regression (structural)                                                                |
| I8 Renewal preserves identity and epoch | OPS-03 (idempotent re-acquire), OPS-06 (renew ok keeps epoch 1)                                                                     | regression                                                                             |
| I9 Restart survival                     | —                                                                                                                                   | **Stage 11** (crash/restart suite); epoch durability structurally via WAL-backed table |
| I10 Fail-closed                         | OPS-01 (no rows after invalid ops); denied ops leave state unchanged (OPS-04, OPS-06, OPS-07)                                       | regression                                                                             |
| I11 Key independence                    | INV-I11                                                                                                                             | regression; cross-key races in stage 10                                                |

## Notes

- OPS-01 also asserts the invalid-input block leaves zero rows (I10).
- Timestamp masking (`in_future` flags) keeps expected output deterministic;
  exact expiry values are never asserted, only ordering vs server time.
- Stage 10 (isolation): simultaneous acquire, renew-vs-takeover,
  release-vs-acquire, blocked-acquire wake behavior — I1, I4, I6, I11 races.
- Stage 10 suite: `test/specs/*.spec` via `make installcheck` —
  compete (I1 single-winner, all start orders), races (renew/release vs
  acquire/takeover: I1, I3), stale-client (I2, I3 post-takeover
  rejection), rollback-race (S8, I6: blocked acquirer resolved by
  COMMIT/ROLLBACK of the competing transaction — ordering proven by
  `<waiting ...>` serialization, not sleeps), independent-keys (I11).
- Waiter wake (`test/wait-wake.sh`, `make check-wait`): a blocking
  acquirer must observe a release by another session within its wait
  bound — S4.1 blocking mode. Not expressible in isolationtester (the
  waiter sleeps on a timer, not a lock); asserted via two concurrent
  sessions with a generous bound, so it tests ordering, not timing.
- Stage 11 (failure): crash/restart (I9, D1–D3), session termination,
  resource-exhaustion fail-closed behavior.