[srivatsansamraj]

&Wtf8 arguments now include unpaired surrogate code points. The model keeps the longest well-formed WTF-8 prefix of its nondeterministic storage, the way any_str_ref does for UTF-8. It no longer converts the output of the &str model.

WTF-8 differs from UTF-8 in one row of the byte table: after ED, the second byte may also be A0..=BF, which encodes a surrogate. One sequence stays excluded: a lead surrogate (ED A0..=AF ..) directly followed by a trail surrogate (ED B0..=BF ..). Well-formed WTF-8, which Wtf8::from_bytes_unchecked requires, writes that pair as the four-byte encoding of one supplementary code point, so the model ends the prefix there. Every well-formed string up to the bound is still generated: a string of length k arises from storage whose byte at k does not continue it.

core has no WTF-8 validator, so the check is written out in the model. Continuation bytes are checked by index, which leaves no inner loop for symbolic execution to unwind. With this model the three harnesses in cargo_autoharness_wtf8 take 10 to 11 s each, against 15 to 17 s with the &str-based one (one run each).

Tests:

• tests/expected/wtf8-surrogates calls the model at a bound of 6, which holds two surrogates. It asserts that no lead surrogate is followed by a trail surrogate. It covers a string ending in a lead surrogate, one starting with a trail surrogate, and a trail followed by a lead. With the previous model the three covers are unsatisfiable, and without the pair check the assertion fails.
• cargo_autoharness_wtf8 gains a cover for an unpaired surrogate, unsatisfiable before this change.
• The docs no longer say surrogates are excluded.

This builds on #4809. Only the last commit is new here.

Resolves #4859

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

[Copilot]

Copilot review overview

🟢 Approval recommended

The implementation and regression coverage are sound, with only minor stale compiler comments remaining.

Review effort: Balanced
Findings: 2

Open (2)

• Correct comment describing any_wtf8_ref output · New
• Update comment for AnyWtf8RefModel storage selection · New

What changed in this PR

Adds bounded autoharness generation for well-formed &Wtf8 values, including unpaired surrogates.

Changes:

• Introduces a dedicated WTF-8 prefix validator and model.
• Integrates the model into autoharness generation.
• Adds regression tests and documentation updates.

File	Description
tests/​script-based-pre/​cargo_autoharness_wtf8/​wtf8.sh	Runs autoharness integration checks.
tests/​script-based-pre/​cargo_autoharness_wtf8/​wtf8.expected	Defines expected verification output.
tests/​script-based-pre/​cargo_autoharness_wtf8/​src/​lib.rs	Exercises generated &Wtf8 values.
tests/​script-based-pre/​cargo_autoharness_wtf8/​config.yml	Configures the script-based test.
tests/​script-based-pre/​cargo_autoharness_wtf8/​Cargo.toml	Defines the test crate.
tests/​expected/​wtf8-surrogates/​main.rs	Verifies surrogate handling and well-formedness.
tests/​expected/​wtf8-surrogates/​expected	Records expected surrogate-test results.
library/​kani/​src/​lib.rs	Enables internal WTF-8 APIs.
library/​kani_core/​src/​arbitrary.rs	Implements bounded WTF-8 generation.
kani-compiler/​src/​kani_middle/​transform/​automatic.rs	Generates autoharness arguments through the new model.
kani-compiler/​src/​kani_middle/​mod.rs	Recognizes core::wtf8::Wtf8.
kani-compiler/​src/​kani_middle/​kani_functions.rs	Registers the WTF-8 model marker.
docs/​src/​reference/​experimental/​autoharness.md	Documents bounded WTF-8 support.

---

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

[feliperodri]

@srivatsansamraj needs a rebase

[srivatsansamraj]

Rebased onto main now that #4809 is in.