From d2b70b7e151a97895dbd83bd97f02ac259881a09 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 3 Sep 2026 18:13:33 +0000 Subject: [PATCH 1/2] The writer set for a contended authority: given a path, print who is open-PR writing it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This repository's authorities are single by construction (DESIGN §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, in full, every time. 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= A subject ending in `/` asks about a subtree; anything else names one file, and the report prints which rule it used. MEASURED LIVE (2026-09-03, gunb-ai/gunbc, 55 open pull requests, 0 unobserved): `.github/workflows/witnesses.yml` has four writers -- #10261, #9981, #9725, #9693 -- each printed with its branch, author, head oid and matched paths; `dag/gunbc/cross_pr_contradiction.dag` has none, and says so in words. WHY IT IS NOT A WIDENING OF `gunbc.cross_pr_contradiction`. That instrument reads the same population to ask whether two branches move one roster IDENTITY in opposite directions, and states in its own header that a same-direction overlap index is out of scope for it: 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. RENAME DETECTION IS OFF, AND THAT IS THE ONE NEW EXTDEPS OPERATION. `diff.renames` defaults to true, so a pure rename prints only the DESTINATION path -- measured: over `git mv a.txt b.txt`, `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, so `extdeps.git.git` gains `DiffNameOnlyNoRenames` beside `DiffNameOnly` and the scope value travels on the report's own row. EMPTY IS NOT ABSENT (DESIGN §5). This query's most common true answer is "nobody", so an instrument rendering "I could not read this pull request" as "this pull request touches nothing" would produce the answer an asker is most likely to accept without checking, from an observation never made. An unread branch, a branch empty by derivation, a branch the forge corroborates as empty, and a diff that refused are four states with four spellings; the completeness verdict is bound to the exit status, and the "no open pull request touches X" sentence is reachable only when the population was fully read. `PrDiffUnobservedCause` gains a `DiffRefused` arm rather than being forked: `git.Core.Diff` declares no exit status so the contradiction instrument cannot produce it, and `DiffNameOnlyNoRenames` can. One vocabulary, one set of consequences. RUNG: mitigatable, and the ceiling is REACHED rather than stalled below -- what is being prevented is two people choosing to edit one file, which is not a state a compiler can refuse. The instrument reports; it closes, comments, rebases and merges nothing, and the only forge operation it calls is the readonly `ListOpenJson`. EVIDENCE. 13 witnesses in dag/test/claim/path_writer_set_witness_test.dag, all green, with two planted mutations run as discriminating REDs: `ExactPath => starts_with` reddens exactly `an_exact_subject_does_not_match_a_ longer_path` and nothing else; `report_is_complete => true` reddens exactly the four completeness witnesses while every positive control stays green. The 27 `cross_pr_contradiction` witnesses stay green over the added arm. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AinEdiYkU1u4HYnS6DUP78 --- dag/extdeps/git/git.dag | 26 ++ dag/extdeps/github/pulls.dag | 2 +- dag/gunbc/cross_pr_contradiction.dag | 18 + .../path_writer_set_instrument.dag | 341 ++++++++++++++++ dag/gunbc/path_writer_set.dag | 382 ++++++++++++++++++ .../claim/path_writer_set_witness_test.dag | 278 +++++++++++++ 6 files changed, 1046 insertions(+), 1 deletion(-) create mode 100644 dag/gunbc/instruments/path_writer_set_instrument.dag create mode 100644 dag/gunbc/path_writer_set.dag create mode 100644 dag/test/claim/path_writer_set_witness_test.dag 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..f3460f50cec --- /dev/null +++ b/dag/gunbc/path_writer_set.dag @@ -0,0 +1,382 @@ +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, "`") + ) + ] + } + } +} + +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("pull_requests\t", to_string(report.observations.length())), + concat("unobserved\t", to_string(report_unobserved(report: report).length())), + concat("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..804a4b25553 --- /dev/null +++ b/dag/test/claim/path_writer_set_witness_test.dag @@ -0,0 +1,278 @@ +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 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") +} From 804dfa0f4aeaf0c923428ee10841e114b616a9b9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 3 Sep 2026 18:37:17 +0000 Subject: [PATCH 2/2] Make the summary row unmiscountable: total_writers / total_unobserved, and the witness that keeps it so THE DEFECT WAS IN THE OUTPUT FORMAT, NOT ONLY IN THE READER. The obvious way to count this report's answer is `grep -c '^writer'`. The summary read `writers8` above rows spelled `writer#10263...`, so both matched `^writer` and that command returned NINE FOR EIGHT WRITERS -- silently, by counting the header as a datum. `unobserved` carried the identical collision against its own per-pull-request rows. It is not hypothetical. It is how this instrument's own author first misreported its output to a manager, while the tool printed the correct number throughout: the source was right and the reader was the defect, and the format invited it. A header note 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 become `total_pull_requests` / `total_unobserved` / `total_writers`, chosen until THE NAIVE COMMAND IS CORRECT rather than merely warned about: `grep -c '^writer'` and `grep -c '^unobserved'` now yield exactly the row counts they look like they yield. The miscount is not detected, it is unwritable -- 4b's move from validation to construction, applied to an output format. EVIDENCE. `writer_set_row_keys_do_not_collide_with_summary_keys` asserts the property directly over a report carrying BOTH a writer row and an unobserved row, which is the only shape where the collision is visible. Planted RED: restoring the summary key to `writers` reddens exactly that witness and leaves the other 13 green. 14 witnesses green on the repair. Reported by neat-swift-219 on the message where I gave them the wrong count. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AinEdiYkU1u4HYnS6DUP78 --- dag/gunbc/path_writer_set.dag | 24 +++++++++++++-- .../claim/path_writer_set_witness_test.dag | 29 +++++++++++++++++++ 2 files changed, 50 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/path_writer_set.dag b/dag/gunbc/path_writer_set.dag index f3460f50cec..330c96be0b6 100644 --- a/dag/gunbc/path_writer_set.dag +++ b/dag/gunbc/path_writer_set.dag @@ -297,6 +297,24 @@ fn writer_summary_lines(report: WriterSetReport) -> List { } } +// 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( @@ -304,9 +322,9 @@ fn writer_set_lines(report: WriterSetReport) -> List { 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("pull_requests\t", to_string(report.observations.length())), - concat("unobserved\t", to_string(report_unobserved(report: report).length())), - concat("writers\t", to_string(report.writers.length())) + 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) ), diff --git a/dag/test/claim/path_writer_set_witness_test.dag b/dag/test/claim/path_writer_set_witness_test.dag index 804a4b25553..627a9ab6751 100644 --- a/dag/test/claim/path_writer_set_witness_test.dag +++ b/dag/test/claim/path_writer_set_witness_test.dag @@ -266,6 +266,35 @@ test fn an_unread_pull_request_is_named_with_its_cause() -> Bool { && 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 {