Skip to content

Engine: add lookarounds to bool_tree #31

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
shilangyu wants to merge 5 commits into
base: mw/reverse-pikevm
Choose a base branch
from
Draft

Engine: add lookarounds to bool_tree #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
be403bb
Engine: add backward direction for PikeVM
shilangyu Mar 17, 2026
f2cf328
Engine: prove complexity for both directions of PikeVM
shilangyu Mar 17, 2026
c96617d
Engine: add direction to bool_tree
shilangyu Mar 18, 2026
634539d
Engine: add lookarounds to bool_tree
shilangyu Mar 23, 2026
e91d625
Semantics: move some list lemmas to ListLemmas
shilangyu May 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
330 changes: 202 additions & 128 deletions Engine/BooleanSemantics.v
View file
Open in desktop

Large diffs are not rendered by default.

430 changes: 225 additions & 205 deletions Engine/Complexity.v
View file
Open in desktop

Large diffs are not rendered by default.

30 changes: 15 additions & 15 deletions Engine/Correctness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,14 +43,14 @@ Section Correctness.
Context (rer: RegExpRecord).

Definition trc_pike_tree := @trc pike_tree_state pike_tree_step.
Definition trc_pike_vm (c:code) := @trc pike_vm_state (pike_vm_step rer c).
Definition trc_pike_vm (c:code) (dir:Direction) := @trc pike_vm_state (pike_vm_step rer c dir).

(* The Pike invariant is preserved through the TRC *)
Lemma vm_to_tree:
forall svm1 st1 svm2 code
(STWF: stutter_wf rer code)
(INVARIANT: pike_inv rer code st1 svm1)
(TRCVM: trc_pike_vm code svm1 svm2),
(TRCVM: trc_pike_vm code forward svm1 svm2),
exists st2, trc_pike_tree st1 st2 /\ pike_inv rer code st2 svm2.
Proof.
intros svm1 st1 svm2 code STWF INVARIANT TRCVM.
Expand All @@ -68,8 +68,8 @@ Qed.
Theorem pike_vm_to_pike_tree:
forall r inp tree result,
pike_regex r ->
bool_tree rer [Areg r] inp CanExit tree ->
trc_pike_vm (compilation r) (pike_vm_initial_state inp) (PVS_final result) ->
bool_tree rer [Areg r] inp CanExit forward tree ->
trc_pike_vm (compilation r) forward (pike_vm_initial_state inp) (PVS_final result) ->
trc_pike_tree (pike_tree_initial_state tree inp) (PTS_final result).
Proof.
intros r inp tree result SUBSET TREE TRCVM.
Expand All @@ -82,8 +82,8 @@ Qed.
Theorem pike_vm_to_pike_tree_unanchored {strs:StrSearch}:
forall r inp tree result future_tree,
pike_regex r ->
bool_tree rer [Areg r] inp CanExit tree ->
trc_pike_vm (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp) (PVS_final result) ->
bool_tree rer [Areg r] inp CanExit forward tree ->
trc_pike_vm (compilation r) forward (pike_vm_initial_state_unanchored (extract_literal rer r) inp forward) (PVS_final result) ->
future_tree_shape rer r inp future_tree ->
exists future, may_erase future_tree future /\
trc_pike_tree (pike_tree_initial_state_unanchored tree future inp) (PTS_final result).
Expand Down Expand Up @@ -117,7 +117,7 @@ Theorem pike_vm_correct:
(* `tree` is the tree of the regex `r` for the input `inp` *)
is_tree rer [Areg r] inp GroupMap.empty forward tree ->
(* the result of the PikeVM is `result` *)
trc_pike_vm (compilation r) (pike_vm_initial_state inp) (PVS_final result) ->
trc_pike_vm (compilation r) forward (pike_vm_initial_state inp) (PVS_final result) ->
(* This `result` is the priority result of the `tree` *)
result = first_leaf tree inp.
Proof.
Expand All @@ -139,7 +139,7 @@ Theorem pike_vm_correct_unanchored {strs:StrSearch}:
(* `tree` is the tree of the regex `[^]*?r` for the input `inp` *)
is_tree rer [Areg (lazy_prefix r)] inp GroupMap.empty forward tree ->
(* the result of the PikeVM is `result` *)
trc_pike_vm (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp) (PVS_final result) ->
trc_pike_vm (compilation r) forward (pike_vm_initial_state_unanchored (extract_literal rer r) inp forward) (PVS_final result) ->
(* This `result` is the priority result of the `tree` *)
result = first_leaf tree inp.
Proof.
Expand All @@ -161,7 +161,7 @@ Theorem pike_vm_same_warblre:
RegExpRecord.capturingGroupsCount rer = StaticSemantics.countLeftCapturingParensWithin wr nil ->
EarlyErrors.Pass_Regex wr nil ->
forall result,
trc_pike_vm (compilation lr) (pike_vm_initial_state inp) (PVS_final result) ->
trc_pike_vm (compilation lr) forward (pike_vm_initial_state inp) (PVS_final result) ->
EquivDef.equiv_res result ((EquivMain.compilePattern wr rer) (input_str inp) (idx inp)).
Proof.
intros lr wr inp Hpike Hequiv Hcapcount HearlyErrors.
Expand All @@ -183,7 +183,7 @@ Theorem pike_vm_same_warblre_str0:
RegExpRecord.capturingGroupsCount rer = StaticSemantics.countLeftCapturingParensWithin wr nil ->
EarlyErrors.Pass_Regex wr nil ->
forall result,
trc_pike_vm (compilation lr) (pike_vm_initial_state (init_input str0)) (PVS_final result) ->
trc_pike_vm (compilation lr) forward (pike_vm_initial_state (init_input str0)) (PVS_final result) ->
EquivDef.equiv_res result ((EquivMain.compilePattern wr rer) str0 0).
Proof.
intros lr wr str0 Hpike Hequiv Hcapcount HearlyErrors.
Expand All @@ -203,7 +203,7 @@ Theorem pike_vm_warblre:
(* such that it is in the supported PikeVM subset *)
pike_regex r ->
(* When PikeVM reaches a final result *)
trc_pike_vm (compilation r) (pike_vm_initial_state inp) (PVS_final result) ->
trc_pike_vm (compilation r) forward (pike_vm_initial_state inp) (PVS_final result) ->
(* this result is equal to Warblre's execution result *)
(compilePattern rw rer) (input_str inp) (idx inp) = to_MatchState result (RegExpRecord.capturingGroupsCount rer).
Proof.
Expand Down Expand Up @@ -254,7 +254,7 @@ Qed.
Theorem memobt_to_memotree:
forall r inp tree result initms finalms initts,
pike_regex r ->
bool_tree rer [Areg r] inp CanExit tree ->
bool_tree rer [Areg r] inp CanExit forward tree ->
seen_inclusion rer (compilation r) initts initms None None ->
trc_memo_bt (compilation r) (MemoBT.initial_state inp initms) (MBT_final result finalms) ->
exists finalts, trc_memo_tree (initial_tree_state tree inp initts) (MTree_final result finalts) /\
Expand All @@ -264,14 +264,14 @@ Proof.
generalize (initial_memo_inv_inclusion rer r inp tree (compilation r) initts initms TREE (@eq_refl _ _) SUBSET INCL).
intros INIT.
eapply memobt_to_tree in TRCBT as [btfinal [TRCTREE INV]]; eauto.
- inversion INV. subst. eauto.
- inversion INV. subst. eauto.
- eapply compilation_stutter_wf; eauto.
Qed.

Theorem memobt_to_memotree_init:
forall r inp tree result finalms,
pike_regex r ->
bool_tree rer [Areg r] inp CanExit tree ->
bool_tree rer [Areg r] inp CanExit forward tree ->
trc_memo_bt (compilation r) (MemoBT.initial_state inp initial_memoset) (MBT_final result finalms) ->
exists finalts, trc_memo_tree (initial_tree_state tree inp initial_seentrees) (MTree_final result finalts) /\
(result = None -> seen_inclusion rer (compilation r) finalts finalms None None).
Expand Down Expand Up @@ -328,7 +328,7 @@ Theorem memobt_correct:
/\ (result = None -> correctms finalms (compilation r)).
Proof.
intros r inp tree result initms finalms SUBSET CORRECT TREE TRC.
destruct CORRECT as [initts [INCL NOLEAF]].
destruct CORRECT as [initts [INCL NOLEAF]].
eapply encode_equal with (b:=CanExit) in TREE as BOOLTREE; try solve[pike_subset].
eapply memobt_to_memotree in TRC as [ts [TRC CORRECT]]; eauto.
assert (SUBTREE: pike_subtree tree).
Expand Down
Loading