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
49 changes: 30 additions & 19 deletions dag/gunbc/scm/commit_closure_json_v2.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,16 @@ import gunbc.scm.commit_closure {
unresolved_identities,
closure_is_complete,
}
import gunbc.scm.object_table_json {
ObjectTableDecodeRefusal,
ObjectTableUnknownKindTag,
ObjectTableUnknownConnectiveTag,
ObjectTableUnknownBehaviorTag,
ObjectTableUnknownLabelTag,
ObjectTableEdgeTargetUnresolved,
ObjectTableObjectCollision,
object_table_load_standing,
}
import gunbc.scm.load_standing {
LoadStanding,
LoadComplete,
Expand Down Expand Up @@ -147,15 +157,10 @@ import gunbc.scm.object_store {
type ClosureDocRefusal
= ClosureDocMemberReadRefused { cause: MemberReadRefusal }
| ClosureDocFormatUnrecognized { found: String }
| ClosureDocUnknownKindTag { found: String }
| ClosureDocUnknownConnectiveTag { found: String }
| ClosureDocUnknownBehaviorTag { found: String }
| ClosureDocUnknownLabelTag { found: String }
| ClosureDocEdgeTargetUnresolved { reference: String }
| ClosureDocRootPositionUnresolved { reference: String }
| ClosureDocObjectCollision { identity: ObjectId }
| ClosureDocUnexpectedMember { context: ClosureDocMemberContext, key: String }
| ClosureDocTargetReferenceRefused { cause: TargetReferenceRefusal }
| ClosureDocObjectTableRefused { cause: ObjectTableDecodeRefusal }

// THE ENCODE DOMAIN IS ITS OWN TYPE, and this split is a correctness fix rather than tidiness.
//
Expand Down Expand Up @@ -349,7 +354,7 @@ fn position_of(positions: EncodePositions, identity: ObjectId) -> String? {
// parents, so by the time an edge is encoded its target already holds a position. Answering some
// plausible reference here would emit an image that decodes to a DIFFERENT program, which is exactly
// the fabricated plausible output DESIGN section 5 forbids. The empty string is not a sentinel the
// decoder tolerates -- ClosureDocEdgeTargetUnresolved refuses it -- so an ordering regression surfaces as
// decoder tolerates -- ObjectTableEdgeTargetUnresolved refuses it -- so an ordering regression surfaces as
// a typed refusal at load rather than as a silently wrong store.
// A TARGET IS ONE OF TWO ARMS, AND WHICH ONE IS A FACT ABOUT THIS DOCUMENT, NOT ABOUT THE WORLD.
//
Expand Down Expand Up @@ -551,7 +556,7 @@ fn decode_connective(kind_value: JsonValue, tag: String) -> ConnectiveDecode {
else if tag == "arrow" { ConnectiveDecoded { connective: Arrow } }
else if tag == "cardinality" { ConnectiveDecoded { connective: Cardinality } }
else if tag == "instantiation" { ConnectiveDecoded { connective: Instantiation } }
else { ConnectiveDecodeFailed { cause: ClosureDocUnknownConnectiveTag { found: tag } } }
else { ConnectiveDecodeFailed { cause: ClosureDocObjectTableRefused { cause: ObjectTableUnknownConnectiveTag { found: tag } } } }
}

type BehaviorDecode
Expand All @@ -565,7 +570,7 @@ fn decode_behavior(tag: String) -> BehaviorDecode {
else if tag == "loop" { BehaviorDecoded { behavior: Loop } }
else if tag == "bind" { BehaviorDecoded { behavior: Bind } }
else if tag == "match" { BehaviorDecoded { behavior: Match } }
else { BehaviorDecodeFailed { cause: ClosureDocUnknownBehaviorTag { found: tag } } }
else { BehaviorDecodeFailed { cause: ClosureDocObjectTableRefused { cause: ObjectTableUnknownBehaviorTag { found: tag } } } }
}

type KindDecode
Expand Down Expand Up @@ -624,7 +629,7 @@ fn decode_kind(kind_value: JsonValue) -> KindDecode {
_ => KindDecodeFailed { cause: ClosureDocMemberReadRefused { cause: MemberReadWrongShape { key: "behavior" } } }
}
} else {
KindDecodeFailed { cause: ClosureDocUnknownKindTag { found: tag } }
KindDecodeFailed { cause: ClosureDocObjectTableRefused { cause: ObjectTableUnknownKindTag { found: tag } } }
}
_ => KindDecodeFailed { cause: ClosureDocMemberReadRefused { cause: MemberReadWrongShape { key: "kind" } } }
}
Expand Down Expand Up @@ -685,7 +690,7 @@ fn decode_label(edge_value: JsonValue) -> LabelDecode {
} else if tag == "positional" {
decode_positional_label(edge_value: edge_value)
} else {
LabelDecodeFailed { cause: ClosureDocUnknownLabelTag { found: tag } }
LabelDecodeFailed { cause: ClosureDocObjectTableRefused { cause: ObjectTableUnknownLabelTag { found: tag } } }
}
_ => LabelDecodeFailed { cause: ClosureDocMemberReadRefused { cause: MemberReadWrongShape { key: "label" } } }
}
Expand Down Expand Up @@ -771,7 +776,7 @@ fn decode_edge_step(positions: DecodePositions, acc: EdgeAcc, edge_value: JsonVa
Absent =>
EdgeAcc {
edges: acc.edges,
refusal: Present { value: ClosureDocEdgeTargetUnresolved { reference: reference } },
refusal: Present { value: ClosureDocObjectTableRefused { cause: ObjectTableEdgeTargetUnresolved { reference: reference } } },
}
}
}
Expand Down Expand Up @@ -850,7 +855,7 @@ fn decode_object_members(acc: DecodeAcc, object_value: JsonValue) -> DecodeAcc {
store: acc.store,
positions: acc.positions,
next: acc.next,
refusal: Present { value: ClosureDocObjectCollision { identity: i } },
refusal: Present { value: ClosureDocObjectTableRefused { cause: ObjectTableObjectCollision { identity: i } } },
}
Stored { store: next_store, identity: identity } =>
DecodeAcc {
Expand Down Expand Up @@ -988,24 +993,30 @@ fn decode_closure_document_body(v: JsonValue) -> ClosureDocLoadOutcome {
// standing that permits superseding a newer generation, so an inherited arm sits one step from a
// reader overwriting a writer's valid document. Descending makes the next mode fail to compile
// here, where whoever adds it can see what it would cost.
// THE OBJECT-TABLE ARM BINDS ITS PAYLOAD AND PASSES IT ON; IT DOES NOT DISCARD IT. A bare binding in
// the arm carrying the payload is the tell DESIGN names for "total at the level examined, blind one
// level down", so it is worth saying which this is: the cause is handed to the authority that owns it
// and descends per cause, rather than collapsed into one standing here. Reading it as the defect
// would invert the fix -- classifying the six object-table causes at THIS grain is exactly what would
// hand an identity collision the one standing permitting supersession.
//
// The two remaining nested matches below are descent-in-place over populations whose owners carry no
// classifier (gunbc.scm.json_member, gunbc.scm.target_reference). They are not inconsistent with the
// delegating arm above: the object-table module owns a classifier and those two do not, so each cause
// is classified by whoever owns it.
fn closure_document_load_standing(cause: ClosureDocRefusal) -> LoadStanding {
match cause {
ClosureDocFormatUnrecognized { found: _ } => LoadUnsupportedProtocol
ClosureDocObjectCollision { identity: _ } => LoadIdentityCollision
ClosureDocMemberReadRefused { cause: c } =>
match c {
MemberReadSubjectNotObject => LoadDocumentMalformed
MemberReadMissing { key: _ } => LoadDocumentMalformed
MemberReadDuplicated { key: _ } => LoadDocumentMalformed
MemberReadWrongShape { key: _ } => LoadDocumentMalformed
}
ClosureDocUnknownKindTag { found: _ } => LoadDocumentMalformed
ClosureDocUnknownConnectiveTag { found: _ } => LoadDocumentMalformed
ClosureDocUnknownBehaviorTag { found: _ } => LoadDocumentMalformed
ClosureDocUnknownLabelTag { found: _ } => LoadDocumentMalformed
ClosureDocUnexpectedMember { context: _, key: _ } => LoadDocumentMalformed
ClosureDocEdgeTargetUnresolved { reference: _ } => LoadDocumentMalformed
ClosureDocRootPositionUnresolved { reference: _ } => LoadDocumentMalformed
ClosureDocObjectTableRefused { cause: c } => object_table_load_standing(cause: c)
ClosureDocTargetReferenceRefused { cause: c } =>
match c {
TargetReferenceMemberReadRefused { cause: _ } => LoadDocumentMalformed
Expand Down
18 changes: 18 additions & 0 deletions dag/gunbc/scm/json_member.dag
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,24 @@ module gunbc.scm.json_member
// authority substitution: one carrier's vocabulary borrowed to answer for another's, with nothing
// false in either half and the arrow between them invented.
//
// THAT CLASS WAS CLOSED INCOMPLETELY, and this paragraph is the correction rather than a rewrite of
// the one above. Extracting this module (#9048) rerouted most of those reads but left TWO of the four
// it names -- `root` and `message`, in repository_envelope's decode_commit_members -- still wrapping a
// MemberReadRefusal in RepositoryDecodeClosureDocRefusal, whose declared field is ClosureDocRefusal.
// They were repaired later, in the object-table authority cut.
//
// The header stood for a day claiming a coverage it did not have, which is the more serious half: a
// carrier asserting a class is closed is read as evidence, and a reader checking this module would
// have found the claim and stopped. The two sites survived review because the CORRECT arm sits three
// and seven lines away in the same match, shape-identical to the wrong one.
//
// They also compiled, and that is a separate defect this module cannot fix: a coproduct value of the
// wrong coproduct type is accepted 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. That is the ordinary compiler floor ("values inhabit declared
// types"), it is handed to the compiler lane with the fixture, and until it is walled, nothing
// mechanically prevents this class from recurring here.
//
// The refusal population here is exactly what reading a named member can fail with, and nothing
// wider. A domain wraps it in one arm rather than restating its members, so a new member-read
// failure mode is added once here and every domain's classifier refuses to compile until it says
Expand Down
104 changes: 104 additions & 0 deletions dag/gunbc/scm/object_table_json.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
module gunbc.scm.object_table_json

// DECODING THE OBJECT TABLE IS ONE OPERATION WITH ONE FAILURE POPULATION, and this module owns both.
// It was previously homed inside gunbc.scm.commit_closure_json_v2 with its failures typed as THAT
// module's ClosureDocRefusal, so six object-population causes sat in a coproduct that also answers
// for envelope format and closure-root facts. A consumer matching that type had to handle causes
// from three different owners, and no reader could tell from the type which owner produced which.
//
// THE MEASURED COST WAS NOT STYLISTIC, and it is the reason this cut is a correctness fix rather
// than tidiness. closure_document_load_standing maps ObjectTableObjectCollision to
// LoadIdentityCollision and the five tag/reference causes to LoadDocumentMalformed. Per
// gunbc.scm.load_standing, LoadDocumentMalformed is THE ONLY standing that
// standing_may_supersede_generation answers true for. So any consumer that classified the six
// together -- at the grain of one wrapping arm rather than per cause -- would hand an identity
// collision the one standing permitted to overwrite a newer generation. Both colliding records are
// legitimate and the coincidence is honest, so that is a valid generation destroyed by a reader's
// own collapse: the DESIGN gunbc.scm specimen, where an older reader supersedes a newer writer's
// document through a single outer arm that looked total.
//
// THE FORMAT VOCABULARY STAYS HERE, NOT IN gunbc.scm.object_store. These causes name JSON tags and
// document-local references, and object_store is format-agnostic -- it imports only v2.std.node and
// std.types and mentions JSON nowhere. Moving a `found: String` JSON tag into it would be the layer
// inversion gunbc.scm.json_member's header already names. The object TABLE is a JSON-document
// concept; the object STORE is not.
//
// THIS MODULE OWNS ITS OWN CLASSIFIER, which is a deliberate departure from the sibling extraction.
// gunbc.scm.json_member carries no classifier: the closure classifier descends into MemberReadRefusal
// in place, as it also does into TargetReferenceRefusal. Descent would be correct here too. It is not
// what this module does, because descent-in-place makes the closure module grow a new inner arm every
// time THIS module gains a cause, so it would pay maintenance for a population it does not own.
// Delegation is the only form where adding an object-table cause is one edit in one module.
//
// WHAT THE DELEGATION DOES AND DOES NOT MAKE UNREPRESENTABLE, stated precisely because an earlier
// revision of this paragraph overclaimed it and a reviewer was right to catch that (review 55811).
//
// UNREPRESENTABLE: naming an INDIVIDUAL object-table cause in a match over ClosureDocRefusal. A
// consumer cannot write `ObjectTableObjectCollision => LoadDocumentMalformed`, because the closure
// type's arms do not include it. That is the specific misclassification that was writable before this
// cut and is not writable after it, and it is the dangerous one: it targets exactly one cause, needs
// no wildcard, and reads as total.
//
// STILL WRITABLE: collapsing the whole population behind the wrapper binding --
// `ClosureDocObjectTableRefused { cause: _ } => LoadDocumentMalformed`. That would give a collision
// the supersession-permitting standing just as surely. This cut does NOT wall it, and the rung for
// that class is MECHANICALLY PREVENTABLE, not structural: what changed is that the collapse now
// requires a bare binding over a foreign authority's population, which is the tell DESIGN already
// names, rather than an innocuous-looking per-cause arm.
//
// WHY NOT WALL IT HERE: the proposed remedy -- have decode_object_table expose its own outcome
// boundary before translation -- rests on a premise that is false as measured. 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 --
// the same defect this module exists to remove, pointing the other way.
//
// NEXT-RUNG TRIGGER: a decode_object_table whose member-read and unexpected-member causes are
// themselves owned elsewhere, leaving a residue this module can own outright. That is a separate cut
// with its own census, not a line in this one.

import std.types { String }
import gunbc.scm.object_store { ObjectId }
import gunbc.scm.load_standing {
LoadStanding,
LoadDocumentMalformed,
LoadIdentityCollision,
}

// SIX CAUSES, TWO REMEDIES, AND THE SPLIT BETWEEN THEM IS THE WHOLE POINT OF THE TYPE.
//
// Five of these say the document does not conform to a schema this build claims to understand: a tag
// naming a kind, connective, behavior or label that is not in the closed vocabulary, or an edge
// target naming a position the document does not carry. Those are malformed bytes to a reader that
// should have understood them.
//
// ObjectTableObjectCollision is NOT that, and conflating it with the five is the error this type
// exists to prevent. Two distinct records claiming one structural locator is an honest hash
// coincidence between two legitimate objects, not damage to either. It is a limitation of the
// locator's representation, and the remedy is to widen the locator -- never to discard a generation.
type ObjectTableDecodeRefusal
= ObjectTableUnknownKindTag { found: String }
| ObjectTableUnknownConnectiveTag { found: String }
| ObjectTableUnknownBehaviorTag { found: String }
| ObjectTableUnknownLabelTag { found: String }
| ObjectTableEdgeTargetUnresolved { reference: String }
| ObjectTableObjectCollision { identity: ObjectId }

// THE AUTHORITY THAT OWNS THE CAUSES OWNS THE STANDING DECISION, per DESIGN section 3: the dispatch
// selecting a realization is itself realization, so each format classifies ITS OWN refusals into the
// shared vocabulary and the consumer sees only the standing. gunbc.scm.load_standing's header states
// the same rule from the other side -- a new format is a new classifier beside its own refusals.
//
// This match is exhaustive over the six and assigns per cause, never per group. The collision arm is
// the load-bearing one: it must not reach LoadDocumentMalformed, because that is the only standing
// permitting supersession.
fn object_table_load_standing(cause: ObjectTableDecodeRefusal) -> LoadStanding {
match cause {
ObjectTableObjectCollision { identity: _ } => LoadIdentityCollision
ObjectTableUnknownKindTag { found: _ } => LoadDocumentMalformed
ObjectTableUnknownConnectiveTag { found: _ } => LoadDocumentMalformed
ObjectTableUnknownBehaviorTag { found: _ } => LoadDocumentMalformed
ObjectTableUnknownLabelTag { found: _ } => LoadDocumentMalformed
ObjectTableEdgeTargetUnresolved { reference: _ } => LoadDocumentMalformed
}
}
4 changes: 2 additions & 2 deletions dag/gunbc/scm/repository_envelope.dag
Original file line number Diff line number Diff line change
Expand Up @@ -507,15 +507,15 @@ fn decode_commit_members(positions: DecodePositions, acc: CommitDecodeAcc, value
Absent =>
match read_member(v: value, key: "root") {
MemberFailed { cause: c } =>
CommitDecodeAcc { commits: acc.commits, refusal: Present { value: RepositoryDecodeClosureDocRefusal { cause: c } } }
CommitDecodeAcc { commits: acc.commits, refusal: Present { value: RepositoryMemberReadRefused { cause: c } } }
MemberObject { value: root_value } =>
match decode_commit_root(positions: positions, root_value: root_value) {
CommitRootRefused { cause: c } =>
CommitDecodeAcc { commits: acc.commits, refusal: Present { value: c } }
CommitRootDecoded { root: root } =>
match read_string_member(v: value, key: "message") {
MemberFailed { cause: c } =>
CommitDecodeAcc { commits: acc.commits, refusal: Present { value: RepositoryDecodeClosureDocRefusal { cause: c } } }
CommitDecodeAcc { commits: acc.commits, refusal: Present { value: RepositoryMemberReadRefused { cause: c } } }
MemberString { value: message } =>
CommitDecodeAcc {
commits: concat([RepositoryCommit { root: root, message: message }], acc.commits),
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/scm/target_reference.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ module gunbc.scm.target_reference
//
// The split is the repair. Three operations decode this same syntax: an edge inside an object
// record, a closure document's root, and a repository commit's root. Previously one shared decoder
// resolved the position for all three and reported failure as ClosureDocEdgeTargetUnresolved, so a
// resolved the position for all three and reported failure as ObjectTableEdgeTargetUnresolved (gunbc.scm.object_table_json), so a
// closure root naming a position nobody defined was reported as an EDGE target unresolved -- an edge
// that does not exist, inside an object that was never named. The repository then compensated with an
// adapter that translated that edge cause back into a commit-root cause, recovering by context what
Expand Down
Loading
Loading