theorem Regex.Backtracker.captureNextAux.mem_of_mem_visited {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry σ nfa startPos)} {s✝ : Fin nfa.nodes.size} {i : Fin (startPos.remainingBytes + 1)} (hmem : visited.get s✝ i = true) : (captureNextAux σ nfa wf startPos visited stack).2.get s✝ i = true

theorem Regex.Backtracker.captureNextAux.mem_stack_top {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry σ nfa startPos)} (entry : StackEntry σ nfa startPos) (stack' : List (StackEntry σ nfa startPos)) (hstack : entry :: stack' = stack) : (captureNextAux σ nfa wf startPos visited stack).2.get entry.state entry.pos.index = true

def Regex.Backtracker.captureNextAux.StackInv {s : String} {nfa : NFA} {startPos : s.ValidPos} (wf : nfa.WellFormed) (bvpos : Data.BVPos startPos) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop

Equations

• Regex.Backtracker.captureNextAux.StackInv wf bvpos stack = ∀ entry ∈ stack, Regex.Backtracker.Path nfa wf bvpos.current entry.pos.current entry.state entry.update

theorem Regex.Backtracker.captureNextAux.StackInv.intro {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} (bvpos : Data.BVPos startPos) : StackInv wf bvpos [{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }]

theorem Regex.Backtracker.captureNextAux.StackInv.path {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {bvpos : Data.BVPos startPos} {entry : StackEntry (HistoryStrategy s) nfa startPos} {stack' : List (StackEntry (HistoryStrategy s) nfa startPos)} (inv : StackInv wf bvpos (entry :: stack')) : Path nfa wf bvpos.current entry.pos.current entry.state entry.update

theorem Regex.Backtracker.captureNextAux.StackInv.le {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {bvpos : Data.BVPos startPos} {entry : StackEntry (HistoryStrategy s) nfa startPos} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} (inv : StackInv wf bvpos (entry :: stack)) : bvpos ≤ entry.pos

theorem Regex.Backtracker.captureNextAux.StackInv.preserves' {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {bvpos : Data.BVPos startPos} {entry : StackEntry (HistoryStrategy s) nfa startPos} {stack' : List (StackEntry (HistoryStrategy s) nfa startPos)} (inv : StackInv wf bvpos (entry :: stack')) (nextEntries : List (StackEntry (HistoryStrategy s) nfa startPos)) (hstack : stack = nextEntries ++ stack') (hnext : ∀ entry' ∈ nextEntries, ∃ (update : Option (ℕ × s.ValidPos)), nfa.Step 0 (↑entry.state) entry.pos.current (↑entry'.state) entry'.pos.current update ∧ entry'.update = List.append entry.update (List.ofOption update)) : StackInv wf bvpos stack

theorem Regex.Backtracker.captureNextAux.StackInv.preserves {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {bvpos : Data.BVPos startPos} {stack' : List (StackEntry (HistoryStrategy s) nfa startPos)} {update : (HistoryStrategy s).Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} (inv : StackInv wf bvpos ({ update := update, state := state, pos := pos } :: stack')) : StackInv wf bvpos (pushNext (HistoryStrategy s) nfa wf startPos stack' update state pos)

theorem Regex.Backtracker.captureNextAux.path_done_of_some {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {update' : (HistoryStrategy s).Update} {visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {bvpos : Data.BVPos startPos} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited stack = (some update', visited')) (inv : StackInv wf bvpos stack) : ∃ (state : Fin nfa.nodes.size) (bvpos' : Data.BVPos startPos), nfa[state] = NFA.Node.done ∧ bvpos ≤ bvpos' ∧ Path nfa wf bvpos.current bvpos'.current state update'

def Regex.Backtracker.captureNextAux.ClosureInv {s : String} {nfa : NFA} {startPos : s.ValidPos} (bvpos₀ : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop

Equations

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

theorem Regex.Backtracker.captureNextAux.ClosureInv.preserves' {s : String} {nfa : NFA} {startPos : s.ValidPos} {bvpos₀ : Data.BVPos startPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {entry : StackEntry (HistoryStrategy s) nfa startPos} {stack' : List (StackEntry (HistoryStrategy s) nfa startPos)} (inv : ClosureInv bvpos₀ visited (entry :: stack)) (nextEntries : List (StackEntry (HistoryStrategy s) nfa startPos)) (hstack : stack' = nextEntries ++ stack) (hnext : ∀ (state' : Fin nfa.nodes.size) (bvpos' : Data.BVPos startPos) (update : Option (ℕ × s.ValidPos)), nfa.Step 0 (↑entry.state) entry.pos.current (↑state') bvpos'.current update → ∃ entry' ∈ nextEntries, entry'.state = state' ∧ entry'.pos = bvpos') : ClosureInv bvpos₀ (visited.set entry.state entry.pos.index) stack'

theorem Regex.Backtracker.captureNextAux.ClosureInv.preserves {s : String} {nfa : NFA} {startPos : s.ValidPos} {bvpos₀ : Data.BVPos startPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {update : (HistoryStrategy s).Update} {state : Fin nfa.nodes.size} {bvpos : Data.BVPos startPos} (wf : nfa.WellFormed) (inv : ClosureInv bvpos₀ visited ({ update := update, state := state, pos := bvpos } :: stack)) (hdone : nfa[state] ≠ NFA.Node.done) : ClosureInv bvpos₀ (visited.set state bvpos.index) (pushNext (HistoryStrategy s) nfa wf startPos stack update state bvpos)

theorem Regex.Backtracker.captureNextAux.step_closure {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {bvpos₀ bvpos : Data.BVPos startPos} {result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited stack = result) (isNone : result.1 = none) (cinv : ClosureInv bvpos₀ visited stack) (stinv : StackInv wf bvpos stack) : ClosureInv bvpos₀ 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 {s : String} {nfa : NFA} {startPos : s.ValidPos} (bvpos₀ : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop

Equations

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

def Regex.Backtracker.captureNextAux.PathClosure {s : String} {nfa : NFA} {startPos : s.ValidPos} (bvpos₀ : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop

Equations

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

theorem Regex.Backtracker.captureNextAux.PathClosure.zero {s : String} {nfa : NFA} {startPos : s.ValidPos} {bvpos₀ : Data.BVPos startPos} : PathClosure bvpos₀ (Data.BitMatrix.zero nfa.nodes.size (startPos.remainingBytes + 1))

theorem Regex.Backtracker.captureNextAux.PathClosure.of_step_closure {s : String} {nfa : NFA} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {bvpos₀ : Data.BVPos startPos} (wf : nfa.WellFormed) (h : StepClosure bvpos₀ visited) : PathClosure bvpos₀ visited

theorem Regex.Backtracker.captureNextAux.path_closure {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {bvpos₀ bvpos : Data.BVPos startPos} {result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited stack = result) (isNone : result.1 = none) (cinv : ClosureInv bvpos₀ visited stack) (stinv : StackInv wf bvpos stack) : PathClosure bvpos₀ 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 {s : String} {nfa : NFA} {startPos : s.ValidPos} (wf : nfa.WellFormed) (bvpos₀ bvpos : Data.BVPos startPos) (visited visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop

Equations

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

theorem Regex.Backtracker.captureNextAux.VisitedInv.rfl {s : String} {nfa : NFA} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (wf : nfa.WellFormed) (bvpos₀ bvpos : Data.BVPos startPos) : VisitedInv wf bvpos₀ bvpos visited visited

theorem Regex.Backtracker.captureNextAux.VisitedInv.preserves {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {bvpos₀ bvpos : Data.BVPos startPos} {visited visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {bvpos' : Data.BVPos startPos} {state : Fin nfa.nodes.size} (inv : VisitedInv wf bvpos₀ bvpos visited visited') (update : List (ℕ × s.ValidPos)) (path : Path nfa wf bvpos.current bvpos'.current state update) : VisitedInv wf bvpos₀ bvpos visited (visited'.set state bvpos'.index)

theorem Regex.Backtracker.captureNextAux.visited_inv_of_none {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {bvpos₀ bvpos : Data.BVPos startPos} {visited visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited' stack = result) (isNone : result.1 = none) (vinv : VisitedInv wf bvpos₀ bvpos visited visited') (stinv : StackInv wf bvpos stack) : VisitedInv wf bvpos₀ bvpos visited result.2

def Regex.Backtracker.captureNextAux.NotDoneInv {s : String} {nfa : NFA} {startPos : s.ValidPos} (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop

Equations

• Regex.Backtracker.captureNextAux.NotDoneInv visited = ∀ (state : Fin nfa.nodes.size) (bvpos : Regex.Data.BVPos startPos), visited.get state bvpos.index = true → nfa[state] ≠ Regex.NFA.Node.done

theorem Regex.Backtracker.captureNextAux.NotDoneInv.zero {s : String} {nfa : NFA} {startPos : s.ValidPos} : NotDoneInv (Data.BitMatrix.zero nfa.nodes.size (startPos.remainingBytes + 1))

theorem Regex.Backtracker.captureNextAux.NotDoneInv.preserves {s : String} {nfa : NFA} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {state : Fin nfa.nodes.size} {bvpos : Data.BVPos startPos} (inv : NotDoneInv visited) (h : nfa[state] ≠ NFA.Node.done) : NotDoneInv (visited.set state bvpos.index)

theorem Regex.Backtracker.captureNextAux.not_done_of_none {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited stack = result) (isNone : result.1 = none) (inv : NotDoneInv visited) : NotDoneInv result.2