contract(custody-schema): revision 13 — withdraw wrong §4.5 repair attribution (sol r12 F20 residual)
ci/woodpecker/pr/ci Pipeline was successful
ci/woodpecker/pr/ci Pipeline was successful
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.
This commit is contained in:
@@ -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 —
|
||||
|
||||
Reference in New Issue
Block a user