theorem Regex.VM.εClosure.pushNext.mem_of_mem_stack {σ : Strategy} {nfa : NFA} {it : String.Iterator} {node : NFA.Node} {inBounds : node.inBounds nfa.nodes.size} {update : σ.Update} {stack : εStack σ nfa} {entry : σ.Update × Fin nfa.nodes.size} (mem : entry ∈ stack) : entry ∈ pushNext σ nfa it node inBounds update stack

theorem Regex.VM.εClosure.subset {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} (h : εClosure σ nfa wf it matched next stack = (matched', next')) : next.states ⊆ next'.states

theorem Regex.VM.εClosure.mem_next_of_mem_stack {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} {entry : σ.Update × Fin nfa.nodes.size} (h : εClosure σ nfa wf it matched next stack = (matched', next')) (mem_stack : entry ∈ stack) : entry.2 ∈ next'.states

theorem Regex.VM.εClosure.eq_updates_of_mem_next {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} {i : Fin nfa.nodes.size} (h : εClosure σ nfa wf it matched next stack = (matched', next')) (mem' : i ∈ next.states) : next'.updates[i] = next.updates[i]

theorem Regex.VM.εClosure.eq_matched_some {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} (h : εClosure σ nfa wf it matched next stack = (matched', next')) (isSome : matched.isSome = true) : matched' = matched

theorem Regex.VM.εClosure.matched_inv {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} (h : εClosure σ nfa wf it matched next stack = (matched', next')) (inv : ∀ (isSome : matched.isSome = true), ∃ i ∈ next.states, nfa[i] = NFA.Node.done ∧ next.updates[i] = matched.get isSome) (isSome' : matched'.isSome = true) : ∃ i ∈ next'.states, nfa[i] = NFA.Node.done ∧ next'.updates[i] = matched'.get isSome'

theorem Regex.VM.εClosure.not_done_of_none {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} (result : Option σ.Update × SearchState σ nfa) (h : εClosure σ nfa wf it matched next stack = result) (isNone : result.1 = none) (inv : SearchState.NotDoneInv σ nfa next) : SearchState.NotDoneInv σ nfa result.2

def Regex.VM.εClosure.LowerInvStep {σ : Strategy} {nfa : NFA} (it : String.Iterator) (states : Data.SparseSet nfa.nodes.size) (stack : εStack σ nfa) : Prop

Equations

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

def Regex.VM.εClosure.LowerBoundStep {nfa : NFA} (it : String.Iterator) (states : Data.SparseSet nfa.nodes.size) : Prop

Equations

• Regex.VM.εClosure.LowerBoundStep it states = ∀ (i j : Fin nfa.nodes.size) (update : Option (ℕ × String.Pos)), i ∈ states → nfa.εStep' it i j update → j ∈ states

def Regex.VM.εClosure.LowerBound {nfa : NFA} (it : String.Iterator) (states : Data.SparseSet nfa.nodes.size) : Prop

Equations

• Regex.VM.εClosure.LowerBound it states = ∀ (i j : Fin nfa.nodes.size) (update : List (ℕ × String.Pos)), i ∈ states → nfa.εClosure' it i j update → j ∈ states

theorem Regex.VM.εClosure.LowerBound.of_empty {nfa : NFA} {it : String.Iterator} {states : Data.SparseSet nfa.nodes.size} (h : states.isEmpty = true) : LowerBound it states

theorem Regex.VM.εClosure.LowerBound.of_step {nfa : NFA} {it : String.Iterator} {states : Data.SparseSet nfa.nodes.size} (h : LowerBoundStep it states) : LowerBound it states

theorem Regex.VM.εClosure.LowerInvStep.preserves' {σ : Strategy} {nfa : NFA} {it : String.Iterator} {stack : εStack σ nfa} {states : Data.SparseSet nfa.nodes.size} {entry : σ.Update × Fin nfa.nodes.size} {stack' : εStack σ nfa} (hmem : entry.2 ∉ states) (nextEntries : εStack σ nfa) (hstack : stack' = nextEntries ++ stack) (h : ∀ (j : Fin nfa.nodes.size) (update : Option (ℕ × String.Pos)), nfa.εStep' it entry.2 j update → ∃ (update' : σ.Update), (update', j) ∈ nextEntries) (inv : LowerInvStep it states (entry :: stack)) : LowerInvStep it (states.insert entry.2 hmem) stack'

theorem Regex.VM.εClosure.LowerInvStep.preserves {σ : Strategy} {nfa : NFA} {it : String.Iterator} {stack : εStack σ nfa} {states : Data.SparseSet nfa.nodes.size} {entry : σ.Update × Fin nfa.nodes.size} (wf : nfa.WellFormed) (hmem : entry.2 ∉ states) (inv : LowerInvStep it states (entry :: stack)) : LowerInvStep it (states.insert entry.2 hmem) (pushNext σ nfa it nfa[entry.2] ⋯ entry.1 stack)

theorem Regex.VM.εClosure.lower_bound_step {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {matched : Option σ.Update} {next : SearchState σ nfa} {stack : εStack σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} {it : String.Iterator} (h : εClosure σ nfa wf it matched next stack = (matched', next')) (inv : LowerInvStep it next.states stack) : LowerBoundStep it next'.states

theorem Regex.VM.εClosure.lower_bound {σ : Strategy} {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option σ.Update} {next : SearchState σ nfa} {matched' : Option σ.Update} {next' : SearchState σ nfa} {i : Fin nfa.nodes.size} {update : σ.Update} (h : εClosure σ nfa wf it matched next [(update, i)] = (matched', next')) (lb : LowerBound it next.states) : LowerBound it next'.states

structure Regex.VM.εClosure.UpperInv {nfa : NFA} (states₀ : Data.SparseSet nfa.nodes.size) (it₀ : String.Iterator) (i₀ : Fin nfa.nodes.size) (update₀ : List (ℕ × String.Pos)) (next : SearchState HistoryStrategy nfa) (stack : εStack HistoryStrategy nfa) : Prop

Intuition: given that we reached i₀ (from nfa.start) with it₀ and update₀, the εClosure traversal first puts states reachable from i₀ into the stack with an appropriate update list. Next, the traversal pops the states from the stack and writes them to next, recording the update list to updates for the necessary states. Since we only care about ε-transitions, the iterator doesn't change during the traversal.

At the end of the traversal, we can guarantee that all states in next were already in states₀ or they are reachable from i₀ with the updates written to next.updates.

• mem_stack (update : HistoryStrategy.Update) (j : Fin nfa.nodes.size) : (update, j) ∈ stack → ∃ (update' : List (ℕ × String.Pos)), update = update₀ ++ update' ∧ nfa.εClosure' it₀ i₀ j update'
• mem_next (j : Fin nfa.nodes.size) : j ∈ next.states → j ∈ states₀ ∨ ∃ (update' : List (ℕ × String.Pos)), nfa.εClosure' it₀ i₀ j update' ∧ (writeUpdate nfa[j] = true → next.updates[j] = update₀ ++ update')

theorem Regex.VM.εClosure.UpperInv.it_valid {nfa : NFA} {states₀ : Data.SparseSet nfa.nodes.size} {it₀ : String.Iterator} {i₀ : Fin nfa.nodes.size} {update₀ : List (ℕ × String.Pos)} {next : SearchState HistoryStrategy nfa} {stack : εStack HistoryStrategy nfa} {entry : HistoryStrategy.Update × Fin nfa.nodes.size} (inv : UpperInv states₀ it₀ i₀ update₀ next (entry :: stack)) : it₀.Valid

theorem Regex.VM.εClosure.UpperInv.preserves' {nfa : NFA} {states₀ : Data.SparseSet nfa.nodes.size} {it₀ : String.Iterator} {i₀ : Fin nfa.nodes.size} {update₀ : List (ℕ × String.Pos)} {next : SearchState HistoryStrategy nfa} {entry : List (ℕ × String.Pos) × Fin nfa.nodes.size} {stack stack' : εStack HistoryStrategy nfa} {node : NFA.Node} (hn : nfa[entry.2] = node) (nextEntries : εStack HistoryStrategy nfa) (hstack : stack' = nextEntries ++ stack) (not_mem : entry.2 ∉ next.states) (h : ∀ (update : HistoryStrategy.Update) (j : Fin nfa.nodes.size), (update, j) ∈ nextEntries → ∃ (update' : Option (ℕ × String.Pos)), update = entry.1 ++ List.ofOption update' ∧ nfa.εStep' it₀ entry.2 j update') (inv : UpperInv states₀ it₀ i₀ update₀ next (entry :: stack)) : UpperInv states₀ it₀ i₀ update₀ { states := next.states.insert entry.2 not_mem, updates := if writeUpdate node = true then next.updates.set (↑entry.2) entry.1 ⋯ else next.updates } stack'

theorem Regex.VM.εClosure.UpperInv.preserves {nfa : NFA} {states₀ : Data.SparseSet nfa.nodes.size} {it₀ : String.Iterator} {i₀ : Fin nfa.nodes.size} {update₀ : List (ℕ × String.Pos)} {next : SearchState HistoryStrategy nfa} {stack : εStack HistoryStrategy nfa} {update : List (ℕ × String.Pos)} {state : Fin nfa.nodes.size} (wf : nfa.WellFormed) (not_mem : state ∉ next.states) (inv : UpperInv states₀ it₀ i₀ update₀ next ((update, state) :: stack)) : UpperInv states₀ it₀ i₀ update₀ { states := next.states.insert state not_mem, updates := if writeUpdate nfa[state] = true then next.updates.set (↑state) update ⋯ else next.updates } (pushNext HistoryStrategy nfa it₀ nfa[state] ⋯ update stack)

theorem Regex.VM.εClosure.upper_boundAux {nfa : NFA} {wf : nfa.WellFormed} {matched : Option (List (ℕ × String.Pos))} {next : SearchState HistoryStrategy nfa} {stack : εStack HistoryStrategy nfa} {matched' : Option (List (ℕ × String.Pos))} {next' : SearchState HistoryStrategy nfa} (states₀ : Data.SparseSet nfa.nodes.size) (it₀ : String.Iterator) (i₀ : Fin nfa.nodes.size) (update₀ : List (ℕ × String.Pos)) (h : εClosure HistoryStrategy nfa wf it₀ matched next stack = (matched', next')) (inv₀ : UpperInv states₀ it₀ i₀ update₀ next stack) : UpperInv states₀ it₀ i₀ update₀ next' []

All new states in next' are reachable from the starting state i₀ and have corresponding updates in next'.updates.

theorem Regex.VM.εClosure.UpperInv.intro {nfa : NFA} {next : SearchState HistoryStrategy nfa} {i₀ : Fin nfa.nodes.size} {update₀ : List (ℕ × String.Pos)} (it₀ : String.Iterator) (v : it₀.Valid) : UpperInv next.states it₀ i₀ update₀ next [(update₀, i₀)]

Upper invariant at the start of the εClosure traversal.

theorem Regex.VM.εClosure.upper_bound {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option (List (ℕ × String.Pos))} {next : SearchState HistoryStrategy nfa} {matched' : Option (List (ℕ × String.Pos))} {next' : SearchState HistoryStrategy nfa} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (h : εClosure HistoryStrategy nfa wf it matched next [(update, i)] = (matched', next')) (v : it.Valid) (j : Fin nfa.nodes.size) : j ∈ next'.states → j ∈ next.states ∨ ∃ (update' : List (ℕ × String.Pos)), nfa.εClosure' it i j update' ∧ (writeUpdate nfa[j] = true → next'.updates[j] = update ++ update')

theorem Regex.VM.εClosure.mem_next {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option (List (ℕ × String.Pos))} {next : SearchState HistoryStrategy nfa} {matched' : Option (List (ℕ × String.Pos))} {next' : SearchState HistoryStrategy nfa} {i : Fin nfa.nodes.size} {update : HistoryStrategy.Update} (h : εClosure HistoryStrategy nfa wf it matched next [(update, i)] = (matched', next')) (lb : LowerBound it next.states) {j : Fin nfa.nodes.size} {update' : List (ℕ × String.Pos)} (cls : nfa.εClosure' it i j update') : j ∈ next'.states

εClosure inserts all states in the ε-closure of i into next.states.

theorem Regex.VM.εClosure.write_updates_of_mem_next {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option (List (ℕ × String.Pos))} {next : SearchState HistoryStrategy nfa} {matched' : Option (List (ℕ × String.Pos))} {next' : SearchState HistoryStrategy nfa} {i j : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (h : εClosure HistoryStrategy nfa wf it matched next [(update, i)] = (matched', next')) (v : it.Valid) (mem : j ∈ next'.states) : j ∈ next.states ∨ ∃ (update' : List (ℕ × String.Pos)), nfa.εClosure' it i j update' ∧ (writeUpdate nfa[j] = true → next'.updates[j] = update ++ update')

All states in next'.states are already in next.states or they are reachable from i with the updates written to next'.updates.

theorem Regex.VM.εClosure.write_updates {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option (List (ℕ × String.Pos))} {next : SearchState HistoryStrategy nfa} {matched' : Option (List (ℕ × String.Pos))} {next' : SearchState HistoryStrategy nfa} {i j : Fin nfa.nodes.size} {update update' : List (ℕ × String.Pos)} (v : it.Valid) (h : εClosure HistoryStrategy nfa wf it matched next [(update, i)] = (matched', next')) (lb : LowerBound it next.states) (cls : nfa.εClosure' it i j update') : j ∈ next.states ∨ ∃ (update' : List (ℕ × String.Pos)), nfa.εClosure' it i j update' ∧ (writeUpdate nfa[j] = true → next'.updates[j] = update ++ update')

For all states in the ε-closure of i, it's already in next.states or there is a path from i whose updates are written to next.updates. The written update list can be different since the traversal may have reached the state through a different path.

theorem Regex.VM.εClosure.inv_of_inv {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {matched : Option (List (ℕ × String.Pos))} {next : SearchState HistoryStrategy nfa} {matched' : Option (List (ℕ × String.Pos))} {next' : SearchState HistoryStrategy nfa} {it₀ : String.Iterator} (h : εClosure HistoryStrategy nfa wf it matched next [([], ⟨nfa.start, ⋯⟩)] = (matched', next')) (eqs : it.toString = it₀.toString) (le : it₀.pos ≤ it.pos) (v : it.Valid) (inv : SearchState.Inv nfa wf it₀ it next) : SearchState.Inv nfa wf it₀ it next'