docs: custody-schema contract revision 8 (sol r7 residual F15: declared hold deadline + arrival-order grants make the one-cycle bound wall-clock provable)

docs/requirements/custody-schema.md

@@ -133,6 +133,27 @@ repeated-contention variant, and a third static control failing an
 implementation that defers a skipped locator to a later cycle
 (F15).
 
+Revision 8 (sol r7 residual F15): the one-cycle bound gains its
+missing termination proof. §3.7 adds two liveness rules for the
+locator lock: a declared finite HOLD DEADLINE, enforced with
+session-level timeout mechanisms on every lock-holding path — a
+live holder that stalls past the deadline is terminated, session
+end releases the lock, and the stalled-holder schedule collapses
+into the already-harmless crash window — and an arrival-order
+GRANT rule, so a blocked waiter's wait is bounded by the current
+holder and the waiters already ahead, never by later arrivals.
+§4.5's blocking retry therefore terminates within a wall-clock
+bound fixed when it starts waiting, and the implementing PR
+derives and declares a maximum cycle duration whose exceedance is
+surfaced as an error, never a silent hang. §7.10 adds the
+hold-deadline control (a non-cooperating stalled holder is
+terminated at the deadline and the orphan is still deleted before
+cycle completion), the grant-order control (a stream of later
+contenders cannot starve the queued repair, and the declared
+cycle-duration limit is exercised as a checked bound), and a
+fourth static control failing any lock-holding path without the
+declared deadline (F15).
+
 This contract binds the profile-category registry (§2), the custody
 placement rule (§3), the pointer schema (§4), the consent schema and its
 evaluation (§5), mode application (§6), witnesses (§7), and disclosed
@@ -328,7 +349,27 @@ with contract 6 (`mode-conversion.md`), identity with
    slot) (e.g. a session-scoped `pg_advisory_lock` on a stable hash
    of the triple), held until step 2 commits or the writer's session
    ends (session end releases it automatically, so a crashed holder
-   never wedges the locator). Writers to one locator are therefore
+   never wedges the locator). Two liveness rules bound this
+   exclusion. **Hold deadline:** every session that acquires a
+   locator lock — ordinary writer, managed deleter (§4.7),
+   reconciliation repair (§4.5) — runs under a declared finite hold
+   deadline: the implementing PR declares the value and enforces it
+   with the database's session-level timeout mechanisms (statement
+   timeout and idle-in-transaction timeout, plus an application
+   deadline covering step 1's brain commit), so a holder that
+   stalls past the deadline has its session TERMINATED — session
+   end then releases the lock automatically per the rule above, and
+   the terminated holder's partial protocol is exactly the crash
+   window the tokens already make harmless (§4.5, §4.7). No holder
+   — live, stalled, or crashed — holds a locator lock longer than
+   the declared deadline. **Grant order:** conflicting waiters on
+   one locator lock are granted in arrival order — a requester that
+   starts waiting after another never acquires before it (the
+   queue-order grant of the pinned advisory-lock mechanism,
+   witnessed §7.10) — so a blocked waiter's wait is bounded by the
+   current holder's remaining deadline plus the deadline-bounded
+   holds of the waiters already ahead of it, never by later
+   arrivals. Writers to one locator are therefore
    totally ordered; writes to distinct locators do not contend.
    Because no two same-locator writes interleave, a completed write
    always leaves the pointer's `content_hash` describing the blob
@@ -446,12 +487,23 @@ with contract 6 (`mode-conversion.md`), identity with
    in-scope pointer has been processed under its locator lock;
    deferral moves work to the end of the cycle, never into a later
    one, so the one-cycle bound above holds unconditionally on lock
-   contention. The blocking retry terminates: every §3.7 hold is
+   contention. The blocking retry terminates within a WALL-CLOCK
-   transaction- or session-scoped and session end releases the lock
+   BOUND, not merely eventually: every holder is subject to the
-   automatically (§3.7), so no holder — live or crashed — can hold
+   §3.7 hold deadline (a stalled live session is terminated at the
-   a locator past its session; a cycle whose retry is still blocked
+   deadline and session end releases the lock — voluntary release
-   has not completed, and the orphan is deleted the moment the lock
+   is not assumed), and grants follow §3.7 arrival order (no later
-   becomes available, before the cycle reports completion.
+   requester overtakes the queued retry), so once the retry blocks
+   it acquires within the current holder's remaining deadline plus
+   the deadline-bounded holds of the waiters already queued ahead —
+   a finite quantity fixed when the retry starts waiting,
+   independent of how many contenders arrive later. Cycle
+   completion is therefore itself bounded: the implementing PR
+   derives and declares a maximum cycle duration from the declared
+   hold deadline, the sweep scope, and the retry queue, and a cycle
+   exceeding its declared maximum is surfaced as an error — never a
+   silent hang. A cycle whose retry is still blocked has not
+   completed, and the orphan is deleted before the cycle reports
+   completion, within the declared bound.
    The repair DELETE is additionally token-conditioned like §4.7
    step 2: it records the row's `id` and `generation` when it
    observes the content absent and conditions the DELETE on BOTH —
@@ -891,7 +943,22 @@ declared profile table" means `profile_answers` (§3.5).
     releases and asserts the queued locator is retried until
     acquired — the orphan is still deleted by cycle completion once
     the last holder releases, never dropped after one failed
-    attempt. A
+    attempt. A **hold-deadline control** starts from a pre-existing
+    orphan, has a live holder acquire the orphan's locator lock and
+    stall past the declared §3.7 hold deadline WITHOUT ending its
+    session (idle transaction kept open), and asserts the holder's
+    session is terminated at the deadline, the lock releases
+    without any voluntary action by the holder, and the queued
+    blocking retry then deletes the orphan under the recorded
+    token before the cycle reports completion — proving termination
+    does not depend on a cooperative holder. A **grant-order
+    control** blocks the end-of-cycle retry behind a holder, keeps
+    a stream of later contenders requesting the same locator lock
+    while the retry waits, and asserts the retry acquires before
+    every later contender and the cycle completes within its
+    declared maximum duration — proving later arrivals cannot
+    starve the queued repair, and exercising the declared
+    cycle-duration limit as a checked bound rather than prose. A
     static control asserts the deletion implementation conditions on
     BOTH the recorded row `id` and `generation` — not on
     `content_hash` and not on `generation` alone — a second
@@ -902,7 +969,11 @@ declared profile table" means `profile_answers` (§3.5).
     queues a failed try-acquire for a within-cycle blocking retry —
     an implementation that defers a skipped locator to a later
     cycle, or that reports cycle completion with a queued locator
-    unprocessed, FAILS.
+    unprocessed, FAILS. A fourth static control asserts every
+    lock-holding path (ordinary write §3.7, managed deletion §4.7,
+    reconciliation repair §4.5) is configured with the declared
+    §3.7 hold deadline — an implementation with any unbounded
+    lock-holding path FAILS.
 11. **Default-deny and granularity witnesses:** an agent grantee with
     no active row is refused; with a `granted` row for category A
     only, category B is refused; with agent X granted, agent Y of the
@@ -1082,9 +1153,12 @@ UPDATE` as the first statement of its transaction, and the
     ordinary writers, managed deletion, and reconciliation repair
     (try-acquire with the revision-7 within-cycle blocking retry,
     so a failed try-acquire defers repair to the end of the cycle,
-    never past it), so live interleavings between any two mutators
+    never past it; per revision 8 every hold runs under a declared
-    are excluded by one serialization protocol (§3.7, §4.5, §4.7,
+    finite hold deadline with arrival-order grants, so the deferred
-    §7.16).
+    repair — and with it cycle completion — is wall-clock bounded,
+    not merely eventual), so live interleavings between any two
+    mutators are excluded by one serialization protocol (§3.7,
+    §4.5, §4.7, §7.16).
 17. The compare-and-delete managed-deletion step: deletion step 2 is
     conditioned on the PAIR of the target row's uuid `id` (the
     immutable row-incarnation identity) and its monotonic