Three scan-producer defects that #11564 merged without

dag/extdeps/github/code_search.dag

@@ -73,10 +73,44 @@ type CodeSearchRepository {
 // a population.
 data retrievable_result_ceiling: Int = 1000
 
+// A PAGE SIZE IS ADMITTED BEFORE IT IS DIVIDED BY, AND AN EARLIER CUT DIVIDED BY WHATEVER ARRIVED.
+// deepest_retrievable_page took a bare Int and computed retrievable_result_ceiling / per_page, so a
+// caller supplying a size outside the endpoint's domain got a bound that looked derived and was
+// nonsense: per_page = 1000 yields a bound of ONE PAGE, and a walk that reads one page and finds it
+// short reports StoppedExhausted -- a partial first page presented as a complete population. GitHub
+// serves at most max_per_page results per page for this endpoint, and nothing refused above it.
+//
+// The domain is upstream's, so the admission lives here rather than in a consumer: this is the
+// endpoint's documented contract, not a policy any caller may choose. The admitted carrier is
+// sole_constructor, so it can be built only by the admission below -- an unadmitted Int cannot reach
+// the division at all, which is the difference between refusing a bad bound and being unable to
+// compute one.
+type CodeSearchPageSize sole_constructor { size: Int }
+
+type CodeSearchPageSizeAdmission
+  = CodeSearchPageSizeAdmitted { page_size: CodeSearchPageSize }
+  | CodeSearchPageSizeRefused { observed: Int, cause: NonEmptyStr }
+
+fn admit_code_search_page_size(observed: Int) -> CodeSearchPageSizeAdmission {
+  if observed < 1 {
+    CodeSearchPageSizeRefused {
+      observed: observed,
+      cause: "a page size below one asks the endpoint for no results per page, and dividing the retrievable ceiling by it yields no usable bound" as NonEmptyStr,
+    }
+  } else if observed > max_per_page {
+    CodeSearchPageSizeRefused {
+      observed: observed,
+      cause: join(["code search serves at most ", to_string(max_per_page), " results per page, so a larger size is silently truncated upstream and the walk bound derived from it understates the pages that exist"], "") as NonEmptyStr,
+    }
+  } else {
+    CodeSearchPageSizeAdmitted { page_size: CodeSearchPageSize { size: observed } }
+  }
+}
+
 // 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
+fn deepest_retrievable_page(page_size: CodeSearchPageSize) -> Int {
+  retrievable_result_ceiling / page_size.size
 }
 
 type CodeSearchHit {

dag/gunbc/ci_workflow_scan_producer.dag

@@ -3,8 +3,8 @@ 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 {
+  CodeSearchPageSize,
   CodeSearchPage,
   CodeSearchHit,
   code_search_hits_read,
@@ -22,6 +22,7 @@ import gunbc.github_observation_record {
   GithubObservation,
   GithubObservationRequest,
   CodeSearchPageRequest,
+  digest_unobservable,
   ObservationCompleteness,
   ObservationComplete,
   ObservationTruncatedUpstream,
@@ -186,7 +187,7 @@ fn scan_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),
+    body_digest: digest_unobservable(),
     completeness: completeness,
     budget: budget_unobservable(),
   )
@@ -283,16 +284,22 @@ fn page_completeness(read_count: Int, per_page: Int, page: Int) -> ObservationCo
 // 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
+// the endpoint will serve. THE PAGE SIZE ARRIVES ADMITTED rather than as a bare Int: an earlier cut
+// took one and divided the retrievable ceiling by it, so a caller passing 1000 got a bound of ONE
+// PAGE and a short first page then reported StoppedExhausted -- a partial page presented as a
+// complete population, which is the same shape as every other defect this module is about. The
+// admission is extdeps.github.code_search admit_code_search_page_size, because the 1..max_per_page
+// domain is the endpoint's contract rather than this lane's policy. 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,
+  page_size: CodeSearchPageSize,
   observed_at: NonEmptyStr,
   api_version: NonEmptyStr,
-) -> ScanReceipt uses net: Network {
-  let bound = deepest_retrievable_page(per_page: per_page)
+) -> ScanOutcome uses net: Network {
+  let per_page = page_size.size
+  let bound = deepest_retrievable_page(page_size: page_size)
   let walked = fold(
     nat_range_inclusive(1, bound as Nat),
     init: initial_walk_state(),
@@ -308,7 +315,7 @@ fn scan_partition(
       )
     },
   )
-  ScanReceipt {
+  let receipt = ScanReceipt {
     query: query,
     per_page: per_page,
     page_bound: bound,
@@ -321,17 +328,48 @@ fn scan_partition(
     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<CodeSearchHit>) -> List<CodeSearchHit> {
   if scan_is_a_declared_population(receipt: receipt) {
-    hits
+    ScanOutcome { receipt: receipt, disposition: ScanDeclaredPopulation { hits: walked.hits } }
   } else {
-    []
+    ScanOutcome { receipt: receipt, disposition: ScanNotAPopulation }
   }
 }
+
+// THE HITS AND THE STANDING ARE BOUND, NOT MERELY COLOCATED, AND THE DIFFERENCE IS THE WHOLE POINT.
+// Two revisions got this wrong in opposite directions. The first kept the hits off the receipt and
+// offered a gate taking (receipt, hits) -- but scan_partition dropped walked.hits, so no caller
+// could obtain the list and the gate was uninvokable. The second added this coproduct and an
+// EXPORTED MINT over two independently supplied values, which fixes the honest production call and
+// leaves the dishonest one writable: a caller could still pair a green receipt for population A
+// with hits from population B and get ScanDeclaredPopulation, because ScanReceipt is freely
+// constructible and nothing bound the two arguments to one walk.
+//
+// SO THE POSITIVE CARRIER IS sole_constructor AND IS MINTED ONLY HERE, inside the fold that HAS the
+// walk state -- the receipt and the hits come from one `walked` and cannot come from anywhere else.
+// The judgement itself stays ordinary and freely testable as scan_is_a_declared_population over a
+// receipt, which is what the hermetic claims exercise; what they can no longer do is mint the
+// production-positive carrier, which is correct, because the live route that would justify one is
+// still missing and says so.
+// TWO TYPES, BECAUSE sole_constructor SEALS A RECORD AND IS DISCARDED ON A COPRODUCT. An earlier cut
+// wrote `type ScanOutcome sole_constructor = <coproduct>` and claimed the cross-population pairing
+// was unwritable. It was not: v1.02_parse threads the modifier into the anonymous-record arm and
+// drops it on every other `=` right-hand side. That hole is not a fact discovered here: it is the
+// rostered class gunbc.recurring_failure_mode modifier_accepted_on_a_shape_its_check_cannot_see,
+// which carries its own probe and next-rung trigger -- so an outside module could still author ScanDeclaredPopulation { receipt:
+// from_population_A, hits: from_population_B } directly, which is the exact invalid state the seal
+// was supposed to remove. The honest production path was correct; the dishonest construction stayed
+// available, and green CI could not discharge it because it is a compiler behaviour rather than a
+// test failure.
+//
+// THE RECORD IS WHAT THE LANGUAGE ACTUALLY SEALS: infer's sole_constructor_construction_diags
+// refuses a construction whose span.file differs from the declaring type's. So the judgement is an
+// ordinary coproduct anyone may build, and the AUTHORITY binding a receipt to the hits it came from
+// is a sealed record minted only inside scan_partition, where both come from one walked state.
+type ScanDisposition
+  = ScanDeclaredPopulation { hits: List<CodeSearchHit> }
+  | ScanNotAPopulation
+
+type ScanOutcome sole_constructor {
+  receipt: ScanReceipt
+  disposition: ScanDisposition
+}

dag/gunbc/github_observation_record.dag

@@ -127,14 +127,15 @@ fn observation_is_usable_as_population(c: ObservationCompleteness) -> Bool {
 // 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.
+// re-reading them WHEN IT CAN BE TAKEN, which is a standing rather than a number -- see
+// ObservationDigestStanding below -- 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
+  body_digest: ObservationDigestStanding
   completeness: ObservationCompleteness
   budget: ObservationBudgetStanding
 }
@@ -143,7 +144,7 @@ fn github_observation(
   request: GithubObservationRequest,
   observed_at: NonEmptyStr,
   api_version: NonEmptyStr,
-  body_digest: Fnv1a64Structural,
+  body_digest: ObservationDigestStanding,
   completeness: ObservationCompleteness,
   budget: ObservationBudgetStanding,
 ) -> GithubObservation {
@@ -164,6 +165,29 @@ fn github_observation(
   }
 }
 
+// THE BODY DIGEST THIS TRANSPORT CANNOT TAKE EITHER, AND THE REASON IT IS A STANDING RATHER THAN A
+// HASH OF SOMETHING ELSE. A body digest exists to let a reader check stored bytes without re-reading
+// them, so it is only a digest if it is taken OVER THOSE BYTES. This transport decodes a response
+// into a modelled shape and exposes no raw body anywhere, so for a decoded read there are no bytes
+// to hash -- and hashing what IS in reach produces a value that looks checkable and discriminates
+// nothing.
+//
+// THAT IS NOT HYPOTHETICAL, IT IS WHAT THIS MODULE'S FIRST CONSUMER DID. An earlier revision of
+// gunbc.ci_workflow_scan_producer scan_observation stored content_hash_atom(value: query), so every
+// record a scan emitted carried the SAME digest, and a reader checking bytes against it would have
+// got a green establishing nothing about the bytes. DESIGN section 5: no fabricated plausible
+// output. A field that cannot be filled honestly is modelled as unfilled, exactly as the budget
+// one below is, rather than filled with whatever was nearby.
+type ObservationDigestStanding
+  = DigestUnobservable { reason: NonEmptyStr }
+  | DigestObserved { digest: Fnv1a64Structural }
+
+data decoded_response_has_no_body_bytes_reason: NonEmptyStr = "this transport hands back a decoded shape and exposes no raw response body, so no digest can be taken over the bytes that were actually received; a hash of the request or of the decoded value would check a different thing while reading as a body digest"
+
+fn digest_unobservable() -> ObservationDigestStanding {
+  DigestUnobservable { reason: decoded_response_has_no_body_bytes_reason }
+}
+
 // 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

dag/test/claim/ci_workflow_scan_producer_witness_test.dag

@@ -7,6 +7,9 @@ import extdeps.github.code_search {
   CodeSearchHit,
   CodeSearchRepository,
   retrievable_result_ceiling,
+  CodeSearchPageSizeAdmitted,
+  CodeSearchPageSizeRefused,
+  admit_code_search_page_size,
   deepest_retrievable_page,
 }
 import gunbc.ci_workflow_source_read {
@@ -50,10 +53,28 @@ import gunbc.ci_workflow_scan_producer {
 // 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.
+// Every fixture below is a SUPPLIED page rather than a fetched one, and THE PAIRING OBLIGATION IS
+// NOT DISCHARGED IN THIS CHANGE. An earlier revision of this annotation said it was -- "met by
+// scan_partition, which calls the same folds against perform_code_search_page: the real route still
+// executes" -- and that sentence was doing the work of a claim while being prose. No claim in this
+// module invokes scan_partition, nothing else in the corpus invokes it either, and an annotation is
+// never evidence that a machine claim holds (DESIGN section 4c). The test the obligation actually
+// sets is that DELETING THE INTEGRATION MUST MAKE A CONTROL FAIL; delete perform_code_search_page's
+// call site today and every claim below stays green, which is the definition of the gap rather than
+// a quibble about wording.
+//
+// WHY IT CANNOT BE DISCHARGED HERE, stated so the gap is bounded rather than open-ended:
+// perform_code_search_page needs a network and a GitHub credential, and the witness lanes run with
+// neither. WHAT DISCHARGES IT: one inhabitance claim executed against the live endpoint, asserting
+// the ROUTE and not only the answer -- that a real CodeSearchPage reaches scan_observation and the
+// record it produces carries the query it was asked for. That is the same shape of evidence the
+// review sheet converge takes, and it is a receipt from a run rather than a lane that can be made
+// to pass without a token.
+//
+// So what the claims below establish is bounded and worth saying exactly: they discriminate at the
+// boundary where the MEANING is decided -- what a page and a walk state mean for whether a sample
+// may be called a census -- and they establish nothing about whether GitHub emits the shapes they
+// supply.
 
 fn w_repo() -> CodeSearchRepository {
   CodeSearchRepository {
@@ -193,6 +214,26 @@ test fn no_pages_read_leaves_the_size_unobserved() -> Bool {
 
 // 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.
+// THIS PAIR AND THE ONE BELOW ARE THE JUDGEMENT'S WALL AND CONTROL, AND THEY TEST THE JUDGEMENT
+// RATHER THAN THE CARRIER -- deliberately, which is the point of the ScanOutcome repair.
+//
+// WHAT IS FREELY CONSTRUCTIBLE AND WHAT IS NOT, stated exactly, because an earlier version of this
+// note got it backwards and named the wrong type as the wall. ScanDeclaredPopulation is an ORDINARY
+// ScanDisposition arm: any module may build it, and that is safe precisely because it carries NO
+// RECEIPT and therefore authorizes nothing. What cannot be built outside scan_partition is
+// ScanOutcome -- the sealed record that BINDS a receipt to a disposition -- so the invalid state the
+// carrier removes is a receipt from walk A paired with hits from walk B, not the existence of a
+// disposition value.
+//
+// So claims may and do construct dispositions; they cannot mint the authority that makes one a
+// scan's result. That is the wall working, and testing the judgement here is not a coverage gap.
+//
+// An earlier revision of this PR added two NEW claims here and called them that wall and control.
+// They were byte-identical in subject, inputs and expectation to this pair -- two names for one
+// fact, run twice -- and neither reached ScanOutcome or scan_partition at all, so they discriminated
+// nothing the branch did not already discriminate while being cited as coverage for the repair.
+// They are deleted; what is freely testable is scan_is_a_declared_population over a supplied
+// receipt, and these two already establish it.
 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 },
@@ -221,8 +262,15 @@ test fn an_exhausted_walk_over_a_saturated_query_is_not_a_population() -> Bool {
 // 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
+  match admit_code_search_page_size(observed: 100) {
+    CodeSearchPageSizeAdmitted { page_size: hundred } =>
+      deepest_retrievable_page(page_size: hundred) == 10
+        && match admit_code_search_page_size(observed: 50) {
+          CodeSearchPageSizeAdmitted { page_size: fifty } => deepest_retrievable_page(page_size: fifty) == 20
+          CodeSearchPageSizeRefused { observed: _, cause: _ } => false
+        }
+    CodeSearchPageSizeRefused { observed: _, cause: _ } => false
+  }
 }
 
 // A WALK WITH NO STOP REASON STOPPED BECAUSE IT RAN OUT OF PAGES, and saying so is what keeps
@@ -245,3 +293,34 @@ test fn a_full_page_record_names_the_next_page() -> Bool {
     ObservationRefused { cause: _ } => false
   }
 }
+
+
+// THE PAGE SIZE IS ADMITTED BEFORE THE WALK BOUND IS DERIVED FROM IT, and these three claims are the
+// wall and its controls. An earlier cut divided the retrievable ceiling by whatever Int arrived: a
+// caller passing 1000 got a bound of ONE PAGE, so a short first page reported StoppedExhausted and a
+// partial result was presented as a complete population -- the same shape as every other defect this
+// module exists to close, reached through a parameter rather than through an observation.
+test fn a_page_size_above_the_endpoint_maximum_is_refused() -> Bool {
+  match admit_code_search_page_size(observed: 1000) {
+    CodeSearchPageSizeRefused { observed: o, cause: c } =>
+      o == 1000 && string_contains(s: c as String, pattern: "at most")
+    CodeSearchPageSizeAdmitted { page_size: _ } => false
+  }
+}
+
+test fn a_page_size_below_one_is_refused() -> Bool {
+  match admit_code_search_page_size(observed: 0) {
+    CodeSearchPageSizeRefused { observed: o, cause: _ } => o == 0
+    CodeSearchPageSizeAdmitted { page_size: _ } => false
+  }
+}
+
+// THE CONTROL, without which a refusal of everything would satisfy both claims above while making
+// the producer uncallable.
+test fn the_endpoint_maximum_itself_is_admitted_and_bounds_the_walk() -> Bool {
+  match admit_code_search_page_size(observed: 100) {
+    CodeSearchPageSizeAdmitted { page_size: ps } =>
+      ps.size == 100 && deepest_retrievable_page(page_size: ps) == (retrievable_result_ceiling / 100)
+    CodeSearchPageSizeRefused { observed: _, cause: _ } => false
+  }
+}