Claim #1 — Verification of <core::option::Option<T> as option_ext::OptionExt<T>>::map_or_else2 (with creusot 0.13.0)
<core::option::Option<T> as option_ext::OptionExt<T>>::map_or_else2
impl<T> option_ext::OptionExt<T> for Option<T>
pub fn map_or_else2<U, F: FnOnce(T) -> U, D: FnOnce() -> U>(self: Self, f: F, default: D) -> UTool: creusot 0.13.0
Preconditions
(match self { None => default.precondition(()), Some(t) => f.precondition((t,)) })
Evidence
What is trusted
From the report
The unchanged method delegates to Option::map_or_else. Its proof relies on Creusot's standard specifications for that operation and FnOnce, as well as the verifier and its logical models. The standard option specification describes the same selected branch and closure postcondition; this run does not verify the Rust standard-library implementation. Callback correctness is supplied by its own contract, not established for arbitrary user closures here.
Technical limitations
From the report
This is a partial-correctness result: the postcondition holds when the call returns, and the proof does not establish termination or unconditional safety from panics in callbacks. It does not establish arbitrary external effects, exact runtime call counts, general aliasing properties, allocation behavior, or arbitrary destructor panics.
The verified source retains the release's executable self.map_or_else(default, f) body and runtime signature. It adds verification annotations and an erased logical trait observation; the observation is the identity for Option<T>. The other two methods are excluded from this Creusot configuration but remain present in native builds. This report does not cover those methods or third-party implementations of the trait.
Tool limitations
Verification is relative to the supplied specifications and trusted contracts. Results apply to the compilation target used for verification. The standard-library specifications do not exclude all panics: Vec capacity overflow in operations such as push, insert, and extend is not ruled out, including for vectors of zero-sized types. Out-of-memory failures are also outside the guarantees. The standard vec! macro is unsupported; verified code must use the Creusot replacement where needed. Reference: https://github.com/creusot-rs/creusot/blob/v0.13.0/guide/src/limitations.md