[Lean Squad] feat(fv): Task 2 — informal spec for ValidateOptionsArgumentArity

[Evangelink]

🔬 Lean Squad — automated formal verification agent run 25389586397

Summary

Extracts an informal specification for CommandLineOptionsValidator.ValidateOptionsArgumentArity — the pure validation function that checks each parsed option's argument count against its declared ArgumentArity bounds (Phase 2 for Target 4).

Also syncs TARGETS.md to reflect phases from previously merged PRs (#7918, #7919, #7934).

Changes

• formal-verification/specs/validateoptionsargumentarity_informal.md — new informal spec
• formal-verification/TARGETS.md — sync phases for targets 3, 5, 7 to phase 2; advance target 4 to phase 2

Spec Highlights

ValidateOptionsArgumentArity aggregates argument counts across all occurrences of the same option name, then classifies violations into three branches:

Condition	Error message
Max == 0 && arity > 0	"expects no arguments"
arity < Min	"expects at least {Min} arguments"
arity > Max	"expects at most {Max} arguments"

All violations are collected before returning (no short-circuit).

Findings

ID	Type	Description
OQ-1	Design gap	Absent required options (Min > 0, option not in parseResult) are not caught here; delegated to ValidateConfigurationAsync (extension-defined, no guarantee).
OQ-2	Pre-condition violation risk	providerAndOptionByOptionName[optionName] throws KeyNotFoundException if called before ValidateNoUnknownOptions; safe only due to call order in ValidateAsync.
OQ-3	Message asymmetry	Max == 0 case emits "expects no arguments" instead of "expects at most 0 arguments" — diverges from the general branch.
OQ-4	Grammar defect	"expects at least 1 arguments" uses incorrect plural.

Task 3 Status

Lean toolchain installation is blocked by network firewall in the CI sandbox. Task 3 (Formal Spec Writing) cannot proceed until elan is reachable from the runner. The CI workflow (lean-proofs.yml) is in place for when Lean becomes available.

Approximations for Lean Model

• Model int as Lean Int; Int32.MaxValue as 2147483647
• Abstract ICommandLineOptionsProvider to (String × String) (DisplayName, Uid)
• Model parseResult.Options as List (String × List String)
• Focus on the Boolean structure of validity, not error string formatting

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

# Create a new branch
git checkout -b lean-squad/task2-validateoptionsargumentarity-2026-05-05-2b0ed393bfdc3a78

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25389586397/aw-lean-squad-task2-validateoptionsargumentarity-2026-05-05.patch

# Push the branch to origin
git push origin lean-squad/task2-validateoptionsargumentarity-2026-05-05-2b0ed393bfdc3a78

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

Show patch preview (289 of 289 lines)

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

Extract informal specification for
CommandLineOptionsValidator.ValidateOptionsArgumentArity, the pure
validation function that checks each parsed option's argument count
against its declared ArgumentArity bounds.

Key findings documented:
- OQ-1: Absent required options (Min>0, option missing from parse
  result) are not caught; delegated to ValidateConfigurationAsync.
- OQ-2: KeyNotFoundException if called out-of-order before
  ValidateNoUnknownOptions filters unknown option names.
- OQ-3: Asymmetric error message for Max==0 case vs general >Max.
- OQ-4: Grammar defect — 'expects at least 1 arguments'.

Also syncs TARGETS.md phases: targets 3, 5, 7 advanced to phase 2
reflecting previously merged informal spec PRs (#7919, #7918, #7934).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/TARGETS.md                |  18 +-
 .../validateoptionsargumentarity_informal.md  | 212 ++++++++++++++++++
 2 files changed, 221 insertions(+), 9 deletions(-)
 create mode 100644 formal-verification/specs/validateoptionsargumentarity_informal.md

diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
index d3b921907..6b2ace058 100644
--- a/formal-verification/TARGETS.md
+++ b/formal-verification/TARGETS.md
@@ -18,21 +18,21 @@
 |---|------|------|-------|--------|----------|
 | 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/Microsof
... (truncated)

[Evangelink]

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