ch:ownership-borrowing: ch:ownership-borrowing

Problem and result. Implement the finite protocol of definition 46.2. Owned and unavailable states carry no live lifetime; shared states carry a nonempty collection of distinct lifetimes; exclusive states carry a nonempty stack whose head is the only lifetime that may end. The decidable result is seven named Boolean outcomes followed by the exact summary printed in Appendix E.

Representation. Use one datatype with constructors Owned, Dead, Shared (List Nat), and Exclusive (List Nat). The chapter’s shared state is a set, but a list makes lexical nesting executable while a membership check enforces distinctness. Exclusive lifetimes must remain a list because reclamation is last-in, first-out. Two Boolean flags cannot record nested lifetimes or distinguish inner from outer scope exit.

Represent commands by constructors for shared begin/end, exclusive begin/reborrow/end, read, write, and move. Return either Rejected or Accepted Mode; rejection is then distinct from a successful transition to Dead. The model omits payload values because its oracle concerns authority transitions only.

First complete version. Begin with the owned and dead modes and with move, read, and write. Move changes only Owned to Dead; read accepts every live mode; write accepts owned or exclusive access. A list driver applies one command at a time and stops at rejection. The use-after-move case must already reject.

Remaining cases. Add shared begin and end. Beginning from owned creates a singleton stack, nested begin pushes a fresh lifetime, and end accepts only the head. Then add exclusive begin, reborrow, and end. Reborrow pushes a fresh lifetime; end must match the head and returns ownership only after removing the last lifetime. Test the positive nested cases before the negative interference cases, then add owner reuse and the foreign-shared-lifetime rejection to expose both reclamation and handle ownership.

A failing version. Permit BeginShared from Exclusive. The program still typechecks, but the named exclusive-sharing case changes from rejection to acceptance. Removing the head comparison in EndExclusive instead makes the outer-lifetime-first case accept. Each failure identifies one lost invariant. Removing the membership comparison in EndShared makes the foreign-lifetime case accept and reproduces the missing-side-condition fault that the mathematical rule excludes.

Acceptance test. Run the four checks recorded in subsubappendix E.3.21. Require the seven PASS lines in the exercise’s order, the exact final summary, one passing inline corpus, and audit output []. Restore the accepted source after each diagnostic mutation and repeat all four checks.

Mathematical boundary. The program illustrates the transition cases used by lemma 46.4, theorem 46.5. It emits no typing derivation or runtime resource map and proves neither result. It does not implement Affe, Oxide, Pure Borrow, uniqueness typing, or the scheduler, and supplies no evidence for a Pure Borrow conjecture.