Skip to content

Commit 9ada694

Browse files
dkcummingdkcumming
authored
Verify Rust Standard Library - Challenge 11: Safety of Methods for Numeric Primitive Types (#985)
This PR adds infrastructure for verify-rust-std ([docs](https://model-checking.github.io/verify-rust-std/) / [github](https://github.com/model-checking/verify-rust-std/)) challenges. challenges and implements [Challenge 11: Safety of Methods for Numeric Primitives](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html): - Proof harnesses verifying correctness under preconditions (symbolic inputs) - Fail harnesses verifying UB detection when preconditions are violated, with expected output files - All verify-rust-std proofs run with `--terminate-on-thunk` - K simplification lemmas added for shift mask identities Part 3 (floats) is blocked: KMIR lacks float value support. Harnesses exist in to_int_unchecked-fail.rs and should be moved to to_int_unchecked.rs once passing. Progress Part 1 - Unsafe Integer Methods (`i8`–`i128`, `u8`–`u128`). Proofs for soundness and proofs catching UB: - [x] `unchecked_add` - [x] `unchecked_sub` - [x] `unchecked_mul` - [x] `unchecked_shl` - [x] `unchecked_shr` - [x] `unchecked_neg` (signed only) Part 2 - Safe API Verification. Proofs for soundness: - [x] `wrapping_shl` (`i8`–`i128`, `u8`–`u128`) - [x] `wrapping_shr` (`i8`–`i128`, `u8`–`u128`) - [x] `widening_mul` (`u8`–`u64`) - [x] `carrying_mul` (`u8`–`u64`) Part 3 — Float to Integer Conversion: - [ ] `to_int_unchecked` (`f16`, `f32`, `f64`, `f128`) See "Floats" section below ### Floats #995 added preliminary float support for KMIR, however due to conflicts with expected behaviours with floats in the [Solana equivalance proof harness'](https://github.com/runtimeverification/solana-token/tree/proofs/specs/shared) they have since been reverted. Concrete and symbolic floats will be revisited in future work. For contributors: The haskell backend does not contain a float module and will fail for any float hooks. This means that symbolic floats or any float expression that is not able to be rewritten by the booster backend or simplified / executed by the LLVM backend will fail. While verification of floats as mapping to real numbers remains open research, bitvector verification is well defined and would be sufficient to solve this verification problem. If A. a Float.hs module was added to the haskell-backend, and B. the z3 dependency was connected to solve queries such as this with bitvectors, then I believe this challenge is achievable.
1 parent abd122e commit 9ada694

78 files changed

Lines changed: 3278 additions & 2 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/test.yml‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,8 +74,12 @@ jobs:
7474
test-args: '-k "test_prove and not test_prove_termination"'
7575
parallel: 6
7676
timeout: 150
77+
- name: 'Verify Rust Std'
78+
test-args: '-k test_verify_rust_std'
79+
parallel: 6
80+
timeout: 60
7781
- name: 'Remainder'
78-
test-args: '-k "not llvm and not test_run_smir_random and not test_exec_smir and not test_prove_termination and not test_prove"'
82+
test-args: '-k "not llvm and not test_run_smir_random and not test_exec_smir and not test_prove_termination and not test_prove and not test_verify_rust_std"'
7983
parallel: 6
8084
timeout: 60
8185
steps:

‎Makefile‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,10 @@ test-integration: stable-mir-json build
5656
$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
5757
--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
5858

59+
test-verify-rust-std: stable-mir-json build
60+
$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration/test_integration.py::test_verify_rust_std --maxfail=1 --verbose \
61+
--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
62+
5963
.PHONY: test-stable-mir-ui
6064
test-stable-mir-ui: stable-mir-json build
6165
@test -n "$(RUST_DIR_ROOT)" || (echo "RUST_DIR_ROOT is required. Example: RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui"; exit 2)

‎kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -163,6 +163,17 @@ power of two but the semantics will always operate with these particular ones.
163163
rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma]
164164
```
165165

166+
Shift operations like `wrapping_shl` mask the shift amount with `BITS - 1` (e.g., `rhs & 7` for `u8`).
167+
When the shift amount is already known to be less than `BITS`, the mask is a no-op.
168+
169+
```k
170+
rule VAL &Int 7 => VAL requires 0 <=Int VAL andBool VAL <Int 8 [simplification, preserves-definedness, smt-lemma]
171+
rule VAL &Int 15 => VAL requires 0 <=Int VAL andBool VAL <Int 16 [simplification, preserves-definedness, smt-lemma]
172+
rule VAL &Int 31 => VAL requires 0 <=Int VAL andBool VAL <Int 32 [simplification, preserves-definedness, smt-lemma]
173+
rule VAL &Int 63 => VAL requires 0 <=Int VAL andBool VAL <Int 64 [simplification, preserves-definedness, smt-lemma]
174+
rule VAL &Int 127 => VAL requires 0 <=Int VAL andBool VAL <Int 128 [simplification, preserves-definedness, smt-lemma]
175+
```
176+
166177
Repeated bit-masking can be simplified in an even more general way:
167178

168179
```k

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
# Challenge 0011: Safety of Methods for Numeric Primitive Types
2+
3+
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`.
4+
5+
## Part 1: Unsafe Integer Methods
6+
7+
All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128
8+
9+
- [x] `unchecked_add`
10+
- [x] `unchecked_sub`
11+
- [x] `unchecked_mul`
12+
- [x] `unchecked_shl`
13+
- [x] `unchecked_shr`
14+
15+
Signed only: i8, i16, i32, i64, i128
16+
17+
- [x] `unchecked_neg`
18+
19+
## Part 2: Safe API Verification
20+
21+
All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128
22+
23+
- [x] `wrapping_shl`
24+
- [x] `wrapping_shr`
25+
26+
Unsigned only: u8, u16, u32, u64
27+
28+
- [x] `widening_mul`
29+
- [x] `carrying_mul`
30+
31+
## Part 3: Float to Integer Conversion
32+
33+
TODO: Currently floats are unsupported. The required harnesses are stored in
34+
`to_int_unchecked-fail.txt` (renamed from `.rs` to exclude from tests). Once
35+
float support is added, this file should be renamed to `to_int_unchecked.rs`
36+
and tests that demonstrate KMIR catching `UB` should be added to
37+
`to_int_unchecked-fail.rs`.
38+
39+
Types: f16, f32, f64, f128
40+
41+
- [ ] `to_int_unchecked`

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#![feature(bigint_helper_methods)]
2+
3+
fn main() {
4+
carrying_mul_u8(0, 0, 0);
5+
carrying_mul_u16(0, 0, 0);
6+
carrying_mul_u32(0, 0, 0);
7+
carrying_mul_u64(0, 0, 0);
8+
}
9+
10+
fn carrying_mul_u8(a: u8, b: u8, c: u8) {
11+
let (lo, hi) = a.carrying_mul(b, c);
12+
let expected = (a as u16) * (b as u16) + (c as u16);
13+
assert!(lo == (expected as u8));
14+
assert!(hi == ((expected >> u8::BITS) as u8));
15+
}
16+
17+
fn carrying_mul_u16(a: u16, b: u16, c: u16) {
18+
let (lo, hi) = a.carrying_mul(b, c);
19+
let expected = (a as u32) * (b as u32) + (c as u32);
20+
assert!(lo == (expected as u16));
21+
assert!(hi == ((expected >> u16::BITS) as u16));
22+
}
23+
24+
fn carrying_mul_u32(a: u32, b: u32, c: u32) {
25+
let (lo, hi) = a.carrying_mul(b, c);
26+
let expected = (a as u64) * (b as u64) + (c as u64);
27+
assert!(lo == (expected as u32));
28+
assert!(hi == ((expected >> u32::BITS) as u32));
29+
}
30+
31+
fn carrying_mul_u64(a: u64, b: u64, c: u64) {
32+
let (lo, hi) = a.carrying_mul(b, c);
33+
let expected = (a as u128) * (b as u128) + (c as u128);
34+
assert!(lo == (expected as u64));
35+
assert!(hi == ((expected >> u64::BITS) as u64));
36+
}

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (56 steps)
7+
├─ 3
8+
│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege
9+
│ span: 301
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 128 , Signed ) , 128 , tru
16+
┃ │ span: 301
17+
┃ │
18+
┃ │ (70 steps)
19+
┃ ├─ 6 (terminal)
20+
┃ │ #EndProgram ~> .K
21+
┃ │
22+
┃ ┊ constraint: true
23+
┃ ┊ subst: ...
24+
┃ └─ 2 (leaf, target, terminal)
25+
┃ #EndProgram ~> .K
26+
┃
27+
┗━━┓
28+
│
29+
└─ 5 (leaf, terminal)
30+
thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true )
31+
span: 301
32+
33+
34+

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (56 steps)
7+
├─ 3
8+
│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer
9+
│ span: 115
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 16 , Signed ) , 16 , true
16+
┃ │ span: 115
17+
┃ │
18+
┃ │ (70 steps)
19+
┃ ├─ 6 (terminal)
20+
┃ │ #EndProgram ~> .K
21+
┃ │
22+
┃ ┊ constraint: true
23+
┃ ┊ subst: ...
24+
┃ └─ 2 (leaf, target, terminal)
25+
┃ #EndProgram ~> .K
26+
┃
27+
┗━━┓
28+
│
29+
└─ 5 (leaf, terminal)
30+
thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) ,
31+
span: 115
32+
33+
34+

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (56 steps)
7+
├─ 3
8+
│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer
9+
│ span: 146
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 32 , Signed ) , 32 , true
16+
┃ │ span: 146
17+
┃ │
18+
┃ │ (70 steps)
19+
┃ ├─ 6 (terminal)
20+
┃ │ #EndProgram ~> .K
21+
┃ │
22+
┃ ┊ constraint: true
23+
┃ ┊ subst: ...
24+
┃ └─ 2 (leaf, target, terminal)
25+
┃ #EndProgram ~> .K
26+
┃
27+
┗━━┓
28+
│
29+
└─ 5 (leaf, terminal)
30+
thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) ,
31+
span: 146
32+
33+
34+

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (56 steps)
7+
├─ 3
8+
│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer
9+
│ span: 177
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 64 , Signed ) , 64 , true
16+
┃ │ span: 177
17+
┃ │
18+
┃ │ (70 steps)
19+
┃ ├─ 6 (terminal)
20+
┃ │ #EndProgram ~> .K
21+
┃ │
22+
┃ ┊ constraint: true
23+
┃ ┊ subst: ...
24+
┃ └─ 2 (leaf, target, terminal)
25+
┃ #EndProgram ~> .K
26+
┃
27+
┗━━┓
28+
│
29+
└─ 5 (leaf, terminal)
30+
thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) ,
31+
span: 177
32+
33+
34+

‎kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (56 steps)
7+
├─ 3
8+
│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer
9+
│ span: 53
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 8 , Signed ) , 8 , true )
16+
┃ │ span: 53
17+
┃ │
18+
┃ │ (70 steps)
19+
┃ ├─ 6 (terminal)
20+
┃ │ #EndProgram ~> .K
21+
┃ │
22+
┃ ┊ constraint: true
23+
┃ ┊ subst: ...
24+
┃ └─ 2 (leaf, target, terminal)
25+
┃ #EndProgram ~> .K
26+
┃
27+
┗━━┓
28+
│
29+
└─ 5 (leaf, terminal)
30+
thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) ,
31+
span: 53
32+
33+
34+

0 commit comments

Comments
 (0)