Ability to refer to pre-/post-conditions of closures in specifications

[coeff-aij]

Description

In order to support the formal verification of higher-order functions (e.g., Option::map, Option::unwrap_or_else), it is necessary to refer to the pre-conditions and post-conditions of the closures passed as arguments within the #[thrust::requires] and #[thrust::ensures] attributes.

Currently, there is no established syntax to express that a function's correctness depends on the contract of a provided function object f.
I propose adding a syntax like f.precondition(...) and f.postcondition(...)(or a similar mechanism) to represent these contracts.

Example

#[thrust::requires(true)]
#[thrust::ensures(
    (self == std::option::Option::<T0>::None() && result == self)
    || (exists i: T0. self == std::option::Option::<T0>::Some(i) && (
            f.precondtition(i)
            && exists j: T0. f.postcondition(i, j)
            && result == std::option::Option::<T0>::Some(j)
        ))
)]
pub const fn map<U, F>(self, f: F) -> Option<U>
where
    F: [const] FnOnce(T) -> U + [const] Destruct,
{
    match self {
        Some(x) => Some(f(x)),
        None => None,
    }
}

#[thrust::requires(true)]
#[thrust::ensures(
    (self == std::option::Option::<T0>::None() && result == exists i: T0.
        f.precondtition() && f.postcondition(i)
        && result = std::option::Option::<T0>::Some(i)
    )
    || (exists j: T0. self == std::option::Option::<T0>::Some(j) && result == j)
)]
pub const fn unwrap_or_else<F>(self, f: F) -> T
where
    F: [const] FnOnce() -> T + [const] Destruct,
{
    match self {
        Some(x) => x,
        None => f(),
    }
}