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

Module LangTests.
7
8
  Definition add := (Lit 21 + Lit 21)%L.
  Goal  σ, prim_step add σ (Lit 42) σ None.
9
  Proof. intros; do_step done. Qed.
10
  Definition rec_app : expr := (rec:: #0 #1) (Lit 0).
Ralf Jung's avatar
Ralf Jung committed
11
  Goal  σ, prim_step rec_app σ rec_app σ None.
12
  Proof. Set Printing All. intros; do_step done. Qed.
13
14
  Definition lam : expr := λ: #0 + Lit 21.
  Goal  σ, prim_step (lam (Lit 21)) σ add σ None.
15
16
17
18
19
  Proof.
    (* FIXME WTF why does it print all the "S (S (S..."?? *)
    rewrite /lam /Lam.
    intros; do_step done.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
20
21
End LangTests.

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

27
28
  Definition e  : expr := let: ref (Lit 1) in #0 <- !#0 + Lit 1; !#0.
  Goal  σ E, (ownP σ : iProp heap_lang Σ)  (wp E e (λ v, (v = LitV 2))).
29
30
  Proof.
    move=> σ E. rewrite /e.
31
    rewrite -wp_let. rewrite -wp_alloc_pst; last done.
32
33
34
    apply sep_intro_True_r; first done.
    rewrite -later_intro. apply forall_intro=>l.
    apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
35
    rewrite -later_intro. asimpl.
36
    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
37
    (* FIXME: doing simpl here kills the Seq, turns it all the way into Rec *)
38
    rewrite -(wp_bindi (StoreRCtx (LocV _))).
39
    rewrite -(wp_bindi (BinOpLCtx PlusOp _)).
40
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
41
    { by rewrite lookup_insert. } (* RJ FIXME: figure out why apply and eapply fail. *)
42
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
43
    rewrite -wp_bin_op // -later_intro.
44
    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
45
46
    { by rewrite lookup_insert. }
    { done. }
47
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
48
    rewrite -wp_seq -wp_value -later_intro.
49
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
50
    { by rewrite lookup_insert. }
51
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
52
53
    by apply const_intro.
  Qed.
54

55
  Definition FindPred (n2 : expr) : expr :=
56
    rec:: (let: #1 + Lit 1 in if #0 < n2.[ren(+3)] then #1 #0 else #2).
57
  Definition Pred : expr :=
58
    λ: (if #0  Lit 0 then Lit 0 else FindPred #0 (Lit 0))%L.
Ralf Jung's avatar
Ralf Jung committed
59

60
  Lemma FindPred_spec n1 n2 E Q :
61
    ( (n1 < n2)  Q (LitV $ pred n2))  wp E (FindPred (Lit n2) (Lit n1)) Q.
62
63
64
65
66
67
68
  Proof.
    revert n1. apply löb_all_1=>n1.
    rewrite -wp_rec //. asimpl.
    (* Get rid of the ▷ in the premise. *)
    etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
    { apply and_mono; first done. by rewrite -later_intro. }
    apply later_mono.
69
    (* Go on *)
70
    rewrite -wp_let.
71
72
    rewrite -wp_bin_op //. asimpl.
    rewrite -(wp_bindi (IfCtx _ _)).
73
    rewrite -!later_intro /=.
74
    apply wp_lt; intros Hn12.
75
    * rewrite -wp_if_true.
76
      rewrite -!later_intro. asimpl.
77
      rewrite (forall_elim (S n1)).
78
79
80
      eapply impl_elim; first by eapply and_elim_l. apply and_intro.
      + apply const_intro; omega.
      + by rewrite !and_elim_r.
81
    * rewrite -wp_if_false.
82
      rewrite -!later_intro -wp_value' //.
83
      rewrite and_elim_r. apply const_elim_l=>Hle.
Ralf Jung's avatar
Ralf Jung committed
84
      by replace n1 with (pred n2) by omega.
85
86
87
  Qed.

  Lemma Pred_spec n E Q :
88
    Q (LitV $ pred n)  wp E (Pred $ Lit n) Q.
89
90
  Proof.
    rewrite -wp_lam //. asimpl.
91
    rewrite -(wp_bindi (IfCtx _ _)).
92
    apply later_mono, wp_le=> Hn.
93
    - rewrite -wp_if_true.
Ralf Jung's avatar
Ralf Jung committed
94
      rewrite -!later_intro -wp_value' //.
Ralf Jung's avatar
Ralf Jung committed
95
      by replace n with 0 by omega.
96
    - rewrite -wp_if_false.
97
      rewrite -!later_intro -FindPred_spec.
Ralf Jung's avatar
Ralf Jung committed
98
      auto using and_intro, const_intro with omega.
99
  Qed.
Ralf Jung's avatar
Ralf Jung committed
100

101
  Goal  E,
102
    True  wp (Σ:=Σ) E (let: Pred $ Lit 42 in Pred #0) (λ v, (v = LitV 40)).
Ralf Jung's avatar
Ralf Jung committed
103
104
105
106
107
  Proof.
    intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
    asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
    rewrite -Pred_spec -later_intro. by apply const_intro.
  Qed.
108
End LiftingTests.