Commit 145abe3c authored by Lennard Gäher's avatar Lennard Gäher
Browse files

experiment: make types Type-indexed to avoid ugly typecasts in type_read_end

parent 98e8e98e
......@@ -3,7 +3,7 @@ From refinedc.rust_typing Require Import programs uninit.
Set Default Proof Using "Type".
(* "entry-point" statement *)
Definition introduce_typed_stmt {Σ} `{!typeGS Σ} E L π (fn : function) (ls : list loc) (R : val rt : type, rt.(ty_rtype) iProp Σ) : iProp Σ :=
Definition introduce_typed_stmt {Σ} `{!typeGS Σ} E L π (fn : function) (ls : list loc) (R : val rt, type rt rt iProp Σ) : iProp Σ :=
let Q := (subst_stmt (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1)
(val_of_loc <$> ls))) <$> fn.(f_code) in
typed_stmt E L (Goto fn.(f_init)) fn ls R Q π .
......@@ -17,8 +17,9 @@ Section function.
(* this does not take an rtype, since we essentially pull that part out to
[fp_rtype] and [fp_fr] below, in order to support existential quantifiers *)
Record fn_ret := mk_FR {
fr_rty : type;
fr_ref : fr_rty.(ty_rtype);
fr_rt : Type;
fr_ty : type fr_rt;
fr_ref : fr_rt;
fr_R : iProp Σ;
}.
......@@ -27,7 +28,7 @@ Section function.
We also directly require an inG proof for ghost variables to that type.
Maybe there is a nicer way to bundle that up?
*)
fp_atys : list (@sigT type (λ rt, ty_rtype rt * (ghost_varG Σ rt.(ty_rtype)))%type);
fp_atys : list (@sigT Type (λ rt, type rt * rt * (ghost_varG Σ rt))%type);
(* bundled assume condition *)
fp_Pa : iProp Σ;
(* external lifetimes, parameterized over a lifetime for the function *)
......@@ -45,38 +46,41 @@ Section function.
We don't allow [retty] to depend on [exty], since [exty] should not quantify over any lifetimes for this computation to work.
FIXME Maybe we can generalize this with some more typeclass magic.
*)
Definition map_rtype : (@sigT Type (λ rt, type rt * rt * (ghost_varG Σ rt))%type) rtype :=
(λ '(existT rt (ty, _, _)), {| rt_rty := rt; rt_ty := ty|}).
Definition FP_wf
E
(atys : list (@sigT type (λ rt, ty_rtype rt * (ghost_varG Σ rt.(ty_rtype)))%type))
`{!ListTyWf (map projT1 atys)}
(atys : list (@sigT Type (λ rt, type rt * rt * (ghost_varG Σ rt))%type))
`{!ListTyWf (map map_rtype atys)}
(pa : iProp Σ)
(exty : Type)
(retty : type)
(retrt : Type)
(retty : type retrt)
`{!TyWf retty}
(fr_ref : exty retty.(ty_rtype))
(fr_ref : exty retrt)
(fr_R : exty iProp Σ) :=
FP
atys
pa
(λ ϝ, E ϝ ++
tyl_wf_E (map projT1 atys) ++
tyl_outlives_E (map projT1 atys) ϝ ++
tyl_wf_E (map map_rtype atys) ++
tyl_outlives_E (map map_rtype atys) ϝ ++
ty_wf_E retty ++
ty_outlives_E retty ϝ)
exty
(λ e, mk_FR retty (fr_ref e) (fr_R e)).
(λ e, mk_FR retrt retty (fr_ref e) (fr_R e)).
(* the return continuation for type-checking the body.
We need to be able to transform ownership of the return type given by [typed_stmt]
to the type + ensures condition that the function really needs to return *)
(* TODO: require something on lifetime contexts? (that ϝ is still in the context?)*)
Definition fn_ret_prop {B} π (fr : B fn_ret) : val ty : type, ty.(ty_rtype) iProp Σ :=
(λ v ty r, v ◁ᵥ{π} r @ ty -
Definition fn_ret_prop {B} π (fr : B fn_ret) : val rt, type rt rt iProp Σ :=
(λ v rt (ty : type rt) r, v ◁ᵥ{π} r @ ty -
(* there exists an inhabitant of the spec-level existential *)
x,
(* st. the return type is satisfied *)
v ◁ᵥ{π} (fr x).(fr_ref) @ (fr x).(fr_rty)
v ◁ᵥ{π} (fr x).(fr_ref) @ (fr x).(fr_ty)
(* and the ensures-condition is satisfied *)
(fr x).(fr_R))%I.
......@@ -107,7 +111,7 @@ Section function.
(* initial stack *)
let Qinit :=
named_lfts
([list] l;tlsa;(fp x).(fp_atys), let '(existT ty (r, _)) := t in l ◁ₗ[π, Owned] r @ ( ty))
([list] l;tlsa;(fp x).(fp_atys), let '(existT rt (ty, r, _)) := t in l ◁ₗ[π, Owned] r @ ( ty))
([list] l;plsv;fn.(f_local_vars), (l ◁ₗ[π, Owned] .@ ( uninit p.2)))
(fp x).(fp_Pa) in
(* external lifetime context: can require external lifetimes syntactically outlive the function lifetime, as well as syntactic constraints between universal lifetimes *)
......@@ -121,8 +125,7 @@ Section function.
(* TODO: need a notion of equivalence on functions? *)
Program Definition function_ptr (fp : A fn_params) : type := {|
st_rtype := loc;
Program Definition function_ptr (fp : A fn_params) : type loc := {|
st_own π r v := ( fn f, v = val_of_loc f fntbl_entry f fn typed_function π fn fp)%I;
st_layout := void*;
|}.
......@@ -148,16 +151,16 @@ Notation "'fn(∀' x ':' A ',' E ';' r1 '@' T1 ',' .. ',' rN '@' TN ';' Pa ')' '
(* For now, we just define notations for a limited number of parameters (currently up to 3) *)
(* FIXME: proper printing *)
Notation "'fn(∀' x ':' A ',' E ';' Pa ')' '→' '∃' y ':' B ',' r '@' rty ';' Pr" :=
((fun x => FP_wf E (@nil _) Pa%I B rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
((fun x => FP_wf E (@nil _) Pa%I B _ rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
(at level 99, Pr at level 200, x pattern, y pattern) : stdpp_scope.
Notation "'fn(∀' x ':' A ',' E ';' r1 '@' T1 ';' Pa ')' '→' '∃' y ':' B ',' r '@' rty ';' Pr" :=
((fun x => FP_wf E (@cons (@sigT type _) (existT T1%I (r1, _)) (@nil _)) Pa%I B rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
((fun x => FP_wf E (@cons (@sigT Type _) (existT _ (T1, r1, _)) (@nil _)) Pa%I B _ rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
(at level 99, Pr at level 200, x pattern, y pattern) : stdpp_scope.
Notation "'fn(∀' x ':' A ',' E ';' r1 '@' T1 ',' r2 '@' T2 ';' Pa ')' '→' '∃' y ':' B ',' r '@' rty ';' Pr" :=
((fun x => FP_wf E (@cons _ (existT T1%I (r1, _)) $ @cons _ (existT T2%I (r2, _)) $ (@nil _)) Pa%I B rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
((fun x => FP_wf E (@cons _ (existT _ (T1, r1, _)) $ @cons _ (existT _ (T2, r2, _)) $ (@nil _)) Pa%I B _ rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
(at level 99, Pr at level 200, x pattern, y pattern) : stdpp_scope.
Notation "'fn(∀' x ':' A ',' E ';' r1 '@' T1 ',' r2 '@' T2 ',' r3 '@' T3 ';' Pa ')' '→' '∃' y ':' B ',' r '@' rty ';' Pr" :=
((fun x => FP_wf E (@cons _ (existT T1%I (r1, _)) $ @cons _ (existT T2%I (r2, _)) $ @cons _ (existT T3%I (r3, _)) $ (@nil _)) Pa%I B rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
((fun x => FP_wf E (@cons _ (existT _ (T1, r1, _)) $ @cons _ (existT _ (T2, r2, _)) $ @cons _ (existT _ (T3, r3, _)) $ (@nil _)) Pa%I B _ rty (λ y, r%I) (λ y, Pr%I)) : A fn_params)
(at level 99, Pr at level 200, x pattern, y pattern) : stdpp_scope.
Module test.
......
......@@ -6,8 +6,7 @@ Section int.
Context `{!typeGS Σ}.
(* Separate definition such that we can make it typeclasses opaque later. *)
Program Definition int (it : int_type) : type := {|
st_rtype := Z;
Program Definition int (it : int_type) : type Z := {|
st_own tid z v := val_to_Z v it = Some z;
st_layout := it_layout it;
|}%I.
......@@ -44,8 +43,7 @@ Section boolean.
Context `{!typeGS Σ}.
(* Separate definition such that we can make it typeclasses opaque later. *)
Program Definition boolean (it : int_type) : type := {|
st_rtype := bool;
Program Definition boolean (it : int_type) : type bool := {|
st_own tid b v := val_to_Z v it = Some (Z_of_bool b);
st_layout := it_layout it;
|}%I.
......@@ -70,19 +68,19 @@ Notation "bool< it >" := (boolean it) (only printing, format "'bool<' it '>'") :
Section typing.
Context `{typeGS Σ}.
Lemma type_val_int z it π (T : rt, rt.(ty_rtype) iProp Σ):
z it T (int it) z - typed_value (i2v z it) π T.
Lemma type_val_int z it π (T : rt, type rt rt iProp Σ):
z it T _ (int it) z - typed_value (i2v z it) π T.
Proof.
iIntros "[%Hn HT] #LFT".
move: Hn => /(val_of_Z_is_Some None) [v Hv].
move: (Hv) => /val_to_of_Z Hn.
iExists (int it), z. iFrame "HT". iPureIntro.
iExists Z, (int it), z. iFrame "HT". iPureIntro.
by rewrite /i2v Hv /=.
Qed.
Global Instance type_val_int_inst n it π : TypedValue (i2v n it) π :=
λ T, i2p (type_val_int n it π T).
Lemma type_relop_int_int E L it v1 (n1 : Z) v2 (n2 : Z) (T : val rt, rt.(ty_rtype) iProp Σ) b op π :
Lemma type_relop_int_int E L it v1 (n1 : Z) v2 (n2 : Z) (T : val rt, type rt rt iProp Σ) b op π :
match op with
| EqOp rit => Some (bool_decide (n1 = n2)%Z, rit)
| NeOp rit => Some (bool_decide (n1 n2)%Z, rit)
......@@ -91,15 +89,15 @@ Section typing.
| LeOp rit => Some (bool_decide (n1 <= n2)%Z, rit)
| GeOp rit => Some (bool_decide (n1 >= n2)%Z, rit)
| _ => None
end = Some (b, i8)
(n1 it - n2 it - T (i2v (Z_of_bool b) i8) (boolean i8) b) -
end = Some (b, u8)
(n1 it - n2 it - T (i2v (Z_of_bool b) u8) bool (boolean u8) b) -
typed_bin_op E L v1 (v1 ◁ᵥ{π} n1 @ int it) v2 (v2 ◁ᵥ{π} n2 @ int it) op (IntOp it) (IntOp it) π T.
Proof.
iIntros "%Hop HT %Hv1 %Hv2 %Φ % % #LFT #HE HL HΦ".
iDestruct ("HT" with "[] []" ) as "HT".
1-2: iPureIntro; by apply: val_to_Z_in_range.
have [v Hv]:= val_of_Z_bool_is_Some None i8 b.
iApply (wp_binop_det_pure (i2v (Z_of_bool b) i8)).
have [v Hv]:= val_of_Z_bool_is_Some None u8 b.
iApply (wp_binop_det_pure (i2v (Z_of_bool b) u8)).
{ rewrite /i2v Hv /=.
split; last (move => ->; by econstructor).
destruct op => //; inversion 1; by simplify_eq. }
......@@ -132,19 +130,19 @@ Section typing.
Lemma type_val_bool' b π :
(val_of_bool b) ◁ᵥ{π} b @ boolean u8.
Proof. iIntros. by destruct b. Qed.
Lemma type_val_bool b π (T : rt, rt.(ty_rtype) iProp Σ) :
(T (boolean u8) b) - typed_value (val_of_bool b) π T.
Proof. iIntros "HT #LFT". iExists (boolean u8), b. iFrame. iApply type_val_bool'. Qed.
Lemma type_val_bool b π (T : rt, type rt rt iProp Σ) :
(T bool (boolean u8) b) - typed_value (val_of_bool b) π T.
Proof. iIntros "HT #LFT". iExists bool, (boolean u8), b. iFrame. iApply type_val_bool'. Qed.
Global Instance type_val_bool_inst b π : TypedValue (val_of_bool b) π :=
λ T, i2p (type_val_bool b π T).
Lemma type_relop_bool_bool E L it v1 b1 v2 b2 (T : val rt, rt.(ty_rtype) iProp Σ) b op π :
Lemma type_relop_bool_bool E L it v1 b1 v2 b2 (T : val rt, type rt rt iProp Σ) b op π :
match op with
| EqOp rit => Some (eqb b1 b2, rit)
| NeOp rit => Some (negb (eqb b1 b2), rit)
| _ => None
end = Some (b, u8)
(T (i2v (Z_of_bool b) u8) (boolean u8) b) -
(T (i2v (Z_of_bool b) u8) bool (boolean u8) b) -
typed_bin_op E L v1 (v1 ◁ᵥ{π} b1 @ boolean it) v2 (v2 ◁ᵥ{π} b2 @ boolean it) op (IntOp it) (IntOp it) π T.
Proof.
iIntros "%Hop HT %Hv1 %Hv2 %Φ % % #LFT #HE HL HΦ".
......
This diff is collapsed.
......@@ -21,10 +21,9 @@ Definition place_rfn_in {rt : Type} (r : place_rfn rt) :=
Section place_rfn_wrap.
Context `{typeGS Σ} (inner : type).
Context `{typeGS Σ} {rt} (inner : type rt).
Program Definition place_wrap : type := {|
ty_rtype := place_rfn inner.(ty_rtype);
Program Definition place_wrap : type (place_rfn rt) := {|
ty_own_val tid r v :=
( ri, place_rfn_cond r ri inner.(ty_own_val) tid ri v)%I;
ty_layout := inner.(ty_layout);
......@@ -62,7 +61,7 @@ Section place_rfn_wrap.
End place_rfn_wrap.
Section mut_ref.
Context `{typeGS Σ} (inner : type) `{ghost_varG Σ inner.(ty_rtype)}.
Context `{typeGS Σ} {rt} (inner : type rt) `{ghost_varG Σ rt}.
Implicit Types (κ : lft) (γ : gname).
(* TODO: additionally define a shortcut that includes the place_wrap for the inner type.
......@@ -73,7 +72,7 @@ Section mut_ref.
(* Mutable references only really make sense when the inner type is a refinement type,
because we cannot make strong updates to the inner type -- thus the inner refinement needs to be
exposed through the mutable reference's refinement *)
Program Definition mut_ref (κ : lft) : type := {|
Program Definition mut_ref (κ : lft) : type (rt * gname) := {|
ty_own_val tid '(r, γ) v :=
( (l : loc), v = l l `has_layout_loc` inner.(ty_layout)
gvar_obs γ r
......@@ -219,9 +218,10 @@ End mut_ref_ltype.
Section ltype_agree.
Context `{typeGS Σ}
(rt : type)
`{ghost_varG Σ (rt.(ty_rtype))}
`{ghost_varG Σ (rt.(ty_rtype) * gname)}.
{rt}
(ty: type rt)
`{ghost_varG Σ rt}
`{ghost_varG Σ (rt * gname)}.
(* problem: the mut_ref doesn't wrap a place_rfn around the inner thing; the mut_ref is already refined by place_rfn
......@@ -234,7 +234,7 @@ Section ltype_agree.
*)
Lemma mut_ref_unfold κ :
ltype_eq _ (mut_ltype ( (rt)) κ ( (rt))) ( (mut_ref (rt) κ)).
ltype_eq _ (mut_ltype ( (ty)) κ ( (ty))) ( (mut_ref (ty) κ)).
Proof.
(* TODO *)
(*
......@@ -292,15 +292,14 @@ Section ltype_agree.
End ltype_agree.
Section shr_ref.
Context `{typeGS Σ} (inner : type).
Context `{typeGS Σ} {rt} (inner : type rt).
Implicit Types (κ : lft).
(* this is almost a simple type, but we have to be careful with
the sharing predicate: we want to obtain the knowledge that l points to
a location not under a later (to prove the agreement with the ltype unfolding),
so the simple_type interface doesn't suffice *)
Program Definition shr_ref κ : type := {|
ty_rtype := inner.(ty_rtype);
Program Definition shr_ref κ : type rt := {|
ty_own_val tid r v := ( l, v = val_of_loc l inner.(ty_shr) κ tid r l)%I;
ty_layout := ref_layout;
ty_shr κ' tid r l :=
......@@ -372,12 +371,12 @@ End shr_ref_ltype.
Section ltype_agree.
Context `{typeGS Σ}
(rt : type)
`{ghost_varG Σ rt.(ty_rtype)}
`{ghost_varG Σ (rt.(ty_rtype) * gname)}.
{rt}
(ty : type rt)
`{ghost_varG Σ rt}.
Lemma shr_ref_unfold κ :
ltype_eq _ (shr_ltype κ ( rt)) ( (shr_ref rt κ)).
ltype_eq _ (shr_ltype κ ( ty)) ( (shr_ref ty κ)).
Proof.
(* TODO *)
(*
......
......@@ -18,17 +18,16 @@ Definition thread_id := na_inv_pool_name.
(**
Types are defined via ownership of values with a determined layout.
This encodes that types are always movable in Rust.
This encodes that types are always movable in Rust.
TODO: if we want to support pinning, we may want to add ownership of locations
TODO: if we want to support pinning, we may want to add ownership of locations
as an additional predicate here.
*)
Record type `{typeGS Σ} := {
ty_rtype : Type;
ty_own_val : thread_id ty_rtype val iProp Σ;
Record type `{typeGS Σ} (rt : Type) := {
ty_own_val : thread_id rt val iProp Σ;
ty_layout : layout;
ty_shr : lft thread_id ty_rtype loc iProp Σ;
ty_drop : ty_rtype iProp Σ;
ty_shr : lft thread_id rt loc iProp Σ;
ty_drop : rt iProp Σ;
ty_depth : nat;
ty_has_layout tid v r : ty_own_val tid r v - v `has_layout_val` ty_layout;
......@@ -45,84 +44,94 @@ Record type `{typeGS Σ} := {
}.
Arguments ty_own_val : simpl never.
Existing Instance ty_shr_persistent.
Arguments ty_own_val {_ _ _}.
Arguments ty_layout {_ _ _}.
Arguments ty_shr {_ _ _}.
Arguments ty_drop {_ _ _}.
Arguments ty_depth {_ _ _}.
(*Existing Instance ty_drop_timeless.*)
Record rtype `{typeGS Σ} := {
rt_rty : Type;
rt_ty : type rt_rty;
}.
(** Well-formedness of a type with respect to lifetimes.
[ty_lfts] is the set of lifetimes that needs to be active for this type to make sense.
[ty_wf_E] is a set of inclusion constraints on lifetimes that need to hold for the type to make sense.
*)
Class TyWf `{!typeGS Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
Arguments ty_lfts {_ _} _ {_}.
Arguments ty_wf_E {_ _} _ {_}.
Class TyWf `{!typeGS Σ} {rt} (ty : type rt) := { ty_lfts : list lft; ty_wf_E : elctx }.
Arguments ty_lfts {_ _ _} _ {_}.
Arguments ty_wf_E {_ _ _} _ {_}.
(* generate a constraint that a type outlives κ *)
Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
Definition ty_outlives_E `{!typeGS Σ} {rt} (ty : type rt) `{!TyWf ty} (κ : lft) : elctx :=
(λ α, (κ, α)) <$> ty.(ty_lfts).
(* Lift TyWf to lists. We cannot use `Forall` because that one is restricted to Prop. *)
Inductive ListTyWf `{!typeGS Σ} : list type Type :=
Inductive ListTyWf `{!typeGS Σ} : list rtype Type :=
| list_ty_wf_nil : ListTyWf []
| list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
| list_ty_wf_cons ty tyl `{!TyWf ty.(rt_ty), !ListTyWf tyl} : ListTyWf (ty::tyl).
Existing Class ListTyWf.
Existing Instances list_ty_wf_nil list_ty_wf_cons.
Fixpoint tyl_lfts `{!typeGS Σ} tyl {WF : ListTyWf tyl} : list lft :=
match WF with
| list_ty_wf_nil => []
| list_ty_wf_cons ty [] => ty.(ty_lfts)
| list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
| list_ty_wf_cons ty [] => ty.(rt_ty).(ty_lfts)
| list_ty_wf_cons ty tyl => ty.(rt_ty).(ty_lfts) ++ tyl.(tyl_lfts)
end.
Fixpoint tyl_wf_E `{!typeGS Σ} tyl {WF : ListTyWf tyl} : elctx :=
match WF with
| list_ty_wf_nil => []
| list_ty_wf_cons ty [] => ty.(ty_wf_E)
| list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
| list_ty_wf_cons ty [] => ty.(rt_ty).(ty_wf_E)
| list_ty_wf_cons ty tyl => ty.(rt_ty).(ty_wf_E) ++ tyl.(tyl_wf_E)
end.
Fixpoint tyl_outlives_E `{!typeGS Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
match WF with
| list_ty_wf_nil => []
| list_ty_wf_cons ty [] => ty_outlives_E ty κ
| list_ty_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
| list_ty_wf_cons ty [] => ty_outlives_E ty.(rt_ty) κ
| list_ty_wf_cons ty tyl => ty_outlives_E ty.(rt_ty) κ ++ tyl.(tyl_outlives_E) κ
end.
(** simple types *)
(* Simple types are copy, have a simple sharing predicate, and do not nest. *)
Record simple_type `{!typeGS Σ} :=
{ st_rtype : Type;
st_own : thread_id st_rtype val iProp Σ;
Record simple_type `{!typeGS Σ} (rt : Type) :=
{ st_own : thread_id rt val iProp Σ;
st_layout : layout;
st_size_eq tid r v : st_own tid r v - v `has_layout_val` st_layout;
st_own_persistent tid r v : Persistent (st_own tid r v)
st_own_persistent tid r v : Persistent (st_own tid r v)
}.
Existing Instance st_own_persistent.
Instance: Params (@st_own) 3 := {}.
Instance: Params (@st_own) 4 := {}.
Arguments st_own {_ _ _}.
Arguments st_layout {_ _ _ }.
Program Definition ty_of_st `{!typeGS Σ} (st : simple_type) : type :=
{| ty_rtype := st.(st_rtype);
ty_own_val tid r v := (st.(st_own) tid r v)%I;
Program Definition ty_of_st `{!typeGS Σ} rt (st : simple_type rt) : type rt :=
{| ty_own_val tid r v := (st.(st_own) tid r v)%I;
ty_layout := st.(st_layout);
ty_shr κ tid r l :=
( vl, &frac{κ} (λ q, l {q} vl) st.(st_own) tid r vl l `has_layout_loc` st.(st_layout))%I;
ty_drop _ := True%I;
ty_depth := 1;
ty_depth := 1;
|}.
Next Obligation.
iIntros (?? st tid v r). iApply st_size_eq.
Next Obligation.
iIntros (??? st tid v r). iApply st_size_eq.
Qed.
Next Obligation.
iIntros (?? st E κ l tid r ??) "#LFT Hly Hmt Hκ".
iIntros (??? st E κ l tid r ??) "#LFT Hly Hmt Hκ".
iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
iMod (bor_persistent with "LFT Hown Hκ") as "[Hown Hκ]"; first solve_ndisj.
iMod (bor_fracture (λ q, l {q} vl)%I with "LFT Hmt") as "Hfrac"; [eauto with iFrame.. |].
iMod (bor_fracture (λ q, l {q} vl)%I with "LFT Hmt") as "Hfrac"; [eauto with iFrame.. |].
eauto with iFrame.
Qed.
Next Obligation.
iIntros (?? st κ κ' tid r l) "#Hord H".
iIntros (??? st κ κ' tid r l) "#Hord H".
iDestruct "H" as (vl) "[#Hf #Hown]".
iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
Qed.
......@@ -139,7 +148,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
| S n => shrN.@l shr_locsE (l + 1%nat) n
end.
Class Copyable `{!typeGS Σ} (ty : type) := {
Class Copyable `{!typeGS Σ} {rt} (ty : type rt) := {
copy_own_persistent tid r v : Persistent (ty.(ty_own_val) tid r v);
copy_shr_acc κ tid E F l r q :
lftN shrN E shr_locsE l (ty.(ty_layout).(ly_size) + 1) F
......@@ -152,9 +161,9 @@ Class Copyable `{!typeGS Σ} (ty : type) := {
}.
Existing Instance copy_own_persistent.
Program Instance simple_type_copyable `{typeGS Σ} (st : simple_type) : Copyable st.
Program Instance simple_type_copyable `{typeGS Σ} rt (st : simple_type rt) : Copyable st.
Next Obligation.
iIntros (?? st κ tid E F l r ? ??) "LFT (%v & Hf & #Hown & Hly) Htok Hlft".
iIntros (??? st κ tid E F l r ? ??) "LFT (%v & Hf & #Hown & Hly) Htok Hlft".
iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first solve_ndisj.
iModIntro. iFrame "Hly". iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
......@@ -176,14 +185,14 @@ Bind Scope bi_scope with type.
Section ltype.
Context `{typeGS Σ}.
(*
(*
[PlaceIn]: the current inner refinement is accurate (no blocking of the inner refinement).
[PlaceNotIn]: the current inner refinement is unknown, either because it is currently blocked, or because it was force-unblocked.
*)
Inductive place_rfn_mode := PlaceModeIn | PlaceModeNoInfo.
(* concrete refinements *)
Inductive place_rfn (rt : Type) :=
| PlaceIn (r : rt)
Inductive place_rfn (rt : Type) :=
| PlaceIn (r : rt)
| PlaceNoInfo.
Global Arguments PlaceIn {_}.
Global Arguments PlaceNoInfo {_}.
......@@ -197,13 +206,13 @@ Proof. refine (populate PlaceModeNoInfo). Qed.
Inductive bor_kind :=
| Owned | Shared (κ : lft) | Uniq (κ : lft) (γ : gname).
(**
(**
ltypes have a refinement (they are refinement types).
This is necessary for incorporating mutable references sensibly
(they require some interaction with the child ltype for refinement).
(they require some interaction with the child ltype for refinement).
*)
(* ltypes are indexed by the type for refinements to make a nice statement
(* ltypes are indexed by the type for refinements to make a nice statement
for ltype_eq possible (without requiring that the packaged types are equal and
having typecasts). *)
Record ltype (rty : Type) := mk_ltype {
......@@ -216,11 +225,11 @@ Record ltype (rty : Type) := mk_ltype {
ltype_depth : nat;
}.
Global Arguments ltype_own {_}.
Global Arguments ltype_own {_}.
Global Arguments ltype_depth {_}.
Global Existing Instance ltype_shr_pers.
Definition ltype_eq (rty : Type) (lt1 lt2 : ltype rty) : iProp Σ :=
Definition ltype_eq (rty : Type) (lt1 lt2 : ltype rty) : iProp Σ :=
( k π r l, (|={lftE}=> lt1.(ltype_own) k π r l) |={lftE}=> lt2.(ltype_own) k π r l).
Class LTyWf `{!typeGS Σ} {rt} (lty : ltype rt) := { lty_lfts : list lft; lty_wf_E : elctx }.
......@@ -234,17 +243,17 @@ End ltype.
(* TODO: is there a smarter setup for ltypes? there's a lot of duplication here... *)
Section ltypes.
Context `{typeGS Σ} (rt : type) `{ghost_varG Σ rt.(ty_rtype)} .
Program Definition lty_of_ty : ltype rt.(ty_rtype) := {|
Context `{typeGS Σ} {rt} (ty : type rt) `{ghost_varG Σ rt} .
Program Definition lty_of_ty : ltype rt := {|
ltype_own k π r l :=
match k with
| Owned => l `has_layout_loc` rt.(ty_layout) l : rt.(ty_own_val) π r
| Uniq κ γ =>
l `has_layout_loc` rt.(ty_layout) gvar_obs γ r
|={lftE}=> &pin{κ} ( r', gvar_auth γ r' l : rt.(ty_own_val) π r')
| Shared κ => rt.(ty_shr) κ π r l
| Owned => l `has_layout_loc` ty.(ty_layout) l : ty.(ty_own_val) π r
| Uniq κ γ =>
l `has_layout_loc` ty.(ty_layout) gvar_obs γ r
|={lftE}=> &pin{κ} (