proofs.rs

Recorded run

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 ===