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

  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))).
Ralf Jung's avatar
Ralf Jung committed
71
72
73
74
75
  Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
                             (LitNat 0)
                             (App (FindPred (Var 0)) (LitNat 0))
                         ).

76
77
78
79
80
81
82
83
84
85
86
87
88
  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.
89
90
    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
    rewrite -(wp_bind (LeLCtx EmptyCtx _)).
91
    rewrite -wp_plus -!later_intro. simpl.
Ralf Jung's avatar
Ralf Jung committed
92
93
    apply wp_le; intros Hn12.
    - rewrite -wp_case_inl //.
94
      rewrite -!later_intro. asimpl.
95
      rewrite (forall_elim (S n1)).
96
97
98
      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
99
    - rewrite -wp_case_inr //.
100
      rewrite -!later_intro -wp_value' //.
101
      rewrite and_elim_r. apply const_elim_l=>Hle.
102
103
104
105
106
107
108
      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.
109
    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
Ralf Jung's avatar
Ralf Jung committed
110
111
112
    apply later_mono, wp_le; intros Hn.
    - rewrite -wp_case_inl //.
      rewrite -!later_intro -wp_value' //.
113
      assert (Heq: n = 0) by omega. by subst n.
Ralf Jung's avatar
Ralf Jung committed
114
115
    - rewrite -wp_case_inr //.
      rewrite -!later_intro -FindPred_spec. apply and_intro.
116
117
      + by apply const_intro; omega.
      + done.
118
  Qed.
Ralf Jung's avatar
Ralf Jung committed
119
120
121
122
123
124
125

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