symbol_ghost.v 2.17 KB
Newer Older
1
From iris.algebra Require Import auth numbers.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
From iris.base_logic Require Import lib.own.
From iris.proofmode Require Export tactics.

Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
8
9
10
11
12
13
14
15
16
(** * Ghost theory for the [unsafe_symbol_adt] exercise *)
(** This file defines the ghost resources [counter] and [symbol] using Iris's
generic mechanism for ghost state. These resources satisfy the following laws:

<<
  counter_alloc:      |==> ∃ γ, counter γ n
  counter_exclusive:  counter γ n1 -∗ counter γ n2 -∗ False
  counter_inc:        counter γ n ==∗ counter γ (S n) ∗ symbol γ n
  symbol_obs:         counter γ n -∗ symbol γ s -∗ ⌜(s < n)%nat⌝
>>
*)

17
18
Class symbolG Σ := { symbol_inG :> inG Σ (authR max_natUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR max_natUR)].
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
21
22

Instance subG_symbolΣ {Σ} : subG symbolΣ Σ  symbolG Σ.
Proof. solve_inG. Qed.

23
Section symbol_ghost.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
  Context `{!symbolG Σ}.

26
27
  Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat n)).
  Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat (S n))).
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
33
34
35
36

  Global Instance counter_timeless γ n : Timeless (counter γ n).
  Proof. apply _. Qed.
  Global Instance symbol_timeless γ n : Timeless (symbol γ n).
  Proof. apply _. Qed.

  Global Instance symbol_persistent γ n : Persistent (symbol γ n).
  Proof. apply _. Qed.

37
  Lemma counter_alloc n :  |==>  γ, counter γ n.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  Proof.
39
    iMod (own_alloc ( (MaxNat n)   (MaxNat n))) as (γ) "[Hγ Hγf]";
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
      first by apply auth_both_valid.
    iExists γ. by iFrame.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
48
  Lemma counter_exclusive γ n1 n2 : counter γ n1 - counter γ n2 - False.
  Proof.
    apply bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
  Lemma counter_inc γ n : counter γ n == counter γ (S n)  symbol γ n.
  Proof.
    rewrite -own_op.
52
    apply own_update, auth_update_alloc, max_nat_local_update.
53
    simpl. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
57
58
  Qed.

  Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat.
  Proof.
    iIntros "Hc Hs".
59
    iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid.
60
    iPureIntro. simpl in *. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  Qed.
62
End symbol_ghost.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64

Typeclasses Opaque counter symbol.