wsat.v 8.61 KB
Newer Older
1 2
Require Export program_logic.model prelude.co_pset.
Require Export algebra.cmra_big_op algebra.cmra_tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Hint Extern 10 ({_} _) => solve_validN.
5 6
Local Hint Extern 1 ({_} gst _) => apply gst_validN.
Local Hint Extern 1 ({_} wld _) => apply wld_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8 9
Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
    (σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12 13 14
  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 
15
    wld r !! i {S n} Some (to_agree (Next (iProp_unfold P))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17
     r', rs !! i = Some r'  P n r'
}.
18 19 20 21
Arguments wsat_pre_valid {_ _ _ _ _ _ _} _.
Arguments wsat_pre_state {_ _ _ _ _ _ _} _.
Arguments wsat_pre_dom {_ _ _ _ _ _ _} _ _ _.
Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23 24
Definition wsat {Λ Σ}
  (n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  match n with 0 => True | S n =>  rs, wsat_pre n E σ rs (r  big_opM rs) end.
26
Instance: Params (@wsat) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Arguments wsat : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29

Section wsat.
30 31 32 33 34 35
Context {Λ : language} {Σ : iFunctor}.
Implicit Types σ : state Λ.
Implicit Types r : iRes Λ Σ.
Implicit Types rs : gmap positive (iRes Λ Σ).
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
36
Implicit Types mm : option (iGst Λ Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
Instance wsat_ne' : Proper (dist n ==> impl) (@wsat Λ Σ n E σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40 41 42
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.
43
Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
45
Global Instance wsat_proper n : Proper (() ==> iff) (@wsat Λ Σ n E σ) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49 50 51 52
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].
53
  assert (P' {S n} to_agree $ Next $ iProp_unfold $
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56
                       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. }
57
  assert (P {n'} iProp_fold (later_car (P' (S n)))) as HPP'.
58
  { apply (injective iProp_unfold), (injective Next), (injective to_agree).
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61 62 63 64
    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.
65
Lemma wsat_valid n E σ r : n  0  wsat n E σ r  {n} r.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
67 68
  destruct n; first done.
  intros _ [rs ?]; eapply cmra_validN_op_l, wsat_pre_valid; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
70
Lemma wsat_init k E σ mm : {S k} mm  wsat (S k) E σ (Res  (Excl σ) mm).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Proof.
72
  intros Hv. exists ; constructor; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  * rewrite big_opM_empty right_id.
74 75
    split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
      constructor || apply Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  * by intros i; rewrite lookup_empty=>-[??].
77
  * intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Lemma wsat_open n E σ r i P :
80
  wld r !! i {S n} Some (to_agree (Next (iProp_unfold P)))  i  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82 83 84 85
  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.
86
  { by rewrite (commutative _ rP) -associative big_opM_delete. }
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90 91 92 93 94
  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 :
95
  wld rP !! i {S n} Some (to_agree (Next (iProp_unfold P)))  i  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
96 97 98 99 100
  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.
101
  { by rewrite (commutative _ rP) -associative big_opM_insert. }
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105 106 107 108
  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),
109
        (injective Next), (injective iProp_unfold) in HP.
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113
      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
114
Lemma wsat_update_pst n E σ1 σ1' r rf :
115
  pst r {S n} Excl σ1  wsat (S n) E σ1' (r  rf) 
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  σ1' = σ1   σ2, wsat (S n) E σ2 (update_pst σ2 r  rf).
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119
  intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
  assert (pst rf  pst (big_opM rs) = ) as Hpst'.
120
  { by apply: (excl_validN_inv_l (S n) σ1); rewrite -Hpst_r associative. }
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123
  assert (σ1' = σ1) as ->.
  { apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
    apply (injective Excl).
124
    by rewrite -Hpst_r -Hpst -associative Hpst' (right_id _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
125
  split; [done|exists rs].
126
  by constructor; split_ands'; try (rewrite /= -associative Hpst').
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129
Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ  Prop) :
  mm1 {S n} gst r  mm1 ~~>: (λ mm2, default False mm2 P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131
  wsat (S n) E σ (r  rf)   m2, wsat (S n) E σ (update_gst m2 r  rf)  P m2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
133
  destruct (Hup (mf  gst (rf  big_opM rs)) (S n)) as ([m2|]&?&Hval'); try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
  { by rewrite /= (associative _ mm1) -Hr associative. }
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137 138 139
  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) σ
140
         (Res {[i  to_agree (Next (iProp_unfold P))]}    r) 
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143 144 145 146 147 148 149 150 151 152 153 154
       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.
155
  { by rewrite (commutative _ rP) -associative big_opM_insert. }
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
157 158
  * destruct Hval as (?&?&?);  rewrite -associative Hr.
    split_ands'; rewrite /= ?left_id; [|eauto|eauto].
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160 161
    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 _ _).
162 163
  * by rewrite -associative Hr /= left_id.
  * intros j; rewrite -associative Hr; destruct (decide (j = i)) as [->|].
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165
    + rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi.
    + rewrite lookup_insert_ne //.
166 167 168
      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.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
      apply (injective Some), (injective to_agree),
170
        (injective Next), (injective iProp_unfold) in HP.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
      exists rP; rewrite lookup_insert; split; [|apply HP]; auto.
172
    + rewrite /= lookup_op lookup_singleton_ne // left_id=> ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176
      destruct (Hwld j P') as [r' ?]; auto.
      by exists r'; rewrite lookup_insert_ne.
Qed.
End wsat.