peritem.v 3.02 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.
Zhen Zhang's avatar
Zhen Zhang committed
6
From iris_atomic Require Export treiber misc.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
7
From iris.base_logic.lib Require Import invariants.
Zhen Zhang's avatar
Zhen Zhang committed
8 9

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

Zhen Zhang's avatar
Zhen Zhang committed
13
  Fixpoint is_list_R (hd: loc) (xs: list val) : iProp Σ :=
Zhen Zhang's avatar
Zhen Zhang committed
14 15
    match xs with
    | [] => ( q, hd { q } NONEV)%I
Zhen Zhang's avatar
Zhen Zhang committed
16
    | 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
17 18
    end.

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

Zhen Zhang's avatar
Zhen Zhang committed
21 22
  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
23 24
  Proof.
    induction xs as [|y xs' IHxs'].
25
    - iIntros (hd) "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
26
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
27
    - iIntros (hd) "Hs". simpl.
Zhen Zhang's avatar
Zhen Zhang committed
28
      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
Ralf Jung's avatar
Ralf Jung committed
29 30
      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
31
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
32 33 34 35 36 37

  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
38 39 40
End defs.

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

Zhen Zhang's avatar
Zhen Zhang committed
44 45 46 47
  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
48
  Proof.
49
    iIntros (Φ) "_ HΦ". iApply wp_fupd.
Ralf Jung's avatar
Ralf Jung committed
50
    wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
Zhen Zhang's avatar
Zhen Zhang committed
51
    wp_alloc s as "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
52 53 54 55
    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.
56
    iApply "HΦ". iFrame "#". done.
Zhen Zhang's avatar
Zhen Zhang committed
57 58
  Qed.
  
Zhen Zhang's avatar
Zhen Zhang committed
59 60
  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
61
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
    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
86 87 88
  Qed.

End proofs.