basics.v 5.67 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
(** Testing basic connectives *)
2
From iris_c.vcgen Require Import vcg_solver.
3

Dan Frumin's avatar
Dan Frumin committed
4
Section test.
5 6
  Context `{amonadG Σ}.

Dan Frumin's avatar
Dan Frumin committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 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 96 97 98
  (** dereferencing *)
  Lemma test1 (l : cloc) (v: val) :
    l C v - AWP ∗ᶜ ♯ₗl {{ w, w = v  l C v }}.
  Proof.
    iIntros "Hl1". vcg_solver. auto.
  Qed.

  (** double dereferencing *)
  Lemma test2 (l1 l2 : cloc) (v: val) :
    l1 C cloc_to_val l2 - l2 C v -
    AWP ∗ᶜ ∗ᶜ ♯ₗl1 {{ v, v = #1  l1 C cloc_to_val l2 - l2 C v }}.
  Proof.
    iIntros "Hl1 Hl2". vcg_solver. auto.
  Qed.

  (** sequence points *)
  Lemma test3 (l : cloc) (v: val) :
    l C v - AWP ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗl {{ w, w = v  l C v }}.
  Proof.
    iIntros "Hl1". vcg_solver. auto.
  Qed.

  (** assignments *)
  Lemma test4 (l : cloc) (v1 v2: val) :
    l C v1 - AWP ♯ₗl = a_ret v2 {{ v, v = v2  l C[LLvl] v2 }}.
  Proof.
    iIntros "Hl1". vcg_solver. auto.
  Qed.

  Lemma store_load s l R :
    s C #0 - l C #1 -
    AWP ♯ₗs = ∗ᶜ ♯ₗl @ R {{ _, s C[LLvl] #1  l C #1 }}.
  Proof.
    iIntros "Hs Hl".
    vcg_solver. eauto with iFrame.
  Qed.

  Lemma store_load_load s1 s2 l R :
    s1 C #0 - l C #1 - s2 C #0 -
    AWP ♯ₗs1 = ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗs1 + 42 @ R {{ _, s1 C #1  l C #1 }}.
  Proof.
    iIntros "Hs1 Hl Hs2". vcg_solver. iModIntro.
    rewrite Qp_half_half. eauto with iFrame.
  Qed.


  (** double dereferencing & modification *)
  Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) :
    l1 C cloc_to_val l2 - l2 C v1 -
    r1 C cloc_to_val r2 - r2 C v2 -
    AWP ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1
    {{ w, w = v2 
      l1 C cloc_to_val r2  l2 C v1  r1 C cloc_to_val r2 - r2 C v2 }}.
  Proof.
    iIntros "**". vcg_solver. eauto 40.
  Qed.

  (** par *)
  Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
    l1 C v1 - l2 C v2 -
    AWP ∗ᶜ ♯ₗl1 |||  ∗ᶜ ♯ₗl2
    {{ w, w = (v1, v2)%V  l1 C v1  l2 C v2 }}.
  Proof.
    iIntros "**". vcg_solver. rewrite Qp_half_half. eauto with iFrame.
  Qed.

  Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
    l1 C v1 - l2 C v2 -
    AWP (♯ₗl1 = a_ret v2) |||  (♯ₗl2 = a_ret v1)
    {{ w, w = (v2, v1)%V  l1 C[LLvl] v2  l2 C[LLvl] v1 }}.
  Proof.
    iIntros "**". vcg_solver. eauto with iFrame.
  Qed.

  (** pre bin op *)
  Lemma test6 (l : cloc) (z0 : Z) R:
    l C #z0 -
    AWP ♯ₗl += 1 @ R {{ v, v = #z0  l C[LLvl] #(z0+1) }}.
  Proof.
    iIntros "Hl". vcg_solver. eauto.
  Qed.

  Lemma test7 (l k : cloc) (z0 z1 : Z) R:
    l C #z0 -
    k C #z1 -
    AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @
    R {{ v, v = #(z0+z1)  l C[LLvl] #(z0+1)  k C #z1 }}.
  Proof.
    iIntros "Hl Hk". vcg_solver. eauto with iFrame.
  Qed.

  (** more sequences *)
99
  Lemma test_seq s l :
Dan Frumin's avatar
Dan Frumin committed
100
    s C[ULvl] #0 - l C[ULvl] #1 -
101
    AWP (♯ₗl = 2 ; 1 + (♯ₗ l = 1)) + (♯ₗ s = 4)
Robbert Krebbers's avatar
Robbert Krebbers committed
102
    {{ v, v = #6  s C[LLvl] #4  l C[LLvl] #1 }}.
Dan Frumin's avatar
Dan Frumin committed
103 104
  Proof.
    iIntros "Hs Hl".
Dan Frumin's avatar
Dan Frumin committed
105
    vcg_solver. eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
106 107
  Qed.

108
  Lemma test_seq2 s l :
Dan Frumin's avatar
Dan Frumin committed
109
    s C[ULvl] #0 - l C[ULvl] #1 -
110
    AWP (♯ₗl = 2 ; ∗ᶜ ♯ₗl) + (♯ₗs = 4) {{ v, v = #6  s C[LLvl] #4  l C #2 }}.
Dan Frumin's avatar
Dan Frumin committed
111 112 113
  Proof.
    iIntros "Hs Hl".
    vcg_solver.
Dan Frumin's avatar
Dan Frumin committed
114
    rewrite Qp_half_half. eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
115 116
  Qed.

117
  Lemma test_seq3 l :
Dan Frumin's avatar
Dan Frumin committed
118
    l C #0 -
119
    AWP ♯ₗl = 2 ; 1 + (♯ₗl = 1) {{ _, l C[LLvl] #1 }}.
Dan Frumin's avatar
Dan Frumin committed
120
  Proof.
Dan Frumin's avatar
Dan Frumin committed
121
    iIntros "Hl". vcg_solver. iModIntro. eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
122 123
  Qed.

124
  Lemma test_seq4 l k :
Dan Frumin's avatar
Dan Frumin committed
125 126
    l C #0 -
    k C #0 -
127
    AWP (♯ₗl = 2 ; 1 + (♯ₗl = 1)) + (♯ₗk = 2 ; 1 + (♯ₗk = 1))
Robbert Krebbers's avatar
Robbert Krebbers committed
128
      {{ v, v = #4  l C[LLvl] #1  k C[LLvl] #1 }}.
Dan Frumin's avatar
Dan Frumin committed
129 130
  Proof.
    iIntros "Hl Hk".
Dan Frumin's avatar
Dan Frumin committed
131
    vcg_solver. iModIntro. by eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
132
  Qed.
133 134
  Definition stupid (l : cloc) : expr :=
    a_store (♯ₗ l) ( 1); a_ret #0.
Dan Frumin's avatar
Dan Frumin committed
135

136
  Lemma test_seq_fail l :
Dan Frumin's avatar
Dan Frumin committed
137
    l C[ULvl] #0 -
138 139
    AWP ((stupid l) + (stupid l)) + (a_ret #0) @
        True {{ v, l C #1 }}.
Dan Frumin's avatar
Dan Frumin committed
140
  Proof.
Dan Frumin's avatar
Dan Frumin committed
141
    iIntros "Hl". vcg_solver. Fail by eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
142 143
  Abort.

144
  Lemma test_seq5 l k :
Dan Frumin's avatar
Dan Frumin committed
145 146
    l C #0 -
    k C #0 -
147
    AWP 0 + (♯ₗl = 1 ; ♯ₗk = 2 ; 0) {{ v, v = #0  l C #1  k C #2 }}.
Dan Frumin's avatar
Dan Frumin committed
148
  Proof.
Dan Frumin's avatar
Dan Frumin committed
149
    iIntros "Hl Hk". vcg_solver.
Dan Frumin's avatar
Dan Frumin committed
150 151 152
    repeat iModIntro. by eauto with iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
153
  Lemma test_seq6 l k :
Dan Frumin's avatar
Dan Frumin committed
154 155
    l C #0 -
    k C #0 -
156
    AWP 1 + (♯ₗl = 1 ; (♯ₗk = 2) + ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗk + (♯ₗl = 2))
Robbert Krebbers's avatar
Robbert Krebbers committed
157
      {{ v, v = #5  l C[LLvl] #2  k C #2 }}.
Dan Frumin's avatar
Dan Frumin committed
158 159
  Proof.
    iIntros "Hl Hk". vcg_solver.
Dan Frumin's avatar
Dan Frumin committed
160
    repeat iModIntro. rewrite ?Qp_half_half.
Dan Frumin's avatar
Dan Frumin committed
161 162 163
    eauto with iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
164
  Lemma test_seq7 l :
Dan Frumin's avatar
Dan Frumin committed
165
    l C #0 -
166
    AWP 1 + (♯ₗl = 1 ; ∗ᶜ ♯ₗl + ∗ᶜ ♯ₗl ; ♯ₗl = 2) {{ v, v = #3  l C[LLvl] #2 }}.
Dan Frumin's avatar
Dan Frumin committed
167 168
  Proof.
    iIntros "Hl". vcg_solver.
Dan Frumin's avatar
Dan Frumin committed
169
    repeat iModIntro. rewrite ?Qp_half_half.
Dan Frumin's avatar
Dan Frumin committed
170 171 172
    eauto with iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
173
  (** while *)
174
  Lemma test_while l R :
175
    l C #1 -
176
    AWP while (∗ᶜ ♯ₗl < 2) { ♯ₗl = 1 } @ R {{ _, True }}.
177 178 179 180
  Proof.
    iIntros "Hl".
    iLöb as "IH".
    iApply a_while_spec'. iNext.
Dan Frumin's avatar
Dan Frumin committed
181
    vcg_solver. rewrite Qp_half_half. iIntros  "Hl".
182
    iLeft. iSplitR; eauto.
Dan Frumin's avatar
Dan Frumin committed
183
    vcg_solver. iIntros "Hl". iModIntro. by iApply "IH".
184
  Qed.
Dan Frumin's avatar
Dan Frumin committed
185
End test.