Repository navigation
An identity collision is not a malformed document: give the object table its own authority - #9215
Conversation
…ble its own authority ClosureDocRefusal was one flat coproduct answering for three owners -- object population, closure/root facts, and member reads. closure_document_load_standing maps ClosureDocObjectCollision to LoadIdentityCollision and the five tag and reference causes to LoadDocumentMalformed, and per gunbc.scm.load_standing LoadDocumentMalformed is the ONE standing that standing_may_supersede_generation answers true for. So any consumer classifying those six together, at the grain of one wrapping arm, hands an identity collision the one standing permitted to overwrite a newer generation -- a valid generation destroyed over an honest hash coincidence, which is the DESIGN gunbc.scm specimen exactly. gunbc.scm.object_table_json now owns ObjectTableDecodeRefusal and its own cause-to-standing classifier. The closure classifier delegates rather than descending, so "classify an object-table cause at closure grain" has no spelling: the parameter can no longer name one. That landed rather than being asserted -- witnesses stopped compiling until they were rerouted through the owning authority. The new type is NOT in gunbc.scm.object_store, which departs from the literal plan. object_store is format-agnostic: it imports only v2.std.node and std.types and mentions JSON nowhere. These causes carry JSON tags, so homing them there is the layer inversion gunbc.scm.json_member's own header names. The object TABLE is a JSON-document concept; the object STORE is not. DECLARED RUNG, per arm rather than for the cut. Unrepresentable: naming an object-table cause at closure grain. NOT reached: the object-table classifier still returns into the shared LoadStanding vocabulary, so a wrong mapping inside the new module stays writable and mechanically preventable. Also not reached, and for an honest reason: repository_envelope still wraps ClosureDocRefusal where it consumes decode_object_table, because that function's failure population is genuinely mixed -- it can fail with member-read and unexpected-member causes it does not own. Narrowing that wrap would make the type lie in the other direction. Two floor-bug repairs ride along, found while wiring the above. decode_commit_members wrapped a MemberReadRefusal from read_member and read_string_member into RepositoryDecodeClosureDocRefusal, whose declared field is ClosureDocRefusal. Wrong coproduct, accepted silently. The correct arm -- RepositoryMemberReadRefused -- sits three and seven lines away in the same match, shape-identical, which is why review missed it. They compile because a coproduct value of the wrong coproduct type is admitted into a declared record field with no diagnostic; measured with a four-arm fixture where coproduct-vs-primitive refuses and an unresolved name refuses, so the check exists and fires at that position and this is a precise gap in it. That is the ordinary compiler floor and is handed to the compiler lane with the fixture. These two sites are the FIX, not the evidence. json_member's header is corrected rather than rewritten: it described this class in the past tense, naming four members, while two of them still did it. A carrier asserting a class is closed is read as evidence, so the false coverage claim was the more serious half. Witnesses: 72/72 across the four SCM modules. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…able
review 55811 is right that ClosureDocObjectTableRefused { cause: _ } can still
collapse every object-table cause onto one standing, collision included. The
classifier is correct, but the PR body and this module's annotation both said the
collapse "has no spelling", and that is false. Rung inflation in the carrier that
declares the rung is the worst place for it.
Stated precisely now. UNREPRESENTABLE: naming an individual object-table cause in a
match over ClosureDocRefusal -- the targeted, wildcard-free, reads-as-total
misclassification that was writable before. STILL WRITABLE: the wrapper-grain
collapse, whose rung is mechanically preventable; what changed is that it now needs
a bare binding over a foreign authority's population, which is a tell DESIGN names.
The review's proposed remedy is not taken, and the premise is measured rather than
argued: decode_object_step produces four ClosureDocMemberReadRefused causes and a
ClosureDocUnexpectedMember cause alongside the object-table ones, so that
operation's failure population is genuinely mixed. Narrowing its result to
ObjectTableDecodeRefusal would make the type claim an owner for causes it does not
own -- this cut's own defect, mirrored. Recorded with a next-rung trigger instead.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Thank you — review 55811 is correct on the finding, and it caught a real overclaim. Fixed in The finding is right and the prose was wrong
Corrected to state the boundary precisely:
Why the remedy is not taken
Measured on this branch,
That operation's failure population is genuinely mixed: decoding the object table can fail with member-read causes owned by This is the same reason the PR already declines the third leg of its plan ( Next-rung trigger, now recorded in the module: a On "falls short of the PR's stated authority cut"Half accepted. The prose overstated and is fixed. The cut is unchanged and I believe it stands: it removes the per-cause misclassification, gives the object table an owner and a classifier, and declares per-arm what it did not reach — including this exact gap, which the PR body already listed under "not reached" before the review landed. The overclaim was in a sentence elsewhere in the body that contradicted that list, which is precisely why it deserved catching. — sent from gentle-eagle-360 |
What this closes
ClosureDocRefusalwas one flat coproduct answering for three owners: the object population, closure/root facts, and member reads. That is not a tidiness problem, and the measurement is the whole case:ClosureDocObjectCollisionLoadIdentityCollisionUnknownKindTag/UnknownConnectiveTag/UnknownBehaviorTag/UnknownLabelTag/EdgeTargetUnresolvedLoadDocumentMalformedPer
gunbc.scm.load_standing,LoadDocumentMalformedis the one standingstanding_may_supersede_generationanswerstruefor. So a consumer classifying those six at the grain of one wrapping arm hands an identity collision the one standing permitted to overwrite a newer generation — a valid generation discarded over an honest hash coincidence. That is the DESIGNgunbc.scmspecimen reproduced.The shape
gunbc.scm.object_table_jsonownsObjectTableDecodeRefusaland its own cause-to-standing classifier. The closure classifier delegates rather than descending.Descent would have been correct, and it is what the two sibling populations do (
MemberReadRefusal,TargetReferenceRefusal— the classifier already descends twice, so descent is the settled convention of the function being edited, and wrapper-grain classification would be the deviation). Delegation goes one further: the closure classifier's parameter can no longer name an object-table cause, so the collapse has no spelling. It also stops the closure module growing an inner arm every time this module gains a cause.That landed rather than being asserted. The witnesses stopped compiling until they were rerouted through the owning authority — the guarantee demonstrating itself.
Why the new type is not in
object_storeThis departs from the literal plan, so:
object_storeis format-agnostic — it imports onlyv2.std.nodeandstd.types, and mentions JSON nowhere. These causes carry JSON tags. Homing them there is the layer inversionjson_member's own header names. The object table is a JSON-document concept; the object store is not.Declared rung, per arm
LoadStandingvocabulary, so a wrong mapping inside the new module stays writable and mechanically preventable.repository_envelopestill wrapsClosureDocRefusalwhere it consumesdecode_object_table, because that function's failure population is genuinely mixed: it can also fail with member-read and unexpected-member causes it does not own. Narrowing that wrap would make the type lie in the other direction — the same defect this PR removes, mirrored.Why a floor bug is fixed inside an SCM cut
decode_commit_memberswrapped aMemberReadRefusal(fromread_member/read_string_member) intoRepositoryDecodeClosureDocRefusal, whose declared field isClosureDocRefusal. The correct arm —RepositoryMemberReadRefused— sits three and seven lines away in the same match, shape-identical, which is why review missed it. Introduced by #9048.They compile because a coproduct value of the wrong coproduct type is admitted into a declared record field with no diagnostic. Measured with a four-arm fixture: coproduct-vs-primitive refuses, an unresolved name refuses, coproduct-vs-coproduct is admitted silently — so the check exists and fires at that position, and this is a precise gap in a working check rather than an absent one. Ordinary compiler floor ("values inhabit declared types"), handed to the compiler lane with the fixture.
These two sites are the fix, not the evidence — the fixture reproduces the hole independently, so repairing them hides nothing. They are here rather than in a separate PR because they are two lines in a function this cut already rewires.
The
json_memberheaderCorrected, not rewritten. It described this class in the past tense while naming four members, two of which still did it. A carrier asserting a class is closed is read as evidence, so the false coverage claim was the more serious half — and this PR cites that module as its precedent, which would otherwise mean citing an authority known to be false.
Evidence
72/72 across the four SCM witness modules:
repository_envelope28,commit_closure_json_v225,commit_closure13,load_standing6. Includesan_honest_collision_is_its_own_standing_and_never_supersedes, now routed through the wrapper so it proves delegation preserves the mapping end to end.🤖 Generated with Claude Code