diff --git a/dag/extdeps/git/object_store.dag b/dag/extdeps/git/object_store.dag index f78a4ba3352..57082eb80d0 100644 --- a/dag/extdeps/git/object_store.dag +++ b/dag/extdeps/git/object_store.dag @@ -303,6 +303,49 @@ type GitObjectId = GitSha1ObjectId { digest: GitSha1Digest } | GitSha256ObjectId { digest: GitSha256Digest } +data git_object_id_text_note: String = "THE VALIDATING CONSTRUCTORS. The brands GitSha1Digest and GitSha256Digest are ContentHash brands, and a brand alone admits any string: before these existed, a consumer casting text into one could produce a GitSha1ObjectId carrying \"x\", a 64-digit value labelled sha1, or arbitrary non-hex, and every one of those typechecked as a Git object id (review 2026-07-30, on the merge-admission wire parser that did exactly this). Family is not enough — LENGTH and SYNTAX are what make an object id an object id, and they differ per family, which is precisely why the discriminant exists. + +These reuse git_decode_lower_hex_octets rather than introducing a second hex reader, so the canonical form is one authority: git spells object ids in LOWERCASE hex, and an uppercase or mixed-case spelling refuses rather than being folded, because folding would make two textual forms name one object and quietly break the round trip. A caller holding a foreign-cased id normalizes deliberately at its own boundary." + +fn git_sha1_object_id(hex: String) -> GitObjectId? { + if hex.length() != 40 { + none + } else { + match git_decode_lower_hex_octets(text: hex) { + Absent => none + Present { value: _ } => Present { value: GitSha1ObjectId { digest: hex as GitSha1Digest } } + } + } +} + +fn git_sha256_object_id(hex: String) -> GitObjectId? { + if hex.length() != 64 { + none + } else { + match git_decode_lower_hex_octets(text: hex) { + Absent => none + Present { value: _ } => Present { value: GitSha256ObjectId { digest: hex as GitSha256Digest } } + } + } +} + +data git_object_id_eq_note: String = "Format-aware equality, held beside the type rather than in a consumer: two ids of different families are never equal, so a repository mid SHA-1/SHA-256 transition cannot produce a false match on hex alone. It lived briefly in gunbc.merge_admission, which is generic Git behaviour sitting in one consumer — the §3 fork this move closes." + +fn git_object_id_eq(left: GitObjectId, right: GitObjectId) -> Bool { + match left { + GitSha1ObjectId { digest: l } => + match right { + GitSha1ObjectId { digest: r } => (l as ContentHash) == (r as ContentHash) + GitSha256ObjectId { digest: _ } => false + } + GitSha256ObjectId { digest: l } => + match right { + GitSha256ObjectId { digest: r } => (l as ContentHash) == (r as ContentHash) + GitSha1ObjectId { digest: _ } => false + } + } +} + fn git_object_id_format(oid: GitObjectId) -> GitObjectFormat { match oid { GitSha1ObjectId { digest: _ } => GitObjectFormatSha1 diff --git a/dag/gunbc/ci_materialization.dag b/dag/gunbc/ci_materialization.dag index 52cbfec922e..b20cae249c5 100644 --- a/dag/gunbc/ci_materialization.dag +++ b/dag/gunbc/ci_materialization.dag @@ -2,6 +2,7 @@ module gunbc.ci_materialization import std.types { Bool, Int, List, String } +import std.nat { Nat } import std.disposition { Disposition, Scaffold, RealizationDispatch, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } import std.materialization_ladder { @@ -169,7 +170,17 @@ data ci_floor_resolve_receipt_note: String = "The counted cold-resolve receipt o data ci_floor_resolve_receipt_path: String = "target/floor-resolve-receipt.txt" -data ci_floor_declared_resolve_count: Int = 1 +data ci_floor_declared_resolve_count: Nat = 1 + +data floor_finalization_note: String = "The CI floor's post-batch contract, and it lives HERE rather than in std.realization_schedule because it is a fact about THIS floor's duplicate-computation budget, not about walks in general (review 2026-07-30): the generic carrier takes it as a type parameter, so gunbc_ci_floor_plan returns WalkPlan and every other plan returns WalkPlan. WHAT THAT BUYS, narrowly: the signature DECLARES which finalization family each plan intends, and the std-level coproduct fork is gone. It is NOT a construction wall today — probed by execution, the typechecker does not check a declared return type against the body, so a plan can still return the wrong family and typecheck. Until return-position and annotated-data checking are grounded, the enrolled value witnesses and the executor's parser are the wall; the witnesses dissolve when that checking lands (std.realization_schedule walk_finalization_note carries the probe and the dissolve-on). + +TWO LAWS, ONE FIELD. Materialization disclosure was briefly a `require_materialization_disclosure: Bool` beside the count, and that Bool was a writable bypass with a lie attached: the executor returned before checking the materialization receipt when it was false, while its success message — unconditional on the Bool — still reported that disclosure held. One consumer exists and it requires disclosure, so the `false` state was pre-authored for nobody. Disclosure is now INTRINSIC to the type: inhabiting FloorFinalization is what obligates both laws. A future consumer that genuinely needs resolve-count validation alone introduces its own finalization type when it exists, rather than being pre-authored as a bypass here (§5 — the state a check can be satisfied by editing away is the state that should not be writable). + +declared_resolve_count is Nat, not Int: a negative declared count has no meaning, and making it unrepresentable is cheaper than guaranteeing it mismatches later." + +type FloorFinalization { + declared_resolve_count: Nat +} data ci_sccache_provider_shell_injection_dissolution_trigger: Disposition = Scaffold { dissolves_to: RealizationDispatch, diff --git a/dag/gunbc/merge_admission.dag b/dag/gunbc/merge_admission.dag index a18c772269a..9a753ac6462 100644 --- a/dag/gunbc/merge_admission.dag +++ b/dag/gunbc/merge_admission.dag @@ -1,6 +1,7 @@ module gunbc.merge_admission -import std.types { NonEmptyStr, ContentHash, CommitSha, String, List, Bool, Int } +import std.types { NonEmptyStr, ContentHash, CommitSha, String, List, Bool, Int, PathSegment, path_segment_is_safe } +import extdeps.git.object_store { GitObjectId, GitSha1ObjectId, GitSha256ObjectId, git_object_id_eq } import extdeps.github.checks { CheckConclusion, check_conclusion_is_success, @@ -168,6 +169,7 @@ type MergeAdmissionVerdict | MergeDeniedStaleRoster | MergeDeniedNotSuccess | MergeDeniedWrongAttempt + | MergeDeniedSubjectMismatch data merge_admission_enforcement_policy: AdmissionPolicy = KeyedReceipt @@ -202,35 +204,62 @@ fn classify_merge_admission_verdict( data merge_admission_attempt_scope_note: String = "ATTEMPT SCOPE (ruling 2026-07-30): the receipt carries the walk-attempt identity in the PAYLOAD, not just the path, and the gate requires receipt.attempt_id == current — path identity alone is not enough, because a misrouted read must fail on the content too. A receipt from another attempt is neither stale nor fresh: it is NOT THE SUBJECT, so MergeDeniedWrongAttempt is checked FIRST, before conclusion, base, and roster — asking whether a foreign receipt's base is current would be answering a question about the wrong run. The identity derives from GITHUB_RUN_ID + GITHUB_RUN_ATTEMPT + GITHUB_JOB on GitHub; non-GitHub execution must supply GUNBC_WALK_ATTEMPT_ID explicitly or the walk-side composition refuses — never a silent constant like a bare local, which would make every local run one attempt and the wrong-attempt refusal unreachable off CI. Deleting or recreating the attempt directory at walk start remains hygiene; correctness never depends on cleaning a shared path." +data walk_attempt_id_note: String = "The attempt identity is a PATH SEGMENT, because it is concatenated into one: merge_admission_attempt_dir builds /.gunbc/merge-admission//. As a bare NonEmptyStr it was neither path-safe nor wire-safe (review 2026-07-30) — `../other-attempt` escapes the attempt directory, `a/b` invents a level, `.`/`..` alias the parent, and an embedded CR or LF splits the line-oriented receipt written under that name, so two logically distinct attempts could resolve to one filesystem subject or one receipt could be read as two. Both producers — the GitHub-derived composition and the explicit GUNBC_WALK_ATTEMPT_ID pass-through — now go through walk_attempt_id, which is the ONLY constructor and tests std.types.path_segment_is_safe, the single authority for what makes a string safe to concatenate as one path segment. It refuses rather than sanitizing: an encoded segment would denote a different attempt than the one the caller named." + +type WalkAttemptId = PathSegment where brand("WalkAttemptId") + +fn walk_attempt_id(raw: String) -> WalkAttemptId? { + if path_segment_is_safe(raw: raw) { + Present { value: raw as WalkAttemptId } + } else { + none + } +} + +fn walk_attempt_id_eq(left: WalkAttemptId, right: WalkAttemptId) -> Bool { + (left as String) == (right as String) +} + +data git_object_id_grounding_note: String = "The tested base tree is a GitObjectId, not a ContentHash. DESIGN's own §3 residue records that ContentHash is one brand over two unrelated hash families (structural fnv1a64 fingerprints and cited cryptographic digests) with no modeled discriminant; a Git tree object id is a THIRD domain, and admitting it into the same brand would let a gate-roster structural fingerprint inhabit the tested-tree field and typecheck. extdeps.git.object_store.GitObjectId is the existing single authority and already models the SHA-1/SHA-256 repository-format transition, so this grounds on it rather than minting a GitTreeOid nickname beside it (§3). Equality and the validating textual constructors live THERE, not here: both are generic Git behaviour, and holding them in this consumer was a fork this module briefly carried (review 2026-07-30)." + type TestedSubject { - attempt_id: NonEmptyStr + attempt_id: WalkAttemptId head_sha: CommitSha base_ref: String - base_tree_hash: ContentHash + base_tree: GitObjectId } data tested_subject_note: String = "THE SUBJECT THE FLOOR TESTED, captured as the first ordinary batch — before any substantive floor work — and bound into the receipt by the stamp. The stamp must NOT re-read HEAD or re-observe the merge target at stamp time: main can advance during a floor that runs for tens of minutes, and a receipt binding post-floor observations would claim the floor tested a tree it never saw. The gate then fetches the CURRENT target and classifies tested_base_tree_hash against it — two base facts with different jobs, never one observation doing both (the deleted single pre-floor fetch was exactly that fusion, and the freshness hole it left is what the old separate gate step's own fresh fetch existed to catch)." type MergeAdmissionReceiptV2 { - attempt_id: NonEmptyStr + attempt_id: WalkAttemptId pr_number: Int? tested_head_sha: CommitSha - tested_base_tree_hash: ContentHash + tested_base_tree: GitObjectId gate_roster_hash: ContentHash conclusion: CheckConclusion } +data merge_admission_subject_binding_note: String = "THE GATE CONSUMES THE CAPTURED SUBJECT, not merely a self-describing receipt (review 2026-07-30). The v2 receipt carried tested_head_sha from the start, and nothing read it: the classifier checked attempt, conclusion, base, roster, so a receipt was free to RESTATE which subject it allegedly certified and be believed. The subject is captured before the floor runs and is the independent fact; the receipt is the floor's claim about it. Three bindings are therefore required BEFORE any freshness question — same attempt, same head, same base tree — and a mismatch is MergeDeniedSubjectMismatch, its own state: the receipt is well-formed and from this attempt, but it describes work on something other than what was captured, which is neither staleness (a fact about the world moving) nor a wrong attempt (a fact about which run). Asking whether such a receipt's base is current would be answering a question about the wrong subject, which is exactly why WrongAttempt is first and SubjectMismatch is second." + fn classify_merge_admission_verdict_v2( - current_attempt_id: NonEmptyStr, + current_attempt_id: WalkAttemptId, + tested_subject: TestedSubject, receipt: MergeAdmissionReceiptV2, - merge_target_tree_hash: ContentHash, + merge_target_tree: GitObjectId, current_roster_hash: ContentHash, ) -> MergeAdmissionVerdict { - if !((receipt.attempt_id as String) == (current_attempt_id as String)) { + if !walk_attempt_id_eq(left: receipt.attempt_id, right: current_attempt_id) { + MergeDeniedWrongAttempt + } else if !walk_attempt_id_eq(left: tested_subject.attempt_id, right: current_attempt_id) { MergeDeniedWrongAttempt + } else if !(receipt.tested_head_sha == tested_subject.head_sha) { + MergeDeniedSubjectMismatch + } else if !git_object_id_eq(left: receipt.tested_base_tree, right: tested_subject.base_tree) { + MergeDeniedSubjectMismatch } else if !check_conclusion_admits_merge_admission_floor(c: receipt.conclusion) { MergeDeniedNotSuccess - } else if receipt.tested_base_tree_hash != merge_target_tree_hash { + } else if !git_object_id_eq(left: receipt.tested_base_tree, right: merge_target_tree) { MergeDeniedStaleBase } else if receipt.gate_roster_hash != current_roster_hash { MergeDeniedStaleRoster @@ -246,6 +275,7 @@ fn merge_admission_verdict_would_block(v: MergeAdmissionVerdict) -> Bool { MergeDeniedStaleRoster => true MergeDeniedNotSuccess => true MergeDeniedWrongAttempt => true + MergeDeniedSubjectMismatch => true } } @@ -278,6 +308,7 @@ fn receipt_is_admissible( MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } } diff --git a/dag/gunbc/merge_admission_produce.dag b/dag/gunbc/merge_admission_produce.dag index 0f29259d8ae..c51ab474571 100644 --- a/dag/gunbc/merge_admission_produce.dag +++ b/dag/gunbc/merge_admission_produce.dag @@ -1,6 +1,7 @@ module gunbc.merge_admission_produce import std.types { NonEmptyStr, ContentHash, CommitSha, String, Int, List, Bool, GitRef } +import extdeps.git.object_store { GitObjectId, GitSha1ObjectId, GitSha256ObjectId, git_sha1_object_id, git_sha256_object_id } import std.disposition { Disposition, Scaffold, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } import gunbc.repo_identity { gunbc_merge_target_ref } @@ -22,6 +23,8 @@ import extdeps.github.checks { } import gunbc.merge_admission { TestedSubject, + WalkAttemptId, + walk_attempt_id, MergeAdmissionReceiptV2, MergeAdmissionReceipt, mint_merge_admission_receipt, @@ -39,34 +42,55 @@ data merge_admission_receipt_schema_v2: String = "gunbc.merge_admission_receipt. data merge_admission_tested_subject_schema: String = "gunbc.merge_admission_tested_subject.v1" -fn merge_admission_attempt_dir(root: String, attempt_id: NonEmptyStr) -> String { +fn merge_admission_attempt_dir(root: String, attempt_id: WalkAttemptId) -> String { concat(concat(root, "/.gunbc/merge-admission/"), attempt_id as String) } -fn merge_admission_tested_subject_path(root: String, attempt_id: NonEmptyStr) -> String { +fn merge_admission_tested_subject_path(root: String, attempt_id: WalkAttemptId) -> String { concat(merge_admission_attempt_dir(root: root, attempt_id: attempt_id), "/tested-subject.wire") } -fn merge_admission_floor_receipt_path(root: String, attempt_id: NonEmptyStr) -> String { +fn merge_admission_floor_receipt_path(root: String, attempt_id: WalkAttemptId) -> String { concat(merge_admission_attempt_dir(root: root, attempt_id: attempt_id), "/floor-receipt.wire") } data compose_walk_attempt_id_note: String = "Pure composition of the walk-attempt identity from its parts; the ENV OBSERVATION lives with the wet entry, this fn only joins and refuses. Every part must be nonempty — an empty run id, attempt number, or job name yields Absent, and the caller REFUSES the run rather than substituting a constant: a silent local would make every non-GitHub run one attempt, so the wrong-attempt refusal could never fire off CI, which is exactly the unreachable-arm shape §5 forbids. Non-GitHub execution supplies GUNBC_WALK_ATTEMPT_ID explicitly and it passes through compose_explicit_walk_attempt_id under the same nonempty law." -fn compose_walk_attempt_id(run_id: String, run_attempt: String, job: String) -> NonEmptyStr? { +fn compose_walk_attempt_id(run_id: String, run_attempt: String, job: String) -> WalkAttemptId? { if (run_id == "") || (run_attempt == "") || (job == "") { none } else { - Present { - value: concat(concat(concat(concat(run_id, "-"), run_attempt), "-"), job) as NonEmptyStr - } + walk_attempt_id(raw: concat(concat(concat(concat(run_id, "-"), run_attempt), "-"), job)) } } -fn compose_explicit_walk_attempt_id(explicit: String) -> NonEmptyStr? { - if explicit == "" { none } else { Present { value: explicit as NonEmptyStr } } +fn compose_explicit_walk_attempt_id(explicit: String) -> WalkAttemptId? { + walk_attempt_id(raw: explicit) +} + +data git_object_id_wire_note: String = "A Git object id on the wire carries its FORMAT, because the type does: :. An anonymous hex string would be exactly the defect DESIGN's ContentHash-family residue records — a value whose family the reader has to guess — and a repository mid SHA-1/SHA-256 transition is precisely when guessing wrong is possible. This fn owns ONLY the : spelling; whether the hex is a well-formed object id of that family is extdeps.git.object_store's question, answered by git_sha1_object_id / git_sha256_object_id, which check exact length and canonical lowercase hex. An earlier cut cast the suffix straight into the brand, so sha1:x, sha1:not-hex and a 64-digit value labelled sha1 all parsed (review 2026-07-30) — family without length and syntax is not identification." + +fn render_git_object_id_wire(oid: GitObjectId) -> String { + match oid { + GitSha1ObjectId { digest } => concat("sha1:", digest as String) + GitSha256ObjectId { digest } => concat("sha256:", digest as String) + } } +fn parse_git_object_id_wire(raw: String) -> GitObjectId? { + if !(length(split(s: raw, delimiter: ":")) == 2) { + none + } else if split(s: raw, delimiter: ":").first() == "sha1" { + git_sha1_object_id(hex: split(s: raw, delimiter: ":").skip(n: 1).first()) + } else if split(s: raw, delimiter: ":").first() == "sha256" { + git_sha256_object_id(hex: split(s: raw, delimiter: ":").skip(n: 1).first()) + } else { + none + } +} + +data wire_exact_arity_note: String = "BOTH v2 parsers require an EXACT line count, and every required field goes through its domain constructor (review 2026-07-30). The first cut accepted a SUPERSET — `length(lines) >= 5` — so trailing content rode along unread, and it validated only that the schema tag and attempt id were nonempty, leaving base ref, tree, and head SHA free to be empty strings that then bound into a receipt as though observed. Worse, the optional PR line converted a MALFORMED present field into an absent one: parse_int returned Absent on garbage and the receipt parsed clean with pr_number: none, which is the state-space conflation §5 forbids — `not supplied` and `supplied but unreadable` are different facts with different remedies. A seventh line that is not an integer now refuses the whole receipt. Exact arity is what makes a format extension VISIBLE: adding a field means bumping the schema tag, not silently appending a line older readers ignore." + fn render_tested_subject_wire(subject: TestedSubject) -> String { concat( concat( @@ -76,27 +100,37 @@ fn render_tested_subject_wire(subject: TestedSubject) -> String { concat(subject.base_ref, " ") ), - concat(concat(subject.base_tree_hash, " + concat(concat(render_git_object_id_wire(oid: subject.base_tree), " "), subject.head_sha) ) } fn parse_tested_subject_wire(text: String) -> TestedSubject? { let lines = receipt_wire_lines(text: text) - if length(lines) < 5 { + if !(length(lines) == 5) { none } else if !(lines.first() == merge_admission_tested_subject_schema) { none - } else if lines.skip(n: 1).first() == "" { + } else if lines.skip(n: 2).first() == "" { + none + } else if lines.skip(n: 4).first() == "" { none } else { - Present { - value: TestedSubject { - attempt_id: lines.skip(n: 1).first() as NonEmptyStr, - base_ref: lines.skip(n: 2).first(), - base_tree_hash: lines.skip(n: 3).first(), - head_sha: lines.skip(n: 4).first(), - } + match walk_attempt_id(raw: lines.skip(n: 1).first()) { + Absent => none + Present { value: attempt } => + match parse_git_object_id_wire(raw: lines.skip(n: 3).first()) { + Absent => none + Present { value: tree } => + Present { + value: TestedSubject { + attempt_id: attempt, + base_ref: lines.skip(n: 2).first(), + base_tree: tree, + head_sha: lines.skip(n: 4).first(), + } + } + } } } } @@ -109,7 +143,7 @@ fn render_receipt_wire_v2(receipt: MergeAdmissionReceiptV2) -> String { concat(concat(merge_admission_receipt_schema_v2, " "), concat(receipt.attempt_id as String, " ")), - concat(concat(receipt.tested_base_tree_hash, " + concat(concat(render_git_object_id_wire(oid: receipt.tested_base_tree), " "), concat(receipt.gate_roster_hash, " ")) ), @@ -123,28 +157,71 @@ fn render_receipt_wire_v2(receipt: MergeAdmissionReceiptV2) -> String { } } +data wire_pr_number_three_states_note: String = "THREE states, named, because two of them are not the same absence: no seventh line at all (the receipt legitimately carries no PR number), a seventh line that parses, and a seventh line that does not. An Optional> would spell this with two Absents meaning different things — the state-space conflation DESIGN's failure list names — and the language refuses the spelling anyway, since `??` is the null-coalesce operator token and cannot appear in type position. WirePrMalformed is what makes the whole receipt refuse instead of quietly becoming a receipt with no PR number." + +type ReceiptWirePrNumber + = WirePrAbsent + | WirePrPresent { value: Int } + | WirePrMalformed + +fn receipt_wire_v2_pr_number(lines: List) -> ReceiptWirePrNumber { + if length(lines) == 6 { + WirePrAbsent + } else { + match parse_int(s: lines.skip(n: 6).first()) { + Present { value: n } => WirePrPresent { value: n } + Absent => WirePrMalformed + } + } +} + fn parse_receipt_wire_v2(text: String) -> MergeAdmissionReceiptV2? { let lines = receipt_wire_lines(text: text) - if length(lines) < 6 { + if !((length(lines) == 6) || (length(lines) == 7)) { none } else if !(lines.first() == merge_admission_receipt_schema_v2) { none - } else if lines.skip(n: 1).first() == "" { + } else if lines.skip(n: 3).first() == "" { + none + } else if lines.skip(n: 5).first() == "" { none } else { - match parse_check_conclusion(raw: lines.skip(n: 4).first()) { - Present { value: conclusion } => - Present { - value: MergeAdmissionReceiptV2 { - attempt_id: lines.skip(n: 1).first() as NonEmptyStr, - pr_number: if length(lines) >= 7 { parse_int(s: lines.skip(n: 6).first()) } else { none }, - tested_head_sha: lines.skip(n: 5).first(), - tested_base_tree_hash: lines.skip(n: 2).first(), - gate_roster_hash: lines.skip(n: 3).first(), - conclusion: conclusion, - } - } + match walk_attempt_id(raw: lines.skip(n: 1).first()) { Absent => none + Present { value: attempt } => + match parse_git_object_id_wire(raw: lines.skip(n: 2).first()) { + Absent => none + Present { value: tree } => + match parse_check_conclusion(raw: lines.skip(n: 4).first()) { + Absent => none + Present { value: conclusion } => + match receipt_wire_v2_pr_number(lines: lines) { + WirePrMalformed => none + WirePrAbsent => + Present { + value: MergeAdmissionReceiptV2 { + attempt_id: attempt, + pr_number: none, + tested_head_sha: lines.skip(n: 5).first(), + tested_base_tree: tree, + gate_roster_hash: lines.skip(n: 3).first(), + conclusion: conclusion, + } + } + WirePrPresent { value: n } => + Present { + value: MergeAdmissionReceiptV2 { + attempt_id: attempt, + pr_number: Present { value: n }, + tested_head_sha: lines.skip(n: 5).first(), + tested_base_tree: tree, + gate_roster_hash: lines.skip(n: 3).first(), + conclusion: conclusion, + } + } + } + } + } } } } diff --git a/dag/std/realization_schedule.dag b/dag/std/realization_schedule.dag index 87f6452a09b..74d53416eeb 100644 --- a/dag/std/realization_schedule.dag +++ b/dag/std/realization_schedule.dag @@ -207,20 +207,20 @@ type Runnable data walk_plan_note: String = "A walk is TWO populations with DIFFERENT ordering laws, and the type says so where a bare List> could not. `batches` are the ordinary floor: batch boundaries order them, and a failure's consequence is the walk's FloorBatchStopPolicy (StopBeforeDependents on pull_request, FullLedger on push/schedule — where a failed batch deliberately does NOT stop the walk, because the per-batch ledger on main is bisection evidence, operator ruling 2026-07-23). `on_success_stages` run ONLY when the ordinary floor completed AND its receipts finalized and validated; each stage is a barrier — stage N fully completes with zero failures before stage N+1 starts — and stage-to-stage execution is ALWAYS fail-fast, regardless of the ordinary stop policy: FullLedger is an ordinary-floor policy and never applies between stages. WHY THE SECOND POPULATION EXISTS: work whose correctness is conditional on the whole floor being green (the merge-admission stamp is the first occupant — stamping Success is only true if reaching it proves green) cannot be an ordinary trailing batch, because under FullLedger a trailing batch is still reached after a red batch. The prior attempt encoded exactly that and shipped a fail-open; a second attempt then declared stamp-then-gate as one stage and rediscovered the SIBLING defect — members WITHIN a stage run concurrently (distinct entries become distinct spawned units), so intra-stage order does not exist and anything sequential must be ONE claim whose body sequences its steps, or two singleton stages. Both defects are why this is a named type with a note rather than a convention (operator design ruling 2026-07-30). -WHAT THE EXECUTOR ACTUALLY PROVIDES TODAY, stated because a carrier that promises more than its executor delivers is the same defect this type exists to end (review 2026-07-30). The stage BARRIER is real: stage N completes before stage N+1 starts, and a failed stage prevents every later one. THREE GAPS remain, and none is currently reachable because every plan declares an empty stage list: (1) members within a stage run SERIALLY, not concurrently — serial is a strictly stronger order than the contract promises, so no current caller is misled, but wall time, peak memory, and overlap are resource facts a future author would measure wrongly; (2) stages execute through run_memo_shared_claims directly rather than the ordinary unit-lane partition, so they bypass governor admission, batch clamps, and resource-profile enforcement — safe for the negligible admission claims that will occupy them, unsafe for the substantial or host-compiler-spawning claim the generic carrier permits; (3) ONE aggregate stage receipt is written after the whole sequence rather than one per stage before the next begins. The repair is to extract the ordinary batch machinery into a reusable run_stage(stage) — group by entry and mode, acquire governor admission, spawn eligible units, join, write THAT stage receipt — so both populations share one executor and differ only in ordering and failure policy. Until that lands, do not place a Substantial or host-compiler runnable in a stage; the arm-time validator refuses discovery runnables outright, and the profile restriction is the next wall. Every plan function returns WalkPlan — a plan with no postconditions returns on_success_stages: [] — and the executor has ONE strict parser: a malformed or missing field is a hard error, never a fallback to a bare-list reading." +WHAT THE EXECUTOR ACTUALLY PROVIDES TODAY, stated because a carrier that promises more than its executor delivers is the same defect this type exists to end (review 2026-07-30). The stage BARRIER is real: stage N completes before stage N+1 starts, and a failed stage prevents every later one. THREE GAPS remain, and none is currently reachable because every plan declares an empty stage list: (1) members within a stage run SERIALLY, not concurrently — serial is a strictly stronger order than the contract promises, so no current caller is misled, but wall time, peak memory, and overlap are resource facts a future author would measure wrongly; (2) stages execute through run_memo_shared_claims directly rather than the ordinary unit-lane partition, so they bypass governor admission, batch clamps, and resource-profile enforcement — safe for the negligible admission claims that will occupy them, unsafe for the substantial or host-compiler-spawning claim the generic carrier permits; (3) ONE aggregate stage receipt is written after the whole sequence rather than one per stage before the next begins. The repair is to extract the ordinary batch machinery into a reusable run_stage(stage) — group by entry and mode, acquire governor admission, spawn eligible units, join, write THAT stage receipt — so both populations share one executor and differ only in ordering and failure policy. Until that lands, do not place a Substantial or host-compiler runnable in a stage; the arm-time validator refuses discovery runnables outright, and the profile restriction is the next wall. Every plan function returns WalkPlan — a plan with no postconditions returns on_success_stages: [] — and the executor has ONE strict parser: a malformed or missing field is a hard error, never a fallback to a bare-list reading." -data walk_finalization_note: String = "THE PLAN CARRIES ITS FINALIZATION POLICY; the executor never infers it from a function's spelling. The first cut selected finalization by plan-function name (if plan_function == gunbc_ci_floor_plan read the law from the closure) — the same hidden seed-roster convention the WalkPlan carrier was built to remove, reintroduced in the same PR (review 2026-07-30), and the RED fixture made the coupling visible by having to impersonate the production name to arm the contract. As a FIELD, the policy is part of the parsed value: a floor plan without its law is now UNWRITABLE (the strict parser refuses a missing field) rather than checked at arm time, schedule lenses and plan artifacts can see it, and the fixture declares its own policy instead of name-impersonating into one. NoWalkFinalization is the declared empty policy — regen, falsifier, and the plan-artifact shortcut say so explicitly, never by omission." +data walk_finalization_note: String = "THE PLAN CARRIES ITS FINALIZATION POLICY IN ITS TYPE, and the executor never infers it — not from a function's spelling, and not from which arm of a coproduct an authored value happened to pick. Two corrections stacked here. FIRST: the original cut selected finalization by plan-function name (if plan_function == gunbc_ci_floor_plan read the law from the closure) — the same hidden seed-roster convention the WalkPlan carrier was built to remove, reintroduced in the same PR (review 2026-07-30), and the RED fixture made the coupling visible by having to impersonate the production name to arm the contract. Moving it to a field fixed that. SECOND: a field of a coproduct type is still only an authored choice (review 2026-07-30, second pass). With `finalization: WalkFinalization`, `WalkPlan \{ batches: floor_batches, finalization: NoWalkFinalization, .. \}` typechecked — NoWalkFinalization and FloorFinalization inhabit the same sum, so nothing connected floor-shaped work to floor finalization; the production constructor merely chose correctly. So the carrier is PARAMETERIZED: WalkPlan, and gunbc_ci_floor_plan returns WalkPlan while regen, plan-artifact, and falsifier return WalkPlan. One runtime parser still reads both, because the parse is over the finalization VALUE and does not care which instantiation produced it. The parameterization also stops this generic std carrier from owning a growing coproduct of gunbc-specific receipt policies: FloorFinalization moved to gunbc.ci_materialization, beside the declared count it is about, and std keeps only the parameter and the declared-empty inhabitant. -type WalkFinalization - = NoWalkFinalization - | FloorFinalization { - declared_resolve_count: Int - require_materialization_disclosure: Bool - } +WHAT THE PARAMETERIZATION DOES AND DOES NOT BUY, measured rather than assumed — and the measurement contradicted the intent, so the intent is not what gets written down. The review that requested this asked for a construction wall: the floor's return type should REJECT the empty policy. It does not, today. Probed by execution 2026-07-30: replacing the floor's finalization with NoFinalizationDeclared \{\} while the signature still reads WalkPlan TYPECHECKS, and fails only later, at the first field access, as a runtime error. A narrower probe isolates the general defect — the typechecker does not check a function's declared return type against its body at all (`fn f() -> Int \{ \"not an int\" \}` typechecks; so does a mismatched generic instantiation), nor a `data` declaration's annotation against its value, while ARGUMENT position is checked and refuses correctly. So this is a §5 WALL-AFTER-GROUNDING, not a wall now: the class is decidable, the single authority it waits on is return-position typechecking, and until that lands the enforcement is honestly VALIDATION — the enrolled witness floor_plan_projects_the_declared_resolve_count_authority (v2.test.claim.ci_floor_plan_witness) reds when the floor stops projecting the declared count, with a forked-count RED control beside it. Saying the signature walls it would be the same overclaim this note's own history is a record of. dissolve-on: return-position type enforcement in the typechecker, at which point the signature becomes the wall and the witness becomes redundant. + +LANGUAGE-LAYER FINDING recorded rather than absorbed (§5 workaround rule): a one-variant sum cannot be spelled `type T = OneVariant` — that production is the type-ALIAS form, and the compiler reads OneVariant as an unresolved type name (probed by execution). The nullary variant therefore has to be spelled `= NoFinalizationDeclared \{\}`, an empty record variant. That is position-dependent meaning for the same syntax (`= A | B` makes A a variant; `= A` makes A an alias target), and it belongs in the grammar-consolidation lane, not in a silent respelling." + +type NoWalkFinalization + = NoFinalizationDeclared {} -type WalkPlan { +type WalkPlan { batches: List> - finalization: WalkFinalization + finalization: F on_success_stages: List> } diff --git a/dag/std/types.dag b/dag/std/types.dag index b19e49adf21..07b50c906bd 100644 --- a/dag/std/types.dag +++ b/dag/std/types.dag @@ -130,6 +130,21 @@ type LanguageId = String where non_empty type SecretName = String where non_empty type PathSegment = NonEmptyStr where brand("PathSegment") + +data path_segment_safety_note: String = "WHAT MAKES A STRING SAFE TO USE AS ONE PATH SEGMENT — the law, held once, so every branded id that becomes a directory name tests the same thing. The brand alone never carried it: a branded NonEmptyStr accepts \"..\", \"a/b\", and an embedded newline, so a value that typechecked as a segment could still escape its parent directory, alias a sibling, or split a line-oriented file written under that name. The refused set is exactly the characters that change what a concatenated path MEANS — `/` and `\\` introduce a level, `.` and `..` navigate, CR and LF terminate a record in every line-oriented format this repo writes, NUL terminates the string at the syscall boundary. Callers REFUSE on false rather than sanitizing, because a sanitized segment silently denotes something other than what the caller named (§5: a failure arm must refuse, never widen). Percent- or hex-encoding is the reversible alternative and is deliberately not offered until a caller needs a segment it cannot rename. + +This is a PREDICATE, not a constructor, and that is a modeling choice rather than a limitation worked around. A generic `path_segment(raw) -> PathSegment?` would put the branding cast in this module, and each caller would then re-cast the generic segment into its own brand anyway — two casts and two authorities for one law. Holding the law here and letting each branded id (gunbc.merge_admission.walk_attempt_id is the first) construct itself through it keeps one authority for what is hostile and one constructor per brand, which is what §3 asks for. A generic constructor earns its place when a second caller wants a bare PathSegment rather than a brand of its own; none does today." + +fn path_segment_is_safe(raw: String) -> Bool { + !((raw == "") + || (raw == ".") + || (raw == "..") + || string_contains(s: raw, pattern: "/") + || string_contains(s: raw, pattern: "\\") + || string_contains(s: raw, pattern: "\n") + || string_contains(s: raw, pattern: "\x0d") + || string_contains(s: raw, pattern: "\x00")) +} type GlobSegment = NonEmptyStr where brand("GlobSegment") type FilePathParts { segments: List diff --git a/dag/test/claim/merge_admission_actuator_witness_test.dag b/dag/test/claim/merge_admission_actuator_witness_test.dag index 5f898641c36..043da6ba251 100644 --- a/dag/test/claim/merge_admission_actuator_witness_test.dag +++ b/dag/test/claim/merge_admission_actuator_witness_test.dag @@ -31,6 +31,7 @@ test fn enforcement_denies_stale_base_verdict() -> Bool { MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } } @@ -45,6 +46,7 @@ test fn enforcement_denies_stale_roster_verdict() -> Bool { MergeDeniedStaleBase => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } } @@ -59,6 +61,7 @@ test fn enforcement_admits_fresh_verdict() -> Bool { MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } } @@ -77,6 +80,7 @@ test fn enforcement_denies_skipped_fresh_receipt() -> Bool { ) { MergeDeniedNotSuccess => true MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false MergeAdmitted => false MergeDeniedStaleBase => false MergeDeniedStaleRoster => false @@ -98,6 +102,7 @@ test fn enforcement_denies_failure_fresh_receipt() -> Bool { ) { MergeDeniedNotSuccess => true MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false MergeAdmitted => false MergeDeniedStaleBase => false MergeDeniedStaleRoster => false @@ -115,6 +120,7 @@ test fn enforcement_red_on_revert_stale_base() -> Bool { MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } let stale = match classify_merge_admission_verdict( receipt: scenario_pr_x_receipt, @@ -126,6 +132,7 @@ test fn enforcement_red_on_revert_stale_base() -> Bool { MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } fresh && stale } diff --git a/dag/test/claim/merge_admission_attempt_witness_test.dag b/dag/test/claim/merge_admission_attempt_witness_test.dag index fe88f4630e5..198d813483a 100644 --- a/dag/test/claim/merge_admission_attempt_witness_test.dag +++ b/dag/test/claim/merge_admission_attempt_witness_test.dag @@ -1,9 +1,12 @@ module test.claim.merge_admission_attempt_witness -import std.types { NonEmptyStr, ContentHash, CommitSha } +import std.types { NonEmptyStr, ContentHash, CommitSha, String } import extdeps.github.checks { Success, Failure } +import extdeps.git.object_store { GitObjectId, GitSha1ObjectId, GitSha256ObjectId, git_object_id_eq } import gunbc.merge_admission { TestedSubject, + WalkAttemptId, + walk_attempt_id, MergeAdmissionReceiptV2, MergeAdmissionVerdict, MergeAdmitted, @@ -11,6 +14,7 @@ import gunbc.merge_admission { MergeDeniedStaleRoster, MergeDeniedNotSuccess, MergeDeniedWrongAttempt, + MergeDeniedSubjectMismatch, classify_merge_admission_verdict_v2, merge_admission_verdict_would_block, } @@ -26,44 +30,78 @@ import gunbc.merge_admission_produce { render_receipt_wire_v2, parse_receipt_wire_v2, render_receipt_wire, + render_git_object_id_wire, + parse_git_object_id_wire, stamp_floor_receipt_with_conclusion, } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data attempt_a: NonEmptyStr = "12345-1-ci" -data attempt_b: NonEmptyStr = "12345-2-ci" +data attempt_a_raw: String = "12345-1-ci" +data attempt_b_raw: String = "12345-2-ci" data head_sha_fx: CommitSha = "abc1234def5678901234567890abcd1234567890" -data base_tree_fx: ContentHash = "tree-base-current" -data base_tree_stale_fx: ContentHash = "tree-base-stale" +data other_head_sha_fx: CommitSha = "0000000111111112222222233333333444444445" data roster_fx: ContentHash = "roster-current" -fn receipt_fx(attempt: NonEmptyStr, base: ContentHash) -> MergeAdmissionReceiptV2 { +fn attempt_a() -> WalkAttemptId { + match walk_attempt_id(raw: attempt_a_raw) { + Present { value: id } => id + Absent => "unreachable-fixture" as WalkAttemptId + } +} + +fn attempt_b() -> WalkAttemptId { + match walk_attempt_id(raw: attempt_b_raw) { + Present { value: id } => id + Absent => "unreachable-fixture" as WalkAttemptId + } +} + +fn base_tree_fx() -> GitObjectId { + GitSha1ObjectId { digest: "1111111111111111111111111111111111111111" } +} + +fn base_tree_stale_fx() -> GitObjectId { + GitSha1ObjectId { digest: "2222222222222222222222222222222222222222" } +} + +fn subject_fx(attempt: WalkAttemptId, tree: GitObjectId, head: CommitSha) -> TestedSubject { + TestedSubject { + attempt_id: attempt, + head_sha: head, + base_ref: "origin/main", + base_tree: tree, + } +} + +fn receipt_fx(attempt: WalkAttemptId, tree: GitObjectId, head: CommitSha) -> MergeAdmissionReceiptV2 { MergeAdmissionReceiptV2 { attempt_id: attempt, pr_number: Present { value: 7470 }, - tested_head_sha: head_sha_fx, - tested_base_tree_hash: base, + tested_head_sha: head, + tested_base_tree: tree, gate_roster_hash: roster_fx, conclusion: Success, } } -test fn matching_attempt_fresh_base_admits() -> Bool { +test fn matching_attempt_and_subject_with_fresh_base_admits() -> Bool { match classify_merge_admission_verdict_v2( - current_attempt_id: attempt_a, - receipt: receipt_fx(attempt: attempt_a, base: base_tree_fx), - merge_target_tree_hash: base_tree_fx, + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + merge_target_tree: base_tree_fx(), current_roster_hash: roster_fx, ) { MergeAdmitted => true _ => false } } test fn foreign_attempt_refuses_as_wrong_attempt() -> Bool { let v = classify_merge_admission_verdict_v2( - current_attempt_id: attempt_a, - receipt: receipt_fx(attempt: attempt_b, base: base_tree_fx), - merge_target_tree_hash: base_tree_fx, + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + receipt: receipt_fx(attempt: attempt_b(), tree: base_tree_fx(), head: head_sha_fx), + merge_target_tree: base_tree_fx(), current_roster_hash: roster_fx, ) match v { MergeDeniedWrongAttempt => merge_admission_verdict_would_block(v: v) _ => false } @@ -71,37 +109,72 @@ test fn foreign_attempt_refuses_as_wrong_attempt() -> Bool { test fn wrong_attempt_precedes_every_other_refusal() -> Bool { let r = MergeAdmissionReceiptV2 { - attempt_id: attempt_b, + attempt_id: attempt_b(), pr_number: none, - tested_head_sha: head_sha_fx, - tested_base_tree_hash: base_tree_stale_fx, + tested_head_sha: other_head_sha_fx, + tested_base_tree: base_tree_stale_fx(), gate_roster_hash: "roster-stale", conclusion: Failure, } match classify_merge_admission_verdict_v2( - current_attempt_id: attempt_a, + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), receipt: r, - merge_target_tree_hash: base_tree_fx, + merge_target_tree: base_tree_fx(), + current_roster_hash: roster_fx, + ) { MergeDeniedWrongAttempt => true _ => false } +} + +data subject_binding_discriminating_note: String = "The two rows below are the ones the receipt could previously LIE past. Before the gate consumed the captured subject, a receipt in the right attempt could restate any head SHA or any base tree and be classified purely on its own say-so; both cases here classified MergeAdmitted under the old signature and are refusals now. They are the discriminating pair for the binding, not decoration: each varies exactly ONE field away from the admitting case above, so a regression that drops either comparison turns that row green while the other stays red." + +test fn receipt_head_that_differs_from_the_captured_subject_refuses() -> Bool { + let v = classify_merge_admission_verdict_v2( + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: other_head_sha_fx), + merge_target_tree: base_tree_fx(), + current_roster_hash: roster_fx, + ) + match v { MergeDeniedSubjectMismatch => merge_admission_verdict_would_block(v: v) _ => false } +} + +test fn receipt_base_tree_that_differs_from_the_captured_subject_refuses() -> Bool { + match classify_merge_admission_verdict_v2( + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_stale_fx(), head: head_sha_fx), + merge_target_tree: base_tree_stale_fx(), + current_roster_hash: roster_fx, + ) { MergeDeniedSubjectMismatch => true _ => false } +} + +test fn subject_from_another_attempt_refuses_even_with_a_matching_receipt() -> Bool { + match classify_merge_admission_verdict_v2( + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_b(), tree: base_tree_fx(), head: head_sha_fx), + receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + merge_target_tree: base_tree_fx(), current_roster_hash: roster_fx, ) { MergeDeniedWrongAttempt => true _ => false } } -test fn matching_attempt_stale_base_is_stale_not_wrong_attempt() -> Bool { +test fn subject_bound_receipt_on_an_advanced_target_is_stale_not_mismatched() -> Bool { match classify_merge_admission_verdict_v2( - current_attempt_id: attempt_a, - receipt: receipt_fx(attempt: attempt_a, base: base_tree_stale_fx), - merge_target_tree_hash: base_tree_fx, + current_attempt_id: attempt_a(), + tested_subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx), + merge_target_tree: base_tree_stale_fx(), current_roster_hash: roster_fx, ) { MergeDeniedStaleBase => true _ => false } } test fn wire_v2_roundtrips_all_fields_with_pr() -> Bool { - let r = receipt_fx(attempt: attempt_a, base: base_tree_fx) + let r = receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx) match parse_receipt_wire_v2(text: render_receipt_wire_v2(receipt: r)) { Present { value: parsed } => - ((parsed.attempt_id as String) == (attempt_a as String)) + ((parsed.attempt_id as String) == attempt_a_raw) && (parsed.tested_head_sha == head_sha_fx) - && (parsed.tested_base_tree_hash == base_tree_fx) + && git_object_id_eq(left: parsed.tested_base_tree, right: base_tree_fx()) && (parsed.gate_roster_hash == roster_fx) && match parsed.pr_number { Present { value: n } => n == 7470 Absent => false } && match parsed.conclusion { Success => true _ => false } @@ -111,16 +184,16 @@ test fn wire_v2_roundtrips_all_fields_with_pr() -> Bool { test fn wire_v2_roundtrips_without_pr() -> Bool { let r = MergeAdmissionReceiptV2 { - attempt_id: attempt_a, + attempt_id: attempt_a(), pr_number: none, tested_head_sha: head_sha_fx, - tested_base_tree_hash: base_tree_fx, + tested_base_tree: base_tree_fx(), gate_roster_hash: roster_fx, conclusion: Success, } match parse_receipt_wire_v2(text: render_receipt_wire_v2(receipt: r)) { Present { value: parsed } => - match parsed.pr_number { Absent => (parsed.attempt_id as String) == (attempt_a as String) Present { value: _ } => false } + match parsed.pr_number { Absent => (parsed.attempt_id as String) == attempt_a_raw Present { value: _ } => false } Absent => false } } @@ -129,7 +202,7 @@ test fn v1_wire_refused_by_v2_parser() -> Bool { let v1 = render_receipt_wire(receipt: stamp_floor_receipt_with_conclusion( pr_number: Present { value: 7470 }, head_sha: head_sha_fx, - base_tree_hash: base_tree_fx, + base_tree_hash: "1111111111111111111111111111111111111111", conclusion: Success, )) match parse_receipt_wire_v2(text: v1) { @@ -138,35 +211,89 @@ test fn v1_wire_refused_by_v2_parser() -> Bool { } } -test fn tested_subject_wire_roundtrips() -> Bool { - let subj = TestedSubject { - attempt_id: attempt_a, - head_sha: head_sha_fx, - base_ref: "origin/main", - base_tree_hash: base_tree_fx, +data wire_arity_red_note: String = "Every row below was ACCEPTED by the first cut of these parsers. A trailing line rode along unread (the `>= n` superset), and a malformed seventh line silently became pr_number: none — supplied-but-unreadable collapsing into not-supplied. Each row varies one thing from a wire that parses, so a regression that relaxes arity back to a superset turns exactly that row green." + +test fn receipt_wire_with_a_trailing_line_refuses() -> Bool { + let good = render_receipt_wire_v2(receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx)) + match parse_receipt_wire_v2(text: concat(good, "\ntrailing")) { + Present { value: _ } => false + Absent => true + } +} + +test fn receipt_wire_with_a_malformed_pr_line_refuses_the_whole_receipt() -> Bool { + let no_pr = render_receipt_wire_v2(receipt: MergeAdmissionReceiptV2 { + attempt_id: attempt_a(), + pr_number: none, + tested_head_sha: head_sha_fx, + tested_base_tree: base_tree_fx(), + gate_roster_hash: roster_fx, + conclusion: Success, + }) + match parse_receipt_wire_v2(text: concat(no_pr, "\nnot-a-number")) { + Present { value: _ } => false + Absent => true } +} + +test fn subject_wire_with_a_trailing_line_refuses() -> Bool { + let good = render_tested_subject_wire(subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx)) + match parse_tested_subject_wire(text: concat(good, "\ntrailing")) { + Present { value: _ } => false + Absent => true + } +} + +test fn tested_subject_wire_roundtrips() -> Bool { + let subj = subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx) match parse_tested_subject_wire(text: render_tested_subject_wire(subject: subj)) { Present { value: parsed } => - ((parsed.attempt_id as String) == (attempt_a as String)) + ((parsed.attempt_id as String) == attempt_a_raw) && (parsed.head_sha == head_sha_fx) && (parsed.base_ref == "origin/main") - && (parsed.base_tree_hash == base_tree_fx) + && git_object_id_eq(left: parsed.base_tree, right: base_tree_fx()) Absent => false } } test fn subject_wire_refused_by_receipt_parser_and_vice_versa() -> Bool { - let subj = render_tested_subject_wire(subject: TestedSubject { - attempt_id: attempt_a, - head_sha: head_sha_fx, - base_ref: "origin/main", - base_tree_hash: base_tree_fx, - }) - let rec = render_receipt_wire_v2(receipt: receipt_fx(attempt: attempt_a, base: base_tree_fx)) + let subj = render_tested_subject_wire(subject: subject_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx)) + let rec = render_receipt_wire_v2(receipt: receipt_fx(attempt: attempt_a(), tree: base_tree_fx(), head: head_sha_fx)) match parse_receipt_wire_v2(text: subj) { Present { value: _ } => false Absent => true } && match parse_tested_subject_wire(text: rec) { Present { value: _ } => false Absent => true } } +data object_id_validation_red_note: String = "Every raw value below PARSED before the wire parser consumed a validating constructor: it checked one colon, a recognized family prefix and a nonempty suffix, then cast the suffix straight into the brand. So sha1:x was a Git object id, and so was a 64-digit value labelled sha1 — family without length and syntax is not identification, and a receipt binding such a value would compare equal to nothing real while typechecking perfectly." + +test fn object_id_wire_refuses_wrong_length_and_nonhex() -> Bool { + let sha256_hex = "3333333333333333333333333333333333333333333333333333333333333333" + match parse_git_object_id_wire(raw: "sha1:1111") { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: concat("sha1:", sha256_hex)) { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: "sha256:3333") { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: "sha1:zzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzz") { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: "sha1:1111111111111111111111111111111111111111:extra") { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: "md5:1111111111111111111111111111111111111111") { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: "sha1:") { Present { value: _ } => false Absent => true } +} + +test fn object_id_wire_carries_its_format_and_refuses_an_anonymous_hex() -> Bool { + let sha1_wire = render_git_object_id_wire(oid: base_tree_fx()) + let sha256 = GitSha256ObjectId { digest: "3333333333333333333333333333333333333333333333333333333333333333" } + match parse_git_object_id_wire(raw: sha1_wire) { + Present { value: back } => git_object_id_eq(left: back, right: base_tree_fx()) + Absent => false + } + && match parse_git_object_id_wire(raw: "1111111111111111111111111111111111111111") { + Present { value: _ } => false + Absent => true + } + && match parse_git_object_id_wire(raw: "md5:1111") { Present { value: _ } => false Absent => true } + && match parse_git_object_id_wire(raw: render_git_object_id_wire(oid: sha256)) { + Present { value: back } => !git_object_id_eq(left: back, right: base_tree_fx()) + Absent => false + } +} + test fn attempt_id_composes_from_nonempty_parts() -> Bool { match compose_walk_attempt_id(run_id: "12345", run_attempt: "1", job: "ci") { Present { value: id } => (id as String) == "12345-1-ci" @@ -181,10 +308,28 @@ test fn attempt_id_refuses_any_empty_part() -> Bool { && match compose_explicit_walk_attempt_id(explicit: "") { Present { value: _ } => false Absent => true } } +data attempt_id_path_safety_red_note: String = "Each raw value below was ACCEPTED as an attempt id before walk_attempt_id existed, and each one breaks something specific once concatenated into /.gunbc/merge-admission//: `../other-attempt` reads another attempt's receipt, `a/b` invents a directory level, `.` and `..` alias the parent, and an embedded newline splits the line-oriented receipt written beneath it. They are checked through BOTH constructors because both read operator-controlled environment strings." + +test fn attempt_id_refuses_path_traversal_and_separators() -> Bool { + match compose_explicit_walk_attempt_id(explicit: "../other-attempt") { Present { value: _ } => false Absent => true } + && match compose_explicit_walk_attempt_id(explicit: "a/b") { Present { value: _ } => false Absent => true } + && match compose_explicit_walk_attempt_id(explicit: "..") { Present { value: _ } => false Absent => true } + && match compose_explicit_walk_attempt_id(explicit: ".") { Present { value: _ } => false Absent => true } + && match compose_explicit_walk_attempt_id(explicit: "a\\b") { Present { value: _ } => false Absent => true } + && match compose_walk_attempt_id(run_id: "12345", run_attempt: "1", job: "ci/deploy") { Present { value: _ } => false Absent => true } +} + +test fn attempt_id_refuses_embedded_line_terminators() -> Bool { + match compose_explicit_walk_attempt_id(explicit: "a\nb") { Present { value: _ } => false Absent => true } + && match compose_explicit_walk_attempt_id(explicit: "a\x0db") { Present { value: _ } => false Absent => true } + && match compose_explicit_walk_attempt_id(explicit: "a\x00b") { Present { value: _ } => false Absent => true } + && match compose_walk_attempt_id(run_id: "12345", run_attempt: "1\n2", job: "ci") { Present { value: _ } => false Absent => true } +} + test fn attempt_paths_are_attempt_scoped_and_distinct() -> Bool { - let subj = merge_admission_tested_subject_path(root: "/repo", attempt_id: attempt_a) - let rec_a = merge_admission_floor_receipt_path(root: "/repo", attempt_id: attempt_a) - let rec_b = merge_admission_floor_receipt_path(root: "/repo", attempt_id: attempt_b) + let subj = merge_admission_tested_subject_path(root: "/repo", attempt_id: attempt_a()) + let rec_a = merge_admission_floor_receipt_path(root: "/repo", attempt_id: attempt_a()) + let rec_b = merge_admission_floor_receipt_path(root: "/repo", attempt_id: attempt_b()) string_contains(s: subj, pattern: "/.gunbc/merge-admission/12345-1-ci/") && string_contains(s: rec_a, pattern: "/12345-1-ci/") && !(rec_a == rec_b) diff --git a/dag/test/claim/merge_admission_enforcement_witness_test.dag b/dag/test/claim/merge_admission_enforcement_witness_test.dag index e4adf8ec1f0..3eea9b1d66e 100644 --- a/dag/test/claim/merge_admission_enforcement_witness_test.dag +++ b/dag/test/claim/merge_admission_enforcement_witness_test.dag @@ -131,7 +131,7 @@ test fn wire_stale_base_fails_verdict_parse_path() -> Bool { MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false - MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } Absent => false } @@ -148,6 +148,7 @@ test fn fresh_verdict_is_merge_admitted() -> Bool { MergeDeniedStaleRoster => false MergeDeniedNotSuccess => false MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false } } @@ -159,6 +160,7 @@ test fn red_verdict_is_merge_denied_not_success() -> Bool { ) { MergeDeniedNotSuccess => true MergeDeniedWrongAttempt => false + MergeDeniedSubjectMismatch => false MergeAdmitted => false MergeDeniedStaleBase => false MergeDeniedStaleRoster => false diff --git a/dag/tools/merge_admission_gate.dag b/dag/tools/merge_admission_gate.dag index 1d88d0f93fa..6128737a789 100644 --- a/dag/tools/merge_admission_gate.dag +++ b/dag/tools/merge_admission_gate.dag @@ -11,6 +11,8 @@ import gunbc.merge_admission { MergeDeniedStaleBase, MergeDeniedStaleRoster, MergeDeniedNotSuccess, + MergeDeniedWrongAttempt, + MergeDeniedSubjectMismatch, MergeAdmitted, } import gunbc.merge_admission_produce { @@ -31,6 +33,7 @@ fn verdict_reason(v: MergeAdmissionVerdict) -> String { MergeDeniedStaleRoster => "stale gate roster — re-run CI after criteria change" MergeDeniedNotSuccess => "receipt conclusion is not success" MergeDeniedWrongAttempt => "receipt belongs to a different walk attempt — not the subject; re-run CI" + MergeDeniedSubjectMismatch => "receipt describes a different head or base tree than this attempt captured — not the subject; re-run CI" } } diff --git a/src/v1/05_emit_core_support.dag b/src/v1/05_emit_core_support.dag index 9fa2498bb57..325dde1ca4f 100644 --- a/src/v1/05_emit_core_support.dag +++ b/src/v1/05_emit_core_support.dag @@ -228,6 +228,8 @@ fn language_spec(target: RenderTarget) -> LanguageSpec { language_spec_for_target(target: target) } +data escape_string_literal_control_chars_note: String = "TWO defects, one in each half of the CR step. The DELIMITER used to be \"\\r\", but this language's tokenizer has no \\r escape (its table is \\\" \\\\ \\n \\t \\{ \\} and \\xHH), so that delimiter was the two characters backslash and r, not a carriage return: carriage returns have passed through unescaped into every emitted target for as long as the function has existed, dead in practice only because no corpus string carried one. The first that did turned it into a hard emit failure. The REPLACEMENT was then briefly \\r and \\0, which is a second, subtler version of the same mistake: this function is TARGET-INDEPENDENT — emit_string_literal invokes it for Rust, Dag, Go and Python alike, and never sees a RenderTarget — so a Rust-shaped escape is only correct for one of the four projections, and \\r emitted into a Dag literal reproduces the exact backslash-r bug the delimiter half just fixed (review 2026-07-30). The spelling is therefore \\x0d and \\x00, the hex form all four target grammars accept, and the acceptance is a round trip through every target rather than a Rust regen fixed point, which proves only the Rust projection. Recorded rather than quietly respelled because the class is the point: a target-specific escape inside a target-independent function is invisible until a projection other than the one under test carries the character." + fn escape_string_literal_body(s: String) -> String { let escaped_backslash = s |> split(delimiter: "\\") |> join(separator: "\\\\") @@ -236,8 +238,10 @@ fn escape_string_literal_body(s: String) -> String { let escaped_newline = escaped_quote |> split(delimiter: "\n") |> join(separator: "\\n") let escaped_return = escaped_newline - |> split(delimiter: "\r") |> join(separator: "\\r") - escaped_return + |> split(delimiter: "\x0d") |> join(separator: "\\x0d") + let escaped_nul = escaped_return + |> split(delimiter: "\x00") |> join(separator: "\\x00") + escaped_nul |> split(delimiter: "\t") |> join(separator: "\\t") } diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index e4547723d45..f3dda34ca31 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -583,53 +583,69 @@ struct ParsedWalkPlan { on_success_stages: Vec>, } -/// Parse `WalkFinalization` — the plan-carried policy (walk_finalization_note): the -/// executor never selects finalization by a plan function's spelling. A missing or -/// unrecognized variant is a hard error, so a floor plan without its law is -/// unwritable rather than discovered at arm time. +/// Parse the plan-carried finalization VALUE (walk_finalization_note). The executor +/// never selects finalization by a plan function's spelling, and — since the carrier +/// became `WalkPlan` — it does not need to care which instantiation produced the +/// value either: ONE parser reads both. An unrecognized shape is a hard error, and that +/// refusal is load-bearing rather than belt-and-braces: the plan function's declared +/// return type does NOT bound what its body returns (the typechecker does not check +/// return position), so this parser and the enrolled value witnesses are what actually +/// stop a plan from carrying the wrong finalization family. +/// +/// `Nat` reaches the interpreter as a native `Int` (the numeric tower is grounded), so +/// a negative value cannot arrive from a well-typed plan; it is still refused rather +/// than carried into a count comparison it could only lose. fn finalization_from_value( v: &Value, ctx: &InterpContext, ) -> Result, String> { + // The two inhabitants have DIFFERENT runtime shapes, and that is a consequence of + // the carrier split rather than an accident to paper over: FloorFinalization is a + // standalone record in gunbc.ci_materialization (Value::Record), while + // NoFinalizationDeclared is the nullary variant of std's NoWalkFinalization sum + // (Value::Variant). Both are matched by TYPE NAME — never by "has a field called + // declared_resolve_count", which would admit any record that happened to carry one. + let floor_from_fields = + |fields: &[(v1_compiler::v1_interpreter::Symbol, Value)]| -> Result { + match ctx.field(fields, "declared_resolve_count") { + Some(Value::Int(n)) if *n >= 0 => Ok(*n), + Some(Value::Int(n)) => Err(format!( + "FloorFinalization.declared_resolve_count is Nat, got {n}" + )), + other => Err(format!( + "FloorFinalization.declared_resolve_count must be a Nat, got {other:?}" + )), + } + }; match v { + Value::Record { + type_name, fields, .. + } if ctx.sym_eq(*type_name, "FloorFinalization") => Ok(Some(FloorFinalization { + declared_resolve_count: floor_from_fields(fields)?, + })), Value::Variant { variant_name, fields, .. } => { - if ctx.sym_eq(*variant_name, "NoWalkFinalization") { + if ctx.sym_eq(*variant_name, "NoFinalizationDeclared") { Ok(None) } else if ctx.sym_eq(*variant_name, "FloorFinalization") { - let declared = match ctx.field(fields, "declared_resolve_count") { - Some(Value::Int(n)) => *n, - other => { - return Err(format!( - "FloorFinalization.declared_resolve_count must be an Int, got {other:?}" - )) - } - }; - let disclosure = match ctx.field(fields, "require_materialization_disclosure") { - Some(Value::Bool(b)) => *b, - other => { - return Err(format!( - "FloorFinalization.require_materialization_disclosure must be a Bool, \ - got {other:?}" - )) - } - }; + // Retained because the same declaration can reach the interpreter as a + // record OR as a variant depending on how it was constructed; refusing + // one spelling of a value the model does admit would be a false wall. Ok(Some(FloorFinalization { - declared_resolve_count: declared, - require_materialization_disclosure: disclosure, + declared_resolve_count: floor_from_fields(fields)?, })) } else { - Err(format!( - "WalkPlan.finalization: unknown variant (expected NoWalkFinalization or \ - FloorFinalization)" - )) + Err( + "unknown variant (expected NoFinalizationDeclared or FloorFinalization)" + .to_string(), + ) } } other => Err(format!( - "WalkPlan.finalization must be a WalkFinalization variant, got {}", + "must be a NoFinalizationDeclared or FloorFinalization value, got {}", ctx.format_value(other) )), } @@ -645,8 +661,8 @@ fn walk_plan_from_plan(plan: &Value, ctx: &InterpContext) -> Result fields, other => { return Err(format!( - "expected a WalkPlan record {{ batches, on_success_stages }}, got {} — \ - every plan function returns WalkPlan (std.realization_schedule \ + "expected a WalkPlan record {{ batches, finalization, on_success_stages }}, \ + got {} — every plan function returns WalkPlan (std.realization_schedule \ walk_plan_note); there is deliberately no bare-list fallback", ctx.format_value(other) )) @@ -662,7 +678,7 @@ fn walk_plan_from_plan(plan: &Value, ctx: &InterpContext) -> Result]) -> Vec` where regen/falsifier/plan-artifact return +/// `WalkPlan` — a declaration, not a guarantee: the typechecker +/// does not check return position, so the value is what decides, and the enrolled +/// witnesses in v2.test.claim.ci_floor_plan_witness are what check the value. struct FloorFinalization { declared_resolve_count: i64, - require_materialization_disclosure: bool, } /// Validate the floor's finalization laws against the walk's own records. Returns the /// list of typed refusals (empty = contract satisfied). The receipt FILES keep being /// written by the walk — they are observability — this validates the laws the deleted /// shell steps used to re-derive from those files. +/// +/// `plan_site` is the `::` the value was read from, so a refusal +/// locates the field it actually consumed rather than always pointing at the +/// production authority — the fixture and any future plan declare their own counts. fn validate_floor_finalization( fin: &FloorFinalization, + plan_site: &str, batch_records: &[BatchRecord], ) -> Vec { let mut refusals = Vec::new(); @@ -3239,17 +3268,18 @@ fn validate_floor_finalization( if resolves_total as i64 != fin.declared_resolve_count { refusals.push(format!( "floor resolve count {} differs from declared {}: duplicate-computation debt \ - changed - update ci_floor_declared_resolve_count consciously \ - (dag/gunbc/ci_materialization.dag)", + changed - update the count this plan declared, at \ + {plan_site} WalkPlan.finalization.declared_resolve_count \ + (the production floor projects it from gunbc.ci_materialization \ + ci_floor_declared_resolve_count; a fixture or another plan declares its own)", resolves_total, fin.declared_resolve_count )); } // Law 2 — materialization disclosure (ci_floor_materialization_receipt_note): // receipt exists, keyed/unkeyed/duplicated parse, keyed nonzero. Read from the // file because the accumulator is process-global and already harvested into it. - if !fin.require_materialization_disclosure { - return refusals; - } + // Unconditional: disclosure is intrinsic to FloorFinalization, so there is no + // early return that could skip this law while the caller reports it held. let path = std::path::Path::new("target/floor-materialization-receipt.txt"); match std::fs::read_to_string(path) { Err(_) => refusals.push("floor materialization receipt missing - fail closed".to_string()), @@ -3283,6 +3313,7 @@ fn validate_floor_finalization( fn run_walk( source_roots: &[String], + plan_site: &str, batches: &[Vec], on_success_stages: &[Vec], floor_finalization: Option<&FloorFinalization>, @@ -3589,7 +3620,7 @@ fn run_walk( // materialization gate steps): validated AFTER the receipts wrote and BEFORE the // on-success stages, so a violation blocks admission instead of post-dating it. if let Some(fin) = floor_finalization { - let refusals = validate_floor_finalization(fin, &batch_records); + let refusals = validate_floor_finalization(fin, plan_site, &batch_records); if refusals.is_empty() { if !ordinary_failed { eprintln!( @@ -3922,6 +3953,7 @@ fn run_perturb_check( // serial, matching the prior fixed width-1 semantics. let outcome = run_walk( &[temp_root], + &format!("{plan_entry}::{plan_function} (perturb re-walk)"), &remapped, &[], None, @@ -4353,6 +4385,7 @@ fn run() -> Result { let outcome = run_walk( &source_roots, + &format!("{plan_entry}::{plan_function}"), &batches, &on_success_stages, floor_finalization.as_ref(), @@ -4538,6 +4571,10 @@ mod tests { } } + /// The `::` a refusal locates itself at — the same shape the + /// production caller passes. + const TEST_PLAN_SITE: &str = "src/v2/workflow/ci_floor_plan.dag::gunbc_ci_floor_plan"; + // Floor finalization law 1 (in-executor form of the deleted resolve-receipt gate // step): the count is recomputed from batch records by the same nonzero- // resolve_nanos rule the receipt writer uses. Declared-vs-actual mismatch refuses @@ -4548,10 +4585,9 @@ mod tests { fn floor_finalization_refuses_on_resolve_count_mismatch_both_directions() { let fin = FloorFinalization { declared_resolve_count: 1, - require_materialization_disclosure: true, }; let over = [finalization_record(&[5, 7])]; - let refusals = validate_floor_finalization(&fin, &over); + let refusals = validate_floor_finalization(&fin, TEST_PLAN_SITE, &over); assert!( refusals .iter() @@ -4559,7 +4595,7 @@ mod tests { "over-count must refuse: {refusals:?}" ); let under = [finalization_record(&[])]; - let refusals = validate_floor_finalization(&fin, &under); + let refusals = validate_floor_finalization(&fin, TEST_PLAN_SITE, &under); assert!( refusals .iter() @@ -4572,10 +4608,9 @@ mod tests { fn floor_finalization_matching_count_leaves_only_the_materialization_arm() { let fin = FloorFinalization { declared_resolve_count: 2, - require_materialization_disclosure: true, }; let records = [finalization_record(&[3, 0, 9])]; - let refusals = validate_floor_finalization(&fin, &records); + let refusals = validate_floor_finalization(&fin, TEST_PLAN_SITE, &records); // resolve law satisfied (two nonzero-resolve results); under cargo test no // materialization receipt file exists, so exactly the missing-receipt refusal // remains — proving law 2 fails closed on absence rather than passing. diff --git a/src/v1/stage0/src/std_realization_schedule.rs b/src/v1/stage0/src/std_realization_schedule.rs index 9da34c4b70e..748fe5f29d9 100644 --- a/src/v1/stage0/src/std_realization_schedule.rs +++ b/src/v1/stage0/src/std_realization_schedule.rs @@ -2,10 +2,10 @@ // Source module: std.realization_schedule use self::CostBasis::*; +use self::NoWalkFinalization::*; use self::NodeFrontierSelection::*; use self::Runnable::*; use self::RunnableMemoryClass::*; -use self::WalkFinalization::*; use self::WitnessKind::*; use self::WitnessSpan::*; pub use crate::std_execution_mode::execution_mode_eq; @@ -312,7 +312,7 @@ pub enum Runnable { pub fn walk_plan_note() -> String { thread_local! { static CACHED: String = { - "A walk is TWO populations with DIFFERENT ordering laws, and the type says so where a bare List> could not. `batches` are the ordinary floor: batch boundaries order them, and a failure's consequence is the walk's FloorBatchStopPolicy (StopBeforeDependents on pull_request, FullLedger on push/schedule — where a failed batch deliberately does NOT stop the walk, because the per-batch ledger on main is bisection evidence, operator ruling 2026-07-23). `on_success_stages` run ONLY when the ordinary floor completed AND its receipts finalized and validated; each stage is a barrier — stage N fully completes with zero failures before stage N+1 starts — and stage-to-stage execution is ALWAYS fail-fast, regardless of the ordinary stop policy: FullLedger is an ordinary-floor policy and never applies between stages. WHY THE SECOND POPULATION EXISTS: work whose correctness is conditional on the whole floor being green (the merge-admission stamp is the first occupant — stamping Success is only true if reaching it proves green) cannot be an ordinary trailing batch, because under FullLedger a trailing batch is still reached after a red batch. The prior attempt encoded exactly that and shipped a fail-open; a second attempt then declared stamp-then-gate as one stage and rediscovered the SIBLING defect — members WITHIN a stage run concurrently (distinct entries become distinct spawned units), so intra-stage order does not exist and anything sequential must be ONE claim whose body sequences its steps, or two singleton stages. Both defects are why this is a named type with a note rather than a convention (operator design ruling 2026-07-30).\n\nWHAT THE EXECUTOR ACTUALLY PROVIDES TODAY, stated because a carrier that promises more than its executor delivers is the same defect this type exists to end (review 2026-07-30). The stage BARRIER is real: stage N completes before stage N+1 starts, and a failed stage prevents every later one. THREE GAPS remain, and none is currently reachable because every plan declares an empty stage list: (1) members within a stage run SERIALLY, not concurrently — serial is a strictly stronger order than the contract promises, so no current caller is misled, but wall time, peak memory, and overlap are resource facts a future author would measure wrongly; (2) stages execute through run_memo_shared_claims directly rather than the ordinary unit-lane partition, so they bypass governor admission, batch clamps, and resource-profile enforcement — safe for the negligible admission claims that will occupy them, unsafe for the substantial or host-compiler-spawning claim the generic carrier permits; (3) ONE aggregate stage receipt is written after the whole sequence rather than one per stage before the next begins. The repair is to extract the ordinary batch machinery into a reusable run_stage(stage) — group by entry and mode, acquire governor admission, spawn eligible units, join, write THAT stage receipt — so both populations share one executor and differ only in ordering and failure policy. Until that lands, do not place a Substantial or host-compiler runnable in a stage; the arm-time validator refuses discovery runnables outright, and the profile restriction is the next wall. Every plan function returns WalkPlan — a plan with no postconditions returns on_success_stages: [] — and the executor has ONE strict parser: a malformed or missing field is a hard error, never a fallback to a bare-list reading.".to_string() + "A walk is TWO populations with DIFFERENT ordering laws, and the type says so where a bare List> could not. `batches` are the ordinary floor: batch boundaries order them, and a failure's consequence is the walk's FloorBatchStopPolicy (StopBeforeDependents on pull_request, FullLedger on push/schedule — where a failed batch deliberately does NOT stop the walk, because the per-batch ledger on main is bisection evidence, operator ruling 2026-07-23). `on_success_stages` run ONLY when the ordinary floor completed AND its receipts finalized and validated; each stage is a barrier — stage N fully completes with zero failures before stage N+1 starts — and stage-to-stage execution is ALWAYS fail-fast, regardless of the ordinary stop policy: FullLedger is an ordinary-floor policy and never applies between stages. WHY THE SECOND POPULATION EXISTS: work whose correctness is conditional on the whole floor being green (the merge-admission stamp is the first occupant — stamping Success is only true if reaching it proves green) cannot be an ordinary trailing batch, because under FullLedger a trailing batch is still reached after a red batch. The prior attempt encoded exactly that and shipped a fail-open; a second attempt then declared stamp-then-gate as one stage and rediscovered the SIBLING defect — members WITHIN a stage run concurrently (distinct entries become distinct spawned units), so intra-stage order does not exist and anything sequential must be ONE claim whose body sequences its steps, or two singleton stages. Both defects are why this is a named type with a note rather than a convention (operator design ruling 2026-07-30).\n\nWHAT THE EXECUTOR ACTUALLY PROVIDES TODAY, stated because a carrier that promises more than its executor delivers is the same defect this type exists to end (review 2026-07-30). The stage BARRIER is real: stage N completes before stage N+1 starts, and a failed stage prevents every later one. THREE GAPS remain, and none is currently reachable because every plan declares an empty stage list: (1) members within a stage run SERIALLY, not concurrently — serial is a strictly stronger order than the contract promises, so no current caller is misled, but wall time, peak memory, and overlap are resource facts a future author would measure wrongly; (2) stages execute through run_memo_shared_claims directly rather than the ordinary unit-lane partition, so they bypass governor admission, batch clamps, and resource-profile enforcement — safe for the negligible admission claims that will occupy them, unsafe for the substantial or host-compiler-spawning claim the generic carrier permits; (3) ONE aggregate stage receipt is written after the whole sequence rather than one per stage before the next begins. The repair is to extract the ordinary batch machinery into a reusable run_stage(stage) — group by entry and mode, acquire governor admission, spawn eligible units, join, write THAT stage receipt — so both populations share one executor and differ only in ordering and failure policy. Until that lands, do not place a Substantial or host-compiler runnable in a stage; the arm-time validator refuses discovery runnables outright, and the profile restriction is the next wall. Every plan function returns WalkPlan — a plan with no postconditions returns on_success_stages: [] — and the executor has ONE strict parser: a malformed or missing field is a hard error, never a fallback to a bare-list reading.".to_string() }; } CACHED.with(|c: &String| c.clone()) @@ -321,51 +321,26 @@ pub fn walk_plan_note() -> String { pub fn walk_finalization_note() -> String { thread_local! { static CACHED: String = { - "THE PLAN CARRIES ITS FINALIZATION POLICY; the executor never infers it from a function's spelling. The first cut selected finalization by plan-function name (if plan_function == gunbc_ci_floor_plan read the law from the closure) — the same hidden seed-roster convention the WalkPlan carrier was built to remove, reintroduced in the same PR (review 2026-07-30), and the RED fixture made the coupling visible by having to impersonate the production name to arm the contract. As a FIELD, the policy is part of the parsed value: a floor plan without its law is now UNWRITABLE (the strict parser refuses a missing field) rather than checked at arm time, schedule lenses and plan artifacts can see it, and the fixture declares its own policy instead of name-impersonating into one. NoWalkFinalization is the declared empty policy — regen, falsifier, and the plan-artifact shortcut say so explicitly, never by omission.".to_string() + "THE PLAN CARRIES ITS FINALIZATION POLICY IN ITS TYPE, and the executor never infers it — not from a function's spelling, and not from which arm of a coproduct an authored value happened to pick. Two corrections stacked here. FIRST: the original cut selected finalization by plan-function name (if plan_function == gunbc_ci_floor_plan read the law from the closure) — the same hidden seed-roster convention the WalkPlan carrier was built to remove, reintroduced in the same PR (review 2026-07-30), and the RED fixture made the coupling visible by having to impersonate the production name to arm the contract. Moving it to a field fixed that. SECOND: a field of a coproduct type is still only an authored choice (review 2026-07-30, second pass). With `finalization: WalkFinalization`, `WalkPlan { batches: floor_batches, finalization: NoWalkFinalization, .. }` typechecked — NoWalkFinalization and FloorFinalization inhabit the same sum, so nothing connected floor-shaped work to floor finalization; the production constructor merely chose correctly. So the carrier is PARAMETERIZED: WalkPlan, and gunbc_ci_floor_plan returns WalkPlan while regen, plan-artifact, and falsifier return WalkPlan. One runtime parser still reads both, because the parse is over the finalization VALUE and does not care which instantiation produced it. The parameterization also stops this generic std carrier from owning a growing coproduct of gunbc-specific receipt policies: FloorFinalization moved to gunbc.ci_materialization, beside the declared count it is about, and std keeps only the parameter and the declared-empty inhabitant.\n\nWHAT THE PARAMETERIZATION DOES AND DOES NOT BUY, measured rather than assumed — and the measurement contradicted the intent, so the intent is not what gets written down. The review that requested this asked for a construction wall: the floor's return type should REJECT the empty policy. It does not, today. Probed by execution 2026-07-30: replacing the floor's finalization with NoFinalizationDeclared {} while the signature still reads WalkPlan TYPECHECKS, and fails only later, at the first field access, as a runtime error. A narrower probe isolates the general defect — the typechecker does not check a function's declared return type against its body at all (`fn f() -> Int { \"not an int\" }` typechecks; so does a mismatched generic instantiation), nor a `data` declaration's annotation against its value, while ARGUMENT position is checked and refuses correctly. So this is a §5 WALL-AFTER-GROUNDING, not a wall now: the class is decidable, the single authority it waits on is return-position typechecking, and until that lands the enforcement is honestly VALIDATION — the enrolled witness floor_plan_projects_the_declared_resolve_count_authority (v2.test.claim.ci_floor_plan_witness) reds when the floor stops projecting the declared count, with a forked-count RED control beside it. Saying the signature walls it would be the same overclaim this note's own history is a record of. dissolve-on: return-position type enforcement in the typechecker, at which point the signature becomes the wall and the witness becomes redundant.\n\nLANGUAGE-LAYER FINDING recorded rather than absorbed (§5 workaround rule): a one-variant sum cannot be spelled `type T = OneVariant` — that production is the type-ALIAS form, and the compiler reads OneVariant as an unresolved type name (probed by execution). The nullary variant therefore has to be spelled `= NoFinalizationDeclared {}`, an empty record variant. That is position-dependent meaning for the same syntax (`= A | B` makes A a variant; `= A` makes A an alias target), and it belongs in the grammar-consolidation lane, not in a silent respelling.".to_string() }; } CACHED.with(|c: &String| c.clone()) } -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] #[serde(tag = "_variant")] -pub enum WalkFinalization { - NoWalkFinalization, - FloorFinalization { - declared_resolve_count: i64, - require_materialization_disclosure: bool, - }, -} -impl WalkFinalization { - pub fn declared_resolve_count(&self) -> i64 { - match self { - WalkFinalization::NoWalkFinalization => { - panic!("no declared_resolve_count on unit variant") - } - WalkFinalization::FloorFinalization { - declared_resolve_count: __val, - .. - } => __val.clone(), - } - } - pub fn require_materialization_disclosure(&self) -> bool { - match self { - WalkFinalization::NoWalkFinalization => { - panic!("no require_materialization_disclosure on unit variant") - } - WalkFinalization::FloorFinalization { - require_materialization_disclosure: __val, - .. - } => __val.clone(), - } - } +pub enum NoWalkFinalization { + NoFinalizationDeclared, } #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct WalkPlan { +pub struct WalkPlan { pub batches: Rc>>>>, - pub finalization: Rc, + pub finalization: F, pub on_success_stages: Rc>>>>, + pub _phantom: std::marker::PhantomData, } pub fn node_frontier_selection_applied(sel: NodeFrontierSelection) -> bool { @@ -632,3 +607,5 @@ pub struct SelectionOff; pub struct SelectionApplied; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct SelectionPredictOnly; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct NoFinalizationDeclared; diff --git a/src/v1/stage0/src/std_types.rs b/src/v1/stage0/src/std_types.rs index 52de08824a3..a58ab28be53 100644 --- a/src/v1/stage0/src/std_types.rs +++ b/src/v1/stage0/src/std_types.rs @@ -255,6 +255,25 @@ pub type SecretName = String; pub type PathSegment = String; +pub fn path_segment_safety_note() -> String { + thread_local! { + static CACHED: String = { + "WHAT MAKES A STRING SAFE TO USE AS ONE PATH SEGMENT — the law, held once, so every branded id that becomes a directory name tests the same thing. The brand alone never carried it: a branded NonEmptyStr accepts \"..\", \"a/b\", and an embedded newline, so a value that typechecked as a segment could still escape its parent directory, alias a sibling, or split a line-oriented file written under that name. The refused set is exactly the characters that change what a concatenated path MEANS — `/` and `\\` introduce a level, `.` and `..` navigate, CR and LF terminate a record in every line-oriented format this repo writes, NUL terminates the string at the syscall boundary. Callers REFUSE on false rather than sanitizing, because a sanitized segment silently denotes something other than what the caller named (§5: a failure arm must refuse, never widen). Percent- or hex-encoding is the reversible alternative and is deliberately not offered until a caller needs a segment it cannot rename.\n\nThis is a PREDICATE, not a constructor, and that is a modeling choice rather than a limitation worked around. A generic `path_segment(raw) -> PathSegment?` would put the branding cast in this module, and each caller would then re-cast the generic segment into its own brand anyway — two casts and two authorities for one law. Holding the law here and letting each branded id (gunbc.merge_admission.walk_attempt_id is the first) construct itself through it keeps one authority for what is hostile and one constructor per brand, which is what §3 asks for. A generic constructor earns its place when a second caller wants a bare PathSegment rather than a brand of its own; none does today.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +pub fn path_segment_is_safe(raw: String) -> bool { + !((((((((raw.clone() == "".to_string()) || (raw.clone() == ".".to_string())) + || (raw.clone() == "..".to_string())) + || v1_rt::string_contains(&raw, "/".to_string())) + || v1_rt::string_contains(&raw, "\\".to_string())) + || v1_rt::string_contains(&raw, "\n".to_string())) + || v1_rt::string_contains(&raw, "\x0d".to_string())) + || v1_rt::string_contains(&raw, "\x00".to_string())) +} + pub type GlobSegment = String; #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] diff --git a/src/v1/stage0/src/v1_compiler_emit_core_support.rs b/src/v1/stage0/src/v1_compiler_emit_core_support.rs index 8b0b02a54d6..fd0671c9726 100644 --- a/src/v1/stage0/src/v1_compiler_emit_core_support.rs +++ b/src/v1/stage0/src/v1_compiler_emit_core_support.rs @@ -515,6 +515,15 @@ pub fn language_spec(target: RenderTarget) -> Rc { language_spec_for_target(target.clone()) } +pub fn escape_string_literal_control_chars_note() -> String { + thread_local! { + static CACHED: String = { + "TWO defects, one in each half of the CR step. The DELIMITER used to be \"\\r\", but this language's tokenizer has no \\r escape (its table is \\\" \\\\ \\n \\t \\{ \\} and \\xHH), so that delimiter was the two characters backslash and r, not a carriage return: carriage returns have passed through unescaped into every emitted target for as long as the function has existed, dead in practice only because no corpus string carried one. The first that did turned it into a hard emit failure. The REPLACEMENT was then briefly \\r and \\0, which is a second, subtler version of the same mistake: this function is TARGET-INDEPENDENT — emit_string_literal invokes it for Rust, Dag, Go and Python alike, and never sees a RenderTarget — so a Rust-shaped escape is only correct for one of the four projections, and \\r emitted into a Dag literal reproduces the exact backslash-r bug the delimiter half just fixed (review 2026-07-30). The spelling is therefore \\x0d and \\x00, the hex form all four target grammars accept, and the acceptance is a round trip through every target rather than a Rust regen fixed point, which proves only the Rust projection. Recorded rather than quietly respelled because the class is the point: a target-specific escape inside a target-independent function is invisible until a projection other than the one under test carries the character.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn escape_string_literal_body(s: String) -> String { { let escaped_backslash = Rc::new( @@ -543,13 +552,21 @@ pub fn escape_string_literal_body(s: String) -> String { let escaped_return = Rc::new( escaped_newline .clone() - .split(&"\\r".to_string()) + .split(&"\x0d".to_string()) .map(|s| s.to_string()) .collect::>(), ) - .join(&"\\r".to_string()); - Rc::new( + .join(&"\\x0d".to_string()); + let escaped_nul = Rc::new( escaped_return + .clone() + .split(&"\x00".to_string()) + .map(|s| s.to_string()) + .collect::>(), + ) + .join(&"\\x00".to_string()); + Rc::new( + escaped_nul .clone() .split(&"\t".to_string()) .map(|s| s.to_string()) diff --git a/src/v2/lens/inert_carrier.dag b/src/v2/lens/inert_carrier.dag index 4b8957066e9..2908ac29b09 100644 --- a/src/v2/lens/inert_carrier.dag +++ b/src/v2/lens/inert_carrier.dag @@ -14,7 +14,6 @@ data inert_carrier_roster: List = [ inert_row(unit: "AccessPolicy", reason: "modeled access-policy carrier with no live consumer yet (facts-before-abstraction: the data row lands ahead of its reader)"), inert_row(unit: "CargoDependency", reason: "modeled cargo-manifest carrier awaiting the emitted-crate-partition consumer"), inert_row(unit: "CargoPackage", reason: "modeled cargo-manifest carrier awaiting the emitted-crate-partition consumer"), - inert_row(unit: "FilePermissions", reason: "modeled filesystem-semantics carrier with no live consumer yet"), inert_row(unit: "FloorWitnessRow", reason: "modeled floor-receipt carrier with no live consumer yet"), inert_row(unit: "FreeOutput", reason: "modeled output carrier with no live consumer yet"), inert_row(unit: "GcpProject", reason: "modeled gcp extdeps carrier with no live consumer yet"), diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index 3af0594ba67..ed1a98b97f1 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -6,6 +6,10 @@ import std.realization { import v2.workflow.ci_floor_plan { gunbc_falsifier_ordinary_batches, gunbc_ci_floor_ordinary_batches, + gunbc_ci_floor_plan, + gunbc_ci_regen_floor_plan, + gunbc_ci_plan_artifact_plan, + gunbc_falsifier_plan, floor_schedule_for, corpus_runnable_for, execution_corpus_runnable_for, corpus_witness_entries, execution_witness_entries, @@ -69,6 +73,8 @@ import std.realization_schedule { ScheduleWitnessEntry, schedule_witness_entry_eq, CorpusWitnessKind, ExecutionWitnessKind } +import std.realization_schedule { WalkPlan, NoWalkFinalization, NoFinalizationDeclared } +import gunbc.ci_materialization { FloorFinalization, ci_floor_declared_resolve_count } import std.execution_mode { Hermetic, Wet, execution_mode_eq } import v2.std.algebra { length, list_snoc_item, skip } import v2.std.collection { List } @@ -643,3 +649,57 @@ test fn ci_corpus_discovery_flip_witnesses() -> Bool { && witness_regen_spec_carries_no_witness_corpus() && schedule_discovery_batch_count(batches: floor_schedule_for(spec: zero_roster_spec, serialize_heavy: true)) == 0 } + +data floor_finalization_witness_note: String = "THESE ROWS ARE THE ENFORCEMENT, and that is a correction to what was expected. The review that asked for finalization witnesses expected the parameterized WalkPlan to do the work by construction — the floor's return type rejecting the empty policy — leaving these rows as secondary evidence. Probed by execution: it does not. Substituting NoFinalizationDeclared \{\} into gunbc_ci_floor_plan while its signature still reads WalkPlan typechecks and fails only at the first field access, because the typechecker does not check a declared return type against the body (a narrower probe: `fn f() -> Int \{ \"not an int\" \}` also typechecks, while argument position IS checked). So the signature declares intent and the row below is what actually refuses. std.realization_schedule walk_finalization_note carries the finding and its dissolve-on. + +ONE property is genuinely not witnessable: materialization disclosure is intrinsic to FloorFinalization, so there is no Bool to assert. + +The three no-finalization rows below WERE briefly omitted as tautologies, and that reasoning was wrong (review 2026-07-30, corrected). It assumed the declared return type bounds the runtime value. The probe above shows it does not: a function declared `-> WalkPlan` can return a record carrying FloorFinalization, and a caller reading the signature would never know. Matching the ACTUAL value is therefore load-bearing, not a match over a one-inhabitant type — the inhabitant set at runtime is not one. Their mutation control is to substitute FloorFinalization into each body while leaving the signature unchanged; each corresponding row must red. + +What IS falsifiable is WHICH count the floor projects: any Nat typechecks, so the row below asserts it projects the single authority gunbc.ci_materialization.ci_floor_declared_resolve_count, and the RED control forks that count by one and proves the same predicate refuses. Both execute." + +fn floor_plan_declared_resolve_count() -> Int { + gunbc_ci_floor_plan().finalization.declared_resolve_count +} + +fn plan_declares_authority_count(p: WalkPlan) -> Bool { + p.finalization.declared_resolve_count == ci_floor_declared_resolve_count +} + +fn forked_count_floor_plan() -> WalkPlan { + WalkPlan { + batches: gunbc_ci_floor_ordinary_batches(), + finalization: FloorFinalization { + declared_resolve_count: ci_floor_declared_resolve_count + 1, + }, + on_success_stages: [], + } +} + +test fn floor_plan_projects_the_declared_resolve_count_authority() -> Bool { + plan_declares_authority_count(p: gunbc_ci_floor_plan()) + && floor_plan_declared_resolve_count() == ci_floor_declared_resolve_count +} + +test fn forked_declared_count_is_refused_by_the_same_predicate() -> Bool { + !plan_declares_authority_count(p: forked_count_floor_plan()) +} + +fn plan_carries_no_finalization(plan: WalkPlan) -> Bool { + match plan.finalization { + NoFinalizationDeclared => true + _ => false + } +} + +test fn regen_plan_carries_no_finalization() -> Bool { + plan_carries_no_finalization(plan: gunbc_ci_regen_floor_plan()) +} + +test fn plan_artifact_plan_carries_no_finalization() -> Bool { + plan_carries_no_finalization(plan: gunbc_ci_plan_artifact_plan()) +} + +test fn falsifier_plan_carries_no_finalization() -> Bool { + plan_carries_no_finalization(plan: gunbc_falsifier_plan()) +} diff --git a/src/v2/test/fixture/floor_skip/budget_red_control_plan.dag b/src/v2/test/fixture/floor_skip/budget_red_control_plan.dag index f1dc8b9a945..a7300062052 100644 --- a/src/v2/test/fixture/floor_skip/budget_red_control_plan.dag +++ b/src/v2/test/fixture/floor_skip/budget_red_control_plan.dag @@ -4,9 +4,9 @@ import std.realization_schedule { Runnable, RunnableSingleClaim, WalkPlan, - FloorFinalization, runnable_resource_profile_negligible } +import gunbc.ci_materialization { FloorFinalization } import v2.std.collection { List } import std.types { Int } @@ -20,14 +20,13 @@ fn budget_red_control_claim() -> Runnable { } } -data budget_red_control_declared_resolve_note: String = "The fixture DECLARES its finalization policy in its own plan value (declared 1: exactly one single-claim batch paying exactly one entry resolve) — it no longer needs a name-impersonated projection fn, because the policy is a WalkPlan FIELD (walk_finalization_note): the executor reads the parsed value, and a floor plan without its law is unwritable rather than discovered missing at arm time." +data budget_red_control_declared_resolve_note: String = "The fixture DECLARES its finalization policy in its own plan value (declared 1: exactly one single-claim batch paying exactly one entry resolve) — it no longer needs a name-impersonated projection fn, because the policy is a WalkPlan FIELD (walk_finalization_note): the executor reads the parsed value. The return type WalkPlan declares which family this fixture carries; it does not make the empty policy unwritable, since the typechecker does not check a return type against the body (std.realization_schedule walk_finalization_note). Materialization disclosure is intrinsic to FloorFinalization, so this fixture obligates both floor laws by inhabiting the type — there is no Bool to set." -fn gunbc_ci_floor_plan() -> WalkPlan { +fn gunbc_ci_floor_plan() -> WalkPlan { WalkPlan { batches: [[budget_red_control_claim()]], finalization: FloorFinalization { declared_resolve_count: 1, - require_materialization_disclosure: true, }, on_success_stages: [], } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 75eebbfd346..9326c1865af 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -69,10 +69,10 @@ import std.realization_schedule { runnable_selection_applied, runnable_step_label, WalkPlan, - WalkFinalization, NoWalkFinalization, - FloorFinalization, + NoFinalizationDeclared, } +import gunbc.ci_materialization { FloorFinalization } import v2.lens.schedule_lens { schedule_lens_verdict_for_ci_floor, schedule_lens_batch_has_any_cheap_gate } import v2.std.lens_verdict { Holds, NotApplicable, Unrealized, Violation } import v2.workflow.executor { @@ -1235,39 +1235,38 @@ fn gunbc_ci_plan_artifact_ordinary_batches() -> List> { floor_compile_clean_batch(batches: gunbc_ci_floor_ordinary_batches()) } -data walk_plan_uniformity_note: String = "EVERY plan function returns WalkPlan, including the three with no postconditions — on_success_stages: [] is a declared empty set, not an omission the executor papers over. The executor has ONE strict parser for the record shape; there is deliberately NO fallback from a failed record parse to a bare-List> reading, because that fallback would let a malformed plan silently run with its success stages dropped — the exact silent-widen shape §5 forbids. The `_plan` names replace the `_batches` names in the same motion (operator ruling 2026-07-30): a function whose value now carries postcondition stages must not keep a name that says it returns only batches, or the next author reasonably assumes the stages are not part of the value. The four argv/step consumers follow automatically because they derive from the floor_plan_function / plan_artifact_plan_function / regen_floor_plan_function / falsifier_plan_function constants (gunbc.ci_spec, gunbc.falsifier_workflow) — those constants are the single naming authority, renamed with the functions." +data walk_plan_uniformity_note: String = "EVERY plan function returns WalkPlan, including the three with no postconditions — on_success_stages: [] is a declared empty set, not an omission the executor papers over. The INSTANTIATION is where the four differ: this floor returns WalkPlan while regen, plan-artifact, and falsifier return WalkPlan. That DECLARES the intended finalization family and removes the std-level coproduct fork; it does not enforce either, because the typechecker does not check a declared return type against the body (probed by execution — std.realization_schedule walk_finalization_note carries it). Enforcement is the enrolled value witnesses in v2.test.claim.ci_floor_plan_witness plus the executor's runtime parser, and those dissolve when return-position checking lands. The executor has ONE strict parser for the record shape; there is deliberately NO fallback from a failed record parse to a bare-List> reading, because that fallback would let a malformed plan silently run with its success stages dropped — the exact silent-widen shape §5 forbids. The `_plan` names replace the `_batches` names in the same motion (operator ruling 2026-07-30): a function whose value now carries postcondition stages must not keep a name that says it returns only batches, or the next author reasonably assumes the stages are not part of the value. The four argv/step consumers follow automatically because they derive from the floor_plan_function / plan_artifact_plan_function / regen_floor_plan_function / falsifier_plan_function constants (gunbc.ci_spec, gunbc.falsifier_workflow) — those constants are the single naming authority, renamed with the functions." -fn gunbc_ci_floor_plan() -> WalkPlan { +fn gunbc_ci_floor_plan() -> WalkPlan { WalkPlan { batches: gunbc_ci_floor_ordinary_batches(), finalization: FloorFinalization { declared_resolve_count: ci_floor_declared_resolve_count, - require_materialization_disclosure: true, }, on_success_stages: [], } } -fn gunbc_ci_regen_floor_plan() -> WalkPlan { +fn gunbc_ci_regen_floor_plan() -> WalkPlan { WalkPlan { batches: gunbc_ci_regen_floor_ordinary_batches(), - finalization: NoWalkFinalization, + finalization: NoFinalizationDeclared {}, on_success_stages: [], } } -fn gunbc_ci_plan_artifact_plan() -> WalkPlan { +fn gunbc_ci_plan_artifact_plan() -> WalkPlan { WalkPlan { batches: gunbc_ci_plan_artifact_ordinary_batches(), - finalization: NoWalkFinalization, + finalization: NoFinalizationDeclared {}, on_success_stages: [], } } -fn gunbc_falsifier_plan() -> WalkPlan { +fn gunbc_falsifier_plan() -> WalkPlan { WalkPlan { batches: gunbc_falsifier_ordinary_batches(), - finalization: NoWalkFinalization, + finalization: NoFinalizationDeclared {}, on_success_stages: [], } }