specs.v 1.84 KB
Newer Older
Daniel Gratzer's avatar
Daniel Gratzer committed
1 2 3 4 5 6
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export proofmode notation.

(** General (HoCAP-style) spec for a concurrent bag ("per-elemt spec") *)
Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag {
7 8
  is_bag (P : val  iProp Σ) (s : val) : iProp Σ;
  bag_pers (P : val  iProp Σ) (s : val) : Persistent (is_bag P s);
Daniel Gratzer's avatar
Daniel Gratzer committed
9 10 11
  new_bag : val;
  bag_push : val;
  bag_pop : val;
12
  mk_bag_spec (P : val  iProp Σ) :
Daniel Gratzer's avatar
Daniel Gratzer committed
13 14
    {{{ True }}}
      new_bag #()
15 16 17 18 19
    {{{ s, RET s; is_bag P s }}};
  bag_push_spec (P : val  iProp Σ) s v :
    {{{ is_bag P s  P v }}} bag_push s v {{{ RET #(); True }}};
  bag_pop_spec (P : val  iProp Σ) s :
    {{{ is_bag P s }}} bag_pop s {{{ ov, RET ov; ov = NONEV   v, ov = SOMEV v  P v }}}
Daniel Gratzer's avatar
Daniel Gratzer committed
20 21 22
}.
Arguments concurrent_bag _ {_}.

23
(** General (CAP-style) spec for a concurrent stack *)
Daniel Gratzer's avatar
Daniel Gratzer committed
24 25 26

Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {
  is_stack (N : namespace) (P : list val  iProp Σ) (s : val) : iProp Σ;
27
  stack_pers (N : namespace) (P : list val  iProp Σ) (s : val) : Persistent (is_stack N P s);
Daniel Gratzer's avatar
Daniel Gratzer committed
28 29 30 31 32 33 34 35 36 37 38
  new_stack : val;
  stack_push : val;
  stack_pop : val;
  new_stack_spec (N : namespace) (P : list val  iProp Σ) :
    {{{ P [] }}} new_stack #() {{{ v, RET v; is_stack N P v }}};
  stack_push_spec (N : namespace) (P : list val  iProp Σ) (Ψ : val  iProp Σ) s v :
    {{{ is_stack N P s   xs, P xs ={   N}= P (v :: xs)  Ψ #()}}}
      stack_push s v
    {{{ RET #(); Ψ #() }}};
  stack_pop_spec (N : namespace) (P : list val  iProp Σ) Ψ s :
    {{{ is_stack N P s 
39
        ( v xs, P (v :: xs) ={   N}= P xs  Ψ (SOMEV v)) 
Daniel Gratzer's avatar
Daniel Gratzer committed
40 41 42 43 44
        (P [] ={   N}= P []  Ψ NONEV) }}}
      stack_pop s
    {{{ v, RET v; Ψ v }}};
}.
Arguments concurrent_stack _ {_}.