runtimeverification · Stevengre · Dec 16, 2025 · Dec 12, 2025 · Dec 12, 2025 · Dec 15, 2025
diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -305,21 +305,33 @@ The call stack is not necessarily empty at this point so it is left untouched.
 `Call` is calling another function, setting up its stack frame and
 where the returned result should go.
 
-
 ```k
-  // Intrinsic function call - execute directly without state switching
-  rule [termCallIntrinsic]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _
-         =>
-           #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET)
+  syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction)
+
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), _SPAN))
+        => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND)
+        ...
        </k>
-    requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
+
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), _SPAN))
+        => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND)
+        ...
+       </k>
+      <locals> LOCALS </locals>
+
+  // Intrinsic function call - execute directly without state switching
+  rule [termCallIntrinsic]:
+        <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND) ~> _
+         => #execIntrinsic(FUNC, ARGS, DEST) ~> #continueAt(TARGET)
+        </k>
+    requires isIntrinsicFunction(FUNC)
 
   // Regular function call - full state switching and stack setup
-  rule [termCallFunction]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _
-         =>
-           #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
+  rule [termCallFunction]:
+       <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND) ~> _
+        => #setUpCalleeData(FUNC, ARGS)
        </k>
-       <currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
+       <currentFunc> CALLER => FTY </currentFunc>
        <currentFrame>
          <currentBody> _ </currentBody>
          <caller> OLDCALLER => CALLER </caller>
@@ -329,7 +341,7 @@ where the returned result should go.
          <locals> LOCALS </locals>
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
-    requires notBool isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
+    requires notBool isIntrinsicFunction(FUNC)
 
   syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function]
   rule isIntrinsicFunction(IntrinsicFunction(_)) => true
@@ -338,11 +350,6 @@ where the returned result should go.
   syntax KItem ::= #continueAt(MaybeBasicBlockIdx)
   rule <k> #continueAt(someBasicBlockIdx(TARGET)) => #execBlockIdx(TARGET) ... </k>
   rule <k> #continueAt(noBasicBlockIdx) => .K ... </k>
-
-  syntax Ty ::= #tyOfCall( Operand ) [function, total]
-
-  rule #tyOfCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _)))) => Ty
-  rule #tyOfCall(_) => ty(-1) [owise] // copy, move, non-zero size: not supported
 ```
 
 The local data has to be set up for the call, which requires information about the local variables of a call. This step is separate from the above call stack setup because it needs to retrieve the locals declaration from the body. Arguments to the call are `Operands` which refer to the old locals (`OLDLOCALS` below), and the data is either _copied_ into the new locals using `#setArgs`, or it needs to be _shared_ via references.
@@ -412,7 +419,8 @@ An operand may be a `Reference` (the only way a function could access another fu
      andBool isTypedValue(CALLERLOCALS[I])
     [preserves-definedness] // valid list indexing checked
 
-  rule <k> #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems)))
+  // TODO: This is not safe, need to add more checks to this.
+  rule <k> #setArgFromStack(IDX, operandMove(place(local(I), _)))
         =>
            #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
         ...

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -130,6 +130,17 @@ Constant operands are simply decoded according to their type.
     requires typeInfoVoidType =/=K lookupTy(TY)
 ```
 
+Function pointers are zero-sized constants whose `Ty` is a key in the function table instaed of the type table.
+
+```k
+  rule <k> operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, ty(ID) #as TY, _)))
+        => FunPtr(TY)
+       ...
+       </k>
+    requires typeInfoVoidType ==K lookupTy(TY) // not a valid type info
+     andBool lookupFunction(TY) =/=K monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(ID), noBody ) // valid function Ty
+```
+
 ### Copying and Moving
 
 When an operand is `Copied` by a read, the original remains valid (see `false` passed to `#readProjection`).

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md
@@ -51,6 +51,8 @@ The special `Moved` value represents values that have been used and should not b
                                                           [symbol(Value::PtrLocal)]
                    // pointer to a local TypedValue (on the stack)
                    // fields are the same as in Reference
+                 | FunPtr ( Ty )
+                   // function pointer, created by operandConstant only. Ty is a key in the function table
                  | AllocRef ( AllocId , ProjectionElems , Metadata )
                                                           [symbol(Value::AllocRef)]
                    // reference to static allocation, by AllocId, possibly projected, carrying metadata if applicable

diff --git a/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected b/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (42 steps)
+│  (44 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709
 ┃

diff --git a/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected b/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (225 steps)
+│  (228 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

diff --git a/kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected b/kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (34 steps)
+│  (35 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709
 ┃

diff --git a/...tegration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected b/...tegration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (112 steps)
+│  (114 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃
@@ -14,7 +14,7 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃  │
-┃  │  (5 steps)
+┃  │  (6 steps)
 ┃  └─ 6 (stuck, leaf)
 ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
 ┃
@@ -25,7 +25,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
    │
-   │  (181 steps)
+   │  (182 steps)
    ├─ 7 (terminal)
    │   #EndProgram ~> .K
    │

diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (727 steps)
+│  (736 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

diff --git a/.../src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected b/.../src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (212 steps)
+│  (216 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

diff --git a/kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs b/kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs
@@ -0,0 +1,27 @@
+use std::convert::TryFrom;
+use std::array;
+
+// inspired by solana-pubkey but very simple code
+#[allow(dead_code)]
+struct EightBytes([u8;8]);
+
+impl From<[u8;8]> for EightBytes {
+    fn from(bytes: [u8;8]) -> Self { Self(bytes) } 
+}
+
+// causing problems with the extraction
+// the `try_from` and `from` from stdlib are not available in the SMIR
+impl TryFrom<&[u8]> for EightBytes {
+    type Error = array::TryFromSliceError;
+    fn try_from(bytes: &[u8]) -> Result<EightBytes, Self::Error> {
+        <[u8;8]>::try_from(bytes).map(Self::from) 
+    }
+}
+
+fn main() {
+    let bytes: [u8;8] = [1,2,3,4,5,6,7,8];
+    let _unused = EightBytes::from(bytes);
+    let slice: &[u8] = &bytes;
+    let thing: Result<EightBytes, _> = EightBytes::try_from(slice);
+    assert!(thing.is_ok());
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (8 steps)
+│  (10 steps)
 └─ 3 (stuck, leaf)
     #ProgramError ( AssertInhabitedFailure ) ~> .K
     function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: src/rust/library/std/src/rt.rs:194
 │
-│  (6 steps)
+│  (7 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: src/rust/library/std/src/rt.rs:194
 │
-│  (6 steps)
+│  (7 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (147 steps)
+│  (148 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

diff --git a/...egration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected b/...egration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (59 steps)
+│  (61 steps)
 └─ 3 (stuck, leaf)
     #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
     span: 32

diff --git a/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected b/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (830 steps)
+│  (837 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (866 steps)
+│  (877 steps)
 └─ 3 (stuck, leaf)
     #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
     span: 32

diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (151 steps)
+│  (154 steps)
 ├─ 3
 │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (1990 steps)
+│  (2000 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio
     span: 146

diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (487 steps)
+│  (491 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ..
     span: 219

diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (105 steps)
+│  (106 steps)
 ├─ 3
 │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (731 steps)
+│  (740 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: src/rust/library/std/src/rt.rs:194
 │
-│  (13 steps)
+│  (14 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 3 ) )
 │   function: foo
@@ -94,11 +94,11 @@ Node roles (exclusive):
 Leaf paths from init:
   total leaves (non-root): 1
   reachable leaves       : 1
-  total steps            : 33
+  total steps            : 34
 
-  leaf 2 (path 1/3): steps 33, path 1 -> 3 -> 5 -> 7 -> 9 -> 11 -> 2
-  leaf 2 (path 2/3): steps 46, path 1 -> 3 -> 4 -> 6 -> 2
-  leaf 2 (path 3/3): steps 47, path 1 -> 3 -> 5 -> 7 -> 8 -> 10 -> 2
+  leaf 2 (path 1/3): steps 34, path 1 -> 3 -> 5 -> 7 -> 9 -> 11 -> 2
+  leaf 2 (path 2/3): steps 47, path 1 -> 3 -> 4 -> 6 -> 2
+  leaf 2 (path 3/3): steps 48, path 1 -> 3 -> 5 -> 7 -> 8 -> 10 -> 2
 
 LEAF <k> CELLS
 ---------------

diff --git a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (31 steps)
+│  (34 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toLocal ( 1 ) , thunk ( #decodeConstant ( constantKindAllo
     span: 48

diff --git a/...sts/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/...sts/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (43 steps)
+│  (44 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
 ┃
@@ -15,7 +15,7 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
 ┃  │
-┃  │  (5 steps)
+┃  │  (6 steps)
 ┃  └─ 6 (stuck, leaf)
 ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
 ┃      span: 32
@@ -27,7 +27,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
    │
-   │  (209 steps)
+   │  (211 steps)
    ├─ 7
    │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset (
    │   span: 87
@@ -51,7 +51,7 @@
    ┃  ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( range ( #map
    ┃  ┃  │   span: 87
    ┃  ┃  │
-   ┃  ┃  │  (113 steps)
+   ┃  ┃  │  (114 steps)
    ┃  ┃  └─ 13 (stuck, leaf)
    ┃  ┃      #traverseProjection ( toLocal ( 5 ) , Range ( range ( #mapOffset ( ARG_ARRAY1:Li
    ┃  ┃      span: 97

diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (119 steps)
+│  (120 steps)
 ├─ 3
 │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
 │   function: main

diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected
@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (51 steps)
+│  (52 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) )
 ┃