basics.v 3.66 KB
Newer Older
1
2
3
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
4
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
5
From iris_c.c_translation Require Import monad translation proofmode derived.
6
7
8
9
10
From iris_c.lib Require Import locking_heap U.

Section test.
  Context `{amonadG Σ}.

Dan Frumin's avatar
Dan Frumin committed
11
12
  Lemma test1 (l : cloc) (v: val) :
    l C v - awp (∗ᶜ ♯ₗl) True (λ w, w = v  l C v).
13
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
    iIntros "Hl1". vcg_solver. auto.
15
   Qed.
16
17

  (* double dereferencing *)
Dan Frumin's avatar
Dan Frumin committed
18
19
20
  Lemma test2 (l1 l2 : cloc) (v: val) :
    l1 C cloc_to_val l2 - l2 C v -
    awp ( ∗ᶜ ∗ᶜ ♯ₗl1) True (λ v, v = #1  l1 C cloc_to_val l2 - l2 C v).
21
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
    iIntros "Hl1 Hl2". vcg_solver. auto.
23
24
  Qed.

Dan Frumin's avatar
Dan Frumin committed
25
26
  Lemma test3 (l : cloc) (v: val) :
    l C v - awp (∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗl) True (λ w, w = v  l C v).
27
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
    iIntros "Hl1". vcg_solver. auto.
29
30
  Qed.

Dan Frumin's avatar
Dan Frumin committed
31
32
  Lemma test4 (l : cloc) (v1 v2: val) :
    l C v1 - awp ( ♯ₗl = a_ret v2) True (λ v, v = v2  l C[LLvl] v2).
33
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    iIntros "Hl1". vcg_solver. auto.
35
36
37
  Qed.

  (* double dereferencing & modification *)
Dan Frumin's avatar
Dan Frumin committed
38
39
40
41
  Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) :
    l1 C cloc_to_val l2 - l2 C v1 -
    r1 C cloc_to_val r2 - r2 C v2 -
    awp ( ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1 ) True
42
43
    (λ w, w = v2 
      l1 C cloc_to_val r2  l2 C v1  r1 C cloc_to_val r2 - r2 C v2).
44
  Proof.
Dan Frumin's avatar
Dan Frumin committed
45
    iIntros "**". vcg_solver. eauto 40.
46
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
47

Dan Frumin's avatar
Dan Frumin committed
48
  Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
Léon Gondelman's avatar
Léon Gondelman committed
49
    l1 C v1 - l2 C v2 -
Dan Frumin's avatar
Dan Frumin committed
50
      awp ( ∗ᶜ ♯ₗl1 |||  ∗ᶜ ♯ₗl2) True
Léon Gondelman's avatar
Léon Gondelman committed
51
52
53
54
55
       (λ w, w = (v1, v2)%V  l1 C v1  l2 C v2).
  Proof.
    iIntros "**". vcg_solver. rewrite Qp_half_half. eauto with iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
56
  Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
Léon Gondelman's avatar
Léon Gondelman committed
57
    l1 C v1 - l2 C v2 -
Dan Frumin's avatar
Dan Frumin committed
58
      awp ( (♯ₗl1 = a_ret v2) |||  (♯ₗl2 = a_ret v1) ) True
Léon Gondelman's avatar
Léon Gondelman committed
59
60
61
62
63
       (λ w, w = (v2, v1)%V  l1 C[LLvl] v2  l2 C[LLvl] v1).
  Proof.
    iIntros "**". vcg_solver. eauto with iFrame.
  Qed.

64
65

  Definition c_id : val := λ: "v", a_ret ("v").
66
67
68
69
70


  Lemma test_invoke_1 (l: cloc)  R :
    l C #42 -
      AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42   l C #42 }}%I.
71
72
  Proof.
    iIntros "Hl". vcg_solver.
73
74
75
    iIntros "Hl". awp_lam. awp_ret_value.
    vcg_continue. eauto.
  Qed.
76

77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
  Definition plus_pair : val := λ: "vv",
    let: "v1" := Fst "vv" in
    let: "v2" := Snd "vv" in
    (a_ret "v1") + (a_ret "v2").

  Lemma test_invoke_21 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_22 (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.
Léon Gondelman's avatar
Léon Gondelman committed
100

101
   Lemma test6 (l : cloc) (z0 : Z) R:
Dan Frumin's avatar
Dan Frumin committed
102
    l C #z0 -
Dan Frumin's avatar
Dan Frumin committed
103
    AWP ♯ₗl += 1 @ R {{ v, v = #z0  l C[LLvl] #(z0+1) }}.
Dan Frumin's avatar
Dan Frumin committed
104
105
106
107
  Proof.
    iIntros "Hl". vcg_solver. eauto.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
108
  Lemma test7 (l k : cloc) (z0 z1 : Z) R:
Dan Frumin's avatar
Dan Frumin committed
109
110
    l C #z0 -
    k C #z1 -
Dan Frumin's avatar
Dan Frumin committed
111
    AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @
112
    R {{ v, v = #(z0+z1)  l C[LLvl] #(z0+1)  k C #z1 }}.
Dan Frumin's avatar
Dan Frumin committed
113
114
115
116
  Proof.
    iIntros "Hl Hk". vcg_solver. eauto with iFrame.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
117
End test.