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

[Evangelink]

Summary

🔬 Lean Squad — this PR was created automatically by the Lean Squad formal verification agent (run 25624386123).

Task 2: Informal Spec Extraction for EnvironmentVariableParser.ParseBool.

---

What This PR Does

Adds formal-verification/specs/environmentvariableparser_parsebool_informal.md, a precise informal specification for the ParseBool static method nested inside LLMEnvironmentDetector (used by BooleanEnvironmentRule to detect whether an AI coding agent is present via environment variables).

Updates formal-verification/TARGETS.md to register this as Target #8 at Phase 2.

---

Target

private static bool ParseBool(string? str, bool defaultValue)

Located in src/Platform/Microsoft.Testing.Platform/Helpers/LLMEnvironmentDetector.cs.

---

Spec Highlights

• Input partition: Truthy set T = {1, true, yes, on} (case-insensitive), Falsy set F = {0, false, no, off} (case-insensitive), Default set D = everything else including null and "".
• Key invariants: totality (never throws), determinism, partition disjointness (T ∩ F = ∅), null-is-default, empty-is-default, default-independence for recognised tokens.
• Theorems of interest: 8 theorems, all provable by decide in Lean 4 after defining the finite token sets.
• Open questions: OQ-1 (idempotency/round-trip: ParseBool(bool.ToString(), def') = ParseBool(str, def) — analysed and likely holds), OQ-2 (default symmetry), OQ-3 (locale independence), OQ-4 (token coverage).
• No bugs found in this target; the function is straightforward and total.

---

Files Changed

File	Change
formal-verification/specs/environmentvariableparser_parsebool_informal.md	New — full informal specification
formal-verification/TARGETS.md	Updated — Target #8 added at Phase 2

---

Next Step

Task 3: Write Lean 4 formal spec for this target (blocked until Lean toolchain is installable in the CI environment).

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

# Create a new branch
git checkout -b lean-squad/task2-parsebool-informal-2026-05-10-222b284addd25f3e

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

# Push the branch to origin
git push origin lean-squad/task2-parsebool-informal-2026-05-10-222b284addd25f3e

# Create the pull request
gh pr create --title '[Lean Squad] feat: [Lean Squad] informal spec for EnvironmentVariableParser.ParseBool' --base main --head lean-squad/task2-parsebool-informal-2026-05-10-222b284addd25f3e --repo microsoft/testfx

Show patch preview (243 of 243 lines)

From f5cf1b8bbbe1ed150e517d8afc03584dfcdc2686 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Sun, 10 May 2026 08:50:18 +0000
Subject: [PATCH] feat: [Lean Squad] informal spec for
 EnvironmentVariableParser.ParseBool

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>
---
 formal-verification/TARGETS.md                |   2 +
 ...onmentvariableparser_parsebool_informal.md | 190 ++++++++++++++++++
 2 files changed, 192 insertions(+)
 create mode 100644 formal-verification/specs/environmentvariableparser_parsebool_informal.md

diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
index d3b921907..1fc32d4d0 100644
--- a/formal-verification/TARGETS.md
+++ b/formal-verification/TARGETS.md
@@ -23,6 +23,7 @@
 | 5 | `CommandLineParseResult.Equals` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ParseResult.cs` | 1 | Identified | — |
 | 6 | `ResponseFileHelper.SplitCommandLine` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ResponseFileHelper.cs` | 2 | Informal spec extracted | [PR #7899](https://github.com/microsoft/testfx/pull/7899) |
 | 7 | `TreeNodeFilter.MatchFilterPattern` | `src/Platform/Microsoft.Testing.Platform/Requests/TreeNodeFilter/TreeNodeFilter.cs` | 2 | Informal spec extracted | — |
+| 8 | `EnvironmentVariableParser.ParseBool` | `src/Platform/Microsoft.Testing.Platform/Helpers/LLMEnvironmentDetector.cs` | 2 | Informal spec extracted | — |
 
 ## Priority Order
 
@@ -33,6 +34,7 
... (truncated)