From 11c6989ee7ff812975d2190748ec4da577df90c6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 30 Nov 2016 02:24:32 +0100
Subject: [PATCH] Use new lemmas of Iris about updates that take a step.
---
opam.pins | 2 +-
theories/lifetime/shr_borrow.v | 2 +-
theories/typing/perm_incl.v | 2 +-
theories/typing/type.v | 36 +++++++++----------
theories/typing/type_incl.v | 9 ++---
theories/typing/typing.v | 64 +++++++++++++++-------------------
6 files changed, 51 insertions(+), 64 deletions(-)
diff --git a/opam.pins b/opam.pins
index febb0c13..1aed0164 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#90f773c0eb319320932edfd4a5fbe878673bb3de
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#f49a7f18c4afc34b9d2766f2b18e45e1a3cd38e7
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 5584c2d5..4f5042ef 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import gmap auth frac.
From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export borrow derived.
+From lrust.lifetime Require Export derived.
(** Shared bors *)
Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 162bfe6d..d83416a3 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -1,7 +1,7 @@
From Coq Require Import Qcanon.
From iris.base_logic Require Import big_op.
From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow reborrow.
+From lrust.lifetime Require Import borrow frac_borrow reborrow.
Import Perm Types.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9b64209d..e9b99373 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Export thread_local.
From iris.program_logic Require Import hoare.
From lrust.lang Require Export heap notation.
-From lrust.lifetime Require Import frac_borrow reborrow.
+From lrust.lifetime Require Import borrow frac_borrow reborrow.
Class iris_typeG Σ := Iris_typeG {
type_heapG :> heapG Σ;
@@ -180,9 +180,8 @@ Section types.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hb". set_solver.
+ - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "[Hb Htok]". set_solver.
{ rewrite bor_unfold_idx. iExists i. eauto. }
- iIntros "!>". iNext. iMod "Hb" as "[Hb Htok]".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done.
iApply "Hclose". eauto.
- iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
@@ -194,10 +193,8 @@ Section types.
iIntros (q') "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
- iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
- iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
- iMod ("Hclose" with "Htok"). iFrame.
- iApply (ty.(ty_shr_mono) with "LFT Hκ"); last done. done.
+ iMod ("Hvs" $! q'' with "Htok") as "[Hshr Htok]".
+ iMod ("Hclose" with "Htok") as "$". by iApply (ty.(ty_shr_mono) with "LFT Hκ").
Qed.
Next Obligation. done. Qed.
@@ -234,12 +231,10 @@ Section types.
- iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ rewrite (bor_unfold_idx κ'). eauto. }
iMod (bor_unnest with "LFT Hb") as "Hb". set_solver.
- iIntros "!>". iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
- - iMod (step_fupd_mask_mono _ _ _ _ True%I with "[]") as "Hclose'"; last first.
- iIntros "!>". iNext. iMod "Hclose'" as "_".
- iMod ("Hclose" with "[]") as "_"; by eauto. eauto. done. set_solver.
+ - iMod ("Hclose" with "[]") as "_". by eauto.
+ iApply step_fupd_mask_mono; last by eauto. done. set_solver.
Qed.
Next Obligation.
intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
@@ -251,9 +246,8 @@ Section types.
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros (q) "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
- iMod ("Hvs" $! q' with "Htok") as "Hclose'". iIntros "!>". iNext.
- iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply (ty_shr_mono with "LFT Hκ0"); last done. done.
+ iMod ("Hvs" $! q' with "Htok") as "[#Hshr Htok]".
+ iMod ("Hclose" with "Htok") as "$". by iApply (ty_shr_mono with "LFT Hκ0").
Qed.
Next Obligation. done. Qed.
@@ -319,8 +313,10 @@ Section types.
repeat setoid_rewrite tl_own_union; first last.
set_solver. set_solver. set_solver. set_solver.
iDestruct "Htl" as "[[Htl1 Htl2] $]".
- iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". done. set_solver.
- iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. set_solver.
+ iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]".
+ done. set_solver.
+ iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]".
+ done. set_solver.
destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
rewrite !split_prod_mt.
@@ -352,8 +348,8 @@ Section types.
⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
Proof.
iSplit; iIntros "H".
- - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]". subst.
- iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
+ - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]".
+ subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
iExists vl'. by iFrame.
- iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
@@ -390,8 +386,8 @@ Section types.
rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
Qed.
Next Obligation.
- iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
- simpl. by iDestruct (sum_size_eq with "Hown") as %->.
+ iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)".
+ subst. simpl. by iDestruct (sum_size_eq with "Hown") as %->.
Qed.
Next Obligation.
intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index 060c52bc..163cf82d 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -1,7 +1,7 @@
From iris.base_logic Require Import big_op.
From iris.program_logic Require Import hoare.
From lrust.typing Require Export type perm_incl.
-From lrust.lifetime Require Import frac_borrow.
+From lrust.lifetime Require Import frac_borrow borrow.
Import Types.
@@ -63,9 +63,7 @@ Section ty_incl.
iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
iExists _. by iFrame.
- iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
- iIntros (q') "!#Hκ".
- iMod ("Hvs" $! _ with "Hκ") as "Hvs'". iIntros "!>". iNext.
- iMod "Hvs'" as "[Hshr $]". iModIntro.
+ iIntros (q') "!#Hκ". iMod ("Hvs" $! _ with "Hκ") as "[Hshr $]".
by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
Qed.
@@ -83,8 +81,7 @@ Section ty_incl.
iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
iFrame. iIntros (q') "!#Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
- iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext.
- iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+ iMod ("Hupd" with "*Htok") as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty_shr_mono with "LFT Hincl' H").
Qed.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 4cf5f3a0..f83e2b66 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
From lrust.lang Require Export notation memcpy.
From lrust.typing Require Export type perm.
From lrust Require Import typing.perm_incl lang.proofmode.
-From lrust.lifetime Require Import frac_borrow reborrow.
+From lrust.lifetime Require Import frac_borrow reborrow borrow.
Import Types Perm.
@@ -142,11 +142,10 @@ Section typing.
Lemma typed_endlft κ Ï:
typed_step (κ ∋ Ï âˆ— 1.[κ] ∗ †κ) Endlft (λ _, Ï)%P.
Proof.
- iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
- iApply wp_fupd. iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
- iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done.
- iDestruct ("Hend" with "Htok") as "$". by wp_seq.
- iIntros (v) "[#Hκ _]". by iApply fupd_mask_mono; last iApply "Hextr".
+ rewrite /killable /extract. iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
+ iDestruct ("Hend" with "Htok") as "Hend".
+ iApply (wp_fupd_step with "Hend"); try done. wp_seq.
+ iIntros "!>H†". by iApply fupd_mask_mono; last iApply "Hextr".
Qed.
Lemma typed_alloc Ï (n : nat):
@@ -296,16 +295,15 @@ Section typing.
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
- iSpecialize ("Hown" $! _ with "Htok2").
- iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
- - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q'''} v ∗ ⌜v = #vlâŒ)%I); try done.
- iSplitL "Hown"; last by wp_read; eauto.
- iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
- last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
- - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
- iMod ("Hclose'" with "[$H↦]") as "Htok'".
- iMod ("Hclose" with "[$Htok $Htok']") as "$".
- iFrame "#". iExists _. eauto.
+ iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok2]"); try done.
+ - rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
+ { by rewrite (comm (R:=eq)) -union_difference_L. }
+ iApply step_fupd_mask_frame_r; try set_solver.
+ iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok2").
+ set_solver. repeat apply union_least; solve_ndisj.
+ - wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
+ iSplitL "Hshr"; first by iExists _; auto.
+ iMod ("Hclose'" with "[$H↦]") as "?". iApply "Hclose". iFrame.
Qed.
Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
@@ -324,15 +322,12 @@ Section typing.
iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton.
- iApply (wp_strong_mono ⊤ ⊤ _ (λ v, _ ∗ ⌜v = #l'⌠∗ l ↦#l')%I). done.
- iSplitR "Hbor H↦"; last first.
- - iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done; last first.
- iSplitL "Hbor". by iApply (bor_unnest with "LFT Hbor"). wp_read. auto.
- - iIntros (v) "(Hbor & % & H↦)". subst.
- iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
- iMod ("Hclose" with "Htok") as "$". iFrame "#".
- iExists _. iSplitR. done. iApply (bor_shorten with "[] Hbor").
+ iApply (wp_fupd_step _ (⊤∖↑lftN) with "[Hbor]"); try done.
+ by iApply (bor_unnest with "LFT Hbor").
+ wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
+ - iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
+ - iMod ("Hclose'" with "[$H↦]") as "[_ ?]". by iApply "Hclose".
Qed.
Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
@@ -349,17 +344,16 @@ Section typing.
iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
{ iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
- iSpecialize ("Hown" $! _ with "Htok").
- iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
- - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q''} v ∗ ⌜v = #l'âŒ)%I); try done.
- iSplitL "Hown"; last by wp_read; eauto.
- iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
- last iApply "Hown"; (set_solver || rewrite ?disjoint_union_l; solve_ndisj).
- - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
- iMod ("Hclose''" with "Htok") as "Htok".
- iMod ("Hclose'" with "[$H↦]") as "Htok'".
- iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _.
- iSplitL. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+ iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok]"); try done.
+ - rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
+ { by rewrite (comm (R:=eq)) -union_difference_L. }
+ iApply step_fupd_mask_frame_r; try set_solver.
+ iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok").
+ set_solver. repeat apply union_least; solve_ndisj.
+ - wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
+ + iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+ + iMod ("Hclose''" with "Htok"). iMod ("Hclose'" with "[$H↦]").
+ iApply "Hclose". iFrame.
Qed.
Definition update (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
--
GitLab