docs: custody-schema contract revision 5 (sol r4 residuals F9/F11 + F12/F13)
ci/woodpecker/pr/ci Pipeline failed
ci/woodpecker/pr/ci Pipeline failed
This commit is contained in:
@@ -77,6 +77,26 @@ and fault-injection witnesses (F11). §8 discloses every rule above
|
||||
plus the previously undisclosed §4.3 committed-tree/symlink rule
|
||||
(F6).
|
||||
|
||||
Revision 5 (sol r4 findings F9/F11 residual, F12/F13 new): the
|
||||
pointer row gains a monotonic `generation` counter bumped by every
|
||||
upsert, and managed-deletion step 2 conditions on the generation
|
||||
recorded in step 1 instead of the content hash, closing the
|
||||
identical-content ABA in which a byte-identical rewrite reproduced
|
||||
the old hash and a stale deletion unpointed fresh content (F9). The
|
||||
ordered-write protocol gains a contract-defined locator scheme —
|
||||
injective over (category, slot), with the slot set fixed to the
|
||||
single value `answer` at version 1 — and a per-locator advisory lock
|
||||
spanning both steps, so same-locator writers are serialized and a
|
||||
completed write always leaves the pointer hash describing the
|
||||
current blob; §7.16 adds the concurrent-writer,
|
||||
crash-before-acknowledgment, stale-retry, and locator-injectivity
|
||||
witnesses (F11). Cascaded consent deletion now emits a semantic
|
||||
cessation event in the same transaction as the referent deletion,
|
||||
written by a trigger on the consent table, so the audit trail
|
||||
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).
|
||||
|
||||
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
|
||||
@@ -249,26 +269,65 @@ with contract 6 (`mode-conversion.md`), identity with
|
||||
follows it (§7.1 asserts the FK types match the live referenced
|
||||
columns).
|
||||
7. **Ordered sensitive-write protocol.** An ordinary sensitive write
|
||||
spans two stores and is ordered, content first: step 1 commits the
|
||||
content to the owning user's brain at a deterministic locator —
|
||||
the implementing PR declares a locator scheme that maps (category,
|
||||
answer slot) to one `brain_ref`, so a retry of the same write
|
||||
resolves to the same path; step 2, only after step 1 has
|
||||
spans two stores and is ordered, content first.
|
||||
|
||||
**Locator scheme.** The locator is a pure function
|
||||
`L(category_key, slot) → brain_ref` declared by the implementing
|
||||
PR, with three contract-bound properties: it is deterministic (a
|
||||
retry of the same write resolves to the same path), it is
|
||||
INJECTIVE — distinct (category_key, slot) pairs map to distinct
|
||||
`brain_ref` values, witnessed with a collision control (§7.16) —
|
||||
and it is stable across releases (a scheme change is a contract
|
||||
amendment with a migration). An **answer slot** is the stable
|
||||
identifier of one answer's position within a category; at
|
||||
version 1 every registry category is single-valued (mirroring
|
||||
§3.5's UNIQUE (`user_id`, `category_key`)), so the slot set is
|
||||
the single constant `answer`. An amendment introducing a
|
||||
multi-valued category must extend the slot set while preserving
|
||||
injectivity.
|
||||
|
||||
**Serialization.** The entire write — both steps — runs under a
|
||||
per-locator mutual exclusion: before step 1 the writer acquires
|
||||
an exclusive advisory lock keyed on (`user_id`, `category_key`,
|
||||
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
|
||||
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
|
||||
currently committed at the locator — the divergent interleaving
|
||||
(writer A's pointer over writer B's content) is unschedulable,
|
||||
not merely unlikely.
|
||||
|
||||
**Steps.** Step 1 commits the content to the owning user's brain
|
||||
at `L(category_key, slot)`; 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)) in its own
|
||||
database transaction inside the §2.6 fence. The write is
|
||||
acknowledged to the caller only after step 2 commits. Interruption
|
||||
before step 1 leaves both stores unchanged. Interruption between
|
||||
the steps leaves committed brain content with no pointer:
|
||||
unpointed content is inert — it lives in the correct custody
|
||||
store, no read path serves it (reads resolve through pointers
|
||||
only), and nothing dangles in the database. The client's retry —
|
||||
the write was never acknowledged — recommits the same locator and
|
||||
completes the pointer upsert, converging to the pointed state.
|
||||
The reverse order (pointer before content) is forbidden: an
|
||||
ordinary write never creates a pointer whose content has not
|
||||
committed. Witness §7.16 fault-injects both interruption points
|
||||
and drives the retry convergence.
|
||||
existing row for that (user, category, brain_ref), incrementing
|
||||
`generation` per §4.1) in its own database transaction inside the
|
||||
§2.6 fence. The write is acknowledged to the caller only after
|
||||
step 2 commits. Interruption before step 1 leaves both stores
|
||||
unchanged. Interruption between the steps leaves committed brain
|
||||
content with no pointer: unpointed content is inert — it lives in
|
||||
the correct custody store, no read path serves it (reads resolve
|
||||
through pointers only), and nothing dangles in the database.
|
||||
Interruption after step 2 commits but before the acknowledgment
|
||||
reaches the caller leaves the converged state; the retry below
|
||||
observes it and returns success without corrupting it. The
|
||||
client's retry — the write was never acknowledged — re-acquires
|
||||
the locator lock, recommits the same locator, and completes the
|
||||
pointer upsert, converging to the pointed state; the retry is
|
||||
idempotent whichever interruption point preceded it. A stale
|
||||
retry (an earlier write retried after a later same-locator write
|
||||
completed) also executes under the lock and leaves a consistent
|
||||
pointed state — same-locator outcomes are last-completed-write
|
||||
wins, and no completion order can leave the hash describing a
|
||||
non-current blob. The reverse order (pointer before content) is
|
||||
forbidden: an ordinary write never creates a pointer whose
|
||||
content has not committed. Witness §7.16 fault-injects the
|
||||
interruption points, drives retry convergence, the same-locator
|
||||
concurrent interleaving, the stale retry, and the injectivity
|
||||
control.
|
||||
|
||||
## 4. Pointer schema
|
||||
|
||||
@@ -281,6 +340,7 @@ with contract 6 (`mode-conversion.md`), identity with
|
||||
| `category_key` | text | NOT NULL, FK → profile_category_registry(category_key) |
|
||||
| `brain_ref` | text | NOT NULL, CHECK against the §4.3 grammar |
|
||||
| `content_hash` | text | NOT NULL (§4.4 construction) |
|
||||
| `generation` | bigint | NOT NULL (1 on insert; every §3.7 upsert increments) |
|
||||
| `created_at` | timestamptz | NOT NULL |
|
||||
| `updated_at` | timestamptz | NOT NULL |
|
||||
| `mismatch_at` | timestamptz | NULL unless the pointer is in the §4.6 mismatch state |
|
||||
@@ -336,6 +396,12 @@ 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.
|
||||
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
|
||||
@@ -350,21 +416,28 @@ with contract 6 (`mode-conversion.md`), identity with
|
||||
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 `content_hash` of the row it
|
||||
brain repository, recording the `generation` of the row it
|
||||
intends to delete as read 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
|
||||
`content_hash` equal to the recorded value. A concurrent §3.6
|
||||
write that recreates the same locator with new content commits a
|
||||
new hash on the pointer row, so step 2's condition fails, deletes
|
||||
nothing, and the fresh content stays pointed — deletion never
|
||||
removes a pointer for content it did not delete. 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 the concurrent-rewrite interleaving).
|
||||
`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).
|
||||
|
||||
## 5. Consent schema and evaluation
|
||||
|
||||
@@ -450,14 +523,32 @@ NULL)` — and the partial unique index UNIQUE (`user_id`,
|
||||
migration — the referent FK's `ON DELETE CASCADE` removes that
|
||||
grantee's consent rows in the same transaction as the referent
|
||||
deletion. Access ends with the rows (§5.3 default deny: no row, no
|
||||
access); no UPDATE is performed, so no actor question arises. The
|
||||
durable record of the grants and their lifecycle is the audit
|
||||
event table (§1.8): every mutation carried an `audit_event_id`,
|
||||
and audit events are not deleted by the cascade. The same rule
|
||||
already governs subject cessation via the `user_id` FK. §7.12
|
||||
witnesses the subject predicate, its refusal complement, and the
|
||||
cascade; every §7.3-enumerated consent-mutation route asserts the
|
||||
subject predicate.
|
||||
access); no UPDATE is performed, so no actor question arises.
|
||||
**Cessation event.** The cascade is not silent: an AFTER DELETE
|
||||
trigger on `profile_consents` inserts, for every deleted row whose
|
||||
deletion the §5.5 trigger permitted (i.e. a cessation cascade),
|
||||
one semantic **consent-cessation event** into the §1.8 audit
|
||||
event table, in the same database transaction as the referent
|
||||
deletion — if the deleting transaction rolls back, no cessation
|
||||
event survives, and if it commits, the events commit with it.
|
||||
Each event carries: the cause (`subject-cessation` or
|
||||
`grantee-cessation`, plus the parent table and deleted key), the
|
||||
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
|
||||
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
|
||||
cascade (audit events are never cascade-deleted), and the
|
||||
cessation event records when, why, and by whom the active grant
|
||||
ended. The same rule already governs subject cessation via the
|
||||
`user_id` FK. §7.12 witnesses the subject predicate, its refusal
|
||||
complement, the cascade, and the cessation event's atomicity,
|
||||
fields, and survival; every §7.3-enumerated consent-mutation
|
||||
route asserts the subject predicate.
|
||||
|
||||
5. **Revocation and re-grant.** Revocation flips exactly one active
|
||||
row to `revoked` and stamps `revoked_at`; it is effective for every
|
||||
@@ -549,12 +640,12 @@ declared profile table" means `profile_answers` (§3.5).
|
||||
(hierarchy §5.2) audit write path inserts into (§1.8 binding);
|
||||
and every FK column's declared type equals the referenced
|
||||
column's live declared type — in particular each `user_id` is
|
||||
`text` matching `users.id` and `agent_id` is `uuid` matching
|
||||
`agents.id` (§3.6 binding).
|
||||
`text` matching `users.id` (§3.6 binding) and `agent_id` is
|
||||
`uuid` matching `agents.id` (§5.2 binding).
|
||||
2. **Column-type allowlist witness:** the custody tables and
|
||||
`profile_answers` use only the column types named in
|
||||
§2.1/§3.5/§4.1/§5.1/§5.2/§6.3 (uuid, text, integer, timestamptz,
|
||||
boolean) — no bytea, json/jsonb, array, vector, or tsvector
|
||||
§2.1/§3.5/§4.1/§5.1/§5.2/§6.3 (uuid, text, integer, bigint,
|
||||
timestamptz, boolean) — no bytea, json/jsonb, array, vector, or tsvector
|
||||
column exists in them, closing the encoded/derived-representation
|
||||
routes by type rather than by probe alone.
|
||||
3. **Closed write-route witness** (hierarchy contract §6.3, full
|
||||
@@ -664,13 +755,18 @@ 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
|
||||
interleaving:** deletion step 1 commits; before step 2 runs, a
|
||||
concurrent §3.7 write recreates the same `brain_ref` with new
|
||||
content and completes its pointer upsert (new `content_hash`);
|
||||
step 2 then executes its compare-and-delete — the witness 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 (§4.7).
|
||||
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
|
||||
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
|
||||
static control asserts the deletion implementation conditions on
|
||||
`generation`, not on `content_hash` (§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
|
||||
@@ -697,7 +793,17 @@ declared profile table" means `profile_answers` (§3.5).
|
||||
consent evaluation for that grantee refuses (no row), the linked
|
||||
audit events survive, and no other grantee's rows are touched; a
|
||||
connector-registry amendment migration removing a key cascades
|
||||
identically (§5.4).
|
||||
identically (§5.4). **Cessation events:** the same deletions
|
||||
each produce one consent-cessation event per removed row in the
|
||||
§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
|
||||
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
|
||||
operation; and a subject-cessation (`users` row) deletion
|
||||
produces its events identically (§5.4).
|
||||
13. **Revocation/re-grant witnesses:** after revocation commits, the
|
||||
next evaluation refuses and the revoked row persists unmutated; a
|
||||
full grant → revoke → re-grant cycle yields two rows (one
|
||||
@@ -724,7 +830,7 @@ declared profile table" means `profile_answers` (§3.5).
|
||||
user B's content (§6.6); inserting a second `custody_config` row
|
||||
violates the §6.3 singleton constraint.
|
||||
16. **Ordered-write protocol witnesses:** the §3.7 protocol is
|
||||
fault-injected at both interruption points: killed before the
|
||||
fault-injected at its interruption points: killed before the
|
||||
brain commit, both stores are unchanged and the caller receives
|
||||
no acknowledgment; killed between the brain commit and the
|
||||
pointer upsert, the brain holds unpointed content, no pointer row
|
||||
@@ -732,10 +838,34 @@ declared profile table" means `profile_answers` (§3.5).
|
||||
received no acknowledgment — then the retried write recommits the
|
||||
same deterministic locator, completes the pointer upsert, and the
|
||||
witness asserts the converged state (one pointer, verifying hash,
|
||||
content served to the subject). 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.6).
|
||||
content served to the subject); killed after the pointer commit
|
||||
but before the acknowledgment reaches the caller, the retry
|
||||
executes under the locator lock, observes the converged state,
|
||||
returns success, and the witness asserts exactly one pointer with
|
||||
a verifying hash and an unchanged answer (idempotent completion,
|
||||
no duplicate content commit that changes the served bytes).
|
||||
**Same-locator interleaving:** two concurrent writers to one
|
||||
(user, category, slot) run to completion; the witness asserts
|
||||
both are serialized by the §3.7 advisory lock (their step-1/step-2
|
||||
spans do not interleave), the final pointer's hash verifies
|
||||
against the blob committed at the locator, and no `mismatch_at`
|
||||
is stamped by a subsequent read; a control with the lock removed
|
||||
schedules the divergent order (A's pointer upsert after B's
|
||||
content commit) and asserts the witness DETECTS the divergence —
|
||||
proving the lock is what excludes it. **Stale retry:** writer A
|
||||
is interrupted before acknowledgment; writer B then completes a
|
||||
full write to the same locator; A's retry executes under the
|
||||
lock and the witness asserts the end state is consistent (the
|
||||
pointer's hash verifies against the current blob — last
|
||||
completed write wins, no permanent mismatch). **Locator
|
||||
injectivity:** the declared scheme maps every distinct
|
||||
(category_key, slot) pair in the registry to a distinct
|
||||
`brain_ref` (exhaustive at version 1: seven categories x the
|
||||
`answer` slot), and a deliberately colliding scheme control
|
||||
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).
|
||||
|
||||
## 8. Drafting additions (PRD §12.1 disclosure)
|
||||
|
||||
@@ -751,9 +881,14 @@ ratification; none is claimed as a PRD mandate, and each is severable:
|
||||
same transaction; access ends through default deny, and durable
|
||||
history is carried by the §1.8 audit event table. The trigger's
|
||||
DELETE prong permits a child-row DELETE only when the referenced
|
||||
subject or grantee row is absent (§5.4, §5.5). This replaces the
|
||||
revision-2 system-actor auto-revocation predicate, which is
|
||||
withdrawn.
|
||||
subject or grantee row is absent (§5.4, §5.5). Each cascaded
|
||||
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
|
||||
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.
|
||||
4. The `custody_config` election record for the Standalone layout,
|
||||
singleton by constraint (§6.3).
|
||||
5. The domain-separated keyed `content_hash` construction, its key
|
||||
@@ -771,7 +906,8 @@ UPDATE` as the first statement of its transaction, and the
|
||||
supported version is an exported compile-time constant in the
|
||||
custody module of the shared schema package, read under the same
|
||||
lock as the decision it gates (§2.6, §2.7).
|
||||
10. Subject-only consent mutation authority (§5.4, first predicate).
|
||||
10. Subject-only consent mutation authority (§5.4, the single
|
||||
subject predicate).
|
||||
11. The declared non-sensitive profile table `profile_answers` and
|
||||
its closed schema (§3.5).
|
||||
12. The typed grantee referent columns, the
|
||||
@@ -792,11 +928,18 @@ UPDATE` as the first statement of its transaction, and the
|
||||
content-first at a deterministic locator, pointer upsert second
|
||||
in its own transaction, acknowledgement only after the pointer
|
||||
commit, idempotent retry convergence, and the
|
||||
pointer-before-content prohibition (§3.7, §7.16).
|
||||
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).
|
||||
17. The compare-and-delete managed-deletion step: deletion step 2 is
|
||||
conditioned on the `content_hash` recorded in step 1, so a
|
||||
concurrent recreate of the same locator is never unpointed by a
|
||||
stale deletion (§4.7, §7.10).
|
||||
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).
|
||||
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
|
||||
|
||||
Reference in New Issue
Block a user