Autoharness: models for alloc types in the verify-std flow #4807

Requested feature: autoharness models for heap types (Vec, String, Box, Rc, Arc, and the BoundedArbitrary implementations) in the verify-std flow, where they are currently absent.

Use case: on a whole-library verify-std run (nightly-2026-08-21, with --bounded-arguments), 6,869 functions are skipped for a missing Arbitrary implementation. Roughly a thousand of them take an alloc type: methods on Vec<T> and &mut Vec<T> (about 120), VecDeque (about 115), String (about 210), BinaryHeap, CString, ByteString, Wtf8Buf, and the alloc and std functions that take any of these. The implementations exist in library/kani, but verify-std compiles core, alloc and std against kani_core only, and kani_lib!(core) cannot implement Arbitrary for a type defined in alloc. #4721 and #4698 note the models are "absent in verify-std's no-core flow". This asks whether closing that is wanted, and in what shape.

Link to relevant documentation (Rust reference, Nomicon, RFC): https://doc.rust-lang.org/alloc/ (the crate that defines Vec, String and Box; core cannot name them)

Test case:

$ kani autoharness -Z autoharness --bounded-arguments --list --std ./library
...
| alloc | <vec::Vec<i32> as core::clone::Clone>::clone | Missing Arbitrary implementation for argument(s) self: &vec::Vec<i32> |
| alloc | vec::Vec::<i32>::clear                        | Missing Arbitrary implementation for argument(s) self: &mut vec::Vec<i32> |

A shape that seems to fit what is already there: find_kani_functions collects marked functions from every crate in the graph rather than the first one that has any (is_optional already tolerates the partial set when compiling core); kani_lib! gains an (alloc) arm that implements core::kani::Arbitrary for alloc's types, with those implementations moved from library/kani into kani_core so there is one source; and verify-rust-std adds kani_core::kani_lib!(alloc); beside the existing line for core. About 20 changed lines in the compiler, about 350 moved in the library, one line in verify-rust-std; verify_std_cmd can exercise it in minutes. I can take it if the shape is right, or adjust it.