sts.v 6.11 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2
From iris.algebra Require Export sts.
3
From iris.proofmode Require Import tactics.
4
Set Default Proof Using "Type*".
Ralf Jung's avatar
Ralf Jung committed
5 6
Import uPred.

7
(** The CMRA we need. *)
8 9
Class stsG Σ (sts : stsT) := StsG {
  sts_inG :> inG Σ (stsR sts);
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  sts_inhabited :> Inhabited (sts.state sts);
Ralf Jung's avatar
Ralf Jung committed
11
}.
12
Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (constRF (stsR sts)) ].
13

14 15 16
Instance subG_stsΣ Σ sts :
  subG (stsΣ sts) Σ  Inhabited (sts.state sts)  stsG Σ sts.
Proof. intros ?%subG_inG ?. by split. Qed.
17

18
Section definitions.
19
  Context `{stsG Σ sts} (γ : gname).
20 21

  Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
22
    own γ (sts_frag S T).
23
  Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iProp Σ :=
24
    own γ (sts_frag_up s T).
25
  Definition sts_inv (φ : sts.state sts  iProp Σ) : iProp Σ :=
26
    ( s, own γ (sts_auth s )  φ s)%I.
27
  Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts  iProp Σ) : iProp Σ :=
28
    inv N (sts_inv φ).
Ralf Jung's avatar
Ralf Jung committed
29

30 31 32 33 34 35
  Global Instance sts_inv_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) sts_inv.
  Proof. solve_proper. Qed.
  Global Instance sts_inv_proper :
    Proper (pointwise_relation _ () ==> ()) sts_inv.
  Proof. solve_proper. Qed.
36
  Global Instance sts_ownS_proper : Proper (() ==> () ==> (⊣⊢)) sts_ownS.
37
  Proof. solve_proper. Qed.
38
  Global Instance sts_own_proper s : Proper (() ==> (⊣⊢)) (sts_own s).
39
  Proof. solve_proper. Qed.
40
  Global Instance sts_ctx_ne `{!invG Σ} n N :
41 42
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
  Proof. solve_proper. Qed.
43
  Global Instance sts_ctx_proper `{!invG Σ} N :
44
    Proper (pointwise_relation _ () ==> (⊣⊢)) (sts_ctx N).
45
  Proof. solve_proper. Qed.
46
  Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
47
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
  Global Instance sts_own_persistent s : PersistentP (sts_own s ).
49
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ).
51
  Proof. apply _. Qed.
52
End definitions.
53

Ralf Jung's avatar
Ralf Jung committed
54
Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
55 56 57
Instance: Params (@sts_inv) 4.
Instance: Params (@sts_ownS) 4.
Instance: Params (@sts_own) 5.
58
Instance: Params (@sts_ctx) 6.
Ralf Jung's avatar
Ralf Jung committed
59 60

Section sts.
61 62
  Context `{invG Σ, stsG Σ sts}.
  Implicit Types φ : sts.state sts  iProp Σ.
Ralf Jung's avatar
Ralf Jung committed
63
  Implicit Types N : namespace.
64
  Implicit Types P Q R : iProp Σ.
Ralf Jung's avatar
Ralf Jung committed
65
  Implicit Types γ : gname.
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

69 70
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
71
  Lemma sts_ownS_weaken γ S1 S2 T1 T2 :
72
    T2  T1  S1  S2  sts.closed S2 T2 
73
    sts_ownS γ S1 T1 == sts_ownS γ S2 T2.
74
  Proof. intros ???. by apply own_update, sts_update_frag. Qed.
75

76
  Lemma sts_own_weaken γ s S T1 T2 :
77
    T2  T1  s  S  sts.closed S T2 
78
    sts_own γ s T1 == sts_ownS γ S T2.
79
  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
80

Ralf Jung's avatar
Ralf Jung committed
81
  Lemma sts_ownS_op γ S1 S2 T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
82
    T1  T2  sts.closed S1 T1  sts.closed S2 T2 
83
    sts_ownS γ (S1  S2) (T1  T2) ⊣⊢ (sts_ownS γ S1 T1  sts_ownS γ S2 T2).
84
  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
Ralf Jung's avatar
Ralf Jung committed
85

86
  Lemma sts_alloc φ E N s :
87
     φ s ={E}=  γ, sts_ctx γ N φ  sts_own γ s (  sts.tok s).
88
  Proof.
89
    iIntros "Hφ". rewrite /sts_ctx /sts_own.
90
    iMod (own_alloc (sts_auth s (  sts.tok s))) as (γ) "Hγ".
91 92
    { apply sts_auth_valid; set_solver. }
    iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
93
    iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
Ralf Jung's avatar
Ralf Jung committed
94
    rewrite /sts_inv. iNext. iExists s. by iFrame.
Ralf Jung's avatar
Ralf Jung committed
95
  Qed.
96

97
  Lemma sts_accS φ E γ S T :
98
     sts_inv γ φ  sts_ownS γ S T ={E}=  s,
99 100
      s  S   φ s   s' T',
      sts.steps (s, T) (s', T')   φ s' ={E}=  sts_inv γ φ  sts_own γ s' T'.
101
  Proof.
Ralf Jung's avatar
Ralf Jung committed
102 103
    iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
    iDestruct "Hinv" as (s) "[>Hγ Hφ]".
104
    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
105 106
    assert (s  S) by eauto using sts_auth_frag_valid_inv.
    assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
107
    rewrite sts_op_auth_frag //.
108
    iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
109
    iIntros (s' T') "[% Hφ]".
110
    iMod (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
111
    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
112
    iModIntro. iNext. iExists s'; by iFrame.
Ralf Jung's avatar
Ralf Jung committed
113 114
  Qed.

115
  Lemma sts_acc φ E γ s0 T :
116
     sts_inv γ φ  sts_own γ s0 T ={E}=  s,
117 118
      sts.frame_steps T s0 s   φ s   s' T',
      sts.steps (s, T) (s', T')   φ s' ={E}=  sts_inv γ φ  sts_own γ s' T'.
Ralf Jung's avatar
Ralf Jung committed
119
  Proof. by apply sts_accS. Qed.
120

121
  Lemma sts_openS φ E N γ S T :
122 123
    N  E 
    sts_ctx γ N φ  sts_ownS γ S T ={E,E∖↑N}=  s,
124
      s  S   φ s   s' T',
125
      sts.steps (s, T) (s', T')   φ s' ={E∖↑N,E}= sts_own γ s' T'.
Ralf Jung's avatar
Ralf Jung committed
126 127 128 129 130 131 132 133
  Proof.
    iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
    (* The following is essentially a very trivial composition of the accessors
       [sts_acc] and [inv_open] -- but since we don't have any good support
       for that currently, this gets more tedious than it should, with us having
       to unpack and repack various proofs.
       TODO: Make this mostly automatic, by supporting "opening accessors
       around accessors". *)
134 135 136
    iMod (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
    iModIntro. iExists s. iFrame. iIntros (s' T') "H".
    iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
137 138
  Qed.

139
  Lemma sts_open φ E N γ s0 T :
140 141
    N  E 
    sts_ctx γ N φ  sts_own γ s0 T ={E,E∖↑N}=  s,
142
      sts.frame_steps T s0 s   φ s   s' T',
143
      sts.steps (s, T) (s', T')   φ s' ={E∖↑N,E}= sts_own γ s' T'.
144
  Proof. by apply sts_openS. Qed.
Ralf Jung's avatar
Ralf Jung committed
145
End sts.