Skip to content
Merged
Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
c78322b
Give the SCM object store two kinds of object, so a file has somewher…
Sep 1, 2026
8b57788
Apply the authored-source tagging rule to both arms, and make the inv…
Sep 1, 2026
921a90c
Execute the authored-source checkout refusal instead of arguing it fr…
Sep 1, 2026
22dfe35
Refuse for the right owner: split MemberFailed, and stop reporting a …
Sep 1, 2026
7f92f9d
Put every annotation above a subject, and ask the store for a NODE wh…
Sep 1, 2026
ceb3c9f
Brand a node reference so a file cannot inhabit a program position, a…
Sep 1, 2026
488b09d
Compare records by what the identity is derived from, and count the d…
Sep 1, 2026
fc10106
Name the identity rule for its subject, and freeze a predecessor docu…
Sep 1, 2026
dce2a40
The module names the codec and the tag names the version: retire a su…
Sep 1, 2026
71a5c49
Merge remote-tracking branch 'origin/main' into scm-object-model
Sep 1, 2026
9fefe55
Restore the rung-drop row an auto-merge deleted, and revert a module …
Sep 1, 2026
5ba7ade
Execute the authored-source wire round trip in both arms
Sep 1, 2026
40927ea
Integrate main, regenerating the projections rather than picking a side
Sep 1, 2026
8907b18
Make a node requirement a proposition, and let only the store answer it
Sep 1, 2026
8cf125c
Canonicalize on the other route too, and stop fabricating a collision
Sep 1, 2026
b8682d7
Derive dependency order instead of trusting insertion order
Sep 1, 2026
e710a35
Delete the two node-presence predicates the census replaced
Sep 1, 2026
651c991
Name the repository codec for the tag it implements, and freeze a rea…
Sep 1, 2026
837115a
Integrate main
Sep 1, 2026
54cd2e4
Read both census populations everywhere, not just the absent one
Sep 1, 2026
9bdd976
Seal the raw closure encoder behind a carrier the bad state cannot in…
Sep 1, 2026
103f2d5
Separate a wrong-kind commit root from an absent one, and execute the…
Sep 1, 2026
bec5a32
Make the commit-root fold exhaustive instead of rostering its wildcard
Sep 2, 2026
689a2b5
Carry the standing to its destination, scope the image claim, sweep t…
Sep 2, 2026
66f72d5
State the populations that exist, not the ones these notes were writt…
Sep 2, 2026
f9bbb36
Merge remote-tracking branch 'origin/main' into scm-object-model
Sep 2, 2026
e141a76
Exclude witness helpers from the census denominator, by name
Sep 2, 2026
5bdb538
Regenerate the Rust source-type bindings from their authority
Sep 2, 2026
f25132c
Two claims quantified over a population they did not check
Sep 2, 2026
aec3deb
Merge remote-tracking branch 'origin/main' into scm-object-model
Sep 2, 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
1 change: 1 addition & 0 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,7 @@ At a service boundary, rung honesty has a commercial consequence: a dimension ma
Every newly discovered error class — incident, review finding, runtime exception, falsifier divergence — files or updates one row: invalid state, harm, distinguishing facts, rung found at, ceiling with reason, next trigger. Declared drops are rostered in full — previous rung, temporary rung, reason, population, restoration trigger — in [docs/design-ledgers.md](docs/design-ledgers.md), authority `gunbc.rung_drop`. A drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, so the trigger is the whole check. The ones standing today:

- **Emitted-bytes fixture witnesses in a required lane** — declared 2026-09-01
- **Direct-call argument TYPE-COMPAT judgment inside v2.* modules (one of two arms; inhabitance still runs)** — declared 2026-09-01
- **CI required-run composition** — declared 2026-08-15
- **Self-host emission board measurement** — declared 2026-08-24
- **Regen candidate-tree producer** — declared 2026-08-20
Expand Down
9 changes: 9 additions & 0 deletions dag/gunbc/rung_drop.dag
Original file line number Diff line number Diff line change
Expand Up @@ -92,8 +92,17 @@ data fabric_evidence_gating: RungDrop = RungDrop { identity: "fabric_evidence_ga

data emitted_bytes_witness_required_lane: RungDrop = RungDrop { identity: "emitted_bytes_witness_required_lane" as NonEmptyStr, subject: "Emitted-bytes fixture witnesses in a required lane", declared: "2026-09-01", standing: Standing, authored: "Witness enrollment — **RUNG DROP, DECLARED (2026-09-01, gunbc#9850 witness enrollment).** PREVIOUS RUNG: none to lower — this declares that the mechanically-preventable rung for the emission-follows-resolution class (the 139-row use-line shadow repaired in gunbc#9850) is held by a test OUTSIDE the required aggregate. TEMPORARY RUNG: the discriminating RED and positive controls are enrolled as `emit_import_lines_follow_resolved_binding_identity` in `v1.compiler.compiler_tests_rust`, emitted into `compiler_tests.rs` and executed by `repo_self_test_command` (`cargo test --release -p v1-compiler --lib`) in the `rust-unit-tests` job of `gunbc.witness_floor_workflow` — which runs on every push and pull request but is NOT a `needs` of the required aggregate, so a regression reddens a visible job without blocking the merge. REASON: no substrate-visible surface exposes EMITTED BYTES to a `dag/test/claim` witness (the host census builtin carries diagnostics only), so the assertion is inexpressible in the required floor today; promoting `rust-unit-tests` to required was measured 2026-09-01 at 23/25 recent completions green with both failures runner-environment faults (shared-runner `$HOME`/cargo-shim class) — an ~8% infra-noise rate ruled too high to make 612 tests merge-blocking fleet-wide tonight. POPULATION: the emission-follows-resolution witness matrix (String RED, structural-Bool and non-kernel controls) plus every other `compiler_tests` row asserting on emitted bytes. RESTORATION TRIGGER, named at capability grain: a required-lane capability SUFFICIENT to execute, on the real acceptance path, a fixture assertion that a named `pub use` line is ABSENT from emitted bytes for a sole-exporter structural type resolved to a host-realized kernel scalar, and PRESENT for a structural kernel carrying a connective (Bool = True | False) — via either (i) `rust-unit-tests` promoted into the required aggregate after its runner-fault class is retired or priced, or (ii) a substrate-visible emitted-bytes probe surface admitted under the scaffold doctrine. A surface that can read emitted bytes but cannot discriminate those two cases does NOT satisfy this trigger." }

data direct_call_arg_seam_v2_exemption: RungDrop = RungDrop {
identity: "direct_call_arg_seam_v2_exemption" as NonEmptyStr,
subject: "Direct-call argument TYPE-COMPAT judgment inside v2.* modules (one of two arms; inhabitance still runs)",
declared: "2026-09-01",
standing: Standing,
authored: "**ONE OF THE TWO DIRECT-CALL ARGUMENT JUDGMENTS IS SWITCHED OFF FOR EVERY `v2.*` MODULE, AND THIS ROW DECLARES THAT RUNG (2026-09-01).** The suppressed arm is `arg_compat_diags`; the inhabitance arm beside it is ungated and still runs there. That split is measured below, not assumed, and the loose reading -- that argument checking is off in `v2.*` -- is what this row exists to stop being repeated. `v1.compiler.infer` `module_skips_direct_call_arg_check` returns true for every module whose declared name begins with `v2.`, so at a direct call inside such a module the argument-position TYPE-COMPAT judgment does not run. It is ONE of two arms and the measurement below says which: the ungated inhabitance arm still runs there, so this is a narrowed judgment, not an absent one. The predicate is not new and its cost is not disputed: `gunbc.doc_graph_roots` already names it as the one in-tree violation of the no-escape-hatch clause, in its own words that the compiler being bootstrapped is authored under weaker checks than ordinary source. What has never existed is this row. PREVIOUS RUNG AT THIS ROW'S OWN SUBJECT GRAIN: NONE STOOD, and saying otherwise would be the cross-path inflation DESIGN 4b(1) forbids (codex review 58154, which caught it here). The subject is the compat arm INSIDE `v2.*`. That arm has never executed there -- the exemption predates this row -- so there is no rung for this row to have lowered and none is claimed. What the fixture establishes is a DIFFERENT path: that the suppressed check operates OUTSIDE the exemption, on the same tree and the same binary, which is what makes the exemption a real loss of an available guarantee rather than a check nobody has. Those two facts must not be averaged: `mechanically preventable outside v2.*` and `never executed inside v2.*` are separate paths, and a class's rung is the MINIMUM across its in-scope paths. This row therefore declares a STANDING ABSENCE at its subject grain rather than a regression, and it is filed as a drop because the obligation 4b(3) attaches -- population, reason, and a trigger that can retire it -- is the obligation an undeclared permanent exemption was escaping. TEMPORARY RUNG for the compat arm inside `v2.*`: mitigatable where the emitted-Rust self-host closure covers the module, because a wrong argument surviving acceptance becomes a rustc type error in the emitted crate -- refused late, in the wrong compiler, in the wrong phase -- and UNGUARDED on the source-acceptance path for every `v2.*` module that closure does not reach. Those are two paths and the row reports the MINIMUM, so the temporary rung for this subject is UNGUARDED, not mitigatable; the mitigated path is named because it bounds where the loss is observable at all, never to raise the reported rung. The ungated inhabitance arm keeps its rung throughout and is NOT part of this drop. REASON: the exemption's stated justification is representation-gap false positives at the argument seam — the same four classes the conformance lane grounds (brand aliases, optionality's two representations, anonymous record literals, expansion depth) — plus an unlocated historical claim of 104 TypeMismatch false positives that two audits have failed to find a receipt for. Its deletion is gunbc#8924, which is COMPLETE and MEASURED and CLOSED, held because its one missing precondition is a resolve-layer seam whose repair was DECLINED at the owning layer on 2026-08-22 with no owner and no schedule. THE POPULATION IS RESTATED HERE AND IT IS NOT THE ONE THE HOLD WAS PRICED AGAINST. The reopening condition recorded on `gunbc.doc_graph_roots` bounds the blast radius at 9 declarations under `src/v2/extdeps/formatters/`. The predicate's actual population is EVERY MODULE WHOSE DECLARED NAME BEGINS WITH `v2.` — the instrument is the predicate itself, re-derivable by matching `^module v2.` against the corpus's module declarations, and the count is deliberately not transcribed here. That population includes the SELF-HOST EMISSION CLOSURE. WHAT THE EXEMPTION ACTUALLY SUPPRESSES, MEASURED AT DIAGNOSTIC IDENTITY RATHER THAN ARGUED FROM THE PREDICATE. The instrument is one fixture authored twice, byte-identical but for its module line and a renaming of every declaration so nothing resolves across the pair, run through a gunbc built from this tree. Three arms each: a local alias parameter (`type Wrapped = FreeMonoid<Char>` declared in the calling module), a cross-module declaration-path parameter (`v2.std.text.String`), and an `Int` parameter as control, each receiving a kernel `String` actual. NON-`v2.` MODULE: the local-alias arm is ADMITTED with no diagnostic; the declaration-path arm REFUSES with `value does not inhabit its declared type at the direct call argument`, declared `Node(std.algebra.FreeMonoid<Product(Char)>)` produced `Primitive(String)`; the control REFUSES TWICE, once with `type mismatch: expected Primitive(Int), got Primitive(String)` and once with the inhabitance message. `v2.*` MODULE: the local-alias arm is ADMITTED; the declaration-path arm REFUSES with the SAME inhabitance message; the control refuses with the inhabitance message ONLY. EXACTLY ONE DIAGNOSTIC IDENTITY DISAPPEARS across the pair -- the `type mismatch` row -- and every other identity is preserved. That is the drop, measured: this exemption suppresses `arg_compat_diags` and NOTHING ELSE. THE SCOPE OF THE LOSS IS THEREFORE NARROWER THAN THE PREDICATE NAME SUGGESTS, and stating it narrowly is the point of measuring it. `v1.compiler.infer` computes `arg_compat_diags` under this gate and calls `direct_call_argument_inhabitance_diags` immediately after with NO gate, both feeding one `concat`, so the INHABITANCE judgment runs inside `v2.*` exactly as it runs everywhere else. A reader who takes the argument judgment to be off in `v2.*` -- as the first draft of this row did -- will misattribute every surviving refusal and every surviving admission. CONSEQUENTLY THIS ROW CLAIMS NO SELF-HOST HARM AND NAMES NONE. The specimen anyone reaches for first is `src/v2/std/integer.dag` calling `v2.std.text` `string_head`, whose emitted Rust rustc refuses; that call is NOT hidden by this exemption, because the surviving inhabitance arm is the one that judges its shape and the fixture shows the compat arm would not have refused it either. That shape belongs to a DIFFERENT and already-standing declaration, `text_boundary_identity_wall`. Citing it here would be an unbacked execution claim. THE CLAIM IS NOT THAT THE BLAST RADIUS NOW EXCEEDS 9. It is that THE SUBJECT CHANGED and the old bound no longer describes what is being bought, which is a reason to re-measure; a declared drop whose population is measured against a subject it no longer covers is the drop lying about its own size. ONE CONSEQUENCE FOR ANY READER OF A GREEN `v2.*` CALL SITE, stated precisely because the loose version of it is the easiest false inference available here and this row asserted the loose version first: a `v2.*` call site accepted WITHOUT a compat diagnostic says nothing, because that arm cannot speak there; a `v2.*` call site accepted with no INHABITANCE diagnostic says exactly what it says everywhere else, because that arm is ungated. A discriminating red for the SUPPRESSED arm is therefore only authorable in a non-`v2.` module -- not because the wall is absent in `v2.*`, but because only one of its two arms is. RESTORATION TRIGGER, named at capability grain: the resolve-layer seam capability that makes `arg_compat_diags` RUNNABLE on `v2.*` modules -- the argument-position conformance relation grounding the representation gaps that motivated the exemption (brand aliases, optionality's two representations, anonymous record literals, expansion depth), so that the compat arm refuses genuinely wrong argument bindings inside `v2.*` without fabricating a refusal against those four grounded classes. That capability is SUFFICIENT only under a two-direction A/B measured the way this row's own population was: the twin fixture re-run, with the `type mismatch` identity PRESENT on both the non-`v2.` and the `v2.*` side, and the corpus's existing `v2.*` call sites still ADMITTED. gunbc#8924 MERGING IS NOT THIS TRIGGER, and neither is any measurement that only re-prices the hold; the trigger is the seam being repaired at its owning layer, which was DECLINED on 2026-08-22 and is UNOWNED as of this declaration -- a trigger nobody is holding is still a trigger, and a reader must be able to see that nobody is holding it."
}

data rung_drop_roster: List<RungDrop> = [
emitted_bytes_witness_required_lane,
direct_call_arg_seam_v2_exemption,
floor_cut,
measurement_bankruptcy,
regen_producer,
Expand Down
60 changes: 50 additions & 10 deletions dag/gunbc/scm/checkout.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,16 @@ import gunbc.scm.ancestry { RepositoryCommitRef }
import gunbc.scm.object_store {
ObjectId,
ObjectRecord,
SemanticNodeObjectRef,
NodeTarget,
NodeTargetResolved,
NodeTargetUnresolved,
ObjectStore,
StoredEdge,
find_object,
NodeRecordFound,
NodeRecordAbsent,
NodeRecordIsAuthoredSource,
find_node_record,
}

// A COMMIT IS A ROOT IDENTITY AND NOTHING ELSE. No parent, no author, no timestamp, no message, no
Expand All @@ -25,11 +32,19 @@ import gunbc.scm.object_store {
// and a single timeline. Keeping the commit to its root is what lets two commits be compared,
// deduplicated and reconstructed without consulting any history at all.
type Commit {
root: ObjectId
root: NodeTarget
}

// AN AUTHORED SOURCE AT A PROGRAM POSITION IS ITS OWN REFUSAL, NOT A MISSING OBJECT.
//
// Once the store holds two kinds of object, a checkout can reach an identity that IS present and is
// a file rather than a program. Reporting that as MissingObject would send an operator looking for
// bytes that are right there, which is the not-applicable-rendered-as-malformed failure -- the two
// have opposite remedies. It is also not silently skippable: reconstructing the node without that
// child would hand back a program the commit does not name.
type CheckoutRefusal
= MissingObject { identity: ObjectId }
| ObjectIsAuthoredSource { identity: ObjectId }

type CheckoutOutcome
= CheckedOut { program: Node }
Expand Down Expand Up @@ -59,7 +74,7 @@ fn checkout_edge_step(store: ObjectStore, acc: CheckoutEdgeAcc, stored: StoredEd
match acc.refusal {
Present { value: _ } => acc
Absent =>
match checkout_object(store: store, identity: stored.target) {
match checkout_node_target(store: store, target: stored.target) {
CheckoutRefused { cause: cause } =>
CheckoutEdgeAcc { edges: acc.edges, refusal: Present { value: cause } }
CheckedOut { program: child } =>
Expand All @@ -71,6 +86,23 @@ fn checkout_edge_step(store: ObjectStore, acc: CheckoutEdgeAcc, stored: StoredEd
}
}

// AN UNCONTAINED TARGET IS RESOLVED HERE, NOT PREJUDGED ABSENT. The arm records that the DOCUMENT
// did not carry the object; it does not record that this store lacks it, and a graft may have
// supplied it since. So both arms go through the same lookup and the uncontained one keeps the two
// negatives apart -- absent, or a file -- exactly as the resolved arm does.
fn checkout_node_target(store: ObjectStore, target: NodeTarget) -> CheckoutOutcome {
match target {
NodeTargetResolved(reference) => checkout_object(store: store, identity: reference)
NodeTargetUnresolved(locator) =>
match find_node_record(store: store, identity: locator) {
NodeRecordAbsent { identity: i } => CheckoutRefused { cause: MissingObject { identity: i } }
NodeRecordIsAuthoredSource { identity: i } =>
CheckoutRefused { cause: ObjectIsAuthoredSource { identity: i } }
NodeRecordFound(record) => checkout_record(store: store, record: record)
}
}
}

fn checkout_record(store: ObjectStore, record: ObjectRecord) -> CheckoutOutcome {
match fold(
record.children,
Expand All @@ -86,10 +118,18 @@ fn checkout_record(store: ObjectStore, record: ObjectRecord) -> CheckoutOutcome
}
}

fn checkout_object(store: ObjectStore, identity: ObjectId) -> CheckoutOutcome {
match find_object(store: store, identity: identity) {
Absent => CheckoutRefused { cause: MissingObject { identity: identity } }
Present { value: record } => checkout_record(store: store, record: record)
// THE REFUSALS SURVIVE THE BRAND, AND SAYING WHY IS THE HONEST PART. A SemanticNodeObjectRef was
// minted against an object of node kind IN SOME STORE; it does not carry WHICH store. A reference
// minted against one store and resolved against another can therefore still find nothing, or find a
// file -- so these two arms are a live boundary between stores rather than a wall the brand already
// built. What the brand removes is the AUTHORING mistake: no caller can hand this function a
// locator it never resolved to a node at all.
fn checkout_object(store: ObjectStore, identity: SemanticNodeObjectRef) -> CheckoutOutcome {
match find_node_record(store: store, identity: identity.locator) {
NodeRecordAbsent { identity: i } => CheckoutRefused { cause: MissingObject { identity: i } }
NodeRecordIsAuthoredSource { identity: i } =>
CheckoutRefused { cause: ObjectIsAuthoredSource { identity: i } }
NodeRecordFound(record) => checkout_record(store: store, record: record)
}
}

Expand All @@ -100,7 +140,7 @@ fn checkout_object(store: ObjectStore, identity: ObjectId) -> CheckoutOutcome {
// agreement, which is precisely the property that makes a monotonic store unable to name a program
// on its own.
fn checkout(store: ObjectStore, commit: Commit) -> CheckoutOutcome {
checkout_object(store: store, identity: commit.root)
checkout_node_target(store: store, target: commit.root)
}

// The rebuilt program carries OccurrenceSynthetic throughout, because occurrence identity is
Expand All @@ -109,7 +149,7 @@ fn checkout(store: ObjectStore, commit: Commit) -> CheckoutOutcome {
// and reconstruct identically. Round-trip equality is therefore asserted on content identity, never
// on occurrence provenance -- and asserting it on provenance would be asserting the one property the
// model says must not matter.
fn commit_of_root(root: ObjectId) -> Commit {
fn commit_of_root(root: NodeTarget) -> Commit {
Commit { root: root }
}

Expand Down Expand Up @@ -177,7 +217,7 @@ fn checkout_repository_at(repo: RepositoryEnvelope, reference: RepositoryCommitR
match commit_at_reference(commits: repo.commits, reference: reference) {
Absent => CheckoutReferenceUnresolved { reference: reference }
Present { value: selected } =>
match checkout(store: repo.store, commit: commit_of_root(root: selected.root)) {
match checkout(store: repo.store, commit: commit_of_root(root: NodeTargetResolved(selected.root))) {
CheckoutRefused { cause: cause } =>
CheckoutProgramUnreconstructable { reference: reference, cause: cause }
CheckedOut { program: program } =>
Expand Down
Loading
Loading