tests.v 4.79 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2
Require Import modures.logic.
3
Require Import barrier.lifting barrier.sugar.
4
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
5
6

Module LangTests.
7
8
  Definition add :=  Plus (LitNat 21) (LitNat 21).
  Goal  σ, prim_step add σ (LitNat 42) σ None.
Ralf Jung's avatar
Ralf Jung committed
9
  Proof.
10
    constructor.
Ralf Jung's avatar
Ralf Jung committed
11
12
  Qed.

13
  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
14
  Definition rec_app := App rec (LitNat 0).
Ralf Jung's avatar
Ralf Jung committed
15
16
  Goal  σ, prim_step rec_app σ rec_app σ None.
  Proof.
17
    move=>?. eapply BetaS.
Ralf Jung's avatar
Ralf Jung committed
18
19
20
    reflexivity.
  Qed.

21
22
  Definition lam := Lam (Plus (Var 0) (LitNat 21)).
  Goal  σ, prim_step (App lam (LitNat 21)) σ add σ None.
Ralf Jung's avatar
Ralf Jung committed
23
24
25
26
27
28
29
30
  Proof.
    move=>?. eapply BetaS. reflexivity.
  Qed.
End LangTests.

Module ParamTests.
  Print Assumptions Σ.
End ParamTests.
31
32
33
34

Module LiftingTests.
  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
  Definition e3 := Load (Var 0).
35
  Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
36
37
38
39
  Definition e := Let (Alloc (LitNat 1)) e2.
  Goal  σ E, (ownP (Σ:=Σ) σ)  (wp (Σ:=Σ) E e (λ v, (v = LitNatV 2))).
  Proof.
    move=> σ E. rewrite /e.
40
    rewrite -wp_let. rewrite -wp_alloc_pst; last done.
41
42
43
    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=>_.
44
    rewrite -later_intro. asimpl.
45
46
47
    rewrite -(wp_bind (SeqCtx EmptyCtx (Load (Loc _)))).
    rewrite -(wp_bind (StoreRCtx (LocV _) EmptyCtx)).
    rewrite -(wp_bind (PlusLCtx EmptyCtx _)).
48
49
50
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
    { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
Ralf Jung's avatar
Ralf Jung committed
51
    rewrite -wp_plus -later_intro.
52
53
54
55
    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
    { apply: lookup_insert. }
    { reflexivity. }
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
56
    rewrite -wp_lam // -later_intro. asimpl.
57
58
59
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
    { apply: lookup_insert. }
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
60
61
    by apply const_intro.
  Qed.
62
63
64
65
66
67
68
69

  Import Nat.

  Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
                                      (App f Sn1)
                                      n1.
  Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1))
                                     (FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))).
Ralf Jung's avatar
Ralf Jung committed
70
71
72
73
74
  Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
                             (LitNat 0)
                             (App (FindPred (Var 0)) (LitNat 0))
                         ).

75
76
77
78
79
80
81
82
83
84
85
86
87
  Lemma FindPred_spec n1 n2 E Q :
    ((n1 < n2)  Q (LitNatV $ pred n2)) 
       wp (Σ:=Σ) E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
  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.
    (* Go on. *)
    rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
    rewrite -wp_plus. asimpl.
88
    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
89
90
91
92
93
94
    rewrite -!later_intro. simpl.
    apply wp_lt; intros Hn12.
    - (* TODO RJ: It would be better if we could use wp_if_true here
         (and below). But we cannot, because the substitutions in there
         got already unfolded. *)
      rewrite -wp_case_inl //.
95
      rewrite -!later_intro. asimpl.
96
      rewrite (forall_elim (S n1)).
97
98
99
      eapply impl_elim; first by eapply and_elim_l. apply and_intro.
      + apply const_intro; omega.
      + by rewrite !and_elim_r.
Ralf Jung's avatar
Ralf Jung committed
100
    - rewrite -wp_case_inr //.
101
      rewrite -!later_intro -wp_value' //.
102
      rewrite and_elim_r. apply const_elim_l=>Hle.
103
104
105
106
107
108
109
      assert (Heq: n1 = pred n2) by omega. by subst n1.
  Qed.

  Lemma Pred_spec n E Q :
    Q (LitNatV $ pred n)  wp (Σ:=Σ) E (App Pred (LitNat n)) Q.
  Proof.
    rewrite -wp_lam //. asimpl.
110
    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
Ralf Jung's avatar
Ralf Jung committed
111
112
113
    apply later_mono, wp_le; intros Hn.
    - rewrite -wp_case_inl //.
      rewrite -!later_intro -wp_value' //.
114
      assert (Heq: n = 0) by omega. by subst n.
Ralf Jung's avatar
Ralf Jung committed
115
116
    - rewrite -wp_case_inr //.
      rewrite -!later_intro -FindPred_spec. apply and_intro.
117
118
      + by apply const_intro; omega.
      + done.
119
  Qed.
Ralf Jung's avatar
Ralf Jung committed
120
121
122
123
124
125
126

  Goal  E, True  wp (Σ:=Σ) E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, (v = LitNatV 40)).
  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.
127
End LiftingTests.