From 922dd7ee417610cab81726a224cc2839328e666b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 16:19:42 +0000 Subject: [PATCH] docs(D5.1c): add explicit revisit trigger + tracking issue for the deferred exclusivity axis MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The decline of transitive borrow_mut propagation through MOS wrapper summaries was already recorded as D5.1c, but without a concrete reactivation condition or a live tracker. Add both: the revisit trigger (land the borrow-kind axis alongside the first interprocedural exclusivity consumer — an OWN006/011/012/013-class conflict checked across the call boundary), the cheap-to-reverse rationale (the skeleton already preserves the forward edges, so the future work is additive), and a link to the tracking issue #122. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KkpSWNx7ARLpQeAs13kkyA --- docs/notes/d5-ownership-transfer.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index c4aa7f63..41336ec8 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -276,8 +276,14 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa behaviour unchanged, `$borrow_mut` wrapper tests, and mixed-path regressions proving ambiguous flows degrade to silence (not shared borrow). Prior art: Rust `&`/`&mut`, RustBelt exclusivity, Oxide's `shrd|uniq`, Polonius's per-loan invalidation — exclusivity is a distinct semantic - axis, not coarser metadata. Tracked here so the deferral is recorded, not buried (Codex P2 / - CodeRabbit Major on #113). + axis, not coarser metadata. **Revisit trigger:** land the axis alongside the first + *interprocedural exclusivity consumer* — i.e. when an OWN006/011/012/013-class conflict is + checked *across* the call boundary (today exclusivity is enforced only intraprocedurally and at + the *direct* `$borrow_mut` call). Until that reader exists the summary axis has no consumer, so + the decline costs no observable soundness and stays cheap to reverse: the forward edges are + already preserved in the skeleton (`PathAction(kind="forward", …)`), so the future work is + additive (leaf borrow-kind + a join), not a solver rebuild. Tracked here so the deferral is + recorded, not buried (Codex P2 / CodeRabbit Major on #113); live tracker: **#122**. - **D5.2 — T1 return-value door (shipped).** A `fresh`-returning call becomes an **acquire site**. `_build_skeletons` now infers the return kind (`_infer_return_skeleton`): a body that `acquire`s a local and returns it is `fresh` (a factory), and a single returned local that is