[srivatsansamraj]

This adds a model for &Wtf8 arguments under --bounded-arguments. Before it, 32 functions in core on a whole-library verify-std run were skipped for a missing Arbitrary implementation.

WTF-8 is a superset of UTF-8. So any_wtf8_ref is Wtf8::from_str over the existing string model, any_str_ref, with the string bound. This covers only the UTF-8 subset: values holding unpaired surrogate code points are not generated, and the reference says so. Generating them needs an encoder that coalesces surrogate pairs; #4859 tracks it.

Wtf8 has no diagnostic item, so is_wtf8 matches it by name inside core::wtf8. &mut Wtf8 stays unsupported, as &mut str does. The kani crate gains #![feature(wtf8_internals)]. std does not re-export the module, so the model names the type through core.

Tests, in cargo_autoharness_wtf8 (same shape as cargo_autoharness_byte_str):

• without --bounded-arguments, the functions are reported as requiring it;
• with it, an unchecked index fails on the empty value;
• covers show that the empty, the 4-byte and a specific string are generated.

This branch includes #4804 and #4806; only the last two commits are new here.

Resolves #4808

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

[feliperodri]

Approving, with one docs line I would like before merge. This is stacked on #4804 and #4806, so it lands third.

The gap is real — 32 functions in core skipped — and the model is the right shape.

Verified rather than read:

• Your test passes on this branch: 2 verified, the expected failure, 3/3 covers, and the without-flag skip line.
• The coverage restriction is exactly what you describe, and I measured it: a cover for a lone surrogate (ED A0..BF ..) is UNSATISFIABLE, while empty and 4-byte covers are satisfied. So harnesses over &Wtf8 will report Success having explored only the UTF-8 half.
• core::wtf8 does offer from_bytes_unchecked, so the conservative choice here was a choice, not a limitation — worth the praise inline.

The one thing I would fix before merge is the user-facing docs: they list &Wtf8 beside &str with only a length bound, so a reader will assume full WTF-8 coverage. One sentence naming the surrogate exclusion, as your description already does, closes it.

Also note this is behind main (now nightly-2026-09-22), and if you are rebasing the stack anyway, the inner-match drift I raised on #4804 is worth folding in here — with three ADTs sharing one guard, the unguarded catch-all now decides what an unrecognised ADT becomes.

[feliperodri]

@srivatsansamraj this one needs a rebase.