translation.v 8.29 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1 2
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.algebra Require Import frac auth.
Dan Frumin's avatar
Dan Frumin committed
4
From iris_c.lib Require Import locking_heap mset flock U.
Dan Frumin's avatar
Dan Frumin committed
5
From iris_c.c_translation Require Import monad lifting proofmode.
Léon Gondelman's avatar
Léon Gondelman committed
6

Dan Frumin's avatar
Dan Frumin committed
7 8
Definition a_alloc : val := λ: "x",
  a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x".
Léon Gondelman's avatar
Léon Gondelman committed
9 10 11 12

Definition a_store : val := λ: "x1" "x2",
  a_bind (λ: "vv",
    a_atomic_env (λ: "env",
Dan Frumin's avatar
Dan Frumin committed
13
      mset_add (Fst "vv") "env" ;;
Léon Gondelman's avatar
Léon Gondelman committed
14 15 16 17 18 19 20 21
      Fst "vv" <- Snd "vv" ;;
      Snd "vv"
    )
  ) (a_par "x1" "x2").

Definition a_load : val := λ: "x",
  a_bind (λ: "v",
    a_atomic_env (λ: "env",
Dan Frumin's avatar
Dan Frumin committed
22
      assert: (mset_member "v" "env" = #false);;
Léon Gondelman's avatar
Léon Gondelman committed
23 24 25 26 27
      !"v"
    )
  ) "x".

Definition a_un_op (op : un_op) : val := λ: "x",
28
  a_bind (λ: "v", a_ret (λ: <>, UnOp op "v")) "x".
Léon Gondelman's avatar
Léon Gondelman committed
29 30 31

Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
  a_bind (λ: "vv",
32
    a_ret (BinOp op (Fst "vv") (Snd "vv"))
Léon Gondelman's avatar
Léon Gondelman committed
33 34 35 36
  ) (a_par "x1" "x2").

(* M () *)
(* The eta expansion is used to turn it into a value *)
37 38
Definition a_seq : val := λ: <>,
  a_atomic_env (λ: "env", mset_clear "env").
Dan Frumin's avatar
Dan Frumin committed
39

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
40 41
Definition a_seq_bind : val := λ: "e1" "e2",
  a_bind (λ: "x", a_seq #();;; "e2" "x") "e1".
42

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
43 44
Notation "e1 ;;;; e2" :=
  (a_seq_bind e1 (λ: <>, e2))%E (at level 80, right associativity).
45 46 47 48

Definition a_if : val := λ: "cnd" "e1" "e2",
  a_bind (λ: "c", if: "c" then "e1" else "e2") "cnd".

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
49 50 51
Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
    a_if "cnd" ("bdy" ;;;; "while" "cnd" "bdy") (a_ret #()).
52

Dan Frumin's avatar
Dan Frumin committed
53
Section proofs.
Dan Frumin's avatar
Dan Frumin committed
54
  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Dan Frumin's avatar
Dan Frumin committed
55

56
  Lemma a_seq_spec R Φ :
Dan Frumin's avatar
Dan Frumin committed
57
    U (Φ #()) -
58
    awp (a_seq #()) R Φ.
Dan Frumin's avatar
Dan Frumin committed
59
  Proof.
60
    iIntros "HΦ". rewrite /a_seq. awp_lam.
Dan Frumin's avatar
Dan Frumin committed
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
    iApply wp_fupd.
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
    wp_let. iApply (mset_clear_spec with "HX").
    iNext. iIntros "HX".
    iDestruct "HΦ" as (us) "[Hus HΦ]".
    clear Hlocks.
    iInduction us as [|u us] "IH" forall (σ); simpl.
    - iModIntro. iFrame "HR". iSplitR "HΦ".
      + iExists , σ. iFrame. iPureIntro.
        rewrite /correct_locks /set_Forall. set_solver.
      + by iApply "HΦ".
    - iDestruct "Hus" as "[Hu Hus]".
      iAssert (⌜σ !! u.1 = Some LLvl%I) with "[Hσ Hu]" as %?.
      { rewrite mapsto_eq /mapsto_def.
        iDestruct "Hu" as "[Hu Hl]".
          by iDestruct (own_valid_2 with "Hσ Hl")
            as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
      iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]".
      iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX").
      { iIntros "Hus". iApply "HΦ". by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
85
      { rewrite -bi.big_sepM_insert_override; eauto. }
Dan Frumin's avatar
Dan Frumin committed
86 87
  Qed.

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
88 89 90 91 92 93
  Lemma a_sequence_spec R Φ (e1 e2 : expr) :
    AsVal e2 
    awp e1 R (λ v, U (awp (e2 v) R Φ)) -
    awp (a_seq_bind e1 e2) R Φ.
  Proof.
    iIntros ([v2 <-%of_to_val]) "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95
    awp_apply (a_wp_awp with "H"); iIntros (v) "H".
    rewrite /a_seq_bind /=. do 2 awp_lam.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
96 97
    iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
    awp_lam. iApply awp_bind. iApply a_seq_spec.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
    iModIntro. by awp_lam.
99
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
100

101
  Lemma a_load_spec R (l : loc) (v : val) Φ :
Dan Frumin's avatar
Dan Frumin committed
102 103 104 105 106
    l U v -
    (l U v - Φ v) -
    awp (a_load (a_ret #l)) R Φ.
  Proof.
    unfold a_load. iIntros "Hv HΦ".
Dan Frumin's avatar
Dan Frumin committed
107
    rewrite /a_ret.
Dan Frumin's avatar
Dan Frumin committed
108
    do 2 awp_lam.
Dan Frumin's avatar
Dan Frumin committed
109 110
    iApply awp_bind.
    iApply awp_value.
Dan Frumin's avatar
Dan Frumin committed
111
    awp_let.
Dan Frumin's avatar
Dan Frumin committed
112 113
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
Dan Frumin's avatar
Dan Frumin committed
114 115 116 117 118 119 120 121 122 123
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
    iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
    assert (#l  X).
    { unfold correct_locks in *. intros Hx. apply Hl.
      destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
    wp_let.
    wp_apply wp_assert.
    wp_apply (mset_member_spec #l env with "HX").
124
    iIntros "Henv /=". case_decide; first by exfalso. simpl.
Dan Frumin's avatar
Dan Frumin committed
125 126
    wp_op. iSplit; eauto. iNext. wp_seq.
    rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". wp_load.
Dan Frumin's avatar
Dan Frumin committed
127 128 129 130
    iCombine "Hv Hl" as "Hv". iFrame "HR".
    iSplitR "HΦ Hv".
    - iExists X,σ. by iFrame.
    - by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
131 132
  Qed.

133 134
  Lemma a_alloc_spec R (ev : expr) (v : val) Φ :
    IntoVal ev v 
Dan Frumin's avatar
Dan Frumin committed
135
    ( l, l U v - Φ #l) -
136
    awp (a_alloc (a_ret ev)) R Φ.
Dan Frumin's avatar
Dan Frumin committed
137
  Proof.
138
    intros <-%of_to_val.
Dan Frumin's avatar
Dan Frumin committed
139 140 141 142 143 144 145
    unfold a_alloc. iIntros "HΦ".
    rewrite /a_ret.
    do 2 awp_lam.
    iApply awp_bind. iApply awp_value.
    awp_let.
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
Dan Frumin's avatar
Dan Frumin committed
146
    rewrite {2}/env_inv.
147 148
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
Dan Frumin's avatar
Dan Frumin committed
149 150
    iApply wp_fupd.
    wp_let. wp_alloc l as "Hl".
Dan Frumin's avatar
Dan Frumin committed
151 152
    iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
    { remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
      iExFalso. rewrite (bi.big_sepM_lookup _ σ l _); last eauto.
Dan Frumin's avatar
Dan Frumin committed
154 155
      iDestruct "Hls" as (v') "Hl'".
      by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
Dan Frumin's avatar
Dan Frumin committed
156 157
    iDestruct "Hl" as "[Hl Hl']".
    iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
Dan Frumin's avatar
Dan Frumin committed
158 159
    iModIntro. iFrame "HR". iSplitR "HΦ Hl'".
    - iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
      + rewrite bi.big_sepM_insert; eauto. iFrame. eauto.
Dan Frumin's avatar
Dan Frumin committed
161 162
      + iPureIntro. by rewrite locked_locs_alloc_unlocked.
    - by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
163
  Qed.
Dan Frumin's avatar
Dan Frumin committed
164

Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
165 166 167 168 169 170
  Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
    awp e1 R (λ v,  l : loc, v = #l  Ψ1 l)-
    awp e2 R Ψ2 -
    ( (l : loc) w,
      Ψ1 l - Ψ2 w - ( v, l U v  (l L w - Φ w))) -
    awp (a_store e1 e2) R Φ.
Dan Frumin's avatar
Dan Frumin committed
171
  Proof.
Robbert Krebbers's avatar
WIP  
Robbert Krebbers committed
172
    iIntros "H1 H2 HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
    iApply awp_bind. iApply (awp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". iDestruct "H1" as (l ->) "H1". awp_lam.
    iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
Dan Frumin's avatar
Dan Frumin committed
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
    iApply awp_atomic_env.
    iIntros (env) "Henv HR".
    rewrite {2}/env_inv.
    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
    iDestruct "Hlocks" as %Hlocks.
    iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
    assert (#l  X).
    { unfold correct_locks in *. intros Hx. apply Hl.
      destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
    wp_let. wp_proj.
    wp_apply (mset_add_spec with "[$HX]"); eauto.
    iIntros "HX". wp_seq.
    iAssert (⌜σ !! l = Some ULvl%I) with "[Hσ Hv]" as %?.
    { rewrite mapsto_eq /mapsto_def.
      iDestruct "Hv" as "[Hv Hl]".
      by iDestruct (own_valid_2 with "Hσ Hl")
        as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
    iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]".
    do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
    iDestruct "Hv" as "[Hv Hl]".
Robbert Krebbers's avatar
Robbert Krebbers committed
198
    rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done.
Dan Frumin's avatar
Dan Frumin committed
199 200 201 202 203 204 205 206 207
    iDestruct "Hls" as "[Hl' Hls]".
    iDestruct "Hl'" as (?) "Hl'".
    iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
    iCombine "Hv Hl'" as "Hv".
    wp_store.
    iDestruct "Hv" as "[Hv Hl']".
    iSpecialize ("Hls" with "[Hl']"); eauto.
    wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv".
    - iExists ({[#l]}  X),(<[l:=LLvl]> σ). iFrame. iSplitL.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
      + rewrite -bi.big_sepM_insert_override; eauto.
Dan Frumin's avatar
Dan Frumin committed
209 210 211 212 213 214
      + (* TODO: a separate lemma somewhere *)
        iPureIntro. rewrite locked_locs_lock.
        revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
    - iApply "HΦ". iFrame.
  Qed.

215
  Lemma a_if_true_spec R (e1 e2 : val) Φ :
216 217
     awp e1 R Φ - awp (a_if (a_ret #true) e1 e2) R Φ.
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
218 219
    iIntros "HΦ".
    do 4 awp_lam.
220 221 222
    iApply awp_bind.
    iApply awp_value.
    awp_lam. by awp_if_true.
223 224
  Qed.

225
  Lemma a_if_false_spec R (e1 e2 : val) Φ :
226 227
     awp e2 R Φ - awp (a_if (a_ret #false) e1 e2) R Φ.
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
228 229
    iIntros "HΦ".
    do 4 awp_lam.
230 231 232
    iApply awp_bind.
    iApply awp_value.
    awp_lam. by awp_if_false.
233
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
234 235 236 237 238 239 240 241

  Lemma a_if_spec R (e e1 e2 : val) Φ:
    awp e R (λ cnd, (cnd = #true  awp e1 R Φ)  (cnd = #false  awp e2 R Φ)) -
    awp (a_if e e1 e2) R Φ.
  Proof.
    iIntros "HΦ". do 3 awp_lam.
    iApply awp_bind. iApply (awp_wand with "HΦ").
    iIntros (v) "[[% H] | [% H]]"; subst; by repeat awp_pure _.
242
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
243 244


Dan Frumin's avatar
Dan Frumin committed
245
End proofs.