diff --git a/dag/extdeps/git/git.dag b/dag/extdeps/git/git.dag index 413a5e172c0..41c37550bb8 100644 --- a/dag/extdeps/git/git.dag +++ b/dag/extdeps/git/git.dag @@ -845,6 +845,17 @@ fn git_observe_meta_shell_fragment() -> String { // diff-files: each incorporates the index and can therefore report a false difference when the // index is the stale side of the three-way state being diagnosed. +// WHY `DiffNameOnlyNoRenames` EXISTS BESIDE `DiffNameOnly`, WHICH IS THE ONLY DIFFERENCE A READER +// WILL WANT EXPLAINED. `diff.renames` defaults to true, so a pure rename prints only the +// DESTINATION path: over a `git mv a.txt b.txt`, `git diff --name-only HEAD~1 HEAD` prints `b.txt` +// alone while the same diff with `--no-renames` prints `a.txt` and `b.txt` (measured in a scratch +// repository, 2026-09-03). A caller asking which branches touch a path would therefore be told +// nobody touches it by the branch that is DELETING it -- the answer least safe to be wrong about, +// and the reason `gunbc.path_writer_set` requires the rename-blind reading. +// +// They are two operations rather than one with a flag because they model two different upstream +// behaviours -- git's rename-detecting diff and its path-literal diff -- and a caller must choose +// which question it is asking. `DiffNameOnly` remains correct for the destination-only view. service git.Core { operation CurrentBranch { input {} @@ -989,6 +1000,21 @@ service git.Core { } } + operation DiffNameOnlyNoRenames { + input { base: GitRef, head: GitRef = "HEAD" } + output { + paths: List from "stdout_lines" + success: Bool from "exit_success" + stderr: String from "stderr" + } + readonly + transport shell { argv: ["git", "diff", "--name-only", "--no-renames", "{base}", "{head}"] } + exit { + 0 => Unit + 128 => String "Invalid ref or not a git repository" + } + } + operation DiffNameOnlyMerge { input { base: GitRef, head: GitRef = "HEAD" } output { diff --git a/dag/extdeps/github/pulls.dag b/dag/extdeps/github/pulls.dag index eaafe2cc719..75a0038a929 100644 --- a/dag/extdeps/github/pulls.dag +++ b/dag/extdeps/github/pulls.dag @@ -158,7 +158,7 @@ service github.CliPulls { "--repo", "{repo}", "--state", "open", "--limit", "1000", - "--json", "number,title,url,headRefName,headRefOid,isDraft,state,changedFiles", + "--json", "author,number,title,url,headRefName,headRefOid,isDraft,state,changedFiles", ] } } diff --git a/dag/gunbc/cross_pr_contradiction.dag b/dag/gunbc/cross_pr_contradiction.dag index eeb32ebf7ef..9152eb874ec 100644 --- a/dag/gunbc/cross_pr_contradiction.dag +++ b/dag/gunbc/cross_pr_contradiction.dag @@ -388,11 +388,24 @@ type PrDiffObservation | PrDiffEmptyCorroborated { pull_number: Int, head_oid: String } | PrDiffUnobserved { pull_number: Int, cause: PrDiffUnobservedCause } +// `DiffRefused` IS PRODUCED BY NO CALLER IN THIS MODULE, AND THAT IS DELIBERATE. `git.Core.Diff` +// declares only a `diff` output, so a refused diff and an empty one are the same value on this +// instrument's path and the refusal is folded into `DiffEmptyUnderived`. The arm is produced by +// `gunbc.path_writer_set`, whose observation runs `git.Core.DiffNameOnlyNoRenames` and therefore CAN +// tell those apart. +// +// The arm lives HERE rather than in a second cause coproduct because "why a pull request's diff +// could not be observed" is one vocabulary with one set of consequences -- the observation is +// unread, the population is incomplete, the report may not be mistaken for a clean one -- and +// forking it per instrument would give one meaning two spellings (DESIGN section 3). This module +// gains a total arm it does not construct; that is the cost of one authority, and it is smaller +// than the cost of two. type PrDiffUnobservedCause = HeadRefUnresolved { ref_name: String, detail: String } | HeadRefStale { ref_name: String, expected_oid: String, local_oid: String } | MergeBaseUnavailable { head_oid: String, detail: String } | DiffEmptyUnderived { head_oid: String, forge_changed_files: Int } + | DiffRefused { head_oid: String, detail: String } fn pr_diff_unobserved_cause_text(cause: PrDiffUnobservedCause) -> String { match cause { @@ -408,6 +421,11 @@ fn pr_diff_unobserved_cause_text(cause: PrDiffUnobservedCause) -> String { ) MergeBaseUnavailable { head_oid: h, detail: d } => concat(concat("no merge base against ", h), concat(": ", d)) + DiffRefused { head_oid: h, detail: d } => + concat( + concat("the diff against ", h), + concat(" did not run: ", d) + ) DiffEmptyUnderived { head_oid: h, forge_changed_files: n } => concat( concat("the diff against ", h), diff --git a/dag/gunbc/instruments/path_writer_set_instrument.dag b/dag/gunbc/instruments/path_writer_set_instrument.dag new file mode 100644 index 00000000000..08f28f46c20 --- /dev/null +++ b/dag/gunbc/instruments/path_writer_set_instrument.dag @@ -0,0 +1,341 @@ +module tools.path_writer_set_instrument + +import std.types { Bool, GitRef, Int, List, NonEmptyStr, String } +import extdeps.git +import extdeps.git.inspect +import extdeps.github.pulls +import extdeps.languages.json.parse { + parse_json_document, + JsonDocumentParsed, + JsonDocumentUnreadable, + json_document_gap_text, + json_object_unique_member, + JsonMemberFound, + JsonMemberAbsent, + JsonMemberDuplicated, + JsonMemberNotAnObject, + json_string_value_or_empty +} +import extdeps.languages.json.emit { JsonValue, JsonNull, JsonBool, JsonNumber, JsonString, JsonArray, JsonObject } +import gunbc.cli_wire { CliWireResponse } +import gunbc.cross_pr_contradiction { + PrDiffUnobservedCause, + HeadRefUnresolved, + HeadRefStale, + MergeBaseUnavailable, + DiffRefused, + DiffEmptyUnderived +} +import gunbc.path_writer_set { + PullIdentity, + PrPathObservation, + PrPathsRead, + PrPathsEmptyDerived, + PrPathsEmptyCorroborated, + PrPathsUnobserved, + WriterSetReport, + writer_set_report, + writer_set_response, + writer_set_refusal +} + +// THE WRITER-SET INSTRUMENT: the observation half. +// +// The model, the match rule, the completeness contract and every reason this exists are in +// `gunbc.path_writer_set`. This module only supplies the live population -- the open pull requests +// and the paths each one changes -- and hands the model's answer to the host to print. +// +// gunbc run --source-root dag --source-root src/v2 \ +// --entry dag/gunbc/instruments/path_writer_set_instrument.dag --function writers \ +// --arg repo=gunb-ai/gunbc --arg path=dag/gunbc/pr_digests.dag +// +// A subject ending in `/` asks about a subtree: `--arg path=dag/gunbc/instruments/`. +// +// THE ANSWER IS PRINTED, NOT WRITTEN TO A FILE, and that is a difference from its scanning +// neighbours rather than an oversight. `cross_pr_contradiction_instrument` requires a report path +// because it produces a corpus-wide scan someone reads later; this produces a handful of rows in +// answer to a question asked a moment ago, and routing that through a temporary file would put a +// filesystem write between an operator and their own answer. `gunbc.cli_wire` is the modeled route +// for exactly this, and `gunbc.scm.cli` is its existing consumer. +// +// THE DIFF IS READ FROM THE LOCAL CLONE, NOT FROM THE FORGE, and the staleness that invites is +// closed by construction rather than by hoping the clone is fresh -- the mechanism is the one +// `cross_pr_contradiction_instrument` established and its reasoning is not repeated here. GitHub is +// the authority for WHICH pull requests are open and what each head commit IS; the local object +// store is the authority for what that commit CONTAINS, so a local ref disagreeing with the head +// oid GitHub reports REFUSES that pull request by name. A prune-fetch runs first so the ordinary +// case converges rather than refusing. +// +// IT READS. The only GitHub operation invoked below is `github.CliPulls.ListOpenJson`, which is +// `readonly`; the only git operations are fetch-prune, ref resolution, merge-base and a name-only +// diff. A reviewer checking that claim should grep this module for a `github.` call and find one. + +type PullRequestRow { + pull: PullIdentity + head_oid: String + changed_files: Int +} + +type PullRequestRowsRead + = PullRequestRowsParsed { rows: List } + | PullRequestRowsUnreadable { detail: String } + +fn json_member_string(value: JsonValue, key: String) -> String { + match json_object_unique_member(v: value, key: key) { + JsonMemberFound { value: found } => json_string_value_or_empty(v: found) + JsonMemberAbsent => "" + JsonMemberDuplicated { count: _ } => "" + JsonMemberNotAnObject => "" + } +} + +// THE AUTHOR IS A NESTED OBJECT IN THE FORGE'S LISTING (`author.login`), so it is read through two +// member lookups rather than one. An unreadable author is spelled `(author unread)` rather than +// left blank: a blank column reads as a real empty name, and this instrument's whole output is a +// list of people to talk to. +fn json_member_author_login(value: JsonValue) -> String { + match json_object_unique_member(v: value, key: "author") { + JsonMemberFound { value: author } => { + let login = json_member_string(value: author, key: "login") + if login == "" { "(author unread)" } else { login } + } + JsonMemberAbsent => "(author unread)" + JsonMemberDuplicated { count: _ } => "(author unread)" + JsonMemberNotAnObject => "(author unread)" + } +} + +// A JSON NUMBER THAT COULD NOT BE READ IS NOT ZERO. `changedFiles` is legitimately 0 for a +// contentless pull request and that value is what decides whether an empty diff is CORROBORATED or +// a refusal, so folding "absent" into 0 would let a listing-shape change silently promote every +// unreadable row to "the forge agrees this branch is empty". +type JsonIntField + = JsonIntPresent { value: Int } + | JsonIntUnreadable + +fn json_member_int(value: JsonValue, key: String) -> JsonIntField { + match json_object_unique_member(v: value, key: key) { + JsonMemberFound { value: found } => + match found { + JsonNumber { lexeme: lex } => JsonIntPresent { value: parse_int(s: lex as String) } + JsonNull => JsonIntUnreadable + JsonBool { value: _ } => JsonIntUnreadable + JsonString { value: _ } => JsonIntUnreadable + JsonArray { elements: _ } => JsonIntUnreadable + JsonObject { members: _ } => JsonIntUnreadable + } + JsonMemberAbsent => JsonIntUnreadable + JsonMemberDuplicated { count: _ } => JsonIntUnreadable + JsonMemberNotAnObject => JsonIntUnreadable + } +} + +type PullRequestRowRead + = PullRequestRowOk { row: PullRequestRow } + | PullRequestRowUnreadable + +fn pull_request_row(value: JsonValue) -> PullRequestRowRead { + match json_member_int(value: value, key: "number") { + JsonIntUnreadable => PullRequestRowUnreadable + JsonIntPresent { value: number } => + match json_member_int(value: value, key: "changedFiles") { + JsonIntUnreadable => PullRequestRowUnreadable + JsonIntPresent { value: changed_files } => { + let head_ref_name = json_member_string(value: value, key: "headRefName") + let head_oid = json_member_string(value: value, key: "headRefOid") + if number <= 0 || head_ref_name == "" || head_oid == "" || changed_files < 0 { + PullRequestRowUnreadable + } else { + PullRequestRowOk { + row: PullRequestRow { + pull: PullIdentity { + number: number, + author: json_member_author_login(value: value), + head_ref_name: head_ref_name, + title: json_member_string(value: value, key: "title") + }, + head_oid: head_oid, + changed_files: changed_files + } + } + } + } + } + } +} + +fn pull_request_row_read_is_ok(read: PullRequestRowRead) -> Bool { + match read { + PullRequestRowOk { row: _ } => true + PullRequestRowUnreadable => false + } +} + +fn pull_request_rows(listing: String) -> PullRequestRowsRead { + match parse_json_document(s: listing) { + JsonDocumentUnreadable { gap: gap } => + PullRequestRowsUnreadable { + detail: concat("gh pr list --json output is ", json_document_gap_text(gap: gap)) + } + JsonDocumentParsed { value: value } => + match value { + JsonArray { elements: elements } => { + let reads = map(elements, element => pull_request_row(value: element)) + let broken = filter(reads, read => !pull_request_row_read_is_ok(read: read)) + if broken.length() > 0 { + PullRequestRowsUnreadable { + detail: concat( + to_string(broken.length()), + " listed pull request(s) carried no readable number, head ref name, head oid, or changed-file count — the listing shape changed and no writer set may be reported over it" + ) + } + } else { + PullRequestRowsParsed { + rows: flat_map( + reads, + read => match read { + PullRequestRowOk { row: row } => [row] + PullRequestRowUnreadable => [] + } + ) + } + } + } + JsonNull => PullRequestRowsUnreadable { detail: "gh pr list returned a JSON null, not an array" } + JsonBool { value: _ } => PullRequestRowsUnreadable { detail: "gh pr list returned a JSON boolean, not an array" } + JsonNumber { lexeme: _ } => PullRequestRowsUnreadable { detail: "gh pr list returned a JSON number, not an array" } + JsonString { value: _ } => PullRequestRowsUnreadable { detail: "gh pr list returned a JSON string, not an array" } + JsonObject { members: _ } => PullRequestRowsUnreadable { detail: "gh pr list returned a JSON object, not an array" } + } + } +} + +// ONE PULL REQUEST. Every arm that cannot answer produces a NAMED refusal carrying the pull request, +// and none of them produces an empty path list. +// +// THE DIFF IS TAKEN AGAINST THE MERGE BASE, computed here and passed to the two-dot operation. That +// is the same revision pair `base...head` names, resolved by this module rather than by git's range +// syntax -- and the merge base is needed here anyway, because whether the head is an ancestor of the +// base is what separates a DERIVED empty branch from an unread one. +// +// RENAME DETECTION IS OFF: `DiffNameOnlyNoRenames`, for the reason `gunbc.path_writer_set` +// `diff_path_scope_text` states -- a branch that renames or deletes the subject is a writer of it, +// and git's default would print only the destination path. +fn observe_pull_request(base: String, repository_path: String, row: PullRequestRow) -> PrPathObservation { + let local_ref = concat("origin/", row.pull.head_ref_name) + let resolved = git.Inspect.ResolveRefCommit(ref: local_ref as GitRef) + if !resolved.success || (resolved.sha as String) == "" { + PrPathsUnobserved { + pull: row.pull, + cause: HeadRefUnresolved { ref_name: local_ref, detail: resolved.stderr } + } + } else { + let local_oid = resolved.sha as String + if local_oid != row.head_oid { + PrPathsUnobserved { + pull: row.pull, + cause: HeadRefStale { ref_name: local_ref, expected_oid: row.head_oid, local_oid: local_oid } + } + } else { + let baseline = git.Inspect.MergeBase( + repository_path: repository_path, + left: base as GitRef, + right: local_oid as GitRef + ) + if !baseline.success || (baseline.sha as String) == "" { + PrPathsUnobserved { + pull: row.pull, + cause: MergeBaseUnavailable { head_oid: local_oid, detail: baseline.stderr } + } + } else { + if (baseline.sha as String) == local_oid { + PrPathsEmptyDerived { pull: row.pull, head_oid: local_oid } + } else { + let observed = git.Core.DiffNameOnlyNoRenames( + base: (baseline.sha as String) as GitRef, + head: local_oid as GitRef + ) + if !observed.success { + PrPathsUnobserved { + pull: row.pull, + cause: DiffRefused { head_oid: local_oid, detail: observed.stderr } + } + } else { + let touched = map(observed.paths, p => p as String) + if touched.length() == 0 { + if row.changed_files == 0 { + PrPathsEmptyCorroborated { pull: row.pull, head_oid: local_oid } + } else { + PrPathsUnobserved { + pull: row.pull, + cause: DiffEmptyUnderived { head_oid: local_oid, forge_changed_files: row.changed_files } + } + } + } else { + PrPathsRead { pull: row.pull, head_oid: local_oid, touched: touched } + } + } + } + } + } + } +} + +// A LOOKUP THAT NEVER GOT ITS POPULATION IS A REFUSAL, NOT AN EMPTY WRITER SET. A failed fetch, a +// refused listing or a listing whose shape changed all end here rather than producing a report with +// zero observations in it, because `writer_set_report` over an empty observation list would render +// a complete, believable "nobody is writing this". +type WriterSetScan + = WriterSetScanned { report: WriterSetReport } + | WriterSetScanRefused { stage: String, detail: String } + +fn scan_writer_set(repo: String, subject: String, base: String, repository_path: String) -> WriterSetScan { + let fetched = git.Core.FetchPrune(remote: "origin") + if !fetched.success { + WriterSetScanRefused { stage: "fetch", detail: concat("git fetch --prune origin refused: ", fetched.stderr) } + } else { + let listing = github.CliPulls.ListOpenJson(repo: repo as NonEmptyStr) + if !listing.success { + WriterSetScanRefused { stage: "listing", detail: concat("gh pr list refused: ", listing.stderr) } + } else { + match pull_request_rows(listing: listing.stdout) { + PullRequestRowsUnreadable { detail: detail } => + WriterSetScanRefused { stage: "listing_shape", detail: detail } + PullRequestRowsParsed { rows: rows } => + WriterSetScanned { + report: writer_set_report( + subject: subject, + observations: map( + rows, + row => observe_pull_request(base: base, repository_path: repository_path, row: row) + ) + ) + } + } + } + } +} + +fn writer_set_scan_response(scan: WriterSetScan) -> CliWireResponse { + match scan { + WriterSetScanned { report: report } => writer_set_response(report: report) + WriterSetScanRefused { stage: stage, detail: detail } => + writer_set_refusal(reason: concat(concat(stage, "\t"), detail)) + } +} + +fn writers(repo: String, path: String) -> CliWireResponse { + if repo == "" { + writer_set_refusal(reason: "writers: --arg repo= is required") + } else { + if path == "" { + writer_set_refusal( + reason: "writers: --arg path= is required — the writer set is a query about one subject, and a missing subject is not an empty one" + ) + } else { + writer_set_scan_response( + scan: scan_writer_set(repo: repo, subject: path, base: "origin/main", repository_path: ".") + ) + } + } +} diff --git a/dag/gunbc/path_writer_set.dag b/dag/gunbc/path_writer_set.dag new file mode 100644 index 00000000000..330c96be0b6 --- /dev/null +++ b/dag/gunbc/path_writer_set.dag @@ -0,0 +1,400 @@ +module gunbc.path_writer_set + +import std.types { Bool, Int, List, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.render { + Document, + Leaf, + RenderFrame, + Append, + RenderCapability, + plain_line +} +import std.symbols { Ascii } +import extdeps.render.surface { RenderTarget, PlainTerminal } +import gunbc.cli_wire { CliWireResponse, cli_wire_response } +import gunbc.cross_pr_contradiction { + PrDiffUnobservedCause, + pr_diff_unobserved_cause_text +} + +// THE WRITER SET FOR A CONTENDED AUTHORITY. +// +// WHAT IT ANSWERS. Given one path, WHO IS CURRENTLY WRITING IT -- every open pull request whose +// diff against its own merge base touches that path. One question, asked of the live fleet, printed. +// +// WHY IT IS WORTH ASKING. This repository's authorities are single by construction (DESIGN section +// 3), which makes them contention points: one file is where a concept lives, so every lane touching +// that concept edits that file. A lane about to restructure a module cannot see, from its own +// branch, that three other branches are already rewriting it -- the conflict is created at authoring +// time and discovered at merge time, by whoever lands second. The displaced cost is the rework the +// later lane pays, and it is paid in full every time. This answers the question BEFORE the edit. +// +// IT REPORTS. Nothing here closes, comments, edits, rebases or merges. The report is the deliverable. +// +// WHAT THIS IS NOT, AND THE NEIGHBOUR IT DELIBERATELY DOES NOT WIDEN INTO. +// `gunbc.cross_pr_contradiction` reads the same population and asks a different question: whether +// two branches move one ROSTER IDENTITY in opposite directions. It states in its own header that a +// same-direction overlap index is out of scope for it, because 45 of the 53 multi-PR keys its hand +// run found were same-direction and would have buried the one row that mattered. That ruling is +// correct FOR A SCAN over the whole corpus, and it is exactly why this is a QUERY: the subject is +// supplied by the asker, so there is no population to bury a finding in. The two share the +// observation vocabulary -- `PrDiffUnobservedCause` is imported, not re-coined -- and share nothing +// else, because the grains genuinely differ: that instrument extracts quoted identities from a +// unified diff, this one reads a path list. +// +// THE RUNG IS `mitigatable`, AND THE CEILING IS NAMED. This is an advisory reader over open pull +// requests; it gates nothing, and no report can make a concurrent edit unwritable. Nothing above +// mitigation is reachable for it: what is being prevented is two humans choosing to edit one file, +// which is not a state a compiler can refuse. NEXT-RUNG TRIGGER: none -- this class's ceiling is +// mitigation, and the ceiling is REACHED rather than stalled below. + +// --------------------------------------------------------------------------------------------- +// THE SUBJECT AND WHAT COUNTS AS TOUCHING IT. +// +// THE MATCH RULE IS DERIVED FROM THE SUBJECT'S OWN SPELLING, and it travels with the report on its +// own row. A query whose scope is implicit is the one that quietly answers a narrower question than +// it was asked: `dag/gunbc` meaning "that file" and `dag/gunbc` meaning "that subtree" are different +// questions with different writer sets, and a rule that guesses between them decides for the asker +// while reporting itself complete. So the trailing separator SAYS which was asked, and the report +// prints the rule it used. +type PathMatchRule + = ExactPath + | DirectoryPrefix + +fn path_match_rule(subject: String) -> PathMatchRule { + if ends_with(s: subject, suffix: "/") { DirectoryPrefix } else { ExactPath } +} + +fn path_match_rule_text(rule: PathMatchRule) -> String { + match rule { + ExactPath => + "exact path equality — the subject names one file (end the subject with `/` to ask about a subtree)" + DirectoryPrefix => + "directory prefix — the subject ends with `/`, so every changed path beneath it counts" + } +} + +fn path_touches_subject(changed: String, subject: String, rule: PathMatchRule) -> Bool { + match rule { + ExactPath => changed == subject + DirectoryPrefix => starts_with(s: changed, prefix: subject) + } +} + +// RENAMES ARE THE REASON THE OBSERVATION MUST BE TAKEN WITHOUT RENAME DETECTION, and this is where +// that requirement is recorded rather than left to whoever next edits the observation half. +// +// git's `diff.renames` defaults to true, so a pure rename reports only the DESTINATION path +// (measured: `git mv a.txt b.txt` then `git diff --name-only HEAD~1 HEAD` prints `b.txt` alone, +// while `--no-renames` prints both). The branch RENAMING OR DELETING the contended authority is +// precisely the writer a lane most needs to know about, and rename detection makes it invisible. +// `extdeps.git.git` therefore carries `DiffNameOnlyNoRenames` as its own operation, and this scope +// value is printed so a report taken any other way is legible as a different observation. +type DiffPathScope + = | EveryChangedPathBothSidesOfARename + +fn diff_path_scope_text(scope: DiffPathScope) -> String { + match scope { + EveryChangedPathBothSidesOfARename => + "every changed path, rename detection disabled — a branch renaming or deleting the subject is a writer of it" + } +} + +data writer_set_diff_scope: DiffPathScope = EveryChangedPathBothSidesOfARename + +// --------------------------------------------------------------------------------------------- +// WHO A WRITER IS. +// +// "WHO" IS THE PULL REQUEST, ITS BRANCH AND ITS AUTHOR, NOT A NUMBER. The asker's next action is +// to read a branch or talk to somebody, and a bare integer supports neither. All four fields are +// read from the forge's own listing, so none of them is inferred. +// +// THE BRANCH IS THE IDENTIFYING COLUMN IN THIS FLEET, AND THE AUTHOR IS THE COARSER ONE. Measured +// on gunb-ai/gunbc (2026-09-03, `gh pr list --state open --json author`): 39 of 55 open pull +// requests report `author.login` as `app/gunbai-bot` and 16 report a human login, because the +// sessions that do most of the writing push through one app installation. So `author` separates +// automation from human and no further, while `head_ref_name` -- which carries the session name -- +// is what tells two automated writers apart. +// +// Both are carried, and the first draft of this annotation is the reason to say why. It asserted +// that EVERY open pull request is authored by the bot, from a three-row sample; the first live run +// of this instrument printed a human-authored writer and refuted it. The claim that survives is the +// weaker one above, and the row that survives carries both fields -- dropping `author` would make +// this module assert that the branch name IS the author, which is a fact about this repository's +// current automation rather than about pull requests. +type PullIdentity { + number: Int + author: String + head_ref_name: String + title: String +} + +fn pull_identity_text(pull: PullIdentity) -> String { + concat( + concat("#", to_string(pull.number)), + concat( + concat("\t", pull.author), + concat(concat("\t", pull.head_ref_name), concat("\t", pull.title)) + ) + ) +} + +// --------------------------------------------------------------------------------------------- +// ONE PULL REQUEST'S OBSERVATION. +// +// EMPTY IS NOT ABSENT, AND THIS COPRODUCT IS WHERE THAT IS ENFORCED -- the same discipline +// `gunbc.cross_pr_contradiction` establishes for its own observation, and for a sharper reason here. +// This query's most common true answer is "nobody", so an instrument that renders "I could not read +// this pull request" as "this pull request touches nothing" produces the answer the asker is most +// likely to accept without checking, from an observation that was never made. The whole value of +// the query is that a clean "nobody" can be trusted, and it can only be trusted if an unread branch +// is spelled differently from a branch that touches nothing. +// +// The two admissible emptinesses are the ones its neighbour derived and are kept apart for its +// reasons: DERIVED means the head is an ancestor of the base, so the branch contains nothing; +// CORROBORATED means the forge reports zero changed files and the local diff agrees. +type PrPathObservation + = PrPathsRead { pull: PullIdentity, head_oid: String, touched: List } + | PrPathsEmptyDerived { pull: PullIdentity, head_oid: String } + | PrPathsEmptyCorroborated { pull: PullIdentity, head_oid: String } + | PrPathsUnobserved { pull: PullIdentity, cause: PrDiffUnobservedCause } + +fn pr_path_observation_pull(observation: PrPathObservation) -> PullIdentity { + match observation { + PrPathsRead { pull: p, head_oid: _, touched: _ } => p + PrPathsEmptyDerived { pull: p, head_oid: _ } => p + PrPathsEmptyCorroborated { pull: p, head_oid: _ } => p + PrPathsUnobserved { pull: p, cause: _ } => p + } +} + +fn pr_path_observation_is_unobserved(observation: PrPathObservation) -> Bool { + match observation { + PrPathsRead { pull: _, head_oid: _, touched: _ } => false + PrPathsEmptyDerived { pull: _, head_oid: _ } => false + PrPathsEmptyCorroborated { pull: _, head_oid: _ } => false + PrPathsUnobserved { pull: _, cause: _ } => true + } +} + +// --------------------------------------------------------------------------------------------- +// THE JOIN. +// +// A WRITER ROW CARRIES THE PATHS THAT MATCHED, NOT A BOOLEAN. Under `ExactPath` that list is the +// subject and says nothing new; under `DirectoryPrefix` it is the whole content of the answer -- +// "this branch is somewhere under dag/gunbc" is not actionable, "this branch rewrites +// dag/gunbc/pr_digests.dag" is. Carrying the evidence for the verdict beside the verdict is the +// same choice `KeyDirections` makes next door, for the same reason. +type WriterRow { + pull: PullIdentity + head_oid: String + matched: List +} + +fn observation_writer_row( + observation: PrPathObservation, + subject: String, + rule: PathMatchRule +) -> List { + match observation { + PrPathsRead { pull: pull, head_oid: oid, touched: touched } => { + let matched = filter(touched, p => path_touches_subject(changed: p, subject: subject, rule: rule)) + if matched.length() == 0 { + [] + } else { + [WriterRow { pull: pull, head_oid: oid, matched: matched }] + } + } + PrPathsEmptyDerived { pull: _, head_oid: _ } => [] + PrPathsEmptyCorroborated { pull: _, head_oid: _ } => [] + PrPathsUnobserved { pull: _, cause: _ } => [] + } +} + +type WriterSetReport { + subject: String + rule: PathMatchRule + scope: DiffPathScope + observations: List + writers: List +} + +fn writer_set_report(subject: String, observations: List) -> WriterSetReport { + let rule = path_match_rule(subject: subject) + WriterSetReport { + subject: subject, + rule: rule, + scope: writer_set_diff_scope, + observations: observations, + writers: flat_map( + observations, + o => observation_writer_row(observation: o, subject: subject, rule: rule) + ) + } +} + +fn report_unobserved(report: WriterSetReport) -> List { + filter(report.observations, o => pr_path_observation_is_unobserved(observation: o)) +} + +// COMPLETENESS IS A PROPERTY OF THE OBSERVATION, NOT OF THE FINDING, and here it decides whether +// the ANSWER may be believed rather than merely how many rows it has. A writer this report names is +// real whatever else failed; what it may never do is let "no writers listed" be read as "nobody is +// writing this" over a population it could not fully read. The exit status is bound to THIS. +fn report_is_complete(report: WriterSetReport) -> Bool { + report_unobserved(report: report).length() == 0 +} + +// --------------------------------------------------------------------------------------------- +// THE REPORT AS LINES. + +fn writer_row_lines(row: WriterRow) -> List { + append( + [ + concat( + concat("writer\t", pull_identity_text(pull: row.pull)), + concat("\t", row.head_oid) + ) + ], + items: map(row.matched, p => concat(" touches\t", p)) + ) +} + +fn unobserved_line(observation: PrPathObservation) -> List { + match observation { + PrPathsUnobserved { pull: pull, cause: cause } => + [ + concat( + concat("unobserved\t", pull_identity_text(pull: pull)), + concat("\t", pr_diff_unobserved_cause_text(cause: cause)) + ) + ] + PrPathsRead { pull: _, head_oid: _, touched: _ } => [] + PrPathsEmptyDerived { pull: _, head_oid: _ } => [] + PrPathsEmptyCorroborated { pull: _, head_oid: _ } => [] + } +} + +// NOBODY IS AN ANSWER AND IS SAID IN WORDS. A report whose writer list is empty renders as a header +// and then nothing, which is indistinguishable to a reader from a report that failed to render its +// rows -- the empty-observation narrow carried to a human. The sentence is only reachable when the +// population was fully read, because that is the only state in which it is true. +fn writer_summary_lines(report: WriterSetReport) -> List { + if report.writers.length() > 0 { + flat_map(report.writers, row => writer_row_lines(row: row)) + } else { + if report_is_complete(report: report) { + [concat("no open pull request touches ", report.subject)] + } else { + [ + concat( + "no writer found among the pull requests that COULD be read — the population is incomplete, so this is not the answer `nobody is writing ", + concat(report.subject, "`") + ) + ] + } + } +} + +// NO SUMMARY KEY IS A PREFIX OF A ROW KEY, AND THAT IS THE POINT OF THE `total_` PREFIXES. +// +// The first cut of this renderer wrote the count as `writers8` above rows spelled +// `writer#10263...`. Both match `^writer`, so the obvious way to count the answer -- +// `grep -c '^writer'` -- returns EIGHT PLUS ONE, silently, by counting the header as a datum. That +// is not hypothetical: it is how this instrument's own author first misreported its output, while +// the tool printed the correct number the whole time. `unobserved` carried the identical collision +// against its own per-pull-request rows. +// +// A note in the header telling readers to mind the summary row would be a rule, and a rule is not a +// firing mechanism. The shape is. So the summary keys are renamed until the naive command is +// CORRECT rather than merely warned about: with `total_writers` and `total_unobserved`, +// `grep -c '^writer'` and `grep -c '^unobserved'` both yield exactly the row count they look like +// they yield. The miscount is not detected, it is unwritable -- the section 4b move from validation +// to construction, applied to an output format. +// +// `writer_set_row_keys_do_not_collide_with_summary_keys` is the executing evidence, and it goes red +// on any future summary key that reintroduces the prefix. +fn writer_set_lines(report: WriterSetReport) -> List { + append( + append( + [ + concat("subject\t", report.subject), + concat("match_rule\t", path_match_rule_text(rule: report.rule)), + concat("diff_scope\t", diff_path_scope_text(scope: report.scope)), + concat("total_pull_requests\t", to_string(report.observations.length())), + concat("total_unobserved\t", to_string(report_unobserved(report: report).length())), + concat("total_writers\t", to_string(report.writers.length())) + ], + items: writer_summary_lines(report: report) + ), + items: flat_map(report.observations, o => unobserved_line(observation: o)) + ) +} + +// --------------------------------------------------------------------------------------------- +// THE ANSWER AND THE VERDICT, WHICH ARE TWO FACTS. +// +// FINDING WRITERS IS A SUCCESSFUL QUERY. Contention is what was asked about, so exiting nonzero on +// a nonempty writer set would report the instrument's subject as the instrument's failure and make +// a script unable to tell a contended path from a broken lookup. Failing to READ some pull request +// exits nonzero, for the reason `report_is_complete` states. +fn writer_set_exit(report: WriterSetReport) -> ProcessExit { + if report_is_complete(report: report) { + ExitSuccess + } else { + exit_failure( + reason: concat( + to_string(report_unobserved(report: report).length()), + " open pull request(s) could not be read — the printed writer set is real but is not known to be complete" + ) + ) + } +} + +// THE CAPABILITY IS DECLARED, NOT DETECTED -- the same standing choice `gunbc.scm.cli` makes and +// for its reason: no colour, ASCII, no cursor addressing is the floor every terminal meets, and a +// module that cannot observe the real terminal must not fabricate one. When a host learns to report +// a capability it passes one in and these rows become the fallback rather than the answer. +data plain_terminal_capability: RenderCapability = RenderCapability { + color: false, + tier: Ascii, + cursor_addressable: false +} + +data plain_terminal_target: RenderTarget = PlainTerminal + +fn text_lines_document(lines: List) -> Document { + Document { + blocks: [ + Leaf { + frame: RenderFrame { + lines: map(lines, l => plain_line(text: l)), + cursor_action: Append + } + } + ] + } +} + +// THE REFUSAL STILL PRINTS. A query invoked without a subject has no writer set to report and an +// operator who must be told why; `CliWireResponse` carries exactly that pair, and the argument that +// a refusal should print nothing and exit nonzero loses to the one this repository already made +// when it built that carrier. +fn writer_set_refusal(reason: String) -> CliWireResponse { + cli_wire_response( + doc: text_lines_document(lines: [concat("refused\t", reason)]), + target: plain_terminal_target, + capability: plain_terminal_capability, + exit: exit_failure(reason: reason) + ) +} + +fn writer_set_response(report: WriterSetReport) -> CliWireResponse { + cli_wire_response( + doc: text_lines_document(lines: writer_set_lines(report: report)), + target: plain_terminal_target, + capability: plain_terminal_capability, + exit: writer_set_exit(report: report) + ) +} diff --git a/dag/test/claim/path_writer_set_witness_test.dag b/dag/test/claim/path_writer_set_witness_test.dag new file mode 100644 index 00000000000..627a9ab6751 --- /dev/null +++ b/dag/test/claim/path_writer_set_witness_test.dag @@ -0,0 +1,307 @@ +module test.claim.path_writer_set_witness_test + +import std.types { Bool, Int, List, String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.cross_pr_contradiction { HeadRefStale, DiffRefused, DiffEmptyUnderived } +import gunbc.path_writer_set { + PathMatchRule, + ExactPath, + DirectoryPrefix, + path_match_rule, + path_match_rule_text, + path_touches_subject, + PullIdentity, + PrPathObservation, + PrPathsRead, + PrPathsEmptyDerived, + PrPathsEmptyCorroborated, + PrPathsUnobserved, + WriterSetReport, + writer_set_report, + report_is_complete, + report_unobserved, + writer_set_lines, + writer_set_exit, + diff_path_scope_text, + writer_set_diff_scope +} +import std.process { ProcessExit, ExitSuccess, ExitFailure } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE DISCRIMINATING FIXTURES FOR THE WRITER-SET QUERY. +// +// Every subject here is authored in this file. The live population is the open pull requests, which +// change hourly, so a witness reading them would assert whatever the fleet happened to be doing and +// could not go red on a defect. These fixtures cannot lose their subject. + +fn pull(number: Int, author: String) -> PullIdentity { + PullIdentity { + number: number, + author: author, + head_ref_name: concat("session/branch-", to_string(number)), + title: concat("some work on ", to_string(number)) + } +} + +fn read_of(number: Int, author: String, touched: List) -> PrPathObservation { + PrPathsRead { pull: pull(number: number, author: author), head_oid: concat("oid-", to_string(number)), touched: touched } +} + +data subject_file: String = "dag/gunbc/fixture_contended_authority.dag" + +// --------------------------------------------------------------------------------------------- +// THE MATCH RULE. + +// THE RULE IS DERIVED FROM THE SPELLING, AND THE TWO SPELLINGS ASK DIFFERENT QUESTIONS. This is the +// pair that goes red if `path_match_rule` ever guesses -- for instance by treating a subject with +// no dot as a directory. Both halves are asserted: a prefix rule applied to an exact subject would +// pass the first clause alone. +test fn the_trailing_separator_decides_the_rule() -> Bool { + let exact = path_match_rule(subject: "dag/gunbc/pr_digests.dag") + let prefix = path_match_rule(subject: "dag/gunbc/") + match exact { + ExactPath => + match prefix { + DirectoryPrefix => true + ExactPath => false + } + DirectoryPrefix => false + } +} + +// A SIBLING WHOSE NAME EXTENDS THE SUBJECT IS NOT THE SUBJECT. `dag/gunbc/pr_digests.dag` and +// `dag/gunbc/pr_digests.dag.bak` share a prefix, and an exact query answered by prefix matching +// would name a writer of a file nobody asked about. This goes red the moment `ExactPath` is +// implemented as `starts_with`. +test fn an_exact_subject_does_not_match_a_longer_path() -> Bool { + path_touches_subject(changed: "dag/gunbc/pr_digests.dag", subject: "dag/gunbc/pr_digests.dag", rule: ExactPath) + && !path_touches_subject(changed: "dag/gunbc/pr_digests.dag.bak", subject: "dag/gunbc/pr_digests.dag", rule: ExactPath) +} + +test fn a_directory_subject_matches_beneath_it_and_nothing_else() -> Bool { + path_touches_subject(changed: "dag/gunbc/instruments/ci_gates.dag", subject: "dag/gunbc/instruments/", rule: DirectoryPrefix) + && !path_touches_subject(changed: "dag/gunbc/pr_digests.dag", subject: "dag/gunbc/instruments/", rule: DirectoryPrefix) +} + +// --------------------------------------------------------------------------------------------- +// THE JOIN. + +// THE POSITIVE CONTROL. Two branches touching one file, one branch touching something else: the +// writer set is the two, and the third is observed and absent from it rather than unread. +test fn every_pull_request_touching_the_subject_is_a_writer() -> Bool { + let report = writer_set_report( + subject: subject_file, + observations: [ + read_of(number: 101, author: "alice", touched: [subject_file, "docs/notes.md"]), + read_of(number: 102, author: "bob", touched: ["src/v2/other.dag"]), + read_of(number: 103, author: "carol", touched: ["docs/notes.md", subject_file]) + ] + ) + report.writers.length() == 2 + && filter(report.writers, w => w.pull.number == 101).length() == 1 + && filter(report.writers, w => w.pull.number == 103).length() == 1 + && report_is_complete(report: report) +} + +// THE WRITER ROW CARRIES THE PATHS THAT MATCHED, and under a directory subject that list IS the +// answer. A row reduced to a boolean would pass a test that only counted writers. +test fn a_writer_row_names_the_paths_that_matched() -> Bool { + let report = writer_set_report( + subject: "dag/gunbc/instruments/", + observations: [ + read_of( + number: 201, + author: "dave", + touched: ["dag/gunbc/instruments/ci_gates.dag", "dag/gunbc/instruments/emit_host_gate.dag", "README.md"] + ) + ] + ) + report.writers.length() == 1 + && filter(report.writers, w => w.matched.length() == 2).length() == 1 +} + +// --------------------------------------------------------------------------------------------- +// EMPTY IS NOT ABSENT. + +// THE PAIR THAT MATTERS. Both arms contribute no writer; only one of them leaves the report +// complete and its "nobody" believable. A model that rendered an unread pull request as one that +// touches nothing would make these two indistinguishable, and this witness is what fails when it +// does. It asserts BOTH the completeness verdict and the exit status, because the exit status is +// what a script branches on and a completeness flag nothing consumes is a decoration. +test fn an_unread_pull_request_and_a_contentless_one_are_different_states() -> Bool { + let contentless = writer_set_report( + subject: subject_file, + observations: [PrPathsEmptyCorroborated { pull: pull(number: 301, author: "erin"), head_oid: "oid-301" }] + ) + let unread = writer_set_report( + subject: subject_file, + observations: [ + PrPathsUnobserved { + pull: pull(number: 302, author: "frank"), + cause: HeadRefStale { ref_name: "origin/x", expected_oid: "aaaa", local_oid: "bbbb" } + } + ] + ) + contentless.writers.length() == 0 + && unread.writers.length() == 0 + && report_is_complete(report: contentless) + && !report_is_complete(report: unread) + && exit_is_success(exit: writer_set_exit(report: contentless)) + && !exit_is_success(exit: writer_set_exit(report: unread)) +} + +fn exit_is_success(exit: ProcessExit) -> Bool { + match exit { + ExitSuccess => true + ExitFailure { code: _, reason: _ } => false + } +} + +// A BRANCH THAT IS AN ANCESTOR OF THE BASE IS EMPTY BY DERIVATION AND STILL COMPLETE. The third +// non-writer arm, held apart from the unread one for the same reason. +test fn a_derived_empty_branch_leaves_the_report_complete() -> Bool { + let report = writer_set_report( + subject: subject_file, + observations: [PrPathsEmptyDerived { pull: pull(number: 303, author: "grace"), head_oid: "oid-303" }] + ) + report.writers.length() == 0 && report_is_complete(report: report) +} + +// A DIFF THAT DID NOT RUN IS UNOBSERVED. This is the arm `gunbc.cross_pr_contradiction` cannot +// produce and this producer can, and it must not be quietly equivalent to a branch that touches +// nothing. +test fn a_refused_diff_is_unobserved() -> Bool { + let report = writer_set_report( + subject: subject_file, + observations: [ + PrPathsUnobserved { + pull: pull(number: 304, author: "heidi"), + cause: DiffRefused { head_oid: "oid-304", detail: "fatal: bad object" } + } + ] + ) + report_unobserved(report: report).length() == 1 && !report_is_complete(report: report) +} + +// AN EMPTY LOCAL DIFF THE FORGE CONTRADICTS IS ALSO UNOBSERVED, not a contentless branch. +test fn a_forge_disagreement_over_an_empty_diff_is_not_an_observation() -> Bool { + let report = writer_set_report( + subject: subject_file, + observations: [ + PrPathsUnobserved { + pull: pull(number: 305, author: "ivan"), + cause: DiffEmptyUnderived { head_oid: "oid-305", forge_changed_files: 7 } + } + ] + ) + !report_is_complete(report: report) +} + +// --------------------------------------------------------------------------------------------- +// WHAT THE ANSWER SAYS. + +fn lines_contain(lines: List, needle: String) -> Bool { + filter(lines, l => string_contains(l, needle)).length() > 0 +} + +// NOBODY IS SAID IN WORDS, AND ONLY WHEN IT IS TRUE. A complete report with no writers says so; an +// INCOMPLETE one with no writers must not, because that sentence would be the answer the asker is +// most likely to accept without checking. The two clauses are the discriminating pair: a renderer +// that printed the same sentence for both would pass the first alone. +test fn nobody_is_an_answer_only_over_a_complete_population() -> Bool { + let complete = writer_set_lines( + report: writer_set_report( + subject: subject_file, + observations: [PrPathsEmptyCorroborated { pull: pull(number: 401, author: "judy"), head_oid: "oid-401" }] + ) + ) + let incomplete = writer_set_lines( + report: writer_set_report( + subject: subject_file, + observations: [ + PrPathsUnobserved { + pull: pull(number: 402, author: "ken"), + cause: DiffRefused { head_oid: "oid-402", detail: "fatal: bad object" } + } + ] + ) + ) + lines_contain(lines: complete, needle: concat("no open pull request touches ", subject_file)) + && !lines_contain(lines: incomplete, needle: concat("no open pull request touches ", subject_file)) + && lines_contain(lines: incomplete, needle: "the population is incomplete") +} + +// THE ANSWER NAMES WHO, NOT JUST HOW MANY. The author and the branch are what the asker acts on; +// a row carrying only a number would pass every counting witness above. +test fn a_writer_row_names_the_author_and_the_branch() -> Bool { + let lines = writer_set_lines( + report: writer_set_report( + subject: subject_file, + observations: [read_of(number: 501, author: "mallory", touched: [subject_file])] + ) + ) + lines_contain(lines: lines, needle: "#501") + && lines_contain(lines: lines, needle: "mallory") + && lines_contain(lines: lines, needle: "session/branch-501") + && lines_contain(lines: lines, needle: concat(" touches\t", subject_file)) +} + +// EVERY UNREAD PULL REQUEST IS NAMED IN THE OUTPUT WITH ITS CAUSE. A count alone tells the asker +// the answer is incomplete without telling them which branch to go and look at. +test fn an_unread_pull_request_is_named_with_its_cause() -> Bool { + let lines = writer_set_lines( + report: writer_set_report( + subject: subject_file, + observations: [ + PrPathsUnobserved { + pull: pull(number: 601, author: "niaj"), + cause: HeadRefStale { ref_name: "origin/session/branch-601", expected_oid: "aaaa", local_oid: "bbbb" } + } + ] + ) + ) + lines_contain(lines: lines, needle: "unobserved\t#601") + && lines_contain(lines: lines, needle: "niaj") + && lines_contain(lines: lines, needle: "the local ref is stale") +} + +// THE NAIVE COUNT IS THE CORRECT COUNT, AND THIS IS THE WITNESS THAT KEEPS IT SO. +// +// The obvious way to count this report's answer is `grep -c '^writer'`. Under the first cut of the +// renderer -- summary `writers8` above rows `writer#10263...` -- that command returned +// nine for eight writers, counting the header as a datum, and it is how this instrument's own +// author first misreported its output. The repair was to rename the summary keys so the naive +// command is CORRECT rather than warned about, and this witness is the thing that fails if any +// future summary key reintroduces the prefix. It asserts the property directly -- lines beginning +// `writer` number exactly the writers, lines beginning `unobserved` number exactly the unobserved -- +// over a report that has BOTH kinds of row, which is the only shape where the collision is visible. +test fn writer_set_row_keys_do_not_collide_with_summary_keys() -> Bool { + let report = writer_set_report( + subject: subject_file, + observations: [ + read_of(number: 701, author: "olivia", touched: [subject_file]), + read_of(number: 702, author: "peggy", touched: [subject_file]), + PrPathsUnobserved { + pull: pull(number: 703, author: "quentin"), + cause: DiffRefused { head_oid: "oid-703", detail: "fatal: bad object" } + } + ] + ) + let lines = writer_set_lines(report: report) + filter(lines, l => starts_with(s: l, prefix: "writer")).length() == 2 + && filter(lines, l => starts_with(s: l, prefix: "unobserved")).length() == 1 + && report.writers.length() == 2 + && report_unobserved(report: report).length() == 1 +} + +// THE REPORT STATES ITS OWN SCOPE. A writer set taken with rename detection ON is a different +// observation, and a report that did not say which it was would be quoted as the other. +test fn the_report_states_its_rule_and_its_diff_scope() -> Bool { + let lines = writer_set_lines( + report: writer_set_report(subject: "dag/gunbc/", observations: []) + ) + lines_contain(lines: lines, needle: path_match_rule_text(rule: DirectoryPrefix)) + && lines_contain(lines: lines, needle: diff_path_scope_text(scope: writer_set_diff_scope)) + && lines_contain(lines: lines, needle: "rename detection disabled") +}