[Lean Squad] feat(fv): Task 2 + Task 9 — CommandLineOptionsValidator informal spec & CI simplification

[Evangelink]

Summary

🔬 Lean Squad — automated formal verification agent run on 2026-04-30.

This PR implements two selected tasks from the weighted task draw:

• Task 2 (Informal Spec Extraction): informal spec for CommandLineOptionsValidator.ValidateOptionsArgumentArity
• Task 9 (CI Automation): remove unused Mathlib dependency to simplify CI

---

Task 2 — Informal Spec: CommandLineOptionsValidator.ValidateOptionsArgumentArity

New file: formal-verification/specs/commandlineoptionsvalidator_arity_informal.md

The spec covers the private ValidateOptionsArgumentArity validation step inside the
CommandLineOptionsValidator.ValidateAsync pipeline. This function checks that the
total number of arguments supplied for each parsed option falls within its declared
ArgumentArity bounds [Min, Max].

Key findings in the spec

• OQ-1 (design issue): providerAndOptionByOptionName[optionName] throws
  KeyNotFoundException if an unknown option somehow reaches this step. The function
  relies on ValidateNoUnknownOptions running first — a convention, not a type-level
  guarantee. A safe TryGetValue would be more robust.
• OQ-3 (design issue): Options with Min > 0 that are entirely absent from the
  parse result are not detected here — GroupBy produces no group for them.
  Required-option enforcement must happen elsewhere (provider-level ValidateConfigurationAsync).
• The special-case check Max == 0 AND T > 0 selects a better user-facing error than
  the generic "expects at most N arguments" branch.

Proposed Lean theorems (7)

1. valid_iff_all_in_range
2. invalid_if_flag_has_args
3. invalid_if_below_min
4. invalid_if_above_max
5. errors_independent
6. empty_input_is_valid
7. zeroOrMore_always_valid

---

Task 9 — CI Simplification: Remove Mathlib

Changed files: formal-verification/lean/lakefile.toml, .github/workflows/lean-proofs.yml

The lakefile.toml previously declared a [[require]] dependency on
leanprover-community/mathlib4 v4.14.0. No .lean source files exist yet in
FVSquad/, so this dependency was never used — but it caused CI to attempt a heavy
network fetch of Mathlib during lake update.

Changes:

• Removed the [[require]] mathlib block from lakefile.toml
• Removed the lake update step from lean-proofs.yml (no external deps to resolve)
• Added a comment in lakefile.toml explaining when to re-add Mathlib

The lake update step will be re-introduced when the first .lean file imports
Mathlib, at which point the lock file (lake-manifest.json) should also be committed.

---

TARGETS.md update

Target #4 (CommandLineOptionsValidator arity validation) advanced from Phase 1 to Phase 2.
All 7 FV targets are now at Phase 2 (informal spec extracted).

---

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

---

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

# Create a new branch
git checkout -b lean-squad/task2-commandlineoptionsvalidator-task9-ci-2026-04-30-053b75db2d145ac5 main

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

# Push the branch and create the pull request
git push origin lean-squad/task2-commandlineoptionsvalidator-task9-ci-2026-04-30-053b75db2d145ac5
gh pr create --title '[Lean Squad] feat(fv): Task 2 + Task 9 — CommandLineOptionsValidator informal spec & CI simplification' --base main --head lean-squad/task2-commandlineoptionsvalidator-task9-ci-2026-04-30-053b75db2d145ac5 --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.