Tracking issue for async/await in Kani (feature async-lib)

[fzaiser]

Requested feature: async/await
Use case: to support popular libraries like tokio
Link to relevant documentation (Rust reference, Nomicon, RFC):

• async/await primer
• RFC proposing async/await (partially outdated)

Test case

use std::{
    future::Future,
    pin::Pin,
    task::{Context, RawWaker, RawWakerVTable, Waker},
};

#[kani::proof]
fn main() {
    let result = block_on(async { 42 }, 1);
    assert_eq!(result, Some(42));
}

fn block_on<F: Future>(mut fut: F, limit: usize) -> Option<<F as Future>::Output> {
    let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
    let cx = &mut Context::from_waker(&waker);
    for _ in 0..limit {
        let pinned = unsafe { Pin::new_unchecked(&mut fut) };
        match pinned.poll(cx) {
            std::task::Poll::Ready(res) => return Some(res),
            std::task::Poll::Pending => continue,
        }
    }
    None
}

const NOOP_RAW_WAKER: RawWaker = {
    unsafe fn clone_waker(_: *const ()) -> RawWaker {
        NOOP_RAW_WAKER
    }
    unsafe fn wake(_: *const ()) {}
    unsafe fn wake_by_ref(_: *const ()) {}
    unsafe fn drop_waker(_: *const ()) {}
    RawWaker::new(
        std::ptr::null(),
        &RawWakerVTable::new(clone_waker, wake, wake_by_ref, drop_waker),
    )
};

Progress

This issue is to track progress on the implementation:

• support generators (PR Implement support for generators #1378)
• support async/await (PR Add basic support for async/.await #1414)
• add kani::block_on to a new kani::futures library (PR Add a kani::futures library containing block_on #1427)
• allow #[kani::async_proof] on async functions (no need for poll_repeat in the above example). This could be later extended to allow different runtimes. (PR Implement #[kani::async_proof] attribute #1430)
• Adding async verification examples to the Kani test suite #1663: add tests from popular libraries: futures-rs, async_std, tokio
• think about how to support task spawning, e.g. tokio::spawn
• Document support for thread local and for async/.await #1482
• Warn if async harness does not have an unwind bound #1517