Claim #2 — Lowercase encoding requires an exact output length
pub fn encode_to_slice<T: AsRef<[u8]>>(input: T, output: &mut [u8]) -> Result<(), FromHexError>Tool: creusot 0.13.0
Overview
Under the shared AsRef assumption, encode_to_slice writes two lowercase hexadecimal digits per input byte when the output length is exactly twice the input length. Otherwise it returns InvalidStringLength with the output unchanged. The verified codec has no arithmetic or indexing panics over these inputs.
Preconditions
true
Evidence
https://github.com/nyuichi/rust-crate-proofs/tree/c6d8352aecd423d311f26e64bef3ed37ec950b84
What is trusted
From the report
The generic AsRef<[u8]> bridge is assumed to return normally with the byte slice described by the input's logical model. Both public wrappers depend on this correspondence. A user-defined AsRef implementation that panics is not covered by the codec's panic-freedom result. The codec loops and error branches have body proofs; Creusot's core-operation models remain assumptions.
Technical limitations
From the report
The fork extracts the slice cores, uses high * 16 + low to combine decoded nibbles, and checks the exact encoding length through division/remainder instead of input.len() * 2. The recorded proof checks these modified bodies and their contracts; it does not formally establish equivalence to all behavior of the published crate. Alloc-backed convenience functions, formatting, serde, other generic adapters and other feature configurations are outside this report. Machine-readable claims remain panic_contract; exact codec behavior is supported by the source postconditions and recorded proofs.
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