sync.v 703 Bytes
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2 3 4 5 6
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.

Section sync.
  Context `{!heapG Σ} (N : namespace).
7

Zhen Zhang's avatar
Zhen Zhang committed
8
  Definition synced R (f' f: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
9 10
    (  P Q (x: val), ({{ R  P x }} f x {{ v, R  Q x v }}) 
                       ({{ P x }} f' x {{ v, Q x v }}))%I.
Zhen Zhang's avatar
Zhen Zhang committed
11 12

  Definition is_syncer (R: iProp Σ) (s: val) :=
13
    (  (f : val), WP s f {{ f', synced R f' f }})%I.
Zhen Zhang's avatar
Zhen Zhang committed
14 15 16 17

  Definition mk_syncer_spec (mk_syncer: val) :=
     (R: iProp Σ) (Φ: val -> iProp Σ),
      heapN  N 
18
      heap_ctx  R  ( s, is_syncer R s - Φ s)  WP mk_syncer #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
19
End sync.