From c6a2237dded52f7225f6a0b9431e43b97b5c8b08 Mon Sep 17 00:00:00 2001 From: fred Date: Thu, 27 Aug 2026 02:22:17 -0500 Subject: [PATCH] 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) --- docs/requirements/custody-schema.md | 282 +++++++++++++++++++++++----- 1 file changed, 231 insertions(+), 51 deletions(-) diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index 164ce4f8..56ffa283 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -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 - 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 + through a **deadline supervisor** whose liveness is INDEPENDENT + of the holder — a separate live component, not a timer inside + the possibly-stalled holder process, that observes lock + acquisition times and terminates the database session of any + holder past its deadline. The database's session-level timeout + mechanisms (statement timeout, idle-in-transaction timeout) are + 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 - queue-order grant of the pinned advisory-lock mechanism, - witnessed §7.10) — so a blocked waiter's wait is bounded by the + starts waiting after another never acquires before it. The + implementing PR MUST bind this property to a mechanism, not + 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 - at most one cycle, and repair performs no database content write. + deleted by the next triggered reconciliation cycle that reports + 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 - skipped locator is queued within the SAME cycle, and before the - cycle completes the sweep revisits every queued locator with a - blocking acquire and runs the same locked observation and - token-conditioned repair, retrying until the lock is acquired. A + failed try-acquire defers the locator, never discharges it — and + the deferral RESERVES its place: at the moment the try-acquire + fails, the sweep submits the locator's blocking lock request + (the **reservation point**), so the request enters the lock + 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 - deadline and session end releases the lock — voluntary release - is not assumed), and grants follow §3.7 arrival order (no later - 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. + §3.7 hold deadline (a stalled live session is terminated by the + independent supervisor at the deadline and session end releases + the lock — voluntary release is not assumed), and grants follow + §3.7 arrival order (no later requester overtakes the queued + reservation), so the reservation is granted within the current + holder's remaining deadline plus the deadline-bounded holds of + the waiters already queued ahead — a finite quantity fixed at + its reservation point, independent of how many contenders + arrive later. Cycle completion is therefore itself bounded by a + COMPUTED maximum fixed within the cycle: the implementing PR + declares the hold deadline `D`, a sweep-pass bound `S` over the + cycle's scope (the scope is snapshotted when the cycle starts), + and a per-locator repair bound `R` (at most `D`), and computes + the cycle maximum `M = S + Σᵢ (D·(Qᵢ+1) + R)` over the reserved + 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, - recording the target row's `id` AND `generation` as read after + commits the content deletion to the user's brain repository as + 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 - 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 + while the reservation waits, and asserts the reservation is + granted before every later contender and the cycle completes + within its computed maximum `M` — proving later arrivals cannot + starve the queued repair, and exercising the computed + 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 — - an implementation that defers a skipped locator to a later - cycle, or that reports cycle completion with a queued locator - unprocessed, FAILS. A fourth static control asserts every + reserves a failed try-acquire's queue place at skip time for a + within-cycle blocking acquire — an implementation that defers + a skipped locator to a later cycle other than through the §4.5 + 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 - mutators are excluded by one serialization protocol (§3.7, + not merely eventual; per revision 9 the deadline is enforced + 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