Update dependencies

Author: anfelor

Makefile.coq.conf

@@ -46,7 +46,7 @@ COQMF_COQLIB=/Users/anton/.opam/AddressC/lib/coq/
 COQMF_COQCORELIB=/Users/anton/.opam/AddressC/lib/coq/../coq-core/
 COQMF_DOCDIR=/Users/anton/.opam/AddressC/share/doc/
 COQMF_OCAMLFIND=/Users/anton/.opam/AddressC/bin/ocamlfind
-COQMF_CAMLFLAGS=-thread -rectypes -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
+COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 COQMF_WARN=-warn-error +a-3
 COQMF_HASNATDYNLINK=true
 COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
@@ -67,5 +67,5 @@ COQMF_COQPROJECTNATIVEFLAG = no
 #                                                                             #
 ###############################################################################
 
-COQMF_OTHERFLAGS = '-w' '-notation-overridden' '-w' '-redundant-canonical-projection' '-w' '-convert_concl_no_check' '-w' '-undeclared-scope' '-w' '-cannot-define-projection' '-w' '-ambiguous-paths'
+COQMF_OTHERFLAGS = '-w' '-notation-overridden' '-w' '-redundant-canonical-projection' '-w' '-convert_concl_no_check' '-w' '-undeclared-scope' '-w' '-cannot-define-projection' '-w' '-ambiguous-paths' '-w' '-non-reversible-notation' '-w' '-notation-bound-to-variable' '-w' '-ltac2-missing-notation-var'
 COQMF_INSTALLCOQDOCROOT = fip_iris

README.md

@@ -8,7 +8,7 @@ All primitives come with a high degree of automation thanks to [Diaframe](https:
 used in particular to show correctness of various tree insertion 
 algorithms (see our [techreport][fiptree-tr]).
 
-[fiptree-tr]: https://www.microsoft.com/en-us/research/publication/a-functional-correspondence-between-top-down-and-bottom-up-tree-algorithms-fast-and-correct-fully-in-place-functions-with-first-class-constructor-contexts-and-zippers-tr/
+[fiptree-tr]: https://www.microsoft.com/en-us/research/publication/fiptree-tr/
 
 AddressC is especially powerful for imperative algorithms which arise naturally from a functional version.
 As an example, take the `reverse` function:
@@ -95,11 +95,11 @@ to obtain AddressC code which corresponds closely to the pseudo-code presented i
 original papers. To learn more about this work,
 please refer [to our paper][fiptree-tr]:
 ```
-@TechReport{Lorenzen:correspondence,
+@TechReport{Lorenzen:bst-essence,
   author = {Lorenzen, Anton and Leijen, Daan and Swierstra, Wouter and Lindley, Sam},
-  title = {A Functional Correspondence between Top-down and Bottom-up Tree Algorithms},
+  title = {The Functional Essence of Imperative Binary Search Trees},
   year = 2023,
-  month = Jul,
+  month = Dec,
   institution = {Microsoft Research},
   number = {MSR-TR-2023-28}
 }
@@ -110,15 +110,15 @@ please refer [to our paper][fiptree-tr]:
 The Coq code is known to compile with:
 
 ```
-coq                         8.17.0                     The Coq Proof Assistant
-coq-core                    8.17.0                     The Coq Proof Assistant -- Core Binaries and Tools
-coq-diaframe                dev.2023-06-15.0.1c3b5549  Diaframe: Automation for Iris
-coq-diaframe-heap-lang      dev.2023-06-15.0.1c3b5549  Diaframe: Automation for Iris's Heap Lang
-coq-equations               1.3+8.17                   A function definition package for Coq
-coq-iris                    dev.2023-06-14.0.f0e415b6  A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
-coq-iris-heap-lang          dev.2023-06-14.0.f0e415b6  The canonical example language for Iris
-coq-stdlib                  8.17.0                     The Coq Proof Assistant -- Standard Library
-coq-stdpp                   dev.2023-06-01.0.d1254759  An extended "Standard Library" for Coq
+coq                    8.19.1                    The Coq Proof Assistant
+coq-core               8.19.1                    The Coq Proof Assistant -- Core Binaries and Tools
+coq-diaframe           dev.2024-02-21.0.9c606e4f Diaframe: Automation for Iris
+coq-diaframe-heap-lang dev.2024-02-21.0.9c606e4f Diaframe: Automation for Iris's Heap Lang
+coq-equations          1.3+8.19                  A function definition package for Coq
+coq-iris               dev.2024-02-16.1.06f499e0 A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
+coq-iris-heap-lang     dev.2024-02-16.1.06f499e0 The canonical example language for Iris
+coq-stdlib             8.19.1                    The Coq Proof Assistant -- Standard Library
+coq-stdpp              dev.2024-02-09.0.cafd7113 An extended "Standard Library" for Coq
 ```
 
 ## Compilation

_CoqProject

@@ -12,6 +12,12 @@
 -arg -w -arg -ambiguous-paths
 -arg -native-compiler -arg no
 
+# Disable notation warnings for our C-style syntax
+-arg -w -arg -non-reversible-notation
+-arg -w -arg -notation-bound-to-variable
+
+# TODO: New warning which fires for our C-style variable hack
+-arg -w -arg -ltac2-missing-notation-var
 
 theories/idents.v
 theories/lang.v

theories/append_wand.v

@@ -65,11 +65,11 @@ Proof.
         wp_heap. wp_enter_loop. wp_heap. iModIntro.
         iExists xx, _, (compose acc (fun ys' => x :: ys')), p', (p'' +ₗ 1%nat).
         unfold array at 1. iDecompose "Hp". iFrame. iSplitL.
-        - iSteps. unfold array. iSteps.
+        - iSteps.
         - done. }
     + iExists xs, _, (fun ys' => z :: ys'), p, (p +ₗ 1%nat).
-      iFrame. unfold array. iDecompose "Hp". iFrame.
-      iSplitL. 1: unfold array; iSteps. iSteps. 
+      fold is_list. unfold array. iFrame.
+      iDecompose "Hp" as "p0 p1". iSplitL "p0"; iSteps.
 Qed.
 
 End proof.

theories/lang.v

@@ -42,8 +42,7 @@ End Private.
 
 Notation "'var:' x := e1 'in' e2" :=
   (Lam (ident_to_string! x)%binder ((fun (x : expr) => e2%E) (Load (ident_to_string! x)%binder)) (Alloc e1%E))
-  (at level 100, x at level 100, e1, e2 at level 200, right associativity,
-   format "'[' 'var:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+  (at level 100, x at level 100, e1, e2 at level 200, right associativity) : expr_scope.
 
 Notation "'var:' x := e1 'in' e2" :=
   (Lam x%binder e2%V (Alloc e1%V))
@@ -78,8 +77,7 @@ Notation "'fun:' ( a ) { e }" :=
     ((fun a =>
       e%E)
     (Load (ident_to_string! a)%binder)))
-  (at level 200, a at level 1, e at level 200,
-   format "'[' 'fun:' ( a ) '/  ' { e } ']'").
+  (at level 200, a at level 1, e at level 200).
 
 Notation "'fun:' ( a , b ) { e }" :=
   (LamV (ident_to_string! a)%binder
@@ -89,8 +87,7 @@ Notation "'fun:' ( a , b ) { e }" :=
           e%E)
         (Load (ident_to_string! b)%binder))))
     (Load (ident_to_string! a)%binder)))
-  (at level 200, a, b at level 1, e at level 200,
-   format "'[' 'fun:' ( a , b ) '/  ' { e } ']'").
+  (at level 200, a, b at level 1, e at level 200).
 
 Notation "'fun:' ( a , b , c ) { e }" :=
   (LamV (ident_to_string! a)%binder
@@ -103,8 +100,7 @@ Notation "'fun:' ( a , b , c ) { e }" :=
             (Load (ident_to_string! c)%binder))))
         (Load (ident_to_string! b)%binder))))
     (Load (ident_to_string! a)%binder)))
-  (at level 200, a, b, c at level 1, e at level 200,
-   format "'[' 'fun:' ( a , b , c ) '/  ' { e } ']'").
+  (at level 200, a, b, c at level 1, e at level 200).
 
 Notation "'fun:' ( a , b , c , d ) { e }" :=
   (LamV (ident_to_string! a)%binder
@@ -120,8 +116,7 @@ Notation "'fun:' ( a , b , c , d ) { e }" :=
             (Load (ident_to_string! c)%binder))))
         (Load (ident_to_string! b)%binder))))
     (Load (ident_to_string! a)%binder)))
-  (at level 200, a, b, c, d at level 1, e at level 200,
-   format "'[' 'fun:' ( a , b , c , d ) '/  ' { e } ']'").
+  (at level 200, a, b, c, d at level 1, e at level 200).
 
 Notation "'fun:' ( a , b , c , d , e ) { e2 }" :=
   (LamV (ident_to_string! a)%binder
@@ -140,8 +135,7 @@ Notation "'fun:' ( a , b , c , d , e ) { e2 }" :=
             (Load (ident_to_string! c)%binder))))
         (Load (ident_to_string! b)%binder))))
     (Load (ident_to_string! a)%binder)))
-  (at level 200, a, b, c, d, e at level 1, e2 at level 200,
-   format "'[' 'fun:' ( a , b , c , d , e ) '/  ' { e2 } ']'").
+  (at level 200, a, b, c, d, e at level 1, e2 at level 200).
 
 Notation "'ret:' e" := e%E (at level 20) : expr_scope. 
 
@@ -285,39 +279,56 @@ End proofs.
 
 (* --------- Tactics ----------- *)
 
+(* We wan to call iSplitL using a selection pattern which includes a fresh ident,
+   but unfortunately the current implementation does not support this.
+   Thus, we duplicate the iSplitL tactic here: *)
+Tactic Notation "ISplitL" constr(Hs) :=
+  iStartProof;
+  let Δ := iGetCtx in
+  eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
+    [tc_solve ||
+     let P := match goal with |- FromSep ?P _ _ => P end in
+     fail "iSplitL:" P "not a separating conjunction"
+    |pm_reduce;
+     lazymatch goal with
+     | |- False => let Hs := iMissingHypsCore Δ Hs in
+                 fail "iSplitL: hypotheses" Hs "not found"
+     | _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
+     end].
+
 Tactic Notation "wp_begin" constr(x1) :=
   let phi := fresh "Φ" in
   let Hphi := iFresh in
   iIntros (phi); iIntros x1; iIntros [IIdent Hphi];
-  wp_rec; wp_apply wp_wand_l; iFrame; repeat wp_lam; clear phi.
+  wp_rec; wp_apply wp_wand_l; ISplitL [Hphi]; first iFrame; repeat wp_lam; clear phi.
 
 Tactic Notation "wp_begin" constr(x1) ";" ident(x2) :=
   let phi := fresh "Φ" in
   let Hphi := iFresh in
   iIntros (phi); iIntros x1; iIntros [IIdent Hphi];
   wp_alloc x2;
-  wp_rec; wp_apply wp_wand_l; iFrame; repeat wp_lam; clear phi.
+  wp_rec; wp_apply wp_wand_l; ISplitL [Hphi]; first iFrame; repeat wp_lam; clear phi.
 
 Tactic Notation "wp_begin" constr(x1) ";" ident(x2) "," ident(x3) :=
   let phi := fresh "Φ" in
   let Hphi := iFresh in
   iIntros (phi); iIntros x1; iIntros [IIdent Hphi];
   wp_alloc x3; wp_alloc x2;
-  wp_rec; wp_apply wp_wand_l; iFrame; repeat wp_lam; clear phi.
+  wp_rec; wp_apply wp_wand_l; ISplitL [Hphi]; first iFrame; repeat wp_lam; clear phi.
 
 Tactic Notation "wp_begin" constr(x1) ";" ident(x2) "," ident(x3) "," ident(x4) :=
   let phi := fresh "Φ" in
   let Hphi := iFresh in
   iIntros (phi); iIntros x1; iIntros [IIdent Hphi];
   wp_alloc x4; wp_alloc x3; wp_alloc x2;
-  wp_rec; wp_apply wp_wand_l; iFrame; repeat wp_lam; clear phi.
+  wp_rec; wp_apply wp_wand_l; ISplitL [Hphi]; first iFrame; repeat wp_lam; clear phi.
 
 Tactic Notation "wp_begin" constr(x1) ";" ident(x2) "," ident(x3) "," ident(x4) "," ident(x5) :=
   let phi := fresh "Φ" in
   let Hphi := iFresh in
   iIntros (phi); iIntros x1; iIntros [IIdent Hphi];
   wp_alloc x5; wp_alloc x4; wp_alloc x3; wp_alloc x2;
-  wp_rec; wp_apply wp_wand_l; iFrame; repeat wp_lam; clear phi.
+  wp_rec; wp_apply wp_wand_l; ISplitL [Hphi]; first iFrame; repeat wp_lam; clear phi.
 
 Tactic Notation "wp_var" ident(x) :=
   wp_alloc x; wp_let.
@@ -380,8 +391,14 @@ Tactic Notation "wp_heap" :=
         || wp_load_offset || wp_store_offset
         || let x := fresh in (wp_alloc x; try done) ).
 
+Tactic Notation "if_decide" :=
+  let H := fresh in case_bool_decide as H; try inversion H.
+
+Tactic Notation "invalid_case" :=
+  (subst; done) || lia.
+
 Tactic Notation "wp_type" :=
-  iSteps; try (repeat case_bool_decide; iSteps).
+  iSteps; try (repeat if_decide; try invalid_case; iSteps).
 
 Tactic Notation "wp_while" constr(Hinv) :=
   wp_apply (wp_while_inv Hinv).

theories/splay_bu.v

@@ -248,9 +248,9 @@ Proof.
     destruct t' as [|l x r].
     + iDecompose "Ht". wp_type.
     + iDestruct "Ht" as (? ? ?) "[-> [? [Hl Hr]]]". wp_heap.
-      unfold bu_insert_go at 1. case_bool_decide; wp_heap.
+      unfold bu_insert_go at 1. if_decide; wp_heap.
       { wp_type. }
-      { case_bool_decide; wp_heap.
+      { if_decide; wp_heap.
         - destruct l; iDecompose "Hl"; wp_heap; wp_type.
         - destruct r; iDecompose "Hr"; wp_heap; wp_type. }
   - wp_type.

theories/splay_td.v

@@ -137,14 +137,14 @@ Proof.
     destruct t' as [|l x r].
     + iDecompose "Ht". wp_heap. wp_type.
     + iDestruct "Ht" as (? ? ?) "(-> & ? & Hl & Hr)". wp_heap.
-      unfold td_insert_go at 1. case_bool_decide; wp_heap. { wp_type. }
-      { case_bool_decide; wp_heap.
+      unfold td_insert_go at 1. if_decide; wp_heap. { wp_type. }
+      { if_decide; wp_heap.
         - destruct l; iDecompose "Hl".
           + wp_heap. wp_type.
-          + wp_heap. case_bool_decide; wp_heap; wp_type.
+          + wp_heap. if_decide; wp_heap; wp_type.
         - destruct r; iDecompose "Hr".
           + wp_heap. wp_type.
-          + wp_heap. case_bool_decide; wp_heap; wp_type; iExFalso; lia. }
+          + wp_heap. if_decide; wp_heap; wp_type. }
   - wp_type.
 Qed.
 

theories/tree_td.v

@@ -23,7 +23,7 @@ Proof. iSteps. Qed.
 Instance is_tree_node_hint (p : loc) (x : Z) (l_r l_l : val) t :
 HINT ε₁ ✱ [ l r ; (p +ₗ 0) ↦ l_l ∗ (p +ₗ 1) ↦ #x ∗ (p +ₗ 2) ↦ l_r ∗ is_tree l l_l ∗ is_tree r l_r ∗ ⌜t = Node l x r⌝]
   ⊫ [id]; is_tree t #p ✱ [⌜t = Node l x r⌝].
-Proof. unfold is_tree, array. simpl. iSteps. Qed.
+Proof. iSteps. Qed.
 
 (* We want to figure out if a tree is a Leaf or a Node from the "t != NULL" check.
    To achieve this, Ike Mulder wrote this typeclass inference code. *)
@@ -119,22 +119,22 @@ Lemma tree_of_ctx (z : ctx) (t : tree) (zv : loc) (hv : loc) (tv : val) :
 Proof.
   iIntros "[Hz [Hhv Ht]]". iInduction z as [|z x r|l x z] "IH" forall (zv hv t).
   - iDecompose "Hz". iSteps.
-  - iDecompose "Hz" as (? ? ?) "H1 H2 H3 H4". iExists #x. iFrame.
+  - iDecompose "Hz" as (? ? ?) "H1 H2 H3 H4". iExists #x. iSteps.
     iPoseProof ("IH" $! (Loc.add x 0) hv t with "H3 Hhv Ht") as "[%l' [H1' H2']]".
-    iExists x, l', x0. unfold array, harray. iSteps.
-  - iDecompose "Hz" as (? ? ?) "H1 H2 H3 H4". iExists #x0. iFrame.
+    iExists l', x0. unfold array, harray. iSteps.
+  - iDecompose "Hz" as (? ? ?) "H1 H2 H3 H4". iExists #x0. iSteps.
     iPoseProof ("IH" $! (Loc.add x0 2) hv t with "H3 Hhv Ht") as "[%r' [H1' H2']]".
-    iExists x0, x1, r'. unfold array, harray. iSteps.
+    iExists x1, r'. unfold array, harray. iSteps.
 Qed.
 
 Lemma ctx0_of_ctx (z1 : ctx) (z2 : ctx) (zv1 : loc) (hv1 : loc) (zv2 : loc) (hv2 : loc) :
     is_ctx z1 zv1 hv1 ∗ hv1 ↦ #zv2 ∗ is_ctx0 z2 zv2 hv2 -∗ ∃ (zv1' : loc), zv1 ↦ #zv1' ∗ is_ctx0 (comp z1 z2) zv1' hv2.
 Proof.
   iIntros "[Hz [Hhv Ht]]". iInduction z1 as [|z x r|l x z] "IH" forall (zv1 hv1 z2 zv2 hv2).
   - iDecompose "Hz". iExists zv2. iFrame.
-  - iDecompose "Hz". iExists x. iFrame. iExists x0. iFrame.
+  - iDecompose "Hz". iExists x. iFrame.
     iApply (ctx_of_ctx0). iSteps. repeat rewrite (Loc.add_0). iSteps.
-  - iDecompose "Hz". iExists x0. iFrame. iExists x1. iFrame.
+  - iDecompose "Hz". iExists x0. iFrame.
     iApply (ctx_of_ctx0). iSteps. repeat rewrite (Loc.add_0). iSteps.
 Qed.
 

theories/zip.v

@@ -30,8 +30,7 @@ Lemma heap_is_higher_rank_correct `{!heapGS Σ} (rk1 rk2 x1 x2 : Z) :
     heap_is_higher_rank #rk1 #rk2 #x1 #x2
   {{{ v, RET v; ∃ (b : bool), ⌜v = #b⌝ ∗ ⌜b = is_higher_rank rk1 rk2 x1 x2⌝ }}}.
 Proof.
-  wp_begin "H". unfold is_higher_rank.
-  repeat case_bool_decide; iSteps.
+  wp_begin "H". unfold is_higher_rank. repeat case_bool_decide; iSteps.
 Qed.
 
 (* Recursive *)

theories/zip_bu.v

@@ -230,7 +230,7 @@ Proof.
       iIntros (v) "[%b [Hv Hb]]". unfold bu_insert_go.
       destruct b; iDestruct "Hv" as %->; iDestruct "Hb" as %<-.
       { wp_type. }
-      { wp_heap. case_bool_decide.
+      { wp_heap. if_decide.
         - wp_type.
         - wp_pures. wp_load. wp_alloc Hk as "Hk'". wp_load. wp_alloc Ht as "Ht'".
           wp_apply (heap_unzip_correct (Node rk l x r) k with "[Hp Hl Hr Hk' Ht']").