diff --git a/theories/rust_typing/existentials_na.v b/theories/rust_typing/existentials_na.v
index 4ee51a8b35f2a8c325abb2e2ff9a9f7c8161cd7a..e4cc7cb22ed77bc5562accb78ab5ff7f470315d0 100644
--- a/theories/rust_typing/existentials_na.v
+++ b/theories/rust_typing/existentials_na.v
@@ -208,864 +208,489 @@ End contr.
Notation "'∃na;' P ',' τ" := (na_ex_plain_t _ _ P τ) (at level 40) : stdpp_scope.
-Section generated_code.
- From refinedrust Require Import typing.
-
- Section UnsafeCell_sls.
- Context `{!refinedrustGS Σ}.
-
- Definition UnsafeCell_sls : struct_layout_spec := mk_sls "UnsafeCell" [
- ("value", IntSynType I32)] StructReprTransparent.
- Definition UnsafeCell_st : syn_type := UnsafeCell_sls.
- End UnsafeCell_sls.
-
- Section Cell_sls.
- Context `{!refinedrustGS Σ}.
-
- Definition Cell_sls : struct_layout_spec := mk_sls "Cell" [
- ("value", UnsafeCell_st)] StructReprRust.
- Definition Cell_st : syn_type := Cell_sls .
- End Cell_sls.
-
- Section code.
- Context `{!refinedrustGS Σ}.
- Open Scope printing_sugar.
-
- Definition UnsafeCell_new_def : function := {|
- f_args := [
- ("value", (it_layout I32) : layout)
- ];
- f_local_vars := [
- ("__0", (use_layout_alg' (UnsafeCell_st)) : layout);
- ("__2", (it_layout I32) : layout)
- ];
- f_code :=
- <[
- "_bb0" :=
- "__2" <-{ IntOp I32 } use{ IntOp I32 } ("value");
- "__0" <-{ (use_op_alg' (UnsafeCell_st)) } StructInit UnsafeCell_sls [("value", use{ IntOp I32 } ("__2") : expr)];
- return (use{ (use_op_alg' (UnsafeCell_st)) } ("__0"))
- ]>%E $
- ∅;
- f_init := "_bb0";
- |}.
-
- Definition UnsafeCell_into_inner_def : function := {|
- f_args := [
- ("self", (use_layout_alg' (UnsafeCell_st)) : layout)
- ];
- f_local_vars := [
- ("__0", (it_layout I32) : layout)
- ];
- f_code :=
- <[
- "_bb0" :=
- "__0" <-{ IntOp I32 } use{ IntOp I32 } (("self") at{ UnsafeCell_sls } "value");
- return (use{ IntOp I32 } ("__0"))
- ]>%E $
- ∅;
- f_init := "_bb0";
- |}.
-
- Definition UnsafeCell_get_old_def : function := {|
- f_args := [
- ("self", void* : layout)
- ];
- f_local_vars := [
- ("__0", (it_layout I32) : layout)
- ];
- f_code :=
- <[
- "_bb0" :=
- annot: CopyLftNameAnnot "plft3" "ulft__";
- "__0" <-{ IntOp I32 } use{ IntOp I32 } ((!{ PtrOp } ( "self" )) at{ (UnsafeCell_sls) } "value");
- return (use{ IntOp I32 } ("__0"))
- ]>%E $
- ∅;
- f_init := "_bb0";
- |}.
-
- Definition UnsafeCell_get_def : function := {|
- f_args := [
- ("self", void* : layout)
- ];
- f_local_vars := [
- ("__0", void* : layout);
- ("__2", void* : layout);
- ("__3", void* : layout)
- ];
- f_code :=
- <[
- "_bb0" :=
- annot: CopyLftNameAnnot "plft3" "ulft_1";
- "__3" <-{ PtrOp } &raw{ Shr } (!{ PtrOp } ( "self" ));
- "__2" <-{ PtrOp } use{ PtrOp } ("__3");
- "__0" <-{ PtrOp } use{ PtrOp } ("__2");
- return (use{ PtrOp } ("__0"))
- ]>%E $
- ∅;
- f_init := "_bb0";
- |}.
-
- Definition Cell_new_def (UnsafeCell_new_loc : loc) : function := {|
- f_args := [
- ("value", (it_layout I32) : layout)
- ];
- f_local_vars := [
- ("__0", (use_layout_alg' (Cell_st)) : layout);
- ("__2", (use_layout_alg' (UnsafeCell_st)) : layout);
- ("__3", (it_layout I32) : layout)
- ];
- f_code :=
- <[
- "_bb0" :=
- "__3" <-{ IntOp I32 } use{ IntOp I32 } ("value");
- "__2" <-{ (use_op_alg' (UnsafeCell_st)) } CallE UnsafeCell_new_loc [] [] [@{expr} use{ IntOp I32 } ("__3")];
- Goto "_bb1"
- ]>%E $
- <[
- "_bb1" :=
- "__0" <-{ (use_op_alg' (Cell_st)) } StructInit Cell_sls [("value", use{ (use_op_alg' (UnsafeCell_st)) } ("__2") : expr)];
- return (use{ (use_op_alg' (Cell_st)) } ("__0"))
- ]>%E $
- ∅;
- f_init := "_bb0";
- |}.
-
- Definition Cell_into_inner_def (UnsafeCell_into_inner_loc : loc) : function := {|
- f_args := [
- ("self", (use_layout_alg' (Cell_st)) : layout)
- ];
- f_local_vars := [
- ("__0", (it_layout I32) : layout);
- ("__2", (use_layout_alg' (UnsafeCell_st)) : layout)
- ];
- f_code :=
- <[
- "_bb0" :=
- "__2" <-{ (use_op_alg' (UnsafeCell_st)) } use{ (use_op_alg' (UnsafeCell_st)) } (("self") at{ Cell_sls } "value");
- "__0" <-{ IntOp I32 } CallE UnsafeCell_into_inner_loc [] [] [@{expr} use{ (use_op_alg' (UnsafeCell_st)) } ("__2")];
- Goto "_bb1"
- ]>%E $
- <[
- "_bb1" :=
- return (use{ IntOp I32 } ("__0"))
- ]>%E $
- ∅;
- f_init := "_bb0";
- |}.
-
- End code.
-
- Section UnsafeCell_ty.
- Context `{!refinedrustGS Σ}.
-
- Definition UnsafeCell_ty : type (plist place_rfn [Z : Type]).
- Proof using Type*. exact (struct_t UnsafeCell_sls +[(int I32)]). Defined.
-
- Definition UnsafeCell_rt : Type.
- Proof using . let __a := eval hnf in (rt_of UnsafeCell_ty) in exact __a. Defined.
-
- Global Typeclasses Transparent UnsafeCell_ty.
- Global Typeclasses Transparent UnsafeCell_rt.
- End UnsafeCell_ty.
- Global Arguments UnsafeCell_rt : clear implicits.
-
- Section UnsafeCell_inv_t.
- Context `{!refinedrustGS Σ}.
-
- Program Definition UnsafeCell_inv_t_inv_spec : na_ex_inv_def (UnsafeCell_rt) (Z) :=
- na_mk_ex_inv_def
- ((Z)%type)
- (xmap)
- (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌠∗ ⌜Zeven x⌠∗ True)%I
- [] [].
-
- Definition UnsafeCell_inv_t : type (Z) :=
- na_ex_plain_t _ _ UnsafeCell_inv_t_inv_spec UnsafeCell_ty.
-
- Definition UnsafeCell_inv_t_rt : Type.
- Proof using. let __a := eval hnf in (rt_of UnsafeCell_inv_t) in exact __a. Defined.
-
- Global Typeclasses Transparent UnsafeCell_inv_t.
- Global Typeclasses Transparent UnsafeCell_inv_t_rt.
- End UnsafeCell_inv_t.
- Global Arguments UnsafeCell_inv_t_rt : clear implicits.
-
- Section Cell_ty.
- Context `{!refinedrustGS Σ}.
-
- Definition Cell_ty : type (plist place_rfn [UnsafeCell_inv_t_rt : Type]).
- Proof using Type*. exact (struct_t Cell_sls +[UnsafeCell_inv_t]). Defined.
- Definition Cell_rt : Type.
- Proof using . let __a := eval hnf in (rt_of Cell_ty) in exact __a. Defined.
-
- Global Typeclasses Transparent Cell_ty.
- Global Typeclasses Transparent Cell_rt.
- End Cell_ty.
- Global Arguments Cell_rt : clear implicits.
-
- Section Cell_inv_t.
- Context `{!refinedrustGS Σ}.
-
- Program Definition Cell_inv_t_inv_spec : na_ex_inv_def (Cell_rt) (Z) :=
- na_mk_ex_inv_def
- ((Z)%type)
- (xmap)
- (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌠∗ ⌜Zeven x⌠∗ True)%I
- [] [].
-
- Definition Cell_inv_t : type (Z) :=
- na_ex_plain_t _ _ Cell_inv_t_inv_spec Cell_ty.
-
- Definition Cell_inv_t_rt : Type.
- Proof using . let __a := eval hnf in (rt_of Cell_inv_t) in exact __a. Defined.
-
- Global Typeclasses Transparent Cell_inv_t.
- Global Typeclasses Transparent Cell_inv_t_rt.
- End Cell_inv_t.
- Global Arguments Cell_inv_t_rt : clear implicits.
-
- Section specs.
- Context `{RRGS: !refinedrustGS Σ}.
-
- Definition type_of_UnsafeCell_new :=
- fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ Ï, []); x :@: (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)))
- → ∃ _ : unit, x @ UnsafeCell_inv_t; (λ π : thread_id, True).
-
- Definition type_of_UnsafeCell_into_inner :=
- fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ Ï, []); x :@: UnsafeCell_inv_t; (λ Ï€ : thread_id, True))
- → ∃ _ : unit, x @ (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)).
-
- Definition type_of_UnsafeCell_get_old :=
- fn(∀ ( *[ulft_1]) : 1 | ( *[]) : ([]) | (x) : (_), (λ Ï, []); x :@: (shr_ref ulft_1 UnsafeCell_inv_t); (λ Ï€ : thread_id, True))
- → ∃ _ : unit, x @ (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)).
-
- Definition type_of_Cell_new :=
- fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (Z), (λ Ï, []); x :@: (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)))
- → ∃ _ : unit, x @ Cell_inv_t; (λ π : thread_id, True).
-
- Definition type_of_Cell_into_inner :=
- fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (_), (λ Ï, []); x :@: Cell_inv_t; (λ Ï€ : thread_id, True))
- → ∃ _ : unit, x @ (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)).
- End specs.
-
- Section proof.
- Context `{RRGS: !refinedrustGS Σ}.
-
- Definition UnsafeCell_new_lemma (Ï€ : thread_id) : Prop :=
- syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
- ⊢ typed_function π (UnsafeCell_new_def ) [UnsafeCell_st; IntSynType I32] (<tag_type> type_of_UnsafeCell_new ).
-
- Definition UnsafeCell_into_inner_lemma (Ï€ : thread_id) : Prop :=
- syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
- ⊢ typed_function π (UnsafeCell_into_inner_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_into_inner ).
-
- Definition UnsafeCell_get_old_lemma (Ï€ : thread_id) : Prop :=
- syn_type_is_layoutable (Cell_st) →
- ⊢ typed_function π (UnsafeCell_get_old_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_get_old ).
-
- Definition Cell_new_lemma (Ï€ : thread_id) : Prop :=
- ∀ (UnsafeCell_new_loc : loc) ,
- syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
- syn_type_is_layoutable ((Cell_sls : syn_type)) →
- UnsafeCell_new_loc â—áµ¥{Ï€} UnsafeCell_new_loc @ function_ptr [IntSynType I32] (<tag_type> spec! ( *[]) : 0 | ( *[]) : ([]), type_of_UnsafeCell_new (RRGS := RRGS) <MERGE!>) -∗
- typed_function π (Cell_new_def UnsafeCell_new_loc ) [Cell_st; UnsafeCell_st; IntSynType I32] (<tag_type> type_of_Cell_new ).
- End proof.
-
- Ltac UnsafeCell_new_prelude :=
- unfold UnsafeCell_new_lemma;
- set (FN_NAME := FUNCTION_NAME "UnsafeCell_new");
- intros;
- iStartProof;
- let Ï := fresh "Ï" in
- start_function "UnsafeCell_new" Ï ( [] ) ( [] ) ( x ) ( x );
- set (loop_map := BB_INV_MAP (PolyNil));
- intros arg_value local___0 local___2;
- init_lfts (named_lft_update "_flft" Ï $ ∅ );
- init_tyvars ( ∅ ).
-
- Ltac UnsafeCell_into_inner_prelude :=
- unfold UnsafeCell_into_inner_lemma;
- set (FN_NAME := FUNCTION_NAME "UnsafeCell_into_inner");
- intros;
- iStartProof;
- let Ï := fresh "Ï" in
- start_function "UnsafeCell_into_inner" Ï ( [] ) ( [] ) ( x ) ( x );
- set (loop_map := BB_INV_MAP (PolyNil));
- intros arg_self local___0;
- init_lfts (named_lft_update "_flft" Ï $ ∅ );
- init_tyvars ( ∅ ).
-
- Ltac UnsafeCell_get_old_prelude :=
- unfold UnsafeCell_get_old_lemma;
- set (FN_NAME := FUNCTION_NAME "Cell_get");
- intros;
- iStartProof;
- let Ï := fresh "Ï" in
- let ulft__ := fresh "ulft__" in
- start_function "UnsafeCell_get_old" Ï ( [ ulft__ [] ] ) ( [] ) ( x ) ( x );
- set (loop_map := BB_INV_MAP (PolyNil));
- intros arg_self local___0;
- init_lfts (named_lft_update "ulft__" ulft__ $ named_lft_update "_flft" Ï $ ∅ );
- init_tyvars ( ∅ ).
-
- Ltac Cell_new_prelude :=
- unfold Cell_new_lemma;
- set (FN_NAME := FUNCTION_NAME "Cell_new");
- intros;
- iStartProof;
- let Ï := fresh "Ï" in
- start_function "Cell_T_new" Ï ( [] ) ( [] ) ( x ) ( x );
- set (loop_map := BB_INV_MAP (PolyNil));
- intros arg_value local___0 local___2 local___3;
- init_lfts (named_lft_update "_flft" Ï $ ∅ );
- init_tyvars ( ∅ ).
-
- (* === V TYPING RULES V === *)
-
- Section na_subtype.
- Context `{!typeGS Σ}.
- Context {rt X : Type} (P : na_ex_inv_def rt X).
-
- Lemma owned_subtype_na_ex_plain_t π E L (ty : type rt) (r : rt) (r' : X) T :
- (prove_with_subtype E L false ProveDirect (P.(na_inv_P) π r r') (λ L1 _ R, R -∗ T L1))
- ⊢ owned_subtype π E L false r r' ty (∃na; P, ty) T.
- Proof.
- unfold owned_subtype, prove_with_subtype.
-
- (* Nothing has changed *)
- iIntros "HT".
- iIntros (????) "#CTX #HE HL".
- iMod ("HT" with "[//] [//] [//] CTX HE HL") as "(%L2 & % & %R2 & >(Hinv & HR2) & HL & HT)".
- iExists L2. iFrame. iPoseProof ("HT" with "HR2") as "$". iModIntro.
- iSplitR; last iSplitR.
- - simpl. iPureIntro.
- intros ly1 ly2 Hly1 HLy2. f_equiv. by eapply syn_type_has_layout_inj.
- - simpl. eauto.
- - iIntros (v) "Hv0".
- iEval (rewrite /ty_own_val/=).
- eauto with iFrame.
- Qed.
-
- Global Instance owned_subtype_na_ex_plain_t_inst π E L (ty : type rt) (r : rt) (r' : X) :
- OwnedSubtype π E L false r r' ty (∃na; P, ty) :=
- λ T, i2p (owned_subtype_na_ex_plain_t π E L ty r r' T).
-
- Lemma na_ex_plain_t_open_owned F π (ty : type rt) (wl : bool) (l : loc) (x : X) :
- lftE ⊆ F →
- l â—â‚—[Ï€, Owned wl] PlaceIn x @ (â— (∃na; P, ty)) ={F}=∗
- ∃ r : rt, P.(na_inv_P) π r x ∗
- l â—â‚—[Ï€, Owned false] PlaceIn r @ (â— ty) ∗
- (∀ rt' (lt' : ltype rt') (r' : place_rfn rt'),
- l â—â‚—[Ï€, Owned false] r' @ lt' -∗
- ⌜ltype_st lt' = ty_syn_type ty⌠-∗
- l â—â‚—[Ï€, Owned wl] r' @
- (OpenedLtype lt' (◠ty) (◠∃na; P, ty)
- (λ (r : rt) (x : X), P.(na_inv_P) π r x)
- (λ r x, True)))%I.
- Proof.
- (* Nothing has changed *)
- iIntros (?) "Hb".
- rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hsc & #Hlb & Hcred & %x' & Hrfn & Hb)".
- iMod (maybe_use_credit with "Hcred Hb") as "(Hcred & Hat & Hb)"; first done.
+Section na_subtype.
+ Context `{!typeGS Σ}.
+ Context {rt X : Type} (P : na_ex_inv_def rt X).
- unfold ty_own_val, na_ex_plain_t at 2.
- iDestruct "Hb" as "(%v & Hl & %r & HP & Hv)".
+ Lemma owned_subtype_na_ex_plain_t π E L (ty : type rt) (r : rt) (r' : X) T :
+ (prove_with_subtype E L false ProveDirect (P.(na_inv_P) π r r') (λ L1 _ R, R -∗ T L1))
+ ⊢ owned_subtype π E L false r r' ty (∃na; P, ty) T.
+ Proof.
+ unfold owned_subtype, prove_with_subtype.
+
+ (* Nothing has changed *)
+ iIntros "HT".
+ iIntros (????) "#CTX #HE HL".
+ iMod ("HT" with "[//] [//] [//] CTX HE HL") as "(%L2 & % & %R2 & >(Hinv & HR2) & HL & HT)".
+ iExists L2. iFrame. iPoseProof ("HT" with "HR2") as "$". iModIntro.
+ iSplitR; last iSplitR.
+ - simpl. iPureIntro.
+ intros ly1 ly2 Hly1 HLy2. f_equiv. by eapply syn_type_has_layout_inj.
+ - simpl. eauto.
+ - iIntros (v) "Hv0".
+ iEval (rewrite /ty_own_val/=).
+ eauto with iFrame.
+ Qed.
- iDestruct "Hrfn" as "<-".
- iModIntro. iExists r. iFrame.
- iSplitL "Hl Hv".
- { rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iExists ly. iFrame "#%". iSplitR; first done.
- iExists r. iSplitR; first done. iModIntro. eauto with iFrame. }
-
- iIntros (rt' lt' r') "Hb %Hst".
- rewrite ltype_own_opened_unfold /opened_ltype_own.
- iExists ly. rewrite Hst.
- do 5 iR; iFrame.
-
- clear -Halg Hly.
- iApply (logical_step_intro_maybe with "Hat").
- iIntros "Hcred' !>".
- iIntros (r' r'' κs) "HP".
- iSplitR; first done.
- iIntros "Hdead Hl".
- rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hl" as "(%ly' & _ & _ & Hsc' & _ & _ & %r0 & -> & >Hb)".
- iDestruct "Hb" as "(%v' & Hl & Hv)".
- iMod ("HP" with "Hdead" ) as "HP".
- iModIntro.
- rewrite ltype_own_core_equiv. simp_ltypes.
- rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iExists ly. simpl. iFrame "#%". iFrame.
- iExists r''. iSplitR; first done. iModIntro.
- iExists v'. iFrame. iExists r0. by iFrame.
- Qed.
-
- Lemma typed_place_na_ex_plain_t_owned π E L l (ty : type rt) x wl bmin K T :
- (∀ r, introduce_with_hooks E L (P.(na_inv_P) π r x)
- (λ L2, typed_place π E L2 l
- (OpenedLtype (◠ty) (◠ty) (◠(∃na; P, ty)) (λ (r : rt) (x : X), P.(na_inv_P) π r x) (λ r x, True))
- (#r) bmin (Owned wl) K
- (λ L2 κs li b2 bmin' rti ltyi ri strong weak,
- (* no weak update possible - after all, we have just opened this invariant *)
- T L2 κs li b2 bmin' rti ltyi ri strong None)))
- ⊢ typed_place π E L l (◠(∃na; P, ty))%I (#x) bmin (Owned wl) K T.
- Proof.
- unfold introduce_with_hooks, typed_place.
-
- (* Nothing has changed *)
- iIntros "HT". iIntros (F ???) "#CTX #HE HL Hincl Hb Hcont".
- iApply fupd_place_to_wp.
- iMod (na_ex_plain_t_open_owned with "Hb") as "(%r & HP & Hb & Hcl)"; first done.
- iPoseProof ("Hcl" with "Hb []") as "Hb"; first done.
- iMod ("HT" with "[] HE HL HP") as "(%L2 & HL & HT)"; first done.
- iApply ("HT" with "[//] [//] CTX HE HL Hincl Hb").
- iModIntro. iIntros (L' κs l2 b2 bmin0 rti ltyi ri strong weak) "Hincl Hl Hc".
- iApply ("Hcont" with "Hincl Hl").
- iSplit; last done.
- iDestruct "Hc" as "[Hc _]".
- destruct strong; last done.
- simp_ltypes. done.
- Qed.
-
- Global Instance na_typed_place_ex_plain_t_owned_inst π E L l (ty : type rt) x wl bmin K `{!TCDone (K ≠[])} :
- TypedPlace E L π l (◠(∃na; P, ty))%I #x bmin (Owned wl) K | 15 :=
- λ T, i2p (typed_place_na_ex_plain_t_owned π E L l ty x wl bmin K T).
-
-
- Lemma opened_na_ltype_acc_owned π {rt_cur rt_inner} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) Cpre Cpost l wl r :
- l â—â‚—[Ï€, Owned wl] r @ OpenedNaLtype lt_cur lt_inner Cpre Cpost -∗
- l â—â‚—[Ï€, Owned false] r @ lt_cur ∗
- (∀ rt_cur' (lt_cur' : ltype rt_cur') r',
- l â—â‚—[Ï€, Owned false] r' @ lt_cur' -∗
- ⌜ltype_st lt_cur' = ltype_st lt_cur⌠-∗
- l â—â‚—[Ï€, Owned wl] r' @ OpenedNaLtype lt_cur' lt_inner Cpre Cpost).
- Proof.
- (* Nothing has changed *)
+ Global Instance owned_subtype_na_ex_plain_t_inst π E L (ty : type rt) (r : rt) (r' : X) :
+ OwnedSubtype π E L false r r' ty (∃na; P, ty) :=
+ λ T, i2p (owned_subtype_na_ex_plain_t π E L ty r r' T).
+
+ Lemma na_ex_plain_t_open_owned F π (ty : type rt) (wl : bool) (l : loc) (x : X) :
+ lftE ⊆ F →
+ l â—â‚—[Ï€, Owned wl] PlaceIn x @ (â— (∃na; P, ty)) ={F}=∗
+ ∃ r : rt, P.(na_inv_P) π r x ∗
+ l â—â‚—[Ï€, Owned false] PlaceIn r @ (â— ty) ∗
+ (∀ rt' (lt' : ltype rt') (r' : place_rfn rt'),
+ l â—â‚—[Ï€, Owned false] r' @ lt' -∗
+ ⌜ltype_st lt' = ty_syn_type ty⌠-∗
+ l â—â‚—[Ï€, Owned wl] r' @
+ (OpenedLtype lt' (◠ty) (◠∃na; P, ty)
+ (λ (r : rt) (x : X), P.(na_inv_P) π r x)
+ (λ r x, True)))%I.
+ Proof.
+ (* Nothing has changed *)
+ iIntros (?) "Hb".
+ rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hsc & #Hlb & Hcred & %x' & Hrfn & Hb)".
+ iMod (maybe_use_credit with "Hcred Hb") as "(Hcred & Hat & Hb)"; first done.
+
+ unfold ty_own_val, na_ex_plain_t at 2.
+ iDestruct "Hb" as "(%v & Hl & %r & HP & Hv)".
+
+ iDestruct "Hrfn" as "<-".
+ iModIntro. iExists r. iFrame.
+ iSplitL "Hl Hv".
+ { rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iExists ly. iFrame "#%". iSplitR; first done.
+ iExists r. iSplitR; first done. iModIntro. eauto with iFrame. }
+
+ iIntros (rt' lt' r') "Hb %Hst".
+ rewrite ltype_own_opened_unfold /opened_ltype_own.
+ iExists ly. rewrite Hst.
+ do 5 iR; iFrame.
+
+ clear -Halg Hly.
+ iApply (logical_step_intro_maybe with "Hat").
+ iIntros "Hcred' !>".
+ iIntros (r' r'' κs) "HP".
+ iSplitR; first done.
+ iIntros "Hdead Hl".
+ rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iDestruct "Hl" as "(%ly' & _ & _ & Hsc' & _ & _ & %r0 & -> & >Hb)".
+ iDestruct "Hb" as "(%v' & Hl & Hv)".
+ iMod ("HP" with "Hdead" ) as "HP".
+ iModIntro.
+ rewrite ltype_own_core_equiv. simp_ltypes.
+ rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iExists ly. simpl. iFrame "#%". iFrame.
+ iExists r''. iSplitR; first done. iModIntro.
+ iExists v'. iFrame. iExists r0. by iFrame.
+ Qed.
- rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
- iIntros "(%ly & ? & ? & ? & ? & $ & Hcl)".
- iIntros (rt_cur' lt_cur' r') "Hown %Hst".
- rewrite ltype_own_opened_na_unfold /opened_ltype_own.
- iExists ly. rewrite Hst. eauto with iFrame.
- Qed.
-
- Lemma typed_place_opened_na_owned π E L {rt_cur rt_inner} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) Cpre Cpost r bmin0 l wl P''' T :
- typed_place π E L l lt_cur r bmin0 (Owned false) P''' (λ L' κs l2 b2 bmin rti ltyi ri strong weak,
- T L' κs l2 b2 bmin rti ltyi ri
- (option_map (λ strong, mk_strong strong.(strong_rt)
- (λ rti2 ltyi2 ri2, OpenedNaLtype (strong.(strong_lt) _ ltyi2 ri2) lt_inner Cpre Cpost)
- (λ rti2 ri2, strong.(strong_rfn) _ ri2)
- strong.(strong_R)) strong)
- (* no weak access possible -- we currently don't have the machinery to restore and fold invariants at this point, though we could in principle enable this *)
- None)
- ⊢ typed_place π E L l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r bmin0 (Owned wl) P''' T.
- Proof.
- unfold introduce_with_hooks, typed_place.
-
- (* Nothing has changed *)
- iIntros "HT". iIntros (Φ F ??) "#CTX #HE HL #Hincl0 Hl HR".
- iPoseProof (opened_na_ltype_acc_owned with "Hl") as "(Hl & Hcl)".
- iApply ("HT" with "[//] [//] CTX HE HL [] Hl").
- { destruct bmin0; done. }
- iIntros (L' ??????? strong weak) "? Hl Hv".
- iApply ("HR" with "[$] Hl").
- iSplit; last done.
- destruct strong as [ strong | ]; last done.
- iIntros (???) "Hl Hst".
- iDestruct "Hv" as "[Hv _]".
- iMod ("Hv" with "Hl Hst") as "(Hl & %Hst & $)".
- iPoseProof ("Hcl" with "Hl [//]") as "Hl".
- cbn. eauto with iFrame.
- Qed.
-
- Global Instance typed_place_opened_na_owned_inst π E L {rt_cur rt_inner} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) Cpre Cpost r bmin0 l wl P :
- TypedPlace E L π l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r bmin0 (Owned wl) P | 5 :=
- λ T, i2p (typed_place_opened_na_owned π E L lt_cur lt_inner Cpre Cpost r bmin0 l wl P T).
-
- Lemma na_ex_plain_t_open_shared E F π (ty : type rt) q κ l (x : X) :
- lftE ⊆ E →
- ↑shrN.@l ⊆ E →
- (shr_locsE l 1 ⊆ F) →
-
- lft_ctx -∗
- na_own π F -∗
- £ 1 -∗ (* Required: P.(na_inv_P) is not Timeless *)
-
- q.[κ] -∗
- l â—â‚—[Ï€, Shared κ] (#x) @ (â— (∃na; P, ty)) ={E}=∗
-
- ∃ r : rt,
- P.(na_inv_P) π r x ∗
- (l â—â‚—[Ï€, Owned false] (#r) @ (â— ty)) ∗
- &na{κ,π,shrN.@l} (∃ r' : rt, l ↦: ty_own_val ty π r' ∗ na_inv_P P π r' x) ∗
-
- ( ∀ r' : rt,
- l â—â‚—[Ï€, Owned false] #r' @ (â— ty) ∗ P.(na_inv_P) Ï€ r' x ={E}=∗
- q.[κ] ∗ na_own π F ).
- Proof.
- iIntros (???) "#LFT Hna Hcred Hq #Hb".
- iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hb".
- iDestruct "Hb" as (ly Halg Hly) "(Hsc & Hlb & %v & -> & #Hb)".
-
- iMod (fupd_mask_mono with "Hb") as "#Hb'"; first done; iClear "Hb".
- iEval (unfold ty_shr, na_ex_plain_t) in "Hb'".
- iDestruct "Hb'" as "(Hscr & Hbor & %ly' & %Hly' & %Halg')".
-
- iMod (na_bor_acc with "LFT Hbor Hq Hna") as "((%r & Hl & HP) & Hna & Hvs)"; [ set_solver.. |].
- iApply (lc_fupd_add_later with "Hcred").
-
- do 2 iModIntro; iExists r; iFrame.
+ Lemma typed_place_na_ex_plain_t_owned π E L l (ty : type rt) x wl bmin K T :
+ (∀ r, introduce_with_hooks E L (P.(na_inv_P) π r x)
+ (λ L2, typed_place π E L2 l
+ (OpenedLtype (◠ty) (◠ty) (◠(∃na; P, ty)) (λ (r : rt) (x : X), P.(na_inv_P) π r x) (λ r x, True))
+ (#r) bmin (Owned wl) K
+ (λ L2 κs li b2 bmin' rti ltyi ri strong weak,
+ (* no weak update possible - after all, we have just opened this invariant *)
+ T L2 κs li b2 bmin' rti ltyi ri strong None)))
+ ⊢ typed_place π E L l (◠(∃na; P, ty))%I (#x) bmin (Owned wl) K T.
+ Proof.
+ unfold introduce_with_hooks, typed_place.
+
+ (* Nothing has changed *)
+ iIntros "HT". iIntros (F ???) "#CTX #HE HL Hincl Hb Hcont".
+ iApply fupd_place_to_wp.
+ iMod (na_ex_plain_t_open_owned with "Hb") as "(%r & HP & Hb & Hcl)"; first done.
+ iPoseProof ("Hcl" with "Hb []") as "Hb"; first done.
+ iMod ("HT" with "[] HE HL HP") as "(%L2 & HL & HT)"; first done.
+ iApply ("HT" with "[//] [//] CTX HE HL Hincl Hb").
+ iModIntro. iIntros (L' κs l2 b2 bmin0 rti ltyi ri strong weak) "Hincl Hl Hc".
+ iApply ("Hcont" with "Hincl Hl").
+ iSplit; last done.
+ iDestruct "Hc" as "[Hc _]".
+ destruct strong; last done.
+ simp_ltypes. done.
+ Qed.
- iSplitL "Hl".
- { rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iExists ly => /=.
- iFrame (Halg Hly) "Hlb Hscr"; iR.
- iExists r; iR.
- by iModIntro. }
+ Global Instance na_typed_place_ex_plain_t_owned_inst π E L l (ty : type rt) x wl bmin K `{!TCDone (K ≠[])} :
+ TypedPlace E L π l (◠(∃na; P, ty))%I #x bmin (Owned wl) K | 15 :=
+ λ T, i2p (typed_place_na_ex_plain_t_owned π E L l ty x wl bmin K T).
- iR; iIntros (r') "(Hl & HP)".
- iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hl".
- iDestruct "Hl" as (???) "(_ & _ & _ & (% & <- & Hl)) /=".
- iMod (fupd_mask_mono with "Hl") as "Hl"; first solve_ndisj.
-
- iApply ("Hvs" with "[Hl HP] Hna").
- iExists r'; iFrame.
- Qed.
-
- Lemma na_own_split π E E' :
- E' ⊆ E ->
- na_own π E -∗ na_own π E' ∗ na_own π (E ∖ E').
- Proof.
- iIntros (?) "Hna".
- rewrite comm.
-
- iApply na_own_union.
- { set_solver. }
-
- replace E with ((E ∖ E') ∪ E') at 1; first done.
-
- set_unfold.
- split; first intuition.
- destruct (decide (x ∈ E')); intuition.
- Qed.
-
- Lemma typed_place_na_ex_plain_t_shared π E L l (ty : type rt) x κ bmin K T :
- find_in_context (FindNaOwn) (λ '(π', mask),
- ⌜π = π'⌠∗
- ⌜↑shrN.@l ⊆ mask⌠∗
- prove_with_subtype E L false ProveDirect (£ 1) (λ L1 _ R, R -∗
- li_tactic (lctx_lft_alive_count_goal E L1 κ) (λ '(κs, L2),
- ∀ r, introduce_with_hooks E L2
- (P.(na_inv_P) π r x ∗
- l â—â‚—[Ï€, Owned false] (#r) @
- (OpenedNaLtype (â— ty) (â— ty)
- (λ rfn, P.(na_inv_P) π rfn x)
- (λ _, na_own π (↑shrN.@l) ∗ llft_elt_toks κs)) ∗
- na_own π (mask ∖ ↑shrN.@l))
- (λ L3,
- typed_place π E L3 l
- (ShadowedLtype (AliasLtype _ (ty_syn_type ty) l) #tt (◠(∃na; P, ty)))
- (#x) (bmin ⊓ₖ Shared κ) (Shared κ) K
- (λ L4 κs li b2 bmin' rti ltyi ri strong weak,
- T L4 κs li b2 bmin' rti ltyi ri strong None)))))
- ⊢ typed_place π E L l (◠(∃na; P, ty))%I (#x) bmin (Shared κ) K T.
- Proof.
- rewrite /find_in_context.
- iDestruct 1 as ([Ï€' mask]) "(Hna & <- & % & HT) /=".
-
- rewrite /typed_place /introduce_with_hooks.
- iIntros (Φ ???) "#(LFT & TIME & LLCTX) #HE HL ? Hl Hcont".
-
- rewrite /prove_with_subtype.
- iApply fupd_place_to_wp.
-
- iMod ("HT" with "[] [] [] [$LFT $TIME $LLCTX] HE HL")
- as "(% & % & % & >(Hcred & HR) & HL & HT)"; [ done.. |].
- iSpecialize ("HT" with "HR").
-
- rewrite /li_tactic /lctx_lft_alive_count_goal.
- iDestruct "HT" as (???) "HT".
-
- iMod (fupd_mask_subseteq (lftE ∪ shrE)) as "Hf"; first done.
- iMod (lctx_lft_alive_count_tok with "HE HL") as (q) "(Htok & Htokcl & HL)"; [ solve_ndisj.. |].
- iPoseProof (na_own_split with "Hna") as "(Hna & Hna')"; first done.
- iMod (na_ex_plain_t_open_shared with "LFT Hna Hcred Htok Hl") as (r) "(HP & Hl & #Hbor & Hvs)"; [ try solve_ndisj.. |].
- iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hl".
- iDestruct "Hl" as (ly Halg Hly) "(#Hsc & #Hlb & _ & (% & <- & Hl))".
+ Lemma opened_na_ltype_acc_owned π {rt_cur rt_inner} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) Cpre Cpost l wl r :
+ l â—â‚—[Ï€, Owned wl] r @ OpenedNaLtype lt_cur lt_inner Cpre Cpost -∗
+ l â—â‚—[Ï€, Owned false] r @ lt_cur ∗
+ (∀ rt_cur' (lt_cur' : ltype rt_cur') r',
+ l â—â‚—[Ï€, Owned false] r' @ lt_cur' -∗
+ ⌜ltype_st lt_cur' = ltype_st lt_cur⌠-∗
+ l â—â‚—[Ï€, Owned wl] r' @ OpenedNaLtype lt_cur' lt_inner Cpre Cpost).
+ Proof.
+ (* Nothing has changed *)
- iMod ("HT" with "[] HE HL [$HP Hl Htokcl Hvs Hna']") as "HT"; first solve_ndisj.
- { rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
- iFrame.
- iExists ly; repeat iR.
+ rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
+ iIntros "(%ly & ? & ? & ? & ? & $ & Hcl)".
+ iIntros (rt_cur' lt_cur' r') "Hown %Hst".
+ rewrite ltype_own_opened_na_unfold /opened_ltype_own.
+ iExists ly. rewrite Hst. eauto with iFrame.
+ Qed.
- iSplitL "Hl".
- { rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iExists ly; repeat iR.
- by iExists r; iR. }
+ Lemma typed_place_opened_na_owned π E L {rt_cur rt_inner} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) Cpre Cpost r bmin0 l wl P''' T :
+ typed_place π E L l lt_cur r bmin0 (Owned false) P''' (λ L' κs l2 b2 bmin rti ltyi ri strong weak,
+ T L' κs l2 b2 bmin rti ltyi ri
+ (option_map (λ strong, mk_strong strong.(strong_rt)
+ (λ rti2 ltyi2 ri2, OpenedNaLtype (strong.(strong_lt) _ ltyi2 ri2) lt_inner Cpre Cpost)
+ (λ rti2 ri2, strong.(strong_rfn) _ ri2)
+ strong.(strong_R)) strong)
+ (* no weak access possible -- we currently don't have the machinery to restore and fold invariants at this point, though we could in principle enable this *)
+ None)
+ ⊢ typed_place π E L l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r bmin0 (Owned wl) P''' T.
+ Proof.
+ unfold introduce_with_hooks, typed_place.
+
+ (* Nothing has changed *)
+ iIntros "HT". iIntros (Φ F ??) "#CTX #HE HL #Hincl0 Hl HR".
+ iPoseProof (opened_na_ltype_acc_owned with "Hl") as "(Hl & Hcl)".
+ iApply ("HT" with "[//] [//] CTX HE HL [] Hl").
+ { destruct bmin0; done. }
+ iIntros (L' ??????? strong weak) "? Hl Hv".
+ iApply ("HR" with "[$] Hl").
+ iSplit; last done.
+ destruct strong as [ strong | ]; last done.
+ iIntros (???) "Hl Hst".
+ iDestruct "Hv" as "[Hv _]".
+ iMod ("Hv" with "Hl Hst") as "(Hl & %Hst & $)".
+ iPoseProof ("Hcl" with "Hl [//]") as "Hl".
+ cbn. eauto with iFrame.
+ Qed.
- iApply logical_step_intro.
+ Global Instance typed_place_opened_na_owned_inst π E L {rt_cur rt_inner} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) Cpre Cpost r bmin0 l wl P :
+ TypedPlace E L π l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r bmin0 (Owned wl) P | 5 :=
+ λ T, i2p (typed_place_opened_na_owned π E L lt_cur lt_inner Cpre Cpost r bmin0 l wl P T).
- iIntros (r') "Hinv Hl".
- iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hl".
- iDestruct "Hl" as (ly' Halg' Hly') "(_ & #Hlb' & _ & (% & <- & Hl))".
+ Lemma na_ex_plain_t_open_shared E F π (ty : type rt) q κ l (x : X) :
+ lftE ⊆ E →
+ ↑shrN.@l ⊆ E →
+ (shr_locsE l 1 ⊆ F) →
- iMod ("Hvs" with "[Hl Hinv]") as "(? & ?)".
- { iFrame.
- rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iExists ly'; repeat iR.
- by iExists r'; iR. }
+ lft_ctx -∗
+ na_own π F -∗
+ £ 1 -∗ (* Required: P.(na_inv_P) is not Timeless *)
- iFrame.
- by iApply "Htokcl". }
+ q.[κ] -∗
+ l â—â‚—[Ï€, Shared κ] (#x) @ (â— (∃na; P, ty)) ={E}=∗
- iDestruct "HT" as (?) "(HL & HT)".
+ ∃ r : rt,
+ P.(na_inv_P) π r x ∗
+ (l â—â‚—[Ï€, Owned false] (#r) @ (â— ty)) ∗
+ &na{κ,π,shrN.@l} (∃ r' : rt, l ↦: ty_own_val ty π r' ∗ na_inv_P P π r' x) ∗
- iApply ("HT" with "[//] [//] [$LFT $TIME $LLCTX] HE HL [] []").
- { iApply bor_kind_min_incl_r. }
- { rewrite ltype_own_shadowed_unfold /shadowed_ltype_own.
+ ( ∀ r' : rt,
+ l â—â‚—[Ï€, Owned false] #r' @ (â— ty) ∗ P.(na_inv_P) Ï€ r' x ={E}=∗
+ q.[κ] ∗ na_own π F ).
+ Proof.
+ iIntros (???) "#LFT Hna Hcred Hq #Hb".
+ iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hb".
+ iDestruct "Hb" as (ly Halg Hly) "(Hsc & Hlb & %v & -> & #Hb)".
- iR; iSplitL.
- { rewrite ltype_own_alias_unfold /alias_lty_own.
- iExists ly. by repeat iR. }
+ iMod (fupd_mask_mono with "Hb") as "#Hb'"; first done; iClear "Hb".
+ iEval (unfold ty_shr, na_ex_plain_t) in "Hb'".
+ iDestruct "Hb'" as "(Hscr & Hbor & %ly' & %Hly' & %Halg')".
- rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iExists ly; repeat iR.
- iExists x; repeat iR.
+ iMod (na_bor_acc with "LFT Hbor Hq Hna") as "((%r & Hl & HP) & Hna & Hvs)"; [ set_solver.. |].
+ iApply (lc_fupd_add_later with "Hcred").
- rewrite /ty_shr /na_ex_plain_t.
- repeat iR.
- by iExists ly; repeat iR. }
+ do 2 iModIntro; iExists r; iFrame.
- iMod "Hf" as "_".
- iIntros "!>" (? ? ? ? ? ? ? ? strong ?) "Hincl Hl [ Hstrong _ ]".
-
- iApply ("Hcont" with "Hincl Hl").
- destruct strong; iSplit; [| done.. ].
- by simp_ltypes.
- Qed.
-
- Global Instance typed_place_na_ex_plain_t_shared_inst π E L l (ty : type rt) x κ bmin K `{!TCDone (K ≠[])} :
- TypedPlace E L π l (◠(∃na; P, ty))%I #x bmin (Shared κ) K | 15 :=
- λ T, i2p (typed_place_na_ex_plain_t_shared π E L l ty x κ bmin K T).
-
- Lemma typed_place_alias_shared π E L l l2 rt''' (r : place_rfn rt''') st bmin0 κ P''' T :
- find_in_context (FindLoc l2) (λ '(existT rt2 (lt2, r2, b2, π2)),
- ⌜π = π2⌠∗
- typed_place π E L l2 lt2 r2 b2 b2 P''' (λ L' κs li b3 bmin rti ltyi ri strong weak,
- T L' κs li b3 bmin rti ltyi ri
- (fmap (λ strong, mk_strong (λ _, _) (λ _ _ _, AliasLtype rt''' st l2) (λ _ _, r)
- (* give back ownership through R *)
- (λ rti2 ltyi2 ri2, l2 â—â‚—[Ï€, b2] strong.(strong_rfn) _ ri2 @ strong.(strong_lt) _ ltyi2 ri2 ∗ strong.(strong_R) _ ltyi2 ri2)) strong)
- None))
- ⊢ typed_place π E L l (AliasLtype rt''' st l2) r bmin0 (Shared κ) P''' T.
- Proof.
- unfold find_in_context, typed_place.
-
- iDestruct 1 as ((rt2 & (((lt & r''') & b2) & π2))) "(Hl2 & <- & HP)". simpl.
- iIntros (????) "#CTX #HE HL #Hincl Hl Hcont".
- rewrite ltype_own_alias_unfold /alias_lty_own.
- iDestruct "Hl" as "(%ly & % & -> & #? & #?)".
-
- iApply ("HP" with "[//] [//] CTX HE HL [] Hl2").
- { iApply bor_kind_incl_refl. }
- iIntros (L' κs l2 b0 bmin rti ltyi ri strong weak) "#Hincl1 Hl2 Hcl HT HL".
- iApply ("Hcont" with "[//] Hl2 [Hcl] HT HL").
-
- iSplit; last done.
-
- destruct strong as [ strong |]; last done.
- iDestruct "Hcl" as "[Hcl _]"; simpl.
-
- iIntros (rti2 ltyi2 ri2) "Hl2 %Hst".
- iMod ("Hcl" with "Hl2 [//]") as "(Hl & % & Hstrong)".
- iModIntro.
+ iSplitL "Hl".
+ { rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iExists ly => /=.
+ iFrame (Halg Hly) "Hlb Hscr"; iR.
+ iExists r; iR.
+ by iModIntro. }
- rewrite ltype_own_alias_unfold /alias_lty_own.
- iFrame. iSplit; [| done].
- iExists ly; by repeat iR.
- Qed.
- Global Instance typed_place_alias_shared_inst π E L l l2 rt r st bmin0 κ P :
- TypedPlace E L π l (AliasLtype rt st l2) r bmin0 (Shared κ) P :=
- λ T, i2p (typed_place_alias_shared π E L l l2 rt r st bmin0 κ P T).
-
- Lemma stratify_ltype_alias_shared π E L mu mdu ma {M} (m : M) l l2 rt''' st r κ (T : stratify_ltype_cont_t) :
- ( if decide (ma = StratNoRefold)
- then
- T L True _ (AliasLtype rt''' st l2) r
- else
- find_in_context (FindLoc l2) (λ '(existT rt2 (lt2, r2, b2, π2)),
- ⌜π = π2⌠∗ ⌜ltype_st lt2 = st⌠∗ ⌜b2 = Owned false⌠∗
- (* recursively stratify *)
- stratify_ltype π E L mu mdu ma m l2 lt2 r2 b2
- (λ L2 R rt2' lt2' r2',
- (T L2 ((l2 â—â‚—[Ï€, Owned false] r2' @ lt2') ∗ R) rt''' (AliasLtype rt''' st l2) r))))
- ⊢ stratify_ltype π E L mu mdu ma m l (AliasLtype rt''' st l2) r (Shared κ) T.
- Proof.
- rewrite /stratify_ltype /find_in_context.
- iIntros "HT".
-
- destruct (decide (ma = StratNoRefold)) as [-> | ].
- { iIntros (????) "#CTX #HE HL Hl". iModIntro. iExists _, _, _, _, _. iFrame.
- iSplitR; first done. iApply logical_step_intro. by iFrame. }
-
- iDestruct "HT" as ([rt2 [[[lt2 r2] b2] π2]]) "(Hl2 & <- & <- & -> & HT)"; simpl.
-
- iIntros (????) "#CTX #HE HL Hl".
- rewrite ltype_own_alias_unfold /alias_lty_own.
- simp_ltypes.
-
- iDestruct "Hl" as "(%ly & %Halg & -> & %Hly & Hlb)".
-
- iMod ("HT" with "[//] [//] [//] CTX HE HL Hl2") as (L3 R rt2' lt2' r2') "(HL & %Hst & Hstep & HT)".
- iModIntro. iExists _, _, _, _, _.
- iFrame; iR.
+ iR; iIntros (r') "(Hl & HP)".
+ iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hl".
+ iDestruct "Hl" as (???) "(_ & _ & _ & (% & <- & Hl)) /=".
+ iMod (fupd_mask_mono with "Hl") as "Hl"; first solve_ndisj.
+
+ iApply ("Hvs" with "[Hl HP] Hna").
+ iExists r'; iFrame.
+ Qed.
+
+ Lemma na_own_split π E E' :
+ E' ⊆ E ->
+ na_own π E -∗ na_own π E' ∗ na_own π (E ∖ E').
+ Proof.
+ iIntros (?) "Hna".
+ rewrite comm.
+
+ iApply na_own_union.
+ { set_solver. }
+
+ replace E with ((E ∖ E') ∪ E') at 1; first done.
+
+ set_unfold.
+ split; first intuition.
+ destruct (decide (x ∈ E')); intuition.
+ Qed.
+
+ Lemma typed_place_na_ex_plain_t_shared π E L l (ty : type rt) x κ bmin K T :
+ find_in_context (FindNaOwn) (λ '(π', mask),
+ ⌜π = π'⌠∗
+ ⌜↑shrN.@l ⊆ mask⌠∗
+ prove_with_subtype E L false ProveDirect (£ 1) (λ L1 _ R, R -∗
+ li_tactic (lctx_lft_alive_count_goal E L1 κ) (λ '(κs, L2),
+ ∀ r, introduce_with_hooks E L2
+ (P.(na_inv_P) π r x ∗
+ l â—â‚—[Ï€, Owned false] (#r) @
+ (OpenedNaLtype (â— ty) (â— ty)
+ (λ rfn, P.(na_inv_P) π rfn x)
+ (λ _, na_own π (↑shrN.@l) ∗ llft_elt_toks κs)) ∗
+ na_own π (mask ∖ ↑shrN.@l))
+ (λ L3,
+ typed_place π E L3 l
+ (ShadowedLtype (AliasLtype _ (ty_syn_type ty) l) #tt (◠(∃na; P, ty)))
+ (#x) (bmin ⊓ₖ Shared κ) (Shared κ) K
+ (λ L4 κs li b2 bmin' rti ltyi ri strong weak,
+ T L4 κs li b2 bmin' rti ltyi ri strong None)))))
+ ⊢ typed_place π E L l (◠(∃na; P, ty))%I (#x) bmin (Shared κ) K T.
+ Proof.
+ rewrite /find_in_context.
+ iDestruct 1 as ([Ï€' mask]) "(Hna & <- & % & HT) /=".
+
+ rewrite /typed_place /introduce_with_hooks.
+ iIntros (Φ ???) "#(LFT & TIME & LLCTX) #HE HL ? Hl Hcont".
+
+ rewrite /prove_with_subtype.
+ iApply fupd_place_to_wp.
+
+ iMod ("HT" with "[] [] [] [$LFT $TIME $LLCTX] HE HL")
+ as "(% & % & % & >(Hcred & HR) & HL & HT)"; [ done.. |].
+ iSpecialize ("HT" with "HR").
+
+ rewrite /li_tactic /lctx_lft_alive_count_goal.
+ iDestruct "HT" as (???) "HT".
+
+ iMod (fupd_mask_subseteq (lftE ∪ shrE)) as "Hf"; first done.
+ iMod (lctx_lft_alive_count_tok with "HE HL") as (q) "(Htok & Htokcl & HL)"; [ solve_ndisj.. |].
+ iPoseProof (na_own_split with "Hna") as "(Hna & Hna')"; first done.
+ iMod (na_ex_plain_t_open_shared with "LFT Hna Hcred Htok Hl") as (r) "(HP & Hl & #Hbor & Hvs)"; [ try solve_ndisj.. |].
+
+ iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hl".
+ iDestruct "Hl" as (ly Halg Hly) "(#Hsc & #Hlb & _ & (% & <- & Hl))".
+
+ iMod ("HT" with "[] HE HL [$HP Hl Htokcl Hvs Hna']") as "HT"; first solve_ndisj.
+ { rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
+ iFrame.
+ iExists ly; repeat iR.
+
+ iSplitL "Hl".
+ { rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iExists ly; repeat iR.
+ by iExists r; iR. }
- iApply (logical_step_compose with "Hstep").
iApply logical_step_intro.
- iIntros "($ & $)".
-
- rewrite ltype_own_alias_unfold /alias_lty_own.
- by iExists ly; iFrame.
- Qed.
- Global Instance stratify_ltype_alias_shared_inst π E L mu mdu ma {M} (m : M) l l2 rt st r κ :
- StratifyLtype π E L mu mdu ma m l (AliasLtype rt st l2) r (Shared κ) :=
- λ T, i2p (stratify_ltype_alias_shared π E L mu mdu ma m l l2 rt st r κ T).
-
- Lemma stratify_ltype_opened_na_Owned {rt_cur rt_inner} π E L mu mdu ma {M} (ml : M) l
- (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner)
- (Cpre Cpost : rt_inner → iProp Σ) r (T : stratify_ltype_cont_t) :
- stratify_ltype π E L mu mdu ma ml l lt_cur r (Owned false)
- (λ L' R rt_cur' lt_cur' (r' : place_rfn rt_cur'),
- if decide (ma = StratNoRefold)
- then (* keep it open *)
- T L' R _ (OpenedNaLtype lt_cur' lt_inner Cpre Cpost) r'
- else (* fold the invariant *)
- ∃ ri,
- (* show that the core of lt_cur' is a subtype of lt_inner *)
- weak_subltype E L' (Owned false) (r') (#ri) lt_cur' lt_inner (
- (* re-establish the invariant *)
- prove_with_subtype E L' true ProveDirect (Cpre ri)
- (λ L'' _ R2, T L'' (Cpost ri ∗ R2 ∗ R) unit (AliasLtype unit (ltype_st lt_inner) l) #tt)))
- ⊢ stratify_ltype π E L mu mdu ma ml l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r (Owned false) T.
- Proof.
- rewrite /stratify_ltype /weak_subltype /prove_with_subtype.
-
- iIntros "Hstrat" (F ???) "#CTX #HE HL Hl".
- rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
- iDestruct "Hl" as "(%ly & %Halg & %Hly & #Hlb & %Hst & Hl & Hcl)".
- iMod ("Hstrat" with "[//] [//] [//] CTX HE HL Hl") as "(%L2 & %R & %rt_cur' & %lt_cur' & %r' & HL & %Hst' & Hstep & HT)".
+ iIntros (r') "Hinv Hl".
+ iEval (rewrite ltype_own_ofty_unfold /lty_of_ty_own) in "Hl".
+ iDestruct "Hl" as (ly' Halg' Hly') "(_ & #Hlb' & _ & (% & <- & Hl))".
- destruct (decide (ma = StratNoRefold)) as [-> | ].
- - (* don't fold *)
- iModIntro.
- iExists _, _, _, _, _; iFrame; iR.
+ iMod ("Hvs" with "[Hl Hinv]") as "(? & ?)".
+ { iFrame.
+ rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iExists ly'; repeat iR.
+ by iExists r'; iR. }
- iApply (logical_step_compose with "Hstep").
- iApply logical_step_intro.
- iIntros "(Hl & $)".
+ iFrame.
+ by iApply "Htokcl". }
- rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
- iExists ly; iFrame.
- rewrite -Hst'; do 3 iR.
- done.
+ iDestruct "HT" as (?) "(HL & HT)".
- - (* fold it again *)
- iDestruct "HT" as "(%ri & HT)".
- iMod ("HT" with "[//] CTX HE HL") as "(Hincl & HL & HT)".
- iMod ("HT" with "[//] [//] [//] CTX HE HL") as "(%L3 & %κs & %R2 & Hstep' & HL & HT)".
+ iApply ("HT" with "[//] [//] [$LFT $TIME $LLCTX] HE HL [] []").
+ { iApply bor_kind_min_incl_r. }
+ { rewrite ltype_own_shadowed_unfold /shadowed_ltype_own.
- iExists L3, _, _, _, _; iFrame.
- iSplitR.
- { by simp_ltypes. }
+ iR; iSplitL.
+ { rewrite ltype_own_alias_unfold /alias_lty_own.
+ iExists ly. by repeat iR. }
- iApply logical_step_fupd.
- iApply (logical_step_compose with "Hstep").
- iPoseProof (logical_step_mask_mono with "Hcl") as "Hcl"; first done.
- iApply (logical_step_compose with "Hcl").
- iApply (logical_step_compose with "Hstep'").
- iApply logical_step_intro.
+ rewrite ltype_own_ofty_unfold /lty_of_ty_own.
+ iExists ly; repeat iR.
+ iExists x; repeat iR.
- iIntros "!> (Hpre & $) Hcl (Hl & $)".
- iMod (ltype_incl_use with "Hincl Hl") as "Hl"; first done.
+ rewrite /ty_shr /na_ex_plain_t.
+ repeat iR.
+ by iExists ly; repeat iR. }
- iPoseProof ("Hcl" with "Hpre Hl") as "Hvs".
- iSplitL "".
- { rewrite ltype_own_alias_unfold /alias_lty_own.
- rewrite -Hst.
+ iMod "Hf" as "_".
+ iIntros "!>" (? ? ? ? ? ? ? ? strong ?) "Hincl Hl [ Hstrong _ ]".
- by iExists ly; repeat iR. }
+ iApply ("Hcont" with "Hincl Hl").
+ destruct strong; iSplit; [| done.. ].
+ by simp_ltypes.
+ Qed.
- iMod (fupd_mask_mono with "Hvs") as "Hvs"; first set_solver.
- done.
- Qed.
+ Global Instance typed_place_na_ex_plain_t_shared_inst π E L l (ty : type rt) x κ bmin K `{!TCDone (K ≠[])} :
+ TypedPlace E L π l (◠(∃na; P, ty))%I #x bmin (Shared κ) K | 15 :=
+ λ T, i2p (typed_place_na_ex_plain_t_shared π E L l ty x κ bmin K T).
+
+ Lemma typed_place_alias_shared π E L l l2 rt''' (r : place_rfn rt''') st bmin0 κ P''' T :
+ find_in_context (FindLoc l2) (λ '(existT rt2 (lt2, r2, b2, π2)),
+ ⌜π = π2⌠∗
+ typed_place π E L l2 lt2 r2 b2 b2 P''' (λ L' κs li b3 bmin rti ltyi ri strong weak,
+ T L' κs li b3 bmin rti ltyi ri
+ (fmap (λ strong, mk_strong (λ _, _) (λ _ _ _, AliasLtype rt''' st l2) (λ _ _, r)
+ (* give back ownership through R *)
+ (λ rti2 ltyi2 ri2, l2 â—â‚—[Ï€, b2] strong.(strong_rfn) _ ri2 @ strong.(strong_lt) _ ltyi2 ri2 ∗ strong.(strong_R) _ ltyi2 ri2)) strong)
+ None))
+ ⊢ typed_place π E L l (AliasLtype rt''' st l2) r bmin0 (Shared κ) P''' T.
+ Proof.
+ unfold find_in_context, typed_place.
- Global Instance stratify_ltype_opened_na_owned_inst {rt_cur rt_inner} π E L mu mdu ma {M} (ml : M) l
- (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (Cpre Cpost : rt_inner → iProp Σ) r:
- StratifyLtype π E L mu mdu ma ml l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r (Owned false) := λ T, i2p (stratify_ltype_opened_na_Owned π E L mu mdu ma ml l lt_cur lt_inner Cpre Cpost r T).
+ iDestruct 1 as ((rt2 & (((lt & r''') & b2) & π2))) "(Hl2 & <- & HP)". simpl.
+ iIntros (????) "#CTX #HE HL #Hincl Hl Hcont".
+ rewrite ltype_own_alias_unfold /alias_lty_own.
+ iDestruct "Hl" as "(%ly & % & -> & #? & #?)".
- End na_subtype.
+ iApply ("HP" with "[//] [//] CTX HE HL [] Hl2").
+ { iApply bor_kind_incl_refl. }
+ iIntros (L' κs l2 b0 bmin rti ltyi ri strong weak) "#Hincl1 Hl2 Hcl HT HL".
+ iApply ("Hcont" with "[//] Hl2 [Hcl] HT HL").
- (* === ^ TYPING RULES ^ === *)
+ iSplit; last done.
- Section proof.
- Context `{!refinedrustGS Σ}.
+ destruct strong as [ strong |]; last done.
+ iDestruct "Hcl" as "[Hcl _]"; simpl.
- Lemma UnsafeCell_new_proof (Ï€ : thread_id) :
- UnsafeCell_new_lemma π.
- Proof.
- UnsafeCell_new_prelude.
+ iIntros (rti2 ltyi2 ri2) "Hl2 %Hst".
+ iMod ("Hcl" with "Hl2 [//]") as "(Hl & % & Hstrong)".
+ iModIntro.
- repeat liRStep; liShow.
+ rewrite ltype_own_alias_unfold /alias_lty_own.
+ iFrame. iSplit; [| done].
+ iExists ly; by repeat iR.
+ Qed.
+ Global Instance typed_place_alias_shared_inst π E L l l2 rt r st bmin0 κ P :
+ TypedPlace E L π l (AliasLtype rt st l2) r bmin0 (Shared κ) P :=
+ λ T, i2p (typed_place_alias_shared π E L l l2 rt r st bmin0 κ P T).
+
+ Lemma stratify_ltype_alias_shared π E L mu mdu ma {M} (m : M) l l2 rt''' st r κ (T : stratify_ltype_cont_t) :
+ ( if decide (ma = StratNoRefold)
+ then
+ T L True _ (AliasLtype rt''' st l2) r
+ else
+ find_in_context (FindLoc l2) (λ '(existT rt2 (lt2, r2, b2, π2)),
+ ⌜π = π2⌠∗ ⌜ltype_st lt2 = st⌠∗ ⌜b2 = Owned false⌠∗
+ (* recursively stratify *)
+ stratify_ltype π E L mu mdu ma m l2 lt2 r2 b2
+ (λ L2 R rt2' lt2' r2',
+ (T L2 ((l2 â—â‚—[Ï€, Owned false] r2' @ lt2') ∗ R) rt''' (AliasLtype rt''' st l2) r))))
+ ⊢ stratify_ltype π E L mu mdu ma m l (AliasLtype rt''' st l2) r (Shared κ) T.
+ Proof.
+ rewrite /stratify_ltype /find_in_context.
+ iIntros "HT".
- all: print_remaining_goal.
- Unshelve. all: sidecond_solver.
- Unshelve. all: sidecond_hammer.
- Unshelve. all: print_remaining_sidecond.
- Qed.
+ destruct (decide (ma = StratNoRefold)) as [-> | ].
+ { iIntros (????) "#CTX #HE HL Hl". iModIntro. iExists _, _, _, _, _. iFrame.
+ iSplitR; first done. iApply logical_step_intro. by iFrame. }
- Lemma UnsafeCell_into_inner_proof (Ï€ : thread_id) :
- UnsafeCell_into_inner_lemma π.
- Proof.
- UnsafeCell_into_inner_prelude.
+ iDestruct "HT" as ([rt2 [[[lt2 r2] b2] π2]]) "(Hl2 & <- & <- & -> & HT)"; simpl.
- repeat liRStep; liShow.
+ iIntros (????) "#CTX #HE HL Hl".
+ rewrite ltype_own_alias_unfold /alias_lty_own.
+ simp_ltypes.
- all: print_remaining_goal.
- Unshelve. all: sidecond_solver.
- Unshelve. all: sidecond_hammer.
- Unshelve. all: print_remaining_sidecond.
- Qed.
+ iDestruct "Hl" as "(%ly & %Halg & -> & %Hly & Hlb)".
- Lemma Cell_new_proof (Ï€ : thread_id) :
- Cell_new_lemma π.
- Proof.
- Cell_new_prelude.
+ iMod ("HT" with "[//] [//] [//] CTX HE HL Hl2") as (L3 R rt2' lt2' r2') "(HL & %Hst & Hstep & HT)".
+ iModIntro. iExists _, _, _, _, _.
+ iFrame; iR.
- repeat liRStep; liShow.
+ iApply (logical_step_compose with "Hstep").
+ iApply logical_step_intro.
+ iIntros "($ & $)".
- all: print_remaining_goal.
- Unshelve. all: sidecond_solver.
- Unshelve. all: sidecond_hammer.
- Unshelve. all: print_remaining_sidecond.
- Qed.
+ rewrite ltype_own_alias_unfold /alias_lty_own.
+ by iExists ly; iFrame.
+ Qed.
+ Global Instance stratify_ltype_alias_shared_inst π E L mu mdu ma {M} (m : M) l l2 rt st r κ :
+ StratifyLtype π E L mu mdu ma m l (AliasLtype rt st l2) r (Shared κ) :=
+ λ T, i2p (stratify_ltype_alias_shared π E L mu mdu ma m l l2 rt st r κ T).
+
+ Lemma stratify_ltype_opened_na_Owned {rt_cur rt_inner} π E L mu mdu ma {M} (ml : M) l
+ (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner)
+ (Cpre Cpost : rt_inner → iProp Σ) r (T : stratify_ltype_cont_t) :
+ stratify_ltype π E L mu mdu ma ml l lt_cur r (Owned false)
+ (λ L' R rt_cur' lt_cur' (r' : place_rfn rt_cur'),
+ if decide (ma = StratNoRefold)
+ then (* keep it open *)
+ T L' R _ (OpenedNaLtype lt_cur' lt_inner Cpre Cpost) r'
+ else (* fold the invariant *)
+ ∃ ri,
+ (* show that the core of lt_cur' is a subtype of lt_inner *)
+ weak_subltype E L' (Owned false) (r') (#ri) lt_cur' lt_inner (
+ (* re-establish the invariant *)
+ prove_with_subtype E L' true ProveDirect (Cpre ri)
+ (λ L'' _ R2, T L'' (Cpost ri ∗ R2 ∗ R) unit (AliasLtype unit (ltype_st lt_inner) l) #tt)))
+ ⊢ stratify_ltype π E L mu mdu ma ml l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r (Owned false) T.
+ Proof.
+ rewrite /stratify_ltype /weak_subltype /prove_with_subtype.
- Lemma UnsafeCell_get_old_proof (Ï€ : thread_id) :
- UnsafeCell_get_old_lemma π.
- Proof.
- UnsafeCell_get_old_prelude.
+ iIntros "Hstrat" (F ???) "#CTX #HE HL Hl".
+ rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
+
+ iDestruct "Hl" as "(%ly & %Halg & %Hly & #Hlb & %Hst & Hl & Hcl)".
+ iMod ("Hstrat" with "[//] [//] [//] CTX HE HL Hl") as "(%L2 & %R & %rt_cur' & %lt_cur' & %r' & HL & %Hst' & Hstep & HT)".
+
+ destruct (decide (ma = StratNoRefold)) as [-> | ].
+ - (* don't fold *)
+ iModIntro.
+ iExists _, _, _, _, _; iFrame; iR.
+
+ iApply (logical_step_compose with "Hstep").
+ iApply logical_step_intro.
+ iIntros "(Hl & $)".
+
+ rewrite ltype_own_opened_na_unfold /opened_na_ltype_own.
+ iExists ly; iFrame.
+ rewrite -Hst'; do 3 iR.
+ done.
+
+ - (* fold it again *)
+ iDestruct "HT" as "(%ri & HT)".
+ iMod ("HT" with "[//] CTX HE HL") as "(Hincl & HL & HT)".
+ iMod ("HT" with "[//] [//] [//] CTX HE HL") as "(%L3 & %κs & %R2 & Hstep' & HL & HT)".
+
+ iExists L3, _, _, _, _; iFrame.
+ iSplitR.
+ { by simp_ltypes. }
+
+ iApply logical_step_fupd.
+ iApply (logical_step_compose with "Hstep").
+ iPoseProof (logical_step_mask_mono with "Hcl") as "Hcl"; first done.
+ iApply (logical_step_compose with "Hcl").
+ iApply (logical_step_compose with "Hstep'").
+ iApply logical_step_intro.
+
+ iIntros "!> (Hpre & $) Hcl (Hl & $)".
+ iMod (ltype_incl_use with "Hincl Hl") as "Hl"; first done.
+
+ iPoseProof ("Hcl" with "Hpre Hl") as "Hvs".
+ iSplitL "".
+ { rewrite ltype_own_alias_unfold /alias_lty_own.
+ rewrite -Hst.
+
+ by iExists ly; repeat iR. }
+
+ iMod (fupd_mask_mono with "Hvs") as "Hvs"; first set_solver.
+ done.
+ Qed.
- repeat liRStep; liShow.
-
- Unshelve. all: sidecond_solver.
- Unshelve. all: sidecond_hammer.
- Unshelve. all: print_remaining_sidecond.
- Qed.
- End proof.
+ Global Instance stratify_ltype_opened_na_owned_inst {rt_cur rt_inner} π E L mu mdu ma {M} (ml : M) l
+ (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (Cpre Cpost : rt_inner → iProp Σ) r:
+ StratifyLtype π E L mu mdu ma ml l (OpenedNaLtype lt_cur lt_inner Cpre Cpost) r (Owned false) := λ T, i2p (stratify_ltype_opened_na_Owned π E L mu mdu ma ml l lt_cur lt_inner Cpre Cpost r T).
-End generated_code.
+End na_subtype.
diff --git a/theories/rust_typing/existentials_na_test.v b/theories/rust_typing/existentials_na_test.v
new file mode 100644
index 0000000000000000000000000000000000000000..3944978bc02a4b89f2d40d9f2f074f942776f54f
--- /dev/null
+++ b/theories/rust_typing/existentials_na_test.v
@@ -0,0 +1,375 @@
+(* NOTE: This file is expected to be deleted when the `rr_frontend` will be done. *)
+
+From refinedrust Require Import automation.
+From refinedrust Require Import existentials_na.
+From refinedrust Require Import typing.
+
+Section UnsafeCell_sls.
+ Context `{!refinedrustGS Σ}.
+
+ Definition UnsafeCell_sls : struct_layout_spec := mk_sls "UnsafeCell" [
+ ("value", IntSynType I32)] StructReprTransparent.
+ Definition UnsafeCell_st : syn_type := UnsafeCell_sls.
+End UnsafeCell_sls.
+
+Section Cell_sls.
+ Context `{!refinedrustGS Σ}.
+
+ Definition Cell_sls : struct_layout_spec := mk_sls "Cell" [
+ ("value", UnsafeCell_st)] StructReprRust.
+ Definition Cell_st : syn_type := Cell_sls .
+End Cell_sls.
+
+Section code.
+ Context `{!refinedrustGS Σ}.
+ Open Scope printing_sugar.
+
+ Definition UnsafeCell_new_def : function := {|
+ f_args := [
+ ("value", (it_layout I32) : layout)
+ ];
+ f_local_vars := [
+ ("__0", (use_layout_alg' (UnsafeCell_st)) : layout);
+ ("__2", (it_layout I32) : layout)
+ ];
+ f_code :=
+ <[
+ "_bb0" :=
+ "__2" <-{ IntOp I32 } use{ IntOp I32 } ("value");
+ "__0" <-{ (use_op_alg' (UnsafeCell_st)) } StructInit UnsafeCell_sls [("value", use{ IntOp I32 } ("__2") : expr)];
+ return (use{ (use_op_alg' (UnsafeCell_st)) } ("__0"))
+ ]>%E $
+ ∅;
+ f_init := "_bb0";
+ |}.
+
+ Definition UnsafeCell_into_inner_def : function := {|
+ f_args := [
+ ("self", (use_layout_alg' (UnsafeCell_st)) : layout)
+ ];
+ f_local_vars := [
+ ("__0", (it_layout I32) : layout)
+ ];
+ f_code :=
+ <[
+ "_bb0" :=
+ "__0" <-{ IntOp I32 } use{ IntOp I32 } (("self") at{ UnsafeCell_sls } "value");
+ return (use{ IntOp I32 } ("__0"))
+ ]>%E $
+ ∅;
+ f_init := "_bb0";
+ |}.
+
+ Definition UnsafeCell_get_old_def : function := {|
+ f_args := [
+ ("self", void* : layout)
+ ];
+ f_local_vars := [
+ ("__0", (it_layout I32) : layout)
+ ];
+ f_code :=
+ <[
+ "_bb0" :=
+ annot: CopyLftNameAnnot "plft3" "ulft__";
+ "__0" <-{ IntOp I32 } use{ IntOp I32 } ((!{ PtrOp } ( "self" )) at{ (UnsafeCell_sls) } "value");
+ return (use{ IntOp I32 } ("__0"))
+ ]>%E $
+ ∅;
+ f_init := "_bb0";
+ |}.
+
+ Definition UnsafeCell_get_def : function := {|
+ f_args := [
+ ("self", void* : layout)
+ ];
+ f_local_vars := [
+ ("__0", void* : layout);
+ ("__2", void* : layout);
+ ("__3", void* : layout)
+ ];
+ f_code :=
+ <[
+ "_bb0" :=
+ annot: CopyLftNameAnnot "plft3" "ulft_1";
+ "__3" <-{ PtrOp } &raw{ Shr } (!{ PtrOp } ( "self" ));
+ "__2" <-{ PtrOp } use{ PtrOp } ("__3");
+ "__0" <-{ PtrOp } use{ PtrOp } ("__2");
+ return (use{ PtrOp } ("__0"))
+ ]>%E $
+ ∅;
+ f_init := "_bb0";
+ |}.
+
+ Definition Cell_new_def (UnsafeCell_new_loc : loc) : function := {|
+ f_args := [
+ ("value", (it_layout I32) : layout)
+ ];
+ f_local_vars := [
+ ("__0", (use_layout_alg' (Cell_st)) : layout);
+ ("__2", (use_layout_alg' (UnsafeCell_st)) : layout);
+ ("__3", (it_layout I32) : layout)
+ ];
+ f_code :=
+ <[
+ "_bb0" :=
+ "__3" <-{ IntOp I32 } use{ IntOp I32 } ("value");
+ "__2" <-{ (use_op_alg' (UnsafeCell_st)) } CallE UnsafeCell_new_loc [] [] [@{expr} use{ IntOp I32 } ("__3")];
+ Goto "_bb1"
+ ]>%E $
+ <[
+ "_bb1" :=
+ "__0" <-{ (use_op_alg' (Cell_st)) } StructInit Cell_sls [("value", use{ (use_op_alg' (UnsafeCell_st)) } ("__2") : expr)];
+ return (use{ (use_op_alg' (Cell_st)) } ("__0"))
+ ]>%E $
+ ∅;
+ f_init := "_bb0";
+ |}.
+
+ Definition Cell_into_inner_def (UnsafeCell_into_inner_loc : loc) : function := {|
+ f_args := [
+ ("self", (use_layout_alg' (Cell_st)) : layout)
+ ];
+ f_local_vars := [
+ ("__0", (it_layout I32) : layout);
+ ("__2", (use_layout_alg' (UnsafeCell_st)) : layout)
+ ];
+ f_code :=
+ <[
+ "_bb0" :=
+ "__2" <-{ (use_op_alg' (UnsafeCell_st)) } use{ (use_op_alg' (UnsafeCell_st)) } (("self") at{ Cell_sls } "value");
+ "__0" <-{ IntOp I32 } CallE UnsafeCell_into_inner_loc [] [] [@{expr} use{ (use_op_alg' (UnsafeCell_st)) } ("__2")];
+ Goto "_bb1"
+ ]>%E $
+ <[
+ "_bb1" :=
+ return (use{ IntOp I32 } ("__0"))
+ ]>%E $
+ ∅;
+ f_init := "_bb0";
+ |}.
+End code.
+
+Section UnsafeCell_ty.
+ Context `{!refinedrustGS Σ}.
+
+ Definition UnsafeCell_ty : type (plist place_rfn [Z : Type]).
+ Proof using Type*. exact (struct_t UnsafeCell_sls +[(int I32)]). Defined.
+
+ Definition UnsafeCell_rt : Type.
+ Proof using . let __a := eval hnf in (rt_of UnsafeCell_ty) in exact __a. Defined.
+
+ Global Typeclasses Transparent UnsafeCell_ty.
+ Global Typeclasses Transparent UnsafeCell_rt.
+End UnsafeCell_ty.
+Global Arguments UnsafeCell_rt : clear implicits.
+
+Section UnsafeCell_inv_t.
+ Context `{!refinedrustGS Σ}.
+
+ Program Definition UnsafeCell_inv_t_inv_spec : na_ex_inv_def (UnsafeCell_rt) (Z) :=
+ na_mk_ex_inv_def
+ ((Z)%type)
+ (xmap)
+ (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌠∗ ⌜Zeven x⌠∗ True)%I
+ [] [].
+
+ Definition UnsafeCell_inv_t : type (Z) :=
+ na_ex_plain_t _ _ UnsafeCell_inv_t_inv_spec UnsafeCell_ty.
+
+ Definition UnsafeCell_inv_t_rt : Type.
+ Proof using. let __a := eval hnf in (rt_of UnsafeCell_inv_t) in exact __a. Defined.
+
+ Global Typeclasses Transparent UnsafeCell_inv_t.
+ Global Typeclasses Transparent UnsafeCell_inv_t_rt.
+End UnsafeCell_inv_t.
+Global Arguments UnsafeCell_inv_t_rt : clear implicits.
+
+Section Cell_ty.
+ Context `{!refinedrustGS Σ}.
+
+ Definition Cell_ty : type (plist place_rfn [UnsafeCell_inv_t_rt : Type]).
+ Proof using Type*. exact (struct_t Cell_sls +[UnsafeCell_inv_t]). Defined.
+ Definition Cell_rt : Type.
+ Proof using . let __a := eval hnf in (rt_of Cell_ty) in exact __a. Defined.
+
+ Global Typeclasses Transparent Cell_ty.
+ Global Typeclasses Transparent Cell_rt.
+End Cell_ty.
+Global Arguments Cell_rt : clear implicits.
+
+Section Cell_inv_t.
+ Context `{!refinedrustGS Σ}.
+
+ Program Definition Cell_inv_t_inv_spec : na_ex_inv_def (Cell_rt) (Z) :=
+ na_mk_ex_inv_def
+ ((Z)%type)
+ (xmap)
+ (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌠∗ ⌜Zeven x⌠∗ True)%I
+ [] [].
+
+ Definition Cell_inv_t : type (Z) :=
+ na_ex_plain_t _ _ Cell_inv_t_inv_spec Cell_ty.
+
+ Definition Cell_inv_t_rt : Type.
+ Proof using . let __a := eval hnf in (rt_of Cell_inv_t) in exact __a. Defined.
+
+ Global Typeclasses Transparent Cell_inv_t.
+ Global Typeclasses Transparent Cell_inv_t_rt.
+End Cell_inv_t.
+Global Arguments Cell_inv_t_rt : clear implicits.
+
+Section specs.
+ Context `{RRGS: !refinedrustGS Σ}.
+
+ Definition type_of_UnsafeCell_new :=
+ fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ Ï, []); x :@: (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)))
+ → ∃ _ : unit, x @ UnsafeCell_inv_t; (λ π : thread_id, True).
+
+ Definition type_of_UnsafeCell_into_inner :=
+ fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ Ï, []); x :@: UnsafeCell_inv_t; (λ Ï€ : thread_id, True))
+ → ∃ _ : unit, x @ (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)).
+
+ Definition type_of_UnsafeCell_get_old :=
+ fn(∀ ( *[ulft_1]) : 1 | ( *[]) : ([]) | (x) : (_), (λ Ï, []); x :@: (shr_ref ulft_1 UnsafeCell_inv_t); (λ Ï€ : thread_id, True))
+ → ∃ _ : unit, x @ (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)).
+
+ Definition type_of_Cell_new :=
+ fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (Z), (λ Ï, []); x :@: (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)))
+ → ∃ _ : unit, x @ Cell_inv_t; (λ π : thread_id, True).
+
+ Definition type_of_Cell_into_inner :=
+ fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (_), (λ Ï, []); x :@: Cell_inv_t; (λ Ï€ : thread_id, True))
+ → ∃ _ : unit, x @ (int I32); (λ Ï€ : thread_id, (⌜Zeven xâŒ)).
+End specs.
+
+Section proof.
+ Context `{RRGS: !refinedrustGS Σ}.
+
+ Definition UnsafeCell_new_lemma (Ï€ : thread_id) : Prop :=
+ syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
+ ⊢ typed_function π (UnsafeCell_new_def ) [UnsafeCell_st; IntSynType I32] (<tag_type> type_of_UnsafeCell_new ).
+
+ Definition UnsafeCell_into_inner_lemma (Ï€ : thread_id) : Prop :=
+ syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
+ ⊢ typed_function π (UnsafeCell_into_inner_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_into_inner ).
+
+ Definition UnsafeCell_get_old_lemma (Ï€ : thread_id) : Prop :=
+ syn_type_is_layoutable (Cell_st) →
+ ⊢ typed_function π (UnsafeCell_get_old_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_get_old ).
+
+ Definition Cell_new_lemma (Ï€ : thread_id) : Prop :=
+ ∀ (UnsafeCell_new_loc : loc) ,
+ syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
+ syn_type_is_layoutable ((Cell_sls : syn_type)) →
+ UnsafeCell_new_loc â—áµ¥{Ï€} UnsafeCell_new_loc @ function_ptr [IntSynType I32] (<tag_type> spec! ( *[]) : 0 | ( *[]) : ([]), type_of_UnsafeCell_new (RRGS := RRGS) <MERGE!>) -∗
+ typed_function π (Cell_new_def UnsafeCell_new_loc ) [Cell_st; UnsafeCell_st; IntSynType I32] (<tag_type> type_of_Cell_new ).
+End proof.
+
+Ltac UnsafeCell_new_prelude :=
+ unfold UnsafeCell_new_lemma;
+ set (FN_NAME := FUNCTION_NAME "UnsafeCell_new");
+ intros;
+ iStartProof;
+ let Ï := fresh "Ï" in
+ start_function "UnsafeCell_new" Ï ( [] ) ( [] ) ( x ) ( x );
+ set (loop_map := BB_INV_MAP (PolyNil));
+ intros arg_value local___0 local___2;
+ init_lfts (named_lft_update "_flft" Ï $ ∅ );
+ init_tyvars ( ∅ ).
+
+Ltac UnsafeCell_into_inner_prelude :=
+ unfold UnsafeCell_into_inner_lemma;
+ set (FN_NAME := FUNCTION_NAME "UnsafeCell_into_inner");
+ intros;
+ iStartProof;
+ let Ï := fresh "Ï" in
+ start_function "UnsafeCell_into_inner" Ï ( [] ) ( [] ) ( x ) ( x );
+ set (loop_map := BB_INV_MAP (PolyNil));
+ intros arg_self local___0;
+ init_lfts (named_lft_update "_flft" Ï $ ∅ );
+ init_tyvars ( ∅ ).
+
+Ltac UnsafeCell_get_old_prelude :=
+ unfold UnsafeCell_get_old_lemma;
+ set (FN_NAME := FUNCTION_NAME "Cell_get");
+ intros;
+ iStartProof;
+ let Ï := fresh "Ï" in
+ let ulft__ := fresh "ulft__" in
+ start_function "UnsafeCell_get_old" Ï ( [ ulft__ [] ] ) ( [] ) ( x ) ( x );
+ set (loop_map := BB_INV_MAP (PolyNil));
+ intros arg_self local___0;
+ init_lfts (named_lft_update "ulft__" ulft__ $ named_lft_update "_flft" Ï $ ∅ );
+ init_tyvars ( ∅ ).
+
+Ltac Cell_new_prelude :=
+ unfold Cell_new_lemma;
+ set (FN_NAME := FUNCTION_NAME "Cell_new");
+ intros;
+ iStartProof;
+ let Ï := fresh "Ï" in
+ start_function "Cell_T_new" Ï ( [] ) ( [] ) ( x ) ( x );
+ set (loop_map := BB_INV_MAP (PolyNil));
+ intros arg_value local___0 local___2 local___3;
+ init_lfts (named_lft_update "_flft" Ï $ ∅ );
+ init_tyvars ( ∅ ).
+
+Section proof.
+ Context `{!refinedrustGS Σ}.
+
+ Lemma UnsafeCell_new_proof (Ï€ : thread_id) :
+ UnsafeCell_new_lemma π.
+ Proof.
+ UnsafeCell_new_prelude.
+
+ repeat liRStep; liShow.
+
+ all: print_remaining_goal.
+ Unshelve. all: sidecond_solver.
+ Unshelve. all: sidecond_hammer.
+ Unshelve. all: print_remaining_sidecond.
+ Qed.
+
+ Lemma UnsafeCell_into_inner_proof (Ï€ : thread_id) :
+ UnsafeCell_into_inner_lemma π.
+ Proof.
+ UnsafeCell_into_inner_prelude.
+
+ repeat liRStep; liShow.
+
+ all: print_remaining_goal.
+ Unshelve. all: sidecond_solver.
+ Unshelve. all: sidecond_hammer.
+ Unshelve. all: print_remaining_sidecond.
+ Qed.
+
+ Lemma Cell_new_proof (Ï€ : thread_id) :
+ Cell_new_lemma π.
+ Proof.
+ Cell_new_prelude.
+
+ repeat liRStep; liShow.
+
+ all: print_remaining_goal.
+ Unshelve. all: sidecond_solver.
+ Unshelve. all: sidecond_hammer.
+ Unshelve. all: print_remaining_sidecond.
+ Qed.
+
+ Lemma UnsafeCell_get_old_proof (Ï€ : thread_id) :
+ UnsafeCell_get_old_lemma π.
+ Proof.
+ UnsafeCell_get_old_prelude.
+
+ do 324 liRStep; liShow.
+
+ (* TODO: This instance isn't properly found *)
+ iApply stratify_ltype_shadowed_shared.
+
+ repeat liRStep; liShow.
+
+ Unshelve. all: sidecond_solver.
+ Unshelve. all: sidecond_hammer.
+ Unshelve. all: print_remaining_sidecond.
+ Qed.
+End proof.