invoke.v 1.08 KB
Newer Older
1
(** Testing function calls and CWP resources *)
2
From iris_c.vcgen Require Import proofmode.
3 4

Section tests_vcg.
5
  Context `{cmonadG Σ}.
6

7
  Definition c_id : val := λ: "v", c_ret "v".
8 9 10

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

  Definition plus_pair : val := λ: "vv",
18 19 20
    "v1" ←ᶜ c_ret (Fst "vv");
    "v2" ←ᶜ c_ret (Snd "vv");
    (c_ret "v1") + (c_ret "v2").
21 22

  Lemma test_invoke_2 R :
23
    CWP call (c_ret plus_pair) (21 ||| 21) @ R {{ v, v = #42 }}%I.
24
  Proof.
25
    iIntros. vcg. iIntros "!> $ !>". cwp_lam. vcg. by vcg_continue.
26 27 28 29
  Qed.

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