[Lean Squad] feat(fv): Task 6 — correspondence review + Task 9 — CI improvements

[Evangelink]

Task 6 — Correspondence Review

Updates formal-verification/CORRESPONDENCE.md to add detailed correspondence sections for the four targets that now have merged informal specifications:

New sections added

Target	C# source	Lean type planned
ResponseFileHelper.SplitCommandLine	Two-state machine with Boundary enum	inductive SplitState + def splitCommandLine : String → List String
CommandLineParser.ParseOptionAndSeparators	IndexOfAny([':', '=']) + TrimStart('-')	def parseOptionAndSeparators : String → String × Option String
CommandLineParseResult.Equals	Index-based positional equality loop	instance : DecidableEq CommandLineParseResult
CommandLineOptionsValidator arity validation	Grouped arg count vs ArgumentArity.Min/.Max	def validateArity : ArgumentArity → Nat → Option String

Each section documents:

• Type / function mapping table
• Deliberate approximations (e.g., IEnumerable → List, char.IsWhiteSpace → ASCII subset)
• Excluded properties (error messages, GetHashCode, etc.)
• Key theorems with planned native_decide / decide / simp approach
• Open questions for design review

Phase corrections

• TreeNodeFilter.MatchFilterPattern (Target 3): Phase 1 → Phase 2 (informal spec in open PR [Lean Squad] feat(fv): Task 2 — informal spec for TreeNodeFilter.MatchFilterPattern #7934)
• CommandLineOptionsValidator, CommandLineParseResult.Equals: Phase 1 → Phase 2 (informal specs merged)
• Updated TARGETS.md table rows 4 and 5 accordingly

---

Task 9 — CI Automation

lean-proofs.yml improvements

1. elan version: v4.2.1 → v3.1.0 — the version verified to work on this codebase.
2. Cache key: Now includes lake-manifest.json in the hash key, ensuring the cached .lake/packages directory is invalidated when dependencies change.
3. Dependency resolution: Added hashFiles('lake-manifest.json') == '' guard — lake update is skipped when lake-manifest.json already exists (reproducible builds use the pinned manifest).

lakefile.toml — remove unused mathlib dependency

The mathlib dependency was included speculatively but no .lean files use it. Keeping it would require downloading ~700 MB of Mathlib during CI when the first .lean files are added. Removed now; will be re-added per-target when a .lean file actually imports Mathlib.

lake-manifest.json — add empty manifest

Adds formal-verification/lean/lake-manifest.json with an empty packages array. This:

• Lets lake build run without first running lake update (faster CI)
• Provides a concrete file to hash in the CI cache key
• Documents the zero-dependency baseline

FVSquad/README.md update

Updated planned targets table to reflect all 7 targets at Phase 2.

---

Other

• REPORT.md: Updated Status, Summary, Targets table (all 7 at Phase 2), and prepended this run's row to the Run History table.

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

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

---

Warning

Protected Files — Push Permission Denied

This was originally intended as a pull request, but the patch modifies protected files. A human must create the pull request manually.

Protected files

• .github/workflows/lean-proofs.yml

The push was rejected because GitHub Actions does not have workflows permission to push these changes, and is never allowed to make such changes, or other authorization being used does not have this permission.

Create the pull request manually

# Download the patch from the workflow run
gh run download 25156674261 -n agent -D /tmp/agent-25156674261

# Create a new branch
git checkout -b lean-squad/task6-correspondence-task9-ci-2026-04-30-0c0aff48b7b0bec3 main

# Apply the patch (--3way handles cross-repo patches)
git am --3way /tmp/agent-25156674261/aw-lean-squad-task6-correspondence-task9-ci-2026-04-30.patch

# Push the branch and create the pull request
git push origin lean-squad/task6-correspondence-task9-ci-2026-04-30-0c0aff48b7b0bec3
gh pr create --title '[Lean Squad] feat(fv): Task 6 — correspondence review + Task 9 — CI improvements' --base main --head lean-squad/task6-correspondence-task9-ci-2026-04-30-0c0aff48b7b0bec3 --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.