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.

Reproduced on a whole-library verify-std run on nightly-2026-08-21. Before the change, a run stopped after 11 crates had printed 412,399 lines, 411,806 of them these two messages. With it, a complete run over 32 crate compilations printed 85,262 lines and neither message. That run needed a local workaround for #4794 (since fixed by #4820) and the NonNull fixes in #4801.

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.

[feliperodri]

Approving.

I hit this myself without looking for it: a std autoharness run of mine logged 1,278 of each message in a 3,317-line log, roughly 77% of the output, at ERROR level, for something non-fatal. Your numbers match what I saw.

The fix is in the right place. slice_validity_assume's only callers are any_slice_ref_unbounded, any_slice_mut_unbounded and any_vec_unbounded, all three already in KaniModel::is_optional() — the hook was simply missed when that list was written. If it is absent its callers are too, and the library body is unreachable!(), so a genuinely missed lowering still fails loudly rather than silently.

Two non-blocking asks: fold your reproduction comment into the description, which still says you have not reproduced the output; and file the NonNull pattern-type and RAW_PTR_FROM_BOX findings from that comment separately — the second looks related to #4800.

[srivatsansamraj]

Thanks, folded the reproduction into the description; both findings are filed as #4800 and fixed together in #4801.