From eb34c4bc0d35676f7a12d1cbde1530dd56cbf333 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 11 Aug 2021 12:25:04 +0200
Subject: [PATCH] Bump dependency

---
 coq-lambda-rust.opam                       | 2 +-
 theories/lang/spawn.v                      | 2 +-
 theories/typing/lib/arc.v                  | 8 ++++----
 theories/typing/lib/brandedvec.v           | 2 +-
 theories/typing/lib/rc/rc.v                | 8 ++++----
 theories/typing/lib/refcell/ref_code.v     | 8 ++++----
 theories/typing/lib/refcell/refcell_code.v | 4 ++--
 theories/typing/lib/refcell/refmut_code.v  | 6 +++---
 theories/typing/own.v                      | 2 +-
 9 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index f71b1606..b67874bb 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-08-10.0.d486f5e1") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-08-11.1.57194191") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 19a617f9..a5e4797c 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -91,7 +91,7 @@ Lemma spawn_spec Ψ e (f : val) tid :
   {{{ γc γe c, RET #c; join_handle γc γe c Ψ }}}.
 Proof.
   iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
-  wp_let. wp_alloc l as "Hl" "H†". wp_let.
+  wp_let. wp_alloc l as "Hm" "Hl" "H†". wp_let.
   iMod (own_alloc (Excl ())) as (γe) "Hγe"; first done.
   rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "Hl" as "[Hc Hd]". wp_write.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 33810f34..f584e7c5 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1162,7 +1162,7 @@ Section arc.
     - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
       wp_apply wp_new=>//; [set_solver+|lia|].
-      iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>". rewrite -!lock Nat2Z.id.
+      iIntros (l) "(H† & Hlvl & Hml) (#Hν & Hown & H†') !>". rewrite -!lock Nat2Z.id.
       wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
       wp_op. wp_op. iDestruct "Hown" as (vl) "[H↦ Hown]".
@@ -1184,7 +1184,7 @@ Section arc.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
     - iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
-      iIntros (l) "/= (H† & Hl)". wp_let. wp_op.
+      iIntros (l) "/= (H† & Hl & Hm)". wp_let. wp_op.
       rewrite heap_mapsto_vec_singleton. wp_write. wp_let.
       wp_bind (of_val clone).
       iApply (wp_wand with "[Hna]").
@@ -1202,9 +1202,9 @@ Section arc.
       iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %Hsz.
       iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
-      wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl')". wp_let. wp_op.
+      wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl' & Hm')". wp_let. wp_op.
       rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
-      rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+      rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
       wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [done|..].
       { by rewrite repeat_length. } { by rewrite Hsz. }
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 51ccdcc2..677d1e25 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -182,7 +182,7 @@ Section typing.
     wp_let.
     wp_op. rewrite bool_decide_false; [|lia].
     wp_case.
-    wp_alloc n as "Hn" "Hdead".
+    wp_alloc n as "Hm" "Hn" "Hdead".
     wp_let.
     rewrite !heap_mapsto_vec_singleton.
     wp_write.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 9a965176..f23113f4 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1049,7 +1049,7 @@ Section code.
         wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
         iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; [set_solver+|lia|done|].
         rewrite -!lock Nat2Z.id.
-        iNext. iIntros (lr) "/= ([H†|%] & H↦lr) [Hty Hproto] !>"; last lia.
+        iNext. iIntros (lr) "/= ([H†|%] & H↦lr & Hm) [Hty Hproto] !>"; last lia.
         rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
         wp_let. wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_op. wp_op.
         iDestruct "Hty" as (vlr) "[H↦vlr Hty]". rewrite shift_loc_assoc.
@@ -1072,7 +1072,7 @@ Section code.
         iApply type_assign; [solve_typing..|].
         iApply type_jump; solve_typing.
     - wp_apply wp_new; [done|lia|done|].
-      iIntros (lr) "/= ([H†|%] & H↦lr)"; last lia.
+      iIntros (lr) "/= ([H†|%] & H↦lr & Hm)"; last lia.
       iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
       iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
       rewrite heap_mapsto_vec_singleton. wp_write.
@@ -1107,9 +1107,9 @@ Section code.
       iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %Hsz.
       iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
-      wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl')". wp_let. wp_op.
+      wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl' & Hm')". wp_let. wp_op.
       rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
-      rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+      rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
       wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]");
         [by rewrite ?repeat_length ?Hsz //..|].
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 1efbe3bb..6d7bb9c4 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -74,7 +74,7 @@ Section ref_functions.
       - by rewrite /= agree_idemp.
       - apply frac_valid. rewrite /= -Hq'q'' comm_L.
         by apply Qp_add_le_mono_l, Qp_div_le. }
-    wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr)".
+    wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr&?)".
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
@@ -222,7 +222,7 @@ Section ref_functions.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; try done.
-    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -301,7 +301,7 @@ Section ref_functions.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; [done..|].
-    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -343,7 +343,7 @@ Section ref_functions.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
       iFrame. }
-    iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefs) "[Hrefs† Hrefs]".
+    iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefs) "(Hrefs† & Hrefs & ?)".
     rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
     iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 138cd08a..ff38fa76 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -167,7 +167,7 @@ Section refcell_functions.
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
       simpl. iApply type_jump; solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
-      iIntros (lref) "(H† & Hlref)". wp_let.
+      iIntros (lref) "(H† & Hlref & Hlm)". wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
@@ -267,7 +267,7 @@ Section refcell_functions.
     iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
     - wp_write. wp_apply wp_new; [done..|].
-      iIntros (lref) "(H† & Hlref)". wp_let.
+      iIntros (lref) "(H† & Hlref & Hm)". wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       destruct st as [[[[ν []] s] n]|]; try done.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 94722140..893d3a09 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -193,7 +193,7 @@ Section refmut_functions.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν q γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; first done. done. done.
-    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -272,7 +272,7 @@ Section refmut_functions.
     iDestruct "Hrefmut" as "[[Hrefmut↦1 Hrefmut↦2] Hrefmut]".
     iDestruct "Hrefmut" as (ν qν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; [done..|].
-    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -317,7 +317,7 @@ Section refmut_functions.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
       iFrame. }
-    iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefmuts) "[Hrefmuts† Hrefmuts]".
+    iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefmuts) "(Hrefmuts† & Hrefmuts & ?)".
     rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
     iDestruct "Hrefmuts" as "(Hrefmuts1 & Hrefmuts2 & Hrefmuts3 & Hrefmuts4)".
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 1fa5fb5c..47500610 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -255,7 +255,7 @@ Section typing.
   Proof.
     iIntros (? tid qmax) "#LFT #HE $ $ _".
     iApply wp_new; try done. iModIntro.
-    iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
+    iIntros (l) "(H† & Hlft & Hmeta)". rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
     iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length.
   Qed.
-- 
GitLab