heap_lang.v 5.2 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
End tests.

Section printing_tests.
  Context `{heapG Σ}.

124
125
126
127
  (* 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. *)

128
129
130
131
132
133
134
135
136
  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.

137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
  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
155
156
157
158
159
160
161
162
163
  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.

164
End printing_tests.
165

166
167
168
Section error_tests.
  Context `{heapG Σ}.

169
170
171
172
173
174
  Check "not_cas".
  Lemma not_cas :
    (WP #() {{ _, True }})%I.
  Proof.
    Fail wp_cas_suc.
  Abort.
175
176
End error_tests.

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