tests.v 3.19 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2
From program_logic Require Import ownership hoare auth.
3
From heap_lang Require Import wp_tactics heap notation.
4
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
5

6
Section LangTests.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8
  Definition add := ('21 + '21)%L.
  Goal  σ, prim_step add σ ('42) σ None.
9
  Proof. intros; do_step done. Qed.
10
  Definition rec_app : expr := ((rec: "f" "x" := "f" "x") '0).
Ralf Jung's avatar
Ralf Jung committed
11
  Goal  σ, prim_step rec_app σ rec_app σ None.
12 13
  Proof.
    intros. rewrite /rec_app. (* FIXME: do_step does not work here *)
14
    by eapply (Ectx_step  _ _ _ _ _ []), (BetaS _ _ _ _ '0).
15
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17
  Definition lam : expr := λ: "x", "x" + '21.
  Goal  σ, prim_step (lam '21)%L σ add σ None.
18 19
  Proof.
    intros. rewrite /lam. (* FIXME: do_step does not work here *)
20
    by eapply (Ectx_step  _ _ _ _ _ []), (BetaS "" "x" ("x" + '21) _ '21).
21
  Qed.
Ralf Jung's avatar
Ralf Jung committed
22 23
End LangTests.

24
Section LiftingTests.
25
  Context `{heapG Σ}.
26
  Local Notation iProp := (iPropG heap_lang Σ).
27 28
  Implicit Types P Q : iPropG heap_lang Σ.
  Implicit Types Φ : val  iPropG heap_lang Σ.
29 30

  Definition heap_e  : expr :=
31
    let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
32 33
  Lemma heap_e_spec E N :
     nclose N  E  heap_ctx N  || heap_e @ E {{ λ v, v = '2 }}.
34
  Proof.
35
    rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
36
    wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
37
    wp_let. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
38
    wp_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
39
    wp_seq. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
40
      by apply const_intro.
41
  Qed.
42

43
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
44
    rec: "pred" "x" "y" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
45
      let: "yp" := "y" + '1 in
46
      if: "yp" < "x" then "pred" "x" "yp" else "y".
47
  Definition Pred : val :=
48
    λ: "x",
49
      if: "x"  '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
Ralf Jung's avatar
Ralf Jung committed
50

51
  Lemma FindPred_spec n1 n2 E Φ :
Ralf Jung's avatar
Ralf Jung committed
52 53
    n1 < n2  
    Φ '(n2 - 1)  || FindPred 'n2 'n1 @ E {{ Φ }}.
54
  Proof.
Ralf Jung's avatar
Ralf Jung committed
55
    revert n1. wp_rec=>n1 Hn.
56
    wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
58
      by rewrite left_id -always_wand_impl always_elim wand_elim_r.
59
    - assert (n1 = n2 - 1) as -> by omega; auto with I.
60 61
  Qed.

62
  Lemma Pred_spec n E Φ :  Φ (LitV (n - 1))  || Pred 'n @ E {{ Φ }}.
63
  Proof.
64
    wp_lam. wp_op=> ?; wp_if.
65
    - wp_op. wp_op.
66
      ewp apply FindPred_spec; last omega.
67
      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
68
    - by ewp apply FindPred_spec; eauto with omega.
69
  Qed.
Ralf Jung's avatar
Ralf Jung committed
70

71
  Lemma Pred_user E :
72
    (True : iProp)  || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}.
Ralf Jung's avatar
Ralf Jung committed
73
  Proof.
74
    intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
Ralf Jung's avatar
Ralf Jung committed
75
  Qed.
76
End LiftingTests.
77 78

Section ClosedProofs.
79
  Definition Σ : iFunctorG := heapF .:: endF.
80
  Notation iProp := (iPropG heap_lang Σ).
81

82
  Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
83 84
  Proof.
    apply ht_alt. rewrite (heap_alloc  nroot); last by rewrite nclose_nroot.
85
    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
86 87 88
    rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
  Qed.

89
  Print Assumptions heap_e_closed.
90
End ClosedProofs.