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

[github-actions]

Summary

Extracts a detailed informal specification for CommandLineParser.TryUnescape — the pure function that strips surrounding quotes and applies backslash-escape rules to command-line argument tokens.

This is Task 2 (Informal Spec Extraction) in the Lean Squad formal-verification pipeline.

What's included

• formal-verification/specs/commandlineparser_tryunescape_informal.md — full informal spec with:

  • Precise description of three parsing modes (unquoted pass-through, single-quoted literal, double-quoted with backslash escapes)
  • 24 properties across 5 property groups
  • 6 documented edge cases, including two confirmed bugs
  • Concrete examples table
  • Open questions for maintainer input

• formal-verification/TARGETS.md — target Porting latest changes. #2 (TryUnescape) advanced from phase 1 → 2

Confirmed bugs identified during spec extraction

Bug 1 — Length-1 single-quote ' throws ArgumentOutOfRangeException

input.IndexOf('\'', 1, input.Length - 2)

When input = "'" (length 1), input.Length - 2 = -1. Passing count = -1 to IndexOf(char, int, int) throws ArgumentOutOfRangeException. No existing test covers this case.

Bug 2 — Length-1 double-quote " throws on slice

When input = "\"" (length 1), evaluating input[1..^1] = input[1..0] (start=1, end=0) produces an invalid range and throws. No existing test covers this case.

Suggested fix for both: add a length guard before branching into quoted modes:

if (input.Length < 2) return true; // treat as unquoted pass-through

Next step

Task 3: Write the Lean 4 formal spec (formal-verification/lean/FVSquad/CommandLineParserTryUnescape.lean) once the Lean toolchain becomes available in the CI environment. The Lean toolchain is currently blocked by the network firewall in the runner.

---

🔬 Lean Squad — this PR was created by the automated Lean Squad formal-verification agent.

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-2026-04-25-19d4666508cf1804.

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 (240 of 240 lines)

From bee65c5e433cff85f5c0b5132e0a981e75b71af7 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sat, 25 Apr 2026 16:26:07 +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 informal specification for TryUnescape from Parser.cs covering:
- Three parsing modes: unquoted (pass-through), single-quoted (literal), double-quoted (backslash escapes)
- 24 properties across 5 property groups
- 6 edge cases including two confirmed bugs (length-1 quote inputs throw exceptions)
- Clarifying examples and open questions

🔬 Lean Squad — automated FV informal spec.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/TARGETS.md                |   2 +-
 .../commandlineparser_tryunescape_informal.md | 193 ++++++++++++++++++
 2 files changed, 194 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.ParseOptionAndSeparators` | `src/Platform/Microsoft.Testing.Platform/Command
... (truncated)

[Evangelink]

Closing — the Lean formal verification workflow is being removed in #8121.