theorem
Regex.Backtracker.captureNextAux.mem_or_path_of_mem_of_none
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(hres :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }] = result)
(isNone : result.1 = none)
:
VisitedInv wf bvpos₀ bvpos visited result.2
theorem
Regex.Backtracker.captureNextAux.PathClosure.preserves
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(hres :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }] = result)
(isNone : result.1 = none)
(cls : PathClosure bvpos₀ visited)
:
PathClosure bvpos₀ result.2
theorem
Regex.Backtracker.captureNextAux.mem_of_path_of_none
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(hres :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }] = result)
(isNone : result.1 = none)
(le₀ : bvpos₀ ≤ bvpos)
(cls : PathClosure bvpos₀ visited)
(bvpos' : Data.BVPos startPos)
(state : Fin nfa.nodes.size)
(update : List (ℕ × s.ValidPos))
(path : Path nfa wf bvpos.current bvpos'.current state update)
:
theorem
Regex.Backtracker.captureNextAux.mem_iff_mem_or_path_of_none
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(hres :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }] = result)
(isNone : result.1 = none)
(le₀ : bvpos₀ ≤ bvpos)
(cls : PathClosure bvpos₀ visited)
(bvpos' : Data.BVPos startPos)
(state : Fin nfa.nodes.size)
(le₀' : bvpos₀ ≤ bvpos')
:
structure
Regex.Backtracker.captureNext.go.Inv
{s : String}
{nfa : NFA}
{startPos : s.ValidPos}
(wf : nfa.WellFormed)
(bvpos₀ bvpos : Data.BVPos startPos)
(visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1))
:
- closure : captureNextAux.PathClosure bvpos₀ visited
- mem_iff_path (state' : Fin nfa.nodes.size) (bvpos' : Data.BVPos startPos) : bvpos₀ ≤ bvpos' → (visited.get state' bvpos'.index = true ↔ ∃ (bvposPrev : Data.BVPos startPos) (update : List (ℕ × s.ValidPos)), bvpos₀ ≤ bvposPrev ∧ bvposPrev < bvpos ∧ Path nfa wf bvposPrev.current bvpos'.current state' update)
Instances For
theorem
Regex.Backtracker.captureNext.go.Inv.zero
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ : Data.BVPos startPos}
:
Inv wf bvpos₀ bvpos₀ (Data.BitMatrix.zero nfa.nodes.size (startPos.remainingBytes + 1))
theorem
Regex.Backtracker.captureNext.go.Inv.mem_iff_of_aux_none
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(haux :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }] = result)
(isNone : result.1 = none)
(le₀ : bvpos₀ ≤ bvpos)
(inv : Inv wf bvpos₀ bvpos visited)
(state' : Fin nfa.nodes.size)
(bvpos' : Data.BVPos startPos)
(le₀' : bvpos₀ ≤ bvpos')
:
result.2.get state' bvpos'.index = true ↔ (∃ (bvposPrev : Data.BVPos startPos) (update : List (ℕ × s.ValidPos)),
bvpos₀ ≤ bvposPrev ∧ bvposPrev < bvpos ∧ Path nfa wf bvposPrev.current bvpos'.current state' update) ∨ ∃ (update : List (ℕ × s.ValidPos)), Path nfa wf bvpos.current bvpos'.current state' update
theorem
Regex.Backtracker.captureNext.go.Inv.preservesAux
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(haux :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := bvpos }] = result)
(isNone : result.1 = none)
(ne : bvpos ≠ s.endBVPos startPos)
(le₀ : bvpos₀ ≤ bvpos)
(inv : Inv wf bvpos₀ bvpos visited)
:
theorem
Regex.Backtracker.captureNext.go.Inv.mem_iff_path_of_aux_none_endBVPos
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{result : Option (HistoryStrategy s).Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(haux :
captureNextAux (HistoryStrategy s) nfa wf startPos visited
[{ update := (HistoryStrategy s).empty, state := ⟨nfa.start, ⋯⟩, pos := s.endBVPos startPos }] = result)
(isNone : result.1 = none)
(inv : Inv wf bvpos₀ (s.endBVPos startPos) visited)
(state' : Fin nfa.nodes.size)
(bvpos' : Data.BVPos startPos)
(le₀' : bvpos₀ ≤ bvpos')
:
theorem
Regex.Backtracker.captureNext.go.ne_done_of_path_of_none
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos₀ bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
(hres : go (HistoryStrategy s) nfa wf startPos bvpos visited = none)
(le₀ : bvpos₀ ≤ bvpos)
(inv : Inv wf bvpos₀ bvpos visited)
(ndinv : captureNextAux.NotDoneInv visited)
(bvpos' bvpos'' : Data.BVPos startPos)
(state : Fin nfa.nodes.size)
(update : List (ℕ × s.ValidPos))
:
theorem
Regex.Backtracker.captureNext.go.path_done_of_some
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{startPos : s.ValidPos}
{bvpos : Data.BVPos startPos}
{visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
{update : (HistoryStrategy s).Update}
(hres : go (HistoryStrategy s) nfa wf startPos bvpos visited = some update)
:
∃ (state : Fin nfa.nodes.size) (bvpos' : Data.BVPos startPos) (bvpos'' : Data.BVPos startPos),
nfa[state] = NFA.Node.done ∧ bvpos ≤ bvpos' ∧ Path nfa wf bvpos'.current bvpos''.current state update