[Lean Squad] feat(fv): Task 1 — expand FV targets to include SplitCommandLine and TreeNodeFilter#7849
Merged
Evangelink merged 3 commits intomainfrom Apr 27, 2026
Conversation
…TreeNodeFilter Add two new FV targets identified through codebase survey: 1. ResponseFileHelper.SplitCommandLine — pure tokeniser with state machine structure. Properties: empty input → empty output; whitespace splits tokens; double-quotes group tokens and are stripped from output. 2. TreeNodeFilter.MatchFilterPattern — recursive Boolean filter evaluator. Ideal for structural induction proofs of Boolean-algebra laws: De Morgan, double negation, idempotence, and commutativity. Abstract match predicate keeps the Lean model clean. Also: - Correct TryUnescape phase in TARGETS.md table (phase 2, not 1) - Elevate TreeNodeFilter to priority 3 (above ParseOptionAndSeparators) due to its mathematical richness - Update REPORT.md run history and status 🔬 Lean Squad — automated FV research agent. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Updates the Lean Squad formal-verification planning docs to expand the set of FV targets to include ResponseFileHelper.SplitCommandLine and TreeNodeFilter.MatchFilterPattern, and to reflect updated status/prioritization.
Changes:
- Extend the FV target list from 5 to 7 targets, adding
SplitCommandLineandMatchFilterPattern, and adjust the priority ordering. - Add research notes/spec outlines for the two new targets, including candidate properties to verify and modeling approximations.
- Update the FV project report (status/summary/run history) to reflect the expanded research scope and current toolchain constraints.
Show a summary per file
| File | Description |
|---|---|
| formal-verification/TARGETS.md | Adds two new targets and revises priority order + notes. |
| formal-verification/RESEARCH.md | Adds new research sections for SplitCommandLine and MatchFilterPattern, plus related open questions. |
| formal-verification/REPORT.md | Updates project status, summary, targets list, and run history to include the new targets. |
Copilot's findings
- Files reviewed: 3/3 changed files
- Comments generated: 3
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
Member
Author
|
@copilot resolve the merge conflicts in this pull request |
…on/TARGETS.md Co-authored-by: Evangelink <11340282+Evangelink@users.noreply.github.com>
Contributor
Done. Merged |
YuliiaKovalova
approved these changes
Apr 27, 2026
Evangelink
deleted the
lean-squad/task1-new-targets-2026-04-26-af98d23215b156cc
branch
This was referenced Apr 27, 2026
Closed
This was referenced May 4, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add 13 unit tests covering RetryAttribute constructor validation, BackoffType property validation, and ExecuteAsync retry logic:
Fixes #7824