Rocq 9.0.0

.github/workflows/ci.yml

@@ -20,16 +20,15 @@ jobs:
         with:
           ocaml-compiler: 4.14.2
           dune-cache: true
-          opam-disable-sandboxing: true
-          opam-pin: false
 
       - name: Install opam dependencies
-        run:  |
-          opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#a1ffc3f2e47d942ad9e1194dfb71f0783ead6d8a
+        run: |
+          # keep the Warblre ref in sync with the README
+          opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#1657babedb991424e225d689c3ee8b0e151e9f5d
           opam install . --deps-only
 
       - name: Dune build
-        run:  opam exec -- dune build
+        run: opam exec -- dune build
 
-      - name: Check compiled libraries (coqchk)
-        run: opam exec -- coqchk -silent --output-context $(cat _CoqProject) _build/default/*/*.vo
+      - name: Check compiled libraries (rocqchk)
+        run: opam exec -- rocqchk -silent --output-context -R _build/default Linden _build/default/*/*.vo

.gitignore

@@ -10,3 +10,4 @@ _build
 _opam
 \#*.*\#
 *.v~
+_RocqProject

Engine/BooleanSemantics.v

@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -138,7 +138,7 @@ Inductive bool_encoding: LoopBool -> input -> actions -> Prop :=
     (ENCODE: bool_encoding b str cont),
     bool_encoding b str (Aclose gid::cont)
 | cons_true:
-  forall stk str head 
+  forall stk str head
     (ENCODE: bool_encoding CanExit str stk)
     (STRICT: strict_suffix str head forward),
     bool_encoding CanExit str (Acheck head::stk)
@@ -191,7 +191,7 @@ Proof.
   intros b str cont H.
   remember (Acheck str::cont) as prevcont.
   induction H; intros; auto; inversion Heqprevcont.
-  subst. apply ss_neq in STRICT. contradiction. 
+  subst. apply ss_neq in STRICT. contradiction.
 Qed.
 
 Lemma encode_next:
@@ -321,7 +321,7 @@ Proof.
   intros r str t PIKE H.
   eapply encode_equal; eauto.
   { constructor; constructor; auto. }
-  constructor. constructor. 
+  constructor. constructor.
 Qed.
 
 

Engine/Complexity.v

@@ -1,6 +1,6 @@
 (** * Complexity of the PikeVM algorithm *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -245,7 +245,7 @@ Lemma compilation_nonempty:
   forall r, nonempty (compilation r).
 Proof.
   intros. unfold compilation. destruct compile. unfold nonempty, size.
-  rewrite app_length. simpl. lia.
+  rewrite length_app. simpl. lia.
 Qed.
 
 (* Some bytecode is well-formed if every target label belongs in some range *)
@@ -361,7 +361,7 @@ Proof.
   intros pc i next GET IN.
   assert (HL: pc < length (c ++ [Accept])).
   { eapply nth_error_Some. unfold get_pc in GET. rewrite GET. intros HI. inversion HI. }
-  rewrite app_length in HL. simpl in HL.
+  rewrite length_app in HL. simpl in HL.
   assert (pc = length c \/ pc < length c) as [ACC|H1] by lia.
   (* accept *)
   { subst. assert (get_pc (c ++ [Accept]) (length c) = get_pc [Accept] 0).
@@ -373,7 +373,7 @@ Proof.
   { unfold get_pc in GET. rewrite nth_error_app1 in GET; auto. }
   assert (POS: pc >= 0) by lia.
   specialize (nfa_wf r c 0 (length c) pc next i REP POS H1 GETI IN) as WF.
-  unfold size. rewrite app_length. simpl. lia.
+  unfold size. rewrite length_app. simpl. lia.
 Qed.
 
 Lemma eps_step_blocked_wf:
@@ -498,7 +498,7 @@ Proof.
     + intros n lit0 H. eapply search_in_range; 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.
-      rewrite app_length. simpl. lia.
+      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.
     + constructor.
@@ -520,7 +520,7 @@ Proof.
     + unfold add_thread. apply wf_new; auto.
     + specialize (free_add seen (size code) dist (pc,gm,b) SEENWF UNSEEN) as FREE.
       apply wf_size in FREE; auto. apply eps_step_active in STEP0.
-      unfold measure, free. rewrite app_length. simpl. simpl in FREE. lia.
+      unfold measure, free. rewrite length_app. simpl. simpl in FREE. lia.
   (* 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. }
@@ -541,7 +541,7 @@ Proof.
          eapply eps_step_blocked_wf in STEP0 as [i [GET IN]]; eauto.
      + unfold add_thread. apply wf_new; auto.
      + specialize (free_add seen (size code) dist (pc,gm,b) SEENWF UNSEEN RANGE) as FREE.
-       apply wf_size in FREE. unfold measure, free. rewrite app_length. simpl. simpl in FREE. lia.
+       apply wf_size in FREE. unfold measure, free. rewrite length_app. simpl. simpl in FREE. lia.
 Qed.
 
 (** * Code Size  *)
@@ -579,23 +579,23 @@ Proof.
   - destruct (compile r1 (S start)) eqn:C1. destruct (compile r2 (S l)) eqn:C2.
     erewrite <- IHr1; eauto. 2: pike_subset.
     erewrite <- IHr2; eauto. 2: pike_subset.
-    inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+    inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
   - destruct (compile r1 start) eqn:C1. destruct (compile r2 l) eqn:C2.
     erewrite <- IHr1; eauto. 2: pike_subset.
     erewrite <- IHr2; eauto. 2: pike_subset.
-    inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+    inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
   - destruct min; destruct (destruct_delta delta) as [DZ | [D1 | [DINF | [delta' [DUN N3]]]]]; subst; try solve[pike_subset].
     + inversion COMP. auto.
     + destruct (compile r (S (S (S start)))) eqn:C1.
       erewrite <- IHr; eauto. 2: pike_subset.
-      inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+      inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
     + destruct (compile r (S (S (S start)))) eqn:C1.
       erewrite <- IHr; eauto. 2: pike_subset.
-      inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+      inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
     + inversion SUBSET; subst; lia.
   - destruct (compile r (S start)) eqn:C1.
     erewrite <- IHr; eauto. 2: pike_subset.
-    inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+    inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
 Qed.
 
 Theorem compilation_size:
@@ -604,7 +604,7 @@ Theorem compilation_size:
     size (compilation r) = codesize r.
 Proof.
   unfold codesize, size, compilation. intros r H. destruct (compile r 0) eqn:COMP.
-  apply compile_size in COMP; auto. rewrite <- COMP. rewrite app_length. simpl. lia.
+  apply compile_size in COMP; auto. rewrite <- COMP. rewrite length_app. simpl. lia.
 Qed.
 
 (* relating this compilation size to the size of the regex *)
@@ -642,7 +642,7 @@ Proof.
   - unfold pike_vm_initial_state. rewrite <- compilation_size; auto.
     constructor; auto.
     + intros t H. destruct H. 2: inversion H.
-      subst. simpl. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite app_length.
+      subst. simpl. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite length_app.
       simpl. lia.
     + intros t H. inversion H.
     + constructor.
@@ -661,7 +661,7 @@ Proof.
   - unfold pike_vm_initial_state_unanchored. rewrite <- compilation_size; auto.
     constructor; auto.
     + intros t H. destruct H. 2: inversion H.
-      subst. simpl. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite app_length.
+      subst. simpl. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite length_app.
       simpl. lia.
     + intros t H. inversion H.
     + constructor.

Engine/Correctness.v

@@ -1,6 +1,6 @@
 (** * Correctness theorems for the PikeVM engine  *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.

Engine/FunctionalMemoBT.v

@@ -1,6 +1,6 @@
 (* The MemoBT algorithm, expressed as a fuel-based function *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.

Engine/FunctionalPikeVM.v

@@ -1,6 +1,6 @@
 (* The PikeVM algorithm, expressed as a fuel-based function *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -216,7 +216,7 @@ End FunctionalPikeVM.
 
 From Linden Require Import Inst.
 From Warblre Require Import Inst.
-Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Stdlib.Strings.Ascii Stdlib.Strings.String.
 Open Scope string_scope.
 
 Section Example.

Engine/MemoBT.v

@@ -1,7 +1,7 @@
 (** * MemoBT algorithm  *)
 (* A backtracking algorithm on the extended NFA, with memoization *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -35,7 +35,7 @@ Section MemoBT.
     MBT [(0, GroupMap.empty, CanExit, inp)] initial_memoset.
 
   (** * MemoBT small-step semantics *)
-  
+
   Inductive exec_result : Type :=
   | FoundMatch: leaf -> exec_result
   | Explore: stack -> exec_result.
@@ -77,7 +77,7 @@ Section MemoBT.
         end
     end.
 
-  
+
   Inductive memobt_step (c:code) : mbt_state -> mbt_state -> Prop :=
   (* we exhausted all configurations, there is no match *)
   | mbt_nomatch: forall ms,
@@ -102,7 +102,7 @@ Section MemoBT.
 
   (** * MemoBT properties  *)
 
-  Theorem memobt_deterministic: 
+  Theorem memobt_deterministic:
      forall c mbs mbs1 mbs2
     (STEP1: memobt_step c mbs mbs1)
     (STEP2: memobt_step c mbs mbs2),

Engine/MemoEquiv.v

@@ -1,6 +1,6 @@
 (** * Equivalence between MemoBT algorithm and MemoTree algorithm  *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 
@@ -16,7 +16,7 @@ Section MemoEquiv.
   Context {params: LindenParameters}.
   Context {MS: MemoSet params}.
   Context (rer: RegExpRecord).
-  
+
   (* FIXME: these are generalizations of definitions used in the PikeEquiv proof *)
   (* it could be nice to only use the generalized version everywhere *)
   (* I should write an NFA library *)
@@ -77,7 +77,7 @@ Section MemoEquiv.
       simpl in IHTC1. destruct IHTC1; subst; simpl; auto.
   Qed.
 
-  
+
   Lemma tc_same_tree:
     forall code inp t1 gm1 t2 gm2 pc b
       (TC1: tree_config code (t1,gm1,inp) (pc,gm1,b,inp))
@@ -88,7 +88,7 @@ Section MemoEquiv.
     eapply tc_same_interm in TC1; eauto. simpl in TC1. auto.
   Qed.
 
-  
+
   (* the initial active config and the initial active tree are related with the invariant *)
   Lemma initial_tree_config:
     forall r code tree inp
@@ -117,7 +117,7 @@ Section MemoEquiv.
       (LTC: list_tree_config code treelist threadlist)
       (TC: tree_config code (tree, gm, inp) (pc, gm, b, inp)),
       list_tree_config code ((tree,gm,inp)::treelist) ((pc,gm,b,inp)::threadlist).
-  
+
   Lemma ltc_app:
     forall code tl1 tl2 vl1 vl2
       (LTC1: list_tree_config code tl1 vl1)
@@ -153,14 +153,14 @@ 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 [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)
@@ -197,7 +197,7 @@ Section MemoEquiv.
     - right. split; auto. exists ts. exists gms. split; auto. lia.
   Qed.
 
-  
+
   Definition head_pc (stk:list config) : label :=
     match stk with
     | [] => 0
@@ -332,7 +332,7 @@ Section MemoEquiv.
       repeat invert_rep. simpl. rewrite CONSUME, READ. split; auto. split; auto.
       eapply tc_eq; eauto.
       2: { pike_subset. }
-      replace (pc + 1) with (S pc) by lia. auto.      
+      replace (pc + 1) with (S pc) by lia. auto.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
       repeat (econstructor; eauto). pike_subset.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
@@ -358,7 +358,7 @@ Section MemoEquiv.
     - repeat invert_rep. simpl. rewrite OPEN. split; auto.
       eapply tc_eq; eauto.
       2: { pike_subset. }
-      replace (pc+1) with (S pc) by lia. 
+      replace (pc+1) with (S pc) by lia.
       apply cons_bc with (pcmid:=end1); repeat (econstructor; eauto).
   Qed.
 
@@ -375,15 +375,15 @@ Section MemoEquiv.
     induction TREE; intros; subst; try inversion HeqTCLOSE; subst.
     - repeat invert_rep. simpl. rewrite CLOSE. split; auto.
       econstructor; eauto. 2: pike_subset.
-      replace (pc + 1) with (S pc) by lia. auto. 
+      replace (pc + 1) with (S pc) by lia. auto.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
       repeat (econstructor; eauto). pike_subset.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
     - destruct greedy; inversion CHOICE.
   Qed.
 
-  Lemma exec_reset:  
+  Lemma exec_reset:
     forall gidl tree inp code pc b gm,
       tree_config code (GroupAction (Reset gidl) tree, gm, inp) (pc,gm,b,inp)  ->
       stutters pc code = false ->
@@ -436,7 +436,7 @@ Section MemoEquiv.
     - repeat invert_rep. simpl. rewrite CHECK, ANCHOR. split; auto.
       eapply tc_eq; eauto.
       2: { pike_subset. }
-      replace (pc+1) with (S pc) by lia. 
+      replace (pc+1) with (S pc) by lia.
       assumption.
   Qed.
 
@@ -502,7 +502,7 @@ Section MemoEquiv.
               { constructor. replace (S pc+1+1) with (S (S (S pc))) by lia. auto. }
               repeat (econstructor; eauto).
             * apply tc_eq with (actions:=cont); auto. pike_subset.
-        }      
+        }
       + { (* Star *)
           destruct plus; inversion DINF.
           repeat invert_rep. destruct greedy; inversion CHOICE; subst.
@@ -670,14 +670,14 @@ Section MemoEquiv.
         exists pcstart. exists b. split; try split; try lia.
         * simpl. rewrite JMP. auto.
         * apply tc_eq with (actions:=Areg (Quantified greedy 0 (NoI.N 1 + NoI.N 0)%NoI r1) :: cont); try constructor; auto; pike_subset.
-          eapply tree_quant_free; eauto.        
+          eapply tree_quant_free; eauto.
       (* Star *)
       + destruct plus; inversion DINF. invert_rep.
         { invert_rep. invert_rep; try in_subset. destruct greedy; stutter. }
         exists pcstart. exists b. split; try split; try lia.
         * simpl. rewrite JMP. auto.
         * apply tc_eq with (actions:=Areg (Quantified greedy 0 (NoI.N 1 + +∞)%NoI r1) :: cont); try constructor; auto; pike_subset.
-          eapply tree_quant_free; eauto.        
+          eapply tree_quant_free; eauto.
       (* Unsupported *)
       + rewrite DUN in SUBSET. inversion SUBSET; inversion H1; inversion H4; subst; lia.
     - invert_rep.
@@ -722,7 +722,7 @@ Section MemoEquiv.
       unfold PikeVM.upd_label. eauto.
   Qed.
 
-  
+
 
   Theorem invariant_preservation:
   forall code mts1 mbs1 mbs2