basics.v 1.51 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
6
7
8
9
10
11
From iris_c.c_translation Require Import monad translation proofmode notation.
From iris_c.lib Require Import locking_heap U.

Section test.
  Context `{amonadG Σ}.

  Lemma test1 (l : loc) (v: val) :
12
    l C v - awp (∗ᶜ l) True (λ w, w = v  l C v).
13
14
  Proof.
    iIntros "Hl1". vcg_solver.
15
   Qed.
16
17
18
19

  (* double dereferencing *)
  Lemma test2 (l1 l2 : loc) (v: val) :
    l1 C #l2 - l2 C v -
20
    awp ( ∗ᶜ ∗ᶜ l1) True (λ v, v = #1  l1 C #l2 - l2 C v).
21
22
23
24
25
  Proof.
    iIntros "Hl1 Hl2". vcg_solver.
  Qed.

  Lemma test3 (l : loc) (v: val) :
26
    l C v - awp (∗ᶜ l ; ∗ᶜ l) True (λ w, w = v  l C v).
27
28
29
30
31
  Proof.
    iIntros "Hl1". vcg_solver. iModIntro. eauto.
  Qed.

  Lemma test4 (l : loc) (v1 v2: val) :
32
    l C v1 - awp ( l = ret v2) True (λ v, v = v2  l C[LLvl] v2).
33
34
35
36
37
38
39
40
  Proof.
    iIntros "Hl1". vcg_solver.
  Qed.

  (* double dereferencing & modification *)
  Lemma test5 (l1 l2 r1 r2 : loc) (v1 v2: val) :
    l1 C #l2 - l2 C v1 -
    r1 C #r2 - r2 C v2 -
41
    awp ( l1 = r1 ; ∗ᶜ ∗ᶜ l1 ) True
42
43
44
45
46
47
      (λ w, w = v2  l1 C #r2  l2 C v1  r1 C #r2 - r2 C v2).
  Proof.
    iIntros "Hl1 Hl2 Hr1 Hr2". vcg_solver. iModIntro. eauto.
  Qed.

End test.