Skip to content

Commits on Source 22

......@@ -13,3 +13,4 @@ build-dep/
Makefile.coq
Makefile.coq.conf
.coqdeps.d
_opam
......@@ -35,10 +35,6 @@ build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
TIMING_PROJECT: "lambda-rust"
TIMING_CONF: "coq-8.7.2"
tags:
- fp-timing
build-coq.dev:
<<: *template
......
Missing APIs from the types we cover (APIs have been added after this formalization was done)
# Cell
* Structural conversion for slices. The matching operations in our model would be
`&mut Cell<(A, B)>` -> `(&mut Cell<A>, &mut Cell<B>)` and
`&Cell<(A, B)>` -> `(&Cell<A>, &Cell<B>)`.
# RefCell
* RefMut::split: https://github.com/rust-lang/rust/pull/51466
......@@ -46,26 +46,25 @@ theories/typing/cont.v
theories/typing/function.v
theories/typing/typing.v
theories/typing/soundness.v
theories/typing/lib/cell.v
theories/typing/lib/diverging_static.v
theories/typing/lib/fake_shared.v
theories/typing/lib/option.v
theories/typing/lib/panic.v
theories/typing/lib/swap.v
theories/typing/lib/take_mut.v
theories/typing/lib/option.v
theories/typing/lib/fake_shared.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
theories/typing/lib/join.v
theories/typing/lib/diverging_static.v
theories/typing/lib/take_mut.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/arc.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/refcell/refcell_code.v
theories/typing/lib/refcell/refcell.v
theories/typing/lib/refcell/ref.v
theories/typing/lib/refcell/refmut.v
theories/typing/lib/refcell/refcell_code.v
theories/typing/lib/refcell/ref_code.v
theories/typing/lib/refcell/refmut_code.v
theories/typing/lib/refcell/refmut.v
theories/typing/lib/refcell/ref.v
theories/typing/lib/rwlock/rwlock.v
theories/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard.v
......
......@@ -47,7 +47,8 @@ Module Type lifetime_sig.
End defs.
(** Notation *)
Notation "q .[ κ ]" := (lft_tok q κ) (format "q .[ κ ]", at level 0) : bi_scope.
Notation "q .[ κ ]" := (lft_tok q κ)
(format "q .[ κ ]", at level 0) : bi_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
......
From lrust.lifetime Require Export primitive.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.bi Require Import big_op.
Set Default Proof Using "Type".
Section accessors.
......
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
......
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking reborrow.
From iris.algebra Require Import csum auth frac gmap agree.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
......
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Import faking.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
......
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.bi Require Import big_op.
From lrust.lifetime.model Require Import boxes.
From lrust.lifetime Require Export lifetime_sig.
From gpfsl.lang Require Export lattice_cmra.
......
From lrust.lifetime.model Require Export primitive.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
......
......@@ -76,9 +76,6 @@ Qed.
Global Instance own_bor_into_sep κ x x1 x2 :
IsOp x x1 x2 IntoSep (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
Proof. rewrite /IsOp /IntoSep=>->. by rewrite own_bor_op. Qed.
Global Instance own_bor_into_and κ x x1 x2 p :
IsOp x x1 x2 IntoAnd p (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
Proof. rewrite /IsOp /IntoAnd=>->. by rewrite own_bor_op sep_and. Qed.
Lemma own_bor_valid κ x : own_bor κ x -∗ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ (x y).
......@@ -110,11 +107,8 @@ Proof.
Qed.
Global Instance own_cnt_into_sep κ x x1 x2 :
IsOp x x1 x2 IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
Proof. rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op. Qed.
Global Instance own_cnt_into_and κ x x1 x2 p :
IsOp x x1 x2 IntoAnd p (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
Proof.
rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite own_cnt_op sep_and.
rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
Qed.
Lemma own_cnt_valid κ x : own_cnt κ x -∗ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
......@@ -147,11 +141,8 @@ Proof.
Qed.
Global Instance own_inh_into_sep κ x x1 x2 :
IsOp x x1 x2 IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
Proof. rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op. Qed.
Global Instance own_inh_into_and κ x x1 x2 p :
IsOp x x1 x2 IntoAnd p (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
Proof.
rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite own_inh_op sep_and.
rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
Qed.
Lemma own_inh_valid κ x : own_inh κ x -∗ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
......
From lrust.lifetime Require Import borrow accessors.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
......
......@@ -407,7 +407,7 @@ Section typing.
(subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn fp).
Proof.
iIntros (<- ->) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
iIntros (<- ->) "#Hbody /=". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ unlock. rewrite /= decide_left. done. }
iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
......
From iris.proofmode Require Import tactics.
From iris.bi Require Import big_op.
From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
......
......@@ -25,7 +25,7 @@ Section fake_shared.
{ iApply frac_bor_iff; last done. iIntros "!>!# *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
by iApply ty_shr_mono. }
simpl. by iApply ty_shr_mono. }
do 2 wp_seq.
iApply (type_type [] _ _ [ x box (&shr{α}(box ty)) ]
with "[] LFT [] Hna HL Hk [HT]"); last first.
......
From iris.proofmode Require Import tactics.
From iris.bi Require Import big_op.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
......
......@@ -202,8 +202,8 @@ Section code.
delete [ #1; "g"];; return: ["r"].
Lemma mutexguard_derefmut_type ty `{!TyWf ty} :
typed_val mutexguard_derefmut (fn (fun '(α, β) =>
FP_wf [# &uniq{α}(mutexguard β ty)]%T (&uniq{α}ty)%T)).
typed_val mutexguard_derefmut
(fn( '(α, β), ; &uniq{α}(mutexguard β ty)) &uniq{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
......@@ -244,8 +244,8 @@ Section code.
Definition mutexguard_deref : val := mutexguard_derefmut.
Lemma mutexguard_deref_type ty `{!TyWf ty} :
typed_val mutexguard_derefmut (fn (fun '(α, β) =>
FP_wf [# &shr{α}(mutexguard β ty)]%T (&shr{α}ty)%T)).
typed_val mutexguard_derefmut
(fn( '(α, β), ; &shr{α}(mutexguard β ty)) &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
......
......@@ -25,7 +25,7 @@ Section ref.
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
ν q γ β ty', ty.(ty_shr) (α ν) tid lv
α β &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty')
q.[ν] own γ ( reading_st q ν)
q.[ν] own γ ( reading_stR q ν)
| _ => False
end;
ty_shr κ tid l :=
......@@ -33,7 +33,7 @@ Section ref.
κ ν &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc])
ty.(ty_shr) (α ν) tid lv
(α β) &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty')
&na{κ, tid, refcell_refN}own γ ( reading_st q ν) |}%I.
&na{κ, tid, refcell_refN}own γ ( reading_stR q ν) |}%I.
Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
......
......@@ -11,34 +11,27 @@ Section ref_functions.
Lemma refcell_inv_reading_inv tid l γ α ty q ν :
refcell_inv tid l γ α ty -∗
own γ ( reading_st q ν) -∗
own γ ( reading_stR q ν) -∗
(q' : Qp) n, l #(Zpos n) (q q')%Qc
own γ ( Some (to_agree ν, Cinr (q', n)) reading_st q ν)
ty.(ty_shr) (α ν) tid (l + 1)
own γ ( (refcell_st_to_R $ Some (ν, false, q', n)) reading_stR q ν)
((1).[ν] ={lftN histN,histN}▷=∗ &{α}((l + 1) ↦∗: ty_own ty tid))
q'', (q' + q'' = 1)%Qp q''.[ν].
( q'', (q' + q'' = 1)%Qp q''.[ν])
ty.(ty_shr) (α ν) tid (l + 1).
Proof.
iIntros "INV H◯".
iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
iAssert ( q' n, st Some (to_agree ν, Cinr (q', n)) q q'⌝%Qc)%I with
"[#]" as (q' n) "[Hst %]".
{ iDestruct (own_valid_2 with "H● H◯") as %[[[=]|
(? & [agν st'] & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
- iExists q, xH. iSplit; iPureIntro. by constructor. done.
- iClear "∗#".
revert Hle Hv=>/prod_included [/= /agree_included Hag /csum_included
[-> [//] | [[?[?[//]]] | [?[[q' n] [Heq [-> Hle]]]]]]] [Hagok _].
revert Heq. intros [= <-]. revert Hle=>/prod_included [/= Hqq' _].
iExists q', n. iSplit.
+ iPureIntro. rewrite (agree_op_inv agν) //. by rewrite comm -Hag.
+ by revert Hqq'=>/frac_included_weak. }
iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
destruct st' as [?[|[]|]]; destruct Hst' as [Hag Hst']; try by inversion Hst'.
apply (inj Cinr), (inj2 pair) in Hst'.
destruct Hst' as [<-%leibniz_equiv <-%leibniz_equiv]. simpl in *.
setoid_rewrite <-Hag. iDestruct "INV" as (ν') "(Hag & Hν & Hshr & Hq')".
iDestruct "Hag" as %<-%(inj to_agree)%leibniz_equiv.
iExists q', n. rewrite own_op. by iFrame.
iAssert ( q' n, st Some (ν, false, q', n) q q'⌝%Qc)%I with
"[#]" as (q' n) "[%%]".
{ destruct st as [[[[??]?]?]|];
iDestruct (own_valid_2 with "H● H◯")
as %[[[=]|(?&[[? q'] n]&[=<-]&[=]&[[[Eq_ag ?%leibniz_equiv]_]|Hle])]
%option_included Hv]%auth_valid_discrete_2; simpl in *; subst.
- apply (inj to_agree), (inj2 pair) in Eq_ag.
destruct Eq_ag. setoid_subst. eauto.
- revert Hle=> /prod_included [/= /prod_included
[/= /to_agree_included [/= ??] /frac_included_weak ?] _].
setoid_subst. eauto. }
setoid_subst. iExists q', n. rewrite own_op. by iFrame.
Qed.
(* Cloning a ref. We need to increment the counter. *)
......@@ -51,11 +44,9 @@ Section ref_functions.
letalloc: "r" <-{2} !"x'" in
delete [ #1; "x"];; return: ["r"].
(* FIXME : using λ instead of fun triggers an anomaly.
See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
Lemma ref_clone_type ty `{!TyWf ty} :
typed_val ref_clone (fn (fun '(α, β) =>
FP_wf [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
typed_val ref_clone (fn( '(α, β), ; &shr{α}(ref β ty)) ref β ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
......@@ -75,12 +66,12 @@ Section ref_functions.
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iDestruct (refcell_inv_reading_inv with "INV H◯")
as (q' n) "(H↦lrc & _ & [H● H◯] & Hshr' & H & Hq')".
as (q' n) "(H↦lrc & _ & [H● H◯] & H & Hq' & Hshr')".
wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
split; [|split; last done].
(op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
......@@ -91,9 +82,8 @@ Section ref_functions.
wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
{ iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
- rewrite /= agree_idemp. auto.
- iExists _. iFrame.
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op !pair_op agree_idemp.
iFrame. iExists _. iFrame.
rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
......@@ -117,7 +107,7 @@ Section ref_functions.
Lemma ref_deref_type ty `{!TyWf ty} :
typed_val ref_deref
(fn (fun '(α, β) => FP_wf [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
(fn( '(α, β), ; &shr{α}(ref β ty)) &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
......@@ -167,27 +157,27 @@ Section ref_functions.
iMod (lft_incl_acc with "Hαβ Hα") as () "[Hβ Hcloseα]". done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct (refcell_inv_reading_inv with "INV [$H◯]")
as (q' n) "(H↦lrc & >% & H●◯ & Hshr & H† & Hq')". iDestruct "Hq'" as (q'') ">[% Hν']".
as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)".
iDestruct "Hq'" as (q'') ">[% Hν']".
wp_read. wp_let. wp_op. wp_write.
iAssert (|={lftN histN,histN}▷=> refcell_inv tid lrc γ β ty')%I
with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
{ iDestruct (own_valid with "H●◯") as %[[ _ [Heq%(inj Cinr)|Hincl%csum_included]
%Some_included]%Some_pair_included [_ Hv]]%auth_valid_discrete_2.
- destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
{ iDestruct (own_valid with "H●◯") as
%[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
%Some_included _]%auth_valid_discrete_2.
- simpl in *. setoid_subst.
iExists None. iFrame. iMod (own_update with "H●◯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
apply cancel_local_update_unit, _. }
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
iAssert (lrc #(Z.pos n'))%I with "[H↦lrc]" as "H↦lrc".
- simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
iAssert (lrc #(Z.pos n'))%I with "[H↦lrc]" as "$".
{ destruct n'; [|done..]. by rewrite /= Pos.pred_double_succ. }
iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
iMod (own_update with "H●◯") as "$".
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
apply (cancel_local_update_unit (reading_st q ν)), _. }
iExists ν. iFrame. iApply step_fupd_intro; first set_solver. iIntros "!>".
iSplitR; first done. iExists (q+q'')%Qp. iFrame.
rewrite -(agree_idemp (to_agree _)) -!pair_op Some_op.
apply (cancel_local_update_unit (reading_stR q ν)), _. }
iApply step_fupd_intro; first set_solver. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
wp_bind Endlft. iApply (wp_mask_mono _ (lftN histN)); first done.
iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
......@@ -259,4 +249,115 @@ Section ref_functions.
iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
iApply type_jump; solve_typing.
Qed.
(* Apply a function within the ref, and create two ref,
typically for splitting the reference. *)
Definition ref_map_split (call_once : val) : val :=
funrec: <> ["ref"; "f"] :=
let: "call_once" := call_once in
let: "x'" := !"ref" in
letalloc: "x" <- "x'" in
letcall: "r" := "call_once" ["f"; "x"]%E in
let: "a" := !"r" in
let: "b" := !("r" + #1) in
delete [ #2; "r"];;
let: "rc" := !("ref" + #1) in
let: "n" := !"rc" in
"rc" <- "n" + #1;;
delete [ #2; "ref"];;
let: "refs" := new [ #4 ] in
"refs" <- "a";;
"refs" + #1 <- "rc";;
"refs" + #2 <- "b";;
"refs" + #3 <- "rc";;
return: ["refs"].
Lemma ref_map_split_type ty ty1 ty2 call_once fty
`{!TyWf ty, !TyWf ty1, !TyWf ty2, !TyWf fty} :
(* fty : for<'a>, FnOnce(&'a ty) -> (&'a ty1, &'a ty2),
as witnessed by the impl call_once *)
typed_val call_once
(fn( α, ; fty, &shr{α}ty) Π[&shr{α}ty1; &shr{α}ty2])
typed_val (ref_map_split call_once)
(fn( α, ; ref α ty, fty) Π[ref α ty1; ref α ty2]).
Proof.
intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
inv_vec arg=>ref env. simpl_subst.
iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
iDestruct "Href" as "[Href Href†]".
iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
try iDestruct "Href" as "[_ >[]]".
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
wp_read. wp_let. wp_apply wp_new; [done..|].
iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
rewrite -[ϝ in (α ν) ϝ](right_id_L static ()).
iApply (type_call_iris _ [α ν; ϝ] (α ν) [_; _]
with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
iMod ("Hclose2" with "Hϝ HL") as "HL".
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[#Hr1' H]".
iDestruct "H" as (vl2 ? ->) "[#Hr2' ->]".
destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Hr1 Hr2 Hr†]")=>//.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct (refcell_inv_reading_inv with "INV Hγ")
as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefs) "[Hrefs† Hrefs]".
rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
iMod ("Hclosena" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op !pair_op agree_idemp.
iFrame. iExists _. iFrame.
rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefs box (Π[ref α ty1; ref α ty2]) ]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //= -freeable_sz_full.
iFrame. iExists [_;_;_;_].
rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton !shift_loc_assoc.
iFrame. iExists [_;_], [_;_]. iSplit=>//=.
iSplitL "Hν H◯"; [by auto 10 with iFrame|]. iExists [_;_], [].
iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
iApply type_jump; solve_typing.
Qed.
End ref_functions.