type.v 26.8 KB
Newer Older
1
From iris.base_logic.lib Require Export na_invariants.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.base_logic Require Import big_op.
3
From lrust.lang Require Export proofmode notation.
4
From lrust.lifetime Require Export frac_borrow.
5
From lrust.typing Require Export base.
6
From lrust.typing Require Import lft_contexts.
7
Set Default Proof Using "Type".
8

9
Class typeG Σ := TypeG {
10
  type_heapG :> lrustG Σ;
11
  type_lftG :> lftG Σ;
12
  type_na_invG :> na_invG Σ;
13
  type_frac_borrowG :> frac_borG Σ
14
}.
15

Ralf Jung's avatar
Ralf Jung committed
16
Definition lftE : coPset := lftN.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
17
Definition lrustN := nroot .@ "lrust".
18
Definition shrN  := lrustN .@ "shr".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
19

20
21
22
23
24
25
26
Definition thread_id := na_inv_pool_name.

Record type `{typeG Σ} :=
  { ty_size : nat;
    ty_own : thread_id  list val  iProp Σ;
    ty_shr : lft  thread_id  loc  iProp Σ;

Ralf Jung's avatar
Ralf Jung committed
27
    ty_shr_persistent κ tid l : Persistent (ty_shr κ tid l);
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

    ty_size_eq tid vl : ty_own tid vl - length vl = ty_size;
    (* The mask for starting the sharing does /not/ include the
       namespace N, for allowing more flexibility for the user of
       this type (typically for the [own] type). AFAIK, there is no
       fundamental reason for this.
       This should not be harmful, since sharing typically creates
       invariants, which does not need the mask.  Moreover, it is
       more consistent with thread-local tokens, which we do not
       give any.

       The lifetime token is needed (a) to make the definition of simple types
       nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
       we can have emp == sum [].
     *)
    ty_share E κ l tid q : lftE  E 
      lft_ctx - &{κ} (l ↦∗: ty_own tid) - q.[κ] ={E}=
      ty_shr κ tid l  q.[κ];
    ty_shr_mono κ κ' tid l :
47
      κ'  κ - ty_shr κ tid l - ty_shr κ' tid l
48
49
50
51
52
53
  }.
Existing Instance ty_shr_persistent.
Instance: Params (@ty_size) 2.
Instance: Params (@ty_own) 2.
Instance: Params (@ty_shr) 2.

54
Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
Ralf Jung's avatar
Ralf Jung committed
55

56
57
58
59
60
Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
Arguments ty_lfts {_ _} _ {_}.
Arguments ty_wf_E {_ _} _ {_}.

Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
61
  (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
62
63
64
65
66
67
68
69
70
71
72
73
74
75

Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
  ty.(ty_outlives_E) β + E 
  lctx_lft_incl E L α β 
  elctx_sat E L (ty.(ty_outlives_E) α).
Proof.
  unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
  - solve_typing.
  - apply elctx_sat_lft_incl.
    + etrans; first done. eapply lctx_lft_incl_external, elem_of_submseteq, Hsub.
      set_solver.
    + apply IH, Hαβ. etrans; last done. by apply submseteq_cons.
Qed.

Ralf Jung's avatar
comment    
Ralf Jung committed
76
(* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
77
78
79
80
81
82
83
84
85
Inductive TyWfLst `{typeG Σ} : list type  Type :=
| tyl_wf_nil : TyWfLst []
| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
Existing Class TyWfLst.
Existing Instances tyl_wf_nil tyl_wf_cons.

Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
  match WF with
  | tyl_wf_nil => []
86
87
  | tyl_wf_cons ty [] => ty.(ty_lfts)
  | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
88
89
90
91
92
  end.

Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
  match WF with
  | tyl_wf_nil => []
93
94
  | tyl_wf_cons ty [] => ty.(ty_wf_E)
  | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
95
96
97
98
99
  end.

Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
  match WF with
  | tyl_wf_nil => []
100
101
  | tyl_wf_cons ty [] => ty.(ty_outlives_E) κ
  | tyl_wf_cons ty tyl => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
102
103
104
105
106
107
108
  end.

Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
  tyl.(tyl_outlives_E) β + E 
  lctx_lft_incl E L α β 
  elctx_sat E L (tyl.(tyl_outlives_E) α).
Proof.
109
  induction WF as [|? [] ?? IH]=>/=.
110
  - solve_typing.
111
  - intros. by eapply ty_outlives_E_elctx_sat.
112
113
114
115
  - intros. apply elctx_sat_app, IH; [eapply ty_outlives_E_elctx_sat| |]=>//;
      (etrans; [|done]); solve_typing.
Qed.

116
117
118
Record simple_type `{typeG Σ} :=
  { st_own : thread_id  list val  iProp Σ;
    st_size_eq tid vl : st_own tid vl - length vl = 1%nat;
Ralf Jung's avatar
Ralf Jung committed
119
    st_own_persistent tid vl : Persistent (st_own tid vl) }.
120
121
122
Existing Instance st_own_persistent.
Instance: Params (@st_own) 2.

Ralf Jung's avatar
Ralf Jung committed
123
124
125
126
127
128
Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
  {| ty_size := 1; ty_own := st.(st_own);
     (* [st.(st_own) tid vl] needs to be outside of the fractured
         borrow, otherwise I do not know how to prove the shr part of
         [subtype_shr_mono]. *)
     ty_shr := λ κ tid l,
129
               ( vl, &frac{κ} (λ q, l ↦∗{q} vl)   st.(st_own) tid vl)%I
Ralf Jung's avatar
Ralf Jung committed
130
131
132
133
  |}.
Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
  iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
134
135
  iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
  iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
136
137
  iMod (bor_persistent_tok with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
  iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
Ralf Jung's avatar
Ralf Jung committed
138
139
140
141
142
143
Qed.
Next Obligation.
  iIntros (?? st κ κ' tid l) "#Hord H".
  iDestruct "H" as (vl) "[#Hf #Hown]".
  iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
Qed.
144

145
Coercion ty_of_st : simple_type >-> type.
146

147
148
Delimit Scope lrust_type_scope with T.
Bind Scope lrust_type_scope with type.
149

150
151
152
153
(* OFE and COFE structures on types and simple types. *)
Section ofe.
  Context `{typeG Σ}.

154
155
156
157
158
159
160
161
162
163
  Inductive type_equiv' (ty1 ty2 : type) : Prop :=
    Type_equiv :
      ty1.(ty_size) = ty2.(ty_size) 
      ( tid vs, ty1.(ty_own) tid vs  ty2.(ty_own) tid vs) 
      ( κ tid l, ty1.(ty_shr) κ tid l  ty2.(ty_shr) κ tid l) 
      type_equiv' ty1 ty2.
  Instance type_equiv : Equiv type := type_equiv'.
  Inductive type_dist' (n : nat) (ty1 ty2 : type) : Prop :=
    Type_dist :
      ty1.(ty_size) = ty2.(ty_size) 
Ralf Jung's avatar
Ralf Jung committed
164
      ( tid vs, ty1.(ty_own) tid vs {n} ty2.(ty_own) tid vs) 
165
166
167
168
169
      ( κ tid l, ty1.(ty_shr) κ tid l {n} ty2.(ty_shr) κ tid l) 
      type_dist' n ty1 ty2.
  Instance type_dist : Dist type := type_dist'.

  Let T := prodC
Ralf Jung's avatar
Ralf Jung committed
170
    (prodC natC (thread_id -c> list val -c> iProp Σ))
171
172
    (lft -c> thread_id -c> loc -c> iProp Σ).
  Let P (x : T) : Prop :=
Ralf Jung's avatar
Ralf Jung committed
173
    ( κ tid l, Persistent (x.2 κ tid l)) 
Ralf Jung's avatar
Ralf Jung committed
174
    ( tid vl, x.1.2 tid vl - length vl = x.1.1) 
175
    ( E κ l tid q, lftE  E 
Ralf Jung's avatar
Ralf Jung committed
176
      lft_ctx - &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -
177
      q.[κ] ={E}= x.2 κ tid l  q.[κ]) 
178
    ( κ κ' tid l, κ'  κ - x.2 κ tid l - x.2 κ' tid l).
179
180

  Definition type_unpack (ty : type) : T :=
Ralf Jung's avatar
Ralf Jung committed
181
    (ty.(ty_size), λ tid vl, (ty.(ty_own) tid vl), ty.(ty_shr)).
182
  Program Definition type_pack (x : T) (H : P x) : type :=
Ralf Jung's avatar
Ralf Jung committed
183
    {| ty_size := x.1.1; ty_own tid vl := x.1.2 tid vl; ty_shr := x.2 |}.
184
185
186
187
188
189
190
191
192
193
194
  Solve Obligations with by intros [[??] ?] (?&?&?&?).

  Definition type_ofe_mixin : OfeMixin type.
  Proof.
    apply (iso_ofe_mixin type_unpack).
    - split; [by destruct 1|by intros [[??] ?]; constructor].
    - split; [by destruct 1|by intros [[??] ?]; constructor].
  Qed.
  Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.

  Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
195
  Proof. intros ?? EQ. apply EQ. Qed.
196
  Global Instance ty_size_proper : Proper (() ==> eq) ty_size.
197
198
  Proof. intros ?? EQ. apply EQ. Qed.
  Global Instance ty_own_ne n:
Ralf Jung's avatar
Ralf Jung committed
199
    Proper (dist n ==> eq ==> eq ==> dist n) ty_own.
200
  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
201
  Global Instance ty_own_proper : Proper (() ==> eq ==> eq ==> ()) ty_own.
202
  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
203
  Global Instance ty_shr_ne n :
204
205
    Proper (dist n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
206
  Global Instance ty_shr_proper :
207
208
209
    Proper (() ==> eq ==> eq ==> eq ==> ()) ty_shr.
  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.

210
211
  Global Instance type_cofe : Cofe typeC.
  Proof.
212
213
    apply (iso_cofe_subtype' P type_pack type_unpack).
    - by intros [].
214
215
    - split; [by destruct 1|by intros [[??] ?]; constructor].
    - by intros [].
216
217
    - (* TODO: automate this *)
      repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
Ralf Jung's avatar
Ralf Jung committed
218
      + apply uPred.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
219
220
221
      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
222
  Qed.
223
224
225
226
227
228
229
230

  Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
    St_equiv :
      ( tid vs, ty1.(ty_own) tid vs  ty2.(ty_own) tid vs) 
      st_equiv' ty1 ty2.
  Instance st_equiv : Equiv simple_type := st_equiv'.
  Inductive st_dist' (n : nat) (ty1 ty2 : simple_type) : Prop :=
    St_dist :
Ralf Jung's avatar
Ralf Jung committed
231
      ( tid vs, ty1.(ty_own) tid vs {n} (ty2.(ty_own) tid vs)) 
232
233
234
      st_dist' n ty1 ty2.
  Instance st_dist : Dist simple_type := st_dist'.

Ralf Jung's avatar
Ralf Jung committed
235
236
  Definition st_unpack (ty : simple_type) : thread_id -c> list val -c> iProp Σ :=
    λ tid vl, ty.(ty_own) tid vl.
237
238
239
240
241
242

  Definition st_ofe_mixin : OfeMixin simple_type.
  Proof.
    apply (iso_ofe_mixin st_unpack).
    - split; [by destruct 1|by constructor].
    - split; [by destruct 1|by constructor].
243
  Qed.
244
245
246
  Canonical Structure stC : ofeT := OfeT simple_type st_ofe_mixin.

  Global Instance st_own_ne n :
Ralf Jung's avatar
Ralf Jung committed
247
    Proper (dist n ==> eq ==> eq ==> dist n) st_own.
248
249
250
  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
  Global Instance st_own_proper : Proper (() ==> eq ==> eq ==> ()) st_own.
  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
251

252
  Global Instance ty_of_st_ne : NonExpansive ty_of_st.
253
  Proof.
254
    intros n ?? EQ. constructor; try apply EQ. done.
Ralf Jung's avatar
Ralf Jung committed
255
    - simpl. intros; repeat f_equiv. apply EQ.
256
  Qed.
257
258
  Global Instance ty_of_st_proper : Proper (() ==> ()) ty_of_st.
  Proof. apply (ne_proper _). Qed.
259
260
End ofe.

Ralf Jung's avatar
Ralf Jung committed
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
(** Special metric for type-nonexpansive and Type-contractive functions. *)
Section type_dist2.
  Context `{typeG Σ}.

  (* Size and shr are n-equal, but own is only n-1-equal.
     We need this to express what shr has to satisfy on a Type-NE-function:
     It may only depend contractively on own. *)
  (* TODO: Find a better name for this metric. *)
  Inductive type_dist2 (n : nat) (ty1 ty2 : type) : Prop :=
    Type_dist2 :
      ty1.(ty_size) = ty2.(ty_size) 
      ( tid vs, dist_later n (ty1.(ty_own) tid vs) (ty2.(ty_own) tid vs)) 
      ( κ tid l, ty1.(ty_shr) κ tid l {n} ty2.(ty_shr) κ tid l) 
      type_dist2 n ty1 ty2.

  Global Instance type_dist2_equivalence : Equivalence (type_dist2 n).
  Proof.
    constructor.
    - by constructor.
    - intros ?? Heq; constructor; symmetry; eapply Heq.
    - intros ??? Heq1 Heq2; constructor; etrans; (eapply Heq1 || eapply Heq2).
  Qed.

  Definition type_dist2_later (n : nat) ty1 ty2 : Prop :=
    match n with O => True | S n => type_dist2 n ty1 ty2 end.
  Arguments type_dist2_later !_ _ _ /.

  Global Instance type_dist2_later_equivalence n :
    Equivalence (type_dist2_later n).
  Proof. destruct n as [|n]. by split. apply type_dist2_equivalence. Qed.

  (* The hierarchy of metrics:
     dist n → type_dist2 n → dist_later n → type_dist2_later. *)
  Lemma type_dist_dist2 n ty1 ty2 : dist n ty1 ty2  type_dist2 n ty1 ty2.
  Proof. intros EQ. split; intros; try apply dist_dist_later; apply EQ. Qed.
  Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2  dist_later n ty1 ty2.
  Proof.
    intros EQ. destruct n; first done. split; intros; try apply EQ.
    apply dist_S, EQ.
  Qed.
  Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2  type_dist2_later n ty1 ty2.
  Proof. destruct n; first done. exact: type_dist_dist2. Qed.
  Lemma type_dist2_dist n ty1 ty2 : type_dist2 (S n) ty1 ty2  dist n ty1 ty2.
  Proof. move=>/type_dist2_dist_later. done. Qed.
  Lemma type_dist2_S n ty1 ty2 : type_dist2 (S n) ty1 ty2  type_dist2 n ty1 ty2.
  Proof. intros. apply type_dist_dist2, type_dist2_dist. done. Qed.

  Lemma ty_size_type_dist n : Proper (type_dist2 n ==> eq) ty_size.
  Proof. intros ?? EQ. apply EQ. Qed.
  Lemma ty_own_type_dist n:
    Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
  Lemma ty_shr_type_dist n :
    Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
End type_dist2.

(** Type-nonexpansive and Type-contractive functions. *)
(* Note that TypeContractive is neither weaker nor stronger than Contractive, because
   (a) it allows the dependency of own on shr to be non-expansive, and
   (b) it forces the dependency of shr on own to be doubly-contractive.
   It would be possible to weaken this so that no double-contractivity is required.
   However, then it is no longer possible to write TypeContractive as just a
   Proper, which makes it significantly more annoying to use.
   For similar reasons, TypeNonExpansive is incomparable to NonExpansive.
*)
Notation TypeNonExpansive T := ( n, Proper (type_dist2 n ==> type_dist2 n) T).
Notation TypeContractive T := ( n, Proper (type_dist2_later n ==> type_dist2 n) T).

Section type_contractive.
  Context `{typeG Σ}.

  Lemma type_ne_dist_later T :
    TypeNonExpansive T   n, Proper (type_dist2_later n ==> type_dist2_later n) T.
  Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.

  (* From the above, it easily follows that TypeNonExpansive functions compose with
     TypeNonExpansive and with TypeContractive functions. *)
  Lemma type_ne_ne_compose T1 T2 :
    TypeNonExpansive T1  TypeNonExpansive T2  TypeNonExpansive (T1  T2).
  Proof. intros NE1 NE2 ? ???; simpl. apply: NE1. exact: NE2. Qed.

  Lemma type_contractive_compose_right T1 T2 :
    TypeContractive T1  TypeNonExpansive T2  TypeContractive (T1  T2).
  Proof. intros HT1 HT2 ? ???. apply: HT1. exact: type_ne_dist_later. Qed.

  Lemma type_contractive_compose_left T1 T2 :
    TypeNonExpansive T1  TypeContractive T2  TypeContractive (T1  T2).
  Proof. intros HT1 HT2 ? ???; simpl. apply: HT1. exact: HT2. Qed.

  (* Show some more relationships between properties. *)
  Lemma type_contractive_type_ne T :
    TypeContractive T  TypeNonExpansive T.
  Proof.
    intros HT ? ???. apply type_dist_dist2, dist_later_dist, type_dist2_dist_later, HT. done.
  Qed.

  Lemma type_contractive_ne T :
    TypeContractive T  NonExpansive T.
  Proof.
    intros HT ? ???. apply dist_later_dist, type_dist2_dist_later, HT, type_dist_dist2. done.
  Qed.

  (* Simple types *)
  Global Instance ty_of_st_type_ne n :
    Proper (dist_later n ==> type_dist2 n) ty_of_st.
  Proof.
    intros ???. constructor.
    - done.
370
    - intros. destruct n; first done; simpl. f_equiv. done.
Ralf Jung's avatar
Ralf Jung committed
371
372
373
374
375
376
377
    - intros. solve_contractive.
  Qed.
End type_contractive.

(* Tactic automation. *)
Ltac f_type_equiv :=
  first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
Ralf Jung's avatar
Ralf Jung committed
378
          match goal with | |- @dist_later ?A _ ?n ?x ?y =>
Ralf Jung's avatar
Ralf Jung committed
379
380
381
382
383
384
                            destruct n as [|n]; [exact I|change (@dist A _ n x y)]
          end ].
Ltac solve_type_proper :=
  constructor;
  solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).

385
386
387
388

Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
  match n with
  | 0%nat => 
389
  | S n => shrN.@l  shr_locsE (l + 1%nat) n
390
391
392
  end.

Class Copy `{typeG Σ} (t : type) := {
Ralf Jung's avatar
Ralf Jung committed
393
  copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
  copy_shr_acc κ tid E F l q :
    lftE  shrN  E  shr_locsE l (t.(ty_size) + 1)  F 
    lft_ctx - t.(ty_shr) κ tid l - na_own tid F - q.[κ] ={E}=
        q', na_own tid (F  shr_locsE l t.(ty_size)) 
         (l ↦∗{q'}: t.(ty_own) tid) 
      (na_own tid (F  shr_locsE l t.(ty_size)) - l ↦∗{q'}: t.(ty_own) tid
                                  ={E}= na_own tid F  q.[κ])
}.
Existing Instances copy_persistent.
Instance: Params (@Copy) 2.

Class LstCopy `{typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
Instance: Params (@LstCopy) 2.
Global Instance lst_copy_nil `{typeG Σ} : LstCopy [] := List.Forall_nil _.
Global Instance lst_copy_cons `{typeG Σ} ty tys :
  Copy ty  LstCopy tys  LstCopy (ty :: tys) := List.Forall_cons _ _ _.

Class Send `{typeG Σ} (t : type) :=
  send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl - t.(ty_own) tid2 vl.
Instance: Params (@Send) 2.

Class LstSend `{typeG Σ} (tys : list type) := lst_send : Forall Send tys.
Instance: Params (@LstSend) 2.
Global Instance lst_send_nil `{typeG Σ} : LstSend [] := List.Forall_nil _.
Global Instance lst_send_cons `{typeG Σ} ty tys :
  Send ty  LstSend tys  LstSend (ty :: tys) := List.Forall_cons _ _ _.

Class Sync `{typeG Σ} (t : type) :=
  sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l - t.(ty_shr) κ tid2 l.
Instance: Params (@Sync) 2.

Class LstSync `{typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
Instance: Params (@LstSync) 2.
Global Instance lst_sync_nil `{typeG Σ} : LstSync [] := List.Forall_nil _.
Global Instance lst_sync_cons `{typeG Σ} ty tys :
  Sync ty  LstSync tys  LstSync (ty :: tys) := List.Forall_cons _ _ _.

Ralf Jung's avatar
Ralf Jung committed
431
432
433
434
435
Section type.
  Context `{typeG Σ}.

  (** Copy types *)
  Lemma shr_locsE_shift l n m :
436
    shr_locsE l (n + m) = shr_locsE l n  shr_locsE (l + n) m.
Ralf Jung's avatar
Ralf Jung committed
437
438
439
440
441
442
443
444
  Proof.
    revert l; induction n; intros l.
    - rewrite shift_loc_0. set_solver+.
    - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
      set_solver+.
  Qed.

  Lemma shr_locsE_disj l n m :
445
    shr_locsE l n ## shr_locsE (l + n) m.
Ralf Jung's avatar
Ralf Jung committed
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
  Proof.
    revert l; induction n; intros l.
    - simpl. set_solver+.
    - rewrite -Nat.add_1_l Nat2Z.inj_add /=.
      apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
      clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
      rewrite shift_loc_assoc. apply disjoint_union_r. split.
      + apply ndot_ne_disjoint. destruct l. intros [=]. omega.
      + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
  Qed.

  Lemma shr_locsE_shrN l n :
    shr_locsE l n  shrN.
  Proof.
    revert l; induction n=>l /=; first by set_solver+.
    apply union_least; last by auto. solve_ndisj.
  Qed.

  Lemma shr_locsE_subseteq l n m :
    (n  m)%nat  shr_locsE l n  shr_locsE l m.
  Proof.
    induction 1; first done. etrans; first done.
    rewrite -Nat.add_1_l [(_ + _)%nat]comm_L shr_locsE_shift. set_solver+.
  Qed.

  Lemma shr_locsE_split_tok l n m tid :
    na_own tid (shr_locsE l (n + m)) 
473
      na_own tid (shr_locsE l n)  na_own tid (shr_locsE (l + n) m).
Ralf Jung's avatar
Ralf Jung committed
474
475
476
477
  Proof.
    rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
  Qed.

478
  Global Instance copy_equiv : Proper (equiv ==> impl) Copy.
Ralf Jung's avatar
Ralf Jung committed
479
480
481
482
483
484
485
486
487
488
  Proof.
    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1. split.
    - intros. rewrite -EQown. apply _.
    - intros *. rewrite -EQsz -EQshr. setoid_rewrite <-EQown.
      apply copy_shr_acc.
  Qed.

  Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
  Next Obligation.
    iIntros (st κ tid E ? l q ? HF) "#LFT #Hshr Htok Hlft".
489
    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
Ralf Jung's avatar
Ralf Jung committed
490
    iDestruct "Hshr" as (vl) "[Hf Hown]".
491
    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first solve_ndisj.
Ralf Jung's avatar
Ralf Jung committed
492
493
494
495
496
497
498
499
500
501
502
503
    iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
    iSplitL "Hmt1"; first by auto with iFrame.
    iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
    iDestruct ("Htok" with "Htok2") as "$".
    iAssert ( length vl = length vl')%I as ">%".
    { iNext. iDestruct (st_size_eq with "Hown") as %->.
      iDestruct (st_size_eq with "Hown'") as %->. done. }
    iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
    iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
  Qed.

  (** Send and Sync types *)
504
  Global Instance send_equiv : Proper (equiv ==> impl) Send.
Ralf Jung's avatar
Ralf Jung committed
505
506
507
508
509
  Proof.
    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
    rewrite /Send=>???. rewrite -!EQown. auto.
  Qed.

510
  Global Instance sync_equiv : Proper (equiv ==> impl) Sync.
Ralf Jung's avatar
Ralf Jung committed
511
512
513
514
515
  Proof.
    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
    rewrite /Send=>????. rewrite -!EQshr. auto.
  Qed.

516
  Global Instance ty_of_st_sync st : Send (ty_of_st st)  Sync (ty_of_st st).
Ralf Jung's avatar
Ralf Jung committed
517
518
519
520
521
522
  Proof.
    iIntros (Hsend κ tid1 tid2 l). iDestruct 1 as (vl) "[Hm Hown]".
    iExists vl. iFrame "Hm". iNext. by iApply Hsend.
  Qed.
End type.

523
Definition type_incl `{typeG Σ} (ty1 ty2 : type) : iProp Σ :=
524
525
    (ty1.(ty_size) = ty2.(ty_size) 
     (  tid vl, ty1.(ty_own) tid vl - ty2.(ty_own) tid vl) 
526
     (  κ tid l, ty1.(ty_shr) κ tid l - ty2.(ty_shr) κ tid l))%I.
527
528
529
530
Instance: Params (@type_incl) 2.
(* Typeclasses Opaque type_incl. *)

Definition subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
531
   qL, llctx_interp L qL -  (elctx_interp E - type_incl ty1 ty2).
532
533
534
535
536
537
538
539
540
Instance: Params (@subtype) 4.

(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
  subtype E L ty1 ty2  subtype E L ty2 ty1.
Instance: Params (@eqtype) 4.

Section subtyping.
  Context `{typeG Σ}.
541

Ralf Jung's avatar
Ralf Jung committed
542
543
544
545
546
547
  Global Instance type_incl_ne : NonExpansive2 type_incl.
  Proof.
    intros n ?? [EQsz1%leibniz_equiv EQown1 EQshr1] ?? [EQsz2%leibniz_equiv EQown2 EQshr2].
    rewrite /type_incl. repeat ((by auto) || f_equiv).
  Qed.

Ralf Jung's avatar
Ralf Jung committed
548
  Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
549
550
551
552
553
554
555
556
557
558
559
560
561

  Lemma type_incl_refl ty : type_incl ty ty.
  Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.

  Lemma type_incl_trans ty1 ty2 ty3 :
    type_incl ty1 ty2 - type_incl ty2 ty3 - type_incl ty1 ty3.
  Proof.
    iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
    iSplit; first (iPureIntro; etrans; done).
    iSplit; iAlways; iIntros.
    - iApply "Ho23". iApply "Ho12". done.
    - iApply "Hs23". iApply "Hs12". done.
  Qed.
562

563
  Lemma subtype_refl E L ty : subtype E L ty ty.
564
  Proof. iIntros (?) "_ !# _". iApply type_incl_refl. Qed.
565
  Global Instance subtype_preorder E L : PreOrder (subtype E L).
566
  Proof.
567
    split; first by intros ?; apply subtype_refl.
568
569
570
571
572
    intros ty1 ty2 ty3 H12 H23. iIntros (?) "HL".
    iDestruct (H12 with "HL") as "#H12".
    iDestruct (H23 with "HL") as "#H23".
    iClear "∗". iIntros "!# #HE".
    iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
Ralf Jung's avatar
Ralf Jung committed
573
  Qed.
574
575

  Lemma subtype_Forall2_llctx E L tys1 tys2 qL :
Ralf Jung's avatar
Ralf Jung committed
576
577
578
579
580
581
582
583
584
585
586
587
588
    Forall2 (subtype E L) tys1 tys2 
    llctx_interp L qL -  (elctx_interp E -
           [ list] tys  (zip tys1 tys2), type_incl (tys.1) (tys.2)).
  Proof.
    iIntros (Htys) "HL".
    iAssert ([ list] tys  zip tys1 tys2,
              (elctx_interp _ - type_incl (tys.1) (tys.2)))%I as "#Htys".
    { iApply big_sepL_forall. iIntros (k [ty1 ty2] Hlookup).
      move:Htys => /Forall2_Forall /Forall_forall=>Htys.
      iApply (Htys (ty1, ty2)); first by exact: elem_of_list_lookup_2. done. }
    iClear "∗". iIntros "!# #HE". iApply (big_sepL_impl with "[$Htys]").
    iIntros "!# * % #Hincl". by iApply "Hincl".
  Qed.
589

590
  Lemma equiv_subtype E L ty1 ty2 : ty1  ty2  subtype E L ty1 ty2.
591
592
  Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.

593
594
  Lemma eqtype_unfold E L ty1 ty2 :
    eqtype E L ty1 ty2 
595
    ( qL, llctx_interp L qL -  (elctx_interp E -
596
597
      (ty1.(ty_size) = ty2.(ty_size) 
      (  tid vl, ty1.(ty_own) tid vl  ty2.(ty_own) tid vl) 
598
      (  κ tid l, ty1.(ty_shr) κ tid l  ty2.(ty_shr) κ tid l)))%I).
599
600
  Proof.
    split.
601
602
603
604
605
606
    - iIntros ([EQ1 EQ2] qL) "HL".
      iDestruct (EQ1 with "HL") as "#EQ1".
      iDestruct (EQ2 with "HL") as "#EQ2".
      iClear "∗". iIntros "!# #HE".
      iDestruct ("EQ1" with "HE") as "[#Hsz [#H1own #H1shr]]".
      iDestruct ("EQ2" with "HE") as "[_ [#H2own #H2shr]]".
607
608
609
610
      iSplit; last iSplit.
      + done.
      + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
      + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
611
612
613
614
615
    - intros EQ. split; (iIntros (qL) "HL";
      iDestruct (EQ with "HL") as "#EQ";
      iClear "∗"; iIntros "!# #HE";
      iDestruct ("EQ" with "HE") as "[% [#Hown #Hshr]]";
      (iSplit; last iSplit)).
616
617
618
619
620
621
622
623
      + done.
      + iIntros "!#* H". by iApply "Hown".
      + iIntros "!#* H". by iApply "Hshr".
      + done.
      + iIntros "!#* H". by iApply "Hown".
      + iIntros "!#* H". by iApply "Hshr".
  Qed.

624
  Lemma eqtype_refl E L ty : eqtype E L ty ty.
625
626
  Proof. by split. Qed.

627
  Lemma equiv_eqtype E L ty1 ty2 : ty1  ty2  eqtype E L ty1 ty2.
628
629
  Proof. by split; apply equiv_subtype. Qed.

630
631
  Global Instance subtype_proper E L :
    Proper (eqtype E L ==> eqtype E L ==> iff) (subtype E L).
632
633
  Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.

634
  Global Instance eqtype_equivalence E L : Equivalence (eqtype E L).
635
636
  Proof.
    split.
637
    - by split.
638
639
640
    - intros ?? Heq; split; apply Heq.
    - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
  Qed.
641

642
643
644
645
646
647
648
649
650
651
  Lemma type_incl_simple_type (st1 st2 : simple_type) :
     ( tid vl, st1.(st_own) tid vl - st2.(st_own) tid vl) -
    type_incl st1 st2.
  Proof.
    iIntros "#Hst". iSplit; first done. iSplit; iAlways.
    - iIntros. iApply "Hst"; done.
    - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
      by iApply "Hst".
  Qed.

652
  Lemma subtype_simple_type E L (st1 st2 : simple_type) :
653
    ( qL, llctx_interp L qL -  (elctx_interp E -
654
        tid vl, st1.(st_own) tid vl - st2.(st_own) tid vl)) 
655
    subtype E L st1 st2.
656
  Proof.
657
    intros Hst. iIntros (qL) "HL". iDestruct (Hst with "HL") as "#Hst".
658
659
    iClear "∗". iIntros "!# #HE". iApply type_incl_simple_type.
    iIntros "!#" (??) "?". by iApply "Hst".
660
  Qed.
Ralf Jung's avatar
Ralf Jung committed
661
662

  Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
Ralf Jung's avatar
Ralf Jung committed
663
    E1 + E2  L1 + L2 
Ralf Jung's avatar
Ralf Jung committed
664
665
    subtype E1 L1 ty1 ty2  subtype E2 L2 ty1 ty2.
  Proof.
666
667
668
669
    iIntros (HE12 ? Hsub qL) "HL". iDestruct (Hsub with "[HL]") as "#Hsub".
    { rewrite /llctx_interp. by iApply big_sepL_submseteq. }
    iClear "∗". iIntros "!# #HE". iApply "Hsub".
    rewrite /elctx_interp. by iApply big_sepL_submseteq.
Ralf Jung's avatar
Ralf Jung committed
670
  Qed.
671
End subtyping.
Ralf Jung's avatar
Ralf Jung committed
672

673
674
Section type_util.
  Context `{typeG Σ}.
675

676
677
678
679
680
681
682
683
684
  Lemma heap_mapsto_ty_own l ty tid :
    l ↦∗: ty_own ty tid   (vl : vec val ty.(ty_size)), l ↦∗ vl  ty_own ty tid vl.
  Proof.
    iSplit.
    - iIntros "H". iDestruct "H" as (vl) "[Hl Hown]".
      iDestruct (ty_size_eq with "Hown") as %<-.
      iExists (list_to_vec vl). rewrite vec_to_list_of_list. iFrame.
    - iIntros "H". iDestruct "H" as (vl) "[Hl Hown]". eauto with iFrame.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
685

686
687
End type_util.

688
Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
689
690
Hint Resolve subtype_refl eqtype_refl : lrust_typing.
Hint Opaque subtype eqtype : lrust_typing.