diff --git a/.gitattributes b/.gitattributes index 7f0cf20a378..e13fd124bea 100644 --- a/.gitattributes +++ b/.gitattributes @@ -6,6 +6,9 @@ # Integration policy — deterministic generated projections: provisional ours during merge, # then regenerate from merged authorities before commit (charter four-case policy row 1). +# ROW ORDER IS LOAD-BEARING: the last matching line wins, so the stage0 unset rows must +# follow the stage0 glob. Transposed, they are inert and a hand-maintained file silently +# acquires the driver. .gitattributes merge=generated-artifact .githooks/generated-artifact-merge merge=generated-artifact @@ -77,3 +80,40 @@ docs/plans/value-null-split.md merge=generated-artifact docs/plans/wiring-liveness-preflight.md merge=generated-artifact src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs merge=generated-artifact src/v1/stage0/src/v1_interpreter_dispatch_generated.rs merge=generated-artifact +src/v1/stage0/src/*.rs merge=generated-artifact +src/v1/stage0/Cargo.toml merge=generated-artifact +src/v1/stage0/src/bounded_shell_host_drain.rs !merge +src/v1/stage0/src/census_exclude_derive.rs !merge +src/v1/stage0/src/cli_run.rs !merge +src/v1/stage0/src/codex_app_server_stdio_session.rs !merge +src/v1/stage0/src/coproduct_reflection.rs !merge +src/v1/stage0/src/cssl_seed_linked_closure_assembly.rs !merge +src/v1/stage0/src/data_initializer_identity.rs !merge +src/v1/stage0/src/declaration_index.rs !merge +src/v1/stage0/src/derived_realization_schedule.rs !merge +src/v1/stage0/src/main.rs !merge +src/v1/stage0/src/memory_governor.rs !merge +src/v1/stage0/src/phase_profile.rs !merge +src/v1/stage0/src/pre_push.rs !merge +src/v1/stage0/src/recorded_fixture.rs !merge +src/v1/stage0/src/required_regen_host.rs !merge +src/v1/stage0/src/resolved_graph_cache.rs !merge +src/v1/stage0/src/shared_typecheck_store.rs !merge +src/v1/stage0/src/std_lens_verdict.rs !merge +src/v1/stage0/src/usv_pilot_v2_std_algebra.rs !merge +src/v1/stage0/src/usv_pilot_v2_std_collection.rs !merge +src/v1/stage0/src/usv_pilot_v2_std_node.rs !merge +src/v1/stage0/src/v1_interpreter.rs !merge +src/v1/stage0/src/v2_compiler_body_producer.rs !merge +src/v1/stage0/src/v2_compiler_compile.rs !merge +src/v1/stage0/src/v2_compiler_discovery_enumeration.rs !merge +src/v1/stage0/src/v2_compiler_infer.rs !merge +src/v1/stage0/src/v2_compiler_normalize.rs !merge +src/v1/stage0/src/v2_compiler_parse_engine_hooks.rs !merge +src/v1/stage0/src/v2_compiler_program_assembly.rs !merge +src/v1/stage0/src/v2_compiler_program_partition.rs !merge +src/v1/stage0/src/v2_compiler_resolve.rs !merge +src/v1/stage0/src/v2_compiler_source_authority.rs !merge +src/v1/stage0/src/v2_compiler_target_carriers.rs !merge +src/v1/stage0/src/v2_compiler_tokenize.rs !merge +src/v1/stage0/src/v2_compiler_use_site_verdict.rs !merge diff --git a/Cargo.lock b/Cargo.lock index 393130f2b97..23a4c6c7088 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -951,7 +951,6 @@ dependencies = [ "v1-stage0-runtime", "v1-stage0-std-core", "v1-stage0-std-surface", - "v1-stage0-v1-infer", ] [[package]] @@ -968,6 +967,7 @@ dependencies = [ "v1-stage0-runtime", "v1-stage0-std-core", "v1-stage0-std-surface", + "v1-stage0-v1-artifact", ] [[package]] diff --git a/dag/gunbc/generated_projection_paths.dag b/dag/gunbc/generated_projection_paths.dag index 4ac830e49a2..24bd7eb7e95 100644 --- a/dag/gunbc/generated_projection_paths.dag +++ b/dag/gunbc/generated_projection_paths.dag @@ -1,6 +1,11 @@ module gunbc.generated_projection_paths import gunbc.generated_artifact { committed_generated_artifact_paths } +import gunbc.stage0_cargo_manifest { stage0_cargo_toml_repo_path } +import gunbc.stage0_rust_source_lifecycle_scaffold { + derived_hand_maintained_disposition_repo_paths, + stage0_src_repo_prefix +} import std.types { List, String } // One source remains after the stage0_emit_plan deletion, so a row is its path. The @@ -52,3 +57,105 @@ fn deterministic_generated_projection_paths() -> GeneratedProjectionPathsOutcome |> map(path => GeneratedProjectionPathRow { path: path }) deterministic_generated_projection_paths_from_rows(rows: rows) } + +// THE STAGE0 ARM IS A COMPLEMENT, NOT A ROSTER, AND THAT IS THE WHOLE CONSTRUCTION. +// +// The stage0 seed mirror is the artifact the generated-artifact merge driver was written for +// (DESIGN records the #7836 receipt: the ours side dropped authority-derived bytes twice, +// against this mirror). Its arm routed through gunbc.stage0_emit_plan, which the #8406 regen +// cut deleted at the root. Nothing refused, because the consumer that needed it — this module — +// was outside the deletion census, so the population silently narrowed to the committed +// registry and every emitted stage0 source lost its merge attribute. +// +// A PATH LIST CANNOT BE THE REPAIR, IN EITHER OF ITS TWO SPELLINGS. A hand roster is what stood +// in for the dead derivation before and is what #8674 deleted; and the live derivation that +// replaced it (gunbc.stage0_rust_source_lifecycle_scaffold derived_generated_stage0_repo_paths) +// takes two OBSERVATIONS as its inputs — git ls-files and a git show of the emitted-population +// manifest. Reaching it from here would make a committed byte projection a function of somebody's +// working tree: two clones at one commit could disagree about what .gitattributes must contain, +// and the drift gate would then refuse or pass on a fact about a checkout rather than about the +// model. So the arm is rebuilt from the pure half of the same authority instead. +// +// The pure half is the crate layout's own claim. hand_maintained_stage0_filenames() names every +// direct child of the stage0 source root that is NOT emitted, and Git attributes express a +// complement directly, because the last matching line wins and `!attr` unsets: one glob claims +// the directory's direct children and one unset row per hand-maintained member takes them back +// out. A newly emitted stage0 file is then covered BY CONSTRUCTION — nobody has to remember it, +// which is exactly the failure that produced this defect, and the reason the class does not go +// back to a roster that goes stale between authoring and merge. +// +// THE ORDER OF THESE ROWS IS A CORRECTNESS PROPERTY AND IT FAILS SILENTLY. Last match wins, so +// an unset row emitted ABOVE the glob is inert — and inert in the dangerous direction, since the +// hand-maintained file then silently acquires the driver with no diagnostic anywhere. The glob is +// therefore constructed ahead of the unsets here rather than sorted into them, and +// test.claim.generated_projection_merge_rows_witness reds when the two are transposed. +// +// THE OVER-CLAIM IS THE SAFE DIRECTION, WHICH IS WHY COVERAGE-BY-DEFAULT IS ADMISSIBLE HERE AND +// #8674 REJECTED THE SAME COMPLEMENT FOR ITS OWN QUESTION. That module classifies maintenance +// disposition, where a complement makes an unregistered file "generated" by definition and drives +// the unclassified refusal's firing rate to zero — an absorbing arm. This module answers a +// different question with asymmetric failure directions: an over-claimed hand file gets a LOUD +// driver refusal at merge time, recoverable in place; an under-claimed generated file gets a +// SILENT text merge that drops authority-derived bytes. The complement errs toward the loud one. +// +// THE UNSET POPULATION IS LAYOUT MEMBERSHIP MINUS THE ARTIFACT REGISTRY, and that subtraction is +// load-bearing rather than defensive: bootstrap_stage0_crate_layout_generated.rs and +// v1_interpreter_dispatch_generated.rs are BOTH hand_maintained_stage0_filenames() members (they +// are pub-mod-declared by hand) and registry artifacts already carrying the attribute today. An +// unset row for either would REMOVE working coverage. derived_hand_maintained_disposition_repo_paths() +// is the existing authority for exactly that difference; this module joins it rather than +// recomputing it. +data stage0_generated_source_complement_note: String = "Cross-authority receipt for the complement, measured at d311b1ceab: the stage0 source root holds 173 direct children and hand_maintained_stage0_filenames() claims 37, so the complement is 136; the emitter's own declaration (src/v1/stage0/src/emitted_population.rs) names 137 direct children. The two agree exactly except main.rs, which is the single emitter_produced_divergent_registrations row — a file the emitter emits and whose committed bytes deliberately diverge from it, so regeneration is NOT its recovery and the unset row is correct. Two independently derived populations agreeing on 136 of 137 is the evidence that the layout claim is the right complement basis. THE FILE HEADER IS NOT THE POPULATION and was tested and rejected as one: 135 files carry '// Generated by v1 compiler -- do not edit.' at that ref, and the header disagrees with the model in BOTH directions — main.rs and std_lens_verdict.rs carry it and are hand-maintained, while compiler_tests.rs, emitted_population.rs and v1_rt.rs lack it and are in the emitted-population manifest." + +type GeneratedProjectionMergeSetting + = MergeGeneratedArtifact + | MergeAttributeUnspecified + +type GeneratedProjectionMergeRow { + pattern: String + setting: GeneratedProjectionMergeSetting +} + +type GeneratedProjectionMergeRowsOutcome + = GeneratedProjectionMergeRowsAccepted { rows: List } + | GeneratedProjectionMergeRowsRefused { cause: GeneratedProjectionPathsRefusal } + +data stage0_generated_source_pattern: String = concat(stage0_src_repo_prefix, "*.rs") + +data stage0_generated_source_pattern_note: String = "A slash-bearing Git attributes pattern does not match across '/', so this claims the DIRECT CHILDREN of the stage0 source root and leaves bin/, cli_run/ and module_path_index/ untouched. That is the correct scope and not a convenient one: every emitted stage0 source is a direct child (measured at d311b1ceab — zero of the emitter-declared sources sit in a subdirectory), and the three subdirectories are hand-maintained Rust the crate layout claim does not enumerate at file grain, so a wider glob would over-claim a population no authority here can take back out." + +fn stage0_generated_projection_merge_rows() -> List { + concat( + [ + GeneratedProjectionMergeRow { + pattern: stage0_generated_source_pattern, + setting: MergeGeneratedArtifact + }, + GeneratedProjectionMergeRow { + pattern: stage0_cargo_toml_repo_path, + setting: MergeGeneratedArtifact + } + ], + derived_hand_maintained_disposition_repo_paths() + |> sort_by(path => path) + |> map(path => GeneratedProjectionMergeRow { + pattern: path, + setting: MergeAttributeUnspecified + }) + ) +} + +fn deterministic_generated_projection_merge_rows() -> GeneratedProjectionMergeRowsOutcome { + match deterministic_generated_projection_paths() { + GeneratedProjectionPathsRefused { cause } => GeneratedProjectionMergeRowsRefused { cause: cause } + GeneratedProjectionPathsAccepted { paths } => GeneratedProjectionMergeRowsAccepted { + rows: concat( + paths |> map(path => GeneratedProjectionMergeRow { + pattern: path, + setting: MergeGeneratedArtifact + }), + stage0_generated_projection_merge_rows() + ) + } + } +} diff --git a/dag/gunbc/gitattributes_emit.dag b/dag/gunbc/gitattributes_emit.dag index 259eeaefa19..7d2e30477d6 100644 --- a/dag/gunbc/gitattributes_emit.dag +++ b/dag/gunbc/gitattributes_emit.dag @@ -1,23 +1,46 @@ module gunbc.gitattributes_emit import gunbc.generated_projection_paths { - GeneratedProjectionPathsAccepted, - GeneratedProjectionPathsRefused, - deterministic_generated_projection_paths + GeneratedProjectionMergeRow, + GeneratedProjectionMergeSetting, + GeneratedProjectionMergeRowsAccepted, + GeneratedProjectionMergeRowsRefused, + MergeAttributeUnspecified, + MergeGeneratedArtifact, + deterministic_generated_projection_merge_rows } type GitattributesGenerationOutcome = GitattributesGenerated { content: String } | GitattributesGenerationRefused -data gitattributes_emit_authority_note: String = "THE committed byte projection through which Git receives the relevant subset of the modeled repository-path policy (generated-file conflict policy charter, lane 2, operator-ruled 2026-08-01). Presentation-policy rows (linguist) and integration-policy rows (merge driver attribute) are orthogonal facts derived from separate authorities — generated provenance does not imply linguist-hidden, and neither row is hand-authored in the committed file. The merge-attribute population is gunbc.generated_projection_paths.deterministic_generated_projection_paths(), joining committed generated artifacts with plan-derived stage0 Rust and refusing duplicate paths before row emission; committed_generated_artifact_paths() remains the heal/registry authority. .gitattributes classifies itself through the same derivation with no handwritten self-row. The merge-driver DEFINITION lives in repository-local Git config (gunbc.repo_local_git_config), not in this file." +data gitattributes_emit_authority_note: String = "THE committed byte projection through which Git receives the relevant subset of the modeled repository-path policy (generated-file conflict policy charter, lane 2, operator-ruled 2026-08-01). Presentation-policy rows (linguist) and integration-policy rows (merge driver attribute) are orthogonal facts derived from separate authorities — generated provenance does not imply linguist-hidden, and neither row is hand-authored in the committed file. The merge-attribute population is gunbc.generated_projection_paths deterministic_generated_projection_merge_rows(), which joins TWO arms: the committed generated-artifact registry, at exact-path grain with duplicate paths refused before row emission; and the stage0 seed mirror, as a directory glob over the stage0 source root's direct children plus one unset row per hand-maintained member, ordered glob-first because the last matching attributes line wins. THIS SENTENCE PREVIOUSLY DESCRIBED AN ARM THAT DID NOT EXIST — it claimed a join with plan-derived stage0 Rust for months after the #8406 regen cut deleted gunbc.stage0_emit_plan at the root, while the population was in fact the registry alone and every emitted stage0 source carried no merge attribute at all. The prose was the only place the arm survived, which is why it is corrected here rather than quietly widened: a note asserting an arm nobody can execute is what let the gap stand. committed_generated_artifact_paths() remains the heal/registry authority. .gitattributes classifies itself through the same derivation with no handwritten self-row. The merge-driver DEFINITION lives in repository-local Git config (gunbc.repo_local_git_config), not in this file." + + +data generated_projection_paths_join_seam_note: String = "Seam history for the two-arm population. #7609 (operator sequence step 4, 2026-08-01) established deterministic_generated_projection_paths() as the registry roster joined with a stage0 arm derived from gunbc.stage0_emit_plan. The #8406 regen cut deleted that plan at the root and the arm went with it silently, because this consumer sat outside the deletion census. The arm is restored as a COMPLEMENT rather than a path list, for reasons carried at its construction site in gunbc.generated_projection_paths: a path list — hand-authored or derived — leaves the invalid state writable, and the only surviving derived population takes live git observations as inputs, which a committed byte projection may not depend on. Duplicate refusal remains fail-closed inside the registry arm (counted diagnostic), not silent dedup." -data generated_projection_paths_join_seam_note: String = "Seam for #7609 (operator sequence step 4, crisp-bat-830 2026-08-01): merry-deer-815 owns deterministic_generated_projection_paths() = committed_generated_artifact_paths ++ stage0-derived repo paths. Single consumer: generated_projection_merge_policy_lines() below. Duplicate refusal is fail-closed inside that fn (counted diagnostic), not silent dedup. still-carp-272 does not author a parallel join — reviews the stacked #7609 change only." data dag_linguist_presentation_policy_pattern: String = "**/*.dag" data dag_linguist_presentation_policy_attribute: String = "linguist-language=Rust" data generated_projection_merge_attribute: String = "merge=generated-artifact" +// `!attr` is Git's UNSET-AND-DO-NOT-INHERIT spelling, which is the one this needs: the row must +// return the path to `unspecified`, not set the attribute to some other value, so that a +// hand-maintained stage0 source keeps ordinary text merging. Verified by execution against real +// `git check-attr`, glob and unset row together. +data generated_projection_merge_attribute_unset: String = "!merge" + +fn merge_attribute_token(setting: GeneratedProjectionMergeSetting) -> String { + match setting { + MergeGeneratedArtifact => generated_projection_merge_attribute + MergeAttributeUnspecified => generated_projection_merge_attribute_unset + } +} + +fn merge_policy_line(row: GeneratedProjectionMergeRow) -> String { + concat(concat(row.pattern, " "), merge_attribute_token(setting: row.setting)) +} + fn gitattributes_header_lines() -> List { [ "# gunbc .gitattributes — generated from dag/gunbc/gitattributes_emit.dag — do not hand-edit.", @@ -38,12 +61,15 @@ fn generated_projection_merge_policy_lines() -> GitattributesGenerationOutcome { let header = [ "# Integration policy — deterministic generated projections: provisional ours during merge,", "# then regenerate from merged authorities before commit (charter four-case policy row 1).", + "# ROW ORDER IS LOAD-BEARING: the last matching line wins, so the stage0 unset rows must", + "# follow the stage0 glob. Transposed, they are inert and a hand-maintained file silently", + "# acquires the driver.", "" ] - match deterministic_generated_projection_paths() { - GeneratedProjectionPathsRefused { cause: _ } => GitattributesGenerationRefused - GeneratedProjectionPathsAccepted { paths } => GitattributesGenerated { - content: join_lines(lines: concat(header, map(paths, p => concat(concat(p, " "), generated_projection_merge_attribute)))) + match deterministic_generated_projection_merge_rows() { + GeneratedProjectionMergeRowsRefused { cause: _ } => GitattributesGenerationRefused + GeneratedProjectionMergeRowsAccepted { rows } => GitattributesGenerated { + content: join_lines(lines: concat(header, map(rows, row => merge_policy_line(row: row)))) } } } diff --git a/dag/test/claim/generated_projection_merge_rows_witness_test.dag b/dag/test/claim/generated_projection_merge_rows_witness_test.dag new file mode 100644 index 00000000000..3bdc9b0e9f2 --- /dev/null +++ b/dag/test/claim/generated_projection_merge_rows_witness_test.dag @@ -0,0 +1,164 @@ +module test.claim.generated_projection_merge_rows_witness + +import gunbc.generated_projection_paths { + GeneratedProjectionMergeRow, + GeneratedProjectionMergeSetting, + GeneratedProjectionMergeRowsAccepted, + GeneratedProjectionMergeRowsRefused, + MergeAttributeUnspecified, + MergeGeneratedArtifact, + deterministic_generated_projection_merge_rows, + stage0_generated_source_pattern +} +import gunbc.gitattributes_emit { + GitattributesGenerated, + GitattributesGenerationRefused, + expected_gitattributes, + merge_attribute_token, + generated_projection_merge_attribute, + generated_projection_merge_attribute_unset +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// SUBSTRATE INPUTS ONLY, AND THAT IS THE POINT RATHER THAN A CONVENIENCE. The sibling witness +// test.claim.gitattributes_emit_witness reads the committed .gitattributes, so it is +// ReadsLiveTree and the required floor DECLINES it — it is discovered, counted, and never run. +// Every claim below is a function of the model alone, so this module executes where that one +// cannot, which is what makes it evidence rather than specification. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_note: String = "The executing evidence for the stage0 arm of the generated-projection merge-attribute population. THE POPULATION IS THE CANONICAL THING THAT GOES GREEN BY BEING EMPTY, so no claim here is a count: each names an identity and asserts its setting and its POSITION. Two of them are discriminating REDs with different subjects — one goes red if the stage0 arm is absent (the defect this module was authored against, where every emitted stage0 source carried merge: unspecified), one goes red if the glob and the unset rows are transposed (a silent failure with no diagnostic anywhere, since the last matching attributes line wins and an unset row above the glob is inert). EACH WITNESS CARRIES ITS OWN NON-VACUITY PRECONDITION rather than relying on a sibling: an absence claim is TRUE over an empty population, so a witness whose guard lived in another test would go permanently, silently green the day that sibling was renamed — the decoration DESIGN calls worse than absent. The registry-coverage control covers BOTH known members of its class (bootstrap_stage0_crate_layout_generated.rs and v1_interpreter_dispatch_generated.rs), because half a population asserted by prose is not evidence for the other half. Per DESIGN 4b(4) these stay enrolled after they green: they become the regression controls that the arm and its order remain real." + +fn merge_rows() -> List { + match deterministic_generated_projection_merge_rows() { + GeneratedProjectionMergeRowsRefused { cause: _ } => [] + GeneratedProjectionMergeRowsAccepted { rows } => rows + } +} + +type MergeRowIndexScan { + found: Bool + idx: Int +} + +fn scan_index(patterns: List, wanted: String) -> Int { + let scan = fold(patterns, init: MergeRowIndexScan { found: false, idx: 0 }, f: fn(acc, candidate) { + if acc.found { + acc + } else { + if candidate == wanted { + MergeRowIndexScan { found: true, idx: acc.idx } + } else { + MergeRowIndexScan { found: false, idx: acc.idx + 1 } + } + } + }) + if scan.found { scan.idx } else { 0 - 1 } +} + +fn row_index_of(pattern: String) -> Int { + scan_index(patterns: merge_rows() |> map(row => row.pattern), wanted: pattern) +} + +fn emitted_line_index_of(line: String) -> Int { + match expected_gitattributes() { + GitattributesGenerationRefused => 0 - 1 + GitattributesGenerated { content } => + scan_index(patterns: split(s: content, delimiter: "\n"), wanted: line) + } +} + +// Settings are compared through their rendered attribute token rather than by variant equality. +// The token is what Git actually receives, so a claim stated in tokens cannot pass while the +// emitted byte says something else — and it is the same projection the emitter uses, not a second +// spelling of the mapping. +fn setting_token(setting: GeneratedProjectionMergeSetting) -> String { + merge_attribute_token(setting: setting) +} + +fn has_setting(pattern: String, setting: GeneratedProjectionMergeSetting) -> Bool { + merge_rows() |> any(row => + row.pattern == pattern && setting_token(setting: row.setting) == setting_token(setting: setting) + ) +} + +// THE ARM ITSELF. Red before the stage0 arm existed: the emitted population was exactly the +// committed generated-artifact registry, which names no stage0 source glob at all. +test fn witness_stage0_generated_source_glob_is_claimed_holds() -> Bool { + has_setting(pattern: stage0_generated_source_pattern, setting: MergeGeneratedArtifact) + && stage0_generated_source_pattern == "src/v1/stage0/src/*.rs" +} + +// A NAMED EMITTED SOURCE RESOLVES THROUGH THE GLOB AND CARRIES NO UNSET ROW. cli_run.rs would +// resolve to unspecified if it were hand-maintained; v1_compiler_emit_rust.rs is emitted, so no +// unset row may claim it. Naming an identity rather than counting is what keeps this from +// passing vacuously on an empty population. +test fn witness_emitted_stage0_source_is_not_unset_holds() -> Bool { + row_index_of(pattern: stage0_generated_source_pattern) >= 0 + && !has_setting( + pattern: "src/v1/stage0/src/v1_compiler_emit_rust.rs", + setting: MergeAttributeUnspecified + ) +} + +// A HAND-MAINTAINED DIRECT CHILD IS TAKEN BACK OUT. cli_run.rs is on the crate layout's claim +// and is not a registry artifact, so the complement must unset it. +test fn witness_hand_maintained_stage0_source_is_unset_holds() -> Bool { + row_index_of(pattern: stage0_generated_source_pattern) >= 0 + && has_setting(pattern: "src/v1/stage0/src/cli_run.rs", setting: MergeAttributeUnspecified) +} + +// THE SUBTRACTION THAT PROTECTS EXISTING COVERAGE. bootstrap_stage0_crate_layout_generated.rs is +// BOTH a crate-layout member and a registry artifact carrying the attribute today; an unset row +// for it would REMOVE working coverage rather than add any. +fn registry_stage0_artifact_keeps_coverage(path: String) -> Bool { + has_setting(pattern: path, setting: MergeGeneratedArtifact) + && !has_setting(pattern: path, setting: MergeAttributeUnspecified) +} + +test fn witness_registry_artifact_keeps_coverage_holds() -> Bool { + registry_stage0_artifact_keeps_coverage( + path: "src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs" + ) + && registry_stage0_artifact_keeps_coverage( + path: "src/v1/stage0/src/v1_interpreter_dispatch_generated.rs" + ) +} + +// ORDER IS A CORRECTNESS PROPERTY AND FAILS SILENTLY. The last matching attributes line wins, so +// the glob must precede every unset row. Transposed, the unset rows are inert and every +// hand-maintained stage0 source silently acquires the driver, with no diagnostic anywhere. +test fn witness_glob_precedes_every_unset_row_holds() -> Bool { + let glob_index = row_index_of(pattern: stage0_generated_source_pattern) + glob_index >= 0 + && merge_rows() |> all(row => match row.setting { + MergeGeneratedArtifact => true + MergeAttributeUnspecified => row_index_of(pattern: row.pattern) > glob_index + }) +} + +// AND THE ORDER SURVIVES INTO THE BYTES, not only into the row list. The rendered glob line must +// appear before the rendered unset line for a named hand-maintained path. +test fn witness_rendered_order_places_glob_before_unset_holds() -> Bool { + let glob_line = concat(concat(stage0_generated_source_pattern, " "), generated_projection_merge_attribute) + let unset_line = concat(concat("src/v1/stage0/src/cli_run.rs", " "), generated_projection_merge_attribute_unset) + let glob_at = emitted_line_index_of(line: glob_line) + let unset_at = emitted_line_index_of(line: unset_line) + glob_at >= 0 && unset_at >= 0 && glob_at < unset_at +} + +// RED CONTROL: a pattern the model never derives must not appear. +test fn witness_red_unknown_pattern_absent_holds() -> Bool { + !has_setting(pattern: "__gunbc_red_control_absent_pattern__", setting: MergeGeneratedArtifact) + && !has_setting(pattern: "__gunbc_red_control_absent_pattern__", setting: MergeAttributeUnspecified) +} + +test fn witness_holds() -> Bool { + witness_stage0_generated_source_glob_is_claimed_holds() + && witness_emitted_stage0_source_is_not_unset_holds() + && witness_hand_maintained_stage0_source_is_unset_holds() + && witness_registry_artifact_keeps_coverage_holds() + && witness_glob_precedes_every_unset_row_holds() + && witness_rendered_order_places_glob_before_unset_holds() + && witness_red_unknown_pattern_absent_holds() +} diff --git a/docs/plans/generated-file-conflict-policy.md b/docs/plans/generated-file-conflict-policy.md index 9f12090268b..63b959df2eb 100644 --- a/docs/plans/generated-file-conflict-policy.md +++ b/docs/plans/generated-file-conflict-policy.md @@ -193,9 +193,10 @@ projection + the emitted `.gitattributes` itself). ## Lane 3 — derive stage0 output membership (gates the emitted-Rust extension) -**LANDED, BY A DIFFERENT DERIVATION THAN THIS LANE PLANNED.** `generated_stage0_files` -was a handwritten filename list — the second-authority shape exactly — and it is now -deleted. The derivation this lane sketched routed through the stage0 emission plan: +**LANDED, AND THIS SECTION PREVIOUSLY MARKED IT LANDED ON A HALF THAT DID NOT REACH ITS +CONSUMER.** `generated_stage0_files` was a handwritten filename list — the second-authority +shape exactly — and it is deleted. The derivation this lane sketched routed through the +stage0 emission plan: ```text stage0 emission plan → produced module/file identities → canonical output paths @@ -203,19 +204,37 @@ stage0 emission plan → produced module/file identities → canonical output pa ``` That route is not available: `gunbc.stage0_emit_plan` was deleted at the root by the -regen cut (#8406), which is also what left the roster producerless. What landed instead -is the derivation the executing host already performed — `required_regen_host` -`committed_generated_basenames` — lifted into `.dag` as -`gunbc.stage0_rust_source_lifecycle_scaffold derived_generated_stage0_repo_paths`: a direct-child -`.rs` under the stage0 source root that `v2.compiler.self_host.stage0_crate_layout` -does not claim IS generated. Same single authority, reached from the committed tree -rather than from a plan, and it makes `.dag` and the host agree by construction. - -Only after this derivation lands do stage0 emitted `.rs` outputs join the -generated-projection merge policy (lane 2's rows). Extending `.gitattributes` from the -handwritten roster would propagate the existing dual representation into another -generated file. Resolution guidance for emitted `.rs` meanwhile stays: take either side, -rerun `regen_stage0`, verify divergence 0 — never hand-pick hunks. +regen cut (#8406), which is also what left the roster producerless. A derivation did land +in its place — `gunbc.stage0_rust_source_lifecycle_scaffold derived_generated_stage0_repo_paths`, +which reads the emitter's own declared population at a revision and intersects it with the +tracked tree. **The last sentence of the old text — "the derived paths feed the merge-attribute +population" — was never true of it.** The derivation landed; the join this lane names as its own +gate did not, and for months `.gitattributes` covered only the committed generated-artifact +registry while every emitted stage0 source resolved to `merge: unspecified`. That is the artifact +the driver was written for (DESIGN's #7836 receipt is against this mirror), so the driver +protected everything except its own subject. + +**THE JOIN COULD NOT HAVE BEEN MADE THE WAY THIS LANE PLANNED IT, AND THAT IS WHY IT SAT.** +`derived_generated_stage0_repo_paths` takes two live observations — `git ls-files` and a +`git show` of the emitted-population manifest — while `.gitattributes` is a committed byte +projection reached through a pure generator that the drift gate assesses purely. Wiring one to +the other would make the file's expected bytes a function of somebody's working tree: two clones +at one commit could disagree about what it must contain. + +**WHAT LANDED INSTEAD IS A COMPLEMENT, NOT A PATH LIST.** `gunbc.generated_projection_paths` +`deterministic_generated_projection_merge_rows` emits one glob claiming the direct children of +the stage0 source root, followed by one unset row per `v2.compiler.self_host.stage0_crate_layout` +`hand_maintained_stage0_filenames` member that is not itself a registry artifact. Row order is +load-bearing — the last matching attributes line wins, so an unset row above the glob is inert in +the dangerous direction. A newly emitted stage0 source is covered by construction, which is what +a roster of any kind cannot do: the population gained three files during the hours this defect was +being diagnosed. + +**RECOVERY GUIDANCE, CORRECTED.** The old text said to rerun `regen_stage0`. That binary was +deleted by #8406, so the instruction named nothing for as long as it stood. The route is +`claim_executor --required-regen`, and for the generated-artifact registry, `main_wet` on +`dag/tools/generated_artifact_gate.dag`. Take either side, regenerate from the merged +authorities, verify divergence 0 — never hand-pick hunks. **Acceptance wall (operator second-pass review, 2026-08-01):** an Unavailable/Refused source supply cannot project to an ordinary empty list or a syntactically valid generated