From be403bbf880a9e800648ddbc06b8c4d65ee1d2d4 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 17 Mar 2026 19:35:54 +0100 Subject: [PATCH 1/5] 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 f2cf32859e358fa7bfb53dc3604c31363389c6de Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 17 Mar 2026 21:27:14 +0100 Subject: [PATCH 2/5] 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 c96617daa4abce94a2409aaa83b7ed17d1dc5574 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Wed, 18 Mar 2026 17:43:18 +0100 Subject: [PATCH 3/5] Engine: add direction to bool_tree --- Engine/BooleanSemantics.v | 280 +++++++++++++++++++++----------------- Engine/Correctness.v | 8 +- Engine/MemoEquiv.v | 33 +++-- Engine/PikeEquiv.v | 58 ++++---- Engine/PikeTree.v | 8 +- Engine/TreeRep.v | 11 +- 6 files changed, 221 insertions(+), 177 deletions(-) diff --git a/Engine/BooleanSemantics.v b/Engine/BooleanSemantics.v index 77e8fcae..5d506acc 100644 --- a/Engine/BooleanSemantics.v +++ b/Engine/BooleanSemantics.v @@ -31,88 +31,88 @@ Section BooleanSemantics. (** * Boolean Semantics *) (* where checks consult the boolean instead of actually comparing strings *) - Inductive bool_tree: actions -> input -> LoopBool -> tree -> Prop := + Inductive bool_tree: actions -> input -> LoopBool -> Direction -> tree -> Prop := | tree_done: (* nothing to do on an empty list of actions *) - forall inp b, - bool_tree [] inp b Match + forall inp b dir, + bool_tree [] inp b dir Match | tree_check: (* pops a successful check from the action list *) (* NEW: this only checks the boolean allows exit and not the strcheck in the tree *) - forall inp strcheck cont treecont - (TREECONT: bool_tree cont inp CanExit treecont), - bool_tree (Acheck strcheck :: cont) inp CanExit (Progress treecont) + forall inp strcheck cont treecont dir + (TREECONT: bool_tree cont inp CanExit dir treecont), + bool_tree (Acheck strcheck :: cont) inp CanExit dir (Progress treecont) | tree_check_fail: (* pops a failing check from the action list *) - forall inp strcheck cont, - bool_tree (Acheck strcheck :: cont) inp CannotExit Mismatch + forall inp strcheck cont dir, + bool_tree (Acheck strcheck :: cont) inp CannotExit dir Mismatch | tree_close: (* pops the closing of a group from the action list *) - forall inp b cont treecont gid - (TREECONT: bool_tree cont inp b treecont), - bool_tree (Aclose gid :: cont) inp b (GroupAction (Close gid) treecont) + forall inp b cont treecont gid dir + (TREECONT: bool_tree cont inp b dir treecont), + bool_tree (Aclose gid :: cont) inp b dir (GroupAction (Close gid) treecont) | tree_epsilon: - forall inp b cont tcont - (ISTREE: bool_tree cont inp b tcont), - bool_tree ((Areg Epsilon)::cont) inp b tcont + forall inp b cont tcont dir + (ISTREE: bool_tree cont inp b dir tcont), + bool_tree ((Areg Epsilon)::cont) inp b dir tcont | tree_char: - forall c cd inp b nextinp cont tcont - (READ: read_char rer cd inp forward = Some (c, nextinp)) + forall c cd inp b nextinp cont tcont dir + (READ: read_char rer cd inp dir = Some (c, nextinp)) (* NEW: changes the boolean to CanExit *) - (TREECONT: bool_tree cont nextinp CanExit tcont), - bool_tree (Areg (Regex.Character cd) :: cont) inp b (Read c tcont) + (TREECONT: bool_tree cont nextinp CanExit dir tcont), + bool_tree (Areg (Regex.Character cd) :: cont) inp b dir (Read c tcont) | tree_char_fail: - forall cd inp b cont - (READ: read_char rer cd inp forward = None), - bool_tree (Areg (Regex.Character cd) :: cont) inp b Mismatch + forall cd inp b cont dir + (READ: read_char rer cd inp dir = None), + bool_tree (Areg (Regex.Character cd) :: cont) inp b dir Mismatch | tree_disj: - forall r1 r2 cont t1 t2 inp b - (ISTREE1: bool_tree (Areg r1 :: cont) inp b t1) - (ISTREE2: bool_tree (Areg r2 :: cont) inp b t2), - bool_tree (Areg (Disjunction r1 r2) :: cont) inp b (Choice t1 t2) + forall r1 r2 cont t1 t2 inp b dir + (ISTREE1: bool_tree (Areg r1 :: cont) inp b dir t1) + (ISTREE2: bool_tree (Areg r2 :: cont) inp b dir t2), + bool_tree (Areg (Disjunction r1 r2) :: cont) inp b dir (Choice t1 t2) | tree_sequence: (* adding next regex to the continuation *) - forall r1 r2 cont t inp b - (CONT: bool_tree (Areg r1 :: Areg r2 :: cont) inp b t), - bool_tree (Areg (Sequence r1 r2) :: cont) inp b t + forall r1 r2 cont t inp b dir + (CONT: bool_tree (seq_list r1 r2 dir ++ cont) inp b dir t), + bool_tree (Areg (Sequence r1 r2) :: cont) inp b dir t | tree_quant_forced: (* the quantifier is forced to iterate, because there is a strictly positive minimum *) - forall r1 greedy min plus cont titer inp b gidl + forall r1 greedy min plus cont titer inp b gidl dir (* the list of capture groups to reset *) (RESET: gidl = def_groups r1) (* doing one iteration *) - (ISTREE1: bool_tree (Areg r1 :: Areg (Quantified greedy min plus r1) :: cont) inp b titer), - bool_tree (Areg (Quantified greedy (S min) plus r1) :: cont) inp b (GroupAction (Reset gidl) titer) + (ISTREE1: bool_tree (Areg r1 :: Areg (Quantified greedy min plus r1) :: cont) inp b dir titer), + bool_tree (Areg (Quantified greedy (S min) plus r1) :: cont) inp b dir (GroupAction (Reset gidl) titer) | tree_quant_done: (* the quantifier is done iterating, because min and max are zero *) - forall r1 greedy cont tskip inp b - (SKIP: bool_tree cont inp b tskip), - bool_tree (Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp b tskip + forall r1 greedy cont tskip inp b dir + (SKIP: bool_tree cont inp b dir tskip), + bool_tree (Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp b dir tskip | tree_quant_free: (* the quantifier is free to iterate or stop *) - forall r1 greedy plus cont titer tskip tquant inp b gidl + forall r1 greedy plus cont titer tskip tquant inp b gidl dir (* the list of capture groups to reset *) (RESET: gidl = def_groups r1) (* doing one iteration, then a check, then executing the next quantifier *) (* NEW: switching the boolean to CannotExit *) - (ISTREE1: bool_tree (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 plus r1) :: cont) inp CannotExit titer) + (ISTREE1: bool_tree (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 plus r1) :: cont) inp CannotExit dir titer) (* skipping the quantifier entirely *) - (SKIP: bool_tree cont inp b tskip) + (SKIP: bool_tree cont inp b dir tskip) (CHOICE: tquant = greedy_choice greedy (GroupAction (Reset gidl) titer) tskip), - bool_tree (Areg (Quantified greedy 0 (NoI.N 1 + plus)%NoI r1) :: cont) inp b tquant + bool_tree (Areg (Quantified greedy 0 (NoI.N 1 + plus)%NoI r1) :: cont) inp b dir tquant | tree_group: - forall r1 cont treecont inp b gid - (TREECONT: bool_tree (Areg r1 :: Aclose gid :: cont) inp b treecont), - bool_tree (Areg (Group gid r1) :: cont) inp b (GroupAction (Open gid) treecont) + forall r1 cont treecont inp b gid dir + (TREECONT: bool_tree (Areg r1 :: Aclose gid :: cont) inp b dir treecont), + bool_tree (Areg (Group gid r1) :: cont) inp b dir (GroupAction (Open gid) treecont) | tree_anchor: - forall a cont treecont inp b + forall a cont treecont inp b dir (ANCHOR: anchor_satisfied rer a inp = true) - (TREECONT: bool_tree cont inp b treecont), - bool_tree (Areg (Anchor a) :: cont) inp b (AnchorPass a treecont) + (TREECONT: bool_tree cont inp b dir treecont), + bool_tree (Areg (Anchor a) :: cont) inp b dir (AnchorPass a treecont) | tree_anchor_fail: - forall a cont inp b + forall a cont inp b dir (ANCHOR: anchor_satisfied rer a inp = false), - bool_tree (Areg (Anchor a) :: cont) inp b Mismatch. + bool_tree (Areg (Anchor a) :: cont) inp b dir Mismatch. (** * Boolean Tree Equivalence *) @@ -124,45 +124,66 @@ Section BooleanSemantics. (** * First Step: encoding the invariant *) -Inductive bool_encoding: LoopBool -> input -> actions -> Prop := +Inductive bool_encoding: LoopBool -> input -> actions -> Direction -> Prop := (* an empty continuation can be encoded with any boolean *) | nil_encode: - forall str b, - bool_encoding b str [] + forall str b dir, + bool_encoding b str [] dir | cons_reg: - forall b str cont r - (ENCODE: bool_encoding b str cont), - bool_encoding b str (Areg r::cont) + forall b str cont r dir + (ENCODE: bool_encoding b str cont dir), + bool_encoding b str (Areg r::cont) dir | cons_close: - forall b str cont gid - (ENCODE: bool_encoding b str cont), - bool_encoding b str (Aclose gid::cont) + forall b str cont gid dir + (ENCODE: bool_encoding b str cont dir), + bool_encoding b str (Aclose gid::cont) dir | cons_true: - forall stk str head - (ENCODE: bool_encoding CanExit str stk) - (STRICT: strict_suffix str head forward), - bool_encoding CanExit str (Acheck head::stk) + forall stk str head dir + (ENCODE: bool_encoding CanExit str stk dir) + (STRICT: strict_suffix str head dir), + bool_encoding CanExit str (Acheck head::stk) dir | cons_false: (* when we push the current string to the stack *) - forall b stk str - (ENCODE: bool_encoding b str stk), - bool_encoding CannotExit str (Acheck str::stk). + forall b stk str dir + (ENCODE: bool_encoding b str stk dir), + bool_encoding CannotExit str (Acheck str::stk) dir. (* when we are already encoded with true, reading a new character preserves this true encoding *) (* when we are encoded with false, reading a new character switches to being encoded with true *) -Lemma true_encoding: +Lemma true_encoding_forward: forall str c pref cont b, - bool_encoding b (Input (c::str) pref) cont -> - bool_encoding CanExit (Input str (c::pref)) cont. + bool_encoding b (Input (c::str) pref) cont forward -> + bool_encoding CanExit (Input str (c::pref)) cont forward. Proof. intros str c pref cont b H. remember (Input (c::str) pref) as prevstr. - induction H; intros. + remember forward as dir. + induction H; intros; subst. - constructor. - constructor; auto. - constructor; auto. - - constructor; auto. rewrite Heqprevstr in STRICT. + - constructor; auto. + eapply ss_next; eauto. simpl. auto. + - constructor. + + apply IHbool_encoding; auto. + + subst. simpl. + eapply ss_advance; eauto. +Qed. + +Lemma true_encoding_backward: + forall str c next cont b, + bool_encoding b (Input next (c::str)) cont backward -> + bool_encoding CanExit (Input (c::next) str) cont backward. +Proof. + intros str c next cont b H. + remember (Input next (c::str)) as nextstr. + remember backward as dir. + induction H; intros; subst. + - constructor. + - constructor; auto. + - constructor; auto. + - constructor; auto. eapply ss_next; eauto. simpl. auto. - constructor. + apply IHbool_encoding; auto. @@ -172,12 +193,12 @@ Qed. (* if the string is different than the check, we know the boolean is true *) Lemma encoding_different: - forall b str strcheck cont, - bool_encoding b str (Acheck strcheck::cont) -> + forall b str strcheck cont dir, + bool_encoding b str (Acheck strcheck::cont) dir -> str <> strcheck -> b = CanExit. Proof. - intros b0 str [strcheck pref] cont H. + intros b0 str [strcheck pref] cont dir H. remember (Acheck (Input strcheck pref)::cont) as prevcont. induction H; intros; auto; inversion Heqprevcont; exfalso; auto. @@ -185,32 +206,32 @@ Qed. (* if the check is going to fail, we know the boolean is false *) Lemma encoding_same: - forall b str cont, - bool_encoding b str (Acheck str::cont) -> b = CannotExit. + forall b str cont dir, + bool_encoding b str (Acheck str::cont) dir -> b = CannotExit. Proof. - intros b str cont H. + intros b str cont dir H. remember (Acheck str::cont) as prevcont. induction H; intros; auto; inversion Heqprevcont. subst. apply ss_neq in STRICT. contradiction. Qed. Lemma encode_next: - forall b inp cont r, - bool_encoding b inp (Areg r::cont) <-> - bool_encoding b inp cont. + forall b inp cont r dir, + bool_encoding b inp (Areg r::cont) dir <-> + bool_encoding b inp cont dir. Proof. - intros b inp cont r. split; intros H. + intros b inp cont r dir. split; intros H. - inversion H; subst. inversion ENCODE; subst; auto. - destruct inp. constructor. inversion H; subst; auto. Qed. Lemma encode_close: - forall b inp cont g, - bool_encoding b inp (Aclose g::cont) <-> - bool_encoding b inp cont. + forall b inp cont g dir, + bool_encoding b inp (Aclose g::cont) dir <-> + bool_encoding b inp cont dir. Proof. - intros b inp cont g. split; intros H. + intros b inp cont g dir. split; intros H. - inversion H; subst. inversion ENCODE; subst; auto. - destruct inp. constructor. inversion H; subst; auto. @@ -220,10 +241,10 @@ Qed. (* Here we encode the invariant that the current input is always either equal or strict suffix of any checks in the current list of actions *) Lemma encoding_suffix: - forall b inp act chk, - bool_encoding b inp act -> + forall b inp act chk dir, + bool_encoding b inp act dir -> In (Acheck chk) act -> - inp = chk \/ strict_suffix inp chk forward. + inp = chk \/ strict_suffix inp chk dir. Proof. intros. induction H. - inversion H0. @@ -239,23 +260,22 @@ Qed. (* the two tree constructions are equal *) Theorem encode_equal: - forall inp cont b t gm + forall inp cont b dir t gm (PIKE: pike_actions cont) - (ENCODE: bool_encoding b inp cont) - (TREE: is_tree rer cont inp gm forward t), - bool_tree cont inp b t. + (ENCODE: bool_encoding b inp cont dir) + (TREE: is_tree rer cont inp gm dir t), + bool_tree cont inp b dir t. Proof. - intros inp cont b t gm PIKE ENCODE TREE. + intros inp cont b dir t gm PIKE ENCODE TREE. generalize dependent b. - remember forward as dir. induction TREE; inversion PIKE; subst; intros; - try solve[constructor; auto]; try solve [inversion H1; inversion H0]. + try solve[constructor; auto]; try solve[inversion H1; inversion H0]. - assert (b = CanExit). { eapply encoding_different; eauto. eapply ss_neq; eauto. } subst. constructor. eapply IHTREE; eauto. inversion ENCODE; subst; auto. - - assert (inp = strcheck \/ strict_suffix inp strcheck forward). + - assert (inp = strcheck \/ strict_suffix inp strcheck dir). { eapply encoding_suffix; eauto. simpl. auto. } destruct H; try contradiction. subst. assert (b = CannotExit). @@ -268,8 +288,11 @@ Proof. - apply encode_next in ENCODE. subst. econstructor; eauto. apply IHTREE; auto. destruct nextinp. destruct inp. simpl in READ. - destruct next0; inversion READ. destruct (char_match rer t cd); inversion READ; subst. - eapply true_encoding; eauto. + destruct dir. + + destruct next0; inversion READ. destruct (char_match rer t cd); inversion READ; subst. + eapply true_encoding_forward; eauto. + + destruct pref0; inversion READ. destruct (char_match rer t cd); inversion READ; subst. + eapply true_encoding_backward; eauto. - apply encode_next in ENCODE. inversion H1. inversion H0. subst. constructor. + apply IHTREE1; auto. { pike_subset. } @@ -277,9 +300,9 @@ Proof. + apply IHTREE2; auto. { pike_subset. } apply encode_next. auto. - - constructor. subst. simpl in IHTREE. apply IHTREE; eauto. - { pike_subset. } - inversion ENCODE; subst; constructor; constructor; auto. + - constructor. apply IHTREE; eauto. + { destruct dir; pike_subset. } + destruct dir; inversion ENCODE; subst; constructor; constructor; auto. - inversion ENCODE. subst. constructor; auto. - destruct (destruct_delta (NoI.N 1 + plus)%NoI) as [DZ | [D1 | [DINF | [delta' [DUN N3]]]]]. (* Zero repetitions *) @@ -313,12 +336,12 @@ Proof. Qed. Corollary boolean_correct: - forall r inp t, + forall r inp dir t, pike_regex r -> - is_tree rer [Areg r] inp GroupMap.empty forward t -> - bool_tree [Areg r] inp CanExit t. + is_tree rer [Areg r] inp GroupMap.empty dir t -> + bool_tree [Areg r] inp CanExit dir t. Proof. - intros r str t PIKE H. + intros r str dir t PIKE H. eapply encode_equal; eauto. { constructor; constructor; auto. } constructor. constructor. @@ -327,15 +350,17 @@ Qed. (* Pike actions translate to Pike trees *) Theorem subset_semantics: - forall actions tree inp b + forall actions tree inp b dir (SUBSET: pike_actions actions) - (ISTREE: bool_tree actions inp b tree), + (ISTREE: bool_tree actions inp b dir tree), pike_subtree tree. Proof. - intros actions tree inp b SUBSET ISTREE. - induction ISTREE; try eapply IHISTREE; pike_subset. - - eapply IHISTREE1. pike_subset. - - eapply IHISTREE2. pike_subset. + intros actions tree inp b dir SUBSET ISTREE. + induction ISTREE; + pike_subset; + try (eapply IHISTREE || eapply IHISTREE1 || eapply IHISTREE2); + pike_subset. + - destruct dir; pike_subset. - destruct plus; inversion H3. destruct greedy; pike_subset. + eapply IHISTREE1. pike_subset. + eapply IHISTREE1. pike_subset. @@ -344,19 +369,18 @@ Proof. + eapply IHISTREE1. pike_subset. + eapply IHISTREE1. pike_subset. - destruct plus; inversion H3. - - eapply IHISTREE. pike_subset. Qed. (** * Determinism *) (* I can't use determinism of is_tree since I've only proved one direction of equivalence *) Theorem bool_tree_determ: - forall actions i b t1 t2, - bool_tree actions i b t1 -> - bool_tree actions i b t2 -> + forall actions i b dir t1 t2, + bool_tree actions i b dir t1 -> + bool_tree actions i b dir t2 -> t1 = t2. Proof. - intros actions i b t1 t2 H H0. + intros actions i b dir t1 t2 H H0. generalize dependent t2. induction H; intros; try solve[inversion H0; subst; auto; f_equal; apply IHbool_tree; auto]. @@ -382,16 +406,16 @@ Qed. (* the other direction of implication is obtained using only determinism and productivity *) Theorem bool_to_istree: - forall acts b inp t, - bool_encoding b inp acts -> + forall acts b inp dir t, + bool_encoding b inp acts dir -> pike_actions acts -> - bool_tree acts inp b t -> - is_tree rer acts inp GroupMap.empty forward t. + bool_tree acts inp b dir t -> + is_tree rer acts inp GroupMap.empty dir t. Proof. - intros acts b inp t ENCODE H H0. + intros acts b inp dir t ENCODE H H0. (* productivity *) - assert (exists t', is_tree rer acts inp GroupMap.empty forward t') as [t' ISTREE]. - { destruct (compute_tree rer acts inp GroupMap.empty forward (S (actions_fuel acts inp forward))) eqn:PROD. + assert (exists t', is_tree rer acts inp GroupMap.empty dir t') as [t' ISTREE]. + { destruct (compute_tree rer acts inp GroupMap.empty dir (S (actions_fuel acts inp dir))) eqn:PROD. 2: { generalize functional_terminates. intros H1. apply H1 in PROD; auto; lia. } exists t0. eapply compute_is_tree; eauto. } eapply encode_equal in ISTREE as BOOLTREE; eauto. @@ -400,24 +424,24 @@ Qed. Qed. Theorem bool_to_istree_regex: - forall r inp t, + forall r inp dir t, pike_regex r -> - bool_tree [Areg r] inp CanExit t -> - is_tree rer [Areg r] inp GroupMap.empty forward t. + bool_tree [Areg r] inp CanExit dir t -> + is_tree rer [Areg r] inp GroupMap.empty dir t. Proof. - intros r inp t H H0. - assert (bool_encoding CanExit inp [Areg r]) by (constructor; constructor). + intros r inp dir t H H0. + assert (bool_encoding CanExit inp [Areg r] dir) by (constructor; constructor). eapply bool_to_istree; eauto; pike_subset. Qed. Theorem booltree_istree_equiv: - forall r inp t, + forall r inp dir t, pike_regex r -> - bool_tree [Areg r] inp CanExit t <-> - is_tree rer [Areg r] inp GroupMap.empty forward t. + bool_tree [Areg r] inp CanExit dir t <-> + is_tree rer [Areg r] inp GroupMap.empty dir t. Proof. - intros r inp t SUBSET. split. + intros r inp dir t SUBSET. split. - apply bool_to_istree_regex; auto. - apply boolean_correct; auto. Qed. diff --git a/Engine/Correctness.v b/Engine/Correctness.v index 38d7d2dc..7f81bf65 100644 --- a/Engine/Correctness.v +++ b/Engine/Correctness.v @@ -68,7 +68,7 @@ Qed. Theorem pike_vm_to_pike_tree: forall r inp tree result, pike_regex r -> - bool_tree rer [Areg r] inp CanExit tree -> + bool_tree rer [Areg r] inp CanExit forward tree -> trc_pike_vm (compilation r) forward (pike_vm_initial_state inp) (PVS_final result) -> trc_pike_tree (pike_tree_initial_state tree inp) (PTS_final result). Proof. @@ -82,7 +82,7 @@ Qed. Theorem pike_vm_to_pike_tree_unanchored {strs:StrSearch}: forall r inp tree result future_tree, pike_regex r -> - bool_tree rer [Areg r] inp CanExit tree -> + bool_tree rer [Areg r] inp CanExit forward tree -> trc_pike_vm (compilation r) forward (pike_vm_initial_state_unanchored (extract_literal rer r) inp forward) (PVS_final result) -> future_tree_shape rer r inp future_tree -> exists future, may_erase future_tree future /\ @@ -254,7 +254,7 @@ Qed. Theorem memobt_to_memotree: forall r inp tree result initms finalms initts, pike_regex r -> - bool_tree rer [Areg r] inp CanExit tree -> + bool_tree rer [Areg r] inp CanExit forward tree -> seen_inclusion rer (compilation r) initts initms None None -> trc_memo_bt (compilation r) (MemoBT.initial_state inp initms) (MBT_final result finalms) -> exists finalts, trc_memo_tree (initial_tree_state tree inp initts) (MTree_final result finalts) /\ @@ -271,7 +271,7 @@ Qed. Theorem memobt_to_memotree_init: forall r inp tree result finalms, pike_regex r -> - bool_tree rer [Areg r] inp CanExit tree -> + bool_tree rer [Areg r] inp CanExit forward tree -> trc_memo_bt (compilation r) (MemoBT.initial_state inp initial_memoset) (MBT_final result finalms) -> exists finalts, trc_memo_tree (initial_tree_state tree inp initial_seentrees) (MTree_final result finalts) /\ (result = None -> seen_inclusion rer (compilation r) finalts finalms None None). diff --git a/Engine/MemoEquiv.v b/Engine/MemoEquiv.v index d3d20907..dca50c07 100644 --- a/Engine/MemoEquiv.v +++ b/Engine/MemoEquiv.v @@ -27,7 +27,7 @@ Section MemoEquiv. Inductive tree_config (code:code) : (tree * group_map * input) -> config -> Prop := | tc_eq: forall inp tree gm pc b actions - (TREE: bool_tree rer actions inp b tree) + (TREE: bool_tree rer actions inp b forward tree) (CONT: actions_rep actions code pc) (SUBSET: pike_actions actions), tree_config code (tree, gm, inp) (pc, gm, b, inp) @@ -93,7 +93,7 @@ Section MemoEquiv. Lemma initial_tree_config: forall r code tree inp (COMPILE: compilation r = code) - (TREE: bool_tree rer [Areg r] inp CanExit tree) + (TREE: bool_tree rer [Areg r] inp CanExit forward tree) (SUBSET: pike_regex r), tree_config code (tree, GroupMap.empty,inp) (0, GroupMap.empty, CanExit,inp). Proof. @@ -152,7 +152,7 @@ Section MemoEquiv. specialize (INCL pc b inp SEEN) as [[t [gm [IN EQ]]] | [ST [cur [H _]]]]; eauto. inversion H. Qed. - + Lemma add_inclusion: forall treeseen memoset code inp tree pc gm b nextcurrent nextpc (INCL: seen_inclusion code treeseen memoset (Some (tree,gm,inp)) (Some pc)) @@ -163,13 +163,13 @@ Section MemoEquiv. unfold seen_inclusion in *. intros pc0 b0 inp0 SEEN. apply is_memo_add in SEEN. destruct SEEN as [EQ|SEEN]. - inversion EQ. subst. left. exists tree. exists gm. split; auto. apply in_add. left. auto. - - specialize (INCL pc0 b0 inp0 SEEN). + - specialize (INCL pc0 b0 inp0 SEEN). destruct INCL as [[ts [gms [SEENs TTs]]] | [ST [cur [Hcur [ts [gms [GEQ [EQ TTS]]]]]]]]. + left. exists ts. exists gms. split; auto. apply in_add. right; auto. + left. exists ts. exists gms. split; auto. apply in_add. left; auto. inversion EQ. auto. Qed. - + Lemma skip_inclusion: forall code inp treeseen memoset tree gm currentpc (INCL: seen_inclusion code treeseen memoset (Some (tree, gm, inp)) currentpc) @@ -206,7 +206,7 @@ Section MemoEquiv. - right. split; auto. exists nextpc. split; auto. exists ts. exists gms. split; auto. inversion Hcur. lia. Qed. - + Definition head_pc (stk:list config) : option label := match stk with | [] => None @@ -234,12 +234,12 @@ Section MemoEquiv. Proof. intros c. unfold seen_inclusion. intros pc b inp SEEN. rewrite initial_empty in SEEN. inversion SEEN. - Qed. + Qed. (* the initial states of both smallstep semantics are related with the invariant *) Lemma initial_memo_inv_inclusion: forall r inp tree code ts ms - (TREE: bool_tree rer [Areg r] inp CanExit tree) + (TREE: bool_tree rer [Areg r] inp CanExit forward tree) (COMPILE: compilation r = code) (SUBSET: pike_regex r) (INCL: seen_inclusion code ts ms None None), @@ -263,7 +263,7 @@ Section MemoEquiv. Lemma initial_memo_inv: forall r inp tree code - (TREE: bool_tree rer [Areg r] inp CanExit tree) + (TREE: bool_tree rer [Areg r] inp CanExit forward tree) (COMPILE: compilation r = code) (SUBSET: pike_regex r), memo_inv code (initial_tree_state tree inp initial_seentrees) (MemoBT.initial_state inp initial_memoset). @@ -298,13 +298,14 @@ Section MemoEquiv. unfold exec_tree in TREESTEP. destruct t; inversion TREESTEP; subst. clear TREESTEP. inversion TC; subst; try no_stutter. remember Match as TMATCH. + remember forward as dir. (* here we have to proceed by induction because there are many ways to get a Match tree *) (* it could be epsilon, it could be epsilon followed by epsilon etc *) induction TREE; intros; subst; try inversion HeqTMATCH. - simpl. invert_rep. rewrite ACCEPT. auto. - repeat invert_rep. apply IHTREE; auto. pike_subset. - - repeat invert_rep. apply IHTREE; auto. - repeat (econstructor; eauto). pike_subset. + - repeat invert_rep. eapply IHTREE; eauto; pike_subset. + repeat (econstructor; eauto). - repeat invert_rep. apply IHTREE; auto. pike_subset. - destruct greedy; inversion CHOICE. Qed. @@ -320,6 +321,7 @@ Section MemoEquiv. inversion TC; subst; try no_stutter. 2: { simpl in TREESTEP. inversion TREESTEP. } remember Mismatch as TMIS. + remember forward as dir. induction TREE; intros; subst; try inversion HeqMIS; subst; simpl in TREESTEP; try solve[inversion TREESTEP]. - repeat invert_rep. simpl. rewrite END. auto. @@ -344,6 +346,7 @@ Section MemoEquiv. intros t pc gm b inp code char TC NOSTUTTER. inversion TC; subst; try invert_rep. remember (Read char t) as TREAD. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTREAD; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. exists nextinp. @@ -369,6 +372,7 @@ Section MemoEquiv. intros t pc gm b inp code gid TC NOSTUTTER. inversion TC; subst; try invert_rep. remember (GroupAction (Open gid) t) as TOPEN. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTOPEN; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. @@ -392,6 +396,7 @@ Section MemoEquiv. intros t pc gm b inp code gid TC NOSTUTTER. inversion TC; subst; try no_stutter. remember (GroupAction (Close gid) t) as TCLOSE. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTCLOSE; subst. - repeat invert_rep. simpl. rewrite CLOSE. split; auto. econstructor; eauto. 2: pike_subset. @@ -427,6 +432,7 @@ Section MemoEquiv. intros t pc gm b inp code TC NOSTUTTER. inversion TC; subst; try no_stutter. remember (Progress t) as TPASS. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTPASS; subst. - repeat invert_rep. pike_subset. simpl. exists pcmid. rewrite END. split; auto. econstructor; eauto. @@ -447,6 +453,7 @@ Section MemoEquiv. intros t pc gm b inp code a TC NOSTUTTER. inversion TC; subst; try no_stutter. remember (AnchorPass a t) as TANCHOR. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTANCHOR; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. @@ -473,6 +480,7 @@ Section MemoEquiv. unfold exec_tree in TREESTEP. inversion TREESTEP. subst. clear TREESTEP. inversion TC; subst; try no_stutter. remember (Choice tree1 tree2) as TCHOICE. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTCHOICE; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. exists [(S pc,gm,b,inp);(S end1,gm,b,inp)]. split. @@ -621,7 +629,8 @@ Section MemoEquiv. simpl. rewrite BEGIN. auto. } (* at a jmp instruction *) generalize dependent pc. - induction TREE; intros. + remember forward as dir. + induction TREE; intros; subst. - invert_rep. stutter. exists pcstart. exists b. split; try split; try lia. + simpl. rewrite JMP. auto. diff --git a/Engine/PikeEquiv.v b/Engine/PikeEquiv.v index 5f1cbd9b..d2f19d9f 100644 --- a/Engine/PikeEquiv.v +++ b/Engine/PikeEquiv.v @@ -26,7 +26,7 @@ Section PikeEquiv. Inductive tree_thread (code:code) (inp:input) : (tree * group_map) -> thread -> Prop := | tt_eq: forall tree gm pc b actions - (TREE: bool_tree rer actions inp b tree) + (TREE: bool_tree rer actions inp b forward tree) (CONT: actions_rep actions code pc) (SUBSET: pike_actions actions), tree_thread code inp (tree, gm) (pc, gm, b) @@ -46,7 +46,7 @@ Inductive tree_thread (code:code) (inp:input) : (tree * group_map) -> thread -> Lemma initial_tree_thread: forall r code tree inp (COMPILE: compilation r = code) - (TREE: bool_tree rer [Areg r] inp CanExit tree) + (TREE: bool_tree rer [Areg r] inp CanExit forward tree) (SUBSET: pike_regex r), tree_thread code inp (tree, GroupMap.empty) (0, GroupMap.empty, CanExit). Proof. @@ -87,24 +87,25 @@ 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 dir pc b + forall tree gm inp code 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 dir inp = EpsMatch. + epsilon_step rer (pc, gm, b) code forward inp = EpsMatch. Proof. - intros tree gm inp code dir pc b TREESTEP NOSTUTTER TT. + intros tree gm inp code 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. + remember forward as dir. (* here we have to proceed by induction because there are many ways to get a Match tree *) (* it could be epsilon, it could be epsilon followed by epsilon etc *) induction TREE; intros; subst; try inversion HeqTMATCH. - simpl. repeat invert_rep. rewrite ACCEPT. auto. - repeat invert_rep. pike_subset. - - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat (econstructor; eauto). pike_subset. + - repeat invert_rep. eapply IHTREE; eauto; pike_subset. + repeat (econstructor; eauto). - repeat invert_rep. pike_subset. - destruct greedy; inversion CHOICE. Qed. @@ -123,6 +124,7 @@ Proof. unfold tree_bfs_step in TREESTEP. destruct tree; inversion TREESTEP. subst. clear TREESTEP. inversion TT; subst; try no_stutter. remember (Read c nexttree) as TREAD. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTREAD; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - assert (CHECK: check_read rer cd inp forward = CanRead /\ advance_input inp forward = Some nextinp) by (apply can_read_correct; eauto). @@ -150,6 +152,7 @@ Proof. intros gid tree gm inp code pc b TT NOSTUTTER. inversion TT; subst; try invert_rep. remember (GroupAction (Open gid) tree) as TOPEN. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTOPEN; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. @@ -175,6 +178,7 @@ Proof. intros gid tree gm inp code pc b TT NOSTUTTER. inversion TT; subst; try no_stutter. remember (GroupAction (Close gid) tree) as TCLOSE. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTCLOSE; subst. - repeat invert_rep. simpl. rewrite CLOSE. split; auto. econstructor; eauto. 2: pike_subset. @@ -191,10 +195,11 @@ Theorem no_tree_reset: (* A tree corresponding to some actions cannot start with ResetGroups *) forall gidl tree inp actions b, pike_actions actions -> - bool_tree rer actions inp b (GroupAction (Reset gidl) tree) -> False. + bool_tree rer actions inp b forward (GroupAction (Reset gidl) tree) -> False. Proof. intros gidl tree inp actions b PIKE H. remember (GroupAction (Reset gidl) tree) as TRESET. + remember forward as dir. induction H; inversion HeqTRESET; subst; auto. - pike_subset. - apply IHbool_tree; auto. pike_subset. @@ -226,6 +231,7 @@ Proof. intros gm inp code pc b TT NOSTUTTER. inversion TT; subst; try no_stutter. remember (Mismatch) as TMIS. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTMIS; subst. - repeat invert_rep. simpl. rewrite END. auto. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. @@ -239,15 +245,16 @@ Proof. Qed. Theorem generate_checkpass: - forall tree gm inp code dir pc b + forall tree gm inp code 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 dir inp = EpsActive [(nextpc,gm,CanExit)] /\ + exists nextpc, epsilon_step rer (pc, gm, b) code forward inp = EpsActive [(nextpc,gm,CanExit)] /\ tree_thread code inp (tree,gm) (nextpc,gm,CanExit). Proof. - intros tree gm inp code dir pc b TT NOSTUTTER. + intros tree gm inp code pc b TT NOSTUTTER. inversion TT; subst; try no_stutter. remember (Progress tree) as TPASS. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTPASS; subst. - repeat invert_rep. pike_subset. simpl. exists pcmid. rewrite END. split; auto. econstructor; eauto. @@ -268,6 +275,7 @@ Proof. intros tree gm inp code pc b a TT NOSTUTTER. inversion TT; subst; try no_stutter. remember (AnchorPass a tree) as TANCHOR. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTANCHOR; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. @@ -283,18 +291,19 @@ Qed. Theorem generate_choice: - forall tree1 tree2 gm inp code dir pc b treeactive + forall tree1 tree2 gm inp code 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 dir inp = EpsActive threadactive /\ + epsilon_step rer (pc, gm, b) code forward inp = EpsActive threadactive /\ list_tree_thread code inp treeactive threadactive. Proof. - intros tree1 tree2 gm inp code dir pc b treeactive TREESTEP NOSTUTTER TT. + intros tree1 tree2 gm inp code 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. + remember forward as dir. induction TREE; intros; subst; try inversion HeqTCHOICE; subst. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - repeat invert_rep. exists [(S pc,gm,b);(S end1,gm,b)]. split. @@ -425,14 +434,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 dir pc b + forall tree gm inp code 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 dir inp = EpsActive [(nextpc,gm,nextb)] /\ + epsilon_step rer (pc,gm,b) code forward inp = EpsActive [(nextpc,gm,nextb)] /\ tree_thread code inp (tree,gm) (nextpc,gm,nextb). Proof. - intros tree gm inp code dir pc b TT STUTTER. + intros tree gm inp code pc b TT STUTTER. inversion TT; subst. (* reset is not stuttering *) 2: { unfold stutters in STUTTER. rewrite RESET in STUTTER. inversion STUTTER. } @@ -441,7 +450,8 @@ Proof. simpl. rewrite BEGIN. auto. } (* at a jmp instruction *) generalize dependent pc. - induction TREE; intros. + remember forward as dir. + induction TREE; intros; subst. - invert_rep. stutter. exists pcstart. exists b. split; try split; try lia. + simpl. rewrite JMP. auto. @@ -605,7 +615,7 @@ Inductive future_nextprefix (code:code): input -> option tree -> option (nat * l (FUTURE: future = lazy_iter c t1 t2) (COMPILE: compilation r = code) (SUBSET: pike_regex r) - (T1: bool_tree rer [Areg r] (Input next (c::pref)) CanExit t1) + (T1: bool_tree rer [Areg r] (Input next (c::pref)) CanExit forward t1) (T2: future_tree_shape rer r (Input next (c::pref)) t2) (LIT: extract_literal rer r = lit), future_nextprefix code (Input (c::next) pref) (Some future) (Some (0, lit, strs)). @@ -896,7 +906,7 @@ Lemma future_nextprefix_tree_acceleration: compilation r = code /\ pike_regex r /\ extract_literal rer r = lit /\ - bool_tree rer [Areg r] (advance_input_n inp (S n) forward) CanExit t /\ + bool_tree rer [Areg r] (advance_input_n inp (S n) forward) CanExit forward t /\ future_tree_shape rer r (advance_input_n inp (S n) forward) acc. Proof. intros code inp n lit strs future t acc FUTUREPREFIX TREEACC. @@ -1075,7 +1085,7 @@ Qed. (* the initial states of both smallstep semantics are related with the invariant *) Lemma initial_pike_inv: forall r inp tree code - (TREE: bool_tree rer [Areg r] inp CanExit tree) + (TREE: bool_tree rer [Areg r] inp CanExit forward tree) (COMPILE: compilation r = code) (SUBSET: pike_regex r), pike_inv code (pike_tree_initial_state tree inp) (pike_vm_initial_state inp). @@ -1086,7 +1096,7 @@ Qed. Lemma initial_pike_inv_unanchored {strs:StrSearch}: forall r inp tree code future_tree - (TREE: bool_tree rer [Areg r] inp CanExit tree) + (TREE: bool_tree rer [Areg r] inp CanExit forward tree) (COMPILE: compilation r = code) (SUBSET: pike_regex r) (SHAPE: future_tree_shape rer r inp future_tree), @@ -1226,7 +1236,7 @@ Proof. destruct (stutters pc code) eqn:STUTTERS. { (* stuttering step *) - right. apply stutter_step with (dir:=forward) in TT as H; auto. + right. apply stutter_step 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 +1255,7 @@ Proof. + eapply pikeinv; try (eapply add_inclusion; eauto); try constructor; eauto. apply ltt_app; eauto. (* match *) - - left. eapply generate_match with (dir:=forward) in TREESTEP as THREADSTEP; eauto. + - left. eapply generate_match 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/PikeTree.v b/Engine/PikeTree.v index d2e7bd18..9e93b3ac 100644 --- a/Engine/PikeTree.v +++ b/Engine/PikeTree.v @@ -93,7 +93,7 @@ Section PikeTree. Definition initial_future_actions_unanchored (r: regex) (inp: input) := [Areg (Regex.Character CdAll); Acheck inp; Areg dot_star; Areg r]. Definition future_tree_shape (r: regex) (inp: input) (future: tree): Prop := - bool_tree rer (initial_future_actions_unanchored r inp) inp CannotExit future. + bool_tree rer (initial_future_actions_unanchored r inp) inp CannotExit forward future. Definition initial_future_unanchored (r: regex) (inp: input) (future: option tree): Prop := exists tree, future_tree_shape r inp tree /\ may_erase tree future. @@ -387,8 +387,8 @@ Section PikeTree. forall t r inp tree future, pike_regex r -> initial_future_unanchored r inp future -> - bool_tree rer [Areg r] inp CanExit t -> - bool_tree rer [Areg (lazy_prefix r)] inp CanExit tree -> + bool_tree rer [Areg r] inp CanExit forward t -> + bool_tree rer [Areg (lazy_prefix r)] inp CanExit forward tree -> piketreeinv (pike_tree_initial_state_unanchored t future inp) (first_leaf tree inp). Proof. unfold initial_future_unanchored, future_tree_shape. @@ -533,7 +533,7 @@ Section PikeTree. forall r inp future nextinp acc t, future_tree_shape r inp future -> tree_acceleration inp future nextinp acc t -> - bool_tree rer [Areg r] nextinp CanExit t /\ future_tree_shape r nextinp acc. + bool_tree rer [Areg r] nextinp CanExit forward t /\ future_tree_shape r nextinp acc. Proof. unfold future_tree_shape, initial_future_actions_unanchored. intros r inp future nextinp acc t FUTURE ACC. diff --git a/Engine/TreeRep.v b/Engine/TreeRep.v index fd36ac6d..1326fa37 100644 --- a/Engine/TreeRep.v +++ b/Engine/TreeRep.v @@ -152,12 +152,13 @@ Theorem actions_tree_rep: forall actions code pc inp b t (SUBSET: pike_actions actions) (ACT: actions_rep actions code pc) - (TREE: bool_tree rer actions inp b t), + (TREE: bool_tree rer actions inp b forward t), tree_rep t code pc inp b. Proof. intros actions code pc inp b t SUBSET ACT TREE. generalize dependent code. generalize dependent pc. - induction TREE; intros. + remember forward as dir. + induction TREE; intros; subst. (* Match *) - remember [] as emp. induction ACT; inversion Heqemp. + constructor. auto. @@ -209,7 +210,7 @@ Proof. invert_rep. inversion NFA; subst. 2: { in_subset. } eapply tr_choice; eauto. - + eapply IHTREE1. pike_subset. + + eapply IHTREE1; eauto. pike_subset. eapply cons_bc with (pcmid:=end1); try constructor; eauto. eapply jump_bc; eauto. + eapply IHTREE2; eauto. pike_subset. @@ -330,8 +331,8 @@ Lemma actions_rep_unicity: pike_actions a2 -> actions_rep a1 code pc -> actions_rep a2 code pc -> - bool_tree rer a1 inp b t1 -> - bool_tree rer a2 inp b t2 -> + bool_tree rer a1 inp b forward t1 -> + bool_tree rer a2 inp b forward t2 -> t1 = t2. Proof. intros. eapply actions_tree_rep in H1; eauto. From 634539d1407b6366651257e0f8932a9782057034 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Mon, 23 Mar 2026 17:13:12 +0100 Subject: [PATCH 4/5] Engine: add lookarounds to bool_tree --- Engine/BooleanSemantics.v | 50 +++++++++++++++++++++++++++++++++++++++ Engine/MemoEquiv.v | 5 ++++ Engine/PikeEquiv.v | 3 +++ Engine/TreeRep.v | 3 +++ Semantics/Tree.v | 48 +++++++++++++++++++++++++++++++++++++ 5 files changed, 109 insertions(+) diff --git a/Engine/BooleanSemantics.v b/Engine/BooleanSemantics.v index 5d506acc..40654eb6 100644 --- a/Engine/BooleanSemantics.v +++ b/Engine/BooleanSemantics.v @@ -104,6 +104,19 @@ Section BooleanSemantics. forall r1 cont treecont inp b gid dir (TREECONT: bool_tree (Areg r1 :: Aclose gid :: cont) inp b dir treecont), bool_tree (Areg (Group gid r1) :: cont) inp b dir (GroupAction (Open gid) treecont) + | tree_lk: + forall lk r1 cont treecont treelk inp b gmlk dir + (TREELK: bool_tree [Areg r1] inp b (lk_dir lk) treelk) + (* since we have no backreferences, we do not care about the group map *) + (RES_LK: lk_result lk treelk GroupMap.empty inp = Some gmlk) + (TREECONT: bool_tree cont inp b dir treecont), + bool_tree (Areg (Lookaround lk r1) :: cont) inp b dir (LK lk treelk treecont) + | tree_lk_fail: + forall lk r1 cont treelk inp b dir + (TREELK: bool_tree [Areg r1] inp b (lk_dir lk) treelk) + (* since we have no backreferences, we do not care about the group map *) + (FAIL_LK: lk_result lk treelk GroupMap.empty inp = None), + bool_tree (Areg (Lookaround lk r1) :: cont) inp b dir (LKFail lk treelk) | tree_anchor: forall a cont treecont inp b dir (ANCHOR: anchor_satisfied rer a inp = true) @@ -255,6 +268,36 @@ Proof. - simpl in H0. destruct H0 as [H0|IN]; try inversion H0; auto. Qed. +Lemma lk_result_indep_none: + forall lk treelk gm1 gm2 inp, + lk_result lk treelk gm1 inp = None -> + lk_result lk treelk gm2 inp = None. +Proof. + unfold lk_result. + intros. + destruct positivity. + - destruct tree_res eqn:Hres1; [now destruct l|]. + now rewrite res_indep with (1:=Hres1). + - destruct tree_res eqn:Hres1; [|discriminate]. + eapply res_indep_some in Hres1 as [? Hres]; eauto. + now rewrite Hres. +Qed. + +Lemma lk_result_indep_some: + forall lk treelk gm1 gm2 gmlk1 inp, + lk_result lk treelk gm1 inp = Some gmlk1 -> + exists gmlk2, lk_result lk treelk gm2 inp = Some gmlk2. +Proof. + unfold lk_result. + intros. + destruct positivity. + - destruct tree_res eqn:Hres1; [|discriminate]. + eapply res_indep_some in Hres1 as [? Hres]; eauto. + destruct x. + eexists. now rewrite Hres. + - destruct tree_res eqn:Hres1; [now destruct l|injection H as <-]. + eexists. now rewrite res_indep with (1:=Hres1). +Qed. (** * Second Step: encoding equality *) (* the two tree constructions are equal *) @@ -398,6 +441,13 @@ Qed. subst. f_equal. + f_equal. apply IHbool_tree1; auto. + apply IHbool_tree2; auto. + - inversion H1; subst; eauto. + f_equal; eauto. + specialize (IHbool_tree1 treelk0 ltac:(eauto)). subst. + congruence. + - inversion H0; subst; eauto. + { specialize (IHbool_tree treelk0 ltac:(eauto)). subst. congruence. } + f_equal; eauto. - inversion H0; subst; rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. f_equal. apply IHbool_tree. auto. - inversion H0; subst; rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. auto. diff --git a/Engine/MemoEquiv.v b/Engine/MemoEquiv.v index dca50c07..74418cbd 100644 --- a/Engine/MemoEquiv.v +++ b/Engine/MemoEquiv.v @@ -330,6 +330,8 @@ Section MemoEquiv. - repeat invert_rep. eapply IHTREE; repeat (econstructor; eauto); pike_subset. - repeat invert_rep. eapply IHTREE; eauto. pike_subset. - destruct greedy; inversion TREESTEP. + - pike_subset. + - pike_subset. - repeat invert_rep. simpl. rewrite CHECK, ANCHOR. auto. Qed. @@ -714,6 +716,9 @@ Section MemoEquiv. exists pcstart. exists b. split; try split; try lia. * simpl. rewrite JMP. auto. * apply tc_eq with (actions:=Areg (Group gid r1):: cont); try constructor; auto; pike_subset. + (* lookarounds *) + - pike_subset. + - pike_subset. - invert_rep. { invert_rep. invert_rep; try in_subset; try stutter. } exists pcstart. exists b. split; try split; try lia. diff --git a/Engine/PikeEquiv.v b/Engine/PikeEquiv.v index d2f19d9f..94865028 100644 --- a/Engine/PikeEquiv.v +++ b/Engine/PikeEquiv.v @@ -535,6 +535,9 @@ Proof. exists pcstart. exists b. split; try split; try lia. * simpl. rewrite JMP. auto. * apply tt_eq with (actions:=Areg (Group gid r1):: cont); try constructor; auto; pike_subset. + (* lookarounds *) + - pike_subset. + - pike_subset. - invert_rep. { invert_rep. invert_rep; try in_subset; try stutter. } exists pcstart. exists b. split; try split; try lia. diff --git a/Engine/TreeRep.v b/Engine/TreeRep.v index 1326fa37..4ab9638f 100644 --- a/Engine/TreeRep.v +++ b/Engine/TreeRep.v @@ -290,6 +290,9 @@ Proof. eapply tr_open; eauto. eapply IHTREE; eauto. pike_subset. repeat (econstructor; eauto). + (* lookarounds *) + - pike_subset. + - pike_subset. (* anchor *) - remember (Areg (Anchor a) :: cont) as anchorcont. induction ACT; inversion Heqanchorcont; subst; diff --git a/Semantics/Tree.v b/Semantics/Tree.v index 776b86cd..06dcb622 100644 --- a/Semantics/Tree.v +++ b/Semantics/Tree.v @@ -318,6 +318,40 @@ Section Tree. + eapply leaves_indep_neglk; eauto. Qed. + Lemma app_neq_nil: + forall A (l1 l2: list A), + l1 ++ l2 <> [] <-> l1 <> [] \/ l2 <> []. + Proof. + intros A l1 l2. + split; intro H. + - destruct l1, l2; rewrite ?app_nil_r in *; eauto. + left. easy. + - destruct H. + + now destruct l1. + + destruct l2; [easy|]. + now destruct l1. + Qed. + + Lemma leaves_indep_nonempty: + forall t gm1 gm2 inp1 inp2 dir1 dir2, + tree_leaves t gm1 inp1 dir1 <> [] -> tree_leaves t gm2 inp2 dir2 <> []. + Proof. + induction t; simpl; intros; + try easy; + try eauto using IHt. + - rewrite app_neq_nil in *. + destruct H; eauto. + - destruct positivity. + + destruct (tree_leaves t1 gm1) eqn:Hleaves1; [easy|destruct l]. + assert (Hleaves1': tree_leaves t1 gm1 inp1 (lk_dir lk) <> []) by now rewrite Hleaves1. + eapply IHt1 with (gm2:=gm2) (inp2:=inp2) (dir2 := lk_dir lk) in Hleaves1'. + destruct (tree_leaves t1 gm2) eqn:Hleaves2; [easy|destruct l]. + eauto. + + destruct (tree_leaves t1 gm1) eqn:Hleaves1; [|easy]. + rewrite leaves_indep with (1:=Hleaves1). + eauto. + Qed. + (* Corollary: argument irrelevance in terms of tree_res *) (* A lemma about hd_error *) @@ -336,6 +370,20 @@ Section Tree. intros. rewrite first_tree_leaf, hd_error_none_nil in *. eauto using leaves_indep. Qed. + + Lemma res_indep_some: + forall t gm1 gm2 inp1 inp2 dir1 dir2 leaf1, + tree_res t gm1 inp1 dir1 = Some leaf1 -> + exists leaf2, tree_res t gm2 inp2 dir2 = Some leaf2. + Proof. + intros. + rewrite first_tree_leaf in H. + assert (H1: tree_leaves t gm1 inp1 dir1 <> []) by (destruct tree_leaves; easy). + eapply leaves_indep_nonempty with (gm2:=gm2) (inp2:=inp2) (dir2:=dir2) in H1. + destruct (tree_leaves t gm2) eqn:H2; [easy|]. + exists l. now rewrite first_tree_leaf, H2. + Qed. + Lemma leaf_eq_dec (l1 l2: leaf): {l1 = l2} + {l1 <> l2}. Proof. decide equality. From e91d625d71c06e4574e6fab50b19398038878f0f Mon Sep 17 00:00:00 2001 From: shilangyu Date: Wed, 6 May 2026 17:37:40 +0200 Subject: [PATCH 5/5] Semantics: move some list lemmas to ListLemmas --- Rewriting/Equivalence.v | 2 +- Semantics/Tree.v | 35 +---------------------------------- Utils/ListLemmas.v | 29 +++++++++++++++++++++++++++++ 3 files changed, 31 insertions(+), 35 deletions(-) diff --git a/Rewriting/Equivalence.v b/Rewriting/Equivalence.v index 24d805f7..7ffe0fa3 100644 --- a/Rewriting/Equivalence.v +++ b/Rewriting/Equivalence.v @@ -2,7 +2,7 @@ From Stdlib Require Export Bool Arith List Equivalence Lia. From Warblre Require Import Base RegExpRecord. From Linden Require Import Regex Chars Groups Tree Semantics FunctionalSemantics FunctionalUtils ComputeIsTree Parameters - LWParameters LeavesEquivalence FlatMap. + LWParameters LeavesEquivalence FlatMap ListLemmas. Export ListNotations. diff --git a/Semantics/Tree.v b/Semantics/Tree.v index 06dcb622..d8146753 100644 --- a/Semantics/Tree.v +++ b/Semantics/Tree.v @@ -2,6 +2,7 @@ From Stdlib Require Import List. Import ListNotations. From Linden Require Import Regex Chars Groups Parameters LWParameters. +From Linden Require Import ListLemmas. From Stdlib Require Import PeanoNat. From Warblre Require Import Typeclasses Parameters Base. @@ -217,18 +218,6 @@ Section Tree. forall gm idx dir, tree_res t gm idx dir = hd_error (tree_leaves t gm idx dir). - (* intermediate lemma about hd_error *) - Lemma hd_error_app: - forall A (l1 l2:list A), - hd_error (l1 ++ l2) = - match (hd_error l1) with - | Some h => Some h - | None => hd_error l2 - end. - Proof. - intros A l1 l2. induction l1; simpl; auto. - Qed. - (* Intermediate lemma for positive lookarounds *) Lemma first_tree_leaf_poslk: forall lk tlk t1, @@ -318,20 +307,6 @@ Section Tree. + eapply leaves_indep_neglk; eauto. Qed. - Lemma app_neq_nil: - forall A (l1 l2: list A), - l1 ++ l2 <> [] <-> l1 <> [] \/ l2 <> []. - Proof. - intros A l1 l2. - split; intro H. - - destruct l1, l2; rewrite ?app_nil_r in *; eauto. - left. easy. - - destruct H. - + now destruct l1. - + destruct l2; [easy|]. - now destruct l1. - Qed. - Lemma leaves_indep_nonempty: forall t gm1 gm2 inp1 inp2 dir1 dir2, tree_leaves t gm1 inp1 dir1 <> [] -> tree_leaves t gm2 inp2 dir2 <> []. @@ -354,14 +329,6 @@ Section Tree. (* Corollary: argument irrelevance in terms of tree_res *) - (* A lemma about hd_error *) - Lemma hd_error_none_nil {A}: - forall l: list A, hd_error l = None <-> l = []. - Proof. - intro l. split; intro H. - - destruct l. + reflexivity. + discriminate. - - subst l. reflexivity. - Qed. Lemma res_indep: forall t gm1 gm2 inp1 inp2 dir1 dir2, diff --git a/Utils/ListLemmas.v b/Utils/ListLemmas.v index b70d0170..af9384fe 100644 --- a/Utils/ListLemmas.v +++ b/Utils/ListLemmas.v @@ -60,3 +60,32 @@ Proof. - discriminate. - now inversion 1. Qed. + +Lemma app_neq_nil: + forall A (l1 l2: list A), + l1 ++ l2 <> [] <-> l1 <> [] \/ l2 <> []. +Proof. + intros A l1 l2. + split; intro H. + - destruct l1, l2; rewrite ?app_nil_r in *; eauto. + left. easy. + - destruct H. + + now destruct l1. + + destruct l2; [easy|]. + now destruct l1. +Qed. + +Lemma hd_error_none_nil {A}: + forall l: list A, hd_error l = None <-> l = []. +Proof. now destruct l. Qed. + +Lemma hd_error_app: + forall A (l1 l2:list A), + hd_error (l1 ++ l2) = + match (hd_error l1) with + | Some h => Some h + | None => hd_error l2 + end. +Proof. + intros A l1 l2. induction l1; simpl; auto. +Qed.