MQ PR1 (model): a lowering closes its image; derived nodes mint OccurrenceProjected

[gunbai-bot]

PR1 of 2 (model) for MQ node adhoc-2713665c-ef7. This PR lands the id source, the image-closing pass, and the rule revision. PR2 is the cut: it migrates every producer in one change, adds the admission wall, and moves the consumers. Rulings: gentle-koi-724 and neat-boar-16 (both approved option B, with conditions); every condition is addressed below.

The defect

A lowering builds an image of several nodes from one authored node, and the old rule in v2.std.node let every one of them carry the source's OccurrenceMinted. The eager-newt-412 census found collisions in all 145 observed modules. Within one tree, an occurrence no longer identified a node.

The rule (revised in v2.std.node)

• node_lowered_from now marks a node as a member of its source's image.
• The builder that returns the image root closes the image with project_image_occurrences(root, snapshot).
• The root the builder names keeps OccurrenceMinted. The root is not inferred from shape.
• Every other member, in pre-order, becomes OccurrenceProjected { id, caused_by: source }.

Id source and collision argument (std.occurrence_identity)

The id is derive_projected_occurrence(snapshot, source, k) = N + cantor(source, k), where k ≥ 1.

• N and the scope come from one value. OccurrenceAllocatorSnapshot carries both the parse's next_id and its allocator-domain digest, so they cannot come from two different parses. The cause really is in the same allocator, so scoping it by that allocator's digest is honest.
• Why this cannot collide.
  • Authored ids fall in [0, N), and derived ids are ≥ N.
  • Cantor pairing never maps two different pairs to the same number.
  • Each source is unique because the parser minted it, and each k is unique within one source's image.
• Why a bare Int and not a structural id. The arm's id must stay a bare OccurrenceId. Two consumers need it:
  • v2.workflow.legacy_binding_delta insertion_provenance_entry wraps it in ScopedOccurrenceRef.
  • v2.lens.identity_captured_navigation node_source_symbol looks spans up by it.
• Bound. Each operand must be below 2^30, so the value stays below 2^62. Anything else is a typed refusal: ProjectedSourceNotAuthoredInSnapshot or ProjectedOrdinalOutOfRange.
• Stability. Depending on N adds no instability. Authored ids are dense and already shift under any token insertion, and annotations are disjoint from allocation (DESIGN §4c).
• Idempotence and nesting. A node is in the image when it is minted with the source, or projected with the source as its cause in the same scope. So a nested same-source image is renumbered over the outer image instead of colliding with it, and applying the pass twice gives the same result.
• What the pass never rewrites. Nodes carrying another source's occurrence, synthetic nodes, and projections whose cause is in a foreign scope.

Evidence (local executor, this branch)

I ran the witnesses with gunbc run built from this tree, through a scratch driver that ANDs every test fn in v2.test.provenance.image_occurrence_projection.

• Result: all 8 held (rc=0).
• Mutation: reverting the pass to stamp the source back produced rc=1, naming image_projection_three_derived_members_get_distinct_caused_ids_holds.
• Controls:
  • ≥3 derived members get distinct ids, each with caused_by = source.
  • Other sources and synthetic nodes are untouched.
  • Nested same-source images get distinct ids.
  • The pass is idempotent.
  • A foreign-scope cause is ignored.
  • A source outside the snapshot is refused.
  • k = 0 is refused.
  • A projected root is refused.

Rung, stated honestly. Until PR2 lands, the rule is stated and nothing enforces it. PR2 adds the admission wall that refuses two nodes with one minted id. Its red control is an image root with its closing pass removed.

Consumption (§3c)

The new declarations are consumed by the witnesses here. Their production consumers are the image-root builders in PR2, which is a declared frontier.

PR2 plan: producer classification

There are 52 grep sites plus one the grep missed (std/inhabitance.dag:338, derived). bfl = src/v2/compiler/body_lowering_fold.dag.

Class	Sites	PR2 action
Carry-forward (same node rebuilt; keeps its occurrence)	node_rebuild, node_minimal:405; 03_resolve 895, 921, 948, 985, 1210, 1672, 1747; bfl 3138, 4114, 4131, 4210	none
Single-node images (root only)	dag.dag 5690; node_query 272, 287, 450; target_model 4725; sugar 116/269/303; bfl 526, 1023, 1040, 1328, 1852/1859/1866, 2059, 2197, 2400, 4640, 5854, 7990	none; the pass is a no-op
Multi-node images (root plus derived members; close at the named root)	fn decl: root 3154; Arrow 3429; order Transform, spine and one label per parameter (arrow_signature 42/65, list_introduction 34/39)	close at 3154
	data decl: root 3393; Arrow 3377	close at 3393
	function value: root 4247; derived 4255, 4244, plus order nodes	close at 4247
	operation: root 8480; derived domain, 8445, and order nodes	close at 8480
	service: root 8634; derived 8632	close at 8634
	type decl: root 8111; derived 8085	close at 8111
	where clause: root 790; derived 780, 772, 749/755	close at 790
	T<A>?: root Cardinality 2000; derived Instantiation 1982	close at 2000
	namespace graft: root 644; one wrapper per segment 609; body 596	close at 644
	list literal: root Transform list_introduction:39; derived spine :34	close at bfl 7770
	postfix chain: projections at node_query 374; spine at bfl 4947/5004	close at the chain's final node
Rootless images (fixed in PR2, each with its own control)	(1) bfl 3376: declared_signature(source: type_expr) stands for no node	use source: shell
	(2) postfix chains ending in a call or cast, where the outer node is synthetic	name the root explicitly
	(3) lower_list_introduction called alone	close at the literal

Consumers moved in PR2, in the same motion as the producers:

• reference_conservation: follows caused_by to the authored source instead of reading Absent, which would otherwise flood false DroppedReference results. Its DISSOLUTION note is retired.
• occurrence_role: counts Projected as derived, not unminted.
• 02_parse and identity_captured_navigation: reviewed arm by arm.
• The census: must reach 0 collisions.

PR2 receipts:

• A floor claim over a real multi-construct module showing no duplicate minted ids.
• The eager-newt-412 census reaching 0 over the observed set.
• The XL-2: sequence-operand refs reach resolve — operator expressions lower whole, a sequence operand is never narrowed #12145 conservation control set unchanged.
• Seed base-vs-head showing no true→false.

PR3 plan (separate from PR2; model-first)

Goal: one parse per file per ingest. Its control goes RED on a second parse. There is no v1 patch: v1 keeps the double parse until the v2 front end replaces it on the floor path.

PR3 is owned by bold-fox-455 and starts after PR2 lands. It begins with a chain re-derivation (DESIGN §6b): can the reference reading consume the compile's graph-scoped parse, or does closure discovery truly need a parse before the graph scope exists? The answer goes to gentle-koi-724 before any model PR. Consumers: the facts occurrence key (quiet-gull-780), 02_parse, program_assembly. The re-derivation picks one of:

1. Reuse the graph-scoped parse. The reference reading that decides the closure consumes the same parse that compile carries. This involves no identity change, keeps occurrence_identity_scope_law as it is, and keeps the key shape unchanged. Preferred if it holds.
2. Per-file source-local ids. Only if (1) cannot hold. This amends occurrence_identity_scope_law first: per-file scope, snapshot and N, plus cross-file assignment at the closure fold. Every authored and derived id is re-keyed. It changes the key shape, so quiet-gull-780 is told before the front end moves (eager-newt-412's facts occurrence key consumes it). The derivation N + cantor(source, k) still holds, with one snapshot per file.

PR2 introduces no source-local ids, so PR3 does not depend on any.

Do not merge: neat-boar-16 enqueues.

🤖 Generated with Claude Code

[gunbai-bot]

Addressing review 72543 (/api/reviews/72543/artifacts/stdout.log). Both findings were verified against the code, and both are fixed in this push.

1. Meaning fork on OccurrenceProjected: fixed by reconciling the arm's contract, not by adding an arm.
A fourth arm was ruled out earlier (GAP-1 in the model review): every total match would change, and the two cases do not differ in shape. They differ in where the cause's scope lies.

• Carrier doc. std.occurrence_identity now states the arm's contract: "a real occurrence of the containing graph that has a cause and no author". It names both producers.
  • A projector insertion has its cause in a foreign allocator domain.
  • A same-graph lowering member has its cause in its own graph's domain, with a derived id.
  • scoped_occurrence_ref_in_scope(caused_by, <containing scope>) is the single test that tells them apart.
• Consumer. v2.workflow.legacy_binding_delta insertion_provenance_entry now returns NotAnInsertion for a same-scope cause. Only a foreign-scope cause becomes ProjectedAsInsertion.
• Control. The new lbd_same_scope_projected_member_is_not_an_insertion_holds is paired with the existing insertion witness, which uses a base-scope cause.

2. Collision argument depended on an unenforced allocator invariant: fixed with a seal.

• The seal. occurrence_allocator_seal(alloc, scope) returns the snapshot together with a continuation allocator, already advanced past [N, N + occurrence_derived_span()). Any allocation after the seal comes from the continuation.
• The comment. It states the rung honestly as mitigatable: an allocator is an immutable value, so a caller can still reuse the pre-seal one. It also says the snapshot record remains writable, as every .dag record is.
• Control. image_projection_seal_continuation_allocates_above_every_derived_id_holds: the first post-seal id exceeds the largest derivable id.

Evidence. I ran these locally, not in CI, using gunbc run built from this tree over a scratch driver that ANDs 11 claims: the 9 image-projection claims plus 2 delta claims.

• The unmutated tree held (rc=0).
• A seal that returns the unadvanced allocator failed (rc=1), naming the seal control.
• A delta without the scope branch failed (rc=1), naming the same-scope control.

This push also regenerates the stage0 mirror std_occurrence_identity.rs (the generated failure on 86156a4).

— sent from bold-fox-455

[gunbai-bot]

Re review 72565's open question on the cost of list_snoc_item inside project_image_edges: I checked, and it is not quadratic. std.algebra list_snoc_item is xs |> list_push(item), and the realization (v1_rt list_push) takes the vector by value (mut list: Vec<T>) and pushes onto it. Since the fold moves its accumulator, each append is amortized O(1) and the pass is linear in the image. That is also why I chose it over the concat accumulator in the first draft; concat copies. No code change.

— sent from bold-fox-455