translation.v 27.6 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.
Léon Gondelman's avatar
Léon Gondelman committed
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.
Léon Gondelman's avatar
Léon Gondelman committed
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.
Léon Gondelman's avatar
Léon Gondelman committed
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.
Léon Gondelman's avatar
Léon Gondelman committed
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 (λ: "env", mset_clear "env") ;;
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",
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
  (* sequence point at the end of a function *)
  "v" ←ᶜ f "arg" ;
141
  c_ret "v".
Robbert Krebbers's avatar
Robbert Krebbers committed
142
(* TODO: Similar notation for recursive functions *)
143
Notation "'λᶜ' x , e" := (c_fun (λ: x, e)%V)
Robbert Krebbers's avatar
Robbert Krebbers committed
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 149
  (* sequence point before a function call *)
  "fa" ←ᶜ ("f" ||| "arg");
150
  c_atomic (λ: <>, (Fst "fa") (Snd "fa")).
151
Notation "'callᶜ' f a" :=
152
  (c_call f a)%E
153 154
  (at level 10, f, a at level 9,
   format "'callᶜ'  f  a") : expr_scope.
155

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

159 160 161 162 163
Inductive cbin_op :=
  | CBinOp : bin_op  cbin_op
  | PtrPlusOp : cbin_op
  | PtrLtOp : cbin_op.

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

172
Definition c_ptr_lt : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  (* all binds should be non-sequenced *)
Dan Frumin's avatar
Dan Frumin committed
174
  "pq" ←ᶜ ("x" ||| "y");;
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176 177 178 179 180 181
  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"
182
        then c_ret (Snd "p" < Snd "q") else c_ret #false
Robbert Krebbers's avatar
Robbert Krebbers committed
183 184
     end
  end.
185

186
Definition c_bin_op (op : cbin_op) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  (* all binds should be non-sequenced *)
188
  match op with
189 190
  | CBinOp op' => λ: "x1" "x2",
     "vv" ←ᶜ "x1" ||| "x2" ;;
191 192 193
     c_ret (BinOp op' (Fst "vv") (Snd "vv"))
  | PtrPlusOp => c_ptr_plus
  | PtrLtOp   => c_ptr_lt
194
  end.
195 196 197 198 199 200 201 202 203 204 205
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.
206

207 208 209
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
210 211 212 213 214
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;
215
     o   int_of_val v2;
Robbert Krebbers's avatar
Robbert Krebbers committed
216
     Some (cloc_to_val (cl + o))
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218 219 220 221 222
  | PtrLtOp =>
     cl1  cloc_of_val v1;
     cl2  cloc_of_val v2;
     Some #(cloc_lt cl1 cl2)
  end.

223
Definition c_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
224
  (* all binds should be non-sequenced *)
225
  "lv" ←ᶜ ("x" ||| "y");;
226 227 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").
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.
232

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

236 237 238
  Lemma cwp_alloc R Φ Ψ1 Ψ2 e1 e2 :
    CWP e1 @ R {{ Ψ1 }} -
    CWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
239 240
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  n : nat,
               v1 = #n    n  0%nat  
241
               cl, block_info cl true n - cl C replicate n v2 - Φ (cloc_to_val cl)) -
242
    CWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
243
  Proof.
244
    iIntros "H1 H2 HΦ".
245 246 247 248 249
    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.
250
    iDestruct ("HΦ" with "H1 H2") as (n -> ?) "HΦ".
251 252 253
    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
254
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_pures.
255
    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
Robbert Krebbers's avatar
Robbert Krebbers committed
256
    wp_alloc l as "Hl".
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
257 258 259 260
    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
261 262 263 264
    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
265 266 267
    - iApply ("HΦ" $! (CLoc l 0) with "Hinfo Hl").
  Qed.

268 269
  Lemma cwp_free R Φ e :
    CWP e @ R {{ v,  cl ws,  v = cloc_to_val cl  
270
                             block_info cl true (length ws)  cl C ws  Φ #() }} -
271
    CWP free(e) @ R {{ Φ }}.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
272 273
  Proof.
    iIntros "H".
274 275 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.
    iIntros (v). iDestruct 1 as (cl ws ->) "(Hinfo & Hcl & HΦ)". cwp_pures.
    iApply cwp_atomic_env. iIntros (env) "Henv HR". wp_pures.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
278 279 280 281 282 283 284 285 286
    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.
287 288 289
    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
290
    iAssert ( Ψ (n : nat),  n  length ws  
291
      (is_mset env X - Ψ #()) - WP c_free_check env #(cloc_base cl) #n {{ Ψ }})%I
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311
      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.
    iIntros "!> {$HΦ $HR}". 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. 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.
312 313
  Qed.

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

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

376 377
  Lemma cwp_load R Φ q e :
    CWP e @ R {{ v,  cl w,  v = cloc_to_val cl  
Robbert Krebbers's avatar
Robbert Krebbers committed
378
                            cl C{q} w  (cl C{q} w - Φ w) }} -
379
    CWP ∗ᶜe @ R {{ Φ }}.
380
  Proof.
381 382
    iIntros "H". iApply cwp_load_exists_frac.
    cwp_apply (cwp_wand with "H").
383
    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
384 385
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
386
  (* Internal spec: breaks the abstraction/notation *)
387 388 389
  Lemma cwp_seq_bind' R Φ e (f: val) :
    CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -
    CWP c_seq_bind e f @ R {{ Φ }}.
390 391
  Proof.
    iIntros "H".
392 393 394 395
    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_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
Robbert Krebbers's avatar
Robbert Krebbers committed
396 397
    iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
    wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
Robbert Krebbers's avatar
Robbert Krebbers committed
398
    rewrite U_eq. iDestruct "H" as (us) "[Hus H]".
Dan Frumin's avatar
Dan Frumin committed
399
    iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
400
    - iModIntro. iSplitR "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
401
      + iExists , σ. by iFrame.
402
      + iNext. cwp_lam. by iApply "H".
403
    - iDestruct "Hus" as "[Hu Hus]".
Robbert Krebbers's avatar
Robbert Krebbers committed
404
      iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz].
405
      iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
406 407
      iApply ("IH" with "Hus [H Hu] Hσ Hlocks").
      iIntros "Hus". iApply "H". by iFrame.
408 409
  Qed.

410 411 412
  Lemma cwp_seq_bind R Φ x e1 e2 :
    CWP e1 @ R {{ v, U (CWP subst' x v e2 @ R {{ Φ }}) }} -
    CWP x ←ᶜ e1 ; e2 @ R {{ Φ }}.
413
  Proof.
414 415
    iIntros "H". cwp_pures. iApply cwp_seq_bind'.
    iApply (cwp_wand with "H"); iIntros (v) "H !>". by cwp_lam.
416 417
  Qed.

418
  (* Internal spec: breaks the abstraction/notation *)
419 420
  Lemma cwp_mut_bind' R Φ e (f: val) :
    CWP e @ R {{ v, U ( cl,
421
      cl C v -
422 423
      CWP f (cloc_to_val cl) @ R {{ w,  v', cl C v'  Φ w }}) }} -
    CWP c_mut_bind e f @ R {{ Φ }}.
424 425
  Proof.
    iIntros "H".
426 427 428 429
    cwp_apply (cwp_wp with "H"); iIntros (ev) "H". cwp_lam. cwp_pures.
    iApply cwp_seq_bind'; iApply (cwp_wand with "H"); iIntros (v) "H !>".
    cwp_pures. iApply cwp_bind.
    cwp_apply cwp_atomic_env; iIntros (env) "Henv $". iApply wp_fupd.
430 431 432 433 434 435 436 437 438 439
    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 /=.
440 441 442
    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.
443 444 445 446 447 448 449 450
    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. }
451
    cwp_pures. iApply cwp_ret. by iApply wp_value.
452 453
  Qed.

454 455
  Lemma cwp_mut_bind R Φ x e1 e2 :
    CWP e1 @ R {{ v, U ( cl,
456
      cl C v -
457 458
      CWP subst' x (cloc_to_val cl) e2 @ R {{ w,  v', cl C v'  Φ w }}) }} -
    CWP x mut e1 ; e2 @ R {{ Φ }}.
459
  Proof.
460 461 462
    iIntros "H". cwp_pures. iApply cwp_mut_bind'.
    iApply (cwp_wand with "H"); iIntros (v) "H !>"; iIntros (cl) "Hcl".
    cwp_lam. by iApply "H".
463 464
  Qed.

465 466 467 468
  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 {{ Φ }}.
469
  Proof.
470 471 472 473
    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").
    iIntros (v') "[[-> ?] | [-> ?]] !>"; by cwp_pures.
474 475
  Qed.

476 477 478 479
  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
480

481
  Lemma cwp_whileV R Φ c e :
Robbert Krebbers's avatar
Robbert Krebbers committed
482
    (* The later is crucial for Löb induction *)
483 484
     CWP c @ R {{ v,
        v = #true  U (CWP e @ R {{ _, U (CWP whileV (c) { e } @ R {{ Φ }})}})
Robbert Krebbers's avatar
Robbert Krebbers committed
485
       v = #false  U (Φ #()) }} -
486
    CWP whileV (c) { e } @ R {{ Φ }}.
487
  Proof.
488 489 490
    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").
Robbert Krebbers's avatar
Robbert Krebbers committed
491
    iIntros (v') "[[-> H] | [-> H]] !>".
492 493 494
    - cwp_pures. iApply cwp_seq_bind'.
      iApply (cwp_wand with "H"); iIntros (w) "H !>". by cwp_lam.
    - cwp_pures. iApply cwp_ret. by iApply wp_value.
495 496
  Qed.

497
  Lemma cwp_whileV_inv I R Φ c e :
Dan Frumin's avatar
Dan Frumin committed
498
    I -
499 500 501
     (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
502 503
  Proof.
    iIntros "HI #Hinv". iLöb as "IH".
504 505
    iApply cwp_whileV. iNext.
    iSpecialize ("Hinv" with "HI"). iApply (cwp_wand with "Hinv").
Dan Frumin's avatar
Dan Frumin committed
506 507
    iIntros (v) "[[-> H]|[-> H]] /="; first by auto.
    iLeft. iSplit; first done. iModIntro.
508
    iApply (cwp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
509 510
  Qed.

511
  Lemma cwp_while_inv I R Φ c e :
Robbert Krebbers's avatar
Robbert Krebbers committed
512
    I -
513 514 515
     (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
516
  Proof.
517
    iIntros "HI #Hinv". iApply cwp_while. by iApply (cwp_whileV_inv with "HI Hinv").
Dan Frumin's avatar
Dan Frumin committed
518
  Qed.
519

520 521 522
  Lemma cwp_fun R Φ e mx v :
    CWP subst' mx v e @ R {{ λ w, U (Φ w) }} -
    CWP (λᶜ mx, e)%V v @ R {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
523
  Proof.
524 525 526
    iIntros "H". cwp_lam. iApply cwp_seq_bind; simpl. cwp_lam.
    iApply (cwp_wand with "H"); iIntros (w) "H !>".
    by iApply cwp_ret; iApply wp_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528
  Qed.

529 530 531 532 533
  Lemma cwp_call R Ψ1 Ψ2 Φ ef ea :
    CWP ef @ R {{ Ψ1 }} -
    CWP ea @ R {{ Ψ2 }} -
    ( f a, Ψ1 f - Ψ2 a - U (R -  CWP f a {{ v, R  Φ v }})) -
    CWP call ef ea @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
534
  Proof.
535
    iIntros "H1 H2 H".
536 537 538 539
    cwp_apply (cwp_wp with "H2"); iIntros (vf) "H2".
    cwp_apply (cwp_wp with "H1"); iIntros (va) "H1".
    cwp_lam. cwp_pures.
    iApply cwp_seq_bind'. iApply (cwp_par with "H1 H2").
540
    iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2"); iModIntro.
541 542 543 544
    cwp_pures.
    iApply cwp_atomic. iIntros "HR". iSpecialize ("H" with "HR").
    iExists True%I. iModIntro; iSplit; first done. cwp_pures.
    iApply (cwp_wand with "H"); eauto.
Dan Frumin's avatar
Dan Frumin committed
545 546
  Qed.

547 548 549
  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 {{ Φ }}.
550
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
551
    iIntros "H".
552 553 554
    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
555
    iDestruct "HΦ" as (w0) "[% H]".
556
    iApply cwp_ret. by wp_op.
557 558
  Qed.

559 560 561
  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
562 563
                        v1 = cloc_to_val cl  
                        v2 = #n  
Robbert Krebbers's avatar
Robbert Krebbers committed
564
                       Φ (cloc_to_val (cl + n)) }} -
565
    CWP c_ptr_plus e1 e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
566
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
    iIntros "He2 HΦ".
568 569 570 571
    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.
572 573
    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
    rewrite cloc_to_val_eq.
574
    cwp_pures. iApply cwp_ret. by iApply wp_value.
Dan Frumin's avatar
Dan Frumin committed
575 576
  Qed.

577 578 579
  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
580 581 582
                        v1 = cloc_to_val p  
                        v2 = cloc_to_val q  
                       Φ #(cloc_lt p q) }} -
583
    CWP c_ptr_lt e1 e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
584
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
    iIntros "He1 HΦ".
586 587 588 589
    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.
590
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
591
    rewrite cloc_to_val_eq /cloc_lt /=. cwp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
592
    case_bool_decide as Hp; subst.
593 594
    - rewrite (bool_decide_true (#ql = #ql)) //. cwp_pures.
      iApply cwp_ret. by iApply wp_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
    - rewrite /= bool_decide_false; last congruence.
596
      cwp_if. iApply cwp_ret. by iApply wp_value.
597 598
  Qed.

599 600
  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
601
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, cbin_op_eval op v1 v2 = Some w  Φ w) -
602
    CWP c_bin_op op e1 e2 @ R {{ Φ }}.
603 604 605
  Proof.
    iIntros "H1 H2 HΦ".
    destruct op as [op'| |].
606 607 608 609 610 611 612 613
    - 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
614 615
      iIntros (v1) "HΨ1"; iIntros (v2) "HΨ2".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
616
      destruct (cloc_of_val v1) as [cl|] eqn:Hcl; simplify_eq/=.
617
      destruct (int_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
618
      iExists cl,o. iFrame.
619 620
      rewrite -(cloc_to_of_val v1 cl) //.
      by destruct v2; repeat (case_match || simplify_eq/=).
621 622
    - iApply (cwp_ptr_lt with "H1").
      iApply (cwp_wand with "H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
623 624
      iIntros (v2) "HΨ2"; iIntros (v1) "HΨ1".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
625 626 627 628
      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) //.
629 630
  Qed.

631 632
  Lemma cwp_pre_bin_op R Φ Ψ1 Ψ2 e1 e2 op :
    CWP e1 @ R {{ Ψ1 }} - CWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
633
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
634 635 636
       cl v w,  v1 = cloc_to_val cl  
                cl C v 
                 cbin_op_eval op v v2 = Some w  
Robbert Krebbers's avatar
Robbert Krebbers committed
637
                (cl C[LLvl] w - Φ v)) -
638
    CWP c_pre_bin_op op e1 e2 @ R {{ Φ }}.
639
  Proof.
640
    iIntros "He1 He2 HΦ".
641 642 643 644 645
    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.
    iApply cwp_atomic.
646
    iIntros "$ !>". iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
647 648
    simplify_eq/=. iExists True%I. iSplit; first done. cwp_pures.
    iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value.
649
    iExists cl, v; iFrame. iSplit; first done.
650 651
    iIntros "Hl". cwp_pures. iApply cwp_bind.
    iApply (cwp_store _ _
652
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
653 654 655
    - 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
656 657
      iIntros (? ? -> ->); eauto.
    - iIntros (? ? -> ->).
658
      iExists _, _; iFrame. iSplit; first done.
659
      iIntros "?". cwp_seq. iApply cwp_ret; iApply wp_value.
660
      iIntros "_". by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
661
  Qed.
Dan Frumin's avatar
Dan Frumin committed
662
End proofs.
Dan Frumin's avatar
Dan Frumin committed
663 664

(* Make sure that we only use the provided rules and don't break the abstraction *)
665 666
Typeclasses Opaque c_alloc c_store c_load c_un_op c_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_seq_bind c_if c_while c_call.