translation.v 27.8 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
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
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
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");;
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229 230
  "ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;
  c_ret (Fst "lv") = c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;
  c_ret "ov".
231 232
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.
233

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

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

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

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

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

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

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

Dan Frumin's avatar
Dan Frumin committed
408 409 410 411 412 413 414 415 416 417 418 419
  (* Internal spec: breaks the abstraction/notation *)
  Lemma cwp_seq_bind' R Φ e (f: val) :
    CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -
    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.

420 421 422
  Lemma cwp_seq_bind R Φ x e1 e2 :
    CWP e1 @ R {{ v, U (CWP subst' x v e2 @ R {{ Φ }}) }} -
    CWP x ←ᶜ e1 ; e2 @ R {{ Φ }}.
423
  Proof.
424 425
    iIntros "H". cwp_pures. iApply cwp_seq_bind'.
    iApply (cwp_wand with "H"); iIntros (v) "H !>". by cwp_lam.
426 427
  Qed.

428
  (* Internal spec: breaks the abstraction/notation *)
429 430
  Lemma cwp_mut_bind' R Φ e (f: val) :
    CWP e @ R {{ v, U ( cl,
431
      cl C v -
432 433
      CWP f (cloc_to_val cl) @ R {{ w,  v', cl C v'  Φ w }}) }} -
    CWP c_mut_bind e f @ R {{ Φ }}.
434 435
  Proof.
    iIntros "H".
436 437 438 439
    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.
440 441 442 443 444 445 446 447 448 449
    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 /=.
450 451 452
    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.
453 454 455 456 457 458 459 460
    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. }
461
    cwp_pures. iApply cwp_ret. by iApply wp_value.
462 463
  Qed.

464 465
  Lemma cwp_mut_bind R Φ x e1 e2 :
    CWP e1 @ R {{ v, U ( cl,
466
      cl C v -
467 468
      CWP subst' x (cloc_to_val cl) e2 @ R {{ w,  v', cl C v'  Φ w }}) }} -
    CWP x mut e1 ; e2 @ R {{ Φ }}.
469
  Proof.
470 471 472
    iIntros "H". cwp_pures. iApply cwp_mut_bind'.
    iApply (cwp_wand with "H"); iIntros (v) "H !>"; iIntros (cl) "Hcl".
    cwp_lam. by iApply "H".
473 474
  Qed.

475 476 477 478
  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 {{ Φ }}.
479
  Proof.
480 481 482 483
    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.
484 485
  Qed.

486 487 488 489
  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
490

491
  Lemma cwp_whileV R Φ c e :
Robbert Krebbers's avatar
Robbert Krebbers committed
492
    (* The later is crucial for Löb induction *)
493 494
     CWP c @ R {{ v,
        v = #true  U (CWP e @ R {{ _, U (CWP whileV (c) { e } @ R {{ Φ }})}})
Robbert Krebbers's avatar
Robbert Krebbers committed
495
       v = #false  U (Φ #()) }} -
496
    CWP whileV (c) { e } @ R {{ Φ }}.
497
  Proof.
498 499 500
    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
501
    iIntros (v') "[[-> H] | [-> H]] !>".
502 503 504
    - 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.
505 506
  Qed.

507
  Lemma cwp_whileV_inv I R Φ c e :
Dan Frumin's avatar
Dan Frumin committed
508
    I -
509 510 511
     (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
512 513
  Proof.
    iIntros "HI #Hinv". iLöb as "IH".
514 515
    iApply cwp_whileV. iNext.
    iSpecialize ("Hinv" with "HI"). iApply (cwp_wand with "Hinv").
Dan Frumin's avatar
Dan Frumin committed
516 517
    iIntros (v) "[[-> H]|[-> H]] /="; first by auto.
    iLeft. iSplit; first done. iModIntro.
518
    iApply (cwp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
519 520
  Qed.

521
  Lemma cwp_while_inv I R Φ c e :
Robbert Krebbers's avatar
Robbert Krebbers committed
522
    I -
523 524 525
     (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
526
  Proof.
527
    iIntros "HI #Hinv". iApply cwp_while. by iApply (cwp_whileV_inv with "HI Hinv").
Dan Frumin's avatar
Dan Frumin committed
528
  Qed.
529

530 531 532
  Lemma cwp_fun R Φ e mx v :
    CWP subst' mx v e @ R {{ λ w, U (Φ w) }} -
    CWP (λᶜ mx, e)%V v @ R {{ Φ }}.
533
  Proof.
534 535 536
    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.
537 538
  Qed.

539 540 541 542 543
  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
544
  Proof.
545
    iIntros "H1 H2 H".
546 547 548
    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
549 550 551 552 553 554
    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.
    iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro.
    iSpecialize ("H" with "HR"). cwp_pures.
555
    iApply (cwp_wand with "H"); eauto.
Dan Frumin's avatar
Dan Frumin committed
556 557
  Qed.

558 559 560
  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 {{ Φ }}.
561
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
    iIntros "H".
563 564 565
    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
566
    iDestruct "HΦ" as (w0) "[% H]".
567
    iApply cwp_ret. by wp_op.
568 569
  Qed.

570 571 572
  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
573 574
                        v1 = cloc_to_val cl  
                        v2 = #n  
Robbert Krebbers's avatar
Robbert Krebbers committed
575
                       Φ (cloc_to_val (cl + n)) }} -
576
    CWP c_ptr_plus e1 e2 @ R {{ Φ }}.
577
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
    iIntros "He2 HΦ".
579 580 581 582
    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.
583 584
    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
    rewrite cloc_to_val_eq.
585
    cwp_pures. iApply cwp_ret. by iApply wp_value.
586 587
  Qed.

588 589 590
  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
591 592 593
                        v1 = cloc_to_val p  
                        v2 = cloc_to_val q  
                       Φ #(cloc_lt p q) }} -
594
    CWP c_ptr_lt e1 e2 @ R {{ Φ }}.
595
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
596
    iIntros "He1 HΦ".
597 598 599 600
    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.
601
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
602
    rewrite cloc_to_val_eq /cloc_lt /=. cwp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
    case_bool_decide as Hp; subst.
604 605
    - rewrite (bool_decide_true (#ql = #ql)) //. cwp_pures.
      iApply cwp_ret. by iApply wp_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
    - rewrite /= bool_decide_false; last congruence.
607
      cwp_if. iApply cwp_ret. by iApply wp_value.
608 609
  Qed.

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

642 643
  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
644
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
645 646 647
       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
648
                (cl C[LLvl] w - Φ v)) -
649
    CWP c_pre_bin_op op e1 e2 @ R {{ Φ }}.
650
  Proof.
651
    iIntros "He1 He2 HΦ".
652 653 654 655
    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.
Robbert Krebbers's avatar
Robbert Krebbers committed
656
    iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
657
    iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value.
658
    iExists cl, v; iFrame. iSplit; first done.
659 660
    iIntros "Hl". cwp_pures. iApply cwp_bind.
    iApply (cwp_store _ _
661
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
662 663 664
    - 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
665 666
      iIntros (? ? -> ->); eauto.
    - iIntros (? ? -> ->).
667
      iExists _, _; iFrame. iSplit; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
668
      iIntros "?". cwp_seq. iApply cwp_ret; iApply wp_value. by iApply "HΦ".
669
  Qed.
Dan Frumin's avatar
Dan Frumin committed
670
End proofs.
671 672

(* Make sure that we only use the provided rules and don't break the abstraction *)
Robbert Krebbers's avatar
Robbert Krebbers committed
673 674
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.