[Lean Squad] feat(fv): Task 1 — expand FV targets from 7 to 14 with detailed research

[Evangelink]

Summary

🔬 Lean Squad — Task 1: Research & Target Identification (run 25605962330)

Expands the formal-verification documentation to cover all 14 identified FV targets (previously only 7 were documented in TARGETS.md).

Changes

formal-verification/TARGETS.md

• Expands target list from 7 → 14 targets
• Fixes phase assignments: CommandLineParseResult.Equals was listed as Phase 1 but its informal spec was merged; corrected to Phase 2
• Adds Targets 7–14:
  • EnvironmentVariableParser.ParseBool (Phase 1 — informal spec drafted but unmerged)
  • CommandLineOptionsValidator.ValidateOptionsArgumentArity (Phase 1)
  • PasteArguments.AppendArgument (Phase 1 — Windows CL quoting rules)
  • ValidationResult (Phase 1 — discriminated union invariant)
  • TreeNodeFilter.TokenizeFilter (Phase 1)
  • TimeSpanParser.TryParse (Phase 1)
  • CommandLineOption name validation (Phase 1)
  • PasteArguments.ContainsNoWhitespaceOrQuotes (Phase 1 — pure predicate)
• Reorganises priority order into two tiers: "Phase 2 → 3" and "Phase 1 → 2"
• Notes the Lean toolchain blocker

formal-verification/RESEARCH.md

• Adds research sections for six new targets (Targets 8–13) with: file path, FV rationale (★ rating), properties to verify, and approximation notes
• Adds two new open questions about round-trip proofs and empty option name semantics

Targets at Phase 2 (informal specs merged, awaiting Lean toolchain)

1. ArgumentArity — decidable by decide
2. CommandLineParser.TryUnescape — security-relevant; BUG-1/BUG-2 found
3. CommandLineParser.ParseOptionAndSeparators — BUG-5 found
4. CommandLineParseResult.Equals — equivalence-relation laws
5. ResponseFileHelper.SplitCommandLine — BUG-3/BUG-4 found
6. TreeNodeFilter.MatchFilterPattern — Boolean algebra laws

🔬 This PR was created by the Lean Squad automated formal verification agent. It contains no executable code changes — only documentation updates.

Generated by 📐 Lean Squad, see workflow run.

---

Note

This was originally intended as a pull request, but the git push operation failed.

Workflow Run: View run details and download patch artifact

The patch file is available in the agent artifact in the workflow run linked above.

To create a pull request with the changes:

# Download the artifact from the workflow run
gh run download 25605962330 -n agent -D /tmp/agent-25605962330

# Create a new branch
git checkout -b lean-squad/task1-expand-targets-2026-05-09-c46cc8273c792a1f

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25605962330/aw-lean-squad-task1-expand-targets-2026-05-09.patch

# Push the branch to origin
git push origin lean-squad/task1-expand-targets-2026-05-09-c46cc8273c792a1f

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — expand FV targets from 7 to 14 with detailed research' --base main --head lean-squad/task1-expand-targets-2026-05-09-c46cc8273c792a1f --repo microsoft/testfx

Show patch preview (269 of 269 lines)

From 53287f3e82d3fda5c55edc050b4ff6b05a32ec9c Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sat, 9 May 2026 16:32:38 +0000
Subject: [PATCH] fv: expand FV targets from 7 to 14 with detailed research
 notes
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Task 1: Research & Target Identification

- TARGETS.md: expand from 7 to 14 targets; fix phase assignments
  (CommandLineParseResult.Equals is phase 2 with merged spec);
  add Targets 7-14 covering ParseBool, ValidateOptionsArgumentArity,
  PasteArguments.AppendArgument, ValidationResult,
  TreeNodeFilter.TokenizeFilter, TimeSpanParser.TryParse,
  CommandLineOption name validation, and
  PasteArguments.ContainsNoWhitespaceOrQuotes
- RESEARCH.md: add six new target research sections (Targets 8-13)
  each with file path, FV rationale, properties to verify, and
  approximation notes; add two new open questions

🔬 Lean Squad — automated FV agent | run 25605962330

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/RESEARCH.md | 152 ++++++++++++++++++++++++++++++++
 formal-verification/TARGETS.md  |  53 +++++++----
 2 files changed, 190 insertions(+), 15 deletions(-)

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..d8860d5ff 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -193,6 +193,156 @@ A pure recursive function that evaluates whether a test-node path and property b
 
 ---
 
+### Target 8 — `EnvironmentVariableParser.ParseBool` ★★★★★
+
+**File**: `src/Platform/Microsoft.Testing.Platform/Helpers/EnvironmentVariableParser.cs` (approx.)
+**Type**: `string? → bool`
+
+A pure function that maps an environment-variable string value to a Boolean: returns `true` for `"1"`, `"yes"`, `"true"`, `"on"` (case-insensitive); `false` for `"0"`, `"no"`, `"false"`, `"off"` (case-insensitive); and `false` for
... (truncated)

[Evangelink]

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