rules.v 7.61 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.program_logic Require Import ectx_lifting.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
6
From iris.proofmode Require Import tactics.
Dan Frumin's avatar
Dan Frumin committed
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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
12
Class heapIG Σ := HeapIG {
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  heapI_invG : invG Σ;
Dan Frumin's avatar
Dan Frumin committed
14
  heapI_gen_heapG :> gen_heapG loc val Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
15
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

Dan Frumin's avatar
Dan Frumin committed
17 18 19 20 21
Instance heapIG_irisG `{heapIG Σ} : irisG lang Σ := {
  iris_invG := heapI_invG;
  state_interp := gen_heap_ctx
}.
Global Opaque iris_invG.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30
  Context `{heapIG Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32
  Implicit Types σ : state.

Dan Frumin's avatar
Dan Frumin committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 :
Dan Frumin's avatar
Dan Frumin committed
65
  {{{  l ↦ᵢ{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Proof.
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
73
  
74
  Lemma wp_store E l v' e v :
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 :
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 :
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  Proof. exact: wp_ectx_bind. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118

119
  Lemma wp_rec E e1 e2 v Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    to_val e2 = Some v 
121
     WP e1.[(Rec e1), e2 /] @ E {{ Φ }}  WP App (Rec e1) e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123
  Proof.
    intros <-%of_to_val.
Dan Frumin's avatar
Dan Frumin committed
124
    rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _) (e1.[Rec e1,of_val v/])); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127
  Qed.

128
  Lemma wp_tlam E e Φ :  WP e @ E {{ Φ }}  WP TApp (TLam e) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Proof.
Dan Frumin's avatar
Dan Frumin committed
130
    rewrite -(wp_lift_pure_det_head_step_no_fork (TApp _) e); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
  Qed.

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

143 144 145 146 147 148 149 150 151
  Lemma wp_pack E e1 e2 v Φ :
    to_val e1 = Some v 
     WP e2.[e1/] @ E {{ Φ }}  WP Unpack (Pack e1) e2 @ E {{ Φ }}.
  Proof.
    intros <-%of_to_val. 
    rewrite -(wp_lift_pure_det_head_step_no_fork (Unpack _ _) e2.[of_val v/]); eauto.
    intros; inv_head_step; eauto.
  Qed.

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

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

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

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

  Lemma wp_fork E e Φ :
187
     (|={E}=> Φ UnitV)   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  rewrite -(wp_lift_pure_det_head_step (Fork e) Unit [e]) //=; eauto.
190
  - by rewrite later_sep -(wp_value_fupd _ _ Unit) // big_sepL_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  - intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
194 195
  Lemma wp_if_true E e1 e2 Φ :
     WP e1 @ E {{ Φ }}  WP If (# true) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
  Proof.
Dan Frumin's avatar
Dan Frumin committed
197
    rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e1); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
201 202
  Lemma wp_if_false E e1 e2 Φ :
     WP e2 @ E {{ Φ }}  WP If (# false) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  Proof.
Dan Frumin's avatar
Dan Frumin committed
204
    rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e2); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207
  Qed.

208
  Lemma wp_nat_binop E op a b Φ :
Amin Timany's avatar
Amin Timany committed
209
     (|={E}=> Φ (binop_eval op a b))  WP BinOp op (#n a) (#n b) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
  Proof.
Dan Frumin's avatar
Dan Frumin committed
211
    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val _))
212
      -?wp_value_fupd'; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
    intros; inv_head_step; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
  Qed.
215
End lang_rules.