From a0b45f8c50065871205abfca899644271cc4751c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2021 09:34:01 +0100
Subject: [PATCH] update dependencies
---
coq-lambda-rust.opam | 2 +-
theories/lang/lib/arc.v | 8 ++++----
theories/lifetime/model/reborrow.v | 2 +-
theories/typing/lib/rc/rc.v | 4 ++--
theories/typing/lib/rc/weak.v | 4 ++--
theories/typing/lib/refcell/ref_code.v | 4 ++--
theories/typing/lib/refcell/refcell_code.v | 2 +-
theories/typing/lib/refcell/refmut_code.v | 2 +-
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
9 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index e17cdd0a..6e7efb62 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2021-01-26.2.79f2f36f") | (= "dev") }
+ "coq-iris" { (= "dev.2021-02-10.0.7b4a04ce") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 90d563ba..c648706c 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -274,12 +274,12 @@ Section arc.
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
- apply frac_valid'. rewrite -Hq comm_L.
+ apply frac_valid. rewrite -Hq comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw Hâ— HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
- rewrite [(qq / 2)%Qp â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
+ rewrite [(qq / 2)%Qp â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
@@ -405,10 +405,10 @@ Section arc.
{ apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
apply op_local_update_discrete=>Hv. constructor; last done.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
- apply frac_valid'. rewrite /= -Heq comm_L.
+ apply frac_valid. rewrite /= -Heq comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
- rewrite /= [xH â‹… _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
+ rewrite /= [xH â‹… _]comm_L frac_op [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
Qp_div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
iExists q. auto with iFrame.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 8d85d84c..721a53a4 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -94,7 +94,7 @@ Proof.
iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
- iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+ iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
by iFrame.
Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 30f9e0d1..a02cd0c7 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -590,13 +590,13 @@ Section code.
iMod (own_update with "Hrcâ—") as "[Hrcâ— Hrctok2]".
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
- split; simpl; last done. apply frac_valid'. rewrite /= -H comm_L.
+ split; simpl; last done. apply frac_valid. rewrite /= -H comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
rewrite right_id -Some_op -Cinl_op -pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc◠Hl'1 Hl'2 Hl'†Hνtok2 Hν†$Hna]") as "Hna".
{ iExists _. iFrame "Hrcâ—". iExists _. rewrite Z.add_comm. iFrame.
- rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
iApply (type_type _ _ _ [ x ◠box (&shr{α}(rc ty)); #lr ◠box (rc ty)]
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 987eb1b9..91b5c4e0 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -167,13 +167,13 @@ Section code.
iMod (own_update with "Hrcâ—") as "[Hrcâ— Hrctok2]".
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
- split; simpl; last done. apply frac_valid'.
+ split; simpl; last done. apply frac_valid.
rewrite /= -Hq''q0 comm_L. by apply Qp_add_le_mono_l, Qp_div_le. }
rewrite right_id -Some_op -Cinl_op -pair_op.
iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc◠Hl'1 Hl'2 Hl'†Hν2 Hν†$Hna]") as "Hna".
{ iExists _. iFrame "Hrcâ—". iExists _. rewrite Z.add_comm. iFrame.
- rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
iApply (type_type _ _ _ [ w ◠box (&shr{α}(weak ty)); #lr ◠box (uninit 2);
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index bf9ac8b1..27baff9c 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -73,7 +73,7 @@ Section ref_functions.
(op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite /= -Hq'q'' comm_L.
+ - 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)".
iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I with "[H↦1 H↦2]" as "H↦".
@@ -335,7 +335,7 @@ Section ref_functions.
(op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite /= -Hq1q2 comm_L.
+ - apply frac_valid. rewrite /= -Hq1q2 comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 6bda8af9..881ba5c6 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -184,7 +184,7 @@ Section refcell_functions.
(op_local_update_discrete _ _ (reading_stR (q'/2)%Qp ν)) => ?.
split; [split|].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite /= -Hqq' comm_L.
+ - apply frac_valid. rewrite /= -Hqq' comm_L.
by apply Qp_add_le_mono_l, Qp_div_le.
- done. }
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 25ade67a..2a32ac07 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -309,7 +309,7 @@ Section refmut_functions.
(op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite /= -Hqq1 comm_L.
+ - apply frac_valid. rewrite /= -Hqq1 comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2e1340a2..175cf68c 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -193,7 +193,7 @@ Section rwlock_functions.
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
split; [split|].
- by rewrite /= Hag agree_idemp.
- - apply frac_valid'. rewrite /= -Hqq' comm_L.
+ - apply frac_valid. rewrite /= -Hqq' comm_L.
by apply Qp_add_le_mono_l, Qp_div_le.
- done. }
iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
--
GitLab