Report #27 — Either branch operations, payload conversions and conditional composition

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

41 verified claims · 0 findings

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

nyuichi · 2026-11-05 01:23 UTC

Revision v8 · v7 · v6 · v5 · v4 · v3 · v2 · v1

Overview

The new manual Iterator::next implementation for Either passes the selected inner iterator state to its next dictionary and returns exactly its Option<Item> with the updated state under the same Either tag. None still retains the returned updated state. Normal item/state helpers assume only the selected inner next result; identical modeled failure/divergence propagate without using the other dictionary. This does not prove arbitrary inner iterator progress, termination, length bounds or fusedness. The new map_either/map_either_with contracts preserve the present variant while replacing its payload with the selected callback result; the context-aware form forwards the original context. Normal results require success only at that actual payload/context, and modeled failure/divergence propagate unchanged. inspect_left/right call the selected borrowed-value callback and return the original modeled self after success; on the other variant they return self without any callback premise. This self-retention is a property of the extracted shared-reference value model and does not certify unchanged observable Rust interior/global state under arbitrary callbacks. For either 1.19.0 with default features on x86_64, the forty-one named APIs have the following value-model contracts. either dispatches only to the callback for the present variant, passing exactly its payload; either_with additionally passes the original context as the first pair element. either_into dispatches that payload to the corresponding Into dictionary. Their main contracts preserve the selected computation's whole modeled Result without assuming success. Separate normal-value contracts need success only at the selected payload/context; failure and divergence helpers retain the same modeled outcome. The unused callback/conversion dictionary is unconstrained. Twelve earlier callback APIs compose a mathematical callback under their explicit normal-result premises for every callback argument, with selected failure propagated and nonselected results preserved. The real impl<T> IntoEither for T dictionary is linked to its original default, so into_either_with requires only normal predicate behavior at the actual borrowed input. Predicates/projections identify and retain the exact variant and optional payload; flip swaps it and flipping twice reconstructs the original. Eager selection preserves the indicated payload or supplied alternative. Optional and tuple factoring preserve tags and exact components. as_ref preserves the borrowed view; as_mut's backward function writes a matching-variant replacement payload back. The original handwritten conversions map Result Ok to Right and Err to Left, with exact payloads, and reverse those mappings; both roundtrips reconstruct every variant. left_or_default/right_or_default preserve the matching payload without a Default premise and otherwise delegate the Default computation's entire modeled outcome. Normal fallback values, modeled failure and divergence have separate explicit premises. The earlier thirty APIs return normally in this model under their stated conditions; the Default fallback pair and the three dispatch APIs retain abstract selected-computation outcomes. These are value-semantic guarantees with the destructor and callback boundaries stated below. Separate supplemental Lean proofs cover the original shared-reference and mutable-reference specialized copied/cloned methods. copied preserves the selected branch and payload; mutable copied also preserves both extracted backward-state values. cloned delegates exactly to the selected Clone dictionary, preserving its modeled Result including failure/divergence, and wraps a successful clone in the same branch. Mutable cloned additionally preserves the two extracted backward-model values. These four specialized Rust methods are not registered machine claims because source-scanner specialized-owner matching remains blocked; the existing40 mappings remain unchanged. The original DoubleEndedIterator::next_back method exactly delegates to the selected inner dictionary, returning its Option and updated state in the same Either branch and preserving modeled failure or divergence. This contract imposes no independent iterator correctness or termination law.

Findings (0)

No findings reported.

APIs (41)

Methods

`impl Either<(L, T), (R, T)>`

pub fn factor_second(self: Self) -> (Either<L, R>, T)

Claim #12

`impl Either<(T, L), (T, R)>`

pub fn factor_first(self: Self) -> (T, Either<L, R>)

Claim #11

`impl Either<L, R>`

pub fn as_mut(self: &mut Self) -> Either<&mut L, &mut R>

Claim #14

pub fn as_ref(self: &Self) -> Either<&L, &R>

Claim #13

pub fn either<F, G, T>(self: Self, f: F, g: G) -> T where F: FnOnce(L) -> T, G: FnOnce(R) -> T

Claim #33

pub fn either_into<T>(self: Self) -> T where L: Into<T>, R: Into<T>

Claim #35

pub fn either_with<Ctx, F, G, T>(self: Self, ctx: Ctx, f: F, g: G) -> T where F: FnOnce(Ctx, L) -> T, G: FnOnce(Ctx, R) -> T

Claim #34

pub fn flip(self: Self) -> Either<R, L>

Claim #5

pub fn inspect_left<F>(self: Self, f: F) -> Self where F: FnOnce(&L)

Claim #38

pub fn inspect_right<F>(self: Self, f: F) -> Self where F: FnOnce(&R)

Claim #39

pub fn is_left(self: &Self) -> bool

Claim #1

pub fn is_left_and<F>(self: Self, f: F) -> bool where F: FnOnce(L) -> bool

Claim #15

pub fn is_left_or<F>(self: Self, f: F) -> bool where F: FnOnce(R) -> bool

Claim #17

pub fn is_right(self: &Self) -> bool

Claim #2

pub fn is_right_and<F>(self: Self, f: F) -> bool where F: FnOnce(R) -> bool

Claim #16

pub fn is_right_or<F>(self: Self, f: F) -> bool where F: FnOnce(L) -> bool

Claim #18

pub fn left(self: Self) -> Option<L>

Claim #3

pub fn left_and<S>(self: Self, other: Either<S, R>) -> Either<S, R>

Claim #8

pub fn left_and_then<F, S>(self: Self, f: F) -> Either<S, R> where F: FnOnce(L) -> Either<S, R>

Claim #25

pub fn left_or(self: Self, other: L) -> L

Claim #6

pub fn left_or_default(self: Self) -> L where L: Default

Claim #31

pub fn left_or_else<F>(self: Self, f: F) -> L where F: FnOnce(R) -> L

Claim #23

pub fn map_either<F, G, M, S>(self: Self, f: F, g: G) -> Either<M, S> where F: FnOnce(L) -> M, G: FnOnce(R) -> S

Claim #36

pub fn map_either_with<Ctx, F, G, M, S>(self: Self, ctx: Ctx, f: F, g: G) -> Either<M, S> where F: FnOnce(Ctx, L) -> M, G: FnOnce(Ctx, R) -> S

Claim #37

pub fn map_left<F, M>(self: Self, f: F) -> Either<M, R> where F: FnOnce(L) -> M

Claim #19

pub fn map_left_or<F, S>(self: Self, default: S, f: F) -> S where F: FnOnce(L) -> S

Claim #21

pub fn map_right<F, S>(self: Self, f: F) -> Either<L, S> where F: FnOnce(R) -> S

Claim #20

pub fn map_right_or<F, S>(self: Self, default: S, f: F) -> S where F: FnOnce(R) -> S

Claim #22

pub fn right(self: Self) -> Option<R>

Claim #4

pub fn right_and<S>(self: Self, other: Either<L, S>) -> Either<L, S>

Claim #9

pub fn right_and_then<F, S>(self: Self, f: F) -> Either<L, S> where F: FnOnce(R) -> Either<L, S>

Claim #26

pub fn right_or(self: Self, other: R) -> R

Claim #7

pub fn right_or_default(self: Self) -> R where R: Default

Claim #32

pub fn right_or_else<F>(self: Self, f: F) -> R where F: FnOnce(L) -> R

Claim #24

`impl Either<core::option::Option<L>, core::option::Option<R>>`

pub fn factor_none(self: Self) -> Option<Either<L, R>>

Claim #10

Trait implementations

`impl core::iter::traits::double_ended::DoubleEndedIterator for Either<L, R>`

pub fn next_back(self: &mut Self) -> Option<<Self as core::iter::traits::iterator::Iterator>::Item>

Claim #41

`impl core::iter::traits::iterator::Iterator for Either<L, R>`

pub fn next(self: &mut Self) -> Option<<Self as core::iter::traits::iterator::Iterator>::Item>

Claim #40

`impl either::IntoEither for T`

pub fn into_either(self: Self, into_left: bool) -> Either<Self, Self>

Claim #27

pub fn into_either_with<F>(self: Self, into_left: F) -> Either<Self, Self> where F: FnOnce(&Self) -> bool

Claim #28

Recorded callables

<core::result::Result<R, L> as From<either::Either<L, R>>>::from recorded callable · signature and safety not recorded

Claim #30

<either::Either as From<core::result::Result<R, L>>>::from recorded callable · signature and safety not recorded

Claim #29

Evidence

https://github.com/nyuichi/rust-crate-proofs/tree/2f299a765ca1880602d29b7d52433bc63aea0a25

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-27-source-1
git -C report-27-source-1 checkout --detach 2f299a765ca1880602d29b7d52433bc63aea0a25
git -C report-27-source-1 submodule update --init --recursive --checkout
cd report-27-source-1/either/1.19.0/aeneas/2026-11-05/proofs

lake build +BothProofs +CallbackProofs +DefaultProofs +IntoEitherProofs +IteratorProofs +MapInspectProofs +NextBackProofs +Proofs +ResultProofs

printf '%s' 'import Lean
import BothProofs
import CallbackProofs
import DefaultProofs
import IntoEitherProofs
import IteratorProofs
import MapInspectProofs
import NextBackProofs
import Proofs
import ResultProofs
open Lean Elab Command

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

run_cmd do
  let theorem_name := `NextBackProofs.next_back_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: NextBackProofs.next_back_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in NextBackProofs.next_back_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:NextBackProofs.next_back_spec"
' | 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 · 41 checks passed · 0 failed

2026-11-05T17:03:13.784503568+00:00 · 103.9 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.is_left_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.is_left_spec`	Passed	Claim #1
Lean checked theorem Proofs.is_right_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.is_right_spec`	Passed	Claim #2
Lean checked theorem Proofs.left_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.left_spec`	Passed	Claim #3
Lean checked theorem Proofs.right_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.right_spec`	Passed	Claim #4
Lean checked theorem Proofs.flip_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.flip_spec`	Passed	Claim #5
Lean checked theorem Proofs.left_or_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.left_or_spec`	Passed	Claim #6
Lean checked theorem Proofs.right_or_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.right_or_spec`	Passed	Claim #7
Lean checked theorem Proofs.left_and_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.left_and_spec`	Passed	Claim #8
Lean checked theorem Proofs.right_and_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.right_and_spec`	Passed	Claim #9
Lean checked theorem Proofs.factor_none_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.factor_none_spec`	Passed	Claim #10
Lean checked theorem Proofs.factor_first_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.factor_first_spec`	Passed	Claim #11
Lean checked theorem Proofs.factor_second_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.factor_second_spec`	Passed	Claim #12
Lean checked theorem Proofs.as_ref_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.as_ref_spec`	Passed	Claim #13
Lean checked theorem Proofs.as_mut_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.as_mut_spec`	Passed	Claim #14
Lean checked theorem CallbackProofs.is_left_and_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.is_left_and_spec`	Passed	Claim #15
Lean checked theorem CallbackProofs.is_right_and_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.is_right_and_spec`	Passed	Claim #16
Lean checked theorem CallbackProofs.is_left_or_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.is_left_or_spec`	Passed	Claim #17
Lean checked theorem CallbackProofs.is_right_or_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.is_right_or_spec`	Passed	Claim #18
Lean checked theorem CallbackProofs.map_left_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.map_left_spec`	Passed	Claim #19
Lean checked theorem CallbackProofs.map_right_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.map_right_spec`	Passed	Claim #20
Lean checked theorem CallbackProofs.map_left_or_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.map_left_or_spec`	Passed	Claim #21
Lean checked theorem CallbackProofs.map_right_or_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.map_right_or_spec`	Passed	Claim #22
Lean checked theorem CallbackProofs.left_or_else_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.left_or_else_spec`	Passed	Claim #23
Lean checked theorem CallbackProofs.right_or_else_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.right_or_else_spec`	Passed	Claim #24
Lean checked theorem CallbackProofs.left_and_then_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.left_and_then_spec`	Passed	Claim #25
Lean checked theorem CallbackProofs.right_and_then_spec; axioms limited to propext, Classical.choice, Quot.sound `CallbackProofs.right_and_then_spec`	Passed	Claim #26
Lean checked theorem IntoEitherProofs.into_either_blanket_spec; axioms limited to propext, Classical.choice, Quot.sound `IntoEitherProofs.into_either_blanket_spec`	Passed	Claim #27
Lean checked theorem IntoEitherProofs.into_either_with_blanket_spec; axioms limited to propext, Classical.choice, Quot.sound `IntoEitherProofs.into_either_with_blanket_spec`	Passed	Claim #28
Lean checked theorem ResultProofs.from_result_spec; axioms limited to propext, Classical.choice, Quot.sound `ResultProofs.from_result_spec`	Passed	Claim #29
Lean checked theorem ResultProofs.from_either_spec; axioms limited to propext, Classical.choice, Quot.sound `ResultProofs.from_either_spec`	Passed	Claim #30
Lean checked theorem DefaultProofs.left_or_default_spec; axioms limited to propext, Classical.choice, Quot.sound `DefaultProofs.left_or_default_spec`	Passed	Claim #31
Lean checked theorem DefaultProofs.right_or_default_spec; axioms limited to propext, Classical.choice, Quot.sound `DefaultProofs.right_or_default_spec`	Passed	Claim #32
Lean checked theorem BothProofs.either_spec; axioms limited to propext, Classical.choice, Quot.sound `BothProofs.either_spec`	Passed	Claim #33
Lean checked theorem BothProofs.either_with_spec; axioms limited to propext, Classical.choice, Quot.sound `BothProofs.either_with_spec`	Passed	Claim #34
Lean checked theorem BothProofs.either_into_spec; axioms limited to propext, Classical.choice, Quot.sound `BothProofs.either_into_spec`	Passed	Claim #35
Lean checked theorem MapInspectProofs.map_either_spec; axioms limited to propext, Classical.choice, Quot.sound `MapInspectProofs.map_either_spec`	Passed	Claim #36
Lean checked theorem MapInspectProofs.map_either_with_spec; axioms limited to propext, Classical.choice, Quot.sound `MapInspectProofs.map_either_with_spec`	Passed	Claim #37
Lean checked theorem MapInspectProofs.inspect_left_spec; axioms limited to propext, Classical.choice, Quot.sound `MapInspectProofs.inspect_left_spec`	Passed	Claim #38
Lean checked theorem MapInspectProofs.inspect_right_spec; axioms limited to propext, Classical.choice, Quot.sound `MapInspectProofs.inspect_right_spec`	Passed	Claim #39
Lean checked theorem IteratorProofs.next_spec; axioms limited to propext, Classical.choice, Quot.sound `IteratorProofs.next_spec`	Passed	Claim #40
Lean checked theorem NextBackProofs.next_back_spec; axioms limited to propext, Classical.choice, Quot.sound `NextBackProofs.next_back_spec`	Passed	Claim #41

Execution details

Started: 2026-11-05T17:03:13.784503568+00:00
Finished: 2026-11-05T17:04:57.643230946+00:00
Platform: linux x86_64
Rust compiler: rustc 1.100.0-nightly (923c95cdf 2026-09-16) binary: rustc commit-hash: 923c95cdf5ba65cea505aa2ea829f578e1506ed8 commit-date: 2026-09-16 host: x86_64-unknown-linux-gnu release: 1.100.0-nightly LLVM version: 23.1.1
Working directory: either/1.19.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: 2f299a765ca1880602d29b7d52433bc63aea0a25

Diagnostics & logs

=== stdout ===
✔ [1795/1805] Built ReferenceSupplement.Either (1.6s)
✔ [1796/1805] Built Generated.Either (1.9s)
ℹ [1797/1805] Built IntoEitherProofs (2.9s)
info: IntoEitherProofs.lean:55:0: 'IntoEitherProofs.into_either_default_spec' depends on axioms: [propext, Quot.sound]
info: IntoEitherProofs.lean:56:0: 'IntoEitherProofs.into_either_with_default_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:57:0: 'IntoEitherProofs.callback_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:58:0: 'IntoEitherProofs.selected_dispatch' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:59:0: 'IntoEitherProofs.dispatch_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:61:0: 'IntoEitherProofs.blanket_dispatch_is_original_default' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:62:0: 'IntoEitherProofs.into_either_blanket_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:63:0: 'IntoEitherProofs.into_either_with_blanket_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IntoEitherProofs.lean:64:0: 'IntoEitherProofs.blanket_callback_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1798/1805] Built ReferenceSupplementProofs (3.1s)
info: ReferenceSupplementProofs.lean:13:0: 'ReferenceSupplementProofs.shared_copied' depends on axioms: [propext, Quot.sound]
info: ReferenceSupplementProofs.lean:14:0: 'ReferenceSupplementProofs.shared_cloned_left' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReferenceSupplementProofs.lean:15:0: 'ReferenceSupplementProofs.shared_cloned_right' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReferenceSupplementProofs.lean:16:0: 'ReferenceSupplementProofs.mut_copied' depends on axioms: [propext, Quot.sound]
info: ReferenceSupplementProofs.lean:17:0: 'ReferenceSupplementProofs.mut_cloned_left' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReferenceSupplementProofs.lean:18:0: 'ReferenceSupplementProofs.mut_cloned_right' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1799/1805] Built MapInspectProofs (3.0s)
info: MapInspectProofs.lean:149:0: 'MapInspectProofs.map_either_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:151:0: 'MapInspectProofs.map_either_normal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:153:0: 'MapInspectProofs.map_either_left_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:155:0: 'MapInspectProofs.map_either_left_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:157:0: 'MapInspectProofs.map_either_right_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:159:0: 'MapInspectProofs.map_either_right_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:161:0: 'MapInspectProofs.map_either_with_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:163:0: 'MapInspectProofs.map_either_with_normal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:165:0: 'MapInspectProofs.map_either_with_left_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:167:0: 'MapInspectProofs.map_either_with_left_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:169:0: 'MapInspectProofs.map_either_with_right_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:171:0: 'MapInspectProofs.map_either_with_right_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:173:0: 'MapInspectProofs.inspect_left_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:175:0: 'MapInspectProofs.inspect_left_normal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:177:0: 'MapInspectProofs.inspect_left_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:179:0: 'MapInspectProofs.inspect_left_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:181:0: 'MapInspectProofs.inspect_left_short_circuit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:183:0: 'MapInspectProofs.inspect_right_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:185:0: 'MapInspectProofs.inspect_right_normal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:187:0: 'MapInspectProofs.inspect_right_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:189:0: 'MapInspectProofs.inspect_right_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: MapInspectProofs.lean:191:0: 'MapInspectProofs.inspect_right_short_circuit' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1800/1805] Built NextBackProofs (3.1s)
info: NextBackProofs.lean:13:0: 'NextBackProofs.left' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NextBackProofs.lean:14:0: 'NextBackProofs.right' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NextBackProofs.lean:15:0: 'NextBackProofs.next_back_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1802/1807] Built IteratorProofs (3.3s)
info: IteratorProofs.lean:63:0: 'IteratorProofs.next_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:64:0: 'IteratorProofs.next_left_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:65:0: 'IteratorProofs.next_right_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:66:0: 'IteratorProofs.next_left_none_writeback' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:67:0: 'IteratorProofs.next_right_none_writeback' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:68:0: 'IteratorProofs.next_left_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:69:0: 'IteratorProofs.next_right_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:70:0: 'IteratorProofs.next_left_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: IteratorProofs.lean:71:0: 'IteratorProofs.next_right_divergence' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1803/1807] Built DefaultProofs (2.7s)
warning: DefaultProofs.lean:5:75: Variable name `r` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _r

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DefaultProofs.lean:13:75: Variable name `r` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _r

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DefaultProofs.lean:27:56: Variable name `l` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _l

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DefaultProofs.lean:35:60: Variable name `l` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _l

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: DefaultProofs.lean:49:0: 'DefaultProofs.left_or_default_spec' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:50:0: 'DefaultProofs.left_or_default_selected' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:51:0: 'DefaultProofs.left_or_default_normal' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:52:0: 'DefaultProofs.left_or_default_failure' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:53:0: 'DefaultProofs.left_or_default_divergence' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:54:0: 'DefaultProofs.right_or_default_spec' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:55:0: 'DefaultProofs.right_or_default_selected' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:56:0: 'DefaultProofs.right_or_default_normal' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:57:0: 'DefaultProofs.right_or_default_failure' depends on axioms: [propext, Quot.sound]
info: DefaultProofs.lean:58:0: 'DefaultProofs.right_or_default_divergence' depends on axioms: [propext, Quot.sound]
ℹ [1804/1807] Built BothProofs (2.6s)
info: BothProofs.lean:108:0: 'BothProofs.either_spec' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:109:0: 'BothProofs.either_normal' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:110:0: 'BothProofs.either_left_failure' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:111:0: 'BothProofs.either_right_failure' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:112:0: 'BothProofs.either_left_divergence' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:113:0: 'BothProofs.either_right_divergence' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:114:0: 'BothProofs.either_with_spec' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:115:0: 'BothProofs.either_with_normal' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:116:0: 'BothProofs.either_with_left_failure' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:117:0: 'BothProofs.either_with_right_failure' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:118:0: 'BothProofs.either_with_left_divergence' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:119:0: 'BothProofs.either_with_right_divergence' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:121:0: 'BothProofs.either_into_spec' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:122:0: 'BothProofs.either_into_normal' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:123:0: 'BothProofs.either_into_left_failure' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:124:0: 'BothProofs.either_into_right_failure' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:125:0: 'BothProofs.either_into_left_divergence' depends on axioms: [propext, Quot.sound]
info: BothProofs.lean:126:0: 'BothProofs.either_into_right_divergence' depends on axioms: [propext, Quot.sound]
ℹ [1805/1807] Built ResultProofs (2.6s)
info: ResultProofs.lean:23:0: 'ResultProofs.from_result_spec' depends on axioms: [propext, Quot.sound]
info: ResultProofs.lean:24:0: 'ResultProofs.from_either_spec' depends on axioms: [propext, Quot.sound]
info: ResultProofs.lean:25:0: 'ResultProofs.result_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResultProofs.lean:26:0: 'ResultProofs.either_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1806/1807] Built CallbackProofs (2.9s)
warning: CallbackProofs.lean:8:75: Variable name `r` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _r

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:23:58: Variable name `l` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _l

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:38:56: Variable name `l` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _l

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:53:75: Variable name `r` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _r

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:98:77: Variable name `r` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _r

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:113:60: Variable name `l` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _l

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:125:33: Variable name `S` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _S

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:131:36: Variable name `S` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _S

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:136:42: Variable name `S` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _S

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:140:34: Variable name `S` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _S

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:146:37: Variable name `S` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _S

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: CallbackProofs.lean:151:43: Variable name `S` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _S

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: CallbackProofs.lean:186:0: 'CallbackProofs.is_left_and_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:187:0: 'CallbackProofs.is_left_and_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:188:0: 'CallbackProofs.is_left_and_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:189:0: 'CallbackProofs.is_right_and_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:190:0: 'CallbackProofs.is_right_and_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:191:0: 'CallbackProofs.is_right_and_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:192:0: 'CallbackProofs.is_left_or_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:193:0: 'CallbackProofs.is_left_or_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:194:0: 'CallbackProofs.is_left_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:195:0: 'CallbackProofs.is_right_or_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:196:0: 'CallbackProofs.is_right_or_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:197:0: 'CallbackProofs.is_right_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:198:0: 'CallbackProofs.map_left_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: CallbackProofs.lean:199:0: 'CallbackProofs.map_left_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: CallbackProofs.lean:200:0: 'CallbackProofs.map_left_short_circuit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: CallbackProofs.lean:201:0: 'CallbackProofs.map_right_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: CallbackProofs.lean:202:0: 'CallbackProofs.map_right_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: CallbackProofs.lean:203:0: 'CallbackProofs.map_right_short_circuit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: CallbackProofs.lean:205:0: 'CallbackProofs.map_left_or_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:206:0: 'CallbackProofs.map_left_or_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:207:0: 'CallbackProofs.map_left_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:208:0: 'CallbackProofs.map_right_or_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:209:0: 'CallbackProofs.map_right_or_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:210:0: 'CallbackProofs.map_right_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:211:0: 'CallbackProofs.left_or_else_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:212:0: 'CallbackProofs.left_or_else_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:213:0: 'CallbackProofs.left_or_else_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:214:0: 'CallbackProofs.right_or_else_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:215:0: 'CallbackProofs.right_or_else_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:216:0: 'CallbackProofs.right_or_else_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:217:0: 'CallbackProofs.left_and_then_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:218:0: 'CallbackProofs.left_and_then_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:219:0: 'CallbackProofs.left_and_then_short_circuit' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:220:0: 'CallbackProofs.right_and_then_spec' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:221:0: 'CallbackProofs.right_and_then_failure' depends on axioms: [propext, Quot.sound]
info: CallbackProofs.lean:222:0: 'CallbackProofs.right_and_then_short_circuit' depends on axioms: [propext, Quot.sound]
⚠ [1807/1807] Built Proofs (2.4s)
warning: Proofs.lean:10:149: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:10:166: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:10:179: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:10:193: This simp argument is unused:
  Either.flip

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:10:206: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:10:222: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:11:168: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:11:181: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:11:195: This simp argument is unused:
  Either.flip

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:11:208: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:11:224: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:12:128: This simp argument is unused:
  Either.is_left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_right, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:12:144: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:12:174: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:12:188: This simp argument is unused:
  Either.flip

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:12:201: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:12:217: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:13:130: This simp argument is unused:
  Either.is_left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_right, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:13:146: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:13:163: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:13:190: This simp argument is unused:
  Either.flip

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:13:203: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:13:219: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:14:133: This simp argument is unused:
  Either.is_left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_right, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:14:149: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:14:166: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:14:179: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:14:206: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:14:222: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:15:100: This simp argument is unused:
  Either.is_left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_right, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:15:116: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:15:133: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:15:146: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:15:173: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:15:189: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:16:148: This simp argument is unused:
  Either.is_left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_right, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:16:164: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:16:181: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:16:194: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:16:208: This simp argument is unused:
  Either.flip

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:16:237: This simp argument is unused:
  Either.right_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.left_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:17:150: This simp argument is unused:
  Either.is_left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_right, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:17:166: This simp argument is unused:
  Either.is_right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.left, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:17:183: This simp argument is unused:
  Either.left

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.right, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:17:196: This simp argument is unused:
  Either.right

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.flip, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:17:210: This simp argument is unused:
  Either.flip

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.left_or, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:17:223: This simp argument is unused:
  Either.left_or

Hint: Omit it from the simp argument list.
  [apply] simp [Either.is_left, Either.is_right, Either.left, Either.right, Either.flip, Either.right_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:33:87: This simp argument is unused:
  P.Insts.CoreOpsFunctionFnOnceTupleLEither

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleREither,
    P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once, P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once,
    Either.Left.constructor, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:33:130: This simp argument is unused:
  P.Insts.CoreOpsFunctionFnOnceTupleREither

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleLEither,
    P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once, P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once,
    Either.Left.constructor, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:33:226: This simp argument is unused:
  P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleLEither,
    P.Insts.CoreOpsFunctionFnOnceTupleREither, P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once,
    Either.Left.constructor, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:33:304: This simp argument is unused:
  Either.Right.constructor

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleLEither,
    P.Insts.CoreOpsFunctionFnOnceTupleREither, P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once,
    P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once, Either.Left.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:34:88: This simp argument is unused:
  P.Insts.CoreOpsFunctionFnOnceTupleLEither

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleREither,
    P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once, P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once,
    Either.Left.constructor, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:34:131: This simp argument is unused:
  P.Insts.CoreOpsFunctionFnOnceTupleREither

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleLEither,
    P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once, P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once,
    Either.Left.constructor, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:34:174: This simp argument is unused:
  P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleLEither,
    P.Insts.CoreOpsFunctionFnOnceTupleREither, P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once,
    Either.Left.constructor, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:34:280: This simp argument is unused:
  Either.Left.constructor

Hint: Omit it from the simp argument list.
  [apply] simp [EitherOptionOption.factor_none, core.option.Option.map, P.Insts.CoreOpsFunctionFnOnceTupleLEither,
    P.Insts.CoreOpsFunctionFnOnceTupleREither, P.Insts.CoreOpsFunctionFnOnceTupleLEither.call_once,
    P.Insts.CoreOpsFunctionFnOnceTupleREither.call_once, Either.Right.constructor]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Proofs.lean:36:0: 'Proofs.as_ref_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:37:0: 'Proofs.as_mut_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:38:0: 'Proofs.left_and_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:39:0: 'Proofs.right_and_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:40:0: 'Proofs.factor_first_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:41:0: 'Proofs.factor_second_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:42:0: 'Proofs.factor_none_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:44:0: 'Proofs.is_left_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:45:0: 'Proofs.is_right_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:46:0: 'Proofs.left_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:47:0: 'Proofs.right_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:48:0: 'Proofs.flip_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:49:0: 'Proofs.flip_twice' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:50:0: 'Proofs.left_or_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:51:0: 'Proofs.right_or_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:53:0: 'CallbackProofs.is_left_and_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:54:0: 'CallbackProofs.is_left_and_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:55:0: 'CallbackProofs.is_left_and_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:56:0: 'CallbackProofs.is_right_and_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:57:0: 'CallbackProofs.is_right_and_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:58:0: 'CallbackProofs.is_right_and_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:59:0: 'CallbackProofs.is_left_or_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:60:0: 'CallbackProofs.is_left_or_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:61:0: 'CallbackProofs.is_left_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:62:0: 'CallbackProofs.is_right_or_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:63:0: 'CallbackProofs.is_right_or_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:64:0: 'CallbackProofs.is_right_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:65:0: 'CallbackProofs.map_left_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:66:0: 'CallbackProofs.map_left_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:67:0: 'CallbackProofs.map_left_short_circuit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:68:0: 'CallbackProofs.map_right_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:69:0: 'CallbackProofs.map_right_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:70:0: 'CallbackProofs.map_right_short_circuit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:72:0: 'CallbackProofs.map_left_or_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:73:0: 'CallbackProofs.map_left_or_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:74:0: 'CallbackProofs.map_left_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:75:0: 'CallbackProofs.map_right_or_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:76:0: 'CallbackProofs.map_right_or_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:77:0: 'CallbackProofs.map_right_or_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:78:0: 'CallbackProofs.left_or_else_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:79:0: 'CallbackProofs.left_or_else_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:80:0: 'CallbackProofs.left_or_else_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:81:0: 'CallbackProofs.right_or_else_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:82:0: 'CallbackProofs.right_or_else_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:83:0: 'CallbackProofs.right_or_else_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:84:0: 'CallbackProofs.left_and_then_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:85:0: 'CallbackProofs.left_and_then_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:86:0: 'CallbackProofs.left_and_then_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:87:0: 'CallbackProofs.right_and_then_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:88:0: 'CallbackProofs.right_and_then_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:89:0: 'CallbackProofs.right_and_then_short_circuit' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:91:0: 'IntoEitherProofs.into_either_default_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:92:0: 'IntoEitherProofs.into_either_with_default_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:93:0: 'IntoEitherProofs.callback_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:94:0: 'IntoEitherProofs.selected_dispatch' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:95:0: 'IntoEitherProofs.dispatch_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:96:0: 'IntoEitherProofs.blanket_dispatch_is_original_default' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:97:0: 'IntoEitherProofs.into_either_blanket_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:98:0: 'IntoEitherProofs.into_either_with_blanket_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:99:0: 'IntoEitherProofs.blanket_callback_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:101:0: 'ResultProofs.from_result_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:102:0: 'ResultProofs.from_either_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:103:0: 'ResultProofs.result_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:104:0: 'ResultProofs.either_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:106:0: 'DefaultProofs.left_or_default_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:107:0: 'DefaultProofs.left_or_default_selected' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:108:0: 'DefaultProofs.left_or_default_normal' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:109:0: 'DefaultProofs.left_or_default_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:110:0: 'DefaultProofs.left_or_default_divergence' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:111:0: 'DefaultProofs.right_or_default_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:112:0: 'DefaultProofs.right_or_default_selected' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:113:0: 'DefaultProofs.right_or_default_normal' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:114:0: 'DefaultProofs.right_or_default_failure' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:115:0: 'DefaultProofs.right_or_default_divergence' depends on axioms: [propext, Quot.sound]
Build completed successfully (1807 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.is_left_spec
proofs.rs:checked:Proofs.is_right_spec
proofs.rs:checked:Proofs.left_spec
proofs.rs:checked:Proofs.right_spec
proofs.rs:checked:Proofs.flip_spec
proofs.rs:checked:Proofs.left_or_spec
proofs.rs:checked:Proofs.right_or_spec
proofs.rs:checked:Proofs.left_and_spec
proofs.rs:checked:Proofs.right_and_spec
proofs.rs:checked:Proofs.factor_none_spec
proofs.rs:checked:Proofs.factor_first_spec
proofs.rs:checked:Proofs.factor_second_spec
proofs.rs:checked:Proofs.as_ref_spec
proofs.rs:checked:Proofs.as_mut_spec
proofs.rs:checked:CallbackProofs.is_left_and_spec
proofs.rs:checked:CallbackProofs.is_right_and_spec
proofs.rs:checked:CallbackProofs.is_left_or_spec
proofs.rs:checked:CallbackProofs.is_right_or_spec
proofs.rs:checked:CallbackProofs.map_left_spec
proofs.rs:checked:CallbackProofs.map_right_spec
proofs.rs:checked:CallbackProofs.map_left_or_spec
proofs.rs:checked:CallbackProofs.map_right_or_spec
proofs.rs:checked:CallbackProofs.left_or_else_spec
proofs.rs:checked:CallbackProofs.right_or_else_spec
proofs.rs:checked:CallbackProofs.left_and_then_spec
proofs.rs:checked:CallbackProofs.right_and_then_spec
proofs.rs:checked:IntoEitherProofs.into_either_blanket_spec
proofs.rs:checked:IntoEitherProofs.into_either_with_blanket_spec
proofs.rs:checked:ResultProofs.from_result_spec
proofs.rs:checked:ResultProofs.from_either_spec
proofs.rs:checked:DefaultProofs.left_or_default_spec
proofs.rs:checked:DefaultProofs.right_or_default_spec
proofs.rs:checked:BothProofs.either_spec
proofs.rs:checked:BothProofs.either_with_spec
proofs.rs:checked:BothProofs.either_into_spec
proofs.rs:checked:MapInspectProofs.map_either_spec
proofs.rs:checked:MapInspectProofs.map_either_with_spec
proofs.rs:checked:MapInspectProofs.inspect_left_spec
proofs.rs:checked:MapInspectProofs.inspect_right_spec
proofs.rs:checked:IteratorProofs.next_spec
proofs.rs:checked:NextBackProofs.next_back_spec

=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas
info: aeneas: checking out revision 'be86ab0f1989d04944292b345b24c435be3ad10a'
info: mathlib: materializing new dependency
info: mathlib: fetching revision '56a005855ea17e0b0958f73ec801ae140b0a1679' from https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '56a005855ea17e0b0958f73ec801ae140b0a1679'
info: plausible: materializing new dependency
info: plausible: fetching revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24' from https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24'
info: LeanSearchClient: materializing new dependency
info: LeanSearchClient: fetching revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372' from https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372'
info: importGraph: materializing new dependency
info: importGraph: fetching revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93' from https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93'
info: proofwidgets: materializing new dependency
info: proofwidgets: fetching revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04' from https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04'
info: aesop: materializing new dependency
info: aesop: fetching revision '4a174c490d8707121c4a9290800489f105d85e07' from https://github.com/leanprover-community/aesop
info: aesop: checking out revision '4a174c490d8707121c4a9290800489f105d85e07'
info: Qq: materializing new dependency
info: Qq: fetching revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8' from https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8'
info: batteries: materializing new dependency
info: batteries: fetching revision '66e469188fe07963e5cf666c7d4433f45b8131c5' from https://github.com/leanprover-community/batteries
info: batteries: checking out revision '66e469188fe07963e5cf666c7d4433f45b8131c5'
info: Cli: materializing new dependency
info: Cli: fetching revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8' from https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8'

Environment

Original crates.io either 1.19.0 Rust and Cargo.toml, archive-compared; default features on x86_64-unknown-linux-gnu. Rust nightly-2026-09-17, Charon 08d7c9d50144bd84848212c24701253585e90d1f, Aeneas be86ab0f1989d04944292b345b24c435be3ad10a, Lean 4.35.0. Forty-one callable roots plus one actual blanket-implementation metadata root are extracted together into a single unchanged Generated.Either module; nine primary proof modules and all forty-one machine claims are jointly imported and audited. Official Charon exclusions omit twelve uncalled core Iterator defaults and official Aeneas trait filtering omits unsupported sibling methods; the original next body is byte-identical before/after filtering. No new standard model is introduced. Supplemental original source/archive/LLBC and six standard-axiom theorem audits are preserved in evidence/reference4. Integration re-generates with the official namespace flag and changes proof imports/namespace qualification only; producer compiled target caches are excluded from the public subset and enumerated separately.

What is trusted

The Rust compiler, official Charon/Aeneas translation, standard-library value models and Lean kernel are trusted. Transitive theorem axioms are restricted to propext, Classical.choice and Quot.sound. No additional axioms or custom models are used. Generic FnOnce, Into and Default computations are explicit dictionary parameters; their concrete implementations and effects are not independently verified here. Reference contracts use Aeneas's value/backward-function semantics and do not independently prove the Rust borrow checker or aliasing model. The reference4 supplement uses the same official pinned translation with a separate official namespace. Its six theorems use only the standard Lean axioms. Clone dictionary correspondence is conditional; no law that clone output equals input is assumed.

Technical limitations

Iterator::next writeback is a value/backward-state model guarantee under the supplied inner next dictionary, not verification of that concrete iterator or all Rust memory/external effects. No size_hint/len/count, finite-length or fused-iterator guarantee is added. For inspect_left/right, returning self in the extracted model must not be read as proving that callbacks cannot mutate interior/global state or that physical Rust payloads stay observationally unchanged. Only the forty-one mapped callables and their stated composition helpers are verified, not every public API. The new dispatch contracts establish branch/payload/context forwarding and modeled Result delegation, not arbitrary callback or Into correctness, success, termination, panic freedom or captured-state effects. Their normal-value theorems assume the selected call succeeds at that argument. No arbitrary mutable-context writeback or eager argument-construction claim is added. Rust Drop for discarded callbacks/payloads can panic, diverge or affect global state; destructor execution, unwind/return ordering, resource consumption and external effects are outside the value model. Modeled fail/div propagation is not a specification of every Rust panic payload or unwinding behavior. Default implementation values/termination/effects remain unverified. IntoEither uses the actual blanket dispatch, but its predicate/reference semantics retain the stated model boundary. Other inherent methods, iterator and pinning APIs, most trait/blanket implementations and serde remain unproved. into_inner still fails the untouched generated Lean do-match elaborator for the repeated T parameter; factor_ok/factor_err remain blocked by their current extraction/model limitations. All-feature/no-default configurations and other targets are not proved. The four reference-method results are supplementary model proofs only; ambiguous nominal source keys are not substituted for exact shared/mutable receiver identities. They do not guarantee arbitrary Clone correctness or termination, interior/global state preservation, Drop/panic/unwinding, external effects or physical aliasing/lifetimes. Backward-value equalities are not independent Rust memory proofs. The supplemental model and primary model are compiled in separate Lean module environments because their generated global discriminant-instance names collide on simultaneous import; no simultaneous model-equivalence bridge is claimed. The primary mappings now number41; next_back retains the selected dictionary and value-model assumptions, without arbitrary iterator termination, Drop/panic/unwinding, interior/global effect or independent memory guarantees.

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 (2)

CrateReports

serde ^1.0.95 · optional—

serde_json ^1.0.0 · dev—

Comments (0)

No comments.