translation.v 28.3 KB
Newer Older
1
From iris_c.c_translation Require Export monad.
2 3 4 5
From iris_c.lib Require Export U.
From iris_c.c_translation Require Export proofmode.
From iris.heap_lang Require Export assert.
From iris_c.lib Require Import mset flock list.
6

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

10
Definition c_alloc : val := λ: "x1" "x2",
11 12 13
  "vv" ←ᶜ "x1" ||| "x2" ;;
  let: "n" := Fst "vv" in
  let: "v" := Snd "vv" in
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  assert: (#0 < "n");;
15
  c_atomic_env (λ: <>, SOME (ref (SOME (#true, lreplicate "n" "v")), #0)).
16
Notation "'allocᶜ' ( e1 , e2 )" :=
17
  (c_alloc e1%E e2%E) (at level 10, e1, e2 at level 99) : expr_scope.
18

19
Definition c_free_check : val :=
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
20 21 22 23 24 25
  rec: "go" "env" "l" "n" :=
  if: "n" = #0 then #() else
  let: "n" := "n" - #1 in
  assert: (mset_member ("l", "n") "env" = #false);;
  "go" "env" "l" "n".

26
Definition c_free : val := λ: "x",
27
  "v" ←ᶜ "x";;
28
  c_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31 32 33 34 35
    match: "v" with
      NONE => assert: #false (* null pointer *)
    | SOME "li" =>
       let: "l" := Fst "li" in
       let: "i" := Snd "li" in
       match: !"l" with
         NONE => assert: #false (* location already freed, double free *)
36 37 38 39 40
       | SOME "kll" =>
          let: "k" := Fst "kll" in
          let: "ll" := Snd "kll" in
          (* Make sure its not a block scoped variable *)
          assert: ("k" = #true);;
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
41 42
          (* We need to make sure `i = 0` and that all `0 ... length of block`
          are unlocked. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
          assert: ("i" = #0);;
          let: "n" := llength "ll" in
45
          c_free_check "env" "l" "n";;
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47
         "l" <- NONE
       end
48 49
    end
  ).
50
Notation "'freeᶜ' ( e )" :=
51
  (c_free e%E) (at level 10, e at level 99) : expr_scope.
52

53
Definition c_store : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  "vv" ←ᶜ "x1" ||| "x2" ;;
55
  c_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59 60 61 62 63 64
    match: Fst "vv" with
      NONE => assert: #false (* null pointer *)
    | SOME "li" =>
       let: "l" := Fst "li" in
       let: "i" := Snd "li" in
       let: "v" := Snd "vv" in
       mset_add ("l", "i") "env" ;;
       match: !"l" with
         NONE => assert: #false (* store after free *)
65
       | SOME "kll" => "l" <- SOME (Fst "kll", linsert "i" "v" (Snd "kll")) ;; "v"
Robbert Krebbers's avatar
Robbert Krebbers committed
66
       end
67
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  ).
69
Notation "e1 =ᶜ e2" := (c_store e1%E e2%E) (at level 80) : expr_scope.
70

71
Definition c_load : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  "v" ←ᶜ "x";;
73
  c_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76 77 78 79 80 81
    match: "v" with
      NONE => assert: #false (* null pointer *)
    | SOME "li" =>
       let: "l" := Fst "li" in
       let: "i" := Snd "li" in
       assert: (mset_member ("l", "i") "env" = #false);;
       match: !"l" with
         NONE => assert: #false (* load after free *)
82
       | SOME "kll" => llookup "i" (Snd "kll")
Robbert Krebbers's avatar
Robbert Krebbers committed
83
       end
84
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
  ).
Notation "∗ᶜ e" :=
87
  (c_load e)%E (at level 20, right associativity) : expr_scope.
88

89
Notation "'skipᶜ'" := (c_ret #()).
Dan Frumin's avatar
Dan Frumin committed
90

91
Definition c_seq_bind : val := λ: "x" "f",
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  "a" ←ᶜ "x" ;;
93
  c_atomic_env mset_clear ;;
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  "f" "a".
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Notation "x ←ᶜ e1 ;ᶜ e2" :=
96
  (c_seq_bind e1%E (λ: x, e2)%E)%E
97 98
  (at level 100, e1 at next level, e2 at level 200, right associativity,
   format "'[' x  ←ᶜ  '[' e1 ']' ;ᶜ  '/' e2 ']'") : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Notation "e1 ;ᶜ e2" :=
100
  (c_seq_bind e1%E (λ: <>, e2)%E)%E
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  (at level 100, e2 at level 200,
102
   format "'[' '[hv' '[' e1 ']'  ;ᶜ ']'  '/' e2 ']'") : expr_scope.
103

104
Definition c_mut_bind : val := λ: "x" "f",
105
  "v" ←ᶜ "x" ;
106
  "l" ←ᶜ c_atomic_env (λ: <>, ref (SOME (#false, lreplicate #1 "v"))) ;;
107
  "b" ←ᶜ "f" (SOME ("l", #0)) ;;
108 109
  c_atomic_env (λ: <>, "l" <- NONE) ;;
  c_ret "b".
110
Notation "x ←mutᶜ e1 ;ᶜ e2" :=
111
  (c_mut_bind e1 (λ: x, e2))%E
112 113
  (at level 100, e1 at next level, e2 at level 200, right associativity,
   format "'[' x  ←mutᶜ  '[' e1 ']' ;ᶜ  '/' e2 ']'") : expr_scope.
114

115
Definition c_if : val := λ: "cnd" "e1" "e2",
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117
  (* sequenced binds needed here; there should be sequence point after the conditional *)
  "c" ←ᶜ "cnd" ;
Robbert Krebbers's avatar
Robbert Krebbers committed
118
  if: "c" then "e1" #() else "e2" #().
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Notation "'ifᶜ' ( cnd ) { e1 } 'elseᶜ' { e2 }" :=
120
  (c_if cnd%E (λ: <>, e1)%E (λ: <>, e2)%E)
121 122
  (at level 10, cnd, e1, e2 at level 99,
   format "'[v' 'ifᶜ'  ( cnd )  {  '/  ' '[' e1 ']'  '/' }  'elseᶜ'  {  '/  ' '[' e2 ']'  '/' } ']'") : expr_scope.
123

124
Definition c_while: val :=
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
125
  rec: "while" "cnd" "bdy" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127
    if ("cnd" #()) { "bdy" #() ; "while" "cnd" "bdy" }
    else { skip }.
128
Notation "'whileᶜ' ( cnd ) { e }" := (c_while (λ: <>, cnd)%E (λ: <>, e)%E)
129 130 131
  (at level 10, cnd, e at level 99,
   format "'[v' 'whileᶜ'  ( cnd )  {  '/  ' '[' e ']'  '/' } ']'") : expr_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
(* A version of while with value lambdas, this is an artifact because of the way
heap_lang works in Coq *)
134
Notation "'whileVᶜ' ( cnd ) { e }" := (c_while (LamV <> cnd) (LamV <> e))
135 136
  (at level 10, cnd, e at level 99,
   format "'[v' 'whileVᶜ'  ( cnd )  {  '/  ' '[' e ']' '/'  } ']'") : expr_scope.
137

138
Definition c_fun (f : expr) : val := λ: "arg",
139 140
  (* sequence point at the end of a function *)
  "v" ←ᶜ f "arg" ;
141
  c_ret "v".
142
(* TODO: Similar notation for recursive functions *)
143
Notation "'λᶜ' x , e" := (c_fun (λ: x, e)%V)
144 145 146
  (at level 200, x at level 1, e at level 200,
   format "'[' 'λᶜ'  x ,  '/  ' e ']'") : val_scope.

147
Definition c_call : val := λ: "f" "arg",
148
  (* sequence point before a function call *)
Dan Frumin's avatar
Dan Frumin committed
149 150 151 152
  "fa" ←ᶜ ("f" ||| "arg") ;;
  c_atomic (λ: <>,
    c_atomic_env mset_clear ;;
    (Fst "fa") (Snd "fa")).
153
Notation "'callᶜ' f a" :=
154
  (c_call f a)%E
155 156
  (at level 10, f, a at level 9,
   format "'callᶜ'  f  a") : expr_scope.
157

158 159
Definition c_un_op (op : un_op) : val := λ: "x",
  "v" ←ᶜ "x" ;; c_ret (UnOp op "v").
Robbert Krebbers's avatar
Robbert Krebbers committed
160

161 162 163 164 165
Inductive cbin_op :=
  | CBinOp : bin_op  cbin_op
  | PtrPlusOp : cbin_op
  | PtrLtOp : cbin_op.

166
Definition c_ptr_plus : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  (* all binds should be non-sequenced *)
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170
  "vv" ←ᶜ ("x" ||| "y");;
  match: Fst "vv" with
    NONE => assert #false (* null pointer *)
171
  | SOME "li" => c_ret (SOME (Fst "li", Snd "vv" + Snd "li"))
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  end.
173

174
Definition c_ptr_lt : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  (* all binds should be non-sequenced *)
176
  "pq" ←ᶜ ("x" ||| "y");;
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180 181 182 183
  match: Fst "pq" with
    NONE => assert #false (* null pointer *)
  | SOME "p" =>
     match: Snd "pq" with
       NONE => assert #false (* null pointer *)
     | SOME "q" =>
        if: Fst "p" = Fst "q"
184
        then c_ret (Snd "p" < Snd "q") else c_ret #false
Robbert Krebbers's avatar
Robbert Krebbers committed
185 186
     end
  end.
187

188
Definition c_bin_op (op : cbin_op) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  (* all binds should be non-sequenced *)
190
  match op with
191 192
  | CBinOp op' => λ: "x1" "x2",
     "vv" ←ᶜ "x1" ||| "x2" ;;
193 194 195
     c_ret (BinOp op' (Fst "vv") (Snd "vv"))
  | PtrPlusOp => c_ptr_plus
  | PtrLtOp   => c_ptr_lt
196
  end.
197 198 199 200 201 202 203 204 205 206 207
Notation "e1 +ᶜ e2" := (c_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 50) : expr_scope.
Notation "e1 -ᶜ e2" := (c_bin_op (CBinOp MinusOp) e1%E e2%E) (at level 35) : expr_scope.
Notation "e1 *ᶜ e2" := (c_bin_op (CBinOp MultOp) e1%E e2%E) (at level 40) : expr_scope.
Notation "e1 ≤ᶜ e2" := (c_bin_op (CBinOp LeOp) e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 <ᶜ e2" := (c_bin_op (CBinOp LtOp) e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 ==ᶜ e2" := (c_bin_op (CBinOp EqOp) e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 !=ᶜ e2" := (c_un_op NegOp (c_bin_op (CBinOp EqOp) e1%E e2%E)) (at level 70): expr_scope.
Notation "~ᶜ e" := (c_un_op NegOp e%E) (at level 20, right associativity) : expr_scope.

Notation "e1 +∗ᶜ e2" := (c_bin_op PtrPlusOp e1%E e2%E) (at level 50) : expr_scope.
Notation "e1 <∗ᶜ e2" := (c_bin_op PtrLtOp e1%E e2%E)  (at level 70) : expr_scope.
208

209 210 211
Definition int_of_val (v : val) : option Z :=
  match v with LitV (LitInt x) => Some x | _ => None end.

Robbert Krebbers's avatar
Robbert Krebbers committed
212 213 214 215 216
Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
  match op with
  | CBinOp op' => bin_op_eval op' v1 v2
  | PtrPlusOp =>
     cl  cloc_of_val v1;
217
     o   int_of_val v2;
Robbert Krebbers's avatar
Robbert Krebbers committed
218
     Some (cloc_to_val (cl + o))
Robbert Krebbers's avatar
Robbert Krebbers committed
219 220 221 222 223 224
  | PtrLtOp =>
     cl1  cloc_of_val v1;
     cl2  cloc_of_val v2;
     Some #(cloc_lt cl1 cl2)
  end.

225
Definition c_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
226
  (* all binds should be non-sequenced *)
227
  "lv" ←ᶜ ("x" ||| "y");;
228 229 230 231
  c_atomic (λ: <>,
    "ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;
    c_ret (Fst "lv") = c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;
    c_ret "ov").
232 233
Notation "e1 +=ᶜ e2" := (c_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +∗=ᶜ e2" := (c_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
234

Dan Frumin's avatar
Dan Frumin committed
235
Section proofs.
236
  Context `{cmonadG Σ}.
Dan Frumin's avatar
Dan Frumin committed
237

238 239 240
  Lemma cwp_alloc R Φ Ψ1 Ψ2 e1 e2 :
    CWP e1 @ R {{ Ψ1 }} -
    CWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
241 242
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  n : nat,
               v1 = #n    n  0%nat  
243
               cl, block_info cl true n - cl C replicate n v2 - Φ (cloc_to_val cl)) -
244
    CWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
245
  Proof.
246
    iIntros "H1 H2 HΦ".
247 248 249 250 251
    cwp_apply (cwp_wp with "H2"); iIntros (v2) "H2".
    cwp_apply (cwp_wp with "H1"); iIntros (v1) "H1".
    cwp_lam. cwp_pures.
    iApply cwp_bind. iApply (cwp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures.
252
    iDestruct ("HΦ" with "H1 H2") as (n -> ?) "HΦ".
253 254 255
    cwp_apply wp_assert. wp_op. rewrite bool_decide_true; last lia.
    iSplit; first done. iNext. cwp_pures.
    iApply cwp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_pures.
257
    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
Robbert Krebbers's avatar
Robbert Krebbers committed
258
    wp_alloc l as "Hl".
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
259 260 261 262
    iMod (full_locking_heap_alloc_upd with "Hσ Hl")
      as (?) "(Hσ & Hinfo & Hl)"; first done.
    { by destruct n. }
    wp_pures. iIntros "!>". rewrite cloc_to_val_eq replicate_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265 266
    iSplitL "Hlocks 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.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
267 268 269
    - iApply ("HΦ" $! (CLoc l 0) with "Hinfo Hl").
  Qed.

270
  Lemma cwp_free R Φ e :
Dan Frumin's avatar
Dan Frumin committed
271 272
    CWP e @ R {{ v, R ={}=  cl ws,  v = cloc_to_val cl  
                        block_info cl true (length ws)  cl C ws  R  Φ #() }} -
273
    CWP free(e) @ R {{ Φ }}.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
274 275
  Proof.
    iIntros "H".
276 277
    cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
    iApply cwp_bind. iApply (cwp_wand with "H"). clear v.
Dan Frumin's avatar
Dan Frumin committed
278
    iIntros (v) "H". cwp_pures.
279
    iApply cwp_atomic_env. iIntros (env) "Henv HR". wp_pures.
Dan Frumin's avatar
Dan Frumin committed
280
    iMod ("H" with "HR") as (cl ws ->) "(Hinfo & Hcl & $ & HΦ)". cwp_pures.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
281 282 283 284 285 286 287 288 289
    rewrite cloc_to_val_eq. wp_pures.
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
    iAssert   i : nat, is_Some (ws !! i)  (cl + i)  locked_locs σ⌝%I as %Hlocked.
    { iIntros (i [w Hi]). rewrite /mapsto_list.
      iDestruct (big_sepL_lookup with "Hcl") as "H"; first done.
      by iApply (full_locking_heap_unlocked with "[$]"). }
    iMod (full_locking_heap_free_upd with "Hσ Hinfo Hcl")
      as (ll Hoff Hl) "[Hl Hclose]".
    wp_load. wp_pures. rewrite Hoff.
290 291 292
    wp_apply wp_assert; wp_pures; iSplit; first done. iNext.
    wp_apply wp_assert; wp_pures; iSplit; first done. iNext.
    wp_pures. wp_apply (llength_spec with "[//]"); iIntros "_"; wp_pures.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
293
    iAssert ( Ψ (n : nat),  n  length ws  
294
      (is_mset env X - Ψ #()) - WP c_free_check env #(cloc_base cl) #n {{ Ψ }})%I
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
295 296 297 298 299 300 301 302 303 304 305 306
      with "[Hlocks]" as "Hcheck".
    { iIntros (Ψ n Hn) "HΨ". iInduction n as [|n] "IH" forall (Ψ Hn).
      { wp_lam; wp_pures. by iApply "HΨ". }
      wp_lam; wp_pures. wp_apply wp_assert.
      rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
      wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks"; case_bool_decide.
      { destruct (HX (#(cloc_base cl), #n)%V) as (cl'&[= <-]&?); first done.
        destruct (Hlocked n); first by (apply lookup_lt_is_Some_2; lia).
        destruct cl; simplify_eq/=. by rewrite /cloc_plus /= Z.add_0_r. }
      wp_op. iSplit; first done. iNext; wp_pures.
      iApply ("IH" with "[%] Hlocks HΨ"). lia. }
    wp_apply ("Hcheck" with "[//]"); iIntros "Hlock". wp_pures. wp_store.
Dan Frumin's avatar
Dan Frumin committed
307
    iIntros "!> {$HΦ}". iExists X, _.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
308 309 310 311 312 313 314
    iFrame "Hlock". iSplit; last by iApply "Hclose".
    iPureIntro; intros w Hw. destruct (HX _ Hw) as (cl'&Hcl&Hin).
    exists cl';  split; first done. apply locked_locs_free_heap; first done.
    intros (?&?&?). destruct (Hlocked (Z.to_nat (cloc_offset cl'))).
    { apply lookup_lt_is_Some_2, Nat2Z.inj_lt. rewrite Z2Nat.id; lia. }
    destruct cl, cl'; simplify_eq/=.
    by rewrite /cloc_plus /= Z.add_0_r Z2Nat.id; last lia.
315 316
  Qed.

317 318 319
  Lemma cwp_store R Φ Ψ1 Ψ2 e1 e2 :
    CWP e1 @ R {{ Ψ1 }} -
    CWP e2 @ R {{ Ψ2 }} -
Dan Frumin's avatar
Dan Frumin committed
320 321
    ( v1 v2, Ψ1 v1 - Ψ2 v2 - R ={}=  cl w,
         v1 = cloc_to_val cl   cl C w  (cl C[LLvl] v2 ={}= R  Φ v2)) -
322
    CWP e1 = e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
323
  Proof.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
324
    iIntros "H1 H2 HΦ".
325 326 327 328 329 330
    cwp_apply (cwp_wp with "H2"); iIntros (v2) "H2".
    cwp_apply (cwp_wp with "H1"); iIntros (v1) "H1".
    cwp_lam. cwp_pures.
    iApply cwp_bind. iApply (cwp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures.
    iApply cwp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
Dan Frumin's avatar
Dan Frumin committed
332
    iMod ("HΦ" with "H1 H2 HR") as (cl w ->) "[Hl HΦ]".
333
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
334
    iDestruct (mapsto_offset_non_neg with "Hl") as %?.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
    assert ((#(cloc_base cl), #(cloc_offset cl))%V  X) as HclX.
336
    { intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
337
    iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
338
    wp_pures. rewrite cloc_to_val_eq. wp_pures.
339
    wp_apply (mset_add_spec with "[$]"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
    iIntros "Hlocks /="; wp_pures.
341
    wp_load; wp_pures.
342 343
    iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
    wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
Robbert Krebbers's avatar
Robbert Krebbers committed
344 345
    iApply wp_fupd. wp_store.
    iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
Dan Frumin's avatar
Dan Frumin committed
346 347
    iMod ("HΦ" with "Hl") as "HΦ".
    iIntros "!> !>". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
348
    iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]}  X), _.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
    iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
Dan Frumin's avatar
Dan Frumin committed
350 351
  Qed.

352
  Lemma cwp_load_exists_frac R Φ e :
Dan Frumin's avatar
Dan Frumin committed
353 354
    CWP e @ R {{ v, R ={}=  cl q w,  v = cloc_to_val cl  
                        cl C{q} w  (cl C{q} w ={}= R  Φ w) }} -
355
    CWP ∗ᶜe @ R {{ Φ }}.
356
  Proof.
357
    iIntros "H".
358 359
    cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
    iApply cwp_bind. iApply (cwp_wand with "H"). clear v.
Dan Frumin's avatar
Dan Frumin committed
360
    iIntros (v) "H". cwp_pures.
361
    iApply cwp_atomic_env. iIntros (env) "Henv HR".
Dan Frumin's avatar
Dan Frumin committed
362 363
    iMod ("H" with "HR")  as (cl q w ->) "[Hl HΦ]".
    iDestruct (mapsto_offset_non_neg with "Hl") as %?.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
365
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
    assert ((#(cloc_base cl), #(cloc_offset cl))%V  X) as HclX.
367
    { intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
368
    iMod (full_locking_heap_load_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
369
    wp_pures. rewrite cloc_to_val_eq. wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
371
    rewrite bool_decide_false //.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
    wp_op. iSplit; first done. iNext; wp_seq.
373 374
    wp_load; wp_match.
    iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
Dan Frumin's avatar
Dan Frumin committed
375
    iApply wp_fupd.
376
    wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
377
    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
Dan Frumin's avatar
Dan Frumin committed
378 379
    iMod ("HΦ" with "Hl") as "[$ $]".
    iIntros "!> !>". iExists X, _. by iFrame.
380 381
  Qed.

382
  Lemma cwp_load R Φ q e :
Dan Frumin's avatar
Dan Frumin committed
383 384
    CWP e @ R {{ v, R ={}=  cl w,  v = cloc_to_val cl  
                      cl C{q} w  (cl C{q} w ={}= R  Φ w) }} -
385
    CWP ∗ᶜe @ R {{ Φ }}.
386
  Proof.
387 388
    iIntros "H". iApply cwp_load_exists_frac.
    cwp_apply (cwp_wand with "H").
Dan Frumin's avatar
Dan Frumin committed
389 390
    iIntros (v). iIntros "H HR".
    iMod ("H" with "HR") as (cl w ->) "[H1 H2]". eauto 100 with iFrame.
391 392
  Qed.

Dan Frumin's avatar
Dan Frumin committed
393 394 395 396
  (** Helper lemma *)
  Lemma cwp_mset_clear R Φ :
     U (Φ #()) -
    CWP c_atomic_env mset_clear @ R {{ Φ }}.
397
  Proof.
Dan Frumin's avatar
Dan Frumin committed
398 399 400
    iIntros "HΦ". iApply cwp_atomic_env.
    iIntros (env). iDestruct (1) as (X σ _) "[Hlocks Hσ]".
    iIntros "$". iApply wp_fupd.
401
    wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
Dan Frumin's avatar
Dan Frumin committed
402
    rewrite U_eq. iDestruct "HΦ" as (us) "[Hus H]".
403
    iInduction us as [|[ul [uq uv]] us] "IH" using gmultiset_ind forall (σ); simpl.
Dan Frumin's avatar
Dan Frumin committed
404
    - iModIntro. iSplitR "H Hus".
Robbert Krebbers's avatar
Robbert Krebbers committed
405
      + iExists , σ. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
406
      + iNext. by iApply "H".
407
    - iDestruct "Hus" as "[Hu Hus]". rewrite !big_sepMS_singleton /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
      iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz].
409
      iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
410
      iApply ("IH" with "Hus [H Hu] Hσ Hlocks").
411
      iIntros "Hus". iApply "H". iFrame. by rewrite !big_sepMS_singleton /=.
412 413
  Qed.

Dan Frumin's avatar
Dan Frumin committed
414 415
  (* Internal spec: breaks the abstraction/notation *)
  Lemma cwp_seq_bind' R Φ e (f: val) :
416
    CWP e @ R {{ v,  U (CWP f v @ R {{ Φ }}) }} -
Dan Frumin's avatar
Dan Frumin committed
417 418 419 420 421 422 423 424 425
    CWP c_seq_bind e f @ R {{ Φ }}.
  Proof.
    iIntros "H".
    cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
    iApply cwp_bind. iApply (cwp_wand with "H"). iIntros (w) "H".
    cwp_pures. iApply cwp_bind. iApply cwp_mset_clear.
    iNext. iModIntro. by cwp_lam.
  Qed.

426
  Lemma cwp_seq_bind R Φ x e1 e2 :
427
    CWP e1 @ R {{ v,  U (CWP subst' x v e2 @ R {{ Φ }}) }} -
428
    CWP x ←ᶜ e1 ; e2 @ R {{ Φ }}.
429
  Proof.
430
    iIntros "H". cwp_pures. iApply cwp_seq_bind'.
431
    iApply (cwp_wand with "H"); iIntros (v) "H !> !>". by cwp_lam.
432 433
  Qed.

434
  (* Internal spec: breaks the abstraction/notation *)
435 436
  Lemma cwp_mut_bind' R Φ e (f: val) :
    CWP e @ R {{ v, U ( cl,
437
      cl C v -
438 439
      CWP f (cloc_to_val cl) @ R {{ w,  v', cl C v'  Φ w }}) }} -
    CWP c_mut_bind e f @ R {{ Φ }}.
440 441
  Proof.
    iIntros "H".
442
    cwp_apply (cwp_wp with "H"); iIntros (ev) "H". cwp_lam. cwp_pures.
443
    iApply cwp_seq_bind'; iApply (cwp_wand with "H"); iIntros (v) "H !> !>".
444 445
    cwp_pures. iApply cwp_bind.
    cwp_apply cwp_atomic_env; iIntros (env) "Henv $". iApply wp_fupd.
446 447 448 449 450 451 452 453 454 455
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". wp_pures.
    wp_apply (lreplicate_spec 1 with "[//]"); iIntros (ll Hll).
    wp_alloc l as "Hl".
    iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "(Hσ & Hinfo & Hl)"=> //=.
    iDestruct "Hl" as "[Hl _]".
    iIntros "!> !>". iSplitL "Hlocks 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_unlocked. }
    iSpecialize ("H" with "Hl"). rewrite cloc_to_val_eq /=.
456 457 458
    cwp_pures. iApply cwp_bind. cwp_pures. iApply (cwp_wand with "H").
    iIntros (w). iDestruct 1 as (v') "[Hl H]". cwp_pures. iApply cwp_bind.
    cwp_apply cwp_atomic_env; iIntros (env') "Henv $". iApply wp_fupd.
459 460 461 462 463 464 465 466
    iDestruct "Henv" as (X' σ' HX') "[Hlock Hσ]". wp_pures.
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?.
    iMod (full_locking_heap_free_upd _ _ [_] with "Hσ Hinfo [$Hl //]")
      as (ll' _ _) "[Hll Hclose] /=".
    wp_store. iIntros "!> !>". iSplitL "Hlock Hll Hclose".
    { iExists X', _. iFrame "Hlock". iSplit; last by iApply "Hclose".
      iPureIntro; intros w' Hw'. destruct (HX' _ Hw') as (cl'&Hcl&Hin).
      exists cl';  split; first done. rewrite locked_locs_delete. set_solver. }
467
    cwp_pures. iApply cwp_ret. by iApply wp_value.
468 469
  Qed.

470 471
  Lemma cwp_mut_bind R Φ x e1 e2 :
    CWP e1 @ R {{ v, U ( cl,
472
      cl C v -
473 474
      CWP subst' x (cloc_to_val cl) e2 @ R {{ w,  v', cl C v'  Φ w }}) }} -
    CWP x mut e1 ; e2 @ R {{ Φ }}.
475
  Proof.
476 477 478
    iIntros "H". cwp_pures. iApply cwp_mut_bind'.
    iApply (cwp_wand with "H"); iIntros (v) "H !>"; iIntros (cl) "Hcl".
    cwp_lam. by iApply "H".
479 480
  Qed.

481 482 483 484
  Lemma cwp_if R Φ c e1 e2 :
    CWP c @ R {{ v, (v = #true  U (CWP e1 @ R {{ Φ }})) 
                    (v = #false  U (CWP e2 @ R {{ Φ }})) }} -
    CWP if (c) { e1 } else { e2 } @ R {{ Φ }}.
485
  Proof.
486 487 488
    iIntros "H". rewrite /c_if -lock. cwp_pures.
    cwp_apply (cwp_wp with "H"). iIntros (v) "H". cwp_pures.
    iApply cwp_seq_bind'. iApply (cwp_wand with "H").
489
    iIntros (v') "[[-> ?] | [-> ?]] !> !>"; by cwp_pures.
490 491
  Qed.

492 493 494 495
  Lemma cwp_while R Φ c e :
    CWP whileV (c) { e } @ R {{ Φ }} -
    CWP while (c) { e } @ R {{ Φ }}.
  Proof. iIntros "H". by cwp_pures. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
496

497
  Lemma cwp_whileV R Φ c e :
Robbert Krebbers's avatar
Robbert Krebbers committed
498
    (* The later is crucial for Löb induction *)
499 500
     CWP c @ R {{ v,
        v = #true  U (CWP e @ R {{ _, U (CWP whileV (c) { e } @ R {{ Φ }})}})
Robbert Krebbers's avatar
Robbert Krebbers committed
501
       v = #false  U (Φ #()) }} -
502
    CWP whileV (c) { e } @ R {{ Φ }}.
503
  Proof.
504 505 506
    iIntros "H". cwp_lam. cwp_pures. rewrite /c_if -lock. cwp_pures.
    cwp_apply (cwp_wp with "H"). iIntros (v) "H". cwp_lam. cwp_pures.
    iApply cwp_seq_bind'. iApply (cwp_wand with "H").
507
    iIntros (v') "[[-> H] | [-> H]] !> !>".
508
    - cwp_pures. iApply cwp_seq_bind'.
509
      iApply (cwp_wand with "H"); iIntros (w) "H !> !>". by cwp_lam.
510
    - cwp_pures. iApply cwp_ret. by iApply wp_value.
511 512
  Qed.

513
  Lemma cwp_whileV_inv I R Φ c e :
Dan Frumin's avatar
Dan Frumin committed
514
    I -
515 516 517
     (I - CWP c @ R {{ v, (v = #false  U (Φ #())) 
                            (v = #true  U (CWP e @ R {{ _, U I }})) }}) -
    CWP whileV (c) { e } @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
518 519
  Proof.
    iIntros "HI #Hinv". iLöb as "IH".
520 521
    iApply cwp_whileV. iNext.
    iSpecialize ("Hinv" with "HI"). iApply (cwp_wand with "Hinv").
Dan Frumin's avatar
Dan Frumin committed
522 523
    iIntros (v) "[[-> H]|[-> H]] /="; first by auto.
    iLeft. iSplit; first done. iModIntro.
524
    iApply (cwp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
525 526
  Qed.

527
  Lemma cwp_while_inv I R Φ c e :
Robbert Krebbers's avatar
Robbert Krebbers committed
528
    I -
529 530 531
     (I - CWP c @ R {{ v, (v = #false  U (Φ #())) 
                            (v = #true  U (CWP e @ R {{ _, U I }})) }}) -
    CWP while (c) { e } @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
532
  Proof.
533
    iIntros "HI #Hinv". iApply cwp_while. by iApply (cwp_whileV_inv with "HI Hinv").
Dan Frumin's avatar
Dan Frumin committed
534
  Qed.
535

536 537 538
  Lemma cwp_fun R Φ e mx v :
    CWP subst' mx v e @ R {{ λ w, U (Φ w) }} -
    CWP (λᶜ mx, e)%V v @ R {{ Φ }}.
539
  Proof.
540
    iIntros "H". cwp_lam. iApply cwp_seq_bind; simpl. cwp_lam.
541
    iApply (cwp_wand with "H"); iIntros (w) "H !> !>".
542
    by iApply cwp_ret; iApply wp_value.
543 544
  Qed.

545 546 547
  Lemma cwp_call R Ψ1 Ψ2 Φ ef ea :
    CWP ef @ R {{ Ψ1 }} -
    CWP ea @ R {{ Ψ2 }} -
Dan Frumin's avatar
Dan Frumin committed
548
    ( f a, Ψ1 f - Ψ2 a - R -  U (CWP f a {{ v, R  Φ v }})) -
549
    CWP call ef ea @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
550
  Proof.
551
    iIntros "H1 H2 H".
552 553 554
    cwp_apply (cwp_wp with "H2"); iIntros (vf) "H2".
    cwp_apply (cwp_wp with "H1"); iIntros (va) "H1".
    cwp_lam. cwp_pures.
Dan Frumin's avatar
Dan Frumin committed
555 556 557 558
    iApply cwp_bind. iApply (cwp_par with "H1 H2").
    iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2").
    cwp_pures. iApply cwp_atomic. iIntros "HR". iNext.
    iExists True%I. iSplitR; first done. cwp_pures.
Dan Frumin's avatar
Dan Frumin committed
559
    iSpecialize ("H" with "HR").
Dan Frumin's avatar
Dan Frumin committed
560
    iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro.
Dan Frumin's avatar
Dan Frumin committed
561
    cwp_pures.
562
    iApply (cwp_wand with "H"); eauto.
Dan Frumin's avatar
Dan Frumin committed
563 564
  Qed.

565 566 567
  Lemma cwp_un_op R Φ op e :
    CWP e @ R {{ v,  w, un_op_eval op v = Some w  Φ w }} -
    CWP c_un_op op e @ R {{ Φ }}.
568
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
    iIntros "H".
570 571 572
    cwp_apply (cwp_wp with "H"); iIntros (v) "HΦ"; cwp_lam; cwp_pures.
    iApply cwp_bind.
    iApply (cwp_wand with "HΦ"); iIntros (w) "HΦ"; cwp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
    iDestruct "HΦ" as (w0) "[% H]".
574
    iApply cwp_ret. by wp_op.
575 576
  Qed.

577 578 579
  Lemma cwp_ptr_plus R Φ Ψ2 e1 e2 :
    CWP e2 @ R {{ Ψ2 }} -
    CWP e1 @ R {{ v1,  v2, Ψ2 v2 -  cl (n : Z),
Robbert Krebbers's avatar
Robbert Krebbers committed
580 581
                        v1 = cloc_to_val cl  
                        v2 = #n  
Robbert Krebbers's avatar
Robbert Krebbers committed
582
                       Φ (cloc_to_val (cl + n)) }} -
583
    CWP c_ptr_plus e1 e2 @ R {{ Φ }}.
584
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
    iIntros "He2 HΦ".
586 587 588 589
    cwp_apply (cwp_wp with "He2"); iIntros (a2) "Ha2".
    cwp_apply (cwp_wp with "HΦ"); iIntros (a1) "Ha1". cwp_lam; cwp_pures.
    iApply cwp_bind. iApply (cwp_par with "Ha1 Ha2").
    iIntros "!>" (v1 v2) "Hv1 Hv2 !>". cwp_pures.
590 591
    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
    rewrite cloc_to_val_eq.
592
    cwp_pures. iApply cwp_ret. by iApply wp_value.
593 594
  Qed.

595 596 597
  Lemma cwp_ptr_lt R Φ Ψ1 e1 e2 :
    CWP e1 @ R {{ Ψ1 }} -
    CWP e2 @ R {{ v2,  v1, Ψ1 v1 -  p q,
Robbert Krebbers's avatar
Robbert Krebbers committed
598 599 600
                        v1 = cloc_to_val p  
                        v2 = cloc_to_val q  
                       Φ #(cloc_lt p q) }} -
601
    CWP c_ptr_lt e1 e2 @ R {{ Φ }}.
602
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
    iIntros "He1 HΦ".
604 605 606 607
    cwp_apply (cwp_wp with "HΦ"); iIntros (a2) "Ha2".
    cwp_apply (cwp_wp with "He1"); iIntros (a1) "Ha1". cwp_lam; cwp_pures.
    iApply cwp_bind. iApply (cwp_par with "Ha1 Ha2").
    iIntros "!>" (v1 v2) "Hv1 Hv2 !>". cwp_let.
608
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
609
    rewrite cloc_to_val_eq /cloc_lt /=. cwp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
    case_bool_decide as Hp; subst.
611 612
    - rewrite (bool_decide_true (#ql = #ql)) //. cwp_pures.
      iApply cwp_ret. by iApply wp_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
    - rewrite /= bool_decide_false; last congruence.
614
      cwp_if. iApply cwp_ret. by iApply wp_value.
615 616
  Qed.

617 618
  Lemma cwp_bin_op R Φ Ψ1 Ψ2 op e1 e2 :
    CWP e1 @ R {{ Ψ1 }} - CWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
619
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, cbin_op_eval op v1 v2 = Some w  Φ w) -
620
    CWP c_bin_op op e1 e2 @ R {{ Φ }}.
621 622 623
  Proof.
    iIntros "H1 H2 HΦ".
    destruct op as [op'| |].
624 625 626 627 628 629 630 631
    - cwp_apply (cwp_wp with "H2"); iIntros (v2) "HΨ2".
      cwp_apply (cwp_wp with "H1"); iIntros (v1) "HΨ1". cwp_lam; cwp_pures.
      iApply cwp_bind.
      iApply (cwp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
      iNext. iIntros (w1 w2) "HΨ1 HΨ2 !>". cwp_pures.
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w0 ?) "H". iApply cwp_ret. by wp_op.
    - iApply (cwp_ptr_plus with "H2").
      iApply (cwp_wand with "H1").
Robbert Krebbers's avatar
Robbert Krebbers committed
632 633
      iIntros (v1) "HΨ1"; iIntros (v2) "HΨ2".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
634
      destruct (cloc_of_val v1) as [cl|] eqn:Hcl; simplify_eq/=.
635
      destruct (int_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
636
      iExists cl,o. iFrame.
637 638
      rewrite -(cloc_to_of_val v1 cl) //.
      by destruct v2; repeat (case_match || simplify_eq/=).
639 640
    - iApply (cwp_ptr_lt with "H1").
      iApply (cwp_wand with "H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
641 642
      iIntros (v2) "HΨ2"; iIntros (v1) "HΨ1".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
643 644 645 646
      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) //.
647 648
  Qed.

649 650
  Lemma cwp_pre_bin_op R Φ Ψ1 Ψ2 e1 e2 op :
    CWP e1 @ R {{ Ψ1 }} - CWP e2 @ R {{ Ψ2 }} -
651
    ( v1 v2, Ψ1 v1 - Ψ2 v2 - R ={}=
Robbert Krebbers's avatar
Robbert Krebbers committed
652 653 654
       cl v w,  v1 = cloc_to_val cl  
                cl C v 
                 cbin_op_eval op v v2 = Some w  
655
                (cl C[LLvl] w ={}= R  Φ v)) -
656
    CWP c_pre_bin_op op e1 e2 @ R {{ Φ }}.
657
  Proof.
658
    iIntros "He1 He2 HΦ".
659 660 661 662
    cwp_apply (cwp_wp with "He2"); iIntros (a2) "Ha2".
    cwp_apply (cwp_wp with "He1"); iIntros (a1) "Ha1". cwp_lam; cwp_pures.
    iApply cwp_bind. iApply (cwp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". cwp_pures.
663 664 665
    iApply cwp_atomic. iIntros "HR !>".
    iExists True%I. iSplitR; first done. cwp_lam. cwp_pures.
    iMod ("HΦ" with "Hv1 Hv2 HR") as (cl v w ->) "(Hl & % & HΦ)".
666
    iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value.
Dan Frumin's avatar
Dan Frumin committed
667 668
    iIntros "HR !>". iExists cl, v; iFrame. iSplit; first done.
    iIntros "Hl !>". cwp_pures. iApply cwp_bind.
669
    iApply (cwp_store _ _
670
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
671 672 673
    - cwp_proj. iApply cwp_ret; by wp_value_head.
    - iApply (cwp_bin_op _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
        try (try cwp_proj; iApply cwp_ret; by wp_value_head).
Robbert Krebbers's avatar
Robbert Krebbers committed
674 675
      iIntros (? ? -> ->); eauto.
    - iIntros (? ? -> ->).
Dan Frumin's avatar
Dan Frumin committed
676
      iIntros "HR !>". iExists _, _; iFrame. iSplit; first done.
677 678
      iIntros "Hcl !>". cwp_seq. iMod ("HΦ" with "Hcl") as "[$ HΦ]".
      iApply cwp_ret; iApply wp_value. eauto.
679
  Qed.
Dan Frumin's avatar
Dan Frumin committed
680
End proofs.
681 682

(* Make sure that we only use the provided rules and don't break the abstraction *)
Robbert Krebbers's avatar
Robbert Krebbers committed
683 684
Typeclasses Opaque c_alloc c_store c_load c_un_op c_bin_op c_pre_bin_op c_seq_bind c_if c_while c_call.
Global Opaque c_alloc c_store c_load c_un_op c_bin_op c_pre_bin_op c_seq_bind c_if c_while c_call.