[Lean Squad] feat(fv): Task 1 — add 3 new FV targets (PasteArguments, TimeSpanParser, TokenizeFilter)

[Evangelink]

🔬 Lean Squad — Task 1: Research & Target Identification

This PR adds three new formally-verified targets to the FV pipeline, bringing the total identified target count from 7 to 10.

New Targets

Target 8 — PasteArguments.AppendArgument ★★★★☆

File: src/Platform/Microsoft.Testing.Platform/Helpers/PasteArguments.cs

Mirrors System.Private.CoreLib/PasteArguments.cs from dotnet/runtime. Implements the Win32 command-line argument quoting algorithm with inline documentation of the backslash/quote rules.

Key properties to verify:

• ContainsNoWhitespaceOrQuotes(s) is true iff s has no whitespace or " characters
• Simple args pass through verbatim (no quoting added)
• Empty string produces "" (two quotes)
• Backslash doubling rule: trailing N backslashes → 2N backslashes before closing "
• 2N+1 backslashes before " → N literal backslashes + literal "
• Concrete test-vector equivalence for all 6 cases in PasteArgumentsTests

Target 9 — TimeSpanParser.TryParse ★★★☆☆

File: src/Platform/Microsoft.Testing.Platform/Helpers/TimeSpanParser.cs

Regex-fronted suffix-dispatch parser for human-readable time strings ("5400s", "90m", "500ms").

Key properties to verify:

• TryParse(null) / TryParse("") → (false, TimeSpan.Zero)
• Parse / TryParse consistency theorem
• Per-suffix dispatch: "s" → seconds, "m" → minutes (not milliseconds — "ms"/"mil" checked first), "h" → hours, "d" → days
• No-suffix input treated as milliseconds

Target 10 — TreeNodeFilter.TokenizeFilter ★★★☆☆

File: src/Platform/Microsoft.Testing.Platform/Requests/TreeNodeFilter/TreeNodeFilter.cs

Tokenizer/lexer for the tree-node filter language. Natural companion to the already-identified MatchFilterPattern target (Target 7).

Key properties to verify:

• Every yielded token is non-empty
• "/" is only emitted as a separator when openedSquareBrackets == 0
• Escape sequences \c → Regex.Escape(c.ToString()) in the current token (not a standalone token)
• Trailing backslash → InvalidOperationException
• * → ".*" in the output token
• "!=" is yielded as a two-character atomic token

Files changed

• formal-verification/TARGETS.md — expanded target table (7 → 10), updated Priority Order and Notes
• formal-verification/RESEARCH.md — added three new research sections (one per target) with properties, approximations, and FV rationale

---

🔬 This PR was created automatically by the Lean Squad FV agent.
Run: https://github.com/microsoft/testfx/actions/runs/25410825850

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 25410825850 -n agent -D /tmp/agent-25410825850

# Create a new branch
git checkout -b lean-squad/task1-new-targets-2026-05-06-4b79fc8141effe2f

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

# Push the branch to origin
git push origin lean-squad/task1-new-targets-2026-05-06-4b79fc8141effe2f

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — add 3 new FV targets (PasteArguments, TimeSpanParser, TokenizeFilter)' --base main --head lean-squad/task1-new-targets-2026-05-06-4b79fc8141effe2f --repo microsoft/testfx

Show patch preview (162 of 162 lines)

From 0611e6741ae9db116ae6bbbde3ca7dba95961e4a Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Wed, 6 May 2026 01:07:07 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=201=20=E2=80=94=20add=203=20ne?=
 =?UTF-8?q?w=20FV=20targets=20(PasteArguments,=20TimeSpanParser,=20Tokeniz?=
 =?UTF-8?q?eFilter)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add three new formally-verified targets to TARGETS.md and RESEARCH.md:

- Target 8: PasteArguments.AppendArgument — Win32 argv escaping with
  well-documented backslash/quote rules; round-trip and structural
  output properties provable by omega and decide.
- Target 9: TimeSpanParser.TryParse — suffix-dispatch time parser;
  Parse/TryParse consistency and per-suffix dispatch theorems.
- Target 10: TreeNodeFilter.TokenizeFilter — filter lexer with
  non-empty-token guarantee, separator-suppression-inside-brackets
  invariant, and escape-sequence correctness.

Also updates Priority Order and Notes sections in TARGETS.md to reflect
the broader target landscape (now 10 targets).

🔬 Lean Squad — automated FV agent

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

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..97d51fdcb 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -208,3 +208,88 @@ A pure recursive function that evaluates whether a test-node path and property b
 - Is the lack of a `Min ≤ Max` invariant in `ArgumentArity` a real bug or an accepted API choice? Worth filing an issue if a "bad" arity causes unexpected validator behaviour.
 - For `SplitCommandLine`, is the two-adjacent-quoted-strings case (`"a""b"`) intended to produce one token `ab` or two 
... (truncated)

[Evangelink]

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