-- 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');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 11 at RAISE
SELECT lease.acquire('k', '', interval '1s');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 11 at RAISE
SELECT lease.acquire('k', 'a', interval '0');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 11 at RAISE
SELECT lease.acquire('k', 'a', NULL);
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 11 at RAISE
SELECT lease.acquire(NULL, 'a', interval '1s');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 11 at RAISE
SELECT lease.acquire('k', 'a', interval '1s', interval '-1s');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 11 at RAISE
SELECT lease.renew('k', 'a', 1, interval '0');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function renew(text,text,bigint,interval) line 8 at RAISE
SELECT lease.renew('k', 'a', NULL, interval '1s');
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function renew(text,text,bigint,interval) line 8 at RAISE
SELECT lease.release('k', '', 1);
ERROR:  invalid_input
DETAIL:  a key/owner argument is NULL or empty, ttl is not positive, or wait is negative (acquire only)
CONTEXT:  PL/pgSQL function release(text,text,bigint) line 7 at RAISE
-- state must be untouched by all of the above
SELECT count(*) AS rows_after_invalid FROM lease.leases;
 rows_after_invalid 
--------------------
                  0
(1 row)

-- =====================================================================
-- 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');
 acquired | epoch | in_future 
----------+-------+-----------
 t        |     1 | t
(1 row)

SELECT held, owner, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.inspect('job-1');
 held | owner | epoch | in_future 
------+-------+-------+-----------
 t    | alice |     1 | t
(1 row)

-- =====================================================================
-- 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');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT held, owner, epoch FROM lease.inspect('job-1');
 held | owner | epoch 
------+-------+-------
 t    | alice |     1
(1 row)

-- =====================================================================
-- 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');
 acquired | epoch | expires_at 
----------+-------+------------
 f        |       | 
(1 row)

SELECT held, owner, epoch FROM lease.inspect('job-1');
 held | owner | epoch 
------+-------+-------
 t    | alice |     1
(1 row)

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

-- =====================================================================
-- 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');
 status | in_future 
--------+-----------
 ok     | t
(1 row)

SELECT status FROM lease.renew('job-1', 'bob', 1, interval '10s');     -- not_owner
  status   
-----------
 not_owner
(1 row)

SELECT status FROM lease.renew('job-1', 'alice', 99, interval '10s');  -- epoch_mismatch
     status     
----------------
 epoch_mismatch
(1 row)

SELECT status FROM lease.renew('never', 'alice', 1, interval '10s');   -- not_owner
  status   
-----------
 not_owner
(1 row)

SELECT held, owner, epoch FROM lease.inspect('job-1');
 held | owner | epoch 
------+-------+-------
 t    | alice |     1
(1 row)

-- =====================================================================
-- 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
  status   
-----------
 not_owner
(1 row)

SELECT status FROM lease.release('job-1', 'alice', 99);                -- epoch_mismatch
     status     
----------------
 epoch_mismatch
(1 row)

SELECT status FROM lease.release('job-1', 'alice', 1);                 -- ok
 status 
--------
 ok
(1 row)

SELECT held, owner, epoch, expires_at FROM lease.inspect('job-1');     -- free, epoch retained
 held | owner | epoch | expires_at 
------+-------+-------+------------
 f    |       |     2 | 
(1 row)

SELECT status FROM lease.renew('job-1', 'alice', 1, interval '10s');   -- not_owner after release
  status   
-----------
 not_owner
(1 row)

SELECT status FROM lease.release('job-1', 'alice', 1);                 -- not_owner (already free)
  status   
-----------
 not_owner
(1 row)

-- =====================================================================
-- INV-I2 Epoch monotonicity across a takeover/release chain
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('job-1', 'bob', interval '10s');    -- 3
 acquired | epoch 
----------+-------
 t        |     3
(1 row)

SELECT status FROM lease.release('job-1', 'bob', 3);                          -- -> 4
 status 
--------
 ok
(1 row)

SELECT acquired, epoch FROM lease.acquire('job-1', 'carol', interval '10s');  -- 5
 acquired | epoch 
----------+-------
 t        |     5
(1 row)

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

SELECT status FROM lease.release('job-1', 'carol', 5);   -- not_owner second
  status   
-----------
 not_owner
(1 row)

-- =====================================================================
-- 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');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT pg_sleep(0.1);
 pg_sleep 
----------
 
(1 row)

SELECT held, owner, epoch FROM lease.inspect('short');               -- reports unowned
 held | owner | epoch 
------+-------+-------
 f    |       |     1
(1 row)

SELECT status FROM lease.renew('short', 'alice', 1, interval '10s'); -- lapsed (own lease)
 status 
--------
 lapsed
(1 row)

SELECT status FROM lease.renew('short', 'bob', 2, interval '10s');   -- not_owner (never held)
  status   
-----------
 not_owner
(1 row)

SELECT acquired, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.acquire('short', 'bob', interval '10s');                -- takeover, epoch 2
 acquired | epoch | in_future 
----------+-------+-----------
 t        |     2 | t
(1 row)

-- =====================================================================
-- 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');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT pg_sleep(0.1);
 pg_sleep 
----------
 
(1 row)

SELECT status FROM lease.release('brief', 'dave', 1);                -- lapsed
 status 
--------
 lapsed
(1 row)

SELECT status FROM lease.release('brief', 'erin', 1);                -- not_owner (never held)
  status   
-----------
 not_owner
(1 row)

-- =====================================================================
-- 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
 acquired | epoch 
----------+-------
 t        |     7
(1 row)

SELECT acquired, epoch, expires_at
  FROM lease.acquire('job-1', 'bob', interval '10s', interval '0.2s');        -- raises timeout
ERROR:  timeout
DETAIL:  blocking acquire exceeded the wait bound
CONTEXT:  PL/pgSQL function acquire(text,text,interval,interval) line 80 at RAISE
-- =====================================================================
-- 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');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT pg_sleep(0.1);
 pg_sleep 
----------
 
(1 row)

SELECT held FROM lease.inspect('clock-key');   -- server clock, not client, lapsed it
 held 
------
 f
(1 row)

-- =====================================================================
-- TXN-01 Acquire inside a transaction that commits: persists
-- =====================================================================
BEGIN;
SELECT acquired, epoch FROM lease.acquire('txn-key', 'alice', interval '10s');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

COMMIT;
SELECT held, owner, epoch FROM lease.inspect('txn-key');
 held | owner | epoch 
------+-------+-------
 t    | alice |     1
(1 row)

-- =====================================================================
-- TXN-02 Acquire inside a transaction that rolls back: undone (S8, I6)
-- =====================================================================
BEGIN;
SELECT acquired, epoch FROM lease.acquire('txn-rb', 'alice', interval '10s');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

ROLLBACK;
SELECT held, owner, epoch, expires_at FROM lease.inspect('txn-rb');   -- empty: never existed
 held | owner | epoch | expires_at 
------+-------+-------+------------
(0 rows)

-- TXN-03 Renew inside a rolled-back transaction: undone
SELECT acquired, epoch FROM lease.acquire('txn-rb2', 'alice', interval '10s');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

BEGIN;
SELECT status FROM lease.renew('txn-rb2', 'alice', 1, interval '10s');
 status 
--------
 ok
(1 row)

ROLLBACK;
-- original expiry remains in the future (renew undone; lease still held)
SELECT held, owner, epoch FROM lease.inspect('txn-rb2');
 held | owner | epoch 
------+-------+-------
 t    | alice |     1
(1 row)

-- TXN-04 Release inside a rolled-back transaction: undone
BEGIN;
SELECT status FROM lease.release('txn-rb2', 'alice', 1);
 status 
--------
 ok
(1 row)

ROLLBACK;
SELECT held, owner, epoch FROM lease.inspect('txn-rb2');   -- still held by alice
 held | owner | epoch 
------+-------+-------
 t    | alice |     1
(1 row)

-- =====================================================================
-- INV-I11 Key independence: operations on distinct keys never interact
-- =====================================================================
SELECT acquired, epoch FROM lease.acquire('indep-a', 'alice', interval '10s');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT acquired, epoch FROM lease.acquire('indep-b', 'bob', interval '10s');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT status FROM lease.release('indep-a', 'alice', 1);
 status 
--------
 ok
(1 row)

SELECT acquired, epoch FROM lease.acquire('indep-b', 'carol', interval '10s');  -- still held by bob
 acquired | epoch 
----------+-------
 f        |      
(1 row)

SELECT held, owner FROM lease.inspect('indep-b');
 held | owner 
------+-------
 t    | bob
(1 row)

-- =====================================================================
-- 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
 held | owner | epoch 
------+-------+-------
 t    | carol |     7
(1 row)

SELECT status FROM lease.release('job-1', 'carol', 7);   -- -> 8
 status 
--------
 ok
(1 row)

SELECT acquired, epoch FROM lease.acquire('job-1', 'alice', interval '10s');  -- 9
 acquired | epoch 
----------+-------
 t        |     9
(1 row)

-- =====================================================================
-- 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)
 status 
--------
 ok
(1 row)

SELECT status FROM lease.release('job-1', 'alice', 9);
 status 
--------
 ok
(1 row)

SELECT status FROM lease.renew('job-1', 'alice', 10, interval '10s'); -- not_owner (free)
  status   
-----------
 not_owner
(1 row)

-- =====================================================================
-- 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');
 acquired | epoch 
----------+-------
 t        |     1
(1 row)

SELECT pg_sleep(0.1);
 pg_sleep 
----------
 
(1 row)

SELECT acquired, epoch, expires_at > clock_timestamp() AS in_future
  FROM lease.acquire('lapse-self', 'alice', interval '10s');   -- takeover, epoch 2
 acquired | epoch | in_future 
----------+-------+-----------
 t        |     2 | t
(1 row)

-- =====================================================================
-- 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)
 held | owner | epoch 
------+-------+-------
(0 rows)

SELECT acquired, epoch FROM lease.acquire('job-1', 'dave', interval '10s');  -- fresh key, epoch 1
 acquired | epoch 
----------+-------
 t        |     1
(1 row)