Claim #2 — Verification of <nohash_hasher::NoHashHasher as Clone>::clone (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

Coverage consists of Default, Clone, ten integer writers, write, and finish in the stated debug/release configurations. General Debug behavior beyond the separate u8/default-format/fixed-writer Kani domain, other inherited Hasher default methods beyond the four supplemental actual-caller API families described here, full trait-instance integration, custom Hash implementations, BuildHasherDefault, and HashMap/HashSet behavior are not verified. In particular, this does not establish that a custom IsEnabled type obeys the required single-integer-write Hash protocol. Other targets were not checked. The upstream no-std IsEnabled doctest refers to the std-only IntMap alias and does not compile; the no-std unit tests and proved method bodies pass. A supplementary clone_from theorem composes the actual clone body with the official standard-library default model and proves exact replacement by source; it is not an independent std-body proof or a separate published API claim. write_length_prefix is the pinned nightly hasher_prefixfree_extras API, not a stable-interface guarantee. The new inherited-family results are supplemental actual-caller contracts, not new registered machine API claims; primary coverage stays14. The generic contracts distinguish debug and release receiver layouts and retain IsEnabled/trait correspondence assumptions. Panic messages, unwinding, global effects, other targets/profiles and const evaluation are not established. Kani900 has narrower concrete-T/reachable-state domains and is not a premise of the generic Lean proofs. The producer consolidated regeneration script was not rerun; earlier successful individual extractions/source guards and complete kernel audits are retained, and the formal recorded build recompiles all13 supplemental declarations. The producer READY compiled_sidecars0 flag was inaccurate; twenty listed compiler sidecars are excluded from this public source subset, with an exact erratum list. write_str is also a pinned nightly hasher_prefixfree_extras API, not a stable-interface guarantee. Its producer READY zero-sidecar flag was inaccurate: sixteen listed compiler sidecars are excluded from this public87-file source subset, with exact hashes and an erratum retained. The write_str results remain supplemental actual-caller contracts with no new registered API claims. Modeled fail panic does not specify panic hooks, messages/locations, unwind/global effects or independent physical memory/alias/lifetime guarantees. Other targets/compiler settings and const evaluation are outside scope. Initial dead TwoPhaseMut-copy translation failures remain historical; the intermediate failing LLBC was not separately frozen before official re-extraction. No source, LLBC or generated body was hand edited. Consolidated portable regeneration/replay has not been run; individual generation, proof and coimport successes are retained.