diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index 3c7992b7..ca9c8b36 100644 --- a/docs/requirements/custody-schema.md +++ b/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 - records the row's `generation` when it observes the content - absent and conditions the DELETE on it, so a concurrent §3.7 - write that recommits the locator between the observation and the - delete (bumping `generation`) makes the repair match zero rows — - reconciliation never unpoints content it did not observe absent. + Per-pointer repair runs under the §3.7 locator lock: before + observing content absence for a pointer, reconciliation acquires + the pointer's locator lock (a try-acquire is permitted — a + locator whose lock is held is skipped and repaired on the next + cycle, so the sweep never blocks behind a writer), holds it + 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 - brain repository, recording the `generation` of the row it - intends to delete as read before step 1; step 2, only after step 1 + transaction. **Lock coverage**: the deleter FIRST acquires the + §3.7 advisory lock on the target locator (`user_id`, + `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 - `generation` equal to the recorded value. The token is the - generation, not the content hash, deliberately: every §3.7 upsert - increments `generation` even when it recommits byte-identical - content (whose §4.4 hash is unchanged), so a concurrent §3.7 - write that recreates the same locator — with new content OR with - identical content — moves the row past the recorded generation, - step 2's condition matches zero rows, deletes nothing, and the - fresh content stays pointed. Deletion never removes a pointer for - a write it did not observe; the hash-token ABA (identical bytes - reproducing the recorded value) is unrepresentable because the - counter never repeats. 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). + conditioned on the recorded `id` AND `generation`. The token is + this PAIR, not the content hash and not the generation alone, + deliberately: every §3.7 upsert increments `generation` even + when it recommits byte-identical content (whose §4.4 hash is + unchanged), so a same-row rewrite moves the row past the + recorded generation; and the uuid `id` is minted fresh on every + insert and never reused, so a row REINCARNATION — the orphan row + deleted by §4.5 repair, then an ordinary write recreating the + locator with a fresh row whose `generation` is back at 1 — + cannot reproduce the recorded pair even though the counter value + repeats. In every such case step 2 matches zero rows, deletes + nothing, and the fresh content stays pointed: deletion never + removes a pointer row it did not observe. The lock excludes the + live interleavings; the pair token makes the crash windows + 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 + 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 - (grantee type and ref, `category_key`, `state`, `granted_at`, - `revoked_at`), and the event time. The snapshot is consent + direct referential action) — an immutable snapshot of the ended + grant identifying its exact row and subject: the deleted 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 - runs, a concurrent §3.7 write recreates the same `brain_ref` and - completes its pointer upsert; step 2 then executes its - compare-and-delete. The witness drives this once with CHANGED + interleavings (two):** deletion step 1 commits and the deleting + session is fault-injected dead before step 2 — the §4.7 lock + releases with the session, opening the crash window; a + 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 - same-locator writers (§3.7, §7.16). + per-locator advisory lock spanning both steps — held, per + 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 - step 1 (revision 5; the revision-4 `content_hash` token is - withdrawn as ABA-prone under identical-content rewrites), so a - concurrent recreate of the same locator — changed or - byte-identical — is never unpointed by a stale deletion (§4.1, - §4.7, §7.10). + conditioned on the PAIR of the target row's uuid `id` (the + immutable row-incarnation identity) and its monotonic + `generation` counter, both recorded in step 1 under the locator + lock (revision 6; the revision-4 `content_hash` token was + withdrawn as ABA-prone under identical-content rewrites, and the + 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