proofs.rs

Report #13 — bs58 0.5.1 builder initialization and alphabet selection

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

4 verified claims · 3 findings

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

MasWag · 2026-11-03 03:48 UTC

Revision v1

Overview

bs58 provides Base58 encoding and decoding through builder APIs. With the default features (std and alloc, without check or cb58), encode::EncodeBuilder::new and decode::DecodeBuilder::new store the supplied input and alphabet with checksum mode disabled. Their respective with_alphabet methods replace the stored alphabet while preserving the input and disabled checksum state. These statements cover arbitrary inputs satisfying the API's AsRef<[u8]> bound and arbitrary supplied alphabets; the builder stores the alphabet rather than validating it.

These guarantees concern builder state only. They do not establish what happens when the builder later encodes or decodes data.

Findings (3)

APIs (4)

Recorded callables

decode::DecodeBuilder::new recorded callable · signature and safety not recorded
Claim #1
decode::DecodeBuilder::with_alphabet recorded callable · signature and safety not recorded
Claim #2
encode::EncodeBuilder::new recorded callable · signature and safety not recorded
Claim #3
encode::EncodeBuilder::with_alphabet recorded callable · signature and safety not recorded
Claim #4

Evidence

https://github.com/MasWag/crate-proofs/tree/1c8a2741db2110c65d2457d36723612560bbe5f4

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/MasWag/crate-proofs report-13-source-1
git -C report-13-source-1 checkout --detach 1c8a2741db2110c65d2457d36723612560bbe5f4
git -C report-13-source-1 submodule update --init --recursive --checkout
cd report-13-source-1/bs58/0.5.1/.work/build/default/x86_64-unknown-linux-gnu/proofs

lake build +Proofs +Proofs.Builder

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

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

run_cmd do
  let theorem_name := `bs58.decode_builder_new_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: bs58.decode_builder_new_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 bs58.decode_builder_new_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:bs58.decode_builder_new_spec"

run_cmd do
  let theorem_name := `bs58.decode_builder_with_alphabet_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: bs58.decode_builder_with_alphabet_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 bs58.decode_builder_with_alphabet_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:bs58.decode_builder_with_alphabet_spec"

run_cmd do
  let theorem_name := `bs58.encode_builder_new_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: bs58.encode_builder_new_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 bs58.encode_builder_new_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:bs58.encode_builder_new_spec"

run_cmd do
  let theorem_name := `bs58.encode_builder_with_alphabet_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: bs58.encode_builder_with_alphabet_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 bs58.encode_builder_with_alphabet_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:bs58.encode_builder_with_alphabet_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 · 4 checks passed · 0 failed

2026-11-03T03:31:43.317445654+00:00 · 193.9 seconds · Exit code 0

Recorded on the author’s machine.

CheckResultClaim
Lean checked theorem bs58.decode_builder_new_spec; axioms limited to propext, Classical.choice, Quot.sound
bs58.decode_builder_new_spec
PassedClaim #1
Lean checked theorem bs58.decode_builder_with_alphabet_spec; axioms limited to propext, Classical.choice, Quot.sound
bs58.decode_builder_with_alphabet_spec
PassedClaim #2
Lean checked theorem bs58.encode_builder_new_spec; axioms limited to propext, Classical.choice, Quot.sound
bs58.encode_builder_new_spec
PassedClaim #3
Lean checked theorem bs58.encode_builder_with_alphabet_spec; axioms limited to propext, Classical.choice, Quot.sound
bs58.encode_builder_with_alphabet_spec
PassedClaim #4
Execution details
Started
2026-11-03T03:31:43.317445654+00:00
Finished
2026-11-03T03:34:57.251782236+00:00
Platform
linux x86_64
Rust compiler
rustc 1.94.1 (e408947bf 2026-03-25) binary: rustc commit-hash: e408947bfd200af42db322daf0fadfe7e26d3bd1 commit-date: 2026-03-25 host: x86_64-unknown-linux-gnu release: 1.94.1 LLVM version: 21.1.8
Working directory
bs58/0.5.1/.work/build/default/x86_64-unknown-linux-gnu/proofs
Environment overrides
None recorded
Git repository
https://github.com/MasWag/crate-proofs
Git commit
1c8a2741db2110c65d2457d36723612560bbe5f4
Diagnostics & logs
=== stdout ===
✔ [1796/1798] Built Bs58 (23s)
✔ [1797/1798] Built Proofs.Builder (34s)
✔ [1798/1798] Built Proofs (39s)
Build completed successfully (1798 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"I","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"asRef","type":"Aeneas.Std.core.convert.AsRef I (Aeneas.Std.Slice Aeneas.Std.U8)","type_segments":[{"ref":"Aeneas.Std.core.convert.AsRef","text":"Aeneas.Std.core.convert.AsRef"},{"text":" "},{"text":"I"},{"text":" "},{"text":"("},{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"},{"text":")"}]},{"binder":"explicit","kind":"variable","name":"input","type":"I","type_segments":[{"text":"I"}]},{"binder":"explicit","kind":"variable","name":"alpha","type":"bs58.alphabet.Alphabet","type_segments":[{"ref":"bs58.alphabet.Alphabet","text":"bs58.alphabet.Alphabet"}]}],"conclusion":"bs58.encode.EncodeBuilder.new asRef input alpha =\n  Aeneas.Std.Result.ok { input := input, alpha := alpha, check := bs58.Check.Disabled }","conclusion_segments":[{"ref":"bs58.encode.EncodeBuilder.new","text":"bs58.encode.EncodeBuilder.new"},{"text":" "},{"text":"asRef"},{"text":" "},{"text":"input"},{"text":" "},{"text":"alpha"},{"ref":"Eq","text":" =\n  "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"ref":"bs58.encode.EncodeBuilder.mk","text":"{ "},{"text":"input"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" := "},{"text":"input"},{"ref":"bs58.encode.EncodeBuilder.mk","text":", "},{"text":"alpha"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" := "},{"text":"alpha"},{"ref":"bs58.encode.EncodeBuilder.mk","text":", "},{"text":"check"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" := "},{"ref":"bs58.Check.Disabled","text":"bs58.Check.Disabled"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" }"}],"definitions":[{"module":"Aeneas.Std.Core.Convert","name":"Aeneas.Std.core.convert.AsRef","source":{"first_line":27,"last_line":29}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Bs58","name":"bs58.alphabet.Alphabet","source":{"first_line":23,"last_line":28}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder","source":{"first_line":64,"last_line":70}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder.new","source":{"first_line":72,"last_line":80}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder.mk","source":{"first_line":67,"last_line":67}},{"module":"Bs58","name":"bs58.Check.Disabled","source":{"first_line":34,"last_line":34}}],"definitions_truncated":false,"first_line":7,"last_line":12,"module":"Proofs.Builder","program":null,"program_head":null,"statement":"∀ {I : Type u_1} (asRef : Aeneas.Std.core.convert.AsRef.{u_1, 0} I (Aeneas.Std.Slice.{0} Aeneas.Std.U8)) (input : I)\n  (alpha : bs58.alphabet.Alphabet),\n  @Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (bs58.encode.EncodeBuilder.{u_1} I))\n    (@bs58.encode.EncodeBuilder.new.{u_1} I asRef input alpha)\n    (@Aeneas.Std.Result.ok.{u_1} (bs58.encode.EncodeBuilder.{u_1} I)\n      (@bs58.encode.EncodeBuilder.mk.{u_1} I input alpha bs58.Check.Disabled))","theorem":"bs58.encode_builder_new_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"I","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"asRef","type":"Aeneas.Std.core.convert.AsRef I (Aeneas.Std.Slice Aeneas.Std.U8)","type_segments":[{"ref":"Aeneas.Std.core.convert.AsRef","text":"Aeneas.Std.core.convert.AsRef"},{"text":" "},{"text":"I"},{"text":" "},{"text":"("},{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"},{"text":")"}]},{"binder":"explicit","kind":"variable","name":"builder","type":"bs58.decode.DecodeBuilder I","type_segments":[{"ref":"bs58.decode.DecodeBuilder","text":"bs58.decode.DecodeBuilder"},{"text":" "},{"text":"I"}]},{"binder":"explicit","kind":"variable","name":"alpha","type":"bs58.alphabet.Alphabet","type_segments":[{"ref":"bs58.alphabet.Alphabet","text":"bs58.alphabet.Alphabet"}]}],"conclusion":"bs58.decode.DecodeBuilder.with_alphabet asRef builder alpha =\n  Aeneas.Std.Result.ok { input := builder.input, alpha := alpha, check := builder.check }","conclusion_segments":[{"ref":"bs58.decode.DecodeBuilder.with_alphabet","text":"bs58.decode.DecodeBuilder.with_alphabet"},{"text":" "},{"text":"asRef"},{"text":" "},{"text":"builder"},{"text":" "},{"text":"alpha"},{"ref":"Eq","text":" =\n  "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"ref":"bs58.decode.DecodeBuilder.mk","text":"{ "},{"text":"input"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" := "},{"text":"builder"},{"text":"."},{"ref":"bs58.decode.DecodeBuilder.input","text":"input"},{"ref":"bs58.decode.DecodeBuilder.mk","text":", "},{"text":"alpha"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" := "},{"text":"alpha"},{"ref":"bs58.decode.DecodeBuilder.mk","text":", "},{"text":"check"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" := "},{"text":"builder"},{"text":"."},{"ref":"bs58.decode.DecodeBuilder.check","text":"check"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" }"}],"definitions":[{"module":"Aeneas.Std.Core.Convert","name":"Aeneas.Std.core.convert.AsRef","source":{"first_line":27,"last_line":29}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder","source":{"first_line":36,"last_line":42}},{"module":"Bs58","name":"bs58.alphabet.Alphabet","source":{"first_line":23,"last_line":28}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder.with_alphabet","source":{"first_line":54,"last_line":62}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder.mk","source":{"first_line":39,"last_line":39}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder.input","source":{"first_line":40,"last_line":40}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder.check","source":{"first_line":42,"last_line":42}}],"definitions_truncated":false,"first_line":29,"last_line":35,"module":"Proofs.Builder","program":null,"program_head":null,"statement":"∀ {I : Type u_1} (asRef : Aeneas.Std.core.convert.AsRef.{u_1, 0} I (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n  (builder : bs58.decode.DecodeBuilder.{u_1} I) (alpha : bs58.alphabet.Alphabet),\n  @Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (bs58.decode.DecodeBuilder.{u_1} I))\n    (@bs58.decode.DecodeBuilder.with_alphabet.{u_1} I asRef builder alpha)\n    (@Aeneas.Std.Result.ok.{u_1} (bs58.decode.DecodeBuilder.{u_1} I)\n      (@bs58.decode.DecodeBuilder.mk.{u_1} I (@bs58.decode.DecodeBuilder.input.{u_1} I builder) alpha\n        (@bs58.decode.DecodeBuilder.check.{u_1} I builder)))","theorem":"bs58.decode_builder_with_alphabet_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"I","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"asRef","type":"Aeneas.Std.core.convert.AsRef I (Aeneas.Std.Slice Aeneas.Std.U8)","type_segments":[{"ref":"Aeneas.Std.core.convert.AsRef","text":"Aeneas.Std.core.convert.AsRef"},{"text":" "},{"text":"I"},{"text":" "},{"text":"("},{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"},{"text":")"}]},{"binder":"explicit","kind":"variable","name":"input","type":"I","type_segments":[{"text":"I"}]},{"binder":"explicit","kind":"variable","name":"alpha","type":"bs58.alphabet.Alphabet","type_segments":[{"ref":"bs58.alphabet.Alphabet","text":"bs58.alphabet.Alphabet"}]}],"conclusion":"bs58.decode.DecodeBuilder.new asRef input alpha =\n  Aeneas.Std.Result.ok { input := input, alpha := alpha, check := bs58.Check.Disabled }","conclusion_segments":[{"ref":"bs58.decode.DecodeBuilder.new","text":"bs58.decode.DecodeBuilder.new"},{"text":" "},{"text":"asRef"},{"text":" "},{"text":"input"},{"text":" "},{"text":"alpha"},{"ref":"Eq","text":" =\n  "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"ref":"bs58.decode.DecodeBuilder.mk","text":"{ "},{"text":"input"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" := "},{"text":"input"},{"ref":"bs58.decode.DecodeBuilder.mk","text":", "},{"text":"alpha"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" := "},{"text":"alpha"},{"ref":"bs58.decode.DecodeBuilder.mk","text":", "},{"text":"check"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" := "},{"ref":"bs58.Check.Disabled","text":"bs58.Check.Disabled"},{"ref":"bs58.decode.DecodeBuilder.mk","text":" }"}],"definitions":[{"module":"Aeneas.Std.Core.Convert","name":"Aeneas.Std.core.convert.AsRef","source":{"first_line":27,"last_line":29}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Bs58","name":"bs58.alphabet.Alphabet","source":{"first_line":23,"last_line":28}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder","source":{"first_line":36,"last_line":42}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder.new","source":{"first_line":44,"last_line":52}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bs58","name":"bs58.decode.DecodeBuilder.mk","source":{"first_line":39,"last_line":39}},{"module":"Bs58","name":"bs58.Check.Disabled","source":{"first_line":34,"last_line":34}}],"definitions_truncated":false,"first_line":22,"last_line":27,"module":"Proofs.Builder","program":null,"program_head":null,"statement":"∀ {I : Type u_1} (asRef : Aeneas.Std.core.convert.AsRef.{u_1, 0} I (Aeneas.Std.Slice.{0} Aeneas.Std.U8)) (input : I)\n  (alpha : bs58.alphabet.Alphabet),\n  @Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (bs58.decode.DecodeBuilder.{u_1} I))\n    (@bs58.decode.DecodeBuilder.new.{u_1} I asRef input alpha)\n    (@Aeneas.Std.Result.ok.{u_1} (bs58.decode.DecodeBuilder.{u_1} I)\n      (@bs58.decode.DecodeBuilder.mk.{u_1} I input alpha bs58.Check.Disabled))","theorem":"bs58.decode_builder_new_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"I","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"asRef","type":"Aeneas.Std.core.convert.AsRef I (Aeneas.Std.Slice Aeneas.Std.U8)","type_segments":[{"ref":"Aeneas.Std.core.convert.AsRef","text":"Aeneas.Std.core.convert.AsRef"},{"text":" "},{"text":"I"},{"text":" "},{"text":"("},{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"},{"text":")"}]},{"binder":"explicit","kind":"variable","name":"builder","type":"bs58.encode.EncodeBuilder I","type_segments":[{"ref":"bs58.encode.EncodeBuilder","text":"bs58.encode.EncodeBuilder"},{"text":" "},{"text":"I"}]},{"binder":"explicit","kind":"variable","name":"alpha","type":"bs58.alphabet.Alphabet","type_segments":[{"ref":"bs58.alphabet.Alphabet","text":"bs58.alphabet.Alphabet"}]}],"conclusion":"bs58.encode.EncodeBuilder.with_alphabet asRef builder alpha =\n  Aeneas.Std.Result.ok { input := builder.input, alpha := alpha, check := builder.check }","conclusion_segments":[{"ref":"bs58.encode.EncodeBuilder.with_alphabet","text":"bs58.encode.EncodeBuilder.with_alphabet"},{"text":" "},{"text":"asRef"},{"text":" "},{"text":"builder"},{"text":" "},{"text":"alpha"},{"ref":"Eq","text":" =\n  "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"ref":"bs58.encode.EncodeBuilder.mk","text":"{ "},{"text":"input"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" := "},{"text":"builder"},{"text":"."},{"ref":"bs58.encode.EncodeBuilder.input","text":"input"},{"ref":"bs58.encode.EncodeBuilder.mk","text":", "},{"text":"alpha"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" := "},{"text":"alpha"},{"ref":"bs58.encode.EncodeBuilder.mk","text":", "},{"text":"check"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" := "},{"text":"builder"},{"text":"."},{"ref":"bs58.encode.EncodeBuilder.check","text":"check"},{"ref":"bs58.encode.EncodeBuilder.mk","text":" }"}],"definitions":[{"module":"Aeneas.Std.Core.Convert","name":"Aeneas.Std.core.convert.AsRef","source":{"first_line":27,"last_line":29}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder","source":{"first_line":64,"last_line":70}},{"module":"Bs58","name":"bs58.alphabet.Alphabet","source":{"first_line":23,"last_line":28}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder.with_alphabet","source":{"first_line":82,"last_line":90}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder.mk","source":{"first_line":67,"last_line":67}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder.input","source":{"first_line":68,"last_line":68}},{"module":"Bs58","name":"bs58.encode.EncodeBuilder.check","source":{"first_line":70,"last_line":70}}],"definitions_truncated":false,"first_line":14,"last_line":20,"module":"Proofs.Builder","program":null,"program_head":null,"statement":"∀ {I : Type u_1} (asRef : Aeneas.Std.core.convert.AsRef.{u_1, 0} I (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n  (builder : bs58.encode.EncodeBuilder.{u_1} I) (alpha : bs58.alphabet.Alphabet),\n  @Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (bs58.encode.EncodeBuilder.{u_1} I))\n    (@bs58.encode.EncodeBuilder.with_alphabet.{u_1} I asRef builder alpha)\n    (@Aeneas.Std.Result.ok.{u_1} (bs58.encode.EncodeBuilder.{u_1} I)\n      (@bs58.encode.EncodeBuilder.mk.{u_1} I (@bs58.encode.EncodeBuilder.input.{u_1} I builder) alpha\n        (@bs58.encode.EncodeBuilder.check.{u_1} I builder)))","theorem":"bs58.encode_builder_with_alphabet_spec","translation_rerun":false,"version":1}

=== stderr ===
Environment

The selected model uses unmodified Aeneas be86ab0f1989d04944292b345b24c435be3ad10a, Charon 08d7c9d50144bd84848212c24701253585e90d1f, and Lean 4.35.0 on Linux x86_64. The default feature configuration is used for extraction. The native Rust tests and checksum reproductions are separate from the formal proof; the checksum reproductions enable check and cb58. The release archive inventory is pinned in source.lock.json; the exact tool commits and reviewed proofs-rs CLI patch are recorded in toolchain.lock.json and the patch. Aeneas and Charon have empty patch lists; the CLI patch prepares managed inputs and catalogs public methods in generic inherent impls before standard Lake build and audit.

What is trusted

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

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

Dependencies (8)

CrateReports
assert_matches ^1.3.0 · dev—
base58 ^0.1.0 · dev—
criterion ^0.5 · dev—
rust-base58 ^0.0.4 · dev—
sha2 ^0.10 · optional—
smallvec ^1 · optional—
tinyvec ^1.6.0 · dev—
tinyvec ^1.6.0 · optional—

Comments (0)

No comments.

Sign in to comment.