Claim #2 — with_key preserves every supplied u64 initial state
impl FnvHasher
pub fn with_key(key: u64) -> FnvHasherTool: creusot 0.13.0
Overview
For every u64 key, with_key returns that exact initial state without panicking. The key is the starting hash state; this result does not establish a cryptographic keyed-hash property.
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