Report #16 — option-ext 0.2.0 option branch behavior

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

3 verified claims · 0 findings

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

MasWag · 2026-11-03 13:04 UTC

Revision v1

Overview

These contracts describe the three OptionExt operations for arbitrary option values and generic callback types. For contains, None returns false; Some(value) returns the result of comparing the candidate to value, in that order. If the selected comparison succeeds and reflects a chosen relation, the returned Boolean reflects that relation. No equality laws are assumed.

For map_or2, None returns the supplied default and Some(value) returns the mapping result, provided the selected mapping succeeds. The default is a value constructed by the caller before the method is entered. For the adapted map_or_else2 body described below, None returns the default callback's result and Some(value) returns the mapping callback's result, provided the selected callback succeeds. The unused callback needs no success assumption. The branch equations also preserve a selected comparison or callback failure in the translation.

Findings (0)

No findings reported.

APIs (3)

Trait implementations

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

pub fn contains<U>(self: &Self, x: &U) -> bool where U: PartialEq<T>

Claim #1

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

Claim #2

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

Claim #3

Evidence

https://github.com/MasWag/crate-proofs/tree/d515d59559746c5bbca74d3e33626cc814519a48

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/MasWag/crate-proofs report-16-source-1
git -C report-16-source-1 checkout --detach d515d59559746c5bbca74d3e33626cc814519a48
git -C report-16-source-1 submodule update --init --recursive --checkout
cd report-16-source-1/option-ext/0.2.0/.work/build/default/aarch64-apple-darwin/proofs

lake build +AdaptedContracts +Contracts

printf '%s' 'import Aeneas
import AdaptedContracts
import Contracts
set_option pp.all true
set_option pp.universes true
set_option pp.explicit true
set_option pp.fullNames true
set_option pp.notation false
set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 10000000
-- proofs.rs adapter for Lean 4.35.0 / Aeneas be86ab0f.
-- Uses Lean'\''s environment, Meta telescope and pretty-printer, never source parsing.
open Lean Meta Elab Command
namespace ProofsProbe
meta def moduleOf (env : Environment) (n : Name) : String :=
  match env.getModuleIdxFor? n with
  | some idx => env.header.moduleNames[idx.toNat]!.toString
  | none => ""
meta def pretty (e : Expr) : MetaM String := do
  let s := (← ppExpr e).pretty
  if s.contains '\''⋯'\'' then
    throwError "Lean display contains an omission marker (or literal ⋯); refusing an incomplete proposition"
  if s.utf8ByteSize > 1000000 then throwError "Proposition exceeds 1,000,000-byte recording limit"
  return s
-- The full statement stays explicit; the inspection view uses Lean notation.
meta def readable (e : Expr) : MetaM String :=
  withOptions (fun o =>
    let o := o.setBool `pp.all false
    let o := o.setBool `pp.explicit false
    let o := o.setBool `pp.universes false
    o.setBool `pp.notation true) (pretty e)
-- Only a constant'\''s own tag grants a link; names in plain text are never guessed.
partial def segments (code : Widget.CodeWithInfos) (ref : Option Name := none) : Array Json :=
  match code with
  | .text text => #[Json.mkObj (([("text", toJson text)]) ++
      (ref.toList.map fun n => ("ref", toJson n.toString)))]
  | .append parts => parts.foldl (fun acc part => acc ++ segments part ref) #[]
  | .tag info part =>
    let ref := match info.info.val.info with
      | .ofTermInfo ti => ti.expr.constName?
      | _ => none
    segments part ref
meta def readableFields (key : String) (e : Expr) : MetaM (List (String × Json)) := do
  let text ← readable e
  let base := [(key, toJson text)]
  try
    let code ← withOptions (fun o =>
      let o := o.setBool `pp.all false
      let o := o.setBool `pp.explicit false
      let o := o.setBool `pp.universes false
      let o := o.setBool `pp.notation true
      o.setBool `pp.tagAppFns true) (Widget.ppExprTagged e)
    let parts := segments code
    let joined := String.join (parts.toList.map fun j =>
      (j.getObjValAs? String "text").toOption.getD "")
    if joined != text || parts.size > 10000 || joined.utf8ByteSize > 1000000 then
      return base
    return base ++ [(key ++ "_segments", toJson parts)]
  catch _ => return base
meta def inspect (n : Name) (ty : Expr) (manual : Bool) : MetaM (Option Json) := do
  let env ← getEnv
  forallTelescope ty fun xs conclusion => do
    let programExpr ← try
      let normalized ← Aeneas.Utils.normalizeLetBindings conclusion
      let (expr, _) ← Aeneas.Step.getStepSpecFunArgsExpr normalized
      pure (some expr)
    catch _ => pure none
    if programExpr.isNone && !manual then return none
    let full ← pretty ty
    let program ← match programExpr with
      | some expr => pure (toJson (← readable expr))
      | none => pure Json.null
    let head := toJson (programExpr.bind (·.getAppFn.constName?) |>.map Name.toString)
    let mut binders := #[]
    for x in xs do
      let d ← x.fvarId!.getDecl
      let prop ← isProp d.type
      binders := binders.push (Json.mkObj ((← readableFields "type" d.type) ++ [
        ("name", toJson d.userName.toString),
        ("kind", toJson (if d.binderInfo.isInstImplicit then "instance" else if prop then "hypothesis" else "variable")),
        ("binder", toJson (if d.binderInfo.isInstImplicit then "instance" else if d.binderInfo.isExplicit then "explicit" else "implicit"))]))
    if binders.size > 1000 then throwError "More than 1000 binders"
    let some ranges ← findDeclarationRanges? n | throwError "Missing theorem source range: {n}"
    let axioms ← Lean.collectAxioms n
    let constants := ty.getUsedConstants
    let mut definitions := #[]
    for nm in constants.extract 0 100 do
      let ranges ← findDeclarationRanges? nm
      definitions := definitions.push (Json.mkObj [
        ("name", toJson nm.toString), ("module", toJson (moduleOf env nm)),
        ("source", match ranges with
          | some r => Json.mkObj [("first_line", toJson r.range.pos.line), ("last_line", toJson r.range.endPos.line)]
          | none => Json.null)])
    return some (Json.mkObj ((← readableFields "conclusion" conclusion) ++ [
      ("version", toJson (1 : Nat)), ("theorem", toJson n.toString),
      ("module", toJson (moduleOf env n)), ("statement", toJson full),
      ("binders", toJson binders),
      ("program", program), ("program_head", head),
      ("axioms", toJson (axioms.map Name.toString)),
      ("first_line", toJson ranges.range.pos.line), ("last_line", toJson ranges.range.endPos.line),
      ("definitions", toJson definitions), ("definitions_truncated", toJson (decide (constants.size > 100))),
      ("translation_rerun", toJson false)]))
end ProofsProbe

run_cmd do
  let manual : Array Name := #[`OptionExtContracts.contains_relation_correct, `OptionExtContracts.map_or2_correct, `OptionExtAdaptedContracts.map_or_else2_correct]
  let localModules : Array String := #[]
  let roots : Array Name := #[]
  let env ← getEnv
  let mut closure : Array Name := #[]
  let mut pending := roots.toList
  while !pending.isEmpty do
    let m := pending.head!
    pending := pending.tail!
    if !closure.contains m then
      closure := closure.push m
      if let some idx := env.header.moduleNames.findIdx? (· == m) then
        pending := (env.header.moduleData[idx]!.imports.toList.map (·.module)) ++ pending
  let scope := closure.filter (fun m => localModules.contains m.toString)
  for n in manual do
    match env.find? n with
    | some (.thmInfo _) => pure ()
    | _ => throwError "Expected a theorem: {n}"
  for (n, ci) in env.constants.toList do
    let explicit := manual.contains n
    if explicit || scope.contains (ProofsProbe.moduleOf env n).toName then
      if let .thmInfo th := ci then
        let result ← liftTermElabM <| ProofsProbe.inspect n th.type explicit
        if let some value := result then
          liftIO <| IO.println ("proofs.rs:formal:" ++ value.compress)

run_cmd do
  let theorem_name := `OptionExtContracts.contains_relation_correct
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OptionExtContracts.contains_relation_correct"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OptionExtContracts.contains_relation_correct: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OptionExtContracts.contains_relation_correct"

run_cmd do
  let theorem_name := `OptionExtContracts.map_or2_correct
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OptionExtContracts.map_or2_correct"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OptionExtContracts.map_or2_correct: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OptionExtContracts.map_or2_correct"

run_cmd do
  let theorem_name := `OptionExtAdaptedContracts.map_or_else2_correct
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OptionExtAdaptedContracts.map_or_else2_correct"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OptionExtAdaptedContracts.map_or_else2_correct: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OptionExtAdaptedContracts.map_or_else2_correct"
' | lake env lean --stdin

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 · 3 checks passed · 0 failed

2026-11-03T13:03:16.830847+00:00 · 21.3 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem OptionExtContracts.contains_relation_correct; axioms limited to propext, Classical.choice, Quot.sound `OptionExtContracts.contains_relation_correct`	Passed	Claim #1
Lean checked theorem OptionExtContracts.map_or2_correct; axioms limited to propext, Classical.choice, Quot.sound `OptionExtContracts.map_or2_correct`	Passed	Claim #2
Lean checked theorem OptionExtAdaptedContracts.map_or_else2_correct; axioms limited to propext, Classical.choice, Quot.sound `OptionExtAdaptedContracts.map_or_else2_correct`	Passed	Claim #3

Execution details

Started: 2026-11-03T13:03:16.830847+00:00
Finished: 2026-11-03T13:03:38.107883+00:00
Platform: macos aarch64
Rust compiler: rustc 1.94.1 (e408947bf 2026-03-25) binary: rustc commit-hash: e408947bfd200af42db322daf0fadfe7e26d3bd1 commit-date: 2026-03-25 host: aarch64-apple-darwin release: 1.94.1 LLVM version: 21.1.8
Working directory: option-ext/0.2.0/.work/build/default/aarch64-apple-darwin/proofs
Environment overrides: None recorded
Git repository: https://github.com/MasWag/crate-proofs
Git commit: d515d59559746c5bbca74d3e33626cc814519a48

Diagnostics & logs

=== stdout ===
✔ [1796/1799] Built OptionExtAdapted (1.5s)
✔ [1797/1799] Built OptionExt (1.5s)
✔ [1798/1799] Built AdaptedContracts (1.7s)
✔ [1799/1799] Built Contracts (1.7s)
Build completed successfully (1799 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"U","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"F","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"D","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"explicit","kind":"variable","name":"fInst","type":"Aeneas.Std.core.ops.function.FnOnce F T U","type_segments":[{"ref":"Aeneas.Std.core.ops.function.FnOnce","text":"Aeneas.Std.core.ops.function.FnOnce"},{"text":" "},{"text":"F"},{"text":" "},{"text":"T"},{"text":" "},{"text":"U"}]},{"binder":"explicit","kind":"variable","name":"dInst","type":"Aeneas.Std.core.ops.function.FnOnce D Unit U","type_segments":[{"ref":"Aeneas.Std.core.ops.function.FnOnce","text":"Aeneas.Std.core.ops.function.FnOnce"},{"text":" "},{"text":"D"},{"text":" "},{"ref":"Unit","text":"Unit"},{"text":" "},{"text":"U"}]},{"binder":"explicit","kind":"variable","name":"self","type":"Option T","type_segments":[{"ref":"Option","text":"Option"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"f","type":"F","type_segments":[{"text":"F"}]},{"binder":"explicit","kind":"variable","name":"d","type":"D","type_segments":[{"text":"D"}]},{"binder":"explicit","kind":"variable","name":"mapping","type":"T → U","type_segments":[{"text":"T"},{"text":" → "},{"text":"U"}]},{"binder":"explicit","kind":"variable","name":"defaultValue","type":"U","type_segments":[{"text":"U"}]},{"binder":"explicit","kind":"hypothesis","name":"selected","type":"match self with\n| Option.none => dInst.call_once d () = Aeneas.Std.Result.ok defaultValue\n| Option.some x => fInst.call_once f x = Aeneas.Std.Result.ok (mapping x)","type_segments":[{"text":"match "},{"text":"self"},{"text":" with\n| "},{"ref":"Option.none","text":"Option.none"},{"text":" => "},{"text":"dInst"},{"text":"."},{"ref":"Aeneas.Std.core.ops.function.FnOnce.call_once","text":"call_once"},{"text":" "},{"text":"d"},{"text":" "},{"ref":"Unit.unit","text":"("},{"ref":"Unit.unit","text":")"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"defaultValue"},{"text":"\n| "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"x"},{"text":" => "},{"text":"fInst"},{"text":"."},{"ref":"Aeneas.Std.core.ops.function.FnOnce.call_once","text":"call_once"},{"text":" "},{"text":"f"},{"text":" "},{"text":"x"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"("},{"text":"mapping"},{"text":" "},{"text":"x"},{"text":")"}]}],"conclusion":"∃ u,\n  OptionExtAdaptedContracts.mapOrElse fInst dInst self f d = Aeneas.Std.Result.ok u ∧\n    u = OptionExtAdaptedContracts.mapLazyDefault mapping defaultValue self","conclusion_segments":[{"text":"∃ "},{"text":"u"},{"text":",\n  "},{"ref":"OptionExtAdaptedContracts.mapOrElse","text":"OptionExtAdaptedContracts.mapOrElse"},{"text":" "},{"text":"fInst"},{"text":" "},{"text":"dInst"},{"text":" "},{"text":"self"},{"text":" "},{"text":"f"},{"text":" "},{"text":"d"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"u"},{"ref":"And","text":" ∧\n    "},{"text":"u"},{"ref":"Eq","text":" = "},{"ref":"OptionExtAdaptedContracts.mapLazyDefault","text":"OptionExtAdaptedContracts.mapLazyDefault"},{"text":" "},{"text":"mapping"},{"text":" "},{"text":"defaultValue"},{"text":" "},{"text":"self"}],"definitions":[{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce","source":{"first_line":44,"last_line":46}},{"module":"Init.Prelude","name":"Unit","source":{"first_line":214,"last_line":224}},{"module":"Init.Prelude","name":"Option","source":{"first_line":3047,"last_line":3058}},{"module":"AdaptedContracts","name":"OptionExtAdaptedContracts.mapLazyDefault.match_1","source":null},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce.call_once","source":{"first_line":46,"last_line":46}},{"module":"Init.Prelude","name":"Unit.unit","source":{"first_line":226,"last_line":231}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"AdaptedContracts","name":"OptionExtAdaptedContracts.mapOrElse","source":{"first_line":6,"last_line":6}},{"module":"AdaptedContracts","name":"OptionExtAdaptedContracts.mapLazyDefault","source":{"first_line":8,"last_line":13}}],"definitions_truncated":false,"first_line":38,"last_line":50,"module":"AdaptedContracts","program":null,"program_head":null,"statement":"∀ {T U F D : Type} (fInst : Aeneas.Std.core.ops.function.FnOnce.{0, 0, 0} F T U)\n  (dInst : Aeneas.Std.core.ops.function.FnOnce.{0, 0, 0} D Unit U) (self : Option.{0} T) (f : F) (d : D)\n  (mapping : T → U) (defaultValue : U)\n  (selected :\n    @OptionExtAdaptedContracts.mapLazyDefault.match_1.{1} T (fun (self : Option.{0} T) => Prop) self\n      (fun (_ : Unit) =>\n        @Eq.{1} (Aeneas.Std.Result.{0} U)\n          (@Aeneas.Std.core.ops.function.FnOnce.call_once.{0, 0, 0} D Unit U dInst d Unit.unit)\n          (@Aeneas.Std.Result.ok.{0} U defaultValue))\n      fun (x : T) =>\n      @Eq.{1} (Aeneas.Std.Result.{0} U) (@Aeneas.Std.core.ops.function.FnOnce.call_once.{0, 0, 0} F T U fInst f x)\n        (@Aeneas.Std.Result.ok.{0} U (mapping x))),\n  @Exists.{1} U fun (u : U) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} U)\n        (@OptionExtAdaptedContracts.mapOrElse.{0, 0, 0, 0} T U F D fInst dInst self f d)\n        (@Aeneas.Std.Result.ok.{0} U u))\n      (@Eq.{1} U u (@OptionExtAdaptedContracts.mapLazyDefault T U mapping defaultValue self))","theorem":"OptionExtAdaptedContracts.map_or_else2_correct","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"implicit","kind":"variable","name":"U","type":"Type u_2","type_segments":[{"text":"Type u_2"}]},{"binder":"explicit","kind":"variable","name":"eqInst","type":"Aeneas.Std.core.cmp.PartialEq U T","type_segments":[{"ref":"Aeneas.Std.core.cmp.PartialEq","text":"Aeneas.Std.core.cmp.PartialEq"},{"text":" "},{"text":"U"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"relation","type":"U → T → Prop","type_segments":[{"text":"U"},{"text":" → "},{"text":"T"},{"text":" → "},{"text":"Prop"}]},{"binder":"explicit","kind":"variable","name":"opt","type":"Option T","type_segments":[{"ref":"Option","text":"Option"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"x","type":"U","type_segments":[{"text":"U"}]},{"binder":"explicit","kind":"hypothesis","name":"selected","type":"∀ (t : T), opt = Option.some t → ∃ b, eqInst.eq x t = Aeneas.Std.Result.ok b ∧ (b = Bool.true ↔ relation x t)","type_segments":[{"text":"∀ ("},{"text":"t"},{"text":" : "},{"text":"T"},{"text":"), "},{"text":"opt"},{"ref":"Eq","text":" = "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"t"},{"text":" → "},{"text":"∃ "},{"text":"b"},{"text":", "},{"text":"eqInst"},{"text":"."},{"ref":"Aeneas.Std.core.cmp.PartialEq.eq","text":"eq"},{"text":" "},{"text":"x"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"b"},{"ref":"And","text":" ∧ "},{"ref":"Iff","text":"("},{"text":"b"},{"ref":"Eq","text":" = "},{"ref":"Bool.true","text":"Bool.true"},{"ref":"Iff","text":" ↔ "},{"text":"relation"},{"text":" "},{"text":"x"},{"text":" "},{"text":"t"},{"ref":"Iff","text":")"}]}],"conclusion":"∃ out,\n  OptionExtContracts.contains eqInst opt x = Aeneas.Std.Result.ok out ∧\n    (out = Bool.true ↔\n      match opt, selected with\n      | Option.none, selected => False\n      | Option.some t, selected => relation x t)","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"OptionExtContracts.contains","text":"OptionExtContracts.contains"},{"text":" "},{"text":"eqInst"},{"text":" "},{"text":"opt"},{"text":" "},{"text":"x"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"Iff","text":"("},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"Bool.true","text":"Bool.true"},{"ref":"Iff","text":" ↔\n      "},{"text":"match "},{"text":"opt"},{"text":", "},{"text":"selected"},{"text":" with\n      | "},{"ref":"Option.none","text":"Option.none"},{"text":", "},{"text":"selected"},{"text":" => "},{"ref":"False","text":"False"},{"text":"\n      | "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"t"},{"text":", "},{"text":"selected"},{"text":" => "},{"text":"relation"},{"text":" "},{"text":"x"},{"text":" "},{"text":"t"},{"ref":"Iff","text":")"}],"definitions":[{"module":"Aeneas.Std.Core.Cmp","name":"Aeneas.Std.core.cmp.PartialEq","source":{"first_line":13,"last_line":16}},{"module":"Init.Prelude","name":"Option","source":{"first_line":3047,"last_line":3058}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Init.Prelude","name":"Option.some","source":{"first_line":3057,"last_line":3058}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"Bool","source":{"first_line":99,"last_line":111}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Cmp","name":"Aeneas.Std.core.cmp.PartialEq.eq","source":{"first_line":15,"last_line":15}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Core","name":"Iff","source":{"first_line":183,"last_line":194}},{"module":"Init.Prelude","name":"Bool.true","source":{"first_line":110,"last_line":111}},{"module":"Contracts","name":"OptionExtContracts.contains","source":{"first_line":19,"last_line":19}},{"module":"Contracts","name":"OptionExtContracts.contains_relation_correct.match_1","source":null},{"module":"Init.Prelude","name":"Option.none","source":{"first_line":3055,"last_line":3056}},{"module":"Init.Prelude","name":"False","source":{"first_line":274,"last_line":282}}],"definitions_truncated":false,"first_line":38,"last_line":49,"module":"Contracts","program":null,"program_head":null,"statement":"∀ {T : Type u_1} {U : Type u_2} (eqInst : Aeneas.Std.core.cmp.PartialEq.{u_2, u_1} U T) (relation : U → T → Prop)\n  (opt : Option.{u_1} T) (x : U)\n  (selected :\n    ∀ (t : T),\n      @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →\n        @Exists.{1} Bool fun (b : Bool) =>\n          And\n            (@Eq.{1} (Aeneas.Std.Result.{0} Bool) (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)\n              (@Aeneas.Std.Result.ok.{0} Bool b))\n            (Iff (@Eq.{1} Bool b Bool.true) (relation x t))),\n  @Exists.{1} Bool fun (out : Bool) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} Bool) (@OptionExtContracts.contains.{u_1, u_2} T U eqInst opt x)\n        (@Aeneas.Std.Result.ok.{0} Bool out))\n      (Iff (@Eq.{1} Bool out Bool.true)\n        (@OptionExtContracts.contains_relation_correct.match_1.{u_1, u_2, 1} T U eqInst relation x\n          (fun (opt : Option.{u_1} T)\n              (selected :\n                ∀ (t : T),\n                  @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →\n                    @Exists.{1} Bool fun (b : Bool) =>\n                      And\n                        (@Eq.{1} (Aeneas.Std.Result.{0} Bool)\n                          (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)\n                          (@Aeneas.Std.Result.ok.{0} Bool b))\n                        (Iff (@Eq.{1} Bool b Bool.true) (relation x t))) =>\n            Prop)\n          opt selected\n          (fun\n              (selected :\n                ∀ (t : T),\n                  @Eq.{u_1 + 1} (Option.{u_1} T) (@Option.none.{u_1} T) (@Option.some.{u_1} T t) →\n                    @Exists.{1} Bool fun (b : Bool) =>\n                      And\n                        (@Eq.{1} (Aeneas.Std.Result.{0} Bool)\n                          (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)\n                          (@Aeneas.Std.Result.ok.{0} Bool b))\n                        (Iff (@Eq.{1} Bool b Bool.true) (relation x t))) =>\n            False)\n          fun (t : T)\n            (selected :\n              ∀ (t_1 : T),\n                @Eq.{u_1 + 1} (Option.{u_1} T) (@Option.some.{u_1} T t) (@Option.some.{u_1} T t_1) →\n                  @Exists.{1} Bool fun (b : Bool) =>\n                    And\n                      (@Eq.{1} (Aeneas.Std.Result.{0} Bool)\n                        (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t_1)\n                        (@Aeneas.Std.Result.ok.{0} Bool b))\n                      (Iff (@Eq.{1} Bool b Bool.true) (relation x t_1))) =>\n          relation x t))","theorem":"OptionExtContracts.contains_relation_correct","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"implicit","kind":"variable","name":"V","type":"Type u_2","type_segments":[{"text":"Type u_2"}]},{"binder":"implicit","kind":"variable","name":"F","type":"Type u_3","type_segments":[{"text":"Type u_3"}]},{"binder":"explicit","kind":"variable","name":"call","type":"Aeneas.Std.core.ops.function.FnOnce F T V","type_segments":[{"ref":"Aeneas.Std.core.ops.function.FnOnce","text":"Aeneas.Std.core.ops.function.FnOnce"},{"text":" "},{"text":"F"},{"text":" "},{"text":"T"},{"text":" "},{"text":"V"}]},{"binder":"explicit","kind":"variable","name":"mapping","type":"T → V","type_segments":[{"text":"T"},{"text":" → "},{"text":"V"}]},{"binder":"explicit","kind":"variable","name":"opt","type":"Option T","type_segments":[{"ref":"Option","text":"Option"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"f","type":"F","type_segments":[{"text":"F"}]},{"binder":"explicit","kind":"variable","name":"default","type":"V","type_segments":[{"text":"V"}]},{"binder":"explicit","kind":"hypothesis","name":"selected","type":"∀ (t : T), opt = Option.some t → call.call_once f t = Aeneas.Std.Result.ok (mapping t)","type_segments":[{"text":"∀ ("},{"text":"t"},{"text":" : "},{"text":"T"},{"text":"), "},{"text":"opt"},{"ref":"Eq","text":" = "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"t"},{"text":" → "},{"text":"call"},{"text":"."},{"ref":"Aeneas.Std.core.ops.function.FnOnce.call_once","text":"call_once"},{"text":" "},{"text":"f"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"("},{"text":"mapping"},{"text":" "},{"text":"t"},{"text":")"}]}],"conclusion":"∃ out,\n  OptionExtContracts.map_or2 call opt f default = Aeneas.Std.Result.ok out ∧\n    out = OptionExtContracts.mapDefault mapping default opt","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"OptionExtContracts.map_or2","text":"OptionExtContracts.map_or2"},{"text":" "},{"text":"call"},{"text":" "},{"text":"opt"},{"text":" "},{"text":"f"},{"text":" "},{"text":"default"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"OptionExtContracts.mapDefault","text":"OptionExtContracts.mapDefault"},{"text":" "},{"text":"mapping"},{"text":" "},{"text":"default"},{"text":" "},{"text":"opt"}],"definitions":[{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce","source":{"first_line":44,"last_line":46}},{"module":"Init.Prelude","name":"Option","source":{"first_line":3047,"last_line":3058}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Init.Prelude","name":"Option.some","source":{"first_line":3057,"last_line":3058}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce.call_once","source":{"first_line":46,"last_line":46}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Contracts","name":"OptionExtContracts.map_or2","source":{"first_line":20,"last_line":20}},{"module":"Contracts","name":"OptionExtContracts.mapDefault","source":{"first_line":13,"last_line":17}}],"definitions_truncated":false,"first_line":60,"last_line":68,"module":"Contracts","program":null,"program_head":null,"statement":"∀ {T : Type u_1} {V : Type u_2} {F : Type u_3} (call : Aeneas.Std.core.ops.function.FnOnce.{u_3, u_1, u_2} F T V)\n  (mapping : T → V) (opt : Option.{u_1} T) (f : F) (default : V)\n  (selected :\n    ∀ (t : T),\n      @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →\n        @Eq.{u_2 + 1} (Aeneas.Std.Result.{u_2} V)\n          (@Aeneas.Std.core.ops.function.FnOnce.call_once.{u_3, u_1, u_2} F T V call f t)\n          (@Aeneas.Std.Result.ok.{u_2} V (mapping t))),\n  @Exists.{u_2 + 1} V fun (out : V) =>\n    And\n      (@Eq.{u_2 + 1} (Aeneas.Std.Result.{u_2} V) (@OptionExtContracts.map_or2.{u_1, u_2, u_3} T V F call opt f default)\n        (@Aeneas.Std.Result.ok.{u_2} V out))\n      (@Eq.{u_2 + 1} V out (@OptionExtContracts.mapDefault.{u_1, u_2} T V mapping default opt))","theorem":"OptionExtContracts.map_or2_correct","translation_rerun":false,"version":1}

=== stderr ===

Environment

The selected profile uses the pinned registry release, Aeneas and Charon revisions without patches, and Lean 4.35.0 on aarch64-apple-darwin. Local proofs-rs CLI patches prepare pinned inputs and correct API discovery for Rust raw-identifier modules such as r#impl and Rust 2015 crate-root imports; they do not change the Lean models or contracts. Their scope and validation are recorded with the tool lock. The profile specification, source and tool locks, adaptation check, and results record provide the contracts and reproducibility evidence. Native tests of the release and adapted code are separate from the formal contracts.

What is trusted

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

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

Dependencies (0)

No direct dependencies.

Comments (0)

No comments.