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

6
7
8
9
10
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.

Module sts.
Ralf Jung's avatar
Ralf Jung committed
11
12
13
14
(** This module is *not* meant to be imported. Instead, just use "sts.ctx" etc.
    like you would use "auth_ctx" etc. *)
Export algebra.sts.sts.

15
16
17
18
19
20
21
22
Record Sts {A B} := {
  st : relation A;
  tok    : A  set B;
}.
Arguments Sts : clear implicits.

Class InG Λ Σ (i : gid) {A B} (sts : Sts A B) := {
  inG :> ghost_ownership.InG Λ Σ i (stsRA sts.(st) sts.(tok));
23
  inh :> Inhabited A;
Ralf Jung's avatar
Ralf Jung committed
24
25
26
}.

Section definitions.
27
28
  Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ i sts} (γ : gname).
  Definition inv  (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
29
    ( s, own i γ (sts_auth sts.(st) sts.(tok) s )  φ s)%I.
30
  Definition states (S : set A) (T: set B) : iPropG Λ Σ :=
Ralf Jung's avatar
Ralf Jung committed
31
    ( closed sts.(st) sts.(tok) S T 
32
33
34
35
36
     own i γ (sts_frag sts.(st) sts.(tok) S T))%I.
  Definition state (s : A) (T: set B) : iPropG Λ Σ :=
    own i γ (sts_frag sts.(st) sts.(tok) (sts.up sts.(st) sts.(tok) s T) T).
  Definition ctx (N : namespace) (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
    invariants.inv N (inv φ).
Ralf Jung's avatar
Ralf Jung committed
37
End definitions.
38
39
40
Instance: Params (@inv) 8.
Instance: Params (@states) 8.
Instance: Params (@ctx) 9.
Ralf Jung's avatar
Ralf Jung committed
41
42

Section sts.
43
  Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ StsI sts}.
Ralf Jung's avatar
Ralf Jung committed
44
45
46
47
48
  Context (φ : A  iPropG Λ Σ).
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types γ : gname.

49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
  Lemma alloc N s :
    φ s  pvs N N ( γ, ctx StsI sts γ N φ  state StsI sts γ s (set_all  sts.(tok) s)).
  Proof.
    eapply sep_elim_True_r.
    { eapply (own_alloc StsI (sts_auth sts.(st) sts.(tok) s (set_all  sts.(tok) s)) N).
      apply discrete_valid=>/=. solve_elem_of. }
    rewrite pvs_frame_l. apply pvs_strip_pvs.
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
    transitivity ( inv StsI sts γ φ  state StsI sts γ s (set_all  sts.(tok) s))%I.
    { rewrite /inv -later_intro -(exist_intro s).
      rewrite [(_  φ _)%I]comm -assoc. apply sep_mono; first done.
      rewrite -own_op. apply equiv_spec, own_proper.
      split; first split; simpl.
      - intros; solve_elem_of-.
      - intros _. split_ands; first by solve_elem_of-.
Ralf Jung's avatar
Ralf Jung committed
64
        + apply closed_up. solve_elem_of-.
65
66
67
68
69
70
        + constructor; last solve_elem_of-. apply sts.elem_of_up. 
      - intros _. constructor. solve_elem_of-. }
    rewrite (inv_alloc N) /ctx pvs_frame_r. apply pvs_mono.
    by rewrite always_and_sep_l.
  Qed.

71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
  Lemma opened E γ S T :
    ( inv StsI sts γ φ  own StsI γ (sts_frag sts.(st) sts.(tok) S T))
       pvs E E ( s,  (s  S)   φ s  own StsI γ (sts_auth sts.(st) sts.(tok) s T)).
  Proof.
    rewrite /inv. rewrite later_exist sep_exist_r. apply exist_elim=>s.
    rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite -(exist_intro s).
    rewrite [(_  ▷φ _)%I]comm -!assoc -own_op -[(▷φ _  _)%I]comm.
    rewrite own_valid_l discrete_validI.
    rewrite -!assoc. apply const_elim_sep_l=>-[? [Hcl Hdisj]]. simpl in Hdisj, Hcl.
    inversion_clear Hdisj. rewrite const_equiv // left_id.
    rewrite comm. apply sep_mono; first done.
    apply equiv_spec, own_proper. split; first split; simpl.
    - intros Hdisj. split_ands; first by solve_elem_of-.
      + done.
      + constructor; [done | solve_elem_of-].
    - intros _. by eapply closed_disjoint.
    - intros _. constructor. solve_elem_of-.
  Qed.

  Lemma closing E γ s T s' S' T' :
    step sts.(st) sts.(tok) (s, T) (s', T')  s'  S'  closed sts.(st) sts.(tok) S' T' 
    ( φ s'  own StsI γ (sts_auth sts.(st) sts.(tok) s T))
     pvs E E ( inv StsI sts γ φ  own StsI γ (sts_frag sts.(st) sts.(tok) S' T')).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
96
97
98
99
100
101
102
103
104
105
106
107
108
109
    intros Hstep Hin Hcl. rewrite /inv -(exist_intro s').
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
    rewrite -pvs_frame_l. apply sep_mono; first done.
    rewrite -later_intro.
    transitivity (pvs E E (own StsI γ (sts_auth sts.(st) sts.(tok) s' T'))).
    { by apply own_update, sts_update. }
    apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
    split; first split; simpl.
    - intros _. by eapply closed_disjoint.
    - intros ?. split_ands; first by solve_elem_of-.
      + done.
      + constructor; [done | solve_elem_of-].
    - intros _. constructor. solve_elem_of-.
  Qed.
110

111
112
End sts.

Ralf Jung's avatar
Ralf Jung committed
113
End sts.