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

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

24 25 26 27
Section LiftingTests.
  Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
  Implicit Types P : iPropG heap_lang Σ.
  Implicit Types Q : val  iPropG heap_lang Σ.
28

29
  Definition e  : expr :=
30
    let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
31
  Goal  γh N, heap_ctx HeapI γh N  wp N e (λ v, v = '2).
32
  Proof.
33 34
    move=> γh N. rewrite /e.
    rewrite -(wp_bindi (LetCtx _ _)). eapply wp_alloc; eauto; [].
35
    rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
36 37
    rewrite -wp_let //= -later_intro.
    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))) /=. 
38 39
    rewrite -(wp_bindi (StoreRCtx (LocV _))) /=.
    rewrite -(wp_bindi (BinOpLCtx PlusOp _)) /=.
40 41
    eapply wp_load; eauto with I; []. apply sep_mono; first done.
    rewrite -later_intro; apply wand_intro_l.
42
    rewrite -wp_bin_op // -later_intro.
43 44
    eapply wp_store; eauto with I; []. apply sep_mono; first done.
    rewrite -later_intro. apply wand_intro_l.
45
    rewrite -wp_seq -wp_value' -later_intro.
46 47
    eapply wp_load; eauto with I; []. apply sep_mono; first done.
    rewrite -later_intro. apply wand_intro_l.
48 49
    by apply const_intro.
  Qed.
50

51
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
52
    rec: "pred" "x" "y" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
53
      let: "yp" := "y" + '1 in
54
      if: "yp" < "x" then "pred" "x" "yp" else "y".
55
  Definition Pred : val :=
56
    λ: "x",
57
      if: "x"  '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
Ralf Jung's avatar
Ralf Jung committed
58

59
  Lemma FindPred_spec n1 n2 E Q :
60
    ( (n1 < n2)  Q '(n2 - 1))  wp E (FindPred 'n2 'n1) Q.
61
  Proof.
62
    revert n1; apply löb_all_1=>n1.
63
    rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?.
64
    (* first need to do the rec to get a later *)
65
    wp_rec>.
66
    (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
67 68 69
    rewrite ->(later_intro (Q _)); rewrite -!later_and; apply later_mono.
    wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?.
    - wp_if. rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
70
      by rewrite left_id impl_elim_l.
71
    - assert (n1 = n2 - 1) as -> by omega.
72
      wp_if. auto with I.
73 74
  Qed.

75
  Lemma Pred_spec n E Q :  Q (LitV (n - 1))  wp E (Pred 'n)%L Q.
76
  Proof.
77
    wp_rec>; apply later_mono; wp_bin_op=> ?.
78 79 80 81 82
    - wp_if. wp_un_op. wp_bin_op.
      wp_focus (FindPred _ _); rewrite -FindPred_spec.
      apply and_intro; first auto with I omega.
      wp_un_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
    - wp_if. rewrite -FindPred_spec. auto with I omega.
83
  Qed.
Ralf Jung's avatar
Ralf Jung committed
84

85
  Goal  E,
86
    True  wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
Ralf Jung's avatar
Ralf Jung committed
87
  Proof.
88
    intros E.
89 90
    wp_focus (Pred '42); rewrite -Pred_spec -later_intro.
    wp_rec. rewrite -Pred_spec -later_intro; auto with I.
Ralf Jung's avatar
Ralf Jung committed
91
  Qed.
92
End LiftingTests.