sts.v 5.8 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 47
  Proof. apply _. Qed.
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

Ralf Jung's avatar
Ralf Jung committed
49
Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
50 51 52 53
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
54 55

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

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

70
  Lemma sts_own_weaken γ s S T1 T2 :
71
    T2  T1  s  S  sts.closed S T2 
72
    sts_own γ s T1 =r=> sts_ownS γ S T2.
73
  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
74

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

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

Ralf Jung's avatar
Ralf Jung committed
91 92
  Lemma sts_accS E γ S T :
     sts_inv γ φ  sts_ownS γ S T ={E}=>  s,
93
       (s  S)   φ s   s' T',
Ralf Jung's avatar
Ralf Jung committed
94
       sts.steps (s, T) (s', T')   φ s' ={E}=  sts_inv γ φ  sts_own γ s' T'.
95
  Proof.
Ralf Jung's avatar
Ralf Jung committed
96 97
    iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
    iDestruct "Hinv" as (s) "[>Hγ Hφ]".
98
    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
99 100
    assert (s  S) by eauto using sts_auth_frag_valid_inv.
    assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
101 102 103 104 105
    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
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
    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".
130
    iVs ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
131 132
  Qed.

133 134 135
  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
136
       (sts.frame_steps T s0 s)   φ s   s' T',
137 138
       (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
139
End sts.