[Lean Squad] feat(fv): Task 2 — informal spec for CommandLineParser.TryUnescape

[github-actions]

🔬 Lean Squad — automated formal verification agent

Summary

This PR adds the informal specification for CommandLineParser.TryUnescape, advancing it from phase 1 (identified) to phase 2 (informal spec extracted).

Target

• Function: static bool TryUnescape(string, string?, IEnvironment, out string?, out string?)
• File: src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs
• Task: Task 2 — Informal Spec Extraction

Changes

• formal-verification/specs/commandlineparser_tryunescape_informal.md — full informal specification
• formal-verification/TARGETS.md — advances TryUnescape to phase 2

Specification Highlights

The spec documents:

1. Three unescaping modes matching POSIX shell quoting rules:

   • Unquoted: identity passthrough
   • Single-quoted: strips outer ' quotes, no escape sequences, rejects interior '
   • Double-quoted: strips outer " quotes, applies backslash escapes: \\, \", \$, \`, \<newline>

2. 15 verifiable properties across 4 groups (passthrough, single-quote, double-quote, edge cases)

3. Potential bug identified (Open Question Initial commit! 🎉 #1):

   • Input "'" (a single ' character, length 1) matches both StartsWith("'") and EndsWith("'"), then calls input.IndexOf('\'', 1, input.Length - 2) = IndexOf('\'', 1, -1) — which throws ArgumentOutOfRangeException in .NET. No test covers this case.

4. Lean model approximation — three-case conditional with abstract newline parameter, global String.Replace modelling.

Verification Status

LEAN_AVAILABLE = false
Reason: elan download blocked by network firewall in runner environment.
Task 3 (Lean formal spec) deferred until Lean toolchain is accessible.

Next Steps

• Task 3: Write formal-verification/lean/FVSquad/TryUnescape.lean with type definitions and theorem stubs.
• Investigate potential bug with single-char ' input.

Generated by 📐 Lean Squad, see workflow run.

---

Note

This was originally intended as a pull request, but GitHub Actions is not permitted to create or approve pull requests in this repository.
The changes have been pushed to branch lean-squad/task2-tryunescape-informal-2026-04-25-d2f24c7c8ada3080.

Click here to create the pull request

To fix the permissions issue, go to Settings → Actions → General and enable Allow GitHub Actions to create and approve pull requests. See also: gh-aw FAQ

Show patch preview (249 of 249 lines)

From e178f18343f43063073790e0119d7431fdaabb16 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sat, 25 Apr 2026 08:33:42 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=202=20=E2=80=94=20informal=20s?=
 =?UTF-8?q?pec=20for=20CommandLineParser.TryUnescape?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Extract precise informal specification for TryUnescape:
- Documents three unescaping modes (unquoted passthrough, single-quoted, double-quoted)
- 15 properties across 4 groups for Lean formalisation
- Identifies potential bug: single-char '\'' input triggers ArgumentOutOfRangeException
- Documents POSIX compliance intent and approximations for Lean model
- Advances TryUnescape to phase 2 in TARGETS.md

🔬 Lean Squad AI-generated formal verification artifact.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/TARGETS.md                |   2 +-
 .../commandlineparser_tryunescape_informal.md | 201 ++++++++++++++++++
 2 files changed, 202 insertions(+), 1 deletion(-)
 create mode 100644 formal-verification/specs/commandlineparser_tryunescape_informal.md

diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
index 2e0fee3a8..488ff4a7b 100644
--- a/formal-verification/TARGETS.md
+++ b/formal-verification/TARGETS.md
@@ -17,7 +17,7 @@
 | # | Name | File | Phase | Status | PR/Issue |
 |---|------|------|-------|--------|----------|
 | 1 | `ArgumentArity` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ArgumentArity.cs` | 2 | Informal spec extracted | [PR #7799](https://github.com/microsoft/testfx/pull/7799) |
-| 2 | `CommandLineParser.TryUnescape` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` | 1 | Identified | — |
+| 2 | `CommandLineParser.TryUnescape` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` | 2 | Informal spec extracted | — |
 | 3 | `CommandLineParser.Pars
... (truncated)