Commit 91237cf7 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (which now contains `ufrac_auth`).

parent 356a30f7
Pipeline #17363 failed with stage
in 9 minutes and 4 seconds
-Q theories iron
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-undeclared-scope,-convert_concl_no_check
theories/algebra/ufrac_auth.v
theories/bi/fracpred.v
theories/proofmode/fracpred.v
theories/iron_logic/iron.v
......
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2019-06-06.3.ec161a20") | (= "dev") }
"coq-iris" { (= "dev.2019-06-11.5.e65b06a7") | (= "dev") }
]
(** This file provides the unbounded fractional authoritative camera: a version
of the fractional authoritative camera that can be used with fractions [> 1].
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 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
>>>
- We no longer have the [◯?{1} a] is the exclusive fragmental element (cf.
[frac_auth_frag_validN_op_1_l]).
*)
From iris.algebra Require Export auth frac.
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 ufrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR ufracR A)).
Definition ufrac_authUR (A : cmraT) : ucmraT :=
authUR (optionUR (prodR ufracR A)).
Definition ufrac_auth_auth {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
(Some (q,x)).
Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
(Some (q,x)).
Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
Instance: Params (@ufrac_auth_auth) 2 := {}.
Instance: Params (@ufrac_auth_frag) 2 := {}.
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 ufrac_auth.
Context {A : cmraT}.
Implicit Types a b : A.
Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_auth_proper q : Proper (() ==> ()) (@ufrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_frag_ne q : NonExpansive (@ufrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_frag_proper q : Proper (() ==> ()) (@ufrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_auth_discrete a : Discrete a Discrete (?{q} a).
Proof.
intros; apply (@auth_auth_discrete (optionUR (prodR fracR A)));
[apply Some_discrete|]; apply _.
Qed.
Global Instance ufrac_auth_frag_discrete a : Discrete a Discrete (?{q} a).
Proof.
intros; apply (@auth_frag_discrete (optionUR (prodR fracR A))), Some_discrete;
apply _.
Qed.
Lemma ufrac_auth_validN n a p : {n} a {n} (?{p} a ?{p} a).
Proof. by rewrite auth_both_validN. Qed.
Lemma ufrac_auth_valid p a : a (?{p} a ?{p} a).
Proof. intros. by apply (@auth_both_valid_2 (optionUR (prodR ufracR A))). Qed.
Lemma ufrac_auth_agreeN n p a b : {n} (?{p} a ?{p} b) a {n} b.
Proof.
rewrite auth_both_validN => -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[//]|[[[p' ?] ?] [/=]]].
rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed.
Lemma ufrac_auth_agree p a b : (?{p} a ?{p} b) a b.
Proof.
intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
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 ufrac_auth_includedN n p q a b : {n} (?{p} a ?{q} b) Some b {n} Some a.
Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
(?{p} a ?{q} b) Some b Some a.
Proof. rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _] //. Qed.
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, 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, ufrac_auth_included. Qed.
Lemma ufrac_auth_auth_validN n q a : {n} (?{q} a) {n} a.
Proof.
rewrite -auth_auth_validN. split; [by intros []|].
repeat split; simpl; by try apply: ucmra_unit_leastN.
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 ufrac_auth_frag_validN n q a : {n} (?{q} a) {n} a.
Proof. split. by intros [??]. by split. Qed.
Lemma ufrac_auth_frag_valid q a : (?{q} a) a.
Proof. split. by intros [??]. by split. Qed.
Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ?{q1+q2} (a1 a2) ?{q1} a1 ?{q2} a2.
Proof. done. Qed.
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_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 -ufrac_auth_frag_op -core_id_dup.
Qed.
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 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.
intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.
split.
- split; by apply cmra_valid_validN.
- rewrite -pair_op Some_op Heq comm.
destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
Qed.
End ufrac_auth.
......@@ -4,9 +4,8 @@ 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 ufrac excl.
From iris.algebra Require Import big_op gmap ufrac excl ufrac_auth.
From iron.iron_logic Require Export weakestpre adequacy.
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".
......@@ -34,7 +33,7 @@ Proof.
(* TODO: refactor this proof so we don't have the two cases *)
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']]".
iMod (own_alloc (U{1} (U{1/2} U{1/2} ε))) as (γ) "[Hσ [Hp Hp']]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
by apply ufrac_auth_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first by apply auth_auth_valid.
......@@ -51,8 +50,8 @@ Proof.
iModIntro. iApply ("H" with "Hctx").
- intros Hwp; eapply (iron_wp_adequacy _ _ _ _ _ _ (1 / 2 / 2) (Some (1 / 2)%Qp)).
iIntros (? κs) "".
iMod (own_alloc (?{1} (to_heap σ)
(?{1/2} (to_heap σ) ?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]".
iMod (own_alloc (U{1} (to_heap σ)
(U{1/2} (to_heap σ) U{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]".
{ 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 by apply auth_auth_valid.
......@@ -99,7 +98,7 @@ Proof.
eapply (iron_wp_all_adequacy _ heap_lang _ _ σ2' _ _ (λ _, σ2' = σ2) _ ε);
[|done]; iIntros (? κs) "".
iMod (own_alloc ( )) as (γf) "Hf"; first by apply auth_auth_valid.
iMod (own_alloc (?{1} (to_heap ) (?{1/2} (to_heap ) ?{1/2} ε)))
iMod (own_alloc (U{1} (to_heap ) (U{1/2} (to_heap ) U{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
......@@ -124,7 +123,7 @@ Proof.
eapply (iron_wp_all_adequacy _ heap_lang _ _ σ1 σ2' _ _ (λ _, σ2' = σ2) _
(Some (1 / 2)%Qp)); [|done]; iIntros (? κs) "".
iMod (own_alloc ( )) as (γf) "Hf"; first by apply auth_auth_valid.
iMod (own_alloc (?{1} (to_heap σ1) (?{1/2} (to_heap σ1) ?{1/2} ε)))
iMod (own_alloc (U{1} (to_heap σ1) (U{1/2} (to_heap σ1) U{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
......
(** 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 excl frac_auth gmap agree gmultiset ufrac.
From iris.algebra Require Import excl frac_auth gmap agree gmultiset ufrac ufrac_auth.
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 ufrac_auth.
Set Default Proof Using "Type".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (agreeR valC)).
......@@ -29,7 +28,7 @@ Arguments heapG_name {_} _ : assert.
Arguments heapG_fork_post_name {_} _ : assert.
Definition heap_perm `{hG : heapG Σ} (π : frac) : iProp Σ :=
own (heapG_name hG) (?{π} ε).
own (heapG_name hG) (U{π} ε).
Instance perm_fractional `{hG : heapG Σ} : Fractional heap_perm.
Proof. intros π1 π2. by rewrite -own_op -ufrac_auth_frag_op left_id. Qed.
......@@ -44,7 +43,7 @@ Definition heap_ctx `{hG : heapG Σ} (σ : state) (_ : list ()) (n : nat) : iPro
size πfs = n
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.
own (heapG_name hG) (U{1%Qp ? πf} (to_heap σ)))%I.
Definition heap_fork_post `{hG : heapG Σ} : iProp Σ :=
( i π,
from_option heap_perm True π
......@@ -63,7 +62,7 @@ Section definitions.
Definition mapsto_def (l : loc) (q : Qp) (v : val) : ironProp Σ :=
FracPred (from_option
(λ π, own (heapG_name hG) (?{π} {[ l := (q, to_agree v) ]}))
(λ π, own (heapG_name hG) (U{π} {[ l := (q, to_agree v) ]}))
False)%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
......@@ -193,7 +192,7 @@ Section heap.
by iDestruct "Hσ" as ([π3|] [π4|] ?) "[? _]".
Qed.
Lemma big_mapsto_alt_1 σ π :
([ map] l v σ, l v) (Some π) own (heapG_name H) (?{π} (to_heap σ)).
([ map] l v σ, l v) (Some π) own (heapG_name H) (U{π} (to_heap σ)).
Proof.
revert π. induction σ as [|l v σ Hl IH] using map_ind=> π.
{ rewrite big_sepM_empty fracPred_at_emp. iIntros ([=]). }
......@@ -206,7 +205,7 @@ Section heap.
Qed.
Lemma big_mapsto_alt_2 σ π :
σ
own (heapG_name H) (?{π} (to_heap σ)) ([ map] l v σ, l v) (Some π).
own (heapG_name H) (U{π} (to_heap σ)) ([ map] l v σ, l v) (Some π).
Proof.
revert π. induction σ as [|l v σ Hl IH] using map_ind; [done|intros π _].
rewrite to_heap_insert. destruct (decide (σ = )) as [->|].
......@@ -228,7 +227,7 @@ Section heap.
σ = σ' .
Proof.
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
iAssert (own (heapG_name H) (U{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 %?%ufrac_auth_agree%(inj _). }
iInduction (map_wf πfs) as [πfs _] "IH".
......
......@@ -17,8 +17,7 @@ From iron.iron_logic Require Import lifting.
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 ufrac_auth.
From iris.algebra Require Import frac_auth ufrac_auth.
Set Default Proof Using "Type".
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
......
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