wsat.v 8.45 KB
 Robbert Krebbers committed Jan 16, 2016 1 ``````Require Export iris.model prelude.co_pset. `````` Robbert Krebbers committed Jan 18, 2016 2 ``````Local Hint Extern 10 (_ ≤ _) => omega. `````` Robbert Krebbers committed Jan 16, 2016 3 4 5 6 7 ``````Local Hint Extern 10 (✓{_} _) => solve_validN. Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN. Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN. Record wsat_pre {Σ} (n : nat) (E : coPset) `````` Ralf Jung committed Jan 21, 2016 8 `````` (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := { `````` Robbert Krebbers committed Jan 16, 2016 9 10 11 12 13 14 15 16 17 18 19 20 21 `````` wsat_pre_valid : ✓{S n} r; wsat_pre_state : pst r ≡ Excl σ; wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i); wsat_pre_wld i P : i ∈ E → wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) → ∃ r', rs !! i = Some r' ∧ P n r' }. Arguments wsat_pre_valid {_ _ _ _ _ _} _. Arguments wsat_pre_state {_ _ _ _ _ _} _. Arguments wsat_pre_dom {_ _ _ _ _ _} _ _ _. Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _. `````` Ralf Jung committed Jan 21, 2016 22 ``````Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : Prop := `````` Robbert Krebbers committed Jan 16, 2016 23 24 `````` match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end. Instance: Params (@wsat) 4. `````` Robbert Krebbers committed Jan 18, 2016 25 ``````Arguments wsat : simpl never. `````` Robbert Krebbers committed Jan 16, 2016 26 27 28 29 `````` Section wsat. Context {Σ : iParam}. Implicit Types σ : istate Σ. `````` Ralf Jung committed Jan 21, 2016 30 31 ``````Implicit Types r : iRes Σ. Implicit Types rs : gmap positive (iRes Σ). `````` Robbert Krebbers committed Jan 16, 2016 32 33 34 35 36 37 38 39 40 41 42 ``````Implicit Types P : iProp Σ. Instance wsat_ne' : Proper (dist n ==> impl) (wsat (Σ:=Σ) n E σ). Proof. intros [|n] E σ r1 r2 Hr; first done; intros [rs [Hdom Hv Hs Hinv]]. exists rs; constructor; intros until 0; setoid_rewrite <-Hr; eauto. Qed. Global Instance wsat_ne n : Proper (dist n ==> iff) (wsat (Σ:=Σ) n E σ) | 1. Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed. Global Instance wsat_proper n : Proper ((≡) ==> iff) (wsat (Σ:=Σ) n E σ) | 1. Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed. `````` Robbert Krebbers committed Jan 18, 2016 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 ``````Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r. Proof. destruct n as [|n], n' as [|n']; simpl; try by (auto with lia). intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto. intros i P ? HiP; destruct (wld (r ⋅ big_opM rs) !! i) as [P'|] eqn:HP'; [apply (injective Some) in HiP|inversion_clear HiP]. assert (P' ={S n}= to_agree \$ Later \$ iProp_unfold \$ iProp_fold \$ later_car \$ P' (S n)) as HPiso. { rewrite iProp_unfold_fold later_eta to_agree_car //. apply (map_lookup_validN _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. } assert (P ={n'}= iProp_fold (later_car (P' (S n)))) as HPP'. { apply (injective iProp_unfold), (injective Later), (injective to_agree). by rewrite -HiP -(dist_le _ _ _ _ HPiso). } destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto. { by rewrite HP' -HPiso. } assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto). exists r'; split; [done|apply HPP', uPred_weaken with r' n; auto]. Qed. Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r. `````` Robbert Krebbers committed Jan 16, 2016 62 63 64 65 ``````Proof. destruct n; [intros; apply cmra_valid_0|intros [rs ?]]. eapply cmra_valid_op_l, wsat_pre_valid; eauto. Qed. `````` Ralf Jung committed Jan 25, 2016 66 ``````Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl σ) m). `````` Robbert Krebbers committed Jan 20, 2016 67 ``````Proof. `````` Ralf Jung committed Jan 25, 2016 68 `````` intros Hv. exists ∅; constructor; auto. `````` Robbert Krebbers committed Jan 20, 2016 69 `````` * rewrite big_opM_empty right_id. `````` Ralf Jung committed Jan 25, 2016 70 71 `````` split_ands'; try (apply cmra_valid_validN, ra_empty_valid); constructor || apply Hv. `````` Robbert Krebbers committed Jan 20, 2016 72 73 74 `````` * by intros i; rewrite lookup_empty=>-[??]. * intros i P ?; rewrite /= (left_id _ _) lookup_empty; inversion_clear 1. Qed. `````` Robbert Krebbers committed Jan 16, 2016 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 ``````Lemma wsat_open n E σ r i P : wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) → i ∉ E → wsat (S n) ({[i]} ∪ E) σ r → ∃ rP, wsat (S n) E σ (rP ⋅ r) ∧ P n rP. Proof. intros HiP Hi [rs [Hval Hσ HE Hwld]]. destruct (Hwld i P) as (rP&?&?); [solve_elem_of +|by apply lookup_wld_op_l|]. assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr. { by rewrite (commutative _ rP) -(associative _) big_opM_delete. } exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto. * intros j; rewrite lookup_delete_is_Some Hr. generalize (HE j); solve_elem_of +Hi. * intros j P'; rewrite Hr=> Hj ?. setoid_rewrite lookup_delete_ne; last (solve_elem_of +Hi Hj). apply Hwld; [solve_elem_of +Hj|done]. Qed. Lemma wsat_close n E σ r i P rP : wld rP !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) → i ∉ E → wsat (S n) E σ (rP ⋅ r) → P n rP → wsat (S n) ({[i]} ∪ E) σ r. Proof. intros HiP HiE [rs [Hval Hσ HE Hwld]] ?. assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver). assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr. { by rewrite (commutative _ rP) -(associative _) big_opM_insert. } exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto. * intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst. + rewrite !lookup_op HiP !op_is_Some; solve_elem_of -. + destruct (HE j) as [Hj Hj']; auto; solve_elem_of +Hj Hj'. * intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst. + rewrite !lookup_wld_op_l ?HiP; auto=> HP. apply (injective Some), (injective to_agree), (injective Later), (injective iProp_unfold) in HP. exists rP; split; [rewrite lookup_insert|apply HP]; auto. + intros. destruct (Hwld j P') as (r'&?&?); auto. exists r'; rewrite lookup_insert_ne; naive_solver. Qed. `````` Robbert Krebbers committed Jan 18, 2016 110 111 112 ``````Lemma wsat_update_pst n E σ1 σ1' r rf : pst r ={S n}= Excl σ1 → wsat (S n) E σ1' (r ⋅ rf) → σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf). `````` Robbert Krebbers committed Jan 16, 2016 113 ``````Proof. `````` Robbert Krebbers committed Jan 18, 2016 114 115 116 117 118 119 120 121 122 `````` intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *. assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'. { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r (associative _). } assert (σ1' = σ1) as ->. { apply leibniz_equiv, (timeless _), dist_le with (S n); auto. apply (injective Excl). by rewrite -Hpst_r -Hpst -(associative _) Hpst' (right_id _). } split; [done|exists rs]. by constructor; split_ands'; try (rewrite /= -(associative _) Hpst'). `````` Robbert Krebbers committed Jan 16, 2016 123 ``````Qed. `````` Ralf Jung committed Jan 21, 2016 124 ``````Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) : `````` Robbert Krebbers committed Jan 16, 2016 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 `````` m1 ≼{S n} gst r → m1 ⇝: P → wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2. Proof. intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]]. destruct (Hup (mf ⋅ gst (rf ⋅ big_opM rs)) (S n)) as (m2&?&Hval'). { by rewrite /= (associative _ m1) -Hr (associative _). } exists m2; split; [exists rs; split; split_ands'; auto|done]. Qed. Lemma wsat_alloc n E1 E2 σ r P rP : ¬set_finite E1 → P n rP → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) → ∃ i, wsat (S n) (E1 ∪ E2) σ (Res {[i ↦ to_agree (Later (iProp_unfold P))]} ∅ ∅ ⋅ r) ∧ wld r !! i = None ∧ i ∈ E1. Proof. intros HE1 ? [rs [Hval Hσ HE Hwld]]. assert (∃ i, i ∈ E1 ∧ wld r !! i = None ∧ wld rP !! i = None ∧ wld (big_opM rs) !! i = None) as (i&Hi&Hri&HrPi&Hrsi). { exists (coPpick (E1 ∖ (dom _ (wld r) ∪ (dom _ (wld rP) ∪ dom _ (wld (big_opM rs)))))). rewrite -!not_elem_of_dom -?not_elem_of_union -elem_of_difference. apply coPpick_elem_of=>HE'; eapply HE1, (difference_finite_inv _ _), HE'. by repeat apply union_finite; apply dom_finite. } assert (rs !! i = None). { apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'. rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. } assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr. { by rewrite (commutative _ rP) -(associative _) big_opM_insert. } exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto. * destruct Hval as (?&?&?); rewrite -(associative _) Hr. split_ands'; rewrite /= ?(left_id _ _); [|eauto|eauto]. intros j; destruct (decide (j = i)) as [->|]. + by rewrite !lookup_op Hri HrPi Hrsi !(right_id _ _) lookup_singleton. + by rewrite lookup_op lookup_singleton_ne // (left_id _ _). * by rewrite -(associative _) Hr /= (left_id _ _). * intros j; rewrite -(associative _) Hr; destruct (decide (j = i)) as [->|]. + rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi. + rewrite lookup_insert_ne //. rewrite lookup_op lookup_singleton_ne // (left_id _ _); eauto. * intros j P'; rewrite -(associative _) Hr; destruct (decide (j=i)) as [->|]. + rewrite /= !lookup_op Hri HrPi Hrsi (right_id _ _) lookup_singleton=>? HP. apply (injective Some), (injective to_agree), (injective Later), (injective iProp_unfold) in HP. exists rP; rewrite lookup_insert; split; [|apply HP]; auto. + rewrite /= lookup_op lookup_singleton_ne // (left_id _ _)=> ??. destruct (Hwld j P') as [r' ?]; auto. by exists r'; rewrite lookup_insert_ne. Qed. End wsat.``````