Claim #1 — Default initializes the FNV-1a offset basis
<fnv::FnvHasher as Default>::default
impl Default for FnvHasher
pub fn default() -> FnvHasherTool: creusot 0.13.0
Overview
default returns state 0xcbf29ce484222325 without panicking, under the shared verifier assumptions.
Preconditions
true
Evidence
What is trusted
From the report
The four methods contain no local trusted implementation bodies. Their guarantees rely on Creusot's core-operation specifications, including slice access, bitwise XOR and wrapping multiplication, and on the verifier and solvers interpreting those specifications correctly. These library models are assumptions, not proofs of the Rust standard library.
Technical limitations
From the report
The fork replaces the upstream iterator loop with an index-based while loop and adds the FNV recurrence and loop invariants. The XOR and wrapping-multiply operations are retained, but this recording does not establish formal equivalence to the published release. It covers --no-default-features, not the std feature or the HashMap, HashSet and BuildHasherDefault implementations behind the crate's type aliases. Exact FNV-1a output does not establish collision resistance or resistance to adversarial hash-table inputs. Machine-readable claims remain panic_contract; the exact state 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