Function spawn

pub fn spawn<F, T>(f: F) -> JoinHandle<T>where
    F: FnOnce(Ghost<Tokens<'_>>) -> T + Send + 'static,
    T: Send + 'static,

Expand description

Creusot wrapper around std::thread::spawn.

The only difference is that the closure gives access to a fresh token object

requires

forall<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) ==> f.precondition((t,))

ensures

exists<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) && forall<r> result.valid_result(r) ==> f.postcondition_once((t,), r)

spawn