[Lean Squad] feat(fv): Task 1 — expand FV targets to 10 (TokenizeFilter, OptionName, GetElementCounts)

[Evangelink]

🔬 Lean Squad — automated formal verification agent run #25248106771.

---

Changes

Task 1 — Research & Target Identification

This run surveyed the codebase and identified three new FV-amenable targets, expanding the total from 7 to 10.

New Target 8: TreeNodeFilter.TokenizeFilter ★★★★★

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

A pure lexer function that converts a raw filter string into a token stream. Interesting properties:

• Backslash escape: \x → Regex.Escape(x) appended to current fragment
• Wildcard * → ".*" expansion
• Two-character != merges into a single token
• ! after ( → unary-not token; ! elsewhere → treated as literal character
• Trailing backslash → InvalidOperationException
• Natural companion to MatchFilterPattern (Target 7): together they form a verified lexer+evaluator pipeline

New Target 9: CommandLineOption name validation ★★★★☆

File: src/Platform/Microsoft.Testing.Platform/CommandLine/CommandLineOption.cs

The name validation predicate extracted from the constructor: each character must satisfy IsLetterOrDigit || c == '-' || c == '?'. Properties:

• Compositional: valid iff every character is valid
• Decidable for concrete names → decide proofs work
• Connects to ArgumentArity (both validated in same constructor)

New Target 10: CollectionAssert.GetElementCounts ★★★☆☆

File: src/TestFramework/TestFramework/Assertions/CollectionAssert.Helpers.cs

First MSTest-framework target (beyond MTP). A pure frequency-map builder used by IsSubsetOfHelper and FindMismatchedElement. Key invariant: sum(map.values) + nullCount = input.length. Modelled as a fold over a list.

Updated TARGETS.md

• Fixed phase for Targets 4 and 5 (both at phase 2 — informal specs extracted in prior runs)
• Updated priority order to include all 10 targets
• Updated Notes section

Note: Task 3 (Formal Spec Writing in Lean 4) remains blocked — the network firewall in the sandbox prevents elan/curl from downloading the Lean toolchain. CI (lean-proofs.yml) remains the path to verified proofs.

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

# Create a new branch
git checkout -b lean-squad/task1-expand-fv-targets-2026-05-02-17b8d460a7988a79

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

# Push the branch to origin
git push origin lean-squad/task1-expand-fv-targets-2026-05-02-17b8d460a7988a79

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — expand FV targets to 10 (TokenizeFilter, OptionName, GetElementCounts)' --base main --head lean-squad/task1-expand-fv-targets-2026-05-02-17b8d460a7988a79 --repo microsoft/testfx

Show patch preview (174 of 174 lines)

From 5cf26831e25332898d0395dd9a6505b57e6815a3 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sat, 2 May 2026 08:48:31 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=201=20=E2=80=94=20expand=20FV?=
 =?UTF-8?q?=20targets=20to=2010,=20add=20TokenizeFilter,=20OptionName,=20G?=
 =?UTF-8?q?etElementCounts?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add three new FV targets to RESEARCH.md and TARGETS.md:
- Target 8: TreeNodeFilter.TokenizeFilter (pure lexer, escape/wildcard properties)
- Target 9: CommandLineOption name validation (character predicate, decidable)
- Target 10: CollectionAssert.GetElementCounts (multiset histogram, completeness invariant)

Also update TARGETS.md priority order to reflect all 7 existing targets at phase 2,
and note that Targets 8, 9, 10 are at phase 1 (identified, awaiting informal spec).

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

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..8adbd4166 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -193,6 +193,94 @@ A pure recursive function that evaluates whether a test-node path and property b
 
 ---
 
+### Target 8 — `TreeNodeFilter.TokenizeFilter` — Filter Lexer ★★★★★
+
+**File**: `src/Platform/Microsoft.Testing.Platform/Requests/TreeNodeFilter/TreeNodeFilter.cs`
+**Type**: `string → IEnumerable<string>` (private static, called by `ParseFilter`)
+
+A pure lexer that converts a raw filter string (e.g., `"Namespace/Class&Method[Prop=Val]"`) into a sequence of tokens. Tokens are either single-character operator strings (`(`, `)`, `[`, `]`, `&`, `|`, `=`, `/`), the two-character not-equals string `"!="`, the una
... (truncated)

[Evangelink]

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