invoke.v 1.05 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
(** Testing function calls and AWP resources *)
2
From iris_c.vcgen Require Import proofmode.
Dan Frumin's avatar
Dan Frumin committed
3 4 5 6

Section tests_vcg.
  Context `{amonadG Σ}.

7
  Definition c_id : val := λ: "v", a_ret "v".
Dan Frumin's avatar
Dan Frumin committed
8 9 10

  Lemma test_invoke_1 (l: cloc)  R :
    l C #42 -
11
    AWP call c_id (∗ᶜ ♯ₗl) @ R {{ v, v = #42  l C #42 }}%I.
Dan Frumin's avatar
Dan Frumin committed
12
  Proof.
13 14
    iIntros "Hl". vcg. iIntros "Hl !> $".
    awp_lam. vcg. iIntros "Hl". vcg_continue. eauto.
Dan Frumin's avatar
Dan Frumin committed
15 16 17
  Qed.

  Definition plus_pair : val := λ: "vv",
18 19
    "v1" ←ᶜ a_ret (Fst "vv");
    "v2" ←ᶜ a_ret (Snd "vv");
Dan Frumin's avatar
Dan Frumin committed
20 21 22
    (a_ret "v1") + (a_ret "v2").

  Lemma test_invoke_2 R :
23
    AWP call plus_pair (21 ||| 21) @ R {{ v, v = #42 }}%I.
Dan Frumin's avatar
Dan Frumin committed
24
  Proof.
25
    iIntros. vcg. iIntros "!> $". awp_lam. vcg. by vcg_continue.
Dan Frumin's avatar
Dan Frumin committed
26 27 28 29
  Qed.

  Lemma test_invoke_3 (l : cloc) R :
    l C #21 -
30
    AWP call plus_pair (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl) @ R
31
      {{ v, v = #42   l C #21 }}%I.
Dan Frumin's avatar
Dan Frumin committed
32
  Proof.
33 34
    iIntros. vcg. iIntros "Hl !> $". awp_lam. vcg.
    iIntros "Hl". vcg_continue; eauto.
Dan Frumin's avatar
Dan Frumin committed
35 36
  Qed.
End tests_vcg.