feat: total fnmatch with proven glob semantics

AGENTS.md

@@ -13,7 +13,7 @@ Qed/
   Shell.lean           Shell command execution and quoting utilities
   Agent.lean           Shared agent invocation (env var constants, default commands)
   Integrity.lean       Content-addressed spec integrity (SHA-256 hashing, git checks)
-  Ignore.lean          .qedignore parsing and fnmatch glob matching (*, ?, [abc], [!abc], ! negation)
+  Ignore.lean          .qedignore parsing and total glob matching (*, ?, [abc], [!abc], ! negation)
   ContractLock.lean    Verification contract locking (glob expansion, theorem extraction, lock file I/O)
   SpecLoader.lean      Load and pin spec files from disk (returns Spec.Pinned)
   Parser.lean          JSON spec parser (Lean.Json → Spec, parseFromJson for roundtrip proofs)
@@ -44,7 +44,7 @@ Qed/Proofs/
   LockRoundtrip.lean      Lock file writer↔reader roundtrip (parseLockFileFromJson ∘ lockFileToJson = ok)
   ShellProperties.lean    shellQuote produces exactly one shell word; command-last structure
   VerifierProperties.lean Proof-target resolution and sorry detection
-  IgnoreProperties.lean   .qedignore parse output contract and pattern precedence
+  IgnoreProperties.lean   Glob semantics, .qedignore parse contract, pattern precedence
   GlobProperties.lean     Valid glob patterns contain no shell metacharacters
   IntegrityEvents.lean    State machine response to the integrityViolation event
   WorkerLoopProperties.lean  step=transition, buildPrompt preserves the operator prompt
@@ -67,6 +67,7 @@ specs/                 qed's own specs (dogfooding)
   state-machine.spec.toml  State machine correctness — 13 proofs + agent
   parser.spec.toml         Parser correctness — 6 proofs + agent
   verify-mode.spec.toml    Verify mode correctness — 1 proof + commands + agent
+  ignore.spec.toml         .qedignore and glob correctness — 7 proofs + command + agent
   conventions.spec.toml    Convention adherence — naming, DRY, doc accuracy
   docs.spec.toml           Documentation accuracy — freshness + agent
 DocGen/
@@ -158,7 +159,7 @@ qed                   # run the binary (.lake/build/bin on PATH via .envrc)
 
 ## Proven properties
 
-The `Qed/Proofs/` directory contains 120+ theorems, every one checked by Lean 4's kernel — no `sorry`, no `native_decide`. See [docs/proven-properties.md](docs/proven-properties.md) for what they guarantee.
+The `Qed/Proofs/` directory contains 130 theorems, every one checked by Lean 4's kernel — no `sorry`, no `native_decide`. See [docs/proven-properties.md](docs/proven-properties.md) for what they guarantee.
 
 ## Repo-specific conventions
 

Qed/Ignore.lean

@@ -5,92 +5,77 @@ namespace Qed.Ignore
 /-- Path to the ignore file (relative to project root). -/
 def ignoreFileName : String := ".qedignore"
 
-/-- Match a single character against a bracket expression like `[abc]` or `[!abc]`.
-    Returns `(matched, remainingPattern)` where remainingPattern is after the `]`.
-    Returns `none` if the bracket expression is malformed (no closing `]`). -/
-private def matchBracket (patternChars : List Char) (character : Char)
-    : Option (Bool × List Char) :=
-  let (negate, rest) := match patternChars with
-    | '!' :: tail => (true, tail)
-    | chars => (false, chars)
-  let rec go (remaining : List Char) (matched : Bool) : Option (Bool × List Char) :=
-    match remaining with
-    | [] => none
-    | ']' :: tail =>
-      let result := if negate then !matched else matched
-      some (result, tail)
-    | low :: '-' :: high :: tail =>
-      if high == ']' then
-        let hit := character == low || character == '-'
-        let result := if negate then !(matched || hit) else (matched || hit)
-        some (result, tail)
-      else
-        go tail (matched || (low ≤ character && character ≤ high))
-    | c :: tail =>
-      go tail (matched || c == character)
-  go rest false
-
-/-- Inner loop for fnmatch. Backtracking on `*` means structural recursion
-    cannot be proved — each backtrack resets `pat` to a saved position while
-    advancing `str` by one, so termination is O(p×n) but not structurally
-    decreasing. Marked partial since this is runtime-only code. -/
-private partial def fnmatchGo (pat : List Char) (str : List Char)
-    (starPat : Option (List Char)) (starString : Option (List Char)) : Bool :=
-  match pat, str with
-  | [], [] => true
-  | [], _ =>
-    match starPat, starString with
-    | some sp, some ss =>
-      match ss with
-      | [] => false
-      | _ :: rest => fnmatchGo sp rest (some sp) (some rest)
-    | _, _ => false
-  | '*' :: patRest, _ =>
-    fnmatchGo patRest str (some patRest) (some str)
-  | '?' :: patRest, c :: strRest =>
-    if c == '/' then
-      match starPat, starString with
-      | some sp, some ss =>
-        match ss with
-        | [] => false
-        | _ :: rest => fnmatchGo sp rest (some sp) (some rest)
-      | _, _ => false
+/-- Scan the body of a bracket expression, after any leading `!`.
+    Returns whether `character` is in the set, and the pattern remaining after
+    the closing `]`. `none` when there is no closing `]`. -/
+def scanBracket (negate : Bool) (character : Char) :
+    List Char → Bool → Option (Bool × List Char)
+  | [], _ => none
+  | ']' :: tail, matched => some (if negate then !matched else matched, tail)
+  | low :: '-' :: high :: tail, matched =>
+    if high == ']' then
+      let hit := character == low || character == '-'
+      some (if negate then !(matched || hit) else matched || hit, tail)
     else
-      fnmatchGo patRest strRest starPat starString
+      scanBracket negate character tail
+        (matched || (low ≤ character && character ≤ high))
+  | c :: tail, matched => scanBracket negate character tail (matched || c == character)
+
+/-- Match a single character against a bracket expression like `[abc]`,
+    `[!abc]`, or `[a-z]`. -/
+def matchBracket (patternChars : List Char) (character : Char) :
+    Option (Bool × List Char) :=
+  match patternChars with
+  | '!' :: tail => scanBracket true character tail false
+  | chars => scanBracket false character chars false
+
+/-- A bracket expression consumes at least its closing `]`, so what remains is
+    strictly shorter. This is what makes `matchGlob` terminate. -/
+theorem scanBracket_shrinks {negate : Bool} {character : Char}
+    {chars : List Char} {matched result : Bool} {rest : List Char}
+    (h : scanBracket negate character chars matched = some (result, rest)) :
+    rest.length < chars.length := by
+  fun_induction scanBracket negate character chars matched <;> simp_all <;> omega
+
+theorem matchBracket_shrinks {chars : List Char} {character : Char}
+    {result : Bool} {rest : List Char}
+    (h : matchBracket chars character = some (result, rest)) :
+    rest.length < chars.length := by
+  unfold matchBracket at h
+  split at h
+  · exact Nat.lt_succ_of_lt (scanBracket_shrinks h)
+  · exact scanBracket_shrinks h
+
+-- The `h` binder below is used only by `decreasing_by`, which the
+-- unused-variable linter does not scan.
+set_option linter.unusedVariables false in
+/-- Match a pattern against a name, character by character.
+    `*` consumes any run of characters, including `/`; `?` consumes exactly one
+    character that is not `/`; `[…]` consumes one character from the class. -/
+def matchGlob : List Char → List Char → Bool
+  | [], str => str.isEmpty
+  | '*' :: patRest, [] => matchGlob patRest []
+  | '*' :: patRest, c :: strRest =>
+    matchGlob patRest (c :: strRest) || matchGlob ('*' :: patRest) strRest
+  | _ :: _, [] => false
+  | '?' :: patRest, c :: strRest => c != '/' && matchGlob patRest strRest
   | '[' :: patRest, c :: strRest =>
-    match matchBracket patRest c with
-    | some (true, remaining) => fnmatchGo remaining strRest starPat starString
-    | _ =>
-      match starPat, starString with
-      | some sp, some ss =>
-        match ss with
-        | [] => false
-        | _ :: rest => fnmatchGo sp rest (some sp) (some rest)
-      | _, _ => false
-  | p :: patRest, c :: strRest =>
-    if p == c then
-      fnmatchGo patRest strRest starPat starString
-    else
-      match starPat, starString with
-      | some sp, some ss =>
-        match ss with
-        | [] => false
-        | _ :: rest => fnmatchGo sp rest (some sp) (some rest)
-      | _, _ => false
-  | _ :: _, [] =>
-    match starPat, starString with
-    | some sp, some ss =>
-      match ss with
-      | [] => false
-      | _ :: rest => fnmatchGo sp rest (some sp) (some rest)
-    | _, _ => false
+    match h : matchBracket patRest c with
+    | some (true, remaining) => matchGlob remaining strRest
+    | _ => false
+  | p :: patRest, c :: strRest => p == c && matchGlob patRest strRest
+termination_by pat str => pat.length + str.length
+decreasing_by
+  all_goals simp_all
+  all_goals try omega
+  all_goals (have := matchBracket_shrinks h; omega)
 
 /-- Match a name against a glob pattern (fnmatch-style).
-    Supports: `*` (any sequence), `?` (any single char),
-    `[abc]` (character class), `[!abc]` (negated class), `[a-z]` (range).
-    Uses the two-pointer backtracking algorithm (iterative, O(p×n) worst case). -/
+    Supports: `*` (any sequence, separators included), `?` (any single
+    character except `/`), `[abc]` (character class), `[!abc]` (negated class),
+    `[a-z]` (range). -/
 def fnmatch (pattern : String) (name : String) : Bool :=
-  fnmatchGo pattern.toList name.toList none none
+  matchGlob pattern.toList name.toList
 
 /-- Parse a .qedignore file into a list of patterns.
     Format: one pattern per line, `#` for comments, blank lines skipped. -/

Qed/Proofs/IgnoreProperties.lean

@@ -6,10 +6,14 @@ namespace Qed.Proofs.IgnoreProperties
 
 open Qed Qed.Ignore
 
-/-! # .qedignore parsing and pattern precedence
+/-! # .qedignore parsing, glob semantics, and pattern precedence -/
 
-The precedence theorems treat `fnmatch` as an abstract predicate, so they hold
-however globbing itself behaves. -/
+/-- A pattern character with no special meaning to `matchGlob`. -/
+def isLiteralChar (c : Char) : Bool := c != '*' && c != '?' && c != '['
+
+-- ═══════════════════════════════════════════════════════════════════
+-- parseIgnoreFile output contract
+-- ═══════════════════════════════════════════════════════════════════
 
 /-- Blank lines are dropped, so no downstream match is ever attempted against
     the empty pattern. -/
@@ -32,6 +36,106 @@ theorem parseIgnoreFile_no_comments (contents : String) :
   simp only [Bool.and_eq_true, Bool.not_eq_true'] at hcond
   exact hcond.2
 
+-- ═══════════════════════════════════════════════════════════════════
+-- Glob semantics
+-- ═══════════════════════════════════════════════════════════════════
+
+/-- **`*` semantics:** a leading `*` matches exactly when some suffix of the
+    name matches the rest of the pattern. -/
+theorem matchGlob_star_iff_suffix (patRest str : List Char) :
+    matchGlob ('*' :: patRest) str = true ↔
+      ∃ suffix, suffix <:+ str ∧ matchGlob patRest suffix = true := by
+  induction str with
+  | nil =>
+    constructor
+    · intro h
+      exact ⟨[], List.nil_suffix, by simpa [matchGlob] using h⟩
+    · rintro ⟨suffix, hsuf, hm⟩
+      have hnil : suffix = [] := List.eq_nil_of_suffix_nil hsuf
+      subst hnil
+      simpa [matchGlob] using hm
+  | cons c s ih =>
+    rw [show matchGlob ('*' :: patRest) (c :: s)
+          = (matchGlob patRest (c :: s) || matchGlob ('*' :: patRest) s) from by
+            simp [matchGlob]]
+    simp only [Bool.or_eq_true]
+    constructor
+    · rintro (h | h)
+      · exact ⟨c :: s, List.suffix_refl _, h⟩
+      · obtain ⟨suffix, hsuf, hm⟩ := ih.mp h
+        exact ⟨suffix, hsuf.trans (List.suffix_cons c s), hm⟩
+    · rintro ⟨suffix, hsuf, hm⟩
+      rcases List.suffix_cons_iff.mp hsuf with rfl | hsuf'
+      · exact Or.inl hm
+      · exact Or.inr (ih.mpr ⟨suffix, hsuf', hm⟩)
+
+/-- A bare `*` matches every name, path separators included — so `*` in a
+    `.qedignore` ignores the whole tree, not just its top level. -/
+theorem star_matches_everything (str : List Char) : matchGlob ['*'] str = true := by
+  induction str with
+  | nil => simp [matchGlob]
+  | cons c s ih => simp [matchGlob, ih]
+
+/-- **`?` semantics:** exactly one character, and never a path separator. -/
+theorem question_matches_one (patRest str : List Char) (c : Char) :
+    matchGlob ('?' :: patRest) (c :: str) = true ↔
+      c ≠ '/' ∧ matchGlob patRest str = true := by
+  simp [matchGlob]
+
+private theorem literal_ne {p : Char} (hlit : isLiteralChar p = true) :
+    p ≠ '*' ∧ p ≠ '?' ∧ p ≠ '[' := by
+  unfold isLiteralChar at hlit
+  simp only [Bool.and_eq_true, bne_iff_ne, ne_eq] at hlit
+  exact ⟨hlit.1.1, hlit.1.2, hlit.2⟩
+
+private theorem matchGlob_literal_nil {p : Char} (ps : List Char)
+    (hlit : isLiteralChar p = true) : matchGlob (p :: ps) [] = false := by
+  have h := literal_ne hlit
+  rw [matchGlob]
+  all_goals simp_all
+
+private theorem matchGlob_literal_cons {p : Char} (ps str : List Char) (c : Char)
+    (hlit : isLiteralChar p = true) :
+    matchGlob (p :: ps) (c :: str) = (p == c && matchGlob ps str) := by
+  have h := literal_ne hlit
+  rw [matchGlob]
+  all_goals simp_all
+
+/-- **Literal semantics:** a pattern with no wildcards is an exact-match test —
+    it matches its own text and nothing else. -/
+theorem literal_matches_iff (pattern str : List Char)
+    (hlit : pattern.all isLiteralChar = true) :
+    matchGlob pattern str = true ↔ pattern = str := by
+  induction pattern generalizing str with
+  | nil => cases str <;> simp [matchGlob]
+  | cons p ps ih =>
+    simp only [List.all_cons, Bool.and_eq_true] at hlit
+    cases str with
+    | nil => simp [matchGlob_literal_nil ps hlit.1]
+    | cons c cs =>
+      rw [matchGlob_literal_cons ps cs c hlit.1]
+      simp only [Bool.and_eq_true, beq_iff_eq]
+      rw [ih cs hlit.2]
+      constructor
+      · rintro ⟨rfl, rfl⟩; rfl
+      · intro h; injection h with h1 h2; exact ⟨h1, h2⟩
+
+/-- A literal prefix followed by `*` matches every name carrying that prefix. -/
+theorem literal_star_matches_prefix (literal rest : List Char)
+    (hlit : literal.all isLiteralChar = true) :
+    matchGlob (literal ++ ['*']) (literal ++ rest) = true := by
+  induction literal with
+  | nil => simpa using star_matches_everything rest
+  | cons p ps ih =>
+    simp only [List.all_cons, Bool.and_eq_true] at hlit
+    simp only [List.cons_append]
+    rw [matchGlob_literal_cons (ps ++ ['*']) (ps ++ rest) p hlit.1]
+    simp [ih hlit.2]
+
+-- ═══════════════════════════════════════════════════════════════════
+-- shouldIgnore precedence
+-- ═══════════════════════════════════════════════════════════════════
+
 /-- Last matching pattern wins, positive direction: a trailing plain pattern
     that matches ignores the name whatever the earlier patterns decided. -/
 theorem shouldIgnore_append_positive (patterns : List String)

Tests/Ignore.lean

@@ -59,6 +59,50 @@ def testFnmatchBracketNegated : IO Bool := do
   -- Arrange / Act / Assert
   return fnmatch "[!0-9]" "a" && !fnmatch "[!0-9]" "5"
 
+-- fnmatch: backtracking
+
+def testFnmatchRepeatedStarsBacktrack : IO Bool := do
+  -- Arrange / Act / Assert
+  return fnmatch "*a*a*a*" "aaaa" && fnmatch "*a*b*c*" "xxaxxbxxcxx" &&
+    !fnmatch "*a*a*a*" "aa" && fnmatch "a**b" "ab" && fnmatch "*a" "aa"
+
+def testFnmatchStarWithTrailingWildcards : IO Bool := do
+  -- Arrange / Act / Assert
+  return fnmatch "*?" "ab" && fnmatch "?*" "ab" && fnmatch "*[ab]" "xb" &&
+    !fnmatch "*[ab]" "xc"
+
+-- fnmatch: path separators
+
+def testFnmatchStarCrossesSeparator : IO Bool := do
+  -- Arrange / Act / Assert
+  return fnmatch "*" "a/b" && fnmatch "a*b" "a/x/b" &&
+    fnmatch "*.log" "dir/x.log" && fnmatch "*/*" "a/b"
+
+def testFnmatchQuestionRejectsSeparator : IO Bool := do
+  -- Arrange / Act / Assert
+  return !fnmatch "?" "/" && !fnmatch "a?b" "a/b" && fnmatch "a?b" "axb"
+
+def testFnmatchBracketAcceptsSeparator : IO Bool := do
+  -- Arrange / Act / Assert
+  return fnmatch "[/]" "/" && fnmatch "[a/]" "/" && fnmatch "[a-c]*" "b/x"
+
+-- fnmatch: malformed bracket expressions
+
+def testFnmatchUnterminatedBracketNeverMatches : IO Bool := do
+  -- Arrange / Act / Assert
+  return !fnmatch "[" "[" && !fnmatch "[abc" "a" && !fnmatch "a[b" "a[b"
+
+def testFnmatchEmptyBracketClasses : IO Bool := do
+  -- Arrange / Act / Assert
+  return !fnmatch "[]" "]" && fnmatch "[!]" "]" && fnmatch "[a-]" "-"
+
+-- fnmatch: empty pattern and name
+
+def testFnmatchEmpty : IO Bool := do
+  -- Arrange / Act / Assert
+  return fnmatch "" "" && !fnmatch "" "a" && fnmatch "*" "" &&
+    !fnmatch "?" ""
+
 -- fnmatch: combined wildcards
 
 def testFnmatchCombined : IO Bool := do
@@ -105,6 +149,14 @@ def ignoreTests : List (String × IO Bool) := [
   ("testFnmatchBracketClass", testFnmatchBracketClass),
   ("testFnmatchBracketRange", testFnmatchBracketRange),
   ("testFnmatchBracketNegated", testFnmatchBracketNegated),
+  ("testFnmatchRepeatedStarsBacktrack", testFnmatchRepeatedStarsBacktrack),
+  ("testFnmatchStarWithTrailingWildcards", testFnmatchStarWithTrailingWildcards),
+  ("testFnmatchStarCrossesSeparator", testFnmatchStarCrossesSeparator),
+  ("testFnmatchQuestionRejectsSeparator", testFnmatchQuestionRejectsSeparator),
+  ("testFnmatchBracketAcceptsSeparator", testFnmatchBracketAcceptsSeparator),
+  ("testFnmatchUnterminatedBracketNeverMatches", testFnmatchUnterminatedBracketNeverMatches),
+  ("testFnmatchEmptyBracketClasses", testFnmatchEmptyBracketClasses),
+  ("testFnmatchEmpty", testFnmatchEmpty),
   ("testFnmatchCombined", testFnmatchCombined),
   ("testShouldIgnoreBasic", testShouldIgnoreBasic),
   ("testShouldIgnoreNegation", testShouldIgnoreNegation),