Repository navigation

Explicit capability changes: action deltas, freezes, two-phase activation, joins as reached meets - #190

Draft

JonasAlaif wants to merge 15 commits into

mainfrom

two-phase-reservation

Draft

Explicit capability changes: action deltas, freezes, two-phase activation, joins as reached meets#190
JonasAlaif wants to merge 15 commits into
mainfrom
two-phase-reservation

Commits on Nov 12, 2026
- Freeze places for shared and two-phase borrows; explicit activation
  JonasAlaif
  committed
  3a58f2b
- Freeze before read unpackings; Refreeze instead of the upward walk
  JonasAlaif
  committed
  867c34f
- Fold Restore into RemoveEdge
  JonasAlaif
  committed
  fac07ec
- Record the capability effects of an added edge in AddEdge
  JonasAlaif
  committed
  809e8e9
- Make capability changes at joins explicit
  JonasAlaif
  committed
  0abfdcf
- Unpack places at joins to match the other path
  JonasAlaif
  committed
  60aeea6
- Detach raw pointer dereferences from dead pointers
  JonasAlaif
  committed
  6bf9fe8
- Detach borrowed shared referents to pack read unpackings
  JonasAlaif
  committed
  28b8a73
- Make every capability change an explicit, recorded action delta
  JonasAlaif
  committed
  26ebec3
- Join by reaching the joined state with the obtain machinery
  JonasAlaif
  committed
  ada9f24
- Record what loans and freezes take; give back exactly that
  JonasAlaif
  committed
  4b981ff
- Lend a referent through its reference at a join
  JonasAlaif
  committed
  58c50bd
- Join records like capabilities; give them back along the layout
  JonasAlaif
  committed
  f9dae19
- Freeze or lend at the loop head what its loans block
  JonasAlaif
  committed
  01455e5
Commits on Nov 13, 2026
- Keep a packed enum frozen on its borrowed variant
  JonasAlaif
  committed
  f8c3608