Claim #1 — Verification of <core::option::Option<T> as option_ext::OptionExt<T>>::contains (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

<core::option::Option<T> as option_ext::OptionExt<T>>::contains

impl<T> option_ext::OptionExt<T> for Option<T>
pub fn contains<U>(self: &Self, x: &U) -> bool where U: PartialEq<T>

Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

This claim has no explanation of its own. Read the report Overview, and treat the formal statement below as authoritative. See Concepts and terminology.

Preconditions

For each selected Some payload, U::eq(candidate, payload) succeeds and returns a Boolean reflecting the specified relation.

Formal statement

OptionExtContracts.contains_relation_correct

for allT : Type u_1

for allU : Type u_2

for alleqInst : Aeneas.Std.core.cmp.PartialEq U T

for allrelation : U → T → Prop

for allopt : Option T

for allx : U

assumeselected : ∀ (t : T), opt = Option.some t → ∃ b, eqInst.eq x t = Aeneas.Std.Result.ok b ∧ (b = Bool.true ↔ relation x t)

then∃ out, OptionExtContracts.contains eqInst opt x = Aeneas.Std.Result.ok out ∧ (out = Bool.true ↔ match opt, selected with | Option.none, selected => False | Option.some t, selected => relation x t)

Complete Lean proposition

∀ {T : Type u_1} {U : Type u_2} (eqInst : Aeneas.Std.core.cmp.PartialEq.{u_2, u_1} U T) (relation : U → T → Prop)
  (opt : Option.{u_1} T) (x : U)
  (selected :
    ∀ (t : T),
      @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →
        @Exists.{1} Bool fun (b : Bool) =>
          And
            (@Eq.{1} (Aeneas.Std.Result.{0} Bool) (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)
              (@Aeneas.Std.Result.ok.{0} Bool b))
            (Iff (@Eq.{1} Bool b Bool.true) (relation x t))),
  @Exists.{1} Bool fun (out : Bool) =>
    And
      (@Eq.{1} (Aeneas.Std.Result.{0} Bool) (@OptionExtContracts.contains.{u_1, u_2} T U eqInst opt x)
        (@Aeneas.Std.Result.ok.{0} Bool out))
      (Iff (@Eq.{1} Bool out Bool.true)
        (@OptionExtContracts.contains_relation_correct.match_1.{u_1, u_2, 1} T U eqInst relation x
          (fun (opt : Option.{u_1} T)
              (selected :
                ∀ (t : T),
                  @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →
                    @Exists.{1} Bool fun (b : Bool) =>
                      And
                        (@Eq.{1} (Aeneas.Std.Result.{0} Bool)
                          (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)
                          (@Aeneas.Std.Result.ok.{0} Bool b))
                        (Iff (@Eq.{1} Bool b Bool.true) (relation x t))) =>
            Prop)
          opt selected
          (fun
              (selected :
                ∀ (t : T),
                  @Eq.{u_1 + 1} (Option.{u_1} T) (@Option.none.{u_1} T) (@Option.some.{u_1} T t) →
                    @Exists.{1} Bool fun (b : Bool) =>
                      And
                        (@Eq.{1} (Aeneas.Std.Result.{0} Bool)
                          (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)
                          (@Aeneas.Std.Result.ok.{0} Bool b))
                        (Iff (@Eq.{1} Bool b Bool.true) (relation x t))) =>
            False)
          fun (t : T)
            (selected :
              ∀ (t_1 : T),
                @Eq.{u_1 + 1} (Option.{u_1} T) (@Option.some.{u_1} T t) (@Option.some.{u_1} T t_1) →
                  @Exists.{1} Bool fun (b : Bool) =>
                    And
                      (@Eq.{1} (Aeneas.Std.Result.{0} Bool)
                        (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t_1)
                        (@Aeneas.Std.Result.ok.{0} Bool b))
                      (Iff (@Eq.{1} Bool b Bool.true) (relation x t_1))) =>
          relation x t))

Theorem source at recorded commit · Recorded check

Referenced definitions (up to 100 direct references)

Aeneas.Std.core.cmp.PartialEq · Aeneas.Std.Core.Cmp
Option · Init.Prelude
Eq · Init.Prelude
Option.some · Init.Prelude
Exists · Init.Core
Bool · Init.Prelude
And · Init.Prelude
Aeneas.Std.Result · Aeneas.Std.Primitives
Aeneas.Std.core.cmp.PartialEq.eq · Aeneas.Std.Core.Cmp
Aeneas.Std.Result.ok · Aeneas.Std.Primitives
Iff · Init.Core
Bool.true · Init.Prelude
OptionExtContracts.contains
OptionExtContracts.contains_relation_correct.match_1 · Contracts
Option.none · Init.Prelude
False · Init.Prelude

Mapping: manual. Translation was not rerun by this recording.

Evidence

https://github.com/MasWag/crate-proofs/blob/d515d59559746c5bbca74d3e33626cc814519a48/option-ext/0.2.0/aeneas/profiles/default/proofs/Contracts.lean#L38-L49

What is trusted

From the report

The results depend on the Rust-to-Lean translation, Lean, and the relevant Aeneas models. In particular, the shared-reference PartialEq model forwards the candidate and contained value to the underlying comparison in that order; correspondence of that model to Rust is trusted. The contracts do not establish that an arbitrary user comparison or callback succeeds or satisfies a chosen relation. The map_or2 proof includes the extracted standard Option::map_or body.

Technical limitations

From the report

The contains and map_or2 bodies are from the unchanged 0.2.0 release. For map_or_else2, verification uses a source adaptation: its call to Option::map_or_else(default, f) is replaced with a direct match that calls f(value) for Some(value) and default() for None. This was needed because the original delegated zero-argument callback could not be translated by the pinned Aeneas toolchain. An exact source check identifies this as the only implementation change, and source review supports the correspondence of the two branch selections; equivalence to the release body is not formally proved.

The result equations are not a trace or side-effect call-count proof. They do not establish arbitrary callback effects, interior-mutability behavior, aliasing properties, or behavior of panicking destructors outside the translation model. Success depends on the selected operation, so this is not unconditional panic freedom.

Tool limitations

Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Read and join the discussion on the report →