Function contract doesn't propagate `const` function bodies correctly

[thanhnguyen-aws]

I tried this code:

#[ensures(|result| result.as_usize().is_power_of_two())]
pub const fn Align_of<T>() -> Self {
    // This can't actually panic since type alignment is always a power of two.
    const { Alignment::new(mem::align_of::<T>()).unwrap() }
}

#[kani::proof_for_contract(Alignment::of)]
pub fn check_of_i32() {
    let _ = Align_of::<i32>();
}

and

#[kani::proof]
pub fn check_of_i32() {
    let a = Align_of::<i32>();
    assert!(a.as_usize().is_power_of_two());
}

using the following command line invocation:

kani src/main.rs  -Z function-contracts

with Kani version: 0.59.0

I expected to see this happen: The same results for both harnesses.

Instead, this happened: The kani::proof_for_contract failed but the kani::proof succeed

[thanhnguyen-aws]

Another example: This harness fails:

#[kani::ensures(|result : &NonNull<T>| !result.as_ptr().is_null())]
pub const fn from_raw_parts_test<T>(
    data_pointer: NonNull<impl ptr::Thin>,
    metadata: <T as ptr::Pointee>::Metadata,
) -> NonNull<T> {
    // SAFETY: The result of `ptr::from::raw_parts_mut` is non-null because `data_pointer` is.
    unsafe {
        NonNull::new_unchecked(ptr::from_raw_parts_mut(data_pointer.as_ptr(), metadata))
    }
}

#[kani::proof_for_contract(from_raw_parts_test)]
pub fn non_null_check_from_raw_parts() {
    let dangling_ptr = NonNull::<i8>::dangling();
    let zero_length = from_raw_parts_test::<()> (dangling_ptr, ());
}

But it will succeed if I add this precondition:

#[kani::requires(!data_pointer.as_ptr().is_null())]

However, this precondition is not necessary because this harness succeeds:

#[kani::proof]
pub fn non_null_check_from_raw_parts() {
    let dangling_ptr = NonNull::<i8>::dangling();
    assert!(!dangling_ptr.as_ptr().is_null());
    let zero_length = from_raw_parts_test::<()> (dangling_ptr, ());
}

And this harness succeeds too:

#[kani::proof]
pub fn non_null_check_from_raw_parts() {
    let dangling_ptr = NonNull::<i8>::dangling();
    let zero_length = from_raw_parts_test::<()> (dangling_ptr, ());
    assert!(!zero_length.as_ptr().is_null());
}

[tautschnig]

For the record, here is a full reproducer of the const vs no-const disparity:

#![feature(ptr_alignment_type)]

use std::ptr::Alignment;
use std::mem;

#[kani::ensures(|result| result.as_usize().is_power_of_two())]
pub const fn Align_of<T>() -> Alignment {
    // This can't actually panic since type alignment is always a power of two.
    const { Alignment::new(mem::align_of::<T>()).unwrap() }
}

#[kani::ensures(|result| result.as_usize().is_power_of_two())]
pub const fn Align_of_no_const<T>() -> Alignment {
    // This can't actually panic since type alignment is always a power of two.
    Alignment::new(mem::align_of::<T>()).unwrap()
}

#[kani::proof_for_contract(Align_of)]
pub fn check_of_i32() {
    let _ = Align_of::<i32>();
}

#[kani::proof_for_contract(Align_of_no_const)]
pub fn check_of_i32_no_const() {
    let _ = Align_of_no_const::<i32>();
}

[tautschnig]

Further note: we already have https://github.com/model-checking/kani/issues/3864 and I wonder whether the second example provided above is the same problem?

[thanhnguyen-aws]

Another example

#[kani::requires(true)]
pub const unsafe fn byte_add_n<T>(s : NonNull<T>, count: usize) -> NonNull<T> {
    unsafe { NonNull::new_unchecked( s.as_ptr().byte_add(count) ) }
}

#[kani::proof_for_contract(byte_add_n)]
pub fn non_null_byte_add_dangling_proof() {
    let ptr = NonNull::<i32>::dangling();
    assert!(ptr.as_ptr().addr() == 4);
    assert!(ptr.as_ptr().addr() <= (isize::MAX as usize) );
    unsafe {
        let _ = byte_add_n(ptr,0);
    }
}

Output: (note that it fail at the assertion before the function call)

Failed Checks: assertion failed: ptr.as_ptr().addr() == 4
 File: "src/main.rs", line 234, in non_null_byte_add_dangling_proof

But this one succeed:

#[kani::proof]
pub fn dangling_addr() {
    let ptr = NonNull::<i32>::dangling();
    assert!(ptr.as_ptr().addr() == 4);
    assert!(ptr.as_ptr().addr() <= (isize::MAX as usize) );
    unsafe {
        let _ = byte_add_n(ptr,0);
    }
}

[carolynzech]

I'm inclined to keep this issue focused on fixing the const body issue for alignment, i.e. fixing https://github.com/model-checking/kani/issues/3905#issuecomment-2682080521. It's possible that each of these examples trace back to the same bug (I hope so!) but we don't have enough evidence of that at this point.

[vonaka]

Just for the record, I believe this boils down to the following:

#[derive(PartialEq)]
enum Enum {
    First,
    Second,
}

#[kani::ensures(|result| *result == Enum::First)]
const fn first() -> Enum {
    const { Enum::First }
}

#[kani::ensures(|result| *result == Enum::Second)]
const fn second() -> Enum {
    Enum::Second
}

// VERIFICATION:- FAILED
// Failed Checks: |result| *result == Enum::First
#[kani::proof_for_contract(first)]
pub fn check_first() {
    let _ = first();
}

// VERIFICATION:- SUCCESSFUL
#[kani::proof_for_contract(second)]
pub fn check_second() {
    let _ = second();
}

Interestingly, if the enum had only one variant, check_first would have succeeded.

[tautschnig]

Given the example provided by @vonaka I am wondering whether this is another case of the problem discussed in https://github.com/model-checking/kani/issues/4009, i.e., a problem caused by (unwanted!) non-deterministic initialisation?