Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
0947e23
The logical half of the closure recut: an incomplete closure can name…
Aug 23, 2026
7b5270c
Rename the fused format to what it is: commit_closure_json_v1, with n…
Aug 23, 2026
4b418e0
Merge remote-tracking branch 'origin/main' into session/closure-recut
Aug 23, 2026
8751801
Two-arm references: positions name what is here, content addresses na…
Aug 23, 2026
5dc74a6
Strip the temporary verification drivers
Aug 23, 2026
19d021b
A target carrying both arms was silently answering with one of them (…
Aug 23, 2026
d735c8b
Publication standings, in a vocabulary no format owns -- and the arm …
Aug 23, 2026
3892cf1
Hoist two comment blocks to module-item grain: DESIGN 4c refuses a bo…
Aug 23, 2026
8dcac7f
Merge branch 'session/closure-recut' into session/load-standings
Aug 23, 2026
1efe07e
Two version names for one realization, and an admission wall two revi…
Aug 23, 2026
1e7a6cc
Merge branch 'session/closure-recut' into session/load-standings
Aug 23, 2026
4d26a39
Fix the stacked-rename dangling import: the witness pointed at commit…
Aug 23, 2026
c856db5
Repoint the eight image.dag citations at the module that exists
Aug 23, 2026
f8b4337
Merge session/closure-recut: the image.dag citation repair
Aug 23, 2026
ade8ad4
Select the target arm on presence, so a broken `at` is refused agains…
Aug 23, 2026
6aad5a2
Merge session/closure-recut: presence-based target arm selection
Aug 23, 2026
51a085a
Fix both quadratic folds in uncontained_targets, and make the order they
Aug 23, 2026
9f7c13a
Fix both quadratic folds in uncontained_targets, and make the order they
Aug 23, 2026
065dfbc
Merge session/closure-recut: cost-shape fix and the order claim that …
Aug 23, 2026
e7e04b5
Merge main: fleet witness repairs and stage0 mirror
Aug 23, 2026
5d2e6db
Merge session/closure-recut (incl. main)
Aug 23, 2026
f0845da
Merge main (#9012): live_deploy cost split
Aug 23, 2026
5d81f8c
Merge session/closure-recut
Aug 23, 2026
6039778
SCM: close an authority-escalation path and a bearer-token admission …
gunbai-bot[bot] Aug 23, 2026
8c707a7
Merge main (00ad29e) into session/load-standings
Aug 23, 2026
345defa
Merge remote-tracking branch 'origin/main' into HEAD
Aug 24, 2026
af0914e
Merge remote-tracking branch 'origin/main' into HEAD
Aug 24, 2026
b9e6c42
Merge remote-tracking branch 'origin/main' into HEAD
Aug 24, 2026
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
94 changes: 69 additions & 25 deletions dag/gunbc/scm/commit_closure.dag
Original file line number Diff line number Diff line change
Expand Up @@ -115,43 +115,87 @@ import gunbc.scm.object_store {
// admit closure A -> token T
// encode closure B with T -> ACCEPTED
//
// The encoder checks that a token is PRESENT, never that it is ABOUT the closure being encoded. That
// is authority substitution in the exact form this repository has already named: a true admission
// about one subject answering for another because no relation binds them. The existing mutation
// (delete the check) proves the check is READ; it proves nothing about what the token is about.
//
// So the honest rung is MITIGATABLE, not structural: an accidental partial write is caught, a
// mis-attributed one is not. This paragraph exists because the reported rung must equal the rung
// executed evidence establishes, and review 54944 read the wall as "structural" -- which is the
// inflation section 4b calls worse than sitting low, since an inflated class never ranks for
// climbing.
//
// NEXT-RUNG TRIGGER, and it is a shape change rather than a check: the admitted carrier binds the
// closure and its unresolved population together --
//
// AdmittedPartialCommitClosure sole_constructor { closure, unresolved, reason }
//
// minted by a function that DERIVES `unresolved` from the closure it is given, with the encoder
// taking the admitted carrier instead of a closure plus a free-floating token. Then "a token for A
// used on B" has no spelling at all. Discriminator the repair owes: an admission produced for A,
// attempted against B, refuses or cannot be constructed.
type PartialClosureAdmission sole_constructor {
// THE ADMISSION IS BOUND TO ITS SUBJECT, and that binding is the whole guarantee.
//
// THE DEFECT THIS REPLACES. The predecessor was PartialClosureAdmission { reason } -- a token minted
// by a public function, carrying no subject. The encoder took a closure PLUS an optional token and
// checked only that a token was PRESENT, never that it was ABOUT the closure being encoded:
//
// admit closure A -> token T
// encode closure B with T -> ACCEPTED
//
// That is authority substitution in its exact form: a true admission about one subject answering for
// another because no relation binds them. sole_constructor did not help, because `.dag` has no
// module privacy -- it blocks the record literal while the public mint stays freely callable. And
// the mutation that existed (delete the check) could never have caught it: deleting a check proves
// the check is READ, which a bearer token satisfies perfectly.
//
// WHY THE REPAIR IS A SHAPE, NOT A CHECK. The carrier holds the closure it admits, so the encoder
// takes ONE argument and there is no second closure to disagree with it. "A token for A used on B"
// is not refused at runtime -- it has no spelling. The mismatch is unconstructible rather than
// caught, which is DESIGN section 4b's top rung and the reason no validator appears beside this.
//
// `unresolved` is DERIVED here from the closure rather than supplied, so it cannot disagree with the
// objects it describes; a caller-supplied population would reintroduce the same substitution one
// field down. The mint refuses a COMPLETE closure, because admitting a partial write for something
// with nothing missing is a category error and would make the carrier's own name a lie.
//
// REMAINING RUNG, stated so it is not read as more than it is: `unresolved` is a List, so an EMPTY
// admitted population is representable in the type even though this mint cannot produce one. The
// corpus has no NonEmptyList, and minting one solely for this field would grow net concepts to buy a
// guarantee the mint's refusal already provides -- so the emptiness exclusion sits at mitigatable
// while the SUBJECT BINDING, which is what the defect was about, is structural. Next-rung trigger: a
// NonEmptyList authority earning its place from more than one consumer.
type AdmittedPartialCommitClosure sole_constructor {
closure: CommitClosure
unresolved: List<ObjectId>
reason: PartialClosureReason
}

// THE REFUSAL IS AN ARM OF THE OUTCOME, not a one-member coproduct beside it. There is exactly one
// way to be refused here -- the closure has nothing missing -- and wrapping that in its own type
// would either read as a type alias or invite a second arm invented to justify the wrapper. If a
// second genuine refusal appears, it joins this coproduct and every match fails to compile HERE,
// which is the behaviour the nesting was for.
type PartialClosureAdmissionOutcome
= PartialClosureAdmitted { admitted: AdmittedPartialCommitClosure }
| ClosureCompleteSoNothingToAdmit

// WHY A CLOSED VOCABULARY RATHER THAN A STRING. A reason nobody can enumerate is a reason nobody can
// refuse, and the two admitted causes have genuinely different owners: one is a transfer decision,
// the other is a graft that object_store deliberately supports.
type PartialClosureReason
= ClosureTrimmedForTransfer
| ClosureGraftedWithoutChildren

fn admit_partial_closure(reason: PartialClosureReason) -> PartialClosureAdmission {
PartialClosureAdmission { reason: reason }
fn admit_partial_commit_closure(
closure: CommitClosure,
reason: PartialClosureReason
) -> PartialClosureAdmissionOutcome {
let unresolved = unresolved_identities(closure: closure)
if list_length(items: unresolved) == 0 {
ClosureCompleteSoNothingToAdmit
} else {
PartialClosureAdmitted {
admitted: AdmittedPartialCommitClosure {
closure: closure,
unresolved: unresolved,
reason: reason,
}
}
}
}

fn admitted_reason(admitted: AdmittedPartialCommitClosure) -> PartialClosureReason {
admitted.reason
}

fn admitted_closure(admitted: AdmittedPartialCommitClosure) -> CommitClosure {
admitted.closure
}

fn admission_reason(admission: PartialClosureAdmission) -> PartialClosureReason {
admission.reason
fn admitted_unresolved(admitted: AdmittedPartialCommitClosure) -> List<ObjectId> {
admitted.unresolved
}

// A closure is the store plus the root the commit names. Nothing about how it is written down.
Expand Down
160 changes: 131 additions & 29 deletions dag/gunbc/scm/commit_closure_json_v2.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,17 @@ import std.types { Bool, Int, List, String, list_length }
import std.content_hash { fnv1a64_structural_hex_digest }
import gunbc.scm.commit_closure {
CommitClosure,
PartialClosureAdmission,
AdmittedPartialCommitClosure,
unresolved_identities,
closure_is_complete,
}
import gunbc.scm.load_standing {
LoadStanding,
LoadComplete,
LoadPartial,
LoadUnsupportedProtocol,
LoadDocumentMalformed,
LoadIdentityCollision,
}
import extdeps.languages.json.emit {
JsonValue,
Expand Down Expand Up @@ -119,7 +128,22 @@ type ClosureDocRefusal
| ClosureDocUnexpectedMember { context: ClosureDocMemberContext, key: String }
| ClosureDocTargetNotOneArm { found: Int }
| ClosureDocUncontainedDigestInvalid { found: String }
| ClosureDocIncompleteWithoutAdmission { identity: String }

// THE ENCODE DOMAIN IS ITS OWN TYPE, and this split is a correctness fix rather than tidiness.
//
// ClosureDocIncompleteWithoutAdmission is produced by encode_complete_closure_document and by nothing
// else -- no decode path can reach it. It nevertheless sat in ClosureDocRefusal, which the LOAD
// classifier matches exhaustively, so closure_document_load_standing was forced to assign a standing
// to a state the loader cannot produce. It answered LoadDocumentMalformed, and malformed is the ONE
// standing standing_may_supersede_generation permits to overwrite a newer document. An encode-only
// state therefore had a route to "may supersede".
//
// That is a closed match over a dishonest domain: exhaustiveness is satisfied, the compiler is
// content, and the arm is answering for something that cannot occur. Splitting the type does not
// hide the arm -- it makes the question unaskable, because the classifier's parameter can no longer
// name this cause. DESIGN section 4b's top rung: not validated, not proven, unrepresentable.
type ClosureDocEncodeRefusal
= ClosureDocIncompleteWithoutAdmission { identity: String }

// THE FORMAT TAG MEANS "I UNDERSTAND THIS EXACT SCHEMA", not "I understand some subset of whatever
// this writer may have meant". So once the tag matches, every JSON object in the document has a
Expand Down Expand Up @@ -428,7 +452,7 @@ fn encoded_root_reference(acc: EncodeAcc, root: ObjectId) -> JsonValue {

type ClosureDocEncodeOutcome
= ClosureDocEncoded { value: JsonValue }
| ClosureDocEncodeRefused { cause: ClosureDocRefusal }
| ClosureDocEncodeRefused { cause: ClosureDocEncodeRefusal }

// AN INCOMPLETE CLOSURE IS NOW REPRESENTABLE, SO THE QUESTION CHANGES FROM "CAN IT BE WRITTEN" TO
// "WAS IT DECIDED".
Expand All @@ -440,44 +464,55 @@ type ClosureDocEncodeOutcome
// closure may be PUBLISHED is a policy question that does not belong in a codec (DESIGN section 3).
//
// What must NOT happen is the refusal quietly becoming optional -- a caller who forgets, and a
// partial document written by accident. So the encoder does not accept a closure plus a caller's
// assurance: it requires a PartialClosureAdmission, which is `sole_constructor` in gunbc.scm.
// commit_closure and therefore cannot be fabricated here. An undeclared partial closure has no token
// to offer and is refused, typed and naming the first identity that would have gone uncontained.
//
// RUNG, STATED HONESTLY BECAUSE THE TOKEN'S STRENGTH IS NOT THE PATH'S. The admission itself is
// unforgeable (structural). This GATE is only mechanically preventable: `encode_closure_document`
// below remains callable directly, so a caller bypassing this entry can still emit uncontained arms
// with no admission. The wall is at the entry, not on the carrier.
// partial document written by accident. The two questions are therefore two ENTRY POINTS rather than
// one entry point with an optional token:
//
// encode_complete_closure_document(closure) refuses if anything is uncontained
// encode_admitted_partial_closure_document(a) total; the admission IS the decision
//
// WHY THE PARTIAL ENTRY TAKES ONE ARGUMENT. Its predecessor took a closure PLUS an optional
// admission and checked only that the admission was PRESENT -- so an admission minted for closure A
// authorized encoding closure B, and no amount of checking inside this function could have noticed,
// because the token carried no subject. The admitted carrier holds its own closure, so there is no
// second closure to disagree with it and the mismatch has no spelling. That is why this entry
// performs no validation at all: there is nothing left to validate.
//
// RUNG, STATED HONESTLY BECAUSE THE CARRIER'S STRENGTH IS NOT THE PATH'S. The subject binding is
// structural. This GATE is still only mechanically preventable: encode_closure_document below
// remains callable directly, so a caller bypassing these entries can emit uncontained arms with no
// admission at all. The wall is on the carrier now, but the module's front door is still ajar.
// dissolve-on: module-private functions in .dag, at which point the unchecked encoder stops being
// reachable and the gate becomes structural. Until then this comment is the only thing saying so.
fn encode_closure_document_checked(
store: ObjectStore,
root: ObjectId,
admission: PartialClosureAdmission?
) -> ClosureDocEncodeOutcome {
match unresolved_identities(closure: CommitClosure { store: store, root: root }) {
fn encode_complete_closure_document(closure: CommitClosure) -> ClosureDocEncodeOutcome {
match unresolved_identities(closure: closure) {
missing =>
if list_length(items: missing) == 0 {
ClosureDocEncoded { value: encode_closure_document(store: store, root: root) }
ClosureDocEncoded {
value: encode_closure_document(store: closure.store, root: closure.root)
}
} else {
match admission {
Present { value: _ } =>
ClosureDocEncoded { value: encode_closure_document(store: store, root: root) }
Absent =>
ClosureDocEncodeRefused {
cause: ClosureDocIncompleteWithoutAdmission {
identity: first_uncontained_key(missing: missing)
}
}
ClosureDocEncodeRefused {
cause: ClosureDocIncompleteWithoutAdmission {
identity: an_uncontained_key(missing: missing)
}
}
}
}
}

// TOTAL, AND THE TOTALITY IS THE CLAIM. Every way of obtaining an AdmittedPartialCommitClosure runs
// through a mint that derived the unresolved population from this very closure, so by the time one
// exists there is nothing this function could refuse that the mint did not already settle.
fn encode_admitted_partial_closure_document(admitted: AdmittedPartialCommitClosure) -> JsonValue {
encode_closure_document(store: admitted.closure.store, root: admitted.closure.root)
}

// The first identity that would have been written as an uncontained arm. Naming one is what makes
// the refusal actionable; naming all of them is the caller's own query via unresolved_identities.
fn first_uncontained_key(missing: List<ObjectId>) -> String {
// AN uncontained key, not THE FIRST. Same correction as an_uncontained_target in repository_envelope:
// the refusal needs one actionable example and no consumer depends on which, so the name should not
// promise an ordering nothing verifies.
fn an_uncontained_key(missing: List<ObjectId>) -> String {
fold(missing, init: "", f: fn(acc, id) {
if acc == "" { object_id_key(identity: id) } else { acc }
})
Expand Down Expand Up @@ -995,3 +1030,70 @@ fn decode_closure_document_body(v: JsonValue) -> ClosureDocLoadOutcome {
_ => ClosureDocRefused { cause: ClosureDocMemberWrongShape { key: "objects" } }
}
}

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

// THIS FORMAT'S REFUSALS, CLASSIFIED BESIDE THE REFUSALS THEMSELVES.
//
// The standing vocabulary is format-agnostic and lives in gunbc.scm.load_standing; the mapping from
// THIS format's causes into it belongs HERE, next to the coproduct it reads, so a new refusal
// variant fails to compile where its author already is rather than in a consumer that has never
// heard of it. A consumer computing this by matching on ClosureDocRefusal would be reaching into one
// format's error enum for a format-agnostic answer -- the placement defect that closed gunbc#8940.
//
// WHY UNKNOWN MEMBERS AND UNKNOWN VARIANT TAGS ARE MALFORMED, NOT A NEWER WRITER, which follows from
// this module's own policy rather than from taste: a schema that grows a member grows a NEW FORMAT
// TAG. So a conforming newer writer emits a new tag; it does not emit this one carrying extras. A
// document under a MATCHED tag with an unrecognized member or variant is a broken document of THIS
// schema, and calling it "needs a compatible reader" would name a remedy that cannot arrive, because
// no conforming writer produced it.
//
// WHY AN UNRESOLVED POSITION IS MALFORMED AND NOT A FETCHABLE ABSENCE. A position denotes nothing
// outside the document that defines it, so an unresolved `at` names no object anyone could supply.
// Fetchable absence is the UNCONTAINED arm, which is not a refusal at all and never reaches here.
//
// WHY A COLLISION IS ITS OWN STANDING. object_store states both colliding records are legitimate and
// the forged pairing is prevented by construction, so a collision means the structural locator
// cannot represent both -- not that either is damaged. Classifying it as malformed would let a
// reader DISCARD A WRITER'S VALID GENERATION over an honest hash coincidence.
fn closure_document_load_standing(cause: ClosureDocRefusal) -> LoadStanding {
match cause {
ClosureDocFormatUnrecognized { found: _ } => LoadUnsupportedProtocol
ClosureDocObjectCollision { identity: _ } => LoadIdentityCollision
ClosureDocNotAnObject => LoadDocumentMalformed
ClosureDocMemberMissing { key: _ } => LoadDocumentMalformed
ClosureDocMemberDuplicated { key: _ } => LoadDocumentMalformed
ClosureDocMemberWrongShape { key: _ } => LoadDocumentMalformed
ClosureDocUnknownKindTag { found: _ } => LoadDocumentMalformed
ClosureDocUnknownConnectiveTag { found: _ } => LoadDocumentMalformed
ClosureDocUnknownBehaviorTag { found: _ } => LoadDocumentMalformed
ClosureDocUnknownLabelTag { found: _ } => LoadDocumentMalformed
ClosureDocUnexpectedMember { context: _, key: _ } => LoadDocumentMalformed
ClosureDocEdgeTargetUnresolved { reference: _ } => LoadDocumentMalformed
ClosureDocRootUnresolved { reference: _ } => LoadDocumentMalformed
ClosureDocTargetNotOneArm { found: _ } => LoadDocumentMalformed
ClosureDocUncontainedDigestInvalid { found: _ } => LoadDocumentMalformed
}
}

// A LOAD THAT SUCCEEDED STILL HAS A STANDING, and it is not always LoadComplete. This is the arm the
// predecessor format could not produce: a document whose uncontained references leave objects the
// store does not hold loads correctly and is PARTIAL, which is a success with an obligation rather
// than a failure. Completeness is derived from the objects, never a flag beside them.
fn loaded_closure_standing(store: ObjectStore, root: ObjectId) -> LoadStanding {
if closure_is_complete(closure: CommitClosure { store: store, root: root }) {
LoadComplete
} else {
LoadPartial
}
}

fn closure_document_standing(outcome: ClosureDocLoadOutcome) -> LoadStanding {
match outcome {
ClosureDocLoaded { store: store, root: root } =>
loaded_closure_standing(store: store, root: root)
ClosureDocRefused { cause: cause } => closure_document_load_standing(cause: cause)
}
}
Loading
Loading