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.

[feliperodri]

Logic LGTM — correctly generates states from both ends since EscapeDefault is double-ended. One thing before merge: format-check is failing in CI, please run ./scripts/kani-fmt.sh and push the fix. Approving on the assumption that's just a formatting nit.

[feliperodri]

@acearyanarun could you tackle the merge conflicts and the CI failures so we get this ready to merge?

[feliperodri]

@acearyanarun @Tianshu-Huang what is the status of this PR?

[acearyanarun]

@acearyanarun @Tianshu-Huang what is the status of this PR?

Hello Felipe, currently looking at this - will let you know status soon

[acearyanarun]

Hello @feliperodri , I resolved the arbitrary.rs conflict against current main, fixed the EscapeDefault script formatting issue, ran ./scripts/kani-fmt.sh,and both targeted EscapeDefault tests pass locally. Please take a look when you get the chance.

[feliperodri]

Re-checked after the merge commit: the implementation is unchanged, and it still verifies.

One gap in the test. tests/kani mode doesn't fail on an unsatisfied kani::cover!, so the direction-specific covers can't catch the regression they were added for. With the whole next_back() block deleted from any(), 6 of 8 covers are satisfied, but the harness still reports SUCCESSFUL and the test passes. Moving the proof to tests/expected/arbitrary/escape_default.rs, with an .expected file that pins 8 of 8 cover properties satisfied (as duration.expected does), makes it fail on exactly that mutation. I checked both ways. tests/kani/char_escape_unicode.rs has the same gap, so no need to fix that here.

[acearyanarun]

@feliperodri Addressed. I moved the EscapeDefault test to the tests/expected suite and added an .expected file that requires all 8 cover properties to be satisfied hence removing the next_back() generation now causes the test to fail. I also added the comment regarding why the front/back steps are intentionally unrolled to avoid loop unwinding. Also, noted, didn't touch char_escape_unicode.rs