Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions dag/gunbc/extdeps_scope_frontier.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
module gunbc.extdeps_scope_frontier

data extdeps_scope_frontier_law: String = "Staged, fail-closed enrollment of the ExternalModelScope requirement (DESIGN §3 'External upstream decomposition'; operator verdicts on gunbc#7556 and gunbc#7571): every extdeps module must eventually carry one extdeps_model_scope: ExternalModelScope declaration. The corpus cannot be gated retroactively red in one change, so enrollment is staged at the storage grain the cover witness walks: every .dag file under dag/extdeps is EXACTLY ONE of scope_carrier_paths (carries a declared scope, admitted by execution), scope_machinery_exempt_paths (the citation vocabulary itself plus synthetic mock corpora — the v2.lens.mandatory_tag region-1 exemption semantics), or a row of the FROZEN legacy manifest (legacy_extdeps_scope_frontier_manifest_path). The live-cover witness (dag/test/claim/external_model_scope_live_cover_witness_test.dag — wet, discovery-excluded per the gunbc.ci_layer_roots wet-integration posture with a documented local recipe; its pure decision fns live HERE and their hermetic RED controls stay discovery-enrolled in dag/test/claim/external_model_scope_witness_test.dag) walks dag/extdeps live, parses the manifest, and refuses any file in none of the three. GRAIN HONESTY (codex review 46258 — the enforcement grain must be stated, not implied): the per-PR MERGE-GATED half is the hermetic one — every rostered path resolves on disk (roster_paths_resolve_on_disk over all three rosters via the filesystem_read checkout carve-out, so a stale or fabricated roster row reds per-PR), the three rosters stay disjoint, carrier files byte-declare the scope, and every pure decision fn keeps its discriminating RED control. The disk-to-roster direction — a NEW dag/extdeps file enrolled in none of the three — and the manifest freeze are ALSO per-PR merge-gated, at diff grain: tools.extdeps_scope_placement_gate (a wet cheap-floor gate added per codex review 46281; its pattern source, the publication placement gate, was later deleted by operator ruling in #7591 — this gate is independent of it) diffs legacy_manifest_freeze_sha..HEAD and refuses any added dag/extdeps .dag file outside carriers-union-machinery (scope_placement_refused_paths) and any manifest row naming a post-freeze-added file (manifest_freeze_holds), with diff failure and parse truncation as refusals, never skips. Diff grain keeps the legacy population green by construction. The wet live-cover witness remains the whole-population re-verification (it walks what IS on disk rather than what the diff says was added) under its documented local recipe. The storage-grain frontier as a whole still dissolves into the v2.lens.mandatory_tag region promotion (compile grain, module-name grain); a new file's only landing states are scope carrier or genuine machinery; it does NOT join the manifest. There are no other exemption channels."
data extdeps_scope_frontier_law: String = "Staged, fail-closed enrollment of the ExternalModelScope requirement (DESIGN §3 'External upstream decomposition'; operator verdicts on gunbc#7556 and gunbc#7571): every extdeps module must eventually carry one extdeps_model_scope: ExternalModelScope declaration. The corpus cannot be gated retroactively red in one change, so enrollment is staged at the storage grain the cover witness walks: every .dag file under dag/extdeps is EXACTLY ONE of scope_carrier_paths (carries a declared scope, admitted by execution), scope_machinery_exempt_paths (the citation vocabulary itself plus synthetic mock corpora — the v2.lens.mandatory_tag region-1 exemption semantics), or a row of the FROZEN legacy manifest (legacy_extdeps_scope_frontier_manifest_path). The live-cover witness (dag/test/claim/external_model_scope_live_cover_witness_test.dag — wet, discovery-excluded per the gunbc.ci_layer_roots wet-integration posture with a documented local recipe; its pure decision fns live HERE and their hermetic RED controls stay discovery-enrolled in dag/test/claim/external_model_scope_witness_test.dag) walks dag/extdeps live, parses the manifest, and refuses any file in none of the three. GRAIN HONESTY (codex review 46258 — the enforcement grain must be stated, not implied): the per-PR MERGE-GATED half is the hermetic one — every rostered path resolves on disk (roster_paths_resolve_on_disk over all three rosters via the filesystem_read checkout carve-out, so a stale or fabricated roster row reds per-PR), the three rosters stay disjoint, carrier files byte-declare the scope, and every pure decision fn keeps its discriminating RED control. The disk-to-roster direction — a NEW dag/extdeps file enrolled in none of the three — and the manifest freeze are ALSO per-PR merge-gated, at diff grain: tools.extdeps_scope_placement_gate (a wet cheap-floor gate added per codex review 46281; its pattern source, the publication placement gate, was later deleted by operator ruling in #7591 — this gate is independent of it) reads TWO bases, one per question: it refuses any dag/extdeps .dag file added by THIS CHANGE (origin/main...HEAD) outside carriers-union-machinery (scope_placement_refused_paths), and refuses any manifest row naming a file added after the freeze anchor over the whole post-freeze population (legacy_manifest_freeze_sha..HEAD, manifest_freeze_holds), with diff failure and parse truncation as refusals, never skips. Merge-base grain on the membership arm is what keeps the refusal attributable to the change that caused it; feeding that arm the freeze base instead made one unrostered file refuse every open branch (gunbc#7644 diagnosis), and the coverage that reading incidentally provided is declared, bounded, and triggered in scope_placement_base_split_note rather than dropped silently. The wet live-cover witness remains the whole-population re-verification (it walks what IS on disk rather than what the diff says was added) under its documented local recipe. The storage-grain frontier as a whole still dissolves into the v2.lens.mandatory_tag region promotion (compile grain, module-name grain); a new file's only landing states are scope carrier or genuine machinery; it does NOT join the manifest. There are no other exemption channels."

data legacy_manifest_shape_note: String = "The legacy population lives OUTSIDE the semantic module as a frozen manifest artifact (operator verdict on gunbc#7571, 2026-08-01: 399 hand-listed rows plus a hand-moved count inside the .dag authority were a second, churn-heavy representation of the extdeps file population). The manifest is one repo-relative path per line; its row count is DERIVED by the parser, never hand-declared; the exact live diff (both directions) is the enforcement. Lifecycle: FROZEN, MECHANICALLY (codex review 46215 — 'review red by inspection' is not enforcement): every manifest row must name a file that already existed at legacy_manifest_freeze_sha, checked by the cover witness against git.Core.DiffNameStatus(freeze..HEAD) — a manifest row for a file added after the freeze refuses (manifest_freeze_holds over PostFreezeObservation), so a new module cannot be smuggled into the legacy population; rows are only ever REMOVED (a module migrates by adding its extdeps_model_scope declaration, moving to scope_carrier_paths, and deleting its manifest row in the same change) — enforced mechanically at line grain by the placement gate, not by review: see manifest_remove_only_note (codex review 46378). Carrier rows are content-verified by the same witness: each scope_carrier_paths file must actually declare extdeps_model_scope on disk, so an asserted-but-undeclared carrier refuses rather than passing on path membership. DISSOLVE-ON: when the manifest drains, the requirement is promoted to a second v2.lens.mandatory_tag region (required_decl_name extdeps_model_scope, required_type_name ExternalModelScope — the same compile-grain wall region 1 already runs for extdeps_external_authority_anchor), at which point the manifest, the parser, the freeze anchor, and the cover witness delete and the module-name grain replaces the storage grain. Paths are discriminators, not gospel (DESIGN §3): the storage grain exists only because the interim cover walker sees files."
data legacy_manifest_shape_note: String = "The legacy population lives OUTSIDE the semantic module as a frozen manifest artifact (operator verdict on gunbc#7571, 2026-08-01: 399 hand-listed rows plus a hand-moved count inside the .dag authority were a second, churn-heavy representation of the extdeps file population). The manifest is one repo-relative path per line; its row count is DERIVED by the parser, never hand-declared; the exact live diff (both directions) is the enforcement. Lifecycle: FROZEN, MECHANICALLY (codex review 46215 — 'review red by inspection' is not enforcement): every manifest row must name a file that already existed at legacy_manifest_freeze_sha, checked by the cover witness against git.Core.DiffNameStatus(freeze..HEAD) — a manifest row for a file added after the freeze refuses (manifest_freeze_holds over DiffAddedObservation), so a new module cannot be smuggled into the legacy population; rows are only ever REMOVED (a module migrates by adding its extdeps_model_scope declaration, moving to scope_carrier_paths, and deleting its manifest row in the same change) — enforced mechanically at line grain by the placement gate, not by review: see manifest_remove_only_note (codex review 46378). Carrier rows are content-verified by the same witness: each scope_carrier_paths file must actually declare extdeps_model_scope on disk, so an asserted-but-undeclared carrier refuses rather than passing on path membership. DISSOLVE-ON: when the manifest drains, the requirement is promoted to a second v2.lens.mandatory_tag region (required_decl_name extdeps_model_scope, required_type_name ExternalModelScope — the same compile-grain wall region 1 already runs for extdeps_external_authority_anchor), at which point the manifest, the parser, the freeze anchor, and the cover witness delete and the module-name grain replaces the storage grain. Paths are discriminators, not gospel (DESIGN §3): the storage grain exists only because the interim cover walker sees files."

data legacy_manifest_freeze_sha_note: String = "The git anchor that makes the manifest's freeze mechanical: the origin/main commit whose tree contains every manifest row. Any file first added AFTER this commit can never be a manifest row (tools.extdeps_scope_placement_gate and the live-cover witness diff freeze..HEAD and refuse the intersection); it must adopt a scope or be genuinely machinery. This anchor never advances while the manifest lives — advancing it would re-open the smuggling channel the freeze closes; it deletes with the manifest on region promotion. ONE recorded re-anchor, in the gate-landing change itself and legitimate exactly once: the original anchor d552ff4036b48bae835f24e9ead322475895d159 predated the gate's existence, and dag/extdeps/languages/lean/overflow.dag (gunbc#7550) then dag/extdeps/project_schedule/cpm_pert.dag (gunbc#7567) merged to main inside that wall-less interim; the anchor moved to the origin/main commit the gate lands against and those rows joined the manifest, because the freeze can only bind from the commit where the wall actually exists. From this commit forward the gate is per-PR merge-gated and the interim class is unreachable."

Expand Down Expand Up @@ -31,18 +31,18 @@ fn carrier_content_declares_scope(content: String) -> Bool {
string_contains(s: content, pattern: "data extdeps_model_scope:")
}

data manifest_freeze_check_note: String = "codex review 46215, finding half 2: the manifest's remove-only lifecycle was review discipline, not mechanics. Closed: every manifest row must name a file that already existed at legacy_manifest_freeze_sha — the live-cover witness diffs freeze..HEAD with the same git.Core.DiffNameStatus + parse the publication placement gate uses, and refuses any manifest row in the added/copied/renamed set. Diff failure and parse truncation are typed refusal arms of PostFreezeObservation, never skips (a broken freeze probe must not report frozen)."
data manifest_freeze_check_note: String = "codex review 46215, finding half 2: the manifest's remove-only lifecycle was review discipline, not mechanics. Closed: every manifest row must name a file that already existed at legacy_manifest_freeze_sha — the live-cover witness diffs freeze..HEAD with the same git.Core.DiffNameStatus + parse the publication placement gate uses, and refuses any manifest row in the added/copied/renamed set. Diff failure and parse truncation are typed refusal arms of DiffAddedObservation, never skips (a broken freeze probe must not report frozen)."

type PostFreezeObservation
= PostFreezeAdded { paths: List<String> }
| PostFreezeDiffFailed
| PostFreezeParseTruncated
type DiffAddedObservation
= AddedPathsObserved { paths: List<String> }
| DiffObserveFailed
| DiffParseTruncated

fn manifest_freeze_holds(manifest: List<String>, observation: PostFreezeObservation) -> Bool {
fn manifest_freeze_holds(manifest: List<String>, observation: DiffAddedObservation) -> Bool {
match observation {
PostFreezeDiffFailed => false
PostFreezeParseTruncated => false
PostFreezeAdded { paths: added } =>
DiffObserveFailed => false
DiffParseTruncated => false
AddedPathsObserved { paths: added } =>
all(manifest, row => !scope_frontier_strings_contain(xs: added, s: row))
}
}
Expand Down Expand Up @@ -112,7 +112,7 @@ fn manifest_line_observation(diff_text: String) -> ManifestLineObservation {
}


data scope_placement_decision_note: String = "The per-PR merge-gated disk-to-roster direction (codex review 46281: the new-file invariant must not wait for the wet lane). scope_placement_refused_paths is the pure decision kernel of tools.extdeps_scope_placement_gate: given the diff-added paths of freeze..HEAD, every added dag/extdeps .dag file must be a member of scope_carrier_paths or scope_machinery_exempt_paths — the frozen manifest is not a landing state for a new file, so it is not consulted for admission (only for the freeze check, manifest_freeze_holds). Diff-grain, so the legacy population stays green by construction: only paths the PR itself adds are judged. The wet live-cover witness remains the whole-population re-verification (walks what IS on disk rather than what the diff SAYS was added)."
data scope_placement_decision_note: String = "The per-PR merge-gated disk-to-roster direction (codex review 46281: the new-file invariant must not wait for the wet lane). scope_placement_refused_paths is the pure decision kernel of tools.extdeps_scope_placement_gate: given the paths a diff reports as ADDED, every such dag/extdeps .dag file must be a member of scope_carrier_paths or scope_machinery_exempt_paths — the frozen manifest is not a landing state for a new file, so it is not consulted for admission (only for the freeze check, manifest_freeze_holds). THE BASE THIS KERNEL IS FED IS THE MERGE BASE origin/main...HEAD, not the freeze anchor (corrected in the gunbc#7644 follow-up; see tools.extdeps_scope_placement_gate scope_placement_base_split_note for the full rationale and the declared coverage narrowing). An earlier revision of this note claimed 'only paths the PR itself adds are judged' while the gate fed the kernel the freeze-base population, so the sentence was true of the INTENT and false of the MECHANISM — the exact defect that let one unrostered file refuse every branch in the fleet. The kernel itself is base-agnostic: it judges whatever added-path list it is handed, which is why the fix was a call-site base and not a change here. The wet live-cover witness remains the whole-population re-verification (walks what IS on disk rather than what the diff SAYS was added)."

fn scope_placement_refused_paths(added: List<String>, carriers: List<String>, machinery: List<String>) -> List<String> {
added |> filter(p =>
Expand Down
Loading
Loading