Challenge 11: Safety of Methods for Numeric Primitive Types

[carolynzech]

Link to challenge: https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html

[Yenyun035]

Hello! We are CMU Team 2 and will be working on this challenge :)

Our team:

• III Project Manager: @parkerqi
• INI Tech Lead: @rajathkotyal
• INI Engineers: @Yenyun035, @lanfeima, @MWDZ

[Yenyun035]

Hello, this is Team 2 :) We have a question regarding how to write proofs.

Per Part 1 of the challenge, we will need to write proofs for unchecked_ methods. We referred to other harnesses in the repo and found that all of them use the kani::proof_for_contract() attribute instead of kani::proof. According to our understanding from this function contract doc, we can use kani::proof_for_contract() when verifying functions that have requires() and/or ensures(). However, in our case, `unchecked_methods inint_macros.rsanduint_macros.rs` do not have any contracts. Therefore, we came up with two approaches and are wondering which to proceed with:

1. kani::proof_for_contract() + a wrapper with contracts around unchecked_* methods. For example:

   
   #[kani::requires(!num1.overflowing_add(num2).1)]
   #[kani::ensures(|ret| *ret >= i8::MIN && *ret <= i8::MAX)]
   fn i8_unchecked_add_wrapper(num1: i8, num2: i8) -> i8 {
   unsafe { num1.unchecked_add(num2) }
   }

// pub const unsafe fn unchecked_add(self, rhs: Self) -> Self

[kani::proof_for_contract(i8_unchecked_add_wrapper)]

pub fn check_unchecked_add_i8() { let num1: i8 = kani::any::(); let num2: i8 = kani::any::();

unsafe {
    // Kani ensures the inputs satisfy preconditions
    i8_unchecked_add_wrapper(num1, num2);
    // Kani ensures the output satisfies postconditions
}

}

2. `kani::proof` + `kani::assume()` for preconditions and `assert()` for postconditions. For example:

// pub const unsafe fn unchecked_add(self, rhs: Self) -> Self

[kani::proof]

pub fn check_unchecked_add_i16() { let num1: i16 = kani::any::(); let num2: i16 = kani::any::();

// overflowing_add return (result, bool) where bool is if
// add will overflow. This check takes the boolean. 
kani::assume(!num1.overflowing_add(num2).1);

unsafe {
    let result = num1.unchecked_add(num2);

    // Either check result
    assert_eq!(Some(result), num1.checked_add(num2));

    // Or check the range of result
    assert!(result >= i16::MIN && result <= i16::MAX);
}

}

Thank you for any guidance and clarifications! @rahulku @feliperodri 

[carolynzech]

@Yenyun035 Good question! We recommend writing contracts and applying them directly to the functions. So, close to what you have for option 1, but omitting the wrapper. For example:

// your contracts go here!
pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { ... }

You can then go ahead and write harnesses for the methods directly, e.g.

#[kani::proof_for_contract(i8::unchecked_add)]
fn harness() {...}

It seems like you have a good handle on how contracts work, but if you are looking for more resources, we recommend looking at the contracts section of our tutorial.

[Yenyun035]

@carolynzech Appreciate it for your response! I just tried to add contracts and write a corresponding harness as you stated. However, I encountered this error:

Failed to resolve checking function i8::unchecked_add because Kani currently cannot resolve path including primitive types

// originated from #[kani::proof_for_contract(i8::unchecked_add)] 

How could this be resolved?

[carolynzech]

@carolynzech Appreciate it for your response! I just tried to add contracts and write a corresponding harness as you stated. However, I encountered this error:

Failed to resolve checking function i8::unchecked_add because Kani currently cannot resolve path including primitive types

// originated from #[kani::proof_for_contract(i8::unchecked_add)] 

How could this be resolved?

@Yenyun035 Ensure that you're running Kani from the features/verify-std branch--we fixed that issue in this PR. See the instructions to build from source.

[Yenyun035]

@carolynzech Hello! Recently our team has been writing proofs for unchecked_{sub, mul, shl, shr}. Each of us has run the proofs on our end, and we ended up passing a different number of checks. For example:

• i8::unchecked_sub proof: @Yenyun035 passed 1229 checks. @lanfeima passed 167 checks.
• i8::unchecked_shl proof: @Yenyun035 passed 1191 checks. @MWDZ passed 138 checks.

What could be the reason? @Yenyun035 and @lanfeima seemed to be using the same toolchain version (nightly-09-08).

[carolynzech]

What could be the reason? @Yenyun035 and @lanfeima seemed to be using the same toolchain version (nightly-09-08).

@Yenyun035 It could be because you're running on different machines--different architectures can perhaps produce different checks. Could you check which versions of Kani and CBMC you're using?

[Yenyun035]

@carolynzech

@Yenyun035 - Mac Pro M1; Kani 0.55.0 and CBMC 6.3.1. @lanfeima - Mac Pro M3; Kani 0.55.0 and CBMC 6.3.1.

[rajathkotyal]

Hi @carolynzech , I ran the same i8::unchecked_sub proof on a : Ubuntu 22.04 Docker : Intel x86 architecture. And got only a 119 checks. With the same Kani, CBMC and Rustup toolchain versions as others.

Our very trivial speculation right now for this is the machine architecture and amount of cpu cores / RAM that is allowed by the system for the verifier to utilize, which in turn could have made cbmc perform lesser checks to accommodate the respective proofs.

To test this out, we are planning to create a Ubuntu docker image with all modules pre installed and run it on different architectures to see if we obtain different results. But if you think we are missing something, or if you have faced a similar kind of issue prior to this with other proofs, please advice. Thanks!

Versions :

[carolynzech]

@rajathkotyal I suspect that this is just caused by architecture differences. As long as you're all running the same versions of Kani and CBMC (and the same harnesses), I wouldn't worry about the different number of checks. I'd recommend focusing on writing other harnesses or contracts for now.

[Yenyun035]

Hi @carolynzech @celinval @feliperodri @zhassan-aws

When I was testing my harness for f32::to_int_unchecked, I encountered the error indicating that float_to_int_unchecked is not currently supported by Kani, as shown below. Is it possible to support it?

SUMMARY:
 ** 1 of 1277 failed (1276 undetermined)
Failed Checks: float_to_int_unchecked is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose
 File: "/Users/yew005/Docs/Academic/CMU/Fall24/practicum/verify-rust-std/library/core/src/convert/num.rs", line 30, in <f32 as convert::num::FloatToInt<i32>>::to_int_unchecked

VERIFICATION:- FAILED
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
Verification Time: 5.8839436s

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

library/core/src/convert/num.rs Line 20 to 35:

20 macro_rules! impl_float_to_int {
21     ($Float:ty => $($Int:ty),+) => {
22         #[unstable(feature = "convert_float_to_int", issue = "67057")]
23         impl private::Sealed for $Float {}
24         $(
25             #[unstable(feature = "convert_float_to_int", issue = "67057")]
26             impl FloatToInt<$Int> for $Float {
27                 #[inline]
28                 unsafe fn to_int_unchecked(self) -> $Int {
29                     // SAFETY: the safety contract must be upheld by the caller.
30                     unsafe { crate::intrinsics::float_to_int_unchecked(self) }
31                 }
32            }
33         )+
34     }
35 }

Test harness:

#[kani::proof_for_contract(f32::to_int_unchecked)]
pub fn checked_to_int_unchecked_f32() {
    let num1: f32 = kani::any::<f32>();

    let result = unsafe { num1.to_int_unchecked::<i32>() };

    assert_eq!(result, num1 as i32);
}

Contracts added to f32::to_int_unchecked (in library/core/src/num/f32.rs):

/// # Safety
///
/// The value must:
///
/// * Not be `NaN`
/// * Not be infinite
/// * Be representable in the return type `Int`, after truncating off its fractional part
/// ...
#[requires(!self.is_nan() && !self.is_infinite())]
#[requires(self >= Self::MIN && self <= Self::MAX)]
pub unsafe fn to_int_unchecked<Int>(self) -> Int
where
    Self: FloatToInt<Int>,
{ ... }

Thank you very much!