bit.v 4.01 KB
Newer Older
1
From iris.proofmode Require Import tactics.
Dan Frumin's avatar
Dan Frumin committed
2
From iris_logrel Require Import logrel examples.lock.
Dan Frumin's avatar
Dan Frumin committed
3

4
Definition bitτ : type :=
Dan Frumin's avatar
Dan Frumin committed
5
  (TExists (TProd (TProd (TVar 0)
6
                         (TArrow (TVar 0) (TVar 0)))
Dan Frumin's avatar
Dan Frumin committed
7
                         (TArrow (TVar 0) (TBool)))).
8
Hint Unfold bitτ : typeable.
9

Dan Frumin's avatar
Dan Frumin committed
10
Definition bit_bool : val :=
Dan Frumin's avatar
Dan Frumin committed
11
  PackV (#true, (λ: "b", "b"  #true), (λ: "b", "b")).
Dan Frumin's avatar
Dan Frumin committed
12 13

Definition flip_nat : val := λ: "n",
14 15 16
  if: "n" = #0
  then #1
  else #0.
Dan Frumin's avatar
Dan Frumin committed
17
Definition bit_nat : val :=
Dan Frumin's avatar
Dan Frumin committed
18
  PackV (#1, flip_nat, (λ: "b", "b" = #1)).
Dan Frumin's avatar
Dan Frumin committed
19

20 21
(** * Typeability *)
(** ** Boolean bit *)
22
Lemma bit_bool_type Γ :
Dan Frumin's avatar
Dan Frumin committed
23
    typed Γ bit_bool bitτ.
Dan Frumin's avatar
Dan Frumin committed
24 25 26
Proof.
  unfold bitτ. simpl. unlock. solve_typed.
  (* TODO: solve_typed does not solve this one without simplifying/unlocking *)
27 28
Qed.
Hint Resolve bit_bool_type : typeable.
Dan Frumin's avatar
Dan Frumin committed
29

30
(** ** Integer bit *)
31 32 33 34 35 36 37 38 39 40 41 42
Lemma flip_nat_type Γ :
  typed Γ flip_nat (TArrow TNat TNat).
Proof. solve_typed. Qed.
Hint Resolve flip_nat_type : typeable.

Lemma bit_nat_type Γ :
  typed Γ bit_nat bitτ.
Proof.
  unfold bitτ.
  simpl. unlock.
  solve_typed.
Qed.
43
Hint Resolve bit_nat_type : typeable.
44 45 46 47

Section bit_refinement.
  Context `{logrelG Σ}.
  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Dan Frumin's avatar
Dan Frumin committed
48

49 50
  Definition bitf (b : bool) : nat :=
    match b with
Dan Frumin's avatar
Dan Frumin committed
51 52
    | true => 1
    | false => 0
53
    end.
Dan Frumin's avatar
Dan Frumin committed
54
  
55
  (* This is the graph of the `bitf` function *)
Dan Frumin's avatar
Dan Frumin committed
56
  Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv,
57
    ( b : bool, vv.1 = #b  vv.2 = #(bitf b))%I.
Dan Frumin's avatar
Dan Frumin committed
58 59
  Next Obligation. solve_proper. Qed.

Dan Frumin's avatar
Dan Frumin committed
60
  Instance bitτi_persistent ww : Persistent (bitτi ww).
Dan Frumin's avatar
Dan Frumin committed
61 62
  Proof. apply _. Qed.

63 64
  Lemma bit_prerefinement Γ :
    {Δ;Γ}  bit_bool log bit_nat : bitτ.
Dan Frumin's avatar
Dan Frumin committed
65
  Proof.
66
    unfold bit_bool, bit_nat; simpl. (* we need this to compute the coercion from values to expression *)
67
    iApply (bin_log_related_pack bitτi).
68
    repeat iApply bin_log_related_pair.
69
    - rel_vals; simpl; eauto. (* TODO: make a rel_finish tactic or change rel_vals *)
Dan Frumin's avatar
Dan Frumin committed
70
    - unfold flip_nat.
71
      iApply bin_log_related_arrow_val; try by unlock.
72 73 74 75
      iIntros "!#" (v1 v2) "/=". (* TODO: notation for LitV? *)
      iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
      rel_rec_l. rel_rec_r.
      rel_op_l. rel_op_r.
Dan Frumin's avatar
Dan Frumin committed
76 77
      destruct b; simpl; rel_if_r; rel_vals; simpl; eauto.
    - iApply bin_log_related_arrow_val; try by unlock.
78 79 80
      iIntros "!#" (v1 v2) "/=". (* TODO: notation for LitV? *)
      iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
      rel_rec_l. rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
81
      rel_op_r.
82
      destruct b; rel_vals; simpl; eauto.
Dan Frumin's avatar
Dan Frumin committed
83 84 85
  Qed.

End bit_refinement.
86 87 88 89 90 91 92

Theorem bit_ctx_refinement :
    bit_bool ctx bit_nat : bitτ.
Proof.
  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
  apply bit_prerefinement.
Qed.
93 94

Definition heapify : val := λ: "b", Unpack "b" $ λ: "b'",
Dan Frumin's avatar
Dan Frumin committed
95
  let: "init" := Fst (Fst "b'") in
96
  let: "flip" := Snd (Fst "b'") in
Dan Frumin's avatar
Dan Frumin committed
97
  let: "view" := Snd "b'" in
98
  let: "x" := ref "init" in
Dan Frumin's avatar
Dan Frumin committed
99 100
  let: "l" := newlock #() in
  let: "flip_ref" := λ: <>, acquire "l";; "x" <- "flip" (!"x");; release "l" in
101
  let: "view_ref" := λ: <>, "view" (!"x") in
Dan Frumin's avatar
Dan Frumin committed
102
  Pack (#(), "flip_ref", "view_ref").
103 104 105 106 107 108 109 110 111 112 113 114 115

Lemma heapify_type Γ :
  typed Γ heapify (TArrow bitτ bitτ).
Proof.
  unfold bitτ. unfold heapify.
  unlock.
  repeat (econstructor; solve_typed). (* TODO: solve_typed does not work by itself :( *)
Qed.
Hint Resolve heapify_type : typeable.

Section heapify_refinement.
  Context `{logrelG Σ}.
  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Dan Frumin's avatar
Dan Frumin committed
116
  Notation D := (prodC valC valC -n> iProp Σ).
117

118 119 120
  Lemma heapify_refinement_ez Γ b1 b2 :
    {Δ;Γ}  b1 log b2 : bitτ -
    {Δ;Γ}  heapify b1 log heapify b2 : bitτ.
121
  Proof.
122
    iIntros "Hb1b2".
123
    iApply bin_log_related_app; eauto.
124
    iApply binary_fundamental; eauto with typeable.
125
  Qed.
Dan Frumin's avatar
Dan Frumin committed
126

127 128 129 130 131 132 133 134 135 136
End heapify_refinement.

Theorem bit_heapify_ctx_refinement :
    heapify bit_bool ctx heapify bit_nat : bitτ.
Proof.
  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
  iStartProof.
  iApply heapify_refinement_ez; eauto.
  iApply bit_prerefinement.
Qed.