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

Module 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  Definition rec_app : expr := ((rec: "f" "x" := "f" "x") '0)%L.
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 *)
Ralf Jung's avatar
Ralf Jung committed
14
    by eapply (Ectx_step  _ _ _ _ _ []), (BetaS _ _ _ _ '0)%L.
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 *)
Ralf Jung's avatar
Ralf Jung committed
20
    by eapply (Ectx_step  _ _ _ _ _ []), (BetaS "" "x" ("x" + '21) _ '21)%L.
21
  Qed.
Ralf Jung's avatar
Ralf Jung committed
22 23
End LangTests.

24
Module LiftingTests.
25 26
  Context {Σ : iFunctor}.
  Implicit Types P : iProp heap_lang Σ.
27
  Implicit Types Q : val  iProp heap_lang Σ.
28

29
  Definition e  : expr :=
Robbert Krebbers's avatar
Robbert Krebbers committed
30
    let: "x" := ref '1 in "x" <- !"x" + '1; !"x".
Ralf Jung's avatar
Ralf Jung committed
31
  Goal  σ E, ownP (Σ:=Σ) σ  wp E e (λ v, v = ('2)%L).
32 33
  Proof.
    move=> σ E. rewrite /e.
34
    rewrite -(wp_bindi (LetCtx _ _)) -wp_alloc_pst //=.
35
    apply sep_intro_True_r; first done.
36 37
    rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
    rewrite right_id; apply const_elim_l=> _.
38 39
    rewrite -wp_let //= -later_intro.
    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))) /=. 
40 41
    rewrite -(wp_bindi (StoreRCtx (LocV _))) /=.
    rewrite -(wp_bindi (BinOpLCtx PlusOp _)) /=.
42
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
43
    { by rewrite lookup_insert. } (* RJ FIXME: figure out why apply and eapply fail. *)
44
    rewrite -later_intro; apply wand_intro_l; rewrite right_id.
45
    rewrite -wp_bin_op // -later_intro.
46
    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
47 48
    { by rewrite lookup_insert. }
    { done. }
49
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
50
    rewrite -wp_seq -wp_value -later_intro.
51
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
52
    { by rewrite lookup_insert. }
53
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
54 55
    by apply const_intro.
  Qed.
56

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

64
  Lemma FindPred_spec n1 n2 E Q :
65
    ( (n1 < n2)  Q (LitV (n2 - 1)))  wp E (FindPred 'n2 'n1)%L Q.
66
  Proof.
67 68 69
    (* FIXME there are some annoying scopes shown here: %Z, %L. *)
    rewrite /FindPred.
    rewrite -(wp_bindi (AppLCtx _)) -wp_let //=.
70
    revert n1. apply löb_all_1=>n1.
71
    rewrite (commutative uPred_and ( _)%I) associative; apply const_elim_r=>?.
72
    rewrite -wp_value' //.
73
    rewrite -wp_rec' // =>-/=.
74 75 76
    (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
    rewrite ->(later_intro (Q _)).
    rewrite -!later_and; apply later_mono.
77
    (* Go on *)
78 79
    rewrite -(wp_bindi (LetCtx _ _)) -wp_bin_op //= -wp_let //=.
    rewrite -(wp_bindi (IfCtx _ _)) /= -!later_intro.
80 81
    apply wp_lt=> ?.
    - rewrite -wp_if_true.
82 83
      rewrite -later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
      rewrite left_id impl_elim_l. by rewrite -(wp_bindi (AppLCtx _)).
84
    - assert (n1 = n2 - 1) as -> by omega.
85 86
      rewrite -wp_if_false.
      by rewrite -!later_intro -wp_value' // and_elim_r.
87 88
  Qed.

89 90 91 92
  (* FIXME : For now apparent reason, I cannot prove this inline. *)
  Lemma Pred_sub_helper n : n - 1 = - (- n + 2 - 1).
  Proof. intros. omega. Qed.

93
  Lemma Pred_spec n E Q :  Q (LitV (n - 1))  wp E (Pred 'n)%L Q.
94
  Proof.
95
    rewrite -wp_lam //=.
96
    rewrite -(wp_bindi (IfCtx _ _)) /=.
97
    apply later_mono, wp_le=> Hn.
98
    - rewrite -wp_if_true.
99 100 101 102 103 104 105 106 107 108
      rewrite -(wp_bindi (UnOpCtx _)).
      (* FIXME use list notation. *)
      rewrite -(wp_bind ((AppLCtx _)::(AppRCtx FindPred)::nil)).
      rewrite -(wp_bindi (BinOpLCtx _ _)).
      rewrite -wp_un_op //=.
      rewrite -wp_bin_op //= -!later_intro.
      rewrite -FindPred_spec. apply and_intro; first by (apply const_intro; omega).
      rewrite -wp_un_op //= -later_intro.
      assert (n - 1 = - (- n + 2 - 1)) as EQ by omega.
      by rewrite EQ.
109
    - rewrite -wp_if_false.
110
      rewrite -!later_intro -FindPred_spec.
Ralf Jung's avatar
Ralf Jung committed
111
      auto using and_intro, const_intro with omega.
112
  Qed.
Ralf Jung's avatar
Ralf Jung committed
113

114
  Goal  E,
Robbert Krebbers's avatar
Robbert Krebbers committed
115
    True  wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x")
Ralf Jung's avatar
Ralf Jung committed
116
                       (λ v, v = ('40)%L).
Ralf Jung's avatar
Ralf Jung committed
117
  Proof.
118 119 120
    intros E.
    rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
    rewrite -Pred_spec -!later_intro /=. by apply const_intro.
Ralf Jung's avatar
Ralf Jung committed
121
  Qed.
122
End LiftingTests.