theorem
Regex.Backtracker.captureNextAux.mem_of_mem_visited
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{s : Fin nfa.nodes.size}
{i : Fin (maxIdx + 1 - startIdx)}
(hmem : visited.get s i = true)
:
theorem
Regex.Backtracker.captureNextAux.mem_stack_top
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
(entry : StackEntry σ nfa startIdx maxIdx)
(stack' : List (StackEntry σ nfa startIdx maxIdx))
(hstack : entry :: stack' = stack)
:
def
Regex.Backtracker.captureNextAux.StackInv
{nfa : NFA}
{startIdx maxIdx : ℕ}
(wf : nfa.WellFormed)
(bit : Data.BoundedIterator startIdx maxIdx)
(stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx))
:
Equations
- Regex.Backtracker.captureNextAux.StackInv wf bit stack = ∀ entry ∈ stack, Regex.Backtracker.Path nfa wf bit.it entry.it.it entry.state entry.update
Instances For
theorem
Regex.Backtracker.captureNextAux.StackInv.intro
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit : Data.BoundedIterator startIdx maxIdx}
(v : bit.Valid)
:
theorem
Regex.Backtracker.captureNextAux.StackInv.path
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit : Data.BoundedIterator startIdx maxIdx}
{entry : StackEntry HistoryStrategy nfa startIdx maxIdx}
{stack' : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
(inv : StackInv wf bit (entry :: stack'))
:
theorem
Regex.Backtracker.captureNextAux.StackInv.reaches
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit : Data.BoundedIterator startIdx maxIdx}
{entry : StackEntry HistoryStrategy nfa startIdx maxIdx}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
(inv : StackInv wf bit (entry :: stack))
:
theorem
Regex.Backtracker.captureNextAux.StackInv.preserves'
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{bit : Data.BoundedIterator startIdx maxIdx}
{entry : StackEntry HistoryStrategy nfa startIdx maxIdx}
{stack' : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
(inv : StackInv wf bit (entry :: stack'))
(nextEntries : List (StackEntry HistoryStrategy nfa startIdx maxIdx))
(hstack : stack = nextEntries ++ stack')
(hnext :
∀ entry' ∈ nextEntries,
∃ (update : Option (ℕ × String.Pos)),
nfa.Step 0 (↑entry.state) entry.it.it (↑entry'.state) entry'.it.it update ∧ entry'.update = List.append entry.update (List.ofOption update))
:
StackInv wf bit stack
theorem
Regex.Backtracker.captureNextAux.StackInv.preserves
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit : Data.BoundedIterator startIdx maxIdx}
{stack' : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{update : HistoryStrategy.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
(inv : StackInv wf bit ({ update := update, state := state, it := it } :: stack'))
:
StackInv wf bit (pushNext HistoryStrategy nfa wf startIdx maxIdx stack' update state it)
theorem
Regex.Backtracker.captureNextAux.path_done_of_some
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{update' : HistoryStrategy.Update}
{visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{bit : Data.BoundedIterator startIdx maxIdx}
(hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited stack = (some update', visited'))
(inv : StackInv wf bit stack)
:
def
Regex.Backtracker.captureNextAux.ClosureInv
{nfa : NFA}
{startIdx maxIdx : ℕ}
(bit₀ : Data.BoundedIterator startIdx maxIdx)
(visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
(stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Regex.Backtracker.captureNextAux.ClosureInv.preserves'
{nfa : NFA}
{startIdx maxIdx : ℕ}
{bit₀ : Data.BoundedIterator startIdx maxIdx}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{entry : StackEntry HistoryStrategy nfa startIdx maxIdx}
{stack' : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
(inv : ClosureInv bit₀ visited (entry :: stack))
(reaches₀ : bit₀.Reaches entry.it)
(nextEntries : List (StackEntry HistoryStrategy nfa startIdx maxIdx))
(hstack : stack' = nextEntries ++ stack)
(hnext :
∀ (state' : Fin nfa.nodes.size) (bit' : Data.BoundedIterator startIdx maxIdx) (update : Option (ℕ × String.Pos)),
nfa.Step 0 (↑entry.state) entry.it.it (↑state') bit'.it update →
∃ entry' ∈ nextEntries, entry'.state = state' ∧ entry'.it = bit')
:
ClosureInv bit₀ (visited.set entry.state entry.it.index) stack'
theorem
Regex.Backtracker.captureNextAux.ClosureInv.preserves
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit₀ : Data.BoundedIterator startIdx maxIdx}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{update : HistoryStrategy.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
(inv : ClosureInv bit₀ visited ({ update := update, state := state, it := it } :: stack))
(reaches₀ : bit₀.Reaches it)
(hdone : nfa[state] ≠ NFA.Node.done)
:
ClosureInv bit₀ (visited.set state it.index) (pushNext HistoryStrategy nfa wf startIdx maxIdx stack update state it)
theorem
Regex.Backtracker.captureNextAux.step_closure
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{bit₀ bit : Data.BoundedIterator startIdx maxIdx}
{result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited stack = result)
(isNone : result.1 = none)
(reaches₀ : bit₀.Reaches bit)
(cinv : ClosureInv bit₀ visited stack)
(stinv : StackInv wf bit stack)
:
ClosureInv bit₀ result.2 []
When the backtracker returns .none, it explores all reachable states and thus the visited set satisfies the closure property under the step relation.
def
Regex.Backtracker.captureNextAux.StepClosure
{nfa : NFA}
{startIdx maxIdx : ℕ}
(bit₀ : Data.BoundedIterator startIdx maxIdx)
(visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Regex.Backtracker.captureNextAux.PathClosure
{nfa : NFA}
{startIdx maxIdx : ℕ}
(bit₀ : Data.BoundedIterator startIdx maxIdx)
(visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Regex.Backtracker.captureNextAux.PathClosure.zero
{nfa : NFA}
{startIdx maxIdx : ℕ}
{bit₀ : Data.BoundedIterator startIdx maxIdx}
:
PathClosure bit₀ (Data.BitMatrix.zero nfa.nodes.size (maxIdx + 1 - startIdx))
theorem
Regex.Backtracker.captureNextAux.PathClosure.of_step_closure
{nfa : NFA}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{bit₀ : Data.BoundedIterator startIdx maxIdx}
(wf : nfa.WellFormed)
(h : StepClosure bit₀ visited)
:
PathClosure bit₀ visited
theorem
Regex.Backtracker.captureNextAux.path_closure
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{bit₀ bit : Data.BoundedIterator startIdx maxIdx}
{result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited stack = result)
(isNone : result.1 = none)
(reaches₀ : bit₀.Reaches bit)
(cinv : ClosureInv bit₀ visited stack)
(stinv : StackInv wf bit stack)
:
PathClosure bit₀ result.2
The closure property of the visited set can be lifted to paths.
Note: nfa.Path requires at least one step, so this is a transitive closure. However, the existence in the visited set
is obviously reflexive.
def
Regex.Backtracker.captureNextAux.VisitedInv
{nfa : NFA}
{startIdx maxIdx : ℕ}
(wf : nfa.WellFormed)
(bit₀ bit : Data.BoundedIterator startIdx maxIdx)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Regex.Backtracker.captureNextAux.VisitedInv.rfl
{nfa : NFA}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{wf : nfa.WellFormed}
{bit₀ bit : Data.BoundedIterator startIdx maxIdx}
(reaches₀ : bit₀.Reaches bit)
:
VisitedInv wf bit₀ bit reaches₀ visited visited
theorem
Regex.Backtracker.captureNextAux.VisitedInv.preserves
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit₀ bit : Data.BoundedIterator startIdx maxIdx}
{reaches₀ : bit₀.Reaches bit}
{visited visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{bit' : Data.BoundedIterator startIdx maxIdx}
{state : Fin nfa.nodes.size}
(inv : VisitedInv wf bit₀ bit reaches₀ visited visited')
(reaches : bit₀.Reaches bit')
(update : List (ℕ × String.Pos))
(path : Path nfa wf bit.it bit'.it state update)
:
VisitedInv wf bit₀ bit reaches₀ visited (visited'.set state bit'.index)
theorem
Regex.Backtracker.captureNextAux.visited_inv_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit₀ bit : Data.BoundedIterator startIdx maxIdx}
{reaches₀ : bit₀.Reaches bit}
{visited visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited' stack = result)
(isNone : result.1 = none)
(vinv : VisitedInv wf bit₀ bit reaches₀ visited visited')
(stinv : StackInv wf bit stack)
:
VisitedInv wf bit₀ bit reaches₀ visited result.2
def
Regex.Backtracker.captureNextAux.NotDoneInv
{nfa : NFA}
{startIdx maxIdx : ℕ}
(visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Regex.Backtracker.captureNextAux.NotDoneInv.zero
{nfa : NFA}
{startIdx maxIdx : ℕ}
:
NotDoneInv (Data.BitMatrix.zero nfa.nodes.size (maxIdx + 1 - startIdx))
theorem
Regex.Backtracker.captureNextAux.NotDoneInv.preserves
{nfa : NFA}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{state : Fin nfa.nodes.size}
{bit : Data.BoundedIterator startIdx maxIdx}
(inv : NotDoneInv visited)
(h : nfa[state] ≠ NFA.Node.done)
:
NotDoneInv (visited.set state bit.index)
theorem
Regex.Backtracker.captureNextAux.not_done_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{stack : List (StackEntry HistoryStrategy nfa startIdx maxIdx)}
{result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited stack = result)
(isNone : result.1 = none)
(inv : NotDoneInv visited)
:
NotDoneInv result.2