[Lean Squad] feat(fv): Task 2 — informal spec for CommandLineOptionsValidator arity validation

[Evangelink]

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

Summary

This PR completes Task 2 (Informal Spec Extraction) for Target 4: CommandLineOptionsValidator.ValidateOptionsArgumentArity.

Changes

• New: formal-verification/specs/commandlineoptionsvalidator_arity_informal.md
• Updated: formal-verification/TARGETS.md — Target 4 → phase 2; fix Target 5 to show phase 2 (spec was merged in PR [Lean Squad] feat(fv): Task 2 — informal spec for CommandLineParseResult.Equals #7918)

Spec Highlights

ValidateOptionsArgumentArity groups all parsed options by name, accumulates their total argument count across all occurrences, then enforces the registered ArgumentArity(Min, Max) constraint with three mutually-exclusive error cases:

Case	Condition	Error type
Expects no arguments	Max == 0 AND arity > 0	Specific "no arguments" message
Too few arguments	arity < Min	"expects at least Min"
Too many arguments	arity > Max AND Max > 0	"expects at most Max"

Open Questions Documented

• OQ-1: Absent required options (Min > 0 but option not in parse result) are not caught here — delegated to ValidateConfigurationAsync. Coverage gap.
• OQ-2: providerAndOptionByOptionName[optionName] will throw KeyNotFoundException if pipeline order changes and ValidateNoUnknownOptions is skipped.
• OQ-3: Arity is aggregated cumulatively across all occurrences — --opt a --opt b yields arity 2, not 1.

Theorems Ready for Lean (Task 3)

7 theorem stubs identified, all provable with omega or decide:

• T2: "no arguments" branch iff Max == 0 AND arity > 0
• T4: three error branches are mutually exclusive given 0 ≤ Min ≤ Max
• T3: exact-arity check correctness
• T5: soundness (if Valid, then Min ≤ arity ≤ Max for every option)

Lean Toolchain Note

Lean is not available in this sandbox (network firewall blocks elan/curl). Task 3 (formal Lean spec) is blocked until the CI toolchain is available.

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

# Create a new branch
git checkout -b lean-squad/task2-informal-spec-arity-validation-2026-05-03-16f4e68783c14e26

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25274572198/aw-lean-squad-task2-informal-spec-arity-validation-2026-05-03.patch

# Push the branch to origin
git push origin lean-squad/task2-informal-spec-arity-validation-2026-05-03-16f4e68783c14e26

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 2 — informal spec for CommandLineOptionsValidator arity validation' --base main --head lean-squad/task2-informal-spec-arity-validation-2026-05-03-16f4e68783c14e26 --repo microsoft/testfx

Show patch preview (210 of 210 lines)

From 835beeb9ca46f3bb129040fe70b6e4af74cbf564 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sun, 3 May 2026 08:48:20 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=202=20=E2=80=94=20informal=20s?=
 =?UTF-8?q?pec=20for=20CommandLineOptionsValidator=20arity=20validation?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Add formal-verification/specs/commandlineoptionsvalidator_arity_informal.md
  with purpose, algorithm, preconditions, postconditions, invariants,
  edge cases, 7 Lean-ready theorem stubs, open questions, and
  approximation notes
- Update TARGETS.md: Target 4 → phase 2, fix Target 5 status (already phase 2 via PR #7918)

🔬 Lean Squad FV agent — run https://github.com/microsoft/testfx/actions/runs/25274572198

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/TARGETS.md                |   8 +-
 ...mandlineoptionsvalidator_arity_informal.md | 150 ++++++++++++++++++
 2 files changed, 154 insertions(+), 4 deletions(-)
 create mode 100644 formal-verification/specs/commandlineoptionsvalidator_arity_informal.md

diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
index d3b921907..704a81095 100644
--- a/formal-verification/TARGETS.md
+++ b/formal-verification/TARGETS.md
@@ -19,8 +19,8 @@
 | 1 | `ArgumentArity` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ArgumentArity.cs` | 2 | Informal spec extracted | [PR #7799](https://github.com/microsoft/testfx/pull/7799) |
 | 2 | `CommandLineParser.TryUnescape` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` | 2 | Informal spec extracted | — |
 | 3 | `CommandLineParser.ParseOptionAndSeparators` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` | 2 | Informal spec extracted | — |
-| 4 | `CommandLineOptionsValidator` arity validation | `src/Platform/Microsoft.Testing.Platform/CommandLine/CommandLineOptions
... (truncated)