Report #19 — bs58 0.5.1: Base58 core and selected builder behavior in a proof fork
21 verified claims · 3 findings
Overview
bs58 converts byte sequences to Base58 symbols and back. This report describes contracts for an adapted proof fork of bs58 0.5.1. A fresh integrated verification checks the selected core functions, helpers and extension wrappers; the previously accepted core result is documented separately. The codec guarantees require a valid alphabet and disabled checksum checking.
The core encoder preserves the input's base-256 numeric value in base 58 and maps each leading zero byte to a leading zero symbol. The decoder preserves the numeric value in base 256 and maps each leading zero symbol to a zero byte. Each returns the exact output prefix and length if it fits, or BufferTooSmall otherwise. For invalid encoded input, the decoder reports the first non-ASCII byte index or the first invalid ASCII character and its index, unless an earlier valid prefix has already exceeded the output capacity, in which case it reports BufferTooSmall first. On success both leave the unused output suffix unchanged; errors do not promise rollback. The fixed-array decoder returns the decoded bytes padded with zeros, without requiring the decoded length to equal the array length. The four selected core functions terminate and satisfy their checked panic obligations within their modeled domains.
Alphabet::new accepts exactly distinct ASCII arrays of 58 bytes and otherwise identifies the first non-ASCII or duplicate byte with its specified indices and character. The selected runtime constructor and convenience contracts cover successful new_unwrap and the validity of BITCOIN, MONERO, RIPPLE, FLICKR and DEFAULT; MONERO and BITCOIN have equal tables, and DEFAULT is BITCOIN. The fixed-array unwrap requires successful decoding; invalid inputs deliberately panic.
For concrete byte-slice inputs and byte-slice targets (and the decoder’s array target), disabled-check builder operations carry the core result and mutation guarantees through the selected dispatch. The encoded length bound for input length n is h(n) = n + floor((n + 1) / 2); evaluating it requires the intermediate and final machine additions to fit usize. Under the stock allocation model, with a valid alphabet and the stated machine addition bounds, the specialized growing-vector encoder appends the exact encoding and succeeds. The corresponding decoder appends the exact decoding on success; it cannot return BufferTooSmall for any input, although character errors remain possible. Both preserve the old vector prefix. On decode error the vector retains its enlarged length and the partially modified appended tail. The into_vec variants start empty and return the exact output on success.
The mathematical relations establish both round trips: decoding an encoding recovers the input bytes, and encoding a valid alphabet-only sequence after decoding recovers that sequence. A separate composed operation establishes the actual encoding-to-decoding vector round trip under its length and alphabet premises. Builder constructors and alphabet setters preserve their specified fields. In the full-feature state projection, checksum setters establish only the resulting mode and version fields. Selected error Clone and PartialEq behavior and Alphabet Clone are also covered by their contracts. See the core specification and extension specification for exact relations.
Findings (3)
Checked decoding changes buffer bytes after the returned length
InvalidChecksum fields disagree with their documentation
APIs (21)
Recorded callables
Evidence
https://github.com/MasWag/crate-proofs/tree/6fb3cb5ed542d95438e778eacf3a5af45d1b0db9
Reproduce
Run locally
git clone -- https://github.com/MasWag/crate-proofs report-19-source-1
git -C report-19-source-1 checkout --detach 6fb3cb5ed542d95438e778eacf3a5af45d1b0db9
git -C report-19-source-1 submodule update --init --recursive --checkout
cd report-19-source-1/bs58/0.5.1/creusot/extensions/publication/crate
cargo creusot --no-cache --span-mode absolute --why3find-arg=-j --why3find-arg=2Source on GitHub · SARIF with logs (.json)
Recorded run
Completed · 65 checks passed · 0 failed
| Check | Result | Claim |
|---|---|---|
| vc_decode_append_step | Passed | Claim #1 |
| vc_decode_horner_step | Passed | Claim #1 |
| vc_decode_into | Passed | Claim #1 |
| vc_decode_tail_step | Passed | Claim #1 |
| vc_full_prefix_le | Passed | Claim #1 |
| vc_len_u8 | Passed | Claim #1 |
| vc_new_unit | Passed | Claim #1 |
| vc_decode_append_step | Passed | Claim #2 |
| vc_decode_horner_step | Passed | Claim #2 |
| vc_decode_into_const | Passed | Claim #2 |
| vc_le_extend_step | Passed | Claim #2 |
| vc_len_u8 | Passed | Claim #2 |
| vc_new_unit | Passed | Claim #2 |
| vc_decode_I | Passed | Claim #3 |
| vc_from_input_I | Passed | Claim #3 |
| vc_new_unwrap | Passed | Claim #3 |
| vc_set_BITCOIN | Passed | Claim #3 |
| vc_set_DEFAULT | Passed | Claim #3 |
| vc_encode_I | Passed | Claim #4 |
| vc_from_input_I | Passed | Claim #4 |
| vc_new_unwrap | Passed | Claim #4 |
| vc_set_BITCOIN | Passed | Claim #4 |
| vc_set_DEFAULT | Passed | Claim #4 |
| vc_bitcoin | Passed | Claim #5 |
| vc_new_unwrap | Passed | Claim #5 |
| vc_append_step | Passed | Claim #6 |
| vc_encode_into | Passed | Claim #6 |
| vc_horner_step | Passed | Claim #6 |
| vc_len_u8 | Passed | Claim #6 |
| vc_new_unit | Passed | Claim #6 |
| vc_len_u8 | Passed | Claim #7 |
| vc_new | Passed | Claim #7 |
| vc_clone_AlphabetError | Passed | Claim #8 |
| vc_clone_DecodeError | Passed | Claim #9 |
| vc_clone_EncodeError | Passed | Claim #10 |
| vc_grow_zero | Passed | Claim #11 |
| vc_len_u8 | Passed | Claim #11 |
| vc_push_u8 | Passed | Claim #11 |
| vc_len_u8 | Passed | Claim #12 |
| vc_pop_u8 | Passed | Claim #12 |
| vc_truncate | Passed | Claim #12 |
| vc_elim_Err | Passed | Claim #13 |
| vc_elim_Ok | Passed | Claim #13 |
| vc_encode_decode_roundtrip | Passed | Claim #13 |
| vc_from_str | Passed | Claim #13 |
| vc_index_Vec_u8_Global | Passed | Claim #13 |
| vc_into_vec | Passed | Claim #13 |
| vc_into_vec'0 | Passed | Claim #13 |
| vc_new_ref_slice_u8 | Passed | Claim #13 |
| vc_new_ref_slice_u8'0 | Passed | Claim #13 |
| vc_elim_Ok | Passed | Claim #14 |
| vc_new | Passed | Claim #14 |
| vc_new_unwrap | Passed | Claim #14 |
| vc_clone_Alphabet | Passed | Claim #15 |
| vc_call_once_impl_32_for_60__39_a_62__32_FnOnce_40__38__39_a_32_mut_32__91_u8_93__41__32__45__62__32_Result_60_usize_44__32_DecodeError_62_ | Passed | Claim #16 |
| vc_decode_with_array_u8_n | Passed | Claim #16 |
| vc_decode_with_T | Passed | Claim #17 |
| vc_decode_with_refmut_T | Passed | Claim #17 |
| vc_call_once_impl_32_for_60__39_a_62__32_FnOnce_40__38__39_a_32_mut_32__91_u8_93__41__32__45__62__32_Result_60_usize_44__32_DecodeError_62_ | Passed | Claim #18 |
| vc_decode_with_slice_u8 | Passed | Claim #18 |
| vc_encode_with_T | Passed | Claim #19 |
| vc_encode_with_refmut_T | Passed | Claim #19 |
| vc_call_once_impl_32_for_60__39_a_62__32_FnOnce_40__38__39_a_32_mut_32__91_u8_93__41__32__45__62__32_Result_60_usize_44__32_EncodeError_62_ | Passed | Claim #20 |
| vc_encode_with_slice_u8 | Passed | Claim #20 |
| vc_max_encoded_len | Passed | Claim #21 |
Execution details
- Started
- 2026-11-04T17:29:49.197007952+00:00
- Finished
- 2026-11-04T17:35:09.887477880+00:00
- Platform
- linux x86_64
- Rust compiler
- rustc 1.98.0-nightly (91fe22da8 2026-06-21) binary: rustc commit-hash: 91fe22da8084a1c9e993d78d4a56f22ab8396236 commit-date: 2026-06-21 host: x86_64-unknown-linux-gnu release: 1.98.0-nightly LLVM version: 22.1.7
- Working directory
- bs58/0.5.1/creusot/extensions/publication/crate
- Environment overrides
- None recorded
- Git repository
- https://github.com/MasWag/crate-proofs
- Git commit
- 6fb3cb5ed542d95438e778eacf3a5af45d1b0db9
Diagnostics & logs
=== stdout ===
Proved (135 files) ✔
=== stderr ===
warning: patch `creusot-std v0.15.0-dev (/home/lab8/mwaga/creusot/creusot-std)` was not used in the crate graph
help: Check that the patched package version and available features are compatible
with the dependency requirements. If the patch has a different version from
what is locked in the Cargo.lock file, run `cargo update` to use the new
version. This may also occur with an optional dependency that is not enabled.
Compiling proc-macro2 v1.0.107
Compiling libc v0.2.191
Compiling quote v1.0.47
Compiling unicode-ident v1.0.27
Compiling getrandom v0.4.3
Compiling cfg-if v1.0.5
Compiling syn v2.0.119
Compiling uuid v1.29.0
Compiling pearlite-syn v0.13.0
Compiling creusot-std-proc v0.13.0
Checking creusot-std v0.13.0
Checking bs58 v0.5.1 (./bs58/0.5.1/creusot/extensions/publication/crate)
warning: unnecessary parentheses around function argument
--> src/lib.rs:491:31
|
491 | && (val@ == 0 ==> (index@ == 0 || output@[index@ - 1] != 0u8))
| ^ ^
|
= note: `#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default
help: remove these parentheses
|
491 - && (val@ == 0 ==> (index@ == 0 || output@[index@ - 1] != 0u8))
491 + && (val@ == 0 ==> index@ == 0 || output@[index@ - 1] != 0u8)
|
warning: unnecessary parentheses around function argument
--> src/lib.rs:833:31
|
833 | && (val@ == 0 ==> (index@ == 0 || output@[index@ - 1] != 0u8))
| ^ ^
|
help: remove these parentheses
|
833 - && (val@ == 0 ==> (index@ == 0 || output@[index@ - 1] != 0u8))
833 + && (val@ == 0 ==> index@ == 0 || output@[index@ - 1] != 0u8)
|
warning: unnecessary parentheses around function argument
--> src/wrappers.rs:128:34
|
128 | #[cfg_attr(creusot, ensures(^(^self) == ^*self))]
| ^ ^
|
help: remove these parentheses
|
128 - #[cfg_attr(creusot, ensures(^(^self) == ^*self))]
128 + #[cfg_attr(creusot, ensures(^^self == ^*self))]
|
warning: unnecessary parentheses around function argument
--> src/wrappers.rs:137:34
|
137 | #[cfg_attr(creusot, ensures(^(^self) == ^*self))]
| ^ ^
|
help: remove these parentheses
|
137 - #[cfg_attr(creusot, ensures(^(^self) == ^*self))]
137 + #[cfg_attr(creusot, ensures(^^self == ^*self))]
|
warning: `result` used as a parameter name. It is confusing because it is also the default name of the function's result
--> src/spec.rs:105:39
|
105 | pub fn alphabet_result(base: Seq<u8>, result: Result<Alphabet, AlphabetError>) -> bool {
| ^^^^^^
|
= note: `#[warn(creusot::result_param)]` on by default
warning: `result` used as a parameter name. It is confusing because it is also the default name of the function's result
--> src/spec.rs:174:39
|
174 | encode: Seq<u8>, decode: Seq<u8>, result: Result<usize, EncodeError>) -> bool {
| ^^^^^^
warning: `result` used as a parameter name. It is confusing because it is also the default name of the function's result
--> src/spec.rs:213:39
|
213 | encode: Seq<u8>, decode: Seq<u8>, result: Result<usize, DecodeError>) -> bool {
| ^^^^^^
warning: `result` used as a parameter name. It is confusing because it is also the default name of the function's result
--> src/spec.rs:226:5
|
226 | result: Result<[u8; N], DecodeError>) -> bool {
| ^^^^^^
warning: `bs58` (lib) generated 8 warnings (run `cargo fix --lib -p bs58` to apply 4 suggestions)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 33.15s
Environment
The original accepted core proof used unmodified Creusot 0.13.0 on x86_64 Linux with its standard models; its results describe that historical run. A fresh integrated run verified the selected core bodies, helpers and extension wrappers together using unmodified Creusot 0.13.0 and its standard models. A local checker audited trait goals and printer identity; it was reviewed and tested with negative controls and does not modify the verifier. A separate native comparison exercised the adapted implementation against the release, including complete modeled byte and error states; finite comparisons are not an equivalence theorem. The extension results and evidence summary describe the fresh run, and tool identities document the toolchain.
The standard cargo-proofs recording imported panic-contract verification for 21 named fork functions, a subset of the selected coverage. The complete functional verification and inventory include the selected generic builder methods and trait refinements omitted from those API bindings. The bindings name functions from the verification fork; Rustdoc signatures and safety classifications were not independently imported. See the recording receipt for the recording and its scope.
What is trusted
The guarantees rely on the Rust compiler, Creusot translation and its shipped standard-library models, Why3 transformations, and SMT solvers. The selected extension uses unmodified standard models, with no trusted application algorithm or arithmetic lemma. Vector correctness relies on the modeled sequence behavior of push, pop, and range indexing; the checked loops preserve the specified byte contents and lengths. Physical capacity-limit panics, including Rust allocation-domain limits, and resource failures are outside these models.
Technical limitations
This is an adapted verification fork, not the unchanged release. The core specializes the generic encoder to byte slices and uses index loops, explicit reversal and bounded arithmetic expressions. The extension specializes inputs and targets and replaces vector resize and truncate with push-zero and pop loops, changing allocation strategy and cost. Vector guarantees cover byte contents and logical length and prefix; capacity, pointer identity, and allocation-call sequence are outside those claims. Its onto_vec adapters call the core directly on the appended tail rather than verifying generic Vec target dispatch. Source review and finite native comparisons support correspondence to the release, but there is no formal release-equivalence theorem. See core correspondence and extension correspondence.
Generic target behavior is conditional on its callback contract; arbitrary legal targets need not invoke the callback. Arbitrary AsRef observations need not be stable. A conventional generic iterator guarantee requires a checked law that the original and cloned IntoIterator values produce identical finite sequences; Clone + IntoIterator alone does not establish it. The runtime fixed-array and alphabet proofs do not establish compiler constant-evaluation semantics. No blanket termination claim is made for the wrappers.
Checksum state updates do not prove digest computation or checked codec behavior. SHA calls lack the necessary contracts in the installed models. String construction and mutation, UTF-8 repair and the ASCII-to-byte bridge also lack the needed model relations; observable formatting is unmodeled. The observed optional-container model gaps include calls used for SmallVec and tinyvec resizing and spare-slice access; their adapters are not covered. The report does not establish whole-crate undefined-behavior freedom, cryptographic properties, or string formatting. The existing findings concern separately reproduced checksum behavior. Details are in the model boundaries.
Tool limitations
Verification is relative to the supplied specifications and trusted contracts. Results apply to the compilation target used for verification. The standard-library specifications do not exclude all panics: Vec capacity overflow in operations such as push, insert, and extend is not ruled out, including for vectors of zero-sized types. Out-of-memory failures are also outside the guarantees. The standard vec! macro is unsupported; verified code must use the Creusot replacement where needed. Reference: https://github.com/creusot-rs/creusot/blob/v0.13.0/guide/src/limitations.md
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.