diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index 56ffa283..d965a665 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -187,6 +187,33 @@ control, and static controls binding the grant-order guarantee and the fenced deletion path; §7.16 adds the static fenced-commit control (F15, F16). +Revision 10 (sol r9 residual F16 + new F17): the brain fence becomes +ABA-resistant. §3.7's fence value is now a per-locator fence EPOCH +with two invariants: every successful brain mutation mints a fresh, +never-reused value — byte-identical recommits and transitions to +absence included, absence being a unique tombstone state rather than +a recurrable bare-missing-path value — and every holder performs a +FENCE-ADVANCE immediately after lock acquisition, minting a fresh +epoch before its first brain observation or mutation, so every +earlier holder's recorded fence is invalidated at handoff, before the +new holder relies on exclusivity. A stale external tail is therefore +refused unconditionally: neither a byte-identical recommit, nor a +return to absence, nor resumption before the new holder's first +mutation can re-present a consumed epoch (F16). The live holder's +fence-pass now follows from handoff invalidation rather than from +lock possession, and a defect-only refusal has a specified +abort-and-surface transition. §4.5 repair performs the advance before +the absence observation it relies on. The unqualified distinct-locator +no-contention claim is narrowed to locator locks: a shared atomic +update point may cost swap-loop retries across locators but never +invalidates a distinct locator's condition — a liveness cost, never a +correctness coupling (F17). §7.10 adds two ABA fence controls +(byte-identical stale deletion; absence→write→delete→stale-writer +resurrection), a handoff-invalidation control with a +repair-observation variant, and a static fence-epoch-invariant +control; §7.16's static fenced-commit control is restated over the +epoch (F16, F17). + 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 @@ -421,7 +448,15 @@ with contract 6 (`mode-conversion.md`), identity with 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 - totally ordered; writes to distinct locators do not contend. + totally ordered; writes to distinct locators do not contend FOR + LOCATOR LOCKS. The brain store's atomic update point MAY be + shared across locators (a single head compare-and-swap in a + git-backed store serializes physically unrelated writes): losing + that swap costs a retry of the swap loop, and the retry + re-validates only the writer's own per-locator condition (Brain + fence below), which an unrelated locator's mutation never + changes — so cross-locator contention at a shared update point + is a liveness cost, never a correctness coupling. 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 @@ -431,31 +466,60 @@ with contract 6 (`mode-conversion.md`), identity with **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 + fence for the external store. The fence is a per-locator **fence + epoch**: a value stored in the brain store, atomically readable + and comparable together with the locator's content state, whose + defining property is that every change to it MINTS a fresh value + never before used at that locator. A per-locator monotonic + counter satisfies this, as does a unique commit identity in a + git-backed store; the locator's content BYTES do not — two + byte-identical states at different times are distinct epochs — + and ABSENCE is itself an epoch-bearing state, recorded as a + unique tombstone, never a bare missing path whose "value" can + recur. Two rules bind the epoch. **Minting:** every successful + brain mutation under a locator lock — a content commit, a + byte-identical recommit, a content deletion (transition to + absence) — advances the locator's epoch to a fresh never-reused + value, atomically with the mutation. **Fence-advance at + acquisition:** immediately after acquiring the locator lock, + before its first brain observation or mutation at the locator, + the holder performs a fence-advance — an atomic epoch mint that + leaves the locator's content presence and bytes unchanged — and + records the resulting epoch as its **fence value**; the advance + invalidates every fence recorded by any earlier holder before + the new holder relies on anything it reads or on its + exclusivity. 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 applied + conditionally: the brain store applies it only if the locator's + epoch at application time still equals the holder's 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 epoch condition re-validated inside the swap loop + when the swap is taken on a coarser head). A stale operation — + one whose session was terminated and whose lock has passed to a + newer holder — is REFUSED unconditionally: its recorded epoch + predates the next holder's fence-advance, so the condition fails + whether the intervening history changed the bytes, recommitted + byte-identical content, returned the locator to absence, or + consists of the advance alone — refusal does not wait for the + new holder's first mutation, and no sequence of mutations can + re-present a consumed epoch. 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. + or hours after the termination. A live holder's own fenced + mutation cannot fail its condition — not because it holds the + lock, but because handoff invalidation plus minting mean the + only epochs minted since its fence-advance are its own; a + holder whose fenced mutation is nonetheless refused (reachable + only under a defect breaching these invariants) MUST abort its + protocol run, release the lock, and surface the error — it + never retries the mutation under its stale fence. Every + brain-mutation path carries the fence, and every brain-RELYING + observation path (reconciliation repair's absence observation, + §4.5) performs its fence-advance before the observation it + relies on; 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)` as a fenced mutation (Brain fence @@ -559,8 +623,12 @@ with contract 6 (`mode-conversion.md`), identity with 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 + the pointer's locator lock, performs the §3.7 fence-advance — + invalidating any stale in-flight operation's fence BEFORE the + observation repair relies on, so no terminated holder's resuming + mutation can change the locator between repair's observation and + its DELETE — holds the lock 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 — and the deferral RESERVES its place: at the moment the try-acquire @@ -655,8 +723,10 @@ with contract 6 (`mode-conversion.md`), identity with 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 as - a FENCED mutation (§3.7 Brain fence — the fence value recorded - immediately after lock acquisition), recording the target row's + a FENCED mutation (§3.7 Brain fence — conditioned on the fence + epoch recorded at the deleter's post-acquisition fence-advance, + and itself minting the locator's unique absence tombstone + epoch), 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 @@ -681,11 +751,14 @@ with contract 6 (`mode-conversion.md`), identity with 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 + deletion is fenced, so once a later holder performs its §3.7 + fence-advance — before that holder's first mutation, and + regardless of whether its eventual commit is byte-identical to + the state the deleter recorded — 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 @@ -1107,7 +1180,37 @@ declared profile table" means `profile_answers` (§3.5). 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 + pointer's hash verifies. Two **ABA fence controls** exercise + value recurrence, the cases a state-equality fence misses. + Byte-identical stale deletion: a §4.7 deleter records its + fence, is suspended inside its step-1 brain deletion and + terminated by the supervisor; a fresh §3.7 writer then + recommits BYTE-IDENTICAL content (unchanged §4.4 hash) with + its pointer upsert and is acknowledged; the stale deletion is + resumed and asserted REFUSED — the identical bytes carry a + fresh epoch — with the content still present, resolving, and + verifying, and no mismatch stamped. Absence resurrection: an + ordinary writer records the locator's ABSENCE as its fence, is + suspended inside step 1 and terminated; a fresh writer + completes an acknowledged write at the locator; a managed + deletion then removes that content and its pointer, returning + the locator to absence; the stale writer is resumed and + asserted REFUSED — the post-deletion absence is a fresh + tombstone epoch, not a recurrence of the recorded one — with + the locator still absent and NO unpointed content existing + anywhere afterward. A **handoff-invalidation control**: a + holder is terminated mid-external-operation; the next holder + acquires the lock and performs its §3.7 fence-advance but has + NOT yet applied any brain mutation when the stale operation is + resumed — the stale operation is asserted refused (the advance + alone invalidated it, before any fresh mutation), and the new + holder's own subsequent fenced mutation is asserted to + succeed. A repair-observation variant runs the same schedule + with reconciliation as the new holder: repair advances, + observes content absence, and the stale writer resuming before + repair's DELETE is asserted refused — the DELETE then + completes under its recorded (`id`, `generation`) token and + NO unpointed content is resurrected at the locator. 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 — @@ -1138,8 +1241,20 @@ declared profile table" means `profile_answers` (§3.5). 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. + mutation conditionally on the recorded §3.7 fence epoch — an + unfenced brain-deletion path FAILS. A seventh static control + asserts the §3.7 fence-epoch invariants: every fenced-mutation + path mints a fresh never-reused per-locator epoch atomically + with its mutation — byte-identical recommits and transitions + to absence (the unique tombstone) included — every + lock-acquiring path that mutates or relies on brain state + (ordinary write §3.7, managed deletion §4.7, reconciliation + repair §4.5) performs the fence-advance immediately after + acquisition and records the post-advance epoch as its fence + value, and no path represents the fence by content bytes, + content hash, or bare path absence — an implementation whose + fence value can recur, or that observes before advancing, + 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 @@ -1248,7 +1363,9 @@ declared profile table" means `profile_answers` (§3.5). 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. + fence epoch — recorded at the route's post-acquisition + fence-advance, the commit itself minting a fresh epoch — an + unfenced brain-commit path FAILS. ## 8. Drafting additions (PRD §12.1 disclosure) @@ -1334,11 +1451,17 @@ UPDATE` as the first statement of its transaction, and the 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). + a locator lock is fenced by a conditional application; per + revision 10 the fence value is an ABA-resistant per-locator + fence EPOCH — minted fresh by every mutation, byte-identical + recommits and transitions to absence (unique tombstone) + included, and advanced by every new holder immediately after + acquisition, before it relies on brain state — so a stale + tail is refused even when bytes or absence recur and even + before the new holder's first mutation), 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 immutable row-incarnation identity) and its monotonic