Repository navigation
An identity that moved, a search that only knew where it moved to, and the duplicate that followed - #11596
An identity that moved, a search that only knew where it moved to, and the duplicate that followed#11596briansrls wants to merge 14 commits into
Conversation
…d the duplicate that followed
gunbc#11485 relocated the review sheet's identity from Drive's appProperties to
properties. The reason was right -- the bootstrap create and the recurring search
run under different OAuth clients, and an app-private marker reads as ABSENT to the
other one, which is itself a way to mint a duplicate. The search query was rewritten
to match. Both halves are correct read alone.
What neither half said is that a file already carrying the old field is still the
review sheet. The operator's live spreadsheet was such a file. The next converge
searched, got a clean well-formed EMPTY result, and created a second spreadsheet
beside one holding real data. Nothing refused, because nothing failed: the lookup
answered the question it was asked. It was recovered BY HAND, and nothing in the
model would have recovered it.
THE EARLIEST UNJUSTIFIED BOUNDARY IS NOT THE QUERY. review_sheet_search_query
implements its own contract correctly. The boundary is one link up, where the
identity RELATION is declared: the relation a converge needs is "is this the review
sheet", and the query was rewritten as though the field NAME were that relation.
Those agreed before the move and agree again once every file has migrated. The
in-between is exactly where this repository stood, and no declaration anywhere said
the in-between existed.
WHAT LANDS.
extdeps.google.drive gains UpdateFileProperties, PATCH /files/{id}. PATCH rather
than PUT because the merge semantics ARE the safety property: the properties map
merges by key, so writing one key leaves every property this repository never wrote
untouched, where a PUT would replace the resource and drop them. The superseded
field is deliberately NOT cleared -- a file carrying both markers is reachable by
either search, which is the state that fails safe while any reader of the old field
may still exist, and clearing it is a second write owed its own readback.
gunbc.review_sheet_drive_converge gains the superseded location and the reading
over it. SupersededSearchReading = SupersededNotConsulted | SupersededRead, and
that first arm is the whole structural claim rather than bookkeeping: "we did not
look" can no longer arrive at the decision wearing the same shape as "we looked and
found nothing", and NO PATH LEADS FROM IT TO Apply. A caller that skips the second
read cannot mint a file, whatever the first read said.
A CREATE NOW REQUIRES ABSENCE ESTABLISHED ACROSS THE WHOLE IDENTITY, not across its
current spelling. Every refusing arm of the superseded read -- unreadable,
incomplete, paged, duplicated -- refuses the converge rather than falling through,
because each is precisely the state that cannot tell a migrated drive from an
unmigrated one. Answering "create" there is this same defect repeated one
generation later.
THE SECOND SEARCH IS ISSUED ONLY WHERE ITS ANSWER CAN CHANGE THE DECISION, which is
also the only place it is safe to skip. An adopted sheet settles the identity, so
the steady state -- every run after the first -- issues exactly the one files.list
it issued before this change.
THE READBACK ASSERTS THE ID, NOT A COUNT, and that is not pedantry. files.update
answering 200 establishes that Drive accepted a write, not that a search on the
current marker now reaches this file, which is the only property the migration
exists to produce. So verification re-asks the ORIGINAL question -- the query that
found nothing before the write -- and requires the answer to be the file we
patched. Exactly-one would also be satisfied by a concurrent create elsewhere, and
adopting that would hand the converge a different spreadsheet than the one holding
the operator's data: the original defect with the roles reversed.
EVIDENCE. Twelve witnesses green by execution, eight new. The wall and its controls
are paired deliberately: unconsulted_superseded_search_refuses_the_create supplies
the EXACT input shape the old fold answered Apply-create for, so it is red against
the previous behaviour rather than merely true; absence_under_both_markers_still_creates
is the positive control without which a fold that refused every absence would
satisfy every other claim while leaving the converge unable to mint the first sheet.
The remaining four are the pre-existing claims, re-shaped by the signature change
and re-run.
THE CLASS IS FILED as gunbc.recurring_failure_mode
identity_relation_modelled_at_its_current_spelling_only, ceiling 3 with the trigger
naming the capability: an identity relation whose locations are an ordered set with
the resolver derived from it, so a relocation is an APPEND and a lookup reading one
element is unwritable. The row also records why no witness held this -- gunbc#11485
shipped a claim asserting the query names `properties`, which is TRUE, went green,
and is about the query's spelling rather than about the relation it decides. The
claim nobody writes is that a subject recorded under the PREVIOUS spelling is still
found.
NOT CLAIMED HERE: a live run. The Drive half has not been executed against the real
API since this change, and the operator's sheet was already migrated by hand, so the
migration arm's live inhabitance is owed by the next real converge rather than
asserted by this PR.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ould not fail
Review 67612 found two things and they are one thing. Taking them in the order
they actually happened rather than the order they were reported.
I AUTHORED THE QUERY SHAPE TWICE TO VARY ONE TOKEN. review_sheet_superseded_search_query
restated `has { key='`, `' and value='`, `' } and mimeType='` and `' and trashed=false`
so that one field name could differ -- two sources for one fact, where an edit to
either clause silently diverges the other, and the diverging thing is precisely the
"identical except the field" relation the migration decision rests on.
AND THEN, HAVING BUILT THE RELATION TWICE, I REACHED FOR A TEST THAT THE TWO COPIES
AGREED. That is validation standing exactly where construction was available, and it
is the move DESIGN section 5 names: a check that re-states a constraint the model
could have carried. The duplication did not merely coexist with the bad test -- it
CREATED the job the bad test was written to do.
THE TEST WAS WORSE THAN ABSENT. Its final conjunct asked whether the legacy query
contains "properties has { key". The legacy query contains "appProperties has { key",
where the P is capital, so the lowercase pattern never matched, the negation was
permanently true, and the `||` short-circuited before the other query was ever
inspected. Green by construction, carrying no information, while its own annotation
cited it as establishing the property the migration decision rests on -- section 4b's
decoration, and the reason that section says to ask whether the RED is authorable
BEFORE writing the check.
THE FIX IS THE CONSTRUCTION, AND IT DISSOLVES THE TEST RATHER THAN REPAIRING IT. One
review_sheet_marker_query(marker_field, marker_value); review_sheet_current_marker_property_field
becomes a declaration beside the superseded one; both wrappers delegate. "Identical
except the field" is now asserted NOWHERE because it cannot be false -- there is one
query shape and the field is the only thing either caller supplies.
WHAT REPLACES IT IS THE RESIDUE THAT CAN STILL GO RED, and I established that by
MUTATION rather than by reading, because reading is what produced a vacuous check in
the first place:
the_superseded_field_is_not_the_current_one -- red when the superseded field is
edited to "properties". That is not a hypothetical: the second search would then
ask the first question again, answer absent for the same reason, and open the
create arm over a drive holding a legacy-marked sheet. The original defect,
reached through the machinery built to prevent it.
each_marker_query_is_the_shared_builder_at_its_declared_field -- red when either
wrapper drifts from the shared fold (mutation: one wrapper appends " and
starred=true").
Both mutations observed FALSE, both restored, both re-observed TRUE, and the working
tree re-checked for residue of either mutation. Sixteen witnesses in the module green
by execution afterwards.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Both findings confirmed and fixed in 19f6e22. They are one thing, and taking them in the order they actually happened rather than the order they were reported makes the repair obvious. The duplication came first, and it created the job the bad test was written to do. I authored the query shape twice to vary one token. Then, having built the relation twice, I reached for a test that the two copies agreed — validation standing exactly where construction was available. And the test was worse than absent, by the mechanism you named. The fix is the construction, and it dissolves the test rather than repairing it. One What replaces it is the residue that can still go red, and I established that by mutation rather than by reading — reading is what produced a vacuous check in the first place:
Both restored, both re-observed The first of those guards something real rather than a style rule: if the superseded field were edited to the current spelling, the second search would ask the first question again, answer absent for the same reason, and open the create arm over a drive holding a legacy-marked sheet — the original defect, reached through the machinery built to prevent it. — sent from zesty-crane-846 |
briansrls
left a comment
There was a problem hiding this comment.
HOLD — source-reviewed exact head 19f6e22585ae643811134ebf17c516e63ba6a104.
The incident analysis is right, but this implementation does not yet close the identity relation it names.
-
The PATCH success body cannot decode under its declared field mask.
UpdateFilePropertiesrequestsfields=idand maps200toDriveFile, whose required fields includenameandmimeType. A real successful PATCH can therefore becomeRestExchangeUndecodable, and this PR explicitly has no live migration run. Either request every required field or introduce the narrow response carrier this operation actually asks GitHub Drive to return. -
The superseded location is skipped exactly when a cross-generation duplicate can exist.
read_superseded_markerreturnsSupersededNotConsultedwhenever the current-marker search finds one file, andensure_review_spreadsheetimmediately returnsNoop. Therefore current-marker file A plus superseded-marker file B is reported converged, although the PR's own failure-mode row says the lookup owes both locations until the old population is established empty. This is the duplicate already minted by the incident, merely hidden by the new/current result.
Until a retirement receipt exists, read and reconcile the full identity extent on every decision that would adopt or create: absent under both may create; the same file under both may adopt; different file IDs must conflict; any unread/incomplete location must refuse. A union search derived from the identity-location carrier would also satisfy that contract.
Nonblocking but worth keeping visible: UpdateFileProperties introduces another hard-coded gunbcReviewSheet spelling beside the declared marker key. The language limitation is real, but it remains an unpinned duplicate authority.
Please do not run or merge this head as the recurring sheet converge. The present source can still hide an existing duplicate and its migration operation has no executable successful decode.
briansrls
left a comment
There was a problem hiding this comment.
Additional blocking finding on the same head: the superseded-marker read cannot generally observe the incident it claims to repair.
The PR says the marker moved from appProperties because bootstrap creation and recurring search use different OAuth clients. Google Drive defines appProperties as private to the requesting application. But read_superseded_marker performs the legacy appProperties query through the current drive.Files credential—the recurring client. In the intended cross-client case, that client cannot see the old marker, so the legacy query can answer a clean SheetAbsent against the original file and the create arm opens again.
A two-query fold is insufficient when one query is structurally blind under the active credential. Recovery needs one of:
- a one-time migration read under the original creating OAuth client;
- an operator/recorded legacy file ID that is independently read and patched;
- or another observable identity shared across clients.
Until that acquisition boundary exists, appProperties absence under the recurring client must not be treated as evidence that no legacy-marked sheet exists. This is the same earliest boundary as the original incident, not a separate optimization.
…s editing A side-chat review held this PR on a visibility boundary, and it is right. The superseded search queries appProperties. extdeps.google.drive -- three hundred lines above the operation I added to it -- already states the governing fact, in an annotation written when gunbc#11485 moved the marker: "A property private to the creating app is invisible to the searching app, so the search would have answered SheetAbsent against a file that exists and the converge would have minted a second spreadsheet." That is my superseded search exactly. It reads an app-private field, this repository never observes which OAuth client its token belongs to, and I treated an empty result as absence and opened the create arm. In the ONE scenario this change was written for -- a bootstrap create under one credential and a recurrence under another -- the search returns empty against a live sheet and the converge mints a duplicate beside it. The fix reproduced the defect it exists to close, one layer in. It is also the class I FILED IN THIS SAME PR. identity_relation_modelled_at_its_current_spelling_only cites absent_reads_identically_to_never_looked as its nearest neighbour and explains the boundary between them; I then built a fresh instance of the neighbour. A row is not a wall, and writing one about a class does not make its author immune to it. THE REPAIR KEEPS THE ASYMMETRY, WHICH IS WHAT STOPS IT BECOMING AN OVER-PROHIBITION (section 4d). A POSITIVE find needs no caveat at all: seeing the file IS the proof it was visible, so the migration path is untouched. Only the ABSENT arm is conditioned, on a SupersededMarkerVisibility the caller supplies. An empty superseded result has two preimages -- no legacy sheet, or a legacy sheet this client cannot see -- and the response cannot tell them apart, so the standing decides rather than the response. WHAT THAT COSTS, STATED PLAINLY RATHER THAN BURIED. The CLI supplies the honest value, which is unobservable, so a drive where neither marker finds anything now REFUSES instead of creating. A genuinely empty drive therefore cannot auto-mint its first sheet until someone establishes the client or supplies the file id, and the refusal names both remedies rather than just stopping. That is a real behavioural narrowing. It is the right trade -- refusing costs an operator one manual step, and creating wrongly costs a live spreadsheet going dark while every later converge adopts the replacement -- but it is a narrowing and the reader should see it. EVIDENCE: absence_under_an_unobservable_superseded_client_refuses_the_create, and its RED is authorable rather than asserted. Mutating the unobservable arm back to Apply-create -- the behaviour this commit removes -- makes it return FALSE; restored, TRUE. Six sibling claims re-run green beside it, including absence_under_both_markers_still_creates, which now supplies an ESTABLISHED visibility and is the control proving the create path is still reachable rather than walled off. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
The HOLD is correct and the fix is in 92cae60. This one is worth stating bluntly: the fix reproduced the defect it exists to close, and the authority was in the file I was editing.
That is my superseded search exactly. It reads an app-private field; this repository never observes which OAuth client its token belongs to; I treated an empty result as absence and opened the create arm. In the one scenario this change was written for — bootstrap under one credential, recurrence under another — the search returns empty against a live sheet and the converge mints a duplicate beside it. It is also the class I filed in this same PR. The repair keeps the asymmetryA positive find needs no caveat — seeing the file is proof it was visible — so the migration path is untouched. Only the absent arm is conditioned, on a What it costs, stated rather than buriedThe CLI supplies the honest value — unobservable — so a drive where neither marker finds anything now refuses instead of creating. A genuinely empty drive cannot auto-mint its first sheet until someone establishes the client or supplies the file id; the refusal names both remedies rather than just stopping. That is a real behavioural narrowing. I think it's the right trade — refusing costs an operator one manual step, creating wrongly costs a live spreadsheet going dark while every later converge adopts the replacement — but it is a narrowing, and a reviewer should weigh it rather than discover it. Evidence
Note the prior floor red on — sent from zesty-crane-846 |
…was dead
Review 67720 is right and the finding is sharper than the caveat I wrote myself. I
told the operator this change "narrows" the create path and that it stays reachable
once someone supplies the basis. Nothing could supply it.
SupersededFieldVisibleToThisClient had NO PRODUCTION CONSTRUCTOR. The only thing
building it was a witness fixture, so: an empty drive always refused; the refusal
named two remedies -- establish the client, or supply the file id -- and NEITHER
EXISTED AS AN INPUT; and the two claims asserting a create was still reachable were
green only through a value the actuator never emits. Deleting that fixture's
visibility would have touched no running entry point while bootstrap stayed dead.
That is the pairing obligation inverted. Supplying an input removed the last
execution of the real path, and the claim that was supposed to be the control for
over-prohibition was the thing hiding it -- DESIGN section 3's designed fixture that
keeps passing by reaching the same verdict through a different mechanism, and
section 4d's cost you never see because it looks like rigor.
TWO REAL ROUTES, READ FROM DISK, one per situation, because naming one would leave
the other refusing with no route -- which is the defect being repaired:
.gunbc/review-sheet-legacy-file-id adopt this sheet; it is migrated through the
same plan, so the marker is written and the
readback still has to find it
.gunbc/review-sheet-no-legacy-sheet this drive holds none; a create is permitted
THE ID IS CONSULTED AHEAD OF EVERY SEARCH, and that ordering is the point rather than
an optimisation: the id exists precisely for the case where NO search can reach the
file, so consulting the searches first and falling back would make the remedy
conditional on the failure mode it was supplied to route around.
THIS IS A HumanIntervention IN THE STRICT SENSE RATHER THAN A GAP DRESSED AS ONE.
Whether a drive holds a sheet marked with an app-private property THIS CREDENTIAL
CANNOT SEE is not observable through this credential at all -- no read closes it, so
it is not a capability waiting to be built. A human with the Drive UI sees the file;
this process cannot. The declaration is the whole remedy, not a placeholder for one.
THE FIXTURE NOW ROUTES THROUGH THE PRODUCTION FOLD. w_visible() calls
visibility_from_declaration rather than naming the arm, so these claims exercise what
the actuator calls and deleting that fold reds them. Beside it a control the change
did not have: no_declaration_leaves_the_superseded_visibility_unobservable, whose RED
is authorable and was observed -- mutating NoDeclaration to read as visible turns it
FALSE. The decision-level claim correctly stays green under that mutation because its
subject is the decision and it supplies its visibility directly; the fold now has its
own control and the decision has its own, which is the split this was missing.
Six claims green by execution, two of them new.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 67720 is right, and the finding is sharper than the caveat I wrote myself. I told the operator this change "narrows" the create path and that it stays reachable once someone supplies the basis. Nothing could supply it. Fixed in bd374a9.
That is the pairing obligation inverted: supplying an input removed the last execution of the real path, and the claim meant to be the control for over-prohibition was the thing concealing it. Two real routes, one per situationNaming one and not the other would leave the other refusing with no route, which is the defect being repaired:
The id is consulted ahead of every search, and that ordering is the point rather than an optimisation: the id exists precisely for the case where no search can reach the file, so consulting the searches first and falling back would make the remedy conditional on the failure mode it was supplied to route around. This is a The fixture now routes through the production fold
Worth noting what that mutation didn't do: Six claims green by execution, two new. — sent from zesty-crane-846 |
… not have caught it
Review 67745 is right on both counts and the second one is the lesson.
WRONG Filesystem. `std.resources` Filesystem is a RESOURCE whose read capability is
`read`, takes a TextFilePath and returns only `content`. The shape this reader uses
-- `Filesystem.Read` returning `.success`, `.content` and `.error` -- is the SERVICE
in extdeps.filesystem.filesystem_io, which I never imported. A resolved declaration
wins over a service of the same spelling, so the resource shadowed the service and
`Read` was not a method on it. `trim` was bare with no std.algebra import beside it.
The corrected imports are exactly what gunbc.instruments.github_app_acquire already
uses for the same job, and I could have copied them from the module I had open two
hours earlier: std.algebra { trim }, extdeps.filesystem.filesystem_io { Filesystem },
and std.resources { Network } alone -- with std.resources.Filesystem named in the
`uses` clause, qualified, which is the only place the resource belongs.
MY VERIFICATION WAS WORTHLESS AND THAT IS THE PART WORTH RECORDING. I typechecked by
running the CLI entry with --function nope, took NoSuchFunction as proof the module
was sound, and reported it as such. That check reaches no body: it is the rostered
class an_unreached_entry_body_is_never_typechecked, and it will report GREEN for any
unresolved name in any function the entry does not call. So the defect was not caught
late; it was never looked for, and I said "typechecks through the CLI" about a body
nothing had compiled.
WHAT REPLACED IT IS EXECUTION, on the exact function. A probe that imports
read_superseded_declaration and matches its result was run against the live
filesystem. With no declaration present both declared paths are read and the fold
answers NoDeclaration. With .gunbc/review-sheet-legacy-file-id present it
short-circuits on the first read and answers DeclaredLegacySheetId carrying the value
FROM DISK -- 1CzExampleLegacyFileId, which no fixture supplied. That is the arm the
review correctly said had no compiling producer, now green by execution rather than
by a typecheck that never ran.
THE GENERAL REPAIR IS NOT DILIGENCE. neat-pike-677's handoff names it from the other
side of the same night: eight review findings on gunbc#11552, every one a
single-authority or honest-reporting defect, two of them reintroduced WHILE writing
the memory about that class -- and the fix was not notes, it was the census that
finds identifiers called but neither declared nor imported. This commit is the fourth
instance today of the same shape. A probe that REACHES the body is the cheap version
of that census and it takes one file.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 67745 is right on both counts, and the second one is the lesson. Fixed in 88da703. Wrong The corrected imports are precisely what My verification was worthless, and that is the part worth recordingI "typechecked" by running the CLI entry with What replaced it is execution on the exact functionA probe that imports
That is the arm you correctly said had no compiling producer, now green by execution rather than by a typecheck that never ran. The general repair is not diligenceThe handoff from the session that landed #11552 names it from the other side of the same night: eight review findings there, every one a single-authority or honest-reporting defect, two reintroduced while writing the memory about that class — and the fix wasn't notes, it was the census that finds identifiers called but neither declared nor imported. This is the fourth instance of that shape today. A probe that reaches the body is the cheap version of that census and it takes one file. — sent from zesty-crane-846 |
Review 67754 found the arm I added to close the duplicate-mint reopening it, and the
authority is in the module I was calling. extdeps.filesystem.filesystem_io states it
plainly: absence is established by a successful listing, NEVER by a failed read --
Read answers success=false both for a path that does not exist and for one that
exists and cannot be read, those two worlds have opposite correct actions, and a
consumer that concludes "not there" from a read failure FAILS TOWARD GOOD NEWS.
THE CONCRETE PATH, WHICH IS NOT HYPOTHETICAL. An operator writes BOTH declarations --
the id, which is the specific statement my own annotation says must win, and the
absence -- and the id file is unreadable through mode bits, a bad mount, or a symlink
the runner cannot open. My reader tested id_read.success, got false, fell through to
the absence file, which reads fine, and reached Apply-create. That mints a second
spreadsheet beside the very legacy sheet the operator had just declared by id: the
defect this whole change exists to close, reached through the one arm the change
added to close it.
THE FOLD ALREADY EXISTED AND I PROJECTED PAST IT. filesystem_exact_read consumes
content, success, error AND error_kind and answers FilesystemExactPathRead |
Absent | Unreadable | KindUnrecognized, where only ABSENT concludes absence and it
does so from the host's own NotFound rather than from a Bool. I read .success and
.content directly instead, which is also an unconverted consumption site growing the
population filesystem_read_outcome_adoption_standing is shrinking.
WHAT LANDS: SupersededMarkerDeclaration gains DeclarationUnreadable, which refuses
the whole decision rather than degrading. Both files route through
filesystem_exact_read. An id that is present-but-unreadable NEVER advances to the
second file; only a host-typed ABSENT does, which is the one arm that genuinely means
"this was not declared". An EMPTY file is also a refusal rather than a shrug: an
operator who meant to declare no legacy sheet writes the other file.
EVIDENCE IS EXECUTION AGAINST THE REAL FILESYSTEM, on the exact function, because a
typecheck through an unreached entry is what let the previous defect through:
A) neither file -> NoDeclaration
B) both, id readable -> id wins, LEGACY-ID-123
C) both, id chmod 000 -> REFUSES, "the host refused this read as
permission_denied: Permission denied (os error 13)"
C is the reviewer's exact scenario and it is the one that used to create. Plus a
decision-level claim, an_unreadable_declaration_refuses_the_whole_decision, green
beside three siblings.
THIS IS THE FIFTH INSTANCE TODAY OF ONE SHAPE -- an absence asserted from something
that did not establish absence. The previous four were mine too. The pattern is not
carelessness about files; it is reaching for the nearest channel that answers rather
than the fold that classifies, and the fold has existed in every case.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ly ignorance
Review 67779 found the arm I added to close the duplicate doing it again, by a third
route. Both findings are real.
THE SHORT-CIRCUIT WAS SILENT WRONGNESS. DeclaredLegacySheetId applied the migration
without reading `observed` or `superseded`, both of which converge_review_spreadsheet
had ALREADY COMPUTED and handed in. The case my annotation never considered: current
marker absent, superseded search naming file A, declaration naming B. The fold patches
B, verify_marker_migration sees only B and answers MigratedAndVerified -- and A stays
on the superseded marker, goes dark, and the run reports success. That is the same
identity split the failure-mode row in this very PR describes, and my own annotation
arguing for the ordering is what made it look deliberate.
It also bypassed the CURRENT search's refusal arms, so a write could land while it was
still unknown whether a current-marked sheet existed -- unreadable, incomplete, paged
and duplicated all stepped over. A line-stop that a later branch can skip is not a
line-stop.
THE RULE THAT KEEPS BOTH PROPERTIES, and it is one sentence: the id is honoured unless
a search POSITIVELY NAMES A DIFFERENT FILE. Absence, unreadability and partial listings
are exactly the ignorance the id was supplied to compensate for, so they do not veto it
-- that is what keeps this from becoming the over-prohibition that killed bootstrap two
revisions ago. A positive find that disagrees is two files answering for one identity,
which only an operator settles. A DUPLICATED superseded find is that same question, so
the declared id must be ONE OF the named files or the disagreement stands.
THE PAIRING FINDING IS ALSO RIGHT AND ITS REPAIR IS NOT A CLAIM. The witnesses
construct SupersededMarkerDeclaration directly and never call
read_superseded_declaration. Claims in this corpus are PURE, so no claim can call a
function that performs a filesystem read; asserting the pairing in a witness is not
available. The honest discharge is an executing entry point, which is the shape
gunbc.instruments.github_app_acquire already uses for its own custody reads rather than
asserting them in prose: review_sheet_declaration_receipt, argv-free, read-only,
performing the two reads the converge performs and reporting which declaration is in
force. Deleting the reader reds it.
EVIDENCE:
three new decision claims, each an arm the first cut got wrong --
a_declared_id_disagreeing_with_the_superseded_find_refuses (names both A and B)
a_declared_id_does_not_bypass_an_unreadable_current_search
a_declared_id_agreeing_with_the_superseded_find_migrates (the control, without
which a fold refusing every declared id would satisfy the other two while making
the id route dead)
and the receipt run live, twice: readable id -> exit 0; id at chmod 000 -> REFUSING,
"the host refused this read as permission_denied: Permission denied (os error 13)".
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 67779 found the arm I added to close the duplicate doing it again by a third route. Both findings are real. Fixed in 3ea1341. The short-circuit was silent wrongness
It also stepped over the current search's refusal arms, so a write could land while it was still unknown whether a current-marked sheet existed. A line-stop a later branch can skip is not a line-stop. The rule that keeps both propertiesThe id is honoured unless a search positively names a different file. Absence, unreadability and partial listings are exactly the ignorance the id was supplied to compensate for, so they don't veto it — that's what keeps this from becoming the over-prohibition that killed bootstrap two revisions ago. A positive find that disagrees is two files answering for one identity, which only an operator settles. A duplicated superseded find is that same question, so the declared id must be one of the named files or the disagreement stands. The pairing finding is right, and its repair is not a claimThe witnesses construct The honest discharge is an executing entry point, which is the shape EvidenceThree new decision claims, each an arm the first cut got wrong:
And the receipt run live, twice: readable id → exit 0; id at — sent from zesty-crane-846 |
… declaration names one of them Two reviews, two real findings, and the second one I had argued myself into. EFFECT PROPAGATION (review 67878). converge_review_spreadsheet now performs a filesystem read, and no stage requires a CALLER to declare a callee's resource: build_item_info populates resource_names from the item's own `uses` clause only, and the transitive effect fixpoint copies resource_names through unchanged. So there is no located refusal and the interpreter runs fine -- the failure surfaces one layer later in 05_emit_rust, which appends `&fs` per callee resource name at the call site while emitting the caller's signature from the caller's own `uses`: an unbound identifier, which that emitter's own header calls a fabricated realization. Fixed by declaring the binding on every function on the chain -- converge_review_sheet_all, converge_drive_half, converge_drive_half_cli -- and NOT on drive_half_exit, which consumes an already-computed report and reaches no read. Declaring an effect a function does not perform is its own defect. VERIFIED BY EMISSION RATHER THAN BY TYPECHECK, because typecheck is precisely what does not see this: a scoped rust emission of this closure now reports NO unbound-fs error. Its one remaining blocking error is at review_sheet_drive_converge.dag:258, `filter in branch condition` inside membership_from_complete_page -- a line this PR does not touch, landed by gunbc#11485 and already on main. THE DUPLICATED-SELECTION ARM (review 67876), and this is the one worth recording. decide_with_declared_id migrated when the operator's declared id was ANY MEMBER of a duplicated superseded find. The other ids stay on appProperties; the next run finds the migrated file, answers Noop, and read_superseded_marker never consults that field again once SheetObservedOne hits -- so they go dark with MigratedAndVerified reported. The harm this PR's own failure-mode row describes, reached through a POSITIVE observation rather than an empty one. I had reasoned that an operator supplying an id IS the adjudication a duplicate needs. The review's sentence is the correction and it is exact: A DECLARATION WRITTEN BEFORE THE SEARCH IS NOT A SELECTION AMONG FILES THE SEARCH THEN FOUND. The operator wrote that id without having seen the duplicates. It was also inconsistent with every neighbour in the same function: a single superseded file that is not the declared id already refuses for this exact reason, current-marker duplicates already refuse even when the declared id is one of them, and with no declaration superseded duplicates always refuse. The module's own standing rule says SheetDuplicated is a refusal and never a selection. One arm disagreed, and it was mine. The arm now refuses and names EVERY id, because the operator has to settle it with all of them in view. a_declared_id_among_superseded_duplicates_still_refuses asserts both ids appear; the agreement and disagreement claims re-run green beside it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Both findings are real and both are fixed in 243ec88. The second one I had argued myself into, so I want to name that rather than just patch it. Effect propagation (review 67878)Your mechanism is right and sharper than I'd have got to. Declared on every function on the chain — Verified by emission, not typecheck, since typecheck is exactly what can't see this: a scoped Rust emission of this closure now reports no unbound-fs error. Its one remaining blocking error is at The duplicated-selection arm (review 67876)
I had reasoned that an operator supplying an id is the adjudication a duplicate needs. Your sentence is the correction and it's exact: a declaration written before the search is not a selection among files the search then found. The operator wrote that id without having seen the duplicates. It was also inconsistent with every neighbour in the same function, as you note — a single superseded file that isn't the declared id already refuses for this precise reason, current-marker duplicates already refuse even when the declared id is among them, and with no declaration superseded duplicates always refuse. The module's own standing rule is that The arm now refuses and names every id, so the operator settles it with all of them in view. Also cleaned up in this push: three files ( — sent from zesty-crane-846 |
briansrls
left a comment
There was a problem hiding this comment.
HOLD — source-reviewed exact head 243ec88738c00f21c6c9cdbad048c841d31326e1.
The declaration reader, typed filesystem absence, disagreement refusals, and exact-ID migration readback are substantial repairs. Two blockers remain.
-
A current-marker hit still hides the legacy identity extent.
read_superseded_markerreturnsSupersededNotConsultedwhenever the current search finds one file, andensure_review_spreadsheetimmediately returnsNoop. Thus current-marker file A plus superseded-marker file B is reported converged whenever no legacy-ID declaration happens to be installed. The witnessexactly_one_match_adopts_without_writingpreserves this path explicitly. This is the cross-generation duplicate the incident created, now hidden by A rather than repaired. Until a migration-complete/old-population-empty receipt exists, adoption as well as creation must reconcile the full identity extent—or require a subject-bound operator declaration before treating A as the sole lineage. -
The PATCH success response still has no executable decode contract.
UpdateFilePropertiesrequestsfields=idbut maps HTTP 200 toDriveFile, whose required fields includenameandmimeType. No source change in this head narrows that carrier or widens the field mask, and the PR still carries no live migration receipt. A legitimate successful PATCH may therefore arrive asRestExchangeUndecodablebefore the exact-ID readback can run. Use a response carrier matching{id}or request every requiredDriveFilefield.
The operator-supplied file ID correctly repairs an invisible legacy file when present, but it cannot make the no-declaration/current-hit path safe, and it does not repair the wire decoder. Do not merge or run this head as the recurring converge.
…s its own response type Side-chat HOLD on 243ec88, two P0s, both real. P0-1 -- A CURRENT-MARKER HIT HID A LEGACY LINEAGE, and this is the adopt-path half of the original incident. read_superseded_marker skipped the second search whenever the current search found a file, so this live state reported converged: properties -> A appProperties -> B no declaration Noop on A, and B invisible to every later run. Exactly the cross-generation duplicate the create path was hardened against, reached through ADOPT instead. I had argued the skip as a cost saving -- an adopted sheet settles the identity -- and that sentence is only true if the identity has one spelling, which is precisely what this whole change exists to deny. A current hit now costs one extra files.list. ONLY A POSITIVE DISAGREEING FIND REFUSES, which is the rule this module already applies to a declared id: an absent, unreadable or partial superseded answer is the ignorance this migration generation lives inside, and refusing there would stop every steady-state run for a condition no read can settle (section 4d). A search that NAMES a second file is two lineages observed, and an operator retires one. P0-2 -- THE PATCH ASKED FOR LESS THAN ITS RESPONSE TYPE REQUIRES. UpdateFileProperties requested fields=id while mapping 200 to DriveFile, whose id, name and mimeType are all required. A perfectly successful PATCH would have decoded short and classified as RestExchangeUndecodable -- a write that LANDED reported as a transport failure, with the readback never running. The mask now names every required field of the type it is declared to produce. Asking for fewer is not an economy; it is a decode refusal waiting for its first success, and this arm has no live execution yet, so nothing would have contradicted it until the first real migration. EVIDENCE, three new claims and the one they correct: a_current_hit_beside_a_disagreeing_legacy_find_refuses names both A and B a_current_hit_matching_the_legacy_find_still_adopts one sheet carrying BOTH markers is one lineage, which is the steady state after any successful migration a_current_hit_with_an_unreadable_legacy_search_still_adopts the deliberate arm, so the wall above cannot become the over-prohibition that killed bootstrap earlier exactly_one_match_adopts_without_writing re-shaped: it passed SupersededNotConsulted and so preserved exactly the behaviour under review; it now names the reading it adopts under Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…copy beside it Review 67958, two findings, both mine and both created by the previous commit. THE ANNOTATIONS STILL CLAIMED THE OLD COST. Both said the superseded search is issued only when the current search finds nothing, so "the steady state issues exactly the one files.list it issued before this change". The commit that closed the adopt-path P0 made that read fire on SheetObservedOne too, so the steady state issues TWO -- and the sentence a later author would use to decide whether the second read is cheap was left asserting the opposite. Section 4c says an annotation must not restate what the declaration structurally says; restating it WRONGLY is the worse case, because it is the only version of the fact a reader can consult without re-deriving the fold. Both now say the cost was ACCEPTED rather than avoided -- one list call per converge, not per row -- and say why the refusing arms still skip it: they have already refused for a reason no superseded-marker file could repair, so the read could not change the decision. That is a reason, not a saving. WORTH RECORDING HOW ONE OF THEM SURVIVED. I rewrote that annotation in the previous commit and it did not take: the replacement was the one edit in that batch I ran WITHOUT an assert, the pattern did not match, and the write reported success. Every other edit in the same script asserted and would have failed loudly. The stale text then sat directly above the code contradicting it through a review round. THE TWO ARMS WERE BYTE-IDENTICAL. SheetAbsent and SheetObservedOne each constructed SupersededRead with the same query and the same visibility -- two copies of one relation, which is the exact forked-copy argument this PR itself makes about the query builder forty lines away. One perform_superseded_read now serves both, and the refusing arms remain the only ones answering NotConsulted. Four claims re-run green, including exactly_one_match_adopts_without_writing and absence_under_both_markers_still_creates -- the adopt and create controls that keep this pair of walls from having closed either path. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 67962, and it is the same class as the commit immediately before it -- an annotation asserting a behaviour the declaration does not have. Two in a row, which is worth saying plainly rather than fixing quietly. The note claimed an operator could run review_sheet_declaration_receipt "to see which declaration is in force". std.process ExitSuccess has NO reason channel, so three of the four arms exit zero and say nothing: an operator cannot tell "no declaration" from "declared absent" from "declared id B" -- all three are a silent exit 0. And declaration_text, written to render all four, had three arms no call site reached: git grep returned the definition and one DeclarationUnreadable use. The precedent the note cited is honest about exactly this. census_app_registration_instruction_receipt says outright that an already-acquired App "exits zero and produces no registration URL at all". I cited it for authority and then claimed a behaviour it explicitly disclaims. WHAT LANDS: declaration_text deleted, its one live arm inlined, and the note rewritten to say what the entry point IS -- a pre-flight refusal. Run it before a converge and it fails loudly when a declaration exists and cannot be read, which is the state that would otherwise surface mid-converge; exit zero means only that nothing here blocks. REPORTING WHICH DECLARATION IS IN FORCE NEEDS A CHANNEL ExitSuccess DOES NOT HAVE, and the tempting workaround is refused in the note rather than taken: returning ExitFailure for an informational path would conflate "nothing is wrong" with "this failed", which is the same conflation gunbc#11552 was reviewed for and repaired. Two unused imports dropped with it. EVIDENCE, executed both ways against the real filesystem: no declaration -> both paths read, exit 0, silent; id at chmod 000 -> "the declaration at .gunbc/review-sheet-legacy-file-id could not be read: the host refused this read as permission_denied: Permission denied (os error 13)". Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 67979. The first finding is the same hole one commit later, reached through
the arm I had just added.
decide_with_declared_id answered Noop whenever the current-marker find EQUALLED the
declared id, without consulting superseded at all. So: an operator declares A; a later
run finds the current marker on A and the superseded search names B; the fold answers
Noop, the converge reports adopted, and B goes dark with success reported. Installing
a declaration SILENTLY DISARMED the wall this same module enforces without one --
adopt_unless_a_legacy_lineage_disagrees, added in the commit before last, with its own
control claim, for exactly this state.
The reasoning error is small and worth naming: I read "the declared id matches, so
there is nothing to migrate" as "so there is nothing to check". Those are different
questions. The declaration decides WHICH file is ours; it never decides whether the
other one matters. The arm now routes through the same fold rather than
short-circuiting, and the witness set -- which had no case with a declaration present
AND a current hit, which is why nothing caught it -- gains both halves:
a_declaration_matching_the_current_hit_still_refuses_a_second_lineage names A and B
a_declaration_matching_the_current_hit_adopts_when_no_second_lineage_exists
the control, so the wall has not closed the ordinary post-migration steady state
THE THIRD COPY OF THE PROPERTY NAME is real and is annotated rather than repaired,
because this operation cannot repair it. review_sheet_marker_property_key is the
authority every SEARCH query is built from; the write side spells it as a literal
because the body builder emits field names as SYNTAX and cannot take a field name from
a parameter. CreateFile already carries the second copy and states that constraint.
This PATCH is the third, and the note now says so plainly -- adding it does not make
the limitation new, it makes it WIDER, and what closes it is a body builder that
accepts a field name as a parameter, at which point all three collapse into the one
declaration. Until then no claim can reach these literals and the agreement is
asserted by a human reading three lines.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
HOLD — exact head 2ab08a832977412c4546f20dcb3f17f5ab5f8c95.
The two prior P0s are repaired:
- every non-refusing current observation now performs the superseded-marker read;
UpdateFilePropertiesnow requestsid,name,mimeType, satisfying the requiredDriveFileresponse fields.
The remaining blocker is now explicit policy rather than a missed branch:
adopt_unless_a_legacy_lineage_disagrees returns Noop when the current marker names file A and the superseded read is SheetAbsent, unreadable, incomplete, or paged. The witness a_current_hit_with_an_unreadable_legacy_search_still_adopts deliberately pins that behavior.
That still admits the exact incident topology:
properties -> duplicate/current file A
appProperties -> original file B, invisible to this OAuth client
legacy search -> clean absent (or otherwise unreadable)
result -> Noop / SpreadsheetAdopted(A)
The positive-disagreement wall never fires because app-private invisibility is the reason B cannot be positively found. The converge then reports the replacement lineage as converged and leaves the original data dark. This is not merely uncertainty around a harmless steady state; it is the original failure mode after the duplicate has already been minted.
There is a second modeling tell at the same boundary: visibility_from_declaration(DeclaredNoLegacySheet) constructs SupersededFieldVisibleToThisClient. An operator declaration that no legacy sheet exists does not establish OAuth-client visibility. It may justify adoption/create under policy, but it is a different fact and should not be laundered into the visibility carrier.
Blunt recommendation: stop iterating this PR as one unit
Ten rounds and several defects introduced by the preceding repair are evidence that three subjects are entangled:
- Pure identity reconciliation — current observation × legacy observation × operator declaration, with an operator ruling on whether current-hit + unresolved legacy extent is converged or non-converged.
- One-time migration actuation — PATCH an explicitly selected file and independently read back the exact ID.
- Generation retirement — a subject-bound receipt that the legacy identity extent is retired, after which the second search and declaration are no longer required.
Split those. The pure decision table should land first and make the controversial arm impossible to hide in transport code. The effectful migration should then consume only its admitted plan and get a live specimen on a disposable/controlled sheet. The recurring converge should not report SpreadsheetAdopted while legacy extent is unresolved; use a distinct non-converged outcome or require the already-modeled operator declaration until a retirement receipt exists.
I do not recommend another solo patch round on this 1,500-line PR. Freeze this head as the study, recut the smaller authorities from current main, and review each exact SHA independently.
The exact-head witnesses workflow is also nonterminal as I write this, but the source HOLD is independent of CI.
|
Closing rather than rebasing, per the side-chat ruling that this PR be parked and its combined migration route not executed. The branch is kept, not deleted — Why it is closed rather than repairedThis PR took ten review rounds, and most of them found a defect introduced by the fix in the round before. The root cause was structural, not effort: it decided the meaning of each reading inside effectful routing, so every repair to one arm opened another. That diagnosis is what produced the recut, and the recut's first cut has now landed. Superseded by #11669 (merged): Cut 1 is deliberately bounded and does not repair the production converge. It provides the authority a future repair is written against. What this branch still holds, and where each piece goesSix files, 14 commits ahead of main. Not salvaged wholesale — the point of the recut is that these are rebuilt against the kernel rather than carried across with their semantics embedded:
Three standing constraints for whoever resumes this
Worth recording for the next reader: an empty 🤖 Generated with Claude Code |
#11485 relocated the review sheet's identity from Drive's
appPropertiestoproperties. The reason was right — the bootstrap create and the recurring search run under different OAuth clients, and an app-private marker reads as absent to the other one, which is itself a way to mint a duplicate. The search query was rewritten to match. Both halves are correct read alone.What neither half said is that a file already carrying the old field is still the review sheet. The operator's live spreadsheet was such a file. The next converge searched, got a clean, well-formed, empty result, and created a second spreadsheet beside one holding real data. Nothing refused, because nothing failed — the lookup answered the question it was asked. It was recovered by hand, and nothing in the model would have recovered it.
The earliest unjustified boundary is not the query
review_sheet_search_queryimplements its own contract correctly. The boundary is one link up, where the identity relation is declared: the relation a converge needs is "is this the review sheet", and the query was rewritten as though the field name were that relation. Those two agree before the move, and agree again once every file has migrated. The in-between is exactly where this repository stood, and no declaration anywhere said the in-between existed.What lands
extdeps.google.drive—UpdateFileProperties,PATCH /files/{id}. PATCH rather than PUT because the merge semantics are the safety property: the properties map merges by key, so writing one key leaves every property this repository never wrote untouched, where a PUT would replace the resource and drop them. The superseded field is deliberately not cleared — a file carrying both markers is reachable by either search, which is the state that fails safe while any reader of the old field may still exist; clearing it is a second write owed its own readback.gunbc.review_sheet_drive_converge— the identity's history.SupersededSearchReading = SupersededNotConsulted | SupersededRead { observation }. That first arm is the structural claim rather than bookkeeping: "we did not look" can no longer arrive at the decision wearing the same shape as "we looked and found nothing", and no path leads from it toApply. A caller that skips the second read cannot mint a file, whatever the first read said.A create now requires absence established across the whole identity, not across its current spelling. Every refusing arm of the superseded read — unreadable, incomplete, paged, duplicated — refuses the converge rather than falling through, because each is precisely the state that cannot tell a migrated drive from an unmigrated one. Answering "create" there is this same defect repeated one generation later (§5: a failure arm must refuse, never widen).
The second search is issued only where its answer can change the decision, which is also the only place it is safe to skip. An adopted sheet settles the identity, so the steady state — every run after the first — issues exactly the one
files.listit issued before this change.The readback asserts the id, not a count.
files.updateanswering 200 establishes that Drive accepted a write, not that a search on the current marker now reaches this file — which is the only property the migration exists to produce. So verification re-asks the original question, the query that found nothing before the write, and requires the answer to be the file we patched. Exactly-one would also be satisfied by a concurrent create elsewhere, and adopting that would hand the converge a different spreadsheet than the one holding the operator's data: the original defect with the roles reversed.Evidence
Twelve witnesses green by execution, eight new. The pairing is deliberate:
unconsulted_superseded_search_refuses_the_createsupplies the exact input shape the old fold answeredApply-create for, so it is red against the previous behaviour rather than merely true.absence_under_both_markers_still_createsis the positive control, without which a fold that refused every absence would satisfy every other claim here while leaving the converge unable to mint the first sheet.The remaining four are pre-existing claims, re-shaped by the signature change and re-run.
The class is filed
gunbc.recurring_failure_modeidentity_relation_modelled_at_its_current_spelling_only— ceiling 3, with the trigger naming the capability: an identity relation whose locations are an ordered set with the resolver derived from it, so a relocation is an append and a lookup reading one element is unwritable.The row also records why no witness held this. #11485 shipped a claim asserting the search query names
propertiesand the marker key. That claim is true, it went green, and it is about the query's spelling rather than about the relation the query decides. A witness discriminates only at the boundary it is pointed at, and every witness in that module pointed at the new spelling because the new spelling was what the change was about. The claim nobody writes is that a subject recorded under the previous spelling is still found.Not claimed here
A live run. The Drive half has not been executed against the real API since this change, and the operator's sheet was already migrated by hand — so there is no legacy-marked file left to exercise the migration arm against. That inhabitance is owed by the next real converge rather than asserted by this PR.
Follow-up to #11581.
🤖 Generated with Claude Code