Treat optional hooks as optional in the missing-function check

[srivatsansamraj]

Description

validate_kani_functions reports a missing Kani function unless it is an optional model:

} else if !matches!(func, KaniFunction::Model(model) if model.is_optional()) {

is_optional exists only on KaniModel, so that arm can never match a hook.
SliceValidityAssume is a hook and is only defined in the kani library, not in
core::kani, so a whole-library run logs, once per crate and at ERROR level:

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

for a condition that is not fatal.

This gives KaniHook the same is_optional method, lets KaniFunction delegate to
whichever variant it holds, and reduces the check to !func.is_optional().

Context

Absence is already handled safely. The hook implementations are a static table keyed by
KaniHook in overrides/hooks.rs, so the implementation is always present; what can be
missing is a marked function in the crate being compiled. If nothing calls
kani::slice_validity_assume, there is nothing to lower.

The doc comment on KaniHook::is_optional follows the wording already on
KaniModel::is_optional, since the reason is the same: defined in kani, absent from
core::kani.

Reported from the verify-rust-std toolchain bump
(model-checking/verify-rust-std#687), where the message is emitted 47,480 times in a
single run and obscured the real blocker.

Resolved issues

Resolves #4795

Testing

cargo build-dev, cargo fmt --check, and cargo clippy --workspace --tests -- -D warnings
with and without RUSTFLAGS="--cfg=kani_sysroot".

No unit test was added: kani_functions.rs has no test module, and the change is a
two-arm delegation over an enum the compiler already checks exhaustively.

I have not reproduced the original log output. Producing it needs a whole-library
verify-std run on nightly-2026-08-21, which currently aborts on #4794.

By submitting this pull request, I confirm that my contribution is made under the terms of
the Apache 2.0 and MIT licenses.

[Copilot]

🟢 Approval recommended

The focused change correctly suppresses misleading errors while preserving validation for required functions.

Pull request overview

Updates Kani’s missing-function validation to recognize optional hooks.

Changes:

• Marks SliceValidityAssume as optional.
• Delegates optionality checks through KaniFunction.

File summaries

File	Description
kani-compiler/src/kani_middle/kani_functions.rs	Adds hook optionality and simplifies validation.

Review details

• Files reviewed: 1/1 changed files
• Comments generated: 0
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[srivatsansamraj]

Reproduced, and the change is verified over the whole library. The "I have not reproduced the original log output" note in the description is out of date.

Before. A run stopped partway, having compiled 11 crates:

total output lines	412,399
Missing kani function, func=Hook(SliceValidityAssume)	205,903
Failed to find `1` Kani functions	205,903

411,806 of 412,399 lines, 99.9%, for a condition that is not fatal. The cost is not hypothetical: that run was killed on the assumption it had failed, because the console showed nothing else. It was compiling core normally at the time.

After. With this change, a complete run over 32 crate compilations:

total output lines	85,262
either message	0

Exit 0, kani-list.json written, 26,975 of 45,796 functions selected across 23 crates.

Three things had to be out of the way to get that far, none of them this PR, listed so the result is not read as a clean-tree run:

• The verify-rust-std branch used carries a local workaround for autoharness: E0080 abort when a const-generic fn has a const {} precondition on its usize param #4794, appending || cfg!(kani) to the core::escape const assertions. autoharness: E0080 abort when a const-generic fn has a const {} precondition on its usize param #4794 is not fixed; it is switched off on that branch.
• assert_is_non_null_like requires NonNull's pointer field to be a pointer or a fat pointer. It holds a pattern_type!(*const T is !null), which is codegenned as a single-field struct, so compiling std aborts on the assertion.
• box_value and deref_box walk RAW_PTR_FROM_BOX = ["0", "pointer", "pointer"], which stops one level above the raw pointer for the same reason. Boxing a function item then fails with Error in struct_expr; value type does not match field type on std::panicking::Hook::into_box.

The last two are unfiled. I will open them separately with a reproduction.