docs: custody-schema contract revision 6 (sol r5 residuals F9/F12 + F14)

docs/requirements/custody-schema.md

@@ -97,6 +97,25 @@ records when and why each active grant ended, not only that it began
 (F12). The stale §3.6/§5.2 cross-references and the "first
 predicate" remnant are corrected (F13).
 
+Revision 6 (sol r5 residuals F9/F12 + F14): the deletion and repair
+token becomes the PAIR (row `id`, `generation`) — the uuid primary
+key is minted fresh on every insert and never reused, so it is the
+row-incarnation identity the bare counter lacked; a stale
+compare-and-delete can no longer match a row reincarnated at
+generation 1 after an orphan-repair delete, and §7.10 adds the
+delete/reinsert ABA control (F9). The §3.7 locator lock now covers
+EVERY blob/pointer mutator for a locator, not only ordinary writers:
+managed deletion (§4.7) and reconciliation repair (§4.5) acquire the
+same advisory lock across their observe-and-mutate spans, so the
+reverse interleaving — a deleter destroying a blob a locked writer
+has committed but not yet pointed — is unschedulable while the
+tokens keep the crash-window (lock released by session death)
+harmless; §7.10 adds the reverse interleaving and its lock-removed
+control (F14). The cessation-event snapshot gains the deleted
+consent row's `id` and its `user_id`, so events from two subjects'
+grants to one ceasing grantee are attributable to their exact rows
+and subjects, witnessed with a two-subject case (F12).
+
 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
@@ -396,12 +415,24 @@ with contract 6 (`mode-conversion.md`), identity with
    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.
-   The repair DELETE is generation-conditioned like §4.7 step 2: it
+   Per-pointer repair runs under the §3.7 locator lock: before
-   records the row's `generation` when it observes the content
+   observing content absence for a pointer, reconciliation acquires
-   absent and conditions the DELETE on it, so a concurrent §3.7
+   the pointer's locator lock (a try-acquire is permitted — a
-   write that recommits the locator between the observation and the
+   locator whose lock is held is skipped and repaired on the next
-   delete (bumping `generation`) makes the repair match zero rows —
+   cycle, so the sweep never blocks behind a writer), holds it
-   reconciliation never unpoints content it did not observe absent.
+   across the observation and the DELETE, and releases it after.
+   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 —
+   the uuid `id` is minted per insert and never reused, so it
+   identifies the row incarnation; `generation` orders upserts
+   within the incarnation. A concurrent §3.7 write that recommits
+   the locator between the observation and the delete (bumping
+   `generation`), and a delete-then-reinsert that reincarnates the
+   locator's row (fresh `id`, `generation` back at 1), each make
+   the repair match zero rows — reconciliation never unpoints
+   content it did not observe absent, under either token
+   dimension.
 6. **Mismatch state.** A failed §4.4 verification stamps the pointer's
    `mismatch_at` and the read is refused; every subsequent read of a
    pointer with `mismatch_at` set is refused without re-serving
@@ -415,29 +446,49 @@ with contract 6 (`mode-conversion.md`), identity with
    the database.
 7. **Managed deletion protocol.** A managed deletion of sensitive
    content spans two stores and is an ordered protocol, not a single
-   transaction: step 1 commits the content deletion to the user's
+   transaction. **Lock coverage**: the deleter FIRST acquires the
-   brain repository, recording the `generation` of the row it
+   §3.7 advisory lock on the target locator (`user_id`,
-   intends to delete as read before step 1; step 2, only after step 1
+   `category_key`, slot) — the same lock ordinary writers hold —
+   before reading the pointer row or touching either store, and
+   holds it until step 2 commits or the deleter's session ends.
+   Every blob/pointer mutator for one locator — ordinary writes
+   (§3.7), managed deletion, and reconciliation repair (§4.5) —
+   therefore serializes on one lock: the reverse interleaving, in
+   which a deleter reads the old pointer and destroys a blob that a
+   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
+   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
-   conditioned on (`user_id`, `category_key`, `brain_ref`) AND
+   conditioned on the recorded `id` AND `generation`. The token is
-   `generation` equal to the recorded value. The token is the
+   this PAIR, not the content hash and not the generation alone,
-   generation, not the content hash, deliberately: every §3.7 upsert
+   deliberately: every §3.7 upsert increments `generation` even
-   increments `generation` even when it recommits byte-identical
+   when it recommits byte-identical content (whose §4.4 hash is
-   content (whose §4.4 hash is unchanged), so a concurrent §3.7
+   unchanged), so a same-row rewrite moves the row past the
-   write that recreates the same locator — with new content OR with
+   recorded generation; and the uuid `id` is minted fresh on every
-   identical content — moves the row past the recorded generation,
+   insert and never reused, so a row REINCARNATION — the orphan row
-   step 2's condition matches zero rows, deletes nothing, and the
+   deleted by §4.5 repair, then an ordinary write recreating the
-   fresh content stays pointed. Deletion never removes a pointer for
+   locator with a fresh row whose `generation` is back at 1 —
-   a write it did not observe; the hash-token ABA (identical bytes
+   cannot reproduce the recorded pair even though the counter value
-   reproducing the recorded value) is unrepresentable because the
+   repeats. In every such case step 2 matches zero rows, deletes
-   counter never repeats. Interruption before step 1 commits leaves
+   nothing, and the fresh content stays pointed: deletion never
-   both stores unchanged. Interruption between the steps leaves a
+   removes a pointer row it did not observe. The lock excludes the
-   dangling pointer, which §4.5 repairs toward deletion within one
+   live interleavings; the pair token makes the crash windows
-   reconciliation cycle. At no point does any compensation write
+   harmless — a deleter whose session dies after step 1 releases
-   content into the database (witness §7.10, including both
+   the lock (§3.7 rule), and whatever runs afterward, its never-run
-   concurrent-rewrite interleavings — changed content and
+   step 2 has no effect and a later deletion request is a NEW
-   identical content).
+   protocol run reading current state. 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
+   compensation write content into the database (witness §7.10,
+   including both concurrent-rewrite interleavings — changed
+   content and identical content — the delete/reinsert
+   reincarnation, and the reverse writer/deleter interleaving with
+   its lock-removed control).
 
 ## 5. Consent schema and evaluation
 
@@ -536,9 +587,16 @@ NULL)` — and the partial unique index UNIQUE (`user_id`,
    initiating actor — a platform surface that deletes a referent
    sets a transaction-local actor variable the trigger reads; absent
    one, the event records actor `system:cascade` (a migration or
-   direct referential action) — a snapshot of the ended grant
+   direct referential action) — an immutable snapshot of the ended
-   (grantee type and ref, `category_key`, `state`, `granted_at`,
+   grant identifying its exact row and subject: the deleted consent
-   `revoked_at`), and the event time. The snapshot is consent
+   row's `id`, its `user_id` (the data subject), grantee type and
+   ref, `category_key`, `state`, `granted_at`, and `revoked_at` —
+   and the event time. The row `id` and `user_id` are REQUIRED
+   precisely because the cause alone identifies only the ceasing
+   referent: when two users hold grants to one ceasing grantee, the
+   cascade removes both rows in one transaction, and only the
+   per-row snapshot distinguishes which subject's grant each event
+   records. The snapshot is consent
    metadata, never profile content, so §3.1 is not implicated. The
    audit table therefore records both ends of every grant's life:
    the mutation events written at grant/revoke time survive the
@@ -755,18 +813,45 @@ declared profile table" means `profile_answers` (§3.5).
     commit and the pointer delete, the dangling pointer is deleted by
     the next reconciliation — and at no point is content written to
     the database or restored to the brain. **Concurrent-rewrite
-    interleavings (two):** deletion step 1 commits; before step 2
+    interleavings (two):** deletion step 1 commits and the deleting
-    runs, a concurrent §3.7 write recreates the same `brain_ref` and
+    session is fault-injected dead before step 2 — the §4.7 lock
-    completes its pointer upsert; step 2 then executes its
+    releases with the session, opening the crash window; a
-    compare-and-delete. The witness drives this once with CHANGED
+    concurrent §3.7 write then recreates the same `brain_ref` and
+    completes its pointer upsert; the stale step-2 compare-and-delete
+    is then replayed with the recorded token. The witness drives
+    this once with CHANGED
     content (new `content_hash`, incremented `generation`) and once
     with BYTE-IDENTICAL content (unchanged `content_hash`,
     incremented `generation` — the ABA case a hash token would
     miss), and in both asserts the DELETE matches zero rows, the
     fresh pointer survives, its content resolves and verifies, and
-    no unpointed content and no dangling pointer exist afterward. A
+    no unpointed content and no dangling pointer exist afterward.
+    **Delete/reinsert reincarnation (third interleaving):** in the
+    same crash window, §4.5 reconciliation first removes the
+    now-orphan pointer row; an ordinary §3.7 write then recreates
+    the locator as a FRESH row — new `id`, `generation` back at 1
+    and therefore EQUAL to the recorded generation value; the
+    replayed stale step 2 is asserted to match ZERO rows (the
+    recorded `id` names the dead incarnation), and the fresh pointer
+    survives with its content resolving and verifying — the case a
+    bare generation token fails. **Reverse writer/deleter
+    interleaving:** a §3.7 writer holds the locator lock and has
+    committed its step-1 brain content but not its pointer upsert
+    when a managed deletion for the same locator starts. The witness
+    asserts the deletion BLOCKS at §4.7 lock acquisition until the
+    writer's pointer upsert and release, and that afterward no
+    acknowledged write's content is absent and no pointer names
+    absent content; a lock-removed control schedules the deleter's
+    observation and content removal inside the writer's
+    step-1-to-step-2 gap and asserts the witness DETECTS the
+    resulting acknowledged-write loss, establishing that the lock is
+    what excludes it. A
     static control asserts the deletion implementation conditions on
-    `generation`, not on `content_hash` (§4.7).
+    BOTH the recorded row `id` and `generation` — not on
+    `content_hash` and not on `generation` alone — and a second
+    static control asserts the managed-deletion and
+    reconciliation-repair implementations each acquire the §3.7
+    locator lock before their observation reads (§4.5, §4.7).
 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
@@ -798,7 +883,14 @@ declared profile table" means `profile_answers` (§3.5).
     §1.8 audit event table, carrying the §5.4 fields (cause with
     parent table and key, actor — the surface-set actor when one
     initiated the deletion, `system:cascade` otherwise — the grant
-    snapshot, and time); an atomicity control rolls the deleting
+    snapshot including the deleted consent row's `id` and `user_id`,
+    and time); a **two-subject discrimination witness** has two
+    distinct users each hold a `granted` row to ONE agent grantee
+    for the SAME category, deletes that grantee's `agents` row, and
+    asserts exactly two cessation events exist and that each event's
+    snapshot carries a distinct consent-row `id` and the correct
+    `user_id` — every event names exactly which subject's grant of
+    which row ended; an atomicity control rolls the deleting
     transaction back after the parent DELETE and asserts no
     cessation event persists (no orphan event without a deletion,
     no deletion without its events); the events survive subsequent
@@ -885,7 +977,10 @@ ratification; none is claimed as a PRD mandate, and each is severable:
    deletion additionally emits a consent-cessation audit event —
    written by an AFTER DELETE trigger in the same transaction as the
    referent deletion, carrying cause, actor (surface-set or
-   `system:cascade`), the grant snapshot, and time — so the audit
+   `system:cascade`), the grant snapshot — which, per revision 6,
+   includes the deleted consent row's `id` and its `user_id`, so
+   events from different subjects' grants to one ceasing grantee
+   remain distinguishable — and time — so the audit
    trail records when and why each active grant ended (§5.4,
    §7.12). This replaces the revision-2 system-actor auto-revocation
    predicate, which is withdrawn.
@@ -931,15 +1026,23 @@ UPDATE` as the first statement of its transaction, and the
     pointer-before-content prohibition — with the revision-5
     locator scheme (injective over (category, slot), the slot set
     fixed to `answer` at version 1, stable across releases) and the
-    per-locator advisory lock spanning both steps that serializes
+    per-locator advisory lock spanning both steps — held, per
-    same-locator writers (§3.7, §7.16).
+    revision 6, by EVERY blob/pointer mutator for the locator:
+    ordinary writers, managed deletion, and reconciliation repair
+    (try-acquire), 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 monotonic `generation` counter recorded in
+    conditioned on the PAIR of the target row's uuid `id` (the
-    step 1 (revision 5; the revision-4 `content_hash` token is
+    immutable row-incarnation identity) and its monotonic
-    withdrawn as ABA-prone under identical-content rewrites), so a
+    `generation` counter, both recorded in step 1 under the locator
-    concurrent recreate of the same locator — changed or
+    lock (revision 6; the revision-4 `content_hash` token was
-    byte-identical — is never unpointed by a stale deletion (§4.1,
+    withdrawn as ABA-prone under identical-content rewrites, and the
-    §4.7, §7.10).
+    revision-5 bare `generation` token is withdrawn as ABA-prone
+    under delete/reinsert reincarnation, where the counter restarts
+    at 1), so a stale deletion surviving a crash window is never
+    able to unpoint a fresh row — changed, byte-identical, or
+    reincarnated (§4.1, §4.7, §7.10).
 18. The sensitive-path write-set closure: a static inventory of every
     table a sensitive-write route can write, required to equal
     exactly the pointer table plus the §1.8 audit event table