feat: total fnmatch with proven glob semantics

[tskovlund]

Summary

Qed/Ignore.lean decides which specs get verified at all, so a wrong answer silently drops verification coverage rather than failing loudly. Until now its matcher was partial: star backtracking reset the pattern pointer while advancing the string pointer, so it was not structurally decreasing, and a partial def is opaque to the kernel with no equational lemmas. Nothing about glob matching could be stated, let alone proven — the precedence proofs on main only work because they treat fnmatch as an abstract predicate.

This replaces the matcher with a structurally terminating one and proves the semantics.

Based on feat/lockfile-roundtrip-proof (#40), not main. Review #40 first; this PR's diff against it is the three files below plus docs.

The matcher

matchGlob recurses on pattern.length + name.length, which strictly decreases in every branch. The bracket case is the only one that needs an argument: scanBracket_shrinks proves a bracket expression always consumes at least its closing ], so the pattern remaining after it is strictly shorter.

To state that lemma, matchBracket is restructured from a let rec closure capturing negate and character into a top-level scanBracket that takes its state explicitly. The lemma then falls out by functional induction.

Qed/Ignore.lean now contains no partial, and specs/ignore.spec.toml has a structural criterion that fails the build if one reappears.

Behaviour is unchanged, and that was checked before the swap

The eight new cases in Tests/Ignore.lean were written and committed against the old implementation (1ae6ead), where they pass — they characterize today's behaviour, not the new code's. They cover repeated-star backtracking, trailing wildcards after a star, separator handling, unterminated brackets, the [] and [!] edge classes, and empty pattern/name.

On top of that, old and new were compared exhaustively during development:

Alphabet	Pairs	Differences
patterns ≤ 4 over a b * ? / [ ] ! -, names ≤ 4 over a b /	893,101	0
patterns ≤ 5 over a * ? / [ ], names ≤ 5 over a /	587,853	0
patterns ≤ 7 over a b *, names ≤ 7 over a b	836,400	0

The old implementation is deleted outright — no compatibility shim, no equivalence theorem against dead code.

What is now proven

• matchGlob_star_iff_suffix — * semantics: a leading * matches exactly when some suffix of the name matches the rest of the pattern
• star_matches_everything — a bare * matches every name, path separators included, so * in a .qedignore ignores the whole tree rather than just its top level
• question_matches_one — ? semantics: exactly one character, and never /
• literal_matches_iff — a pattern with no wildcards is an exact-match test: it matches its own text and nothing else, so archive cannot accidentally ignore archived-specs
• literal_star_matches_prefix — a literal prefix followed by * matches every name carrying that prefix

One thing worth flagging for review, because it is now pinned by proof: * crosses / but ? does not. That asymmetry is pre-existing behaviour, not something this PR introduces — I verified it against the old matcher before writing the theorems. If it is wrong, it is a deliberate separate decision to make, and the proofs will now force the conversation instead of leaving it implicit.

Dogfooding

New specs/ignore.spec.toml owns the subsystem: seven proof criteria, the no-partial structural assertion, and an agent review covering pattern-form coverage and the honesty of the termination measure. It brings qed's self-verification to 10 specs.

Test plan

• lake build — clean, no warnings
• lake test — all 165 tests passed (157 + the 8 new characterization cases)
• devbox run check — build, tests, and both docgen freshness diffs clean
• qed verify --auto — all 10 specs passed
• npx prettier@3 --check . — clean
• qed lock regenerated for the new spec
• Pre-push hook (lake build + qed verify --auto --pin) passed; --pin changed no hashes

No partial and no sorry in Qed/Ignore.lean; no native_decide anywhere in the repo.

GitHub Actions reports no checks on this PR — .github/workflows/ci.yml triggers only on pull requests targeting main, and this one targets feat/lockfile-roundtrip-proof. CI will run once #40 merges and this retargets. The local run above is the same gate CI executes.

🤖 Generated with Claude Code