translation.v 24 KB
Newer Older
1
From iris.heap_lang Require Export proofmode notation.
2
From iris.heap_lang Require Import assert par.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.algebra Require Import frac auth.
4 5 6
From iris_c.lib Require Import mset flock list.
From iris_c.lib Require Export locking_heap U.
From iris_c.c_translation Require Export monad.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
From iris_c.c_translation Require Import proofmode.
8

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

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

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
Definition a_free_check : val :=
  rec: "go" "env" "l" "i" "n" :=
  if: "i" < "n" then
    assert: (mset_member ("l", "i") "env" = #false);;
    "go" "env" "l" (#1 + "i") "n"
  else #().

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

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

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

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

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

Robbert Krebbers's avatar
Nits.  
Robbert Krebbers committed
83
Definition a_seq_bind : val := λ: "f" "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85 86 87 88 89 90
  "a" ←ᶜ "x" ;;
  a_seq #() ;;
  "f" "a".
Notation "e1 ;ᶜ e2" :=
  (a_seq_bind (λ: <>, e2) e1)%E
  (at level 100, e2 at level 200,
   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
91 92

Definition a_if : val := λ: "cnd" "e1" "e2",
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97 98
  "c" ←ᶜ "cnd" ;;
  if: "c" then "e1" #() else "e2" #().
Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" :=
  (a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E)
  (at level 200, e1, e2, e3 at level 200,
   format "'ifᶜ'  ( e1 )  {  e2  }  'elseᶜ'  {  e3  }") : expr_scope.
99

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
100 101
Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105
    a_if ("cnd" #()) (λ: <>, "bdy" #() ; "while" "cnd" "bdy") a_seq%E.
Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
  (at level 200, e1, e2 at level 200,
   format "'whileᶜ'  ( e1 )  {  e2  }") : expr_scope.
106

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

114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
Inductive cbin_op :=
  | CBinOp : bin_op  cbin_op
  | PtrPlusOp : cbin_op
  | PtrLtOp : cbin_op.

(* TODO: move to locking_heap.v ?*)
Definition cloc_add_Z (l : loc) (o : Z) (o' : Z) : option cloc :=
  match o,o' with
  | Z0,Z0 => Some (l, O)
  | Z0,Zpos k => Some (l, Pos.to_nat k)
  | Zpos k,Z0 => Some (l, Pos.to_nat k)
  | Zpos k1,Zpos k2 => Some (l, Pos.to_nat k1 + Pos.to_nat k2)%nat
  | _,_ => None
  end.

Lemma cloc_add_Z_spec l o o' cl :
  cloc_add_Z l o o' = Some cl 
  cl.1 = l   n n', cl.2 = (n + n')%nat  Z.of_nat n = o  Z.of_nat n' = o'.
Proof.
  destruct o as [|o|], o' as [|o'|]; intros; simplify_eq/=; (split; first done).
  naive_solver.
  - exists 0%nat, (Pos.to_nat o'). eauto using positive_nat_Z.
  - exists (Pos.to_nat o),0%nat. eauto using positive_nat_Z.
  - exists (Pos.to_nat o),(Pos.to_nat o'). eauto using Pos2Nat.inj_add, positive_nat_Z.
Qed.

Definition cloc_lt_Z (l1 : loc) (o1 : Z) (l2 : loc) (o2 : Z) : option bool :=
  match o1,o2 with
  | Z0,Z0 => Some false
  | Z0,Zpos k => Some (bool_decide (l1 = l2))
  | Zpos k,Z0 => Some false
  | Zpos k1,Zpos k2 => Some (bool_decide (l1 = l2) && bool_decide (Pos.to_nat k1 < Pos.to_nat k2)%nat)
  | _,_ => None
  end.

Lemma cloc_lt_Z_spec l1 o1 l2 o2 b :
  cloc_lt_Z l1 o1 l2 o2 = Some b 
   n1 n2, Z.of_nat n1 = o1  Z.of_nat n2 = o2  cloc_lt (l1,n1) (l2,n2) = b.
Proof.
  rewrite /cloc_lt /=.
  destruct o1 as [|o1|], o2 as [|o2|]; intros; simplify_eq/=.
  - exists 0%nat,0%nat. repeat split; try done.
    repeat case_bool_decide; try done. inversion H0.
  - exists 0%nat, (Pos.to_nat o2).
    repeat split; try done; first eauto using positive_nat_Z.
    repeat case_bool_decide; try done. exfalso. eauto using Pos2Nat.is_pos.
  - exists (Pos.to_nat o1),0%nat.
    repeat split; try done; first eauto using positive_nat_Z.
    repeat case_bool_decide; try done. exfalso. inversion H0.
  - exists (Pos.to_nat o1),(Pos.to_nat o2).
    repeat split; eauto using positive_nat_Z.
Qed.

Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
  match op with
  | CBinOp op' => bin_op_eval op' v1 v2
  | PtrPlusOp =>
    match v1,v2 with
    | (LitV (LitLoc pl),LitV (LitInt po))%V,LitV (LitInt z) =>
      cloc_to_val <$> cloc_add_Z pl po z
    | _, _ => None
    end
  | PtrLtOp =>
    match v1,v2 with
    | (LitV (LitLoc pl),LitV (LitInt po))%V,
      (LitV (LitLoc ql),LitV (LitInt qo))%V =>
      (LitV  LitBool) <$> cloc_lt_Z pl po ql qo
    | _, _ => None
    end
  end.

185 186
Definition a_ptr_add : val := λ: "x" "y",
  "lo" ←ᶜ ("x" ||| "y");;
187
  let: "o'" := Snd (Fst "lo") + Snd "lo" in
188 189 190 191 192 193
  a_ret (Fst (Fst "lo"), "o'").

Definition a_ptr_lt : val := λ: "x" "y",
  "pq" ←ᶜ ("x" ||| "y");;
  let: "p" := Fst "pq" in
  let: "q" := Snd "pq" in
194
  if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false.
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225

Definition a_bin_op (op : cbin_op) : val :=
  match op with
  | CBinOp op' =>
    λ: "x1" "x2",
    "vv" ←ᶜ "x1" ||| "x2" ;;
    a_ret (BinOp op' (Fst "vv") (Snd "vv"))
  | PtrPlusOp => a_ptr_add
  | PtrLtOp   => a_ptr_lt
  end.

Notation "e1 +ᶜ e2" := (a_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op (CBinOp MinusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op (CBinOp MultOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op (CBinOp LeOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op (CBinOp LtOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op (CBinOp EqOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op (CBinOp EqOp) e1%E e2%E)) (at level 80): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.

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

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

Dan Frumin's avatar
Dan Frumin committed
227
Section proofs.
228
  Context `{amonadG Σ}.
Dan Frumin's avatar
Dan Frumin committed
229

Dan Frumin's avatar
Dan Frumin committed
230
  Lemma a_alloc_spec R Φ Ψ1 e1 e2 :
231
    AWP e1 @ R {{ Ψ1 }} -
Dan Frumin's avatar
Dan Frumin committed
232 233
    AWP e2 @ R {{ v2,  ( v1, Ψ1 v1 -  n : nat,
                           v1 = #n  
234
                           l, l C replicate n v2 - Φ (cloc_to_val l)) }} -
235
    AWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
236
  Proof.
Dan Frumin's avatar
Dan Frumin committed
237
    iIntros "H1 HΦ".
238
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
Dan Frumin's avatar
Dan Frumin committed
239
    awp_apply (a_wp_awp with "HΦ"); iIntros (v2) "H2". awp_lam.
240 241
    iApply awp_bind. iApply (awp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
Dan Frumin's avatar
Dan Frumin committed
242
    iDestruct ("H2" with "H1") as (n ->) "HΦ".
Dan Frumin's avatar
Dan Frumin committed
243
    iApply awp_atomic_env.
244 245 246 247
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
    iApply wp_fupd. wp_alloc l as "Hl".
    iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
248
    iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (l, 0%nat))].
249 250 251
    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.
252 253
  Qed.

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
254
  Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
255 256
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ Ψ2 }} -
257 258
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  cl w,
                 v1 = cloc_to_val cl   cl C w  (cl C[LLvl] v2 - Φ v2)) -
259
    AWP e1 = e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
260
  Proof.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
261
    iIntros "H1 H2 HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
262 263 264
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
    iApply awp_bind. iApply (awp_par with "H1 H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
265
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
266
    iDestruct ("HΦ" with "H1 H2") as ([l i] w ->) "[Hl HΦ]".
Dan Frumin's avatar
Dan Frumin committed
267
    iApply awp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
268 269
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1.
270 271 272
    assert ((#l, #i)%V  X).
    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
    iMod (locking_heap_store with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
273
    wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
274 275
    wp_apply (mset_add_spec with "[$]"); first done.
    iIntros "Hlocks /="; wp_seq.
276
    wp_load; wp_match.
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278 279 280 281
    wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
    iApply wp_fupd. wp_store.
    iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
    iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists ({[(#l, #i)%V]}  X), _. iFrame "Hσ". rewrite locked_locs_lock.
282 283 284
    iIntros "{$Hlocks} !%".
    intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
    eexists; split; [apply (cloc_of_to_val (l,i))|set_solver].
Dan Frumin's avatar
Dan Frumin committed
285 286
  Qed.

287
  Lemma a_load_spec_exists_frac R Φ e :
288 289
    AWP e @ R {{ v,  cl q w,  v = cloc_to_val cl  
                              cl C{q} w  (cl C{q} w - Φ w) }} -
290
    AWP ∗ᶜe @ R {{ Φ }}.
291
  Proof.
292 293
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
295
    iIntros (v). iDestruct 1 as ([l i] q w ->) "[Hl HΦ]". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
296 297 298
    iApply awp_atomic_env. iIntros (env) "Henv HR".
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv.
299 300 301
    assert ((#l, #i)%V  X).
    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
    iMod (locking_heap_load with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
302 303
    wp_let. wp_proj; wp_let. wp_proj; wp_let.
    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
304
    rewrite bool_decide_false //.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
    wp_op. iSplit; first done. iNext; wp_seq.
306
    wp_load; wp_match. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
307 308 309
    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists X, _. by iFrame.
310 311
  Qed.

312
  Lemma a_load_spec R Φ q e :
313 314 315
    AWP e @ R {{ v,  cl w,
                     v = cloc_to_val cl  
                    cl C{q} w  (cl C{q} w - Φ w) }} -
316
    AWP ∗ᶜe @ R {{ Φ }}.
317
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
    iIntros "H". iApply a_load_spec_exists_frac.
319
    awp_apply (awp_wand with "H").
320
    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
321 322 323
  Qed.

  Lemma a_un_op_spec R Φ e op:
324
    AWP e @ R {{ v,  w : val, un_op_eval op v = Some w  Φ w }} -
Dan Frumin's avatar
Dan Frumin committed
325
    AWP a_un_op op e @ R {{ Φ }}.
326 327 328 329 330 331 332 333 334 335 336
  Proof.
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam.
    iApply awp_bind.
    iApply (awp_wand with "HΦ"); iIntros (w) "HΦ"; awp_lam.
    iDestruct "HΦ" as (w0) "[% H]".
    iApply awp_ret. by wp_op.
  Qed.

  Lemma a_seq_spec R Φ :
    U (Φ #()) -
337
    AWP (a_seq #()) @ R {{ Φ }}.
338 339
  Proof.
    iIntros "HΦ". rewrite /a_seq. awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341 342
    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".
343
    iDestruct "HΦ" as (us) "[Hus HΦ]".
Dan Frumin's avatar
Dan Frumin committed
344
    iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
345 346
    - iModIntro. iSplitR "HΦ".
      + iExists , σ. by iFrame.
347 348
      + by iApply "HΦ".
    - iDestruct "Hus" as "[Hu Hus]".
Dan Frumin's avatar
Dan Frumin committed
349 350
      iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz].
      iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
351 352
      iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks").
      iIntros "Hus". iApply "HΦ". by iFrame.
353 354 355 356
  Qed.

  Lemma a_sequence_spec R Φ (f e : expr) :
    AsVal f 
357 358
     AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -
    AWP a_seq_bind f e @ R {{ Φ }}.
359
  Proof.
360
    iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
361 362 363 364 365 366
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
    iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
    awp_lam. iApply awp_bind. iApply a_seq_spec.
    iModIntro. by awp_lam.
  Qed.

367 368
  Lemma a_sequence_spec' R Φ (e e' : expr) :
    Closed [] e' 
369 370
     AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -
    AWP a_seq_bind (λ: <>, e') e @ R {{ Φ }}.
371 372 373 374 375 376 377
  Proof.
    iIntros (?) "He".
    iApply a_sequence_spec.
    iApply (awp_wand with "He"). iNext.
    iIntros (?) "He'". iModIntro. by awp_lam.
  Qed.

378
  Lemma a_while_spec  R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
Robbert Krebbers's avatar
Robbert Krebbers committed
379 380
     AWP a_if c (λ: <>, (λ: <>, b) #() ; while (c) { b }) a_seq @ R {{ Φ }} -
    AWP while (c) { b } @ R {{ Φ }}.
381 382 383 384 385 386 387
  Proof.
    iIntros "H".
    awp_lam. awp_lam. awp_seq.
    iApply "H".
  Qed.

  Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
Robbert Krebbers's avatar
Robbert Krebbers committed
388 389
    AsVal e1 
    AsVal e2 
390 391 392
    AWP e @ R {{ v, (v = #true  AWP e1 #() @ R {{ Φ }}) 
                    (v = #false  AWP e2 #() @ R {{ Φ }}) }} -
    AWP a_if e e1 e2 @ R {{ Φ }}.
393
  Proof.
394
    iIntros ([v1 <-] [v2 <-]) "H".
395 396 397 398 399
    awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
    iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
  Qed.

400
  Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
401 402 403
    AWP e @ R {{ v, (v = #true  AWP e1 @ R {{ Φ }}) 
                    (v = #false  AWP e2 @ R {{ Φ }}) }} -
    AWP if (e) { e1 } else { e2 } @ R {{ Φ }}.
404 405 406 407 408 409 410
  Proof.
    iIntros "He". iApply a_if_spec.
    iApply (awp_wand with "He").
    iIntros (v) "[[% Hv] | [% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto; by awp_lam.
  Qed.

  Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
411 412 413
     AWP c @ R {{ v, v = #true  AWP b @ R {{ _, U (AWP while (c) { b } @ R {{ Φ }}) }}
                     v = #false  AWP a_seq #() @ R {{ Φ }} }} -
    AWP while (c) { b } @ R {{ Φ }}.
414 415 416 417 418 419 420 421 422 423
  Proof.
    iIntros "H".
    awp_lam. awp_lam. awp_seq.
    iApply a_if_spec.
    iApply (awp_wand with "H").
    iIntros (v) "[[% Hv]|[% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto.
    awp_seq. iApply a_sequence_spec'. iNext.
    awp_seq. done.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
424
  Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) :
Dan Frumin's avatar
Dan Frumin committed
425
    IntoVal ef f 
426 427 428
    AWP ea @ R {{ Ψ }} -
    ( a, Ψ a - U (R -  R', R'  (AWP ef a @ R' {{ v, R' - R  Φ v }}))) -
    AWP a_invoke ef ea @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
429
  Proof.
430
    rewrite /IntoVal. iIntros (<-) "Ha Hfa".
Dan Frumin's avatar
Dan Frumin committed
431 432 433 434 435
    rewrite /a_invoke. awp_lam.
    awp_apply (a_wp_awp R with "Ha").
    iIntros (a) "Ha". awp_let.
    iApply a_sequence_spec.
    iApply (awp_wand with "Ha"). clear a.
436
    iNext. iIntros (a) "HΨ".
437 438
    iSpecialize ("Hfa" with "HΨ").
    iModIntro.
Dan Frumin's avatar
Dan Frumin committed
439
    awp_let.
Dan Frumin's avatar
Dan Frumin committed
440
    iApply awp_atomic. iNext. iIntros "HR".
Dan Frumin's avatar
Dan Frumin committed
441 442
    iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
    iExists R'. iFrame. by awp_let.
Dan Frumin's avatar
Dan Frumin committed
443 444
  Qed.

445
  Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
446 447
    AWP e1 @ R {{ Φ }} -
    AWP if (true) { e1 } else { e2 } @ R {{ Φ }}.
448 449 450 451 452 453
  Proof.
    iIntros "HΦ".
    iApply a_if_spec.
    iApply awp_ret. iApply wp_value.
    iLeft. iSplit; eauto. by awp_seq.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
454

455
  Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
456 457
    AWP e2 @ R {{ Φ }} -
    AWP if (false) { e1 } else { e2 } @ R {{ Φ }}.
458 459 460 461 462 463 464
  Proof.
    iIntros "HΦ".
    iApply a_if_spec.
    iApply awp_ret. iApply wp_value.
    iRight. iSplit; eauto. by awp_seq.
  Qed.

465 466 467 468 469
  Lemma a_ptr_add_spec R Φ Ψ2 e1 e2 :
    AWP e2 @ R {{ Ψ2 }} -
    AWP e1 @ R {{ v1,   v2, Ψ2 v2 -  cl (n : nat),
                          v1 = cloc_to_val cl  
                          v2 = #n  
470
                         Φ (cloc_to_val (cloc_add cl n)) }} -
471 472 473 474 475 476 477
    AWP a_ptr_add e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He2 HΦ". rewrite /a_ptr_add.
    awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
478 479 480
    iDestruct ("Hv1" with "Hv2") as ([l o] n -> ->) "HΦ /=".
    do 3 awp_proj. awp_op. awp_let. do 2 awp_proj.
    iApply awp_ret. iApply wp_value. by rewrite -Nat2Z.inj_add.
481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
  Qed.

  Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ v2,   v1, Ψ1 v1 -  p q,
                          v1 = cloc_to_val p  
                          v2 = cloc_to_val q  
                         Φ #(cloc_lt p q) }} -
    AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He1 HΦ". rewrite /a_ptr_add.
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
496 497 498 499
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
    do 2 (awp_proj; awp_let). do 2 awp_proj.
    unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op.
    - destruct Hp as [-> ?%Nat2Z.inj_lt].
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577
      rewrite (bool_decide_true (LitV pl = LitV pl)) //. awp_if. do 2 awp_proj.
      iApply awp_ret. wp_op.
      rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt.
    - rewrite bool_decide_false; last congruence.
      awp_if. iApply awp_ret. by iApply wp_value.
  Qed.

  Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : cbin_op) (e1 e2: expr) :
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, cbin_op_eval op v1 v2 = Some w  Φ w) -
    AWP a_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "H1 H2 HΦ".
    destruct op as [op'| |].
    - awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
      awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
      iApply awp_bind.
      iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
      iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
      iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
      iSpecialize ("HΦ" with "HΨ1 HΨ2").
      iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
    - iApply (a_ptr_add_spec with "H2").
      iApply (awp_wand with "H1").
      iIntros (v1) "HΨ1". iNext.
      iIntros (v2) "HΨ2". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
      destruct v1 as [ | |v11 v12| |],v2 as [|vl| | |]; simplify_eq/=;
      destruct v11 as [|[]| | |],v12 as [|[o| | |]| | |]; simplify_eq/=.
      destruct vl as [o'| | |]; simplify_eq/=.
      destruct (cloc_add_Z l o o') as [cl|] eqn:Hcl; simplify_eq/=.
      apply cloc_add_Z_spec in Hcl.
      destruct Hcl as [Hcl1 (n & n' & Hcl2 & Hn & Hn')]. simplify_eq/=.
      iExists (cl.1,n), n'. repeat iSplit; eauto.
      compute [cloc_add]. simpl. rewrite -Hcl2. iApply "HΦ".
    - iApply (a_ptr_lt_spec with "H1").
      iApply (awp_wand with "H2").
      iIntros (v2) "HΨ2". iNext.
      iIntros (v1) "HΨ1". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
      simpl in hop.
      destruct v1 as [ | |v11 v12| |],v2 as [| |v21 v22 | |]; simplify_eq;
      destruct v11 as [|[| | |l1]| | |],v12 as [|[o1| | |]| | |]; simplify_eq.
      destruct v21 as [|[| | |l2]| | |],v22 as [|[o2| | |]| | |]; simplify_eq/=.
      destruct (cloc_lt_Z l1 o1 l2 o2) as [b|] eqn:Hcl; simplify_eq/=.
      apply cloc_lt_Z_spec in Hcl.
      destruct Hcl as (n1 & n2 & Hn1 & Hn2 & Hlt). simplify_eq/=.
      iExists (l1,n1),(l2,n2). eauto.
  Qed.

  Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 - R -
         cl v w,  v1 = cloc_to_val cl  
                  cl C v 
                   cbin_op_eval op v v2 = Some w  
                  (cl C[LLvl] w - R  Φ v)) -
    AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
    iApply awp_atomic. iNext.
    iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
    simplify_eq/=. iExists True%I. rewrite left_id. awp_lam.
    iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head.
    iExists cl, v; iFrame. iSplit; first done.
    iIntros "Hl". awp_let. iApply awp_bind.
    iApply (a_store_spec _ _
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
    - awp_proj. iApply awp_ret; by wp_value_head.
    - iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
        try (try awp_proj; iApply awp_ret; by wp_value_head).
      iNext. iIntros (? ? -> ->). eauto.
    - iNext. iIntros (? ? -> ->).
      iExists _, _; iFrame. iSplit; first done.
      iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
      iIntros "_". by iApply "HΦ".
578 579
  Qed.

580 581
  Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
    I -
582
     (I - AWP c @ R {{ v, (v = #false  U (Φ #())) 
583
                            (v = #true   AWP b @ R {{ _, U I }}) }}) -
584
    AWP while (c) { b } @ R {{ Φ }}.
585 586 587 588 589 590 591 592
   Proof.
     iIntros "Hi #Hinv". iLöb as "IH".
     iApply a_while_spec. iNext.
     iApply a_if_spec.
     iSpecialize ("Hinv" with "Hi"). iApply (awp_wand with "Hinv").
     iIntros (v) "[(% & H) | (% & H)] //="; subst.
     - iRight. iSplit; by eauto; iApply a_seq_spec.
     - iLeft. iSplit; first eauto. awp_seq.
593
       iApply a_sequence_spec. iNext. awp_seq.
594
       iApply (awp_wand with "H").
595
       iIntros (v) "Hi !>". awp_seq.
596 597
       by iApply ("IH" with "Hi").
   Qed.
Dan Frumin's avatar
Dan Frumin committed
598
End proofs.
599 600

(* Make sure that we only use the provided rules and don't break the abstraction *)
601
Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
602
Global Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.