invariants.v 6.62 KB
Newer Older
1 2
From stdpp Require Export namespaces.
From iris.proofmode Require Import tactics.
3 4 5
From iris.algebra Require Import gmap.
From iris.base_logic.lib Require Export fancy_updates.
From iris.base_logic.lib Require Import wsat.
6
Set Default Proof Using "Type".
7
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

Ralf Jung's avatar
Ralf Jung committed
9 10 11 12 13 14 15 16
(** Semantic Invariants *)
Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
  (  E, ⌜↑N  E  |={E,E  N}=>  P  ( P ={E  N,E}= True))%I.
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
Instance: Params (@inv) 3 := {}.
Typeclasses Opaque inv.
17

Simon Spies's avatar
Simon Spies committed
18 19 20
(** * Invariants *)
Section inv.
  Context `{!invG Σ}.
Ralf Jung's avatar
Ralf Jung committed
21 22 23 24
  Implicit Types i : positive.
  Implicit Types N : namespace.
  Implicit Types E : coPset.
  Implicit Types P Q R : iProp Σ.
Simon Spies's avatar
Simon Spies committed
25

Ralf Jung's avatar
Ralf Jung committed
26 27
  (** ** Internal model of invariants *)
  Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
28
    ( i, i  (N:coPset)  ownI i P)%I.
Simon Spies's avatar
Simon Spies committed
29

Ralf Jung's avatar
Ralf Jung committed
30
  Lemma own_inv_acc E N P :
Ralf Jung's avatar
Ralf Jung committed
31
    N  E  own_inv N P ={E,E∖↑N}=  P  ( P ={E∖↑N,E}= True).
Simon Spies's avatar
Simon Spies committed
32
  Proof.
33
    rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
Simon Spies's avatar
Simon Spies committed
34 35 36 37
    iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
    rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
    rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
    iIntros "(Hw & [HE $] & $) !> !>".
38 39
    iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & $ & HD)".
    iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P). by iFrame.
Simon Spies's avatar
Simon Spies committed
40 41
  Qed.

Ralf Jung's avatar
Ralf Jung committed
42 43 44 45 46 47 48 49 50 51
  Lemma fresh_inv_name (E : gset positive) N :  i, i  E  i  (N:coPset).
  Proof.
    exists (coPpick ( N  gset_to_coPset E)).
    rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference.
    apply coPpick_elem_of=> Hfin.
    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
    apply gset_to_coPset_finite.
  Qed.

  Lemma own_inv_alloc N E P :  P ={E}= own_inv N P.
Simon Spies's avatar
Simon Spies committed
52
  Proof.
Ralf Jung's avatar
Ralf Jung committed
53
    rewrite uPred_fupd_eq. iIntros "HP [Hw $]".
Simon Spies's avatar
Simon Spies committed
54 55
    iMod (ownI_alloc (. (N : coPset)) P with "[$HP $Hw]")
      as (i ?) "[$ ?]"; auto using fresh_inv_name.
56
    do 2 iModIntro. iExists i. auto.
Simon Spies's avatar
Simon Spies committed
57 58
  Qed.

59
  (* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
Ralf Jung's avatar
Ralf Jung committed
60 61
  Lemma own_inv_alloc_open N E P :
    N  E  (|={E, E∖↑N}=> own_inv N P  (P ={E∖↑N, E}= True))%I.
Simon Spies's avatar
Simon Spies committed
62
  Proof.
Ralf Jung's avatar
Ralf Jung committed
63
    rewrite uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
Simon Spies's avatar
Simon Spies committed
64 65 66 67 68 69 70 71
    iMod (ownI_alloc_open (. (N : coPset)) P with "Hw")
      as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
    iAssert (ownE {[i]}  ownE ( N  {[i]})  ownE (E   N))%I
      with "[HE]" as "(HEi & HEN\i & HE\N)".
    { rewrite -?ownE_op; [|set_solver..].
      rewrite assoc_L -!union_difference_L //. set_solver. }
    do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
    iSplitL "Hi".
72
    { iExists i. auto. }
Simon Spies's avatar
Simon Spies committed
73 74 75 76 77 78 79 80
    iIntros "HP [Hw HE\N]".
    iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
    do 2 iModIntro. iSplitL; [|done].
    iCombine "HEi HEN\i HE\N" as "HEN".
    rewrite -?ownE_op; [|set_solver..].
    rewrite assoc_L -!union_difference_L //; set_solver.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
81 82 83
  Lemma own_inv_to_inv M P: own_inv M P  - inv M P.
  Proof.
    iIntros "#I". rewrite inv_eq. iIntros (E H).
Ralf Jung's avatar
Ralf Jung committed
84
    iPoseProof (own_inv_acc with "I") as "H"; eauto.
Ralf Jung's avatar
Ralf Jung committed
85
  Qed.
Simon Spies's avatar
Simon Spies committed
86

Ralf Jung's avatar
Ralf Jung committed
87 88
  (** ** Public API of invariants *)
  Global Instance inv_contractive N : Contractive (inv N).
Simon Spies's avatar
Simon Spies committed
89 90 91 92 93
  Proof. rewrite inv_eq. solve_contractive. Qed.

  Global Instance inv_ne N : NonExpansive (inv N).
  Proof. apply contractive_ne, _. Qed.

Ralf Jung's avatar
Ralf Jung committed
94
  Global Instance inv_proper N : Proper (equiv ==> equiv) (inv N).
Simon Spies's avatar
Simon Spies committed
95 96
  Proof. apply ne_proper, _. Qed.

Ralf Jung's avatar
Ralf Jung committed
97 98
  Global Instance inv_persistent N P : Persistent (inv N P).
  Proof. rewrite inv_eq. apply _. Qed.
Simon Spies's avatar
Simon Spies committed
99

Ralf Jung's avatar
Ralf Jung committed
100
  Lemma inv_alter N P Q:
Simon Spies's avatar
Simon Spies committed
101 102
    inv N P -   (P - Q  (Q - P)) - inv N Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
103 104 105 106
    rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
    iMod ("HI" $! E H) as "[HP Hclose]".
    iDestruct ("Acc" with "HP") as "[$ HQP]".
    iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
Simon Spies's avatar
Simon Spies committed
107 108 109 110
  Qed.

  Lemma inv_iff N P Q :   (P  Q) - inv N P - inv N Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
111
    iIntros "#HPQ #HI". iApply (inv_alter with "HI").
Ralf Jung's avatar
Ralf Jung committed
112
    iIntros "!> !# HP". iSplitL "HP".
Simon Spies's avatar
Simon Spies committed
113
    - by iApply "HPQ".
Ralf Jung's avatar
Ralf Jung committed
114
    - iIntros "HQ". by iApply "HPQ".
Simon Spies's avatar
Simon Spies committed
115 116 117 118
  Qed.

  Lemma inv_alloc N E P :  P ={E}= inv N P.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
119 120
    iIntros "HP". iApply own_inv_to_inv.
    iApply (own_inv_alloc N E with "HP").
Simon Spies's avatar
Simon Spies committed
121 122 123 124 125
  Qed.

  Lemma inv_alloc_open N E P :
    N  E  (|={E, E∖↑N}=> inv N P  (P ={E∖↑N, E}= True))%I.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
126 127
    iIntros (?). iMod own_inv_alloc_open as "[HI $]"; first done.
    iApply own_inv_to_inv. done.
Simon Spies's avatar
Simon Spies committed
128 129
  Qed.

Ralf Jung's avatar
Ralf Jung committed
130
  Lemma inv_acc E N P :
Simon Spies's avatar
Simon Spies committed
131 132
    N  E  inv N P ={E,E∖↑N}=  P  ( P ={E∖↑N,E}= True).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
133
    rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
Simon Spies's avatar
Simon Spies committed
134 135
  Qed.

Ralf Jung's avatar
Ralf Jung committed
136
  (** ** Proof mode integration *)
Simon Spies's avatar
Simon Spies committed
137 138 139 140 141 142 143 144 145 146 147
  Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.

  Global Instance into_acc_inv N P E:
    IntoAcc (X := unit) (inv N P)
            (N  E) True (fupd E (E  N)) (fupd (E  N) E)
            (λ _ : (), ( P)%I) (λ _ : (), ( P)%I) (λ _ : (), None).
  Proof.
    rewrite inv_eq /IntoAcc /accessor bi.exist_unit.
    iIntros (?) "#Hinv _". iApply "Hinv"; done.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
148
  (** ** Derived properties *)
Ralf Jung's avatar
Ralf Jung committed
149
  Lemma inv_acc_strong E N P :
Ralf Jung's avatar
Ralf Jung committed
150 151 152
    N  E  inv N P ={E,E∖↑N}=  P   E',  P ={E',N  E'}= True.
  Proof.
    iIntros (?) "Hinv".
Ralf Jung's avatar
Ralf Jung committed
153
    iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
Ralf Jung's avatar
Ralf Jung committed
154 155 156 157 158 159 160 161
    rewrite difference_diag_L.
    iPoseProof (fupd_mask_frame_r _ _ (E   N) with "H") as "H"; first set_solver.
    rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
    iIntros (E') "HP".
    iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
    by rewrite left_id_L.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
162
  Lemma inv_acc_timeless E N P `{!Timeless P} :
Simon Spies's avatar
Simon Spies committed
163 164
    N  E  inv N P ={E,E∖↑N}= P  (P ={E∖↑N,E}= True).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
165
    iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
Simon Spies's avatar
Simon Spies committed
166 167 168
    iIntros "!> {$HP} HP". iApply "Hclose"; auto.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
169
  Lemma inv_sep_l N P Q : inv N (P  Q) - inv N P.
Simon Spies's avatar
Simon Spies committed
170
  Proof.
Ralf Jung's avatar
Ralf Jung committed
171
    iIntros "#HI". iApply inv_alter; eauto.
Ralf Jung's avatar
Ralf Jung committed
172
    iIntros "!> !# [$ $] $".
Simon Spies's avatar
Simon Spies committed
173 174
  Qed.

Ralf Jung's avatar
Ralf Jung committed
175
  Lemma inv_sep_r N P Q : inv N (P  Q) - inv N Q.
Simon Spies's avatar
Simon Spies committed
176
  Proof.
Ralf Jung's avatar
Ralf Jung committed
177
    rewrite (comm _ P Q). eapply inv_sep_l.
Simon Spies's avatar
Simon Spies committed
178 179
  Qed.

Ralf Jung's avatar
Ralf Jung committed
180
  Lemma inv_sep N P Q : inv N (P  Q) - inv N P  inv N Q.
Simon Spies's avatar
Simon Spies committed
181 182
  Proof.
    iIntros "#H".
Ralf Jung's avatar
Ralf Jung committed
183 184
    iPoseProof (inv_sep_l with "H") as "$".
    iPoseProof (inv_sep_r with "H") as "$".
Simon Spies's avatar
Simon Spies committed
185
  Qed.
186

187
End inv.