[Lean Squad] feat: [Lean Squad] informal spec for EnvironmentVariableParser.ParseBool

[Evangelink]

Extracts a precise informal specification for the pure boolean environment-
variable parser nested in LLMEnvironmentDetector. Documents:

• Input partition into Truthy (T), Falsy (F), and Default (D) sets
• Postconditions, invariants, and edge cases
• Eight theorems of interest all provable by decide
• Open questions OQ-1..OQ-4 (idempotency, locale-independence, token coverage)
• Approximation notes for the future Lean 4 model

Updates TARGETS.md to add target #8 at phase 2.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

Fixes #8081

[Copilot]

Pull request overview

Adds Lean Squad formal-verification documentation for the environment-variable boolean parser used by LLMEnvironmentDetector, and registers it as a new FV target.

Changes:

• Added a new informal specification document for EnvironmentVariableParser.ParseBool (token sets, invariants, edge cases, candidate theorems, open questions).
• Updated formal-verification/TARGETS.md to include Target #8 and added it to the priority list.

Show a summary per file

File	Description
formal-verification/TARGETS.md	Registers EnvironmentVariableParser.ParseBool as Target #8 and adds it to the priority list.
formal-verification/specs/environmentvariableparser_parsebool_informal.md	New informal spec describing the parser’s behavior, partitions, and proposed theorems.

Copilot's findings

Comments suppressed due to low confidence (2)

formal-verification/specs/environmentvariableparser_parsebool_informal.md:159

• Theorem #6 states the round-trip/idempotency property “does not hold in general”, but the Open Questions section (OQ-1) correctly argues it does hold because bool.ToString() returns "True"/"False" and the parser matches those via OrdinalIgnoreCase. This is internally inconsistent and (given the current implementation) incorrect—please align Theorem #6 with the actual behavior (and consider removing OQ-1 as an open question if it’s settled).

5. **Empty → default**: `ParseBool "" def = def`
6. **Idempotency**: `ParseBool (toString (ParseBool str def)) def' = ParseBool str def` — *does not hold in general*; noted as an open question below.
7. **Default independence**: `∀ s ∈ T, ∀ def₁ def₂, ParseBool s def₁ = ParseBool s def₂`
8. **Default independence** (falsy): `∀ s ∈ F, ∀ def₁ def₂, ParseBool s def₁ = ParseBool s def₂`

formal-verification/TARGETS.md:41

• The “Notes” section below still says “Six of the seven targets…” and refers to all targets being in command-line/tree-node subsystems. With Target #8 added under Helpers/LLMEnvironmentDetector.cs, those counts/classification are now out of date—please update the notes to reflect the current target list.

8. **`EnvironmentVariableParser.ParseBool`** — eighth priority. Pure total function; all 8 theorems of interest provable by `decide`. Informal spec extracted this run. **Next: Task 3 (blocked by Lean toolchain).**

## Notes

- Six of the seven targets are in the command-line infrastructure of Microsoft.Testing.Platform; one target is in the tree-node filter subsystem.

• Files reviewed: 2/2 changed files
• Comments generated: 1

[Evangelink]

Summary

Workflow: PR Nitpick Reviewer 🔍
Date: 2026-05-11
Repository: microsoft/testfx

Key Findings

1. Important — Self-contradiction in Theorem 6 vs. OQ-1 (environmentvariableparser_parsebool_informal.md, line 157): Theorem 6 is labelled "does not hold in general", but OQ-1 immediately proves the idempotency round-trip does hold for all C# inputs. This needs to be reconciled to avoid confusing readers and future Lean proof authors.

2. Minor — Missing PR link in TARGETS.md (TARGETS.md, line 26): Target #8 has — in the PR/Issue column even though this PR (#8098) is the originating spec PR. Other targets (#1, #6) consistently include their PR links.

Positive Highlights

• The spec is thorough and well-structured: clear input partitioning into T / F / D, a full invariant list, explicit edge-case table, and approximation notes for the Lean model — exactly the kind of precision useful for formal verification.
• Using StringComparison.OrdinalIgnoreCase and calling out the exact-match exception for "1"/"0" is a subtle but important implementation detail that the spec correctly captures.
• The Notes section in TARGETS.md should be updated separately (it still says "Six of the seven targets" and refers to "command-line infrastructure", but Target #8 is in Helpers).

---

Generated by PR Nitpick Reviewer

🔍 Meticulously inspected by PR Nitpick Reviewer 🔍

[Evangelink]

Nitpick (Important): Theorem 6 states the idempotency property "does not hold in general", but OQ-1 (line 165) concludes it does hold for all inputs, since "True" and "False" (C#'s bool.ToString() output) are both in their respective sets.

These two statements directly contradict each other. For a formal verification spec, this inconsistency is especially important to resolve. Consider either:

• Removing the "does not hold in general" qualifier from Theorem 6 and marking it as provable, or
• Clarifying the general/specific distinction (e.g., noting why it could fail in theory vs. actually holding for C#'s ToString output).

Why it matters: Readers of this spec may be confused about whether Theorem 6 is true, which undermines trust in the formal model.

[Evangelink]

Nitpick (Minor): The PR/Issue column for Target #8 shows —, but this PR (#8098) is the one that introduced the informal spec. Targets #1 and #6 both have their originating PR linked in this column. Consider updating to [PR #8098](https://github.com/microsoft/testfx/pull/8098) for consistency.

Why it matters: Traceability — when looking at the target list, other contributors can follow the link to understand the context behind each spec.