feat(rt): handle zero-sized locals

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

@@ -172,7 +172,7 @@ A variant `#forceSetLocal` is provided for setting the local value without check
 
 ```k
   syntax KItem ::= #setLocalValue( Place, Evaluation ) [strict(2)]
-                 | #forceSetLocal ( Local , Value )
+                 | #forceSetLocal ( Local , Evaluation ) [strict(2)]
 
   rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>
        <locals>
@@ -203,7 +203,7 @@ A variant `#forceSetLocal` is provided for setting the local value without check
      andBool isTypedValue(LOCALS[I])
     [preserves-definedness] // valid list indexing and sort checked
 
-  rule <k> #forceSetLocal(local(I), MBVAL) => .K ... </k>
+  rule <k> #forceSetLocal(local(I), MBVAL:Value) => .K ... </k>
        <locals> LOCALS => LOCALS[I <- typedValue(MBVAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityOf(getLocal(LOCALS, I)))] </locals>
     requires 0 <=Int I andBool I <Int size(LOCALS)
      andBool isTypedLocal(LOCALS[I])
@@ -1064,6 +1064,25 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
   // rule #projectionsFor(CtxPointerOffset(OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(OFFSET, ORIGIN_LENGTH, false) PROJS)
   rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS)
 
+  // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule.
+  rule <k> rvalueRef(REGION, KIND, place(local(I), PROJS))
+        => #forceSetLocal(
+              local(I),
+              #decodeConstant(
+                constantKindZeroSized,
+                tyOfLocal(getLocal(LOCALS, I)),
+                lookupTy(tyOfLocal(getLocal(LOCALS, I)))
+              )
+            )
+        ~> rvalueRef(REGION, KIND, place(local(I), PROJS))
+       ...
+       </k>
+       <locals> LOCALS </locals>
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isNewLocal(LOCALS[I])
+     andBool #zeroSizedType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
+    [preserves-definedness] // valid list indexing checked, zero-sized locals materialise trivially
+
   rule <k> rvalueRef(_REGION, KIND, place(local(I), PROJS))
         => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
         ~> #forRef(#mutabilityOf(KIND), metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO: Sus on this rule

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

@@ -143,6 +143,21 @@ Slices, `str`s  and dynamic types require it, and any `Ty` that `is_sized` does
     [preserves-definedness]
 ```
 
+## Zero-sized types
+
+```k
+  syntax Bool ::= #zeroSizedType ( TypeInfo ) [function, total]
+
+  rule #zeroSizedType(typeInfoTupleType(.Tys)) => true
+  rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true
+  rule #zeroSizedType(typeInfoVoidType) => true
+  // FIXME: Only unit tuples, empty structs, and void are recognized here; other
+  // zero-sized types (e.g. single-variant enums, function or closure items,
+  // newtype wrappers around ZSTs) still fall through because we do not consult
+  // the layout metadata yet. Update once we rely on machineSize(0).
+  rule #zeroSizedType(_) => false [owise]
+```
+
 ```k
 endmodule
 ```