heap_lang.v 2.27 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 5
From iris.heap_lang Require Import adequacy.
From iris.program_logic Require Import ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From iris.heap_lang Require Import proofmode notation.
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 :
     nclose heapN  E  heap_ctx  WP heap_e @ E {{ v, v = #2 }}.
17
  Proof.
18
    iIntros (HN) "#?". 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 :
     nclose heapN  E  heap_ctx  WP heap_e2 @ E {{ v, v = #2 }}.
28
  Proof.
29
    iIntros (HN) "#?". 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
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    rec: "pred" "x" "y" :=
36 37
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
38
  Definition Pred : val :=
39
    λ: "x",
40
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
41
  Global Opaque FindPred Pred.
42

43
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
44
    n1 < n2 
45
    Φ #(n2 - 1)  WP FindPred #n2 #n1 @ E {{ Φ }}.
46
  Proof.
47
    iIntros (Hn) "HΦ". iLöb (n1 Hn) as "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
49
    - iApply ("IH" with "[%] HΦ"). omega.
50
    - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
51 52
  Qed.

53
  Lemma Pred_spec n E Φ :  Φ #(n - 1)  WP Pred #n @ E {{ Φ }}.
54
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
    iIntros "HΦ". wp_lam. wp_op=> ?; wp_if.
56
    - wp_op. wp_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
      wp_apply FindPred_spec; first omega.
58
      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
    - wp_apply FindPred_spec; eauto with omega.
60
  Qed.
Ralf Jung's avatar
Ralf Jung committed
61

62
  Lemma Pred_user E :
63
    True  WP let: "x" := Pred #42 in Pred "x" @ E {{ v, v = #40 }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
65
End LiftingTests.
66

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