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

6
(** The CMRA we need. *)
7
Class stsG Λ Σ (sts : stsT) := StsG {
8
  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
Coercion sts_inG : stsG >-> inG.
12
(** The Functor we need. *)
13
Definition stsGF (sts : stsT) : gFunctor := GFunctor (constRF (stsR sts)).
14
(* Show and register that they match. *)
15
Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
16 17
  `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
Proof. split; try apply _. apply: inGF_inG. Qed.
18

19 20 21 22 23 24 25 26 27 28
Section definitions.
  Context `{i : stsG Λ Σ sts} (γ : gname).
  Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
    own γ (sts_frag S T).
  Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
    own γ (sts_frag_up s T).
  Definition sts_inv (φ : sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    ( s, own γ (sts_auth s )  φ s)%I.
  Definition sts_ctx (N : namespace) (φ: sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    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 40 41 42 43
  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 :
44
    Proper (pointwise_relation _ () ==> ()) (sts_ctx N).
45
  Proof. solve_proper. Qed.
46
  Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
47 48
  Proof. apply _. Qed.
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
49

50
Typeclasses Opaque sts_own sts_ownS sts_ctx.
51 52 53 54
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
55 56

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

64 65
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Ralf Jung's avatar
Ralf Jung committed
66
  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
67
    T2  T1  S1  S2  sts.closed S2 T2 
68
    sts_ownS γ S1 T1 ={E}=> sts_ownS γ S2 T2.
69
  Proof. intros ???. by apply own_update, sts_update_frag. Qed.
70

Ralf Jung's avatar
Ralf Jung committed
71
  Lemma sts_own_weaken E γ s S T1 T2 :
72
    T2  T1  s  S  sts.closed S T2 
73
    sts_own γ s T1 ={E}=> sts_ownS γ S T2.
74
  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
75

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

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

93 94
  Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.

95
  Lemma sts_fsaS E N (Ψ : V  iPropG Λ Σ) γ S T :
Ralf Jung's avatar
Ralf Jung committed
96
    fsaV  nclose N  E 
97
    sts_ctx γ N φ  sts_ownS γ S T  ( s,
98 99 100 101
       (s  S)   φ s -
      fsa (E  nclose N) (λ x,  s' T',
         sts.steps (s, T) (s', T')   φ s'  (sts_own γ s' T' - Ψ x)))
     fsa E Ψ.
102
  Proof.
103 104
    iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
    iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ".
105
    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
106 107 108 109 110
    assert (s  S) by eauto using sts_auth_frag_valid_inv.
    assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
    iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
    { iApply "HΨ"; by iSplit. }
111
    iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)".
112 113 114
    iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
    iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
115
    iNext; iExists s'; by iFrame.
116 117
  Qed.

118
  Lemma sts_fsa E N (Ψ : V  iPropG Λ Σ) γ s0 T :
Ralf Jung's avatar
Ralf Jung committed
119
    fsaV  nclose N  E 
120
    sts_ctx γ N φ  sts_own γ s0 T  ( s,
121 122 123 124 125
       (s  sts.up s0 T)   φ s -
      fsa (E  nclose N) (λ x,  s' T',
         (sts.steps (s, T) (s', T'))   φ s' 
        (sts_own γ s' T' - Ψ x)))
     fsa E Ψ.
126
  Proof. by apply sts_fsaS. Qed.
Ralf Jung's avatar
Ralf Jung committed
127
End sts.