From 2c026313242c688363298add120e0215debf53cc Mon Sep 17 00:00:00 2001 From: fred Date: Thu, 27 Aug 2026 03:47:21 -0500 Subject: [PATCH] custody contract revision 11: acquisition-token guard on the fence-advance (sol r10 F16 residual, F18) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The fence-advance is itself fenced against an older acquisition: a per-locator acquisition token minted by the lock authority at every lock grant, carried unchanged across the acquisition's brain operations and swap-loop retries, compared and recorded by the brain store atomically with every brain mutation (advance included). A superseded acquisition's delayed advance is refused, mints nothing, and yields no usable fence (mandatory abort-release-surface, expected on deadline supersession). The 'refused unconditionally' claim is precisified to the exact linearization boundary; the pre-step-1 interruption predicates are restated over exact content/database state, expressly permitting the advance's epoch/token change (F18). New §7.10 stale-advance refusal and pre-advance linearization controls; token invariants added to the fence static controls (§7.10, §7.16); §8 item 16 and preamble extended. --- docs/requirements/custody-schema.md | 216 ++++++++++++++++++++++++---- 1 file changed, 186 insertions(+), 30 deletions(-) diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index d965a665..b5663299 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -214,6 +214,39 @@ repair-observation variant, and a static fence-epoch-invariant control; §7.16's static fenced-commit control is restated over the epoch (F16, F17). +Revision 11 (sol r10 residual F16 + new F18): the fence-advance +itself is fenced against an older acquisition. §3.7 adds a +per-locator ACQUISITION TOKEN minted by the lock authority at every +lock grant — fresh, strictly increasing, existing before the +holder's first brain operation and carried unchanged through every +brain operation and swap-loop retry of that acquisition — and the +brain store records the greatest accepted token atomically with the +locator's epoch and content state, refusing any brain mutation, +the fence-advance included, that carries an older token. The +advance's acceptance condition is exactly this comparison (an epoch +condition would be circular, an unconditional mint would let a +terminated holder's delayed advance supersede a later holder's); a +refused advance mints nothing and returns no usable fence, with a +mandatory abort-release-surface transition that is an EXPECTED +outcome after deadline supersession, not a defect. Revision 10's +"refused unconditionally" claim is precisified to an exact +boundary: after the newer holder's advance linearizes, every +older-acquisition operation — its delayed advance included — is +refused; a stale content mutation linearizing BEFORE that advance +serializes entirely before anything the new holder relies on (the +advance preserves the content state it finds and mints after it), +indistinguishable from completion before the previous holder's +lock release — the defined legal outcome. The pre-step-1 +interruption predicates in §3.7, §4.7, and the §7.16 fault +injection are restated exactly — content presence, content bytes, +and database rows unchanged, the advance's epoch mint and token +recording expressly permitted — resolving their contradiction with +the mandatory advance (F18). §7.10 adds a stale-advance refusal +control (fresh-writer and repair-observation variants) and a +pre-advance linearization control, and extends the fence-invariant +static control with the token invariants; §7.16's static +fenced-commit control carries the token (F16, F18). + 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 @@ -466,8 +499,17 @@ 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. The fence is a per-locator **fence - epoch**: a value stored in the brain store, atomically readable + fence for the external store. Two per-locator values fence it: + an **acquisition token** ordering holders and a **fence epoch** + ordering mutations. The acquisition token is minted by the lock + authority at EVERY grant of the locator lock: a fresh, strictly + increasing per-locator value handed to the holder with the + grant — it therefore exists before the holder's first brain + operation, independently of any brain state — and carried + UNCHANGED through every brain operation of that acquisition, + including every retry of a swap loop; a holder never re-mints + or refreshes its token. The fence epoch is a per-locator 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 @@ -476,11 +518,18 @@ with contract 6 (`mode-conversion.md`), identity with 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 + recur. Three rules bind them. **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 + value, atomically with the mutation. **Token recording:** the + brain store records, per locator and atomically with the + locator's epoch and content state, the greatest acquisition + token it has accepted; EVERY brain mutation under a locator + lock — the fence-advance below included — presents its holder's + acquisition token, is REFUSED atomically when that token is + less than the recorded value, and records it on acceptance. + **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 @@ -488,37 +537,74 @@ with contract 6 (`mode-conversion.md`), identity with 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 + exclusivity. The advance's OWN acceptance condition is exactly + the token comparison — not the epoch (no fence exists for the + acquisition until the advance returns, so an epoch condition + would be circular) and not nothing (an unconditional mint would + let a terminated holder's delayed advance supersede a later + holder's): the token is minted at lock grant, so it exists + before the advance, and grants for one locator are totally + ordered, so the comparison encodes acquisition order. A refused + advance returns NO usable fence: the holder MUST NOT perform + any brain observation or mutation, MUST abort its protocol run + before any later step, release the lock if it still holds it, + and surface the error — and this refusal is an EXPECTED outcome + for an acquisition whose lock was deadline-released and + re-granted before its delayed advance applied, not a defect. + Every other 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 + fence value AND the token-recording comparison accepts, with + the checks 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 + per-locator conditions 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 + newer holder — is refused at an exact boundary. Once the newer + holder's fence-advance has linearized, EVERY operation of the + older acquisition is refused: its epoch condition fails (the + advance consumed its epoch, and no sequence of mutations can + re-present a consumed one — whether the intervening history + changed the bytes, recommitted byte-identical content, returned + the locator to absence, or consists of the advance alone), its + token comparison fails, and its own delayed fence-advance is + refused by the token comparison, minting nothing — a superseded + acquisition cannot manufacture a fresh fence. Before the newer + advance linearizes, a stale content mutation whose conditions + still hold MAY linearize first: the advance then finds the + post-mutation state, expressly preserves the content presence + and bytes it finds, mints its epoch after that mutation, and + the new holder's first relied-on observation follows its own + advance — so the stale effect serializes entirely before + anything the new holder relies on, indistinguishable from the + same operation completing before the previous holder's lock + release, an outcome the protocol already defines as legal (its + database half remains governed by the (`id`, `generation`) + pair, §4.5, §4.7). These are the only two outcomes: a stale + operation either serializes wholly before the new holder's + advance or is refused; it never applies after the advance, and + 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 fenced - mutation cannot fail its condition — not because it holds the + mutation cannot fail its conditions — 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 + only epochs minted since its fence-advance are its own, and + because lock grants are serialized by the lock itself, no + greater acquisition token can be recorded while it holds the + lock; 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 + brain-mutation path carries the fence and the acquisition + token, 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 + relies on; a path applying an unfenced or token-free brain + mutation fails the §7.10 and §7.16 static controls. **Steps.** Step 1 commits the content to the owning user's brain @@ -528,8 +614,11 @@ with contract 6 (`mode-conversion.md`), identity with 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 + step 2 commits. Interruption before step 1 leaves content + presence, content bytes, and every database row unchanged — the + post-acquisition fence-advance may already have minted an epoch + and recorded an acquisition token, the only brain change the + protocol permits before step 1. 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. @@ -623,10 +712,13 @@ 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, performs the §3.7 fence-advance — + the pointer's locator lock, performs the §3.7 fence-advance + under repair's own acquisition token — 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 + mutation — its delayed fence-advance included, refused by the + §3.7 token comparison — 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 @@ -725,6 +817,7 @@ with contract 6 (`mode-conversion.md`), identity with commits the content deletion to the user's brain repository as a FENCED mutation (§3.7 Brain fence — conditioned on the fence epoch recorded at the deleter's post-acquisition fence-advance, + carrying the deleter's acquisition token, and itself minting the locator's unique absence tombstone epoch), recording the target row's `id` AND `generation` as read after @@ -759,7 +852,11 @@ with contract 6 (`mode-conversion.md`), identity with 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 content presence, content bytes, and every + database row unchanged — the deleter's post-acquisition + fence-advance may already have minted an epoch and recorded an + acquisition token, the only brain change the protocol permits + before step 1. 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, @@ -1210,7 +1307,39 @@ declared profile table" means `profile_answers` (§3.5). 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 + NO unpointed content is resurrected at the locator. A + **stale-advance refusal control** exercises the §3.7 token + guard on the advance itself: writer W1 acquires the locator + lock and its mandatory fence-advance is suspended BEFORE its + atomic application; the independent supervisor terminates W1's + session at the deadline and the lock releases; the next holder + acquires the lock (receiving a greater acquisition token) and + completes its own fence-advance; W1's suspended advance is + then RESUMED and asserted REFUSED by the token comparison — + it mints no epoch and returns no usable fence — and W1's + protocol run is asserted to abort with the error surfaced, + performing no further brain observation or mutation, while + the next holder's fence remains valid and its subsequent + fenced mutation is asserted to succeed. A fresh-writer + variant runs the next holder as an ordinary §3.7 writer + through a full acknowledged write; a repair-observation + variant runs it as §4.5 reconciliation — repair advances, + observes content absence, W1's late advance resumed before + the DELETE is asserted refused and fenceless, and the DELETE + completes under its recorded (`id`, `generation`) token with + no unpointed content resurrected. A **pre-advance + linearization control** exercises the §3.7 legal-outcome + boundary: a terminated holder's stale content mutation is + scheduled to linearize immediately BEFORE the next holder's + fence-advance swap; the control asserts the store serializes + the stale mutation first, the advance preserves the + post-mutation content presence and bytes and mints its epoch + after it, the new holder's first relied-on observation + reflects the committed stale effect, and the end state is + consistent — equivalent to the stale operation having + completed before the previous holder's lock release — with + the stale operation's database half still governed by the + (`id`, `generation`) pair. 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 — @@ -1254,7 +1383,18 @@ declared profile table" means `profile_answers` (§3.5). 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. + FAILS. The same control asserts the §3.7 acquisition-token + invariants: the lock authority mints a fresh, strictly + increasing per-locator token at every lock grant; every + brain-mutation path — the fence-advance included — presents + its holder's token unchanged across every swap-loop retry; + the brain store's token comparison and recording are atomic + with the mutation they guard; the advance is refused when its + token is less than the recorded value; and a refused advance + yields no usable fence — an implementation whose advance + applies unconditionally, that re-mints or refreshes a token + within an acquisition, or whose holder proceeds to any brain + observation or mutation after a refused advance, 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 @@ -1326,7 +1466,10 @@ declared profile table" means `profile_answers` (§3.5). violates the §6.3 singleton constraint. 16. **Ordered-write protocol witnesses:** the §3.7 protocol is fault-injected at its interruption points: killed before the - brain commit, both stores are unchanged and the caller receives + brain commit, content presence, content bytes, and every + database row are unchanged — the post-acquisition + fence-advance's epoch mint and token recording are the only + permitted brain change — and the caller receives no acknowledgment; killed between the brain commit and the pointer upsert, the brain holds unpointed content, no pointer row exists, no read surface serves the content, and the caller @@ -1364,8 +1507,9 @@ declared profile table" means `profile_answers` (§3.5). enumerated sensitive-write route applies its step-1 brain commit as a fenced mutation conditioned on the recorded §3.7 fence epoch — recorded at the route's post-acquisition - fence-advance, the commit itself minting a fresh epoch — an - unfenced brain-commit path FAILS. + fence-advance, the commit itself minting a fresh epoch and + carrying the route's §3.7 acquisition token — an + unfenced or token-free brain-commit path FAILS. ## 8. Drafting additions (PRD §12.1 disclosure) @@ -1458,7 +1602,19 @@ UPDATE` as the first statement of its transaction, and the 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 + before the new holder's first mutation; per revision 11 the + fence-advance itself is guarded by an acquisition token — + minted fresh and strictly increasing by the lock authority at + every lock grant, carried unchanged across an acquisition's + brain operations and swap-loop retries, compared and recorded + by the brain store atomically with every brain mutation, the + advance included — so a superseded acquisition's delayed + advance is refused and mints nothing, a refused advance + yields no usable fence with a mandatory + abort-release-surface transition, and a stale operation + either serializes wholly before the new holder's advance — + the defined legal pre-release-completion-equivalent outcome — + or is refused), 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).