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

[Evangelink]

Summary

🔬 Lean Squad — automated FV agent (run #25266333058)

This PR adds three new formal-verification targets to formal-verification/RESEARCH.md and formal-verification/TARGETS.md, expanding the FV portfolio beyond the existing command-line parsing cluster.

New Targets

Target 8 — PasteArguments.AppendArgument ★★★★★

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

Implements the Windows CreateProcess argument-escaping rules. The backslash-doubling invariants are explicitly documented in the source and a matching test suite already exists (PasteArgumentsTests.cs). Key properties reduce to natural-number arithmetic (2N / 2N+1 backslash rules) — ideal for omega. This is the most immediately FV-amenable new target.

Target 9 — TimeSpanParser.TryParse ★★★☆☆

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

Pure suffix-dispatch parser for human-readable timeout strings ("5400s", "90m", "1.5h", etc.). Suffix-to-unit mapping is exhaustive and mutually exclusive; unit-conversion properties are decidable. Good omega target once the regex match is abstracted as a precondition.

Target 10 — TreeNodeFilter.TokenizeFilter ★★★★☆

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

Deterministic character-level tokenizer that feeds ParseFilter. Complements the already-spec'd MatchFilterPattern (Target 7), together covering the full filter evaluation pipeline. The bracket-depth counter is a Nat; one specified exception case (trailing \) gives a concrete bug-finding opportunity.

Fixes

• Target 5 (CommandLineParseResult.Equals): corrects phase from 1 → 2 (informal spec was merged in PR [Lean Squad] feat(fv): Task 2 — informal spec for CommandLineParseResult.Equals #7918).
• Target 7 (TreeNodeFilter.MatchFilterPattern): adds PR link for [Lean Squad] feat(fv): Task 2 — informal spec for TreeNodeFilter.MatchFilterPattern #7934.
• Priority Order and Notes sections in TARGETS.md updated to reflect 10 total targets.
• Open Questions in RESEARCH.md extended with a note on PasteArguments trailing-backslash behaviour.

Lean Status

Task 3 (Formal Spec Writing) was also selected for this run but could not proceed — curl is blocked by the sandbox network firewall, preventing elan (Lean toolchain) installation. No .lean files have been written or modified. Lean Squad will retry Task 3 in a future run.

Checklist

• RESEARCH.md — three new target entries with benefit, spec size, proof tractability, approximations
• TARGETS.md — three new rows + updated Priority Order + Notes
• Phase fix for Target 5 (1 → 2)
• No .lean files modified (Lean toolchain not available this run)
• 🔬 Lean Squad disclosure included

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

# Create a new branch
git checkout -b lean-squad/task1-research-new-targets-2026-05-03-563a6655e9bbaf75

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

# Push the branch to origin
git push origin lean-squad/task1-research-new-targets-2026-05-03-563a6655e9bbaf75

# 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-research-new-targets-2026-05-03-563a6655e9bbaf75 --repo microsoft/testfx

Show patch preview (186 of 186 lines)

From 930659095aebd3322cd8b04f33d937a988265fad Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sun, 3 May 2026 01:15:11 +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 formal verification targets to RESEARCH.md and TARGETS.md:

- Target 8: PasteArguments.AppendArgument — Windows CreateProcess escaping rules;
  backslash-doubling invariants are explicitly documented; existing test suite;
  properties reduce to natural-number arithmetic (ideal for omega).
- Target 9: TimeSpanParser.TryParse — pure suffix-dispatch parser; unit-conversion
  properties are decidable; good omega target.
- Target 10: TreeNodeFilter.TokenizeFilter — character-level tokenizer complementing
  the already-spec'd MatchFilterPattern; bracket-depth tracked as Nat; one
  specified exception case (trailing backslash).

Also fix Target 5 (CommandLineParseResult.Equals) phase in TARGETS.md from 1→2
(informal spec was merged in PR #7918) and update the PR reference for Target 7.

🔬 Lean Squad — automated FV agent (run https://github.com/microsoft/testfx/actions/runs/25266333058)

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

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..58e8c7630 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -201,6 +201,95 @@ A pure recursive function that evaluates whether a test-node path and property b
 - For simple finite types (like `ArgumentArity` constants), we rely on `decide` for closed proofs.
 - We
... (truncated)

[Evangelink]

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