[Lean Squad] feat(fv): Task 6 — expand Lean–C# correspondence review to all 7 targets

[Evangelink]

Summary

🔬 Lean Squad — automated formal-verification agent | Run: https://github.com/microsoft/testfx/actions/runs/25222665032

This PR completes Task 6 (Correspondence Review) by expanding formal-verification/CORRESPONDENCE.md to cover all seven FV targets.

Changes

Target 3 — TreeNodeFilter.MatchFilterPattern

• Updated phase from 1 → 2 (informal spec was extracted in PR [Lean Squad] feat(fv): Task 2 — informal spec for TreeNodeFilter.MatchFilterPattern #7934)
• Added reference to the informal spec file
• Added 3 open questions about PropertyBag abstraction, withProps scope, and PropertyExpression guard

Target 4 — ResponseFileHelper.SplitCommandLine (was stub)

• Full type mapping: IEnumerable<string> → List String, state machine → pattern match, StringBuilder → index range
• Deliberate approximations: lazy sequence → strict list, state machine inlined, double-quote stripping as character filter
• 6 key theorems including design-issue theorem (adjacent quoted strings → two tokens)

Target 5 — CommandLineParser.ParseOptionAndSeparators (was stub)

• Full type mapping: out parameters → product type, IndexOfAny → findIdx, TrimStart('-') → dropWhile
• 8 key theorems including concrete decide-provable examples and the empty-option-name design issue

Target 6 — CommandLineParseResult.Equals (was stub)

• Full type mapping: sealed class → structure, IReadOnlyList<T> → List T, string[] → List String
• 4 deliberate approximations including ReferenceEquals short-circuit removal
• 8 key theorems for reflexivity, symmetry, transitivity, and differential equality

Target 7 — CommandLineOptionsValidator arity validation (was stub)

• Planned type mapping reusing Target 1 ArgumentArity structure
• 6 planned theorems covering all arity ranges (ZeroOrMore, ExactlyOne, in-range, below-min, above-max)

Lean Toolchain Status

⚠️ Lean toolchain not available in this sandbox (network firewall blocks elan download). Task 3 (Formal Spec Writing) deferred to next run.

Next Steps

• Task 3: Write Lean 4 spec for CommandLineParser.TryUnescape (highest-priority phase-2 target) when toolchain is available
• Optionally advance CommandLineParseResult.Equals to Task 3 (simpler structural equality; all decide-provable)

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

# Create a new branch
git checkout -b lean-squad/task6-correspondence-review-2026-05-01-4ffed3ef95e8ed84

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25222665032/aw-lean-squad-task6-correspondence-review-2026-05-01.patch

# Push the branch to origin
git push origin lean-squad/task6-correspondence-review-2026-05-01-4ffed3ef95e8ed84

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 6 — expand Lean–C# correspondence review to all 7 targets' --base main --head lean-squad/task6-correspondence-review-2026-05-01-4ffed3ef95e8ed84 --repo microsoft/testfx

Show patch preview (260 of 260 lines)

From 72812f8bee3aee17d1b6d68719276307cf2ba5e9 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Fri, 1 May 2026 16:35:18 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=206=20=E2=80=94=20expand=20cor?=
 =?UTF-8?q?respondence=20review=20to=20all=207=20targets?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Update Target 3 (TreeNodeFilter.MatchFilterPattern) from Phase 1 to
  Phase 2, adding informal spec reference and open questions
- Expand 'Remaining Targets' stub into full correspondence sections for:
  - Target 4 (ResponseFileHelper.SplitCommandLine): type mapping,
    approximations, 6 key theorems, 2 open questions
  - Target 5 (CommandLineParser.ParseOptionAndSeparators): type mapping,
    approximations, 8 key theorems including design-issue theorem
  - Target 6 (CommandLineParseResult.Equals): type mapping, approximations,
    8 key theorems for equivalence-relation laws
  - Target 7 (CommandLineOptionsValidator arity validation): planned mapping
    and 6 key theorems; informal spec still pending (phase 1)

🔬 Lean Squad — automated formal-verification agent

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/CORRESPONDENCE.md | 205 +++++++++++++++++++++++++-
 1 file changed, 197 insertions(+), 8 deletions(-)

diff --git a/formal-verification/CORRESPONDENCE.md b/formal-verification/CORRESPONDENCE.md
index 9a23368b4..645420e81 100644
--- a/formal-verification/CORRESPONDENCE.md
+++ b/formal-verification/CORRESPONDENCE.md
@@ -139,7 +139,8 @@ Each section follows a common structure:
 
 **C# file**: `src/Platform/Microsoft.Testing.Platform/Requests/TreeNodeFilter/TreeNodeFilter.cs`
 **Lean file** (planned): `formal-verification/lean/FVSquad/TreeNodeFilter.lean`
-**Phase**: 1 (identified; informal spec not yet written)
+**Informal spec**: `formal-verification/specs/treenodefilter_matchfilterpattern_informal.md`
+**Pha
... (truncated)

[Evangelink]

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