translation.v 21.4 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

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

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

18 19 20 21 22 23 24
Definition a_free_check : val :=
  rec: "go" "env" "l" "i" "n" :=
  if: "i" < "n" then
    assert: (mset_member ("l", "i") "env" = #false);;
    "go" "env" "l" (#1 + "i") "n"
  else #().

Dan Frumin's avatar
Dan Frumin committed
25 26 27 28 29
(* DF: following the discussion with Robbert, it seems that we cannot
   prove this function right now, because our ghost state cannot
   account that we hold permission for the *whole* array.
   
   See the RustBelt paper for the trick to make it work. *)
30 31 32
Definition a_free : val := λ: "x",
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
    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 *)
       | SOME "ll" =>
          (* We need to make sure `i = 0` and that all `0 ... length of block` are
          unlocked. TODO: this means we need to change the spec of `alloc` back so
          that we can actually establish we initially have the pointer to the first
          element of the array. *)
          assert: ("i" = #0);;
          let: "n" := llength "ll" in
          a_free_check "env" "ll" #0 "n";;
         "l" <- NONE
       end
50 51 52
    end
  ).

53
Definition a_store : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55
  "vv" ←ᶜ "x1" ||| "x2" ;;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59 60 61 62 63 64 65 66
    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 *)
       | SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v"
       end
67
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69
  ).
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
70 71

Definition a_load : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76 77 78 79 80 81 82 83
    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 *)
       | SOME "ll" => llookup "i" "ll"
       end
84
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87
  ).
Notation "∗ᶜ e" :=
  (a_load e)%E (at level 9, right associativity) : expr_scope.
88

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

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

Definition a_if : val := λ: "cnd" "e1" "e2",
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105
  (* sequenced binds needed here; there should be sequence point after the conditional *)
  "c" ←ᶜ "cnd" ;
Robbert Krebbers's avatar
Robbert Krebbers committed
106
  if: "c" then "e1" #() else "e2" #().
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110
Notation "'ifᶜ' ( cnd ) { e1 } 'elseᶜ' { e2 }" :=
  (a_if cnd%E (λ: <>, e1)%E (λ: <>, e2)%E)
  (at level 200, cnd, e1, e2 at level 200,
   format "'ifᶜ'  ( cnd )  {  e1  }  'elseᶜ'  {  e2  }") : expr_scope.
111

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
112 113
Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116
    if ("cnd" #()) { "bdy" #() ; "while" "cnd" "bdy" }
    else { skip }.
Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ: <>, e1)%E (λ: <>, e2)%E)
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118
  (at level 200, e1, e2 at level 200,
   format "'whileᶜ'  ( e1 )  {  e2  }") : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120
(* A version of while with value lambdas, this is an artifact because of the way
heap_lang works in Coq *)
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Notation "'whileVᶜ' ( e1 ) { e2 }" := (a_while (LamV <> e1)%V (LamV <> e2)%V)
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123
  (at level 200, e1, e2 at level 200,
   format "'whileVᶜ'  ( e1 )  {  e2  }") : expr_scope.
124

Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
Definition a_call: val := λ: "f" "arg",
  "a" ←ᶜ "arg" ; a_atomic (λ: <>, "f" "a").
127
Notation "'callᶜ' ( f , a )" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  (a_call f a)%E
129
  (at level 100, a at level 200,
130
   format "'callᶜ'  ( f ,  a )") : expr_scope.
131

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

135 136 137 138 139
Inductive cbin_op :=
  | CBinOp : bin_op  cbin_op
  | PtrPlusOp : cbin_op
  | PtrLtOp : cbin_op.

140
Definition a_ptr_plus : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
141
  (* all binds should be non-sequenced *)
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143 144 145 146
  "vv" ←ᶜ ("x" ||| "y");;
  match: Fst "vv" with
    NONE => assert #false (* null pointer *)
  | SOME "li" => a_ret (SOME (Fst "li", Snd "vv" + Snd "li"))
  end.
147 148

Definition a_ptr_lt : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  (* all binds should be non-sequenced *)
150
  "pq" ←ᶜ ("x" ||| "y");;
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154 155 156 157 158 159 160
  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"
        then a_ret (Snd "p" < Snd "q") else a_ret #false
     end
  end.
161 162

Definition a_bin_op (op : cbin_op) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  (* all binds should be non-sequenced *)
164
  match op with
165 166 167 168
  | CBinOp op' => λ: "x1" "x2",
     "vv" ←ᶜ "x1" ||| "x2" ;;
     a_ret (BinOp op' (Fst "vv") (Snd "vv"))
  | PtrPlusOp => a_ptr_plus
169 170
  | PtrLtOp   => a_ptr_lt
  end.
171 172 173 174 175 176 177 178 179 180 181
Notation "e1 +ᶜ e2" := (a_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 50) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op (CBinOp MinusOp) e1%E e2%E) (at level 35) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op (CBinOp MultOp) e1%E e2%E) (at level 40) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op (CBinOp LeOp) e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op (CBinOp LtOp) e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op (CBinOp EqOp) e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op (CBinOp EqOp) e1%E e2%E)) (at level 70): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 20, right associativity) : expr_scope.

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

183 184 185
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
186 187 188 189 190
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;
191
     o   int_of_val v2;
Robbert Krebbers's avatar
Robbert Krebbers committed
192
     Some (cloc_to_val (cl + o))
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197 198
  | PtrLtOp =>
     cl1  cloc_of_val v1;
     cl2  cloc_of_val v2;
     Some #(cloc_lt cl1 cl2)
  end.

199
Definition a_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  (* all binds should be non-sequenced *)
201 202 203 204 205 206 207
  "lv" ←ᶜ ("x" ||| "y");;
  a_atomic (λ: <>,
    "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
    a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
    a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +∗=ᶜ e2" := (a_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
208

Dan Frumin's avatar
Dan Frumin committed
209
Section proofs.
210
  Context `{amonadG Σ}.
Dan Frumin's avatar
Dan Frumin committed
211

212
  Lemma a_alloc_spec R Φ Ψ1 Ψ2 e1 e2 :
213
    AWP e1 @ R {{ Ψ1 }} -
214
    AWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
215 216 217
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  n : nat,
               v1 = #n    n  0%nat  
               l, l C replicate n v2 - Φ (cloc_to_val l)) -
218
    AWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
219
  Proof.
220
    iIntros "H1 H2 HΦ".
221 222
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2".
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
223
    awp_lam. awp_pures.
224
    iApply awp_bind. iApply (awp_par with "H1 H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
225
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_pures.
226
    iDestruct ("HΦ" with "H1 H2") as (n -> ?) "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228
    awp_apply wp_assert. wp_op. rewrite bool_decide_true; last lia.
    iSplit; first done. iNext. awp_pures.
Dan Frumin's avatar
Dan Frumin committed
229
    iApply awp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_pures.
231
    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
Robbert Krebbers's avatar
Robbert Krebbers committed
232
    wp_alloc l as "Hl".
233
    iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
    wp_pures. iIntros "!>". rewrite cloc_to_val_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
235 236 237 238 239
    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.
    - by iApply ("HΦ" $! (CLoc l 0)).
240 241
  Qed.

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
242
  Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
243 244
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  cl w,
               v1 = cloc_to_val cl   cl C w  (cl C[LLvl] v2 - Φ v2)) -
247
    AWP e1 = e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
248
  Proof.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
249
    iIntros "H1 H2 HΦ".
250 251
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2".
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
252
    awp_lam. awp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
    iApply awp_bind. iApply (awp_par with "H1 H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
254
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_pures.
255
    iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]".
Dan Frumin's avatar
Dan Frumin committed
256
    iApply awp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
258
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
259
    iDestruct (mapsto_offset_non_neg with "Hl") as %?.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
    assert ((#(cloc_base cl), #(cloc_offset cl))%V  X) as HclX.
261
    { intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
262
    iMod (full_locking_heap_store_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
263
    wp_pures. rewrite cloc_to_val_eq. wp_pures.
264
    wp_apply (mset_add_spec with "[$]"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
    iIntros "Hlocks /="; wp_pures.
266 267 268
    wp_load; wp_match.
    iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
    wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
Robbert Krebbers's avatar
Robbert Krebbers committed
269 270 271
    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
272
    iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]}  X), _.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
    iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
Dan Frumin's avatar
Dan Frumin committed
274 275
  Qed.

276
  Lemma a_load_spec_exists_frac R Φ e :
277 278
    AWP e @ R {{ v,  cl q w,  v = cloc_to_val cl  
                              cl C{q} w  (cl C{q} w - Φ w) }} -
279
    AWP ∗ᶜe @ R {{ Φ }}.
280
  Proof.
281
    iIntros "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
282
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. awp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
    iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". awp_pures.
285
    iDestruct (mapsto_offset_non_neg with "Hl") as %?.
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287
    iApply awp_atomic_env. iIntros (env) "Henv HR".
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
288
    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
    assert ((#(cloc_base cl), #(cloc_offset cl))%V  X) as HclX.
290
    { intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
291
    iMod (full_locking_heap_load_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
292
    wp_pures. rewrite cloc_to_val_eq. wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
294
    rewrite bool_decide_false //.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
    wp_op. iSplit; first done. iNext; wp_seq.
296 297 298
    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
299 300 301
    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists X, _. by iFrame.
302 303
  Qed.

304
  Lemma a_load_spec R Φ q e :
Robbert Krebbers's avatar
Robbert Krebbers committed
305 306
    AWP e @ R {{ v,  cl w,  v = cloc_to_val cl  
                            cl C{q} w  (cl C{q} w - Φ w) }} -
307
    AWP ∗ᶜe @ R {{ Φ }}.
308
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
    iIntros "H". iApply a_load_spec_exists_frac.
310
    awp_apply (awp_wand with "H").
311
    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
312 313
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316 317
  (* Internal spec: breaks the abstraction/notation *)
  Lemma a_seq_bind_spec' R Φ e (f: val) :
    AWP e @ R {{ v, U (AWP f v @ R {{ Φ }}) }} -
    AWP a_seq_bind e f @ R {{ Φ }}.
318 319
  Proof.
    iIntros "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
320 321 322
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. awp_pures.
    iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
    awp_pures. iApply awp_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
323 324 325
    iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
    iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
    wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
Robbert Krebbers's avatar
Robbert Krebbers committed
326
    iDestruct "H" as (us) "[Hus H]".
Dan Frumin's avatar
Dan Frumin committed
327
    iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
    - iModIntro. iSplitR "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
329
      + iExists , σ. by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
      + iNext. awp_lam. by iApply "H".
331
    - iDestruct "Hus" as "[Hu Hus]".
Robbert Krebbers's avatar
Robbert Krebbers committed
332
      iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz].
333
      iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
334 335
      iApply ("IH" with "Hus [H Hu] Hσ Hlocks").
      iIntros "Hus". iApply "H". by iFrame.
336 337
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
338
  Lemma a_seq_bind_spec R Φ x e1 e2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
339
    AWP e1 @ R {{ v, U (AWP subst' x v e2 @ R {{ Φ }}) }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
340
    AWP x ←ᶜ e1 ; e2 @ R {{ Φ }}.
341
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
342 343
    iIntros "H". awp_pures. iApply a_seq_bind_spec'.
    iApply (awp_wand with "H"); iIntros (v) "H !>". by awp_lam.
344 345
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
346 347 348 349
  Lemma a_if_spec R Φ c e1 e2 :
    AWP c @ R {{ v, (v = #true  U (AWP e1 @ R {{ Φ }})) 
                    (v = #false  U (AWP e2 @ R {{ Φ }})) }} -
    AWP if (c) { e1 } else { e2 } @ R {{ Φ }}.
350
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
351 352 353 354
    iIntros "H". rewrite /a_if -lock. awp_pures.
    awp_apply (a_wp_awp with "H"). iIntros (v) "H". awp_pures.
    iApply a_seq_bind_spec'. iApply (awp_wand with "H").
    iIntros (v') "[[-> ?] | [-> ?]] !>"; by awp_pures.
355 356
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
357 358 359
  Lemma a_while_spec R Φ c e :
    AWP whileV (c) { e } @ R {{ Φ }} -
    AWP while (c) { e } @ R {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
  Proof. iIntros "H". by awp_pures. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
361 362 363 364 365 366 367

  Lemma a_whileV_spec R Φ c e :
    (* The later is crucial for Löb induction *)
     AWP c @ R {{ v,
        v = #true  U (AWP e @ R {{ _, U (AWP whileV (c) { e } @ R {{ Φ }})}})
       v = #false  U (Φ #()) }} -
    AWP whileV (c) { e } @ R {{ Φ }}.
368
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
369 370 371 372
    iIntros "H". awp_lam. awp_pures. rewrite /a_if -lock. awp_pures.
    awp_apply (a_wp_awp with "H"). iIntros (v) "H". awp_lam. awp_pures.
    iApply a_seq_bind_spec'. iApply (awp_wand with "H").
    iIntros (v') "[[-> H] | [-> H]] !>".
Robbert Krebbers's avatar
Robbert Krebbers committed
373 374
    - awp_pures. iApply a_seq_bind_spec'.
      iApply (awp_wand with "H"); iIntros (w) "H !>". by awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
375
    - awp_pures. iApply awp_ret. by iApply wp_value.
376 377
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
378 379 380 381 382 383 384 385 386 387 388 389 390
  Lemma a_while_inv_spec I R Φ c e :
    I -
     (I - AWP c @ R {{ v, (v = #false  U (Φ #())) 
                            (v = #true  U (AWP e @ R {{ _, U I }})) }}) -
    AWP while (c) { e } @ R {{ Φ }}.
   Proof.
     iIntros "HI #Hinv". iApply a_while_spec. iLöb as "IH".
     iApply a_whileV_spec. iNext.
     iSpecialize ("Hinv" with "HI"). iApply (awp_wand with "Hinv").
     iIntros (v) "[[-> H]|[-> H]] /="; first by auto.
     iLeft. iSplit; first done. iModIntro.
     iApply (awp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
   Qed.
391

Robbert Krebbers's avatar
Robbert Krebbers committed
392
  Lemma a_call_spec R Ψ Φ (f : val) ea :
393
    AWP ea @ R {{ Ψ }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
394 395
    ( a, Ψ a - U (R -  R', R'  (AWP f a @ R' {{ v, R' - R  Φ v }}))) -
    AWP call (f, ea) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
396
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
397 398 399 400
    iIntros "Ha Hfa".
    awp_apply (a_wp_awp R with "Ha"); iIntros (va) "Ha". awp_lam. awp_pures.
    iApply a_seq_bind_spec'. iApply (awp_wand with "Ha").
    iIntros (a) "HΨ". iSpecialize ("Hfa" with "HΨ"). iModIntro. awp_pures.
Dan Frumin's avatar
Dan Frumin committed
401
    iApply awp_atomic. iNext. iIntros "HR".
Dan Frumin's avatar
Dan Frumin committed
402
    iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
Robbert Krebbers's avatar
Robbert Krebbers committed
403
    iExists R'. iFrame. by awp_pures.
Dan Frumin's avatar
Dan Frumin committed
404 405
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
406 407 408
  Lemma a_un_op_spec R Φ op e :
    AWP e @ R {{ v,  w, un_op_eval op v = Some w  Φ w }} -
    AWP a_un_op op e @ R {{ Φ }}.
409
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
410 411 412 413 414 415
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam; awp_pures.
    iApply awp_bind.
    iApply (awp_wand with "HΦ"); iIntros (w) "HΦ"; awp_lam.
    iDestruct "HΦ" as (w0) "[% H]".
    iApply awp_ret. by wp_op.
416 417
  Qed.

418
  Lemma a_ptr_plus_spec R Φ Ψ2 e1 e2 :
419
    AWP e2 @ R {{ Ψ2 }} -
420
    AWP e1 @ R {{ v1,  v2, Ψ2 v2 -  cl (n : Z),
Robbert Krebbers's avatar
Robbert Krebbers committed
421 422
                        v1 = cloc_to_val cl  
                        v2 = #n  
Robbert Krebbers's avatar
Robbert Krebbers committed
423
                       Φ (cloc_to_val (cl + n)) }} -
424
    AWP a_ptr_plus e1 e2 @ R {{ Φ }}.
425
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
    iIntros "He2 HΦ".
427
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2".
Robbert Krebbers's avatar
Robbert Krebbers committed
428 429 430
    awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam; awp_pures.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2").
    iIntros "!>" (v1 v2) "Hv1 Hv2 !>". awp_pures.
431 432
    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
    rewrite cloc_to_val_eq.
433
    awp_pures. iApply awp_ret. by iApply wp_value.
434 435 436 437
  Qed.

  Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
    AWP e1 @ R {{ Ψ1 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
438 439 440 441
    AWP e2 @ R {{ v2,  v1, Ψ1 v1 -  p q,
                        v1 = cloc_to_val p  
                        v2 = cloc_to_val q  
                       Φ #(cloc_lt p q) }} -
442 443
    AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
    iIntros "He1 HΦ".
445
    awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2".
Robbert Krebbers's avatar
Robbert Krebbers committed
446 447 448
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam; awp_pures.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2").
    iIntros "!>" (v1 v2) "Hv1 Hv2 !>". awp_let.
449
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451 452
    rewrite cloc_to_val_eq /cloc_lt /=. awp_pures.
    case_bool_decide as Hp; subst.
    - rewrite (bool_decide_true (#ql = #ql)) //. awp_pures.
453
      iApply awp_ret. by iApply wp_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
    - rewrite /= bool_decide_false; last congruence.
455 456 457
      awp_if. iApply awp_ret. by iApply wp_value.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
458
  Lemma a_bin_op_spec R Φ Ψ1 Ψ2 op e1 e2 :
459
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
460
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, cbin_op_eval op v1 v2 = Some w  Φ w) -
461 462 463 464
    AWP a_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "H1 H2 HΦ".
    destruct op as [op'| |].
465
    - awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2".
Robbert Krebbers's avatar
Robbert Krebbers committed
466
      awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam; awp_pures.
467 468
      iApply awp_bind.
      iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
Robbert Krebbers's avatar
Robbert Krebbers committed
469 470
      iNext. iIntros (w1 w2) "HΨ1 HΨ2 !>". awp_pures.
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w0 ?) "H". iApply awp_ret. by wp_op.
471
    - iApply (a_ptr_plus_spec with "H2").
472
      iApply (awp_wand with "H1").
Robbert Krebbers's avatar
Robbert Krebbers committed
473 474
      iIntros (v1) "HΨ1"; iIntros (v2) "HΨ2".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
475
      destruct (cloc_of_val v1) as [cl|] eqn:Hcl; simplify_eq/=.
476
      destruct (int_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
477
      iExists cl,o. iFrame.
478 479
      rewrite -(cloc_to_of_val v1 cl) //.
      by destruct v2; repeat (case_match || simplify_eq/=).
480 481
    - iApply (a_ptr_lt_spec with "H1").
      iApply (awp_wand with "H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483
      iIntros (v2) "HΨ2"; iIntros (v1) "HΨ1".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
484 485 486 487
      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) //.
488 489 490 491
  Qed.

  Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
Robbert Krebbers's avatar
Robbert Krebbers committed
492
    ( v1 v2, Ψ1 v1 - Ψ2 v2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
493 494 495
       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
496
                (cl C[LLvl] w - Φ v)) -
497 498
    AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
499
    iIntros "He1 He2 HΦ".
500
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2".
Robbert Krebbers's avatar
Robbert Krebbers committed
501
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam; awp_pures.
502
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
503 504
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_pures.
    iApply awp_atomic.
Robbert Krebbers's avatar
Robbert Krebbers committed
505 506
    iIntros "!> HR". iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
    simplify_eq/=. iExists True%I. iSplit; first done. awp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
    iApply awp_bind. iApply a_load_spec. iApply awp_ret. iApply wp_value.
508
    iExists cl, v; iFrame. iSplit; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
    iIntros "Hl". awp_pures. iApply awp_bind.
510 511 512 513 514
    iApply (a_store_spec _ _
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
    - awp_proj. iApply awp_ret; by wp_value_head.
    - iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
        try (try awp_proj; iApply awp_ret; by wp_value_head).
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516
      iIntros (? ? -> ->); eauto.
    - iIntros (? ? -> ->).
517
      iExists _, _; iFrame. iSplit; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
518
      iIntros "?". awp_seq. iApply awp_ret; iApply wp_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
519
      iIntros "_". iFrame "HR". by iApply "HΦ".
520
  Qed.
Dan Frumin's avatar
Dan Frumin committed
521
End proofs.
522 523

(* Make sure that we only use the provided rules and don't break the abstraction *)
Robbert Krebbers's avatar
Robbert Krebbers committed
524 525
Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq_bind a_if a_while a_call.
Global Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq_bind a_if a_while a_call a_ret.