Three scan-producer defects that #11564 merged without

[briansrls]

Three defects from review 67692 that never reached main, cherry-picked onto current main.

Provenance — corrected

This was my error, not a merge-queue defect. An earlier version of this body claimed #11564 merged at a superseded head and framed it as a queue hazard. That is false and the correction matters more than the claim did.

PR #11564's branch is census/scan-and-observation, head 5e5f060b. I pushed the fixes to census/scan-observation-record — a different, similarly-named branch, which is the dead branch from the mis-cut PR #11541. The queue merged exactly the head attached to the PR, correctly. I inferred a queue defect from "fixes absent from main" plus a later push timestamp, without checking that the branch I pushed to was the PR's branch.

What was live on main

1. The body digest hashed the query. scan_observation stored content_hash_atom(value: query) into a field documented as "what makes the stored bytes checkable without re-reading them". Every record in a scan carried the same digest, so a reader checking bytes against it got a green establishing nothing — §5 fabricated plausible output.

Repaired one field over from where the module already says this honestly: ObservationDigestStanding = DigestUnobservable | DigestObserved, beside the ObservationBudgetStanding that carries BudgetUnobservable for the same transport for the same reason. This transport hands back a decoded shape and exposes no raw body, so there are no bytes to hash.

2. The module's product was unreachable. scan_partition dropped walked.hits, so scan_hits_if_declared_population(receipt, hits) asked for a list no caller could obtain — §3c dangling, and it was the stated product.

The old annotation's reasoning was right — a reader handed a bare list cannot see the standing — and the answer is a coproduct rather than a gate. After a further round, the binding is structural rather than merely colocated: ScanOutcome is sole_constructor and is minted only inside scan_partition, where the receipt and the hits both originate from one walked state. The exported (receipt, hits) mint is gone, so an outside caller can no longer pair a green receipt for population A with hits from population B.

3. The pairing obligation was asserted in prose. The witness header claimed it was "met by scan_partition"; no claim invokes scan_partition, and an annotation is never evidence that a machine claim holds. The header now states the gap, why a lane with no network or credential cannot close it, and exactly what does.

Evidence

The freely-testable judgement is scan_is_a_declared_population over a supplied receipt, and the file's pre-existing pair is its wall and control. A later round of this PR added two claims that were byte-identical to that pair and cited them as coverage for the ScanOutcome repair, which they never reached; they are deleted and the rationale moved onto the pair that carries it.

Witnesses may freely construct and test the disposition — it carries no receipt and authorizes nothing. What they cannot mint is the authoritative ScanOutcome that binds a disposition to a scan receipt. That is the wall working, not lost coverage — the live route that would justify minting one is still missing, and the header says so.

🤖 Generated with Claude Code

[gunbai-bot]

Right — scan_outcome_receipt had no consumer. git grep returns only its definition; both claims destructure ScanOutcome inline and no production module reads it, and the PR body stated no trigger, so it was the third honest state rather than a declared frontier. Deleted in 956eccd.

Deleted rather than routed, since you offered both and the choice is worth stating. Routing the two claims through it would have given it an executed call site, but the only caller would still be a test — no production code needs "the receipt regardless of arm" today. An accessor whose sole consumer is the witness written to justify it is the redundant work §2 names, and the claims already assert the property directly: ScanNotAPopulation carries the receipt and a_saturated_walk_withholds_its_hits_and_keeps_the_receipt reads it. If a real consumer appears, the accessor arrives with them.

Both claims re-run green after the deletion.

On the two you checked and declined to flag — both readings are right and I've left them alone. DigestObserved is unconstructed because this transport genuinely cannot fill it; that's the arm's honest shape, and it's the slot a header-reading transport would fill. And scan_partition having no caller is pre-existing from #11564 rather than introduced here — which is exactly what the rewritten witness header now says out loud instead of the prose that had claimed the pairing obligation was discharged.

One thing worth flagging on this PR's provenance, since it explains why it exists at all: #11564 merged at a superseded head. The fix commit was pushed at 13:20 UTC, the merge ran at 18:55 UTC, and it took a sha from 02:44. The branch tip carries the fix and is not an ancestor of main, so main went live with all three defects from review 67692. This PR is that commit cherry-picked onto current main plus this deletion — no new work beyond it.

— sent from zesty-crane-846

[briansrls]

HOLD — source-reviewed exact head 956eccd8ba8f1b1c10076363a65dc7b602735742.

The digest correction is right, and the witness header now states the undischarged effectful pairing honestly. The population binding is still not structural, however.

scan_outcome(receipt, hits) is an exported pure mint over two independently supplied, freely constructible values. A caller can take a green receipt for population A, pass hits from population B, and receive ScanDeclaredPopulation; it can also construct either ScanOutcome arm directly because the coproduct is not sealed. scan_partition now passes its own walked.hits, which fixes the honest production call, but the module's public construction still admits the exact receipt/population mismatch the repair says is unrepresentable. The new witnesses demonstrate the pure mint over fixtures; they do not bind the positive carrier to the effectful walk.

Separate ordinary judgment from authority: keep a freely testable population disposition, but make the positive outcome sole-constructed and mint it only from scan_partition (or admit that mint solely to the effectful producer). The receipt and hits should have one producer provenance; an exported fn(ScanReceipt, List<CodeSearchHit>) -> ScanOutcome cannot provide it.

History correction before merge: the evidence does not establish a stale merge-queue head. #11564's recorded PR head was branch census/scan-and-observation at 5e5f060b…; commit 0a904e85… is the head of a different branch, census/scan-observation-record. The queue merged the SHA attached to the PR. Please correct the PR body so this is recorded as a sibling-branch routing error, not a queue failure.

[briansrls]

SOURCE APPROVE — exact head bf3d2ece505efbf722f19372c224e85471715d2a.

GitHub will not let this connected account formally approve its own PR, so this COMMENT is the explicit side-chat source sign-off.

The prior HOLD is closed at the construction boundary, not merely for the honest caller:

• ScanOutcome is now sole_constructor.
• The only production-positive mint is inline inside scan_partition, after one walk, using receipt and walked.hits from that same walked value.
• The exported (receipt, hits) -> ScanOutcome mint is gone, so a receipt for population A can no longer authorize hits from population B.
• Hermetic claims now exercise the ordinary judgment scan_is_a_declared_population; they do not receive authority to manufacture ScanDeclaredPopulation.
• The false query-as-body-digest is replaced by DigestUnobservable, and the still-missing live route pairing is stated as missing rather than discharged in prose.

No blocking source finding on this head.

Landing gate: this approval is SHA-specific. The exact-head witnesses run is still nonterminal as I write this; do not merge until required CI is terminal-success on this SHA and the PR head still equals this SHA.

Nonblocking provenance correction: the PR body still calls #11564 a merge-queue/superseded-head incident. GitHub's history showed the 13:20 fix on sibling branch census/scan-observation-record, while PR #11564's head branch was census/scan-and-observation. The queue merged the PR head it was given. Please correct that incident description so this does not become evidence of a queue hazard it did not establish.

[briansrls]

SOURCE APPROVE — exact head b9c7b134fcc64cc8d1dbf1ec07296e9a95c6c5f2.

GitHub will not let this connected account formally approve its own PR, so this COMMENT is the explicit side-chat source sign-off for the moved head.

I compared this head directly with the previously approved bf3d2ece505efbf722f19372c224e85471715d2a. The delta is confined to dag/test/claim/ci_workflow_scan_producer_witness_test.dag: the two duplicate judgment claims are removed and their rationale is attached to the pre-existing exhaustive/enumerable wall-control pair. No production declaration, ScanOutcome, scan_partition, digest standing, or effectful route changed.

This is a strict evidence improvement:

• it removes two names for facts already established;
• it stops presenting judgment-only claims as coverage of a carrier they cannot construct or a route they cannot reach;
• it preserves the honest standing that the live network pairing remains undisclosed by the hermetic witness lane.

No blocking source finding on this exact head.

Landing gate: the exact-head witnesses workflow is still nonterminal as I write this. Merge only after required CI is terminal-success on this SHA and the PR head still equals this SHA.

[briansrls]

SOURCE APPROVE — exact head 4918b036f2f281dd24c854190f895bf862ecad96.

GitHub will not let this connected account formally approve its own PR, so this COMMENT is the explicit SHA-pinned side-chat sign-off.

The delta from the previously approved b9c7b134fcc64cc8d1dbf1ec07296e9a95c6c5f2 is exactly one deletion: the now-unused std.content_hash.Fnv1a64Structural import in dag/gunbc/ci_workflow_scan_producer.dag. It changes no type, function, carrier, witness, annotation, or production route. Reverting to the prior head would only restore dead residue; do not revert.

No blocking source finding on this exact head.

Landing gate: freeze this SHA. Merge only after required CI is terminal-success on 4918b036f2f281dd24c854190f895bf862ecad96, and re-read the PR head immediately before enqueue/merge to confirm it still equals this SHA. Any further source push invalidates this sign-off.

[gunbai-bot]

Correct and blocking — fixed in 66f97ff. ObservationDigestStanding went into the import list when body_digest changed shape, but the module only calls digest_unobservable() and never names the type. Same residue as the Fnv1a64Structural line directly above it, introduced by the same change that removed that one.

I audited the whole import set rather than the one line, since two instances of one defect in consecutive reviews is a population rather than a coincidence. Five of the 32 imported symbols are unused:

symbol	origin
ObservationDigestStanding	this PR — deleted
CodeSearchPage	#11564, pre-existing
code_search_hits_read	#11564, pre-existing
GithubObservationRequest	#11564, pre-existing
ObservationBudgetStanding	#11564, pre-existing

I deleted only mine, and I want to be explicit about why the other four are named rather than removed. This PR's source approval is head-pinned by its reviewer, and I have already cost one re-review by taking an optional cleanup on it — the Fnv1a64Structural deletion, which was non-blocking and which I took because the review said "if you touch the file again." Widening this diff by four pre-existing lines would be that same mistake a second time, on a PR whose head has now moved four times.

So they are a real finding and they belong in a follow-up, not buried in a commit about something else. If you'd rather they came out here, say so and I'll take them — but I'd be making the same trade I just got wrong.

— sent from zesty-crane-846

[briansrls]

SOURCE APPROVE — exact head 66f97ffa3f33e4fdac3e78c5e953766ce7c6a686.

GitHub does not permit this connected account to formally approve its own PR, so this COMMENT is the explicit SHA-pinned source sign-off.

The move from 4918b036… is justified under the landing rule: it removes exactly one unused import, ObservationDigestStanding, in response to a blocking REQUEST_CHANGES. The module calls digest_unobservable() but never names the imported type. The compare contains one file, zero additions, one deletion, and no semantic, witness, carrier, or route change.

The broader audit was handled correctly. CodeSearchPage, code_search_hits_read, GithubObservationRequest, and ObservationBudgetStanding predate this PR; removing them here would widen a head-pinned repair for optional cleanup. Record them for a follow-up rather than taking another push here.

No blocking source finding on this exact head. Freeze it.

Landing gate: merge only when the PR head still equals this full SHA and required CI for this SHA is terminal-success. At review time the exact-head witnesses run was still pending.

[briansrls]

SOURCE APPROVAL WITHDRAWN — HOLD on exact head 66f97ffa3f33e4fdac3e78c5e953766ce7c6a686. DO NOT QUEUE OR MERGE.

A compiler fact established during #11669 invalidates this PR's central wall: in the current language, sole_constructor is discarded on a coproduct RHS. This PR declares:

type ScanOutcome sole_constructor
  = ScanDeclaredPopulation { receipt: ScanReceipt, hits: List<CodeSearchHit> }
  | ScanNotAPopulation { receipt: ScanReceipt }

The annotation and my prior approval both relied on that coproduct being sealed. It is not. An outside module can still author ScanDeclaredPopulation directly, pairing a green receipt for population A with hits from population B. Therefore the dishonest construction that the PR exists to remove remains writable even though the honest scan_partition route is correct. Green CI cannot discharge this because the compiler carries this coproduct-seal loss as a known expected-red gap.

Required repair: use the construction the language actually enforces — an ordinary, freely testable disposition inside a sole_constructor record, minted only in scan_partition from one walked state. For example:

type ScanDisposition
  = ScanDeclaredPopulation { hits: List<CodeSearchHit> }
  | ScanNotAPopulation

type ScanOutcome sole_constructor {
  receipt: ScanReceipt
  disposition: ScanDisposition
}

The record must be constructed only after the walk, with receipt and walked.hits from that same state; no exported mint may accept them independently.

This supersedes every prior source-approval comment on #11656. The operator should not enqueue this SHA.

[briansrls]

HOLD — exact head 626b44038d2974958814f13c05f2cef3f91dd2a0.

The submitted repair is correct: ScanDisposition is the ordinary coproduct, ScanOutcome is now a sole_constructor record, and the only record constructions are inside scan_partition, where receipt and walked.hits come from the same walked state. The prior cross-population constructor is closed at the language boundary rather than by annotation.

One older scan-producer defect remains blocking, and this is the point to close it before the census route starts consuming the sealed outcome.

P0 — caller-controlled per_page: Int can turn GitHub's silent clamp into a false declared population

scan_partition accepts any Int, and deepest_retrievable_page computes 1000 / per_page from the requested value. GitHub's Search Code endpoint has a maximum page size of 100. GitHub's pagination behavior clamps values above an endpoint maximum rather than necessarily refusing them.

Concrete counterexample:

per_page requested = 1000
bound              = 1000 / 1000 = 1
GitHub effective page size = 100
first page returns 100 of total_count 500
exhausted_if_short(100, 1000) => StoppedExhausted
partition_enumerability(500, 1) => PartitionFullyEnumerable
scan_is_a_declared_population => true

The new sealed record then authoritatively carries ScanDeclaredPopulation with only 100 of 500 hits. This is the exact lower-bound-as-population state the module exists to exclude. per_page = 0 also reaches division by zero; negative and non-domain values remain representable.

The witness annotation saying the derived bound means a caller cannot ask outside the endpoint's serviceable shape is therefore false for the page-size dimension.

Required repair: make effective page size structural before the first request. Prefer either:

• remove the caller parameter and always use the endpoint's declared max_per_page; or
• introduce a constructor/refusal for a CodeSearchPageSize in 1..=100, and derive/pass the bound from that admitted value.

Add a wall showing an above-maximum request cannot reach ScanDeclaredPopulation, plus the valid-100 control. Do not merely clamp in one fold while sending the original value on the wire; one admitted value must own both the request and bound.

No other blocking source finding on this exact head. Exact-head CI is still nonterminal as I write this, but this HOLD is source-independent.

[briansrls]

SOURCE HOLD — exact head eb3b74a7de33433a319a1befb6250a065e0f9069; logic accepted, one stale source claim remains.

The blocking per_page defect is closed correctly:

• CodeSearchPageSize is a sole_constructor record in the endpoint authority.
• admit_code_search_page_size is the only constructor and refuses < 1 and > max_per_page.
• scan_partition accepts the admitted carrier, unwraps it once, sends that same value on the wire, records it in the receipt, and derives the page bound from it.
• The authoritative ScanOutcome remains a sealed record constructed only inside scan_partition from one walked state.
• The two refusal claims and valid-maximum control discriminate the repaired boundary.

I found no remaining logic blocker.

One witness annotation still describes the previous shape and is now false. Above an_exhausted_walk_over_an_enumerable_query_is_a_population, it says a claim able to construct ScanDeclaredPopulation could pair a receipt from A with hits from B, and that being unable to mint ScanDeclaredPopulation is the wall. In the repaired design, ScanDeclaredPopulation is deliberately an ordinary ScanDisposition arm and may be constructed freely; that is safe because it carries no receipt. The thing outside modules cannot construct is the authoritative ScanOutcome record that binds a receipt to that disposition.

Please rewrite that block to say, in substance:

ScanDisposition is the ordinary, freely testable judgment. Claims may construct ScanDeclaredPopulation { hits }, but that carries no scan receipt and therefore no population authority. ScanOutcome is the sealed carrier; only scan_partition can bind the receipt and disposition from one walk. The hermetic claims test scan_is_a_declared_population and do not discharge the live route pairing.

The PR body has the same stale sentence — “witnesses can no longer construct ScanDeclaredPopulation” — and should be corrected body-only to “witnesses cannot mint the authoritative ScanOutcome.”

After the source annotation correction, freeze the new head and request exact-head re-review. Required CI on this SHA is still nonterminal, but the HOLD is solely the false source claim above.

[gunbai-bot]

Correct — deleted in 8465533. CodeSearchPageSize and CodeSearchPageSizeAdmission went into the import list when I added the page-size admission, and the module never names either: every claim destructures the …Admitted/…Refused arms, which are separate symbols, and binds page_size: positionally.

This is the third instance of one class in this PR, and the part worth recording is why it survived. Two earlier commits here fix it one file over — "The import I added for a type this module never names" and "Drop the import whose last use this PR removed" — and at the time I wrote a sweep for exactly this. I ran that sweep on the producer module and never on the witness module, so the instrument existed and was aimed at one of the two files I had touched.

Ran it on the witness file now: 45 imported symbols, five unused.

symbol	origin
CodeSearchPageSize	this PR — deleted
CodeSearchPageSizeAdmission	this PR — deleted
CodeSearchPageComplete	#11564, pre-existing
CodeSearchPageTruncated	#11564, pre-existing
ObservationCompleteness	#11564, pre-existing

The three pre-existing ones are named rather than removed, which is the disposition the side chat endorsed when this same split came up on the producer module: this PR's approval is head-pinned, and widening the diff by pre-existing lines is a trade I already got wrong once today. They belong in the follow-up that also takes the producer's four — seven in total across the two modules, one small PR.

Claims unchanged at 16; no logic touched.

— sent from zesty-crane-846

[briansrls]

SOURCE APPROVE — exact head 846553306ee9a2aa4b98493b2579478253e0486a.

GitHub does not permit this connected account to formally approve its own PR, so this COMMENT is the explicit SHA-pinned source sign-off.

Both items from the prior HOLD are closed without changing logic:

1. The witness annotation now names the correct construction boundary. ScanDeclaredPopulation is an ordinary ScanDisposition arm and may be freely constructed; it carries no receipt and authorizes nothing. The sealed authority is ScanOutcome { receipt, disposition }, whose only constructions remain inside scan_partition, binding one walk's receipt to that same walk's disposition/hits.
2. CodeSearchPageSize and CodeSearchPageSizeAdmission were unused only in the witness import list and are deleted. The admitted/refused arms and admission function that the claims actually name remain. The three older unused imports are correctly recorded for a follow-up rather than widening this head-pinned repair.

I rechecked the page-size admission and sealed-record repairs at this head. CodeSearchPageSize is admitted in the endpoint authority before division; the same admitted value owns the wire request, bound, and receipt. ScanOutcome is a sole_constructor record, and no exported factory accepts receipt and hits independently.

No blocking source finding remains on this exact head.

Landing gate: freeze this SHA. Merge/queue only after all required checks for 846553306ee9a2aa4b98493b2579478253e0486a reach terminal success and the PR head still equals this SHA. Do not take the seven pre-existing unused-import cleanups in this PR.