diff --git a/_CoqProject b/_CoqProject index b4f5b22a8deb3058cc40a9aebb00518c6b07f78f..1a54d06c65d1143359421fe2f0c03983713936d6 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,6 +1,5 @@ -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 diff --git a/opam b/opam index 333b49335aaf25a64944ef2b4a3c7f3b9ac34d18..fd471dabdb890e5a4cf4173e222a96e3db835738 100644 --- a/opam +++ b/opam @@ -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") } ] diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v deleted file mode 100644 index 0e8271bf245cb2fad737e57b2ced0eb9352f5b0d..0000000000000000000000000000000000000000 --- a/theories/algebra/ufrac_auth.v +++ /dev/null @@ -1,142 +0,0 @@ -(** 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. diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v index 08c788a0868c3288fe36ce25ea9f277f674b6cc6..0131ecf3727b117258bd872e138c93f2fc97aa40 100644 --- a/theories/heap_lang/adequacy.v +++ b/theories/heap_lang/adequacy.v @@ -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. } diff --git a/theories/heap_lang/heap.v b/theories/heap_lang/heap.v index ff41e505c50a45a6fad968bb60eb6df1e6c970b7..fec321a96439d0513f530734f8e7d2b70e5c884f 100644 --- a/theories/heap_lang/heap.v +++ b/theories/heap_lang/heap.v @@ -1,14 +1,13 @@ (** 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". diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v index c10416890ed3431fc92ab8b8a32a39f28f42d042..8aa2ebf22e9ed5e18724728176687ab04b3f28f7 100644 --- a/theories/heap_lang/lifting.v +++ b/theories/heap_lang/lifting.v @@ -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