feat: model interior borrows for refcell

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -443,13 +443,162 @@ This does not sacrifice unsoundness as we would not eliminate any assertion fail
 Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreachable`.
 Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error.
 
+#### Drop Terminator
+
+The `Drop` terminator traverses the target place, materialises its value and type information, and then resumes execution at the successor block once the type-directed drop handler has run.
+
+#### Borrow-Aware Drops
+
+Our runtime model tracks RefCell borrow counts for smart-pointer types. Dropping `RefMut<T>` releases the unique borrow by incrementing the cell, while dropping `Ref<T>` decrements the shared borrow count. The helper rules below normalise pointer shapes and apply those updates across the stack.
+
+- Detect `RefMut<T>` / `Ref<T>` via `#isRefMutTy` and `#isRefTy`, which presently match the canonical names that contain `"RefMut<"` or `"Ref<"`.
+- Extract projection data so that borrow cells can be reached regardless of pointer shape or stack depth.
+- Update the borrow cell using `#incCellBorrow` for mutable borrows and `#decCellBorrow` for shared borrows; the cell is represented as a signed 64-bit integer (`rt/data.md`).
+- The model does not assert that the borrow cell currently equals `-1`; repeated drops therefore leave the configuration unchanged.
+
 ```k
-  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
+  // TODO: support general drops (not specifically Ref/RefMut)
+  rule [termDrop]:
+       <k> #execTerminator(terminator(terminatorKindDrop(place(local(I), PROJS), TARGET, _UNWIND), _SPAN))
          =>
-           #execBlockIdx(TARGET)
+           #applyDrop(
+             operandMove(place(local(I), PROJS)),
+             getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)
+           ) ~> #execBlockIdx(TARGET)
         ...
        </k>
+       <locals> LOCALS </locals>
+    requires 0 <=Int I
+     andBool I <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness] // valid local index checked
+
+  syntax KItem ::= #applyDrop ( Evaluation , MaybeTy ) [strict(1)]
+  // std::cell::Ref/RefMut aggregates carry the BorrowRef helper (independent of `T`) in slot 1;
+  rule <k> #applyDrop(Aggregate(_, ARGS), MTY)
+        => #releaseBorrowRef(getValue(ARGS, 1), #isRefMutTy(#lookupMaybeTy(MTY)))
+       ...
+       </k>
+    requires 1 <Int size(ARGS)
+     andBool (#isRefMutTy(#lookupMaybeTy(MTY)) orBool #isRefTy(#lookupMaybeTy(MTY)))
+  rule <k> #applyDrop(_:Value, MTY) => .K ... </k>
+    requires notBool #isRefMutTy(#lookupMaybeTy(MTY))
+     andBool notBool #isRefTy(#lookupMaybeTy(MTY))
+
+  syntax Bool ::= #isRefMutTy ( TypeInfo ) [function, total]
+  rule #isRefMutTy(typeInfoStructType(NAME:String, _, _, _))
+    => findString(NAME, "RefMut<", 0) =/=Int -1
+  rule #isRefMutTy(_) => false [owise]
+
+  syntax Bool ::= #isRefTy ( TypeInfo ) [function, total]
+  rule #isRefTy(typeInfoStructType(NAME:String, _, _, _))
+    => findString(NAME, "Ref<", 0) =/=Int -1
+     andBool findString(NAME, "RefMut<", 0) ==Int -1
+  rule #isRefTy(_) => false [owise]
+
+  // Helper to release borrow reference; Bool indicates mutability
+  syntax KItem ::= #releaseBorrowRef(Value, Bool)
+
+  // Strip tuple/struct wrappers so the borrow cell pointer can be normalised.
+  rule #releaseBorrowRef(Aggregate(_, ListItem(PTR) _), IS_MUT)
+    => #releaseBorrowRef(PTR, IS_MUT)
+
+  // Turn References into PtrLocal so projection traversal can reach the borrow cell.
+  rule #releaseBorrowRef(Reference(OFFSET, PLACE, MUT, META), IS_MUT)
+    => #releaseBorrowRef(PtrLocal(OFFSET, PLACE, MUT, META), IS_MUT)
+
+  // Stack height 0: borrow cell lives in the current frame, adjust projections (respecting pointer metadata).
+  rule <k> #releaseBorrowRef(PtrLocal(0, place(local(J), PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE)), IS_MUT)
+        =>
+          #traverseProjection(
+            toLocal(J),
+            getValue(LOCALS, J),
+            #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE),
+            .Contexts
+          )
+          ~> #readProjection(false)
+          ~> #applyBorrowCellLocal(J, #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE), IS_MUT)
+       ...
+       </k>
+       <locals> LOCALS </locals>
+    requires 0 <=Int J
+     andBool J <Int size(LOCALS)
+     andBool isTypedValue(LOCALS[J])
+    [preserves-definedness]
+
+  // Non-zero stack height: borrow cell resides in an ancestor frame, so traverse via `toStack`.
+  rule <k> #releaseBorrowRef(PtrLocal(OFFSET, place(local(J), PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE)), IS_MUT)
+        =>
+          #traverseProjection(
+            toStack(OFFSET, local(J)),
+            #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
+            #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE),
+            .Contexts
+          )
+          ~> #readProjection(false)
+          ~> #applyBorrowCellStack(OFFSET, J, #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE), IS_MUT)
+       ...
+       </k>
+       <stack> STACK </stack>
+    requires 0 <Int OFFSET
+     andBool OFFSET <=Int size(STACK)
+     andBool isStackFrame(STACK[OFFSET -Int 1])
+    [preserves-definedness]
+
+  // If the value shape does not match the std Ref/RefMut layout (e.g. custom wrappers), bail out without touching memory.
+  rule #releaseBorrowRef(_, _) => .K [owise]
+
+  syntax ProjectionElems ::= #withPointerOffset(ProjectionElems, Int, MetadataSize) [function, total]
+  rule #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE)
+       => appendP(PROJS, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE)))
+    requires PTR_OFFSET =/=Int 0
+  rule #withPointerOffset(PROJS, _PTR_OFFSET, _ORIGIN_SIZE) => PROJS [owise]
+
+  syntax KItem ::= #applyBorrowCellLocal(Int, ProjectionElems, Bool)
+                 | #applyBorrowCellStack(Int, Int, ProjectionElems, Bool)
+
+  // Write the adjusted borrow count back into the current frame's cell.
+  rule <k> CELL:Value ~> #applyBorrowCellLocal(J, PROJS, IS_MUT)
+        =>
+          #setLocalValue(
+            place(local(J), PROJS),
+            #if IS_MUT
+             #then #incCellBorrow(CELL)
+             #else #decCellBorrow(CELL)
+             #fi
+          )
+       ...
+       </k>
+  rule #applyBorrowCellLocal(_, _, _) => .K [owise]
 
+  // Same as above, but for borrow cells located in ancestor stack frames.
+  rule <k> CELL:Value ~> #applyBorrowCellStack(OFFSET, J, PROJS, IS_MUT)
+        =>
+          #traverseProjection(
+            toStack(OFFSET, local(J)),
+            #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
+            PROJS,
+            .Contexts
+          )
+          ~> #writeProjection(
+               #if IS_MUT
+                #then #incCellBorrow(CELL)
+                #else #decCellBorrow(CELL)
+                #fi
+             )
+       ...
+       </k>
+       <stack> STACK </stack>
+    requires 0 <Int OFFSET
+     andBool OFFSET <=Int size(STACK)
+     andBool isStackFrame(STACK[OFFSET -Int 1])
+    [preserves-definedness]
+  rule #applyBorrowCellStack(_, _, _, _) => .K [owise]
+```
+
+#### Unreachable Terminator
+
+```k
   syntax MIRError ::= "ReachedUnreachable"
 
   rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))