atomic.v 3.98 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.program_logic Require Export atomic.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.heap_lang Require Import proofmode notation atomic_heap.
4
5
Set Default Proof Using "Type".

6
7
Unset Mangle Names.

Ralf Jung's avatar
Ralf Jung committed
8
9
10
11
12
13
14
15
16
17
18
19
20
Section tests.
  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
  Import atomic_heap.notation.

  (* FIXME: removing the `val` type annotation breaks printing. *)
  Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
    Q - l  v - WP !#l {{ _, Q }}.
  Proof.
    iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
    iAaccIntro with "Hl"; eauto with iFrame.
  Qed.
End tests.

21
22
23
24
25
26
27
28
29
30
31
32
33
(* Test if we get reasonable error messages with non-laterable assertions in the context. *)
Section error.
  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
  Import atomic_heap.notation.

  Check "non_laterable".
  Lemma non_laterable (P : iProp Σ) (l : loc) :
    P - WP !#l {{ _, True }}.
  Proof.
    iIntros "HP". wp_apply load_spec. Fail iAuIntro.
  Restart.
    iIntros "HP". Fail awp_apply load_spec.
  Abort.
Ralf Jung's avatar
Ralf Jung committed
34
End error.
35
36


37
(* Test if AWP and the AU obtained from AWP print. *)
38
Check "printing".
39
40
41
42
43
44
Section printing.
  Context `{!heapG Σ}.

  Definition code : expr := #().

  Lemma print_both_quant (P : val  iProp Σ) :
Gregory Malecha's avatar
Gregory Malecha committed
45
     <<<  x, P x >>> code @  <<<  y, P y, RET #() >>>.
46
  Proof.
47
    Show. iIntros (Φ) "AU". Show.
48
49
50
51
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Lemma print_first_quant l :
Gregory Malecha's avatar
Gregory Malecha committed
52
     <<<  x, l  x >>> code @  <<< l  x, RET #() >>>.
53
  Proof.
54
    Show. iIntros (Φ) "AU". Show.
55
56
57
58
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Lemma print_second_quant l :
Gregory Malecha's avatar
Gregory Malecha committed
59
     <<< l  #() >>> code @  <<<  y, l  y, RET #() >>>.
60
  Proof.
61
    Show. iIntros (Φ) "AU". Show.
62
63
64
65
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Lemma print_no_quant l :
Gregory Malecha's avatar
Gregory Malecha committed
66
     <<< l  #() >>> code @  <<< l  #(), RET #() >>>.
67
  Proof.
68
    Show. iIntros (Φ) "AU". Show.
69
70
71
72
73
74
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Check "Now come the long pre/post tests".

  Lemma print_both_quant_long l :
Gregory Malecha's avatar
Gregory Malecha committed
75
     <<<  x, l  x  l  x >>> code @  <<<  y, l  y, RET #() >>>.
76
  Proof.
77
    Show. iIntros (Φ) "AU". Show.
78
79
80
  Abort.

  Lemma print_both_quant_longpre l :
Gregory Malecha's avatar
Gregory Malecha committed
81
     <<<  x, l  x  l  x  l  x  l  x  l  x  l  x >>> code @  <<<  y, l  y, RET #() >>>.
82
  Proof.
83
    Show. iIntros (Φ) "AU". Show.
84
85
86
  Abort.

  Lemma print_both_quant_longpost l :
Gregory Malecha's avatar
Gregory Malecha committed
87
     <<<  xx, l  xx  l  xx  l  xx >>> code @  <<<  yyyy, l  yyyy  l  xx  l  xx  l  xx  l  xx  l  xx, RET #() >>>.
88
  Proof.
89
    Show. iIntros (Φ) "?". Show.
90
91
92
  Abort.

  Lemma print_first_quant_long l :
Gregory Malecha's avatar
Gregory Malecha committed
93
     <<<  x, l  x  l  x  l  x  l  x >>> code @  <<< l  x, RET #() >>>.
94
  Proof.
95
    Show. iIntros (Φ) "AU". Show.
96
97
98
  Abort.

  Lemma print_second_quant_long l x :
Gregory Malecha's avatar
Gregory Malecha committed
99
     <<< l  x  l  x  l  x  l  x  l  x  l  x >>> code @  <<<  y, l  y, RET #() >>>.
100
  Proof.
101
    Show. iIntros (Φ) "AU". Show.
102
103
104
  Abort.

  Lemma print_no_quant_long l x :
Gregory Malecha's avatar
Gregory Malecha committed
105
     <<< l  x  l  x  l  x  l  x  l  x  l  x >>> code @  <<< l  #(), RET #() >>>.
106
  Proof.
107
    Show. iIntros (Φ) "AU". Show.
108
109
110
  Abort.

  Lemma print_no_quant_longpre l xx yyyy :
Gregory Malecha's avatar
Gregory Malecha committed
111
     <<< l  xx  l  xx  l  xx  l  xx  l  xx  l  xx  l  xx >>> code @  <<< l  yyyy, RET #() >>>.
112
  Proof.
113
    Show. iIntros (Φ) "AU". Show.
114
115
116
  Abort.

  Lemma print_no_quant_longpost l xx yyyy :
Gregory Malecha's avatar
Gregory Malecha committed
117
     <<< l  xx  l  xx  l  xx >>> code @  <<< l  yyyy  l  xx  l  xx  l  xx  l  xx  l  xx  l  xx, RET #() >>>.
118
  Proof.
119
    Show. iIntros (Φ) "AU". Show.
120
121
  Abort.

Ralf Jung's avatar
Ralf Jung committed
122
123
124
  Check "Prettification".

  Lemma iMod_prettify (P : val  iProp Σ) :
Gregory Malecha's avatar
Gregory Malecha committed
125
     <<<  x, P x >>> !#0 @  <<<  y, P y, RET #() >>>.
Ralf Jung's avatar
Ralf Jung committed
126
127
128
129
  Proof.
    iIntros (Φ) "AU". iMod "AU". Show.
  Abort.

130
End printing.