proofs.rs

Claim #1 — Verification of <&T as unindent::Unindent>::unindent (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

<&T as unindent::Unindent>::unindent

Recorded callable · signature and safety not independently recorded.

Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

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

Preconditions

The underlying T::unindent returns successfully and its output satisfies the chosen postcondition.

Formal statement

unindent.Proofs.shared_unindent_spec

for allT : Type
for allO : Type
for allinst : unindent.unindent.Unindent T O
for allself : T
for allpost : O → Prop
assumeh : ∃ out, inst.unindent self = Aeneas.Std.Result.ok out ∧ post out
then∃ out, unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent inst self = Aeneas.Std.Result.ok out ∧ post out
Complete Lean proposition
∀ {T O : Type} (inst : unindent.unindent.Unindent.{0, 0} T O) (self : T) (post : O → Prop)
  (h :
    @Exists.{1} O fun (out : O) =>
      And
        (@Eq.{1} (Aeneas.Std.Result.{0} O) (@unindent.unindent.Unindent.unindent.{0, 0} T O inst self)
          (@Aeneas.Std.Result.ok.{0} O out))
        (post out)),
  @Exists.{1} O fun (out : O) =>
    And
      (@Eq.{1} (Aeneas.Std.Result.{0} O)
        (@unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent.{0, 0} T O inst self)
        (@Aeneas.Std.Result.ok.{0} O out))
      (post out)

Theorem source at recorded commit · Recorded check

Referenced definitions (up to 100 direct references)

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

Evidence

https://github.com/MasWag/crate-proofs/blob/cabbee9506c6abcc2b9a42e7694ddc2ebdf7f07d/unindent/0.2.4/aeneas/profiles/default/proofs/Proofs/Delegation.lean#L9-L13

What is trusted

From the report

The claim relies on the Aeneas translation and its Rust models, and on Lean's kernel. The underlying implementation's successful result and the chosen output property are premises, not established by this delegation theorem.

Technical limitations

From the report

The core unindent and unindent_bytes algorithms, including UTF-8 preservation and behavior on arbitrary bytes, have not been proved. Nor does this result establish the behavior of the concrete str, String, or byte-slice implementations. Allocation and behavior outside the modeled execution are not established.

Tool limitations

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

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Read and join the discussion on the report →