Tips for verifying usages of HashMap

[fpoli]

Hi! I'm trying to verify some usages of a HashMap, like the example below, and I'm fine with trusting the implementation of HashMap using stubs or contracts. I found a very useful suggestion in #2423 (comment) to add a stub for RandomState::new. This was enough to verify the first assertion. However, the insert call still reaches some problematic code. Before digging deeper in the implementation of HashMap, do you have any suggestions?

#[cfg(kani)]
mod verify {
    use std::collections::HashMap;
    use std::collections::hash_map::RandomState;
    use std::mem::{size_of, size_of_val, transmute};

    #[allow(dead_code)]
    fn concrete_state() -> RandomState {
        let keys: [u64; 2] = [0, 0];
        assert_eq!(size_of_val(&keys), size_of::<RandomState>());
        unsafe { transmute(keys) }
    }

    #[kani::proof]
    #[kani::stub(RandomState::new, concrete_state)]
    #[kani::unwind(3)]
    #[kani::solver(minisat)]
    fn test() {
        let mut map: HashMap<u64, u64> = HashMap::new();
        assert_eq!(map.get(&0), None); // Ok

        // Fails:
        map.insert(0, 0);
        assert_eq!(map.get(&0), Some(&0));
    }
}

...

Check 2209: std::ptr::swap_nonoverlapping_simple_untyped::<usize>.unwind.0
	 - Status: FAILURE
	 - Description: "unwinding assertion loop 0"
	 - Location: ../../../runner/.rustup/toolchains/nightly-2025-01-28-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1143:5 in function std::ptr::swap_nonoverlapping_simple_untyped::<usize>

SUMMARY:
 ** 1 of 2209 failed (2208 undetermined)
Failed Checks: unwinding assertion loop 0
 File: "/Users/runner/.rustup/toolchains/nightly-2025-01-28-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", line 1143, in std::ptr::swap_nonoverlapping_simple_untyped::<usize>

VERIFICATION:- FAILED
[Kani] info: Verification output shows one or more unwinding failures.
[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.
Verification Time: 2.1279416s

Summary:
Verification failed for - verify::test
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

[zhassan-aws]

Hi @fpoli. The failure is due to an insufficient unwind value. This indicates that there's a loop somewhere that requires an unwinding value greater than 3. Verification succeeds if I increase the unwind value to 5:

SUMMARY:
 ** 0 of 2198 failed (60 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 255.76009s

We have a similar test in our regressions:

https://github.com/model-checking/kani/blob/main/tests/perf/hashset/src/lib.rs

[fpoli]

Thanks!