From c81c958003c81d89ce0bedebee881333013758bf Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 12:50:15 +0000 Subject: [PATCH 1/7] XL-5 model-work: the v1 consumer census and the claim conservation wall, on the exact cut's own vocabulary Two carriers, both refusing today by construction, with fixtures that make every refusal executable now rather than at release: - gunbc.v1_consumer_census: consumer x consumed-authority relations in gunbc.replacement_cut BoundaryConsumer / ConsumerDisposition (no minted disposition vocabulary), each row carrying its medium, subject, and the producer + command + revision that found it. Population is honestly PopulationMeasuredLowerBound; the admission gate reads completeness, so the bankruptcy transaction refuses. Four hand-Rust shim consumers the exact vocabulary cannot cite are carried as the projection's own refusal shape, never as fabricated DeclarationRefs. - gunbc.v1_witness_census: one disposition per pre-cutover claim identity (Retired / ReplacedByStronger with an executed red / StillRequired), with floor standing as a SEPARATE axis (v2.workflow.required_floor RequiredFloorDisposition) per ruling, projecting onto EvidenceDisposition. Five-direction identity-join conservation wall; live roster declared Unmeasured until a floor run supplies it. 19 witnesses PASS by execution (claim_batch, remote build at f1f9dd8a077). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- dag/gunbc/v1/v1_consumer_census.dag | 554 ++++++++++++++++++ dag/gunbc/v1/v1_witness_census.dag | 229 ++++++++ .../claim/v1_consumer_census_witness_test.dag | 111 ++++ .../claim/v1_witness_census_witness_test.dag | 123 ++++ .../fixture/v1_consumer_census/specimens.dag | 129 ++++ .../fixture/v1_witness_census/specimens.dag | 126 ++++ 6 files changed, 1272 insertions(+) create mode 100644 dag/gunbc/v1/v1_consumer_census.dag create mode 100644 dag/gunbc/v1/v1_witness_census.dag create mode 100644 dag/test/claim/v1_consumer_census_witness_test.dag create mode 100644 dag/test/claim/v1_witness_census_witness_test.dag create mode 100644 dag/test/fixture/v1_consumer_census/specimens.dag create mode 100644 dag/test/fixture/v1_witness_census/specimens.dag diff --git a/dag/gunbc/v1/v1_consumer_census.dag b/dag/gunbc/v1/v1_consumer_census.dag new file mode 100644 index 00000000000..ed9e2719960 --- /dev/null +++ b/dag/gunbc/v1/v1_consumer_census.dag @@ -0,0 +1,554 @@ +module gunbc.v1_consumer_census + +import std.types { List, String, NonEmptyStr, Bool, Int } +import std.decl_ref { DeclarationRef, decl_ref } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import gunbc.replacement_cut { + BoundaryConsumer, BoundaryCensus, ConsumersEnumerated, + ConsumerDisposition, RetainSameContract, RetainChangedContract, ReplacedByY, EvidenceOnly, Retire, Undecided, + CoverageClaim, Covered, CoverageOpen +} + +// XL-5's FIRST DELIVERABLE: the population that has to be EMPTY before the bankruptcy transaction +// can execute, remeasured at the grain gunbc.replacement_cut requires. XL-5 is primarily a +// deletion, and a deletion's only real question is who is still holding on. This carrier answers +// it at consumer x consumed-authority identity, one disposition per relation, so "is v1 +// unreachable yet" is a JOIN rather than a recollection. +// +// WHY THIS CARRIER SPEAKS gunbc.replacement_cut's VOCABULARY AND MINTS NONE OF ITS OWN. The exact +// cut carrier already owns ConsumerDisposition and BoundaryConsumer, and gunbc.interpreter_replacement_cut +// registered its v1 survey as RegisteredCutRemeasureRequired precisely because that survey was +// authored at module-or-binary grain over a ten-of-125 sample -- a universe too coarse to inhabit +// the exact relation. This census IS that remeasurement (XL-N Manager ruling, 2026-08-29: XL-5 is +// the sole producer of the exact census and discharges the registered obligation). An earlier +// revision of this file minted a four-arm V1ConsumerDisposition beside ConsumerDisposition; that +// was a nickname for a concept with an authority, the DESIGN section 3 fork, and it is gone. The +// four names the XL-5 brief uses map onto the authority's arms without loss: replaced-by-native-v2 +// is ReplacedByY; retired-with-deleted-subject is Retire; still-required-and-blocking is +// RetainSameContract or RetainChangedContract with CoverageOpen -- which admit_replacement_cut_plan +// already refuses as UncoveredSurvivingConsumer; and replaced-by-stronger-witness is ReplacedByY +// naming the witness, with the STRENGTHENING carried by the witness census's evidence rows. +// +// WHAT THIS IS NOT. It is not the v1 exit model: gunbc.v1_deletion_plan owns the four finish lines +// and says it owns nothing else. This census discharges two of them -- InterpreterDeleted and +// ProductsV1Free -- and names them rather than restating their claims. It is not the maintenance +// standing: gunbc.v1_maintenance_standing governs v1 while it lives; this governs what must be +// true for it to stop living. + +data v1_consumer_census_subject_note: String = "WHAT IS BEING CONSUMED, at the grain a deletion actually operates on. These are not folders: src/v1 contains all of them and deleting the folder is the transaction, not the model. The axis matters because the dispositions differ per subject in a way a path cannot express -- the v1 CLI is REPLACED (v2 has to grow the verb), the generated stage0 mirrors are RETIRED WITH THEIR SUBJECT (they are projections of .dag authorities that move), and the v1 .dag source is neither: it is the regeneration loop's SUBJECT, so deleting it retires the loop rather than orphaning it. V1RuntimeBridge is separate from V1CompilerCrate because the bridge is reached by EMITTED code rather than by a caller in the tree, so its consumer population is discovered by a different instrument -- and the floor-cut plan's third measured bound says a reach measurement over one medium reads exactly like a reach measurement over all of them." + +type V1Subject + = V1CompilerCrate + | V1Interpreter + | V1RuntimeBridge + | V1Cli + | V1HostedCiBinary + | V1DagSource + | V1GeneratedStage0Mirror + | V1SerializedArtifact + +fn v1_subject_key(s: V1Subject) -> String { + match s { + V1CompilerCrate => "v1-compiler-crate" + V1Interpreter => "v1-interpreter" + V1RuntimeBridge => "v1-runtime-bridge" + V1Cli => "v1-cli" + V1HostedCiBinary => "v1-hosted-ci-binary" + V1DagSource => "v1-dag-source" + V1GeneratedStage0Mirror => "v1-generated-stage0-mirror" + V1SerializedArtifact => "v1-serialized-artifact" + } +} + +data v1_consumer_census_medium_note: String = "HOW THE DEPENDENCY IS SPELLED, and it is a KEY field rather than a note because the discovery instrument is per-medium and nothing in a per-medium answer announces the media it omitted. The floor-cut replacement plan measured this directly: eight orphan candidates by import graph fell to three once roster rows, test discovery, workflow argv and Cargo bin targets were joined, a five-in-eight false-positive rate produced entirely by asking one medium. A consumer census that swept only Rust `use` edges would have reported this repository's CI as v1-free, because CI reaches v1 through an argv string that no Rust instrument reads. Carrying the medium is what makes the omission of a medium a visible hole rather than a silent green." + +type ConsumerMedium + = CargoManifestDependency + | CargoBinTarget + | WorkflowArgv + | DagArgvRow + | RustUseEdge + | GitHookScript + | CommittedGeneratedMirror + | SerializedArtifactPath + +fn consumer_medium_key(m: ConsumerMedium) -> String { + match m { + CargoManifestDependency => "cargo-manifest-dependency" + CargoBinTarget => "cargo-bin-target" + WorkflowArgv => "workflow-argv" + DagArgvRow => "dag-argv-row" + RustUseEdge => "rust-use-edge" + GitHookScript => "git-hook-script" + CommittedGeneratedMirror => "committed-generated-mirror" + SerializedArtifactPath => "serialized-artifact-path" + } +} + +data v1_consumer_census_producer_note: String = "EVERY ROW NAMES THE INSTRUMENT THAT FOUND IT, AND THE COMMAND THAT RE-DERIVES IT. XL-5's standing rule is that a number without a producer, a source revision and a command is not a number, and DESIGN section 6 states the general form: name the instrument, never transcribe its output. Making the producer a REQUIRED FIELD turns that from a review habit into a construction -- a row with no producer has no constructor, so an author cannot file a consumer they merely remember. The command is carried verbatim so a reader re-derives rather than trusts; the revision is carried because a command's answer is a timestamped observation of a moving tree, not an identifier." + +type DiscoveryProducer { + instrument: String + command: String + source_revision: String +} + +fn discovery_producer(instrument: String, command: String, source_revision: String) -> DiscoveryProducer { + DiscoveryProducer { instrument: instrument, command: command, source_revision: source_revision } +} + +// THE ROW. The relation itself -- consumer x consumed_old_authority x disposition -- is the +// authority's BoundaryConsumer, carried whole rather than re-spelled, so v1_boundary_census() below +// projects straight into the exact carrier's BoundaryCensus. The three fields beside it are this +// census's own facts about how the relation was found. +type V1ConsumerRow { + boundary: BoundaryConsumer + medium: ConsumerMedium + subject: V1Subject + discovered_by: DiscoveryProducer +} + +fn v1cc_nes(s: String) -> NonEmptyStr { s as NonEmptyStr } + +fn v1_row_key(r: V1ConsumerRow) -> String { + concat(concat(concat(concat(r.boundary.consumer.module_path as String, "."), r.boundary.consumer.decl_name as String), " -> "), + concat(concat(r.boundary.consumed_old_authority.module_path as String, "."), r.boundary.consumed_old_authority.decl_name as String)) +} + +// WHICH ARMS BLOCK THE TRANSACTION, read off the authority's own vocabulary. A retained consumer +// with CoverageOpen is exactly what admit_replacement_cut_plan refuses as UncoveredSurvivingConsumer, +// and Undecided is what it refuses as UndispositionedConsumer; this predicate is those two causes +// asked of one row, so the blocking column here and the refusal there cannot disagree. +fn consumer_disposition_blocks(d: ConsumerDisposition) -> Bool { + match d { + RetainSameContract { justification: _, coverage: c } => v1cc_coverage_is_open(c: c) + RetainChangedContract { terminal_contract: _, justification: _, coverage: c } => v1cc_coverage_is_open(c: c) + ReplacedByY { new_authority: _ } => false + EvidenceOnly { surviving_claim: _, reenrolled_witness: _ } => false + Retire { reason: _ } => false + Undecided => true + } +} + +fn v1cc_coverage_is_open(c: CoverageClaim) -> Bool { + match c { + Covered { by: _ } => false + CoverageOpen => true + } +} + +fn consumer_disposition_successors(d: ConsumerDisposition) -> List { + match d { + RetainSameContract { justification: _, coverage: c } => coverage_authorities(c: c) + RetainChangedContract { terminal_contract: _, justification: _, coverage: c } => coverage_authorities(c: c) + ReplacedByY { new_authority: a } => [a as String] + EvidenceOnly { surviving_claim: _, reenrolled_witness: w } => [w as String] + Retire { reason: _ } => [] + Undecided => [] + } +} + +fn coverage_authorities(c: CoverageClaim) -> List { + match c { + Covered { by: b } => [b as String] + CoverageOpen => [] + } +} + +data v1_consumer_census_uncitable_note: String = "A CONSUMER THE EXACT VOCABULARY CANNOT SPELL IS CARRIED AS A REFUSAL, NEVER AS A FABRICATED REFERENCE. gunbc.rust_item_host_observation item_declaration_ref projects a Rust item into DeclarationRef through rust_source_namespace_rows, and those rows claim prefixes under src/v1 only. The four self-host shim crates under dag/gunbc/instruments/ are hand-authored Rust OUTSIDE every claimed prefix, so the projection returns ItemDeclarationRefRefused for each of them -- and a BoundaryConsumer needs a DeclarationRef on both sides. The two dishonest moves are to invent a module path the projection did not produce, or to drop the four from the census because the carrier has no slot for them; both make the population look smaller than it is. So they are carried here in the projection's own refusal shape, with their disposition, and they COUNT toward the blocking column and toward the lower-bound standing below. The capability that dissolves this list is a rust_source_namespace_rows row for the instruments directory, at which point these four become ordinary BoundaryConsumer rows and this list is empty by construction rather than by edit." + +type V1UncitableConsumer { + item_key: String + refusal_detail: String + medium: ConsumerMedium + subject: V1Subject + disposition: ConsumerDisposition + discovered_by: DiscoveryProducer +} + +data v1_consumer_census_population_note: String = "COMPLETENESS IS A STRUCTURAL FACT, NOT A CLAIM IN A COMMENT. The three arms answer the transaction's admission gate OPPOSITELY, and a bare List cannot tell them apart: an empty blocking column means 'nothing blocks' under Complete, 'nothing was measured' under Unmeasured, and 'nothing blocks among what was measured' under MeasuredLowerBound -- three different facts one `[]` would spell identically. gunbc.replacement_cut BoundaryCensus carries ConsumersEnumerated | BoundaryDeclaredEmpty and has no lower-bound arm, because an exact cut may not be authored over a lower bound at all; this carrier is what stands BETWEEN a measurement and that census, and the lower-bound arm is where a partial measurement lives while it is still partial. v2.compiler.effect_demand DemandPopulation carries the same three-way shape for XL-1's demand rows; the two are one concept at two subjects and are not consolidated here because that module is in flight on XL-1's branch and does not exist on main. The dissolution condition below names the merge, not the file." + +type ConsumerPopulation + = PopulationMeasuredComplete { rows: List, joined_media: List } + | PopulationMeasuredLowerBound { rows: List, uncitable: List, missing_basis: String } + | PopulationUnmeasured { reason: String } + +fn consumer_population_rows(p: ConsumerPopulation) -> List { + match p { + PopulationMeasuredComplete { rows: r, joined_media: _ } => r + PopulationMeasuredLowerBound { rows: r, uncitable: _, missing_basis: _ } => r + PopulationUnmeasured { reason: _ } => [] + } +} + +fn consumer_population_uncitable(p: ConsumerPopulation) -> List { + match p { + PopulationMeasuredComplete { rows: _, joined_media: _ } => [] + PopulationMeasuredLowerBound { rows: _, uncitable: u, missing_basis: _ } => u + PopulationUnmeasured { reason: _ } => [] + } +} + +fn consumer_population_is_complete(p: ConsumerPopulation) -> Bool { + match p { + PopulationMeasuredComplete { rows: _, joined_media: _ } => true + PopulationMeasuredLowerBound { rows: _, uncitable: _, missing_basis: _ } => false + PopulationUnmeasured { reason: _ } => false + } +} + +data v1_consumer_census_population_dissolution: DissolutionCondition = unbound_dissolution(description: "dissolve-on: a single generic completeness carrier is declared once and consumed by BOTH this census and v2.compiler.effect_demand, after XL-1's branch merges to main. Until then the two lanes carry the shape separately, which is a known duplicate held deliberately rather than an unnoticed fork. NOT satisfied by either lane deleting its own copy and importing the other's while the other is unmerged -- that produces a carrier whose provider does not exist on main, which is a worse state than the duplicate. The capability this names is one completeness axis with one declaring module reachable from main, not the deletion of a type.") + +// THE PRODUCERS. One declaration per instrument, so a row cites a producer rather than restating a +// command, and re-deriving the whole census is reading the commands below rather than every row. + +data v1_census_revision: String = "f1f9dd8a077f976c48d389201a2c41e54ccd0c15" + +data producer_workflow_argv: DiscoveryProducer = discovery_producer( + instrument: "argv and cargo invocations in the emitted workflow surface, traced back to the .dag step declaration that emits each one", + command: "grep -nE 'target/release/|cargo (build|test).*v1-compiler' .github/workflows/*.yml; then the emitting declaration in gunbc.witness_floor_workflow / gunbc.fleet_desired_admission_workflow / gunbc.fleet_converge_workflow", + source_revision: v1_census_revision, +) + +data producer_cargo_manifest_graph: DiscoveryProducer = discovery_producer( + instrument: "path dependencies among the v1 crate manifests and the workspace member region", + command: "git grep -n 'path = \"\\.\\./stage0' -- '*/Cargo.toml'; sed -n 1,20p Cargo.toml", + source_revision: v1_census_revision, +) + +data producer_rust_bridge_edge: DiscoveryProducer = discovery_producer( + instrument: "v1_rt references in Rust outside src/v1, each projected through gunbc.rust_item_host_observation item_declaration_ref", + command: "git grep -l 'v1_rt' -- '*.rs' | grep -v '^src/v1'", + source_revision: v1_census_revision, +) + +data producer_generated_mirror: DiscoveryProducer = discovery_producer( + instrument: "the committed generated Rust under src/v1, defined by its header rather than by basename, and the .gitattributes rows projected from the artifact registry", + command: "grep -rl 'Generated by' src/v1 --include=*.rs | wc -l; grep -c 'generated-artifact' .gitattributes", + source_revision: v1_census_revision, +) + +data producer_serialized_artifact: DiscoveryProducer = discovery_producer( + instrument: "the receipt paths the required workflow uploads, read from the declarations that name them", + command: "grep -oE '[a-z_]+\\.tsv' .github/workflows/witnesses.yml | sort -u; git grep -nE '^data [a-z_]+_path: String = \"[a-z_]+\\.tsv\"' -- dag/gunbc/witness/witness_floor_workflow.dag", + source_revision: v1_census_revision, +) + +data producer_git_hook: DiscoveryProducer = discovery_producer( + instrument: "v1 binary invocations inside the repository-local git hooks, traced to the emitting declaration", + command: "git grep -n 'target/release' .githooks/; git grep -ln 'generated-artifact-merge' -- 'dag/**/*.dag'", + source_revision: v1_census_revision, +) + +data producer_bin_roster_row: DiscoveryProducer = discovery_producer( + instrument: ".dag roster rows that enumerate v1 binary names for a workflow to build", + command: "git grep -n 'ci_floor_invoked_bins\\|witness_declared_release_bins' -- 'dag/gunbc/**/*.dag'", + source_revision: v1_census_revision, +) + +// IDENTITIES, declared once each. The Rust-item identities follow gunbc.rust_item_host_observation +// rust_source_namespace_rows exactly: src/v1/stage0/src/bin/.rs projects to +// v1_compiler.bin., src/v1/stage0/src/.rs to v1_compiler., src/v1/tests/src/.rs +// to v1_compiler_tests.. Nothing here is a spelling the projection would not produce. + +data claim_executor_bin: DeclarationRef = decl_ref(module_path: "v1_compiler.bin.claim_executor", decl_name: "main") +data gunbc_cli_bin: DeclarationRef = decl_ref(module_path: "v1_compiler.main", decl_name: "main") +data codex_session_bin: DeclarationRef = decl_ref(module_path: "v1_compiler.bin.codex_app_server_stdio_session", decl_name: "main") +data v1_compiler_crate_root: DeclarationRef = decl_ref(module_path: "v1_compiler.lib", decl_name: "lib") +data stage0_partition_rows: DeclarationRef = decl_ref(module_path: "v2.workflow.rust_crate_partition", decl_name: "stage0_partition_crate_rows") +data invoked_bins_row: DeclarationRef = decl_ref(module_path: "gunbc.ci_release_bins", decl_name: "ci_floor_invoked_bins") +data declared_release_bins_row: DeclarationRef = decl_ref(module_path: "gunbc.ci_release_bins", decl_name: "witness_declared_release_bins") +data witness_census_gate: String = "gunbc.v1_witness_census v1_claim_conservation_holds" + +fn retained_open(justification: String) -> ConsumerDisposition { + RetainSameContract { justification: v1cc_nes(s: justification), coverage: CoverageOpen } +} + +fn retired(reason: String) -> ConsumerDisposition { + Retire { reason: v1cc_nes(s: reason) } +} + +fn wfw(decl: String) -> DeclarationRef { + decl_ref(module_path: "gunbc.witness_floor_workflow", decl_name: decl) +} + +fn v1cc_boundary(consumer: DeclarationRef, authority: DeclarationRef, disposition: ConsumerDisposition) -> BoundaryConsumer { + BoundaryConsumer { consumer: consumer, consumed_old_authority: authority, disposition: disposition } +} + +fn tsv_row(path_decl: String) -> V1ConsumerRow { + { + boundary: v1cc_boundary( + consumer: wfw(decl: "witness_floor_tsv_upload_step"), + authority: wfw(decl: path_decl), + disposition: ReplacedByY { new_authority: v1cc_nes(s: witness_census_gate) }, + ), + medium: SerializedArtifactPath, + subject: V1SerializedArtifact, + discovered_by: producer_serialized_artifact, + } +} + +data v1_consumer_roster_note: String = "THE ROSTER. Every relation was established by running its cited producer against the revision above and reading the emitting declaration, and each row's identity is the relation a deletion would break, not the file the evidence was read in. Rows are not ordered by severity: the floor-cut plan's bounds say the dangerous member is the one nobody thought to look for, and ordering by an author's judgement is what lets a reader stop early.\n\nTHE RETAINED-OPEN ROWS ARE THE TRANSACTION. Everything else is discharged by deleting a subject or by a successor that already exists; the rows carrying CoverageOpen are the entire content of 'XL-5 cannot run yet', and each justification names the CAPABILITY that closes it -- never an artifact that would contribute to one, which DESIGN section 4b(3) rules is satisfied while the capability stays dead. That is the honest shape of a bankruptcy: the estate is mostly worthless, and the whole question is the creditors who are still owed.\n\nTHE TSV ROWS ARE FOUR RELATIONS, NOT ONE, because the authority's key is consumer x consumed authority and one upload step consumes four path declarations. Collapsing them would let one disposition stand for four dependencies, which is the exact conflation the key exists to refuse." + +data v1_consumers: List = [ + { + boundary: v1cc_boundary( + consumer: wfw(decl: "build_lane_run_step"), + authority: claim_executor_bin, + disposition: retained_open(justification: "the build lane of the required merge gate runs inside this binary. Closes on: an admitted native v2 compiler that executes the required gate roster end to end on a cold runner with no preinstalled gunbc and no src/v1 present -- NOT the existence of an emitted crate that cargo-checks, which is XL-0's gate and runs nothing"), + ), + medium: WorkflowArgv, + subject: V1HostedCiBinary, + discovered_by: producer_workflow_argv, + }, + { + boundary: v1cc_boundary( + consumer: wfw(decl: "witness_floor_run_step"), + authority: claim_executor_bin, + disposition: retained_open(justification: "the witness floor roster executes inside this binary, so every witness identity in the repository is reached through v1 today. Closes on: a native v2 witness fold that executes the same witness identities and refuses on subject loss -- the identity join gunbc.v1_witness_census carries, never a count of witnesses run"), + ), + medium: WorkflowArgv, + subject: V1HostedCiBinary, + discovered_by: producer_workflow_argv, + }, + { + boundary: v1cc_boundary( + consumer: wfw(decl: "rust_unit_tests_step"), + authority: v1_compiler_crate_root, + disposition: retired(reason: "the job's entire subject is the v1 crate's own #[test] functions, none of which asserts anything outside v1. #9663 added it because those tests ran on no CI path; it is one merge window old and retires with the code it was built to cover rather than being ported"), + ), + medium: WorkflowArgv, + subject: V1CompilerCrate, + discovered_by: producer_workflow_argv, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.fleet_desired_admission_workflow", decl_name: "fleet_desired_admission_build_step"), + authority: gunbc_cli_bin, + disposition: retained_open(justification: "fleet desired-state admission builds the gunbc binary; a product workflow outside the floor cut's boundary by that cut's own exclusion. Closes on: the native v2 binary answering the verbs the fleet workflows actually pass among the five the v1 clap surface declares (Compile, Test, Run, Converge, Serve), with a REFUSAL for any verb it does not answer -- a verb that silently forwards is the falsifier XL-5 lists, not the migration"), + ), + medium: WorkflowArgv, + subject: V1Cli, + discovered_by: producer_workflow_argv, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.fleet_desired_admission_workflow", decl_name: "fleet_desired_admission_decide_step"), + authority: gunbc_cli_bin, + disposition: retained_open(justification: "the decide step invokes `gunbc run` over the corpus to evaluate the admission. Same closing capability as the build step's row; a separate relation because the key is consumer x authority and this step depends on the RUN verb, not merely on the binary existing"), + ), + medium: WorkflowArgv, + subject: V1Cli, + discovered_by: producer_workflow_argv, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.fleet_converge_workflow", decl_name: "fleet_converge_build_job"), + authority: invoked_bins_row, + disposition: retained_open(justification: "the converge build job packs every bin this roster names; the roster names claim_executor and gunbc. Closes with the two CLI rows above; a separate relation because the consumer reaches the bins through a .dag roster row rather than through a literal, and gunbc.ci_release_bins records that this exact roster stranded fleet-converge for two days after FLOOR-Y when a member was removed without draining the row"), + ), + medium: DagArgvRow, + subject: V1HostedCiBinary, + discovered_by: producer_bin_roster_row, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.fleet_converge_workflow", decl_name: "fleet_converge_build_job"), + authority: declared_release_bins_row, + disposition: retained_open(justification: "the same build job packs every witness-declared release bin, all of which are v1-compiler bin targets. Closes on: every member of this roster having its own disposition here -- the roster is a population, and gunbc.ci_release_bins's own lesson is that removing a consumer and removing a member are different edits"), + ), + medium: DagArgvRow, + subject: V1HostedCiBinary, + discovered_by: producer_bin_roster_row, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.host_effect_codex_supervised_turn", decl_name: "host_effect_codex_supervised_turn_bin_name"), + authority: codex_session_bin, + disposition: retained_open(justification: "a PRODUCT integration, not a compiler consumer: the codex stdio session transport is a v1-compiler bin target whose subject has nothing to do with compiling .dag. Its disposition is genuinely open rather than assumed retired, and deleting it as CI cruft would be the deletion-inside-the-deletion-set blind spot the floor cut measured. Closes on: either a native successor for this transport or a retirement with the product owner's cause -- not on the compiler cutover"), + ), + medium: CargoBinTarget, + subject: V1HostedCiBinary, + discovered_by: producer_workflow_argv, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.generated_artifact_merge_driver", decl_name: "generated_artifact_merge_driver_repair_steps"), + authority: claim_executor_bin, + disposition: retired(reason: "the repair recipe names claim_executor --required-regen as the route to regenerate a conflicted src/v1 mirror; with the regeneration SUBJECT deleted the recipe has nothing to regenerate. This retires the RECIPE TEXT for the src/v1 population, not the driver: the driver survives for the surviving generated artifacts, and dropping it would drop the merge protection #7836 twice needed"), + ), + medium: GitHookScript, + subject: V1DagSource, + discovered_by: producer_git_hook, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "v1.compiler.workspace_members", decl_name: "workspace_members_region_begin_marker"), + authority: stage0_partition_rows, + disposition: retired(reason: "the workspace-member region writer is itself under src/v1 and consumes the partition rows to emit the generated member list; it is a consumer INSIDE the deletion set and cannot refuse when both go. Filed as Retire rather than omitted because the floor cut's first measured bound is exactly this class -- a consumer defined and consumed inside the deletion set leaves no diagnostic, so its retirement must be a row, not an absence"), + ), + medium: CargoManifestDependency, + subject: V1GeneratedStage0Mirror, + discovered_by: producer_cargo_manifest_graph, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "v1_compiler_tests.lib", decl_name: "helpers"), + authority: v1_compiler_crate_root, + disposition: retired(reason: "the src/v1/tests crate depends only on v1-compiler, with three features that exist to expose v1 internals to v1's own tests. No manifest outside src/v1 names it"), + ), + medium: CargoManifestDependency, + subject: V1CompilerCrate, + discovered_by: producer_cargo_manifest_graph, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.stage0_rust_source_lifecycle_scaffold", decl_name: "residue_stage0_core_lib_dissolution"), + authority: stage0_partition_rows, + disposition: retired(reason: "an ALREADY-DECLARED open authority contradiction, not a discovery of this census: src/v1/stage0_core/src/lib.rs is tracked on disk, absent from the partition rows and absent from the workspace member list, and the residue row's dissolution reads 'stage0_partition_crate_rows enrolls src/v1/stage0_core OR the crate deletes'. XL-5 satisfies the second arm. Recorded so the transaction is known to DISCHARGE that row rather than orphan it"), + ), + medium: CargoManifestDependency, + subject: V1GeneratedStage0Mirror, + discovered_by: producer_cargo_manifest_graph, + }, + { + boundary: v1cc_boundary( + consumer: decl_ref(module_path: "gunbc.stage0_rust_source_lifecycle_scaffold", decl_name: "stage0_partition_crate_rows_authority_ref"), + authority: stage0_partition_rows, + disposition: retired(reason: "the committed generated mirrors under src/v1 and the .gitattributes rows that route their merges are projections of src/v1 .dag authorities; with the authority deleted a mirror has no producer and is not a survivor to re-home. The .gitattributes rows go with their registry entries, the same motion #9663 performed for the js_site rows"), + ), + medium: CommittedGeneratedMirror, + subject: V1GeneratedStage0Mirror, + discovered_by: producer_generated_mirror, + }, + tsv_row(path_decl: "required_floor_disposition_path"), + tsv_row(path_decl: "expected_red_roster_join_path"), + tsv_row(path_decl: "long_home_storage_agreement_path"), + tsv_row(path_decl: "required_floor_claim_cost_path"), +] + +fn shim_consumer(path: String) -> V1UncitableConsumer { + { + item_key: path, + refusal_detail: "no rust_source_namespace_rows prefix claims this path, so no module path can be derived for it", + medium: RustUseEdge, + subject: V1RuntimeBridge, + disposition: retained_open(justification: "a hand-authored shim standing in for primitive arms the emitted v2 closure does not yet realize; the only Rust outside src/v1 that reaches the v1 runtime bridge. Closes on: the emitted v2 closure realizing those arms so the shim has nothing to bridge -- XL-0's arms-to-zero milestone AS EXECUTED, meaning the emitted crate compiles without a v1_rt path rather than merely cargo-checking with one"), + discovered_by: producer_rust_bridge_edge, + } +} + +data v1_uncitable_consumers: List = [ + shim_consumer(path: "dag/gunbc/instruments/self_host_03_normalize_shims/lib.rs"), + shim_consumer(path: "dag/gunbc/instruments/self_host_body_producer_shims/lib.rs"), + shim_consumer(path: "dag/gunbc/instruments/self_host_parse_engine_hooks_shims/lib.rs"), + shim_consumer(path: "dag/gunbc/instruments/self_host_use_site_verdict_shims/lib.rs"), +] + +// THE POPULATION THIS ROSTER CONSTITUTES TODAY, and it is deliberately not the Complete arm. Seven +// producers were run and none of them joins the others. Filing this as Complete would be the rung +// inflation DESIGN section 4b names as worse than sitting low, because the admission gate below +// reads this field and an inflated Complete would let the transaction execute against a population +// that was never closed. +data v1_consumer_population: ConsumerPopulation = PopulationMeasuredLowerBound { + rows: v1_consumers, + uncitable: v1_uncitable_consumers, + missing_basis: "seven per-medium sweeps, unjoined, plus four consumers the exact vocabulary cannot cite. Three named holes, each of which would produce a row this roster does not have: (1) no producer classifies the .dag argv rows -- 85 .dag files name a v1 binary in a string position and only the two ci_release_bins rosters were traced to a consumer; (2) the deletion-set blind spot the floor cut measured has one row here (workspace_members) and no instrument -- a consumer defined inside src/v1 and consumed inside src/v1 cannot refuse when both go, and only a per-deleted-file question finds the rest; (3) reachability is not measured for any row: every disposition above is a PRESENCE claim, and presence over-approximates demand, which is the reachability_read_as_occupancy class this repository rosters and XL-1 tripped on in its own first census.", +} + +// THE PROJECTION INTO THE EXACT CARRIER. When the population reaches Complete, this is the +// BoundaryCensus the RegisteredExactCut for cut-v1-interpreter is authored over; until then the +// projection exists so the shape is executed now rather than discovered at release, and so the +// consumer identities XL-3 consumes are the authority's BoundaryConsumer rather than a private row. +fn v1_boundary_census(rows: List) -> BoundaryCensus { + ConsumersEnumerated { consumers: rows |> map(r => r.boundary) } +} + +// REFUSAL ONE, in the direction a census is most likely to fail: something is reachable and no row +// disposes it. The discovered population is supplied by the CALLER rather than read from a field +// here, because a census that supplies its own denominator is asserting completeness by writing it +// down -- the change-detector shape DESIGN section 5 names, where automating the literal collapses +// the assertion to measure() == measure(). +fn v1_row_keys(rows: List) -> List { + rows |> map(r => v1_row_key(r: r)) +} + +fn v1_key_in(needle: String, xs: List) -> Bool { + xs |> any(x => x == needle) +} + +fn v1_consumers_undisposed(discovered: List, rows: List) -> List { + discovered |> filter(d => !v1_key_in(needle: d, xs: v1_row_keys(rows: rows))) +} + +fn v1_every_discovered_consumer_disposed(discovered: List, rows: List) -> Bool { + count(v1_consumers_undisposed(discovered: discovered, rows: rows)) == 0 +} + +// REFUSAL TWO, the opposite direction: a row names a relation the discovery population does not +// contain. This catches a roster going stale rather than short -- a consumer repaired upstream +// leaves a row behind, and a stale row is indistinguishable from a live one to every reader who is +// not re-running the producer. +fn v1_rows_naming_no_live_consumer(discovered: List, rows: List) -> List { + rows |> filter(r => !v1_key_in(needle: v1_row_key(r: r), xs: discovered)) +} + +fn v1_every_row_names_a_live_consumer(discovered: List, rows: List) -> Bool { + count(v1_rows_naming_no_live_consumer(discovered: discovered, rows: rows)) == 0 +} + +// REFUSAL THREE, the load-bearing one: A DISPOSITION CANNOT BE MADE TRUE BY EDITING IT. A row may +// CLAIM a successor authority; the claim holds only if that authority appears in a realized +// population supplied from outside this module. Without this arm, ReplacedByY is an author's +// intention typed into a field -- the tell DESIGN section 5 gives for validation standing where +// construction was available. +fn v1_claimed_successors(rows: List) -> List { + rows |> flat_map(r => consumer_disposition_successors(d: r.boundary.disposition)) +} + +fn v1_unrealized_successors(rows: List, realized: List) -> List { + v1_claimed_successors(rows: rows) |> filter(s => !v1_key_in(needle: s, xs: realized)) +} + +fn v1_every_claimed_successor_is_realized(rows: List, realized: List) -> Bool { + count(v1_unrealized_successors(rows: rows, realized: realized)) == 0 +} + +// THE BLOCKING COLUMN, derived rather than authored, over BOTH the citable rows and the uncitable +// ones. This is the number XL-5 reports upward; a filter over the roster rather than a literal, so +// it cannot be edited down without deleting a row -- and deleting a row is what refusal two catches. +fn v1_blocking_consumers(rows: List) -> List { + rows |> filter(r => consumer_disposition_blocks(d: r.boundary.disposition)) +} + +fn v1_blocking_uncitable(uncitable: List) -> List { + uncitable |> filter(u => consumer_disposition_blocks(d: u.disposition)) +} + +fn v1_blocking_consumer_count() -> Int { + count(v1_blocking_consumers(rows: v1_consumers)) + count(v1_blocking_uncitable(uncitable: v1_uncitable_consumers)) +} + +fn v1_consumer_member_count() -> Int { + count(v1_consumers) + count(v1_uncitable_consumers) +} + +// THE ADMISSION GATE FOR THE BANKRUPTCY TRANSACTION. All four conditions, and the first is the one +// a reader will be tempted to drop: a lower-bound population with an empty blocking column says +// nothing blocks AMONG WHAT WAS MEASURED, not the claim the transaction needs. Executing the +// cutover on that is the absorbing-fallback shape read backwards -- ignorance taken as an answer -- +// and it is why completeness is a field the gate reads rather than a sentence in a note. The +// fourth condition is that no uncitable consumer remains, since a consumer the vocabulary cannot +// spell is one the exact cut cannot disposition. +fn v1_bankruptcy_transaction_admitted(population: ConsumerPopulation, realized: List) -> Bool { + let rows = consumer_population_rows(p: population) + consumer_population_is_complete(p: population) + && count(v1_blocking_consumers(rows: rows)) == 0 + && count(consumer_population_uncitable(p: population)) == 0 + && v1_every_claimed_successor_is_realized(rows: rows, realized: realized) +} + +data v1_consumer_census_rung_note: String = "RUNG, at the honest grain, separated from what the roster claims about v1.\n\nTHE CLASS -- 'the cutover deletes a subject nothing succeeded' -- sits at MITIGATABLE today, and this carrier does not move it. Nothing refuses when a consumer is added to the tree; the roster is a hand sweep and an author who forgets to file a row leaves no trace.\n\nWHAT IS CONSTRUCTED, and it is the only rung claim made here: the relation is the authority's own BoundaryConsumer, so a row cannot name a consumer without naming what it consumes; a row has no constructor without a producer carrying a command and a revision; the blocking predicate is derived from the same two arms admit_replacement_cut_plan refuses on, so the blocking column here and the refusal there cannot disagree; and the successor claim is not self-satisfiable at all -- refusal three joins it against a population this module cannot write.\n\nWHAT IS NOT CONSTRUCTED, stated because the gap is the next lane's work rather than an omission: completeness. PopulationMeasuredLowerBound is the honest arm and the admission gate reads it, so the transaction refuses by construction today -- but nothing stops an author from writing PopulationMeasuredComplete over the same unjoined rows. That edit is the one way this carrier can lie, and it is exactly what the next-rung trigger closes." + +data v1_consumer_census_next_rung_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: the discovered consumer population is produced by ONE joined instrument over all eight media -- manifests, bin targets, workflow argv, .dag argv rows, Rust use edges, hook scripts, committed mirrors and serialized artifact paths -- so that adding a consumer in any medium appears in the census without an author remembering to file it, and PopulationMeasuredComplete becomes a fact the instrument establishes rather than a value an author types. NOT satisfied by an instrument covering some media however many rows it finds: a per-medium answer is indistinguishable from a joined one, so a partial join has the same blind spot as no join. NOT satisfied by adding rows by hand.") diff --git a/dag/gunbc/v1/v1_witness_census.dag b/dag/gunbc/v1/v1_witness_census.dag new file mode 100644 index 00000000000..73276cd2b95 --- /dev/null +++ b/dag/gunbc/v1/v1_witness_census.dag @@ -0,0 +1,229 @@ +module gunbc.v1_witness_census + +import std.types { List, String, NonEmptyStr, Bool, Int } +import std.decl_ref { DeclarationRef, decl_ref } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import gunbc.replacement_cut { EvidenceDisposition, ReenrollAgainstY, ReplaceEvidence, RetireEvidence } +import v2.workflow.required_floor { + RequiredFloorDisposition, Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedOutsideRequiredGate, DeclinedCostDebt +} + +// XL-5's SECOND DELIVERABLE: the wall that stops the bankruptcy transaction greening by LOSING +// SUBJECTS. It is a separate carrier from the consumer census because it answers a different +// question in the opposite direction. The consumer census asks what still reaches v1, and its +// success condition is an EMPTY population. This one asks what the v1-hosted floor currently +// establishes, and its success condition is a TOTAL ONE-TO-ONE ACCOUNTING -- an empty population +// here would mean every guarantee in the repository had been dropped. +// +// WHY THIS IS THE FAILURE MODE WORTH BUILDING A WALL FOR. Today every claim identity in this +// repository is executed inside a v1-hosted binary; both required lanes are claim_executor. So the +// cutover moves the ENTIRE claim corpus at once, and the cheapest possible green is a native fold +// that runs a subset and reports success. Nothing in a pass/fail summary distinguishes that from a +// complete run: DESIGN section 5 states the general form -- completeness is an identity join, not +// a count equality -- and a claim count is exactly the count-equality oracle it forbids. The floor +// cut measured the specific instance: 16 of 42 deleted witnesses there were peers dying with their +// subsystem, and the two that mattered were GUARDS deleted alongside what they constrained, which +// produced no artifact and which an artifact-keyed ledger was structurally blind to. +// +// TWO AXES, KEPT APART BY RULING (XL-N Manager, 2026-08-29). FLOOR STANDING is what the required +// floor's scheduler decided about a claim -- Planned, or one of the Declined arms -- and it is the +// authority's own RequiredFloorDisposition, imported rather than re-spelled. CUTOVER DISPOSITION +// is what XL-5 decides about the claim's future. A declined claim is not a retired claim: XL-1 +// measured that DeclinedLongModule is assigned by AUTHORED MODULE NAME, not by cost, and the corpus +// records long/-relocated witnesses that measured 192ms total against a 5000ms budget. So "floor +// declined" is a fact the join carries and the disposition may not read as evidence. + +data v1_claim_disposition_note: String = "THE THREE ARMS THE RULING NAMES, each carrying what makes it checkable rather than the assertion that it holds, and there is no fourth. An undecided claim at cutover time is a lost subject wearing a plan; the population type below is where not-yet-measured is spelled, at the grain of the whole roster rather than per row.\n\nRetired carries the deleted subject and the evidence the deletion was measured, not merely performed. Deleting the OLD RUNNER does not retire a claim -- the claim's subject is what it asserts about, and the runner was only where it executed. This is the arm that removes evidence, so it is the arm that must be hardest to file.\n\nReplacedByStronger carries the replacement identity, the COVERING RELATION stated explicitly, and an EXECUTED red proving the replacement detects the class the old claim detected. 'Stronger' is the word a cutover is most tempted to use for 'different', and an unstated strengthening is how a required subject leaves the tree wearing an upgrade. The red control is the entire content of the arm: DESIGN section 4b says to ask whether a check's RED is authorable before writing the check, and a replacement that cannot go red on the old class is a decoration cited as coverage.\n\nStillRequired carries the surviving subject and the native identity it enters the roster under -- regardless of floor cost policy, per the ruling. This is the arm XL-1 joins into the native implementation roster, so its target identity is a DeclarationRef and not a description.\n\nEACH ARM PROJECTS ONTO gunbc.replacement_cut EvidenceDisposition -- Retired to RetireEvidence, ReplacedByStronger to ReplaceEvidence, StillRequired to ReenrollAgainstY -- so the exact cut's evidence rows are DERIVED from this census rather than authored beside it. The arms here are strictly richer than the authority's (an executed red, a covering relation, a typed target) because the authority's rows are what an admission reads and these are what a reviewer must be able to audit; the projection is lossy in the direction that is safe." + +type ClaimCutoverDisposition + = Retired { deleted_subject: DeclarationRef, evidence: String } + | ReplacedByStronger { replacement: DeclarationRef, covering_relation: String, executed_red: DeclarationRef } + | StillRequired { surviving_subject: DeclarationRef, native_identity: DeclarationRef } + +fn claim_disposition_key(d: ClaimCutoverDisposition) -> String { + match d { + Retired { deleted_subject: _, evidence: _ } => "retired" + ReplacedByStronger { replacement: _, covering_relation: _, executed_red: _ } => "replaced-by-stronger" + StillRequired { surviving_subject: _, native_identity: _ } => "still-required" + } +} + +fn v1_claim_identity_key(r: DeclarationRef) -> String { + concat(concat(r.module_path as String, "::"), r.decl_name as String) +} + +fn claim_disposition_native_targets(d: ClaimCutoverDisposition) -> List { + match d { + Retired { deleted_subject: _, evidence: _ } => [] + ReplacedByStronger { replacement: r, covering_relation: _, executed_red: _ } => [r] + StillRequired { surviving_subject: _, native_identity: n } => [n] + } +} + +fn claim_disposition_red_controls(d: ClaimCutoverDisposition) -> List { + match d { + Retired { deleted_subject: _, evidence: _ } => [] + ReplacedByStronger { replacement: _, covering_relation: _, executed_red: c } => [c] + StillRequired { surviving_subject: _, native_identity: _ } => [] + } +} + +fn v1wc_nes(s: String) -> NonEmptyStr { s as NonEmptyStr } + +fn claim_cutover_evidence_disposition(identity: DeclarationRef, d: ClaimCutoverDisposition) -> EvidenceDisposition { + match d { + Retired { deleted_subject: s, evidence: e } => + RetireEvidence { evidence: v1wc_nes(s: v1_claim_identity_key(r: identity)), retired_subject: v1wc_nes(s: v1_claim_identity_key(r: s)), retirement_reason: v1wc_nes(s: e) } + ReplacedByStronger { replacement: r, covering_relation: _, executed_red: _ } => + ReplaceEvidence { old_evidence: v1wc_nes(s: v1_claim_identity_key(r: identity)), new_evidence: v1wc_nes(s: v1_claim_identity_key(r: r)) } + StillRequired { surviving_subject: s, native_identity: _ } => + ReenrollAgainstY { evidence: v1wc_nes(s: v1_claim_identity_key(r: identity)), surviving_claim: v1wc_nes(s: v1_claim_identity_key(r: s)) } + } +} + +type V1ClaimCutoverRow { + pre_cutover_identity: DeclarationRef + floor_standing: RequiredFloorDisposition + disposition: ClaimCutoverDisposition +} + +fn floor_standing_is_fixture_member(s: RequiredFloorDisposition) -> Bool { + match s { + Planned => false + DeclinedLongModule { matched_prefix: _ } => false + DeclinedFixtureMember { matched_prefix: _ } => true + DeclinedOutsideRequiredGate => false + DeclinedCostDebt => false + } +} + +data v1_claim_population_note: String = "THE PRE-CUTOVER ROSTER IS SUPPLIED, NEVER AUTHORED HERE, and that is the difference between this carrier and a list of claims somebody remembered. The roster's authority is the required floor's own discovery -- the identities the floor run executes or declines, joined by XL-1 with each one's RequiredFloorDisposition -- and this module joins against it. A census that wrote down its own denominator would be satisfiable by shortening the denominator, which is precisely the loss it exists to refuse.\n\nTHE ROSTER IS UNMEASURED IN THIS CARRIER TODAY, filed as Unmeasured rather than as an empty Complete. Reading it requires a full-tree floor run, which XL-5 is not released to perform; the fixtures beside this module drive every assertion over CONTROLLED populations, which is what makes the assertions executable now instead of aspirational. Unmeasured and Complete both carry zero rows and answer the conservation gate OPPOSITELY -- the distinction a bare List cannot make and a note beside it cannot enforce." + +type ClaimPopulation + = ClaimRosterComplete { rows: List, roster_producer: String } + | ClaimRosterUnmeasured { reason: String, what_would_settle_it: String } + +fn claim_population_rows(p: ClaimPopulation) -> List { + match p { + ClaimRosterComplete { rows: r, roster_producer: _ } => r + ClaimRosterUnmeasured { reason: _, what_would_settle_it: _ } => [] + } +} + +fn claim_population_is_complete(p: ClaimPopulation) -> Bool { + match p { + ClaimRosterComplete { rows: _, roster_producer: _ } => true + ClaimRosterUnmeasured { reason: _, what_would_settle_it: _ } => false + } +} + +data v1_claim_live_population: ClaimPopulation = ClaimRosterUnmeasured { + reason: "the pre-cutover claim roster is the set of identities the required floor executes or declines, joined with each one's floor standing; reading it means a full-tree floor run. XL-5 is model-work until its gate releases, so the roster is honestly absent rather than estimated. An estimate here would be worse than an absence: the conservation gate reads this field, and a guessed roster would produce a join that passes against a denominator nobody measured", + what_would_settle_it: "XL-1's joined claim population (full-tree floor claim identities x claim_scope_for x RequiredFloorDisposition) at a named run and revision, landed here as ClaimRosterComplete with that run named as roster_producer, and one disposition per row authored by XL-5", +} + +fn v1_claim_row_keys(rows: List) -> List { + rows |> map(r => v1_claim_identity_key(r: r.pre_cutover_identity)) +} + +fn v1_claim_key_in(needle: String, xs: List) -> Bool { + xs |> any(x => x == needle) +} + +// THE CONSERVATION WALL, IN FIVE DIRECTIONS, AT IDENTITY GRAIN. +// +// Direction one: every identity the pre-cutover roster contains has exactly one row. This is the +// one that catches a lost subject -- a claim that simply stops being executed by the native fold +// leaves no artifact, produces no red, and shortens no number a reader is looking at. +fn v1_claims_unaccounted(roster: List, rows: List) -> List { + roster |> filter(id => !v1_claim_key_in(needle: id, xs: v1_claim_row_keys(rows: rows))) +} + +fn v1_every_claim_accounted(roster: List, rows: List) -> Bool { + count(v1_claims_unaccounted(roster: roster, rows: rows)) == 0 +} + +// Direction two: every row names an identity the roster contains. A row for a claim that does not +// exist pre-cutover is a fabricated subject, and it inflates the accounting in the one place a +// reader checks -- the same row count, with a real subject swapped for an invented one. +fn v1_claim_rows_outside_roster(roster: List, rows: List) -> List { + rows |> filter(r => !v1_claim_key_in(needle: v1_claim_identity_key(r: r.pre_cutover_identity), xs: roster)) +} + +fn v1_every_claim_row_is_in_roster(roster: List, rows: List) -> Bool { + count(v1_claim_rows_outside_roster(roster: roster, rows: rows)) == 0 +} + +// Direction three, the one a count-based accounting cannot express at all: a surviving claim must +// land on a DISTINCT native identity. Two pre-cutover claims both mapped onto one native identity +// is a merge, and a merge is a loss wearing a port -- the accounting stays total, every row has a +// disposition, and one subject has quietly stopped being checked. This is why the join is on +// identities rather than on counts. +fn v1_claim_native_target_keys(rows: List) -> List { + rows |> flat_map(r => claim_disposition_native_targets(d: r.disposition)) |> map(n => v1_claim_identity_key(r: n)) +} + +fn v1_claim_key_occurrences(needle: String, xs: List) -> Int { + count(xs |> filter(x => x == needle)) +} + +fn v1_claim_native_targets_are_distinct(rows: List) -> Bool { + let targets = v1_claim_native_target_keys(rows: rows) + targets |> all(t => v1_claim_key_occurrences(needle: t, xs: targets) == 1) +} + +// Direction four: a replacement's executed red must be a DIFFERENT declaration from both the old +// claim and the replacement. A row naming the replacement, or the old claim, as its own red control +// makes the strongest claim in this census -- 'the replacement detects the old class' -- true by +// writing it, and it is one keystroke away from the honest form. +fn v1_claim_red_control_is_distinct(row: V1ClaimCutoverRow) -> Bool { + let own = v1_claim_identity_key(r: row.pre_cutover_identity) + let targets = v1_claim_native_target_keys(rows: [row]) + claim_disposition_red_controls(d: row.disposition) |> all(c => + v1_claim_identity_key(r: c) != own && !v1_claim_key_in(needle: v1_claim_identity_key(r: c), xs: targets) + ) +} + +fn v1_every_claim_red_control_is_distinct(rows: List) -> Bool { + rows |> all(r => v1_claim_red_control_is_distinct(row: r)) +} + +// Direction five, from the ruling: a FIXTURE OR SUPPORT MODULE IS NOT A CLAIM AND TAKES NO +// DISPOSITION. The floor already names that population structurally -- DeclinedFixtureMember is +// assigned by the module's relation to claims, not by anything about its cost -- so a row carrying +// that standing is a support module folded into the accounting to close a count, and it is refused +// rather than dispositioned. The exclusion is by structural relation, never by disposition. +fn v1_claim_rows_that_are_fixture_members(rows: List) -> List { + rows |> filter(r => floor_standing_is_fixture_member(s: r.floor_standing)) +} + +fn v1_no_fixture_member_carries_a_disposition(rows: List) -> Bool { + count(v1_claim_rows_that_are_fixture_members(rows: rows)) == 0 +} + +// THE GATE. Conservation is all five directions over a COMPLETE roster; any of them dropped is a +// different and weaker claim, and the completeness arm is first for the same reason it is first in +// the consumer census -- a join over an unmeasured roster is vacuously total. +fn v1_claim_conservation_holds(population: ClaimPopulation, roster: List) -> Bool { + let rows = claim_population_rows(p: population) + claim_population_is_complete(p: population) + && v1_every_claim_accounted(roster: roster, rows: rows) + && v1_every_claim_row_is_in_roster(roster: roster, rows: rows) + && v1_claim_native_targets_are_distinct(rows: rows) + && v1_every_claim_red_control_is_distinct(rows: rows) + && v1_no_fixture_member_carries_a_disposition(rows: rows) +} + +// THE NATIVE ROSTER XL-1 JOINS: every StillRequired and ReplacedByStronger target, regardless of +// floor standing. Derived, so it cannot drift from the dispositions that justify it. +fn v1_native_roster(rows: List) -> List { + rows |> flat_map(r => claim_disposition_native_targets(d: r.disposition)) +} + +fn v1_claim_evidence_rows(rows: List) -> List { + rows |> map(r => claim_cutover_evidence_disposition(identity: r.pre_cutover_identity, d: r.disposition)) +} + +data v1_claim_census_rung_note: String = "RUNG. The CLASS -- 'the cutover drops a claim subject and greens' -- sits at MITIGATABLE on the live tree, because the live roster is unmeasured and no gate consumes this carrier yet. Saying that first matters: a conservation wall beside an unmeasured roster is exactly the artifact a reader mistakes for conservation.\n\nWHAT IS CONSTRUCTED: the three-arm disposition has no undecided variant, so a claim cannot be carried through the cutover without an answer; a replacement has no constructor without an executed red and a covering relation; a retirement has none without a named deleted subject and its evidence; a surviving claim has none without a typed native identity; floor standing is the floor's own type, so a standing the floor cannot assign cannot be written here; and the gate cannot be satisfied by an unmeasured roster, because completeness is a field it reads rather than an assumption it makes.\n\nWHAT IS VALIDATED RATHER THAN CONSTRUCTED, and is therefore weaker: distinctness of native targets, distinctness of red controls, and the absence of fixture-member rows are folds over a List, so all three bad states are writable and are caught by an executing witness rather than being unwritable. A Set-keyed carrier would construct the first; nothing available constructs the second, since 'different enough to discriminate' is not decidable from the reference alone -- which is why that arm is a distinctness check and is described as one rather than as proof the control discriminates." + +data v1_claim_census_next_rung_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: the required gate consumes v1_claim_conservation_holds against the roster the floor run itself emits, so a claim identity that stops being executed refuses the merge rather than shortening a summary line. The capability named is a required gate whose denominator is produced by the run being gated -- NOT the landing of a roster file, and NOT this carrier being imported by a test: a roster committed beside the run is the second representation whose drift this census exists to refuse, and an importing test that supplies its own roster proves only that the join function works.") diff --git a/dag/test/claim/v1_consumer_census_witness_test.dag b/dag/test/claim/v1_consumer_census_witness_test.dag new file mode 100644 index 00000000000..217ade5216c --- /dev/null +++ b/dag/test/claim/v1_consumer_census_witness_test.dag @@ -0,0 +1,111 @@ +module test.claim.v1_consumer_census_witness_test + +import std.types { Bool } +import gunbc.replacement_cut { BoundaryCensus, ConsumersEnumerated, BoundaryDeclaredEmpty } +import gunbc.v1_consumer_census { + v1_consumers, v1_uncitable_consumers, v1_consumer_population, + v1_every_discovered_consumer_disposed, v1_every_row_names_a_live_consumer, v1_every_claimed_successor_is_realized, + v1_bankruptcy_transaction_admitted, v1_blocking_consumer_count, v1_consumer_member_count, + v1_boundary_census, consumer_population_is_complete, consumer_population_rows, consumer_population_uncitable +} +import test.fixture.v1_consumer_census.specimens { + clean_rows, clean_discovered, clean_realized, clean_population, + planted_undisposed_discovered, planted_stale_discovered, + planted_unrealized_rows, planted_unrealized_population, + planted_lower_bound_population, planted_unmeasured_population, + planted_blocking_population, planted_covered_unrealized_rows, planted_covered_unrealized_population +} + +// WHAT THIS WITNESS ESTABLISHES, AND WHAT IT DOES NOT. +// +// It does NOT measure the repository. The live roster in gunbc.v1_consumer_census is a hand sweep +// over seven per-medium producers, and no assertion here would move if a new v1 consumer were +// authored tomorrow. Saying that first is the point: a green witness beside a census is exactly the +// artifact a reader mistakes for 'the census is verified'. +// +// What it DOES establish is that the census's refusals DISCRIMINATE -- each goes red on the state +// it exists to catch, and green on the same fixture with that one state removed. Every assertion +// below is therefore a PAIR, and the green half is not decoration: a predicate that returned false +// unconditionally would pass every red-only probe in this file, the positive-control-on-the-plant +// gap this repository has already filed twice. +// +// NO ASSERTION COMPARES ANYTHING TO A LITERAL COUNT. Every number is a fold over a population +// compared to another fold over the same population, so adding a row cannot make this file stale +// and no assertion can be silenced by editing a number. + +fn undisposed_consumer_is_caught() -> Bool { + v1_every_discovered_consumer_disposed(discovered: clean_discovered, rows: clean_rows) + && !v1_every_discovered_consumer_disposed(discovered: planted_undisposed_discovered, rows: clean_rows) +} + +fn stale_row_is_caught() -> Bool { + v1_every_row_names_a_live_consumer(discovered: clean_discovered, rows: clean_rows) + && !v1_every_row_names_a_live_consumer(discovered: planted_stale_discovered, rows: clean_rows) +} + +// A DISPOSITION CANNOT BE MADE TRUE BY EDITING IT, through BOTH arms that carry a successor: the +// ReplacedByY authority and the Covered coverage claim. A refusal that reached only one of them +// would leave the other as the place an author types a name nothing realizes. +fn unrealized_successor_claim_is_caught() -> Bool { + v1_every_claimed_successor_is_realized(rows: clean_rows, realized: clean_realized) + && !v1_every_claimed_successor_is_realized(rows: planted_unrealized_rows, realized: clean_realized) + && !v1_every_claimed_successor_is_realized(rows: planted_covered_unrealized_rows, realized: clean_realized) +} + +// THE ADMISSION GATE REFUSES AN UNMEASURED POPULATION AND A LOWER-BOUND ONE, and admits the +// complete one. The populations differ ONLY in the completeness arm -- same rows, same successors. +fn admission_reads_completeness() -> Bool { + v1_bankruptcy_transaction_admitted(population: clean_population, realized: clean_realized) + && !v1_bankruptcy_transaction_admitted(population: planted_lower_bound_population, realized: clean_realized) + && !v1_bankruptcy_transaction_admitted(population: planted_unmeasured_population, realized: clean_realized) +} + +fn admission_refuses_a_blocking_consumer() -> Bool { + !v1_bankruptcy_transaction_admitted(population: planted_blocking_population, realized: clean_realized) + && consumer_population_is_complete(p: planted_blocking_population) +} + +fn admission_refuses_an_unrealized_successor() -> Bool { + !v1_bankruptcy_transaction_admitted(population: planted_unrealized_population, realized: clean_realized) + && !v1_bankruptcy_transaction_admitted(population: planted_covered_unrealized_population, realized: clean_realized) + && consumer_population_is_complete(p: planted_unrealized_population) +} + +// THE PROJECTION INTO THE EXACT CARRIER ENUMERATES EXACTLY THE ROWS IT WAS GIVEN, and never the +// declared-empty arm: a census with rows that projected to BoundaryDeclaredEmpty would hand the +// exact cut a clean boundary over a population it was told about. +fn boundary_census_enumerates_the_rows() -> Bool { + match v1_boundary_census(rows: clean_rows) { + ConsumersEnumerated { consumers: cs } => count(cs) == count(clean_rows) + BoundaryDeclaredEmpty { basis: _ } => false + } +} + +// THE LIVE TREE REFUSES, AND FOR THE REASONS THE CENSUS RECORDS. Stated as a conjunction because +// 'the gate is false' is also what a broken gate returns: the population is a lower bound AND there +// is at least one blocking consumer AND not every consumer blocks AND the uncitable list is +// non-empty -- four independent facts whose conjunction is what 'XL-5 has not run yet' means. +fn the_live_transaction_refuses_for_recorded_reasons() -> Bool { + !consumer_population_is_complete(p: v1_consumer_population) + && v1_blocking_consumer_count() > 0 + && v1_blocking_consumer_count() < v1_consumer_member_count() + && count(consumer_population_uncitable(p: v1_consumer_population)) > 0 +} + +// THE ROSTER AND THE POPULATION NAME ONE LIST. Two declarations naming one list can disagree in +// exactly one way -- an author filing a row and forgetting the population -- which would leave a +// consumer recorded and unread by the gate. +fn the_live_population_carries_the_whole_roster() -> Bool { + count(v1_consumers) == count(consumer_population_rows(p: v1_consumer_population)) + && count(v1_uncitable_consumers) == count(consumer_population_uncitable(p: v1_consumer_population)) +} + +test fn consumer_census_catches_an_undisposed_consumer() -> Bool { undisposed_consumer_is_caught() } +test fn consumer_census_catches_a_stale_row() -> Bool { stale_row_is_caught() } +test fn consumer_census_catches_an_unrealized_successor_claim() -> Bool { unrealized_successor_claim_is_caught() } +test fn consumer_census_admission_reads_completeness() -> Bool { admission_reads_completeness() } +test fn consumer_census_admission_refuses_a_blocking_consumer() -> Bool { admission_refuses_a_blocking_consumer() } +test fn consumer_census_admission_refuses_an_unrealized_successor() -> Bool { admission_refuses_an_unrealized_successor() } +test fn consumer_census_boundary_census_enumerates_the_rows() -> Bool { boundary_census_enumerates_the_rows() } +test fn consumer_census_live_transaction_refuses_for_recorded_reasons() -> Bool { the_live_transaction_refuses_for_recorded_reasons() } +test fn consumer_census_live_population_carries_the_whole_roster() -> Bool { the_live_population_carries_the_whole_roster() } diff --git a/dag/test/claim/v1_witness_census_witness_test.dag b/dag/test/claim/v1_witness_census_witness_test.dag new file mode 100644 index 00000000000..0afd15e68dc --- /dev/null +++ b/dag/test/claim/v1_witness_census_witness_test.dag @@ -0,0 +1,123 @@ +module test.claim.v1_witness_census_witness_test + +import std.types { Bool } +import gunbc.replacement_cut { EvidenceDisposition, ReenrollAgainstY, ReplaceEvidence, RetireEvidence, EvidenceUndecided } +import gunbc.v1_witness_census { + v1_claim_live_population, + v1_every_claim_accounted, v1_every_claim_row_is_in_roster, v1_claim_native_targets_are_distinct, + v1_every_claim_red_control_is_distinct, v1_no_fixture_member_carries_a_disposition, + v1_claim_conservation_holds, v1_native_roster, v1_claim_evidence_rows, + claim_population_is_complete, claim_population_rows +} +import test.fixture.v1_witness_census.specimens { + clean_rows, clean_roster, clean_population, + planted_unaccounted_roster, + planted_fabricated_rows, planted_fabricated_roster, planted_fabricated_population, + planted_merged_rows, planted_merged_roster, planted_merged_population, + planted_self_control_rows, planted_self_control_roster, planted_self_control_population, + planted_fixture_member_rows, planted_fixture_member_roster, planted_fixture_member_population, + planted_unmeasured_population +} + +// WHAT THIS WITNESS ESTABLISHES. Not that the repository's claims are conserved -- the live roster +// is unmeasured, and this file says so in its last assertion rather than hiding it. What it +// establishes is that the conservation wall DISCRIMINATES in all five directions, each against a +// planted loss and a positive control on the same plant. + +fn lost_subject_is_caught() -> Bool { + v1_every_claim_accounted(roster: clean_roster, rows: clean_rows) + && !v1_every_claim_accounted(roster: planted_unaccounted_roster, rows: clean_rows) +} + +fn fabricated_subject_is_caught() -> Bool { + v1_every_claim_row_is_in_roster(roster: clean_roster, rows: clean_rows) + && !v1_every_claim_row_is_in_roster(roster: planted_fabricated_roster, rows: planted_fabricated_rows) +} + +fn merged_target_is_caught() -> Bool { + v1_claim_native_targets_are_distinct(rows: clean_rows) + && !v1_claim_native_targets_are_distinct(rows: planted_merged_rows) +} + +fn self_referential_red_control_is_caught() -> Bool { + v1_every_claim_red_control_is_distinct(rows: clean_rows) + && !v1_every_claim_red_control_is_distinct(rows: planted_self_control_rows) +} + +fn fixture_member_with_a_disposition_is_caught() -> Bool { + v1_no_fixture_member_carries_a_disposition(rows: clean_rows) + && !v1_no_fixture_member_carries_a_disposition(rows: planted_fixture_member_rows) +} + +// THE GATE HOLDS OVER THE CLEAN ACCOUNTING AND REFUSES EACH PLANT THROUGH THE WHOLE FUNCTION, not +// only through the direction that catches it. A direction that discriminates in isolation and is +// then dropped from the conjunction is a wall with a door in it. +fn the_gate_refuses_every_plant() -> Bool { + v1_claim_conservation_holds(population: clean_population, roster: clean_roster) + && !v1_claim_conservation_holds(population: clean_population, roster: planted_unaccounted_roster) + && !v1_claim_conservation_holds(population: planted_fabricated_population, roster: planted_fabricated_roster) + && !v1_claim_conservation_holds(population: planted_merged_population, roster: planted_merged_roster) + && !v1_claim_conservation_holds(population: planted_self_control_population, roster: planted_self_control_roster) + && !v1_claim_conservation_holds(population: planted_fixture_member_population, roster: planted_fixture_member_roster) +} + +fn the_gate_refuses_an_unmeasured_roster() -> Bool { + !v1_claim_conservation_holds(population: planted_unmeasured_population, roster: []) + && count(claim_population_rows(p: planted_unmeasured_population)) == 0 +} + +// THE NATIVE ROSTER IS EXACTLY THE SURVIVING AND REPLACING TARGETS: over the clean accounting, two +// of three rows survive into it and the retired one does not. Derived from the same dispositions +// the gate reads, so it cannot be curated apart from them. +fn the_native_roster_is_derived() -> Bool { + count(v1_native_roster(rows: clean_rows)) == count(clean_rows) - 1 + && count(v1_native_roster(rows: planted_merged_rows)) == count(planted_merged_rows) +} + +fn evidence_is_reenroll(e: EvidenceDisposition) -> Bool { + match e { + ReenrollAgainstY { evidence: _, surviving_claim: _ } => true + ReplaceEvidence { old_evidence: _, new_evidence: _ } => false + RetireEvidence { evidence: _, retired_subject: _, retirement_reason: _ } => false + EvidenceUndecided { evidence: _ } => false + } +} + +fn evidence_is_undecided(e: EvidenceDisposition) -> Bool { + match e { + ReenrollAgainstY { evidence: _, surviving_claim: _ } => false + ReplaceEvidence { old_evidence: _, new_evidence: _ } => false + RetireEvidence { evidence: _, retired_subject: _, retirement_reason: _ } => false + EvidenceUndecided { evidence: _ } => true + } +} + +// THE PROJECTION INTO THE EXACT CARRIER IS TOTAL AND NEVER UNDECIDED: three rows in, three +// evidence rows out, exactly one of them ReenrollAgainstY, and none EvidenceUndecided -- because +// this census has no undecided arm to project from, and a projection that manufactured one would +// hand the exact cut an open decision this census already closed. +fn the_evidence_projection_is_total() -> Bool { + let rows = v1_claim_evidence_rows(rows: clean_rows) + count(rows) == count(clean_rows) + && count(rows |> filter(e => evidence_is_reenroll(e: e))) == 1 + && count(rows |> filter(e => evidence_is_undecided(e: e))) == 0 +} + +// THE LIVE POPULATION IS HONESTLY UNMEASURED. The one assertion about the real tree, and it asserts +// the census's own admission rather than a result. If someone lands a ClaimRosterComplete here +// without a floor run producing it, this goes red -- the correct response to a roster typed in. +fn the_live_roster_is_declared_unmeasured() -> Bool { + !claim_population_is_complete(p: v1_claim_live_population) + && !v1_claim_conservation_holds(population: v1_claim_live_population, roster: []) +} + +test fn witness_census_catches_a_lost_subject() -> Bool { lost_subject_is_caught() } +test fn witness_census_catches_a_fabricated_subject() -> Bool { fabricated_subject_is_caught() } +test fn witness_census_catches_a_merged_target() -> Bool { merged_target_is_caught() } +test fn witness_census_catches_a_self_referential_red_control() -> Bool { self_referential_red_control_is_caught() } +test fn witness_census_catches_a_fixture_member_with_a_disposition() -> Bool { fixture_member_with_a_disposition_is_caught() } +test fn witness_census_gate_refuses_every_plant() -> Bool { the_gate_refuses_every_plant() } +test fn witness_census_gate_refuses_an_unmeasured_roster() -> Bool { the_gate_refuses_an_unmeasured_roster() } +test fn witness_census_native_roster_is_derived() -> Bool { the_native_roster_is_derived() } +test fn witness_census_evidence_projection_is_total() -> Bool { the_evidence_projection_is_total() } +test fn witness_census_live_roster_is_declared_unmeasured() -> Bool { the_live_roster_is_declared_unmeasured() } diff --git a/dag/test/fixture/v1_consumer_census/specimens.dag b/dag/test/fixture/v1_consumer_census/specimens.dag new file mode 100644 index 00000000000..efb47c30bab --- /dev/null +++ b/dag/test/fixture/v1_consumer_census/specimens.dag @@ -0,0 +1,129 @@ +module test.fixture.v1_consumer_census.specimens + +import std.types { List, String, NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.replacement_cut { BoundaryConsumer, ConsumerDisposition, RetainSameContract, ReplacedByY, Retire, Covered, CoverageOpen } +import gunbc.v1_consumer_census { + V1ConsumerRow, V1UncitableConsumer, ConsumerPopulation, DiscoveryProducer, discovery_producer, + PopulationMeasuredComplete, PopulationMeasuredLowerBound, PopulationUnmeasured, + WorkflowArgv, RustUseEdge, V1HostedCiBinary, V1RuntimeBridge, V1CompilerCrate +} + +// CONTROLLED POPULATIONS FOR THE CONSUMER CENSUS'S REFUSALS. Every assertion in the paired witness +// runs TWICE: once over the clean population, which must hold, and once over a population carrying +// exactly one planted violation, which must not. Both halves are load-bearing and the clean half is +// the one most often skipped -- a planted red with no positive control on the same plant proves the +// assertion can fail, never that it fails FOR THE PLANTED REASON. +// +// WHY A FIXTURE AND NOT THE LIVE ROSTER. The live roster is honestly PopulationMeasuredLowerBound +// with blocking rows, so it makes the admission gate false today -- and an assertion that reads +// false on the live tree cannot tell 'the gate refuses correctly' from 'the gate is stuck off'. The +// fixture supplies the ADMITTED case, which exists nowhere in this repository yet and has no other +// way to be executed before the cutover. DESIGN section 4b: a state unrepresentable in the accepted +// corpus may still be representable as source handed to the compiler by a fixture, and where it +// is, declining the evidence is specification-without-execution. + +fn v1cc_fixture_nes(s: String) -> NonEmptyStr { s as NonEmptyStr } + +data fixture_producer: DiscoveryProducer = discovery_producer( + instrument: "hand-authored fixture; no tree was measured", + command: "none -- this row is a controlled specimen and must never be read as a live observation", + source_revision: "fixture", +) + +data consumer_one: DeclarationRef = decl_ref(module_path: "test.fixture.consumer", decl_name: "one") +data consumer_two: DeclarationRef = decl_ref(module_path: "test.fixture.consumer", decl_name: "two") +data old_authority: DeclarationRef = decl_ref(module_path: "test.fixture.old_root", decl_name: "authority") + +data fixture_native_successor: String = "test.fixture.native successor_target" +data fixture_unrealized_successor: String = "test.fixture.native successor_that_was_never_built" + +fn v1cc_fixture_row(consumer: DeclarationRef, disposition: ConsumerDisposition) -> V1ConsumerRow { + { + boundary: BoundaryConsumer { consumer: consumer, consumed_old_authority: old_authority, disposition: disposition }, + medium: WorkflowArgv, + subject: V1HostedCiBinary, + discovered_by: fixture_producer, + } +} + +// THE CLEAN ROSTER: two consumers, both discharged, no blocking row, every successor realized. +data clean_rows: List = [ + v1cc_fixture_row(consumer: consumer_one, disposition: ReplacedByY { new_authority: v1cc_fixture_nes(s: fixture_native_successor) }), + v1cc_fixture_row(consumer: consumer_two, disposition: Retire { reason: v1cc_fixture_nes(s: "controlled specimen: the fixture declares no other consumer of this subject") }), +] + +data clean_discovered: List = [ + "test.fixture.consumer.one -> test.fixture.old_root.authority", + "test.fixture.consumer.two -> test.fixture.old_root.authority", +] + +data clean_realized: List = [ fixture_native_successor ] + +data clean_population: ConsumerPopulation = PopulationMeasuredComplete { + rows: clean_rows, + joined_media: [ WorkflowArgv, RustUseEdge ], +} + +// PLANT ONE -- a discovered relation with no row. The roster is unchanged; the discovery population +// gains a third relation. This is the shape of the real failure: nobody edits the census, the tree +// grows a consumer, and the census cannot notice. +data planted_undisposed_discovered: List = [ + "test.fixture.consumer.one -> test.fixture.old_root.authority", + "test.fixture.consumer.two -> test.fixture.old_root.authority", + "test.fixture.consumer.three -> test.fixture.old_root.authority", +] + +// PLANT TWO -- a row naming a relation the discovery population does not contain. +data planted_stale_discovered: List = [ + "test.fixture.consumer.one -> test.fixture.old_root.authority", +] + +// PLANT THREE -- a successor claimed and never built. The row is well-formed; the only thing wrong +// is that the authority it names is absent from the realized population, a fact this module cannot +// write. This is the plant that proves a disposition cannot be made true by editing it. +data planted_unrealized_rows: List = [ + v1cc_fixture_row(consumer: consumer_one, disposition: ReplacedByY { new_authority: v1cc_fixture_nes(s: fixture_unrealized_successor) }), +] + +data planted_unrealized_population: ConsumerPopulation = PopulationMeasuredComplete { + rows: planted_unrealized_rows, + joined_media: [ WorkflowArgv ], +} + +// PLANT FOUR -- the same clean rows, filed as a LOWER BOUND with nothing uncitable. Only the +// completeness arm differs; the gate must refuse. This is the plant that distinguishes 'nothing +// blocks' from 'nothing blocks among what was measured'. +data planted_lower_bound_population: ConsumerPopulation = PopulationMeasuredLowerBound { + rows: clean_rows, + uncitable: [], + missing_basis: "controlled specimen: the rows are the clean ones and only the completeness arm differs", +} + +// PLANT FIVE -- an unmeasured population. Zero rows, zero blocking rows, and the gate must refuse. +data planted_unmeasured_population: ConsumerPopulation = PopulationUnmeasured { + reason: "controlled specimen: nothing was measured", +} + +// PLANT SIX -- one retained consumer with CoverageOpen inside an otherwise complete, fully realized +// population. The blocking arm exercised independently of the completeness arm. +data planted_blocking_rows: List = [ + v1cc_fixture_row(consumer: consumer_one, disposition: RetainSameContract { justification: v1cc_fixture_nes(s: "controlled specimen: a creditor that has not been paid"), coverage: CoverageOpen }), +] + +data planted_blocking_population: ConsumerPopulation = PopulationMeasuredComplete { + rows: planted_blocking_rows, + joined_media: [ WorkflowArgv ], +} + +// PLANT SEVEN -- a retained consumer whose coverage IS claimed, so it does not block, but the +// covering authority is not realized. Coverage is a successor claim too, and refusal three must +// reach it through the Covered arm and not only through ReplacedByY. +data planted_covered_unrealized_rows: List = [ + v1cc_fixture_row(consumer: consumer_one, disposition: RetainSameContract { justification: v1cc_fixture_nes(s: "controlled specimen"), coverage: Covered { by: v1cc_fixture_nes(s: fixture_unrealized_successor) } }), +] + +data planted_covered_unrealized_population: ConsumerPopulation = PopulationMeasuredComplete { + rows: planted_covered_unrealized_rows, + joined_media: [ WorkflowArgv ], +} diff --git a/dag/test/fixture/v1_witness_census/specimens.dag b/dag/test/fixture/v1_witness_census/specimens.dag new file mode 100644 index 00000000000..5578959e508 --- /dev/null +++ b/dag/test/fixture/v1_witness_census/specimens.dag @@ -0,0 +1,126 @@ +module test.fixture.v1_witness_census.specimens + +import std.types { List, String } +import std.decl_ref { DeclarationRef, decl_ref } +import v2.workflow.required_floor { RequiredFloorDisposition, Planned, DeclinedLongModule, DeclinedFixtureMember } +import gunbc.v1_witness_census { + V1ClaimCutoverRow, ClaimCutoverDisposition, ClaimPopulation, ClaimRosterComplete, ClaimRosterUnmeasured, + Retired, ReplacedByStronger, StillRequired +} + +// CONTROLLED POPULATIONS FOR THE CLAIM CONSERVATION WALL. The live roster is unmeasured, so every +// assertion in the paired witness would be vacuously true over it -- a join against an empty +// denominator is total for free. That is why these fixtures are not optional: without them the +// conservation wall would be a permanently green check, which DESIGN section 4b calls worse than +// an absent one because it will be cited as coverage. +// +// The five plants are the five ways a total-looking accounting loses a subject, and they are +// deliberately NOT five flavours of the same mistake: a missing row, an invented row, a merge onto +// one native identity, a self-referential red control, and a support module folded in as a claim. +// Only the first is caught by asking 'does every claim have a disposition'. The rest answer yes. + +data claim_a: DeclarationRef = decl_ref(module_path: "test.fixture.claim", decl_name: "alpha") +data claim_b: DeclarationRef = decl_ref(module_path: "test.fixture.claim", decl_name: "beta") +data claim_c: DeclarationRef = decl_ref(module_path: "test.fixture.claim", decl_name: "gamma") + +data native_a: DeclarationRef = decl_ref(module_path: "test.fixture.native", decl_name: "alpha_native") +data native_b: DeclarationRef = decl_ref(module_path: "test.fixture.native", decl_name: "beta_native") +data control_b: DeclarationRef = decl_ref(module_path: "test.fixture.native", decl_name: "beta_red_control") +data deleted_subject: DeclarationRef = decl_ref(module_path: "test.fixture.subject", decl_name: "gamma_subject") + +fn v1wc_fixture_row(identity: DeclarationRef, standing: RequiredFloorDisposition, disposition: ClaimCutoverDisposition) -> V1ClaimCutoverRow { + { pre_cutover_identity: identity, floor_standing: standing, disposition: disposition } +} + +// THE CLEAN ACCOUNTING: three pre-cutover claims, all three arms inhabited on purpose -- an +// accounting exercised only over its most common arm says nothing about the other two. beta is +// floor-declined by module name AND still required, which is the ruling's point: standing is not +// evidence, and a declined claim enters the native roster regardless. +data clean_rows: List = [ + v1wc_fixture_row(identity: claim_a, standing: Planned, disposition: StillRequired { surviving_subject: claim_a, native_identity: native_a }), + v1wc_fixture_row(identity: claim_b, standing: DeclinedLongModule { matched_prefix: "test.claim.long." }, disposition: ReplacedByStronger { + replacement: native_b, + covering_relation: "controlled specimen: the replacement asserts the old claim's property over a strict superset of inputs", + executed_red: control_b, + }), + v1wc_fixture_row(identity: claim_c, standing: Planned, disposition: Retired { + deleted_subject: deleted_subject, + evidence: "controlled specimen: the subject is deleted by the same transaction, and no surviving declaration reaches it", + }), +] + +data clean_roster: List = [ + "test.fixture.claim::alpha", + "test.fixture.claim::beta", + "test.fixture.claim::gamma", +] + +data clean_population: ClaimPopulation = ClaimRosterComplete { rows: clean_rows, roster_producer: "controlled fixture; no floor run" } + +// PLANT ONE -- a roster identity with no row. The lost subject in its purest form. +data planted_unaccounted_roster: List = [ + "test.fixture.claim::alpha", + "test.fixture.claim::beta", + "test.fixture.claim::gamma", + "test.fixture.claim::delta", +] + +// PLANT TWO -- a row for a claim the roster does not contain. Row count unchanged, subject invented. +data planted_fabricated_rows: List = [ + v1wc_fixture_row(identity: claim_a, standing: Planned, disposition: StillRequired { surviving_subject: claim_a, native_identity: native_a }), + v1wc_fixture_row(identity: decl_ref(module_path: "test.fixture.claim", decl_name: "never_existed"), standing: Planned, disposition: StillRequired { surviving_subject: claim_b, native_identity: native_b }), +] + +data planted_fabricated_roster: List = [ + "test.fixture.claim::alpha", + "test.fixture.claim::never_existed_not_in_roster", +] + +data planted_fabricated_population: ClaimPopulation = ClaimRosterComplete { rows: planted_fabricated_rows, roster_producer: "controlled fixture" } + +// PLANT THREE -- two claims mapped onto ONE native identity. Every roster entry has a row, every row +// is in the roster, and one subject is no longer independently checked. +data planted_merged_rows: List = [ + v1wc_fixture_row(identity: claim_a, standing: Planned, disposition: StillRequired { surviving_subject: claim_a, native_identity: native_a }), + v1wc_fixture_row(identity: claim_b, standing: Planned, disposition: StillRequired { surviving_subject: claim_b, native_identity: native_a }), +] + +data planted_merged_roster: List = [ "test.fixture.claim::alpha", "test.fixture.claim::beta" ] + +data planted_merged_population: ClaimPopulation = ClaimRosterComplete { rows: planted_merged_rows, roster_producer: "controlled fixture" } + +// PLANT FOUR -- a replacement whose executed red is the replacement itself. One keystroke from the +// honest form, invisible to every other direction of the join. +data planted_self_control_rows: List = [ + v1wc_fixture_row(identity: claim_b, standing: Planned, disposition: ReplacedByStronger { + replacement: native_b, + covering_relation: "controlled specimen", + executed_red: native_b, + }), +] + +data planted_self_control_roster: List = [ "test.fixture.claim::beta" ] + +data planted_self_control_population: ClaimPopulation = ClaimRosterComplete { rows: planted_self_control_rows, roster_producer: "controlled fixture" } + +// PLANT FIVE -- a fixture member given a disposition. The floor already says this module is a +// support module by its structural relation to claims; a row for it closes a count with a subject +// that was never a claim. +data planted_fixture_member_rows: List = [ + v1wc_fixture_row(identity: claim_a, standing: Planned, disposition: StillRequired { surviving_subject: claim_a, native_identity: native_a }), + v1wc_fixture_row(identity: claim_c, standing: DeclinedFixtureMember { matched_prefix: "test.fixture." }, disposition: Retired { + deleted_subject: deleted_subject, + evidence: "controlled specimen: a support module folded in to close the count", + }), +] + +data planted_fixture_member_roster: List = [ "test.fixture.claim::alpha", "test.fixture.claim::gamma" ] + +data planted_fixture_member_population: ClaimPopulation = ClaimRosterComplete { rows: planted_fixture_member_rows, roster_producer: "controlled fixture" } + +// PLANT SIX -- the clean rows over an UNMEASURED roster. Nothing is wrong with any row; the gate must +// still refuse, because a join whose denominator was never read is total for free. +data planted_unmeasured_population: ClaimPopulation = ClaimRosterUnmeasured { + reason: "controlled specimen: the roster was not read", + what_would_settle_it: "controlled specimen", +} From 3a985c534d0608f2d537bef21939e84d9d14511b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 13:30:00 +0000 Subject: [PATCH 2/7] The four shim consumers become citable by construction: the tooling namespace row, derived citability, and the join on DeclarationRef - gunbc.rust_item_host_observation: the four hand-Rust source prefixes move here from the stage0 scaffold (importing them there would have closed the cycle scaffold -> seed_growth_admission -> this module), and the tooling tree gets its namespace row: `v1_compiled.`, the package the shim crates assemble into -- a crate-named root outside the .dag index like `v1_compiler`, deliberately NOT `tools.` because the citation gate treats a .dag-declared root as in-index. The projection now takes its table as a parameter (`_in` forms); the bare forms pass the live rows. - gunbc.v1_consumer_census: shim citability is DERIVED by running item_declaration_ref_in over the four items against a supplied table. Under the live table all four are BoundaryConsumer rows and the uncitable list is empty by construction; with the tooling row removed all four return to V1UncitableConsumer -- executed as the falsifier. Population stays LowerBound for its three other named holes. - gunbc.v1_witness_census: the roster joins on DeclarationRef via declaration_ref_eq, not on a rendered module::decl string (XL-1's hollow-alias finding). - fixtures: every planted DeclarationRef is now a self-citation of a real declaration -- the required floor's declarations phase refused the first push with CITED-MODULE-ABSENT on invented fixture modules; a plant may be absent from a roster, never from the tree. - list_snoc_item / list_append called with their declared labels. Executed (claim_batch on BuildBuddy): 11 + 10 census witnesses, 6 rust_item_host_observation witnesses including the new tooling projection, 46 stage0_rust_source_lifecycle_scaffold, 7 stage0_rust_product_reachability. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- dag/gunbc/rust_item_host_observation.dag | 54 +++++++- .../stage0_rust_product_reachability.dag | 5 +- .../stage0_rust_source_lifecycle_scaffold.dag | 11 +- dag/gunbc/v1/v1_consumer_census.dag | 119 +++++++++++++++--- dag/gunbc/v1/v1_witness_census.dag | 29 +++-- ...ust_item_host_observation_witness_test.dag | 15 +++ .../claim/v1_consumer_census_witness_test.dag | 44 +++++-- .../fixture/v1_consumer_census/specimens.dag | 25 ++-- .../fixture/v1_witness_census/specimens.dag | 49 ++++---- 9 files changed, 264 insertions(+), 87 deletions(-) diff --git a/dag/gunbc/rust_item_host_observation.dag b/dag/gunbc/rust_item_host_observation.dag index 50b80a75394..bbde80563c4 100644 --- a/dag/gunbc/rust_item_host_observation.dag +++ b/dag/gunbc/rust_item_host_observation.dag @@ -65,11 +65,41 @@ type RustSourceNamespaceRow { namespace_prefix: String } +// THE HAND-RUST SOURCE PREFIXES LIVE HERE, BESIDE THE NAMESPACE TABLE THAT KEYS ON THEM. They were +// authored in gunbc.stage0_rust_source_lifecycle_scaffold as discovery hints, and the namespace row +// for the tooling tree needs the same prefix; importing it from the scaffold would close a real +// cycle (scaffold -> seed_growth_admission -> this module), and restating the literal would be the +// second representation DESIGN section 3 forbids. So the four constants moved to the layer that owns +// "where hand Rust lives and what namespace it carries", and the scaffold imports them from here. +data rust_source_prefix_test_harness: String = "src/v1/tests/" + +data rust_source_prefix_stage0_test: String = "src/v1/stage0/tests/" + +data rust_source_prefix_stage0_example: String = "src/v1/stage0/examples/" + +data rust_source_prefix_tooling: String = "dag/gunbc/instruments/" + +// THE TOOLING ROW IS A CONSEQUENCE OF WHAT THE DIRECTORY IS, NOT A PATH EXCEPTION. The tree the +// scaffold classifies as rust_source_prefix_tooling holds the self-host shim crates: hand Rust that +// stands in for primitive arms the emitted v2 closure does not yet realize, reaching v1_rt to do so, +// and assembled by tools.self_host_curated_seed_linked_harness into ONE Cargo package whose name is +// `v1_compiled` (cssl_v1_compiled_cargo_package_header). The namespace root is therefore the crate +// name, by the same rule that gives src/v1/stage0/src/ the `v1_compiler` root -- the package the +// path compiles into, spelled as Rust spells it. It is deliberately NOT `tools.`, the root the .dag +// instruments beside these files declare: the citation gate (v1_compiler.declaration_index +// citation_is_outside_index) treats a root some .dag module declares as inside the index and refuses +// an absent module under it, so a Rust namespace sharing a .dag root would make every Rust item +// citation under it refuse. `v1_compiler` and `v1_compiled` sit outside the .dag index for exactly +// that reason. Until this row existed the four shim crates that reach v1_rt were consumers +// gunbc.v1_consumer_census could see and the exact cut vocabulary could not spell; removing this +// row returns them to that uncitable state, which test.claim.v1_consumer_census_witness_test +// executes as the falsifier. data rust_source_namespace_rows: List = [ RustSourceNamespaceRow { repo_prefix: "src/v1/stage0/src/bin/", namespace_prefix: "v1_compiler.bin." }, RustSourceNamespaceRow { repo_prefix: "src/v1/stage0/src/", namespace_prefix: "v1_compiler." }, RustSourceNamespaceRow { repo_prefix: "src/v1/stage0/tests/", namespace_prefix: "v1_compiler.tests." }, - RustSourceNamespaceRow { repo_prefix: "src/v1/tests/src/", namespace_prefix: "v1_compiler_tests." } + RustSourceNamespaceRow { repo_prefix: "src/v1/tests/src/", namespace_prefix: "v1_compiler_tests." }, + RustSourceNamespaceRow { repo_prefix: rust_source_prefix_tooling, namespace_prefix: "v1_compiled." } ] type RustModulePathProjection @@ -93,8 +123,16 @@ fn strip_rs_suffix(s: String) -> String { // src/v1/stage0/src/bin/ is a subtree of src/v1/stage0/src/, so a first-match reader would give // every binary the library's namespace and the row order would silently be load-bearing. fn rust_namespace_row_for_path(repo_path: String) -> List { + rust_namespace_row_for_path_in(rows: rust_source_namespace_rows, repo_path: repo_path) +} + +// THE TABLE IS A PARAMETER OF THE FOLD, AND THE LIVE TABLE IS ONE CALLER. A projection that read +// only the declared rows could be exercised against exactly one table, so "what does this path +// project to WITHOUT row R" -- the falsifier for any row -- would be unaskable without editing the +// authority. The `_in` forms take the rows; the bare forms pass the live ones. +fn rust_namespace_row_for_path_in(rows: List, repo_path: String) -> List { fold_list( - xs: rust_source_namespace_rows, + xs: rows, empty: [] as List, cons: fn(best, row) { if !starts_with(s: repo_path, prefix: row.repo_prefix) { @@ -117,8 +155,12 @@ fn rust_namespace_row_for_path(repo_path: String) -> List RustModulePathProjection { + rust_module_path_for_repo_path_in(rows: rust_source_namespace_rows, repo_path: repo_path) +} + +fn rust_module_path_for_repo_path_in(rows: List, repo_path: String) -> RustModulePathProjection { fold_list( - xs: rust_namespace_row_for_path(repo_path: repo_path), + xs: rust_namespace_row_for_path_in(rows: rows, repo_path: repo_path), empty: RustModulePathRefused { repo_path: repo_path, detail: "no rust_source_namespace_rows prefix claims this path, so no module path can be derived for it" @@ -152,6 +194,10 @@ type ItemDeclarationRefProjection | ItemDeclarationRefRefused { item_key: String, detail: String } fn item_declaration_ref(item: RustItemIdentity) -> ItemDeclarationRefProjection { + item_declaration_ref_in(rows: rust_source_namespace_rows, item: item) +} + +fn item_declaration_ref_in(rows: List, item: RustItemIdentity) -> ItemDeclarationRefProjection { let key = rust_item_identity_key(item: item) if item.kind == RustImplMethod || item.kind == RustImplBlock { ItemDeclarationRefUncitable { @@ -159,7 +205,7 @@ fn item_declaration_ref(item: RustItemIdentity) -> ItemDeclarationRefProjection detail: "std.decl_ref DeclField cannot name a method on an impl block, nor an unnamed impl block itself" } } else { - match rust_module_path_for_repo_path(repo_path: item.repo_path as String) { + match rust_module_path_for_repo_path_in(rows: rows, repo_path: item.repo_path as String) { RustModulePathRefused { repo_path: _, detail: detail } => ItemDeclarationRefRefused { item_key: key, detail: detail } RustModulePathProjected { module_path: module_path } => diff --git a/dag/gunbc/stage0/stage0_rust_product_reachability.dag b/dag/gunbc/stage0/stage0_rust_product_reachability.dag index 19da16a9f67..bbcddeedaa7 100644 --- a/dag/gunbc/stage0/stage0_rust_product_reachability.dag +++ b/dag/gunbc/stage0/stage0_rust_product_reachability.dag @@ -8,11 +8,10 @@ import gunbc.stage0_rust_host_observation { RustManifestReadRefused, RustSourceHostObservation } +import gunbc.rust_item_host_observation { rust_source_prefix_stage0_test, rust_source_prefix_test_harness } import gunbc.stage0_rust_source_lifecycle_scaffold { rust_source_path_has_prefix, - path_in_list, - rust_source_prefix_stage0_test, - rust_source_prefix_test_harness + path_in_list } import std.content_hash { Fnv1a64Structural } import v2.std.algebra { fold_list, list_map, list_snoc_item } diff --git a/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag b/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag index b39b52b7960..336040d8df1 100644 --- a/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag +++ b/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag @@ -17,6 +17,9 @@ import gunbc.stage0_rust_host_observation { } import gunbc.generated_artifact { GeneratedArtifact, artifact_path, generated_artifact_registry } import gunbc.seed_growth_admission { seed_growth_roster_well_formed_gate_holds } +import gunbc.rust_item_host_observation { + rust_source_prefix_test_harness, rust_source_prefix_stage0_test, rust_source_prefix_stage0_example, rust_source_prefix_tooling +} import std.content_hash { Fnv1a64Structural } import std.keyed_roster { path_occurrence_count } import std.decl_ref { DeclarationRef, WholeDeclaration } @@ -290,14 +293,6 @@ fn rust_source_manifest_state_verdict(observation: RustSourceHostObservation) -> } } -data rust_source_prefix_test_harness: String = "src/v1/tests/" - -data rust_source_prefix_stage0_test: String = "src/v1/stage0/tests/" - -data rust_source_prefix_stage0_example: String = "src/v1/stage0/examples/" - -data rust_source_prefix_tooling: String = "dag/gunbc/instruments/" - data rust_source_discovery_prefix_hints: List = [ rust_source_prefix_test_harness, rust_source_prefix_tooling, diff --git a/dag/gunbc/v1/v1_consumer_census.dag b/dag/gunbc/v1/v1_consumer_census.dag index ed9e2719960..877645d5f81 100644 --- a/dag/gunbc/v1/v1_consumer_census.dag +++ b/dag/gunbc/v1/v1_consumer_census.dag @@ -1,13 +1,19 @@ module gunbc.v1_consumer_census -import std.types { List, String, NonEmptyStr, Bool, Int } +import std.types { List, String, NonEmptyStr, FilePath, Bool, Int } import std.decl_ref { DeclarationRef, decl_ref } +import v2.std.algebra { fold_list, list_append, list_snoc_item } import std.dissolution { DissolutionCondition, unbound_dissolution } import gunbc.replacement_cut { BoundaryConsumer, BoundaryCensus, ConsumersEnumerated, ConsumerDisposition, RetainSameContract, RetainChangedContract, ReplacedByY, EvidenceOnly, Retire, Undecided, CoverageClaim, Covered, CoverageOpen } +import gunbc.rust_item_identity { RustItemIdentity, RustModule } +import gunbc.rust_item_host_observation { + RustSourceNamespaceRow, rust_source_namespace_rows, item_declaration_ref_in, + ItemDeclarationRefProjection, ItemDeclarationRefProjected, ItemDeclarationRefUncitable, ItemDeclarationRefRefused +} // XL-5's FIRST DELIVERABLE: the population that has to be EMPTY before the bankruptcy transaction // can execute, remeasured at the grain gunbc.replacement_cut requires. XL-5 is primarily a @@ -155,7 +161,7 @@ fn coverage_authorities(c: CoverageClaim) -> List { } } -data v1_consumer_census_uncitable_note: String = "A CONSUMER THE EXACT VOCABULARY CANNOT SPELL IS CARRIED AS A REFUSAL, NEVER AS A FABRICATED REFERENCE. gunbc.rust_item_host_observation item_declaration_ref projects a Rust item into DeclarationRef through rust_source_namespace_rows, and those rows claim prefixes under src/v1 only. The four self-host shim crates under dag/gunbc/instruments/ are hand-authored Rust OUTSIDE every claimed prefix, so the projection returns ItemDeclarationRefRefused for each of them -- and a BoundaryConsumer needs a DeclarationRef on both sides. The two dishonest moves are to invent a module path the projection did not produce, or to drop the four from the census because the carrier has no slot for them; both make the population look smaller than it is. So they are carried here in the projection's own refusal shape, with their disposition, and they COUNT toward the blocking column and toward the lower-bound standing below. The capability that dissolves this list is a rust_source_namespace_rows row for the instruments directory, at which point these four become ordinary BoundaryConsumer rows and this list is empty by construction rather than by edit." +data v1_consumer_census_uncitable_note: String = "A CONSUMER THE EXACT VOCABULARY CANNOT SPELL IS CARRIED AS A REFUSAL, NEVER AS A FABRICATED REFERENCE. gunbc.rust_item_host_observation item_declaration_ref projects a Rust item into DeclarationRef through rust_source_namespace_rows, and a BoundaryConsumer needs a DeclarationRef on both sides. The four self-host shim crates under dag/gunbc/instruments/ are hand-authored Rust that reaches v1_rt; until this lane added the tooling namespace row the projection REFUSED them, and the two dishonest moves were to invent a module path the projection did not produce, or to drop the four because the carrier had no slot for them. So citability is DERIVED, never authored: v1_shim_partition runs the projection over the four items against a supplied namespace table, and a shim lands as a BoundaryConsumer row when the projection answers and in this refusal shape when it does not. Under the live table all four are cited and this list is empty by construction; under the live table with the tooling row removed all four return here -- which is the falsifier the paired witness executes, and the reason the table is a parameter." type V1UncitableConsumer { item_key: String @@ -291,7 +297,7 @@ fn tsv_row(path_decl: String) -> V1ConsumerRow { data v1_consumer_roster_note: String = "THE ROSTER. Every relation was established by running its cited producer against the revision above and reading the emitting declaration, and each row's identity is the relation a deletion would break, not the file the evidence was read in. Rows are not ordered by severity: the floor-cut plan's bounds say the dangerous member is the one nobody thought to look for, and ordering by an author's judgement is what lets a reader stop early.\n\nTHE RETAINED-OPEN ROWS ARE THE TRANSACTION. Everything else is discharged by deleting a subject or by a successor that already exists; the rows carrying CoverageOpen are the entire content of 'XL-5 cannot run yet', and each justification names the CAPABILITY that closes it -- never an artifact that would contribute to one, which DESIGN section 4b(3) rules is satisfied while the capability stays dead. That is the honest shape of a bankruptcy: the estate is mostly worthless, and the whole question is the creditors who are still owed.\n\nTHE TSV ROWS ARE FOUR RELATIONS, NOT ONE, because the authority's key is consumer x consumed authority and one upload step consumes four path declarations. Collapsing them would let one disposition stand for four dependencies, which is the exact conflation the key exists to refuse." -data v1_consumers: List = [ +data v1_static_consumers: List = [ { boundary: v1cc_boundary( consumer: wfw(decl: "build_lane_run_step"), @@ -428,33 +434,108 @@ data v1_consumers: List = [ tsv_row(path_decl: "required_floor_claim_cost_path"), ] -fn shim_consumer(path: String) -> V1UncitableConsumer { +fn v1_shim_disposition() -> ConsumerDisposition { + retained_open(justification: "a hand-authored shim standing in for primitive arms the emitted v2 closure does not yet realize; the only Rust outside src/v1 that reaches the v1 runtime bridge. These shims are themselves v1 CONSUMERS slated for a disposition, not infrastructure that survives the cut. Closes on: the emitted v2 closure realizing those arms so the shim has nothing to bridge -- XL-0's arms-to-zero milestone AS EXECUTED, meaning the emitted crate compiles without a v1_rt path rather than merely cargo-checking with one") +} + +data v1_rt_bridge_authority: DeclarationRef = decl_ref(module_path: "v1_compiler.v1_rt", decl_name: "v1_rt") + +// THE FOUR SHIM ITEMS, at the grain gunbc.rust_item_identity carries: the crate root of each shim +// crate, a RustModule item named for the file. loc is the measured line count at v1_census_revision +// (wc -l) and is metadata; identity is the path and kind. +fn v1_shim_item(path: String, loc: Int) -> RustItemIdentity { + RustItemIdentity { + repo_path: path as FilePath, + kind: RustModule, + name: "lib" as NonEmptyStr, + impl_subject: "", + enclosing_module: "", + start_line: 1, + loc: loc, + } +} + +fn v1_shim_items() -> List { + [ + v1_shim_item(path: "dag/gunbc/instruments/self_host_03_normalize_shims/lib.rs", loc: 23), + v1_shim_item(path: "dag/gunbc/instruments/self_host_body_producer_shims/lib.rs", loc: 10), + v1_shim_item(path: "dag/gunbc/instruments/self_host_parse_engine_hooks_shims/lib.rs", loc: 8), + v1_shim_item(path: "dag/gunbc/instruments/self_host_use_site_verdict_shims/lib.rs", loc: 10), + ] +} + +type V1ShimPartition { + cited: List + uncitable: List +} + +fn v1_shim_cited_row(ref: DeclarationRef) -> V1ConsumerRow { { - item_key: path, - refusal_detail: "no rust_source_namespace_rows prefix claims this path, so no module path can be derived for it", + boundary: v1cc_boundary(consumer: ref, authority: v1_rt_bridge_authority, disposition: v1_shim_disposition()), medium: RustUseEdge, subject: V1RuntimeBridge, - disposition: retained_open(justification: "a hand-authored shim standing in for primitive arms the emitted v2 closure does not yet realize; the only Rust outside src/v1 that reaches the v1 runtime bridge. Closes on: the emitted v2 closure realizing those arms so the shim has nothing to bridge -- XL-0's arms-to-zero milestone AS EXECUTED, meaning the emitted crate compiles without a v1_rt path rather than merely cargo-checking with one"), discovered_by: producer_rust_bridge_edge, } } -data v1_uncitable_consumers: List = [ - shim_consumer(path: "dag/gunbc/instruments/self_host_03_normalize_shims/lib.rs"), - shim_consumer(path: "dag/gunbc/instruments/self_host_body_producer_shims/lib.rs"), - shim_consumer(path: "dag/gunbc/instruments/self_host_parse_engine_hooks_shims/lib.rs"), - shim_consumer(path: "dag/gunbc/instruments/self_host_use_site_verdict_shims/lib.rs"), -] +fn v1_shim_uncitable_row(item_key: String, detail: String) -> V1UncitableConsumer { + { + item_key: item_key, + refusal_detail: detail, + medium: RustUseEdge, + subject: V1RuntimeBridge, + disposition: v1_shim_disposition(), + discovered_by: producer_rust_bridge_edge, + } +} + +// CITABILITY IS THE PROJECTION'S ANSWER, ASKED AGAINST A SUPPLIED TABLE. One fold, two accumulators; +// a shim cannot be in both and cannot be in neither. +fn v1_shim_partition(rows: List) -> V1ShimPartition { + fold_list( + xs: v1_shim_items(), + empty: V1ShimPartition { cited: [], uncitable: [] }, + cons: fn(acc, item) { + match item_declaration_ref_in(rows: rows, item: item) { + ItemDeclarationRefProjected { ref: r } => + V1ShimPartition { cited: list_snoc_item(xs: acc.cited, item: v1_shim_cited_row(ref: r)), uncitable: acc.uncitable } + ItemDeclarationRefUncitable { item_key: k, detail: d } => + V1ShimPartition { cited: acc.cited, uncitable: list_snoc_item(xs: acc.uncitable, item: v1_shim_uncitable_row(item_key: k, detail: d)) } + ItemDeclarationRefRefused { item_key: k, detail: d } => + V1ShimPartition { cited: acc.cited, uncitable: list_snoc_item(xs: acc.uncitable, item: v1_shim_uncitable_row(item_key: k, detail: d)) } + } + } + ) +} + +fn v1_consumers_for(rows: List) -> List { + list_append(left: v1_static_consumers, right: v1_shim_partition(rows: rows).cited) +} + +fn v1_consumers() -> List { + v1_consumers_for(rows: rust_source_namespace_rows) +} + +fn v1_uncitable_consumers() -> List { + v1_shim_partition(rows: rust_source_namespace_rows).uncitable +} // THE POPULATION THIS ROSTER CONSTITUTES TODAY, and it is deliberately not the Complete arm. Seven // producers were run and none of them joins the others. Filing this as Complete would be the rung // inflation DESIGN section 4b names as worse than sitting low, because the admission gate below // reads this field and an inflated Complete would let the transaction execute against a population // that was never closed. -data v1_consumer_population: ConsumerPopulation = PopulationMeasuredLowerBound { - rows: v1_consumers, - uncitable: v1_uncitable_consumers, - missing_basis: "seven per-medium sweeps, unjoined, plus four consumers the exact vocabulary cannot cite. Three named holes, each of which would produce a row this roster does not have: (1) no producer classifies the .dag argv rows -- 85 .dag files name a v1 binary in a string position and only the two ci_release_bins rosters were traced to a consumer; (2) the deletion-set blind spot the floor cut measured has one row here (workspace_members) and no instrument -- a consumer defined inside src/v1 and consumed inside src/v1 cannot refuse when both go, and only a per-deleted-file question finds the rest; (3) reachability is not measured for any row: every disposition above is a PRESENCE claim, and presence over-approximates demand, which is the reachability_read_as_occupancy class this repository rosters and XL-1 tripped on in its own first census.", +fn v1_consumer_population_for(rows: List) -> ConsumerPopulation { + let partition = v1_shim_partition(rows: rows) + PopulationMeasuredLowerBound { + rows: list_append(left: v1_static_consumers, right: partition.cited), + uncitable: partition.uncitable, + missing_basis: "seven per-medium sweeps, unjoined. Three named holes, each of which would produce a row this roster does not have: (1) no producer classifies the .dag argv rows -- 85 .dag files name a v1 binary in a string position and only the two ci_release_bins rosters were traced to a consumer; (2) the deletion-set blind spot the floor cut measured has one row here (workspace_members) and no instrument -- a consumer defined inside src/v1 and consumed inside src/v1 cannot refuse when both go, and only a per-deleted-file question finds the rest; (3) reachability is not measured for any row: every disposition above is a PRESENCE claim, and presence over-approximates demand, which is the reachability_read_as_occupancy class this repository rosters and XL-1 tripped on in its own first census. The uncitable column is NOT a fourth hole any more: under the live namespace table it is empty by construction, and the tooling row that made it so was necessary for Complete, not sufficient.", + } +} + +fn v1_consumer_population() -> ConsumerPopulation { + v1_consumer_population_for(rows: rust_source_namespace_rows) } // THE PROJECTION INTO THE EXACT CARRIER. When the population reaches Complete, this is the @@ -527,11 +608,11 @@ fn v1_blocking_uncitable(uncitable: List) -> List Int { - count(v1_blocking_consumers(rows: v1_consumers)) + count(v1_blocking_uncitable(uncitable: v1_uncitable_consumers)) + count(v1_blocking_consumers(rows: v1_consumers())) + count(v1_blocking_uncitable(uncitable: v1_uncitable_consumers())) } fn v1_consumer_member_count() -> Int { - count(v1_consumers) + count(v1_uncitable_consumers) + count(v1_consumers()) + count(v1_uncitable_consumers()) } // THE ADMISSION GATE FOR THE BANKRUPTCY TRANSACTION. All four conditions, and the first is the one diff --git a/dag/gunbc/v1/v1_witness_census.dag b/dag/gunbc/v1/v1_witness_census.dag index 73276cd2b95..6073ae9cadc 100644 --- a/dag/gunbc/v1/v1_witness_census.dag +++ b/dag/gunbc/v1/v1_witness_census.dag @@ -1,7 +1,7 @@ module gunbc.v1_witness_census import std.types { List, String, NonEmptyStr, Bool, Int } -import std.decl_ref { DeclarationRef, decl_ref } +import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } import std.dissolution { DissolutionCondition, unbound_dissolution } import gunbc.replacement_cut { EvidenceDisposition, ReenrollAgainstY, ReplaceEvidence, RetireEvidence } import v2.workflow.required_floor { @@ -122,8 +122,17 @@ data v1_claim_live_population: ClaimPopulation = ClaimRosterUnmeasured { what_would_settle_it: "XL-1's joined claim population (full-tree floor claim identities x claim_scope_for x RequiredFloorDisposition) at a named run and revision, landed here as ClaimRosterComplete with that run named as roster_producer, and one disposition per row authored by XL-5", } -fn v1_claim_row_keys(rows: List) -> List { - rows |> map(r => v1_claim_identity_key(r: r.pre_cutover_identity)) +// THE JOIN IS ON DeclarationRef, NEVER ON A RENDERED SPELLING. XL-1's producer keys its rows on +// identity_ref: DeclarationRef and derives the dotted string from it; a roster of module::decl +// strings here would be a second spelling of one identity on the join key, the hollow-alias class. +// v1_claim_identity_key survives only as a display projection for the evidence rows the exact cut +// carries as NonEmptyStr, and as the occurrence key for the distinctness folds. +fn v1_claim_ref_in(needle: DeclarationRef, xs: List) -> Bool { + xs |> any(x => declaration_ref_eq(a: x, b: needle)) +} + +fn v1_claim_row_refs(rows: List) -> List { + rows |> map(r => r.pre_cutover_identity) } fn v1_claim_key_in(needle: String, xs: List) -> Bool { @@ -135,22 +144,22 @@ fn v1_claim_key_in(needle: String, xs: List) -> Bool { // Direction one: every identity the pre-cutover roster contains has exactly one row. This is the // one that catches a lost subject -- a claim that simply stops being executed by the native fold // leaves no artifact, produces no red, and shortens no number a reader is looking at. -fn v1_claims_unaccounted(roster: List, rows: List) -> List { - roster |> filter(id => !v1_claim_key_in(needle: id, xs: v1_claim_row_keys(rows: rows))) +fn v1_claims_unaccounted(roster: List, rows: List) -> List { + roster |> filter(id => !v1_claim_ref_in(needle: id, xs: v1_claim_row_refs(rows: rows))) } -fn v1_every_claim_accounted(roster: List, rows: List) -> Bool { +fn v1_every_claim_accounted(roster: List, rows: List) -> Bool { count(v1_claims_unaccounted(roster: roster, rows: rows)) == 0 } // Direction two: every row names an identity the roster contains. A row for a claim that does not // exist pre-cutover is a fabricated subject, and it inflates the accounting in the one place a // reader checks -- the same row count, with a real subject swapped for an invented one. -fn v1_claim_rows_outside_roster(roster: List, rows: List) -> List { - rows |> filter(r => !v1_claim_key_in(needle: v1_claim_identity_key(r: r.pre_cutover_identity), xs: roster)) +fn v1_claim_rows_outside_roster(roster: List, rows: List) -> List { + rows |> filter(r => !v1_claim_ref_in(needle: r.pre_cutover_identity, xs: roster)) } -fn v1_every_claim_row_is_in_roster(roster: List, rows: List) -> Bool { +fn v1_every_claim_row_is_in_roster(roster: List, rows: List) -> Bool { count(v1_claim_rows_outside_roster(roster: roster, rows: rows)) == 0 } @@ -204,7 +213,7 @@ fn v1_no_fixture_member_carries_a_disposition(rows: List) -> // THE GATE. Conservation is all five directions over a COMPLETE roster; any of them dropped is a // different and weaker claim, and the completeness arm is first for the same reason it is first in // the consumer census -- a join over an unmeasured roster is vacuously total. -fn v1_claim_conservation_holds(population: ClaimPopulation, roster: List) -> Bool { +fn v1_claim_conservation_holds(population: ClaimPopulation, roster: List) -> Bool { let rows = claim_population_rows(p: population) claim_population_is_complete(p: population) && v1_every_claim_accounted(roster: roster, rows: rows) diff --git a/dag/test/claim/rust_item_host_observation_witness_test.dag b/dag/test/claim/rust_item_host_observation_witness_test.dag index 0a9042caef7..3847e72ead3 100644 --- a/dag/test/claim/rust_item_host_observation_witness_test.dag +++ b/dag/test/claim/rust_item_host_observation_witness_test.dag @@ -122,6 +122,21 @@ test fn a_path_no_namespace_row_claims_refuses_rather_than_acquiring_one() -> Bo } } +// THE TOOLING TREE CARRIES THE NAME OF THE PACKAGE IT ASSEMBLES INTO. dag/gunbc/instruments/ is the +// scaffold's rust_source_prefix_tooling; its shim crates are assembled into the `v1_compiled` +// package, so a shim crate root projects to v1_compiled..lib -- a root no .dag module +// declares, like v1_compiler -- and a path one directory up is still unclaimed. +test fn the_tooling_tree_projects_to_the_assembled_package_namespace() -> Bool { + match rust_module_path_for_repo_path(repo_path: "dag/gunbc/instruments/self_host_03_normalize_shims/lib.rs") { + RustModulePathProjected { module_path: path } => path == "v1_compiled.self_host_03_normalize_shims.lib" + RustModulePathRefused { repo_path: _, detail: _ } => false + } + && match rust_module_path_for_repo_path(repo_path: "dag/gunbc/not_instruments/lib.rs") { + RustModulePathRefused { repo_path: _, detail: _ } => true + RustModulePathProjected { module_path: _ } => false + } +} + test fn a_nested_source_path_keeps_its_directory_as_a_namespace_segment() -> Bool { match rust_module_path_for_repo_path(repo_path: "src/v1/stage0/src/cli_run/bare_reference_scanner.rs") { RustModulePathProjected { module_path: path } => path == "v1_compiler.cli_run.bare_reference_scanner" diff --git a/dag/test/claim/v1_consumer_census_witness_test.dag b/dag/test/claim/v1_consumer_census_witness_test.dag index 217ade5216c..fe6e5820944 100644 --- a/dag/test/claim/v1_consumer_census_witness_test.dag +++ b/dag/test/claim/v1_consumer_census_witness_test.dag @@ -2,11 +2,13 @@ module test.claim.v1_consumer_census_witness_test import std.types { Bool } import gunbc.replacement_cut { BoundaryCensus, ConsumersEnumerated, BoundaryDeclaredEmpty } +import gunbc.rust_item_host_observation { RustSourceNamespaceRow, rust_source_namespace_rows, rust_source_prefix_tooling } import gunbc.v1_consumer_census { v1_consumers, v1_uncitable_consumers, v1_consumer_population, v1_every_discovered_consumer_disposed, v1_every_row_names_a_live_consumer, v1_every_claimed_successor_is_realized, v1_bankruptcy_transaction_admitted, v1_blocking_consumer_count, v1_consumer_member_count, - v1_boundary_census, consumer_population_is_complete, consumer_population_rows, consumer_population_uncitable + v1_boundary_census, consumer_population_is_complete, consumer_population_rows, consumer_population_uncitable, + v1_shim_partition, v1_shim_items, v1_consumer_population_for } import test.fixture.v1_consumer_census.specimens { clean_rows, clean_discovered, clean_realized, clean_population, @@ -81,23 +83,49 @@ fn boundary_census_enumerates_the_rows() -> Bool { } } +// THE TOOLING NAMESPACE ROW IS LOAD-BEARING, AND ITS ABSENCE IS EXECUTED, NOT DESCRIBED. Under the +// live table every shim projects to a BoundaryConsumer row under the v1_compiled. namespace and nothing is +// uncitable; under the live table with exactly the tooling row removed, every shim returns to the +// uncitable list and none is cited. The two halves together are the falsifier the ruling asked for: +// the row is what makes the four spellable, and the census does not spell them any other way. +fn live_rows_without_tooling() -> List { + rust_source_namespace_rows |> filter(r => r.repo_prefix != rust_source_prefix_tooling) +} + +fn the_tooling_row_decides_shim_citability() -> Bool { + let with = v1_shim_partition(rows: rust_source_namespace_rows) + let without = v1_shim_partition(rows: live_rows_without_tooling()) + count(with.cited) == count(v1_shim_items()) && count(with.uncitable) == 0 + && count(without.uncitable) == count(v1_shim_items()) && count(without.cited) == 0 + && count(live_rows_without_tooling()) == count(rust_source_namespace_rows) - 1 + && (with.cited |> all(r => starts_with(s: r.boundary.consumer.module_path as String, prefix: "v1_compiled."))) +} + +// THE POPULATION IS DERIVED FROM THE SAME PARTITION: with the row, the uncitable column is empty; +// without it, four. Both arms stay LowerBound -- the row was necessary for Complete, not sufficient. +fn the_population_carries_the_partition() -> Bool { + count(consumer_population_uncitable(p: v1_consumer_population_for(rows: rust_source_namespace_rows))) == 0 + && count(consumer_population_uncitable(p: v1_consumer_population_for(rows: live_rows_without_tooling()))) == count(v1_shim_items()) + && !consumer_population_is_complete(p: v1_consumer_population_for(rows: rust_source_namespace_rows)) + && !consumer_population_is_complete(p: v1_consumer_population_for(rows: live_rows_without_tooling())) +} + // THE LIVE TREE REFUSES, AND FOR THE REASONS THE CENSUS RECORDS. Stated as a conjunction because // 'the gate is false' is also what a broken gate returns: the population is a lower bound AND there -// is at least one blocking consumer AND not every consumer blocks AND the uncitable list is -// non-empty -- four independent facts whose conjunction is what 'XL-5 has not run yet' means. +// is at least one blocking consumer AND not every consumer blocks -- three independent facts whose +// conjunction is what 'XL-5 has not run yet' means. fn the_live_transaction_refuses_for_recorded_reasons() -> Bool { - !consumer_population_is_complete(p: v1_consumer_population) + !consumer_population_is_complete(p: v1_consumer_population()) && v1_blocking_consumer_count() > 0 && v1_blocking_consumer_count() < v1_consumer_member_count() - && count(consumer_population_uncitable(p: v1_consumer_population)) > 0 } // THE ROSTER AND THE POPULATION NAME ONE LIST. Two declarations naming one list can disagree in // exactly one way -- an author filing a row and forgetting the population -- which would leave a // consumer recorded and unread by the gate. fn the_live_population_carries_the_whole_roster() -> Bool { - count(v1_consumers) == count(consumer_population_rows(p: v1_consumer_population)) - && count(v1_uncitable_consumers) == count(consumer_population_uncitable(p: v1_consumer_population)) + count(v1_consumers()) == count(consumer_population_rows(p: v1_consumer_population())) + && count(v1_uncitable_consumers()) == count(consumer_population_uncitable(p: v1_consumer_population())) } test fn consumer_census_catches_an_undisposed_consumer() -> Bool { undisposed_consumer_is_caught() } @@ -107,5 +135,7 @@ test fn consumer_census_admission_reads_completeness() -> Bool { admission_reads test fn consumer_census_admission_refuses_a_blocking_consumer() -> Bool { admission_refuses_a_blocking_consumer() } test fn consumer_census_admission_refuses_an_unrealized_successor() -> Bool { admission_refuses_an_unrealized_successor() } test fn consumer_census_boundary_census_enumerates_the_rows() -> Bool { boundary_census_enumerates_the_rows() } +test fn consumer_census_tooling_row_decides_shim_citability() -> Bool { the_tooling_row_decides_shim_citability() } +test fn consumer_census_population_carries_the_partition() -> Bool { the_population_carries_the_partition() } test fn consumer_census_live_transaction_refuses_for_recorded_reasons() -> Bool { the_live_transaction_refuses_for_recorded_reasons() } test fn consumer_census_live_population_carries_the_whole_roster() -> Bool { the_live_population_carries_the_whole_roster() } diff --git a/dag/test/fixture/v1_consumer_census/specimens.dag b/dag/test/fixture/v1_consumer_census/specimens.dag index efb47c30bab..283f50461b9 100644 --- a/dag/test/fixture/v1_consumer_census/specimens.dag +++ b/dag/test/fixture/v1_consumer_census/specimens.dag @@ -31,9 +31,16 @@ data fixture_producer: DiscoveryProducer = discovery_producer( source_revision: "fixture", ) -data consumer_one: DeclarationRef = decl_ref(module_path: "test.fixture.consumer", decl_name: "one") -data consumer_two: DeclarationRef = decl_ref(module_path: "test.fixture.consumer", decl_name: "two") -data old_authority: DeclarationRef = decl_ref(module_path: "test.fixture.old_root", decl_name: "authority") +// EVERY CITATION HERE NAMES A DECLARATION THAT EXISTS, and it is this module's own. The required +// floor's declarations phase resolves every decl_ref in the corpus (CITED-MODULE-ABSENT is a floor +// refusal, executed on the first push of this file against invented fixture modules), so a fixture +// may plant an identity that is absent from a ROSTER but never one that is absent from the TREE. +// The specimens are therefore self-citations: real declarations, controlled membership. +data fixture_module: String = "test.fixture.v1_consumer_census.specimens" +data consumer_one: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "consumer_one") +data consumer_two: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "consumer_two") +data consumer_three_undisposed: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "consumer_three_undisposed") +data old_authority: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "old_authority") data fixture_native_successor: String = "test.fixture.native successor_target" data fixture_unrealized_successor: String = "test.fixture.native successor_that_was_never_built" @@ -54,8 +61,8 @@ data clean_rows: List = [ ] data clean_discovered: List = [ - "test.fixture.consumer.one -> test.fixture.old_root.authority", - "test.fixture.consumer.two -> test.fixture.old_root.authority", + "test.fixture.v1_consumer_census.specimens.consumer_one -> test.fixture.v1_consumer_census.specimens.old_authority", + "test.fixture.v1_consumer_census.specimens.consumer_two -> test.fixture.v1_consumer_census.specimens.old_authority", ] data clean_realized: List = [ fixture_native_successor ] @@ -69,14 +76,14 @@ data clean_population: ConsumerPopulation = PopulationMeasuredComplete { // gains a third relation. This is the shape of the real failure: nobody edits the census, the tree // grows a consumer, and the census cannot notice. data planted_undisposed_discovered: List = [ - "test.fixture.consumer.one -> test.fixture.old_root.authority", - "test.fixture.consumer.two -> test.fixture.old_root.authority", - "test.fixture.consumer.three -> test.fixture.old_root.authority", + "test.fixture.v1_consumer_census.specimens.consumer_one -> test.fixture.v1_consumer_census.specimens.old_authority", + "test.fixture.v1_consumer_census.specimens.consumer_two -> test.fixture.v1_consumer_census.specimens.old_authority", + "test.fixture.v1_consumer_census.specimens.consumer_three_undisposed -> test.fixture.v1_consumer_census.specimens.old_authority", ] // PLANT TWO -- a row naming a relation the discovery population does not contain. data planted_stale_discovered: List = [ - "test.fixture.consumer.one -> test.fixture.old_root.authority", + "test.fixture.v1_consumer_census.specimens.consumer_one -> test.fixture.v1_consumer_census.specimens.old_authority", ] // PLANT THREE -- a successor claimed and never built. The row is well-formed; the only thing wrong diff --git a/dag/test/fixture/v1_witness_census/specimens.dag b/dag/test/fixture/v1_witness_census/specimens.dag index 5578959e508..df3b70a2135 100644 --- a/dag/test/fixture/v1_witness_census/specimens.dag +++ b/dag/test/fixture/v1_witness_census/specimens.dag @@ -19,14 +19,21 @@ import gunbc.v1_witness_census { // one native identity, a self-referential red control, and a support module folded in as a claim. // Only the first is caught by asking 'does every claim have a disposition'. The rest answer yes. -data claim_a: DeclarationRef = decl_ref(module_path: "test.fixture.claim", decl_name: "alpha") -data claim_b: DeclarationRef = decl_ref(module_path: "test.fixture.claim", decl_name: "beta") -data claim_c: DeclarationRef = decl_ref(module_path: "test.fixture.claim", decl_name: "gamma") - -data native_a: DeclarationRef = decl_ref(module_path: "test.fixture.native", decl_name: "alpha_native") -data native_b: DeclarationRef = decl_ref(module_path: "test.fixture.native", decl_name: "beta_native") -data control_b: DeclarationRef = decl_ref(module_path: "test.fixture.native", decl_name: "beta_red_control") -data deleted_subject: DeclarationRef = decl_ref(module_path: "test.fixture.subject", decl_name: "gamma_subject") +// EVERY CITATION HERE NAMES A DECLARATION THAT EXISTS, and it is this module's own. The required +// floor resolves every decl_ref in the corpus (CITED-MODULE-ABSENT refused the first push of this +// file, which cited invented fixture modules), so a plant may be absent from a ROSTER but never from +// the TREE. Roles are carried by the declaration names; membership is what each roster controls. +data fixture_module: String = "test.fixture.v1_witness_census.specimens" +data claim_a: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "claim_a") +data claim_b: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "claim_b") +data claim_c: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "claim_c") +data claim_delta_unaccounted: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "claim_delta_unaccounted") +data claim_never_in_roster: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "claim_never_in_roster") + +data native_a: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "native_a") +data native_b: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "native_b") +data control_b: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "control_b") +data deleted_subject: DeclarationRef = decl_ref(module_path: fixture_module, decl_name: "deleted_subject") fn v1wc_fixture_row(identity: DeclarationRef, standing: RequiredFloorDisposition, disposition: ClaimCutoverDisposition) -> V1ClaimCutoverRow { { pre_cutover_identity: identity, floor_standing: standing, disposition: disposition } @@ -49,32 +56,20 @@ data clean_rows: List = [ }), ] -data clean_roster: List = [ - "test.fixture.claim::alpha", - "test.fixture.claim::beta", - "test.fixture.claim::gamma", -] +data clean_roster: List = [ claim_a, claim_b, claim_c ] data clean_population: ClaimPopulation = ClaimRosterComplete { rows: clean_rows, roster_producer: "controlled fixture; no floor run" } // PLANT ONE -- a roster identity with no row. The lost subject in its purest form. -data planted_unaccounted_roster: List = [ - "test.fixture.claim::alpha", - "test.fixture.claim::beta", - "test.fixture.claim::gamma", - "test.fixture.claim::delta", -] +data planted_unaccounted_roster: List = [ claim_a, claim_b, claim_c, claim_delta_unaccounted ] // PLANT TWO -- a row for a claim the roster does not contain. Row count unchanged, subject invented. data planted_fabricated_rows: List = [ v1wc_fixture_row(identity: claim_a, standing: Planned, disposition: StillRequired { surviving_subject: claim_a, native_identity: native_a }), - v1wc_fixture_row(identity: decl_ref(module_path: "test.fixture.claim", decl_name: "never_existed"), standing: Planned, disposition: StillRequired { surviving_subject: claim_b, native_identity: native_b }), + v1wc_fixture_row(identity: claim_never_in_roster, standing: Planned, disposition: StillRequired { surviving_subject: claim_b, native_identity: native_b }), ] -data planted_fabricated_roster: List = [ - "test.fixture.claim::alpha", - "test.fixture.claim::never_existed_not_in_roster", -] +data planted_fabricated_roster: List = [ claim_a, claim_delta_unaccounted ] data planted_fabricated_population: ClaimPopulation = ClaimRosterComplete { rows: planted_fabricated_rows, roster_producer: "controlled fixture" } @@ -85,7 +80,7 @@ data planted_merged_rows: List = [ v1wc_fixture_row(identity: claim_b, standing: Planned, disposition: StillRequired { surviving_subject: claim_b, native_identity: native_a }), ] -data planted_merged_roster: List = [ "test.fixture.claim::alpha", "test.fixture.claim::beta" ] +data planted_merged_roster: List = [ claim_a, claim_b ] data planted_merged_population: ClaimPopulation = ClaimRosterComplete { rows: planted_merged_rows, roster_producer: "controlled fixture" } @@ -99,7 +94,7 @@ data planted_self_control_rows: List = [ }), ] -data planted_self_control_roster: List = [ "test.fixture.claim::beta" ] +data planted_self_control_roster: List = [ claim_b ] data planted_self_control_population: ClaimPopulation = ClaimRosterComplete { rows: planted_self_control_rows, roster_producer: "controlled fixture" } @@ -114,7 +109,7 @@ data planted_fixture_member_rows: List = [ }), ] -data planted_fixture_member_roster: List = [ "test.fixture.claim::alpha", "test.fixture.claim::gamma" ] +data planted_fixture_member_roster: List = [ claim_a, claim_c ] data planted_fixture_member_population: ClaimPopulation = ClaimRosterComplete { rows: planted_fixture_member_rows, roster_producer: "controlled fixture" } From dc9d3e16653f8a64b1b0c25814b11531889526a0 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 13:49:59 +0000 Subject: [PATCH 3/7] Adjudicate the prefix relocation: six TargetChanged transition-admission rows, blast radius 0 The witness floor was green on the previous push (planned=executed=2829, failed=0); the namespace-wave-admission phase refused 6 unadjudicated binding deltas -- every spelling of the four rust_source_prefix_* constants now binds to gunbc.rust_item_host_observation instead of the scaffold. The rows name each exact (module, enclosing declaration, leaf) and go stale by the trigger the roster already carries: the moment #9675 merges. cargo test -p v1-compiler --test namespace_wave_admission: 33 passed. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- src/v1/stage0/src/namespace_wave_admission.rs | 65 ++++++++++++++++++- 1 file changed, 64 insertions(+), 1 deletion(-) diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index 4fa2876b39a..97d11e53f93 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -367,7 +367,70 @@ pub struct TransitionAdmission { /// the shape the paragraph above records for the first 53. Removed by the trigger they were /// authored with. The roster is EMPTY and empty is not permissive: a run carrying a real /// namespace delta still refuses it as UNADJUDICATED until its author adds a row here. -pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[]; +/// FOURTH ENTRY, SAME RULE (2026-08-29, gunbc#9675). The four `rust_source_prefix_*` constants +/// moved from `gunbc.stage0_rust_source_lifecycle_scaffold` to `gunbc.rust_item_host_observation` +/// -- the namespace table there needs the tooling prefix, and importing it the other way closes +/// the cycle scaffold -> seed_growth_admission -> host_observation. Every spelling that bound to +/// the old declarer now binds to the new one: six `TargetChanged` rows, each naming the exact +/// module, enclosing declaration and leaf, blast radius 0 on every one. These rows go STALE the +/// moment #9675 merges (base and head then both carry the relocation) and are removed by that +/// trigger, exactly as the three shrinks above were. +pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[ + TransitionAdmission { + label: "rust-source-prefix-relocation-01", + subject: AdmissionSubject::Binding { + module: "gunbc.stage0_rust_product_reachability", + in_declaration: "path_is_test_harness", + spelling: "rust_source_prefix_stage0_test", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "rust-source-prefix-relocation-02", + subject: AdmissionSubject::Binding { + module: "gunbc.stage0_rust_product_reachability", + in_declaration: "path_is_test_harness", + spelling: "rust_source_prefix_test_harness", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "rust-source-prefix-relocation-03", + subject: AdmissionSubject::Binding { + module: "gunbc.stage0_rust_source_lifecycle_scaffold", + in_declaration: "rust_source_discovery_prefix_hints", + spelling: "rust_source_prefix_stage0_example", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "rust-source-prefix-relocation-04", + subject: AdmissionSubject::Binding { + module: "gunbc.stage0_rust_source_lifecycle_scaffold", + in_declaration: "rust_source_discovery_prefix_hints", + spelling: "rust_source_prefix_stage0_test", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "rust-source-prefix-relocation-05", + subject: AdmissionSubject::Binding { + module: "gunbc.stage0_rust_source_lifecycle_scaffold", + in_declaration: "rust_source_discovery_prefix_hints", + spelling: "rust_source_prefix_test_harness", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "rust-source-prefix-relocation-06", + subject: AdmissionSubject::Binding { + module: "gunbc.stage0_rust_source_lifecycle_scaffold", + in_declaration: "rust_source_discovery_prefix_hints", + spelling: "rust_source_prefix_tooling", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, +]; /// The denominators a green must name (DESIGN ยง5). A run that cannot say what it covered is /// an instrument failure wearing coverage's clothes. From dbb161638f614feee57389863fa6ac810530e671 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 14:56:06 +0000 Subject: [PATCH 4/7] The producer names the tree it observed, and the live gate is asserted false by execution - DiscoveryProducer.source_revision is std.types CommitSha and it gains source_tree: v2.workflow.floor_discovery FloorDiscoveryTreeId, built from the tree of the measured revision (f1f9dd8a077 -> d806b7d086ef). A String revision is a spelling any later tree can wear; the tree is what the floor keys a discovery on, so after #9676 the population reads as an observation of an OLDER tree until it is rebound -- a visible typed edit rather than a stale string. - consumer_census_live_gate_refuses_even_with_every_successor_realized: v1_bankruptcy_transaction_admitted over the live population is FALSE, including with every claimed successor handed to the gate as realized. 22 witnesses PASS (claim_batch on BuildBuddy). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- dag/gunbc/v1/v1_consumer_census.dag | 28 ++++++++++++++++--- .../claim/v1_consumer_census_witness_test.dag | 13 ++++++++- .../fixture/v1_consumer_census/specimens.dag | 3 +- 3 files changed, 38 insertions(+), 6 deletions(-) diff --git a/dag/gunbc/v1/v1_consumer_census.dag b/dag/gunbc/v1/v1_consumer_census.dag index 877645d5f81..a9a043a2b47 100644 --- a/dag/gunbc/v1/v1_consumer_census.dag +++ b/dag/gunbc/v1/v1_consumer_census.dag @@ -1,6 +1,9 @@ module gunbc.v1_consumer_census -import std.types { List, String, NonEmptyStr, FilePath, Bool, Int } +import std.types { List, String, NonEmptyStr, FilePath, CommitSha, Bool, Int } +import std.content_hash { Sha1Digest } +import extdeps.git.object_store { GitObjectId, GitSha1ObjectId } +import v2.workflow.floor_discovery { FloorDiscoveryTreeId, floor_discovery_tree_id } import std.decl_ref { DeclarationRef, decl_ref } import v2.std.algebra { fold_list, list_append, list_snoc_item } import std.dissolution { DissolutionCondition, unbound_dissolution } @@ -96,11 +99,19 @@ data v1_consumer_census_producer_note: String = "EVERY ROW NAMES THE INSTRUMENT type DiscoveryProducer { instrument: String command: String - source_revision: String + source_revision: CommitSha + source_tree: FloorDiscoveryTreeId } -fn discovery_producer(instrument: String, command: String, source_revision: String) -> DiscoveryProducer { - DiscoveryProducer { instrument: instrument, command: command, source_revision: source_revision } +data v1_consumer_census_binding_note: String = "THE REVISION AND THE TREE ARE TYPED, AND THE TREE IS THE ONE THAT DECIDES. A String revision is a spelling that any later tree can wear; std.types CommitSha is the Git-head vocabulary every consumer already names, and v2.workflow.floor_discovery FloorDiscoveryTreeId is what the floor itself keys a discovery on -- a tree, not a commit, because two commits can carry one tree and one commit is an observation of exactly one. Carrying both makes a row say which tree it observed, so that after an upstream change lands (XL-0, #9676) the census reads as an observation of an OLDER tree rather than as a current fact, and the rebind is a visible edit to two typed fields rather than a stale string nobody re-reads (XL-N Manager ruling, 2026-08-29)." + +fn discovery_producer(instrument: String, command: String, source_revision: String, source_tree_hex: String) -> DiscoveryProducer { + DiscoveryProducer { + instrument: instrument, + command: command, + source_revision: source_revision as CommitSha, + source_tree: floor_discovery_tree_id(object_id: GitSha1ObjectId { digest: Sha1Digest { hex: source_tree_hex } }), + } } // THE ROW. The relation itself -- consumer x consumed_old_authority x disposition -- is the @@ -210,46 +221,55 @@ data v1_consumer_census_population_dissolution: DissolutionCondition = unbound_d data v1_census_revision: String = "f1f9dd8a077f976c48d389201a2c41e54ccd0c15" +data v1_census_tree: String = "d806b7d086efa5e2599060076d4ee8dd61a1168c" + data producer_workflow_argv: DiscoveryProducer = discovery_producer( instrument: "argv and cargo invocations in the emitted workflow surface, traced back to the .dag step declaration that emits each one", command: "grep -nE 'target/release/|cargo (build|test).*v1-compiler' .github/workflows/*.yml; then the emitting declaration in gunbc.witness_floor_workflow / gunbc.fleet_desired_admission_workflow / gunbc.fleet_converge_workflow", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) data producer_cargo_manifest_graph: DiscoveryProducer = discovery_producer( instrument: "path dependencies among the v1 crate manifests and the workspace member region", command: "git grep -n 'path = \"\\.\\./stage0' -- '*/Cargo.toml'; sed -n 1,20p Cargo.toml", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) data producer_rust_bridge_edge: DiscoveryProducer = discovery_producer( instrument: "v1_rt references in Rust outside src/v1, each projected through gunbc.rust_item_host_observation item_declaration_ref", command: "git grep -l 'v1_rt' -- '*.rs' | grep -v '^src/v1'", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) data producer_generated_mirror: DiscoveryProducer = discovery_producer( instrument: "the committed generated Rust under src/v1, defined by its header rather than by basename, and the .gitattributes rows projected from the artifact registry", command: "grep -rl 'Generated by' src/v1 --include=*.rs | wc -l; grep -c 'generated-artifact' .gitattributes", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) data producer_serialized_artifact: DiscoveryProducer = discovery_producer( instrument: "the receipt paths the required workflow uploads, read from the declarations that name them", command: "grep -oE '[a-z_]+\\.tsv' .github/workflows/witnesses.yml | sort -u; git grep -nE '^data [a-z_]+_path: String = \"[a-z_]+\\.tsv\"' -- dag/gunbc/witness/witness_floor_workflow.dag", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) data producer_git_hook: DiscoveryProducer = discovery_producer( instrument: "v1 binary invocations inside the repository-local git hooks, traced to the emitting declaration", command: "git grep -n 'target/release' .githooks/; git grep -ln 'generated-artifact-merge' -- 'dag/**/*.dag'", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) data producer_bin_roster_row: DiscoveryProducer = discovery_producer( instrument: ".dag roster rows that enumerate v1 binary names for a workflow to build", command: "git grep -n 'ci_floor_invoked_bins\\|witness_declared_release_bins' -- 'dag/gunbc/**/*.dag'", source_revision: v1_census_revision, + source_tree_hex: v1_census_tree, ) // IDENTITIES, declared once each. The Rust-item identities follow gunbc.rust_item_host_observation diff --git a/dag/test/claim/v1_consumer_census_witness_test.dag b/dag/test/claim/v1_consumer_census_witness_test.dag index fe6e5820944..5cfbf5d45e6 100644 --- a/dag/test/claim/v1_consumer_census_witness_test.dag +++ b/dag/test/claim/v1_consumer_census_witness_test.dag @@ -8,7 +8,7 @@ import gunbc.v1_consumer_census { v1_every_discovered_consumer_disposed, v1_every_row_names_a_live_consumer, v1_every_claimed_successor_is_realized, v1_bankruptcy_transaction_admitted, v1_blocking_consumer_count, v1_consumer_member_count, v1_boundary_census, consumer_population_is_complete, consumer_population_rows, consumer_population_uncitable, - v1_shim_partition, v1_shim_items, v1_consumer_population_for + v1_shim_partition, v1_shim_items, v1_consumer_population_for, v1_claimed_successors } import test.fixture.v1_consumer_census.specimens { clean_rows, clean_discovered, clean_realized, clean_population, @@ -120,6 +120,16 @@ fn the_live_transaction_refuses_for_recorded_reasons() -> Bool { && v1_blocking_consumer_count() < v1_consumer_member_count() } +// THE GATE ITSELF, EXECUTED ON THE LIVE POPULATION. The assertion above establishes the reasons; +// this one establishes the verdict, and against the most generous realized population that can be +// written -- every successor this census claims, handed to the gate as realized -- so the false +// cannot be coming from an unrealized successor. It comes from the population being a lower bound +// and from blocking consumers, which are the two facts XL-5's gate has not yet discharged. +fn the_live_gate_refuses_even_with_every_successor_realized() -> Bool { + !v1_bankruptcy_transaction_admitted(population: v1_consumer_population(), realized: []) + && !v1_bankruptcy_transaction_admitted(population: v1_consumer_population(), realized: v1_claimed_successors(rows: v1_consumers())) +} + // THE ROSTER AND THE POPULATION NAME ONE LIST. Two declarations naming one list can disagree in // exactly one way -- an author filing a row and forgetting the population -- which would leave a // consumer recorded and unread by the gate. @@ -138,4 +148,5 @@ test fn consumer_census_boundary_census_enumerates_the_rows() -> Bool { boundary test fn consumer_census_tooling_row_decides_shim_citability() -> Bool { the_tooling_row_decides_shim_citability() } test fn consumer_census_population_carries_the_partition() -> Bool { the_population_carries_the_partition() } test fn consumer_census_live_transaction_refuses_for_recorded_reasons() -> Bool { the_live_transaction_refuses_for_recorded_reasons() } +test fn consumer_census_live_gate_refuses_even_with_every_successor_realized() -> Bool { the_live_gate_refuses_even_with_every_successor_realized() } test fn consumer_census_live_population_carries_the_whole_roster() -> Bool { the_live_population_carries_the_whole_roster() } diff --git a/dag/test/fixture/v1_consumer_census/specimens.dag b/dag/test/fixture/v1_consumer_census/specimens.dag index 283f50461b9..5416589a15f 100644 --- a/dag/test/fixture/v1_consumer_census/specimens.dag +++ b/dag/test/fixture/v1_consumer_census/specimens.dag @@ -28,7 +28,8 @@ fn v1cc_fixture_nes(s: String) -> NonEmptyStr { s as NonEmptyStr } data fixture_producer: DiscoveryProducer = discovery_producer( instrument: "hand-authored fixture; no tree was measured", command: "none -- this row is a controlled specimen and must never be read as a live observation", - source_revision: "fixture", + source_revision: "0000000000000000000000000000000000000000", + source_tree_hex: "0000000000000000000000000000000000000000", ) // EVERY CITATION HERE NAMES A DECLARATION THAT EXISTS, and it is this module's own. The required From 37dfabadb7bce395afe1e8104740fec32eeb712f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 30 Aug 2026 02:44:21 +0000 Subject: [PATCH 5/7] Rebind the live measurement to the post-#9676 tree; the fixture-member projection eliminates the two new floor standings Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- dag/gunbc/v1/v1_consumer_census.dag | 6 +++--- dag/gunbc/v1/v1_witness_census.dag | 5 ++++- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/v1/v1_consumer_census.dag b/dag/gunbc/v1/v1_consumer_census.dag index a9a043a2b47..f5c297e5987 100644 --- a/dag/gunbc/v1/v1_consumer_census.dag +++ b/dag/gunbc/v1/v1_consumer_census.dag @@ -219,9 +219,9 @@ data v1_consumer_census_population_dissolution: DissolutionCondition = unbound_d // THE PRODUCERS. One declaration per instrument, so a row cites a producer rather than restating a // command, and re-deriving the whole census is reading the commands below rather than every row. -data v1_census_revision: String = "f1f9dd8a077f976c48d389201a2c41e54ccd0c15" +data v1_census_revision: String = "4012c89dcbccc0307430e965e5637dc01f4ddf0e" -data v1_census_tree: String = "d806b7d086efa5e2599060076d4ee8dd61a1168c" +data v1_census_tree: String = "a47ed8804543badf16f157e8002ba18d1e5f3ba9" data producer_workflow_argv: DiscoveryProducer = discovery_producer( instrument: "argv and cargo invocations in the emitted workflow surface, traced back to the .dag step declaration that emits each one", @@ -550,7 +550,7 @@ fn v1_consumer_population_for(rows: List) -> ConsumerPop PopulationMeasuredLowerBound { rows: list_append(left: v1_static_consumers, right: partition.cited), uncitable: partition.uncitable, - missing_basis: "seven per-medium sweeps, unjoined. Three named holes, each of which would produce a row this roster does not have: (1) no producer classifies the .dag argv rows -- 85 .dag files name a v1 binary in a string position and only the two ci_release_bins rosters were traced to a consumer; (2) the deletion-set blind spot the floor cut measured has one row here (workspace_members) and no instrument -- a consumer defined inside src/v1 and consumed inside src/v1 cannot refuse when both go, and only a per-deleted-file question finds the rest; (3) reachability is not measured for any row: every disposition above is a PRESENCE claim, and presence over-approximates demand, which is the reachability_read_as_occupancy class this repository rosters and XL-1 tripped on in its own first census. The uncitable column is NOT a fourth hole any more: under the live namespace table it is empty by construction, and the tooling row that made it so was necessary for Complete, not sufficient.", + missing_basis: "seven per-medium sweeps, unjoined. Three named holes, each of which would produce a row this roster does not have: (1) no producer classifies the .dag argv rows -- 88 .dag files name a v1 binary in a string position and only the two ci_release_bins rosters were traced to a consumer; (2) the deletion-set blind spot the floor cut measured has one row here (workspace_members) and no instrument -- a consumer defined inside src/v1 and consumed inside src/v1 cannot refuse when both go, and only a per-deleted-file question finds the rest; (3) reachability is not measured for any row: every disposition above is a PRESENCE claim, and presence over-approximates demand, which is the reachability_read_as_occupancy class this repository rosters and XL-1 tripped on in its own first census. The uncitable column is NOT a fourth hole any more: under the live namespace table it is empty by construction, and the tooling row that made it so was necessary for Complete, not sufficient.", } } diff --git a/dag/gunbc/v1/v1_witness_census.dag b/dag/gunbc/v1/v1_witness_census.dag index 6073ae9cadc..59c43fad194 100644 --- a/dag/gunbc/v1/v1_witness_census.dag +++ b/dag/gunbc/v1/v1_witness_census.dag @@ -5,7 +5,8 @@ import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } import std.dissolution { DissolutionCondition, unbound_dissolution } import gunbc.replacement_cut { EvidenceDisposition, ReenrollAgainstY, ReplaceEvidence, RetireEvidence } import v2.workflow.required_floor { - RequiredFloorDisposition, Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedOutsideRequiredGate, DeclinedCostDebt + RequiredFloorDisposition, Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedOutsideRequiredGate, + DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded, DeclinedCostDebt } // XL-5's SECOND DELIVERABLE: the wall that stops the bankruptcy transaction greening by LOSING @@ -93,6 +94,8 @@ fn floor_standing_is_fixture_member(s: RequiredFloorDisposition) -> Bool { DeclinedLongModule { matched_prefix: _ } => false DeclinedFixtureMember { matched_prefix: _ } => true DeclinedOutsideRequiredGate => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false DeclinedCostDebt => false } } From 30e59856183b98d4ae789bed301a44510bff1278 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 30 Aug 2026 02:45:24 +0000 Subject: [PATCH 6/7] Rebind the live measurement to the tree that includes the Symbol authority (24fc4a39); the seven producers agree with the prior measurement Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- dag/gunbc/v1/v1_consumer_census.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/v1/v1_consumer_census.dag b/dag/gunbc/v1/v1_consumer_census.dag index f5c297e5987..9d635182e7d 100644 --- a/dag/gunbc/v1/v1_consumer_census.dag +++ b/dag/gunbc/v1/v1_consumer_census.dag @@ -219,9 +219,9 @@ data v1_consumer_census_population_dissolution: DissolutionCondition = unbound_d // THE PRODUCERS. One declaration per instrument, so a row cites a producer rather than restating a // command, and re-deriving the whole census is reading the commands below rather than every row. -data v1_census_revision: String = "4012c89dcbccc0307430e965e5637dc01f4ddf0e" +data v1_census_revision: String = "0bdb8dc3a22cd4cb7736b7e83d4df6c132051259" -data v1_census_tree: String = "a47ed8804543badf16f157e8002ba18d1e5f3ba9" +data v1_census_tree: String = "168f313cdd9562ff01334c3ac2d154f4c5db6d96" data producer_workflow_argv: DiscoveryProducer = discovery_producer( instrument: "argv and cargo invocations in the emitted workflow surface, traced back to the .dag step declaration that emits each one", From c59f675e7ae0698cb92ef2e35e5a2699e1887b15 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 30 Aug 2026 03:14:27 +0000 Subject: [PATCH 7/7] The census witnesses enroll in the required gate: renamed under the self_host_ seed prefix, and the tooling-tree projection witness moves out of the main-owned module Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01U7GG6M9N2p7dmqHn4tFtii --- dag/gunbc/rust_item_host_observation.dag | 2 +- ...ust_item_host_observation_witness_test.dag | 15 ------------- ..._host_v1_consumer_census_witness_test.dag} | 22 +++++++++++++++++-- ...f_host_v1_witness_census_witness_test.dag} | 2 +- 4 files changed, 22 insertions(+), 19 deletions(-) rename dag/test/claim/{v1_consumer_census_witness_test.dag => self_host_v1_consumer_census_witness_test.dag} (89%) rename dag/test/claim/{v1_witness_census_witness_test.dag => self_host_v1_witness_census_witness_test.dag} (99%) diff --git a/dag/gunbc/rust_item_host_observation.dag b/dag/gunbc/rust_item_host_observation.dag index bbde80563c4..9fc0f4cac90 100644 --- a/dag/gunbc/rust_item_host_observation.dag +++ b/dag/gunbc/rust_item_host_observation.dag @@ -92,7 +92,7 @@ data rust_source_prefix_tooling: String = "dag/gunbc/instruments/" // citation under it refuse. `v1_compiler` and `v1_compiled` sit outside the .dag index for exactly // that reason. Until this row existed the four shim crates that reach v1_rt were consumers // gunbc.v1_consumer_census could see and the exact cut vocabulary could not spell; removing this -// row returns them to that uncitable state, which test.claim.v1_consumer_census_witness_test +// row returns them to that uncitable state, which test.claim.self_host_v1_consumer_census_witness_test // executes as the falsifier. data rust_source_namespace_rows: List = [ RustSourceNamespaceRow { repo_prefix: "src/v1/stage0/src/bin/", namespace_prefix: "v1_compiler.bin." }, diff --git a/dag/test/claim/rust_item_host_observation_witness_test.dag b/dag/test/claim/rust_item_host_observation_witness_test.dag index 3847e72ead3..0a9042caef7 100644 --- a/dag/test/claim/rust_item_host_observation_witness_test.dag +++ b/dag/test/claim/rust_item_host_observation_witness_test.dag @@ -122,21 +122,6 @@ test fn a_path_no_namespace_row_claims_refuses_rather_than_acquiring_one() -> Bo } } -// THE TOOLING TREE CARRIES THE NAME OF THE PACKAGE IT ASSEMBLES INTO. dag/gunbc/instruments/ is the -// scaffold's rust_source_prefix_tooling; its shim crates are assembled into the `v1_compiled` -// package, so a shim crate root projects to v1_compiled..lib -- a root no .dag module -// declares, like v1_compiler -- and a path one directory up is still unclaimed. -test fn the_tooling_tree_projects_to_the_assembled_package_namespace() -> Bool { - match rust_module_path_for_repo_path(repo_path: "dag/gunbc/instruments/self_host_03_normalize_shims/lib.rs") { - RustModulePathProjected { module_path: path } => path == "v1_compiled.self_host_03_normalize_shims.lib" - RustModulePathRefused { repo_path: _, detail: _ } => false - } - && match rust_module_path_for_repo_path(repo_path: "dag/gunbc/not_instruments/lib.rs") { - RustModulePathRefused { repo_path: _, detail: _ } => true - RustModulePathProjected { module_path: _ } => false - } -} - test fn a_nested_source_path_keeps_its_directory_as_a_namespace_segment() -> Bool { match rust_module_path_for_repo_path(repo_path: "src/v1/stage0/src/cli_run/bare_reference_scanner.rs") { RustModulePathProjected { module_path: path } => path == "v1_compiler.cli_run.bare_reference_scanner" diff --git a/dag/test/claim/v1_consumer_census_witness_test.dag b/dag/test/claim/self_host_v1_consumer_census_witness_test.dag similarity index 89% rename from dag/test/claim/v1_consumer_census_witness_test.dag rename to dag/test/claim/self_host_v1_consumer_census_witness_test.dag index 5cfbf5d45e6..0076265c9bf 100644 --- a/dag/test/claim/v1_consumer_census_witness_test.dag +++ b/dag/test/claim/self_host_v1_consumer_census_witness_test.dag @@ -1,8 +1,11 @@ -module test.claim.v1_consumer_census_witness_test +module test.claim.self_host_v1_consumer_census_witness_test import std.types { Bool } import gunbc.replacement_cut { BoundaryCensus, ConsumersEnumerated, BoundaryDeclaredEmpty } -import gunbc.rust_item_host_observation { RustSourceNamespaceRow, rust_source_namespace_rows, rust_source_prefix_tooling } +import gunbc.rust_item_host_observation { + RustSourceNamespaceRow, rust_source_namespace_rows, rust_source_prefix_tooling, + rust_module_path_for_repo_path, RustModulePathProjected, RustModulePathRefused +} import gunbc.v1_consumer_census { v1_consumers, v1_uncitable_consumers, v1_consumer_population, v1_every_discovered_consumer_disposed, v1_every_row_names_a_live_consumer, v1_every_claimed_successor_is_realized, @@ -150,3 +153,18 @@ test fn consumer_census_population_carries_the_partition() -> Bool { the_populat test fn consumer_census_live_transaction_refuses_for_recorded_reasons() -> Bool { the_live_transaction_refuses_for_recorded_reasons() } test fn consumer_census_live_gate_refuses_even_with_every_successor_realized() -> Bool { the_live_gate_refuses_even_with_every_successor_realized() } test fn consumer_census_live_population_carries_the_whole_roster() -> Bool { the_live_population_carries_the_whole_roster() } + +// THE TOOLING TREE CARRIES THE NAME OF THE PACKAGE IT ASSEMBLES INTO. dag/gunbc/instruments/ is the +// scaffold's rust_source_prefix_tooling; its shim crates are assembled into the `v1_compiled` +// package, so a shim crate root projects to v1_compiled..lib -- a root no .dag module +// declares, like v1_compiler -- and a path one directory up is still unclaimed. +test fn consumer_census_tooling_tree_projects_to_the_assembled_package_namespace() -> Bool { + match rust_module_path_for_repo_path(repo_path: "dag/gunbc/instruments/self_host_03_normalize_shims/lib.rs") { + RustModulePathProjected { module_path: path } => path == "v1_compiled.self_host_03_normalize_shims.lib" + RustModulePathRefused { repo_path: _, detail: _ } => false + } + && match rust_module_path_for_repo_path(repo_path: "dag/gunbc/not_instruments/lib.rs") { + RustModulePathRefused { repo_path: _, detail: _ } => true + RustModulePathProjected { module_path: _ } => false + } +} diff --git a/dag/test/claim/v1_witness_census_witness_test.dag b/dag/test/claim/self_host_v1_witness_census_witness_test.dag similarity index 99% rename from dag/test/claim/v1_witness_census_witness_test.dag rename to dag/test/claim/self_host_v1_witness_census_witness_test.dag index 0afd15e68dc..b02e8c4f0a3 100644 --- a/dag/test/claim/v1_witness_census_witness_test.dag +++ b/dag/test/claim/self_host_v1_witness_census_witness_test.dag @@ -1,4 +1,4 @@ -module test.claim.v1_witness_census_witness_test +module test.claim.self_host_v1_witness_census_witness_test import std.types { Bool } import gunbc.replacement_cut { EvidenceDisposition, ReenrollAgainstY, ReplaceEvidence, RetireEvidence, EvidenceUndecided }