invoke.v 1.17 KB
Newer Older
1
(** Testing function calls and AWP resources *)
2
From iris_c.vcgen Require Import vcg_solver.
3 4 5 6 7 8 9 10 11 12 13

Section tests_vcg.
  Context `{amonadG Σ}.

  Definition c_id : val := λ: "v", a_ret ("v").

  Lemma test_invoke_1 (l: cloc)  R :
    l C #42 -
      AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42   l C #42 }}%I.
  Proof.
    iIntros "Hl". vcg_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
    iIntros "Hl". awp_lam. vcg_solver. iIntros "?".
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
    vcg_continue. eauto.
  Qed.

  Definition plus_pair : val := λ: "vv",
    let: "v1" := Fst "vv" in
    let: "v2" := Snd "vv" in
    (a_ret "v1") + (a_ret "v2").

  Lemma test_invoke_2 R :
    AWP call (plus_pair, 21 ||| 21) @ R {{ v, v = #42 }}%I.
  Proof.
    iIntros. vcg_solver. awp_lam.
    do 2  (awp_proj; awp_let).
    vcg_solver. by vcg_continue.
  Qed.

  Lemma test_invoke_3 (l : cloc) R :
    l C #21 -
      AWP call (plus_pair, (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl)) @ R
        {{ v, v = #42   l C #21 }}%I.
  Proof.
    iIntros.  vcg_solver. iIntros "Hl". awp_lam.
    do 2  (awp_proj; awp_let).
    vcg_solver. iIntros "Hl". vcg_continue.
    rewrite Qp_half_half. eauto 42 with iFrame.
  Qed.
End tests_vcg.