ch:place-calculi: place and loan checking

Problem and invariant. Implement one finite diagnostic slice shared by the chapter’s examples while keeping the two source calculi separate. Maintain this invariant: moving a path invalidates exactly its prefix-overlap class, and a loan is collected only when its region occurs in neither variable types nor continuation types.

Two representations. One representation uses tries carrying availability and region entries. The companion uses a root plus a list of numeric fields, lists of qualified loans, and two explicit region-use Booleans. Tries make updates efficient; lists make prefix overlap and every collection premise inspectable.

First complete version. Implement structural isPrefix, then symmetric overlap. Define partial-move readability as non-overlap. Add qualified-loan conflict checking, continuation-aware gcLoans, and finally a strict rank-edge test. The last two cases distinguish dynamic loan release from rejection of a cyclic checker dependency.

Observable result. The accepted corpus prints seven named PASS lines and ends All 7 Chapter 48 corpus cases passed. In particular, it prints both the blocked whole value and readable sibling after one partial move.

A failing version. Replace symmetric prefix overlap by equality of the two field lists. The program remains type-correct, but a root no longer overlaps its descendant; the whole-partial-value oracle fails.

Acceptance test. Run the four commands recorded in appendix E. Require a silent check, one passing inline test, the exact eight-line run transcript, and an empty audit. Restore prefix overlap after replaying the mutation and repeat all four commands.

Mathematical boundary. The program decides a finite path and loan model. It implements neither the Featherweight Rust flow judgment nor the Oxide v4 region-rewriting and frame rules; consequently it proves no progress, preservation, safety, ownership, or termination theorem.