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

[Evangelink]

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

Fixes #7875

[Evangelink]

@copilot resolve the merge conflicts in this pull request

[Copilot]

@copilot resolve the merge conflicts in this pull request

Resolved in 558f754. The only conflict was in formal-verification/TARGETS.md for target 6 (ResponseFileHelper.SplitCommandLine), where main had advanced it to phase 2 with a PR link — accepted that version.

[Copilot]

Pull request overview

Adds a formal-verification (FV) Phase 2 informal specification for TreeNodeFilter.MatchFilterPattern, and updates the FV target tracker to reflect the new phase for Target 7.

Changes:

• Added an informal spec document describing MatchFilterPattern / MatchesFilter semantics, boolean-algebra invariants, and token/regex behavior.
• Updated formal-verification/TARGETS.md to advance Target 7 from phase 1 → phase 2.

Show a summary per file

File	Description
formal-verification/specs/treenodefilter_matchfilterpattern_informal.md	New Phase 2 informal specification for the TreeNodeFilter evaluator and related semantics.
formal-verification/TARGETS.md	Updates Target 7 status to “Informal spec extracted” (phase 2).

Copilot's findings

Comments suppressed due to low confidence (1)

formal-verification/specs/treenodefilter_matchfilterpattern_informal.md:168

• This claims NopExpression is "used internally" as a match-anything sentinel, but there are currently no call sites constructing NopExpression in the TreeNodeFilter parser (and a repo-wide search doesn't find new NopExpression(...)). Consider rephrasing this as an observed evaluator case / legacy hook, or explicitly noting that it is currently not constructed by ParseFilter.

3. **NopExpression as always-true sentinel**: Used internally to represent a "match anything" node in the filter tree. Its `evalFilter(nop, ·) = true` property makes it the identity element for `And` and the absorbing element for `Or`.

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

[Evangelink]

@copilot address review comments

[Copilot]

@copilot address review comments

Addressed in cd3b027:

1. Section 4 taxonomy (lines 41-53): Replaced "five concrete variants" with a clear distinction — 5 concrete C# subclasses (ValueExpression, NopExpression, OperatorExpression, ValueAndPropertyExpression, PropertyExpression) producing 6 semantic evaluation forms (since OperatorExpression covers And/Or/Not). Added an explicit note that PropertyExpression is only valid inside ValueAndPropertyExpression's property sub-tree and is dispatched by MatchProperties, not by the top-level MatchFilterPattern switch.

2. Section 10 postcondition (lines 150-157): Corrected the postcondition from |segments(path)| ≥ |_filters| to prefix-match semantics — the path may have fewer segments than filters (remaining filters are simply not consulted). The new postcondition uses let n = min(|segments(path)|, |_filters|) and the extra-segments guard is |segments(path)| ≤ |_filters| ∨ last filter is ".*.*". Updated the behavior steps accordingly.

[Copilot]

Copilot's findings

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