Skip to content
Snippets Groups Projects
Commit 3ec09815 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'no-dec-agree' into 'master' 

lifetime logic: use agree instead of dec_agree

If you are happy with this, we can merge this and <https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/22>

Cc @robbertkrebbers @jjourdan

See merge request !4
parents 741c78cf 84913cf3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 72 additions and 61 deletions
theories/lifetime/accessors.v
+ 9
− 9
View file @ 3ec09815
From lrust.lifetime Require Export primitive.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
......@@ -14,7 +14,7 @@ Lemma bor_open_internal E P i Pb q :
slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
idx_bor_own 1%Qp i -∗ (q).[i.1] ={E}=∗
▷ lft_bor_alive (i.1) Pb ∗
own_bor (i.1) (◯ {[i.2 := (1%Qp, DecAgree (Bor_open q))]}) ∗ ▷ P.
own_bor (i.1) (◯ {[i.2 := (1%Qp, to_agree (Bor_open q))]}) ∗ ▷ P.
Proof.
iIntros (?) "Hslice Halive Hbor Htok". unfold lft_bor_alive, idx_bor_own.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
......@@ -25,7 +25,7 @@ Proof.
rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
{ eapply singleton_local_update. by rewrite lookup_fmap EQB.
by apply (exclusive_local_update _ (1%Qp, DecAgree (Bor_open q))). }
by apply (exclusive_local_update _ (1%Qp, to_agree (Bor_open q))). }
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
iExists _. iFrame "∗".
rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
......@@ -35,7 +35,7 @@ Qed.
Lemma bor_close_internal E P i Pb q :
↑borN ⊆ E →
slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
own_bor (i.1) (◯ {[i.2 := (1%Qp, DecAgree (Bor_open q))]}) -∗ ▷ P ={E}=∗
own_bor (i.1) (◯ {[i.2 := (1%Qp, to_agree (Bor_open q))]}) -∗ ▷ P ={E}=∗
▷ lft_bor_alive (i.1) Pb ∗ idx_bor_own 1%Qp i ∗ (q).[i.1].
Proof.
iIntros (?) "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
......@@ -47,7 +47,7 @@ Proof.
rewrite -(fmap_insert bor_filled _ _ Bor_in).
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
{ eapply singleton_local_update. by rewrite lookup_fmap EQB.
by apply (exclusive_local_update _ (1%Qp, DecAgree Bor_in)). }
by apply (exclusive_local_update _ (1%Qp, to_agree Bor_in)). }
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[>$ HB]".
iExists _. iFrame "Hbox Hown".
......@@ -103,7 +103,7 @@ Proof.
iDestruct (own_bor_valid_2 with "Hinv Hf")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
[[_<-]%lookup_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
iDestruct (lft_tok_dead with "Htok H†") as "[]".
Qed.
......@@ -181,7 +181,7 @@ Proof.
{ apply auth_update. etrans.
- apply delete_singleton_local_update, _.
- apply (alloc_singleton_local_update _ j
(1%Qp, DecAgree (Bor_open q'))); last done.
(1%Qp, to_agree (Bor_open q'))); last done.
rewrite -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
rewrite own_bor_op. iDestruct "Hown" as "[Hown Hbor]".
......@@ -200,7 +200,7 @@ Proof.
iDestruct (own_bor_valid_2 with "Hinv Hbor")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
[[_<-]%lookup_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
iDestruct (lft_tok_dead with "Htok H†") as "[]".
Qed.
......@@ -234,7 +234,7 @@ Proof.
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
- apply delete_singleton_local_update, _.
- apply (alloc_singleton_local_update _ j (1%Qp, DecAgree (Bor_in))); last done.
- apply (alloc_singleton_local_update _ j (1%Qp, to_agree (Bor_in))); last done.
rewrite -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
......
theories/lifetime/borrow.v
+ 9
− 9
View file @ 3ec09815
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking raw_reborrow.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
......@@ -30,8 +30,8 @@ Proof.
rewrite -(fmap_insert bor_filled _ _ Bor_in).
iMod (own_bor_update with "HownB") as "[HB● HB◯]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ γB (1%Qp, DecAgree Bor_in)); last done.
rewrite lookup_fmap. by destruct (B !! γB). }
(alloc_singleton_local_update _ γB (1%Qp, to_agree Bor_in)); last done.
rewrite lookup_fmap. case:(B !! γB) HBlookup; done. }
rewrite -fmap_insert.
iSpecialize ("Hclose'" with "[Hvs Hinh HboxB HB● HB]").
{ iNext. rewrite /lft_inv. iLeft. iFrame "%".
......@@ -89,12 +89,12 @@ Proof.
{ etrans; last etrans.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
(alloc_singleton_local_update _ γ1 (1%Qp, DecAgree Bor_in)); last done.
(alloc_singleton_local_update _ γ1 (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //.
- apply cmra_update_op; last done.
apply auth_update_alloc,
(alloc_singleton_local_update _ γ2 (1%Qp, DecAgree Bor_in)); last done.
(alloc_singleton_local_update _ γ2 (1%Qp, to_agree Bor_in)); last done.
rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
......@@ -158,7 +158,7 @@ Proof.
apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
(alloc_singleton_local_update _ γ (1%Qp, DecAgree Bor_in)); last done.
(alloc_singleton_local_update _ γ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap !fmap_delete //. }
rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
......@@ -170,9 +170,9 @@ Proof.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
rewrite !big_sepM_insert /=.
+ rewrite (big_sepM_delete _ _ _ _ EQB1) /=.
rewrite (big_sepM_delete _ _ j2 Bor_in) /=. by iDestruct "HB" as "[_ $]".
rewrite lookup_delete_ne //.
+ rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=.
by iDestruct "HB" as "[_ $]". rewrite lookup_delete_ne //.
+ rewrite -fmap_None -lookup_fmap !fmap_delete //.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
......
theories/lifetime/creation.v
+ 3
− 3
View file @ 3ec09815
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Import faking.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
......@@ -42,7 +42,7 @@ Proof.
iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
rewrite (map_fmap_ext _ ((1%Qp,) ∘ DecAgree) B); last naive_solver.
rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
iSpecialize ("Halive'" with "Halive").
......@@ -198,7 +198,7 @@ Proof.
apply lft_alive_in_insert_false; last done.
assert (κ ∉ K). intros ?. eapply H5. 2: eauto. rewrite elem_of_union. eauto.
move: H7. rewrite elem_of_kill_set not_and_l. intros [?|?]. done.
contradict H7. apply elem_of_dom. set_solver +HI Hκ.
contradict H7. apply elem_of_dom. set_solver +HI Hκ.
+ iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
Qed.
End creation.
theories/lifetime/definitions.v
+ 24
− 15
View file @ 3ec09815
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.prelude Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes.
......@@ -20,6 +20,7 @@ Inductive bor_state :=
| Bor_rebor (κ : lft).
Instance bor_state_eq_dec : EqDecision bor_state.
Proof. solve_decision. Defined.
Canonical bor_stateC := leibnizC bor_state.
Definition bor_filled (s : bor_state) : bool :=
match s with Bor_in => true | _ => false end.
......@@ -35,15 +36,16 @@ Record lft_names := LftNames {
}.
Instance lft_names_eq_dec : EqDecision lft_names.
Proof. solve_decision. Defined.
Canonical lft_namesC := leibnizC lft_names.
Definition alftUR := gmapUR atomic_lft lft_stateR.
Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
Definition ilftUR := gmapUR lft (dec_agreeR lft_names).
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap DecAgree.
Definition ilftUR := gmapUR lft (agreeR lft_namesC).
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
Definition borUR := gmapUR slice_name (prodR fracR (dec_agreeR bor_state)).
Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ DecAgree).
Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
Definition inhUR := gset_disjUR slice_name.
......@@ -53,9 +55,9 @@ Class lftG Σ := LftG {
alft_name : gname;
ilft_inG :> inG Σ (authR ilftUR);
ilft_name : gname;
lft_bor_box :> inG Σ (authR borUR);
lft_bor_inG :> inG Σ (authR borUR);
lft_cnt_inG :> inG Σ (authR natUR);
lft_inh_box :> inG Σ (authR inhUR);
lft_inh_inG :> inG Σ (authR inhUR);
}.
Section defs.
......@@ -73,19 +75,19 @@ Section defs.
own ilft_name (● to_ilftUR I).
Definition own_bor (κ : lft)
(x : auth (gmap slice_name (frac * dec_agree bor_state))) : iProp Σ :=
(x : authR borUR) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own ilft_name (◯ {[ κ := to_agree γs ]}) ∗
own (bor_name γs) x)%I.
Definition own_cnt (κ : lft) (x : auth nat) : iProp Σ :=
Definition own_cnt (κ : lft) (x : authR natUR) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own ilft_name (◯ {[ κ := to_agree γs ]}) ∗
own (cnt_name γs) x)%I.
Definition own_inh (κ : lft) (x : auth (gset_disj slice_name)) : iProp Σ :=
Definition own_inh (κ : lft) (x : authR inhUR) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own ilft_name (◯ {[ κ := to_agree γs ]}) ∗
own (inh_name γs) x)%I.
Definition bor_cnt (κ : lft) (s : bor_state) : iProp Σ :=
......@@ -103,7 +105,7 @@ Section defs.
Definition lft_bor_dead (κ : lft) : iProp Σ :=
(∃ (B: gset slice_name) (Pb : iProp Σ),
own_bor κ (● to_gmap (1%Qp, DecAgree Bor_in) B) ∗
own_bor κ (● to_gmap (1%Qp, to_agree Bor_in) B) ∗
box borN (to_gmap false B) Pb)%I.
Definition lft_inh (κ : lft) (s : bool) (Pi : iProp Σ) : iProp Σ :=
......@@ -171,7 +173,7 @@ Section defs.
Definition bor_idx := (lft * slice_name)%type.
Definition idx_bor_own (q : frac) (i : bor_idx) : iProp Σ :=
own_bor (i.1) (◯ {[ i.2 := (q,DecAgree Bor_in) ]}).
own_bor (i.1) (◯ {[ i.2 := (q, to_agree Bor_in) ]}).
Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
(lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
Definition raw_bor (κ : lft) (P : iProp Σ) : iProp Σ :=
......@@ -254,6 +256,13 @@ Lemma lft_vs_unfold κ Pb Pi :
lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
Proof. done. Qed.
Global Instance own_bor_proper κ : Proper ((≡) ==> (≡)) (own_bor κ).
Proof. solve_proper. Qed.
Global Instance own_cnt_proper κ : Proper ((≡) ==> (≡)) (own_cnt κ).
Proof. solve_proper. Qed.
Global Instance own_inh_proper κ : Proper ((≡) ==> (≡)) (own_inh κ).
Proof. solve_proper. Qed.
Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
Proof. solve_proper. Qed.
Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
......
theories/lifetime/faking.v
+ 4
− 4
View file @ 3ec09815
From lrust.lifetime Require Export primitive.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
......@@ -18,14 +18,14 @@ Proof.
{ iModIntro. iExists A, I. by iFrame. }
iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
(frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
(frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
first by apply auth_valid_discrete_2.
iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
as (γinh) "Hinh"; first by done.
set (γs := LftNames γbor γcnt γinh).
iMod (own_update with "HI") as "[HI Hγs]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ κ (DecAgree γs)); last done.
(alloc_singleton_local_update _ κ (to_agree γs)); last done.
by rewrite lookup_fmap HIκ. }
iDestruct "Hγs" as "#Hγs".
iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
......@@ -85,7 +85,7 @@ Proof.
iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
iMod (own_bor_update with "HB●") as "[HB● H◯]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
(alloc_singleton_local_update _ _ (1%Qp, to_agree Bor_in)); last done.
by do 2 eapply lookup_to_gmap_None. }
rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "H◯".
- iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
......
theories/lifetime/primitive.v
+ 14
− 13
View file @ 3ec09815
From lrust.lifetime Require Export definitions.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes fractional.
From iris.proofmode Require Import tactics.
......@@ -10,21 +10,22 @@ Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
{[i := (q%Qp, DecAgree s)]} ≼ to_borUR B → B !! i = Some s.
{[i := (q%Qp, to_agree s)]} ≼ to_borUR B → B !! i = Some s.
Proof.
rewrite singleton_included=> -[qs [/leibniz_equiv_iff]].
rewrite lookup_fmap fmap_Some=> -[s' [? ->]].
by move=> /Some_pair_included [_] /Some_included_total /DecAgree_included=>->.
rewrite singleton_included=> -[qs []]. unfold_leibniz.
rewrite lookup_fmap fmap_Some_equiv=> -[s' [-> ->]].
by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
Qed.
(** Ownership *)
Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
own_ilft_auth I -∗
own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
as %[[? [??]]%singleton_included _]%auth_valid_discrete_2.
unfold to_ilftUR in *. simplify_map_eq; simplify_option_eq; eauto.
as %[[? [Hl ?]]%singleton_included _]%auth_valid_discrete_2.
unfold to_ilftUR in *. simplify_map_eq.
destruct (fmap_Some_equiv' _ _ _ Hl) as (?&?&?). eauto.
Qed.
Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
......@@ -50,13 +51,13 @@ Proof.
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Global Instance own_bor_into_op κ x x1 x2 :
IntoOp x x1 x2 → IntoAnd false (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
Proof.
rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_bor_op.
rewrite /IntoOp /IntoAnd=>->. by rewrite -own_bor_op.
Qed.
Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
......@@ -84,7 +85,7 @@ Proof.
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Global Instance own_cnt_into_op κ x x1 x2 :
......@@ -118,7 +119,7 @@ Proof.
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Global Instance own_inh_into_op κ x x1 x2 :
......@@ -281,7 +282,7 @@ Proof. done. Qed.
Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
Proof.
intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
by rewrite -auth_frag_op op_singleton.
rewrite -auth_frag_op op_singleton pair_op agree_idemp. done.
Qed.
Global Instance idx_bor_own_as_fractional i q :
AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
......
theories/lifetime/raw_reborrow.v
+ 6
− 5
View file @ 3ec09815
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Import faking.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
......@@ -39,8 +39,9 @@ Proof.
iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
{ by rewrite lookup_fmap HB. }
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
{ eapply auth_update. (* FIXME: eapply singleton_local_update loops. *)
apply: singleton_local_update; last eapply
(exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
{ iNext. rewrite /lft_inv. iLeft.
......@@ -58,7 +59,7 @@ Proof.
iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
iMod (own_bor_update with "HB●") as "[HB● Hj]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
(alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HBj. }
iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI". iFrame.
iSplitL "Hj".
......@@ -80,7 +81,7 @@ Proof.
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
(exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iMod (slice_fill _ _ false with "Hislice HP Hbox")
as "Hbox"; first by solve_ndisj.
......
theories/lifetime/reborrow.v
+ 2
− 2
View file @ 3ec09815
From lrust.lifetime Require Export borrow derived.
From lrust.lifetime Require Import raw_reborrow accessors.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
......@@ -75,7 +75,7 @@ Proof.
- rewrite big_sepM_delete; last done. iDestruct "HB" as "[_ $]". }
iMod (raw_bor_unnest' _ false with "[$HI $Hinv] HP Halive [Hvs]") as (Pb'') "([HI Hinv] & HP & Halive & Hvs)";
[solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
{ (* TODO: Use iRewrite supporting cotnractive rewriting. *)
{ (* TODO: Use iRewrite supporting contractive rewriting. *)
iApply (lft_vs_cons with "[]"); last done.
iIntros "[$ Hbor]". iModIntro. iNext. by iRewrite "EQ". }
iMod ("Hclose" with "[-HP]") as "_".
......
theories/typing/sum.v
+ 1
− 1
View file @ 3ec09815
......@@ -156,4 +156,4 @@ Section incl.
iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
Qed.
End incl.
\ No newline at end of file
End incl.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment