refactor: move runtime local access to slot-backed frames

.gitignore

@@ -6,4 +6,5 @@ __pycache__/
 kmir/src/tests/integration/data/**/target
 .DS_Store
 proof/
-/result*
+/result*
+tmp*

kmir/src/kmir/kast.py

@@ -7,7 +7,7 @@
 
 from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst, build_cons
 from pyk.kast.manip import free_vars, split_config_from
-from pyk.kast.prelude.collections import list_empty, list_of
+from pyk.kast.prelude.collections import list_empty, list_of, map_of
 from pyk.kast.prelude.kint import eqInt, intToken, leInt
 from pyk.kast.prelude.ml import mlEqualsTrue
 from pyk.kast.prelude.utils import token
@@ -19,12 +19,11 @@
     BoolValue,
     DynamicSize,
     IntValue,
-    Local,
     Metadata,
-    Place,
     PtrLocalValue,
     RangeValue,
     RefValue,
+    SlotPlace,
     StaticSize,
 )
 
@@ -192,12 +191,16 @@ def init_subst() -> dict[str, KInner]:
             k_cell,
         )
 
+    slot_ids = [token(i) for i in range(len(localvars))]
     subst = Subst(
         {
             **init_subst(),
             **{
                 'K_CELL': k_cell,
-                'LOCALS_CELL': list_of(localvars),
+                'LOCALS_CELL': list_of(slot_ids),
+                'SLOTSTORE_CELL': map_of(zip(slot_ids, localvars, strict=True)),
+                'NEXTSLOT_CELL': token(len(slot_ids)),
+                'GENERATEDCOUNTER_CELL': token(0),
             },
         }
     )
@@ -215,11 +218,15 @@ def _make_symbolic_call_config(
     types: Mapping[Ty, TypeMetadata],
 ) -> tuple[KInner, list[KInner]]:
     locals, constraints = _symbolic_locals(fn_data.args, types)
+    slot_ids = [token(i) for i in range(len(locals))]
     subst = Subst(
         {
             'K_CELL': fn_data.call_terminator,
             'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
-            'LOCALS_CELL': list_of(locals),
+            'LOCALS_CELL': list_of(slot_ids),
+            'SLOTSTORE_CELL': map_of(zip(slot_ids, locals, strict=True)),
+            'NEXTSLOT_CELL': token(len(slot_ids)),
+            'GENERATEDCOUNTER_CELL': token(0),
         },
     )
     empty_config = definition.empty_config(KSort('GeneratedTopCell'))
@@ -373,7 +380,11 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                     mlEqualsTrue(leInt(variant_var, token(max_variant))),
                 ]
                 args = self._fresh_var('ENUM_ARGS')
-                return KApply('Value::Aggregate', (KApply('variantIdx', (variant_var,)), args)), idx_range, None
+                return (
+                    KApply('Value::Aggregate', (KApply('variantIdx', (variant_var,)), args)),
+                    idx_range + [mlEqualsTrue(KApply('allValues', (args,)))],
+                    None,
+                )
 
             case StructT(_, _, fields):
                 field_vars: list[KInner] = []
@@ -390,14 +401,18 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
 
             case UnionT():
                 args = self._fresh_var('ARG_UNION')
-                return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), [], None
+                return (
+                    KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)),
+                    [mlEqualsTrue(KApply('allValues', (args,)))],
+                    None,
+                )
 
             case ArrayT(_, None):
                 elems = self._fresh_var('ARG_ARRAY')
                 l = self._fresh_var('ARG_ARRAY_LEN')
                 return (
                     KApply('Value::Range', (elems,)),
-                    [mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), l))],
+                    [mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), l)), mlEqualsTrue(KApply('allValues', (elems,)))],
                     KApply(
                         'Metadata',
                         (
@@ -450,8 +465,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                     KApply(
                         'Value::Reference',
                         (
-                            token(0),  # Stack OFFSET field
-                            KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
+                            KApply('SlotPlace', (token(ref), KApply('ProjectionElems::empty', ()))),
                             KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
                             metadata if metadata is not None else no_metadata,
                         ),
@@ -468,8 +482,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                     KApply(
                         'Value::PtrLocal',
                         (
-                            token(0),
-                            KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
+                            KApply('SlotPlace', (token(ref), KApply('ProjectionElems::empty', ()))),
                             KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
                             metadata if metadata is not None else no_metadata,
                         ),
@@ -652,15 +665,13 @@ def _random_ptr_value(self, mut: bool, type_info: PtrT | RefT) -> PtrLocalValue
         match type_info:
             case PtrT():
                 return PtrLocalValue(
-                    stack_depth=0,
-                    place=Place(local=Local(ref)),
+                    place=SlotPlace(slot=ref),
                     mut=mut,
                     metadata=metadata,
                 )
             case RefT():
                 return RefValue(
-                    stack_depth=0,
-                    place=Place(local=Local(ref)),
+                    place=SlotPlace(slot=ref),
                     mut=mut,
                     metadata=metadata,
                 )

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

@@ -87,21 +87,54 @@ The implementation requires operands to have identical types (`TY1 ==K TY2`) bef
 Execution gets stuck (no matching rule) when operands have different types or unknown type information.
 
 ```k
-  // Raw eq: dereference operands, extract types, and delegate to typed comparison
+  syntax KItem ::= #getType(Operand)
+                 | #execRawEqCheck(KItem)
+                 | #execRawEqValues(Place, Evaluation, Evaluation) [seqstrict(2,3)]
+
+  // Raw eq: first verify type equality, then compare dereferenced values.
   rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE, _SPAN)
-        => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
-                                  #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
+        => #getType(#withDeref(ARG1))
+        ~> #execRawEqCheck(#getType(#withDeref(ARG2)))
+        ~> #execRawEqValues(PLACE, #withDeref(ARG1), #withDeref(ARG2))
+       ... </k>
+
+  rule <k> #getType(operandCopy(place(local(I), PROJS)))
+        => getTyOf(tyOfLocal(LOCAL), PROJS)
        ... </k>
        <locals> LOCALS </locals>
+       <slotStore> ... SLOT:Int |-> LOCAL:TypedLocal ... </slotStore>
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool SLOT ==Int #frameSlotId(LOCALS, I)
+    [preserves-definedness]
 
-  // Compare values only if types are identical
-  syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
-  rule <k> #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty)
-        => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
+  rule <k> #getType(operandMove(place(local(I), PROJS)))
+        => getTyOf(tyOfLocal(LOCAL), PROJS)
+       ... </k>
+       <locals> LOCALS </locals>
+       <slotStore> ... SLOT:Int |-> LOCAL:TypedLocal ... </slotStore>
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool SLOT ==Int #frameSlotId(LOCALS, I)
+    [preserves-definedness]
+
+  rule <k> #getType(operandConstant(constOperand(_, _, mirConst(_, TY, _)))) => TY ... </k>
+
+  rule <k> #getType(_OP) => TyUnknown ... </k> [owise]
+
+  rule <k> TY1:Ty ~> #execRawEqCheck(#getType(ARG2))
+        => #getType(ARG2)
+        ~> #execRawEqCheck(TY1)
+       ... </k>
+
+  rule <k> TY2:Ty ~> #execRawEqCheck(TY1:Ty)
+        => .K
        ... </k>
     requires TY1 ==K TY2
     [preserves-definedness]
 
+  rule <k> #execRawEqValues(DEST, VAL1:Value, VAL2:Value)
+        => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
+       ... </k>
+
   // Add deref projection to operands
   syntax Operand ::= #withDeref(Operand) [function, total]
   rule #withDeref(operandCopy(place(LOCAL, PROJ)))
@@ -111,18 +144,6 @@ Execution gets stuck (no matching rule) when operands have different types or un
        // must not overwrite the value, just the reference is moved!
   rule #withDeref(OP) => OP [owise]
 
-  // Extract type from operands (locals with projections, constants, fallback to unknown)
-  syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total]
-  rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
-    requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
-    [preserves-definedness]
-  rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
-    requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
-    [preserves-definedness]
-  rule #extractOperandType(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
-  rule #extractOperandType(_, _) => TyUnknown [owise]
 ```
 
 #### Volatile Store (`std::intrinsics::volatile_store`, `std::ptr::write_volatile`)
@@ -191,8 +212,8 @@ the second argument, so the returned difference is always positive.
 
   rule <k> 
         #ptrOffsetDiff(
-          PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF1, _)),
-          PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF2, _)),
+          PtrLocal(PLACE, _, metadata( _ , OFF1, _)),
+          PtrLocal(PLACE, _, metadata( _ , OFF2, _)),
           SIGNED_FLAG,
           DEST
        ) => #setLocalValue(DEST, Integer(OFF1 -Int OFF2, 64, SIGNED_FLAG))
@@ -202,8 +223,8 @@ the second argument, so the returned difference is always positive.
 
   rule <k> 
         #ptrOffsetDiff(
-          PtrLocal(_, _, _, _) #as PTR1,
-          PtrLocal(_, _, _, _) #as PTR2,
+          PtrLocal(_, _, _) #as PTR1,
+          PtrLocal(_, _, _) #as PTR2,
           SIGNED_FLAG,
           _DEST
        ) => #UBErrorPtrOffsetDiff(PTR1, PTR2, SIGNED_FLAG)