heap_lang.v 3.48 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 Export weakestpre total_weakestpre.
3
From iris.heap_lang Require Export lang.
4
From iris.heap_lang Require Import adequacy.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.heap_lang Require Import proofmode notation.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

8
Section LiftingTests.
9
  Context `{heapG Σ}.
10
11
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
12

Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
  Definition simpl_test :
    (10 = 4 + 6)%nat -
    WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, v = #1 }}.
  Proof.
    iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
    match goal with
    | |- context [ (10 = 4 + 6)%nat ] => done
    end.
  Qed.

23
  Definition heap_e : expr :=
24
    let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
25

26
  Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
27
  Proof.
28
    iIntros "". rewrite /heap_e.
29
    wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
30
  Qed.
31

32
  Definition heap_e2 : expr :=
33
34
    let: "x" := ref #1 in
    let: "y" := ref #1 in
35
    "x" <- !"x" + #1 ;; !"x".
36

37
  Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
38
  Proof.
39
    iIntros "". rewrite /heap_e2.
40
    wp_alloc l. wp_let. wp_alloc l'. wp_let.
41
    wp_load. wp_op. wp_store. wp_load. done.
42
43
  Qed.

44
45
46
47
48
  Definition heap_e3 : expr :=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.

49
  Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, v = #1 }]%I.
50
51
52
53
54
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

55
56
57
58
  Definition heap_e4 : expr :=
    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
    ! ! !"x".

59
  Lemma heap_e4_spec : WP heap_e4 [{ v,  v = #1  }]%I.
60
61
62
63
64
  Proof.
    rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
    wp_alloc l''. wp_let. by repeat wp_load.
  Qed.

65
66
67
  Definition heap_e5 : expr :=
    let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".

68
  Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
69
70
71
72
73
  Proof.
    rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
    wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
  Qed.

74
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
75
    rec: "pred" "x" "y" :=
76
77
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
78
  Definition Pred : val :=
79
    λ: "x",
80
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
81

82
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
83
    n1 < n2 
84
    Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E [{ Φ }].
85
  Proof.
86
87
    iIntros (Hn) "HΦ".
    iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
88
89
    wp_rec. wp_let. wp_op. wp_let.
    wp_op; case_bool_decide; wp_if.
90
91
    - iApply ("IH" with "[%] [%] HΦ"); omega.
    - by assert (n1' = n2 - 1) as -> by omega.
92
93
  Qed.

94
  Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
95
  Proof.
96
97
    iIntros "HΦ". wp_lam.
    wp_op. case_bool_decide; wp_if.
98
    - wp_op. wp_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
      wp_apply FindPred_spec; first omega.
100
      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
    - wp_apply FindPred_spec; eauto with omega.
102
  Qed.
Ralf Jung's avatar
Ralf Jung committed
103

104
  Lemma Pred_user E :
105
    WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
107

Ralf Jung's avatar
Ralf Jung committed
108
109
110
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
111

112
End LiftingTests.
113

Ralf Jung's avatar
Ralf Jung committed
114
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
115
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.