Skip to content
Snippets Groups Projects
Commit 97bb9b8b authored by Ralf Jung's avatar Ralf Jung
Browse files

Prove that Cell<T> is a type and copy if T is copy

parent 27e2cf0a
No related branches found
No related tags found
No related merge requests found
Pipeline #
......@@ -30,13 +30,13 @@ Section na_bor.
iExists i. iFrame "#". iApply (na_inv_alloc tid E N with "[Hown]"). auto.
Qed.
Lemma na_bor_acc q κ E :
lftN E N E
lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid E ={E}=∗
P na_own tid (E N)
(P -∗ na_own tid (E N) ={E}=∗ q.[κ] na_own tid E).
Lemma na_bor_acc q κ E F :
lftN E N E N F
lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid F ={E}=∗
P na_own tid (F N)
(P -∗ na_own tid (F N) ={E}=∗ q.[κ] na_own tid F).
Proof.
iIntros (??) "#LFT#HP Hκ Hnaown".
iIntros (???) "#LFT#HP Hκ Hnaown".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
......
......@@ -154,7 +154,7 @@ Section typing.
Proof.
iIntros ( ???) "#LFT HE HL Huniq".
iMod ( with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite /tctx_interp !big_sepL_singleton /=.
rewrite !tctx_interp_singleton /=.
iDestruct "Huniq" as (v) "[% Huniq]".
iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
......@@ -171,7 +171,7 @@ Section typing.
iDestruct (elctx_interp_persist with "HE") as "#HE'".
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
......
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import type_context programs.
Set Default Proof Using "Type".
Section cell.
Context `{typeG Σ}.
Local Hint Extern 1000 (_ _) => set_solver : ndisj.
Program Definition cell (ty : type) :=
{| ty_size := ty.(ty_size);
ty_own := ty.(ty_own);
ty_shr κ tid l := (&na{κ, tid, shrN.@l} l ↦∗: ty.(ty_own) tid)%I |}.
Next Obligation. apply ty_size_eq. Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply bor_na.
Qed.
Next Obligation.
iIntros (ty ?? tid l) "#LFT". iApply na_bor_shorten.
Qed.
(* TODO: non-expansiveness, proper wrt. eqtype *)
Global Instance cell_type :
Copy ty Copy (cell ty).
Proof.
intros ty Hcopy. split; first by intros; simpl; apply _.
iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
(* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
destruct (ty_size ty) as [|sz] eqn:Hsz.
{ iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
iDestruct "Hown" as (vl) "[H↦ #Hown]".
simpl. assert (F = F) as -> by set_solver+.
iAssert ( length vl = ty_size ty)%I with "[#]" as ">EQ".
{ iNext. by iApply ty_size_eq. }
rewrite Hsz. iDestruct "EQ" as %EQ. iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
{ iExists vl. by iFrame. }
iModIntro. iSplitL "".
{ iNext. iExists vl. destruct vl; last done. iFrame "Hown".
by iApply heap_mapsto_vec_nil. }
by iIntros "$ _". }
(* Now we are in the non-0 case. *)
iMod (na_bor_acc with "LFT Hshr Htok Htl") as "($ & Htl & Hclose)"; [solve_ndisj..|].
iDestruct (na_own_acc with "Htl") as "($ & Hclose')"; first by set_solver.
iIntros "!> Htl Hown". iPoseProof ("Hclose'" with "Htl") as "Htl".
iMod ("Hclose" with "Hown Htl") as "[$ $]". done.
Qed.
Global Instance cell_send :
Send ty Send (cell ty).
Proof. intros. split. simpl. apply send_change_tid. Qed.
End cell.
Section typing.
Context `{typeG Σ}.
(* Constructing a cell is a coercion. *)
Lemma tctx_mk_cell E L ty p :
tctx_incl E L [p ty] [p cell ty].
Proof.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
(* Same for the other direction *)
Lemma tctx_unmk_cell E L ty p :
tctx_incl E L [p ty] [p cell ty].
Proof.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
(* TODO: get, set; potentially more operations? *)
End typing.
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