Enable thorough Rust safety verification

[celinval]

Requested feature: Enable users to verify function safety for unsafe functions and safe abstractions
Use case: Prove program safety by applying modular verification.

Rust safety relies on strong type safety checked by the compiler together with proper safety encapsulation. Unsafe code should be local and wrapped in safe functions that meet type safety invariant to avoid safety conditions to propagate to the entire system.

This encapsulation has 3 components that should be verifiable using Kani:

1. Safe abstractions: These are functions that use unsafe code as part of their implementation but they don't require any extra safety condition beyond type safety. I.e.: It should never trigger UB as long as all variables reachable from the function respect their type safety. Furthermore, it should leave all variables in a safe state (including cases where the function panics if unwinding is enabled).
2. Unsafe functions: Unsafe functions have extra safety requirements that go beyond type safety. In order to validate safety of a program, the callee must abide to the safety contracts of the unsafe function (which should be properly documented).
3. Type safety invariant: Types may contain extra safety requirements that go beyond their components safety. For example, Vec contains a raw pointer and a length field that must be kept in sync. The type safety invariant should be met at the boundary of safe functions (some might argue public safe functions only).

Thus, in order to facilitate safety verification, Kani should provide the following:

• Separate safety contract from correctness / panic freedom #3567
• UB checks should fail verification for harnesses annotated with #[should_panic] #3571
• Create a new #[proof_for_safety(fn)] #3579
  • Note that for this mode Kani should be able to just assume that no panic can happen.

Test case:

Here is a dummy example, let's say we have the following Buffer struct and a buggy read_chunk method:

extern crate kani;
use kani::mem::can_dereference;
use kani::{requires};
use std::slice::from_raw_parts;

struct Buffer {
    len: usize,
    data: *mut u8,
}

impl Buffer {
    /// Read `n` bytes.
    ///
    /// This code will panic if the buffer does not contain `n` bytes.
    #[requires(bytes.checked_add(index).map_or(false, |sum| self.len > sum))]
    pub fn read_chunk(&self, index: usize, bytes: usize) -> &[u8] {
        // Panic if the index + bytes is out of bounds.
        if self.len < index + bytes { // -----> Can overflow
            panic!("Buffer size is too small")
        }
        unsafe {
            let start = self.data.add(index);
            from_raw_parts(start, bytes)
        }
    }
}

The first step would be to verify the contract:

/// Check that the code will not panic if the contract is respected.
#[kani::proof_for_contract(Buffer::read_chunk)]
fn check_read_chunk() {
    let len = kani::any_where(|l: &usize| *l <= 20);
    let mut array: [u8; 20] = kani::any();
    let data = unsafe { array.as_mut_ptr().add(20-len) };
    let buf = Buffer { len, data };
    let _ = buf.read_chunk(kani::any(), kani::any());
}

However, that is not enough to ensure the function safety. Verifying the contract will restrict the search space of the harness. A safe abstraction should never trigger UB as long all variables are safe representations of their type.

In order to check that, users need to run their function with arbitrary safe values of their inputs (and static objects). Note that panicking is OK in this scenario. Thus, ideally, users should be able to use the following harness to check for safety.

/// Run the same harness as the proof for contract. Note that `proof_for_safety` will only fail if a UB is detected or
/// if the function leaves any variable in an unsafe state.
#[kani::proof_for_safety]
fn check_read_chunk_no_ub() {
    check_read_chunk();        
}