Determining the valid value range for *const T::offset's count parameter.

[stogaru]

To write a function contract for this function, we need to add a precondition that defines a range for the count parameter. As per the documentation, the *const T::offset function guarantees the safety of the resulting pointer only when the self and the result are in bounds of that allocated object. Therefore, count should be bounded such that self.addr() +/- count is within the start and end addresses of the allocated object.
Is there a way to infer the start and end addresses of the allocated object solely based on the input pointer? Or can we check if self and result are pointing to the same allocation object?

[stogaru]

As per the meeting, the can_write memory predicate added in this PR can be helpful for positive offsets. So, preconditions for functions like add and byte_add can be implemented in the harness. Support for negative offsets has to be implemented.

[feliperodri]

As we discussed offline, we might need new memory predicates to extract some extra information from raw pointers in this case. Let's take a look at this example for instance,

use std::mem;

#[kani::proof]
fn main() {
    // Create a boxed value (heap allocated)
    let boxed_value = Box::new([10, 20, 30, 40, 50]);

    // Get a raw pointer to the boxed value
    let ptr: *const i32 = &*boxed_value as *const i32;

    // Use `size_of_val` to get the size of the allocated object
    let size = mem::size_of_val(&*boxed_value);
    // Get the size in bytes of the type that `ptr` points to.
    let type_size = mem::size_of::<i32>();

    // Output the size of the allocated object
    assert_eq!(size, 20); // [i32; 5] is 5 elements * 4 bytes each = 20 bytes

    // Non-deterministic `count`
    let count: isize = kani::any();
    // Preconditions for `count`
    kani::assume(count > 0 && count < ((size/type_size) as isize));
    unsafe {
        // Use `offset` to move the pointer
        let _new_ptr = ptr.offset(count);
    }
}

Here we are using size_of_val to get the size of the allocated object. Then, we are using size_of to capture the size of the type. However, there is an issue of using this approach in other cases. For example, the offset method requires T: Sized, so writing a contract in this case one must know that size_of and size_of_val will behave the same way.

My recommendation is to write the contracts for this challenge to all functions we can write it today. That way, we will have a list of all functions that we may not be able to verify because we need specific information from the pointer. Let's document everything that we have tried using standard Rust in these contracts (e.g., size_of_val). Let's also propose what a collection of predicates with raw pointer information would look like.

[celinval]

I believe this can be accomplished now with the new same_allocation predicate, right? You can use wrapping_sub to generate the resulting pointer, and check whether it belongs to the same allocation as the initial pointer.

Note that if count is 0, this method is safe.