wsat.v 8.45 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
Require Export iris.model prelude.co_pset.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
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)
8
    (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
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 {_ _ _ _ _ _} _ _ _ _ _.

22
Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
25
Arguments wsat : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29

Section wsat.
Context {Σ : iParam}.
Implicit Types σ : istate Σ.
30 31
Implicit Types r : iRes Σ.
Implicit Types rs : gmap positive (iRes Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
62 63 64 65
Proof.
  destruct n; [intros; apply cmra_valid_0|intros [rs ?]].
  eapply cmra_valid_op_l, wsat_pre_valid; eauto.
Qed.
66
Lemma wsat_init k E σ m : {S k} m  wsat (S k) E σ (Res  (Excl σ) m).
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Proof.
68
  intros Hv. exists ; constructor; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  * rewrite big_opM_empty right_id.
70 71
    split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
      constructor || apply Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74
  * by intros i; rewrite lookup_empty=>-[??].
  * intros i P ?; rewrite /= (left_id _ _) lookup_empty; inversion_clear 1.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
113
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
123
Qed.
124
Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
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.