runtimeverification · Stevengre · Dec 10, 2025 · Dec 9, 2025
diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
@@ -125,6 +125,55 @@ Execution gets stuck (no matching rule) when operands have different types or un
   rule #extractOperandType(_, _) => TyUnknown [owise]
 ```
 
+#### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`)
+
+The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation,
+i.e., pointers that refer to the same place and only differ in their offset from a given base.
+
+Additionally, for `ptr_offset_from_unsigned`, it is _known_ that the first argument has a greater offset than
+the second argument, so the returned difference is always positive.
+
+
+```k
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST)
+        => #ptrOffsetDiff(ARG1, ARG2, true, DEST)
+        ...
+       </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST)
+        => #ptrOffsetDiff(ARG1, ARG2, false, DEST)
+        ...
+       </k>
+
+  syntax KItem ::= #ptrOffsetDiff ( Evaluation , Evaluation , Bool , Place ) [seqstrict(1,2)]
+
+  syntax MIRError ::= UBPtrOffsetDiff
+
+  syntax UBPtrOffsetDiff ::= #UBErrorPtrOffsetDiff( Value , Value , Bool )
+
+  rule <k> 
+        #ptrOffsetDiff(
+          PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF1, _)),
+          PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF2, _)),
+          SIGNED_FLAG,
+          DEST
+       ) => #setLocalValue(DEST, Integer(OFF1 -Int OFF2, 64, SIGNED_FLAG))
+        ...
+       </k>
+    requires (SIGNED_FLAG orBool OFF1 >=Int OFF2)
+
+  rule <k> 
+        #ptrOffsetDiff(
+          PtrLocal(_, _, _, _) #as PTR1,
+          PtrLocal(_, _, _, _) #as PTR2,
+          SIGNED_FLAG,
+          _DEST
+       ) => #UBErrorPtrOffsetDiff(PTR1, PTR2, SIGNED_FLAG)
+        ...
+       </k>
+    [priority(100)]
+```
+
 ```k
 endmodule
 ```
diff --git a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected
@@ -0,0 +1,137 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (296 steps)
+├─ 3 (split)
+│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     0 ==Int ARG_INT1:Int &Int 18446744073709551615
+┃  │
+┃  ├─ 4
+┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
+┃  │
+┃  │  (582 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     notBool 0 ==Int ARG_INT1:Int &Int 18446744073709551615
+   │
+   ├─ 5
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) )
+   │
+   │  (1 step)
+   ├─ 7 (split)
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
+   ┃
+   ┃ (branch)
+   ┣━━┓ subst: .Subst
+   ┃  ┃ constraint:
+   ┃  ┃     1 ==Int ARG_INT1:Int &Int 18446744073709551615
+   ┃  │
+   ┃  ├─ 8
+   ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
+   ┃  │
+   ┃  │  (99 steps)
+   ┃  └─ 10 (stuck, leaf)
+   ┃      #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
+   ┃
+   ┗━━┓ subst: .Subst
+      ┃ constraint:
+      ┃     notBool 1 ==Int ARG_INT1:Int &Int 18446744073709551615
+      │
+      ├─ 9
+      │   #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) )
+      │
+      │  (1 step)
+      ├─ 11 (split)
+      │   #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
+      ┃
+      ┃ (branch)
+      ┣━━┓ subst: .Subst
+      ┃  ┃ constraint:
+      ┃  ┃     2 ==Int ARG_INT1:Int &Int 18446744073709551615
+      ┃  │
+      ┃  ├─ 12
+      ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
+      ┃  │
+      ┃  │  (99 steps)
+      ┃  └─ 14 (stuck, leaf)
+      ┃      #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
+      ┃
+      ┗━━┓ subst: .Subst
+         ┃ constraint:
+         ┃     notBool 2 ==Int ARG_INT1:Int &Int 18446744073709551615
+         │
+         ├─ 13
+         │   #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) )
+         │
+         │  (1 step)
+         ├─ 15 (split)
+         │   #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
+         ┃
+         ┃ (branch)
+         ┣━━┓ subst: .Subst
+         ┃  ┃ constraint:
+         ┃  ┃     3 ==Int ARG_INT1:Int &Int 18446744073709551615
+         ┃  │
+         ┃  ├─ 16
+         ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
+         ┃  │
+         ┃  │  (16 steps)
+         ┃  └─ 18 (stuck, leaf)
+         ┃      #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 0 , place ( ... local: local
+         ┃
+         ┗━━┓ subst: .Subst
+            ┃ constraint:
+            ┃     notBool 3 ==Int ARG_INT1:Int &Int 18446744073709551615
+            │
+            ├─ 17
+            │   #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) )
+            │
+            │  (1 step)
+            ├─ 19 (split)
+            │   #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
+            ┃
+            ┃ (branch)
+            ┣━━┓ subst: .Subst
+            ┃  ┃ constraint:
+            ┃  ┃     4 ==Int ARG_INT1:Int &Int 18446744073709551615
+            ┃  │
+            ┃  ├─ 20
+            ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
+            ┃  │
+            ┃  │  (68 steps)
+            ┃  └─ 22 (stuck, leaf)
+            ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+            ┃      span: 32
+            ┃
+            ┗━━┓ subst: .Subst
+               ┃ constraint:
+               ┃     notBool 4 ==Int ARG_INT1:Int &Int 18446744073709551615
+               │
+               ├─ 21
+               │   #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) )
+               │
+               │  (6 steps)
+               ├─ 23 (terminal)
+               │   #EndProgram ~> .K
+               │
+               ┊  constraint: true
+               ┊  subst: ...
+               └─ 2 (leaf, target, terminal)
+                   #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs b/kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs
@@ -0,0 +1,43 @@
+#![feature(core_intrinsics)]
+use std::intrinsics::ptr_offset_from_unsigned; // core::ptr variant since 1.87.0, not for us
+
+fn testing(mode: isize) {
+    let a = [1, 2, 3, 4, 5];
+    let b = [6, 7, 8, 9, 10];
+    let a_p = &a as *const i32;
+    let b_p = &b as *const i32;
+    let a1: *const i32 = &a[1];
+    let a3: *const i32 = &a[3];
+    let b1: *const i32 = &b[1];
+
+    match mode {
+        0 => unsafe { // correct and expected operation on pointers with offset
+            let a1_p = a_p.add(1);
+            assert_eq!(a1_p.offset_from(a_p), 1);
+            assert_eq!(a_p.offset_from(a1_p), -1);
+            assert_eq!(ptr_offset_from_unsigned(a1_p, a_p), 1);
+        },
+        1 => unsafe { // correct and expected operation on addresses within arrays
+            assert_eq!(a3.offset_from(a1), 2);
+            assert_eq!(a1.offset_from(a3), -2);
+        },
+        2 => unsafe { // different allocation
+            assert_eq!(a1.offset_from(b1), 0xdeadbeef); // UB
+        },
+        3 => unsafe {
+            // violating assumption of a3 > a1
+            assert_eq!(ptr_offset_from_unsigned(a1, a3), 0xdeadbeef); // UB
+        },
+        4 => unsafe {
+            let unit_p: *const () = &();
+            assert_eq!(unit_p.offset_from(unit_p), 0xdeadbeef); // panics
+        },
+        _ => ()
+    }
+}
+
+
+fn main() {
+    testing(0);
+    testing(4);
+}
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
@@ -37,6 +37,7 @@
     'assume-cheatcode': ['check_assume'],
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
+    'test_offset_from-fail': ['testing'],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',
@@ -59,6 +60,7 @@
     'unions-fail',
     'transmute-maybe-uninit-fail',
     'iter_next_2-fail',
+    'test_offset_from-fail',
 ]