docs: custody-schema contract revision 10 (sol r9 F16 residual + F17: ABA-resistant per-locator fence epoch — fresh mint on every mutation incl. byte-identical and absence tombstone, fence-advance at lock acquisition invalidating stale tails before first mutation, repair advances before observing; distinct-locator no-contention narrowed to locator locks)
ci/woodpecker/pr/ci Pipeline was successful
ci/woodpecker/pr/ci Pipeline was successful
This commit is contained in:
@@ -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
|
the fenced deletion path; §7.16 adds the static fenced-commit
|
||||||
control (F15, F16).
|
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
|
This contract binds the profile-category registry (§2), the custody
|
||||||
placement rule (§3), the pointer schema (§4), the consent schema and its
|
placement rule (§3), the pointer schema (§4), the consent schema and its
|
||||||
evaluation (§5), mode application (§6), witnesses (§7), and disclosed
|
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
|
current holder's remaining deadline plus the deadline-bounded
|
||||||
holds of the waiters already ahead of it, never by later
|
holds of the waiters already ahead of it, never by later
|
||||||
arrivals. Writers to one locator are therefore
|
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
|
Because no two same-locator writes interleave, a completed write
|
||||||
always leaves the pointer's `content_hash` describing the blob
|
always leaves the pointer's `content_hash` describing the blob
|
||||||
currently committed at the locator — the divergent interleaving
|
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
|
**Brain fence.** Deadline termination releases the lock while an
|
||||||
external brain operation started by the terminated holder may
|
external brain operation started by the terminated holder may
|
||||||
still be in flight; lock release is therefore not, by itself, a
|
still be in flight; lock release is therefore not, by itself, a
|
||||||
fence for the external store. Every brain mutation performed
|
fence for the external store. The fence is a per-locator **fence
|
||||||
under a locator lock — an ordinary write's step-1 content
|
epoch**: a value stored in the brain store, atomically readable
|
||||||
commit (below), a managed deletion's step-1 content deletion
|
and comparable together with the locator's content state, whose
|
||||||
(§4.7) — is FENCED: immediately after acquiring the lock the
|
defining property is that every change to it MINTS a fresh value
|
||||||
holder records the locator's current brain state (the content
|
never before used at that locator. A per-locator monotonic
|
||||||
version at `L(category_key, slot)`, or its recorded absence) as
|
counter satisfies this, as does a unique commit identity in a
|
||||||
its **fence value**, and the mutation is applied conditionally —
|
git-backed store; the locator's content BYTES do not — two
|
||||||
the brain store applies it only if the locator's state at
|
byte-identical states at different times are distinct epochs —
|
||||||
application time still equals the recorded fence value, with the
|
and ABSENCE is itself an epoch-bearing state, recorded as a
|
||||||
check and the application atomic with respect to other brain
|
unique tombstone, never a bare missing path whose "value" can
|
||||||
mutations (compare-and-swap semantics; an atomic ref update in a
|
recur. Two rules bind the epoch. **Minting:** every successful
|
||||||
git-backed store satisfies this, with the per-locator condition
|
brain mutation under a locator lock — a content commit, a
|
||||||
re-validated inside the swap loop when the swap is taken on a
|
byte-identical recommit, a content deletion (transition to
|
||||||
coarser head). A later holder that commits at the locator
|
absence) — advances the locator's epoch to a fresh never-reused
|
||||||
changes the locator's state, so a stale operation — one whose
|
value, atomically with the mutation. **Fence-advance at
|
||||||
session was terminated and whose lock has passed to a newer
|
acquisition:** immediately after acquiring the locator lock,
|
||||||
holder — no longer matches its recorded fence value and is
|
before its first brain observation or mutation at the locator,
|
||||||
REFUSED atomically: it cannot remove or replace content
|
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
|
committed by any later holder, whether it resumes microseconds
|
||||||
or hours after the termination. A live holder's own mutation
|
or hours after the termination. A live holder's own fenced
|
||||||
passes its fence trivially: it holds the locator lock, so no
|
mutation cannot fail its condition — not because it holds the
|
||||||
other mutator has changed the locator since it recorded the
|
lock, but because handoff invalidation plus minting mean the
|
||||||
value. Every brain-mutation path carries the fence; a path
|
only epochs minted since its fence-advance are its own; a
|
||||||
applying an unfenced brain mutation fails the §7.10 and §7.16
|
holder whose fenced mutation is nonetheless refused (reachable
|
||||||
static controls.
|
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
|
**Steps.** Step 1 commits the content to the owning user's brain
|
||||||
at `L(category_key, slot)` as a fenced mutation (Brain fence
|
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.
|
and repair performs no database content write.
|
||||||
Per-pointer repair runs under the §3.7 locator lock: before
|
Per-pointer repair runs under the §3.7 locator lock: before
|
||||||
observing content absence for a pointer, reconciliation acquires
|
observing content absence for a pointer, reconciliation acquires
|
||||||
the pointer's locator lock, holds it across the observation and
|
the pointer's locator lock, performs the §3.7 fence-advance —
|
||||||
the DELETE, and releases it after. The sweep pass MAY use a
|
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
|
try-acquire so it never blocks mid-pass behind a writer, but a
|
||||||
failed try-acquire defers the locator, never discharges it — and
|
failed try-acquire defers the locator, never discharges it — and
|
||||||
the deferral RESERVES its place: at the moment the try-acquire
|
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
|
pointed, is unschedulable, because the deleter cannot enter its
|
||||||
protocol while the writer holds the lock. **Steps**: step 1
|
protocol while the writer holds the lock. **Steps**: step 1
|
||||||
commits the content deletion to the user's brain repository as
|
commits the content deletion to the user's brain repository as
|
||||||
a FENCED mutation (§3.7 Brain fence — the fence value recorded
|
a FENCED mutation (§3.7 Brain fence — conditioned on the fence
|
||||||
immediately after lock acquisition), recording the target row's
|
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
|
`id` AND `generation` as read after
|
||||||
lock acquisition and before step 1; step 2, only after step 1
|
lock acquisition and before step 1; step 2, only after step 1
|
||||||
has committed, deletes the pointer row in its own database
|
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
|
protocol run reading current state. A deleter TERMINATED at the
|
||||||
§3.7 hold deadline while its step-1 brain deletion is still in
|
§3.7 hold deadline while its step-1 brain deletion is still in
|
||||||
flight is likewise harmless on the brain side: the in-flight
|
flight is likewise harmless on the brain side: the in-flight
|
||||||
deletion is fenced, so once a later holder commits at the
|
deletion is fenced, so once a later holder performs its §3.7
|
||||||
locator, the stale deletion's conditional application fails and
|
fence-advance — before that holder's first mutation, and
|
||||||
removes nothing — content committed and acknowledged after the
|
regardless of whether its eventual commit is byte-identical to
|
||||||
termination cannot be destroyed by the terminated deleter's
|
the state the deleter recorded — the stale deletion's
|
||||||
resuming operation (witness §7.10). Interruption before step 1
|
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
|
commits leaves both stores unchanged. Interruption between the
|
||||||
steps leaves a dangling pointer, which §4.5 repairs toward
|
steps leaves a dangling pointer, which §4.5 repairs toward
|
||||||
deletion within one reconciliation cycle. At no point does any
|
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
|
writer completes a full acknowledged write at the same
|
||||||
locator, and the stale commit is resumed and asserted refused
|
locator, and the stale commit is resumed and asserted refused
|
||||||
— the locator serves the fresh writer's bytes and the fresh
|
— 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
|
cycle that cannot finish within its computed `M` (an injected
|
||||||
sequence of deadline-length holders on a reserved locator) and
|
sequence of deadline-length holders on a reserved locator) and
|
||||||
asserts the cycle reports FAILURE — never completion —
|
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
|
through an application-level FIFO queue — an implementation
|
||||||
relying on an undocumented grant order FAILS. A sixth static
|
relying on an undocumented grant order FAILS. A sixth static
|
||||||
control asserts the managed-deletion brain step applies its
|
control asserts the managed-deletion brain step applies its
|
||||||
mutation conditionally on the recorded §3.7 fence value — an
|
mutation conditionally on the recorded §3.7 fence epoch — an
|
||||||
unfenced brain-deletion path FAILS.
|
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
|
11. **Default-deny and granularity witnesses:** an agent grantee with
|
||||||
no active row is refused; with a `granted` row for category A
|
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
|
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
|
confirmed (§3.7). A second static control asserts every
|
||||||
enumerated sensitive-write route applies its step-1 brain
|
enumerated sensitive-write route applies its step-1 brain
|
||||||
commit as a fenced mutation conditioned on the recorded §3.7
|
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)
|
## 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
|
transition with a durable carry-over set the next cycle
|
||||||
processes first — so the one-cycle orphan bound binds every
|
processes first — so the one-cycle orphan bound binds every
|
||||||
cycle that reports completion — and every brain mutation under
|
cycle that reports completion — and every brain mutation under
|
||||||
a locator lock is fenced by a conditional application the next
|
a locator lock is fenced by a conditional application; per
|
||||||
holder's commit invalidates), so live interleavings between
|
revision 10 the fence value is an ABA-resistant per-locator
|
||||||
any two mutators are excluded by one serialization protocol,
|
fence EPOCH — minted fresh by every mutation, byte-identical
|
||||||
and stale external tails are excluded by the fence (§3.7,
|
recommits and transitions to absence (unique tombstone)
|
||||||
§4.5, §4.7, §7.16).
|
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
|
17. The compare-and-delete managed-deletion step: deletion step 2 is
|
||||||
conditioned on the PAIR of the target row's uuid `id` (the
|
conditioned on the PAIR of the target row's uuid `id` (the
|
||||||
immutable row-incarnation identity) and its monotonic
|
immutable row-incarnation identity) and its monotonic
|
||||||
|
|||||||
Reference in New Issue
Block a user