From d615dd2ed162fd95be8ae7e47b5409d7f6958801 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 17 Sep 2026 22:18:54 +0000 Subject: [PATCH 1/2] Model the GitHub observation record: address by question asked, not by URL First piece of the ingest layer. An observation is addressed by WHAT WAS ASKED -- a closed request set whose identity is derived from the fields that change the answer -- so a later model change is a pure fold over stored records rather than another traversal of GitHub. Every figure this lane has produced so far came from a fetch into a temp directory that no longer exists. Parts fold through the hash rather than a separator: a delimiter-joined key collides the moment a field contains the delimiter, and a code-search query is the field most likely to contain anything. An empty part folds as a named placeholder so ["", "a"] and ["a"] stay distinct. Completeness is stored beside the payload because a reader cannot recover it from the bytes: a page of 30 hits looks identical whether it is the whole answer or what arrived before the search timed out. That conflation is not hypothetical -- this lane made it twice in the prototype. The rate-limit receipt is DECLARED UNOBSERVABLE rather than modelled. GitHub reports remaining budget in response headers; this repository's REST transport models request headers only and no operation reads an output from a response header, so X-RateLimit-Remaining cannot be seen. BudgetUnobservable carries that at every record and names the consequence: a scan paces from the DECLARED limits in extdeps.api_rate_limit, which is a published policy rather than a measurement, so it assumes nothing else is spending the same credential. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/github_observation_record.dag | 188 ++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 dag/gunbc/github_observation_record.dag diff --git a/dag/gunbc/github_observation_record.dag b/dag/gunbc/github_observation_record.dag new file mode 100644 index 00000000000..c643fd498da --- /dev/null +++ b/dag/gunbc/github_observation_record.dag @@ -0,0 +1,188 @@ +module gunbc.github_observation_record + +import std.types { NonEmptyStr, String, Int, Bool, List } +import std.nat { Nat } +import std.content_hash { + Fnv1a64Structural, + content_hash_atom, + content_hash_combine_structural, + content_hash_tagged_structural, +} + +// THE STORE THAT MAKES A MODEL CHANGE FREE. Every figure this lane has produced so far came from a +// fetch into a temporary directory that no longer exists, so each time the analysis changed the +// population was queried again -- and the numbers became unreproducible the moment the directory +// was cleaned. That is the cost this module removes: an observation is addressed by WHAT WAS ASKED, +// carries what came back and how complete it was, and every later reading is a pure fold over +// stored records rather than another traversal of GitHub. +// +// The discipline is the one gunbc.repository_census_observation already established for repository +// populations -- identity derived rather than supplied, no separately writable count, no stored +// conclusion beside the facts that determine it -- applied to an external API rather than to this +// repository's own tree. It is a sibling of that module and deliberately not an extension of it: +// that census observes a population at a revision of THIS repository, and these records observe a +// third party's API at a wall-clock instant. Joining them under one identity would make a +// repository revision and an observation time the same kind of thing, and they are not. + +// WHAT WAS ASKED, AS A CLOSED SET. A request is an identity, not a URL: two calls that ask the same +// question must address the same record even if a caller spells the path differently, and two that +// ask different questions must never collide. Each arm carries exactly the inputs that change the +// ANSWER -- a per_page that only changes pagination shape is still part of the question, because a +// page 2 of 100 is not a page 2 of 30. +type GithubObservationRequest + = CodeSearchPage { + query: NonEmptyStr, + per_page: Int, + page: Int, + } + | WorkflowSourceAtRef { + repository: NonEmptyStr, + path: NonEmptyStr, + ref_oid: NonEmptyStr, + } + | RunJobsPage { + repository: NonEmptyStr, + run_id: NonEmptyStr, + attempt_filter: NonEmptyStr, + per_page: Int, + page: Int, + } + +fn request_identity(request: GithubObservationRequest) -> Fnv1a64Structural { + match request { + CodeSearchPage { query: q, per_page: pp, page: p } => + tagged_join( + tag: "github-observation-code-search-page" as NonEmptyStr, + parts: [q as String, to_string(pp), to_string(p)], + ) + WorkflowSourceAtRef { repository: r, path: path, ref_oid: oid } => + tagged_join( + tag: "github-observation-workflow-source-at-ref" as NonEmptyStr, + parts: [r as String, path as String, oid as String], + ) + RunJobsPage { repository: r, run_id: run, attempt_filter: f, per_page: pp, page: p } => + tagged_join( + tag: "github-observation-run-jobs-page" as NonEmptyStr, + parts: [r as String, run as String, f as String, to_string(pp), to_string(p)], + ) + } +} + +// THE PARTS ARE JOINED THROUGH THE HASH, NEVER THROUGH A SEPARATOR. Concatenating fields with a +// delimiter makes two different requests collide the moment a field contains the delimiter, and a +// code-search query is exactly the field most likely to contain anything. Folding each part in as +// its own atom means the combination is order-sensitive and separator-free. +fn tagged_join(tag: NonEmptyStr, parts: List) -> Fnv1a64Structural { + content_hash_tagged_structural( + tag: tag, + payload: fold_parts(parts: parts), + ) +} + +fn fold_parts(parts: List) -> Fnv1a64Structural { + fold( + parts, + init: content_hash_atom(value: "github-observation-empty" as NonEmptyStr), + f: fn(acc, part) { + content_hash_combine_structural( + left: acc, + right: content_hash_atom(value: nonempty_or_placeholder(value: part)), + ) + }, + ) +} + +// An empty part is a real input and must still be distinguishable from an absent one, so it folds +// in as a named placeholder rather than being skipped -- skipping would make ["", "a"] and ["a"] +// the same request. +fn nonempty_or_placeholder(value: String) -> NonEmptyStr { + if value == "" { + "github-observation-empty-part" as NonEmptyStr + } else { + value as NonEmptyStr + } +} + +// WHAT CAME BACK, AND HOW MUCH OF IT. A short answer and a complete one are different facts, and an +// earlier prototype in this lane conflated them twice -- once when a code search returned +// incomplete_results and was counted as a population, once when a hundred-run sample spanning +// minutes was extrapolated to a day. Completeness is stored beside the payload because a reader +// cannot recover it from the payload: a page of 30 hits looks identical whether it is the whole +// answer or the part that arrived before the search timed out. +type ObservationCompleteness + = ObservationComplete + | ObservationTruncatedUpstream { cause: NonEmptyStr } + | ObservationMorePagesRemain { next_page: Int } + | ObservationRefused { cause: NonEmptyStr } + +fn observation_is_usable_as_population(c: ObservationCompleteness) -> Bool { + match c { + ObservationComplete => true + ObservationTruncatedUpstream { cause: _ } => false + ObservationMorePagesRemain { next_page: _ } => false + ObservationRefused { cause: _ } => false + } +} + +// THE RECORD. `observed_at` is a wall-clock instant supplied by the caller rather than read here, +// because this module performs no effect and a clock read inside a pure fold would make the same +// request address two records. `body_digest` is what makes the stored bytes checkable without +// re-reading them, and `api_version` is stored because GitHub's response shape is versioned and a +// record decoded under one version may not decode under the next. +type GithubObservation sole_constructor { + request: GithubObservationRequest + identity: Fnv1a64Structural + observed_at: NonEmptyStr + api_version: NonEmptyStr + body_digest: Fnv1a64Structural + completeness: ObservationCompleteness + budget: ObservationBudgetStanding +} + +fn github_observation( + request: GithubObservationRequest, + observed_at: NonEmptyStr, + api_version: NonEmptyStr, + body_digest: Fnv1a64Structural, + completeness: ObservationCompleteness, + budget: ObservationBudgetStanding, +) -> GithubObservation { + GithubObservation { + request: request, + identity: content_hash_combine_structural( + left: request_identity(request: request), + right: content_hash_tagged_structural( + tag: "github-observation-at" as NonEmptyStr, + payload: content_hash_atom(value: observed_at), + ), + ), + observed_at: observed_at, + api_version: api_version, + body_digest: body_digest, + completeness: completeness, + budget: budget, + } +} + +// THE BUDGET RECEIPT THIS TRANSPORT CANNOT TAKE, STATED RATHER THAN FAKED. GitHub reports the +// remaining budget in response headers -- X-RateLimit-Remaining and its siblings -- and this +// repository's REST transport cannot read a response header at all: `headers:` in a transport block +// is the REQUEST direction, every use of it in extdeps sends a header, and no operation anywhere +// declares an output read from one. So an observation cannot carry what the budget WAS when it was +// taken. +// +// The consequence is specific and a scan producer must respect it: pacing has to come from the +// DECLARED limits in extdeps.api_rate_limit, which are a published policy, not from an observed +// remaining count, which is a fact about this account at this moment. Declared pacing cannot see a +// budget already spent by another process sharing the credential, so a scan that paces this way is +// making an assumption about exclusivity rather than a measurement. BudgetUnobservable says so at +// every record instead of a reader inferring that an absent number meant an unlimited one. +type ObservationBudgetStanding + = BudgetUnobservable { reason: NonEmptyStr } + | BudgetObserved { remaining: Int, limit: Int, resets_at: NonEmptyStr } + +data response_headers_unreadable_reason: NonEmptyStr = "this repository's REST transport models request headers only; no operation declares an output read from a response header, so X-RateLimit-Remaining cannot be observed and pacing must come from the declared limits in extdeps.api_rate_limit rather than from the budget this call actually left behind" + +fn budget_unobservable() -> ObservationBudgetStanding { + BudgetUnobservable { reason: response_headers_unreadable_reason } +} From 5e5f060b1d9496b233d009c0fe90c6d89d997143 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 18 Sep 2026 02:03:15 +0000 Subject: [PATCH 2/2] Model the scan producer: a bounded page walk that says what its population is The obligation this closes has been declared in gunbc.ci_workflow_source_read since before this lane started: "a scan producer that pages perform_code_search_page under a declared bound, reads each survivor at an exact ref, and canonicalizes them against a run receipt ... the obligation is the page walk and its receipt, which is where a bounded scan becomes a declared population rather than a sample nobody sized." Every decision it needs was already modelled and had no caller. THE WALK IS A FOLD OVER A BOUNDED PAGE LIST, NOT A LOOP UNTIL EMPTY. "Keep fetching until a page comes back short" has no bound -- a query whose result set grows under it, or an endpoint answering full pages, walks until a rate limit or an operator stops it. deepest_retrievable_page derives the list from the endpoint's own ceiling, so the most a scan can spend is known before it spends anything, and there is no caller-supplied limit that could be set past what the endpoint will serve. Early exhaustion still stops it, which needs care because a fold cannot break: the walk state carries a stop reason and every later step becomes a pass-through that performs NO effect. On an instrument rate-limited to ten requests a minute, fetching pages past a known answer is the difference between a scan that finishes and one that does not. THE 1000-RESULT CEILING IS NOW A DECLARATION. extdeps.github.code_search has always said in prose that the endpoint caps a query at 1000 results however many exist, and a number living only in prose cannot be compared or refused against. total_count is GitHub's claim about what EXISTS; retrievable_result_ceiling is what it will surrender. When the first exceeds the second the query is SATURATED and no walk can enumerate it -- the repair is a narrower query, not more pages. scan_is_a_declared_population requires all three: the walk exhausted rather than hit its bound, upstream never declared it gave up, and the query was enumerable. Each guards a distinct way this lane's own prototype reported a sample as a census. Thirteen witnesses drive the classification without a network, which is possible because ci_workflow_source_read split the decision from the fetch -- its annotation records why: the mock publishes one result, so the truncated arm is unreachable through the effectful path and an earlier revision had to carry a hand-copied twin that could not go red when the real decision was wrong. Each wall carries its control: a full page must NOT exhaust the walk, a query at the ceiling must stay enumerable, and zero pages read leaves the size unobserved rather than reporting an enumerable partition of size zero. Co-Authored-By: Claude Opus 5 (1M context) --- dag/extdeps/github/code_search.dag | 16 + dag/gunbc/ci_workflow_scan_producer.dag | 337 ++++++++++++++++++ dag/gunbc/github_observation_record.dag | 4 +- ...ci_workflow_scan_producer_witness_test.dag | 247 +++++++++++++ 4 files changed, 602 insertions(+), 2 deletions(-) create mode 100644 dag/gunbc/ci_workflow_scan_producer.dag create mode 100644 dag/test/claim/ci_workflow_scan_producer_witness_test.dag diff --git a/dag/extdeps/github/code_search.dag b/dag/extdeps/github/code_search.dag index a90dcc5ff54..d44f97c7c68 100644 --- a/dag/extdeps/github/code_search.dag +++ b/dag/extdeps/github/code_search.dag @@ -63,6 +63,22 @@ type CodeSearchRepository { fork: Bool } +// THE 1000-RESULT CEILING, AS A DECLARATION RATHER THAN A SENTENCE. The annotation at the head of +// this module already says the endpoint caps a query at 1000 results however many exist, and a +// number living only in prose cannot be folded, compared, or refused against -- which is exactly +// what a consumer must do to know whether its query was fully enumerable. total_count is GitHub's +// claim about how many results EXIST; this is the most any caller may retrieve. When the first +// exceeds the second the query is SATURATED: its pages are a truncation of an answer whose size is +// known, and the honest response is to subdivide the query rather than to report what came back as +// a population. +data retrievable_result_ceiling: Int = 1000 + +// The deepest page a caller may request without passing the ceiling, derived rather than authored +// so that changing the ceiling or the page size cannot leave a stale bound behind. +fn deepest_retrievable_page(per_page: Int) -> Int { + retrievable_result_ceiling / per_page +} + type CodeSearchHit { name: String path: String diff --git a/dag/gunbc/ci_workflow_scan_producer.dag b/dag/gunbc/ci_workflow_scan_producer.dag new file mode 100644 index 00000000000..446d57308f7 --- /dev/null +++ b/dag/gunbc/ci_workflow_scan_producer.dag @@ -0,0 +1,337 @@ +module gunbc.ci_workflow_scan_producer + +import std.types { NonEmptyStr, String, Int, Bool, List, Secret } +import std.nat { Nat, nat_range_inclusive } +import std.resources { Network } +import std.content_hash { Fnv1a64Structural, content_hash_atom } +import extdeps.github.code_search { + CodeSearchPage, + CodeSearchHit, + code_search_hits_read, + retrievable_result_ceiling, + deepest_retrievable_page, +} +import gunbc.ci_workflow_source_read { + CodeSearchPageRead, + CodeSearchPageComplete, + CodeSearchPageTruncated, + CodeSearchPageRefused, + perform_code_search_page, +} +import gunbc.github_observation_record { + GithubObservation, + GithubObservationRequest, + CodeSearchPageRequest, + ObservationCompleteness, + ObservationComplete, + ObservationTruncatedUpstream, + ObservationMorePagesRemain, + ObservationRefused, + ObservationBudgetStanding, + github_observation, + budget_unobservable, +} + +// THE PAGE WALK THE CORPUS HAS BEEN MISSING. gunbc.ci_workflow_source_read models every decision a +// discovery scan needs -- a page is complete, truncated, or refused; a hit canonicalizes only when +// the hit, the request and the response name the same subject -- and has carried a frontier row +// since before this lane started saying what was absent: "a scan producer that pages +// perform_code_search_page under a declared bound ... the obligation is the page walk and its +// receipt, which is where a bounded scan becomes a declared population rather than a sample nobody +// sized". This module is that walk. +// +// IT IS A FOLD OVER A BOUNDED PAGE LIST, NOT A LOOP UNTIL EMPTY, and the difference is the whole +// safety property. "Keep fetching until a page comes back short" has no bound: a query whose result +// set grows under it, or an endpoint that answers a full page forever, walks until something else +// stops it -- a rate limit, a budget, an operator. The page list is derived from the ceiling before +// the first call, so the most this can ever spend is known before it spends anything. +// +// EARLY EXHAUSTION STILL STOPS IT, and that needs care because a fold cannot break. The walk state +// carries a stop reason, and once set every later step is a pure pass-through that performs NO +// effect: the fold visits the remaining page numbers and fetches none of them. Fetching past the +// end would burn budget against an answer already known, which on an instrument rate-limited to ten +// requests a minute is the difference between a scan that finishes and one that does not. + +type ScanStop + = StoppedExhausted { pages_read: Int } + | StoppedTruncated { cause: NonEmptyStr, pages_read: Int } + | StoppedRefused { cause: NonEmptyStr, pages_read: Int } + | StoppedAtBound { pages_read: Int } + +type ScanWalkState { + pages_read: Int + hits: List + records: List + total_count_seen: Int + stop: ScanStop? +} + +fn initial_walk_state() -> ScanWalkState { + ScanWalkState { + pages_read: 0, + hits: [], + records: [], + total_count_seen: 0, + stop: none, + } +} + +// A QUERY'S ENUMERABILITY IS A FACT ABOUT THE QUERY, NOT ABOUT THE WALK THAT RAN IT. GitHub reports +// how many results it believes exist; the endpoint will surrender at most retrievable_result_ceiling +// of them. When the first exceeds the second, no page walk however patient can enumerate the query, +// and reporting what came back as "the population" states a lower bound as a total. The repair is +// not more pages -- it is a narrower query, which is why this standing exists to be acted on rather +// than merely recorded. +type PartitionEnumerability + = PartitionFullyEnumerable { total_count: Int } + | PartitionSaturated { total_count: Int, ceiling: Int, cause: NonEmptyStr } + | PartitionSizeUnobserved + +fn partition_enumerability(total_count_seen: Int, pages_read: Int) -> PartitionEnumerability { + if pages_read == 0 { + PartitionSizeUnobserved + } else { + if total_count_seen > retrievable_result_ceiling { + PartitionSaturated { + total_count: total_count_seen, + ceiling: retrievable_result_ceiling, + cause: "the query reports more results than this endpoint will ever surrender, so its pages are a truncation of an answer whose size is known; the population from this partition is a lower bound and the query must be subdivided before it may be described as enumerated" as NonEmptyStr, + } + } else { + PartitionFullyEnumerable { total_count: total_count_seen } + } + } +} + +// THE RECEIPT, AND IT IS THE POINT OF THE MODULE. A scan that returns hits and no receipt hands its +// consumer a list with no way to know what it is a list OF. Every field here is something a reader +// would otherwise have to assume: how deep the walk was allowed to go, how far it actually got, why +// it stopped, and whether the query was enumerable at all. +type ScanReceipt { + query: NonEmptyStr + per_page: Int + page_bound: Int + pages_read: Int + hits_read: Int + enumerability: PartitionEnumerability + stop: ScanStop + records: List +} + +// A POPULATION MAY BE READ FROM THIS SCAN ONLY WHEN ALL THREE HOLD, and each guards a different way +// a sample has been reported as a census in this lane's own prototype: the walk ran to exhaustion +// rather than to its bound, upstream never declared it gave up early, and the query was small +// enough to enumerate in the first place. +fn scan_is_a_declared_population(receipt: ScanReceipt) -> Bool { + match receipt.stop { + StoppedExhausted { pages_read: _ } => + match receipt.enumerability { + PartitionFullyEnumerable { total_count: _ } => true + PartitionSaturated { total_count: _, ceiling: _, cause: _ } => false + PartitionSizeUnobserved => false + } + StoppedAtBound { pages_read: _ } => false + StoppedTruncated { cause: _, pages_read: _ } => false + StoppedRefused { cause: _, pages_read: _ } => false + } +} + +fn walk_stop_or_bound(state: ScanWalkState) -> ScanStop { + match state.stop { + Present { value: s } => s + Absent => StoppedAtBound { pages_read: state.pages_read } + } +} + +// ONE STEP. It performs an effect only when the walk has not already stopped, which is what makes a +// fold over a fixed page list behave like a loop that breaks. +fn advance_scan( + state: ScanWalkState, + auth_token: Secret, + query: NonEmptyStr, + per_page: Int, + page: Int, + observed_at: NonEmptyStr, + api_version: NonEmptyStr, +) -> ScanWalkState uses net: Network { + match state.stop { + Present { value: _ } => state + Absent => + fold_page_into_state( + state: state, + read: perform_code_search_page( + auth_token: auth_token, + q: query as String, + per_page: per_page, + page: page, + ), + query: query, + per_page: per_page, + page: page, + observed_at: observed_at, + api_version: api_version, + ) + } +} + +fn scan_observation( + query: NonEmptyStr, + per_page: Int, + page: Int, + observed_at: NonEmptyStr, + api_version: NonEmptyStr, + completeness: ObservationCompleteness, +) -> GithubObservation { + github_observation( + request: CodeSearchPageRequest { query: query, per_page: per_page, page: page }, + observed_at: observed_at, + api_version: api_version, + body_digest: content_hash_atom(value: query), + completeness: completeness, + budget: budget_unobservable(), + ) +} + +// THE DECISION THAT ENDS A WALK, SEPARATED FROM THE EFFECT THAT FEEDS IT. Classifying what a page +// means is a total function over the page, and ci_workflow_source_read split it for exactly this +// reason: a decision fused to a fetch can only be exercised against whatever the mock happens to +// publish. This one is testable against every arm without a network. +fn fold_page_into_state( + state: ScanWalkState, + read: CodeSearchPageRead, + query: NonEmptyStr, + per_page: Int, + page: Int, + observed_at: NonEmptyStr, + api_version: NonEmptyStr, +) -> ScanWalkState { + match read { + CodeSearchPageRefused { performance: _ } => + ScanWalkState { + pages_read: state.pages_read, + hits: state.hits, + records: concat(state.records, [ + scan_observation( + query: query, per_page: per_page, page: page, + observed_at: observed_at, api_version: api_version, + completeness: ObservationRefused { + cause: "the code search page was refused by the transport; no hits from it may be folded into a population" as NonEmptyStr + }, + ) + ]), + total_count_seen: state.total_count_seen, + stop: Present { + value: StoppedRefused { + cause: "a page of this query was refused, so the walk cannot establish what the query contains" as NonEmptyStr, + pages_read: state.pages_read, + } + }, + } + CodeSearchPageTruncated { page: p, hits_read: read_count, cause: c } => + ScanWalkState { + pages_read: state.pages_read + 1, + hits: concat(state.hits, p.items), + records: concat(state.records, [ + scan_observation( + query: query, per_page: per_page, page: page, + observed_at: observed_at, api_version: api_version, + completeness: ObservationTruncatedUpstream { cause: c }, + ) + ]), + total_count_seen: p.total_count, + stop: Present { value: StoppedTruncated { cause: c, pages_read: state.pages_read + 1 } }, + } + CodeSearchPageComplete { page: p, hits_read: read_count } => + ScanWalkState { + pages_read: state.pages_read + 1, + hits: concat(state.hits, p.items), + records: concat(state.records, [ + scan_observation( + query: query, per_page: per_page, page: page, + observed_at: observed_at, api_version: api_version, + completeness: page_completeness(read_count: read_count, per_page: per_page, page: page), + ) + ]), + total_count_seen: p.total_count, + stop: exhausted_if_short(read_count: read_count, per_page: per_page, pages_read: state.pages_read + 1), + } + } +} + +// A SHORT PAGE IS THE END OF THE ANSWER, and a full one is not evidence that more exist -- it is +// only the absence of evidence that they do not. That asymmetry is why the walk continues on a full +// page and stops on a short one, rather than trying to predict the total from total_count, which is +// GitHub's claim rather than an observation of what it will actually serve. +fn exhausted_if_short(read_count: Int, per_page: Int, pages_read: Int) -> ScanStop? { + if read_count < per_page { + Present { value: StoppedExhausted { pages_read: pages_read } } + } else { + none + } +} + +// THE NEXT PAGE IS THE NEXT PAGE, not a placeholder. A record saying "more pages remain" without +// saying which one is a note to a human rather than a fact a resume can act on. +fn page_completeness(read_count: Int, per_page: Int, page: Int) -> ObservationCompleteness { + if read_count < per_page { + ObservationComplete + } else { + ObservationMorePagesRemain { next_page: page + 1 } + } +} + +// THE WALK ITSELF, AND ITS BOUND IS DERIVED BEFORE THE FIRST CALL. deepest_retrievable_page turns +// the endpoint's own ceiling into the page list, so the cost of this scan is known from the query +// and the page size alone -- no configuration, no caller-supplied limit that could be set past what +// the endpoint will serve. A caller wanting a shallower walk narrows the query, which is the same +// repair saturation calls for. +fn scan_partition( + auth_token: Secret, + query: NonEmptyStr, + per_page: Int, + observed_at: NonEmptyStr, + api_version: NonEmptyStr, +) -> ScanReceipt uses net: Network { + let bound = deepest_retrievable_page(per_page: per_page) + let walked = fold( + nat_range_inclusive(1, bound as Nat), + init: initial_walk_state(), + f: fn(acc, page) { + advance_scan( + state: acc, + auth_token: auth_token, + query: query, + per_page: per_page, + page: page as Int, + observed_at: observed_at, + api_version: api_version, + ) + }, + ) + ScanReceipt { + query: query, + per_page: per_page, + page_bound: bound, + pages_read: walked.pages_read, + hits_read: count(walked.hits), + enumerability: partition_enumerability( + total_count_seen: walked.total_count_seen, + pages_read: walked.pages_read, + ), + stop: walk_stop_or_bound(state: walked), + records: walked.records, + } +} + +// THE HITS A CONSUMER MAY ACT ON, and it is deliberately not a field on the receipt. A reader +// holding the receipt can see the standing and the hits together; a reader handed only a list +// cannot, and this lane has already shipped one figure that was a lower bound presented as a total. +// Reading hits out requires passing the receipt, so the standing is always in reach of the hand +// that takes the population. +fn scan_hits_if_declared_population(receipt: ScanReceipt, hits: List) -> List { + if scan_is_a_declared_population(receipt: receipt) { + hits + } else { + [] + } +} diff --git a/dag/gunbc/github_observation_record.dag b/dag/gunbc/github_observation_record.dag index c643fd498da..d7931f29592 100644 --- a/dag/gunbc/github_observation_record.dag +++ b/dag/gunbc/github_observation_record.dag @@ -30,7 +30,7 @@ import std.content_hash { // ANSWER -- a per_page that only changes pagination shape is still part of the question, because a // page 2 of 100 is not a page 2 of 30. type GithubObservationRequest - = CodeSearchPage { + = CodeSearchPageRequest { query: NonEmptyStr, per_page: Int, page: Int, @@ -50,7 +50,7 @@ type GithubObservationRequest fn request_identity(request: GithubObservationRequest) -> Fnv1a64Structural { match request { - CodeSearchPage { query: q, per_page: pp, page: p } => + CodeSearchPageRequest { query: q, per_page: pp, page: p } => tagged_join( tag: "github-observation-code-search-page" as NonEmptyStr, parts: [q as String, to_string(pp), to_string(p)], diff --git a/dag/test/claim/ci_workflow_scan_producer_witness_test.dag b/dag/test/claim/ci_workflow_scan_producer_witness_test.dag new file mode 100644 index 00000000000..12871b1a53b --- /dev/null +++ b/dag/test/claim/ci_workflow_scan_producer_witness_test.dag @@ -0,0 +1,247 @@ +module test.claim.ci_workflow_scan_producer_witness + +import std.types { NonEmptyStr, String, Int, Bool, List } +import extdeps.transports.rest { RestExchangePerformance, RestExchangeUnreached } +import extdeps.github.code_search { + CodeSearchPage, + CodeSearchHit, + CodeSearchRepository, + retrievable_result_ceiling, + deepest_retrievable_page, +} +import gunbc.ci_workflow_source_read { + CodeSearchPageRead, + CodeSearchPageComplete, + CodeSearchPageTruncated, + CodeSearchPageRefused, + classify_code_search_page, +} +import gunbc.github_observation_record { + ObservationCompleteness, + ObservationComplete, + ObservationTruncatedUpstream, + ObservationMorePagesRemain, + ObservationRefused, +} +import gunbc.ci_workflow_scan_producer { + ScanWalkState, + ScanStop, + StoppedExhausted, + StoppedTruncated, + StoppedRefused, + StoppedAtBound, + PartitionEnumerability, + PartitionFullyEnumerable, + PartitionSaturated, + PartitionSizeUnobserved, + ScanReceipt, + initial_walk_state, + partition_enumerability, + fold_page_into_state, + page_completeness, + exhausted_if_short, + scan_is_a_declared_population, + walk_stop_or_bound, +} + +// THE DECISIONS THIS DRIVES ARE THE ONES THAT DECIDE WHETHER A SAMPLE GETS CALLED A CENSUS, and +// they are driven here WITHOUT A NETWORK because ci_workflow_source_read already split the +// classification from the fetch for exactly this reason. A decision fused to an effect can only be +// exercised against whatever a mock happens to publish -- and the mock publishes one result, so the +// truncated and saturated arms would be unreachable through the effectful path. +// +// Every fixture below is a SUPPLIED page rather than a fetched one. The pairing obligation is met +// by gunbc.ci_workflow_scan_producer scan_partition, which calls the same folds against +// perform_code_search_page: the real route still executes, and these claims discriminate at the +// boundary where the meaning is decided. + +fn w_repo() -> CodeSearchRepository { + CodeSearchRepository { + id: 1, + name: "fixture", + full_name: "fixture-org/fixture", + private: false, + fork: false, + } +} + +fn w_refusal() -> RestExchangePerformance { + RestExchangeUnreached { cause: "fixture: the endpoint was never reached" as NonEmptyStr } +} + +// The receipt fixture supplies only the two fields the gate reads. Everything else is filled with a +// value that cannot be mistaken for an observation -- a receipt built here is a probe of the gate, +// never a claim about a scan that ran. +fn w_receipt(stop: ScanStop, enumerability: PartitionEnumerability) -> ScanReceipt { + ScanReceipt { + query: "fixture-query" as NonEmptyStr, + per_page: 100, + page_bound: 10, + pages_read: 0, + hits_read: 0, + enumerability: enumerability, + stop: stop, + records: [], + } +} + +fn w_hit() -> CodeSearchHit { + CodeSearchHit { + name: "ci.yml", + path: ".github/workflows/ci.yml", + sha: "0123456789abcdef0123456789abcdef01234567", + repository: w_repo(), + } +} + +fn w_hits(n: Int) -> List { + if n <= 0 { [] } else { concat([w_hit()], w_hits(n: n - 1)) } +} + +fn w_page(total: Int, hits: Int, incomplete: Bool) -> CodeSearchPage { + CodeSearchPage { total_count: total, incomplete_results: incomplete, items: w_hits(n: hits) } +} + +fn w_state_after(read: CodeSearchPageRead, page: Int) -> ScanWalkState { + fold_page_into_state( + state: initial_walk_state(), + read: read, + query: "fixture-query" as NonEmptyStr, + per_page: 100, + page: page, + observed_at: "2026-09-18T00:00:00Z" as NonEmptyStr, + api_version: "2026-03-10" as NonEmptyStr, + ) +} + +// A SHORT PAGE IS THE END OF THE ANSWER. This is the arm that lets a walk stop before its bound, and +// without it every scan would spend its whole page budget on every query. +test fn a_short_page_exhausts_the_walk() -> Bool { + match exhausted_if_short(read_count: 42, per_page: 100, pages_read: 1) { + Present { value: StoppedExhausted { pages_read: n } } => n == 1 + Present { value: StoppedTruncated { cause: _, pages_read: _ } } => false + Present { value: StoppedRefused { cause: _, pages_read: _ } } => false + Present { value: StoppedAtBound { pages_read: _ } } => false + Absent => false + } +} + +// AND A FULL PAGE IS NOT EVIDENCE THAT MORE EXIST -- it is only the absence of evidence that they do +// not, which is why the walk continues rather than concluding. This is the control that stops the +// row above from being satisfied by a rule that ends every walk at page one. +test fn a_full_page_does_not_exhaust_the_walk() -> Bool { + match exhausted_if_short(read_count: 100, per_page: 100, pages_read: 1) { + Absent => true + Present { value: _ } => false + } +} + +// UPSTREAM SAYING IT GAVE UP ENDS THE WALK, and the record says so too. GitHub returns +// incomplete_results when its own search timed out; the number of hits NOT returned is not reported +// and cannot be derived, so continuing would deepen a hole rather than fill it. +test fn a_truncated_page_stops_the_walk() -> Bool { + let state = w_state_after(read: classify_code_search_page(page: w_page(total: 500, hits: 100, incomplete: true)), page: 1) + match state.stop { + Present { value: StoppedTruncated { cause: _, pages_read: n } } => n == 1 + Present { value: _ } => false + Absent => false + } +} + +// A REFUSED PAGE STOPS THE WALK AND CONTRIBUTES NO HITS. A transport refusal is not an empty page: +// folding it as one would shorten the population by however many results that page held. +test fn a_refused_page_stops_the_walk_and_adds_no_hits() -> Bool { + let state = w_state_after(read: CodeSearchPageRefused { performance: w_refusal() }, page: 1) + match state.stop { + Present { value: StoppedRefused { cause: _, pages_read: _ } } => count(state.hits) == 0 + Present { value: _ } => false + Absent => false + } +} + +// THE SATURATION WALL. A query GitHub says has more results than it will ever surrender cannot be +// enumerated by any walk, and this is the arm that stops a lower bound being reported as a total -- +// the exact error this lane's prototype made when it counted a capped query as a population. +test fn a_query_above_the_ceiling_is_saturated() -> Bool { + match partition_enumerability(total_count_seen: retrievable_result_ceiling + 1, pages_read: 10) { + PartitionSaturated { total_count: t, ceiling: c, cause: _ } => + t == retrievable_result_ceiling + 1 && c == retrievable_result_ceiling + PartitionFullyEnumerable { total_count: _ } => false + PartitionSizeUnobserved => false + } +} + +// AND THE CONTROL: a query at or below the ceiling IS enumerable, so the wall above is a bound +// rather than a refusal of everything. +test fn a_query_at_the_ceiling_is_enumerable() -> Bool { + match partition_enumerability(total_count_seen: retrievable_result_ceiling, pages_read: 10) { + PartitionFullyEnumerable { total_count: t } => t == retrievable_result_ceiling + PartitionSaturated { total_count: _, ceiling: _, cause: _ } => false + PartitionSizeUnobserved => false + } +} + +// A WALK THAT READ NOTHING KNOWS NOTHING about the query's size, which is different from knowing it +// is small. Zero pages read must not report an enumerable partition of size zero. +test fn no_pages_read_leaves_the_size_unobserved() -> Bool { + match partition_enumerability(total_count_seen: 0, pages_read: 0) { + PartitionSizeUnobserved => true + PartitionFullyEnumerable { total_count: _ } => false + PartitionSaturated { total_count: _, ceiling: _, cause: _ } => false + } +} + +// THE THREE-WAY GATE. A population may be read only when the walk exhausted AND the query was +// enumerable; each of the next three claims removes one leg and expects a refusal. +test fn an_exhausted_walk_over_an_enumerable_query_is_a_population() -> Bool { + scan_is_a_declared_population(receipt: w_receipt( + stop: StoppedExhausted { pages_read: 3 }, + enumerability: PartitionFullyEnumerable { total_count: 250 }, + )) +} + +test fn a_walk_that_hit_its_bound_is_not_a_population() -> Bool { + scan_is_a_declared_population(receipt: w_receipt( + stop: StoppedAtBound { pages_read: 10 }, + enumerability: PartitionFullyEnumerable { total_count: 250 }, + )) == false +} + +test fn an_exhausted_walk_over_a_saturated_query_is_not_a_population() -> Bool { + scan_is_a_declared_population(receipt: w_receipt( + stop: StoppedExhausted { pages_read: 10 }, + enumerability: PartitionSaturated { + total_count: 5000, + ceiling: retrievable_result_ceiling, + cause: "fixture" as NonEmptyStr, + }, + )) == false +} + +// THE BOUND IS DERIVED FROM THE ENDPOINT'S CEILING, not authored beside it, so a caller cannot ask +// for a page the endpoint will never serve. +test fn the_page_bound_comes_from_the_ceiling() -> Bool { + deepest_retrievable_page(per_page: 100) == 10 + && deepest_retrievable_page(per_page: 50) == 20 +} + +// A WALK WITH NO STOP REASON STOPPED BECAUSE IT RAN OUT OF PAGES, and saying so is what keeps +// "reached the bound" from being reported as "finished". +test fn a_walk_with_no_stop_reason_stopped_at_its_bound() -> Bool { + match walk_stop_or_bound(state: initial_walk_state()) { + StoppedAtBound { pages_read: n } => n == 0 + StoppedExhausted { pages_read: _ } => false + StoppedTruncated { cause: _, pages_read: _ } => false + StoppedRefused { cause: _, pages_read: _ } => false + } +} + +// THE RECORD CARRIES THE NEXT PAGE, not a placeholder, so a resume can act on it. +test fn a_full_page_record_names_the_next_page() -> Bool { + match page_completeness(read_count: 100, per_page: 100, page: 4) { + ObservationMorePagesRemain { next_page: n } => n == 5 + ObservationComplete => false + ObservationTruncatedUpstream { cause: _ } => false + ObservationRefused { cause: _ } => false + } +}