XL-2 LoweringOccurrenceProjection 3b: census consumes occurrence roles; typed excluded populations; typed missing paths; repin (stacked on #12317)

[gunbai-bot]

XL-2 LoweringOccurrenceProjection, PR 3b: the census consumes occurrence roles; typed excluded populations; typed missing paths; repin

Stacked on #12317 (3a), which is stacked on #12314 and #12305. Retarget each to main as the one below it lands. Design: #12302, §3–§4. XL-2 manager rulings: (1) binders go in a typed counted excluded population; (2) headers get HeaderSegmentsNotRefusalSites with the nesting caveat; (3) nesting-scoped references get their own typed record; (4) deleted sample paths get a typed disposition, plus a repin.

1. The census reads roles (the consumer #12317 declared)

v2.compiler.reference_conservation conservation_against_tree now takes the roles that v2.compiler.occurrence_role dag_occurrence_roles produces for the module.

An atom whose locus is erased is sent by erased_atom_disposition to exactly one count:

• header_channel: a module-header segment (item −1). This is HeaderSegmentsNotRefusalSites.
• role_excluded: the atom has a recorded DeclarationRole, or a ReferenceRole whose category std.occurrence_identity occurrence_category_module_scope_exposure_verdict calls not module-scope (a field label or an argument label).
• locus_erased: otherwise. It now means exactly "a reference lost its locus".

The rule is not restated: the census asks the existing verdict function. An atom with no occurrence and no pool copy is still dropped, whatever its role.

The producer's gaps are carried into every report as role_not_yet_read and role_reader_refused. A binder the producer cannot read yet stays in locus_erased and is also counted there. A role table the grammar does not admit gives a typed unmeasured entry, OccurrenceRoleTableUnadmitted. It never reports every atom as a reference.

The summary line renders all four new numbers.

2. The rehearsal's excluded populations (gunbc.namespace_xl2_rehearsal_census Xl2ExcludedPopulation)

This adds two arms beside Xl2KernelCanonicalReferencesUncounted:

• HeaderSegmentsNotRefusalSites. No resolve refusal is located at a header segment. This was measured on this composition with a module whose header names a nonexistent path. Its atoms are counted by the census header_channel.
• NestingScopedReferencesUncounted. A module nested under a provider's namespace resolves that provider's names with its import stripped, so the residual cannot see the reference, exactly as for kernel names. It is uncounted for the same reason: the resolved arm keeps no tree. The trigger for counting it is that the census carries which scope resolved each reference.
  • Open question, stated rather than answered: is XL-6 meant to keep nesting-granted scope? If not, these references become residual and the arm dissolves. The XL-2 manager has raised this separately.
  • New executing control: a nesting run in the shared warm producer, xl2_nested_reference_survives_the_strip_holds. The provider and the nested module both resolve after the strip, with no residual.

3. Typed missing paths and the repin (v2.compiler.reference_conservation_census)

reference_conservation_path_observation observes each listed path through extdeps.filesystem.filesystem_io filesystem_file_observation. That function establishes absence from a successful listing, never from a failed read (review 71731). Its result is one of:

• SamplePathMissing: the parent directory's listing establishes the file is not there. Only this arm means the pin is stale.
• SamplePathUnreadable { cause }: the file is listed, but its read failed. The host's error is kept, because an unreadable file calls for the opposite fix: investigate the environment, do not repin.
• SamplePathObservationsDisagree / SamplePathSubjectRefused: the listing and the read contradict each other, or the path is malformed.
• SamplePathMeasured / SamplePathGrammarUnprepared: as before.

The rendered census line is derived from the type. Run for real: a missing file, a chmod 000 file and a real module render missing ..., unreadable ... Permission denied (os error 13) and a measured report.

Repin. The sample's rule is now stated exactly: the share is over all .dag files. That wording was ambiguous before, and I fixed it by reproduction: applying the rule at fec339d561 regenerates the original 315-path list with zero differences. Re-applied at main 8fcd8e77b8, it gives 316 paths, and all of them exist on this branch.

Carrier wording for gunbc.compiler_frontend_program_status (proposed, for the next carrier update; not edited here)

Replace the whole why string of the LoweringOccurrenceProjection arm, not only its closing "No fix has merged.". The current opening sentences describe the tag and spine defects in the present tense, and #12305 and #12314 have fixed both. The proposed text:

Reference-position atoms that lowering rebuilds now carry their authored token's occurrence at the two sites that rebuilt them: record-literal tags and pattern constructors are lowered from their tag token (#12305), and dotted-spine segments from their own tokens (#12314). The occurrence-role producer (#12317) and the conservation census that consumes it (#12334) separate binders, labels and module-header segments -- outside the XL-2 residual -- from references, so locus_erased now counts only references that lost their locus. The per-module count is re-derived by v2.compiler.reference_conservation_census reference_conservation_stratified_sample_census rather than transcribed here. Design: docs/plans/lowering-occurrence-projection-design.md.

The arm stays PrerequisiteOutstanding. Adapted from calm-heron-346's draft on #12314.

Evidence (local, seed-run interpreter)

• v2.test.claim.namespace_xl0.reference_conservation, all 19 claims run. 16 are true. The 3 false ones are the same 3 that were false before PR 1: if-arm call argument, list-literal argument, repeated spelling. CI's floor is the authority on those.
  • Updated: the clean control now asserts conserved + locus_erased + role_excluded + header_channel == authored, with every part non-zero. The tag and spine fixtures assert their conserved counts; their erased atoms are now summed across the three channels.
  • New: the_clean_control_counts_its_header_segments_in_the_header_channel_holds (3 segments).
  • New: binders_and_labels_are_role_excluded_not_locus_erased_holds. On the tag fixture it asserts role_excluded=5 (the type, the two fn names, the record-literal label and the pattern label), header=3, locus_erased=3 and not_yet_read=3; the last two are the parameter and field-declaration binders.
• Mutation red: making erased_atom_disposition answer ErasedReference for every role turns the new claim false. The file was restored byte-identical.
• test.claim.namespace_xl2_rehearsal_census, all 8 claims true. The walls claim now checks the three excluded arms by identity, not by count. The new xl2_nested_reference_survives_the_strip_holds passes.
• Path dispositions, run for real: reference_conservation_census_for_paths over a missing file, a chmod 000 file and dag/examples/blackjack/hand.dag. It renders missing ..., then unreadable ... Permission denied (os error 13), then a measured report (authored=8 conserved=2 locus_erased=2 role_excluded=1 header_channel=3 role_not_yet_read=1).
• Resolve-check (NoSuchFunction): all touched modules.
• The admission wall has already fired for real once. After main was merged up the stack, the role table refused the grammar: main had replaced io_block with input_block and output_block. That is fixed in XL-2 LoweringOccurrenceProjection 3a: v2 occurrence-role producer, grammar-admitted table (stacked on #12314) #12317. Without the check, those productions would have been read silently as references.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 71731 in a5a3a4d.

Missing and unreadable are no longer conflated. The census now observes each listed path through the existing authority for exactly this distinction: extdeps.filesystem.filesystem_io filesystem_file_observation. Its own note reads "absence is established by a successful listing, never by a failed read". So:

• SamplePathMissing is now only a path the parent directory's listing establishes as absent, meaning a stale pin.
• SamplePathUnreadable { path, cause } is a listed file whose read failed. The host's error is kept.
• SamplePathObservationsDisagree and SamplePathSubjectRefused are their own arms, each with its cause.
• The type's doc comment now describes each arm exactly.

Run for real over a missing file, a chmod 000 file (as uid 1000, so the permission check discriminates) and a real module:

missing dag/std/no_such_file.dag
unreadable .scratch_xl2/unread/locked.dag .scratch_xl2/unread/locked.dag is listed and could not be read, so it exists and its content is unavailable -- Permission denied (os error 13)
module dag/examples/blackjack/hand.dag authored=8 conserved=2 ...

— sent from tidy-otter-111

[gunbai-bot]

Re review 71744's non-blocking remark, about the repinned list having no re-deriving entry point.

Agreed: the rule is stated exactly, and it was verified by reproducing the original 315-path list at fec339d561, but no .dag entry point re-derives it (DESIGN §6: name the instrument). As the review notes, this PR does not make that worse; the original list was hand-copied too.

A faithful entry point needs a whole-tree walk plus per-file sizes from Filesystem, and the stratum arithmetic in .dag. That is its own change, not something to fold into the census consumer. I am raising it with the XL-2 manager as a follow-up item:

A v2.compiler.reference_conservation_census entry point that derives reference_conservation_stratified_sample_paths by the stated rule at the checked-out tree, plus a claim that the pinned list equals its output. At that point the literal list can stop being hand-maintained.

— sent from tidy-otter-111

[briansrls]

HOLD / REQUEST_CHANGES at exact head 2ed6b27.

Two boundary defects prevent approval. Neither requires reopening the occurrence-role design or completing the ten NameRoleNotYetRead readers.

1. [P2] Preserve the directory identity when splitting a sample path — src/v2/compiler/reference_conservation_census.dag:84-96.

sample_path_parts("/tmp/rc/probe.dag") produces directory="tmp/rc", name="probe.dag": the leading empty component is discarded, so the absolute parent becomes relative. reference_conservation_path_observation then lists that different directory but reads the ORIGINAL absolute path. A readable file can consequently be reported unreadable or observations-disagree. More importantly, when the wrong relative directory exists and omits the name, an existing absolute file whose read fails with permission denied reaches FilesystemFileAbsent and then SamplePathMissing; the original host error is discarded. That recreates the absent-versus-unreadable conflation that review 71731 repaired, through mismatched subjects rather than through the filesystem fold itself.

The same helper gives a bare "probe.dag" an empty directory, so filesystem_listing_observation returns FilesystemDirectorySubjectRefused even though a basename is a valid current-directory read. "./probe.dag" works differently from "probe.dag".

Please preserve the original parent/root, use "." for a basename's parent, and ensure listing membership and file read refer to the same subject. Add controls for a basename, an absolute path, and an absolute unreadable file beside an unrelated empty relative shadow directory. The last case must preserve the host cause and must not become SamplePathMissing. This is a correction at this caller; it does not require a repository-wide filesystem migration.

2. [P2] Do not render unobserved role gaps as zero on normalization refusal — src/v2/compiler/reference_conservation.dag:1085-1094.

After parsing succeeds, dag_occurrence_roles is called only inside the Accepted normalization arm. The Rejected arm instead calls conservation_against_refusal directly; that starts from report_from_population, where role_not_yet_read and role_reader_refused are both zero, and neither is populated on that route. Thus a parsed binder-bearing module which normalization refuses loses the role-gap observation entirely. The same route never consults role-table admission, so a table refusal cannot produce OccurrenceRoleTableUnadmitted there. The promised 'gaps carried into every report' and typed-unmeasured table refusal currently hold only for normalized-success reports.

Please obtain/admit roles once after successful parsing and propagate their gap counts into both normalized-success and normalized-refusal reports. Preserve normalization's own refusal accounting; this is not a request to reclassify a normalization refusal as successful conservation. A refused role table must retain a typed unmeasured disposition rather than disappear behind that other branch. Add a parsed binder-bearing subject with a deliberately refused normalization outcome and assert its gap counts survive, plus a refused-role-table/normalization-refusal control.

Evidence and scope: the exact-head workflow 36324332195 reports success for floor, compiler, clippy, emit-build and witnesses. Those results do not exercise the two counterexamples above. I independently checked the path splitter with a direct Python transliteration and exercised the filesystem observations under an unprivileged local process: the requested absolute file existed, its read failed with errno 13, while the incorrectly selected relative directory listed successfully without that entry. This was a source/host-boundary reproduction, NOT execution of the .dag census. I did not run new .dag/native tests or mutation tests, and I did not independently rerun the sample-selection rule.

The existing-category reuse, typed header/nesting exclusions, and nullary warm specialization are not the reasons for this HOLD. The requested fixes concern subject fidelity and report completeness at the new boundaries. Also retain the existing caveat that locus_erased still contains binders whose roles are not yet read; the PR's own fixture explicitly has three of those.

Head rechecked unchanged before submission. Latest PR metadata now reports mergeable=false against main bcbf786, so CLEAN is no longer confirmed by that read. No enqueue or merge performed. After the fixes, rebind the review to the new exact head and require its merge-group candidate to pass.

[briansrls]

[P2] The splitter changes the listing subject. /tmp/rc/probe.dag becomes directory tmp/rc, but the subsequent Read still uses /tmp/rc/probe.dag. With an empty relative shadow directory and an existing unreadable absolute file, the listing says absent and the read fails, so this caller reports SamplePathMissing and discards PermissionDenied. A bare probe.dag also produces directory "", which the listing-subject admission refuses instead of treating as .. Preserve the absolute parent/root and use . for basenames; exercise the mixed-directory unreadable case so the absence claim is about the path actually requested.

[briansrls]

[P2] The role observation/admission runs only when normalization succeeds. A parsed module whose normalization is Rejected goes straight to conservation_against_refusal, retaining the zero role_not_yet_read/role_reader_refused defaults from report_from_population; it also never surfaces a refused role table as OccurrenceRoleTableUnadmitted. Please carry the role observation across both normalization outcomes, preserving normalization-refusal accounting and typed unmeasured role-table failures. A parsed binder-bearing specimen with an injected normalization refusal should retain its nonzero role-gap count.

[gunbai-bot]

Addressed GitHub review 5330814496 (both inline findings) in b4fceb9.

1. sample_path_parts named the wrong subject.

• It now keeps the parent exactly as the path spells it: /tmp/rc/probe.dag → /tmp/rc, /probe.dag → /, and a bare probe.dag → ..
• The classification is now a pure sample_path_observation_of(path, listing, read). If the listing is of any directory other than the path's own parent, it refuses as a subject mismatch (SamplePathSubjectRefused) instead of asking that listing about the entry. So absence can no longer be read off the wrong directory.
• reference_conservation_path_observation now only performs the two host calls and hands their results to that function.
• New controls in v2.test.claim.namespace_xl0.reference_conservation_census, all given supplied observations:
  • splits for absolute, root, bare and relative paths;
  • an unreadable absolute file gives SamplePathUnreadable, with "Permission denied" kept;
  • the same file observed against a listing of the unrelated empty relative directory gives SamplePathSubjectRefused, never SamplePathMissing;
  • a positive control: a correct parent that does not list the entry gives SamplePathMissing.
• The absolute, root and bare-name split controls are false on the old split.

2. Roles were not observed when normalization refused.

• Roles are now obtained and admitted immediately after a successful parse, in reference_conservation_of_subject_admitted, which takes the admission as a parameter.
• In the refusal arm, the report keeps normalization's own refusal accounting and adds the role gaps. If the table is refused, it records OccurrenceRoleTableUnadmitted instead.
• New controls in v2.test.claim.namespace_xl0.reference_conservation:
  • A parsed, binder-bearing module whose normalization refuses (an else-less if) reports role_not_yet_read == 1, and refused plus drops still cover the whole population. Red run: the old code reports role_not_yet_read=0 on the same subject, with identical refusal accounting (refused=2 authored=12).
  • A planted refused table alongside a normalization refusal surfaces as unmeasured, and the refusal accounting is intact.

— sent from tidy-otter-111

[gunbai-bot]

Re review 71809's non-blocking note, on the atom.item < 0 sentinel in erased_atom_disposition.

Agreed it is weaker than a typed discriminator, but this PR did not introduce it. It is the census population's existing encoding: authored_atom_population starts the walk at item: 0 - 1 for atoms outside every top-level item, and item_pool and item_declaration_found already branch on item < 0 the same way. erased_atom_disposition reads the same fact, so there is one encoding, not a second one.

The typed version is a change to AuthoredAtom.item itself, something like ItemHeader | ItemDeclaration { index }, carried by all three readers at once. Patching only this new reader would split the encoding. I am noting it as a follow-up rather than widening this PR.

— sent from tidy-otter-111

[briansrls]

APPROVE-MERGE at exact head b4fceb9, through the merge queue only. Review 5330814496's two blockers are satisfied.

1. Path-subject fidelity: sample_path_parts preserves the absolute parent/root and uses '.' for a basename. The pure observation boundary checks that the supplied listing is for that very parent before using it as evidence. An empty relative shadow directory cannot establish absence of the requested unreadable absolute file: the mismatch is SamplePathSubjectRefused. With the correct parent, read refusal retains its host cause; genuinely established absence remains SamplePathMissing. The split, wrong-directory, unreadable and positive-missing controls discriminate the former implementation.

2. Report completeness: roles are now observed immediately after successful parsing and consumed by both normalization outcomes. A refused normalization keeps its original authored/refused/dropped accounting while receiving the role-gap observation. A refused role table remains typed unmeasured on that route instead of disappearing behind normalization refusal. The parsed binder-bearing/refused-normalization control and planted-table-refusal control exercise these joins rather than merely checking record construction.

I reviewed the source delta and execution evidence. Exact-head workflow 36333451979 has all five jobs successful, including the floor and its changed-witness qualification. No new local .dag/native test, mutation, sample-selection reproduction, or census run was performed by me.

Scope remains PR3b's census consumption, not completion of every role reader or the real-tree XL-2 rehearsal. In particular, locus_erased still includes binders whose role is not yet read; the explicit role-gap counters must accompany any interpretation of that count. The header/nesting exclusions and open XL-6 question remain qualified as before. The warm specialization shares language-only derived facts, not claim verdicts, and does not raise the claim budget.

This supersedes the previous HOLD. Require a passing merge_group candidate against then-current main; do not direct-merge or bypass checks.

Superseded by APPROVE review 5331373952 on exact head b4fceb9. The path splitter and listing-parent join now preserve the requested subject, and role gaps/table refusal survive normalization refusal with discriminating controls.