diff --git a/theories/rust_typing/existentials_na.v b/theories/rust_typing/existentials_na.v
index eb2234ee03c8da15e448f06398c77a4f349b0744..8c4df67d3fadfdacda04d40fef4b386d4c6c6d48 100644
--- a/theories/rust_typing/existentials_na.v
+++ b/theories/rust_typing/existentials_na.v
@@ -185,7 +185,6 @@ Section na_ex.
iApply fupd_logical_step; iApply logical_step_intro.
- (* NOTE: Is there a simplier setoid_rewrite to do here ? *)
iPoseProof (bor_iff _ _ (∃ x: X, l ↦: ty_own_val ty π x ∗ P.(na_inv_P) π x r) with "[] Hbor") as "Hbor".
{ iNext. iModIntro. iSplit; [iIntros "(% & % & ? & ? & ?)" | iIntros "(% & (% & ? & ?) & ?)"]; eauto with iFrame. }
@@ -250,7 +249,6 @@ Section generated_code.
Section UnsafeCell_sls.
Context `{!refinedrustGS Σ}.
- (* NOTE: Is StructReprTransparent ready? *)
Definition UnsafeCell_sls : struct_layout_spec := mk_sls "UnsafeCell" [
("value", IntSynType I32)] StructReprTransparent.
Definition UnsafeCell_st : syn_type := UnsafeCell_sls.
@@ -817,7 +815,7 @@ Section generated_code.
iDestruct 1 as ([Ï€' mask]) "(Hna & <- & % & HT) /=".
rewrite /typed_place /introduce_with_hooks.
- iIntros (Φ ???) "#(LFT & TIME & LLCTX) #HE HL ? Hl Hcont". (* NOTE: Hincl is not used. *)
+ iIntros (Φ ???) "#(LFT & TIME & LLCTX) #HE HL ? Hl Hcont".
rewrite /prove_with_subtype.
iApply fupd_place_to_wp.
@@ -896,7 +894,6 @@ Section generated_code.
(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)
- (* NOTE: Weak has been skipped here *)
None))
⊢ typed_place π E L l (AliasLtype rt''' st l2) r bmin0 (Shared κ) P''' T.
Proof.
@@ -914,7 +911,6 @@ Section generated_code.
iSplit; last done.
- (* strong *)
destruct strong as [ strong |]; last done.
iDestruct "Hcl" as "[Hcl _]"; simpl.
@@ -940,7 +936,7 @@ Section generated_code.
Lemma stratify_ltype_magic_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 wl (T : stratify_ltype_cont_t) :
+ (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)
@@ -948,12 +944,12 @@ Section generated_code.
T L' R _ (MagicLtype 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 and then fold to lt_full *)
- weak_subltype E L' (Owned false) (r') (#ri) (ltype_core lt_cur') lt_inner (
+ (* 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 (◠(uninit (ltype_st lt_inner))) #tt)))
- ⊢ stratify_ltype π E L mu mdu ma ml l (MagicLtype lt_cur lt_inner Cpre Cpost) r (Owned wl) T.
+ (λ 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 (MagicLtype lt_cur lt_inner Cpre Cpost) r (Owned false) T.
Proof.
rewrite /stratify_ltype /weak_subltype /prove_with_subtype.
@@ -966,8 +962,7 @@ Section generated_code.
destruct (decide (ma = StratNoRefold)) as [-> | ].
- (* don't fold *)
iModIntro.
- iExists _, _, _, _, _.
- iFrame; iR.
+ iExists _, _, _, _, _; iFrame; iR.
iApply (logical_step_compose with "Hstep").
iApply logical_step_intro.
@@ -983,49 +978,30 @@ Section generated_code.
iMod ("HT" with "[//] CTX HE HL") as "(Hincl & HL & HT)".
iMod ("HT" with "[//] [//] [//] CTX HE HL") as "(%L3 & %κs & %R2 & Hstep' & HL & HT)".
- iPoseProof (imp_unblockable_blocked_dead lt_cur') as "(_ & #Hb)".
- set (κs' := ltype_blocked_lfts lt_cur').
+ iExists L3, _, _, _, _; iFrame.
+ iSplitR.
+ { by simp_ltypes. }
- destruct (decide (κs = [] ∧ κs' = [])) as [[-> ->] | ].
- + 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 & $)".
- iPoseProof ("Hb" with "[] Hl") as "Hl".
- { by iApply big_sepL_nil. }
-
- iMod (fupd_mask_mono with "Hl") as "Hl"; first done.
- rewrite ltype_own_core_equiv.
- iMod (ltype_incl_use with "Hincl Hl") as "Hl"; first done.
-
- iPoseProof ("Hcl" with "Hpre Hl") as "Hvs".
- admit.
+ 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.
- + (* iAssert (T L3 (Cpost ri ∗ R2 ∗ R) rt_cur (CoreableLtype (κs' ++ κs) lt_cur) #rf)%I with "[HT]" as "HT". *)
- (* { destruct κs, κs'; naive_solver. } *)
+ iIntros "!> (Hpre & $) Hcl (Hl & $)".
+ iMod (ltype_incl_use with "Hincl Hl") as "Hl"; first done.
- iExists L3, _, _, _, _. iFrame.
- iSplitR.
- { by simp_ltypes. }
+ iPoseProof ("Hcl" with "Hpre Hl") as "Hvs".
+ iSplitL "".
+ { rewrite ltype_own_alias_unfold /alias_lty_own.
+ rewrite -Hst.
- iApply logical_step_fupd.
- iApply (logical_step_compose with "Hstep").
- iPoseProof (logical_step_mask_mono _ F with "Hcl") as "Hcl"; first done.
- iApply (logical_step_compose with "Hcl").
- iApply (logical_step_compose with "Hstep'").
- iApply logical_step_intro.
+ by iExists ly; repeat iR. }
- iIntros "!> (Hpre & $) Hcl (Hl & $)".
- iPoseProof ("Hcl" with "Hpre") as "Hvs".
- Admitted.
+ iMod (fupd_mask_mono with "Hvs") as "Hvs"; first set_solver.
+ done.
+ Qed.
End na_subtype.
@@ -1130,7 +1106,6 @@ Section generated_code.
do 7 liRStep.
do 100 liRStep; liShow.
- (* NOTE: How do we catch up? *)
replace [arg_self; local___0] with [arg_self; local___0; l']; last admit.
rep <- 1 liRStep; liShow.