docs: custody-schema contract revision 9 (sol r8 F15 residual + F16: independent deadline supervisor, brain fence via conditional application, reservation-at-skip, computed fixed cycle maximum with explicit exceedance carry-over)

2026-08-27 02:22:17 -05:00
parent f8ac64f58a
commit c6a2237dde
1 changed files with 231 additions and 51 deletions
@@ -154,6 +154,39 @@ cycle-duration limit is exercised as a checked bound), and a
 fourth static control failing any lock-holding path without the
 declared deadline (F15).
 Revision 9 (sol r8 residual F15 + new F16): the hold deadline
 becomes independently enforceable and the external store gains a
 fence. §3.7's deadline is now enforced by a deadline supervisor
 whose liveness does not depend on the stalled holder — the
 database's timeout mechanisms are defense in depth, not the
 enforcement path, since step 1's brain commit is not a database
 statement — and every brain mutation performed under a locator
 lock is FENCED: applied conditionally on the locator's brain state
 still equaling the value recorded at lock acquisition, so a
 terminated holder's in-flight external operation, resuming after
 the lock has passed on, is refused atomically and can never remove
 or replace a later holder's committed content (F16). §4.5's
 deferred repair now RESERVES its queue place at the moment its
 try-acquire fails, fixing the predecessor set at skip time and
 closing the window between skip and queue entry; the cycle maximum
 becomes the computed formula `M = S + Σᵢ(D·(Qᵢ+1)+R)` over
 snapshots taken at or before each reservation, fixed when the last
 reservation is placed and never enlarged; and exceedance is an
 explicit transition — the cycle reports failure, never completion,
 withdraws its pending reservations, and persists a durable
 carry-over set the next cycle processes first — so the orphan
 bound binds every completing cycle and every non-completing path
 is a surfaced error, and the grant-order rule must be bound to a
 documented mechanism guarantee or an application FIFO queue, not
 assumed (F15). §7.10 adds two external-step deadline controls (a
 stalled managed deletion and a stalled ordinary-writer brain
 commit, each terminated by the supervisor mid-external-operation,
 resumed after a fresh holder's acknowledged write, and asserted
 refused by the fence), the reservation control, the exceedance
 control, and static controls binding the grant-order guarantee and
 the fenced deletion path; §7.16 adds the static fenced-commit
 control (F15, F16).
 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
@@ -354,19 +387,37 @@ with contract 6 (`mode-conversion.md`), identity with
   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
+   through a **deadline supervisor** whose liveness is INDEPENDENT
-   timeout and idle-in-transaction timeout, plus an application
+   of the holder — a separate live component, not a timer inside
-   deadline covering step 1's brain commit), so a holder that
+   the possibly-stalled holder process, that observes lock
-   stalls past the deadline has its session TERMINATED — session
+   acquisition times and terminates the database session of any
-   end then releases the lock automatically per the rule above, and
+   holder past its deadline. The database's session-level timeout
-   the terminated holder's partial protocol is exactly the crash
+   mechanisms (statement timeout, idle-in-transaction timeout) are
-   window the tokens already make harmless (§4.5, §4.7). No holder
+   configured as defense in depth but are not the enforcement
   path: a statement timeout aborts a statement without ending the
   session, an idle-in-transaction timeout fires only on an idle
   open transaction, and step 1's brain commit is not a database
   statement at all — so a session stalled inside an external
   operation is terminated by the supervisor, which no
   database-side mechanism replaces. A holder that stalls past the
   deadline thus has its session TERMINATED — session end then
   releases the lock automatically per the rule above. The
   terminated holder's partial DATABASE protocol is exactly the
   crash window the tokens already make harmless (§4.5, §4.7); its
   possibly still in-flight EXTERNAL operation is made harmless by
   the brain fence below. 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
+   starts waiting after another never acquires before it. The
-   queue-order grant of the pinned advisory-lock mechanism,
+   implementing PR MUST bind this property to a mechanism, not
-   witnessed §7.10) — so a blocked waiter's wait is bounded by the
+   assume it: either it cites the pinned advisory-lock mechanism's
   documented queue-order grant guarantee, or, absent such a
   documented guarantee, it routes every conflicting locator-lock
   acquisition through an application-level FIFO queue whose order
   invariant is itself part of the implementation; the binding is
   checked by a §7.10 static control and the property is exercised
   dynamically (§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
@@ -377,8 +428,38 @@ with contract 6 (`mode-conversion.md`), identity with
   (writer A's pointer over writer B's content) is unschedulable,
   not merely unlikely.
   **Brain fence.** Deadline termination releases the lock while an
   external brain operation started by the terminated holder may
   still be in flight; lock release is therefore not, by itself, a
   fence for the external store. Every brain mutation performed
   under a locator lock — an ordinary write's step-1 content
   commit (below), a managed deletion's step-1 content deletion
   (§4.7) — is FENCED: immediately after acquiring the lock the
   holder records the locator's current brain state (the content
   version at `L(category_key, slot)`, or its recorded absence) as
   its **fence value**, and the mutation is applied conditionally —
   the brain store applies it only if the locator's state at
   application time still equals the recorded fence value, with the
   check and the application atomic with respect to other brain
   mutations (compare-and-swap semantics; an atomic ref update in a
   git-backed store satisfies this, with the per-locator condition
   re-validated inside the swap loop when the swap is taken on a
   coarser head). A later holder that commits at the locator
   changes the locator's state, so a stale operation — one whose
   session was terminated and whose lock has passed to a newer
   holder — no longer matches its recorded fence value and is
   REFUSED atomically: it cannot remove or replace content
   committed by any later holder, whether it resumes microseconds
   or hours after the termination. A live holder's own mutation
   passes its fence trivially: it holds the locator lock, so no
   other mutator has changed the locator since it recorded the
   value. Every brain-mutation path carries the fence; a path
   applying an unfenced brain mutation fails the §7.10 and §7.16
   static controls.
   **Steps.** Step 1 commits the content to the owning user's brain
-   at `L(category_key, slot)`; step 2, only after step 1 has
+   at `L(category_key, slot)` as a fenced mutation (Brain fence
   above); step 2, only after step 1 has
   committed, upserts the pointer row (insert, or update of the
   existing row for that (user, category, brain_ref), incrementing
   `generation` per §4.1) in its own database transaction inside the
@@ -471,39 +552,71 @@ with contract 6 (`mode-conversion.md`), identity with
   user's pointers runs on two triggers: every profile write for that
   user, and a periodic sweep whose interval the implementing PR
   declares (at most daily). A pointer whose content is absent is
-   deleted by the next triggered reconciliation — an orphan survives
+   deleted by the next triggered reconciliation cycle that reports
-   at most one cycle, and repair performs no database content write.
+   COMPLETION — no orphan survives a completed cycle; a cycle that
   cannot complete within its computed maximum fails as an explicit
   surfaced error with durable carry-over (below), never silently —
   and repair performs no database content write.
   Per-pointer repair runs under the §3.7 locator lock: before
   observing content absence for a pointer, reconciliation acquires
   the pointer's locator lock, holds it across the observation and
   the DELETE, and releases it after. The sweep pass MAY use a
   try-acquire so it never blocks mid-pass behind a writer, but a
-   failed try-acquire defers the locator, never discharges it: the
+   failed try-acquire defers the locator, never discharges it — and
-   skipped locator is queued within the SAME cycle, and before the
+   the deferral RESERVES its place: at the moment the try-acquire
-   cycle completes the sweep revisits every queued locator with a
+   fails, the sweep submits the locator's blocking lock request
-   blocking acquire and runs the same locked observation and
+   (the **reservation point**), so the request enters the lock
-   token-conditioned repair, retrying until the lock is acquired. A
+   queue immediately and its predecessor set — the current holder
   plus the waiters already queued at that instant — is fixed at
   skip time; contenders arriving afterward are later arrivals
   that §3.7 grant order places behind it, and there is no window
   between the try-acquire failure and queue entry in which a new
   contender can join the predecessor set. The sweep proceeds with
   the pass while the reservation waits, and before the cycle
   completes it returns to every reserved locator, completes the
   blocking acquire, and runs the same locked observation and
   token-conditioned repair. A
   triggered reconciliation cycle is COMPLETE only when every
   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
+   one except through the exceedance transition below — which
   fails the cycle loudly, never completes it — so the
   completed-cycle bound above holds unconditionally on lock
   contention. The blocking retry terminates within a WALL-CLOCK
   BOUND, not merely eventually: every holder is subject to the
-   §3.7 hold deadline (a stalled live session is terminated at the
+   §3.7 hold deadline (a stalled live session is terminated by the
-   deadline and session end releases the lock — voluntary release
+   independent supervisor at the deadline and session end releases
-   is not assumed), and grants follow §3.7 arrival order (no later
+   the lock — voluntary release is not assumed), and grants follow
-   requester overtakes the queued retry), so once the retry blocks
+   §3.7 arrival order (no later requester overtakes the queued
-   it acquires within the current holder's remaining deadline plus
+   reservation), so the reservation is granted within the current
-   the deadline-bounded holds of the waiters already queued ahead —
+   holder's remaining deadline plus the deadline-bounded holds of
-   a finite quantity fixed when the retry starts waiting,
+   the waiters already queued ahead — a finite quantity fixed at
-   independent of how many contenders arrive later. Cycle
+   its reservation point, independent of how many contenders
-   completion is therefore itself bounded: the implementing PR
+   arrive later. Cycle completion is therefore itself bounded by a
-   derives and declares a maximum cycle duration from the declared
+   COMPUTED maximum fixed within the cycle: the implementing PR
-   hold deadline, the sweep scope, and the retry queue, and a cycle
+   declares the hold deadline `D`, a sweep-pass bound `S` over the
-   exceeding its declared maximum is surfaced as an error — never a
+   cycle's scope (the scope is snapshotted when the cycle starts),
-   silent hang. A cycle whose retry is still blocked has not
+   and a per-locator repair bound `R` (at most `D`), and computes
-   completed, and the orphan is deleted before the cycle reports
+   the cycle maximum `M = S + Σᵢ (D·(Qᵢ+1) + R)` over the reserved
-   completion, within the declared bound.
+   locators `i`, where `Qᵢ` is the number of waiters queued ahead
   of reservation `i` at its reservation point. Every quantity in
   the formula is a snapshot taken at or before the corresponding
   reservation, so `M` is fully determined when the last
   reservation is placed and is NEVER enlarged afterward — queue
   growth after a reservation cannot extend it, because later
   arrivals are not predecessors. **Exceedance transition.** A
   cycle that reaches its computed `M` with reserved locators
   unprocessed stops: it withdraws its pending lock reservations,
   reports FAILURE — never completion — surfaces the error, and
   PERSISTS its unprocessed reserved locators as a durable
   CARRY-OVER set. The next triggered reconciliation cycle takes
   the carry-over set into its scope FIRST — fresh reservations,
   its own computed maximum — before its own sweep. An orphan is
   deleted before its cycle reports completion, within that
   cycle's computed `M`; the only path past a cycle boundary is
   the exceedance transition, an explicit surfaced failure with
   durable carry-over — never a silent hang and never a silent
   drop.
   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 —
@@ -541,8 +654,10 @@ with contract 6 (`mode-conversion.md`), identity with
   lock-holding writer has committed in its step 1 but not yet
   pointed, is unschedulable, because the deleter cannot enter its
   protocol while the writer holds the lock. **Steps**: step 1
-   commits the content deletion to the user's brain repository,
+   commits the content deletion to the user's brain repository as
-   recording the target row's `id` AND `generation` as read after
+   a FENCED mutation (§3.7 Brain fence — the fence value recorded
   immediately after lock acquisition), recording the target row's
   `id` AND `generation` as read after
   lock acquisition and before step 1; step 2, only after step 1
   has committed, deletes the pointer row in its own database
   transaction as a **compare-and-delete** — the DELETE is
@@ -563,7 +678,14 @@ with contract 6 (`mode-conversion.md`), identity with
   harmless — a deleter whose session dies after step 1 releases
   the lock (§3.7 rule), and whatever runs afterward, its never-run
   step 2 has no effect and a later deletion request is a NEW
-   protocol run reading current state. Interruption before step 1
+   protocol run reading current state. A deleter TERMINATED at the
   §3.7 hold deadline while its step-1 brain deletion is still in
   flight is likewise harmless on the brain side: the in-flight
   deletion is fenced, so once a later holder commits at the
   locator, the stale deletion's conditional application fails and
   removes nothing — content committed and acknowledged after the
   termination cannot be destroyed by the terminated deleter's
   resuming operation (witness §7.10). Interruption before step 1
   commits leaves both stores unchanged. Interruption between the
   steps leaves a dangling pointer, which §4.5 repairs toward
   deletion within one reconciliation cycle. At no point does any
@@ -952,13 +1074,47 @@ declared profile table" means `profile_answers` (§3.5).
    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
+    control** blocks the reserved repair behind a holder, keeps
    a stream of later contenders requesting the same locator lock
-    while the retry waits, and asserts the retry acquires before
+    while the reservation waits, and asserts the reservation is
-    every later contender and the cycle completes within its
+    granted before every later contender and the cycle completes
-    declared maximum duration — proving later arrivals cannot
+    within its computed maximum `M` — proving later arrivals cannot
-    starve the queued repair, and exercising the declared
+    starve the queued repair, and exercising the computed
-    cycle-duration limit as a checked bound rather than prose. A
+    cycle maximum as a checked bound rather than prose. A
    **reservation control** has the sweep's try-acquire fail
    against a holder and asserts the blocking lock request is
    enqueued AT the try-acquire failure (the §4.5 reservation
    point), not at end of pass — then starts contenders
    immediately after the failed try-acquire and asserts every one
    is granted after the reservation, and that the cycle's `M` was
    fixed when the last reservation was placed and is not enlarged
    while the late contenders queue. Two **external-step deadline
    controls** exercise termination at the real external boundary,
    not an idle transaction. First, the stalled managed deletion:
    a §4.7 deleter acquires the locator lock and starts its step-1
    brain deletion, which is suspended mid-operation — the session
    neither idle in a transaction nor executing a database
    statement; the control asserts the independent §3.7 supervisor
    terminates the session at the deadline with no cooperation
    from the holder and the lock releases; a fresh §3.7 writer
    then acquires the lock, commits new content at the locator
    with its pointer upsert, and is acknowledged; the suspended
    stale deletion is then RESUMED and asserted REFUSED by the
    brain fence — the fresh content is still present, its pointer
    resolves and verifies, and no mismatch is stamped. Second, the
    stalled ordinary writer: a §3.7 writer stalls inside its
    step-1 brain commit, is terminated at the deadline, a fresh
    writer completes a full acknowledged write at the same
    locator, and the stale commit is resumed and asserted refused
    — the locator serves the fresh writer's bytes and the fresh
    pointer's hash verifies. An **exceedance control** contrives a
    cycle that cannot finish within its computed `M` (an injected
    sequence of deadline-length holders on a reserved locator) and
    asserts the cycle reports FAILURE — never completion —
    surfaces the error, withdraws its pending reservations, and
    persists the carry-over set; the next triggered cycle is
    asserted to take the carry-over locators into scope first and
    delete the orphan before reporting completion. 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
@@ -966,14 +1122,24 @@ declared profile table" means `profile_answers` (§3.5).
    reconciliation-repair implementations each acquire the §3.7
    locator lock before their observation reads (§4.5, §4.7), and a
    third static control asserts the reconciliation implementation
-    queues a failed try-acquire for a within-cycle blocking retry —
+    reserves a failed try-acquire's queue place at skip time for a
-    an implementation that defers a skipped locator to a later
+    within-cycle blocking acquire — an implementation that defers
-    cycle, or that reports cycle completion with a queued locator
+    a skipped locator to a later cycle other than through the §4.5
-    unprocessed, FAILS. A fourth static control asserts every
+    exceedance transition (which fails the cycle and persists the
    carry-over set), or that reports cycle completion with a
    reserved locator 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.
+    lock-holding path FAILS. A fifth static control asserts the
    §3.7 grant-order binding: the implementation either cites the
    pinned advisory-lock mechanism's documented queue-order grant
    guarantee or routes conflicting locator-lock acquisitions
    through an application-level FIFO queue — an implementation
    relying on an undocumented grant order FAILS. A sixth static
    control asserts the managed-deletion brain step applies its
    mutation conditionally on the recorded §3.7 fence value — an
    unfenced brain-deletion 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
@@ -1079,7 +1245,10 @@ declared profile table" means `profile_answers` (§3.5).
    fails the witness. A static control asserts the implementation
    orders content before pointer: no enumerated sensitive-write
    route creates a pointer row before its brain commit has been
-    confirmed (§3.7).
+    confirmed (§3.7). A second static control asserts every
    enumerated sensitive-write route applies its step-1 brain
    commit as a fenced mutation conditioned on the recorded §3.7
    fence value — an unfenced brain-commit path FAILS.
 ## 8. Drafting additions (PRD §12.1 disclosure)
@@ -1156,8 +1325,19 @@ UPDATE` as the first statement of its transaction, and the
    never past it; per revision 8 every hold runs under a declared
    finite hold deadline with arrival-order grants, so the deferred
    repair — and with it cycle completion — is wall-clock bounded,
-    not merely eventual), so live interleavings between any two
+    not merely eventual; per revision 9 the deadline is enforced
-    mutators are excluded by one serialization protocol (§3.7,
+    by a supervisor independent of the holder, the deferred repair
    reserves its queue place at the moment its try-acquire fails,
    the cycle maximum is a computed formula over
    reservation-point snapshots that is fixed when the last
    reservation is placed, exceedance is an explicit failed-cycle
    transition with a durable carry-over set the next cycle
    processes first — so the one-cycle orphan bound binds every
    cycle that reports completion — and every brain mutation under
    a locator lock is fenced by a conditional application the next
    holder's commit invalidates), so live interleavings between
    any two mutators are excluded by one serialization protocol,
    and stale external tails are excluded by the fence (§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