bump Iris: update to stronger CAS requirements

77a45515 · Ralf Jung · 2645095c · 77a45515 · 77a45515 · 77a45515
Commit 77a45515 authored Jul 04, 2018 by Ralf Jung
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,9 +24,9 @@ theories/spanning_tree/spanning.v
 theories/spanning_tree/proof.v

 theories/concurrent_stacks/concurrent_stack1.v
-theories/concurrent_stacks/concurrent_stack2.v
+#theories/concurrent_stacks/concurrent_stack2.v
 theories/concurrent_stacks/concurrent_stack3.v
-theories/concurrent_stacks/concurrent_stack4.v
+#theories/concurrent_stacks/concurrent_stack4.v
 theories/concurrent_stacks/spec.v

 theories/logrel/prelude/base.v

--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-06-26.1.46cb853d") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-07-03.0.4c3f5b17") | (= "dev") }
  "coq-autosubst" { = "dev.coq86" }
 ]
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -16,13 +16,13 @@ Definition mk_stack : val :=
     match: !"r" with
       NONE => #-1
     | SOME "hd" =>
-       if: CAS "r" (SOME "hd") (Snd "hd")
-       then Fst "hd"
+       if: CAS "r" (SOME "hd") (Snd !"hd")
+       then Fst !"hd"
       else "pop" "n"
     end,
    rec: "push" "n" :=
       let: "r'" := !"r" in
-       let: "r''" := SOME ("n", "r'") in
+       let: "r''" := SOME (Alloc ("n", "r'")) in
       if: CAS "r" "r'" "r''"
       then #()
       else "push" "n").
@@ -31,9 +31,20 @@ Section stacks.
  Context `{!heapG Σ}.
  Implicit Types l : loc.

-  Definition is_stack_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
-     val -c> iProp Σ := λ v,
-    (v ≡ NONEV ∨ ∃ (h t : val), v ≡ SOMEV (h, t)%V ∗ P h ∗ ▷ F t)%I.
+  Definition oloc_to_val (h : option loc) : val :=
+    match h with
+    | None => NONEV
+    | Some l => SOMEV #l
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. rewrite /Inj /oloc_to_val=>??. repeat case_match; congruence. Qed.
+
+  Definition is_stack_pre (P : val → iProp Σ) (F : option loc -c> iProp Σ) :
+     option loc -c> iProp Σ := λ v,
+    (match v with
+     | None => True
+     | Some l => ∃ q h t, l ↦{q} (h, oloc_to_val t) ∗ P h ∗ ▷ F t
+     end)%I.

  Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P).
  Proof.
@@ -47,8 +58,8 @@ Section stacks.
  Definition is_stack P := unseal (is_stack_aux P).
  Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P).

-  Definition stack_inv P v :=
-    (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack P v')%I.
+  Definition stack_inv P l :=
+    (∃ ol, l ↦ oloc_to_val ol ∗ is_stack P ol)%I.


  Lemma is_stack_unfold (P : val → iProp Σ) v :
@@ -57,14 +68,15 @@ Section stacks.
    rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)).
  Qed.

-  Lemma is_stack_disj (P : val → iProp Σ) v :
-      is_stack P v -∗ is_stack P v ∗ (v ≡ NONEV ∨ ∃ (h t : val), v ≡ SOMEV (h, t)%V).
+  Lemma is_stack_copy (P : val → iProp Σ) ol :
+      is_stack P ol -∗ is_stack P ol ∗
+           (match ol with None => True | Some l => ∃ q h t, l ↦{q} (h, oloc_to_val t) end).
  Proof.
    iIntros "Hstack".
-    iDestruct (is_stack_unfold with "Hstack") as "[#Hstack|Hstack]".
-    - iSplit; try iApply is_stack_unfold; iLeft; auto.
-    - iDestruct "Hstack" as (h t) "[#Heq rest]".
-      iSplitL; try iApply is_stack_unfold; iRight; auto.
+    iDestruct (is_stack_unfold with "Hstack") as "Hstack". destruct ol; last first.
+    - iSplitL; try iApply is_stack_unfold; auto.
+    - iDestruct "Hstack" as (q h t) "[[Hl1 Hl2] [HP Hrest]]".
+      iSplitR "Hl2"; try iApply is_stack_unfold; simpl; eauto 10 with iFrame.
  Qed.

  (* Per-element invariant (i.e., bag spec). *)
@@ -80,9 +92,9 @@ Section stacks.
    wp_alloc l as "Hl".
    pose proof (nroot .@ "N") as N.
    rewrite -wp_fupd.
-    iMod (inv_alloc N _ (stack_inv P #l) with "[Hl]") as "#Hisstack".
-    iExists l, NONEV; iSplit; iFrame; auto.
-    { iApply is_stack_unfold. iLeft; auto. }
+    iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hisstack".
+    { iExists None; iFrame; auto.
+      iApply is_stack_unfold. auto. }
    wp_let.
    iModIntro.
    iApply "HΦ".
@@ -91,48 +103,36 @@ Section stacks.
      wp_rec.
      wp_bind (! #l)%E.
      iInv N as "Hstack" "Hclose".
-      iDestruct "Hstack" as (l' v') "[>% [Hl' Hstack]]".
-      injection H; intros; subst.
+      iDestruct "Hstack" as (v') "[Hl' Hstack]".
      wp_load.
-      iDestruct (is_stack_disj with "Hstack") as "[Hstack #Heq]".
-      iMod ("Hclose" with "[Hl' Hstack]").
-      iExists l', v'; iFrame; auto.
-      iModIntro.
-      iDestruct "Heq" as "[H | H]".
-      + iRewrite "H".
-        wp_match.
-        iRight; auto.
-      + iDestruct "H" as (h t) "H".
-        iRewrite "H".
-        assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val.
-        assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto).
-        wp_match. fold of_val.
-        unfold subst; simpl; fold subst.
+      destruct v' as [l'|]; simpl; last first.
+      + iMod ("Hclose" with "[Hl' Hstack]") as "_".
+        { rewrite /stack_inv. eauto with iFrame. }
+        iModIntro. wp_match. by iRight.
+      + iDestruct (is_stack_copy with "Hstack") as "[Hstack Hmy]".
+        iDestruct "Hmy" as (q h t) "Hl".
+        iMod ("Hclose" with "[Hl' Hstack]") as "_".
+        { rewrite /stack_inv. eauto with iFrame. }
+        iModIntro. wp_match.
+        wp_load. wp_proj.
        wp_bind (CAS _ _ _).
-        wp_proj.
        iInv N as "Hstack" "Hclose".
-        iDestruct "Hstack" as (l'' v'') "[>% [Hl'' Hstack]]".
-        injection H2; intros; subst.
-        assert (Decision (v'' = InjRV (h, t)%V)) as Heq by apply val_eq_dec.
-        destruct Heq.
-        * wp_cas_suc.
-          iDestruct (is_stack_unfold with "Hstack") as "[Hstack | Hstack]".
-          subst.
-          iDestruct "Hstack" as "%"; discriminate.
-          iDestruct "Hstack" as (h' t') "[% [HP Hstack]]".
-          subst.
-          injection H3.
-          intros.
-          subst.
+        iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
+        destruct (decide (oloc_to_val v'' = oloc_to_val (Some l'))) as [->%oloc_to_val_inj|Hne].
+        * simpl. wp_cas_suc.
+          iDestruct (is_stack_unfold with "Hstack") as "Hstack".
+          iDestruct "Hstack" as (q' h' t') "[Hl' [HP Hstack]]".
+          iDestruct (mapsto_agree with "Hl Hl'") as %[= <- <-%oloc_to_val_inj].
          iMod ("Hclose" with "[Hl'' Hstack]").
-          iExists l'', t'; iFrame; auto.
+          { iExists _. auto with iFrame. }
          iModIntro.
          wp_if.
+          wp_load.
          wp_proj.
          iLeft; auto.
-        * wp_cas_fail.
+        * simpl in Hne. wp_cas_fail.
          iMod ("Hclose" with "[Hl'' Hstack]").
-          iExists l'', v''; iFrame; auto.
+          { iExists v''; iFrame; auto. }
          iModIntro.
          wp_if.
          iApply "IH".
@@ -141,36 +141,31 @@ Section stacks.
      wp_rec.
      wp_bind (! _)%E.
      iInv N as "Hstack" "Hclose".
-      iDestruct "Hstack" as (l' v') "[>% [Hl' Hstack]]".
-      injection H; intros; subst.
+      iDestruct "Hstack" as (v') "[Hl' Hstack]".
      wp_load.
      iMod ("Hclose" with "[Hl' Hstack]").
-      by (iExists l', v'; iFrame).
+      { iExists v'. iFrame. }
      iModIntro.
      wp_let.
+      wp_alloc r'' as "Hr''".
      wp_let.
      wp_bind (CAS _ _ _).
      iInv N as "Hstack" "Hclose".
-      iDestruct "Hstack" as (l'' v'') "[>% [Hl'' Hstack]]".
-      injection H0; intros; subst.
-      assert (Decision (v'' = v'%V)) as Heq by apply val_eq_dec.
-      destruct Heq.
-      + wp_cas_suc.
-        iMod ("Hclose" with "[Hl'' HP Hstack]").
-        iExists l'', (InjRV (v, v')%V).
+      iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
+      wp_cas as ->%oloc_to_val_inj|_.
+      + destruct v'; by right.
+      + iMod ("Hclose" with "[Hl'' Hr'' HP Hstack]").
+        iExists (Some r'').
        iFrame; auto.
-        iSplit; auto.
+        iNext.
        iApply is_stack_unfold.
-        iRight.
-        iExists v, v'.
-        iSplit; auto.
-        subst; iFrame.
+        simpl.
+        iExists _, _, v'. iFrame.
        iModIntro.
        wp_if.
        done.
-      + wp_cas_fail.
-        iMod ("Hclose" with "[Hl'' Hstack]").
-        iExists l'', v''; iFrame; auto.
+      + iMod ("Hclose" with "[Hl'' Hstack]").
+        iExists v''; iFrame; auto.
        iModIntro.
        wp_if.
        iApply "IH".

--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
+(** THIS FILE CURRENTLY DOES NOT COMPILE because it has not been ported to the
+stricter CAS requirements yet. *)
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.

--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -14,13 +14,13 @@ Definition mk_stack : val :=
       (match: !"r" with
          NONE => NONE
        | SOME "hd" =>
-          if: CAS "r" (SOME "hd") (Snd "hd")
-          then SOME (Fst "hd")
+          if: CAS "r" (SOME "hd") (Snd !"hd")
+          then SOME (Fst !"hd")
          else "pop" "n"
        end),
    rec: "push" "n" :=
        let: "r'" := !"r" in
-        let: "r''" := SOME ("n", "r'") in
+        let: "r''" := SOME (Alloc ("n", "r'")) in
        if: CAS "r" "r'" "r''"
        then #()
        else "push" "n").
@@ -32,20 +32,27 @@ Section stack_works.
  Fixpoint is_stack xs v : iProp Σ :=
    (match xs with
     | [] => ⌜v = NONEV⌝
-     | x :: xs => ∃ (t : val), ⌜v = SOMEV (x, t)%V⌝ ∗ is_stack xs t
+     | x :: xs => ∃ q (l : loc) (t : val), ⌜v = SOMEV #l ⌝ ∗ l ↦{q} (x, t) ∗ is_stack xs t
     end)%I.

  Definition stack_inv P v :=
    (∃ l v' xs, ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack xs v' ∗ P xs)%I.

  Lemma is_stack_disj xs v :
-      is_stack xs v -∗ is_stack xs v ∗ (⌜v = NONEV⌝ ∨ ∃ (h t : val), ⌜v = SOMEV (h, t)%V⌝).
+      is_stack xs v -∗ is_stack xs v ∗ (⌜v = NONEV⌝ ∨ ∃ q (l : loc) (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{q} (h, t)).
  Proof.
    iIntros "Hstack".
    destruct xs.
    - iSplit; try iLeft; auto.
-    - iSplit; auto; iRight; iDestruct "Hstack" as (t) "[% Hstack]";
-      iExists v0, t; auto.
+    - simpl. iDestruct "Hstack" as (q l t) "[-> [[Hl Hl'] Hstack]]".
+      iSplitR "Hl"; eauto 10 with iFrame.
+  Qed.
+  Lemma is_stack_unboxed xs v :
+    is_stack xs v -∗ ⌜val_is_unboxed v⌝.
+  Proof.
+    iIntros "Hstack". iDestruct (is_stack_disj with "Hstack") as "[_ [->|Hdisj]]".
+    - done.
+    - iDestruct "Hdisj" as (???? ->) "_". done.
  Qed.

  Lemma is_stack_uniq : ∀ xs ys v,
@@ -53,38 +60,38 @@ Section stack_works.
  Proof.
    induction xs, ys; iIntros (v') "[Hstack1 Hstack2]"; auto.
    - iDestruct "Hstack1" as "%".
-      iDestruct "Hstack2" as (t) "[% Hstack2]".
+      iDestruct "Hstack2" as (???) "[% _]".
      subst.
      discriminate.
    - iDestruct "Hstack2" as "%".
-      iDestruct "Hstack1" as (t) "[% Hstack1]".
+      iDestruct "Hstack1" as (???) "[% _]".
      subst.
      discriminate.
-    - iDestruct "Hstack1" as (t) "[% Hstack1]".
-      iDestruct "Hstack2" as (t') "[% Hstack2]".
-      subst; injection H0; intros; subst.
-      iDestruct (IHxs with "[Hstack1 Hstack2]") as "%".
-        by iSplitL "Hstack1".
+    - simpl. iDestruct "Hstack1" as (q1 l1 t) "[% [Hl1 Hstack1]]".
+      iDestruct "Hstack2" as (q2 l2 t') "[% [Hl2 Hstack2]]".
+      subst; injection H0; intros; subst; clear H0.
+      iDestruct (mapsto_agree with "Hl1 Hl2") as %[= -> ->].
+      iDestruct (IHxs with "[Hstack1 Hstack2]") as "%". by iFrame.
      subst; auto.
  Qed.

  Lemma is_stack_empty : ∀ xs,
-      is_stack xs (InjLV #()) -∗ ⌜xs = []⌝.
+      is_stack xs NONEV -∗ ⌜xs = []⌝.
  Proof.
    iIntros (xs) "Hstack".
    destruct xs; auto.
-    iDestruct "Hstack" as (t) "[% rest]".
+    iDestruct "Hstack" as (?? t) "[% rest]".
    discriminate.
  Qed.
-  Lemma is_stack_cons : ∀ xs h t,
-      is_stack xs (InjRV (h, t)%V) -∗
-               is_stack xs (InjRV (h, t)%V) ∗ ∃ ys, ⌜xs = h :: ys⌝.
+  Lemma is_stack_cons : ∀ xs l,
+      is_stack xs (SOMEV #l) -∗
+               is_stack xs (SOMEV #l) ∗ ∃ q h t ys, ⌜xs = h :: ys⌝ ∗ l ↦{q} (h, t).
  Proof.
-    destruct xs; iIntros (h t) "Hstack".
+    iIntros ([|x xs] l) "Hstack".
    - iDestruct "Hstack" as "%"; discriminate.
-    - iSplit; [auto | iExists xs].
-      iDestruct "Hstack" as (t') "[% Hstack]".
-      injection H; intros; subst; auto.
+    - simpl. iDestruct "Hstack" as (q l' t') "[% [[Hl Hl'] Hstack]]".
+      injection H; intros; subst; clear H.
+      iSplitR "Hl'"; eauto 10 with iFrame.
  Qed.

  (* Whole-stack invariant (P). However:
@@ -117,7 +124,7 @@ Section stack_works.
      wp_bind (! _)%E.
      iInv N as "Hstack" "Hclose".
      iDestruct "Hstack" as (l' v' xs) "[>% [Hl' [Hstack HP]]]".
-      injection H; intros; subst.
+      injection H; intros; subst; clear H.
      wp_load.
      iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto.
      iDestruct "H" as "[% | H]".
@@ -131,10 +138,10 @@ Section stack_works.
        iModIntro.
        wp_match.
        iRight; auto.
-      * iDestruct "H" as (h t) "%".
+      * iDestruct "H" as (q l h t) "[% Hl]".
        subst.
        iMod ("Hclose" with "[Hl' Hstack HP]").
-        { iExists l', (InjRV (h, t)), xs; iSplit; iFrame; auto. }
+        { iExists l', _, xs; iSplit; iFrame; auto. }
        iModIntro.

        assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val.
@@ -142,27 +149,29 @@ Section stack_works.
        wp_match.
        unfold subst; simpl; fold of_val.

+        wp_load.
        wp_proj.
        wp_bind (CAS _ _ _).
        iInv N as "Hstack" "Hclose".
        iDestruct "Hstack" as (l'' v' ys) "[>% [Hl'' [Hstack HP]]]".
-        injection H2; intros; subst.
-        assert (Decision (v' = InjRV (h, t)%V)) as Heq by apply val_eq_dec.
+        injection H1; intros; subst; clear H1.
+        assert (Decision (v' = InjRV #l%V)) as Heq by apply val_eq_dec.
        destruct Heq.
-      + wp_cas_suc.
-        subst.
-        iDestruct (is_stack_cons with "Hstack") as "[Hstack H]".
-        iDestruct "H" as (ys') "%"; subst.
-        iDestruct "Hstack" as (t') "[% Hstack]".
-        injection H3; intros; subst.
+      + subst.
+        wp_cas_suc. destruct ys as [|y ys]; simpl.
+        { iDestruct "Hstack" as %?. done. }
+        iDestruct "Hstack" as (q'' l' t'') "[% [Hl' Hstack]]".
+        injection H1; intros; subst; clear H1.
        iDestruct "Hcont" as "[Hsucc _]".
        iDestruct ("Hsucc" with "[HP]") as "> [HQ HP]"; auto.
-        iMod ("Hclose" with "[Hl'' Hstack HP]").
-        { iExists l'', t', ys'; iSplit; iFrame; auto. }
+        iDestruct (mapsto_agree with "Hl Hl'") as %[= -> ->].
+        iMod ("Hclose" with "[Hl'' Hl' Hstack HP]").
+        { iExists l''. eauto 10 with iFrame. }
        iModIntro.
        wp_if.
+        wp_load.
        wp_proj.
-        iLeft; iExists h; auto.
+        iLeft; iExists _; auto.
      + wp_cas_fail.
        iMod ("Hclose" with "[Hl'' Hstack HP]").
        { iExists l'', v', ys; iSplit; iFrame; auto. }
@@ -175,24 +184,25 @@ Section stack_works.
      wp_bind (! _)%E.
      iInv N as "Hstack" "Hclose".
      iDestruct "Hstack" as (l' v' ys) "[>% [Hl' [Hstack HP]]]".
-      injection H; intros; subst.
+      injection H; intros; subst; clear H.
      wp_load.
      iMod ("Hclose" with "[Hl' Hstack HP]").
      { iExists l', v', ys; iSplit; iFrame; auto. }
      iModIntro.
      wp_let.
+      wp_alloc lp as "Hlp".
      wp_let.
      wp_bind (CAS _ _ _).
      iInv N as "Hstack" "Hclose".
      iDestruct "Hstack" as (l'' v'' xs) "[>% [Hl'' [Hstack HP]]]".
-      injection H0; intros; subst.
+      injection H; intros; subst; clear H.
+      iDestruct (is_stack_unboxed with "Hstack") as "#>%".
      assert (Decision (v' = v''%V)) as Heq by apply val_eq_dec.
      destruct Heq.
-      + wp_cas_suc.
+      + subst. wp_cas_suc.
        iDestruct ("Hpush" with "[HP]") as "> [HP HQ]"; auto.
-        iMod ("Hclose" with "[Hl'' Hstack HP]").
-        { iExists l'', (InjRV (v, v')), (v :: xs); iSplit; iFrame; auto.
-          iExists v'; iSplit; subst; auto. }
+        iMod ("Hclose" with "[Hl'' Hlp Hstack HP]").
+        { iExists l'', _, _. iFrame. simpl. eauto 10 with iFrame. }
        iModIntro.
        wp_if.
        done.

--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
+(** THIS FILE CURRENTLY DOES NOT COMPILE because it has not been ported to the
+stricter CAS requirements yet. *)
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.

--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -56,6 +56,14 @@ Section proof.
                   ⌜hd = SOMEV #l⌝ ∗ rown l (x, tl) ∗ is_list tl xs)%I
    end.

+  Lemma is_list_unboxed hd xs :
+    is_list hd xs -∗ ⌜val_is_unboxed hd⌝.
+  Proof.
+    destruct xs.
+    - iIntros (->). done.
+    - iIntros "Hl". iDestruct "Hl" as (?? ->) "_". done.
+  Qed.
+
  Lemma is_list_duplicate hd xs : is_list hd xs -∗ is_list hd xs ∗ is_list hd xs.
  Proof.
    iInduction xs as [ | x xs ] "IH" forall (hd); simpl; eauto.
@@ -155,6 +163,7 @@ Section proof.
    wp_alloc n as "Hn".
    wp_bind (CAS _ _ _).
    iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
+    iPoseProof (is_list_unboxed with "Hls") as "#>%".
    destruct (decide (o = o')) as [->|?].
    - wp_cas_suc.
      iMod ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".