From 8a03d99e3194d3f36cfb088d23b59ebc2beea010 Mon Sep 17 00:00:00 2001 From: fred Date: Thu, 27 Aug 2026 04:48:07 -0500 Subject: [PATCH] =?UTF-8?q?contract(custody-schema):=20revision=2013=20?= =?UTF-8?q?=E2=80=94=20withdraw=20wrong=20=C2=A74.5=20repair=20attribution?= =?UTF-8?q?=20(sol=20r12=20F20=20residual)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sol's r12 confirm closed F18/F19 and found one MINOR residual on F20: rev 12 assigned the terminated ordinary writer's committed-but-unpointed content to §4.5 repair, but §4.5 enumerates pointers and repairs the opposite state (pointer present, content absent) — unpointed content is outside its input, so the §7.10 assertion had no conforming transition. Per the prescribed correction: the §4.5 repair assertion is removed from §3.7 and §7.10; the no-upsert assertion stays; the state is what §3.7 and §7.16 already define — inert unpointed content (no pointer, no read path, no repair transition; a §4.5 cycle run against it changes nothing), never acknowledged, converging only through the client's retry as a fresh lock acquisition under a new token that recommits and completes the pointer upsert. Preamble Revision 13 paragraph added. --- docs/requirements/custody-schema.md | 38 +++++++++++++++++++++++------ 1 file changed, 31 insertions(+), 7 deletions(-) diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index 612d2ae6..6308a17f 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -268,6 +268,20 @@ pair-conditioned, while a terminated ordinary writer performs no pointer upsert and can continue only through a fresh acquisition under a new token (F20). +Revision 13 (sol r12 confirm, F20 residual): revision 12's +ordinary-writer branch wrongly assigned the terminated writer's +committed-but-unpointed content to §4.5 repair — §4.5 enumerates +pointers and repairs the opposite state (a pointer whose content +is absent); unpointed content is outside its input. The §3.7 +boundary text and the §7.10 control now state what §3.7 and §7.16 +already specified: the state is inert (no pointer references it, +no read path serves it, no repair transition exists for it — a +§4.5 cycle run against it changes nothing), the terminated run is +never acknowledged, and convergence comes only through the +client's retry as a fresh acquisition under a new token, +recommitting and completing the pointer upsert. No behavioral +change; the wrong repair attribution is withdrawn. + 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 @@ -619,9 +633,14 @@ with contract 6 (`mode-conversion.md`), identity with §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 + is exactly the inert step-1-to-step-2 interruption state this + section already defines (no pointer references it, no read + path serves it, and no automatic repair transition exists for + it — §4.5 repairs the opposite state, a pointer whose content + is absent), and the write converges only through the unacknowledged + client's retry, which is a NEW lock acquisition under + a fresh token — recommitting the locator and completing the + pointer upsert — 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 @@ -1399,10 +1418,15 @@ declared profile table" means `profile_answers` (§3.5). (`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 + run is asserted to perform NO pointer upsert and to receive + NO acknowledgment; the committed content is asserted + unpointed and inert — referenced by no pointer, served by no + read path, and subject to no repair transition (a §4.5 cycle + run against the state is asserted to change nothing) — and + convergence is asserted only through the client's retry, + which acquires the lock as a fresh acquisition + under a new token, recommits the locator, and completes the + pointer upsert to the pointed state (§3.7, witness §7.16). 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 —