Split EdgeKind's Read conflation into UsePosition + UseContext (closed unmerged: verified 129/129, no consumer)

[briansrls]

Auto-opened by session-dashboard for session swift-moth-294.
Pushing to ownership-use-site-carrier advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

• TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

[gunbai-bot]

Holding this as a draft deliberately — please do not flip it to ready yet. Two independent reasons, either of which is sufficient.

1. It is a superset of #8574, which is already approved and awaiting merge.

This branch was cut from #8574's head, so it carries 13 commits of which 12 are #8574's:

94a2bba55f  Split walk_expr's use record into observed position and observed context   <- the only new work
00da3fc946  ... 12 commits belonging to #8574

Flipping this to ready would put twelve already-approved commits back in front of a reviewer and split review attention across two PRs holding the same content. The sequencing is: #8574 merges, then I rebase this onto main so it carries one commit.

2. The commit's new field has zero readers, and that is disqualifying on its own.

The change splits walk_expr's use record into two orthogonal observed facts — position (Tail/NonTail, propagates) and context (the immediate syntactic parent, never propagated). Measured on the branch: 34 writes of context:, 0 reads.

That is DESIGN §6's "new artifact with no final consumer." The position half is consumed (it replaces the in_tail test via edge_kind_for_position); the context half is written everywhere and read nowhere. It lands together with the per-use-site move-evidence derivation that reads it, or it does not land.

What the commit is for, since that context is not obvious from the diff alone: Read was the else-branch of a tail test. in_tail is true only at the function-body root and ExprReturn children, so call arguments never receive it, and f(x), S { a: x } and vec![x] all recorded Read while consuming by value — indistinguishable from xs.len(), which genuinely borrows. Read was therefore ignorance wearing the name of a finding, and a proposed third emitter arm keyed on it would have emitted a borrow where an owned value is required. The existing .clone() is not a missing arm; it is the sound answer given a signal that cannot tell borrow from move.

Verification already executed, for whoever picks this up: generation 1 proves nothing here, because a change inside the compiler can only show its own mirror drifting. The oracle is generation 2 — install, rebuild so the compiler contains the new walk, regen again:

required-regen: first_generation_equal=true planned=129 executed=129   EXIT=0

All 129 modules re-emit byte-identically, so the change is behaviour-preserving by execution rather than by argument. It can fail — any third drifting file would falsify it. Binary freshness was proved by content on both sides (new ForEachCollectionUse present, prior build's UnclassifiedPosition absent), which a stale artifact cannot satisfy.

Note the byte oracle's blind spot, since it bears on reviewing the next increment: it cannot see a meaningless field. An earlier version of this commit merged both facts into one carrier, so propagating tail-ness dragged the grandparent's context along — y in f(match x { A => y, B => z }) recorded a call-argument context it does not have — and that version was equally byte-identical. That defect was caught by reading, not by the gate.

— sent from swift-moth-294

[gunbai-bot]

Correcting my earlier comment on this PR: it now carries TWO new commits, not one. My first comment said "13 commits of which 12 are #8574's" and named 94a2bba55f as the only new work. That was true when written and is false now — a second commit landed on this branch and the head moved. Recording it here rather than editing the earlier comment, so the sequence stays readable.

3af7a6dc06  Derive PartialEq bounds on generic fn params from body equality use   <- NEW, independently landable
94a2bba55f  Split walk_expr's use record into observed position and observed context
00da3fc946  ... 12 commits belonging to #8574

The two have opposite readiness, which is exactly why they must not be reviewed as one PR:

commit	state
94a2bba55f ownership carrier	blocked indefinitely — 34 writes of the new context field, 0 reads. A carrier nothing reads has no final consumer, so it cannot land until the per-use-site derivation that reads it lands with it. That derivation is deprioritized.
3af7a6dc06 equality trigger	complete and verified — has consumers, an enrolled witness, and both arms measured on real emission.

These get split. The equality trigger will move to its own PR once the mirror queue ahead of it clears (#8693, then #8691 — that one's regen surface is corpus-wide at ~50 mirrors against my 3, so it goes first and I rebase onto it). This PR keeps the ownership carrier and stays draft.

Why the equality commit is landable on its own, since that is the part a reader would otherwise have to reconstruct from the diff: the emitter derived Clone bounds on generic fn params but derived nothing for equality, so a generic fn comparing two values of its own type param emitted bare and rustc refused it with error[E0369]: binary operation == cannot be applied to type K. Two existing body-reading Clone triggers each declare a depth boundary and both name the same next-rung trigger in the same words — a recursive body walker — so this builds that walker rather than adding a fourth shallow body-reading path beside two already-declared-incomplete ones.

Both arms measured on real emission, same fixture shape, differing only in what the == compares:

positive   row.shape == shape && (row.keys |> any(k => k == key))
        ->  pub fn cap_row_has<K: Clone + PartialEq>(...)

negative   row.shape == shape
        ->  pub fn cap_row_shape_is<K: Clone>(...)

The negative arm is the discriminating one: a generic param is present and a == is present, and it must still earn nothing. A predicate keyed on the operator spelling emits K: Clone + PartialEq there and breaks every caller instantiating K with a non-PartialEq type. Over-approximation is not free in this direction — adding a bound tightens the emitted signature — which is why precision lives in operand type resolution rather than in the shape of the walk.

The expected spelling is externally grounded rather than copied from this tree: another session measured it against rustc on the real emission, hand-adding the bound to the emitted mirror and rebuilding the seed to zero errors, and reported K: Clone + PartialEq — the equality bound composing with the separately derived Clone bound. Clone survives in both arms above.

Corpus safety, with the trigger live: required-regen: first_generation_equal=true planned=129 executed=129. All 129 modules re-emit byte-identically, so it fires nowhere in existing code and adds no spurious bound. That zero also means the corpus supplies no positive evidence, which is why the enrolled witness is a controlled fixture authoring both comparisons itself rather than a pin to a live population.

— sent from swift-moth-294

[gunbai-bot]

CI failure diagnosed: it is not a defect in any commit here, and this PR cannot go green as constituted. Recording the cause and the remedy.

The failing phase is receipt, not regen and not the floor. The floor itself passed completely:

required-floor: planned=9852 executed=9852 terminal=9852 passed=9545
                known_red_held=206 failed=0 stale_quarantine=0
required-ci: phases_run=6 failed=1
required-ci: FAILED PHASE receipt

The receipt phase refused on breadth:

behavioral-receipt: REFUSED — 6 authority modules selected, above the declared cap of 3.
Not sampling the first 3: a partial check reported as a pass is how a gate stops covering
things without anyone finding out.
Selected: extdeps.languages.rust.derive_contracts, extdeps.languages.rust.emit,
v1.compiler.emit_rust, v1.compiler.ownership, v1.compiler.trait_bound_witness,
v1.compiler.trait_derive_emit

Six changed authorities because this branch carries three separate pieces of work at once — #8574's twelve commits, the ownership carrier, and the equality trigger. That is exactly the superset problem documented in the two comments above, now enforced by a gate rather than only by argument.

The remedy is the split, and the gate names it. From claim_executor.rs at the cap:

"Until then a four-authority PR is genuinely more than this gate can check, and saying so is the honest answer rather than checking three of four and printing a pass. A PR that legitimately needs more splits, or the operator raises the number here."

So: split. Raising the cap is an operator decision and not mine to take — and a diff that defeats a fail-closed refusal is a hard reject under §5 regardless of what else it delivers. This is a well-built gate: it declines to sample-and-report-pass, and its dissolution condition is stated (it exists because the differential rebuilds the whole crate per candidate; it is raised, not removed, when per-module compilation makes cost linear in the changed surface).

Verified the split is viable rather than assumed. The equality commit's source diff applies cleanly to current main with no conflicts, confirming it does not depend on #8574. Split apart, each piece is under the cap:

PR	changed authorities
equality trigger (new branch off main)	v1.compiler.emit_rust, v1.compiler.trait_bound_witness, v1.compiler.trait_derive_emit — 3, exactly at the cap
this PR, ownership only, once #8574 merges	v1.compiler.ownership (+v1.compiler.emit_rust for two dead re-export lines) — 2
#8574	its own, already open

So no fix is pushed to this branch. The equality work moves to its own PR; this one keeps the ownership carrier and stays draft until #8574 merges and it can be rebased to carry one commit. The ownership carrier remains blocked on its missing consumer independently of all this — 34 writes, 0 reads.

One thing worth noting for anyone reading the run: the receipt phase's self-test passed immediately before the refusal — receipt-selftest OK both arms discriminate, with the divergent arm correctly catching band_of(100i64) = High vs Mid. The mechanism works; it refused on scope, not on a behavioural disagreement.

— sent from swift-moth-294

[gunbai-bot]

Closing this unmerged, deliberately, with the finding landed first

Ruling: smart-ram-730, who prioritized this lane, reversed that prioritization. The deciding fact is that the consumer this was built for does not exist.

Why it is being closed rather than finished

The carrier is complete and verified. It splits a real state-space conflation in EdgeKind into two orthogonal axes — UsePosition (tail / non-tail) and UseContext (the syntactic role) — threaded through walk_expr and record_use, and it is behaviour-preserving at gen-2 first_generation_equal=true, 129/129.

It also writes context at 34 sites and nothing reads it. That is the DESIGN.md §6 experimental-residue tell, and the reviewer's test in that section — will this survive the terminal architecture substantially unchanged, and be consumed by it — answers no on the second half.

I built it expecting the iter_owned clone-drop decision to be its consumer. It is not, and the reason is better than my design was: that lane proves borrow-safety from the syntactic position of the receiver as an iter_owned argument. That is a local proof — it needs no ownership classification at all, and it is sound precisely where a disposition keyed on Read would not be, because Read fires in genuine by-value-consuming positions too.

So this is not a lane declining to use the carrier. It is a lane that found a proof which does not need one. Manufacturing a plausible consumer to keep verified code alive would be exactly the failure §6 warns about, and neither smart-ram nor I could name a real one after looking.

The finding is landed, which was the condition

I claimed this finding was "already durable" and that was false — I asserted a property of the repository without measuring it. Grepping docs/, src/v1/*.dag and dag/ found no record. It existed only in session memory no one else can read and in message history nobody would search.

It now lives on the carrier itself, as a leading annotation above type EdgeKind in src/v1/ownership.dag: #8710. That annotation records the conflation, the refuted borrow arm and why it fails, where the sound alternative lives, and this PR number as a quarry pointer — so the next person to want the distinction finds it already built and verified instead of rebuilding it blind.

That last part is the whole point of closing this way. A deletion that hides prior art from the person who next needs it is worse than the draft staying open.

What survives, precisely

• The root: Read is the else of in_tail. It conflates provably non-consuming with never classified. Consumed is a deliberate wall, not an oversight.
• The refutation: an arm emitting a borrow wherever Read appears is unsound. Recorded at the declaration, where it would be proposed again.
• The code: quarry in this PR's commits. Two enum declarations and two threaded parameters — cheap to rebuild when a consumer exists, and landed together with it.

Not deleted, not lost, and not pretending to be finished.