[Lean Squad] feat(fv): Task 1 — add 3 new FV targets and sync TARGETS.md phases

[Evangelink]

Summary

🔬 Lean Squad — automated formal verification agent. Run #25331082787.

This PR executes Task 1 (Research & Target Identification) for this run. Task 3 (Lean spec writing) was the primary selected task but remains blocked — the Lean toolchain requires network access to install (elan/curl are firewalled in the sandbox). CI-based verification via leanprover/lean4-action is used instead.

Changes

formal-verification/TARGETS.md

• Phase corrections based on merged PRs:
  • Target 3 (ParseOptionAndSeparators): updated PR reference to #7919
  • Target 5 (CommandLineParseResult.Equals): promoted from phase 1 → phase 2 (spec merged in #7918)
• New targets from merged PR #7849 added to table:
  • Target 8: PasteArguments.AppendArgument — Windows argv escaping, round-trip correctness
  • Target 9: TimeSpanParser.TryParse — suffix-dispatch pure parser
  • Target 10: TreeNodeFilter.TokenizeFilter — tokenizer with trailing-backslash exception
  • Target 11: Sha256Hasher.ToCharsBuffer — branchless hex encoding, all 256 inputs decidable
  • Target 12: ExtensionValidationHelper.ValidateUniqueExtension — duplicate-UID detection
• 3 new targets identified this run:
  • Target 13: ValidationResult algebraic properties — tiny discriminated-union struct; Valid().IsValid = true, Invalid(msg).ErrorMessage = some msg; all properties decide-provable. The [MemberNotNullWhen] invariant is machine-checkable.
  • Target 14: CommandLineOptionsValidator.ValidateNoUnknownOptions — pure function; set-membership property: returns Invalid iff any parsed option name is not in the union of registered names.
  • Target 15: CommandLineOptionsValidator.ValidateOptionsAreNotDuplicated — pure function; uniqueness property: returns Invalid iff any option name is registered by more than one provider.

formal-verification/RESEARCH.md

Added detailed target profiles for Targets 13, 14, and 15:

• Purpose, why FV-amenable, properties to verify, approximations, open questions.

New Targets Detail

Target 13 — ValidationResult

File: src/Platform/Microsoft.Testing.Platform/Extensions/ValidationResult.cs

public readonly struct ValidationResult {
    public bool IsValid { get; }
    [MemberNotNullWhen(false, nameof(ErrorMessage))]
    public string? ErrorMessage { get; }
    public static ValidationResult Valid() => new(true, null);
    public static ValidationResult Invalid(string errorMessage) => new(false, errorMessage);
}

Key theorems: Valid().IsValid = true, ∀ msg, Invalid(msg).IsValid = false, invariant IsValid = false ↔ ErrorMessage.isSome.

Target 14 — ValidateNoUnknownOptions

Pure membership check: parseResult.Options.Names ⊆ validNames → Valid. Monotone in validNames.

Target 15 — ValidateOptionsAreNotDuplicated

Pure uniqueness check: ∀ name, |registerers(name)| ≤ 1 → Valid. Symmetric: provider ordering does not affect outcome.

Why These Targets?

All three are:

• Pure functions / value-type invariants with no side effects or I/O
• Decidable — concrete instances provable by decide in Lean 4
• Complementary — together with existing targets they cover the full command-line validation pipeline
• Self-contained — require minimal abstraction of external types

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

# Create a new branch
git checkout -b lean-squad/task1-new-targets-2026-05-04-run3-fef6317d0138f71d

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25331082787/aw-lean-squad-task1-new-targets-2026-05-04-run3.patch

# Push the branch to origin
git push origin lean-squad/task1-new-targets-2026-05-04-run3-fef6317d0138f71d

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — add 3 new FV targets and sync TARGETS.md phases' --base main --head lean-squad/task1-new-targets-2026-05-04-run3-fef6317d0138f71d --repo microsoft/testfx

Show patch preview (177 of 177 lines)

From 1a5bc0128f41036b03e360804c5a42181f90a473 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 4 May 2026 16:52:18 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=201=20=E2=80=94=20add=203=20ne?=
 =?UTF-8?q?w=20FV=20targets=20and=20update=20TARGETS.md=20phases?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add three new formal verification targets:
- Target 13: ValidationResult algebraic properties (tiny discriminated union, all decide-provable)
- Target 14: CommandLineOptionsValidator.ValidateNoUnknownOptions (set-membership property)
- Target 15: CommandLineOptionsValidator.ValidateOptionsAreNotDuplicated (uniqueness over multi-map)

Also synchronize TARGETS.md with merged PRs:
- Fix Target 5 (CommandLineParseResult.Equals) to phase 2 with PR #7918 reference
- Fix Target 3 (ParseOptionAndSeparators) with PR #7919 reference
- Add Targets 8-12 from merged PR #7849 (PasteArguments, TimeSpanParser, etc.)
- Update notes and priority order

🔬 Lean Squad — automated FV agent.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/RESEARCH.md | 78 +++++++++++++++++++++++++++++++++
 formal-verification/TARGETS.md  | 30 +++++++++----
 2 files changed, 99 insertions(+), 9 deletions(-)

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..63591fa7d 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -201,6 +201,82 @@ A pure recursive function that evaluates whether a test-node path and property b
 - For simple finite types (like `ArgumentArity` constants), we rely on `decide` for closed proofs.
 - We track which theorems are `sorry`-guarded vs. fully proved in `TARGETS.md`.
 
+---
+
+## Target 13: `ValidationResult` algebraic properties
+
+**File**: `src/Platform/Microsoft.Testing.Platform/Extensions/ValidationResult.cs`
+**Type**: `readonly struct Val
... (truncated)

[Evangelink]

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