vcg.v 33.5 KB
Newer Older
1 2 3 4 5
From iris_c.c_translation Require Export translation.
From iris_c.vcgen Require Export forward.
From iris_c.lib Require Import Q.

Section vcg.
6
  Context `{cmonadG Σ}.
7 8 9 10 11 12 13 14 15 16 17

  Definition vcg_continuation (E: known_locs)
      (Φ : known_locs  denv  dval  iProp Σ) (v : val) : iProp Σ :=
    ( E' dv m',
       v = dval_interp E' dv  
       E `prefix_of` E'  
       denv_wf E' m' 
       dval_wf E' dv  
      denv_interp E' m' 
      Φ E' m' dv)%I.

18
  Definition vcg_cwp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr)
19
      (m: denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
20
    wand_denv_interp E m (CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}).
21 22 23 24 25 26 27 28 29

  Definition vcg_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match succ_nat_of_dval dv1 with
    | Some di =>
        cl,
         let i := length E in
         block_info cl true (S (Z.to_nat (dint_interp di))) -
         (cl + 1) C replicate (Z.to_nat (dint_interp di)) (dval_interp E dv2) -
Robbert Krebbers's avatar
Robbert Krebbers committed
30
         Φ (E ++ [cl]) (denv_insert i ULvl 1 dv2 m) (dLocV (dLoc i (dInt 0 None)))
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
    | _ =>
       wand_denv_interp E m ( n : nat,
          dval_interp E dv1 = #n    n  O    cl,
           block_info cl true n -
           cl C replicate n (dval_interp E dv2) -
           vcg_continuation E Φ (cloc_to_val cl))
    end%I.

  Definition vcg_load (E : known_locs) (dv : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match dloc_var_of_dval dv with
    | Some i =>
       match denv_lookup i m with
       | Some (_, dw) => Φ E m dw
       | None =>
         wand_denv_interp E m ( q v,
           dloc_var_interp E i C{q} v 
           (dloc_var_interp E i C[ULvl]{q} dval_interp E (dValUnknown v) -
           vcg_continuation E Φ v))
       end
    | None =>
       wand_denv_interp E m ( (cl : cloc) q v,
         dval_interp E dv = cloc_to_val cl 
         cl C{q} v  (cl C{q} v - vcg_continuation E Φ v))%I
    end%I.

  Definition vcg_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match dloc_var_of_dval dv1 with
    | Some i =>
       match denv_delete_full i m with
       | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
       | None =>
          wand_denv_interp E m ( v : val,
            dloc_var_interp E i C v 
            (dloc_var_interp E i C[LLvl] dval_interp E dv2 -
             vcg_continuation E Φ (dval_interp E dv2)))
       end
    | None =>
       wand_denv_interp E m ( (cl : cloc) (v : val),
         dval_interp E dv1 = cloc_to_val cl 
         cl C v 
         (cl C[LLvl] dval_interp E dv2 -
          vcg_continuation E Φ (dval_interp E dv2)))%I
    end%I.

  Definition vcg_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match dcbin_op_eval E op dv1 dv2 with
    | Some dw => Φ E m dw
    | None =>
       wand_denv_interp E m ( v,
          cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some v  
         vcg_continuation E Φ v)
    end%I.

  Definition vcg_un_op (E : known_locs) (op : un_op) (dv : dval)
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match dun_op_eval E op dv with
    | Some dw => Φ E m dw
    | None =>
       wand_denv_interp E m ( w,
         un_op_eval op (dval_interp E dv) = Some w 
         vcg_continuation E Φ w)
    end%I.

  Definition vcg_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match dloc_var_of_dval dv1 with
    | Some i =>
       match denv_delete_full i m with
       | Some (m', dw) =>
          match dcbin_op_eval E op dw dv2 with
          | Some dw' => Φ E (denv_insert i LLvl 1 dw' m') dw
          | None =>
             wand_denv_interp E m' $  w',
                cbin_op_eval op (dval_interp E dw) (dval_interp E dv2) = Some w' 
               (dloc_var_interp E i C[LLvl] w' - vcg_continuation E Φ (dval_interp E dw))
          end
       | None =>
          wand_denv_interp E m ( v w : val,
            dloc_var_interp E i C v 
             cbin_op_eval op v (dval_interp E dv2) = Some w  
            (dloc_var_interp E i C[LLvl] w - vcg_continuation E Φ v))
       end
    | None =>
       wand_denv_interp E m ( (cl : cloc) (v w : val),
         dval_interp E dv1 = cloc_to_val cl 
         cl C v 
         cbin_op_eval op v (dval_interp E dv2) = Some w 
         (cl C[LLvl] w - vcg_continuation E Φ v))
    end%I.

124 125 126 127
  Definition vcg_call (E : known_locs) (dv1 dv2 : dval)
      (m : denv) (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    (wand_denv_interp E m $ U (
       R -
128
        CWP (dval_interp E dv1) (dval_interp E dv2) {{ v, R  vcg_continuation E Φ v }}))%I.
129

130 131 132 133 134 135 136
  Fixpoint vcg (E : known_locs) (n : nat) (m : denv) (de : dcexpr)
      (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match de, n with
    | _, O => False
    | dCRet de', _ =>
       match dexpr_eval de' with
       | Some dv => Φ E m dv
137
       | None => vcg_cwp_continuation R E de m Φ
138 139 140 141 142 143 144 145
       end
    | dCSeqBind mx de1 de2, S n =>
       vcg E n m de1 R $ λ E m dv1,
         let i := length E in
         vcg E n (denv_unlock m) (dce_subst' E mx dv1 de2) R Φ
    | dCMutBind mx de1 de2, S n =>
       vcg E n m de1 R $ λ E m dv1,  cl,
         let i := length E in
Robbert Krebbers's avatar
Robbert Krebbers committed
146
         let dlv := dLocV (dLoc i (dInt 0 None)) in
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
         vcg (E ++ [cl]) n
           (denv_insert i ULvl 1 dv1 (denv_unlock m))
           (dce_subst' (E ++ [cl]) mx dlv de2) R $ λ E m dv2,
             match denv_delete_full i m with
             | Some (m', _) => Φ E m' dv2
             | _ => wand_denv_interp E m ( v,
                      cl C v  vcg_continuation E Φ (dval_interp E dv2))
             end
    | dCAlloc de1 de2, S n =>
       match forward E n m de1 with
       | Some (m', mNew, dv1) =>
          vcg E n m' de2 R $ λ E m'' dv2,
            vcg_alloc E dv1 dv2 (denv_merge mNew m'') Φ
       | None =>
          match forward E n m de2 with
          | Some (m', mNew, dv2) =>
             vcg E n m' de1 R $ λ E m'' dv1,
               vcg_alloc E dv1 dv2 (denv_merge mNew m'') Φ
165
          | None => vcg_cwp_continuation R E de m Φ
166 167 168 169 170 171 172 173 174 175 176 177 178 179
          end
        end
    | dCLoad de1, S n =>
       vcg E n m de1 R $ λ E m' dv, vcg_load E dv m' Φ
    | dCStore de1 de2, S n =>
       match forward E n m de1 with
       | Some (m', mNew, dv1) =>
          vcg E n m' de2 R $ λ E m'' dv2,
            vcg_store E dv1 dv2 (denv_merge mNew m'') Φ
       | None =>
          match forward E n m de2 with
          | Some (m', mNew, dv2) =>
             vcg E n m' de1 R $ λ E m'' dv1,
               vcg_store E dv1 dv2 (denv_merge mNew m'') Φ
180
          | None => vcg_cwp_continuation R E de m Φ
181 182 183 184 185 186 187 188 189 190 191 192
          end
       end
    | dCBinOp op de1 de2, S n =>
       match forward E n m de1 with
       | Some (m', mNew, dv1) =>
          vcg E n m' de2 R $ λ E m'' dv2,
            vcg_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ
       | None =>
          match forward E n m de2 with
          | Some (m', mNew, dv2) =>
             vcg E n m' de1 R $ λ E m'' dv1,
               vcg_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ
193
          | None => vcg_cwp_continuation R E de m Φ
194 195 196 197 198 199 200 201 202 203 204 205
          end
       end
    | dCPreBinOp op de1 de2, S n =>
       match forward E n m de1 with
       | Some (m', mNew, dv1) =>
          vcg E n m' de2 R $ λ E m'' dv2,
            vcg_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ
       | None =>
          match forward E n m de2 with
          | Some (m', mNew, dv2) =>
             vcg E n m' de1 R $ λ E m'' dv1,
               vcg_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ
206
          | None => vcg_cwp_continuation R E de m Φ
207 208 209 210 211 212 213 214 215 216 217 218 219 220
          end
       end
    | dCUnOp op de, S n =>
       vcg E n m de R $ λ E m dv, vcg_un_op E op dv m Φ
    | dCPar de1 de2, S n =>
       match forward E n m de1 with
       | Some (m', mNew, dv1) =>
          vcg E n m' de2 R $ λ E m'' dv2,
            (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))
       | None =>
          match forward E n m de2 with
          | Some (m', mNew, dv2) =>
             vcg E n m' de1 R $ λ E m'' dv1,
               (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))
221
          | None => vcg_cwp_continuation R E de m Φ
222 223
          end
       end
224
    | dCWhile de1 de2, S n => vcg_cwp_continuation R E (dCWhileV de1 de2) m Φ
225 226 227 228 229 230 231 232 233 234
    | dCCall de1 de2, S n =>
       match forward E n m de1 with
       | Some (m', mNew, dv1) =>
          vcg E n m' de2 R $ λ E m'' dv2,
            vcg_call E dv1 dv2 (denv_merge mNew m'') R Φ
       | None =>
          match forward E n m de2 with
          | Some (m', mNew, dv2) =>
             vcg E n m' de1 R $ λ E m'' dv1,
               vcg_call E dv1 dv2 (denv_merge mNew m'') R Φ
235
          | None => vcg_cwp_continuation R E de m Φ
236 237
          end
       end
238
    | _, S p => vcg_cwp_continuation R E de m Φ
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253
    end%I.

  Definition vcg_while (E : known_locs) (n : nat) (m : denv) (de : dcexpr)
      (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match de with
    | dCWhileV de1 de2 =>
        (vcg E n m de1 R $ λ E m dv1,
           match dknown_bool_of_dval dv1 with
           | Some true =>
              U (vcg E n (denv_unlock m) de2 R $ λ E m _,
                  U (vcg E n (denv_unlock m) (dCWhileV de1 de2) R Φ))
           | Some false => U (Φ E (denv_unlock m) (dLitV dLitUnit))
           | _ =>
              wand_denv_interp E m (
                dval_interp E dv1 = #true 
Robbert Krebbers's avatar
Robbert Krebbers committed
254 255
                (* FIXME, make sure that computation of vcg is blocked in the
                continuation. *)
256 257 258 259 260 261 262 263 264 265
                U (vcg_continuation E (λ E m dv,
                     vcg E n m (dCSeqBind <> de2 (dCWhileV de1 de2)) R Φ) #())
                 dval_interp E dv1 = #false 
                  U (vcg_continuation E Φ #()))
           end)
    | _ => vcg E n m de R Φ
    end%I.
End vcg.

Section vcg_spec.
266
  Context `{cmonadG Σ}.
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300

  Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|].
  Hint Extern 0 (0 < 1)%Q => reflexivity.
  Hint Resolve dknown_bool_of_dval_correct.
  Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct.
  Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop.
  Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct.
  Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct.
  Hint Resolve dce_subst_wf'.
  Hint Resolve denv_wf_dval_wf_lookup.
  Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock.
  Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full.
  Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2.
  Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2.
  Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2.
  Hint Resolve denv_wf_dval_wf_delete_full_2.
  Hint Resolve dexpr_eval_wf.
  Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward.

  Lemma vcg_continuation_correct Φ E m dv :
    denv_wf E m  dval_wf E dv 
    Φ E m dv - denv_interp E m -
    vcg_continuation E Φ (dval_interp E dv).
  Proof. iIntros (??) "H Hm". iExists E, dv, m. eauto with iFrame. Qed.

  Lemma vcg_continuation_mono E E' Φ w :
    E `prefix_of` E'  vcg_continuation E' Φ w - vcg_continuation E Φ w.
  Proof.
    iIntros (Hpre) "Hp".
    iDestruct "Hp" as (E1 dv m' ? Hpre1 ?) "(% & Hm' & H)"; simplify_eq /=.
    iExists E1, dv, m'; repeat (iSplit; first done).
    iSplit. iPureIntro. by trans E'. eauto with iFrame.
  Qed.

301
  Lemma vcg_cwp_continuation_correct R E m de Φ :
302
    denv_wf E m  denv_interp E m -
303 304
    vcg_cwp_continuation R E de m Φ -
    CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}.
305
  Proof.
306
    rewrite /vcg_cwp_continuation. iIntros (?) "Hm Hwp".
307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
    by iApply (wand_denv_interp_spec with "Hwp Hm").
  Qed.

  Lemma vcg_alloc_correct E m dv1 dv2 Φ :
    denv_wf E m  dval_wf E dv1  dval_wf E dv2 
    denv_interp E m -
    vcg_alloc E dv1 dv2 m Φ -
     n : nat, dval_interp E dv1 = #n   n  O%nat  
               ( cl, block_info cl true n -
                      cl C replicate n (dval_interp E dv2) -
                      vcg_continuation E Φ (cloc_to_val cl)).
  Proof.
    iIntros (???) "Hm H". rewrite /vcg_alloc.
    destruct (succ_nat_of_dval dv1) as [di|] eqn:?; last first.
    { iApply (wand_denv_interp_spec with "H Hm"). }
    iExists (S (Z.to_nat (dint_interp di))); simpl.
    iSplit; first by eauto using succ_nat_of_dval_Some.
    iSplit; first done. iIntros (cl) "Hinfo [Hcl Hcls]".
    assert (dloc_var_interp (E ++ [cl]) (length E) = cl) as Hcl.
    { by rewrite /dloc_var_interp (list_lookup_middle _ []). }
Robbert Krebbers's avatar
Robbert Krebbers committed
327
    iExists (E ++ [cl]), (dLocV (dLoc (length E) (dInt 0 None))),
328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434
      (denv_insert (length E) ULvl 1 dv2 m); simpl.
    iSplit; first by rewrite Hcl.
    iSplit; first by eauto using prefix_app_r.
    iSplit; first by eauto using denv_wf_insert_extend.
    iSplit.
    { by rewrite /dloc_wf /= /dloc_var_wf (list_lookup_middle _ []). }
    iSplitL "Hcl Hm"; last by iApply ("H" with "Hinfo Hcls").
    iApply denv_insert_interp; eauto using denv_wf_mono, prefix_app_r.
    iSplitL "Hm".
    { iApply (denv_interp_mono with "Hm"); eauto using prefix_app_r. }
    rewrite Hcl -(dval_interp_mono E (E ++ [cl])); eauto using prefix_app_r.
  Qed.

  Lemma vcg_load_correct E m dv Φ :
    denv_wf E m  denv_interp E m -
    vcg_load E dv m Φ -
     cl q w, dval_interp E dv = cloc_to_val cl 
              cl C{q} w  (cl C{q} w - vcg_continuation E Φ w).
  Proof.
    iIntros (?) "Hm H". rewrite /vcg_load.
    destruct (dloc_var_of_dval dv) as [i|] eqn:?; last first.
    { iApply (wand_denv_interp_spec with "H Hm"). }
    destruct (denv_lookup i m) as [[q dv'] |] eqn:?; simplify_eq /=.
    - destruct (denv_lookup_interp E i q dv' m) as [mf Hmf]=> //.
      iDestruct (Hmf with "Hm") as "[Hmf Hi]".
      iExists _, _, _; iFrame "Hi"; iSplit; first by eauto.
      iIntros "Hi". iDestruct (Hmf with "[$Hmf $Hi]") as "Hm".
      iApply (vcg_continuation_correct with "H"); eauto 10.
    - iDestruct (wand_denv_interp_spec with "H Hm") as (q v) "[Hi H]".
      iExists _, _, _; iFrame; eauto.
  Qed.

  Lemma vcg_store_correct E m dv1 dv2 Φ :
    denv_wf E m  dval_wf E dv1  dval_wf E dv2 
    denv_interp E m -
    vcg_store E dv1 dv2 m Φ -
     cl w, dval_interp E dv1 = cloc_to_val cl 
            cl C w 
            (cl C[LLvl] dval_interp E dv2 - vcg_continuation E Φ (dval_interp E dv2)).
  Proof.
    iIntros (???) "Hm H". rewrite /vcg_store.
    destruct (dloc_var_of_dval dv1) as [i|] eqn:?; last first.
    { iApply (wand_denv_interp_spec with "H Hm"). }
    destruct (denv_delete_full i m)  as [[m' dv_old]|] eqn:?; simplify_eq/=.
    - iDestruct (denv_delete_full_interp with "Hm") as "[Hm Hi]"; eauto.
      iExists _, _; iFrame "Hi"; iSplit; first by eauto. iIntros "Hi".
      iApply (vcg_continuation_correct with "H"); eauto.
      iApply denv_insert_interp; eauto with iFrame.
    - iDestruct (wand_denv_interp_spec with "H Hm") as (w) "[Hi H]".
      iExists _, _; iFrame "Hi"; eauto.
  Qed.

  Lemma vcg_bin_op_correct E m dv1 dv2 op Φ :
    denv_wf E m  dval_wf E dv1  dval_wf E dv2 
    denv_interp E m -
    vcg_bin_op E op dv1 dv2 m Φ -
     w, cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some w 
          vcg_continuation E Φ w.
  Proof.
    iIntros (???) "Hm H". rewrite /vcg_bin_op.
    destruct (dcbin_op_eval _ _ dv1 dv2) as [dw|] eqn:?; last first.
    { iApply (wand_denv_interp_spec with "H Hm"). }
    iExists _; iSplit; first by eauto.
    iApply (vcg_continuation_correct with "H"); eauto.
  Qed.

  Lemma vcg_pre_bin_op_correct E m op dv1 dv2 Φ :
    denv_wf E m  dval_wf E dv1  dval_wf E dv2 
    denv_interp E m -
    vcg_pre_bin_op E op dv1 dv2 m Φ -
     cl v w, dval_interp E dv1 = cloc_to_val cl  cl C v 
              cbin_op_eval op v (dval_interp E dv2) = Some w 
              (cl C[LLvl] w - vcg_continuation E Φ v).
  Proof.
    iIntros (???) "Hm H". rewrite /vcg_pre_bin_op.
    destruct (dloc_var_of_dval dv1) as [i|] eqn:?; last first.
    { iApply (wand_denv_interp_spec with "H Hm"). }
    destruct (denv_delete_full i m)  as [[m' dv_old]|] eqn:?; simplify_eq/=.
    - iDestruct (denv_delete_full_interp with "Hm") as "[Hm Hi]"; eauto.
      destruct (dcbin_op_eval _ _ dv_old dv2) as [dw|] eqn:?; last first.
      { iDestruct (wand_denv_interp_spec with "H Hm") as (w ?) "H".
        eauto 10 with iFrame. }
      iExists _, _, _; iFrame "Hi"; repeat (iSplit; first by eauto). iIntros "Hi".
      iApply (vcg_continuation_correct with "H"); eauto 10.
      iApply denv_insert_interp; eauto with iFrame.
    - iDestruct (wand_denv_interp_spec with "H Hm") as (w ?) "H".
      eauto 10 with iFrame.
  Qed.

  Lemma vcg_un_op_correct E m dv b Φ :
    dval_wf E dv  denv_wf E m 
    denv_interp E m -
    vcg_un_op E b dv m Φ -
     w, un_op_eval b (dval_interp E dv) = Some w 
         vcg_continuation E Φ w.
  Proof.
    iIntros (Hwf Hwf2) "Hm H". rewrite /vcg_un_op.
    destruct (dun_op_eval E b dv) as [dw|] eqn:?.
    - iExists _; iSplit; first by eauto.
      iApply (vcg_continuation_correct with "H"); eauto.
    - by iApply (wand_denv_interp_spec with "H Hm").
  Qed.

  Lemma vcg_correct R E m de Φ n :
    dcexpr_wf E de  denv_wf E m 
    denv_interp E m -
    vcg E n m de R Φ -
435
    CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}.
436 437 438 439 440 441 442
  Proof.
    iIntros (Hde Hm) "Hm H".
    iInduction n as [|n IH] "IH" forall (de Φ E m Hde Hm).
    { by destruct de. }
    destruct de; simplify_eq/=; destruct_and?.
    - (* return *)
      destruct (dexpr_eval _) as [dv1|] eqn:?; simplify_eq /=; last first.
443 444
      { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "$". } 
      iApply cwp_ret. iApply wp_wand; first by iApply dexpr_eval_correct.
445 446 447
      iIntros (v ->). iApply (vcg_continuation_correct with "H"); eauto.
    - (* bind *)
      iDestruct ("IH" with "[] [] Hm H") as "H"; eauto.
448
      iApply cwp_seq_bind. iApply (cwp_wand with "H").
449 450 451 452
      iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
      rewrite (dcexpr_interp_mono E E') // -dcexpr_interp_subst'.
      iDestruct ("IH" with "[] [] Hm H") as "H"; eauto using dcexpr_wf_mono.
453
      iApply (cwp_wand with "H"); iIntros (v) "H".
454 455 456
      by iApply (vcg_continuation_mono with "H").
    - (* mut bind *)
      iDestruct ("IH" with "[] [] Hm H") as "H"; eauto.
457
      iApply cwp_mut_bind. iApply (cwp_wand with "H").
458 459 460 461 462
      iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
      iIntros (cl) "Hcl". iSpecialize ("H" $! cl).
      assert (E' `prefix_of` E' ++ [cl]) by eauto using prefix_app_r.
      set (i := length E').
Robbert Krebbers's avatar
Robbert Krebbers committed
463
      set (dlv := dLocV (dLoc i (dInt 0 None))).
464
      assert (dval_wf (E' ++ [cl]) dlv).
Robbert Krebbers's avatar
Robbert Krebbers committed
465
      { rewrite /dlv /= /dloc_wf /= /dloc_var_wf.
466 467 468 469 470 471 472 473 474 475
        by rewrite (list_lookup_middle _ []). }
      iDestruct ("IH" with "[%] [%] [Hm Hcl] H") as "H".
      { eauto using dcexpr_wf_mono. }
      { eauto using denv_wf_insert_extend. }
      { iApply denv_insert_interp; eauto using denv_wf_mono.
        rewrite /dloc_var_interp (list_lookup_middle _ []) //=.
        rewrite -(denv_interp_mono E'); eauto.
        rewrite -(dval_interp_mono E'); eauto. iFrame. }
      rewrite dcexpr_interp_subst' /= /dloc_var_interp (list_lookup_middle _ []) //=.
      rewrite -(dcexpr_interp_mono E); eauto.
476
      iApply (cwp_wand with "H").
477 478 479 480 481 482 483 484 485 486 487 488
      iIntros (w) "H"; iDestruct "H" as (E'' dw m'' -> ???) "[Hm H]".
      destruct (denv_delete_full i m'') as [[m''' dw']|] eqn:?.
      + iDestruct (denv_delete_full_interp with "Hm") as "[Hm Hl]"; first done.
        rewrite -(dloc_var_interp_mono (E' ++ [cl])) /dloc_var_interp /=; eauto.
        rewrite (list_lookup_middle _ []) //=. iExists _; iFrame "Hl".
        iApply vcg_continuation_mono;
          [|iApply (vcg_continuation_correct with "H")]; eauto.
      + iDestruct (wand_denv_interp_spec with "H Hm") as (v) "[Hl H]".
        iExists _; iFrame "Hl". iApply (vcg_continuation_mono with "H"); eauto.
    - (* alloc *)
      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
      + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
489
        { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". }
490
        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
491
        iApply (cwp_alloc with "[H Hm'] H2").
492 493 494 495 496 497 498 499 500 501
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_alloc_correct with "[HmNew Hm''] H") as (n' ??) "H";
          eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        iExists _; repeat (iSplit; first done). iIntros (cl) "Hinfo Hcl".
        rewrite (dval_interp_mono E E'); eauto.
        by iApply vcg_continuation_mono; last by iApply ("H" with "Hinfo").
      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
502
        iApply (cwp_alloc with "H1 [H Hm']").
503 504 505 506 507 508 509 510 511 512
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_alloc_correct with "[HmNew Hm''] H") as (n' ??) "H";
          eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto.
        iExists _; repeat (iSplit; first done). iIntros (cl) "Hinfo Hcl".
        by iApply vcg_continuation_mono; last by iApply ("H" with "Hinfo").
    - (* load *)
513
      iApply cwp_load_exists_frac. iApply (cwp_wand with "[-]").
514 515 516 517 518 519 520 521
      { iApply ("IH" with "[] [] Hm H"); eauto. }
      iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
      iDestruct (vcg_load_correct with "Hm H") as (cl q w ?) "[Hi H]"; eauto.
      iExists _, _, _; iSplit; first done. iIntros "{$Hi} Hi".
      by iApply vcg_continuation_mono; last by iApply "H".
    - (* assign *)
      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
      + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
522
        { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". }
523
        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
524
        iApply (cwp_store with "[H Hm'] H2").
525 526 527 528 529 530 531 532 533 534
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_store_correct with "[HmNew Hm''] H") as (cl w ?) "[Hi H]";
          eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        iExists _, _; iSplit; first done. iIntros "{$Hi} Hi".
        rewrite (dval_interp_mono E E'); eauto.
        by iApply vcg_continuation_mono; last by iApply "H".
      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
535
        iApply (cwp_store with "H1 [H Hm']").
536 537 538 539 540 541 542 543 544 545 546 547
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_store_correct with "[HmNew Hm''] H") as (cl w ?) "[Hi H]";
          eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto.
        iExists _, _; iSplit; first done. iIntros "{$Hi} Hi".
        by iApply vcg_continuation_mono; last by iApply "H".
    - (* bin op *)
      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
      + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
548
        { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". }
549
        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
550
        iApply (cwp_bin_op with "[H Hm'] H2").
551 552 553 554 555 556 557 558 559
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_bin_op_correct with "[HmNew Hm''] H") as (w ?) "H";
          eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto.
        iExists _; iSplit; first done. by iApply vcg_continuation_mono.
      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
560
        iApply (cwp_bin_op with "H1 [H Hm']").
561 562 563 564 565 566 567 568 569 570 571
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_bin_op_correct with "[HmNew Hm''] H") as (w ?) "H";
          eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto.
        iExists _; iSplit; first done. by iApply vcg_continuation_mono.
    - (* pre bin op *)
      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
      + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
572
        { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". }
573
        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
574
        iApply (cwp_pre_bin_op with "[H Hm'] H2").
575 576 577 578 579 580 581 582 583 584
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_pre_bin_op_correct with "[HmNew Hm''] H")
          as (cl w ??) "(Hi & % & H)"; eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto.
        iExists _, _, _. iFrame "Hi". repeat (iSplit; first done).
        iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H".
      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
585
        iApply (cwp_pre_bin_op with "H1 [H Hm']").
586 587 588 589 590 591 592 593 594 595
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_pre_bin_op_correct with "[HmNew Hm''] H")
          as (cl w ??) "(Hi & % & H)"; eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto.
        iExists _, _, _. iFrame "Hi". repeat (iSplit; first done).
        iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H".
    - (* un op *)
596
      iApply cwp_un_op. iApply (cwp_wand with "[-]").
597 598 599 600 601 602 603
      { iApply ("IH" with "[] [] Hm H"); eauto. }
      iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
      iDestruct (vcg_un_op_correct with "Hm H") as (w ?) "H"; eauto.
      iExists _; iSplit; first by eauto. by iApply vcg_continuation_mono.
    - (* par *)
      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
      + destruct (forward _ _  m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
604
        { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". }
605
        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
606
        iApply (cwp_par with "[H Hm'] H2").
607 608 609 610 611 612 613 614 615
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros "!>" (v1 v2) "H [-> HmNew] !>";
          iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_continuation_correct with "H [Hm'' HmNew]") as "H";
          simpl; split_and?; eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto. by iApply vcg_continuation_mono.
      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
616
        iApply (cwp_par with "H1 [H Hm']").
617 618 619 620 621 622 623 624 625
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros "!>" (v1 v2) "[-> HmNew] H !>";
          iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (vcg_continuation_correct with "H [HmNew Hm'']") as "H";
          simpl; split_and?; eauto using denv_wf_mono, dval_wf_mono.
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        rewrite (dval_interp_mono E E'); eauto. by iApply vcg_continuation_mono.
    - (* while *)
626 627
      iApply cwp_while.
      iDestruct (vcg_cwp_continuation_correct with "Hm H") as "$"; eauto.
628
    - (* whileV *)
629
      by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?".
630
    - (* call *)
631 632
      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
      + destruct (forward _ _  m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
633
        { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". }
634
        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
635
        iApply (cwp_call with "[H Hm'] H2").
636 637 638 639 640 641 642 643
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (f a) "H [-> HmNew]";
          iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H".
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro.
        rewrite (dval_interp_mono E E'); eauto.
644
        iApply (cwp_wand with "H"); iIntros (w) "[$ H]".
645 646
        by iApply vcg_continuation_mono.
      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
647
        iApply (cwp_call with "H1 [H Hm']").
648 649 650 651 652 653 654 655
        { iApply ("IH" with "[] [] Hm' H"); eauto. }
        iIntros (f a) "[-> HmNew] H";
          iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
        iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H".
        { iApply denv_merge_interp; eauto using denv_wf_mono.
          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
        iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro.
        rewrite (dval_interp_mono E E'); eauto.
656
        iApply (cwp_wand with "H"); iIntros (w) "[$ H]".
657
        by iApply vcg_continuation_mono.
658
    - (* unknown *)
659
      by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?".
660 661 662 663 664 665 666
  Qed.

  Lemma vcg_while_correct R E m de Φ n :
    dcexpr_wf E de 
    denv_wf E m 
    denv_interp E m -
    vcg_while E n m de R Φ -
667
    CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}.
668 669
  Proof.
    destruct de; try apply vcg_correct; simpl.
670
    iIntros (??) "Hm H"; destruct_and?. iApply cwp_whileV; iNext.
671
    iDestruct (vcg_correct with "Hm H") as "H"; auto.
672
    iApply (cwp_wand with "H"); iIntros (v) "H".
673 674 675 676 677 678
    iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
    destruct (dknown_bool_of_dval _) as [[]|] eqn:?; simplify_eq/=.
    - iLeft. iSplit; first by eauto.
      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
      rewrite (dcexpr_interp_mono E E') //.
      iDestruct (vcg_correct with "Hm H") as "H"; eauto using dcexpr_wf_mono.
679
      iApply (cwp_wand with "H"); iIntros (v) "H".
680 681 682 683 684
      iDestruct "H" as (E'' dw m'' -> ???) "[Hm H]".
      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
      iDestruct (vcg_correct with "Hm H") as "H";
        simpl; split_and?; eauto using dcexpr_wf_mono.
      rewrite !(dcexpr_interp_mono _ E''); eauto using dcexpr_wf_mono.
685
      iApply (cwp_wand with "H"); iIntros (v) "H".
686 687 688 689 690 691 692 693 694 695 696 697 698
      iApply (vcg_continuation_mono with "H"); eauto.
    - iRight. iSplit; first by eauto.
      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
      iDestruct (vcg_continuation_correct with "H Hm") as "H"; eauto.
      iApply (vcg_continuation_mono with "H"); eauto.
    - iDestruct (wand_denv_interp_spec with "H Hm") as "[[% H]|[% H]]"; last first.
      { iRight. iSplit; first by eauto.
        iModIntro. iApply (vcg_continuation_mono with "H"); eauto. }
      iLeft. iSplit; first done. iModIntro.
      iDestruct "H" as (E'' dw m'' _ ???) "[Hm H]".
      destruct n as [|n]=> //=.
      iDestruct (vcg_correct with "Hm H") as "H"; eauto using dcexpr_wf_mono.
      rewrite (dcexpr_interp_mono E E''); eauto.
699
      iApply (cwp_wand with "H"); iIntros (v) "H".
700 701 702 703 704
      iDestruct "H" as (E''' dw' m''' _ ???) "[Hm H]".
      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
      rewrite !(dcexpr_interp_mono _ E'''); eauto using dcexpr_wf_mono.
      iDestruct (vcg_correct with "Hm H") as "H";
        simpl; split_and?; eauto using dcexpr_wf_mono.
705
      iApply (cwp_wand with "H"); iIntros (v') "H".
706 707 708 709
      iApply (vcg_continuation_mono with "H"); eauto.
  Qed.
End vcg_spec.

710
Arguments vcg_cwp_continuation _ _ _ _ _ _ _ /.
711 712 713 714 715 716
Arguments vcg_alloc _ _ _ _ _ _ _ /.
Arguments vcg_load _ _ _ _ _ _ /.
Arguments vcg_store _ _ _ _ _ _ _ /.
Arguments vcg_bin_op _ _ _ _ _ _ _ _ /.
Arguments vcg_un_op _ _ _ _ _ _ _ /.
Arguments vcg_pre_bin_op _ _ _ _ _ _ _ _ /.
717
Arguments vcg_call _ _ _ _ _ _ _ _ /.