diff --git a/theories/rust_typing/existentials_na.v b/theories/rust_typing/existentials_na.v index c1cba8fa34d504bd15616110018d8b88884cfc8c..fa0815f6fd7a56452934cdfa43c5da8b1ec7b59b 100644 --- a/theories/rust_typing/existentials_na.v +++ b/theories/rust_typing/existentials_na.v @@ -176,7 +176,8 @@ Section na_ex. iMod (bor_persistent with "LFT HP Htok") as "(>HP & Htok)"; first solve_ndisj. iMod (bor_get_persistent _ (ty_sidecond ty) with "LFT [] Hb Htok") as "(Hty & Hb & Htok)"; first solve_ndisj. - { iIntros "Hv". + { iIntros "$ !> !>". + iApply ty_own_val_sidecond. (* NOTE: Use ty_own_val_sidecond *) admit. } @@ -397,7 +398,7 @@ Section generated_code. iStartProof; let Ï := fresh "Ï" in let ulft__ := fresh "ulft__" in - start_function "Cell_get" Ï ( [ [] ulft__] ) ( [ [] ulft__] ) ( x ) ( x ); + start_function "Cell_get" Ï ( [ ulft__ [] ] ) ( [] ) ( x ) ( x ); set (loop_map := BB_INV_MAP (PolyNil)); intros arg_self local___0; init_lfts (named_lft_update "ulft__" ulft__ $ ∅ ); @@ -507,6 +508,70 @@ Section generated_code. simp_ltypes. done. Qed. + Lemma na_ex_plain_t_open_shared F Ï€ (ty : type rt) q κ l (x : X) : + lftE ⊆ F → + ↑shrN.@l ⊆ F → + + na_own Ï€ ⊤ -∗ + q.[κ] -∗ + l â—â‚—[Ï€, Shared κ] (#x) @ (â— (∃na; P, ty)) ={F}=∗ + + ∃ r : rt, P.(na_inv_P) Ï€ r x ∗ + â–· (l â—â‚—[Ï€, Owned false] PlaceIn r @ (â— ty)) ∗ + + (* (∀ (r' : place_rfn rt), *) + ( l â—â‚—[Ï€, Owned false] (#r) @ (â— ty) ={F}=∗ + q.[κ] ∗ na_own Ï€ ⊤ ). + (* TODO: Closing view-shift here. *) + Proof. + iIntros (??) "Hna Hq #Hb". + + iEval (rewrite ltype_own_ofty_unfold) in "Hb". + iDestruct "Hb" as "(%ly & %Halg & %Hly & Hsc & Hlb & %v & -> & #Hb)". + + (* iMod (maybe_use_credit with "Hcred Hb") as "(Hcred & Hat & Hb)"; first done. *) + + 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 "(%r & HP & Hscr & Hr & % & ? & %Halg')". + + iMod (na_bor_acc with "[] [$] [$] [$]") as "(Hl & Hna & Hcont)". + 1-3: solve_ndisj. + { admit. } + + iModIntro. + iExists r. + iSplitR; first done. + + iSplitL "Hl". + { rewrite !ltype_own_ofty_unfold /lty_of_ty_own. + iExists ly. iFrame (Halg Hly) "Hlb Hscr". + iSplitR. + { admit. } + iExists r. iR. + iModIntro. + done. } + + iIntros "Hb". + iEval (rewrite ltype_own_ofty_unfold) in "Hb". + iDestruct "Hb" as "(% & %Halg'' & ? & _ & ? & _ & (% & -> & Hb)) /=". + + (* iAssert (⌜ly0 = ly1âŒ)%I as "<-". *) + (* { iPureIntro; by eapply syn_type_has_layout_inj. } *) + + iMod (fupd_mask_mono with "Hb") as "Hb"; first done. + iApply ("Hcont" with "[$] [$]"). + Admitted. + + Lemma na_typed_place_ex_plain_t_shared Ï€ E L l (ty : type rt) x κ bmin K T : + (∀ r, introduce_with_hooks E L (P.(na_inv_P) Ï€ r x) + (λ L2, typed_place Ï€ E L2 l + (ShadowedLtype (â— ty) #r (â— (∃na; P, ty))) + (#x) bmin (Shared κ) K T)) + ⊢ typed_place Ï€ E L l (â— (∃na; P, ty))%I (#x) bmin (Shared κ) K T. + Proof. + Admitted. End na_subtype. Section proof. @@ -548,23 +613,23 @@ Section generated_code. Unshelve. all: print_remaining_sidecond. Qed. - (* Lemma Cell_get_proof (Ï€ : thread_id) : *) - (* Cell_get_lemma Ï€. *) - (* Proof. *) - (* Cell_get_prelude. *) + Lemma Cell_get_proof (Ï€ : thread_id) : + Cell_get_lemma Ï€. + Proof. + Cell_get_prelude. - (* repeat liRStep; liShow. *) + repeat liRStep; liShow. - (* iApply na_typed_place_ex_plain_t_shared. *) - (* liSimpl; liShow. *) + iApply na_typed_place_ex_plain_t_shared. + liSimpl; liShow. - (* repeat liRStep; liShow. *) + repeat liRStep; liShow. - (* all: print_remaining_goal. *) - (* Unshelve. all: sidecond_solver. *) - (* Unshelve. all: sidecond_hammer. *) - (* Unshelve. all: print_remaining_sidecond. *) - (* Qed. *) + all: print_remaining_goal. + Unshelve. all: sidecond_solver. + Unshelve. all: sidecond_hammer. + Unshelve. all: print_remaining_sidecond. + Qed. End proof.