Commit 65ff62e6 authored by Robbert Krebbers's avatar Robbert Krebbers

ufrac is part of Iris now; make use of that.

parent f7c8b3a3
Pipeline #14383 failed with stage
in 9 minutes and 51 seconds
......@@ -14,11 +14,9 @@ Iron has been built and tested with the following dependencies
## Directory Structure
- In [theories/algebra](theories/algebra) two new cameras are defined.
1. Improper fractions as a camera without identity with addition as
the operation are defined in [theories/algebra/vfrac.v](theories/algebra/vfrac.v).
2. The fractional authoritative camera described in Section 6 with improper fractions is defined
in [theories/algebra/vfrac_auth.v](theories/algebra/vfrac_auth.v).
- In [theories/algebra/ufrac_auth.v](theories/algebra/ufrac_auth.v), the
fractional authoritative camera described in Section 6 with improper
fractions is defined.
- The semantics of the connectives of fractional predicates logic are given in
[theories/bi/fracpred.v](theories/bi/fracpred.v).
......
-Q theories iron
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/algebra/vfrac.v
theories/algebra/vfrac_auth.v
theories/algebra/ufrac_auth.v
theories/bi/fracpred.v
theories/proofmode/fracpred.v
theories/iron_logic/iron.v
......
(** This file provides a version of the fractional authoritative camera that
can be used with fractions [> 1]. This is useful in the state interpretation of
Iron (see the file [heap_lang/heap]), where we want to keep track of a surplus
of fragmental elements by forked-off threads.
(** This file provides the unbounded fractional authoritative camera: a version
of the fractional authoritative camera that can be used with fractions [> 1].
Much of the reasoning principles for this version of the fractional
Most of the reasoning principles for this version of the fractional
authoritative cameras are the same as for the original version. There are two
difference:
- We get the additional rule:
- We get the additional rule that can be used to allocate a "surplus", i.e.
if we have the authoritative element we can always increase its fraction
and allocate a new fragment.
<<<
(a b) ?{p} a ~~> ?{p + q} (a b) ?{q} b
>>>
That can be used to allocate a surplus.
- We no longer have the [?{1} a] is the exclusive fragmental element (cf.
[frac_auth_frag_validN_op_1_l] in Iris).
[frac_auth_frag_validN_op_1_l]).
*)
From iris.algebra Require Export auth frac.
From iron.algebra Require Import vfrac.
From iris.algebra Require Import ufrac.
From iris.algebra Require Export updates local_updates.
From iris.algebra Require Import proofmode_classes.
From Coq Require Import QArith Qcanon.
Definition vfrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR vfracR A)).
Definition vfrac_authUR (A : cmraT) : ucmraT :=
authUR (optionUR (prodR vfracR A)).
Definition ufrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR ufracR A)).
Definition ufrac_authUR (A : cmraT) : ucmraT :=
authUR (optionUR (prodR ufracR A)).
Definition vfrac_auth_auth {A : cmraT} (q : Qp) (x : A) : vfrac_authR A :=
Definition ufrac_auth_auth {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
(Some (q,x)).
Definition vfrac_auth_frag {A : cmraT} (q : Qp) (x : A) : vfrac_authR A :=
Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
(Some (q,x)).
Typeclasses Opaque vfrac_auth_auth vfrac_auth_frag.
Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
Instance: Params (@vfrac_auth_auth) 2 := {}.
Instance: Params (@vfrac_auth_frag) 2 := {}.
Instance: Params (@ufrac_auth_auth) 2.
Instance: Params (@ufrac_auth_frag) 2.
Notation "●?{ q } a" := (vfrac_auth_auth q a) (at level 10, format "●?{ q } a").
Notation "◯?{ q } a" := (vfrac_auth_frag q a) (at level 10, format "◯?{ q } a").
Notation "●?{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●?{ q } a").
Notation "◯?{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯?{ q } a").
Section vfrac_auth.
Section ufrac_auth.
Context {A : cmraT}.
Implicit Types a b : A.
Global Instance vfrac_auth_auth_ne q : NonExpansive (@vfrac_auth_auth A q).
Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_auth_proper q : Proper (() ==> ()) (@vfrac_auth_auth A q).
Global Instance ufrac_auth_auth_proper q : Proper (() ==> ()) (@ufrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_frag_ne q : NonExpansive (@vfrac_auth_frag A q).
Global Instance ufrac_auth_frag_ne q : NonExpansive (@ufrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_frag_proper q : Proper (() ==> ()) (@vfrac_auth_frag A q).
Global Instance ufrac_auth_frag_proper q : Proper (() ==> ()) (@ufrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_auth_discrete a : Discrete a Discrete (?{q} a).
Global Instance ufrac_auth_auth_discrete a : Discrete a Discrete (?{q} a).
Proof. intros; apply Auth_discrete; apply _. Qed.
Global Instance vfrac_auth_frag_discrete a : Discrete a Discrete (?{q} a).
Global Instance ufrac_auth_frag_discrete a : Discrete a Discrete (?{q} a).
Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
Lemma vfrac_auth_validN n a p : {n} a {n} (?{p} a ?{p} a).
Lemma ufrac_auth_validN n a p : {n} a {n} (?{p} a ?{p} a).
Proof. done. Qed.
Lemma vfrac_auth_valid p a : a (?{p} a ?{p} a).
Lemma ufrac_auth_valid p a : a (?{p} a ?{p} a).
Proof. done. Qed.
Lemma vfrac_auth_agreeN n p a b : {n} (?{p} a ?{p} b) a {n} b.
Lemma ufrac_auth_agreeN n p a b : {n} (?{p} a ?{p} b) a {n} b.
Proof.
rewrite auth_validN_eq /= => -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
move=> /discrete_iff /leibniz_equiv_iff; rewrite vfrac_op'=> [/Qp_eq/=].
move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed.
Lemma vfrac_auth_agree p a b : (?{p} a ?{p} b) a b.
Lemma ufrac_auth_agree p a b : (?{p} a ?{p} b) a b.
Proof.
intros. apply equiv_dist=> n. by eapply vfrac_auth_agreeN, cmra_valid_validN.
intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
Qed.
Lemma vfrac_auth_agreeL `{!LeibnizEquiv A} p a b : (?{p} a ?{p} b) a = b.
Proof. intros. by eapply leibniz_equiv, vfrac_auth_agree. Qed.
Lemma ufrac_auth_agreeL `{!LeibnizEquiv A} p a b : (?{p} a ?{p} b) a = b.
Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
Lemma vfrac_auth_includedN n p q a b : {n} (?{p} a ?{q} b) Some b {n} Some a.
Lemma ufrac_auth_includedN n p q a b : {n} (?{p} a ?{q} b) Some b {n} Some a.
Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma vfrac_auth_included `{CmraDiscrete A} q p a b :
Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
(?{p} a ?{q} b) Some b Some a.
Proof. rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _] //. Qed.
Lemma vfrac_auth_includedN_total `{CmraTotal A} n q p a b :
Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
{n} (?{p} a ?{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, vfrac_auth_includedN. Qed.
Lemma vfrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
Lemma ufrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
(?{p} a ?{q} b) b a.
Proof. intros. by eapply Some_included_total, vfrac_auth_included. Qed.
Proof. intros. by eapply Some_included_total, ufrac_auth_included. Qed.
Lemma vfrac_auth_auth_validN n q a : {n} (?{q} a) {n} a.
Lemma ufrac_auth_auth_validN n q a : {n} (?{q} a) {n} a.
Proof.
split; [by intros [_ [??]]|].
repeat split; simpl; by try apply: ucmra_unit_leastN.
Qed.
Lemma vfrac_auth_auth_valid q a : (?{q} a) a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite vfrac_auth_auth_validN. Qed.
Lemma ufrac_auth_auth_valid q a : (?{q} a) a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
Lemma vfrac_auth_frag_validN n q a : {n} (?{q} a) {n} a.
Lemma ufrac_auth_frag_validN n q a : {n} (?{q} a) {n} a.
Proof. split. by intros [??]. by split. Qed.
Lemma vfrac_auth_frag_valid q a : (?{q} a) a.
Lemma ufrac_auth_frag_valid q a : (?{q} a) a.
Proof. split. by intros [??]. by split. Qed.
Lemma vfrac_auth_frag_op q1 q2 a1 a2 : ?{q1+q2} (a1 a2) ?{q1} a1 ?{q2} a2.
Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ?{q1+q2} (a1 a2) ?{q1} a1 ?{q2} a2.
Proof. done. Qed.
Global Instance is_op_vfrac_auth q q1 q2 a a1 a2 :
Global Instance is_op_ufrac_auth q q1 q2 a a1 a2 :
IsOp q q1 q2 IsOp a a1 a2 IsOp' (?{q} a) (?{q1} a1) (?{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_vfrac_auth_core_id q q1 q2 a :
Global Instance is_op_ufrac_auth_core_id q q1 q2 a :
CoreId a IsOp q q1 q2 IsOp' (?{q} a) (?{q1} a) (?{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
by rewrite -vfrac_auth_frag_op -core_id_dup.
by rewrite -ufrac_auth_frag_op -core_id_dup.
Qed.
Lemma vfrac_auth_update p q a b a' b' :
Lemma ufrac_auth_update p q a b a' b' :
(a,b) ~l~> (a',b') ?{p} a ?{q} b ~~> ?{p} a' ?{q} b'.
Proof.
intros. apply: auth_update.
apply: option_local_update. by apply: prod_local_update_2.
Qed.
Lemma vfrac_auth_update' p q a b :
Lemma ufrac_auth_update_surplus p q a b :
(a b) ?{p} a ~~> ?{p + q} (a b) ?{q} b.
Proof.
intros Hconsistent. apply: auth_update_alloc.
......@@ -135,4 +134,4 @@ Section vfrac_auth.
- rewrite -pair_op Some_op Heq comm.
destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
Qed.
End vfrac_auth.
End ufrac_auth.
(** This file provides a version of the fractional camera whose elements can be
between (not including) 0 and infinity. This differs from the standard
fractional camera in [algebra/frac] in the Iris repository, whose elements
be [ 1]. Fractions [> 1] are mainly useful in combination with the fractional
authoritative cameras, as in the file [vfrac_auth].
This file is much the same as the one in the Iris repository. The main
difference is that the validity predicate is changed (it is [True] instead of
[ 1]). To avoid ambiguity in the canonical structure search, we wrap the
type of fractions [vfrac] in a definition instead of a notation. *)
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Definition vfrac := Qp.
Section vfrac.
Canonical Structure vfracC := leibnizC vfrac.
Instance vfrac_valid : Valid vfrac := λ x, True.
Instance vfrac_pcore : PCore vfrac := λ _, None.
Instance vfrac_op : Op vfrac := λ x y, (x + y)%Qp.
Lemma vfrac_included (x y : vfrac) : x y (x < y)%Qc.
Proof. by rewrite Qp_lt_sum. Qed.
Corollary vfrac_included_weak (x y : vfrac) : x y (x y)%Qc.
Proof. intros ?%vfrac_included. auto using Qclt_le_weak. Qed.
Definition vfrac_ra_mixin : RAMixin vfrac.
Proof. split; try apply _; try done. Qed.
Canonical Structure vfracR := discreteR vfrac vfrac_ra_mixin.
Global Instance vfrac_cmra_discrete : CmraDiscrete vfracR.
Proof. apply discrete_cmra_discrete. Qed.
End vfrac.
Global Instance vfrac_cancelable (q : vfrac) : Cancelable q.
Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
Global Instance vfrac_id_free (q : vfrac) : IdFree q.
Proof.
intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
Qed.
Lemma vfrac_op' (q p : vfrac) : (p q) = (p + q)%Qp.
Proof. done. Qed.
Global Instance is_op_vfrac (q : vfrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp vfrac_op' Qp_div_2. Qed.
......@@ -4,23 +4,23 @@ in [iron_logic/adequacy].
Note, we only state adequacy for the lifted logic, because in the Coq
formalization we state all specifications in terms of the lifted logic. *)
From iris.algebra Require Import big_op gmap.
From iris.algebra Require Import big_op gmap ufrac.
From iron.iron_logic Require Export weakestpre adequacy.
From iron.algebra Require Import vfrac_auth vfrac.
From iron.algebra Require Import ufrac_auth.
From iron.heap_lang Require Import heap.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> ironInvPreG Σ;
heap_preG_inG :> inG Σ (vfrac_authR heapUR);
heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC vfracC))));
heap_preG_inG :> inG Σ (ufrac_authR heapUR);
heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC ufracC))));
}.
Definition heapΣ : gFunctors := #[
ironInvΣ;
GFunctor (vfrac_authR heapUR);
GFunctor (authR (gmapUR positive (exclR (optionC vfracC))))].
GFunctor (ufrac_authR heapUR);
GFunctor (authR (gmapUR positive (exclR (optionC ufracC))))].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
......@@ -35,8 +35,8 @@ Proof.
destruct (decide (σ = )) as [->|Heq].
- intros Hwp; eapply (iron_wp_adequacy _ _ _ _ _ _ (1 / 2) ε); iIntros (? κs) "".
iMod (own_alloc (?{1} (?{1/2} ?{1/2} ε))) as (γ) "[Hσ [Hp Hp']]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
by apply vfrac_auth_valid. }
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
by apply ufrac_auth_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
......@@ -53,8 +53,8 @@ Proof.
iIntros (? κs) "".
iMod (own_alloc (?{1} (to_heap σ)
(?{1/2} (to_heap σ) ?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
apply vfrac_auth_valid; by apply to_heap_valid. }
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
......@@ -101,8 +101,8 @@ Proof.
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iMod (own_alloc (?{1} (to_heap ) (?{1/2} (to_heap ) ?{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
apply vfrac_auth_valid; by apply to_heap_valid. }
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _.
iFrame "Hp"; iExists ([ map] l v σ2, l v)%I. iSplitL "Hσ Hf".
......@@ -126,8 +126,8 @@ Proof.
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iMod (own_alloc (?{1} (to_heap σ1) (?{1/2} (to_heap σ1) ?{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
apply vfrac_auth_valid; by apply to_heap_valid. }
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _.
iFrame "Hp"; iExists ([ map] l v σ2, l v)%I. iSplitL "Hσ Hf".
......
(** This file defines the basic points-to [] connectives for the Iron logic
instantiated with the heap_lang language. As a counter part to this, it defines
the state interpretation [heap_ctx]. *)
From iris.algebra Require Import frac_auth gmap agree gmultiset.
From iris.algebra Require Import frac_auth gmap agree gmultiset ufrac.
From iris.base_logic.lib Require Export own.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iron.proofmode Require Export fracpred.
From iron.heap_lang Require Export lang.
From iron.iron_logic Require Export weakestpre.
From iron.algebra Require Import vfrac vfrac_auth.
From iron.algebra Require Import ufrac_auth.
Set Default Proof Using "Type".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (agreeR valC)).
......@@ -18,12 +18,12 @@ Definition to_heap : gmap loc val → heapUR :=
(** The camera we need. *)
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_inG :> inG Σ (vfrac_authR heapUR);
heapG_inG :> inG Σ (ufrac_authR heapUR);
heapG_name : gname;
heapG_fcinv_cinvG : cinvG Σ;
heapG_fcinv_inG : inG Σ (frac_authR vfracR);
heapG_fcinv_inG : inG Σ (frac_authR ufracR);
heapG_fork_post_name : gname;
heapG_fork_postG :> inG Σ (authR (gmapUR positive (exclR (optionC vfracC))));
heapG_fork_postG :> inG Σ (authR (gmapUR positive (exclR (optionC ufracC))));
}.
Arguments heapG_name {_} _ : assert.
Arguments heapG_fork_post_name {_} _ : assert.
......@@ -31,7 +31,7 @@ Arguments heapG_fork_post_name {_} _ : assert.
Definition heap_perm `{hG : heapG Σ} (π : frac) : iProp Σ :=
own (heapG_name hG) (?{π} ε).
Instance perm_fractional `{hG : heapG Σ} : Fractional heap_perm.
Proof. intros π1 π2. by rewrite -own_op -vfrac_auth_frag_op left_id. Qed.
Proof. intros π1 π2. by rewrite -own_op -ufrac_auth_frag_op left_id. Qed.
Definition heapG_ironInvG `{hG : heapG Σ} : ironInvG Σ := {|
perm := heap_perm;
......@@ -42,7 +42,7 @@ Definition heapG_ironInvG `{hG : heapG Σ} : ironInvG Σ := {|
Definition heap_ctx `{hG : heapG Σ} (σ : state) (_ : list ()) (n : nat) : iProp Σ :=
( πfs,
size πfs = n
own (heapG_fork_post_name hG) ( (Excl <$> πfs : gmap _ (excl (option vfrac))))
own (heapG_fork_post_name hG) ( (Excl <$> πfs : gmap _ (excl (option ufrac))))
let πf : option fracR := [^op map] π πfs, π in
own (heapG_name hG) (?{1%Qp ? πf} (to_heap σ)))%I.
Definition heap_fork_post `{hG : heapG Σ} : iProp Σ :=
......@@ -126,7 +126,7 @@ Section heap.
Global Instance mapsto_uniform l q v : Uniform (l {q} v).
Proof.
intros π1 π2. rewrite mapsto_eq /perm /mapsto_def /=.
by rewrite -own_op -vfrac_auth_frag_op right_id.
by rewrite -own_op -ufrac_auth_frag_op right_id.
Qed.
Global Instance mapsto_exist_perm l q v : ExistPerm (l {q} v).
Proof. by rewrite /ExistPerm mapsto_eq. Qed.
......@@ -154,7 +154,7 @@ Section heap.
iStartProof (iProp _). rewrite mapsto_eq /mapsto_def /=.
iIntros ([π1|]) "H1"; iIntros ([π2|]) "H2 //=".
iDestruct (own_valid_2 with "H1 H2") as %Hv.
move: Hv. rewrite -vfrac_auth_frag_op vfrac_auth_frag_valid=>Hv.
move: Hv. rewrite -ufrac_auth_frag_op ufrac_auth_frag_valid=>Hv.
move: Hv. rewrite op_singleton singleton_valid pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
......@@ -174,7 +174,7 @@ Section heap.
Proof.
iStartProof (iProp _). rewrite mapsto_eq /mapsto_def /=.
iIntros ([π1|]) "H1 //=". iDestruct (own_valid with "H1") as %Hv.
move: Hv. rewrite vfrac_auth_frag_valid=> Hv.
move: Hv. rewrite ufrac_auth_frag_valid=> Hv.
move: Hv. by rewrite singleton_valid=> -[? _].
Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 :
......@@ -230,7 +230,7 @@ Section heap.
iIntros (Hπ). iDestruct 1 as (πfs <-) "[Hn Hσ]". iIntros "HQs Hp Hσ'".
iAssert (own (heapG_name H) (?{1%Qp ? ([^op map] π πfs, π)} (to_heap σ')))%I
with "[> Hn HQs Hp Hσ']" as "Hσ'"; last first.
{ by iDestruct (own_valid_2 with "Hσ Hσ'") as %?%vfrac_auth_agree%(inj _). }
{ by iDestruct (own_valid_2 with "Hσ Hσ'") as %?%ufrac_auth_agree%(inj _). }
iInduction (map_wf πfs) as [πfs _] "IH".
destruct (size πfs) as [|m'] eqn:Hsize; simpl.
{ apply map_size_empty_iff in Hsize as ->.
......@@ -280,7 +280,7 @@ Section heap.
iSplit; first (by rewrite map_size_insert // Hsize).
rewrite fmap_insert. iFrame "Hn". by rewrite big_opM_insert // left_id. }
iMod (own_update with "Hσ") as "[Hσ Hp]".
{ apply (vfrac_auth_update' _ π _ (ε : heapUR)).
{ apply (ufrac_auth_update_surplus _ π _ (ε : heapUR)).
rewrite right_id. apply to_heap_valid. }
rewrite right_id. iModIntro. iFrame "Hp".
iExists (<[i:=Some π]> πfs). iSplit; first (by rewrite map_size_insert // Hsize).
......@@ -296,7 +296,7 @@ Section heap.
iIntros (?). rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hp".
iMod (own_update_2 with "Hσ Hp") as "[Hσ Hl]".
{ eapply vfrac_auth_update,
{ eapply ufrac_auth_update,
(alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _))) => //.
by apply lookup_to_heap_None. }
iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame.
......@@ -309,9 +309,9 @@ Section heap.
rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %Hl%vfrac_auth_included_total%heap_singleton_included.
as %Hl%ufrac_auth_included_total%heap_singleton_included.
rewrite to_heap_delete. iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply vfrac_auth_update,
{ eapply ufrac_auth_update,
(delete_singleton_local_update_cancelable _ _ _).
by rewrite /to_heap lookup_fmap Hl. }
iModIntro. iFrame "Hl". iExists πfs. by iFrame.
......@@ -323,7 +323,7 @@ Section heap.
rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl". destruct π as [π|]=>//.
by iDestruct (own_valid_2 with "Hσ Hl")
as %Hl%vfrac_auth_included%Some_included_total%heap_singleton_included.
as %Hl%ufrac_auth_included%Some_included_total%heap_singleton_included.
Qed.
Lemma heap_update σ κ n l v1 v2 π :
......@@ -333,9 +333,9 @@ Section heap.
rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl". destruct π as [π|]=>//.
iDestruct (own_valid_2 with "Hσ Hl")
as %Hl%vfrac_auth_included%Some_included_total%heap_singleton_included.
as %Hl%ufrac_auth_included%Some_included_total%heap_singleton_included.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply vfrac_auth_update, singleton_local_update,
{ eapply ufrac_auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree v2))=> //.
by rewrite /to_heap lookup_fmap Hl. }
iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame.
......
From iron.heap_lang Require Export lang.
From iron.heap_lang Require Import proofmode notation.
From iron.iron_logic Require Import fcinv.
From iron.algebra Require Import vfrac.
From iron.algebra Require Import ufrac.
From iris.algebra Require Import frac_auth.
Section special.
......@@ -40,7 +40,7 @@ Section special.
iDestruct "Hp'" as "[Hp1 Hp2]".
iCombine "HΨ" "Hp2" as "HA".
rewrite -@uniform.
replace (π₁ πc') with (πc' π₁); last by rewrite !vfrac_op' Qp_plus_comm.
replace (π₁ πc') with (πc' π₁); last by rewrite !ufrac_op' Qp_plus_comm.
rewrite @uniform.
iDestruct "HA" as "[HΨ Hp2]".
iMod ("Hclose" with "[HΨ Hγinv Hγauth Hcancel]") as "_".
......@@ -50,7 +50,7 @@ Section special.
iDestruct "HΨ" as "[HΨ $]".
iSplitL "Hγauth".
- simpl. replace ((πc' / 2)%Qp (πc' / 2 + πc)%Qp) with (πc πc'); first done.
by rewrite assoc (vfrac_op' (πc' / 2)%Qp) Qp_div_2 !vfrac_op' Qp_plus_comm.
by rewrite assoc (ufrac_op' (πc' / 2)%Qp) Qp_div_2 !ufrac_op' Qp_plus_comm.
- rewrite /special /bi_or /= fracPred_or_eq /=.
iRight. iClear "#".
rewrite /bi_sep /= fracPred_sep_eq.
......@@ -92,7 +92,7 @@ Section special.
revert HValid. revert Heq. rewrite frac_auth_auth_valid.
rewrite assoc (comm_L _ _ πc'). rewrite (comm_L _ _ πc').
intros Heq HValid.
assert (Heqc := cancelable (πc' : vfrac) (π21 πΨ) πc HValid Heq).
assert (Heqc := cancelable (πc' : ufrac) (π21 πΨ) πc HValid Heq).
iExists (Some πΨ), (Some π21).
iSplit.
+ iPureIntro. rewrite -Some_op. f_equal. inversion Heqc. by rewrite comm_L.
......
......@@ -18,7 +18,7 @@ From iron.heap_lang Require Export lang heap.
From iron.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth.
From iron.algebra Require Import vfrac_auth vfrac.
From iron.algebra Require Import ufrac_auth.
Set Default Proof Using "Type".
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
......
......@@ -5,19 +5,18 @@ the [heap_lang/adequacy] file, where the results are used to show the absence
of memory leaks. *)
From iron.iron_logic Require Export weakestpre.
From iris.program_logic Require Export adequacy.
From iris.algebra Require Import frac_auth.
From iron.algebra Require Import vfrac.
From iris.algebra Require Import frac_auth ufrac.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(* Global functor setup *)
Definition ironInvΣ : gFunctors :=
#[invΣ; cinvΣ; GFunctor (frac_authR vfracR)].
#[invΣ; cinvΣ; GFunctor (frac_authR ufracR)].
Class ironInvPreG (Σ : gFunctors) : Set := IronInvPreG {
iron_inv_invPreG :> invPreG Σ;
iron_inv_cinvPreG :> cinvG Σ;
fcinv_inPreG :> inG Σ (frac_authR vfracR);
fcinv_inPreG :> inG Σ (frac_authR ufracR);
}.
Instance subG_invΣ {Σ} : subG ironInvΣ Σ ironInvPreG Σ.
......
......@@ -12,8 +12,7 @@ The construction of trackable invariants follows the usual Iris pattern: it
uses Iris cancable invariants, and on top of that, uses an authoritative camera
construction to take care of resource transfer. *)
From iron.iron_logic Require Export iron.
From iris.algebra Require Import frac_auth.
From iron.algebra Require Import vfrac.
From iris.algebra Require Import frac_auth ufrac.
From iris.proofmode Require Import tactics.
Record fcinv_name := FcInvName {
......@@ -35,7 +34,7 @@ Definition fcinv_own_eq `{ironInvG Σ} : fcinv_own = _ := fcinv_own_aux.(seal_eq
Definition fcinv_cancel_own_def `{ironInvG Σ} (γ : fcinv_name) (p : frac) : ironProp Σ :=
FracPred (λ π, if π is Some π
then own (fcinv_frac_name γ) (!{p} (π:vfrac)) else False)%I.
then own (fcinv_frac_name γ) (!{p} (π:ufrac)) else False)%I.
Definition fcinv_cancel_own_aux `{ironInvG Σ} : seal fcinv_cancel_own_def. by eexists. Qed.
Definition fcinv_cancel_own `{ironInvG Σ} := fcinv_cancel_own_aux.(unseal).
Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ :=
......@@ -44,7 +43,7 @@ Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ :=
Definition fcinv_def `{ironInvG Σ, invG Σ} (N : namespace) (γ : fcinv_name)
(P : ironProp Σ) : ironProp Σ :=
(<affine> cinv N (fcinv_cinv_name γ) ( π1 π2,
own (fcinv_frac_name γ) (! (π1 ? π2 : vfrac)) perm π1 P π2) )%I.
own (fcinv_frac_name γ) (! (π1 ? π2 : ufrac)) perm π1 P π2) )%I.
Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed.
Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal).
Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq).
......@@ -122,7 +121,7 @@ Proof.
rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq.
iStartProof (iProp _); iIntros (π1) "Hp".
iMod (cinv_alloc_strong _ N) as (γinv ?) "[Hγinv Halloc]".
iMod (own_alloc (! (1%Qp : vfrac) ! (1%Qp : vfrac)))
iMod (own_alloc (! (1%Qp : ufrac) ! (1%Qp : ufrac)))
as (γf) "[Hγauth Hγ]"; first done.
set (γ := FcInvName γinv γf).
iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"].
......@@ -131,8 +130,8 @@ Proof.
iExists (π3 / 2)%Qp, (Some (π3 / 2)%Qp π2). iFrame "Hp'".
iMod (own_update_2 with "Hγauth Hγ") as "[Hγauth Hγ]".
{ by apply frac_auth_update,
(replace_local_update _ ((π3 / 2)%Qp ? π2 : vfrac)). }
iMod ("Halloc" $! ( π1 π2, own (fcinv_frac_name γ) (! (π1 ? π2 : vfrac))
(replace_local_update _ ((π3 / 2)%Qp ? π2 : ufrac)). }
iMod ("Halloc" $! ( π1 π2, own (fcinv_frac_name γ) (! (π1 ? π2 : ufrac))
perm π1 P π2)%I with "[Hγauth Hp HP]"); first by eauto with iFrame.
iModIntro; iSplit; [by rewrite -!cmra_opM_opM_assoc_L /= frac_op' Qp_div_2|].
iExists (Some (π3 / 2)%Qp π2), ε; iSplit; first by rewrite right_id_L.
......
......@@ -30,7 +30,7 @@ From iris.bi.lib Require Export fractional.
From iris.base_logic.lib Require Export fancy_updates invariants.
From iris.base_logic.lib Require Export cancelable_invariants.
From iris.algebra Require Import frac_auth.
From iron.algebra Require Import vfrac.
From iris.algebra Require Import ufrac.
From iris.proofmode Require Import tactics.
From iron.proofmode Require Import fracpred.
......@@ -39,7 +39,7 @@ Class ironInvG (Σ : gFunctors) := IronInvG {
perm_fractional :> Fractional perm;
perm_timeless π :> Timeless (perm π);
fcinv_cinvG :> cinvG Σ;
fcinv_inG :> inG Σ (frac_authR vfracR);
fcinv_inG :> inG Σ (frac_authR ufracR);
}.
Notation ironProp Σ := (fracPred (iProp Σ)).
Notation ironPropC Σ := (fracPredC (iProp Σ)).
......
Markdown is supported
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