Claim #1 — Decoding with exact error priority and partial-output behavior
pub fn decode_to_slice<T: AsRef<[u8]>>(data: T, out: &mut [u8]) -> Result<(), FromHexError>Tool: creusot 0.13.0
Overview
Under the shared AsRef assumption, decode_to_slice handles arbitrary input bytes and output lengths without codec arithmetic or indexing panics. OddLength takes priority over InvalidStringLength and neither modifies output. With matching lengths, the first invalid byte is reported with its character and byte index; only complete preceding pairs are written. Valid mixed-case hexadecimal input produces the complete decoded bytes.
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