[Lean Squad] feat(fv): Task 1 — add 3 new FV targets (UnicodeCharacterUtilities, TestNodeUid, CommandLineOption)

[Evangelink]

🔬 Lean Squad — Task 1: Research & Target Identification

This PR is auto-generated by the Lean Squad formal verification agent.
Run: https://github.com/microsoft/testfx/actions/runs/25310316932

Summary

Adds three new FV-amenable targets to TARGETS.md and RESEARCH.md, bringing the total to 10 identified targets (in the main branch, excluding targets in open PRs).

New Targets

#	Target	File	Key Property
8	UnicodeCharacterUtilities.IsIdentifierStartCharacter / IsIdentifierPartCharacter	src/Analyzers/MSTest.SourceGeneration/Helpers/UnicodeCharacterUtilities.cs	Subsumption: every start char is a part char. ASCII range fully decidable.
9	TestNodeUid equality and implicit conversion	src/Platform/Microsoft.Testing.Platform/Messages/TestNodeUid.cs	Equivalence-relation axioms + operator consistency. Minimal warm-up target.
10	CommandLineOption name-character invariant	src/Platform/Microsoft.Testing.Platform/CommandLine/CommandLineOption.cs	Constructor-enforced predicate: no whitespace/injection chars in option names.

Why These Targets

Target 8 — UnicodeCharacterUtilities: Two pure character-classification functions grounded in the C# Language Specification. For ASCII (0–127), all 128 cases are enumerable. The key subsumption theorem IsIdentifierStartCharacter(c) → IsIdentifierPartCharacter(c) is a structural invariant with direct safety implications — a source generator that violates this would produce invalid C# identifiers. The inverse direction provides evidence-by-example that the predicate is not vacuously true. Decidable via native_decide.

Target 9 — TestNodeUid: The simplest structural-equality target in the codebase. Wraps a single string field; Equals is other?.Value == value. All three equivalence-relation axioms (reflexivity, symmetry, transitivity) are immediately provable by decide/simp, as are operator-consistency theorems (== ↔ Equals). Ideal first fully-proved Lean file once the toolchain is available.

Target 10 — CommandLineOption name validation: The constructor loop ∀i, char.IsLetterOrDigit(name[i]) ∨ name[i] = '-' ∨ name[i] = '?' is a constructor-time pre/post-condition invariant. Proving this demonstrates that once an option is constructed, its name cannot contain spaces, shell metacharacters, or injection sequences. Security-relevant property. Character predicate is decidable for all 128 ASCII codepoints via native_decide.

Files Changed

• formal-verification/TARGETS.md — added rows 8–10 and updated Priority Order and Notes sections
• formal-verification/RESEARCH.md — added research sections for Targets 8, 9, and 10 with rationale, properties to verify, and modelling approximations

Next Steps for These Targets

All three targets are at Phase 1 (identified). Next step is Task 2 (informal spec extraction) for each, followed by Task 3 (Lean 4 formal spec) once the Lean toolchain is available in the runner environment.

🔬 This PR was automatically created by the Lean Squad formal verification agent.

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

# Create a new branch
git checkout -b lean-squad/task1-new-targets-2026-05-04-run2-47fb2611cfdbf3d6

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

# Push the branch to origin
git push origin lean-squad/task1-new-targets-2026-05-04-run2-47fb2611cfdbf3d6

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — add 3 new FV targets (UnicodeCharacterUtilities, TestNodeUid, CommandLineOption)' --base main --head lean-squad/task1-new-targets-2026-05-04-run2-47fb2611cfdbf3d6 --repo microsoft/testfx

Show patch preview (159 of 159 lines)

From 2805ed696c4761cc91e242dd87ae6f1328c94d9f Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 4 May 2026 09:09:42 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=201=20=E2=80=94=20add=203=20ne?=
 =?UTF-8?q?w=20FV=20targets=20(UnicodeCharacterUtilities,=20TestNodeUid,?=
 =?UTF-8?q?=20CommandLineOption)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Identify and document three new FV-amenable targets in TARGETS.md and RESEARCH.md:

- Target 8: UnicodeCharacterUtilities.IsIdentifierStartCharacter / IsIdentifierPartCharacter
  Pure character-classification functions grounded in the C# Language Specification.
  Key theorem: subsumption (every start char is a part char). Fully decidable for ASCII
  (all 128 cases) using native_decide. Used in the MSTest source generator.

- Target 9: TestNodeUid equality and implicit conversion
  Minimal string-wrapper type. All equivalence-relation laws (reflexivity, symmetry,
  transitivity) and operator-consistency theorems are immediately decidable. Ideal
  warm-up target for the first fully-proved Lean file.

- Target 10: CommandLineOption name-character invariant
  Constructor-enforced predicate: every char of Name must satisfy IsLetterOrDigit(c) ||
  c == '-' || c == '?'. Provable as a post-construction invariant. Security-relevant:
  valid option names cannot contain whitespace or injection characters.

🔬 Lean Squad — automated formal verification agent.

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

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..dfef57632 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -193,6 +193,82 @@ A pure recursive funct
... (truncated)

[Evangelink]

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