theorem Regex.NFA.Step.εStep_or_charStep {s : String} {nfa : NFA} {pos pos' : s.ValidPos} {update : Option (ℕ × s.ValidPos)} {i j : ℕ} (wf : nfa.WellFormed) (step : nfa.Step 0 i pos j pos' update) : nfa.εStep' pos ⟨i, ⋯⟩ ⟨j, ⋯⟩ update ∧ pos' = pos ∨ nfa.CharStep pos ⟨i, ⋯⟩ ⟨j, ⋯⟩ ∧ update = none ∧ ∃ (ne : pos ≠ s.endValidPos), pos' = pos.next ne

inductive Regex.NFA.VMPath {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos₀ : s.ValidPos) : s.ValidPos → Fin nfa.nodes.size → List (ℕ × s.ValidPos) → Prop

• init {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} (le : pos₀ ≤ pos) (cls : nfa.εClosure' pos ⟨nfa.start, ⋯⟩ i update) : nfa.VMPath wf pos₀ pos i update
• more {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ : s.ValidPos} {i j k : Fin nfa.nodes.size} {pos pos' : s.ValidPos} {update₁ update₂ update₃ : List (ℕ × s.ValidPos)} (prev : nfa.VMPath wf pos₀ pos i update₁) (step : nfa.CharStep pos i j) (cls : nfa.εClosure' (pos.next ⋯) j k update₂) (hupdate : update₃ = update₁ ++ update₂) (hpos : pos' = pos.next ⋯) : nfa.VMPath wf pos₀ pos' k update₃

theorem Regex.NFA.VMPath.more_εStep {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {i j : Fin nfa.nodes.size} {update₁ : List (ℕ × s.ValidPos)} {update₂ : Option (ℕ × s.ValidPos)} (prev : nfa.VMPath wf pos₀ pos i update₁) (step : nfa.εStep' pos i j update₂) : nfa.VMPath wf pos₀ pos j (update₁ ++ List.ofOption update₂)

theorem Regex.NFA.VMPath.more_charStep {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {i j : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} (prev : nfa.VMPath wf pos₀ pos i update) (step : nfa.CharStep pos i j) : nfa.VMPath wf pos₀ (pos.next ⋯) j update

theorem Regex.NFA.VMPath.more_step {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos pos' : s.ValidPos} {i : Fin nfa.nodes.size} {j : ℕ} {update₁ : List (ℕ × s.ValidPos)} {update₂ : Option (ℕ × s.ValidPos)} (prev : nfa.VMPath wf pos₀ pos i update₁) (step : nfa.Step 0 (↑i) pos j pos' update₂) : nfa.VMPath wf pos₀ pos' ⟨j, ⋯⟩ (update₁ ++ List.ofOption update₂)

theorem Regex.NFA.VMPath.le {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} (path : nfa.VMPath wf pos₀ pos i update) : pos₀ ≤ pos

theorem Regex.NFA.VMPath.εClosure_of_eq_it {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos : s.ValidPos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} (path : nfa.VMPath wf pos pos i update) : nfa.εClosure' pos ⟨nfa.start, ⋯⟩ i update

theorem Regex.NFA.VMPath.eq_or_nfaPath {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} (path : nfa.VMPath wf pos₀ pos i update) : ↑i = nfa.start ∧ update = [] ∧ pos₀ ≤ pos ∨ ∃ (poss : s.ValidPos), pos₀ ≤ poss ∧ nfa.Path 0 nfa.start poss (↑i) pos update

theorem Regex.NFA.VMPath.nfaPath_of_ne {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} (path : nfa.VMPath wf pos₀ pos i update) (ne : ↑i ≠ nfa.start) : ∃ (poss : s.ValidPos), pos₀ ≤ poss ∧ nfa.Path 0 nfa.start poss (↑i) pos update

theorem Regex.NFA.VMPath.concat_nfaPath {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos pos' : s.ValidPos} {i j : ℕ} {update₁ update₂ : List (ℕ × s.ValidPos)} (isLt₁ : i < nfa.nodes.size) (path₁ : nfa.VMPath wf pos₀ pos ⟨i, isLt₁⟩ update₁) (path₂ : nfa.Path 0 i pos j pos' update₂) : nfa.VMPath wf pos₀ pos' ⟨j, ⋯⟩ (update₁ ++ update₂)

theorem Regex.NFA.VMPath.of_nfaPath {s : String} {nfa : NFA} {pos₀ pos pos' : s.ValidPos} {i : ℕ} {update : List (ℕ × s.ValidPos)} (wf : nfa.WellFormed) (le : pos₀ ≤ pos) (path : nfa.Path 0 nfa.start pos i pos' update) : nfa.VMPath wf pos₀ pos' ⟨i, ⋯⟩ update

def Regex.VM.SearchState.Inv {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos₀ pos : s.ValidPos) (next : SearchState (HistoryStrategy s) nfa) : Prop

The invariant for the soundness theorem.

All states in next.state have a corresponding path from nfa.start to the state ending at pos, and their updates are written to next.updates when necessary.

Equations

• One or more equations did not get rendered due to their size.

theorem Regex.VM.SearchState.Inv.of_empty {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos₀ pos : s.ValidPos} {next : SearchState (HistoryStrategy s) nfa} (h : next.states.isEmpty = true) : Inv nfa wf pos₀ pos next

def Regex.VM.SearchState.MemOfPathInv {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos₀ pos : s.ValidPos) (next : SearchState (HistoryStrategy s) nfa) : Prop

The invariant for the completeness theorem. The invariant holds only when returning .none, since we short-circuit when encountering .done.

For all paths ending at pos, the state must be tracked in next.states. We don't care about the updates for the completeness.

Equations

• Regex.VM.SearchState.MemOfPathInv nfa wf pos₀ pos next = ∀ (i : Fin nfa.nodes.size) (update : List (ℕ × s.ValidPos)), nfa.VMPath wf pos₀ pos i update → i ∈ next.states

def Regex.VM.SearchState.NotDoneInv {s : String} (σ : Strategy s) (nfa : NFA) (next : SearchState σ nfa) : Prop

Invariant for the completeness theorem.

The .done state is not in next.states.

Equations

• Regex.VM.SearchState.NotDoneInv σ nfa next = ∀ i ∈ next.states, nfa[i] ≠ Regex.NFA.Node.done

theorem Regex.VM.SearchState.NotDoneInv.of_empty {s : String} {σ : Strategy s} {nfa : NFA} {next : SearchState σ nfa} (h : next.states.isEmpty = true) : NotDoneInv σ nfa next

theorem Regex.NFA.CharStep.write_update {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} (step : nfa.CharStep pos i j) : VM.εClosure.writeUpdate nfa[i] = true