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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 43 additions & 0 deletions dag/extdeps/git/object_store.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 12 additions & 1 deletion dag/gunbc/ci_materialization.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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<FloorFinalization> and every other plan returns WalkPlan<NoWalkFinalization>. 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,
Expand Down
49 changes: 40 additions & 9 deletions dag/gunbc/merge_admission.dag
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -168,6 +169,7 @@ type MergeAdmissionVerdict
| MergeDeniedStaleRoster
| MergeDeniedNotSuccess
| MergeDeniedWrongAttempt
| MergeDeniedSubjectMismatch

data merge_admission_enforcement_policy: AdmissionPolicy = KeyedReceipt

Expand Down Expand Up @@ -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 <root>/.gunbc/merge-admission/<attempt_id>/. 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
Expand All @@ -246,6 +275,7 @@ fn merge_admission_verdict_would_block(v: MergeAdmissionVerdict) -> Bool {
MergeDeniedStaleRoster => true
MergeDeniedNotSuccess => true
MergeDeniedWrongAttempt => true
MergeDeniedSubjectMismatch => true
}
}

Expand Down Expand Up @@ -278,6 +308,7 @@ fn receipt_is_admissible(
MergeDeniedStaleRoster => false
MergeDeniedNotSuccess => false
MergeDeniedWrongAttempt => false
MergeDeniedSubjectMismatch => false
}
}

Expand Down
Loading
Loading