Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion DESIGN.md

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion dag/gunbc/recurring_failure_mode.dag
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ data reachability_read_as_occupancy: RecurringFailureMode = RecurringFailureMode

data total_at_the_level_examined_blind: RecurringFailureMode = RecurringFailureMode {
identity: "total_at_the_level_examined_blind" as NonEmptyStr,
authored: "**total at the level examined, blind one level down** (a judgment is exhaustive over the type it matches and says nothing about the distinction that actually decides the outcome, which lives inside one of its arms. **The pairing is the whole content: the match is exhaustive AND wrong**, and the exhaustiveness is what hides it — there is no missing arm to report, no warning, nothing incomplete, so neither a reviewer reading the match nor a wildcard-free lens can see it. Specimen with a mutation receipt (gunbc.scm, 2026-08-22), **repaired on main 2026-08-25 by gunbc#8973 and kept in the past tense because the mechanism recurs while this instance does not**: a publication fold matched one outer arm carrying a JSON codec's entire refusal enum. It was total over that codec's refusal type, and the enum's arms carried three different publication remedies — a reader limitation, an absent-object problem over a well-formed document, and malformed bytes. Only the third may supersede a head slot, so the collapsed form let an OLDER READER OVERWRITE A NEWER WRITER'S DOCUMENT: data loss produced by the reader's own limitation, from a match that compiled and looked complete. Executed both ways — descending, four witnesses passed; collapsed, the witness driving all three remedies through the single outer arm went red; a temporary decode arm made the fold non-exhaustive; restored control passed. **None of this row's three cited symbols resolved on main, and they failed in two different ways** — measured across main's whole history, not just its head. `repository_load_disposition`, the function this row said performed the collapse, has NEVER existed as code on main: it appears only in this carrier and in the projection, and it names a declaration from the CLOSED attempt gunbc#8940, whose branch was retained in history and never landed. So the row cited a function that was fabricated on the day it was written. `RepositoryDecodeImageRefusal` and `ImageRefusal` were real — they landed with gunbc#8807 and gunbc#8840 and were deleted by gunbc#8965 on 2026-08-23 when the fused format was cut — so those two went stale one day later, by the ordinary route a citation rots when the thing it names is removed. The two halves matter separately because they have different remedies: a fabricated name is caught by resolving symbols before writing them, a deleted one only by a resolver that reruns. Either way a reader applying this entry's own recognition rule grepped for a match that was not there. That is §3's stale-citation class sitting inside the authority that names it, and it is recorded here rather than quietly deleted because a specimen whose symbols cannot be resolved is the failure this row exists to teach, one level up. **What landed is stronger than descending**, and the difference is the reusable part: the remedy vocabulary was hoisted into a module that names no format — `gunbc.scm.load_standing` `LoadStanding`, whose `standing_may_supersede_generation` derives the permission from the standing by one total function — and each format now classifies its own refusals into it (`gunbc.scm.commit_closure_json_v2` `closure_document_load_standing`). Descending inside one codec's enum would have closed the collapse and left the consumer still matching on a format's vocabulary; hoisting leaves the consumer no format arms to collapse, so the next format is a new classifier rather than a new way to reintroduce this defect. Second, independent specimen the same day, in the compiler itself: a census of the fourteen declared-type positions the grammar admits found five accepting a plain kernel value where a coproduct is declared — the judgment is present and total at the level it examines, and never descends. **The tell is a `_` or a bare binding in the arm that carries the payload**, and the test is not whether the match is complete but whether every cause it collapses shares one remedy; the fix is to descend so a new inner arm fails to compile HERE, rather than silently inheriting whichever remedy the outer arm happened to name.)",
authored: "**total at the level examined, blind one level down** (a judgment is exhaustive over the type it matches and says nothing about the distinction that actually decides the outcome, which lives inside one of its arms. **The pairing is the whole content: the match is exhaustive AND wrong**, and the exhaustiveness is what hides it — there is no missing arm to report, no warning, nothing incomplete, so neither a reviewer reading the match nor a wildcard-free lens can see it. Specimen with a mutation receipt (gunbc.scm, 2026-08-22), **repaired on main 2026-08-25 by gunbc#8973 and kept in the past tense because the mechanism recurs while this instance does not**: a publication fold matched one outer arm carrying a JSON codec's entire refusal enum. It was total over that codec's refusal type, and the enum's arms carried three different publication remedies — a reader limitation, an absent-object problem over a well-formed document, and malformed bytes. Only the third may supersede a head slot, so the collapsed form let an OLDER READER OVERWRITE A NEWER WRITER'S DOCUMENT: data loss produced by the reader's own limitation, from a match that compiled and looked complete. Executed both ways — descending, four witnesses passed; collapsed, the witness driving all three remedies through the single outer arm went red; a temporary decode arm made the fold non-exhaustive; restored control passed. **None of this row's three cited symbols resolved on main, and they failed in two different ways** — measured across main's whole history, not just its head. `repository_load_disposition`, the function this row said performed the collapse, has NEVER existed as code on main: it appears only in this carrier and in the projection, and it names a declaration from the CLOSED attempt gunbc#8940, whose branch was retained in history and never landed. So the row cited a function that was fabricated on the day it was written. `RepositoryDecodeImageRefusal` and `ImageRefusal` were real — they landed with gunbc#8807 and gunbc#8840 and were deleted by gunbc#8965 on 2026-08-23 when the fused format was cut — so those two went stale one day later, by the ordinary route a citation rots when the thing it names is removed. The two halves matter separately because they have different remedies: a fabricated name is caught by resolving symbols before writing them, a deleted one only by a resolver that reruns. Either way a reader applying this entry's own recognition rule grepped for a match that was not there. That is §3's stale-citation class sitting inside the authority that names it, and it is recorded here rather than quietly deleted because a specimen whose symbols cannot be resolved is the failure this row exists to teach, one level up. **What landed is stronger than descending**, and the difference is the reusable part: the remedy vocabulary was hoisted into a module that names no format — `gunbc.scm.load_standing` `LoadStanding`, and each format now classifies its own refusals into it (`gunbc.scm.commit_closure_json_v2` `closure_document_load_standing`). Descending inside one codec's enum would have closed the collapse and left the consumer still matching on a format's vocabulary; hoisting leaves the consumer no format arms to collapse, so the next format is a new classifier rather than a new way to reintroduce this defect. **THE HOISTING WAS NECESSARY AND NOT SUFFICIENT, and this sentence is the fourth citation in this row to have gone stale.** It read that the permission was derived `by one total function`, naming `standing_may_supersede_generation` — a `LoadStanding -> Bool` carrying neither the slot the observation was made on nor the generation examined, so a caller could apply it to a slot the evidence never described or to a generation that had moved since it was read. gunbc#9258 deleted it and replaced the destination with `gunbc.scm.supersession` `supersede_head_slot`, where evidence is minted FROM the slot by `observe_generation` — a caller cannot state which generation it examined, only examine one — and the swap refuses unless the slot still holds it. The deletion left this sentence naming a declaration that no longer resolves, one day after it was written, which is the same rot this row already records twice above and is corrected here for the same reason. Second, independent specimen the same day, in the compiler itself: a census of the fourteen declared-type positions the grammar admits found five accepting a plain kernel value where a coproduct is declared — the judgment is present and total at the level it examines, and never descends. **The tell is a `_` or a bare binding in the arm that carries the payload**, and the test is not whether the match is complete but whether every cause it collapses shares one remedy; the fix is to descend so a new inner arm fails to compile HERE, rather than silently inheriting whichever remedy the outer arm happened to name.)",
evidence: [],
}

Expand Down
63 changes: 63 additions & 0 deletions dag/gunbc/scm/repository_envelope.dag
Original file line number Diff line number Diff line change
Expand Up @@ -37,13 +37,20 @@ import extdeps.languages.json.emit {

import gunbc.scm.target_reference {
TargetReferenceRefusal,
TargetReferenceMemberReadRefused,
TargetReferenceUnexpectedMember,
TargetReferenceNotOneArm,
TargetReferenceUncontainedDigestInvalid,
TargetContainedAt,
TargetUncontained,
TargetReferenceRefused,
decode_target_reference,
}
import gunbc.scm.json_member {
MemberReadRefusal,
MemberReadSubjectNotObject,
MemberReadMissing,
MemberReadDuplicated,
MemberReadWrongShape,
MemberValue,
MemberLookupFailed,
Expand All @@ -69,6 +76,12 @@ import gunbc.scm.commit_closure_json_v2 {
position_reference,
unexpected_member_key,
resolve_reference,
closure_document_load_standing,
}
import gunbc.scm.load_standing {
LoadStanding,
LoadUnsupportedProtocol,
LoadDocumentMalformed,
}

// THE ENCODING IS NOT CANONICAL WITH RESPECT TO INSERTION HISTORY, and that is declared here rather
Expand Down Expand Up @@ -656,3 +669,53 @@ fn decode_repository_checkout(
}
}
}

// ------------------------------------------------------------------------------------------------
// Publication standing
// ------------------------------------------------------------------------------------------------

// THE SECOND FORMAT'S CLASSIFIER, AND IT WAS MISSING RATHER THAN UNNECESSARY.
//
// gunbc.scm.commit_closure_json_v2 and gunbc.scm.object_table_json each classify their own refusals
// into the format-agnostic vocabulary; this document format did not, so any consumer deciding what to
// do with a refused repository load had to reach into RepositoryDecodeRefusal and assign a standing
// itself -- one format's error enum answering a format-agnostic question, which is the placement
// defect that closed gunbc#8940 and the reason gunbc.scm.load_standing exists at all. Found by
// auditing every route into the supersession decision rather than by a failure, because a missing
// classifier fails silently: nothing refuses, the consumer simply invents the answer.
//
// EVERY ARM DESCENDS TO THE AUTHORITY THAT OWNS ITS CAUSE. The closure-document arm delegates to that
// format's own classifier; the member-read and target-reference arms descend per cause in place,
// because gunbc.scm.json_member and gunbc.scm.target_reference carry no classifier of their own. A
// bare binding in a payload-carrying arm is the tell DESIGN names for "total at the level examined,
// blind one level down", so a new cause in either population fails to compile HERE.
//
// THE IDENTITY RULE IS A PROTOCOL FACT, NOT DAMAGE, and this is the arm most likely to be got wrong.
// A document naming an identity rule this build does not implement is bytes that may be perfectly
// good and unreadable ONLY HERE -- the same shape as an unrecognized format tag. Calling it malformed
// would let an older reader destroy a newer writer's repository over a rule it simply lacks, which is
// the one outcome the standing vocabulary exists to prevent.
fn repository_envelope_load_standing(cause: RepositoryDecodeRefusal) -> LoadStanding {
match cause {
RepositoryFormatUnrecognized { found: _ } => LoadUnsupportedProtocol
RepositoryIdentityRuleUnrecognized { found: _ } => LoadUnsupportedProtocol
RepositoryDecodeClosureDocRefusal { cause: c } => closure_document_load_standing(cause: c)
RepositoryMemberReadRefused { cause: c } =>
match c {
MemberReadSubjectNotObject => LoadDocumentMalformed
MemberReadMissing { key: _ } => LoadDocumentMalformed
MemberReadDuplicated { key: _ } => LoadDocumentMalformed
MemberReadWrongShape { key: _ } => LoadDocumentMalformed
}
RepositoryTargetReferenceRefused { cause: c } =>
match c {
TargetReferenceMemberReadRefused { cause: _ } => LoadDocumentMalformed
TargetReferenceUnexpectedMember { key: _ } => LoadDocumentMalformed
TargetReferenceNotOneArm { found: _ } => LoadDocumentMalformed
TargetReferenceUncontainedDigestInvalid { found: _ } => LoadDocumentMalformed
}
RepositoryCommitRootReferenceUnresolved { reference: _ } => LoadDocumentMalformed
RepositoryCheckoutReferenceUnresolved { reference: _ } => LoadDocumentMalformed
RepositoryUnexpectedMember { context: _, key: _ } => LoadDocumentMalformed
}
}
32 changes: 21 additions & 11 deletions dag/test/claim/coproduct_payload_soundness_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -160,20 +160,30 @@ test fn cpp_alias_mediated_payload_must_also_refuse() -> Bool {
// FIX and are deliberately not cited here as a population -- nobody has sized this class, and the
// finders asked that no count be inherited from two instances. What makes the class worth a wall
// rather than two repairs is where the mis-routed value LANDS: per `gunbc.scm.load_standing`
// `standing_may_supersede_generation`, `LoadDocumentMalformed` is the only standing permitting
// supersession of a newer generation, so a silently-admitted wrong cause is a route into a
// data-loss class.
// `LoadStanding`, `LoadDocumentMalformed` is the only standing permitting supersession of a newer
// generation, so a silently-admitted wrong cause is a route into a data-loss class.
//
// WHAT THIS ARM DOES NOT DO, AND THE BOUNDARY IS THE POINT. IT CLOSES ONE ROUTE INTO AN
// UNDER-DEFENDED DESTINATION. IT DOES NOT CLOSE THE HAZARD. The destructive operation is authorized
// by a value too lossy to carry the proof it needs: `standing_may_supersede_generation` is
// `LoadStanding -> Bool`, and a Bool carries none of the exact generation observed, the content
// identity examined, the schema identity under which malformedness was established, or a receipt
// joining the refusal to this policy arm. This arm stops ONE PRODUCER from manufacturing a false
// `LoadDocumentMalformed`; it does not make the destination REQUIRE proof, and another producer --
// or an unknown one -- reaches the same arm unchanged. Making supersession proof-bearing and
// generation-bound, so that actuation compares and swaps against the exact generation the evidence
// was gathered from, is a SEPARATE CONTRACT and is deliberately not attempted here.
// by a value too lossy to carry the proof it needs: the permission was `LoadStanding -> Bool`, and a
// Bool carries none of the exact generation observed, the content identity examined, the schema
// identity under which malformedness was established, or a receipt joining the refusal to this
// policy arm. This arm stops ONE PRODUCER from manufacturing a false `LoadDocumentMalformed`; it
// does not make the destination REQUIRE proof, and another producer -- or an unknown one -- reaches
// the same arm unchanged.
//
// THAT SEPARATE CONTRACT LANDED AS gunbc#9258, and this paragraph is repointed rather than deleted
// because the BOUNDARY it states is still exactly this file's. `gunbc.scm.supersession`
// `supersede_head_slot` makes the destination proof-bearing and generation-bound: evidence is minted
// from the slot by `observe_generation`, so a caller cannot state which generation it examined, and
// the swap refuses unless the slot still holds it. A false `LoadDocumentMalformed` therefore no
// longer authorizes replacing a generation nobody read. It still authorizes replacing the generation
// the evidence DID name, which is why closing the producer route measured here remains load-bearing
// and is not subsumed by the destination's repair.
//
// The two sentences above previously named `standing_may_supersede_generation`, which #9258 deleted.
// They are corrected here rather than left standing: a citation naming a declaration that no longer
// resolves is the class this file's neighbouring DESIGN row exists to teach.
//
// AND WHAT DOES NOT FOLLOW, recorded because it is the inference this file is most likely to invite.
// DESIGN already records a SECOND, independent mechanism reaching that same destination
Expand Down
46 changes: 46 additions & 0 deletions dag/test/claim/scm_load_standing_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,14 @@ import gunbc.scm.object_table_json {
ObjectTableObjectCollision,
object_table_load_standing,
}
import gunbc.scm.repository_envelope {
RepositoryFormatUnrecognized,
RepositoryIdentityRuleUnrecognized,
RepositoryUnexpectedMember,
RepositoryEnvelopeMembers,
RepositoryCommitRootReferenceUnresolved,
repository_envelope_load_standing,
}
import gunbc.scm.commit_closure_json_v2 {
ClosureDocRefusal, ClosureDocFormatUnrecognized, ClosureDocObjectTableRefused,
ClosureDocMemberReadRefused,
Expand Down Expand Up @@ -210,3 +218,41 @@ test fn an_honest_collision_is_its_own_standing_and_never_supersedes() -> Bool {
&& !ls_permits(standing: collision)
&& ls_permits(standing: malformed)
}

// THE THIRD FORMAT NOW CLASSIFIES ITS OWN REFUSALS, and until this landed it did not. gunbc#9258
// made the destination proof-bearing; auditing every PRODUCER reaching it found the repository
// envelope had no classifier at all, so a consumer holding a RepositoryDecodeRefusal had to reach
// into that format's error enum and assign a standing itself -- one format's vocabulary answering a
// format-agnostic question, which is the placement defect that closed gunbc#8940. A missing
// classifier fails silently: nothing refuses, the consumer simply invents the answer.
//
// THE IDENTITY-RULE ARM IS THE ONE WORTH PINNING. The envelope versions its node-identity rule
// separately from its schema, so a document may parse perfectly under a derivation rule this build
// does not implement. Those bytes are unreadable ONLY HERE, exactly like an unrecognized format tag,
// and classifying them as damage would let an older reader destroy a newer writer's repository over
// a rule it simply lacks. The malformed pair beside it is what makes the assertion discriminating: a
// classifier answering UnsupportedProtocol for everything would satisfy the first two clauses alone.
//
// THE LAST TWO CLAUSES CARRY IT THROUGH TO THE DESTINATION rather than stopping at the standing,
// because the standing is only interesting for what it authorizes: the protocol gap must not
// supersede a generation and the malformed document must.
test fn an_unimplemented_identity_rule_is_a_protocol_gap_not_damage() -> Bool {
let rule = repository_envelope_load_standing(
cause: RepositoryIdentityRuleUnrecognized { found: "blake3-structural-v2" }
)
let format = repository_envelope_load_standing(
cause: RepositoryFormatUnrecognized { found: "gunbc-scm-repository-v9" }
)
let member = repository_envelope_load_standing(
cause: RepositoryUnexpectedMember { context: RepositoryEnvelopeMembers, key: "provenance" }
)
let unresolved = repository_envelope_load_standing(
cause: RepositoryCommitRootReferenceUnresolved { reference: "11" }
)
standing_eq(a: rule, b: LoadUnsupportedProtocol)
&& standing_eq(a: format, b: LoadUnsupportedProtocol)
&& standing_eq(a: member, b: LoadDocumentMalformed)
&& standing_eq(a: unresolved, b: LoadDocumentMalformed)
&& !ls_permits(standing: rule)
&& ls_permits(standing: member)
}
Loading