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 in int_macros.rs and uint_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::<i8>();
    let num2: i8 = kani::any::<i8>();

    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::<i16>();
    let num2: i16 = kani::any::<i16>();
        
    // 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.