swap.v 891 Bytes
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
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.

8
Section tests_vcg.
9
10
11
  Context `{amonadG Σ}.

  Definition swap : val := λ: "l1" "l2" "r",
12
13
14
15
    (a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
    (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
    (a_store (a_ret "l2") (a_load (a_ret "r"))) ;;;;
    (a_ret #0).
16

Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
  Lemma swap_spec_by_vcg_opt (l1 l2 r : loc) (v1 v2: val) R :
    r C #0 - l1 C v1  l2 C v2 -
    awp (swap #l1 #l2 #r) R (λ _, l2 C v1  l1 C v2).
20
21
  Proof.
    iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
22
    vcg_solver. iIntros "!> !> !>". eauto with iFrame.
23
  Qed.
24
End tests_vcg.