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

[github-actions]

🔬 Lean Squad — Task 2: Informal Spec Extraction.

Extracts a precise informal specification for ParseOptionAndSeparators, the local static function inside CommandLineParser.Parse that splits a combined --key=value / --key:value token into an option name and an optional inline value.

What this adds

formal-verification/specs/commandlineparser_parseoptionandseparators_informal.md

• Purpose: Documents the pure string-split semantics: find first : or =, split there, strip leading - from the option-name prefix.
• 16 named properties across 5 groups:
  • Group 1 — Delimiter-free case (3 props)
  • Group 2 — Delimiter present case (4 props)
  • Group 3 — Structural / Reconstructibility (3 props)
  • Group 4 — Determinism and independence (3 props)
  • Group 5 — Edge cases (3 props)
• Invariants: currentOption is never null, no leading -, no : or = in option name; currentArg is null iff no delimiter.
• Potential issue documented: Empty option name not rejected when delimiter immediately follows dashes (e.g. --:value → currentOption = "").
• Open questions: Interaction with TryUnescape quoting; delimiter-within-quoted-value semantics.
• Approximations for Lean 4: List.dropWhile, List.findIdx?, key lemmas identified.
• 5 concrete Lean #eval examples ready for Task 3.

formal-verification/TARGETS.md — updated phase status for all 7 targets.

Phase progression

CommandLineParser.ParseOptionAndSeparators: Phase 1 → Phase 2 (informal spec extracted)

Also updates TARGETS.md to reflect that targets 6 and 7 now have open spec PRs (#7899 and lean-squad/task2-treenodefilter-spec-2026-04-28).

Relationship to other targets

All three existing informal specs (ArgumentArity, TryUnescape, SplitCommandLine) are for functions in the same command-line infrastructure. ParseOptionAndSeparators is the gateway function — it runs before TryUnescape, and its output currentArg is what TryUnescape processes. Having all three specs enables a future composed proof of the full option-parsing pipeline.

---

🔬 Generated by Lean Squad FV agent. Workflow run.

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-parseoptionandseparators-spec-2026-04-28-0be69994ec126673.

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

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

Extracts a precise informal specification for the ParseOptionAndSeparators
local function in CommandLineParser. Documents:

- Pure string-split function: first-occurrence of ':' or '=' delimiter
- 16 named properties across 5 groups (no-delimiter, delimiter-present,
  reconstructibility, determinism, edge cases)
- TrimStart('-') normalization of option-name prefix
- Edge case: empty option name when delimiter immediately follows dashes
  (e.g. '--:value' produces currentOption = '')
- Interaction with TryUnescape (caller passes currentArg after Trim())
- Approximations for Lean 4 model (List.dropWhile, List.findIdx?)
- 5 concrete Lean examples for #eval tests

Advances CommandLineParser.ParseOptionAndSeparators from phase 1 to phase 2.
Updates TARGETS.md to reflect current phase state of all 7 targets.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/TARGETS.md                |  16 +-
 ...arser_parseoptionandseparators_informal.md | 218 ++++++++++++++++++
 2 files changed, 226 insertions(+), 8 deletions(-)
 create mode 100644 formal-verification/specs/commandlineparser_parseoptionandseparators_informal.md

diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
index 12b9d0277..d3b921907 100644
--- a/formal-verification/TARGETS.md
+++ b/formal-verification/TARGETS.md
@@ -18,19 +18,19 @@
 |---|------|------|-------|--------|----------|
 | 1 | `ArgumentArity` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ArgumentArity.cs` | 2 | Informal spec extracted | [PR #7799](https://github.co
... (truncated)

[Evangelink]

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