diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
index f9a956359..8cc9993ef 100644
--- a/kmir/pyproject.toml
+++ b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.151"
+version = "0.3.152"
 description = ""
 requires-python = "~=3.10"
 dependencies = [
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
index d691d4e14..6c9d75a9c 100644
--- a/kmir/src/kmir/__init__.py
+++ b/kmir/src/kmir/__init__.py
@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.151'
+VERSION: Final = '0.3.152'
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index fac0115fc..78d6fe1a5 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -329,7 +329,7 @@ In contrast to regular write operations, the value does not have to be _mutable_
 
   rule <k> VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT
         =>
-           #projectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true)
+           #projectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts) ~> #writeProjectedUpdate(Moved, true)
            ~> VAL
            ~> CONT
        </k>
@@ -400,11 +400,12 @@ The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` wi
 Write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#projectedUpdate`.
 
 ```k
-  syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, TypedLocal, Contexts , Bool )
+  syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, Contexts )
+                 | #writeProjectedUpdate ( TypedLocal , Bool )
 
   rule <k> #setLocalValue(place(local(I), PROJ), VAL)
          =>
-           #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false)
+           #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts) ~> #writeProjectedUpdate(VAL, false)
        ...
        </k>
        <locals> LOCALS </locals>
@@ -446,37 +447,31 @@ The solution is to use rewrite operations in a downward pass through the project
 
   rule <k> #projectedUpdate(
               DEST,
-              typedValue(Aggregate(IDX, ARGS), TY, MUT),
+              typedValue(Aggregate(IDX, ARGS), TY, _),
               projectionElemField(fieldIdx(I), _) PROJS,
-              UPDATE,
-              CTXTS,
-              FORCE
+              CTXTS
             ) =>
-            #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE)
+            #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, CtxField(TY, IDX, ARGS, I) CTXTS)
           ...
           </k>
     requires 0 <=Int I
      andBool I <Int size(ARGS)
      andBool isTypedLocal(ARGS[I])
-     andBool (FORCE orBool MUT ==K mutabilityMut)
      [preserves-definedness] // valid list indexing checked
 
   rule <k> #projectedUpdate(
               DEST,
-              typedValue(Range(ELEMENTS), TY, MUT),
+              typedValue(Range(ELEMENTS), TY, _),
               projectionElemIndex(local(LOCAL)) PROJS,
-              UPDATE,
-              CTXTS,
-              FORCE
+              CTXTS
            )
           =>
             #projectedUpdate(
               DEST,
               {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue,
               PROJS,
-              UPDATE,
-              CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS,
-              FORCE)
+              CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS
+            )
         ...
         </k>
         <locals> LOCALS </locals>
@@ -487,118 +482,99 @@ The solution is to use rewrite operations in a downward pass through the project
      andBool 0 <=Int #expectUsize({LOCALS[LOCAL]}:>TypedValue)
      andBool #expectUsize({LOCALS[LOCAL]}:>TypedValue) <Int size(ELEMENTS)
      andBool isTypedValue(ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)])
-     andBool (FORCE orBool MUT ==K mutabilityMut)
     [preserves-definedness] // index checked, valid Int can be read, ELEMENT indexable and writeable or forced
 
   rule <k> #projectedUpdate(
               DEST,
-              typedValue(Range(ELEMENTS), TY, MUT),
+              typedValue(Range(ELEMENTS), TY, _),
               projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS,
-              UPDATE,
-              CTXTS,
-              FORCE
+              CTXTS
            )
           =>
             #projectedUpdate(
               DEST,
               {ELEMENTS[OFFSET]}:>TypedValue,
               PROJS,
-              UPDATE,
-              CtxIndex(TY, ELEMENTS, OFFSET) CTXTS,
-              FORCE)
+              CtxIndex(TY, ELEMENTS, OFFSET) CTXTS
+            )
         ...
         </k>
     requires 0 <=Int OFFSET
      andBool OFFSET <Int size(ELEMENTS)
      andBool isTypedValue(ELEMENTS[OFFSET])
-     andBool (FORCE orBool MUT ==K mutabilityMut)
     [preserves-definedness] // ELEMENT indexable and writeable or forced
 
   rule <k> #projectedUpdate(
               DEST,
-              typedValue(Range(ELEMENTS), TY, MUT),
+              typedValue(Range(ELEMENTS), TY, _),
               projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, // from end
-              UPDATE,
-              CTXTS,
-              FORCE
+              CTXTS
            )
           =>
             #projectedUpdate(
               DEST,
               {ELEMENTS[OFFSET]}:>TypedValue,
               PROJS,
-              UPDATE,
-              CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS,
-              FORCE)
+              CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS
+            )
         ...
         </k>
     requires 0 <Int OFFSET
      andBool OFFSET <=Int MINLEN
      andBool MINLEN ==Int size(ELEMENTS) // assumed for valid MIR code
      andBool isTypedValue(ELEMENTS[MINLEN -Int OFFSET])
-     andBool (FORCE orBool MUT ==K mutabilityMut)
     [preserves-definedness] // ELEMENT indexable and writeable or forced
 
   rule <k> #projectedUpdate(
-            _DEST,
-            typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _),
-            projectionElemDeref PROJS,
-            UPDATE,
-            _CTXTS,
-            FORCE
-            )
+             _DEST,
+             typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _), _, _),
+             projectionElemDeref PROJS,
+             _CTXTS
+           )
          =>
-          #projectedUpdate(
+           #projectedUpdate(
               toStack(OFFSET, LOCAL),
               #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET),
               appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest
-              UPDATE,
-              .Contexts, // previous contexts obsolete
-              FORCE
-            )
+              .Contexts // previous contexts obsolete
+           )
         ...
         </k>
         <stack> STACK </stack>
     requires 0 <Int OFFSET
      andBool OFFSET <=Int size(STACK)
      andBool isStackFrame(STACK[OFFSET -Int 1])
-     andBool (FORCE orBool MUT ==K mutabilityMut)
     [preserves-definedness]
 
   rule <k> #projectedUpdate(
-            _DEST,
-            typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _),
-            projectionElemDeref PROJS,
-            UPDATE,
-            _CTXTS,
-            FORCE
-            )
+             _DEST,
+             typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _), _, _),
+             projectionElemDeref PROJS,
+             _CTXTS
+           )
          =>
-          #projectedUpdate(
-              toLocal(I),
-              {LOCALS[I]}:>TypedLocal,
-              appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest
-              UPDATE,
-              .Contexts, // previous contexts obsolete
-              FORCE
-            )
+           #projectedUpdate(
+             toLocal(I),
+             {LOCALS[I]}:>TypedLocal,
+             appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest
+             .Contexts // previous contexts obsolete
+           )
         ...
         </k>
         <locals> LOCALS </locals>
     requires OFFSET ==Int 0
      andBool 0 <=Int I
      andBool I <Int size(LOCALS)
-     andBool (FORCE orBool MUT ==K mutabilityMut)
     [preserves-definedness]
 
-  rule <k> #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false)
+  rule <k> #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) ~> #writeProjectedUpdate(NEW, false)
           =>
             #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS))
         ...
         </k>
      [preserves-definedness] // valid conmtext ensured upon context construction
 
-  rule <k> #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, true)
+  rule <k> #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) ~> #writeProjectedUpdate(NEW, true)
           =>
             #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS))
         ...
@@ -618,7 +594,7 @@ The solution is to use rewrite operations in a downward pass through the project
      andBool I <Int size(LOCALS)
     [preserves-definedness] // valid list indexing checked
 
-  rule <k> #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, _) => .K ... </k>
+  rule <k> #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, CONTEXTS) ~> #writeProjectedUpdate(NEW, _) => .K ... </k>
         <stack> STACK
               =>
                 STACK[(FRAME -Int 1) <-
diff --git a/kmir/uv.lock b/kmir/uv.lock
index 46b3192a6..b74a5d05f 100644
--- a/kmir/uv.lock
+++ b/kmir/uv.lock
@@ -488,7 +488,7 @@ wheels = [
 
 [[package]]
 name = "kmir"
-version = "0.3.151"
+version = "0.3.152"
 source = { editable = "." }
 dependencies = [
     { name = "kframework" },
diff --git a/package/version b/package/version
index c2211bb68..0f5719bf7 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.3.151
+0.3.152