[Lean Squad] feat(fv): Task 2 — informal spec for TreeNodeFilter.MatchFilterPattern

[github-actions]

Summary

Extracts a precise informal specification for TreeNodeFilter.MatchFilterPattern, the core Boolean evaluator of the tree-node filter subsystem in Microsoft.Testing.Platform.

This advances Target 7 (TreeNodeFilter.MatchFilterPattern) from phase 1 (identified) to phase 2 (informal spec extracted).

---

What's in this PR

formal-verification/specs/treenodefilter_matchfilterpattern_informal.md

A comprehensive informal spec covering:

• FilterExpression taxonomy: Maps the C# hierarchy (ValueExpression, NopExpression, OperatorExpression, ValueAndPropertyExpression, PropertyExpression) to an ADT with clear semantics.
• Recursive evaluation semantics: Precise denotational definition of evalFilter and evalProps.
• Boolean algebra invariants (12 properties):
  • Nop is always-true identity (B1)
  • Double negation: ¬¬e ≡ e (B2)
  • De Morgan for Or and And (B3, B4)
  • Commutativity of And/Or (B5, B6)
  • Singleton And/Or reduction (B7, B8)
  • Nop is And-identity and Or-absorber (B9, B10)
  • Vacuous And = true, Or = false (B11, B12)
• Regex semantics: How *, **, \c, and literal chars map to regex patterns; anchored + case-insensitive matching.
• MatchesFilter public entry point postcondition.
• Edge cases: empty PropertyBag, URL-encoded slashes, case sensitivity, vacuous And/Or lists.
• 6 open questions for maintainer review, including NopExpression reachability and empty list semantics.

formal-verification/TARGETS.md

Updates Target 7 phase from 1 → 2.

---

Context

This is part of the ongoing Lean Squad formal verification effort. The next step for this target (Task 3) is writing a Lean 4 formal spec, which is blocked pending Lean toolchain availability in the CI runner.

The Boolean algebra properties (De Morgan, double negation, commutativity) are well-suited to Lean 4 proofs using simp, omega, and structural induction — they should be provable once the toolchain is available.

---

🔬 Lean Squad — this PR was created by an automated FV agent (run #25007678153). All .lean files are subject to review for mathematical correctness. Informal specs are intended as input to human and automated review.

Generated by 📐 Lean Squad, see workflow run.

---

Note

This was originally intended as a pull request, but GitHub Actions is not permitted to create or approve pull requests in this repository.
The changes have been pushed to branch lean-squad/task2-treenodefilter-2026-04-27-937a4dc0191e83e2.

Click here to create the pull request

To fix the permissions issue, go to Settings → Actions → General and enable Allow GitHub Actions to create and approve pull requests. See also: gh-aw FAQ

Show patch preview (253 of 253 lines)

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

Extract precise informal specification for MatchFilterPattern, the core
Boolean evaluator of the TreeNodeFilter subsystem.

The spec covers:
- FilterExpression taxonomy (leaf/nop/and/or/not/withProps)
- Boolean algebra invariants (12 properties: double negation, De Morgan,
  commutativity, vacuous cases, Nop identity/absorption)
- Regex semantics for value tokens (* → .*, ** sentinel, escaping)
- MatchesFilter public entry point postcondition
- Edge cases (empty bag, URL-encoded slashes, case-insensitive matching)
- 6 open questions for maintainer review

Advances Target 7 from phase 1 to phase 2.

🔬 Lean Squad — automated FV agent

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/TARGETS.md                |   2 +-
 ...enodefilter_matchfilterpattern_informal.md | 198 ++++++++++++++++++
 2 files changed, 199 insertions(+), 1 deletion(-)
 create mode 100644 formal-verification/specs/treenodefilter_matchfilterpattern_informal.md

diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
index 12b9d0277..75a21555c 100644
--- a/formal-verification/TARGETS.md
+++ b/formal-verification/TARGETS.md
@@ -22,7 +22,7 @@
 | 4 | `CommandLineOptionsValidator` arity validation | `src/Platform/Microsoft.Testing.Platform/CommandLine/CommandLineOptionsValidator.cs` | 1 | Identified | — |
 | 5 | `CommandLineParseResult.Equals` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ParseResult.cs` | 1 | Identified | — |
 | 6 | `ResponseFileHelper.SplitCommandLine` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Re
... (truncated)