Bump Iris (⊢ changes).

opam

@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
 depends: [
-  "coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") }
+  "coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
 ]

theories/lib/locking_heap.v

@@ -212,7 +212,7 @@ Lemma to_heap_block_info_valid τ : ✓ to_heap_block_info τ.
 Proof. intros l. rewrite lookup_fmap. by destruct (τ !! l) as [[]|]. Qed.
 
 Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
-  (|==> ∃ _ : locking_heapG Σ, full_locking_heap ∅)%I.
+  ⊢ |==> ∃ _ : locking_heapG Σ, full_locking_heap ∅.
 Proof.
   iMod (own_alloc (● to_locking_heap ∅)) as (γ1) "Hh1".
   { by apply auth_auth_valid. }

theories/tests/fact.v

@@ -23,7 +23,7 @@ Section factorial_spec.
   Qed.
 
   Lemma factorial_spec (n: nat) R :
-    CWP factorial #n @ R {{ v, ⌜v = #(fact n)⌝ }}%I.
+    ⊢ CWP factorial #n @ R {{ v, ⌜v = #(fact n)⌝ }}%I.
   Proof.
     iApply cwp_fun; simpl. vcg. iIntros (r c) "**".
     iApply (cwp_wand _ (λ _, c ↦C #n ∗ r ↦C #(fact n))%I with "[-]"); last first.

theories/tests/gcd.v

@@ -51,7 +51,7 @@ Section gcd_spec.
   Qed.
 
   Lemma gcd_robbert_thesis_spec (a b : nat) R :
-    CWP gcd_robbert_thesis (#a, #b)%V @ R {{ v, ⌜v = #(Nat.gcd a b)⌝ }}%I.
+    ⊢ CWP gcd_robbert_thesis (#a, #b)%V @ R {{ v, ⌜v = #(Nat.gcd a b)⌝ }}%I.
   Proof.
     iApply cwp_fun; simpl. vcg; iIntros (p q) "**". iApply (cwp_wand _ (λ _,
       p ↦C #(Nat.gcd a b) ∗ q ↦C #0)%I with "[-]"); last first.

theories/tests/invoke.v

@@ -20,7 +20,7 @@ Section tests_vcg.
     (c_ret "v1") +ᶜ (c_ret "v2").
 
   Lemma test_invoke_2 R :
-    CWP callᶜ (c_ret plus_pair) (♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I.
+    ⊢ CWP callᶜ (c_ret plus_pair) (♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I.
   Proof.
     iIntros. vcg. iIntros "$ !> !>". cwp_lam. vcg. by vcg_continue.
   Qed.

theories/tests/unknowns.v

@@ -31,7 +31,7 @@ Section tests_vcg.
      implementation-defined behaviour *)
   Lemma test3 (n : nat) (m : Z) :
     1 ≤ n →
-    CWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }}%I.
+    ⊢ CWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }}%I.
   Proof.
     intros. vcg. iExists (n). repeat iSplit; eauto.
     { iPureIntro. lia. }
@@ -42,7 +42,7 @@ Section tests_vcg.
 
   Lemma test3_NOMATCH (n m : Z) :
     1 ≤ n →
-    CWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }}%I.
+    ⊢ CWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }}%I.
   Proof.
     intros. vcg.
     match goal with

theories/vcgen/denv.v

@@ -764,7 +764,7 @@ Section denv.
 
   Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
     denv_delete_frac_stack i ms = Some (ms', q, dv) → Forall (denv_wf E) ms →
-    denv_stack_interp E ms ms' (dloc_var_interp E i ↦C{Q_to_Qp q} dval_interp E dv).
+    ⊢ denv_stack_interp E ms ms' (dloc_var_interp E i ↦C{Q_to_Qp q} dval_interp E dv).
   Proof.
     intros Hi Hms. iInduction Hms as [|m ms] "IH" forall (ms' Hi); simplify_eq/=.
     destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:?; simplify_eq/=.
@@ -779,7 +779,7 @@ Section denv.
   Lemma denv_delete_full_stack_interp E i ms ms' q dv :
     denv_delete_full_stack_aux i ms = Some (ms', q, dv) →
     Forall (denv_wf E) ms →
-    denv_stack_interp E ms ms' (dloc_var_interp E i ↦C{Q_to_Qp q} dval_interp E dv).
+    ⊢ denv_stack_interp E ms ms' (dloc_var_interp E i ↦C{Q_to_Qp q} dval_interp E dv).
   Proof.
     intros Hi Hms. iInduction Hms as [|m ms] "IH" forall (ms' q dv Hi); simplify_eq/=.
     destruct (denv_delete_full_aux i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
@@ -805,7 +805,7 @@ Section denv.
   Lemma denv_delete_frac_2_interp E i ms m ms' m' q dv :
     denv_delete_frac_2 i ms m = Some (ms', m', q, dv) →
     Forall (denv_wf E) ms → denv_wf E m →
-    denv_stack_interp E ms ms' (denv_interp E m -∗
+    ⊢ denv_stack_interp E ms ms' (denv_interp E m -∗
       denv_interp E m' ∗ dloc_var_interp E i ↦C{Q_to_Qp q} dval_interp E dv).
   Proof.
     rewrite /denv_delete_frac_2 /denv_wf. intros ?? [??]%andb_True.
@@ -823,7 +823,7 @@ Section denv.
   Lemma denv_delete_full_2_interp E i ms m ms' m' dv :
     denv_delete_full_2 i ms m = Some (ms', m', dv) →
     Forall (denv_wf E) ms → denv_wf E m →
-    denv_stack_interp E ms ms' (denv_interp E m -∗
+    ⊢ denv_stack_interp E ms ms' (denv_interp E m -∗
       denv_interp E m' ∗ dloc_var_interp E i ↦C dval_interp E dv).
   Proof.
     rewrite /denv_delete_full_2 /denv_wf. intros ???.

theories/vcgen/forward.v

@@ -171,7 +171,7 @@ Section forward_spec.
 
   Lemma dexpr_eval_correct E de dv :
     dexpr_eval de = Some dv →
-    WP dexpr_interp E de {{ v, ⌜v = dval_interp E dv⌝ }}%I.
+    ⊢ WP dexpr_interp E de {{ v, ⌜v = dval_interp E dv⌝ }}%I.
   Proof.
     iIntros (Hde). iInduction de as [] "IH" forall (dv Hde); simplify_option_eq.
     - by iApply wp_value.
@@ -189,7 +189,7 @@ Section forward_spec.
   Lemma forward_aux_correct E de ms ms' mNew dv R n :
     forward_aux E n ms de = Some (ms', mNew, dv) →
     Forall (denv_wf E) ms → dcexpr_wf E de →
-    denv_stack_interp E ms ms' (CWP dcexpr_interp E de @ R
+    ⊢ denv_stack_interp E ms ms' (CWP dcexpr_interp E de @ R
       {{ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew }})%I.
   Proof.
     iIntros (Hsp Hms Hde).