From a12194c1066684168bebb70680f4168e1c8f9465 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 17 Mar 2026 19:35:54 +0100 Subject: [PATCH 1/3] Engine: add backward direction for PikeVM --- Engine/Complexity.v | 290 +++++++++++++++++++---------------- Engine/Correctness.v | 22 +-- Engine/FunctionalPikeVM.v | 147 +++++++++++------- Engine/Meta/EngineSpec.v | 8 +- Engine/PikeEquiv.v | 58 +++---- Engine/PikeVM.v | 314 ++++++++++++++++++++++++++++++-------- Semantics/Chars.v | 7 + 7 files changed, 556 insertions(+), 290 deletions(-) diff --git a/Engine/Complexity.v b/Engine/Complexity.v index accf2515..0a4db20b 100644 --- a/Engine/Complexity.v +++ b/Engine/Complexity.v @@ -22,12 +22,12 @@ Section CodeWF. Context (rer: RegExpRecord). Definition size (c:code) : nat := length c. - + (** * Well-formedness of the code *) - + (* first, we show the code is non empty, ensuring that threads generated by prefix acceleration are in range *) Definition nonempty (c:code) : Prop := size c > 0. - + (* Even if the regex is epsilon, adding the accept instruction makes the code non-empty *) Lemma compilation_nonempty: forall r, nonempty (compilation r). @@ -35,14 +35,14 @@ Section CodeWF. intros. unfold compilation. destruct compile. unfold nonempty, size. rewrite length_app. simpl. lia. Qed. - + (* Some bytecode is well-formed if every target label belongs in some range *) Definition code_wf (c:code) (size:nat) := forall pc i next, get_pc c pc = Some i -> In next (next_pcs pc i) -> next < size. - + Lemma nfa_wf: forall r c startl endl pc next i, nfa_rep r c startl endl -> @@ -138,7 +138,7 @@ Section CodeWF. rewrite KILL in GET. inversion GET. subst. simpl in IN. inversion IN. Qed. - + Theorem compiled_wf: forall r, code_wf (compilation r) (size (compilation r)). Proof. @@ -163,39 +163,39 @@ Section CodeWF. specialize (nfa_wf r c 0 (length c) pc next i REP POS H1 GETI IN) as WF. unfold size. rewrite length_app. simpl. lia. Qed. - + Lemma eps_step_blocked_wf: - forall t code inp newt, - epsilon_step rer t code inp = EpsBlocked newt -> + forall t code dir inp newt, + epsilon_step rer t code dir inp = EpsBlocked newt -> exists i, get_pc code (fst (fst t)) = Some i /\ In (fst (fst newt)) (next_pcs (fst (fst t)) i). Proof. - unfold epsilon_step. intros [[pc gm]b] code inp newt H. + unfold epsilon_step. intros [[pc gm]b] code dir inp newt H. destruct (get_pc code pc) eqn:GET; [|inversion H]. destruct b0; inversion H; subst. - - destruct (check_read rer c inp forward); inversion H1; subst. + - destruct (check_read rer c inp dir); inversion H1; subst. simpl; eexists; split; eauto; simpl; auto; lia. - - destruct (anchor_satisfied rer a inp); inversion H1; subst. + - destruct dir, anchor_satisfied; inversion H1; subst. - destruct b; inversion H1. Qed. - + Lemma eps_step_active_wf: - forall t code inp next newt, - epsilon_step rer t code inp = EpsActive next -> + forall t code dir inp next newt, + epsilon_step rer t code dir inp = EpsActive next -> In newt next -> exists i, get_pc code (fst (fst t)) = Some i /\ In (fst (fst newt)) (next_pcs (fst (fst t)) i). Proof. - unfold epsilon_step. intros [[pc gm] b] code inp next newt H IN. + unfold epsilon_step. intros [[pc gm] b] code dir inp next newt H IN. destruct (get_pc code pc) eqn:GET. 2: { inversion H. subst. inversion IN. } destruct b0; inversion H; subst; try solve[inversion IN; subst; try solve [inversion H0]; simpl; eexists; split; eauto; simpl; auto; lia]. - - destruct (check_read rer c inp forward); inversion H1; subst; + - destruct (check_read rer c inp dir); inversion H1; subst; inversion IN; subst; try solve [inversion H0]; simpl; eexists; split; eauto; simpl; auto; lia. - - destruct (anchor_satisfied rer a inp); inversion H1; subst; + - destruct dir, anchor_satisfied; inversion H1; subst; inversion IN; subst; try solve [inversion H0]; simpl; eexists; split; eauto; simpl; auto; lia. - inversion IN; [|inversion H0]; subst; try solve [inversion H1]; @@ -229,7 +229,7 @@ Section CodeWF. - destruct b; subst; inversion H1; subst; inversion IN; subst; try solve [inversion H0]; simpl; eexists; split; eauto; simpl; auto; lia. - Qed. + Qed. End CodeWF. @@ -237,12 +237,12 @@ End CodeWF. Section CodeSize. Context {params: LindenParameters}. - + (** * Code Size *) - + (* Here we prove that the size of the NFA bytecode is linear in the size of the regex *) (* Note that this "size of the regex" counts counted quantifier as being unfolded, so it might not be linear in the size of the textual representation of the regex *) - + (* the exact size of the bytecode *) Fixpoint compsize (r:regex) : nat := match r with @@ -257,9 +257,9 @@ Section CodeSize. | Anchor _ => 1 | _ => 0 end. - + Definition codesize (r:regex) := S (compsize r). - + Lemma compile_size: forall r start endl code, pike_regex r -> @@ -291,7 +291,7 @@ Section CodeSize. erewrite <- IHr; eauto. 2: pike_subset. inversion COMP. subst. simpl. rewrite length_app. simpl. lia. Qed. - + Theorem compilation_size: forall r, pike_regex r -> @@ -300,7 +300,7 @@ Section CodeSize. unfold codesize, size, compilation. intros r H. destruct (compile r 0) eqn:COMP. apply compile_size in COMP; auto. rewrite <- COMP. rewrite length_app. simpl. lia. Qed. - + (* relating this compilation size to the size of the regex *) Theorem compsize_regex_size: forall (r:regex), @@ -312,7 +312,7 @@ Section CodeSize. destruct n; simpl; [lia|]. destruct n; simpl; lia. Qed. - + Corollary comp_size_regex_size: forall r, pike_regex r -> size (compilation r) <= 4 * (regex_size r). @@ -327,13 +327,13 @@ End CodeSize. Section SearchRange. Context {params: LindenParameters}. - + (* we add 1 because we consider that even at the last position, there is work to do to reach the final state *) Definition inpsize (i:input) : nat := match i with | Input next pref => 1 + length next end. - + Lemma inpsize_strict: forall i, inpsize i > 0. Proof. @@ -347,12 +347,12 @@ Section SearchRange. Proof. intros [n1 p1] [n2 p2] H. simpl in H. destruct n1 as [|h1 n1]; inversion H; subst. simpl. lia. Qed. - + (** * Next prefix search is in range *) - + Theorem search_in_range: forall inp lit n lit' (strs:StrSearch) strs', - @next_prefix_counter _ strs inp lit = Some (n, lit', strs') -> + @next_prefix_counter _ strs inp forward lit = Some (n, lit', strs') -> inpsize inp > S n. Proof. intros [next pref] lit n lit' strs strs' H. unfold next_prefix_counter in H. @@ -360,7 +360,7 @@ Section SearchRange. destruct str_search eqn:SEARCH; inversion H; subst. apply str_search_bound in SEARCH. simpl. lia. Qed. - + Lemma advance_inpsize: forall inp1 inp2 n, advance_input inp1 forward = Some inp2 -> @@ -371,7 +371,7 @@ Section SearchRange. destruct next1; inversion H. simpl in H0. simpl. lia. Qed. - + Lemma advance_S_n: forall n next pref c, advance_input_n (Input (c::next) pref) (S n) forward = @@ -379,7 +379,7 @@ Section SearchRange. Proof. intros n next pref c. simpl. f_equal. rewrite <- app_assoc. auto. Qed. - + Lemma advance_n_inpsize: forall inp n, inpsize inp > S n -> @@ -394,7 +394,7 @@ Section SearchRange. specialize (IHn (c::pref) next H0). rewrite advance_S_n. simpl in IHn. simpl. lia. Qed. - + End SearchRange. Section CountedTRC. @@ -408,14 +408,14 @@ Section CountedTRC. (STEP: R x y) (TRC: steps R y n z), steps R x (S n) z. - + Lemma steps_trc: forall A (R:A->A->Prop) (x y:A) n, steps R x n y -> @trc _ R x y. Proof. intros A R x y n H. induction H; econstructor; eauto. Qed. - + Lemma trc_steps: forall A (R:A->A->Prop) (x y:A), @trc _ R x y -> exists n, steps R x n y. @@ -424,7 +424,7 @@ Section CountedTRC. try eapply steps_refl with (n:=0); (* avoiding the shelved goal *) econstructor; eauto. Qed. - + Lemma more_steps: forall A (R:A->A->Prop) x y n m, n <= m -> @@ -437,7 +437,7 @@ Section CountedTRC. - destruct m as [|m]; try lia. econstructor; eauto. apply IHSTEPS. lia. Qed. - + Lemma strong_ind (P : nat -> Prop) : (forall m, (forall k : nat, k < m -> P k) -> P m) -> forall n, P n. @@ -447,17 +447,17 @@ Section CountedTRC. - induction n; intros; apply H; intros; try lia. apply IHn; lia. Qed. - + End CountedTRC. Section PikeVMComplexity. Context {params: LindenParameters}. Context (rer: RegExpRecord). Context {VMS: VMSeen}. - + (** * Free slots *) (* To define the measure, we need a notion of free slots: how many more states can the PikeVM visit *) - + (* well-formedness of a seen set: it was obtained by applying add to the initial seen set *) (* each element that was added is smaller than some `size` constant (size of the bytecode) *) (* and `dist` is the no-duplicate list of distinct elements *) @@ -476,7 +476,7 @@ Section PikeVMComplexity. (SEEN: inseenpc seen pc b = true) (WF: wf seen size dist), wf (add_seenpcs seen pc b) size dist. - + (* The idea of computing the distinct list is that we want the algorithm to be able to switch between any representation *) (* of the seen set, using the quite weak axiomatization VMSeen *) (* But we can prove as an invariant that any representation behaves like a ghost no-duplicate list of pairs *) @@ -495,7 +495,7 @@ Section PikeVMComplexity. try destruct H0; try inversion H0; simpl; auto; try right; apply IHwf; auto. Qed. - + Lemma wf_nodup: forall seen size dist, wf seen size dist -> NoDup dist. @@ -506,7 +506,7 @@ Section PikeVMComplexity. constructor; auto. rewrite <- H. rewrite NEW. auto. Qed. - + (* every element is smaller than the size *) Lemma wf_small: forall seen size dist pc b, @@ -518,20 +518,20 @@ Section PikeVMComplexity. - inversion IN. - destruct IN as [IN|IN]; try inversion IN; subst; auto. Qed. - + (* We will show the dist list is a subset of the following list of all possible elements in a certain range *) Fixpoint possible_elements (size:nat) := match size with | 0 => [] | S n => (n,CanExit)::(n,CannotExit)::(possible_elements n) end. - + Lemma possible_size: forall size, length (possible_elements size) = 2 * size. Proof. intros size. induction size; auto. simpl. lia. Qed. - + Lemma possible_all: forall pc b sizec, pc < sizec -> In (pc, b) (possible_elements sizec). @@ -541,7 +541,7 @@ Section PikeVMComplexity. - subst. simpl. destruct b; auto. - apply IHsizec in H0. simpl. auto. Qed. - + Theorem wf_size: forall seen size dist, wf seen size dist -> length dist <= 2 * size. @@ -552,19 +552,19 @@ Section PikeVMComplexity. unfold incl. intros [pca ba] IN. eapply wf_small in IN; eauto. apply possible_all. auto. Qed. - + (* the number of free slots in a seen set *) (* the total number of slots is 2 times the size of the code: each label can be added with 2 possible LoopBool values *) (* we remove the number of distinct entries in the seen set *) Definition free (codesize:nat) (dist:list (nat*LoopBool)) : nat := (2 * codesize) - length dist. - + Lemma free_initial: forall codesize, free codesize [] = 2 * codesize. Proof. intros codesize. unfold free. simpl. lia. Qed. - + Lemma free_add: forall seen size dist t, wf seen size dist -> @@ -575,9 +575,9 @@ Section PikeVMComplexity. intros seen size count [[pc gm] b] WF SEEN SIZE. unfold seen_thread in SEEN. constructor; auto. Qed. - + (** * Well Formedness Invariant and Measure of PikeVM states *) - + (* The number of free slots decreases at most steps *) (* In some cases (a fork), a new thread is created but the number of free slots decreases: this is why free slots are multiplied by 2 *) (* As we change characters, the seen set might get 2*codesize new free slots (multiplied by 2 for the measure) *) @@ -585,7 +585,7 @@ Section PikeVMComplexity. (* It's (2 + 4*codesize) because we might generate a new thread at each input (for unanchored search) and because of the step it takes to advance *) Definition measure (codesize:nat) (dist:list (nat*LoopBool)) (active blocked:list thread) (inp:input) := (2 * free codesize dist) + length active + length blocked + (inpsize inp * (2 + 4 * codesize)). - + (* The invariant that is preserved through pikeVM execution, with a measure that strictly decreases *) Inductive vm_inv (c:code): pike_vm_state -> nat -> Prop := | inv_final: @@ -600,7 +600,7 @@ Section PikeVMComplexity. (* The next place where the prefix can match is in range of the input *) (RANGEPREF: forall n lit strs, nextprefix = Some (n, lit, strs) -> inpsize inp > S n), vm_inv c (PVS inp active best blocked nextprefix seen) (measure (size c) dist active blocked inp). - + Lemma nonfinal_pos: forall c inp active best blocked nextprefix seen m, vm_inv c (PVS inp active best blocked nextprefix seen) m -> 0 < m. @@ -611,22 +611,22 @@ Section PikeVMComplexity. (** * PikeVM measure decreases *) - + (* epsilon_step cannot generate too many new threads *) Lemma eps_step_active: - forall t code inp next, - epsilon_step rer t code inp = EpsActive next -> + forall t code dir inp next, + epsilon_step rer t code dir inp = EpsActive next -> length next <= 2. Proof. - unfold epsilon_step. intros [[pc gm] b] code inp next H. + unfold epsilon_step. intros [[pc gm] b] code dir inp next H. destruct (get_pc code pc) eqn:GET. 2: { inversion H. simpl. lia. } destruct b0; try solve [inversion H; simpl; lia]. - - destruct (check_read rer c inp forward); try solve [inversion H; simpl; lia]. - - destruct (anchor_satisfied rer a inp); try solve [inversion H; simpl; lia]. + - destruct (check_read rer c inp dir); try solve [inversion H; simpl; lia]. + - destruct dir, anchor_satisfied; try solve [inversion H; simpl; lia]. - destruct b; try solve [inversion H; simpl; lia]. Qed. - + Theorem increase_mult: forall a b x, a < b -> @@ -635,15 +635,15 @@ Section PikeVMComplexity. intros a b c H. repeat rewrite PeanoNat.Nat.mul_succ_r. induction c; try lia. Qed. - - + + (* at each step, the measure strictly decreases *) (* the well-formedness of the seen set is preserved *) Theorem pikevm_decreases: forall code pvs1 pvs2 m1, code_wf code (size code) -> nonempty code -> - pike_vm_step rer code pvs1 pvs2 -> + pike_vm_step rer code forward pvs1 pvs2 -> vm_inv code pvs1 m1 -> exists m2, vm_inv code pvs2 m2 /\ m2 < m1. Proof. @@ -727,13 +727,13 @@ Section PikeVMComplexity. + specialize (free_add seen (size code) dist (pc,gm,b) SEENWF UNSEEN RANGE) as FREE. apply wf_size in FREE. unfold measure, free. rewrite length_app. simpl. simpl in FREE. lia. Qed. - - + + (** * Initial PikeVM Measure *) - + Definition complexity (r:regex) (inp:input) : nat := 1 + (4 * codesize r) + (inpsize inp * (2 + 4 * codesize r)). - + Theorem initial_measure: forall inp r, pike_regex r -> @@ -752,11 +752,11 @@ Section PikeVMComplexity. - unfold complexity, measure. rewrite <- compilation_size; auto. simpl. rewrite free_initial. simpl. lia. Qed. - + Theorem initial_measure_unanchored {strs:StrSearch}: forall inp r, pike_regex r -> - vm_inv (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp) (complexity r inp). + vm_inv (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp forward) (complexity r inp). Proof. intros inp r SUBSET. replace (complexity r inp) with (measure (codesize r) [] [(0, GroupMap.empty, CanExit)] [] inp). @@ -771,80 +771,102 @@ Section PikeVMComplexity. - unfold complexity, measure. rewrite <- compilation_size; auto. simpl. rewrite free_initial. simpl. lia. Qed. - + + Axiom initial_measure_unanchored_backward : + forall {strs:StrSearch} inp r , + pike_regex r -> + vm_inv (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp backward) (complexity r inp). + (** * Bounding the number of PikeVM steps *) - + Lemma pike_vm_bound: forall pvs code n, code_wf code (size code) -> nonempty code -> vm_inv code pvs n -> - exists result, steps (pike_vm_step rer code) pvs n (PVS_final result). + exists result, steps (pike_vm_step rer code forward) pvs n (PVS_final result). Proof. intros pvs code n WF NONEMPTY INV. generalize dependent pvs. induction n using (strong_ind); intros. destruct pvs. 2: { exists best. constructor. } - specialize (pikevm_progress rer code inp active best blocked nextprefix seen) as [next STEP]. + specialize (pikevm_progress rer code forward inp active best blocked nextprefix seen) as [next STEP]. specialize (pikevm_decreases code (PVS inp active best blocked nextprefix seen) next n WF NONEMPTY STEP INV) as [newm [INV2 DECR]]. specialize (H newm DECR next INV2) as [result STEPS]. exists result. apply more_steps with (n:=S newm); try lia. econstructor; eauto. Qed. - + + Axiom pike_vm_bound_backward: + forall pvs code n, + code_wf code (size code) -> + nonempty code -> + vm_inv code pvs n -> + exists result, steps (pike_vm_step rer code backward) pvs n (PVS_final result). + (** * Complexity Theorem *) - + Theorem pikevm_complexity: - forall (r:regex) (inp:input), + forall (r:regex) (inp:input) (dir:Direction), (* for any supported regex r and input inp *) pike_regex r -> (* The initial state reaches a final state in at most (complexity r inp) steps. *) - exists result, steps (pike_vm_step rer (compilation r)) + exists result, steps (pike_vm_step rer (compilation r) dir) (pike_vm_initial_state inp) (complexity r inp) (PVS_final result). Proof. - intros r inp SUBSET. - apply pike_vm_bound. - - apply compiled_wf. - - apply compilation_nonempty. - - apply initial_measure. auto. + intros r inp dir SUBSET. + destruct dir. + - apply pike_vm_bound. + + apply compiled_wf. + + apply compilation_nonempty. + + apply initial_measure. auto. + - apply pike_vm_bound_backward. + + apply compiled_wf. + + apply compilation_nonempty. + + apply initial_measure. auto. Qed. - + Theorem pikevm_complexity_unanchored {strs:StrSearch}: - forall (r:regex) (inp:input), + forall (r:regex) (inp:input) (dir:Direction), (* for any supported regex r and input inp *) pike_regex r -> (* The initial state reaches a final state in at most (complexity r inp) steps. *) - exists result, steps (pike_vm_step rer (compilation r)) - (pike_vm_initial_state_unanchored (extract_literal rer r) inp) (complexity r inp) (PVS_final result). + exists result, steps (pike_vm_step rer (compilation r) dir) + (pike_vm_initial_state_unanchored (extract_literal rer r) inp dir) (complexity r inp) (PVS_final result). Proof. - intros r inp SUBSET. - apply pike_vm_bound. - - apply compiled_wf. - - apply compilation_nonempty. - - apply initial_measure_unanchored; auto. + intros r inp dir SUBSET. + destruct dir. + - apply pike_vm_bound. + + apply compiled_wf. + + apply compilation_nonempty. + + apply initial_measure_unanchored; auto. + - apply pike_vm_bound_backward. + + apply compiled_wf. + + apply compilation_nonempty. + + apply initial_measure_unanchored_backward; auto. Qed. - - + + (** * Termination of the PikeVM algorithm *) - + (* As a corollary, we can deduce that the PikeVM always terminates *) Theorem pike_vm_terminates: - forall r inp, + forall r inp dir, pike_regex r -> - exists result, trc_pike_vm rer (compilation r) (pike_vm_initial_state inp) (PVS_final result). + exists result, trc_pike_vm rer (compilation r) dir (pike_vm_initial_state inp) (PVS_final result). Proof. - intros r inp H. eapply pikevm_complexity in H as [result STEPS]; eauto. + intros r inp dir H. eapply pikevm_complexity in H as [result STEPS]; eauto. exists result. eapply steps_trc; eauto. Qed. - + Theorem pike_vm_terminates_unanchored {strs:StrSearch}: - forall r inp, + forall r inp dir, pike_regex r -> - exists result, trc_pike_vm rer (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp) (PVS_final result). + exists result, trc_pike_vm rer (compilation r) dir (pike_vm_initial_state_unanchored (extract_literal rer r) inp dir) (PVS_final result). Proof. - intros r inp H. eapply pikevm_complexity_unanchored in H as [result STEPS]; eauto. + intros r inp dir H. eapply pikevm_complexity_unanchored in H as [result STEPS]; eauto. exists result. eapply steps_trc; eauto. Qed. - + End PikeVMComplexity. Section MemoBTComplexity. @@ -861,10 +883,10 @@ Section MemoBTComplexity. | valid_suf: forall iorig inp (SUF: strict_suffix inp iorig forward), validinp inp iorig. - + (** * Free slots *) (* To define the measure, we need a notion of free slots: how many more states can MemoBT visit *) - + (* well-formedness of a memoset: it was obtained by applying memoize to the initial set *) (* each element that was added is smaller than some `size` constant (size of the bytecode) *) (* each input is a suffix of an original input `originp` *) @@ -886,7 +908,7 @@ Section MemoBTComplexity. (SEEN: is_memo ms pc b inp = true) (WF: mswf ms size originp dist), mswf (memoize ms pc b inp) size originp dist. - + Lemma mswf_in: forall ms size originp dist, mswf ms size originp dist -> @@ -901,7 +923,7 @@ Section MemoBTComplexity. try destruct H0; try inversion H0; simpl; auto; try right; apply IHmswf; auto. Qed. - + Lemma mswf_nodup: forall ms size originp dist, mswf ms size originp dist -> NoDup dist. @@ -912,7 +934,7 @@ Section MemoBTComplexity. constructor; auto. rewrite <- H. rewrite NEW. auto. Qed. - + (* every element is smaller than the size *) Lemma mswf_small: forall ms size originp dist pc b inp, @@ -935,7 +957,7 @@ Section MemoBTComplexity. intros ms size0 originp dist pc b inp WF IN. induction WF; auto. - inversion IN. - destruct IN as [IN|IN]; try inversion IN; subst; auto. - Qed. + Qed. (* the list of possible elements in the memoset for a fixed input *) Definition possible_fixedinput (size:nat) (inp:input) := @@ -951,14 +973,14 @@ Section MemoBTComplexity. (* list of all possible elements in a memoset *) Definition possible_memo (next pref:list Character) (sizec:nat) := List.flat_map (fun inp => possible_fixedinput sizec inp) (possible_suffixes next pref). - + Lemma possible_fixedsize: forall size inp, length (possible_fixedinput size inp) = 2 * size. Proof. intros size inp. induction size; auto. simpl. rewrite length_map. rewrite possible_size. lia. Qed. - + Lemma possible_fixedall: forall pc b inp sizec, pc < sizec -> @@ -997,7 +1019,7 @@ Section MemoBTComplexity. destruct SUF as [EQ | SUF]; auto. subst. destruct next; simpl; auto. Qed. - + Lemma possible_memosize: forall next pref sizec, length (possible_memo next pref sizec) = 2 * sizec * inpsize (Input next pref). @@ -1019,8 +1041,8 @@ Section MemoBTComplexity. - apply possible_sufall. auto. - apply possible_fixedall. auto. Qed. - - + + (* We have a bound on the numer of distinct elements in a memoset *) Theorem mswf_size: forall ms sizec inp dist, @@ -1028,7 +1050,7 @@ Section MemoBTComplexity. Proof. intros ms size0 [next pref] dist H. rewrite <- possible_memosize. apply NoDup_incl_length. - { eapply mswf_nodup; eauto. } + { eapply mswf_nodup; eauto. } unfold incl. intros [[pca ba] ia] IN. eapply mswf_small in IN as LT; eauto. eapply mswf_valid in IN as VA; eauto. apply possible_memo_all; auto. @@ -1038,7 +1060,7 @@ Section MemoBTComplexity. (* we remove the number of distinct entries in the memoset *) Definition msfree (codesize:nat) (inpsize:nat) (dist:list (nat*LoopBool*input)) : nat := (2 * codesize * inpsize) - length dist. - + Lemma msfree_initial: forall codesize inpsize, msfree codesize inpsize [] = 2 * codesize * inpsize. Proof. @@ -1064,13 +1086,13 @@ Section MemoBTComplexity. Qed. (** * Well Formedness Invariant and Measure of MemoBT states *) - + (* The number of free slots decreases at most steps *) (* In some cases (a fork), a new thread is created but the number of free slots decreases: this is why free slots are multiplied by 2 *) (* We add +1 for the last mbt_nomatch step *) Definition memo_measure (codesize:nat) (inpsize:nat) (dist:list (nat*LoopBool*input)) (stack:list config) := (2 * msfree codesize inpsize dist) + length stack + 1. - + (* The invariant that is preserved through MemoBT execution, with a measure that strictly decreases *) Inductive memo_inv (c:code) (originp:input): mbt_state -> nat -> Prop := | minv_final: @@ -1085,7 +1107,7 @@ Section MemoBTComplexity. (* the seen set is well-formed, and has `count` distinct elements *) (MSWF: mswf ms (size c) originp dist), memo_inv c originp (MBT stk ms) (memo_measure (size c) (inpsize originp) dist stk). - + Lemma memo_nonfinal_pos: forall c originp stk ms m, memo_inv c originp (MBT stk ms) m -> 0 < m. @@ -1095,7 +1117,7 @@ Section MemoBTComplexity. (** * MemoBT measure decreases *) - + (* exec_instr cannot generate too many new threads *) Lemma exec_instr_explore: forall c conf stk, @@ -1134,7 +1156,7 @@ Section MemoBTComplexity. - inversion E; subst. inversion IN; subst; inversion H; subst; try inversion H0; subst; auto. - destruct gm1; inversion E; subst; inversion IN; subst; inversion H; subst; auto. Qed. - + (* at each step, the measure strictly decreases *) (* the well-formedness of the memoset is preserved *) Theorem memobt_decreases: @@ -1178,12 +1200,12 @@ Section MemoBTComplexity. + unfold memo_measure, msfree. apply exec_instr_explore in EXPLORE. rewrite length_app. simpl. eapply msfree_add in MSWF as FREE; eauto. apply mswf_size in FREE. simpl in FREE. lia. Qed. - + (** * Initial MemoBT Measure *) - + Definition mbt_complexity (r:regex) (inp:input) : nat := 2 + 4 * (codesize r * inpsize inp). - + Theorem initial_memo_measure: forall inp r ms dist, pike_regex r -> @@ -1204,7 +1226,7 @@ Section MemoBTComplexity. + intros pc gm b inp0 H. inversion H; inversion H0. subst. left. + rewrite compilation_size; auto. Qed. - + (** * Bounding the number of MemoBT steps *) (* A memoset is valid when it does correspond to some distinct list of elements, @@ -1228,16 +1250,16 @@ Section MemoBTComplexity. exists result. exists finalms. split; auto. apply more_steps with (n:=S newm); try lia. econstructor; eauto. Qed. - + (** * Complexity Theorem *) - + Theorem memobt_complexity: forall (r:regex) (inp:input) (ms:memoset), pike_regex r -> validms ms (codesize r) inp -> exists result finalms, steps (memobt_step rer (compilation r)) (initial_state inp ms) (mbt_complexity r inp) (MBT_final result finalms) /\ - validms finalms (codesize r) inp. + validms finalms (codesize r) inp. Proof. intros r inp ms SUBSET WF. destruct WF as [dist WF]. @@ -1245,7 +1267,7 @@ Section MemoBTComplexity. specialize (memobt_bound _ _ _ _ (compiled_wf r) INV) as [result [finalms [STEPS VALID]]]. exists result. exists finalms. rewrite <- compilation_size; auto. split;auto. eapply more_steps; eauto. Qed. - + Theorem memobt_complexity_empty_memoset: forall (r:regex) (inp:input), (* for any supported regex r and input inp *) @@ -1260,7 +1282,7 @@ Section MemoBTComplexity. Qed. (** * Termination of the MemoBT algorithm *) - + (* As a corollary, we can deduce that the MemoBT algorithm always terminates *) Theorem memobt_terminates: forall r inp, @@ -1270,5 +1292,5 @@ Section MemoBTComplexity. intros r inp H. eapply memobt_complexity_empty_memoset in H as [result [finalms [STEPS VALID]]]; eauto. exists result. exists finalms. eapply steps_trc; eauto. Qed. - + End MemoBTComplexity. diff --git a/Engine/Correctness.v b/Engine/Correctness.v index 96005446..38d7d2dc 100644 --- a/Engine/Correctness.v +++ b/Engine/Correctness.v @@ -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. @@ -69,7 +69,7 @@ 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) -> + 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. @@ -83,7 +83,7 @@ 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) -> + 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). @@ -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. @@ -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. @@ -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. @@ -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. @@ -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. @@ -264,7 +264,7 @@ 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. @@ -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). diff --git a/Engine/FunctionalPikeVM.v b/Engine/FunctionalPikeVM.v index de8d49a2..cbff9faa 100644 --- a/Engine/FunctionalPikeVM.v +++ b/Engine/FunctionalPikeVM.v @@ -19,7 +19,7 @@ Section FunctionalPikeVM. (** * Functional Definition *) (* a functional version of the small step *) -Definition pike_vm_func_step (c:code) (pvs:pike_vm_state) : pike_vm_state := +Definition pike_vm_func_step (c:code) (dir:Direction) (pvs:pike_vm_state) : pike_vm_state := match pvs with | PVS_final _ => pvs | PVS inp active best blocked nextprefix seen => @@ -29,17 +29,17 @@ Definition pike_vm_func_step (c:code) (pvs:pike_vm_state) : pike_vm_state := | [] => match nextprefix with | Some (n, lit, strs) => - let nextinp := advance_input_n inp (S n) forward in - PVS nextinp [pike_vm_initial_thread] best [] (next_prefix_counter nextinp lit) initial_seenpcs (* pvs_acc *) + let nextinp := advance_input_n inp (S n) dir in + PVS nextinp [pike_vm_initial_thread] best [] (next_prefix_counter nextinp dir lit) initial_seenpcs (* pvs_acc *) | None => PVS_final best (* pvs_final *) end | thr::blocked => - match (advance_input inp forward) with + match (advance_input inp dir) with | None => PVS_final best (* pvs_end *) | Some nextinp => match nextprefix with | None => PVS nextinp (thr::blocked) best [] None initial_seenpcs (* pvs_nextchar *) - | Some (0, lit, strs) => PVS nextinp (thr::blocked ++ [pike_vm_initial_thread]) best [] (next_prefix_counter nextinp lit) initial_seenpcs (* pvs_nextchar_generate *) + | Some (0, lit, strs) => PVS nextinp (thr::blocked ++ [pike_vm_initial_thread]) best [] (next_prefix_counter nextinp dir lit) initial_seenpcs (* pvs_nextchar_generate *) | Some (S n, lit, strs) => PVS nextinp (thr::blocked) best [] (Some (n, lit, strs)) initial_seenpcs (* pvs_nextchar_filter *) end end @@ -49,7 +49,7 @@ Definition pike_vm_func_step (c:code) (pvs:pike_vm_state) : pike_vm_state := | true => PVS inp active best blocked nextprefix seen (* pvs_skip *) | false => let nextseen := add_thread seen t in - match (epsilon_step rer t c inp) with + match (epsilon_step rer t c dir inp) with | EpsActive nextactive => PVS inp (nextactive++active) best blocked nextprefix nextseen (* pvs_active *) | EpsMatch => @@ -62,14 +62,14 @@ Definition pike_vm_func_step (c:code) (pvs:pike_vm_state) : pike_vm_state := end. (* looping the small step function until fuel runs out or a final state is reached *) -Fixpoint pike_vm_loop (c:code) (pvs:pike_vm_state) (fuel:nat) : pike_vm_state := +Fixpoint pike_vm_loop (c:code) (dir:Direction) (pvs:pike_vm_state) (fuel:nat) : pike_vm_state := match pvs with | PVS_final _ => pvs | _ => match fuel with | 0 => pvs | S fuel => - pike_vm_loop c (pike_vm_func_step c pvs) fuel + pike_vm_loop c dir (pike_vm_func_step c dir pvs) fuel end end. @@ -88,18 +88,18 @@ Definition getres (pvs:pike_vm_state) : matchres := end. (* Functional version of the PikeVM *) -Definition pike_vm_match (r:regex) (inp:input) : matchres := +Definition pike_vm_match (r:regex) (inp:input) (dir:Direction) : matchres := let code := compilation r in let fuel := vm_fuel r inp in let pvsinit := pike_vm_initial_state inp in - getres (pike_vm_loop code pvsinit fuel). + getres (pike_vm_loop code dir pvsinit fuel). (* Functional version of the unanchored PikeVM *) -Definition pike_vm_match_unanchored {strs:StrSearch} (r:regex) (inp:input) : matchres := +Definition pike_vm_match_unanchored {strs:StrSearch} (r:regex) (inp:input) (dir:Direction): matchres := let code := compilation r in let fuel := vm_fuel r inp in - let pvsinit := pike_vm_initial_state_unanchored (extract_literal rer r) inp in - getres (pike_vm_loop code pvsinit fuel). + let pvsinit := pike_vm_initial_state_unanchored (extract_literal rer r) inp dir in + getres (pike_vm_loop code dir pvsinit fuel). (** * Smallstep correspondence *) @@ -113,29 +113,29 @@ Ltac match_destr:= end. Theorem func_step_correct: - forall c pvs1 pvs2, - pike_vm_func_step c pvs1 = pvs2 -> - pike_vm_step rer c pvs1 pvs2 \/ final_state pvs1. + forall c dir pvs1 pvs2, + pike_vm_func_step c dir pvs1 = pvs2 -> + pike_vm_step rer c dir pvs1 pvs2 \/ final_state pvs1. Proof. - unfold pike_vm_func_step. intros c pvs1 pvs2 H. + unfold pike_vm_func_step. intros c dir pvs1 pvs2 H. repeat match_destr; subst; try solve[left; constructor; auto]. right. constructor. Qed. Corollary func_step_not_final: - forall c inp active best blocked nextprefix seen, - pike_vm_step rer c (PVS inp active best blocked nextprefix seen) (pike_vm_func_step c (PVS inp active best blocked nextprefix seen)). + forall c dir inp active best blocked nextprefix seen, + pike_vm_step rer c dir (PVS inp active best blocked nextprefix seen) (pike_vm_func_step c dir (PVS inp active best blocked nextprefix seen)). Proof. - intros c inp active best blocked nextprefix seen. specialize (func_step_correct c (PVS inp active best blocked nextprefix seen) _ (@eq_refl _ _)). + intros c dir inp active best blocked nextprefix seen. specialize (func_step_correct c dir (PVS inp active best blocked nextprefix seen) _ (@eq_refl _ _)). intros [H|H]; auto. inversion H. Qed. Theorem loop_trc: - forall c pvs1 pvs2 fuel, - pike_vm_loop c pvs1 fuel = pvs2 -> - trc_pike_vm rer c pvs1 pvs2. + forall c dir pvs1 pvs2 fuel, + pike_vm_loop c dir pvs1 fuel = pvs2 -> + trc_pike_vm rer c dir pvs1 pvs2. Proof. - intros c pvs1 pvs2 fuel H. + intros c dir pvs1 pvs2 fuel H. generalize dependent pvs1. induction fuel; intros; simpl in H. { destruct pvs1; inversion H. constructor. constructor. } match_destr; subst. @@ -143,22 +143,21 @@ Proof. - constructor. Qed. - Lemma step_loop: - forall c pvs1 pvs2 fuel, - pike_vm_step rer c pvs1 pvs2 -> - pike_vm_loop c pvs1 (S fuel) = pike_vm_loop c pvs2 fuel. + forall c dir pvs1 pvs2 fuel, + pike_vm_step rer c dir pvs1 pvs2 -> + pike_vm_loop c dir pvs1 (S fuel) = pike_vm_loop c dir pvs2 fuel. Proof. - intros c pvs1 pvs2 fuel H. destruct H; simpl; + intros c dir pvs1 pvs2 fuel H. destruct H; simpl; now rewrite ?ADVANCE, ?SEEN, ?UNSEEN, ?STEP. Qed. Theorem steps_loop: - forall c pvs1 pvs2 fuel, - steps (pike_vm_step rer c) pvs1 fuel (PVS_final pvs2) -> - pike_vm_loop c pvs1 fuel = (PVS_final pvs2). + forall c dir pvs1 pvs2 fuel, + steps (pike_vm_step rer c dir) pvs1 fuel (PVS_final pvs2) -> + pike_vm_loop c dir pvs1 fuel = (PVS_final pvs2). Proof. - intros c pvs1 pvs2 fuel H. remember (PVS_final pvs2) as result. + intros c dir pvs1 pvs2 fuel H. remember (PVS_final pvs2) as result. induction H; subst. - destruct n; simpl; auto. - destruct x. @@ -168,48 +167,94 @@ Qed. (* when the function finishes, it returns the correct result *) Theorem pike_vm_match_correct: - forall r inp result, - pike_vm_match r inp = Finished result -> - trc_pike_vm rer (compilation r) (pike_vm_initial_state inp) (PVS_final result). + forall r dir inp result, + pike_vm_match r inp dir = Finished result -> + trc_pike_vm rer (compilation r) dir (pike_vm_initial_state inp) (PVS_final result). Proof. - unfold pike_vm_match, getres. intros r inp result H. + unfold pike_vm_match, getres. intros r dir inp result H. match_destr; inversion H; subst. eapply loop_trc; eauto. Qed. (* when the function finishes, it returns the correct result *) Theorem pike_vm_match_correct_unanchored {strs:StrSearch}: - forall r inp result, - pike_vm_match_unanchored r inp = Finished result -> - trc_pike_vm rer (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp) (PVS_final result). + forall r dir inp result, + pike_vm_match_unanchored r inp dir = Finished result -> + trc_pike_vm rer (compilation r) dir (pike_vm_initial_state_unanchored (extract_literal rer r) inp dir) (PVS_final result). Proof. - unfold pike_vm_match_unanchored, getres. intros r inp result H. + unfold pike_vm_match_unanchored, getres. intros r dir inp result H. match_destr; inversion H; subst. eapply loop_trc; eauto. Qed. (* the function always terminates *) Theorem pike_vm_match_terminates: - forall r inp, + forall r inp dir, pike_regex r -> - exists result, pike_vm_match r inp = Finished result. + exists result, pike_vm_match r inp dir = Finished result. Proof. - intros r inp SUBSET. unfold pike_vm_match, vm_fuel. - apply pikevm_complexity with (VMS:=VMS) (rer:=rer) (inp:=inp) in SUBSET as [result TERM]. + intros r inp dir SUBSET. unfold pike_vm_match, vm_fuel. + apply pikevm_complexity with (VMS:=VMS) (rer:=rer) (inp:=inp) (dir:=dir) in SUBSET as [result TERM]. exists result. apply steps_loop in TERM. rewrite TERM. auto. Qed. (* the function always terminates *) Theorem pike_vm_match_terminates_unanchored {strs:StrSearch}: - forall r inp, + forall r inp dir, pike_regex r -> - exists result, pike_vm_match_unanchored r inp = Finished result. + exists result, pike_vm_match_unanchored r inp dir = Finished result. Proof. - intros r inp SUBSET. unfold pike_vm_match_unanchored, vm_fuel. - apply pikevm_complexity_unanchored with (strs:=strs) (VMS:=VMS) (rer:=rer) (inp:=inp) in SUBSET as [result TERM]; auto. + intros r inp dir SUBSET. unfold pike_vm_match_unanchored, vm_fuel. + apply pikevm_complexity_unanchored with (strs:=strs) (VMS:=VMS) (rer:=rer) (inp:=inp) (dir:=dir) in SUBSET as [result TERM]; auto. exists result. apply steps_loop in TERM. rewrite TERM. auto. Qed. +(* relating the final state of the reverse direction for the TRC *) +Lemma trc_pike_vm_reverse: + forall c dir pvs result1 result2, + trc_pike_vm rer c dir pvs (PVS_final result1) -> + trc_pike_vm rer c (direction_reverse dir) (pvs_reverse pvs) (PVS_final result2) -> + result1 = leaf_reverse result2. +Proof. + intros c dir pvs result1 result2 H1. + remember (PVS_final result1) as pvs_end. + induction H1; intros H2; subst. + - inversion H2; subst. + + now rewrite leaf_reverse_involutive. + + easy. + - inversion H2; subst. + + now destruct x. + + eapply IHtrc; eauto. + eapply pikevm_step_reverse in STEP as Heq; eauto. + apply f_equal with (f:=pvs_reverse) in Heq. + rewrite pvs_reverse_involutive in Heq. + now subst. +Qed. + +(* expresses anchored matching in the reverse direction in terms of the the other direction *) +Lemma pike_vm_match_reverse : + forall r inp dir result1 result2, + pike_vm_match r inp dir = Finished result1 -> + pike_vm_match r (input_reverse inp) (direction_reverse dir) = Finished result2 -> + result1 = leaf_reverse result2. +Proof. + intros r inp dir result1 result2 H1%pike_vm_match_correct H2%pike_vm_match_correct. + eapply trc_pike_vm_reverse; eauto. +Qed. + +(* expresses unanchored matching in the reverse direction in terms of the the other direction *) +Lemma pike_vm_match_reverse_unanchored {strs:StrSearch}: + forall r inp dir result1 result2, + pike_vm_match_unanchored r inp dir = Finished result1 -> + pike_vm_match_unanchored r (input_reverse inp) (direction_reverse dir) = Finished result2 -> + result1 = leaf_reverse result2. +Proof. + intros r inp dir result1 result2 H1%pike_vm_match_correct_unanchored H2%pike_vm_match_correct_unanchored. + unfold pike_vm_initial_state_unanchored in *. + eapply trc_pike_vm_reverse; eauto. + now rewrite next_prefix_counter_reverse. +Qed. + End FunctionalPikeVM. (** * Execution Examples *) @@ -242,7 +287,7 @@ Section Example. Example nq_inp: input := Input [a;b] []. Lemma nullable_quant: - pike_vm_match (rer_of nq_regex) nq_regex nq_inp = Finished (Some (Input [] [b;a], GroupMap.empty)). + pike_vm_match (rer_of nq_regex) nq_regex nq_inp forward = Finished (Some (Input [] [b;a], GroupMap.empty)). Proof. reflexivity. Qed. (** * Example from the paper - Figure 15 *) @@ -279,7 +324,7 @@ Example final_gm : GroupMap.t := GroupMap.close 1 1 (GroupMap.open 0 1 GroupMap.empty). Lemma paper_pikevm_exec: - pike_vm_match (rer_of paper_regex) paper_regex paper_input = Finished (Some (Input [] [b;a], final_gm)). + pike_vm_match (rer_of paper_regex) paper_regex paper_input forward = Finished (Some (Input [] [b;a], final_gm)). Proof. reflexivity. Qed. End Example. diff --git a/Engine/Meta/EngineSpec.v b/Engine/Meta/EngineSpec.v index 653be4f5..2bd8b926 100644 --- a/Engine/Meta/EngineSpec.v +++ b/Engine/Meta/EngineSpec.v @@ -74,7 +74,7 @@ Defined. (* we show that the PikeVM fits the scheme of an anchored engine *) #[export] #[refine] Instance PikeVMAnchoredEngine: AnchoredEngine rer := { - exec r inp := match pike_vm_match rer r inp with + exec r inp := match pike_vm_match rer r inp forward with | FunctionalPikeVM.OutOfFuel => None | FunctionalPikeVM.Finished res => res end; @@ -83,7 +83,7 @@ Instance PikeVMAnchoredEngine: AnchoredEngine rer := { (* exec_correct *) intros r inp tree Hsubset Htree. rewrite is_pike_regex_correct in Hsubset. - pose proof (pike_vm_match_terminates rer r inp Hsubset) as [res Hmatch]. + pose proof (pike_vm_match_terminates rer r inp forward Hsubset) as [res Hmatch]. rewrite Hmatch. symmetry. eauto using pike_vm_match_correct, pike_vm_correct. Defined. @@ -91,7 +91,7 @@ Defined. (* we show that the PikeVM fits the scheme of an unanchored engine *) #[export] #[refine] Instance PikeVMUnanchoredEngine {strs:StrSearch}: UnanchoredEngine rer := { - un_exec r inp := match pike_vm_match_unanchored rer r inp with + un_exec r inp := match pike_vm_match_unanchored rer r inp forward with | FunctionalPikeVM.OutOfFuel => None | FunctionalPikeVM.Finished res => res end; @@ -100,7 +100,7 @@ Instance PikeVMUnanchoredEngine {strs:StrSearch}: UnanchoredEngine rer := { (* un_exec_correct *) intros r inp tree Hsubset Htree. rewrite is_pike_regex_correct in Hsubset. - pose proof (pike_vm_match_terminates_unanchored rer r inp Hsubset) as [res Hmatch]. + pose proof (pike_vm_match_terminates_unanchored rer r inp forward Hsubset) as [res Hmatch]. rewrite Hmatch. symmetry. eauto using pike_vm_match_correct_unanchored, pike_vm_correct_unanchored. Defined. diff --git a/Engine/PikeEquiv.v b/Engine/PikeEquiv.v index 5f807198..5f1cbd9b 100644 --- a/Engine/PikeEquiv.v +++ b/Engine/PikeEquiv.v @@ -87,13 +87,13 @@ Qed. (* These lemmas discard the stuttering steps by preventing the current pc being at a Jmp instruction *) Theorem generate_match: - forall tree gm inp code pc b + forall tree gm inp code dir pc b (TREESTEP: tree_bfs_step tree gm (idx inp) = StepMatch) (NOSTUTTER: stutters pc code = false) (TT: tree_thread code inp (tree, gm) (pc, gm, b)), - epsilon_step rer (pc, gm, b) code inp = EpsMatch. + epsilon_step rer (pc, gm, b) code dir inp = EpsMatch. Proof. - intros tree gm inp code pc b TREESTEP NOSTUTTER TT. + intros tree gm inp code dir pc b TREESTEP NOSTUTTER TT. unfold tree_bfs_step in TREESTEP. destruct tree; inversion TREESTEP. subst. clear TREESTEP. inversion TT; subst; try no_stutter. remember Match as TMATCH. @@ -115,7 +115,7 @@ Theorem generate_blocked: (TREESTEP: tree_bfs_step tree gm (idx inp) = StepBlocked nexttree) (NOSTUTTER: stutters pc code = false) (TT: tree_thread code inp (tree, gm) (pc, gm, b)), - epsilon_step rer (pc,gm,b) code inp = EpsBlocked (pc+1,gm,CanExit) /\ + epsilon_step rer (pc,gm,b) code forward inp = EpsBlocked (pc+1,gm,CanExit) /\ (forall nextinp, advance_input inp forward = Some nextinp -> tree_thread code nextinp (nexttree,gm) (pc+1,gm,CanExit)) /\ exists nextinp, advance_input inp forward = Some nextinp. Proof. @@ -144,7 +144,7 @@ Theorem generate_open: forall gid tree gm inp code pc b (TT: tree_thread code inp (GroupAction (Open gid) tree, gm) (pc, gm, b)) (NOSTUTTER: stutters pc code = false), - epsilon_step rer (pc, gm, b) code inp = EpsActive [(pc + 1, GroupMap.open (idx inp) gid gm, b)] /\ + epsilon_step rer (pc, gm, b) code forward inp = EpsActive [(pc + 1, GroupMap.open (idx inp) gid gm, b)] /\ tree_thread code inp (tree,GroupMap.open (idx inp) gid gm) (pc + 1, GroupMap.open (idx inp) gid gm, b). Proof. intros gid tree gm inp code pc b TT NOSTUTTER. @@ -169,7 +169,7 @@ Theorem generate_close: forall gid tree gm inp code pc b (TT: tree_thread code inp (GroupAction (Close gid) tree, gm) (pc, gm, b)) (NOSTUTTER: stutters pc code = false), - epsilon_step rer (pc, gm, b) code inp = EpsActive [(pc + 1, GroupMap.close (idx inp) gid gm, b)] /\ + epsilon_step rer (pc, gm, b) code forward inp = EpsActive [(pc + 1, GroupMap.close (idx inp) gid gm, b)] /\ tree_thread code inp (tree,GroupMap.close (idx inp) gid gm) (pc + 1, GroupMap.close (idx inp) gid gm, b). Proof. intros gid tree gm inp code pc b TT NOSTUTTER. @@ -204,10 +204,10 @@ Proof. Qed. Corollary generate_reset: - forall gidl tree inp code pc b gm + forall gidl tree inp code dir pc b gm (TT: tree_thread code inp (GroupAction (Reset gidl) tree, gm) (pc,gm,b)) (NOSTUTTER: stutters pc code = false), - epsilon_step rer (pc,gm,b) code inp = EpsActive [(pc+1, GroupMap.reset gidl gm, b)] /\ + epsilon_step rer (pc,gm,b) code dir inp = EpsActive [(pc+1, GroupMap.reset gidl gm, b)] /\ tree_thread code inp (tree,GroupMap.reset gidl gm) (pc+1, GroupMap.reset gidl gm, b). Proof. intros. @@ -221,7 +221,7 @@ Theorem generate_mismatch: forall gm inp code pc b (TT: tree_thread code inp (Mismatch, gm) (pc, gm, b)) (NOSTUTTER: stutters pc code = false), - epsilon_step rer (pc, gm, b) code inp = EpsActive []. + epsilon_step rer (pc, gm, b) code forward inp = EpsActive []. Proof. intros gm inp code pc b TT NOSTUTTER. inversion TT; subst; try no_stutter. @@ -239,13 +239,13 @@ Proof. Qed. Theorem generate_checkpass: - forall tree gm inp code pc b + forall tree gm inp code dir pc b (TT: tree_thread code inp (Progress tree, gm) (pc, gm, b)) (NOSTUTTER: stutters pc code = false), - exists nextpc, epsilon_step rer (pc, gm, b) code inp = EpsActive [(nextpc,gm,CanExit)] /\ + exists nextpc, epsilon_step rer (pc, gm, b) code dir inp = EpsActive [(nextpc,gm,CanExit)] /\ tree_thread code inp (tree,gm) (nextpc,gm,CanExit). Proof. - intros tree gm inp code pc b TT NOSTUTTER. + intros tree gm inp code dir pc b TT NOSTUTTER. inversion TT; subst; try no_stutter. remember (Progress tree) as TPASS. induction TREE; intros; subst; try inversion HeqTPASS; subst. @@ -262,7 +262,7 @@ Theorem generate_anchorpass: forall tree gm inp code pc b a (TT: tree_thread code inp (AnchorPass a tree, gm) (pc, gm, b)) (NOSTUTTER: stutters pc code = false), - epsilon_step rer (pc, gm, b) code inp = EpsActive [(pc+1,gm,b)] /\ + epsilon_step rer (pc, gm, b) code forward inp = EpsActive [(pc+1,gm,b)] /\ tree_thread code inp (tree,gm) (pc+1,gm,b). Proof. intros tree gm inp code pc b a TT NOSTUTTER. @@ -283,15 +283,15 @@ Qed. Theorem generate_choice: - forall tree1 tree2 gm inp code pc b treeactive + forall tree1 tree2 gm inp code dir pc b treeactive (TREESTEP: tree_bfs_step (Choice tree1 tree2) gm (idx inp) = StepActive treeactive) (NOSTUTTER: stutters pc code = false) (TT: tree_thread code inp (Choice tree1 tree2, gm) (pc, gm, b)), exists threadactive, - epsilon_step rer (pc, gm, b) code inp = EpsActive threadactive /\ + epsilon_step rer (pc, gm, b) code dir inp = EpsActive threadactive /\ list_tree_thread code inp treeactive threadactive. Proof. - intros tree1 tree2 gm inp code pc b treeactive TREESTEP NOSTUTTER TT. + intros tree1 tree2 gm inp code dir pc b treeactive TREESTEP NOSTUTTER TT. unfold tree_bfs_step in TREESTEP. inversion TREESTEP. subst. clear TREESTEP. inversion TT; subst; try no_stutter. remember (Choice tree1 tree2) as TCHOICE. @@ -388,7 +388,7 @@ Theorem generate_active: (NOSTUTTER: stutters pc code = false) (TT: tree_thread code inp (tree, gm) (pc, gm, b)), exists threadactive, - epsilon_step rer (pc, gm, b) code inp = EpsActive threadactive /\ + epsilon_step rer (pc, gm, b) code forward inp = EpsActive threadactive /\ list_tree_thread code inp treeactive threadactive. Proof. intros tree gm inp code pc b treeactive TREESTEP NOSTUTTER TT. @@ -425,14 +425,14 @@ Qed. (* LATER: simplify/automate this proof *) (* in the case where we are at a stuttering step, we show that we still preserve the invariant *) Theorem stutter_step: - forall tree gm inp code pc b + forall tree gm inp code dir pc b (TT: tree_thread code inp (tree,gm) (pc,gm,b)) (STUTTER: stutters pc code = true), exists nextpc nextb, - epsilon_step rer (pc,gm,b) code inp = EpsActive [(nextpc,gm,nextb)] /\ + epsilon_step rer (pc,gm,b) code dir inp = EpsActive [(nextpc,gm,nextb)] /\ tree_thread code inp (tree,gm) (nextpc,gm,nextb). Proof. - intros tree gm inp code pc b TT STUTTER. + intros tree gm inp code dir pc b TT STUTTER. inversion TT; subst. (* reset is not stuttering *) 2: { unfold stutters in STUTTER. rewrite RESET in STUTTER. inversion STUTTER. } @@ -825,7 +825,7 @@ Lemma future_nextprefix_some {strs:StrSearch}: forall inp r code p future, pike_regex r -> compilation r = code -> - next_prefix_counter inp (extract_literal rer r) = Some p -> + next_prefix_counter inp forward (extract_literal rer r) = Some p -> future_tree_shape rer r inp future -> future_nextprefix code inp (Some future) (Some p). Proof. @@ -860,7 +860,7 @@ Lemma next_prefix_counter_none_nores {strs:StrSearch}: forall r inp future, pike_regex r -> future_tree_shape rer r inp future -> - next_prefix_counter inp (extract_literal rer r) = None -> + next_prefix_counter inp forward (extract_literal rer r) = None -> first_leaf future inp = None. Proof. intros r [next pref]. @@ -917,7 +917,7 @@ Qed. Definition stutter_wf (code:code) : Prop := forall pc gm b nextpc nextgm nextb inp, stutters pc code = true -> - epsilon_step rer (pc,gm,b) code inp = EpsActive[(nextpc,nextgm,nextb)] -> + epsilon_step rer (pc,gm,b) code forward inp = EpsActive[(nextpc,nextgm,nextb)] -> pc < nextpc. Lemma nth_nil: @@ -1060,7 +1060,7 @@ Proof. assert (get_pc r_code pc = Some b0). { rewrite nth_error_app1 in NTH; auto. } unfold stutter_wf in COMP. - assert (epsilon_step rer (pc,gm,b) r_code inp = EpsActive [(nextpc,nextgm,nextb)]). + assert (epsilon_step rer (pc,gm,b) r_code forward inp = EpsActive [(nextpc,nextgm,nextb)]). { simpl in H0. unfold get_pc in H0. rewrite NTH in H0. simpl. rewrite H2. destruct b0; auto. } @@ -1091,7 +1091,7 @@ Lemma initial_pike_inv_unanchored {strs:StrSearch}: (SUBSET: pike_regex r) (SHAPE: future_tree_shape rer r inp future_tree), exists future, may_erase future_tree future /\ - pike_inv code (pike_tree_initial_state_unanchored tree future inp) (pike_vm_initial_state_unanchored (extract_literal rer r) inp). + pike_inv code (pike_tree_initial_state_unanchored tree future inp) (pike_vm_initial_state_unanchored (extract_literal rer r) inp forward). Proof. intros. unfold pike_vm_initial_state_unanchored. @@ -1122,7 +1122,7 @@ Theorem invariant_preservation: forall code pts1 pvs1 pvs2 (STWF: stutter_wf code) (INV: pike_inv code pts1 pvs1) - (VMSTEP: pike_vm_step rer code pvs1 pvs2), + (VMSTEP: pike_vm_step rer code forward pvs1 pvs2), (* either we make a step on both sides, preserving invariant *) ( exists pts2, @@ -1196,7 +1196,7 @@ Proof. (* do we have the nextprefix if so, with what counter? *) destruct nextprefix as [[[nextprefix lit] strs]|]; [destruct nextprefix|]. (* nextchar_generate *) - + assert (pvs2 = PVS (Input next (c::pref)) (((pc,gmblocked,b)::threadlist) ++ [pike_vm_initial_thread]) best [] (next_prefix_counter (Input next (c::pref)) lit) initial_seenpcs) + + assert (pvs2 = PVS (Input next (c::pref)) (((pc,gmblocked,b)::threadlist) ++ [pike_vm_initial_thread]) best [] (next_prefix_counter (Input next (c::pref)) forward lit) initial_seenpcs) by eauto using pikevm_deterministic, pvs_nextchar_generate. apply advance_next in ADV. inversion FUTUREPREFIX; subst. left. @@ -1226,7 +1226,7 @@ Proof. destruct (stutters pc code) eqn:STUTTERS. { (* stuttering step *) - right. apply stutter_step in TT as H; auto. + right. apply stutter_step with (dir:=forward) in TT as H; auto. destruct H as [nextpc [nextb [EPSSTEP TT2]]]; subst. assert (pvs2 = (PVS inp ([(nextpc, gm, nextb)] ++ threadactive) best threadblocked nextprefix (add_thread threadseen (pc,gm,b)))). { eapply pikevm_deterministic; eauto. eapply pvs_active; eauto. } @@ -1245,7 +1245,7 @@ Proof. + eapply pikeinv; try (eapply add_inclusion; eauto); try constructor; eauto. apply ltt_app; eauto. (* match *) - - left. eapply generate_match in TREESTEP as THREADSTEP; eauto. + - left. eapply generate_match with (dir:=forward) in TREESTEP as THREADSTEP; eauto. assert (pvs2 = PVS inp [] (Some (inp,gm_of (pc,gm,b))) threadblocked None (add_thread threadseen (pc,gm,b))). { eapply pikevm_deterministic; eauto. constructor; auto. } subst. exists (PTS inp [] (Some (inp,gm)) treeblocked None (add_seentrees treeseen t)). split. diff --git a/Engine/PikeVM.v b/Engine/PikeVM.v index 8beade81..3b5cb18a 100644 --- a/Engine/PikeVM.v +++ b/Engine/PikeVM.v @@ -37,7 +37,7 @@ to the next position where the prefix matches. From Stdlib Require Import List Lia. Import ListNotations. -From Linden Require Import Regex Chars Groups. +From Linden Require Import Regex Chars Groups FunctionalSemantics. From Linden Require Import Tree Semantics NFA. From Linden Require Import BooleanSemantics PikeSubset. From Linden Require Import Parameters SeenSets Prefix. @@ -99,35 +99,58 @@ Inductive epsilon_result : Type := Definition EpsDead : epsilon_result := EpsActive []. +(* flips begin and end input anchors *) +Definition flip_anchor (a:anchor) : anchor := + match a with + | BeginInput => EndInput + | EndInput => BeginInput + | WordBoundary => WordBoundary + | NonWordBoundary => NonWordBoundary + end. + +(* get the anchor to check depending on the direction *) +Definition anchor_dir (a:anchor) (dir:Direction): anchor := + match dir with + | forward => a + | backward => flip_anchor a + end. + +(* get current string position index depending on the direction *) +Definition idx_dir (inp:input) (dir:Direction): nat := + match dir with + | forward => idx inp + | backward => + let 'Input next pref := inp in + List.length next + end. + (* an atomic step for a thread *) -Definition epsilon_step (t:thread) (c:code) (i:input): epsilon_result := - match t with - | (pc, gm, b) => - match get_pc c pc with - | None => EpsDead - | Some instr => - match instr with - | Accept => EpsMatch - | Consume cd => match check_read rer cd i forward with - | CannotRead => EpsDead - | CanRead => EpsBlocked (block_thread t) +Definition epsilon_step (t:thread) (c:code) (dir:Direction) (i:input): epsilon_result := + let '(pc, gm, b) := t in + match get_pc c pc with + | None => EpsDead + | Some instr => + match instr with + | Accept => EpsMatch + | Consume cd => match check_read rer cd i dir with + | CannotRead => EpsDead + | CanRead => EpsBlocked (block_thread t) + end + | CheckAnchor a => match anchor_satisfied rer (anchor_dir a dir) i with + | false => EpsDead + | true => EpsActive [advance_thread t] end - | CheckAnchor a => match anchor_satisfied rer a i with - | false => EpsDead - | true => EpsActive [advance_thread t] - end - | Jmp next => EpsActive [upd_label t next] - | Fork l1 l2 => EpsActive [upd_label t l1; upd_label t l2] - | SetRegOpen gid => EpsActive [open_thread t gid (idx i)] - | SetRegClose gid => EpsActive [close_thread t gid (idx i)] - | ResetRegs gidl => EpsActive [reset_thread t gidl] - | BeginLoop => EpsActive [begin_thread t] - | EndLoop next => match b with - | CannotExit => EpsDead - | CanExit => EpsActive [upd_label t next] - end - | KillThread => EpsDead - end + | Jmp next => EpsActive [upd_label t next] + | Fork l1 l2 => EpsActive [upd_label t l1; upd_label t l2] + | SetRegOpen gid => EpsActive [open_thread t gid (idx_dir i dir)] + | SetRegClose gid => EpsActive [close_thread t gid (idx_dir i dir)] + | ResetRegs gidl => EpsActive [reset_thread t gidl] + | BeginLoop => EpsActive [begin_thread t] + | EndLoop next => match b with + | CannotExit => EpsDead + | CanExit => EpsActive [upd_label t next] + end + | KillThread => EpsDead end end. @@ -141,11 +164,15 @@ Inductive pike_vm_state : Type := (* given an input and literal, we compute the next prefix counter *) (* since the counter is always offset by one, we first try to advance the input before performing a prefix search *) -Definition next_prefix_counter {strs:StrSearch} (inp: input) (lit: literal) : option (nat * literal * StrSearch) := - match advance_input inp forward with +Definition next_prefix_counter {strs:StrSearch} (inp: input) (dir: Direction) (lit: literal) : option (nat * literal * StrSearch) := + match advance_input inp dir with | None => None | Some (Input next pref) => - match str_search (prefix lit) next with + let search := str_search (prefix lit) match dir with + | forward => next + | backward => pref + end in + match search with | None => None | Some n => Some (n, lit, strs) end @@ -153,8 +180,8 @@ Definition next_prefix_counter {strs:StrSearch} (inp: input) (lit: literal) : op Definition pike_vm_initial_thread : thread := (0, GroupMap.empty, CanExit). (* initial state for the PikeVM which operates in unanchored fashion *) -Definition pike_vm_initial_state_unanchored {strs:StrSearch} (lit:literal) (inp:input) : pike_vm_state := - let nextprefix := next_prefix_counter inp lit in +Definition pike_vm_initial_state_unanchored {strs:StrSearch} (lit:literal) (inp:input) (dir:Direction) : pike_vm_state := + let nextprefix := next_prefix_counter inp dir lit in PVS inp [pike_vm_initial_thread] None [] nextprefix initial_seenpcs. (* initial state for the PikeVM which operates in anchored fashion *) Definition pike_vm_initial_state (inp:input) : pike_vm_state := @@ -162,78 +189,78 @@ Definition pike_vm_initial_state (inp:input) : pike_vm_state := (* small-step semantics for the PikeVM algorithm *) -Inductive pike_vm_step (c:code): pike_vm_state -> pike_vm_state -> Prop := +Variant pike_vm_step (c:code) (dir:Direction): pike_vm_state -> pike_vm_state -> Prop := | pvs_final: (* moving to a final state when there are no more active or blocked threads *) forall inp best seen, - pike_vm_step c (PVS inp [] best [] None seen) (PVS_final best) + pike_vm_step c dir (PVS inp [] best [] None seen) (PVS_final best) | pvs_acc: (* if there are no more active or blocked threads and we know where the next prefix matches, *) (* we accelerate to that point *) forall inp best n lit strs nextinp seen - (ADVANCE: advance_input_n inp (S n) forward = nextinp), - pike_vm_step c (PVS inp [] best [] (Some (n, lit, strs)) seen) (PVS nextinp [pike_vm_initial_thread] best [] (next_prefix_counter nextinp lit) initial_seenpcs) + (ADVANCE: advance_input_n inp (S n) dir = nextinp), + pike_vm_step c dir (PVS inp [] best [] (Some (n, lit, strs)) seen) (PVS nextinp [pike_vm_initial_thread] best [] (next_prefix_counter nextinp dir lit) initial_seenpcs) | pvs_end: (* when the list of active is empty and we've reached the end of string *) (* in practice, this rule is never used because we can have no blocked threads *) (* when there is no input left. We keep this rule for convenience in the proofs *) (* and for relating it to the functional version *) forall inp best thr blocked nextprefix seen - (ADVANCE: advance_input inp forward = None), - pike_vm_step c (PVS inp [] best (thr::blocked) nextprefix seen) (PVS_final best) + (ADVANCE: advance_input inp dir = None), + pike_vm_step c dir (PVS inp [] best (thr::blocked) nextprefix seen) (PVS_final best) | pvs_nextchar: (* when the list of active threads is empty (but not blocked), restart from the blocked ones, proceeding to the next character *) (* reset the set of seen pcs *) forall inp1 inp2 best thr blocked seen - (ADVANCE: advance_input inp1 forward = Some inp2), - pike_vm_step c (PVS inp1 [] best (thr::blocked) None seen) (PVS inp2 (thr::blocked) best [] None initial_seenpcs) + (ADVANCE: advance_input inp1 dir = Some inp2), + pike_vm_step c dir (PVS inp1 [] best (thr::blocked) None seen) (PVS inp2 (thr::blocked) best [] None initial_seenpcs) | pvs_nextchar_generate: (* when the list of active threads is empty (but not blocked), restart from the blocked ones, proceeding to the next character *) (* since the nextprefix counter reached zero, we must also append as lowest priority the initial thread *) (* reset the set of seen pcs *) forall inp1 inp2 best lit strs thr blocked seen - (ADVANCE: advance_input inp1 forward = Some inp2), - pike_vm_step c (PVS inp1 [] best (thr::blocked) (Some (0, lit, strs)) seen) (PVS inp2 ((thr::blocked) ++ [pike_vm_initial_thread]) best [] (next_prefix_counter inp2 lit) initial_seenpcs) + (ADVANCE: advance_input inp1 dir = Some inp2), + pike_vm_step c dir (PVS inp1 [] best (thr::blocked) (Some (0, lit, strs)) seen) (PVS inp2 ((thr::blocked) ++ [pike_vm_initial_thread]) best [] (next_prefix_counter inp2 dir lit) initial_seenpcs) | pvs_nextchar_filter: (* when the list of active threads is empty (but not blocked), restart from the blocked ones, proceeding to the next character *) (* since the nextprefix counter is nonzero, we do not append the initial thread *) (* reset the set of seen pcs *) forall inp1 inp2 best n lit strs thr blocked seen - (ADVANCE: advance_input inp1 forward = Some inp2), - pike_vm_step c (PVS inp1 [] best (thr::blocked) (Some (S n, lit, strs)) seen) (PVS inp2 (thr::blocked) best [] (Some (n, lit, strs)) initial_seenpcs) + (ADVANCE: advance_input inp1 dir = Some inp2), + pike_vm_step c dir (PVS inp1 [] best (thr::blocked) (Some (S n, lit, strs)) seen) (PVS inp2 (thr::blocked) best [] (Some (n, lit, strs)) initial_seenpcs) | pvs_skip: (* when the pc has already been seen at this current index, we skip it entirely *) forall inp t active best blocked nextprefix seen (SEEN: seen_thread seen t = true), - pike_vm_step c (PVS inp (t::active) best blocked nextprefix seen) (PVS inp active best blocked nextprefix seen) + pike_vm_step c dir (PVS inp (t::active) best blocked nextprefix seen) (PVS inp active best blocked nextprefix seen) | pvs_active: (* generated new active threads: add them in front of the low-priority ones *) forall inp t active best blocked nextprefix seen nextactive (UNSEEN: seen_thread seen t = false) - (STEP: epsilon_step t c inp = EpsActive nextactive), - pike_vm_step c (PVS inp (t::active) best blocked nextprefix seen) (PVS inp (nextactive++active) best blocked nextprefix (add_thread seen t)) + (STEP: epsilon_step t c dir inp = EpsActive nextactive), + pike_vm_step c dir (PVS inp (t::active) best blocked nextprefix seen) (PVS inp (nextactive++active) best blocked nextprefix (add_thread seen t)) | pvs_match: (* a match is found, discard remaining low-priority active threads *) forall inp t active best blocked nextprefix seen (UNSEEN: seen_thread seen t = false) - (STEP: epsilon_step t c inp = EpsMatch), - pike_vm_step c (PVS inp (t::active) best blocked nextprefix seen) (PVS inp [] (Some (inp,gm_of t)) blocked None (add_thread seen t)) + (STEP: epsilon_step t c dir inp = EpsMatch), + pike_vm_step c dir (PVS inp (t::active) best blocked nextprefix seen) (PVS inp [] (Some (inp,gm_of t)) blocked None (add_thread seen t)) | pvs_blocked: (* add the new blocked thread after the previous ones *) forall inp t active best blocked nextprefix seen newt (UNSEEN: seen_thread seen t = false) - (STEP: epsilon_step t c inp = EpsBlocked newt), - pike_vm_step c (PVS inp (t::active) best blocked nextprefix seen) (PVS inp active best (blocked ++ [newt]) nextprefix (add_thread seen t)). + (STEP: epsilon_step t c dir inp = EpsBlocked newt), + pike_vm_step c dir (PVS inp (t::active) best blocked nextprefix seen) (PVS inp active best (blocked ++ [newt]) nextprefix (add_thread seen t)). (** * PikeVM properties *) Theorem pikevm_deterministic: - forall c pvso pvs1 pvs2 - (STEP1: pike_vm_step c pvso pvs1) - (STEP2: pike_vm_step c pvso pvs2), + forall c dir pvso pvs1 pvs2 + (STEP1: pike_vm_step c dir pvso pvs1) + (STEP2: pike_vm_step c dir pvso pvs2), pvs1 = pvs2. Proof. - intros c pvso pvs1 pvs2 STEP1 STEP2. inversion STEP1; subst. + intros c dir pvso pvs1 pvs2 STEP1 STEP2. inversion STEP1; subst. - inversion STEP2; subst; auto. - inversion STEP2; subst; auto. - inversion STEP2; subst; auto; rewrite ADVANCE in ADVANCE0; inversion ADVANCE0. @@ -253,17 +280,17 @@ Proof. Qed. Theorem pikevm_progress: - forall c inp active best blocked nextprefix seen, + forall c dir inp active best blocked nextprefix seen, exists pvs_next, - pike_vm_step c (PVS inp active best blocked nextprefix seen) pvs_next. + pike_vm_step c dir (PVS inp active best blocked nextprefix seen) pvs_next. Proof. - intros c inp active best blocked nextprefix seen. + intros c dir inp active best blocked nextprefix seen. destruct active as [|[[pc gm] b] active]. - destruct blocked as [|t blocked]. + destruct nextprefix. * destruct p as [[n lit] strs]. eexists. now apply pvs_acc. * eexists. apply pvs_final. - + destruct (advance_input inp forward) eqn:INP. + + destruct (advance_input inp dir) eqn:INP. * destruct nextprefix. -- destruct p as [[n lit] strs], n. ++ eexists. apply pvs_nextchar_generate. eauto. @@ -272,10 +299,175 @@ Proof. * eexists. apply pvs_end. eauto. - destruct (seen_thread seen (pc,gm,b)) eqn:SEEN. { eexists. apply pvs_skip. auto. } - destruct (epsilon_step (pc,gm,b) c inp) eqn:EPS. + destruct (epsilon_step (pc,gm,b) c dir inp) eqn:EPS. + eexists. apply pvs_active; eauto. + eexists. apply pvs_match; eauto. + eexists. apply pvs_blocked; eauto. Qed. +(** Backward direction *) + +(* All proofs about the PikeVM will reason about the forward direction. *) +(* Running the PikeVM in the backward direction means that characters *) +(* are processed right-to-left rather than left-to-right. This direction *) +(* mimics reversing the input which we want to avoid due to it being *) +(* expensive. *) +(* Here, we define the result of the backward direction in terms of the *) +(* forward direction. We essentially reverse everything refering to *) +(* the input. *) + +Definition leaf_reverse (o: option leaf) : option leaf := + match o with + | None => None + | Some (inp, gm) => Some (input_reverse inp, gm) + end. + +Definition direction_reverse (dir: Direction) : Direction := + match dir with + | forward => backward + | backward => forward + end. + +Definition pvs_reverse (pvs: pike_vm_state) : pike_vm_state := + match pvs with + | PVS inp active best blocked nextprefix seen => PVS (input_reverse inp) active (leaf_reverse best) blocked nextprefix seen + | PVS_final best => PVS_final (leaf_reverse best) + end. + +Notation involutive f := (forall x, f (f x) = x). + +Lemma map_map_involutive {A}: forall (f : A -> A) l, + involutive f -> + map f (map f l) = l. +Proof. + intros f l invo. + rewrite map_map. + induction l. + - reflexivity. + - simpl. now rewrite invo, IHl. +Qed. + +Lemma flip_anchor_involutive : involutive flip_anchor. +Proof. now destruct x. Qed. + +Lemma direction_reverse_involutive : involutive direction_reverse. +Proof. now destruct x. Qed. + +Lemma leaf_reverse_involutive : involutive leaf_reverse. +Proof. + destruct x as [[inp gm]|]; simpl; now rewrite ?input_reverse_involutive. +Qed. + +Lemma pvs_reverse_involutive : involutive pvs_reverse. +Proof. + destruct x as [inp active best blocked nextprefix seen|best]; simpl. + - now rewrite input_reverse_involutive, leaf_reverse_involutive. + - now rewrite leaf_reverse_involutive. +Qed. + +Lemma advance_input_reverse_none : forall inp dir, + advance_input inp dir = None <-> advance_input (input_reverse inp) (direction_reverse dir) = None. +Proof. + intros [next pref] dir. + split; intros; now destruct dir, next, pref. +Qed. + +Lemma advance_input_reverse_some : forall inp dir inp', + advance_input inp dir = Some inp' <-> advance_input (input_reverse inp) (direction_reverse dir) = Some (input_reverse inp'). +Proof. + intros [next pref] dir inp'. + split; intros. + - destruct dir, next, pref; discriminate || now injection H as <-. + - destruct dir, next, pref; simpl in *; try discriminate; + inversion H; + eapply f_equal with (f:=input_reverse) in H1; + simpl in H1; + now rewrite H1, input_reverse_involutive. +Qed. + +Lemma advance_input_n_reverse : forall inp dir n, + advance_input_n inp n dir = input_reverse (advance_input_n (input_reverse inp) n (direction_reverse dir)). +Proof. + intros [next pref]. now destruct dir. +Qed. + +Lemma check_read_reverse : + forall cd inp dir, + check_read rer cd inp dir = check_read rer cd (input_reverse inp) (direction_reverse dir). +Proof. + intros ? [next pref]. now destruct dir. +Qed. + +Lemma anchor_satisfied_reverse : + forall a inp, + anchor_satisfied rer a inp = anchor_satisfied rer (flip_anchor a) (input_reverse inp). +Proof. + intros a [next pref]. destruct a, next, pref; simpl; reflexivity || now rewrite Bool.xorb_comm. +Qed. + +Lemma idx_dir_reverse : forall inp dir, + idx_dir inp dir = idx_dir (input_reverse inp) (direction_reverse dir). +Proof. + intros [next pref]. now destruct dir. +Qed. + +Lemma epsilon_step_reverse : + forall t c dir inp, + epsilon_step t c dir inp = epsilon_step t c (direction_reverse dir) (input_reverse inp). +Proof. + intros [[pc gm] b] c dir inp. + simpl. destruct get_pc as [inst|]; [|reflexivity]; destruct inst; try easy. + - now rewrite check_read_reverse. + - unfold anchor_dir. destruct dir; now rewrite anchor_satisfied_reverse, ?flip_anchor_involutive. + - now rewrite idx_dir_reverse. + - now rewrite idx_dir_reverse. +Qed. + +Lemma next_prefix_counter_reverse {strs:StrSearch}: + forall inp dir lit, + next_prefix_counter inp dir lit = next_prefix_counter (input_reverse inp) (direction_reverse dir) lit. +Proof. + now destruct dir, inp as [[|c next] [|c' pref]]. +Qed. + +Hint Rewrite + flip_anchor_involutive + direction_reverse_involutive + leaf_reverse_involutive + pvs_reverse_involutive + input_reverse_involutive + epsilon_step_reverse : invo. + +Tactic Notation "reverse" := autorewrite with invo using try (easy || congruence). + +(* the PikeVM in a forward direction corresponds to a mapped version in the backward direction *) +Lemma pikevm_step_reverse : + forall c dir pvs pvs_next1 pvs_next2, + pike_vm_step c dir pvs pvs_next1 -> + pike_vm_step c (direction_reverse dir) (pvs_reverse pvs) pvs_next2 -> + pvs_next1 = pvs_reverse pvs_next2. +Proof. + intros c dir pvs pvs_next1 pvs_next2 H1 H2. + inversion H1; subst; simpl in *. + - inversion H2; subst. simpl. reverse. + - inversion H2; subst. simpl. + f_equal; reverse. + + apply advance_input_n_reverse. + + now rewrite next_prefix_counter_reverse, advance_input_n_reverse, input_reverse_involutive. + - inversion H2; subst; simpl; reverse; rewrite advance_input_reverse_none in ADVANCE; congruence. + - inversion H2; subst; simpl; rewrite advance_input_reverse_some in ADVANCE; try congruence. + rewrite ADVANCE0 in ADVANCE; injection ADVANCE as ->. + reverse. + - inversion H2; subst; simpl; rewrite advance_input_reverse_some in ADVANCE; try congruence. + rewrite ADVANCE0 in ADVANCE; injection ADVANCE as ->. + f_equal; reverse; eauto using next_prefix_counter_reverse. + - inversion H2; subst; simpl; rewrite advance_input_reverse_some in ADVANCE; try congruence. + rewrite ADVANCE0 in ADVANCE; injection ADVANCE as ->. + reverse. + - inversion H2; subst; simpl; reverse. + - inversion H2; subst; simpl; reverse; rewrite epsilon_step_reverse in STEP; congruence. + - inversion H2; subst; simpl; reverse; rewrite epsilon_step_reverse in STEP; congruence. + - inversion H2; subst; simpl; reverse; rewrite epsilon_step_reverse in STEP; congruence. +Qed. + End PikeVM. diff --git a/Semantics/Chars.v b/Semantics/Chars.v index 67330721..9b092216 100644 --- a/Semantics/Chars.v +++ b/Semantics/Chars.v @@ -68,6 +68,13 @@ Section Chars. Definition init_input (str:string) : input := Input str []. + Definition input_reverse (i: input) : input := + let '(Input next pref) := i in + Input pref next. + + Lemma input_reverse_involutive : forall i, input_reverse (input_reverse i) = i. + Proof. now destruct i. Qed. + (* Definition of when an input is compatible with (i.e. represents) a given input string str0. *) Inductive input_compat: input -> string -> Prop := From 902a5f8f76f227bac8864305a668b3e393489014 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 17 Mar 2026 21:27:14 +0100 Subject: [PATCH 2/3] Engine: prove complexity for both directions of PikeVM --- Engine/Complexity.v | 228 +++++++++++++++++++------------------- Engine/FunctionalPikeVM.v | 8 +- 2 files changed, 117 insertions(+), 119 deletions(-) diff --git a/Engine/Complexity.v b/Engine/Complexity.v index 0a4db20b..534b4923 100644 --- a/Engine/Complexity.v +++ b/Engine/Complexity.v @@ -329,50 +329,57 @@ Section SearchRange. Context {params: LindenParameters}. (* we add 1 because we consider that even at the last position, there is work to do to reach the final state *) - Definition inpsize (i:input) : nat := - match i with - | Input next pref => 1 + length next + Definition inpsize (i:input) (dir:Direction) : nat := + let 'Input next pref := i in + match dir with + | forward => 1 + length next + | backward => 1 + length pref end. Lemma inpsize_strict: - forall i, inpsize i > 0. + forall i dir, inpsize i dir > 0. Proof. - intros [next pref]. simpl. lia. + intros [next pref] dir. simpl. destruct dir; lia. Qed. Lemma advance_input_decreases: - forall i1 i2, - advance_input i1 forward = Some i2 -> - inpsize i2 < inpsize i1. + forall i1 i2 dir, + advance_input i1 dir = Some i2 -> + inpsize i2 dir < inpsize i1 dir. Proof. - intros [n1 p1] [n2 p2] H. simpl in H. destruct n1 as [|h1 n1]; inversion H; subst. simpl. lia. + intros [n1 p1] [n2 p2] [|] H; simpl in *. + - destruct n1; inversion H; subst. simpl. lia. + - destruct p1; inversion H; subst. simpl. lia. Qed. (** * Next prefix search is in range *) Theorem search_in_range: - forall inp lit n lit' (strs:StrSearch) strs', - @next_prefix_counter _ strs inp forward lit = Some (n, lit', strs') -> - inpsize inp > S n. + forall inp lit n lit' (strs:StrSearch) strs' dir, + @next_prefix_counter _ strs inp dir lit = Some (n, lit', strs') -> + inpsize inp dir > S n. Proof. - intros [next pref] lit n lit' strs strs' H. unfold next_prefix_counter in H. - destruct next; simpl in H. inversion H. - destruct str_search eqn:SEARCH; inversion H; subst. - apply str_search_bound in SEARCH. simpl. lia. + intros [next pref] lit n lit' strs strs' dir H. unfold next_prefix_counter in H. + destruct dir. + - destruct next; simpl in H. inversion H. + destruct str_search eqn:SEARCH; inversion H; subst. + apply str_search_bound in SEARCH. simpl. lia. + - destruct pref; simpl in H. inversion H. + destruct str_search eqn:SEARCH; inversion H; subst. + apply str_search_bound in SEARCH. simpl. lia. Qed. Lemma advance_inpsize: - forall inp1 inp2 n, - advance_input inp1 forward = Some inp2 -> - inpsize inp1 > S n -> - inpsize inp2 > n. + forall inp1 inp2 n dir, + advance_input inp1 dir = Some inp2 -> + inpsize inp1 dir > S n -> + inpsize inp2 dir > n. Proof. - intros [next1 pref1] inp2 n H H0. simpl in H. - destruct next1; inversion H. - simpl in H0. simpl. lia. + intros [next1 pref1] inp2 n dir H H0. simpl in H. + destruct dir, next1, pref1; inversion H; simpl in H0 |- *; lia. Qed. - Lemma advance_S_n: + Lemma advance_S_n_forward: forall n next pref c, advance_input_n (Input (c::next) pref) (S n) forward = advance_input_n (Input next (c::pref)) n forward. @@ -380,19 +387,32 @@ Section SearchRange. intros n next pref c. simpl. f_equal. rewrite <- app_assoc. auto. Qed. + Lemma advance_S_n_backward: + forall n next pref c, + advance_input_n (Input next (c::pref)) (S n) backward = + advance_input_n (Input (c::next) pref) n backward. + Proof. + intros n next pref c. simpl. f_equal. rewrite <- app_assoc. auto. + Qed. + Lemma advance_n_inpsize: - forall inp n, - inpsize inp > S n -> - inpsize (advance_input_n inp (S n) forward) < inpsize inp. + forall inp n dir, + inpsize inp dir > S n -> + inpsize (advance_input_n inp (S n) dir) dir < inpsize inp dir. Proof. - intros [next pref] n H. + intros [next pref] n dir H. generalize dependent next. generalize dependent pref. induction n; intros. - - unfold advance_input_n. destruct next; simpl in H; simpl; lia. - - destruct next as [|c next]; simpl in H. lia. - assert (S (length next) > S n) by lia. - specialize (IHn (c::pref) next H0). rewrite advance_S_n. - simpl in IHn. simpl. lia. + - unfold advance_input_n. destruct dir, next, pref; simpl in H; simpl; lia. + - destruct dir. + + destruct next as [|c next]; simpl in H. lia. + assert (S (length next) > S n) by lia. + specialize (IHn (c::pref) next H0). rewrite advance_S_n_forward. + simpl in IHn. simpl. lia. + + destruct pref as [|c pref]; simpl in H. lia. + assert (S (length pref) > S n) by lia. + specialize (IHn pref (c::next) H0). rewrite advance_S_n_backward. + simpl in IHn. simpl. lia. Qed. End SearchRange. @@ -583,13 +603,13 @@ Section PikeVMComplexity. (* As we change characters, the seen set might get 2*codesize new free slots (multiplied by 2 for the measure) *) (* But the input decreases, which makes the measure also decrease, because input size is multiplied by (2 + 4*codesize) *) (* It's (2 + 4*codesize) because we might generate a new thread at each input (for unanchored search) and because of the step it takes to advance *) - Definition measure (codesize:nat) (dist:list (nat*LoopBool)) (active blocked:list thread) (inp:input) := - (2 * free codesize dist) + length active + length blocked + (inpsize inp * (2 + 4 * codesize)). + Definition measure (codesize:nat) (dist:list (nat*LoopBool)) (active blocked:list thread) (inp:input) (dir:Direction) := + (2 * free codesize dist) + length active + length blocked + (inpsize inp dir * (2 + 4 * codesize)). (* The invariant that is preserved through pikeVM execution, with a measure that strictly decreases *) - Inductive vm_inv (c:code): pike_vm_state -> nat -> Prop := + Inductive vm_inv (c:code) (dir:Direction): pike_vm_state -> nat -> Prop := | inv_final: - forall b, vm_inv c (PVS_final b) 0 + forall b, vm_inv c dir (PVS_final b) 0 | inv_pvs: forall inp active best blocked nextprefix seen dist (* the threads in active and blocked have their pc inside the code range *) @@ -598,15 +618,15 @@ Section PikeVMComplexity. (* the seen set is well-formed, and has `count` distinct elements *) (SEENWF: wf seen (size c) dist) (* The next place where the prefix can match is in range of the input *) - (RANGEPREF: forall n lit strs, nextprefix = Some (n, lit, strs) -> inpsize inp > S n), - vm_inv c (PVS inp active best blocked nextprefix seen) (measure (size c) dist active blocked inp). + (RANGEPREF: forall n lit strs, nextprefix = Some (n, lit, strs) -> inpsize inp dir > S n), + vm_inv c dir (PVS inp active best blocked nextprefix seen) (measure (size c) dist active blocked inp dir). Lemma nonfinal_pos: - forall c inp active best blocked nextprefix seen m, - vm_inv c (PVS inp active best blocked nextprefix seen) m -> 0 < m. + forall c dir inp active best blocked nextprefix seen m, + vm_inv c dir (PVS inp active best blocked nextprefix seen) m -> 0 < m. Proof. - intros c inp active best blocked nextprefix seen m H. inversion H. subst. unfold measure. - specialize (inpsize_strict inp) as SIZE. lia. + intros c dir inp active best blocked nextprefix seen m H. inversion H. subst. unfold measure. + specialize (inpsize_strict inp dir) as SIZE. lia. Qed. @@ -640,14 +660,14 @@ Section PikeVMComplexity. (* at each step, the measure strictly decreases *) (* the well-formedness of the seen set is preserved *) Theorem pikevm_decreases: - forall code pvs1 pvs2 m1, + forall code dir pvs1 pvs2 m1, code_wf code (size code) -> nonempty code -> - pike_vm_step rer code forward pvs1 pvs2 -> - vm_inv code pvs1 m1 -> - exists m2, vm_inv code pvs2 m2 /\ m2 < m1. + pike_vm_step rer code dir pvs1 pvs2 -> + vm_inv code dir pvs1 m1 -> + exists m2, vm_inv code dir pvs2 m2 /\ m2 < m1. Proof. - intros code pvs1 pvs2 m1 CODEWF NONEMPTY STEP INV. inversion STEP; subst; simpl measure; inversion INV; subst; + intros code dir pvs1 pvs2 m1 CODEWF NONEMPTY STEP INV. inversion STEP; subst; simpl measure; inversion INV; subst; try destruct t as [[pc gm] b]. (* when reaching a final state, we end up with a measure of 0, while the previous measure was strictly positive *) - exists 0. split. @@ -655,26 +675,26 @@ Section PikeVMComplexity. + apply nonfinal_pos in INV. auto. (* acc: we might add (2*codesize) free slots, but we lose at least one input length *) - specialize (RANGEPREF n lit strs eq_refl). - exists (measure (size code) [] [pike_vm_initial_thread] [] (advance_input_n inp (S n) forward)). split; [constructor|]; auto. + exists (measure (size code) [] [pike_vm_initial_thread] [] (advance_input_n inp (S n) dir) dir). split; [constructor|]; auto. + (* the new generated thread is in range because the code is nonempty *) intros t H. inversion H as [IN1|IN2]; auto. subst. unfold pike_vm_initial_thread. simpl. auto. + constructor. + intros n0 lit0 strs0 H. eapply search_in_range with (strs:=strs); eauto. - + unfold measure. simpl. rewrite free_initial. specialize (advance_n_inpsize inp n RANGEPREF)as ADV. + + unfold measure. simpl. rewrite free_initial. specialize (advance_n_inpsize inp n dir RANGEPREF)as ADV. apply increase_mult with (x:= 4 * size code) in ADV as NEXT. simpl in NEXT. lia. (* end *) - exists 0. split. + constructor. + apply nonfinal_pos in INV. auto. (* nextchar: we might add (2*codesize) free slots, but we lose an input length *) - - exists (measure (size code) [] (thr::blocked) [] inp2). split; [constructor|]; auto. + - exists (measure (size code) [] (thr::blocked) [] inp2 dir). split; [constructor|]; auto. + constructor. + intros n lit strs H; inversion H. + unfold measure. simpl. rewrite free_initial. apply advance_input_decreases in ADVANCE. apply increase_mult with (x:= 4 * size code) in ADVANCE as NEXT. simpl in NEXT. lia. (* nextchar_generate: we might add (2*codesize) free slots, but we lose an input length *) - - exists (measure (size code) [] ((thr::blocked)++[pike_vm_initial_thread]) [] inp2). split; [constructor|]; auto. + - exists (measure (size code) [] ((thr::blocked)++[pike_vm_initial_thread]) [] inp2 dir). split; [constructor|]; auto. + (* the new generated thread is in range because the code is nonempty *) intros t H. apply in_app_or in H as [IN1|IN2]; auto. inversion IN2; inversion H. unfold pike_vm_initial_thread. simpl. auto. @@ -684,20 +704,20 @@ Section PikeVMComplexity. apply increase_mult with (x:= 4 * size code) in ADVANCE as NEXT. simpl in NEXT. rewrite length_app. simpl. lia. (* nextchar_filter: we might add (2*codesize) free slots, but we lose an input length *) - - exists (measure (size code) [] (thr::blocked) [] inp2). split; [constructor|]; auto. + - exists (measure (size code) [] (thr::blocked) [] inp2 dir). split; [constructor|]; auto. + constructor. + intros n0 lit0 strs0 H. inversion H; subst. specialize (RANGEPREF (S n0) lit0 strs0 eq_refl). eapply advance_inpsize; eauto. + unfold measure. simpl. rewrite free_initial. apply advance_input_decreases in ADVANCE. apply increase_mult with (x:= 4 * size code) in ADVANCE as NEXT. simpl in NEXT. lia. (* skip: we lose a thread *) - - exists (measure (size code) dist active blocked inp). split; [constructor|]; auto. + - exists (measure (size code) dist active blocked inp dir). split; [constructor|]; auto. + intros t0 H. apply ACTIVEWF. simpl. right. auto. + unfold measure. simpl. lia. (* active: we may add a new thread, but lose a free slot *) - assert (RANGE: pc < size code). { specialize (ACTIVEWF (pc,gm,b) ltac:(simpl;left;auto)). simpl in ACTIVEWF. auto. } - exists (measure (size code) ((pc,b)::dist) (nextactive++active) blocked inp). split; [constructor|]; auto. + exists (measure (size code) ((pc,b)::dist) (nextactive++active) blocked inp dir). split; [constructor|]; auto. + intros t0 H. apply in_app_or in H as [H|H]. * eapply eps_step_active_wf in STEP0 as [i [GET IN]]; eauto. * apply ACTIVEWF. right. auto. @@ -708,7 +728,7 @@ Section PikeVMComplexity. (* match: we lose a thread and a free slot *) - assert (RANGE: pc < size code). { specialize (ACTIVEWF (pc,gm,b) ltac:(simpl;left;auto)). simpl in ACTIVEWF. auto. } - exists (measure (size code) ((pc,b)::dist) [] blocked inp). split; [constructor|]; auto. + exists (measure (size code) ((pc,b)::dist) [] blocked inp dir). split; [constructor|]; auto. + intros t0 H. inversion H. + unfold add_thread. apply wf_new; auto. + intros n lit strs H; inversion H. @@ -717,7 +737,7 @@ Section PikeVMComplexity. (* blocked: we switch an active thread to blocked, but lose a free slot *) - assert (RANGE: pc < size code). { specialize (ACTIVEWF (pc,gm,b) ltac:(simpl;left;auto)). simpl in ACTIVEWF. auto. } - exists (measure (size code) ((pc,b)::dist) active (blocked++[newt]) inp). split; [constructor|]; auto. + exists (measure (size code) ((pc,b)::dist) active (blocked++[newt]) inp dir). split; [constructor|]; auto. + intros t0 H. apply ACTIVEWF. simpl. right. auto. + intros t0 H. apply in_app_or in H as [H|H]. * eapply BLOCKEDWF; eauto. @@ -731,16 +751,16 @@ Section PikeVMComplexity. (** * Initial PikeVM Measure *) - Definition complexity (r:regex) (inp:input) : nat := - 1 + (4 * codesize r) + (inpsize inp * (2 + 4 * codesize r)). + Definition complexity (r:regex) (inp:input) (dir:Direction): nat := + 1 + (4 * codesize r) + (inpsize inp dir * (2 + 4 * codesize r)). Theorem initial_measure: - forall inp r, + forall inp r dir, pike_regex r -> - vm_inv (compilation r) (pike_vm_initial_state inp) (complexity r inp). + vm_inv (compilation r) dir (pike_vm_initial_state inp) (complexity r inp dir). Proof. - intros inp r SUBSET. - replace (complexity r inp) with (measure (codesize r) [] [(0, GroupMap.empty, CanExit)] [] inp). + intros inp r dir SUBSET. + replace (complexity r inp dir) with (measure (codesize r) [] [(0, GroupMap.empty, CanExit)] [] inp dir). - unfold pike_vm_initial_state. rewrite <- compilation_size; auto. constructor; auto. + intros t H. destruct H. 2: inversion H. @@ -754,12 +774,12 @@ Section PikeVMComplexity. Qed. Theorem initial_measure_unanchored {strs:StrSearch}: - forall inp r, + forall inp r dir, pike_regex r -> - vm_inv (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp forward) (complexity r inp). + vm_inv (compilation r) dir (pike_vm_initial_state_unanchored (extract_literal rer r) inp dir) (complexity r inp dir). Proof. - intros inp r SUBSET. - replace (complexity r inp) with (measure (codesize r) [] [(0, GroupMap.empty, CanExit)] [] inp). + intros inp r dir SUBSET. + replace (complexity r inp dir) with (measure (codesize r) [] [(0, GroupMap.empty, CanExit)] [] inp dir). - unfold pike_vm_initial_state_unanchored. rewrite <- compilation_size; auto. constructor; auto. + intros t H. destruct H. 2: inversion H. @@ -772,57 +792,40 @@ Section PikeVMComplexity. rewrite free_initial. simpl. lia. Qed. - Axiom initial_measure_unanchored_backward : - forall {strs:StrSearch} inp r , - pike_regex r -> - vm_inv (compilation r) (pike_vm_initial_state_unanchored (extract_literal rer r) inp backward) (complexity r inp). - (** * Bounding the number of PikeVM steps *) Lemma pike_vm_bound: - forall pvs code n, + forall pvs code dir n, code_wf code (size code) -> nonempty code -> - vm_inv code pvs n -> - exists result, steps (pike_vm_step rer code forward) pvs n (PVS_final result). + vm_inv code dir pvs n -> + exists result, steps (pike_vm_step rer code dir) pvs n (PVS_final result). Proof. - intros pvs code n WF NONEMPTY INV. generalize dependent pvs. induction n using (strong_ind); intros. + intros pvs code dir n WF NONEMPTY INV. generalize dependent pvs. induction n using (strong_ind); intros. destruct pvs. 2: { exists best. constructor. } - specialize (pikevm_progress rer code forward inp active best blocked nextprefix seen) as [next STEP]. - specialize (pikevm_decreases code (PVS inp active best blocked nextprefix seen) next n WF NONEMPTY STEP INV) as [newm [INV2 DECR]]. + specialize (pikevm_progress rer code dir inp active best blocked nextprefix seen) as [next STEP]. + specialize (pikevm_decreases code dir (PVS inp active best blocked nextprefix seen) next n WF NONEMPTY STEP INV) as [newm [INV2 DECR]]. specialize (H newm DECR next INV2) as [result STEPS]. exists result. apply more_steps with (n:=S newm); try lia. econstructor; eauto. Qed. - Axiom pike_vm_bound_backward: - forall pvs code n, - code_wf code (size code) -> - nonempty code -> - vm_inv code pvs n -> - exists result, steps (pike_vm_step rer code backward) pvs n (PVS_final result). - (** * Complexity Theorem *) Theorem pikevm_complexity: forall (r:regex) (inp:input) (dir:Direction), (* for any supported regex r and input inp *) pike_regex r -> - (* The initial state reaches a final state in at most (complexity r inp) steps. *) + (* The initial state reaches a final state in at most (complexity r inp dir) steps. *) exists result, steps (pike_vm_step rer (compilation r) dir) - (pike_vm_initial_state inp) (complexity r inp) (PVS_final result). + (pike_vm_initial_state inp) (complexity r inp dir) (PVS_final result). Proof. intros r inp dir SUBSET. - destruct dir. - - apply pike_vm_bound. - + apply compiled_wf. - + apply compilation_nonempty. - + apply initial_measure. auto. - - apply pike_vm_bound_backward. - + apply compiled_wf. - + apply compilation_nonempty. - + apply initial_measure. auto. + apply pike_vm_bound. + - apply compiled_wf. + - apply compilation_nonempty. + - apply initial_measure. auto. Qed. Theorem pikevm_complexity_unanchored {strs:StrSearch}: @@ -831,18 +834,13 @@ Section PikeVMComplexity. pike_regex r -> (* The initial state reaches a final state in at most (complexity r inp) steps. *) exists result, steps (pike_vm_step rer (compilation r) dir) - (pike_vm_initial_state_unanchored (extract_literal rer r) inp dir) (complexity r inp) (PVS_final result). + (pike_vm_initial_state_unanchored (extract_literal rer r) inp dir) (complexity r inp dir) (PVS_final result). Proof. intros r inp dir SUBSET. - destruct dir. - - apply pike_vm_bound. - + apply compiled_wf. - + apply compilation_nonempty. - + apply initial_measure_unanchored; auto. - - apply pike_vm_bound_backward. - + apply compiled_wf. - + apply compilation_nonempty. - + apply initial_measure_unanchored_backward; auto. + apply pike_vm_bound. + - apply compiled_wf. + - apply compilation_nonempty. + - apply initial_measure_unanchored; auto. Qed. @@ -992,7 +990,7 @@ Section MemoBTComplexity. Lemma possible_sufsize: forall next pref, - length (possible_suffixes next pref) = inpsize (Input next pref). + length (possible_suffixes next pref) = inpsize (Input next pref) forward. Proof. induction next; intros; simpl; auto. Qed. Lemma no_more_strict_suffix: @@ -1022,7 +1020,7 @@ Section MemoBTComplexity. Lemma possible_memosize: forall next pref sizec, - length (possible_memo next pref sizec) = 2 * sizec * inpsize (Input next pref). + length (possible_memo next pref sizec) = 2 * sizec * inpsize (Input next pref) forward. Proof. intros. unfold possible_memo. erewrite flat_map_constant_length. 2:{ intros x H. apply possible_fixedsize. } @@ -1046,7 +1044,7 @@ Section MemoBTComplexity. (* We have a bound on the numer of distinct elements in a memoset *) Theorem mswf_size: forall ms sizec inp dist, - mswf ms sizec inp dist -> length dist <= 2 * sizec * (inpsize inp). + mswf ms sizec inp dist -> length dist <= 2 * sizec * (inpsize inp) forward. Proof. intros ms size0 [next pref] dist H. rewrite <- possible_memosize. apply NoDup_incl_length. @@ -1106,7 +1104,7 @@ Section MemoBTComplexity. (INPWF: forall pc gm b inp, In (pc, gm, b, inp) stk -> validinp inp originp) (* the seen set is well-formed, and has `count` distinct elements *) (MSWF: mswf ms (size c) originp dist), - memo_inv c originp (MBT stk ms) (memo_measure (size c) (inpsize originp) dist stk). + memo_inv c originp (MBT stk ms) (memo_measure (size c) (inpsize originp forward) dist stk). Lemma memo_nonfinal_pos: forall c originp stk ms m, @@ -1172,7 +1170,7 @@ Section MemoBTComplexity. + econstructor. eauto. + eapply memo_nonfinal_pos; eauto. (* skip *) - - exists (memo_measure (size code) (inpsize originp) dist stk). split. + - exists (memo_measure (size code) (inpsize originp forward) dist stk). split. + constructor; auto. * intros. eapply PCWF; eauto. right. eauto. * intros. eapply INPWF; eauto. right. eauto. @@ -1186,7 +1184,7 @@ Section MemoBTComplexity. { eapply PCWF. left. eauto. } assert (VAL: validinp i originp). { eapply INPWF. left. eauto. } - exists (memo_measure (size code) (inpsize originp) ((pc,b,i)::dist) (nextconfs++stk)). + exists (memo_measure (size code) (inpsize originp forward) ((pc,b,i)::dist) (nextconfs++stk)). split. + constructor; auto. * intros. apply in_app_iff in H as [H1 | H2]. @@ -1204,7 +1202,7 @@ Section MemoBTComplexity. (** * Initial MemoBT Measure *) Definition mbt_complexity (r:regex) (inp:input) : nat := - 2 + 4 * (codesize r * inpsize inp). + 2 + 4 * (codesize r * inpsize inp forward). Theorem initial_memo_measure: forall inp r ms dist, @@ -1215,10 +1213,10 @@ Section MemoBTComplexity. memo_inv (compilation r) inp (initial_state inp ms) measure. Proof. intros inp r ms dist SUBSET WF. - exists (memo_measure (codesize r) (inpsize inp) dist [(0, GroupMap.empty, CanExit,inp)]). + exists (memo_measure (codesize r) (inpsize inp forward) dist [(0, GroupMap.empty, CanExit,inp)]). split. - unfold memo_measure, mbt_complexity. rewrite <- compilation_size; auto. simpl. - pose proof (msfree_initial_dist (size (compilation r)) (inpsize inp) dist) as FREE. simpl. lia. + pose proof (msfree_initial_dist (size (compilation r)) (inpsize inp forward) dist) as FREE. simpl. lia. - unfold initial_state. rewrite <- compilation_size; auto. constructor; auto. + intros pc gm b inp0 H. inversion H; inversion H0. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite length_app. diff --git a/Engine/FunctionalPikeVM.v b/Engine/FunctionalPikeVM.v index cbff9faa..f96a0c9b 100644 --- a/Engine/FunctionalPikeVM.v +++ b/Engine/FunctionalPikeVM.v @@ -74,8 +74,8 @@ Fixpoint pike_vm_loop (c:code) (dir:Direction) (pvs:pike_vm_state) (fuel:nat) : end. (* an upper bound for the fuel necessary to compute a result *) -Definition vm_fuel (r:regex) (inp:input) : nat := - complexity r inp. +Definition vm_fuel (r:regex) (inp:input) (dir:Direction): nat := + complexity r inp dir. Inductive matchres : Type := | OutOfFuel @@ -90,14 +90,14 @@ Definition getres (pvs:pike_vm_state) : matchres := (* Functional version of the PikeVM *) Definition pike_vm_match (r:regex) (inp:input) (dir:Direction) : matchres := let code := compilation r in - let fuel := vm_fuel r inp in + let fuel := vm_fuel r inp dir in let pvsinit := pike_vm_initial_state inp in getres (pike_vm_loop code dir pvsinit fuel). (* Functional version of the unanchored PikeVM *) Definition pike_vm_match_unanchored {strs:StrSearch} (r:regex) (inp:input) (dir:Direction): matchres := let code := compilation r in - let fuel := vm_fuel r inp in + let fuel := vm_fuel r inp dir in let pvsinit := pike_vm_initial_state_unanchored (extract_literal rer r) inp dir in getres (pike_vm_loop code dir pvsinit fuel). From 1c965e82f959622768d7804cddb49a4ba3aab16f Mon Sep 17 00:00:00 2001 From: shilangyu Date: Thu, 4 Jun 2026 19:54:08 +0200 Subject: [PATCH 3/3] Chore: fix rocq 9.2 issues --- Engine/PikeVM.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Engine/PikeVM.v b/Engine/PikeVM.v index 3b5cb18a..c77ea693 100644 --- a/Engine/PikeVM.v +++ b/Engine/PikeVM.v @@ -334,7 +334,7 @@ Definition pvs_reverse (pvs: pike_vm_state) : pike_vm_state := | PVS_final best => PVS_final (leaf_reverse best) end. -Notation involutive f := (forall x, f (f x) = x). +Abbreviation involutive f := (forall x, f (f x) = x). Lemma map_map_involutive {A}: forall (f : A -> A) l, involutive f -> @@ -430,6 +430,7 @@ Proof. now destruct dir, inp as [[|c next] [|c' pref]]. Qed. +Create Rewrite HintDb invo. Hint Rewrite flip_anchor_involutive direction_reverse_involutive