runtimeverification · dkcumming · Mar 11, 2026 · Mar 11, 2026 · Mar 11, 2026 · Mar 11, 2026
diff --git a/Makefile b/Makefile
@@ -56,6 +56,10 @@ test-integration: stable-mir-json build
 	$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
 			--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
 
+test-verify-rust-std: stable-mir-json build
+	$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration/test_integration.py::test_verify_rust_std --maxfail=1 --verbose \
+			--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
+
 # Checks and formatting
 
 format: autoflake isort black nix-fmt

diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
@@ -163,6 +163,17 @@ power of two but the semantics will always operate with these particular ones.
   rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma]
 ```
 
+Shift operations like `wrapping_shl` mask the shift amount with `BITS - 1` (e.g., `rhs & 7` for `u8`).
+When the shift amount is already known to be less than `BITS`, the mask is a no-op.
+
+```k
+  rule VAL &Int 7   => VAL requires 0 <=Int VAL andBool VAL <Int 8   [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int 15  => VAL requires 0 <=Int VAL andBool VAL <Int 16  [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int 31  => VAL requires 0 <=Int VAL andBool VAL <Int 32  [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int 63  => VAL requires 0 <=Int VAL andBool VAL <Int 64  [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int 127 => VAL requires 0 <=Int VAL andBool VAL <Int 128 [simplification, preserves-definedness, smt-lemma]
+```
+
 Repeated bit-masking can be simplified in an even more general way:
 
 ```k

diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md
@@ -0,0 +1,40 @@
+# Challenge 0011: Safety of Methods for Numeric Primitive Types
+
+Tests for [verify-rust-std challenge 0011](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html), which verifies the safety of public unsafe methods for floats and integers in `core::num`.
+
+## Part 1: Unsafe Integer Methods
+
+All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128
+
+- [x] `unchecked_add`
+- [x] `unchecked_sub`
+- [x] `unchecked_mul`
+- [x] `unchecked_shl`
+- [x] `unchecked_shr`
+
+Signed only: i8, i16, i32, i64, i128
+
+- [x] `unchecked_neg`
+
+## Part 2: Safe API Verification
+
+All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128
+
+- [x] `wrapping_shl`
+- [x] `wrapping_shr`
+
+Unsigned only: u8, u16, u32, u64
+
+- [x] `widening_mul`
+- [x] `carrying_mul`
+
+## Part 3: Float to Integer Conversion
+
+TODO: Currently floats are unsupported. However there the required harnesses are
+added to `to_int_unchecked-fail.rs`, once they are passing this file should be
+renamed to `to_int_unchecked.rs` and tests that demonstrate KMIR catching `UB`
+should be added to `to_int_unchecked-fail.rs`.
+
+Types: f16, f32, f64, f128
+
+- [ ] `to_int_unchecked`
diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs
@@ -0,0 +1,36 @@
+#![feature(bigint_helper_methods)]
+
+fn main() {
+    carrying_mul_u8(0, 0, 0);
+    carrying_mul_u16(0, 0, 0);
+    carrying_mul_u32(0, 0, 0);
+    carrying_mul_u64(0, 0, 0);
+}
+
+fn carrying_mul_u8(a: u8, b: u8, c: u8) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u16) * (b as u16) + (c as u16);
+    assert!(lo == (expected as u8));
+    assert!(hi == ((expected >> u8::BITS) as u8));
+}
+
+fn carrying_mul_u16(a: u16, b: u16, c: u16) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u32) * (b as u32) + (c as u32);
+    assert!(lo == (expected as u16));
+    assert!(hi == ((expected >> u16::BITS) as u16));
+}
+
+fn carrying_mul_u32(a: u32, b: u32, c: u32) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u64) * (b as u64) + (c as u64);
+    assert!(lo == (expected as u32));
+    assert!(hi == ((expected >> u32::BITS) as u32));
+}
+
+fn carrying_mul_u64(a: u64, b: u64, c: u64) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u128) * (b as u128) + (c as u128);
+    assert!(lo == (expected as u64));
+    assert!(hi == ((expected >> u64::BITS) as u64));
+}
diff --git a/...-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected b/...-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected
@@ -0,0 +1,38 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (31 steps)
+├─ 3
+│   #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 38 ) , ty ( 39
+│   span: 32
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 340282366920938463463374607
+┃  │   span: 32
+┃  │
+┃  │  (29 steps)
+┃  ├─ 6
+┃  │   #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 3402823669209384634
+┃  │   span: 115
+┃  │
+┃  │  (1 step)
+┃  └─ 7 (leaf, terminal)
+┃      thunk ( #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 34028236692
+┃      span: 115
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 38 ) ,
+       span: 32
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/...ify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected b/...ify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected
@@ -0,0 +1,39 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (31 steps)
+├─ 3
+│   #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 22 ) , ty ( 23
+│   span: 32
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 , 16 , false )
+~> #fr
+┃  │   span: 32
+┃  │
+┃  │  (29 steps)
+┃  ├─ 6
+┃  │   #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 &Int 32767 ,
+┃  │   span: 56
+┃  │
+┃  │  (1 step)
+┃  └─ 7 (leaf, terminal)
+┃      thunk ( #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 &Int
+┃      span: 56
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 22 ) ,
+       span: 32
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/...fy-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected b/...fy-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (22 steps)
+└─ 3 (stuck, leaf)
+    #execIntrinsic ( IntrinsicFunction ( symbol ( "fabsf32" ) ) , operandMove ( plac
+    span: 73
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/...fy-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected b/...fy-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (22 steps)
+└─ 3 (stuck, leaf)
+    #execIntrinsic ( IntrinsicFunction ( symbol ( "fabsf64" ) ) , operandMove ( plac
+    span: 90
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/...data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected b/...data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected
@@ -0,0 +1,34 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3
+│   #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege
+│   span: 301
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 128 , Signed ) , 128 , tru
+┃  │   span: 301
+┃  │
+┃  │  (70 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true )
+       span: 301
+
+
+
diff --git a/.../data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected b/.../data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected
@@ -0,0 +1,34 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3
+│   #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer
+│   span: 115
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 16 , Signed ) , 16 , true
+┃  │   span: 115
+┃  │
+┃  │  (70 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) ,
+       span: 115
+
+
+
diff --git a/.../data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected b/.../data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected
@@ -0,0 +1,34 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3
+│   #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer
+│   span: 146
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 32 , Signed ) , 32 , true
+┃  │   span: 146
+┃  │
+┃  │  (70 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) ,
+       span: 146
+
+
+
diff --git a/.../data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected b/.../data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected
@@ -0,0 +1,34 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3
+│   #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer
+│   span: 177
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 64 , Signed ) , 64 , true
+┃  │   span: 177
+┃  │
+┃  │  (70 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) ,
+       span: 177
+
+
+
diff --git a/...n/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected b/...n/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected
@@ -0,0 +1,34 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3
+│   #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer
+│   span: 53
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 8 , Signed ) , 8 , true )
+┃  │   span: 53
+┃  │
+┃  │  (70 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓
+   │
+   └─ 5 (leaf, terminal)
+       thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) ,
+       span: 53
+
+
+