tests.v 4.71 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2
3
4
Require Import modures.logic.
Require Import barrier.lifting.
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83

  Import Nat.

  Definition Lt e1 e2 := Le (Plus e1 $ LitNat 1) e2.
  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))).
  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.
84
85
    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
    rewrite -(wp_bind (LeLCtx EmptyCtx _)).
86
    rewrite -wp_plus -!later_intro. simpl.
Ralf Jung's avatar
Ralf Jung committed
87
88
    apply wp_le; intros Hn12.
    - rewrite -wp_case_inl //.
89
      rewrite -!later_intro. asimpl.
90
      rewrite (forall_elim (S n1)).
91
92
93
      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
94
    - rewrite -wp_case_inr //.
95
      rewrite -!later_intro -wp_value' //.
96
      rewrite and_elim_r. apply const_elim_l=>Hle.
97
98
99
100
101
102
103
104
105
106
107
      assert (Heq: n1 = pred n2) by omega. by subst n1.
  Qed.

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

  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.
125
End LiftingTests.