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

6
Section LangTests.
7
  Definition add : expr [] := (#21 + #21)%E.
8
  Goal  σ, head_step add σ (#42) σ None.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  Proof. intros; do_head_step done. Qed.
10
  Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E.
11
  Goal  σ, head_step rec_app σ rec_app σ None.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  Proof. intros. rewrite /rec_app. do_head_step done. Qed.
13
  Definition lam : expr [] := (λ: "x", '"x" + #21)%E.
14
  Goal  σ, head_step (lam #21)%E σ add σ None.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  Proof. intros. rewrite /lam. do_head_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.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
    iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
    wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
31
  Qed.
32

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

41
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    n1 < n2 
43
    Φ #(n2 - 1)  WP FindPred #n2 #n1 @ E {{ Φ }}.
44
  Proof.
45
    iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
    wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
    - iApply "IH" "% HΦ". omega.
    - iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.
49
50
  Qed.

51
  Lemma Pred_spec n E Φ :  Φ #(n - 1)  WP Pred #n @ E {{ Φ }}.
52
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
    iIntros "HΦ". wp_lam. wp_op=> ?; wp_if.
54
    - wp_op. wp_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
      wp_apply FindPred_spec; first omega.
56
      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    - wp_apply FindPred_spec; eauto with omega.
58
  Qed.
Ralf Jung's avatar
Ralf Jung committed
59

60
  Lemma Pred_user E :
61
    (True : iProp)  WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ v, v = #40 }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
63
End LiftingTests.
64
65

Section ClosedProofs.
66
  Definition Σ : gFunctors := #[ heapGF ].
67
  Notation iProp := (iPropG heap_lang Σ).
68

69
  Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}.
70
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
    iProof. iIntros "! Hσ".
    iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
Ralf Jung's avatar
Ralf Jung committed
73
    iApply heap_e_spec; last done; by rewrite nclose_nroot.
74
  Qed.
75
End ClosedProofs.