heap_lang_proph.v 2.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Import lang adequacy proofmode notation.
From iris.heap_lang Require Import lang.
Set Default Proof Using "Type".

Section tests.
  Context `{!heapG Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.

  Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
    l  #n -
    proph p vs -
14
    WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, v = #n  vs, proph p vs  l  #(n+1) }}%I.
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
  Proof.
    iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
    wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
  Qed.

  Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
    proph p vs -
    WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, v = #0  vs, proph p vs }}%I.
  Proof.
    iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
    wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
  Qed.

  Lemma test_resolve3 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
    {{{ proph p1 vs1  proph p2 vs2 }}}
      Resolve (Resolve (#n - #n) #p2 #2) #p1 #1 @ s; E
    {{{ RET #0 ;  vs1' vs2', vs1 = (#0, #1)::vs1'  vs2 = (#0, #2)::vs2'  proph p1 vs1'  proph p2 vs2' }}}.
  Proof.
    iIntros (Φ) "[Hp1 Hp2] HΦ".
    wp_apply (wp_resolve with "Hp1"); first done.
    wp_apply (wp_resolve with "Hp2"); first done.
    wp_op.
    iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
    iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
  Qed.

  Lemma test_resolve4 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
    {{{ proph p1 vs1  proph p2 vs2 }}}
      Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E
    {{{ RET #0 ;  vs1' vs2', vs1 = (#0, #1)::vs1'  vs2 = (#0, #2)::vs2'  proph p1 vs1'  proph p2 vs2' }}}.
  Proof.
    iIntros (Φ) "[Hp1 Hp2] HΦ".
    wp_apply (wp_resolve with "Hp1"); first done.
    wp_apply (wp_resolve with "Hp2"); first done.
    wp_op.
    iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
    iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
  Qed.

End tests.