Misleading non-fatal "Failed to find Kani functions" ERROR for optional hooks (SliceValidityAssume) during whole-library runs #4795

Summary

When running autoharness over a large target (the Rust standard library), the compiler logs (per crate):

ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(SliceValidityAssume)
ERROR kani_compiler::kani_middle::kani_functions Failed to find `1` Kani functions

validate_kani_functions (kani-compiler/src/kani_middle/kani_functions.rs:359) emits this via tracing::error! but does not abort — it is non-fatal. The SliceValidityAssumeHook marker (kani::slice_validity_assume, library/kani/src/arbitrary.rs) simply isn't monomorphized into every crate being compiled.

Why file it anyway

It is misleading noise: it is logged at ERROR level, repeated once per crate, and reads like a fatal "failed to find" — but the build succeeds and verification proceeds normally. During the verify-rust-std nightly bump (PR model-checking/verify-rust-std#687) this obscured the real blocker (see companion issue for the autoharness E0080).

Ask

Either:

• downgrade to debug/warn (or suppress) when the only missing entries are optional hooks not reachable in the current crate, or
• clarify the message so it is clearly non-fatal and names which crate/hook is affected.

Notes

SliceValidityAssume is not in the existing "optional model" allowlist (is_optional()), so it always counts toward missing. Confirmed non-fatal in a local autoharness run over the std library.