rules.v 7.51 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export invariants.
Amin Timany's avatar
Amin Timany committed
4 5
From iris.algebra Require Import auth frac agree gmap.
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.base_logic Require Export gen_heap.
7
From iris_examples.logrel.F_mu_ref_conc Require Export lang.
Amin Timany's avatar
Amin Timany committed
8 9 10 11 12 13 14 15 16 17 18
Import uPred.

(** The CMRA for the heap of the implementation. This is linked to the
    physical heap. *)
Class heapIG Σ := HeapIG {
  heapI_invG : invG Σ;
  heapI_gen_heapG :> gen_heapG loc val Σ;
}.

Instance heapIG_irisG `{heapIG Σ} : irisG F_mu_ref_conc_lang Σ := {
  iris_invG := heapI_invG;
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20
  state_interp σ κs _ := gen_heap_ctx σ;
  fork_post _ := True%I;
Amin Timany's avatar
Amin Timany committed
21 22 23 24
}.
Global Opaque iris_invG.

Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v)
Ralf Jung's avatar
Ralf Jung committed
25 26
  (at level 20, q at level 50, format "l  ↦ᵢ{ q }  v") : bi_scope.
Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : bi_scope.
27
Notation "l ↦ᵢ{-} v" := ( q, l ↦ᵢ{q} v)%I (at level 20, format "l  ↦ᵢ{-}  v") : bi_scope.
Amin Timany's avatar
Amin Timany committed
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42

Section lang_rules.
  Context `{heapIG Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
  Implicit Types σ : state.
  Implicit Types e : expr.
  Implicit Types v w : val.

  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]
Ralf Jung's avatar
Ralf Jung committed
43
  | H : head_step ?e _ _ _ _ _ |- _ =>
Amin Timany's avatar
Amin Timany committed
44 45 46 47 48
     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.

49 50
  Local Hint Extern 0 (atomic _) => solve_atomic : core.
  Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Amin Timany's avatar
Amin Timany committed
51

52 53 54
  Local Hint Constructors head_step : core.
  Local Hint Resolve alloc_fresh : core.
  Local Hint Resolve to_of_val : core.
Amin Timany's avatar
Amin Timany committed
55 56 57 58 59 60

  (** Base axioms for core primitives of the language: Stateful reductions. *)
  Lemma wp_alloc E e v :
    IntoVal e v 
    {{{ True }}} Alloc e @ E {{{ l, RET (LocV l); l ↦ᵢ v }}}.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
61
    iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
Amin Timany's avatar
Amin Timany committed
63
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
64
    iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
Amin Timany's avatar
Amin Timany committed
65 66 67 68 69 70 71
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
  Qed.

  Lemma wp_load E l q v :
  {{{  l ↦ᵢ{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}.
  Proof.
    iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
    iIntros (σ1 ???) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Amin Timany's avatar
Amin Timany committed
73 74 75 76 77
    iSplit; first by eauto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
  Qed.

78 79 80 81 82 83 84 85
  Lemma wp_load_frac E l v :
  {{{  l ↦ᵢ{-} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{-} v }}}.
  Proof.
    iIntros (Φ) ">Hl HΦ". iDestruct "Hl" as (q) "Hl".
    iApply (wp_load with "Hl"). iNext. iIntros "Hl".
    iApply "HΦ". by iExists q.
  Qed.

Amin Timany's avatar
Amin Timany committed
86 87 88 89 90
  Lemma wp_store E l v' e v :
    IntoVal e v 
    {{{  l ↦ᵢ v' }}} Store (Loc l) e @ E
    {{{ RET UnitV; l ↦ᵢ v }}}.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
91
    iIntros (<- Φ) ">Hl HΦ".
Amin Timany's avatar
Amin Timany committed
92
    iApply wp_lift_atomic_head_step_no_fork; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    iIntros (σ1 ???) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Amin Timany's avatar
Amin Timany committed
94 95 96 97 98 99 100 101 102 103
    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Φ".
  Qed.

  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
    IntoVal e1 v1  IntoVal e2 v2  v'  v1 
    {{{  l ↦ᵢ{q} v' }}} CAS (Loc l) e1 e2 @ E
    {{{ RET (BoolV false); l ↦ᵢ{q} v' }}}.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
104
    iIntros (<- <- ? Φ) ">Hl HΦ".
Amin Timany's avatar
Amin Timany committed
105
    iApply wp_lift_atomic_head_step_no_fork; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
    iIntros (σ1 ???) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Amin Timany's avatar
Amin Timany committed
107 108 109 110 111
    iSplit; first by eauto.
    iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
  Qed.

112 113 114 115 116 117 118 119 120 121
  Lemma wp_cas_fail_frac E l v' e1 v1 e2 v2 :
    IntoVal e1 v1  IntoVal e2 v2  v'  v1 
    {{{  l ↦ᵢ{-} v' }}} CAS (Loc l) e1 e2 @ E
    {{{ RET (BoolV false); l ↦ᵢ{-} v' }}}.
  Proof.
    iIntros (<- <- ? Φ) ">Hl HΦ". iDestruct "Hl" as (q) "Hl".
    iApply (wp_cas_fail with "Hl"); first done.
    iNext. iIntros "Hl". iApply "HΦ". by iExists q.
  Qed.

Amin Timany's avatar
Amin Timany committed
122 123 124 125 126
  Lemma wp_cas_suc E l e1 v1 e2 v2 :
    IntoVal e1 v1  IntoVal e2 v2 
    {{{  l ↦ᵢ v1 }}} CAS (Loc l) e1 e2 @ E
    {{{ RET (BoolV true); l ↦ᵢ v2 }}}.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
127
    iIntros (<- <- Φ) ">Hl HΦ".
Amin Timany's avatar
Amin Timany committed
128
    iApply wp_lift_atomic_head_step_no_fork; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
    iIntros (σ1 ???) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Amin Timany's avatar
Amin Timany committed
130 131 132 133 134 135 136 137
    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Φ".
  Qed.

  Lemma wp_fork E e Φ :
     (|={E}=> Φ UnitV)   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140
    iIntros "[He HΦ]". iApply wp_lift_atomic_head_step; [done|].
    iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
Amin Timany's avatar
Amin Timany committed
141 142
  Qed.

143 144 145 146 147 148
  Lemma mapsto_frac_duplicable l v :
    l ↦ᵢ{-} v - l ↦ᵢ{-} v  l ↦ᵢ{-} v.
  Proof.
    iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
  Qed.

Amin Timany's avatar
Amin Timany committed
149 150 151
  Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
  Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
  Local Ltac solve_pure_exec :=
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153 154 155
    unfold IntoVal in *;
    repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
    intros ?; apply nsteps_once, pure_head_step_pure_step;
      constructor; [solve_exec_safe | solve_exec_puredet].
Amin Timany's avatar
Amin Timany committed
156 157

  Global Instance pure_rec e1 e2 `{!AsVal e2} :
Robbert Krebbers's avatar
Robbert Krebbers committed
158
    PureExec True 1 (App (Rec e1) e2) e1.[(Rec e1), e2 /].
Amin Timany's avatar
Amin Timany committed
159 160
  Proof. solve_pure_exec. Qed.

161 162 163 164 165 166 167 168 169 170 171 172
  Global Instance pure_lam e1 e2 `{!AsVal e2} :
    PureExec True 1 (App (Lam e1) e2) e1.[e2 /].
  Proof. solve_pure_exec. Qed.

  Global Instance pure_LetIn e1 e2 `{!AsVal e1} :
    PureExec True 1 (LetIn e1 e2) e2.[e1 /].
  Proof. solve_pure_exec. Qed.

  Global Instance pure_seq e1 e2 `{!AsVal e1} :
    PureExec True 1 (Seq e1 e2) e2.
  Proof. solve_pure_exec. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Global Instance pure_tlam e : PureExec True 1 (TApp (TLam e)) e.
Amin Timany's avatar
Amin Timany committed
174 175 176
  Proof. solve_pure_exec. Qed.

  Global Instance pure_fold e `{!AsVal e}:
Robbert Krebbers's avatar
Robbert Krebbers committed
177
    PureExec True 1 (Unfold (Fold e)) e.
Amin Timany's avatar
Amin Timany committed
178 179 180
  Proof. solve_pure_exec. Qed.

  Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} :
Robbert Krebbers's avatar
Robbert Krebbers committed
181
    PureExec True 1 (Fst (Pair e1 e2)) e1.
Amin Timany's avatar
Amin Timany committed
182 183 184
  Proof. solve_pure_exec. Qed.

  Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} :
Robbert Krebbers's avatar
Robbert Krebbers committed
185
    PureExec True 1 (Snd (Pair e1 e2)) e2.
Amin Timany's avatar
Amin Timany committed
186 187 188
  Proof. solve_pure_exec. Qed.

  Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}:
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    PureExec True 1 (Case (InjL e0) e1 e2) e1.[e0/].
Amin Timany's avatar
Amin Timany committed
190 191 192
  Proof. solve_pure_exec. Qed.

  Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}:
Robbert Krebbers's avatar
Robbert Krebbers committed
193
    PureExec True 1 (Case (InjR e0) e1 e2) e2.[e0/].
Amin Timany's avatar
Amin Timany committed
194 195 196
  Proof. solve_pure_exec. Qed.

  Global Instance wp_if_true e1 e2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    PureExec True 1 (If (# true) e1 e2) e1.
Amin Timany's avatar
Amin Timany committed
198 199 200
  Proof. solve_pure_exec. Qed.

  Global Instance wp_if_false e1 e2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
201
    PureExec True 1 (If (# false) e1 e2) e2.
Amin Timany's avatar
Amin Timany committed
202 203 204
  Proof. solve_pure_exec. Qed.

  Global Instance wp_nat_binop op a b :
Robbert Krebbers's avatar
Robbert Krebbers committed
205
    PureExec True 1 (BinOp op (#n a) (#n b)) (of_val (binop_eval op a b)).
Amin Timany's avatar
Amin Timany committed
206 207 208
  Proof. solve_pure_exec. Qed.

End lang_rules.