From 8085982396e7f5c64a943b0febf6ad6b30175140 Mon Sep 17 00:00:00 2001 From: fred Date: Thu, 27 Aug 2026 04:19:19 -0500 Subject: [PATCH] =?UTF-8?q?contract(custody-schema):=20revision=2012=20?= =?UTF-8?q?=E2=80=94=20exact=20token=20comparison=20base=20case,=20split?= =?UTF-8?q?=20stale=20database-half=20boundary?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit sol r11 APPROVE minors: - F19: strictly-less-than refusal made explicit; absent recorded token compares lower than every minted token, first acceptance creates the record; §7.10 virgin-locator control + delayed-first-grant race. - F18 residual closed: §7.10 managed-deletion fault predicate restated as the exact §4.7 predicate (advance's epoch mint and token record permitted). - F20: pre-advance linearization boundary distinguishes database halves — pair-conditioned step 2 for deletion/repair; terminated ordinary writer performs no pointer upsert, retry is a fresh acquisition; §7.10 control runs both branches. - §8 item 16 revision-12 clause; preamble Revision 12 paragraph. --- docs/requirements/custody-schema.md | 88 ++++++++++++++++++++++++++--- 1 file changed, 79 insertions(+), 9 deletions(-) diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index b5663299..612d2ae6 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -247,6 +247,27 @@ 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). +Revision 12 (sol r11 minors F18 residual, F19, F20): three +exactness corrections to the revision-11 mechanism, no behavioral +change. §3.7's token comparison is made exact at both ends: +strictly less-than refuses (an already-recorded token re-presented +by a swap-loop retry or a later mutation of the same acquisition is +accepted), and an absent recorded token compares lower than every +minted token, so a virgin locator's first advance is accepted and +atomically creates the token record — with a §7.10 virgin-locator +control and a delayed-first-grant race variant (F19). §7.10's +remaining managed-deletion fault predicate ("both stores +unchanged") is restated as the exact §4.7 predicate — content +presence, content bytes, and database rows unchanged, the +advance's epoch mint and token recording expressly permitted +(F18 closed). The pre-advance-linearization outcome no longer +assigns the (`id`, `generation`) pair to every stale operation: +the §3.7 boundary text and the §7.10 control now distinguish the +database halves — deletion's and repair's step 2 stays +pair-conditioned, while a terminated ordinary writer performs no +pointer upsert and can continue only through a fresh acquisition +under a new token (F20). + 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 @@ -529,6 +550,16 @@ with contract 6 (`mode-conversion.md`), identity with 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. + The comparison is exact at both ends: it is strictly + less-than — re-presenting the already-recorded token, as a + swap-loop retry or a later mutation of the same acquisition + does, is accepted — and a locator with NO recorded token + compares as lower than every minted token, so a virgin + locator's first presented token is never refused by this + comparison and its acceptance atomically CREATES the token + record; an implementation whose absent-token comparison can + refuse or fail to record the first holder is nonconforming + (witness §7.10). **Fence-advance at acquisition:** immediately after acquiring the locator lock, before its first brain observation or mutation at the locator, @@ -581,9 +612,16 @@ with contract 6 (`mode-conversion.md`), identity with 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 + release, an outcome the protocol already defines as legal. What + the stale operation's DATABASE half may then do depends on its + protocol: a managed deletion's or repair's step 2 remains + conditioned on the recorded (`id`, `generation`) pair (§4.5, + §4.7) and cannot unpoint any later row incarnation; an ordinary + write's terminated run performs NO pointer upsert — its + database session is dead, the committed-but-unpointed content + falls into the existing step-1-to-step-2 interruption window + repaired by §4.5, and any retry is a NEW lock acquisition under + a fresh token, never a continuation of the dead run. 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 @@ -1184,7 +1222,11 @@ declared profile table" means `profile_answers` (§3.5). the next triggered reconciliation deletes the pointer and writes no content anywhere in the database (§4.5). The §4.7 protocol is fault-injected at both interruption points: killed before the - brain commit, both stores are unchanged; killed between the brain + brain commit, content presence, content bytes, and every + database row are 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; killed between the brain 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 @@ -1327,7 +1369,20 @@ declared profile table" means `profile_answers` (§3.5). 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 + no unpointed content resurrected. A **virgin-locator token + control** exercises the §3.7 absent-token base case: the FIRST + lock grant ever issued for a locator (no recorded acquisition + token exists in the brain store) performs its mandatory + fence-advance and is asserted ACCEPTED — the advance mints the + locator's epoch and its acceptance atomically creates the + token record — and the holder's subsequent fenced mutation + succeeds; a delayed-first-grant race variant suspends that + first holder's advance before application, terminates the + session at the deadline, lets a second holder acquire the + lock (receiving a greater token) and complete its own advance, + then resumes the first holder's advance and asserts it REFUSED + by the token comparison — the base case never admits a + superseded first grant. 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 @@ -1337,9 +1392,17 @@ declared profile table" means `profile_answers` (§3.5). 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 + completed before the previous holder's lock release. The + control runs BOTH database-half branches: with the stale + mutation a managed deletion's step-1 brain half, its stale + step-2 DELETE remains conditioned on the recorded + (`id`, `generation`) pair and is asserted to match ZERO rows + against a later row incarnation; with the stale mutation an + ordinary §3.7 writer's step-1 content commit, the terminated + run is asserted to perform NO pointer upsert — the unpointed + content is repaired by §4.5 within one cycle, and a retry of + the write is asserted to run as a fresh lock acquisition + under a new token. 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 — @@ -1614,7 +1677,14 @@ UPDATE` as the first statement of its transaction, and the 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 + or is refused; per revision 12 the token comparison is exact + at both ends — strictly less-than refuses, an absent recorded + token compares lower than every minted token so a virgin + locator's first advance is accepted and creates the record — + and the pre-advance-linearization outcome distinguishes the + stale database halves: pair-conditioned step 2 for deletion + and repair, no pointer upsert ever for a terminated ordinary + writer), 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).