Claim #21 — Verification of bs58::wrappers::max_encoded_len (with creusot 0.13.0)
bs58::wrappers::max_encoded_len
Tool: creusot 0.13.0
Preconditions
(len@ + (len@ + 1) / 2 <= usize::MAX@)
Evidence
What is trusted
From the report
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
From the report
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