BoundedBacktracker

An NFA backed bounded backtracker for executing regex searches with capturing groups (BoundedBacktracker.slots).

This regex engine only implements leftmost-first match semantics and only supports leftmost searches. By design, this backtracking regex engine is bounded. This bound is implemented by not visiting any combination of NFA state ID and position in a haystack more than once.

All searches execute in linear time with respect to the size of the regular expression and search text.

def BoundedBacktracker.Array.Ref.mkRef {α β : Type} [Inhabited β] (arr : Array α) : ST.Ref β (Array α)

make reference of array

Equations

• BoundedBacktracker.Array.Ref.mkRef arr = match ST.Prim.mkRef arr default with | EStateM.Result.ok r a => r

def BoundedBacktracker.Array.Ref.getRefValue {α β : Type} [Inhabited β] (ref : ST.Ref β (Array α)) : Array α

get array of reference

Equations

• BoundedBacktracker.Array.Ref.getRefValue ref = match ST.Prim.Ref.get ref default with | EStateM.Result.ok r a => r

def BoundedBacktracker.Array.Ref.modifyRefValue {α β : Type} [Inhabited β] [DecidableEq β] (ref : ST.Ref β (Array α)) (index : Nat) (value : α) : ST.Ref β (Array α)

modify array, try to perform the update destructively

Equations

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

instance BoundedBacktracker.Array.Ref.instInhabitedRefArray_regex {α β : Type} [Inhabited β] : Inhabited (ST.Ref β (Array α))

Equations

• BoundedBacktracker.Array.Ref.instInhabitedRefArray_regex = { default := BoundedBacktracker.Array.Ref.mkRef #[] }

def BoundedBacktracker.CharPos.posInRange (s : Substring) (pos : String.Pos) : Prop

Equations

• BoundedBacktracker.CharPos.posInRange s pos = (s.startPos ≤ pos ∧ pos ≤ s.stopPos)

structure BoundedBacktracker.CharPos (s : Substring) : Type

Char position in a substring

• pos : String.Pos

  current position

• curr? : Option Char

  char at current position

• prev? : Option Char

  char at previous position

• isPosInRange : posInRange s self.pos

  pos is in range of substring s

• isValidPos : String.Pos.Valid s.str self.pos

  pos is valid string position in s.str

• isValidSubstring : s.Valid

  s is a valid substring

@[reducible, inline]

abbrev BoundedBacktracker.CharPos.PosInRange (s : Substring) : Type

Equations

• BoundedBacktracker.CharPos.PosInRange s = { pos : String.Pos // BoundedBacktracker.CharPos.posInRange s pos ∧ String.Pos.Valid s.str pos }

@[reducible, inline]

abbrev BoundedBacktracker.CharPos.Pair (s : Substring) : Type

Equations

• BoundedBacktracker.CharPos.Pair s = { p : BoundedBacktracker.CharPos.PosInRange s × BoundedBacktracker.CharPos.PosInRange s // p.fst.val ≤ p.snd.val }

instance BoundedBacktracker.instInhabitedCharPosDefaultSubstring : Inhabited (CharPos default)

Equations

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

instance BoundedBacktracker.instToStringCharPos {s : Substring} : ToString (CharPos s)

Equations

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

def BoundedBacktracker.CharPos.toSlotEntry {input : Substring} («at» : CharPos input) : PosInRange input

Equations

• «at».toSlotEntry = ⟨«at».pos, ⋯⟩

def BoundedBacktracker.CharPos.get? (s : Substring) («at» : String.Pos) : Option Char

Equations

• BoundedBacktracker.CharPos.get? s «at» = if «at» < s.stopPos then some (s.get «at») else none

def BoundedBacktracker.CharPos.create (s : Regex.ValidSubstring) («at» : Regex.ValidPos s.val.str) (h : s.val.startPos ≤ «at».val ∧ «at».val ≤ s.val.stopPos) : CharPos s.val

create a CharPos from s and position «at»

Equations

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

theorem BoundedBacktracker.CharPos.valid_prev {s : Substring} (cp : CharPos s) : String.Pos.Valid s.str (s.str.prev cp.pos)

def BoundedBacktracker.CharPos.prev {s : Substring} (cp : CharPos s) : Option (CharPos s)

to prev position of cp

Equations

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

def BoundedBacktracker.CharPos.prevn {s : Substring} (offset : Nat) (cp : CharPos s) : Option (CharPos s)

Equations

• BoundedBacktracker.CharPos.prevn offset cp = if offset ≤ cp.pos.byteIdx then BoundedBacktracker.CharPos.prevn.loop offset (some cp) else none

@[irreducible]

def BoundedBacktracker.CharPos.prevn.loop {s : Substring} (offset : Nat) (cp : Option (CharPos s)) : Option (CharPos s)

Equations

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

theorem BoundedBacktracker.CharPos.valid_next {s : Substring} (cp : CharPos s) (h : cp.pos < s.stopPos) : String.Pos.Valid s.str (s.str.next cp.pos)

def BoundedBacktracker.CharPos.next {s : Substring} (cp : CharPos s) : CharPos s

to next position of cp

Equations

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

def BoundedBacktracker.CharPos.atStart {s : Substring} (cp : CharPos s) : Bool

is CharPos at start position

Equations

• cp.atStart = decide (cp.pos = s.startPos)

def BoundedBacktracker.CharPos.atStop {s : Substring} (cp : CharPos s) : Bool

is CharPos at stop position

Equations

• cp.atStop = decide (cp.pos = s.stopPos)

inductive BoundedBacktracker.Frame (n : Nat) (s : Substring) : Type

Represents a stack frame on the heap while doing backtracking.

• Step {n : Nat} {s : Substring} (sid : Fin n) («at» : CharPos s) : Frame n s

  Look for a match starting at sid and the given position in the haystack.

• RestoreCapture {n : Nat} {s : Substring} (role : NFA.Capture.Role) (slot : Nat) (pos : Option (CharPos.PosInRange s)) : Frame n s

  Reset the given slot to the given pos (which might be None).

instance BoundedBacktracker.instToStringFrame {n : Nat} {s : Substring} : ToString (Frame n s)

Equations

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

structure BoundedBacktracker.HalfMatch : Type

A representation of "half" of a match reported by a DFA.

• pattern : NFA.PatternID

  The pattern ID.

• offset : String.Pos

  The offset of the match.

instance BoundedBacktracker.instInhabitedHalfMatch : Inhabited HalfMatch

Equations

• BoundedBacktracker.instInhabitedHalfMatch = { default := { pattern := 0, offset := 0 } }

instance BoundedBacktracker.instToStringHalfMatch : ToString HalfMatch

Equations

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

@[reducible, inline]

abbrev BoundedBacktracker.Stack (n : Nat) (s : Substring) : Type

The stack of frames

Equations

• BoundedBacktracker.Stack n s = List (BoundedBacktracker.Frame n s)

@[inline]

def BoundedBacktracker.Stack.push {n : Nat} {s : Substring} (stack : Stack n s) (v : Frame n s) : Stack n s

Push frame to stack

Equations

• stack.push v = v :: stack

@[inline]

def BoundedBacktracker.Stack.pop? {n : Nat} {s : Substring} (stack : Stack n s) : Option (Frame n s × Stack n s)

pop head frame from stack

Equations

• BoundedBacktracker.Stack.pop? [] = none
• BoundedBacktracker.Stack.pop? (head :: tail) = some (head, tail)

theorem BoundedBacktracker.Stack.pop?_some_lt {n : Nat} {s : Substring} {a : Frame n s} {s1 : Stack n s} (s✝ : Stack n s) (h : s✝.pop? = some (a, s1)) : List.length s1 < List.length s✝

@[inline]

def BoundedBacktracker.Stack.append {n : Nat} {s : Substring} (stack1 stack2 : Stack n s) : Stack n s

append stacks

Equations

• stack1.append [v1, v2] = v2 :: v1 :: stack1
• stack1.append stack2 = (List.reverse stack2).append stack1

@[inline]

def BoundedBacktracker.Stack.toStack {n : Nat} {s : Substring} (arr : Array (Frame n s)) : Stack n s

Equations

• BoundedBacktracker.Stack.toStack arr = arr.toList

instance BoundedBacktracker.instInhabitedStackDefaultNatSubstring : Inhabited (Stack default default)

Equations

• BoundedBacktracker.instInhabitedStackDefaultNatSubstring = { default := [] }

@[reducible, inline]

abbrev BoundedBacktracker.Visited : Type

The encoded set of (Fin n, HaystackOffset) pairs that have been visited by the backtracker within a single search. Optimization: encode as bits

Equations

• BoundedBacktracker.Visited = Array UInt8

@[reducible, inline]

abbrev BoundedBacktracker.SlotEntry (s : Substring) : Type

SlotEntry consists of slot, group and char pos in s

Equations

• BoundedBacktracker.SlotEntry s = (Nat × Nat × Option (BoundedBacktracker.CharPos.PosInRange s))

def BoundedBacktracker.SearchState.Slots.Valid {s : Substring} (slots : Array (SlotEntry s)) : Bool

Equations

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

@[reducible, inline]

abbrev BoundedBacktracker.SlotsValid (s : Substring) : Type

Equations

• BoundedBacktracker.SlotsValid s = { slots : Array (BoundedBacktracker.SlotEntry s) // BoundedBacktracker.SearchState.Slots.Valid slots = true }

structure BoundedBacktracker.SearchState (n : Nat) (input : Substring) : Type

State of the backtracking search

• stack : Stack n input

  Stack used on the heap for doing backtracking

• visited : ST.Ref Nat Visited

  The encoded set of (Fin n, HaystackOffset) pairs that have been visited by the backtracker within a single search.

• countVisited : Nat

  count of pairs that have been visited

• sid : Fin n

  current state

• at : CharPos input

  position in input string

• slots : Array (SlotEntry input)

  slots, positions of captures in input

• slotsValid : Slots.Valid self.slots = true

  slots are valid

• recentCaptures : Array (Option (String.Pos × String.Pos))

  recent captures of capture groups

• logEnabled : Bool

  is logging enabled

• msgs : Array String

  log msgs

• halfMatch : Option HalfMatch

  HalfMatch

• backtracks : Nat

  count of backtracks

theorem BoundedBacktracker.SearchState.ext {n : Nat} {input : Substring} {x y : SearchState n input} (stack : x.stack = y.stack) (visited : x.visited = y.visited) (countVisited : x.countVisited = y.countVisited) (sid : x.sid = y.sid) («at» : x.at = y.at) (slots : x.slots = y.slots) (recentCaptures : x.recentCaptures = y.recentCaptures) (logEnabled : x.logEnabled = y.logEnabled) (msgs : x.msgs = y.msgs) (halfMatch : x.halfMatch = y.halfMatch) (backtracks : x.backtracks = y.backtracks) : x = y

def BoundedBacktracker.SearchState.fromNfa (nfa : NFA.Checked.NFA) (input : Regex.ValidSubstring) («at» : Regex.ValidPos input.val.str) (logEnabled : Bool) (h : 0 < nfa.n ∧ input.val.startPos ≤ «at».val ∧ «at».val ≤ input.val.stopPos) : SearchState nfa.n input.val

create the SearchState from an NFA

Equations

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

theorem BoundedBacktracker.SearchState.slots_valid_elem_eq_pair {s : Substring} (slots : Array (SlotEntry s)) (h : Slots.Valid slots = true) (i : Fin slots.toList.length) : slots.toList[i].fst = ↑i ∧ slots.toList[i].snd.fst = (↑i).div 2

theorem BoundedBacktracker.SearchState.slots_valid_elem_eq {s : Substring} (slots : Array (SlotEntry s)) (h : Slots.Valid slots = true) (i : Fin slots.toList.length) : ∃ (v : Option (CharPos.PosInRange s)), slots.toList[i] = (↑i, (↑i).div 2, v)

theorem BoundedBacktracker.SearchState.slots_of_modify_valid {s : Substring} (slots : Array (SlotEntry s)) (h : Slots.Valid slots = true) (slot : Nat) (f : Option (CharPos.PosInRange s) → Option (CharPos.PosInRange s)) : Slots.Valid (slots.modify slot (Prod.map id (Prod.map id f))) = true

theorem BoundedBacktracker.SearchState.slots_of_map_valid {s : Substring} (slots : Array (SlotEntry s)) (h : Slots.Valid slots = true) (f : SlotEntry s → SlotEntry s) (hf : ∀ (x : SlotEntry s), (f x).fst = x.fst ∧ (f x).snd.fst = x.snd.fst) : Slots.Valid (Array.map f slots) = true

instance BoundedBacktracker.instNonemptyVisited : Nonempty Visited

def BoundedBacktracker.Visited.index {n : Nat} {s : Substring} (sid : Fin n) (cp : CharPos s) : Nat

get encoded index of Fin n and CharPos in visited array

Equations

• BoundedBacktracker.Visited.index sid cp = ↑sid * (s.stopPos.byteIdx - s.startPos.byteIdx + 1) + cp.pos.byteIdx - s.startPos.byteIdx

theorem BoundedBacktracker.Visited.eq_of_linear_eq {a1 b1 a2 b2 x : Nat} (hb1 : b1 < x) (hb2 : b2 < x) (h : a1 * x + b1 = a2 * x + b2) : a1 = a2 ∧ b1 = b2

theorem BoundedBacktracker.Visited.index_injective {n : Nat} {s : Substring} (sid1 sid2 : Fin n) (cp1 cp2 : CharPos s) (heq : index sid1 cp1 = index sid2 cp2) : ↑sid1 = ↑sid2 ∧ cp1.pos.byteIdx = cp2.pos.byteIdx

index is injective.

def BoundedBacktracker.Visited.checkVisited {n : Nat} {s : Substring} (state : SearchState n s) : Bool × SearchState n s

Check if current Fin n and CharPos in SearchState is already visited. If not visited mark pair as visited.

Equations

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

def BoundedBacktracker.Visited.checkVisited' {n : Nat} {s : Substring} (state : SearchState n s) : Bool × SearchState n s

Check if current Fin n and CharPos in SearchState is already visited. If not visited mark pair as visited.

Equations

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

theorem BoundedBacktracker.Visited.checkVisited'_false_lt {n : Nat} {input : Substring} {s1 : SearchState n input} (s : SearchState n input) (h : checkVisited' s = (false, s1)) : s.countVisited < s1.countVisited

theorem BoundedBacktracker.Visited.checkVisited'_true_eq {n : Nat} {input : Substring} {s1 : SearchState n input} (s : SearchState n input) (h : checkVisited' s = (true, s1)) : s.countVisited = s1.countVisited ∧ List.length s.stack = List.length s1.stack

theorem BoundedBacktracker.capture_groups_eq_of_consecutive_slots {s : Substring} {i s0 g0 : Nat} {v0 : CharPos.PosInRange s} {s1 g1 : Nat} {v1 : CharPos.PosInRange s} (slots : Array (SlotEntry s)) (valid : SearchState.Slots.Valid slots = true) (h : ¬i % 2 = 0) (h0 : slots.get? (i - 1) = some (s0, g0, some v0)) (h1 : slots.get? i = some (s1, g1, some v1)) : g0 = g1

capture groups of consecutive slots are equal

theorem BoundedBacktracker.withMsg_eq {input : Substring} {nfa : NFA.Checked.NFA} {s s1 : SearchState nfa.n input} {msg : Unit → String} (h : BoundedBacktracker.withMsg✝ msg s = s1) : s.countVisited = s1.countVisited ∧ s.stack = s1.stack

theorem BoundedBacktracker.step_match_countVisited_eq {n : Nat} {s : Substring} {p : NFA.PatternID} (s1 s2 : SearchState n s) (h : BoundedBacktracker.step_match✝ p s1 = s2) : s1.countVisited = s2.countVisited

theorem BoundedBacktracker.toNextStep_countVisited_eq {s : Substring} (nfa : NFA.Checked.NFA) (state : NFA.Checked.State nfa.n) (s1 s2 : SearchState nfa.n s) (h : BoundedBacktracker.toNextStep✝ nfa state s1 = s2) : s1.countVisited = s2.countVisited

theorem BoundedBacktracker.toNextStep_eq {input : Substring} {nfa : NFA.Checked.NFA} {state : NFA.Checked.State nfa.n} {s s1 : SearchState nfa.n input} {msg : Unit → String} (h : BoundedBacktracker.toNextStep✝ nfa state (BoundedBacktracker.withMsg✝ msg s) = s1) : s.countVisited = s1.countVisited

theorem BoundedBacktracker.toNextStepChecked_true_lt {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h : BoundedBacktracker.toNextStepChecked✝ nfa s = (true, s1)) : s.countVisited < s1.countVisited

theorem BoundedBacktracker.toNextStepChecked_false_eq {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h : BoundedBacktracker.toNextStepChecked✝ nfa s = (false, s1)) : s.countVisited = s1.countVisited ∧ s.stack = s1.stack

def BoundedBacktracker.steps {s : Substring} (nfa : NFA.Checked.NFA) (state : SearchState nfa.n s) : SearchState nfa.n s

execute next steps in NFA.

Equations

• BoundedBacktracker.steps nfa state = match BoundedBacktracker.toNextStepChecked✝ nfa state with | (true, state) => BoundedBacktracker.steps.loop nfa state | (false, state) => state

@[irreducible]

def BoundedBacktracker.steps.loop {s : Substring} (nfa : NFA.Checked.NFA) (state : SearchState nfa.n s) : SearchState nfa.n s

Equations

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

@[irreducible]

theorem BoundedBacktracker.steps_loop_le {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h : steps.loop nfa s = s1) : s.countVisited ≤ s1.countVisited

theorem BoundedBacktracker.steps_lt_or_eq_lt {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h : steps nfa s = s1) : s.countVisited < s1.countVisited ∨ s.countVisited = s1.countVisited ∧ List.length s.stack = List.length s1.stack

theorem BoundedBacktracker.toNextFrameStep_true_lt_or_eq_lt {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h : BoundedBacktracker.toNextFrameStep✝ nfa s = (true, s1)) : s.countVisited < s1.countVisited ∨ s.countVisited = s1.countVisited ∧ List.length s.stack = List.length s1.stack

theorem BoundedBacktracker.toNextFrameRestoreCapture_true_lt_or_eq_lt {s : Substring} {n : Nat} {s1 : SearchState n s} (slot : Nat) (offset : Option (CharPos.PosInRange s)) (stack : Stack n s) (s✝ : SearchState n s) (h : BoundedBacktracker.toNextFrameRestoreCapture✝ slot offset stack s✝ = (true, s1)) : s✝.countVisited = s1.countVisited ∧ stack = s1.stack

theorem BoundedBacktracker.toNextFrame_true_lt {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h : BoundedBacktracker.toNextFrame✝ nfa s = (true, s1)) : s.countVisited < s1.countVisited ∨ s.countVisited = s1.countVisited ∧ List.length s1.stack < List.length s.stack

theorem BoundedBacktracker.searchState_lexLt {input : Substring} (nfa : NFA.Checked.NFA) (s s1 : SearchState nfa.n input) (h1 : s.countVisited < BoundedBacktracker.visitedSize✝ s) (h2 : BoundedBacktracker.visitedSize✝ s = BoundedBacktracker.visitedSize✝ s1) (h : BoundedBacktracker.toNextFrame✝ nfa s = (true, s1)) : BoundedBacktracker.unvisited✝ s1 < BoundedBacktracker.unvisited✝ s ∨ BoundedBacktracker.unvisited✝ s1 = BoundedBacktracker.unvisited✝ s ∧ List.length s1.stack < List.length s.stack

def BoundedBacktracker.backtrack {s : Substring} (nfa : NFA.Checked.NFA) (state : SearchState nfa.n s) : SearchState nfa.n s

BoundedBacktrack search

Equations

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

@[irreducible]

def BoundedBacktracker.backtrack.loop {s : Substring} (nfa : NFA.Checked.NFA) (state : SearchState nfa.n s) : SearchState nfa.n s

Equations

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

def BoundedBacktracker.matches (s : Regex.ValidSubstring) («at» : Regex.ValidPos s.val.str) (nfa : NFA.Checked.NFA) (logEnabled : Bool) : Array String × Array (Option { m : Regex.ValidSubstring // m.val.str = s.val.str })

Search for the first match of this regex in the haystack given and return log msgs and the matches of each capture group.

Equations

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