translation.v 21.8 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
Definition a_alloc : val := λ: "x1" "x2",
  "vv" ←ᶜ "x1" ||| "x2" ;;
  let: "n" := Fst "vv" in
  let: "v" := Snd "vv" in
17
  a_atomic_env (λ: <>, (ref (SOME (lreplicate "n" "v")), #0)).
18
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
19

20 21 22 23 24 25 26 27 28 29 30 31 32
Definition a_free_check : val :=
  rec: "go" "env" "l" "i" "n" :=
  if: "i" < "n" then
    assert: (mset_member ("l", "i") "env" = #false);;
    "go" "env" "l" (#1 + "i") "n"
  else #().

Definition a_free : val := λ: "x",
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
    let: "l" := Fst "v" in
    let: "i" := Snd "v" in
    match: !"l" with
33
      NONE => assert: #false (* double free *)
34 35 36 37 38
    | SOME "l" =>
       (* We need to make sure `i = 0` and that all `0 ... length of block` are
       unlocked. TODO: this means we need to change the spec of `alloc` back so
       that we can actually establish we initially have the pointer to the first
       element of the array. *)
39
       assert: ("i" = #0);;
40 41 42 43 44 45
       let: "n" := llength "l" in
       a_free_check "env" "l" #0 "n"
       "l" <- NONE
    end
  ).

46
Definition a_store : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
  "vv" ←ᶜ "x1" ||| "x2" ;;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51 52
    let: "l" := Fst (Fst "vv") in
    let: "i" := Snd (Fst "vv") in
    let: "v" := Snd "vv" in
    mset_add ("l", "i") "env" ;;
53
    match: !"l" with
54
      NONE => assert: #false (* store after free *)
55 56
    | SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v"
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
  ).
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
59 60

Definition a_load : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65
    let: "l" := Fst "v" in
    let: "i" := Snd "v" in
    assert: (mset_member ("l", "i") "env" = #false);;
66
    match: !"l" with
67
      NONE => assert: #false (* load after free *)
68 69
    | SOME "ll" => llookup "i" "ll"
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71 72
  ).
Notation "∗ᶜ e" :=
  (a_load e)%E (at level 9, right associativity) : expr_scope.
73 74

Definition a_un_op (op : un_op) : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76
  "v" ←ᶜ "x" ;;
  a_ret (UnOp op "v").
77 78 79

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

Robbert Krebbers's avatar
Nits.  
Robbert Krebbers committed
83
Definition a_seq_bind : val := λ: "f" "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85 86 87 88 89 90
  "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.
91 92

Definition a_if : val := λ: "cnd" "e1" "e2",
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97 98
  "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.
99

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
100 101
Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105
    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.
106

Dan Frumin's avatar
Dan Frumin committed
107 108
Definition a_invoke: val := λ: "f" "arg",
  a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
109
Notation "'callᶜ' ( f , a )" :=
110 111
  ( a_invoke f a)%E
  (at level 100, a at level 200,
112
   format "'callᶜ'  ( f ,  a )") : expr_scope.
113

114 115 116 117 118 119 120 121 122
Inductive cbin_op :=
  | CBinOp : bin_op  cbin_op
  | PtrPlusOp : cbin_op
  | PtrLtOp : cbin_op.

Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
  match op with
  | CBinOp op' => bin_op_eval op' v1 v2
  | PtrPlusOp =>
123 124 125
     cl  cloc_of_val v1;
     o   offset_of_val v2;
     Some (cloc_to_val (cloc_plus cl o))
126
  | PtrLtOp =>
127 128 129
     cl1  cloc_of_val v1;
     cl2  cloc_of_val v2;
     Some #(cloc_lt cl1 cl2)
130 131
  end.

132
Definition a_ptr_plus : val := λ: "x" "y",
133
  "lo" ←ᶜ ("x" ||| "y");;
134
  let: "o'" := Snd (Fst "lo") + Snd "lo" in
135 136 137 138 139 140
  a_ret (Fst (Fst "lo"), "o'").

Definition a_ptr_lt : val := λ: "x" "y",
  "pq" ←ᶜ ("x" ||| "y");;
  let: "p" := Fst "pq" in
  let: "q" := Snd "pq" in
141
  if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false.
142 143 144

Definition a_bin_op (op : cbin_op) : val :=
  match op with
145 146 147 148
  | CBinOp op' => λ: "x1" "x2",
     "vv" ←ᶜ "x1" ||| "x2" ;;
     a_ret (BinOp op' (Fst "vv") (Snd "vv"))
  | PtrPlusOp => a_ptr_plus
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
  | PtrLtOp   => a_ptr_lt
  end.

Notation "e1 +ᶜ e2" := (a_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op (CBinOp MinusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op (CBinOp MultOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op (CBinOp LeOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op (CBinOp LtOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op (CBinOp EqOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op (CBinOp 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.

Notation "e1 +∗ᶜ e2" := (a_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <∗ᶜ e2" := (a_bin_op PtrLtOp e1%E e2%E)  (at level 80) : expr_scope.

Definition a_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
  "lv" ←ᶜ ("x" ||| "y");;
  a_atomic (λ: <>,
    "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
    a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
    a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +∗=ᶜ e2" := (a_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
172

Dan Frumin's avatar
Dan Frumin committed
173
Section proofs.
174
  Context `{amonadG Σ}.
Dan Frumin's avatar
Dan Frumin committed
175

176
  Lemma a_alloc_spec R Φ Ψ1 Ψ2 e1 e2 :
177
    AWP e1 @ R {{ Ψ1 }} -
178 179 180 181
    AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  n : nat,
                 v1 = #n  
                 l, l C replicate n v2 - Φ (cloc_to_val l)) -
182
    AWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
183
  Proof.
184
    iIntros "H1 H2 HΦ".
185
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
186
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
187 188
    iApply awp_bind. iApply (awp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
189
    iDestruct ("HΦ" with "H1 H2") as (n ->) "HΦ".
Dan Frumin's avatar
Dan Frumin committed
190
    iApply awp_atomic_env.
191 192 193
    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".
194
    iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
195
    iIntros "!> !>". rewrite cloc_to_val_eq.
Dan Frumin's avatar
Dan Frumin committed
196
    iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (MkCloc l 0))].
197 198 199
    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.
200 201
  Qed.

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
202
  Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
203 204
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ Ψ2 }} -
205 206
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  cl w,
                 v1 = cloc_to_val cl   cl C w  (cl C[LLvl] v2 - Φ v2)) -
207
    AWP e1 = e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
208
  Proof.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
209
    iIntros "H1 H2 HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211 212
    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
213
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
214
    iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]".
Dan Frumin's avatar
Dan Frumin committed
215
    iApply awp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
217
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
218 219 220
    assert (cloc_to_val cl  X) as HclX.
    { intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
    rewrite cloc_to_val_eq in HclX.
221
    iMod (full_locking_heap_store_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
222
    wp_let. rewrite cloc_to_val_eq. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
223 224
    wp_apply (mset_add_spec with "[$]"); first done.
    iIntros "Hlocks /="; wp_seq.
225
    wp_load; wp_match.
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229
    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Φ".
230 231
    iExists ({[cloc_to_val cl]}  X), _. iFrame "Hσ". rewrite locked_locs_lock.
    iSplit; last by rewrite cloc_to_val_eq. iPureIntro.
232
    intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
233
    eexists. split; [apply (cloc_of_to_val cl)|set_solver].
Dan Frumin's avatar
Dan Frumin committed
234 235
  Qed.

236
  Lemma a_load_spec_exists_frac R Φ e :
237 238
    AWP e @ R {{ v,  cl q w,  v = cloc_to_val cl  
                              cl C{q} w  (cl C{q} w - Φ w) }} -
239
    AWP ∗ᶜe @ R {{ Φ }}.
240
  Proof.
241 242
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
244
    iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246
    iApply awp_atomic_env. iIntros (env) "Henv HR".
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
247
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
248 249 250
    assert (cloc_to_val cl  X) as HclX.
    { intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
    rewrite cloc_to_val_eq in HclX.
251
    iMod (full_locking_heap_load_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
252
    wp_let. rewrite cloc_to_val_eq. wp_proj; wp_let. wp_proj; wp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
254
    rewrite bool_decide_false //.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
    wp_op. iSplit; first done. iNext; wp_seq.
256
    wp_load; wp_match. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258 259
    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists X, _. by iFrame.
260 261
  Qed.

262
  Lemma a_load_spec R Φ q e :
263 264 265
    AWP e @ R {{ v,  cl w,
                     v = cloc_to_val cl  
                    cl C{q} w  (cl C{q} w - Φ w) }} -
266
    AWP ∗ᶜe @ R {{ Φ }}.
267
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
    iIntros "H". iApply a_load_spec_exists_frac.
269
    awp_apply (awp_wand with "H").
270
    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
271 272 273
  Qed.

  Lemma a_un_op_spec R Φ e op:
274
    AWP e @ R {{ v,  w : val, un_op_eval op v = Some w  Φ w }} -
Dan Frumin's avatar
Dan Frumin committed
275
    AWP a_un_op op e @ R {{ Φ }}.
276 277 278 279 280 281 282 283 284 285 286
  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.

  Lemma a_seq_spec R Φ :
    U (Φ #()) -
287
    AWP a_seq #() @ R {{ Φ }}.
288 289
  Proof.
    iIntros "HΦ". rewrite /a_seq. awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
290 291 292
    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".
293
    iDestruct "HΦ" as (us) "[Hus HΦ]".
Dan Frumin's avatar
Dan Frumin committed
294
    iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
295 296
    - iModIntro. iSplitR "HΦ".
      + iExists , σ. by iFrame.
297 298
      + by iApply "HΦ".
    - iDestruct "Hus" as "[Hu Hus]".
299 300 301
      iDestruct (full_locking_heap_locked_present with "Hu Hσ")
        as %[z Hz].
      iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
302 303
      iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks").
      iIntros "Hus". iApply "HΦ". by iFrame.
304 305 306 307
  Qed.

  Lemma a_sequence_spec R Φ (f e : expr) :
    AsVal f 
308 309
     AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -
    AWP a_seq_bind f e @ R {{ Φ }}.
310
  Proof.
311
    iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
312 313 314 315 316 317
    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.

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

329
  Lemma a_while_spec  R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
     AWP a_if c (λ: <>, (λ: <>, b) #() ; while (c) { b }) a_seq @ R {{ Φ }} -
    AWP while (c) { b } @ R {{ Φ }}.
332 333 334 335 336 337 338
  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
339 340
    AsVal e1 
    AsVal e2 
341 342 343
    AWP e @ R {{ v, (v = #true  AWP e1 #() @ R {{ Φ }}) 
                    (v = #false  AWP e2 #() @ R {{ Φ }}) }} -
    AWP a_if e e1 e2 @ R {{ Φ }}.
344
  Proof.
345
    iIntros ([v1 <-] [v2 <-]) "H".
346 347 348 349 350
    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.

351
  Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
352 353 354
    AWP e @ R {{ v, (v = #true  AWP e1 @ R {{ Φ }}) 
                    (v = #false  AWP e2 @ R {{ Φ }}) }} -
    AWP if (e) { e1 } else { e2 } @ R {{ Φ }}.
355 356 357 358 359 360 361
  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} :
362 363 364
     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 {{ Φ }}.
365 366 367 368 369 370 371 372 373 374
  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
375
  Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) :
Dan Frumin's avatar
Dan Frumin committed
376
    IntoVal ef f 
377 378 379
    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
380
  Proof.
381
    rewrite /IntoVal. iIntros (<-) "Ha Hfa".
Dan Frumin's avatar
Dan Frumin committed
382 383 384 385 386
    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.
387
    iNext. iIntros (a) "HΨ".
388 389
    iSpecialize ("Hfa" with "HΨ").
    iModIntro.
Dan Frumin's avatar
Dan Frumin committed
390
    awp_let.
Dan Frumin's avatar
Dan Frumin committed
391
    iApply awp_atomic. iNext. iIntros "HR".
Dan Frumin's avatar
Dan Frumin committed
392 393
    iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
    iExists R'. iFrame. by awp_let.
Dan Frumin's avatar
Dan Frumin committed
394 395
  Qed.

396
  Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
397 398
    AWP e1 @ R {{ Φ }} -
    AWP if (true) { e1 } else { e2 } @ R {{ Φ }}.
399 400 401 402 403 404
  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
405

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

416
  Lemma a_ptr_plus_spec R Φ Ψ2 e1 e2 :
417 418 419 420
    AWP e2 @ R {{ Ψ2 }} -
    AWP e1 @ R {{ v1,   v2, Ψ2 v2 -  cl (n : nat),
                          v1 = cloc_to_val cl  
                          v2 = #n  
421 422
                         Φ (cloc_to_val (cloc_plus cl n)) }} -
    AWP a_ptr_plus e1 e2 @ R {{ Φ }}.
423
  Proof.
424
    iIntros "He2 HΦ". rewrite /a_ptr_plus.
425 426 427 428
    awp_apply (a_wp_awp with "HΦ"); 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.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
429 430
    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
    rewrite cloc_to_val_eq.
431
    do 3 awp_proj. awp_op. awp_let. do 2 awp_proj.
Dan Frumin's avatar
Dan Frumin committed
432
    iApply awp_ret. iApply wp_value. by rewrite Nat.add_comm -Nat2Z.inj_add.
433 434 435 436 437 438 439 440 441 442
  Qed.

  Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ v2,   v1, Ψ1 v1 -  p q,
                          v1 = cloc_to_val p  
                          v2 = cloc_to_val q  
                         Φ #(cloc_lt p q) }} -
    AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
  Proof.
443
    iIntros "He1 HΦ". rewrite /a_ptr_plus.
444 445 446 447
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
448
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
449
    rewrite cloc_to_val_eq.
450
    do 2 (awp_proj; awp_let). do 2 awp_proj.
Dan Frumin's avatar
Dan Frumin committed
451 452
    unfold cloc_lt; simpl. case_bool_decide as Hp; subst; awp_op.
    - rewrite (bool_decide_true (LitV ql = LitV ql)) //. awp_if. do 2 awp_proj.
453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473
      iApply awp_ret. wp_op.
      rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt.
    - rewrite bool_decide_false; last congruence.
      awp_if. iApply awp_ret. by iApply wp_value.
  Qed.

  Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : cbin_op) (e1 e2: expr) :
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, cbin_op_eval op v1 v2 = Some w  Φ w) -
    AWP a_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "H1 H2 HΦ".
    destruct op as [op'| |].
    - 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.
      iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
      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 _.
474
    - iApply (a_ptr_plus_spec with "H2").
475 476 477
      iApply (awp_wand with "H1").
      iIntros (v1) "HΨ1". iNext.
      iIntros (v2) "HΨ2". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
478 479 480 481 482
      simpl in hop.
      destruct (cloc_of_val v1) as [cl|] eqn:Hcl; simplify_eq/=.
      destruct (offset_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
      iExists cl,o. iFrame.
      rewrite -(cloc_to_of_val v1 cl) // (offset_to_of_val v2 o) //.
483 484 485 486 487
    - iApply (a_ptr_lt_spec with "H1").
      iApply (awp_wand with "H2").
      iIntros (v2) "HΨ2". iNext.
      iIntros (v1) "HΨ1". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
      simpl in hop.
488 489 490 491
      destruct (cloc_of_val v1) as [cl1|] eqn:Hcl1; simplify_eq/=.
      destruct (cloc_of_val v2) as [cl2|] eqn:Hcl2; simplify_eq/=.
      iExists cl1, cl2. iFrame.
      rewrite -(cloc_to_of_val v1 cl1) // -(cloc_to_of_val v2 cl2) //.
492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
  Qed.

  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 -
         cl v w,  v1 = cloc_to_val cl  
                  cl C v 
                   cbin_op_eval op v v2 = Some w  
                  (cl C[LLvl] w - R  Φ v)) -
    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.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
    iApply awp_atomic. iNext.
    iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
    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.
    iExists cl, v; iFrame. iSplit; first done.
    iIntros "Hl". awp_let. iApply awp_bind.
    iApply (a_store_spec _ _
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
    - awp_proj. iApply awp_ret; by wp_value_head.
    - iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
        try (try awp_proj; iApply awp_ret; by wp_value_head).
      iNext. iIntros (? ? -> ->). eauto.
    - iNext. iIntros (? ? -> ->).
      iExists _, _; iFrame. iSplit; first done.
      iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
      iIntros "_". by iApply "HΦ".
524 525
  Qed.

526 527
  Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
    I -
528
     (I - AWP c @ R {{ v, (v = #false  U (Φ #())) 
529
                            (v = #true   AWP b @ R {{ _, U I }}) }}) -
530
    AWP while (c) { b } @ R {{ Φ }}.
531 532 533 534 535 536 537 538
   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.
539
       iApply a_sequence_spec. iNext. awp_seq.
540
       iApply (awp_wand with "H").
541
       iIntros (v) "Hi !>". awp_seq.
542 543
       by iApply ("IH" with "Hi").
   Qed.
Dan Frumin's avatar
Dan Frumin committed
544
End proofs.
545 546

(* Make sure that we only use the provided rules and don't break the abstraction *)
547
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.
548
Global 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.