heap_lang.v 5.99 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
    iIntros "". rewrite /heap_e. Show.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
30 31
    wp_alloc l as "?". wp_load. Show.
    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.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
42 43
    wp_alloc l as "Hl". Show. wp_alloc l'.
    wp_load. 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
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
63 64
    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
    wp_alloc l''. by repeat wp_load.
65 66
  Qed.

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

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

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

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

86 87 88 89
  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.

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

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

109
  Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
110
  Proof.
111
    iIntros "HΦ". wp_lam.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
112 113 114
    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
115
    - wp_apply FindPred_spec; eauto with omega.
116
  Qed.
Ralf Jung's avatar
Ralf Jung committed
117

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

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

126 127 128 129 130 131 132
  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
133 134 135 136 137 138 139 140
  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
141
  Check "wp_nonclosed_value".
142 143 144 145
  Lemma wp_nonclosed_value :
    WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
  Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.

146 147 148 149 150
End tests.

Section printing_tests.
  Context `{heapG Σ}.

151 152 153 154
  (* 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. *)

155 156 157 158 159 160 161 162 163
  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.

164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  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
182 183 184 185 186 187 188 189 190
  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.

191
End printing_tests.
192

193 194 195
Section error_tests.
  Context `{heapG Σ}.

196 197
  Check "not_cas".
  Lemma not_cas :
198
    (WP #() #() {{ _, True }})%I.
199 200 201
  Proof.
    Fail wp_cas_suc.
  Abort.
202 203
End error_tests.

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