heap_lang.v 6.14 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 Ltac Backtrace.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

8
Section tests.
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 24
  Definition val_scope_test_1 := SOMEV (#(), #()).

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

28
  Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
29
  Proof.
30
    iIntros "". rewrite /heap_e. Show.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
31 32
    wp_alloc l as "?". wp_load. Show.
    wp_store. by wp_load.
33
  Qed.
34

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

40
  Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
41
  Proof.
42
    iIntros "". rewrite /heap_e2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
43 44
    wp_alloc l as "Hl". Show. wp_alloc l'.
    wp_load. wp_store. wp_load. done.
45 46
  Qed.

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

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

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

62
  Lemma heap_e4_spec : WP heap_e4 [{ v,  v = #1  }]%I.
63
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
64 65
    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
    wp_alloc l''. by repeat wp_load.
66 67
  Qed.

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

71
  Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
72
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
73 74
    rewrite /heap_e5. wp_alloc l. wp_alloc l'.
    wp_load. wp_faa. do 2 wp_load. by wp_pures.
75 76
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
82 83
  Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.

84
  Lemma heap_e7_spec_total l : l  #0 - WP heap_e7 #l [{_,  l  #1 }].
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
  Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.

87 88 89 90
  Check "heap_e7_spec".
  Lemma heap_e7_spec l : ^2 l  #0 - WP heap_e7 #l {{_,  l  #1 }}.
  Proof. iIntros. wp_lam. Show. wp_cas_suc. Show. auto. Qed.

91
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
92
    rec: "pred" "x" "y" :=
93 94
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
95
  Definition Pred : val :=
96
    λ: "x",
97
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
98

99
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
100
    n1 < n2 
101
    Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E [{ Φ }].
102
  Proof.
103 104
    iIntros (Hn) "HΦ".
    iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
105
    wp_rec. wp_pures. case_bool_decide; wp_if.
106 107
    - iApply ("IH" with "[%] [%] HΦ"); omega.
    - by assert (n1' = n2 - 1) as -> by omega.
108 109
  Qed.

110
  Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
111
  Proof.
112
    iIntros "HΦ". wp_lam.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
113 114 115
    wp_op. case_bool_decide.
    - wp_apply FindPred_spec; first omega. wp_pures.
      by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
    - wp_apply FindPred_spec; eauto with omega.
117
  Qed.
Ralf Jung's avatar
Ralf Jung committed
118

119
  Lemma Pred_user E :
120
    WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
121
  Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
122

Ralf Jung's avatar
Ralf Jung committed
123 124 125
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
126

127 128 129 130 131 132 133
  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.

Ralf Jung's avatar
Ralf Jung committed
134 135 136 137 138 139 140 141
  Lemma wp_alloc_split :
    WP Alloc #0 {{ _, True }}%I.
  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.

  Lemma wp_alloc_drop :
    WP Alloc #0 {{ _, True }}%I.
  Proof. wp_alloc l as "_". Show. done. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
142
  Check "wp_nonclosed_value".
143 144 145 146
  Lemma wp_nonclosed_value :
    WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
  Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.

147 148 149
End tests.

Section printing_tests.
150
  Context `{!heapG Σ}.
151

152 153 154 155 156 157
  Lemma ref_print :
    True - WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

158 159 160 161
  (* 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. *)

162 163 164 165 166 167 168 169 170
  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.

171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
  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
189 190 191 192 193 194 195 196 197
  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.

198
End printing_tests.
199

200
Section error_tests.
201
  Context `{!heapG Σ}.
202

203 204
  Check "not_cas".
  Lemma not_cas :
205
    (WP #() #() {{ _, True }})%I.
206 207 208
  Proof.
    Fail wp_cas_suc.
  Abort.
209 210
End error_tests.

211
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
212
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.