heap_lang.v 5.35 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
23
  Definition val_scope_test_1 := SOMEV (#(), #()).

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

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

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

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

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

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

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

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

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

70
  Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
71
72
73
74
75
  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
76
77
78
79
80
  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.

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

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

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

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

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

119
120
121
122
123
124
125
  Lemma wp_cas l v :
    val_is_unboxed v 
    l  v - WP CAS #l v v {{ _, True }}.
  Proof.
    iIntros (?) "?". wp_cas as ? | ?. done. done.
  Qed.

126
127
128
129
130
End tests.

Section printing_tests.
  Context `{heapG Σ}.

131
132
133
134
  (* 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. *)

135
136
137
138
139
140
141
142
143
  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.

144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
  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
162
163
164
165
166
167
168
169
170
  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.

171
End printing_tests.
172

173
174
175
Section error_tests.
  Context `{heapG Σ}.

176
177
178
179
180
181
  Check "not_cas".
  Lemma not_cas :
    (WP #() {{ _, True }})%I.
  Proof.
    Fail wp_cas_suc.
  Abort.
182
183
End error_tests.

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