-- pg_lease regression tests (stage 09).
--
-- Covers every externally observable behavior in specs/SEMANTICS.md and the
-- regression-testable subset of specs/INVARIANTS.md.
-- Invariant -> test mapping: test/INVARIANT-MAP.md.
-- Isolation-level concurrency (I1 races) and restart (I9) are stages 10/11.
--
-- Timestamp outputs are masked as boolean flags so expected output is
-- deterministic.

CREATE EXTENSION pg_lease;

-- =====================================================================
-- OPS-01 Invalid input: fail-closed raises, no state change (S5, S7, I10)
-- =====================================================================
SELECT lease.acquire('', 'a', interval '1s');
SELECT lease.acquire('k', '', interval '1s');
SELECT lease.acquire('k', 'a', interval '0');
SELECT lease.acquire('k', 'a', NULL);
SELECT lease.acquire(NULL, 'a', interval '1s');
SELECT lease.acquire('k', 'a', interval '1s', interval '-1s');
SELECT lease.renew('k', 'a', 1, interval '0');
SELECT lease.renew('k', 'a', NULL, interval '1s');
SELECT lease.release('k', '', 1);
-- state must be untouched by all of the above
SELECT count(*) AS rows_after_invalid FROM lease.leases;

-- =====================================================================
-- OPS-02 Acquire on fresh key: epoch 1, held (S4.1)
-- =====================================================================
SELECT acquired, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.acquire('job-1', 'alice', interval '10s');
SELECT held, owner, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.inspect('job-1');

-- =====================================================================
-- OPS-03 Duplicate acquire by same owner: idempotent, same epoch,
-- expiry unchanged (S4.1, Issue-3 clarification, I8, I10)
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('job-1', 'alice', interval '10s');
SELECT held, owner, epoch FROM lease.inspect('job-1');

-- =====================================================================
-- OPS-04 Acquire while HELD by another owner: denied, no state change
-- (S4.1, S7 not_acquirable, I1)
-- =====================================================================
SELECT acquired, epoch, expires_at FROM lease.acquire('job-1', 'bob', interval '10s');
SELECT held, owner, epoch FROM lease.inspect('job-1');

-- =====================================================================
-- OPS-05 Inspect unleased key: empty result (S4.4)
-- =====================================================================
SELECT held, owner, epoch, expires_at FROM lease.inspect('unleased');

-- =====================================================================
-- OPS-06 Renew: ok; renew by non-holder; renew with wrong epoch;
-- renew unknown key (S4.2, S7, I8)
-- =====================================================================
SELECT status, expires_at > clock_timestamp() AS in_future
  FROM lease.renew('job-1', 'alice', 1, interval '10s');
SELECT status FROM lease.renew('job-1', 'bob', 1, interval '10s');     -- not_owner
SELECT status FROM lease.renew('job-1', 'alice', 99, interval '10s');  -- epoch_mismatch
SELECT status FROM lease.renew('never', 'alice', 1, interval '10s');   -- not_owner
SELECT held, owner, epoch FROM lease.inspect('job-1');

-- =====================================================================
-- OPS-07 Release: wrong owner; wrong epoch; ok; state after release
-- (S4.3, S7, I2, I10)
-- =====================================================================
SELECT status FROM lease.release('job-1', 'bob', 1);                   -- not_owner
SELECT status FROM lease.release('job-1', 'alice', 99);                -- epoch_mismatch
SELECT status FROM lease.release('job-1', 'alice', 1);                 -- ok
SELECT held, owner, epoch, expires_at FROM lease.inspect('job-1');     -- free, epoch retained
SELECT status FROM lease.renew('job-1', 'alice', 1, interval '10s');   -- not_owner after release
SELECT status FROM lease.release('job-1', 'alice', 1);                 -- not_owner (already free)

-- =====================================================================
-- INV-I2 Epoch monotonicity across a takeover/release chain
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('job-1', 'bob', interval '10s');    -- 3
SELECT status FROM lease.release('job-1', 'bob', 3);                          -- -> 4
SELECT acquired, epoch FROM lease.acquire('job-1', 'carol', interval '10s');  -- 5

-- =====================================================================
-- OPS-08 Duplicate release: fails as not_owner (S7)
-- =====================================================================
SELECT status FROM lease.release('job-1', 'carol', 5);   -- ok first
SELECT status FROM lease.release('job-1', 'carol', 5);   -- not_owner second

-- =====================================================================
-- OPS-09 Expiry / lapse: lazy expiry; inspect reports free; lapsed holder's
-- renew fails as lapsed (vs not_owner for a stranger); takeover succeeds
-- with new epoch (S3, S4.1, S7, I1, I4, I5)
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('short', 'alice', interval '50ms');
SELECT pg_sleep(0.1);
SELECT held, owner, epoch FROM lease.inspect('short');               -- reports unowned
SELECT status FROM lease.renew('short', 'alice', 1, interval '10s'); -- lapsed (own lease)
SELECT status FROM lease.renew('short', 'bob', 2, interval '10s');   -- not_owner (never held)
SELECT acquired, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.acquire('short', 'bob', interval '10s');                -- takeover, epoch 2

-- =====================================================================
-- OPS-10 Release after lapse: lapsed (distinguishable from not_owner;
-- spec Issue 4 as amended by the API review, SEMANTICS §7)
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('brief', 'dave', interval '50ms');
SELECT pg_sleep(0.1);
SELECT status FROM lease.release('brief', 'dave', 1);                -- lapsed
SELECT status FROM lease.release('brief', 'erin', 1);                -- not_owner (never held)

-- =====================================================================
-- OPS-11 Blocking acquire: held lease, wait bound expires -> `timeout`
-- error (SQLSTATE 57014), distinguishable from the non-blocking denial
-- of OPS-04 (S4.1, §7). carol re-acquires first (OPS-08 freed job-1).
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('job-1', 'carol', interval '10s');  -- epoch 7
SELECT acquired, epoch, expires_at
  FROM lease.acquire('job-1', 'bob', interval '10s', interval '0.2s');        -- raises timeout

-- =====================================================================
-- INV-I7 No client clock trust: expiry derives from server clock only
-- (structural: no operation accepts a timestamp input; demonstrated by
-- acquiring with TTL and observing server-side expiry governs lapse)
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('clock-key', 'alice', interval '50ms');
SELECT pg_sleep(0.1);
SELECT held FROM lease.inspect('clock-key');   -- server clock, not client, lapsed it

-- =====================================================================
-- TXN-01 Acquire inside a transaction that commits: persists
-- =====================================================================
BEGIN;
SELECT acquired, epoch FROM lease.acquire('txn-key', 'alice', interval '10s');
COMMIT;
SELECT held, owner, epoch FROM lease.inspect('txn-key');

-- =====================================================================
-- TXN-02 Acquire inside a transaction that rolls back: undone (S8, I6)
-- =====================================================================
BEGIN;
SELECT acquired, epoch FROM lease.acquire('txn-rb', 'alice', interval '10s');
ROLLBACK;
SELECT held, owner, epoch, expires_at FROM lease.inspect('txn-rb');   -- empty: never existed

-- TXN-03 Renew inside a rolled-back transaction: undone
SELECT acquired, epoch FROM lease.acquire('txn-rb2', 'alice', interval '10s');
BEGIN;
SELECT status FROM lease.renew('txn-rb2', 'alice', 1, interval '10s');
ROLLBACK;
-- original expiry remains in the future (renew undone; lease still held)
SELECT held, owner, epoch FROM lease.inspect('txn-rb2');

-- TXN-04 Release inside a rolled-back transaction: undone
BEGIN;
SELECT status FROM lease.release('txn-rb2', 'alice', 1);
ROLLBACK;
SELECT held, owner, epoch FROM lease.inspect('txn-rb2');   -- still held by alice

-- =====================================================================
-- INV-I11 Key independence: operations on distinct keys never interact
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('indep-a', 'alice', interval '10s');
SELECT acquired, epoch FROM lease.acquire('indep-b', 'bob', interval '10s');
SELECT status FROM lease.release('indep-a', 'alice', 1);
SELECT acquired, epoch FROM lease.acquire('indep-b', 'carol', interval '10s');  -- still held by bob
SELECT held, owner FROM lease.inspect('indep-b');

-- =====================================================================
-- INV-I2/I9 Epoch continuity: release leaves durable monotonic epoch;
-- next acquire continues from it (fresh-key epoch-1 rule shown in OPS-02)
-- =====================================================================
SELECT held, owner, epoch FROM lease.inspect('job-1');   -- carol, epoch 7
SELECT status FROM lease.release('job-1', 'carol', 7);   -- -> 8
SELECT acquired, epoch FROM lease.acquire('job-1', 'alice', interval '10s');  -- 9

-- =====================================================================
-- S5/S7 Error behavior of renew/release on a FREE key (lapsed-holder
-- distinguishes nothing about who freed it: not_owner, per spec Issue 4)
-- =====================================================================
SELECT status FROM lease.renew('job-1', 'alice', 9, interval '10s');  -- ok (re-acquired above)
SELECT status FROM lease.release('job-1', 'alice', 9);
SELECT status FROM lease.renew('job-1', 'alice', 10, interval '10s'); -- not_owner (free)

-- =====================================================================
-- OPS-12 Same-owner re-acquire of a LAPSED lease: not idempotent —
-- takeover with new epoch and fresh expiry (lazy model, S4.1, I2)
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('lapse-self', 'alice', interval '50ms');
SELECT pg_sleep(0.1);
SELECT acquired, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.acquire('lapse-self', 'alice', interval '10s');   -- takeover, epoch 2

-- =====================================================================
-- OPS-13 Uninstall/reinstall cycle: DROP EXTENSION destroys all state
-- (schema + table + epochs); CREATE EXTENSION starts every key fresh at
-- epoch 1 (review finding: uninstall semantics must be tested)
-- =====================================================================
DROP EXTENSION pg_lease;
CREATE EXTENSION pg_lease;
SELECT held, owner, epoch FROM lease.inspect('job-1');   -- gone (no row: empty result)
SELECT acquired, epoch FROM lease.acquire('job-1', 'dave', interval '10s');  -- fresh key, epoch 1