heap_lang.v 4.98 KB
Newer Older
1
From iris.program_logic Require Export weakestpre total_weakestpre.
2
3
4
From iris.heap_lang Require Import lang adequacy proofmode notation.
(* Import lang *again*. This used to break notation. *)
From iris.heap_lang Require Import lang.
5
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
6

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

Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
16
17
18
19
20
21
  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.

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

25
  Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
26
  Proof.
27
28
29
    iIntros "". rewrite /heap_e. Show.
    wp_alloc l. wp_let. wp_load. Show.
    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.

Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
77
78
  Definition heap_e6 : val := λ: "v", "v" = "v".

  Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w,  w = #true  }})%I.
  Proof. wp_lam. wp_op. by case_bool_decide. Qed.

79
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
80
    rec: "pred" "x" "y" :=
81
82
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
83
  Definition Pred : val :=
84
    λ: "x",
85
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
86

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

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

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

Ralf Jung's avatar
Ralf Jung committed
113
114
115
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
116

117
118
119
120
121
End tests.

Section printing_tests.
  Context `{heapG Σ}.

122
123
124
125
  (* These terms aren't even closed, but that's not what this is about.  The
  length of the variable names etc. has been carefully chosen to trigger
  particular behavior of the Coq pretty printer. *)

126
127
128
129
130
131
132
133
134
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"  {{ Φ }}.
  Proof.
    iIntros "_". Show.
  Abort.

  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
  Proof.
    iIntros "_". Show.
  Abort.

Ralf Jung's avatar
Ralf Jung committed
153
154
155
156
157
158
159
160
161
  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.

162
End printing_tests.
163

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