proofs.rs

Claim #2 — Verification of bs58::decode::DecodeBuilder::with_alphabet (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

bs58::decode::DecodeBuilder::with_alphabet

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

Any existing decoder builder and any supplied alphabet.

Formal statement

bs58.decode_builder_with_alphabet_spec

for allI : Type u_1
for allasRef : Aeneas.Std.core.convert.AsRef I (Aeneas.Std.Slice Aeneas.Std.U8)
for allbuilder : bs58.decode.DecodeBuilder I
for allalpha : bs58.alphabet.Alphabet
thenbs58.decode.DecodeBuilder.with_alphabet asRef builder alpha = Aeneas.Std.Result.ok { input := builder.input, alpha := alpha, check := builder.check }
Complete Lean proposition
∀ {I : Type u_1} (asRef : Aeneas.Std.core.convert.AsRef.{u_1, 0} I (Aeneas.Std.Slice.{0} Aeneas.Std.U8))
  (builder : bs58.decode.DecodeBuilder.{u_1} I) (alpha : bs58.alphabet.Alphabet),
  @Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (bs58.decode.DecodeBuilder.{u_1} I))
    (@bs58.decode.DecodeBuilder.with_alphabet.{u_1} I asRef builder alpha)
    (@Aeneas.Std.Result.ok.{u_1} (bs58.decode.DecodeBuilder.{u_1} I)
      (@bs58.decode.DecodeBuilder.mk.{u_1} I (@bs58.decode.DecodeBuilder.input.{u_1} I builder) alpha
        (@bs58.decode.DecodeBuilder.check.{u_1} I builder)))

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/1c8a2741db2110c65d2457d36723612560bbe5f4/bs58/0.5.1/aeneas/profiles/default/proofs/Proofs/Builder.lean#L29-L35

What is trusted

From the report

The guarantees depend on the correspondence of the Rust source to its Charon and Aeneas translation, the Aeneas models used by that translation, and Lean's kernel and logical foundations.

Technical limitations

From the report

The verified source is the unchanged bs58 0.5.1 release source. The four public proof claims cover only the builder methods described above. They do not establish Base58 output correctness, round trips, alphabet construction, buffer behavior, checksum behavior, or the behavior of other APIs. In particular, the checksum findings in findings.json are separate reproduced behaviors, not consequences of these proofs. The site could not import this release's Rustdoc format. These four API bindings are named in the verification record; Rustdoc signatures and safety classifications were not independently imported.

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 →