Add Arbitrary implementation for std::ascii::EscapeDefault

[acearyanarun]

Summary

Adds an Arbitrary implementation for std::ascii::EscapeDefault.

EscapeDefault was previously unsupported by Autoharness because Kani could not generate arbitrary values for the type. This implementation constructs a valid EscapeDefault and nondeterministically consumes elements from the front and back so that Kani can represent fresh, partially consumed, and exhausted iterator states.

This allows Autoharness to automatically generate and verify harnesses for functions that take std::ascii::EscapeDefault as an argument.

Testing

Added a Kani proof that checks generated EscapeDefault values have at most four remaining elements and confirms that all remaining lengths from 0 through 4 are reachable.

Local verification with CBMC 6.11.0:

• 0 verification failures
• 5 of 5 cover properties satisfied
• VERIFICATION:- SUCCESSFUL

Also added a script-based Autoharness regression test confirming that:

consume_escape_default(std::ascii::EscapeDefault)

is selected by Autoharness and successfully verified.

The script-based-pre regression suite was also run successfully during development.

Motivation

The Autoharness analyzer reports functions being skipped when argument types do not implement Arbitrary. Adding support for EscapeDefault removes that limitation for this type and increases the set of functions eligible for automatic verification.

[acearyanarun]

@Tianshu-Huang @CYJ904 @wodex1nhaoIeng @srivatsansamraj

Opened the Kani PR for the std::ascii::EscapeDefault Arbitrary implementation. Feel free to take a look when you get a chance.

[Copilot]

🟡 Changes recommended

The proof must cover observable front- and back-consumed states to protect the core two-ended generation logic.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Adds Arbitrary support for std::ascii::EscapeDefault, enabling Autoharness verification for functions using this iterator.

Changes:

• Generates fresh, partially consumed, and exhausted iterator states.
• Adds Kani proof and Autoharness regression coverage.
• Requires direction-specific coverage for front and back consumption.

File summaries

File	Description
tests/script-based-pre/autoharness_ascii_escape_default/src/lib.rs	Adds the Autoharness target function.
tests/script-based-pre/autoharness_ascii_escape_default/escape_default.sh	Runs and filters Autoharness output.
tests/script-based-pre/autoharness_ascii_escape_default/escape_default.expected	Defines expected successful output.
tests/script-based-pre/autoharness_ascii_escape_default/config.yml	Configures the regression test.
tests/script-based-pre/autoharness_ascii_escape_default/Cargo.toml	Defines the test crate.
tests/kani/ascii_escape_default.rs	Tests remaining lengths, but lacks direction-specific state coverage.
library/kani/src/arbitrary.rs	Implements Arbitrary for EscapeDefault.

Review details

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

---

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

[CYJ904]

Verified locally on CBMC 6.11.0 — matches the PR description (VERIFICATION:- SUCCESSFUL, 5/5 cover properties, ~0.78s).

Two suggestions, building on Copilot's comment:

1. Direction-specific coverage: current covers only check total remaining count (0–4), so front=2,back=0 and front=1,back=1 are indistinguishable. Worth adding covers for mixed front+back states specifically, since that's the logic actually being tested.

2. Content correctness: the proof checks a count invariant but not that remaining elements match expected values after consumption — a next()/next_back() bookkeeping bug could still pass if the count happens to stay in bounds.