heap_lang.v 2.71 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2
From iris.program_logic Require Export weakestpre hoare.
3
From iris.heap_lang Require Export lang.
4
From iris.heap_lang Require Import adequacy.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.heap_lang Require Import proofmode notation.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

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

13 14
  Definition heap_e  : expr :=
    let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
15

16
  Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
17
  Proof.
18
    iIntros "". rewrite /heap_e.
19
    wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
20
  Qed.
21

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

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

34 35 36 37 38 39 40 41 42 43 44
  Definition heap_e3 : expr :=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.

  Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, v = #1 }}%I.
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

45 46 47 48 49 50 51 52 53 54
  Definition heap_e4 : expr :=
    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
    ! ! !"x".

  Lemma heap_e4_spec : WP heap_e4 {{ v,  v = #1  }}%I.
  Proof.
    rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
    wp_alloc l''. wp_let. by repeat wp_load.
  Qed.

55
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
56
    rec: "pred" "x" "y" :=
57 58
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
59
  Definition Pred : val :=
60
    λ: "x",
61
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
62

63
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
64
    n1 < n2 
65
    Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E {{ Φ }}.
66
  Proof.
67
    iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
68 69
    wp_rec. wp_let. wp_op. wp_let.
    wp_op; case_bool_decide; wp_if.
70
    - iApply ("IH" with "[%] HΦ"). omega.
71
    - by assert (n1 = n2 - 1) as -> by omega.
72 73
  Qed.

74
  Lemma Pred_spec n E Φ :  Φ #(n - 1) - WP Pred #n @ E {{ Φ }}.
75
  Proof.
76 77
    iIntros "HΦ". wp_lam.
    wp_op. case_bool_decide; wp_if.
78
    - wp_op. wp_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
      wp_apply FindPred_spec; first omega.
80
      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    - wp_apply FindPred_spec; eauto with omega.
82
  Qed.
Ralf Jung's avatar
Ralf Jung committed
83

84
  Lemma Pred_user E :
85
    (WP let: "x" := Pred #42 in Pred "x" @ E {{ v, v = #40 }})%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
87
End LiftingTests.
88

89
Lemma heap_e_adequate σ : adequate heap_e σ (= #2).
90
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.