heap_lang.v 2.13 KB
Newer Older
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".
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
  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

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

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

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

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