rules_binary.v 16.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.program_logic Require Import lifting.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
backup    
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).
Dan Frumin's avatar
Dan Frumin committed
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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24

Section definitionsS.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
  Context `{cfgSG Σ, invG Σ}.

27
  Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
28
    own cfg_name ( (, {[ l := (q, to_agree v) ]})).
29
30
  Definition heapS_mapsto_aux : seal heapS_mapsto_def. by eexists. Qed.
  Definition heapS_mapsto := unseal heapS_mapsto_aux.
31
  Definition heapS_mapsto_eq :
32
    @heapS_mapsto = @heapS_mapsto_def := seal_eq heapS_mapsto_aux.
33

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

41
  Definition spec_inv (ρ : cfg lang) : iProp Σ :=
42
    ( tp σ, own cfg_name ( (to_tpool tp, to_gen_heap σ))
Dan Frumin's avatar
Dan Frumin committed
43
                  rtc step ρ (tp,σ))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
45
    inv specN (spec_inv ρ).
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
50
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.
51
Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
52

Dan Frumin's avatar
Dan Frumin committed
53
Section conversions.
54
  Context `{cfgSG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56

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

63
  Lemma tpool_lookup tp j : to_tpool tp !! j = Excl <$> tp !! j.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  Proof.
65
66
67
68
69
    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
70
  Qed.
71
72
73
  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
74

75
76
77
  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
78
  Proof.
79
80
81
82
    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
83
  Qed.
84
85
86
  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
87
  Proof.
88
    rewrite tpool_lookup fmap_is_Some lookup_lt_is_Some. apply to_tpool_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
  Qed.

91
92
  Lemma to_tpool_snoc tp e :
    to_tpool (tp ++ [e]) = <[length tp:=Excl e]>(to_tpool tp).
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  Proof.
94
95
96
97
98
99
    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 //=;
Dan Frumin's avatar
Dan Frumin committed
100
         change (ofe_car exprC) with expr; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
  Qed.

103
104
  Lemma tpool_singleton_included tp j e :
    {[j := Excl e]}  to_tpool tp  tp !! j = Some e.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  Proof.
106
107
    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
108
  Qed.
109
110
111
  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.
Dan Frumin's avatar
Dan Frumin committed
112
113
114
End conversions.

Section cfg.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
  Context `{heapIG Σ, cfgSG Σ}.
Dan Frumin's avatar
Dan Frumin committed
116
117
118
119
120
121
122
123
124
125
126
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
127

128
129
130
131
132
  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.

133
134
135
  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
136
  Proof.
137
138
139
140
141
    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
142
143
  Qed.

144
145
146
147
  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
148

149
  Lemma step_pure E ρ j K e e' :
Robbert Krebbers's avatar
Robbert Krebbers committed
150
    ( σ, head_step e σ e' σ []) 
151
    nclose specN  E 
152
    spec_ctx ρ  j  fill K e ={E}= j  fill K e'.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  Proof.
154
    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
155
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
156
    iDestruct (own_valid_2 with "Hown Hj")
157
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
Amin Timany's avatar
Amin Timany committed
158
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
159
160
161
162
163
    { 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
164
165
  Qed.

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

189
190
  Lemma step_load E ρ j K l q v:
    nclose specN  E 
191
192
    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
193
  Proof.
194
    iIntros (?) "(#Hinv & Hj & Hl)".
195
    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
196
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
197
    iDestruct (own_valid_2 with "Hown Hj")
198
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
199
200
    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]".
201
202
203
204
205
206
    { 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
207
208
  Qed.

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

234
  Lemma step_cas_fail E ρ j K l q v' e1 v1 e2 v2:
235
    to_val e1 = Some v1  to_val e2 = Some v2  nclose specN  E  v'  v1 
236
237
    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
238
  Proof.
239
    iIntros (????) "(#Hinv & Hj & Hl)".
240
    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
241
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
242
    iDestruct (own_valid_2 with "Hown Hj")
243
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
244
245
    iDestruct (own_valid_2 with "Hown Hl")
      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
Amin Timany's avatar
Amin Timany committed
246
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
247
248
249
250
251
252
    { 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
253
254
  Qed.

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

280
281
282
283
284
285
286
287
288
  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
289

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

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

301
302
303
  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)
304
    ={E}= j  fill K (App e2 e1).
305
306
  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.

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

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

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

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

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

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

339
  Lemma step_nat_binop E ρ j K op a b :
340
    nclose specN  E 
341
342
    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
343
344
  Proof. apply step_pure => σ; econstructor. Qed.

345
346
  Lemma step_fork E ρ j K e :
    nclose specN  E 
347
    spec_ctx ρ  j  fill K (Fork e) ={E}=  j', j  fill K (Lit #())%E  j'  e.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
  Proof.
349
    iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
350
    iInv specN as (tp σ) ">[Hown %]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
351
    iDestruct (own_valid_2 with "Hown Hj")
352
353
      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
    assert (j < length tp) by eauto using lookup_lt_Some.
Amin Timany's avatar
Amin Timany committed
354
    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
355
    { by eapply auth_update, prod_local_update_1,
356
        singleton_local_update, (exclusive_local_update _ (Excl (fill K (Lit Unit)))). }
Amin Timany's avatar
Amin Timany committed
357
    iMod (own_update with "Hown") as "[Hown Hfork]".
358
359
360
361
362
    { 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.
363
    iExists (<[j:=fill K (Lit Unit)]> tp ++ [e]), σ.
364
365
    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
366
  Qed.
367
End cfg.