peritem.v 3.06 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Zhen Zhang's avatar
Zhen Zhang committed
4
From iris.proofmode Require Import tactics.
5
From iris.algebra Require Import frac auth gmap csum.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.base_logic Require Import big_op.
Zhen Zhang's avatar
Zhen Zhang committed
7
From iris_atomic Require Export treiber misc.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
8
From iris.base_logic.lib Require Import invariants.
Zhen Zhang's avatar
Zhen Zhang committed
9 10

Section defs.
Zhen Zhang's avatar
Zhen Zhang committed
11
  Context `{heapG Σ} (N: namespace).
Zhen Zhang's avatar
Zhen Zhang committed
12
  Context (R: val  iProp Σ) `{ x, TimelessP (R x)}.
Zhen Zhang's avatar
Zhen Zhang committed
13

Zhen Zhang's avatar
Zhen Zhang committed
14
  Fixpoint is_list_R (hd: loc) (xs: list val) : iProp Σ :=
Zhen Zhang's avatar
Zhen Zhang committed
15 16
    match xs with
    | [] => ( q, hd { q } NONEV)%I
Zhen Zhang's avatar
Zhen Zhang committed
17
    | x :: xs => ( (hd': loc) q, hd {q} SOMEV (x, #hd')  inv N (R x)  is_list_R hd' xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
18 19
    end.

Zhen Zhang's avatar
Zhen Zhang committed
20
  Definition is_bag_R xs s := ( hd: loc, s  #hd  is_list_R hd xs)%I.
Zhen Zhang's avatar
Zhen Zhang committed
21

Zhen Zhang's avatar
Zhen Zhang committed
22 23
  Lemma dup_is_list_R :  xs hd,
    is_list_R hd xs  |==> is_list_R hd xs  is_list_R hd xs.
Zhen Zhang's avatar
Zhen Zhang committed
24 25
  Proof.
    induction xs as [|y xs' IHxs'].
26
    - iIntros (hd) "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
27
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
28
    - iIntros (hd) "Hs". simpl.
Zhen Zhang's avatar
Zhen Zhang committed
29
      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
Ralf Jung's avatar
Ralf Jung committed
30 31
      iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
      iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
32
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
33 34 35 36 37 38

  Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
    {{{ inv N R  Rf }}}
      f x
    {{{ RET #(); Rf }}}.

Zhen Zhang's avatar
Zhen Zhang committed
39 40 41
End defs.

Section proofs.
Zhen Zhang's avatar
Zhen Zhang committed
42
  Context `{heapG Σ} (N: namespace).
Zhen Zhang's avatar
Zhen Zhang committed
43 44
  Context (R: val  iProp Σ).

Zhen Zhang's avatar
Zhen Zhang committed
45 46 47 48
  Definition bag_inv s: iProp Σ := inv N ( xs, is_bag_R N R xs s)%I.

  Lemma new_bag_spec:
    {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
Zhen Zhang's avatar
Zhen Zhang committed
49
  Proof.
50
    iIntros (Φ) "_ HΦ". iApply wp_fupd.
Zhen Zhang's avatar
Zhen Zhang committed
51 52
    wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
    wp_alloc s as "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
53 54 55 56
    iAssert (( xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
    { iFrame. iExists [], l.
      iFrame. simpl. eauto. }
    iMod (inv_alloc N _ ( xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
57
    iApply "HΦ". iFrame "#". done.
Zhen Zhang's avatar
Zhen Zhang committed
58 59
  Qed.
  
Zhen Zhang's avatar
Zhen Zhang committed
60 61
  Lemma push_spec (s: loc) (x: val):
    {{{ R x  bag_inv s }}} push #s x {{{ RET #() ; inv N (R x) }}}.
Zhen Zhang's avatar
Zhen Zhang committed
62
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
    iIntros (Φ) "(HRx & #?) HΦ".
    iLöb as "IH". wp_rec. wp_let.
    wp_bind (! _)%E.
    iInv N as "H1" "Hclose".
    iDestruct "H1" as (xs hd) "[>Hs H1]".
    wp_load. iMod ("Hclose" with "[Hs H1]").
    { iNext. iFrame. iExists xs, hd. iFrame. }
    iModIntro. wp_let. wp_alloc l as "Hl".
    wp_let. wp_bind (CAS _ _ _)%E.
    iInv N as "H1" "Hclose".
    iDestruct "H1" as (xs' hd') "[>Hs H1]".
    destruct (decide (hd = hd')) as [->|Hneq].
    - wp_cas_suc.
      iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
      iMod ("Hclose" with "[Hs Hl H1]").
      { iNext. iFrame. iExists (x::xs'), l.
        iFrame. simpl. iExists hd', 1%Qp. iFrame.
        by iFrame "#". }
      iModIntro. wp_if. by iApply "HΦ".
    - wp_cas_fail.
      iMod ("Hclose" with "[Hs H1]").
      { iNext. iFrame. iExists (xs'), hd'. iFrame. }
      iModIntro. wp_if. iApply ("IH" with "HRx").
      by iNext.
Zhen Zhang's avatar
Zhen Zhang committed
87 88 89
  Qed.

End proofs.