translation.v 17.7 KB
Newer Older
1
From iris.heap_lang Require Export proofmode notation.
2
From iris.heap_lang Require Import assert par.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.algebra Require Import frac auth.
4 5 6
From iris_c.lib Require Import mset flock list.
From iris_c.lib Require Export locking_heap U.
From iris_c.c_translation Require Export monad.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
From iris_c.c_translation Require Import proofmode.
8

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10
Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
11
Notation "♯ₗ l" := (a_ret (cloc_to_val l)) (at level 8, format "♯ₗ l") : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
12

13 14 15 16 17 18
Definition a_alloc : val := λ: "x1" "x2",
  "vv" ←ᶜ "x1" ||| "x2" ;;
  let: "n" := Fst "vv" in
  let: "v" := Snd "vv" in
  a_atomic_env (λ: <>, (ref (lreplicate "n" "v"), #0)).
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
19 20

Definition a_store : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
  "vv" ←ᶜ "x1" ||| "x2" ;;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26 27 28 29
    let: "l" := Fst (Fst "vv") in
    let: "i" := Snd (Fst "vv") in
    let: "v" := Snd "vv" in
    mset_add ("l", "i") "env" ;;
    let: "ll" := !"l" in
    "l" <- linsert "i" "v" "ll" ;;
    "v"
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31
  ).
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
32 33

Definition a_load : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40
    let: "l" := Fst "v" in
    let: "i" := Snd "v" in
    assert: (mset_member ("l", "i") "env" = #false);;
    let: "ll" := !"l" in
    llookup "i" "ll"
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43
  ).
Notation "∗ᶜ e" :=
  (a_load e)%E (at level 9, right associativity) : expr_scope.
44 45

Definition a_un_op (op : un_op) : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47
  "v" ←ᶜ "x" ;;
  a_ret (UnOp op "v").
48

Dan Frumin's avatar
Dan Frumin committed
49 50 51 52
(*Definition a_pre_un_op (op : un_op) : val := λ: "x",
  "l" ←ᶜ "x" ;;ᶜ
  a_atomic (λ: <>, a_store (a_ret "l") (a_un_op op (∗ᶜ (a_ret "l")))).*)

53
Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57 58 59 60 61 62 63
  "vv" ←ᶜ "x1" ||| "x2" ;;
  a_ret (BinOp op (Fst "vv") (Snd "vv")).
Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
64

Dan Frumin's avatar
Dan Frumin committed
65 66
Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y",
  "lv" ←ᶜ ("x" ||| "y");;
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69
  a_atomic (λ: <>,
    "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
    a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
Dan Frumin's avatar
Dan Frumin committed
70 71 72
    a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.

73 74
(* M () *)
(* The eta expansion is used to turn it into a value *)
75 76
Definition a_seq : val := λ: <>,
  a_atomic_env (λ: "env", mset_clear "env").
Dan Frumin's avatar
Dan Frumin committed
77

Robbert Krebbers's avatar
Nits.  
Robbert Krebbers committed
78
Definition a_seq_bind : val := λ: "f" "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81 82 83 84 85
  "a" ←ᶜ "x" ;;
  a_seq #() ;;
  "f" "a".
Notation "e1 ;ᶜ e2" :=
  (a_seq_bind (λ: <>, e2) e1)%E
  (at level 100, e2 at level 200,
   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
86 87

Definition a_if : val := λ: "cnd" "e1" "e2",
Robbert Krebbers's avatar
Robbert Krebbers committed
88 89 90 91 92 93
  "c" ←ᶜ "cnd" ;;
  if: "c" then "e1" #() else "e2" #().
Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" :=
  (a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E)
  (at level 200, e1, e2, e3 at level 200,
   format "'ifᶜ'  ( e1 )  {  e2  }  'elseᶜ'  {  e3  }") : expr_scope.
94

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
95 96
Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99 100
    a_if ("cnd" #()) (λ: <>, "bdy" #() ; "while" "cnd" "bdy") a_seq%E.
Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
  (at level 200, e1, e2 at level 200,
   format "'whileᶜ'  ( e1 )  {  e2  }") : expr_scope.
101

Dan Frumin's avatar
Dan Frumin committed
102 103 104
Definition a_invoke: val := λ: "f" "arg",
  a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".

Dan Frumin's avatar
Dan Frumin committed
105
Section proofs.
106
  Context `{amonadG Σ}.
Dan Frumin's avatar
Dan Frumin committed
107

108 109 110 111 112 113 114
  Lemma a_alloc_spec R Φ Ψ1 Ψ2 e1 e2 :
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  n : nat,
                 v1 = #n  
                 l, (l,O) C replicate n v2 - Φ (cloc_to_val (l,O))) -
    AWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
115
  Proof.
116 117 118 119 120 121
    iIntros "H1 H2 HΦ".
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
    iApply awp_bind. iApply (awp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
    iDestruct ("HΦ" with "H1 H2") as (n ->) "HΦ".
Dan Frumin's avatar
Dan Frumin committed
122
    iApply awp_atomic_env.
123 124 125 126 127 128 129 130
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
    iApply wp_fupd. wp_alloc l as "Hl".
    iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
    iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply "HΦ"].
    iExists X, _. iFrame.
    iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
    exists cl; split; first done. by rewrite locked_locs_alloc_heap.
Dan Frumin's avatar
Dan Frumin committed
131
  Qed.
132

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
133
  Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
134 135
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ Ψ2 }} -
136 137
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  cl w,
                 v1 = cloc_to_val cl   cl C w  (cl C[LLvl] v2 - Φ v2)) -
138
    AWP e1 = e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
139
  Proof.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
140
    iIntros "H1 H2 HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
    iApply awp_bind. iApply (awp_par with "H1 H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
145
    iDestruct ("HΦ" with "H1 H2") as ([l i] w ->) "[Hl HΦ]".
Dan Frumin's avatar
Dan Frumin committed
146
    iApply awp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1.
149 150 151
    assert ((#l, #i)%V  X).
    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
    iMod (locking_heap_store with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
153 154
    wp_apply (mset_add_spec with "[$]"); first done.
    iIntros "Hlocks /="; wp_seq.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158 159 160
    wp_load; wp_let.
    wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
    iApply wp_fupd. wp_store.
    iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
    iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists ({[(#l, #i)%V]}  X), _. iFrame "Hσ". rewrite locked_locs_lock.
161 162 163
    iIntros "{$Hlocks} !%".
    intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
    eexists; split; [apply (cloc_of_to_val (l,i))|set_solver].
Dan Frumin's avatar
Dan Frumin committed
164 165
  Qed.

166
  Lemma a_load_spec_exists_frac R Φ e :
167 168
    AWP e @ R {{ v,  cl q w,  v = cloc_to_val cl  
                              cl C{q} w  (cl C{q} w - Φ w) }} -
169
    AWP ∗ᶜe @ R {{ Φ }}.
170
  Proof.
171 172
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
174
    iIntros (v). iDestruct 1 as ([l i] q w ->) "[Hl HΦ]". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176 177
    iApply awp_atomic_env. iIntros (env) "Henv HR".
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv.
178 179 180
    assert ((#l, #i)%V  X).
    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
    iMod (locking_heap_load with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
181 182
    wp_let. wp_proj; wp_let. wp_proj; wp_let.
    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
183
    rewrite bool_decide_false //.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185 186 187 188
    wp_op. iSplit; first done. iNext; wp_seq.
    wp_load; wp_let. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists X, _. by iFrame.
189 190
  Qed.

191
  Lemma a_load_spec R Φ q e :
192 193 194
    AWP e @ R {{ v,  cl w,
                     v = cloc_to_val cl  
                    cl C{q} w  (cl C{q} w - Φ w) }} -
195
    AWP ∗ᶜe @ R {{ Φ }}.
196
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    iIntros "H". iApply a_load_spec_exists_frac.
198
    awp_apply (awp_wand with "H").
199
    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
200 201 202
  Qed.

  Lemma a_un_op_spec R Φ e op:
203
    AWP e @ R {{ v,  w : val, un_op_eval op v = Some w  Φ w }} -
Dan Frumin's avatar
Dan Frumin committed
204
    AWP a_un_op op e @ R {{ Φ }}.
205 206 207 208 209 210 211 212 213
  Proof.
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam.
    iApply awp_bind.
    iApply (awp_wand with "HΦ"); iIntros (w) "HΦ"; awp_lam.
    iDestruct "HΦ" as (w0) "[% H]".
    iApply awp_ret. by wp_op.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
  (*
  Lemma a_pre_un_op_spec R Φ e op :
    AWP e @ R {{ vl, R -∗ ∃ l v w, l ↦C v ∗ ⌜vl = #l⌝
                        ∗ ⌜un_op_eval op v = Some w⌝
                        ∗ (l ↦C[LLvl] w -∗ R ∗ Φ w) }} -∗
    AWP a_pre_un_op op e @ R {{ Φ }}.
  Proof.
    iIntros "He". rewrite /a_pre_un_op.
    awp_apply (a_wp_awp with "He"); iIntros (?) "HΦ"; awp_lam.
    iApply awp_bind. iApply (awp_wand with "HΦ").
    iIntros (vl) "H". awp_lam.
    iApply awp_atomic. iNext.
    iIntros "R". iDestruct ("H" with "R") as (l v w) "(Hl & % & % & HΦ)".
    simplify_eq/=.
    iExists True%I. rewrite left_id. awp_lam.
    iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I
                             (λ v', ⌜v' = w⌝ ∗ l ↦C v)%I
              with "[] [Hl] [-]").
    - iApply awp_ret. by wp_value_head.
    - iApply a_un_op_spec. iApply a_load_spec.
      iApply awp_ret. wp_value_head.
      iExists _,_; iFrame. iSplit; eauto.
    - iNext. iIntros (? ? ->) "[% Hl]". simplify_eq/=.
      iExists _,_; iFrame. iSplit; eauto.
      iIntros "? _". by iApply "HΦ".
  Qed.
  *)

242
  Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
243
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
244
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, bin_op_eval op v1 v2 = Some w  Φ w) -
Dan Frumin's avatar
Dan Frumin committed
245
    AWP a_bin_op op e1 e2 @ R {{ Φ }}.
246 247 248 249 250
  Proof.
    iIntros "H1 H2 HΦ".
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
    iApply awp_bind.
251
    iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
252 253 254 255 256 257
    iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
    iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
    iSpecialize ("HΦ" with "HΨ1 HΨ2").
    iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
258 259 260
  Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 - R -
261 262 263 264
         cl v w,  v1 = cloc_to_val cl  
                  cl C v 
                   bin_op_eval op v v2 = Some w  
                  (cl C[LLvl] w - R  Φ v)) -
Dan Frumin's avatar
Dan Frumin committed
265 266 267 268 269 270
    AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
Dan Frumin's avatar
Dan Frumin committed
272
    iApply awp_atomic. iNext.
273
    iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
Dan Frumin's avatar
Dan Frumin committed
274 275
    simplify_eq/=. iExists True%I. rewrite left_id. awp_lam.
    iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head.
276
    iExists cl, v; iFrame. iSplit; first done.
Dan Frumin's avatar
Dan Frumin committed
277
    iIntros "Hl". awp_let. iApply awp_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
    iApply (a_store_spec _ _
279
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
Dan Frumin's avatar
Dan Frumin committed
280
    - awp_proj. iApply awp_ret; by wp_value_head.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
    - iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
Dan Frumin's avatar
Dan Frumin committed
282 283 284
        try (try awp_proj; iApply awp_ret; by wp_value_head).
      iNext. iIntros (? ? -> ->). eauto.
    - iNext. iIntros (? ? -> ->).
285 286
      iExists _, _; iFrame. iSplit; first done.
      iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
Dan Frumin's avatar
Dan Frumin committed
287 288 289
      iIntros "_". by iApply "HΦ".
  Qed.

290 291
  Lemma a_seq_spec R Φ :
    U (Φ #()) -
292
    AWP (a_seq #()) @ R {{ Φ }}.
293 294
  Proof.
    iIntros "HΦ". rewrite /a_seq. awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
295 296 297
    iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
    iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
    wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
298
    iDestruct "HΦ" as (us) "[Hus HΦ]".
Dan Frumin's avatar
Dan Frumin committed
299
    iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
300 301
    - iModIntro. iSplitR "HΦ".
      + iExists , σ. by iFrame.
302 303
      + by iApply "HΦ".
    - iDestruct "Hus" as "[Hu Hus]".
Dan Frumin's avatar
Dan Frumin committed
304 305
      iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz].
      iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
306 307
      iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks").
      iIntros "Hus". iApply "HΦ". by iFrame.
308 309 310 311
  Qed.

  Lemma a_sequence_spec R Φ (f e : expr) :
    AsVal f 
312 313
     AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -
    AWP a_seq_bind f e @ R {{ Φ }}.
314
  Proof.
315
    iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
316 317 318 319 320 321
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
    iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
    awp_lam. iApply awp_bind. iApply a_seq_spec.
    iModIntro. by awp_lam.
  Qed.

322 323
  Lemma a_sequence_spec' R Φ (e e' : expr) :
    Closed [] e' 
324 325
     AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -
    AWP a_seq_bind (λ: <>, e') e @ R {{ Φ }}.
326 327 328 329 330 331 332
  Proof.
    iIntros (?) "He".
    iApply a_sequence_spec.
    iApply (awp_wand with "He"). iNext.
    iIntros (?) "He'". iModIntro. by awp_lam.
  Qed.

333
  Lemma a_while_spec  R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
Robbert Krebbers's avatar
Robbert Krebbers committed
334 335
     AWP a_if c (λ: <>, (λ: <>, b) #() ; while (c) { b }) a_seq @ R {{ Φ }} -
    AWP while (c) { b } @ R {{ Φ }}.
336 337 338 339 340 341 342
  Proof.
    iIntros "H".
    awp_lam. awp_lam. awp_seq.
    iApply "H".
  Qed.

  Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
Robbert Krebbers's avatar
Robbert Krebbers committed
343 344
    AsVal e1 
    AsVal e2 
345 346 347
    AWP e @ R {{ v, (v = #true  AWP e1 #() @ R {{ Φ }}) 
                    (v = #false  AWP e2 #() @ R {{ Φ }}) }} -
    AWP a_if e e1 e2 @ R {{ Φ }}.
348
  Proof.
349
    iIntros ([v1 <-] [v2 <-]) "H".
350 351 352 353 354
    awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
    iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
  Qed.

355
  Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
356 357 358
    AWP e @ R {{ v, (v = #true  AWP e1 @ R {{ Φ }}) 
                    (v = #false  AWP e2 @ R {{ Φ }}) }} -
    AWP if (e) { e1 } else { e2 } @ R {{ Φ }}.
359 360 361 362 363 364 365
  Proof.
    iIntros "He". iApply a_if_spec.
    iApply (awp_wand with "He").
    iIntros (v) "[[% Hv] | [% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto; by awp_lam.
  Qed.

  Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
366 367 368
     AWP c @ R {{ v, v = #true  AWP b @ R {{ _, U (AWP while (c) { b } @ R {{ Φ }}) }}
                     v = #false  AWP a_seq #() @ R {{ Φ }} }} -
    AWP while (c) { b } @ R {{ Φ }}.
369 370 371 372 373 374 375 376 377 378
  Proof.
    iIntros "H".
    awp_lam. awp_lam. awp_seq.
    iApply a_if_spec.
    iApply (awp_wand with "H").
    iIntros (v) "[[% Hv]|[% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto.
    awp_seq. iApply a_sequence_spec'. iNext.
    awp_seq. done.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
379
  Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) :
Dan Frumin's avatar
Dan Frumin committed
380
    IntoVal ef f 
381 382 383
    AWP ea @ R {{ Ψ }} -
    ( a, Ψ a - U (R -  R', R'  (AWP ef a @ R' {{ v, R' - R  Φ v }}))) -
    AWP a_invoke ef ea @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
384
  Proof.
385
    rewrite /IntoVal. iIntros (<-) "Ha Hfa".
Dan Frumin's avatar
Dan Frumin committed
386 387 388 389 390
    rewrite /a_invoke. awp_lam.
    awp_apply (a_wp_awp R with "Ha").
    iIntros (a) "Ha". awp_let.
    iApply a_sequence_spec.
    iApply (awp_wand with "Ha"). clear a.
391
    iNext. iIntros (a) "HΨ".
392 393
    iSpecialize ("Hfa" with "HΨ").
    iModIntro.
Dan Frumin's avatar
Dan Frumin committed
394
    awp_let.
Dan Frumin's avatar
Dan Frumin committed
395
    iApply awp_atomic. iNext. iIntros "HR".
Dan Frumin's avatar
Dan Frumin committed
396 397
    iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
    iExists R'. iFrame. by awp_let.
Dan Frumin's avatar
Dan Frumin committed
398 399
  Qed.

400
  Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
401 402
    AWP e1 @ R {{ Φ }} -
    AWP if (true) { e1 } else { e2 } @ R {{ Φ }}.
403 404 405 406 407 408
  Proof.
    iIntros "HΦ".
    iApply a_if_spec.
    iApply awp_ret. iApply wp_value.
    iLeft. iSplit; eauto. by awp_seq.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
409

410
  Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
411 412
    AWP e2 @ R {{ Φ }} -
    AWP if (false) { e1 } else { e2 } @ R {{ Φ }}.
413 414 415 416 417 418 419 420 421
  Proof.
    iIntros "HΦ".
    iApply a_if_spec.
    iApply awp_ret. iApply wp_value.
    iRight. iSplit; eauto. by awp_seq.
  Qed.

  Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
    I -
422
     (I - AWP c @ R {{ v, (v = #false  U (Φ #())) 
423
                            (v = #true   AWP b @ R {{ _, U I }}) }}) -
424
    AWP while (c) { b } @ R {{ Φ }}.
425 426 427 428 429 430 431 432
   Proof.
     iIntros "Hi #Hinv". iLöb as "IH".
     iApply a_while_spec. iNext.
     iApply a_if_spec.
     iSpecialize ("Hinv" with "Hi"). iApply (awp_wand with "Hinv").
     iIntros (v) "[(% & H) | (% & H)] //="; subst.
     - iRight. iSplit; by eauto; iApply a_seq_spec.
     - iLeft. iSplit; first eauto. awp_seq.
433
       iApply a_sequence_spec. iNext. awp_seq.
434
       iApply (awp_wand with "H").
435
       iIntros (v) "Hi !>". awp_seq.
436 437
       by iApply ("IH" with "Hi").
   Qed.
Dan Frumin's avatar
Dan Frumin committed
438
End proofs.
439 440

(* Make sure that we only use the provided rules and don't break the abstraction *)
441 442
Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.