sts.v 5.99 KB
Newer Older
1
From iris.program_logic Require Export invariants.
2
From iris.algebra Require Export sts.
3
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
4
5
Import uPred.

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

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

17
Section definitions.
18
19
20
  Context `{irisG Λ Σ, stsG Σ sts} (γ : gname).

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

29
30
31
32
33
34
  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.
35
  Global Instance sts_ownS_proper : Proper (() ==> () ==> ()) sts_ownS.
36
  Proof. solve_proper. Qed.
37
  Global Instance sts_own_proper s : Proper (() ==> ()) (sts_own s).
38
39
40
41
42
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_ne n N :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_proper N :
43
    Proper (pointwise_relation _ () ==> ()) (sts_ctx N).
44
  Proof. solve_proper. Qed.
45
  Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
46
  Proof. apply _. Qed.
Janno's avatar
Janno committed
47
48
49
50
  Global Instance sts_own_peristent s : PersistentP (sts_own s ).
  Proof. apply _. Qed.
  Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ).
  Proof. apply _. Qed.
51
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
52

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

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

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
95
96
  Lemma sts_accS E γ S T :
     sts_inv γ φ  sts_ownS γ S T ={E}=>  s,
97
       (s  S)   φ s   s' T',
Ralf Jung's avatar
Ralf Jung committed
98
       sts.steps (s, T) (s', T')   φ s' ={E}=  sts_inv γ φ  sts_own γ s' T'.
99
  Proof.
Ralf Jung's avatar
Ralf Jung committed
100
101
    iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
    iDestruct "Hinv" as (s) "[>Hγ Hφ]".
102
    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
103
104
    assert (s  S) by eauto using sts_auth_frag_valid_inv.
    assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
105
106
107
108
109
    rewrite sts_op_auth_frag //.
    iVsIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
    iIntros (s' T') "[% Hφ]".
    iVs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
Ralf Jung's avatar
Ralf Jung committed
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
    iVsIntro. iNext. iExists s'; by iFrame.
  Qed.

  Lemma sts_acc E γ s0 T :
     sts_inv γ φ  sts_own γ s0 T ={E}=>  s,
       sts.frame_steps T s0 s   φ s   s' T',
       sts.steps (s, T) (s', T')   φ s' ={E}=  sts_inv γ φ  sts_own γ s' T'.
  Proof. by apply sts_accS. Qed.
    
  Lemma sts_openS E N γ S T :
    nclose N  E 
    sts_ctx γ N φ  sts_ownS γ S T ={E,EN}=>  s,
       (s  S)   φ s   s' T',
       sts.steps (s, T) (s', T')   φ s' ={EN,E}= sts_own γ s' T'.
  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". *)
    iVs (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
    iVsIntro. iExists s. iFrame. iIntros (s' T') "H".
134
    iVs ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
135
136
  Qed.

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