Report #18 — option-ext 0.2.0 map_or_else2 return behavior

1 verified claim · 0 findings

Recorded by the author; proofs.rs has not re-run it. How to read a report

MasWag · 2026-11-03 13:47 UTC

Revision v1

Overview

For OptionExt::map_or_else2 on Option<T>, the contract requires the selected callback's precondition: the default callback for None, or the mapping callback applied to the contained value for Some. When the method returns, its result satisfies that callback's FnOnce postcondition. The contract also records resolution of the unused consumed closure in Creusot's model. It imposes no invocation precondition on that closure.

Thus, if the selected callback's postcondition specifies a particular result, the method's returned value has that result. The trait contract and its refinement for Option<T> use a checked logical observation of the receiver.

Findings (0)

No findings reported.

APIs (1)

Trait implementations

`impl option_ext::OptionExt<T> for core::option::Option<T>`

pub fn map_or_else2<U, F: FnOnce(T) -> U, D: FnOnce() -> U>(self: Self, f: F, default: D) -> U

Claim #1

Evidence

https://github.com/MasWag/crate-proofs/tree/2ffc99cb6b4d0533c44773bf0b9e1de33d70f90b

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/MasWag/crate-proofs report-18-source-1
git -C report-18-source-1 checkout --detach 2ffc99cb6b4d0533c44773bf0b9e1de33d70f90b
git -C report-18-source-1 submodule update --init --recursive --checkout
cd report-18-source-1/option-ext/0.2.0/creusot

cargo creusot --no-cache --why3session

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 2 checks passed · 0 failed

2026-11-03T13:46:18.509509+00:00 · 16.2 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
vc_map_or_else2_Option_T `option_ext::<core::option::Option<T> as option_ext::OptionExt<T>>::map_or_else2` `option-ext/0.2.0/creusot/src/impl.rs:27`	Passed	Claim #1
vc_map_or_else_T `option_ext::<core::option::Option<T> as option_ext::OptionExt<T>>::map_or_else2` `option-ext/0.2.0/creusot/src/impl.rs:27`	Passed	Claim #1

Execution details

Started: 2026-11-03T13:46:18.509509+00:00
Finished: 2026-11-03T13:46:34.716105+00:00
Platform: macos aarch64
Rust compiler: rustc 1.98.0-nightly (91fe22da8 2026-06-21) binary: rustc commit-hash: 91fe22da8084a1c9e993d78d4a56f22ab8396236 commit-date: 2026-06-21 host: aarch64-apple-darwin release: 1.98.0-nightly LLVM version: 22.1.7
Working directory: option-ext/0.2.0/creusot
Environment overrides: None recorded
Git repository: https://github.com/MasWag/crate-proofs
Git commit: 2ffc99cb6b4d0533c44773bf0b9e1de33d70f90b

Diagnostics & logs

=== stdout ===
Proved (3 files) ✔

=== stderr ===
   Compiling proc-macro2 v1.0.107
   Compiling quote v1.0.47
   Compiling libc v0.2.191
   Compiling unicode-ident v1.0.27
   Compiling getrandom v0.4.3
   Compiling cfg-if v1.0.5
   Compiling syn v2.0.119
   Compiling uuid v1.29.0
   Compiling pearlite-syn v0.13.0 (https://github.com/creusot-rs/creusot?rev=318615be3b8bbc60d1f6d52469ba5c0bdebed4f1#318615be)
   Compiling creusot-std-proc v0.13.0 (https://github.com/creusot-rs/creusot?rev=318615be3b8bbc60d1f6d52469ba5c0bdebed4f1#318615be)
    Checking creusot-std v0.13.0 (https://github.com/creusot-rs/creusot?rev=318615be3b8bbc60d1f6d52469ba5c0bdebed4f1#318615be)
    Checking option-ext v0.2.0 (./option-ext/0.2.0/creusot)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 12.51s

Environment

The selected workspace uses option-ext 0.2.0, unpatched Creusot 0.13.0 and Rust nightly-2026-06-22 on aarch64-apple-darwin. The workspace's scripts/verify.sh runs the verification procedure; its source correspondence check, independent specification, tool lock and results record the supporting evidence. Native tests are separate from the formal proof.

What is trusted

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

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

Updated 2026-09-24 05:03 UTC

creusot 0.13.0 — version details

Dependencies (0)

No direct dependencies.

Comments (0)

No comments.