Skip to content
Snippets Groups Projects
Commit a9ab999a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Type unbox.

parent 6f46c73c
No related branches found
No related tags found
No related merge requests found
......@@ -46,11 +46,12 @@ Section borrow.
apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
Qed.
Lemma type_deref_uniq_own {E L} κ p n ty :
Lemma type_deref_uniq_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ
typed_instruction_ty E L [p &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
Proof.
iIntros () "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iIntros () "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod ( with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
......@@ -69,11 +70,22 @@ Section borrow.
rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
Qed.
Lemma type_deref_shr_own {E L} κ p n ty :
Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
Closed (x :b: []) e
tctx_extract_hasty E L p (&uniq{κ} own n ty) T T'
lctx_lft_alive E L κ
( (v:val), typed_body E L C ((v &uniq{κ} ty) :: T') (subst' x v e))
typed_body E L C T (let: x := !p in e).
Proof.
intros. eapply type_let; [done|by apply type_deref_uniq_own_instr|solve_typing|done].
Qed.
Lemma type_deref_shr_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ
typed_instruction_ty E L [p &shr{κ} own n ty] (!p) (&shr{κ} ty).
Proof.
iIntros () "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iIntros () "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod ( with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
......@@ -81,16 +93,28 @@ Section borrow.
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "* [%] Htok2"). set_solver+.
- wp_read. iIntros "!>[#Hshr Htok2]". iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
- wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _. auto.
Qed.
Lemma type_deref_uniq_uniq {E L} κ κ' p ty :
Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
Closed (x :b: []) e
tctx_extract_hasty E L p (&shr{κ} own n ty) T T'
lctx_lft_alive E L κ
( (v:val), typed_body E L C ((v &shr{κ} ty) :: T') (subst' x v e))
typed_body E L C T (let: x := !p in e).
Proof.
intros. eapply type_let; [done|by apply type_deref_shr_own_instr|solve_typing|done].
Qed.
Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ lctx_lft_incl E L κ κ'
typed_instruction_ty E L [p &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
Proof.
iIntros ( Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iIntros ( Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod ( with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
......@@ -116,7 +140,17 @@ Section borrow.
iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' p ty :
Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
Closed (x :b: []) e
tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T'
lctx_lft_alive E L κ lctx_lft_incl E L κ κ'
( (v:val), typed_body E L C ((v &uniq{κ} ty) :: T') (subst' x v e))
typed_body E L C T (let: x := !p in e).
Proof.
intros. eapply type_let; [done|by apply type_deref_uniq_uniq_instr|solve_typing|done].
Qed.
Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ lctx_lft_incl E L κ κ'
typed_instruction_ty E L [p &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
Proof.
......@@ -139,6 +173,16 @@ Section borrow.
rewrite tctx_interp_singleton tctx_hasty_val' //.
iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
Closed (x :b: []) e
tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T'
lctx_lft_alive E L κ lctx_lft_incl E L κ κ'
( (v:val), typed_body E L C ((v &shr{κ} ty) :: T') (subst' x v e))
typed_body E L C T (let: x := !p in e).
Proof.
intros. eapply type_let; [done|by apply type_deref_shr_uniq_instr|solve_typing|done].
Qed.
End borrow.
Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
......
From lrust.lifetime Require Import definitions.
From lrust.lang Require Import new_delete.
From lrust.typing Require Import programs product product_split own uniq_bor
shr_bor int function lft_contexts uninit cont borrow.
Set Default Proof Using "Type".
Section unbox.
Context `{typeG Σ}.
Definition unbox :=
(funrec: <> ["b"] :=
let: "b'" := !"b" in let: "bx" := !"b'" in
letalloc: "r" := "bx" + #0 in
delete [ #1; "b"] ;; "return" ["r":expr])%E.
Lemma ubox_type :
typed_instruction_ty [] [] [] unbox
(fn (λ α, [α])%EL (λ α, [# own 1 (&uniq{α}own 2 (Π[int; int]))])
(λ α, own 1 (&uniq{α} int))).
Proof.
apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
eapply type_deref; try solve_typing. by apply read_own_move. done.
intros b'; simpl_subst.
eapply type_deref_uniq_own; (try solve_typing)=>bx; simpl_subst.
eapply (type_letalloc_1 (&uniq{α}int)); (try solve_typing)=>r. simpl_subst.
eapply type_delete; try solve_typing.
eapply (type_jump [_]); solve_typing.
Qed.
End unbox.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment