[JonasAlaif]

Capabilities change only through explicit actions, and every action records the capability changes it makes. Reading never weakens E: the place is frozen (the E is suspended) and comes back on the same place. A loan records what it takes and gives back exactly that. Joins are the meet of their predecessors, reached with the same explicit actions, for capabilities and for what is recorded.

Actions

Every PcgAction (borrow and owned) carries capabilities: the changes its rule computes when it is applied, stored in the action. Consumers can read every capability change off the actions.

Action	Effect
Weaken { place, from, to }	Strictly lowers a capability to a real one (E/e → W, E → e). The only weaken: RepackOp::Weaken, RepackOp::IgnoreStorageDead, RegainLoanedCapability and weakens to None are removed.
Freeze { place }	E/e → R. Nothing is given up. An unpacked place takes over the R of its descendants, which become read copies under it.
Unfreeze { place, refrozen }	R → the suspended E, once no borrow of place is left. With refrozen non-empty, those still-borrowed descendants stay frozen and the rest of the unpacking gets E (formerly Refreeze).
ActivateTwoPhaseBorrow { borrow }	The reserved place goes R → lent.
AddEdge / RemoveEdge	Carry what the edge takes and gives back (Add Edge {p} -> {*p} setting p: e, *p: E, Remove Edge borrow: r = &mut x returning E to x). RemoveEdge is applied once; replaces Restore.
Lend { place, edge }	At a join: place is lent to an edge that exists only on another path (a conditional loan, a variant unpacking, a loop abstraction), or to a loan of this path that still blocks it. What it holds is recorded and comes back with the edge's RemoveEdge; a frozen place keeps its record and lends its read copies with it.
UnpackSuspended { place, parts } / PackSuspended { place }	Move a record one level, as a capability would be unpacked or packed: parts get the same, the referent of a mutable reference E with the reference keeping e; a part that records less keeps that. Used at joins and when a loan ends.
WeakenSuspended { place, from, to }	Lowers (or drops) a record: at a join to the meet of the paths, at a loop head to W.
LabelPlace { reason }	States the capabilities it removes. Detach (formerly DetachSharedReferent) gives up the value of a place at a join.
RepackOp::StorageDead	Applied: removes the local's capabilities.

A place with R whose parent has R is a read copy of a frozen ancestor; a place with R whose parent has no R is frozen. There are no R → W or W → W weakens: a dead frozen place is unfrozen first.

Records

PlaceCapabilities keeps, per lent or frozen place, the capability it gets back (its record): AddEdge of a mutable borrow, Freeze and Lend record what they take, and RemoveEdge/Unfreeze give back exactly that.

• Invariant. A lent place, its parts, and the places it is part of (short of a reference to it) hold at most R while the loan lives; the validity check enforces it. Unfreezes skip places within a lent place, and the lazy unfreeze of leaves runs after the dead edges are removed.
• When a loan ends, each record holder in the value of what it blocked comes back once no loan blocks its value. Its record is unpacked along its layout (owned expansions, borrow-PCG expansions, the referent of a reference), entering an enum variant or one of several unpackings only where a remaining loan needs it (the others, holding nothing, are forgotten), and the places that then record something get it back. While only shared borrows block it, it comes back frozen (R, record kept); while a mutable loan does, nothing comes back. Removing an unpacking whose parts record something first packs those records into the base.
• At a join, records are joined like capabilities: at the finest places every path records or covers (including the enum above diverging variants), the meet of what each path has, reached with UnpackSuspended / PackSuspended / WeakenSuspended. The owned layout that another path has below places nobody holds is added (it changes no capability).

Joins

The joined state holds the meet of the predecessors' capabilities: for each place, the capability each path has or gets by unpacking (through derefs), lowered to the smaller one. R and e meet at e (a reference read on one path and with its referent lent on the other keeps its value); other incomparable pairs meet at W. Where one path holds the place frozen and a loan of either path blocks it or an ancestor, an e or W meet is none instead: the loan keeps the place frozen. Where the paths unpack different variants of an enum, the join holds the enum packed. E and W entries swallow their postfixes.

Each predecessor reaches the joined state with explicit actions, computed by one procedure (Pcg::reach in src/pcg/domain/join.rs) that reuses the obtain machinery, in order:

1. StorageDead of locals the other path does not have;
2. move capabilities (freeze, unfreeze, weaken; a place the target unpacks exclusively is unfrozen, one whose parts the target only reads has its freeze moved to them, a place read in the target is frozen);
3. unpack to the joined layout (into a loop head, as the loop invariant unpacks);
4. pack what the joined state holds packed;
5. give up the places the joined state does not hold: lend each, with what it holds, to the edge of the other path that blocks it or an ancestor; else to the loan of this path that blocks it, an ancestor, or another part of the value the join gives up; lend the place itself for an unmatched variant, or unpack toward a part the other path lent (moving a freeze to the read copies); otherwise detach its value with a label.

The dataflow join (meet, then every predecessor reaches it) and the actions on CFG edges (Pcg::bridge) both use it; a lent or added edge drops this path's branch choice. An expansion that a path rebuilds to match the other path keeps that path's guide, so a labelled index guide (#187) keeps its label (expand_to takes the other path's graph as template). The loop head's abstraction edges are added on the bridge where the reached state lacks them.

Loop heads are computed from the entry edge only, so finish_join weakens to W, with recorded obtain and Weaken actions, what a back edge may bring back weakened: every owned place that is not definitely initialized there, and (on main, because of the dead-lifetime weakens of #147) the local references held E or e that are dead there.

Loop heads (from #198)

At a loop head, the capabilities are what the loans of the head's graph leave. For each place in a place that a loan edge lends, or above one (short of a reference to it), looking at the mutable borrows in scope at the head that conflict with it:

• if one covers it (borrows it or a place it is part of), it holds nothing;
• if one takes a part of it, it keeps the R of a read unpacking, and holds nothing if it holds more;
• otherwise it holds at most R.

A two-phase borrow counts as mutable only once activated (its activation dominates the head or lies in the loop). Each lowered place records what it held, so the comeback returns it when the loan ends inside the loop. The head does not unpack enum variants: not every path into the loop matched them. A root of the loop's blockers is lent to the abstraction only if a loan borrows the root or a place it is part of (BorrowCheckerInterface::blocks_entirely): for .. in self.chars.by_ref() in bstr's FieldsWith::next lent all of *self. This replaces the abstraction's capability_updates, which capped only the used places a loan borrows directly, by the loop's own usage: a = &x before a loop that writes x.g after a = &z left x.g: E while Loop(bb1): x -> a lent x.

Frozen enums with a borrowed variant field

A join of a path that borrows a variant field (if let A(ref p, _) = x { a = p }) with one that did not match the variant holds x frozen and packed; the borrowing path keeps the layout x -> x@A -> {0, 1} below it, without read copies. The other path gets that layout too (a frozen place may have layout below it). Ending the freeze of x to borrow another variant mutably (allowed: rustc keeps variants apart under shared loans) or another field of the variant unpacks toward the obtained place and, at each place on the way, one level into the other unpackings that hold a borrowed place; the freeze moves to the topmost read copies that are borrowed or have a borrowed place in their value that their unpacking does not reach:

if let AC::A(ref p, _) = x { a = p; }
if let AC::C(ref mut q) = x { *q = 1; }   // bb6[1]: unpack x@C with capability R
                                          //         Refreeze x to x@A

Before, x was unfrozen whole while p lived (or the join failed: "the join unpacks x, which holds a capability"). The lazy unfreeze of a place also waits for every loan in its value, and the read collapse leaves alone places that hold nothing below a place that holds a capability.

This replaces the owned join (owned_pcg/impl/local/join.rs, owned_pcg/impl/join/*), the separate unpacking/lending/weakening passes of join_owned, the loop-entry upgrade and expansion passes, the abstraction-edge pass of the results cursor, PlaceCapabilities::join, and the silent meet when merging predecessors (now a validity check that they agree).

Other fixes the explicit changes exposed:

• the imaginary target of a false edge gets no edge actions;
• a shared borrow of a reference whose referent is reserved (e) freezes it;
• a place still blocked through a raw pointer is not reported unblocked; raw pointer dereferences are unpackings, not loans;
• activating a two-phase borrow detaches the read copies that dead loans keep from being packed;
• a lent place that was partly moved on one path regains W for the moved part and E for the rest;
• an owned place weakened to W is uninitialised in the initialisation tree;
• the Polonius liveness check no longer tests origin liveness inside the loop over loans;
• the parts of a place under a live borrow stay frozen, and an unpacked place regains nothing itself when its borrow ends;
• labelling one end of a borrow flow edge into the other collapses it.

Diff

Rebased onto main (now including #191, #192, #195, #196). #192's cut of delegation edges uses the new Weaken; 174_linked_hashmap_refresh stays removed as on main. With #192 the loan taken by mem::take in 219 ends before the two-phase activation, so that activation no longer detaches anything (annotation updated).

Tests

On main (this branch) and on the pin base e90a814 (branch two-phase-reservation-e90a814, used by Prusti): the annotation check of every test-files file with PCG_VALIDITY_CHECKS, cargo test --lib, pcg-tests (incl. selected_crates), clippy and fmt. Every commit builds.

New cases: 211 (partly moved vs lent whole; borrowed whole vs in part; and for records: frozen vs lent whole, whole vs part or every part lent, nested structs, reference fields whose referent is lent, enum variant fields per arm, shared and mutable fields of one variant, moved variant fields, arrays unpacked at different indices, borrowed *x with the part's loan ending first; a variant field borrowed on one path, then another variant or field borrowed mutably, or the enum read whole), 229 (variant lend), 230 (lend without the branch choice), 237 (moved in a loop, frozen or lent on entry), 239 (raw pointer deref), 240 (main: dead self across nested loops; the loop-head cases of #198, including bstr's FieldsWith::next and a serde_derive-shaped nested loop). main's 245 and 246 (deferred dead-lifetime weakens) pass unchanged.

Annotation changes on main from the loop-head rule: in 091, 116, 132, 192 a reference that is dead at a loop head while its referent is lent is labelled at the head (*y loop bb1, b_in: W). In 240 (consume, consume_after_branch) and 241, the head no longer unpacks list.tail to Some, so the sibling fields connect to their remote through the whole list↓'r projection (still only to their own remote).

Four rounds of independent review on the explicit actions and the join, then five on the records (each finding confirmed with a probe and fixed; several also failed on the previous head).

Follow-ups

• A loop that borrows a variant field across the back edge and another variant mutably in the body (match x { A(ref p, _) => a = p, B(ref mut q) => *q += 1 }) fails the validity check: the head's abstraction lends the enum whole, so the body's mutable borrow of x@B.0 unfreezes x while it is lent. The head should block the variant field itself, with x frozen and packed and the variant's layout below it, as the join now does.
• Which RemoveEdge carries returning depends on the order dead edges are removed in, which varies between runs.
• Obtaining through a reference that holds e gives its referent E without checking the referent's record.
• Merge owned Expand/Collapse with borrow-PCG expansions (separate PR).
• remove_edges_absent_from and pack_read_unpacking rebuild the frozen graph after every removal; not measured.

Prusti side: prusti/prusti#1609.