rules.v 7.75 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.program_logic Require Import ectx_lifting.
3 4
From iris.base_logic Require Export invariants big_op.
From iris.algebra Require Import auth frac agree gmap.
5
From iris_logrel.F_mu_ref_conc Require Export lang notation.
6
From iris.proofmode Require Import tactics.
7
From iris.base_logic Require Export gen_heap.
8 9
Import uPred.

Robbert Krebbers's avatar
Robbert Krebbers committed
10 11
(** The CMRA for the heap of the implementation. This is linked to the
    physical heap. *)
12 13 14
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
  heapG_gen_heapG :> gen_heapG loc val Σ;
15
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

17 18
Instance heapG_irisG `{heapG Σ} : irisG lang Σ := {
  iris_invG := heapG_invG;
19 20 21
  state_interp := gen_heap_ctx
}.
Global Opaque iris_invG.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23
Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  (at level 20, q at level 50, format "l  ↦ᵢ{ q }  v") : uPred_scope.
25
Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27
Section lang_rules.
28
  Context `{heapG Σ}.
29 30
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32
  Implicit Types σ : state.

33 34 35 36 37 38 39 40 41 42 43 44 45
  Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : _ = of_val ?v |- _ =>
     is_var v; destruct v; first[discriminate H|injection H as H]
  | H : head_step ?e _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

  Local Hint Extern 0 (atomic _) => solve_atomic.
46 47 48 49 50
  Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.

  Local Hint Constructors head_step.
  Local Hint Resolve alloc_fresh.
  Local Hint Resolve to_of_val.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52

  (** Base axioms for core primitives of the language: Stateful reductions. *)
53 54 55
  Lemma wp_alloc E e v :
    to_val e = Some v 
    {{{ True }}} Alloc e @ E {{{ l, RET (LocV l); l ↦ᵢ v }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  Proof.
57 58 59 60 61
    iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>"; iSplit; first by auto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
62 63
  Qed.

64
  Lemma wp_load E l q v :
65
  {{{  l ↦ᵢ{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Proof.
67 68 69 70 71
    iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
    iSplit; first by eauto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  Qed.
73
  
74
  Lemma wp_store E l v' e v :
75 76
    to_val e = Some v 
    {{{  l ↦ᵢ v' }}} Store (Loc l) e @ E
77
    {{{ RET UnitV; l ↦ᵢ v }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  Proof.
79 80 81 82 83 84
    iIntros (<-%of_to_val Φ) ">Hl HΦ".
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
    iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
    iModIntro. iSplit=>//. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
  Qed.

87
  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
88 89
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
    {{{  l ↦ᵢ{q} v' }}} CAS (Loc l) e1 e2 @ E
90
    {{{ RET (BoolV false); l ↦ᵢ{q} v' }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  Proof.
92 93 94 95 96 97
    iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
    iSplit; first by eauto.
    iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99
  Qed.

100
  Lemma wp_cas_suc E l e1 v1 e2 v2 :
101 102
    to_val e1 = Some v1  to_val e2 = Some v2 
    {{{  l ↦ᵢ v1 }}} CAS (Loc l) e1 e2 @ E
103
    {{{ RET (BoolV true); l ↦ᵢ v2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Proof.
105 106 107 108 109 110
    iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
    iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
    iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
    iModIntro. iSplit=>//. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
111 112 113 114 115 116
  Qed.

  (** Helper Lemmas for weakestpre. *)

  Lemma wp_bind {E e} K Φ :
    WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
117
  Proof. exact: wp_ectx_bind. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118

119 120 121 122 123
  Lemma wp_rec E f x erec e1 e2 Φ :
    e1 = Rec f x erec 
    is_Some (to_val e2) 
    Closed (x :b: f :b: ) erec 
     WP subst' f e1 (subst' x e2 erec) @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  Proof.
125 126 127
    intros -> [v2 ?] ?.
    rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
       (subst' f (Rec f x erec) (subst' x e2 erec))); eauto.
128
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
  Qed.

131
  Lemma wp_tlam E e Φ {Hcl: Closed  e} :  WP e @ E {{ Φ }}  WP TApp (TLam e) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Proof.
133
    rewrite -(wp_lift_pure_det_head_step_no_fork (TApp _) e); eauto.
134
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136
  Qed.

137
  Lemma wp_fold E e v Φ :
138
    to_val e = Some v   (|={E}=> Φ v)  WP Unfold (Fold e) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
  Proof.
    intros <-%of_to_val.
141
    rewrite -(wp_lift_pure_det_head_step_no_fork (Unfold _) (of_val v))
142
      -?wp_value_fupd; eauto.
143
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145
  Qed.

146 147
  Lemma wp_pack E e1 e2 v Φ :
    to_val e1 = Some v 
148
     WP (App e2 e1) @ E {{ Φ }}  WP Unpack (Pack e1) e2 @ E {{ Φ }}.
149 150
  Proof.
    intros <-%of_to_val. 
151
    rewrite -(wp_lift_pure_det_head_step_no_fork (Unpack _ _) _); eauto.
152 153 154
    intros; inv_head_step; eauto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
155 156
  Lemma wp_fst E e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2 
157
     (|={E}=> Φ v1)  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  Proof.
159
    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1)
160
      -?wp_value_fupd; eauto.
161
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163 164 165
  Qed.

  Lemma wp_snd E e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2 
166
     (|={E}=> Φ v2)  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  Proof.
168
    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2)
169
      -?wp_value_fupd; eauto.
170
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
171 172 173 174
  Qed.

  Lemma wp_case_inl E e0 v0 e1 e2 Φ :
    to_val e0 = Some v0 
175
     WP (App e1 e0) @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  Proof.
177
    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) _); eauto.
178
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182
  Qed.

  Lemma wp_case_inr E e0 v0 e1 e2 Φ :
    to_val e0 = Some v0 
183
     WP (App e2 e0) @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  Proof.
185
    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _)); eauto.
186
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189
  Qed.

  Lemma wp_fork E e Φ :
190
     (|={E}=> Φ UnitV)   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  Proof.
192
  rewrite -(wp_lift_pure_det_head_step (Fork e) Unit [e]) //=; eauto.
193 194
  - rewrite -(wp_value_fupd _ _ (Lit Unit)); auto.
    by rewrite -step_fupd_intro // right_id later_sep. 
195
  - intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197
  Qed.

198 199
  Lemma wp_if_true E e1 e2 Φ :
     WP e1 @ E {{ Φ }}  WP If (# true) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  Proof.
201
    rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e1); eauto.
202
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204
  Qed.

205 206
  Lemma wp_if_false E e1 e2 Φ :
     WP e2 @ E {{ Φ }}  WP If (# false) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  Proof.
208
    rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e2); eauto.
209
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211
  Qed.

212
  Lemma wp_nat_binop E op a b Φ :
213
     (|={E}=> Φ (binop_eval op a b))  WP BinOp op (#n a) (#n b) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
  Proof.
215
    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val _))
216
      -?wp_value_fupd'; eauto.
217
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  Qed.
219
End lang_rules.