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} {β : Type} [Inhabited β] (arr : Array α) : ST.Ref β (Array α)

make reference of array

Equations

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

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

get array of reference

Equations

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

def BoundedBacktracker.Array.Ref.modifyRefValue {α : Type} {β : 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} {β : Type} [Inhabited β] : Inhabited (ST.Ref β (Array α))

Equations

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

structure BoundedBacktracker.CharPos : Type

Char position in a substring

• s : Substring

  substring

• pos : String.Pos

  current position

• curr? : Option Char

  char at current position

• prev? : Option Char

  char at previous position

instance BoundedBacktracker.instInhabitedCharPos : Inhabited BoundedBacktracker.CharPos

Equations

• BoundedBacktracker.instInhabitedCharPos = { default := { s := default, pos := default, curr? := none, prev? := none } }

instance BoundedBacktracker.instToStringCharPos : ToString BoundedBacktracker.CharPos

Equations

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

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 : Substring) (at : String.Pos) : BoundedBacktracker.CharPos

create a CharPos from s and position «at»

Equations

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

def BoundedBacktracker.CharPos.prevOf (offset : Nat) (cp : BoundedBacktracker.CharPos) : Option BoundedBacktracker.CharPos

Equations

• BoundedBacktracker.CharPos.prevOf offset cp = if offset ≤ cp.pos.byteIdx then let pos := cp.s.prevn offset cp.pos; some (BoundedBacktracker.CharPos.create cp.s pos) else none

def BoundedBacktracker.CharPos.next (cp : BoundedBacktracker.CharPos) : BoundedBacktracker.CharPos

to next position CharPos of cp

Equations

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

def BoundedBacktracker.CharPos.atStart (cp : BoundedBacktracker.CharPos) : Bool

is CharPos at start position

Equations

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

def BoundedBacktracker.CharPos.atStop (cp : BoundedBacktracker.CharPos) : Bool

is CharPos at stop position

Equations

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

inductive BoundedBacktracker.Frame (n : Nat) : Type

Represents a stack frame on the heap while doing backtracking.

• Step: {n : Nat} → Fin n → BoundedBacktracker.CharPos → BoundedBacktracker.Frame n

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

• RestoreCapture: {n : Nat} → NFA.Capture.Role → Nat → Nat × Nat × Option String.Pos → BoundedBacktracker.Frame n

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

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

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 BoundedBacktracker.HalfMatch

Equations

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

instance BoundedBacktracker.instToStringHalfMatch : ToString BoundedBacktracker.HalfMatch

Equations

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

@[reducible, inline]

abbrev BoundedBacktracker.Stack (n : Nat) : Type

The stack of frames

Equations

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

@[inline]

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

Push frame to stack

Equations

• stack.push v = v :: stack

@[inline]

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

pop head frame from stack

Equations

• stack.pop? = match stack with | [] => none | head :: tail => some (head, tail)

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

@[inline]

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

append stacks

Equations

• stack1.append stack2 = match stack2 with | [v1, v2] => v2 :: v1 :: stack1 | x => (List.reverse stack2).append stack1

@[inline]

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

Equations

• BoundedBacktracker.Stack.toStack arr = arr.toList

instance BoundedBacktracker.instInhabitedStackOfNatNat : Inhabited (BoundedBacktracker.Stack 0)

Equations

• BoundedBacktracker.instInhabitedStackOfNatNat = { 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

theorem BoundedBacktracker.SearchState.ext_iff {n : Nat} {x : BoundedBacktracker.SearchState n} {y : BoundedBacktracker.SearchState n} : x = y ↔ x.stack = y.stack ∧ x.visited = y.visited ∧ x.countVisited = y.countVisited ∧ x.sid = y.sid ∧ x.input = y.input ∧ x.at = y.at ∧ x.slots = y.slots ∧ x.recentCaptures = y.recentCaptures ∧ x.logEnabled = y.logEnabled ∧ x.msgs = y.msgs ∧ x.halfMatch = y.halfMatch ∧ x.backtracks = y.backtracks

theorem BoundedBacktracker.SearchState.ext {n : Nat} {x : BoundedBacktracker.SearchState n} {y : BoundedBacktracker.SearchState n} (stack : x.stack = y.stack) (visited : x.visited = y.visited) (countVisited : x.countVisited = y.countVisited) (sid : x.sid = y.sid) (input : x.input = y.input) (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

structure BoundedBacktracker.SearchState (n : Nat) : Type

State of the backtracking search

• stack : BoundedBacktracker.Stack n

  Stack used on the heap for doing backtracking

• visited : ST.Ref Nat BoundedBacktracker.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

• input : Substring

  input string

• at : BoundedBacktracker.CharPos

  position in input string

• slots : Array (Nat × Nat × Option String.Pos)

  slots, positions of captures in haystack

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

  recent captures of capture groups

• logEnabled : Bool

  is logging enabled

• msgs : Array String

  log msgs

• halfMatch : Option BoundedBacktracker.HalfMatch

  HalfMatch

• backtracks : Nat

  count of backtracks

def BoundedBacktracker.SearchState.fromNfa (nfa : NFA.Checked.NFA) (input : Substring) (at : String.Pos) (logEnabled : Bool) (h : 0 < nfa.n) : BoundedBacktracker.SearchState nfa.n

create the SearchState from an NFA

Equations

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

instance BoundedBacktracker.instNonemptyVisited : Nonempty BoundedBacktracker.Visited

Equations

• BoundedBacktracker.instNonemptyVisited = ⋯

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

get encoded index of Fin n an CharPos in visited array

Equations

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

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

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} (state : BoundedBacktracker.SearchState n) : Bool × BoundedBacktracker.SearchState n

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} {s1 : BoundedBacktracker.SearchState n} (s : BoundedBacktracker.SearchState n) (h : BoundedBacktracker.Visited.checkVisited' s = (false, s1)) : s.countVisited < s1.countVisited

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

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

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

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

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

def BoundedBacktracker.steps (nfa : NFA.Checked.NFA) (state : BoundedBacktracker.SearchState nfa.n) : BoundedBacktracker.SearchState nfa.n

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 (nfa : NFA.Checked.NFA) (state : BoundedBacktracker.SearchState nfa.n) : BoundedBacktracker.SearchState nfa.n

Equations

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

@[irreducible]

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

theorem BoundedBacktracker.steps_lt_or_eq_lt (nfa : NFA.Checked.NFA) (s : BoundedBacktracker.SearchState nfa.n) (s1 : BoundedBacktracker.SearchState nfa.n) (h : BoundedBacktracker.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 (nfa : NFA.Checked.NFA) (s : BoundedBacktracker.SearchState nfa.n) (s1 : BoundedBacktracker.SearchState nfa.n) (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 {n : Nat} {s1 : BoundedBacktracker.SearchState n} (slot : Nat) (offset : Nat × Nat × Option String.Pos) (stack : BoundedBacktracker.Stack n) (s : BoundedBacktracker.SearchState n) (h : BoundedBacktracker.toNextFrameRestoreCapture slot offset stack s = (true, s1)) : s.countVisited = s1.countVisited ∧ stack = s1.stack

theorem BoundedBacktracker.toNextFrame_true_lt (nfa : NFA.Checked.NFA) (s : BoundedBacktracker.SearchState nfa.n) (s1 : BoundedBacktracker.SearchState nfa.n) (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 (nfa : NFA.Checked.NFA) (s : BoundedBacktracker.SearchState nfa.n) (s1 : BoundedBacktracker.SearchState nfa.n) (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 (nfa : NFA.Checked.NFA) (state : BoundedBacktracker.SearchState nfa.n) : BoundedBacktracker.SearchState nfa.n

BoundedBacktrack search

Equations

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

@[irreducible]

def BoundedBacktracker.backtrack.loop (nfa : NFA.Checked.NFA) (state : BoundedBacktracker.SearchState nfa.n) : BoundedBacktracker.SearchState nfa.n

Equations

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

def BoundedBacktracker.slots (s : Substring) (at : String.Pos) (nfa : NFA.Checked.NFA) (logEnabled : Bool) : Array String × Array (Option (String.Pos × String.Pos))

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

Equations

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