heap_lang.v 3.05 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2 3
From iris.program_logic Require Import ownership hoare auth.
From iris.heap_lang Require Import wp_tactics heap notation.
4
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
5

6
Section LangTests.
7
  Definition add : expr [] := (#21 + #21)%E.
8
  Goal  σ, prim_step heap_ectx_lang add σ (#42) σ None.
9
  Proof. intros; do_step done. Qed.
10
  Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E.
11
  Goal  σ, prim_step heap_ectx_lang rec_app σ rec_app σ None.
12
  Proof. intros. rewrite /rec_app. do_step done. Qed.
13
  Definition lam : expr [] := (λ: "x", '"x" + #21)%E.
14
  Goal  σ, prim_step heap_ectx_lang (lam #21)%E σ add σ None.
15
  Proof. intros. rewrite /lam. do_step done. Qed.
Ralf Jung's avatar
Ralf Jung committed
16 17
End LangTests.

18
Section LiftingTests.
19
  Context `{heapG Σ}.
20
  Local Notation iProp := (iPropG heap_lang Σ).
21 22
  Implicit Types P Q : iPropG heap_lang Σ.
  Implicit Types Φ : val  iPropG heap_lang Σ.
23

24
  Definition heap_e  : expr [] :=
25
    let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
26
  Lemma heap_e_spec E N :
27
     nclose N  E  heap_ctx N  WP heap_e @ E {{ λ v, v = #2 }}.
28
  Proof.
29
    rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
30
    wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
31
    wp_let. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
32
    wp_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
33
    wp_seq. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
34
      by apply const_intro.
35
  Qed.
36

37
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
38
    rec: "pred" "x" "y" :=
39
      let: "yp" := '"y" + #1 in
40
      if: '"yp" < '"x" then '"pred" '"x" '"yp" else '"y".
41
  Definition Pred : val :=
42
    λ: "x",
43
      if: '"x"  #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
44

45
  Lemma FindPred_spec n1 n2 E Φ :
Ralf Jung's avatar
Ralf Jung committed
46
    n1 < n2  
47
    Φ #(n2 - 1)  WP FindPred #n2 #n1 @ E {{ Φ }}.
48
  Proof.
Ralf Jung's avatar
Ralf Jung committed
49
    revert n1. wp_rec=>n1 Hn.
50
    wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
    - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
52
      by rewrite left_id -always_wand_impl always_elim wand_elim_r.
53
    - assert (n1 = n2 - 1) as -> by omega; auto with I.
54 55
  Qed.

56
  Lemma Pred_spec n E Φ :  Φ #(n - 1)  WP Pred #n @ E {{ Φ }}.
57
  Proof.
58
    wp_lam. wp_op=> ?; wp_if.
59
    - wp_op. wp_op.
60
      ewp apply FindPred_spec; last omega.
61
      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
62
    - by ewp apply FindPred_spec; eauto with omega.
63
  Qed.
Ralf Jung's avatar
Ralf Jung committed
64

65
  Lemma Pred_user E :
66
    (True : iProp)  WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
Ralf Jung's avatar
Ralf Jung committed
67
  Proof.
68
    intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
Ralf Jung's avatar
Ralf Jung committed
69
  Qed.
70
End LiftingTests.
71 72

Section ClosedProofs.
73
  Definition Σ : gFunctors := #[ heapGF ].
74
  Notation iProp := (iPropG heap_lang Σ).
75

76
  Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
77
  Proof.
78
    apply ht_alt. rewrite (heap_alloc nroot ); last by rewrite nclose_nroot.
79
    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
80 81
    rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
  Qed.
82
End ClosedProofs.