rules_binary.v 16.3 KB
Newer Older
1
From iris.program_logic Require Import lifting.
2 3
From iris.algebra Require Import auth frac agree gmap list.
From iris.base_logic Require Import big_op.
4
From iris_logrel.F_mu_ref_conc Require Export rules notation.
5
From iris.proofmode Require Import tactics.
Amin Timany's avatar
Amin Timany committed
6 7
Import uPred.

8 9
Definition specN := nroot .@ "spec".

Robbert Krebbers's avatar
Robbert Krebbers committed
10
(** The CMRA for the heap of the specification. *)
11
Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC).
12
Definition cfgUR := prodUR tpoolUR (gen_heapUR loc val).
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14 15 16 17 18 19
Fixpoint to_tpool_go (i : nat) (tp : list expr) : tpoolUR :=
  match tp with
  | [] => 
  | e :: tp => <[i:=Excl e]>(to_tpool_go (S i) tp)
  end.
Definition to_tpool : list expr  tpoolUR := to_tpool_go 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21

(** The CMRA for the thread pool. *)
22 23 24 25 26
Class logrelG Σ := LogrelG {
  heap_inG :> heapG Σ;
  cfg_inG :> inG Σ (authR cfgUR);
  cfg_name : gname
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28

Section definitionsS.
29
  Context `{logrelG Σ}.
30

31
  Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
32
    own cfg_name ( (, {[ l := (q, to_agree v) ]})).
33 34
  Definition heapS_mapsto_aux : seal heapS_mapsto_def. by eexists. Qed.
  Definition heapS_mapsto := unseal heapS_mapsto_aux.
35
  Definition heapS_mapsto_eq :
36
    @heapS_mapsto = @heapS_mapsto_def := seal_eq heapS_mapsto_aux.
37

38
  Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
39
    own cfg_name ( ({[ j := Excl e ]}, )).
40 41
  Definition tpool_mapsto_aux : seal tpool_mapsto_def. by eexists. Qed.
  Definition tpool_mapsto := unseal tpool_mapsto_aux.
42
  Definition tpool_mapsto_eq :
43
    @tpool_mapsto = @tpool_mapsto_def := seal_eq tpool_mapsto_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
44

45
  Definition spec_inv (ρ : cfg lang) : iProp Σ :=
46
    ( tp σ, own cfg_name ( (to_tpool tp, to_gen_heap σ))
47
                  rtc step ρ (tp,σ))%I.
48
  Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
49
    inv specN (spec_inv ρ).
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53 54
End definitionsS.

Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
  (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : uPred_scope.
Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope.
55
Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
56

57
Section conversions.
58
  Context `{logrelG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60

  (** Conversion to tpools and back *)
61
  Lemma to_tpool_valid es :  to_tpool es.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Proof.
63 64
    rewrite /to_tpool. move: 0.
    induction es as [|e es]=> n //. by apply insert_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66
  Qed.

67
  Lemma tpool_lookup tp j : to_tpool tp !! j = Excl <$> tp !! j.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  Proof.
69 70 71 72 73
    cut ( i, to_tpool_go i tp !! (i + j) = Excl <$> tp !! j).
    { intros help. apply (help 0). }
    revert j. induction tp as [|e tp IH]=> //= -[|j] i /=.
    - by rewrite Nat.add_0_r lookup_insert.
    - by rewrite -Nat.add_succ_comm lookup_insert_ne; last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Qed.
75 76 77
  Lemma tpool_lookup_Some tp j e : to_tpool tp !! j = Excl' e  tp !! j = Some e.
  Proof. rewrite tpool_lookup fmap_Some. naive_solver. Qed.
  Hint Resolve tpool_lookup_Some.
Robbert Krebbers's avatar
Robbert Krebbers committed
78

79 80 81
  Lemma to_tpool_insert tp j e :
    j < length tp 
    to_tpool (<[j:=e]> tp) = <[j:=Excl e]> (to_tpool tp).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  Proof.
83 84 85 86
    intros. apply: map_eq=> i. destruct (decide (i = j)) as [->|].
    - by rewrite tpool_lookup lookup_insert list_lookup_insert.
    - rewrite tpool_lookup lookup_insert_ne // list_lookup_insert_ne //.
      by rewrite tpool_lookup.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  Qed.
88 89 90
  Lemma to_tpool_insert' tp j e :
    is_Some (to_tpool tp !! j) 
    to_tpool (<[j:=e]> tp) = <[j:=Excl e]> (to_tpool tp).
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  Proof.
92
    rewrite tpool_lookup fmap_is_Some lookup_lt_is_Some. apply to_tpool_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94
  Qed.

95 96
  Lemma to_tpool_snoc tp e :
    to_tpool (tp ++ [e]) = <[length tp:=Excl e]>(to_tpool tp).
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Proof.
98 99 100 101 102 103
    intros. apply: map_eq=> i.
    destruct (lt_eq_lt_dec i (length tp)) as [[?| ->]|?].
    - rewrite lookup_insert_ne; last lia. by rewrite !tpool_lookup lookup_app_l.
    - by rewrite lookup_insert tpool_lookup lookup_app_r // Nat.sub_diag.
    - rewrite lookup_insert_ne; last lia.
      rewrite !tpool_lookup ?lookup_ge_None_2 ?app_length //=;
104
         change (ofe_car exprC) with expr; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
  Qed.

107 108
  Lemma tpool_singleton_included tp j e :
    {[j := Excl e]}  to_tpool tp  tp !! j = Some e.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  Proof.
110 111
    move=> /singleton_included [ex [/leibniz_equiv_iff]].
    rewrite tpool_lookup fmap_Some=> [[e' [-> ->]] /Excl_included ?]. by f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
  Qed.
113 114 115
  Lemma tpool_singleton_included' tp j e :
    {[j := Excl e]}  to_tpool tp  to_tpool tp !! j = Excl' e.
  Proof. rewrite tpool_lookup. by move=> /tpool_singleton_included=> ->. Qed.
116 117 118
End conversions.

Section cfg.
119
  Context `{logrelG Σ}.
120 121 122 123 124 125 126 127 128 129 130
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
  Implicit Types σ : state.
  Implicit Types e : expr.
  Implicit Types v : val.

  Local Hint Resolve tpool_lookup.
  Local Hint Resolve tpool_lookup_Some.
  Local Hint Resolve to_tpool_insert.
  Local Hint Resolve to_tpool_insert'.
  Local Hint Resolve tpool_singleton_included.
131

132 133 134 135 136
  Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
  Proof. rewrite heapS_mapsto_eq. apply _. Qed.
  Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
  Proof. apply _. Qed.

137 138 139
  Lemma step_insert K tp j e σ e' σ' efs :
    tp !! j = Some (fill K e)  head_step e σ e' σ' efs 
    step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  Proof.
141 142 143 144 145
    intros. rewrite -(take_drop_middle tp j (fill K e)) //.
    rewrite insert_app_r_alt take_length_le ?Nat.sub_diag /=;
      eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite -(assoc_L (++)) /=.
    eapply step_atomic; eauto. by apply: Ectx_step'.
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147
  Qed.

148 149 150 151
  Lemma step_insert_no_fork K tp j e σ e' σ' :
    tp !! j = Some (fill K e)  head_step e σ e' σ' [] 
    step (tp, σ) (<[j:=fill K e']> tp, σ').
  Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152

153
  Lemma step_pure E ρ j K e e' :
154
    ( σ, head_step e σ e' σ []) 
155
    nclose specN  E 
156
    spec_ctx ρ  j  fill K e ={E}= j  fill K e'.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  Proof.
158
    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
159
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
160
    iDestruct (own_valid_2 with "Hown Hj")
161
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
162
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
163 164 165 166 167
    { by eapply auth_update, prod_local_update_1,
        singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). }
    iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ.
    rewrite to_tpool_insert'; last eauto.
    iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169
  Qed.

170 171
  Lemma step_alloc E ρ j K e v:
    to_val e = Some v  nclose specN  E 
172
    spec_ctx ρ  j  fill K (Alloc e) ={E}=  l, j  fill K (Loc l)  l ↦ₛ v.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Proof.
174
    iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto.
175 176
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
    destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
177
    iDestruct (own_valid_2 with "Hown Hj")
178
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
179
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
180 181 182 183
    { by eapply auth_update, prod_local_update_1,
        singleton_local_update, (exclusive_local_update _ (Excl (fill K (Loc l)))). }
    iMod (own_update with "Hown") as "[Hown Hl]".
    { eapply auth_update_alloc, prod_local_update_2,
184 185
        (alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
      by apply lookup_to_gen_heap_None. }
186 187
    iExists l. rewrite heapS_mapsto_eq /heapS_mapsto_def.
    iFrame "Hj Hl". iApply "Hclose". iNext.
188
    iExists (<[j:=fill K (Loc l)]> tp), (<[l:=v]>σ).
189
    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
190
    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
191 192
  Qed.

193 194
  Lemma step_load E ρ j K l q v:
    nclose specN  E 
195 196
    spec_ctx ρ  j  fill K (Load (Loc l))  l ↦ₛ{q} v
    ={E}= j  fill K (of_val v)  l ↦ₛ{q} v.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
  Proof.
198
    iIntros (?) "(#Hinv & Hj & Hl)".
199
    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
200
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
201
    iDestruct (own_valid_2 with "Hown Hj")
202
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
203 204
    iDestruct (own_valid_2 with "Hown Hl") 
      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_valid_discrete_2.     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
205 206 207 208 209 210
    { by eapply auth_update, prod_local_update_1, singleton_local_update,
        (exclusive_local_update _ (Excl (fill K (of_val v)))). }
    iFrame "Hj Hl". iApply "Hclose". iNext.
    iExists (<[j:=fill K (of_val v)]> tp), σ.
    rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212
  Qed.

213 214
  Lemma step_store E ρ j K l v' e v:
    to_val e = Some v  nclose specN  E 
215
    spec_ctx ρ  j  fill K (Store (Loc l) e)  l ↦ₛ v'
216
    ={E}= j  (fill K (Lit #())%E)  l ↦ₛ v.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  Proof.
218
    iIntros (??) "(#Hinv & Hj & Hl)".
219
    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
220
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
221
    iDestruct (own_valid_2 with "Hown Hj")
222
      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
223 224
    iDestruct (own_valid_2 with "Hown Hl")
      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
225
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
226
    { by eapply auth_update, prod_local_update_1, singleton_local_update,
227
        (exclusive_local_update _ (Excl (fill K (Lit #())%E))). }
228
    iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
229
    { eapply auth_update, prod_local_update_2, singleton_local_update,
230 231
        (exclusive_local_update _ (1%Qp, to_agree v)); last done.
      by rewrite /to_gen_heap lookup_fmap Hl. }
232
    iFrame "Hj Hl". iApply "Hclose". iNext.
233
    iExists (<[j:=fill K (Lit #())%E]> tp), (<[l:=v]>σ).
234
    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
235
    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237
  Qed.

238
  Lemma step_cas_fail E ρ j K l q v' e1 v1 e2 v2:
239
    to_val e1 = Some v1  to_val e2 = Some v2  nclose specN  E  v'  v1 
240 241
    spec_ctx ρ  j  fill K (CAS (Loc l) e1 e2)  l ↦ₛ{q} v'
    ={E}= j  fill K (# false)  l ↦ₛ{q} v'.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  Proof.
243
    iIntros (????) "(#Hinv & Hj & Hl)".
244
    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
245
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
246
    iDestruct (own_valid_2 with "Hown Hj")
247
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
248 249
    iDestruct (own_valid_2 with "Hown Hl")
      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
250
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
251 252 253 254 255 256
    { by eapply auth_update, prod_local_update_1, singleton_local_update,
        (exclusive_local_update _ (Excl (fill K (# false)))). }
    iFrame "Hj Hl". iApply "Hclose". iNext.
    iExists (<[j:=fill K (# false)]> tp), σ.
    rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
  Qed.

259
  Lemma step_cas_suc E ρ j K l e1 v1 v1' e2 v2:
260
    to_val e1 = Some v1  to_val e2 = Some v2  nclose specN  E  v1 = v1' 
261 262
    spec_ctx ρ  j  fill K (CAS (Loc l) e1 e2)  l ↦ₛ v1'
    ={E}= j  fill K (# true)  l ↦ₛ v2.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
  Proof.
264
    iIntros (????) "(#Hinv & Hj & Hl)"; subst.
265
    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
266
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
267
    iDestruct (own_valid_2 with "Hown Hj")
268
      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
269 270
    iDestruct (own_valid_2 with "Hown Hl")
      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
271
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
272 273
    { by eapply auth_update, prod_local_update_1, singleton_local_update,
        (exclusive_local_update _ (Excl (fill K (# true)))). }
274
    iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
275
    { eapply auth_update, prod_local_update_2, singleton_local_update,
276 277
        (exclusive_local_update _ (1%Qp, to_agree v2)); last done.
      by rewrite /to_gen_heap lookup_fmap Hl. }
278 279
    iFrame "Hj Hl". iApply "Hclose". iNext.
    iExists (<[j:=fill K (# true)]> tp), (<[l:=v2]>σ).
280
    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
281
    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283
  Qed.

284 285 286 287 288 289 290 291 292
  Lemma step_rec E ρ j K x f e1 e2 v :
    to_val e2 = Some v 
    Closed (x :b: f :b: ) e1 
    nclose specN  E 
    spec_ctx ρ  j  fill K (App (Rec f x e1) e2)
    ={E}= j  fill K (subst' f (Rec f x e1) (subst' x e2 e1)).
  Proof.
    intros ??. apply step_pure => σ. econstructor; eauto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
293

294
  Lemma step_tlam E ρ j K e :
295
    Closed  e 
296
    nclose specN  E 
297
    spec_ctx ρ  j  fill K (TApp (TLam e)) ={E}= j  fill K e.
298
  Proof. intros ?; apply step_pure => σ; econstructor; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299

300 301
  Lemma step_Fold E ρ j K e v :
    to_val e = Some v  nclose specN  E 
302
    spec_ctx ρ  j  fill K (Unfold (Fold e)) ={E}= j  fill K e.
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304
  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.

305 306 307
  Lemma step_Pack E ρ j K e1 e2 v :
    to_val e1 = Some v  nclose specN  E 
    spec_ctx ρ  j  fill K (Unpack (Pack e1) e2)
308
    ={E}= j  fill K (App e2 e1).
309 310
  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.

311 312
  Lemma step_fst E ρ j K e1 v1 e2 v2 :
    to_val e1 = Some v1  to_val e2 = Some v2  nclose specN  E 
313
    spec_ctx ρ  j  fill K (Fst (Pair e1 e2)) ={E}= j  fill K e1.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315
  Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.

316 317
  Lemma step_snd E ρ j K e1 v1 e2 v2 :
    to_val e1 = Some v1  to_val e2 = Some v2  nclose specN  E 
318
    spec_ctx ρ  j  fill K (Snd (Pair e1 e2)) ={E}= j  fill K e2.
Robbert Krebbers's avatar
Robbert Krebbers committed
319 320
  Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.

321 322
  Lemma step_case_inl E ρ j K e0 v0 e1 e2 :
    to_val e0 = Some v0  nclose specN  E 
323
    spec_ctx ρ  j  fill K (Case (InjL e0) e1 e2)
324
      ={E}= j  fill K (App e1 e0).
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.

327 328
  Lemma step_case_inr E ρ j K e0 v0 e1 e2 :
    to_val e0 = Some v0  nclose specN  E 
329
    spec_ctx ρ  j  fill K (Case (InjR e0) e1 e2)
330
      ={E}= j  fill K (App e2 e0).
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332
  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.

333 334
  Lemma step_if_false E ρ j K e1 e2 :
    nclose specN  E 
335
    spec_ctx ρ  j  fill K (If (# false) e1 e2) ={E}= j  fill K e2.
Robbert Krebbers's avatar
Robbert Krebbers committed
336 337
  Proof. apply step_pure => σ; econstructor. Qed.

338 339
  Lemma step_if_true E ρ j K e1 e2 :
    nclose specN  E 
340
    spec_ctx ρ  j  fill K (If (# true) e1 e2) ={E}= j  fill K e1.
Robbert Krebbers's avatar
Robbert Krebbers committed
341 342
  Proof. apply step_pure => σ; econstructor. Qed.

343
  Lemma step_nat_binop E ρ j K op a b :
344
    nclose specN  E 
345 346
    spec_ctx ρ  j  fill K (BinOp op (#n a) (#n b))
      ={E}= j  fill K (of_val (binop_eval op a b)).
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348
  Proof. apply step_pure => σ; econstructor. Qed.

349 350
  Lemma step_fork E ρ j K e :
    nclose specN  E 
351
    spec_ctx ρ  j  fill K (Fork e) ={E}=  j', j  fill K (Lit #())%E  j'  e.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
  Proof.
353
    iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
354
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
355
    iDestruct (own_valid_2 with "Hown Hj")
356 357
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
    assert (j < length tp) by eauto using lookup_lt_Some.
358
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
359
    { by eapply auth_update, prod_local_update_1,
360
        singleton_local_update, (exclusive_local_update _ (Excl (fill K (Lit Unit)))). }
361
    iMod (own_update with "Hown") as "[Hown Hfork]".
362 363 364 365 366
    { eapply auth_update_alloc, prod_local_update_1,
        (alloc_singleton_local_update _ (length tp) (Excl e)); last done.
      rewrite lookup_insert_ne ?tpool_lookup; last omega.
      by rewrite lookup_ge_None_2. }
    iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
367
    iExists (<[j:=fill K (Lit Unit)]> tp ++ [e]), σ.
368 369
    rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
    eapply rtc_r, step_insert; eauto. econstructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
  Qed.
371
End cfg.