From 80ce5d255abea16884988dd0ffa6e7974252ba59 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Mar 2017 17:39:27 +0100
Subject: [PATCH] Rc::clone
Also tune the simpl behavior of ty_own a little to be less eager with unfolding
---
opam.pins | 2 +-
theories/typing/function.v | 2 +-
theories/typing/lib/cell.v | 2 +-
theories/typing/lib/rc.v | 88 +++++++++++++++++++---
theories/typing/lib/refcell/ref_code.v | 2 +-
theories/typing/lib/refcell/refcell_code.v | 4 +-
theories/typing/lib/refcell/refmut_code.v | 2 +-
theories/typing/lib/rwlock/rwlock_code.v | 4 +-
theories/typing/product_split.v | 2 +-
theories/typing/sum.v | 4 +-
theories/typing/type.v | 4 +-
theories/typing/type_sum.v | 4 +-
12 files changed, 94 insertions(+), 26 deletions(-)
diff --git a/opam.pins b/opam.pins
index e9084293..0af3bc66 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 21fbbdde77c9e8b5d9cf2ad908c0921528ca02f2
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5874f41e10c229d0b7df07a1e4e58f5e61a1af0a
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 2182ff1a..8750b714 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -55,7 +55,7 @@ Section fn.
type_dist2 n') fn.
Proof.
intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
- constructor; simpl.
+ constructor; unfold ty_own; simpl.
(* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
(* The clean way to do this would be to have a metric on type contexts. Oh well. *)
intros tid vl. unfold typed_body.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 6a729cc5..f67534e7 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -49,7 +49,7 @@ Section cell.
Global Instance cell_copy :
Copy ty → Copy (cell ty).
Proof.
- intros ty Hcopy. split; first by intros; simpl; apply _.
+ intros ty Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
(* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index f6b8962f..b0cb325a 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -1,3 +1,4 @@
+From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op.
@@ -45,10 +46,10 @@ Section rc.
ty_shr κ tid l :=
∃ (l' : loc), &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
- ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q',
+ ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
na_inv tid rc_invN (rc_inv tid ν γ l' ty) ∗
- &na{κ, tid, rc_invN}(own γ (◯ Some (q', 1%positive))) ∗
- ty.(ty_shr) κ tid (shift_loc l' 1)
+ &na{κ, tid, rc_shrN}(own γ (◯ Some (q', 1%positive))) ∗
+ ty.(ty_shr) ν tid (shift_loc l' 1)
|}%I.
Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
@@ -60,10 +61,10 @@ Section rc.
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
- set (C := (∃ _ _ _, _ ∗ &na{_,_,_} _ ∗ _)%I).
+ set (C := (∃ _ _ _, _ ∗ _ ∗ &na{_,_,_} _ ∗ _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
with "[Hpbown]") as "#Hinv"; first by iLeft.
- iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
+ iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose1]"; first set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
@@ -98,10 +99,10 @@ Section rc.
iDestruct (frac_bor_lft_incl with "LFT >[Hlft]") as "#Hlft".
{ iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
iMod (bor_na with "Hrc") as "$"; first solve_ndisj.
- iApply ty_shr_mono; done. }
- iMod ("Hclose" with "[]") as "_"; first by auto.
+ by iFrame "#". }
+ iMod ("Hclose1" with "[]") as "_"; first by auto.
by iFrame "#∗".
- - iMod ("Hclose" with "[]") as "_"; first by auto.
+ - iMod ("Hclose1" with "[]") as "_"; first by auto.
iApply step_fupd_intro; first solve_ndisj. iNext. by iFrame.
Qed.
Next Obligation.
@@ -111,10 +112,10 @@ Section rc.
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
- iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (???) "(? & ? & ?)".
+ iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν ?) "(? & ? & ?& ?)".
iExists _, _, _. iModIntro. iFrame. iSplit.
+ - by iApply lft_incl_trans.
- by iApply na_bor_shorten.
- - by iApply ty_shr_mono.
Qed.
End rc.
@@ -137,7 +138,7 @@ Section code.
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]; iIntros (rcbox); simpl_subst.
iApply type_new; [solve_typing..|]; iIntros (rc); simpl_subst.
- iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT".
rewrite (Nat2Z.id (S ty.(ty_size))) 2!tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hrc [Hrcbox Hx]]". destruct x as [[|lx|]|]; try done.
@@ -164,4 +165,69 @@ Section code.
iApply type_delete; [solve_typing..|].
iApply (type_jump [ #_]); solve_typing.
Qed.
+
+ Definition rc_clone : val :=
+ funrec: <> ["rc"] :=
+ let: "rc2" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "count" := !("rc''" +ₗ #0) in
+ "rc''" +ₗ #0 <- "count" +#1;;
+ "rc2" <- "rc''";;
+ delete [ #1; "rc" ];; return: ["rc2"].
+
+ Lemma rc_clone_type ty :
+ typed_val rc_clone (fn(∀ α, [α]; &shr{α} rc ty) → rc ty).
+ Proof.
+ intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_new; [solve_typing..|]; iIntros (rc2); simpl_subst.
+ rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk".
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iIntros "[Hx [Hrc' Hrc2]]". rewrite [[x]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ destruct rc2 as [[|lrc2|]|]; try done. iDestruct "Hrc2" as "[Hrc2 Hrc2†]".
+ iDestruct "Hrc2" as (vl) "Hrc2". rewrite uninit_own.
+ iDestruct "Hrc2" as "[>Hrc2↦ >SZ]". destruct vl as [|]; iDestruct "SZ" as %[=].
+ destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
+ (* All right, we are done preparing our context. Let's get going. *)
+ rewrite {1}/elctx_interp big_sepL_singleton.
+ iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_fupd_step with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "(#Hincl & #Hinv & #Hrctokb & #Hshr)". iModIntro.
+ wp_let. wp_op. rewrite shift_loc_0.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose1)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose2)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as (st) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[Hval|[_ [[qa c] [_ [-> _]]]]]%option_included _]%auth_valid_discrete_2; first done. (* Oh my, what a pattern... *)
+ iDestruct "Hrcst" as (qb) "(>Hl' & >Hl'† & >% & Hνtok & Hν†)".
+ wp_read. wp_let. wp_op. rewrite shift_loc_0. wp_op. wp_write. wp_write.
+ (* And closing it again. *)
+ iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
+ { apply auth_update_alloc,
+ (op_local_update_discrete _ _ (Some ((qb/2)%Qp, 1%positive)))=>-[/= Hqa _].
+ split; simpl; last done. apply frac_valid'. rewrite -H comm_L -{2}(Qp_div_2 qb).
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
+ apply Qcplus_le_mono_r, Qp_ge_0. }
+ rewrite right_id -Some_op pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
+ iMod ("Hclose2" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose1" with "[Hrc● Hl' Hl'† Hνtok2 Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
+ iNext. iPureIntro. rewrite [_ ⋅ _]comm frac_op' -assoc Qp_div_2. done. }
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lrc2 ◁ box (rc ty)]%TC
+ with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame "Hx". iFrame "Hrc2†". iExists _. erewrite heap_mapsto_vec_singleton.
+ iFrame "Hrc2↦". iNext. iRight. iExists _, ν, _. iFrame "#∗". }
+ { rewrite /elctx_interp big_sepL_singleton. iFrame. }
+ iApply type_delete; [solve_typing..|].
+ iApply (type_jump [ #_ ]); solve_typing.
+ Qed.
End code.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index a7ee9b1f..952f950e 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -81,7 +81,7 @@ Section ref_functions.
(op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
split; [|split; last done].
- by rewrite /= agree_idemp.
- - change ((q''/2+q')%Qp ≤ 1%Qp)%Qc. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
+ - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
wp_apply wp_new; [done..|]. iIntros (lr ?) "(%&?&Hlr)".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index c5b433be..93bb78de 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -42,7 +42,7 @@ Section refcell_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
iSplitL "Hx↦".
- iExists _. rewrite uninit_own. auto.
- - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
+ - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply (type_jump [ #_]); solve_typing.
Qed.
@@ -186,7 +186,7 @@ Section refcell_functions.
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
split; [|split].
- by rewrite /= -Hag agree_idemp.
- - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+ - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0.
- done. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c5039c18..5602f7fb 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -210,7 +210,7 @@ Section refmut_functions.
iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
iExists [ #lv'; #lrc].
rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
- iExists ν. rewrite EQ1. eauto 10 with iFrame. }
+ iExists ν. rewrite /= EQ1. eauto 20 with iFrame. }
{ rewrite /elctx_interp !big_sepL_cons /= -lft_tok_sep. iFrame. }
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 18b83f25..8a036dc7 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -42,7 +42,7 @@ Section rwlock_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
iSplitL "Hx↦".
- iExists _. rewrite uninit_own. auto.
- - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
+ - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply (type_jump [ #_]); solve_typing.
Qed.
@@ -193,7 +193,7 @@ Section rwlock_functions.
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
split; [split|].
- by rewrite /= Hag agree_idemp.
- - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+ - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0.
- done. }
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 2d56f54e..47a6b6fa 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -116,7 +116,7 @@ Section product_split.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
- auto 10 with iFrame.
+ rewrite {3}/ty_own /=. auto 10 with iFrame.
Qed.
Lemma tctx_split_own_prod E L n tyl p :
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index f36ed5ae..9f53f4c1 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -107,7 +107,7 @@ Section sum.
{ clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
constructor; simpl.
- by rewrite EQmax.
- - intros tid vl. destruct n as [|n]=> //=. rewrite EQmax.
+ - intros tid vl. destruct n as [|n]=> //=. rewrite /ty_own /= EQmax.
solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
- intros κ tid l. unfold is_pad. rewrite EQmax.
solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
@@ -125,7 +125,7 @@ Section sum.
{ clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
constructor; simpl.
- by rewrite EQmax.
- - intros tid vl. rewrite EQmax.
+ - intros tid vl. rewrite /ty_own /= EQmax.
solve_proper_core ltac:(fun _ => exact:EQnth || f_equiv).
- intros κ tid l. unfold is_pad. rewrite EQmax.
solve_proper_core ltac:(fun _ => exact:EQnth || (eapply ty_size_ne; try reflexivity) || f_equiv).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 94219da4..563a333e 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,6 +51,8 @@ Instance: Params (@ty_size) 2.
Instance: Params (@ty_own) 2.
Instance: Params (@ty_shr) 2.
+Arguments ty_own {_ _} !_ _ !_ /.
+
Record simple_type `{typeG Σ} :=
{ st_own : thread_id → list val → iProp Σ;
st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
@@ -316,7 +318,7 @@ Section type_contractive.
Proof.
intros ???. constructor.
- done.
- - intros. destruct n; first done; simpl. by f_equiv.
+ - intros. destruct n; first done; simpl. f_equiv. f_equiv. done.
- intros. solve_contractive.
Qed.
End type_contractive.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index da864583..2df653e8 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -41,7 +41,7 @@ Section case.
iFrame. iExists _. iFrame. rewrite uninit_own. auto.
- rewrite -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
- iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
+ iFrame. iExists i, vl', vl''. rewrite /= -EQlen app_length nth_lookup EQty /=. auto.
Qed.
Lemma type_case_own E L C T T' p n tyl el :
@@ -91,7 +91,7 @@ Section case.
- iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
[by iIntros "!>$"| |].
{ iExists (#i::vl'++vl'').
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
+ rewrite heap_mapsto_vec_cons heap_mapsto_vec_app /= -EQlen. iFrame. iNext.
iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
iMod ("Hclose" with "Htok") as "[HE HL]".
iApply (Hety with "LFT Hna HE HL HC").
--
GitLab