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

experiment with some lemmas to help reduce boilerplate in unsafe code proofs

parent 4c4298f1
No related branches found
No related tags found
No related merge requests found
Pipeline #
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 4e1bdcc778381975fbcef1c24736ec384c5ba661
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c325f7a97464f0242e534938c5941a72c29452a2
......@@ -200,19 +200,15 @@ Section code.
iIntros (tid qE) "#LFT Hna HE HL Hk HT".
rewrite (Nat2Z.id (S ty.(ty_size))) 2!tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hrc [Hrcbox Hx]]". destruct x as [[|lx|]|]; try done.
iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
destruct rcbox as [[|lrcbox|]|]; try done. iDestruct "Hrcbox" as "[Hrcbox Hrcbox†]".
iDestruct "Hrcbox" as (vl') "Hrcbox". rewrite uninit_own.
iDestruct "Hrcbox" as "[>Hrcbox↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
rewrite heap_mapsto_vec_cons. iDestruct "Hrcbox↦" as "[Hrcbox↦0 Hrcbox↦1]".
destruct rc as [[|lrc|]|]; try done. iDestruct "Hrc" as "[Hrc Hrc†]".
iDestruct "Hrc" as (vl'') "Hrc". rewrite uninit_own.
iDestruct "Hrc" as "[>Hrc↦ >SZ]". destruct vl'' as [|]; iDestruct "SZ" as %[=].
destruct vl'' as [|]; last done. rewrite heap_mapsto_vec_singleton.
iDestruct "HT" as "[Hrc [Hrcbox Hx]]".
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox.
inv_vec vlrcbox=>??. iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
wp_op. rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_apply (wp_memcpy with "[$Hrcbox↦1 $Hx↦]"); [done||lia..|].
wp_apply (wp_memcpy with "[$Hrcbox↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
iIntros "[Hrcbox↦1 Hx↦]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
iApply (type_type _ _ _ [ #lx box (uninit (ty_size ty)); #lrc box (rc ty)]%TC
with "[] LFT Hna HE HL Hk [-]"); last first.
......@@ -247,10 +243,8 @@ Section code.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iIntros "[Hx [Hrc' Hrc2]]". rewrite [[x]]lock.
destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
destruct rc2 as [[|lrc2|]|]; try done. iDestruct "Hrc2" as "[Hrc2 Hrc2†]".
iDestruct "Hrc2" as (vl) "[>Hrc2 >SZ]". rewrite uninit_own.
destruct vl as [|]; iDestruct "SZ" as %[=].
destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
iDestruct (ownptr_uninit_own with "Hrc2") as (lrc2 vlrc2) "(% & Hrc2 & Hrc2†)".
subst rc2. inv_vec vlrc2=>rc2. rewrite heap_mapsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
rewrite {1}/elctx_interp big_sepL_singleton.
iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
......@@ -309,11 +303,9 @@ Section code.
iIntros (tid qE) "#LFT Hna HE HL Hk".
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iIntros "[Hrcx [Hrc' Hx]]". rewrite [[rcx]]lock.
destruct x as [[|x|]|]; try done. simpl of_val. (* TODO: simpl unfolds too much *)
iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[>Hx >SZ]".
rewrite uninit_own. destruct vl as [|]; iDestruct "SZ" as %[=].
destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
destruct rc' as [[|rc'|]|]; try done. simpl.
iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
destruct rc' as [[|rc'|]|]; try done. simpl of_val.
iDestruct "Hrc'" as (l') "[#Hrc' #Hdelay]".
(* All right, we are done preparing our context. Let's get going. *)
rewrite {1}/elctx_interp big_sepL_singleton. iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
......@@ -324,9 +316,9 @@ Section code.
iDestruct "Hproto" as (γ ν q'') "(#Hincl & #Hinv & #Hrctokb & #Hshr)". iModIntro.
wp_op. wp_write.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx box (&shr{α} rc ty); #x box (&shr{α} ty)]%TC
iApply (type_type _ _ _ [ rcx box (&shr{α} rc ty); #lrc2 box (&shr{α} ty)]%TC
with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
iFrame "Hx". iNext. iApply ty_shr_mono; done. }
{ rewrite /elctx_interp big_sepL_singleton. iFrame. }
......@@ -510,10 +502,9 @@ Section code.
destruct rc' as [[|rc'|]|]; try done. rewrite [[rcx]]lock [[x]]lock.
rewrite {1}/elctx_interp big_sepL_singleton.
iMod (bor_acc_cons with "LFT Hrc' HE") as "[Hrc' Hclose1]"; first solve_ndisj.
iDestruct "Hrc'" as (vl) "[>Hrc' Hrcown]".
iDestruct (ty_size_eq with "Hrcown") as "#>%".
destruct vl as [|l vl]; first done. destruct vl; last done.
rewrite heap_mapsto_vec_singleton. wp_read. destruct l as [[|l|]|]; try done.
iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
wp_read. destruct l as [[|l|]|]; try done.
wp_let. wp_op. rewrite shift_loc_0.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
{ (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?)|?]"; last by iRight.
......
......@@ -28,14 +28,12 @@ Section refcell_functions.
iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
iDestruct "HT" as "[Hr Hx]".
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
inv_vec vlr=>??. iDestruct (heap_mapsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
iIntros "[Hr↦1 Hx↦]". wp_seq.
iApply (type_type _ _ _ [ #lx box (uninit (ty_size ty)); #lr box (refcell ty)]%TC
with "[] LFT Hna HE HL Hk [-]"); last first.
......@@ -65,20 +63,20 @@ Section refcell_functions.
iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
iDestruct "HT" as "[Hr Hx]".
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
inv_vec vlx=>-[[|?|?]|????] vl; try iDestruct "Hx" as ">[]". simpl vec_to_list.
iDestruct "Hx" as "[>% Hx]".
iDestruct (heap_mapsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
iIntros "[Hr↦ Hx↦1]". wp_seq.
iApply (type_type _ _ _ [ #lx box (uninit (S (ty_size ty))); #lr box ty]%TC
with "[] LFT Hna HE HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iSplitR "Hr↦ Hx".
- iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
- iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own. iFrame.
rewrite /= vec_to_list_length. auto.
- iExists vl. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
......
......@@ -174,16 +174,38 @@ Section box.
Global Instance box_ne : NonExpansive box.
Proof. apply type_contractive_ne, _. Qed.
End box.
(* For now, we use the instances inherited from own_ptr. *)
(* Global Instance box_send ty :
Send ty → Send (box ty).
Proof. apply _. Qed.
Section util.
Context `{typeG Σ}.
Global Instance box_sync ty :
Sync ty → Sync (box ty).
Proof. apply _. Qed. *)
End box.
Lemma ownptr_own n ty tid v :
(own_ptr n ty).(ty_own) tid [v] ⊣⊢
(l : loc) (vl : vec val ty.(ty_size)), v = #l l ↦∗ vl ty.(ty_own) tid vl freeable_sz n ty.(ty_size) l.
Proof.
iSplit.
- iIntros "Hown". destruct v as [[|l|]|]; try done.
iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_mapsto_ty_own.
iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
- iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
iFrame. iExists _. iFrame.
Qed.
Lemma ownptr_uninit_own n m tid v :
(own_ptr n (uninit m)).(ty_own) tid [v] ⊣⊢
(l : loc) (vl' : vec val m), v = #l l ↦∗ vl' freeable_sz n m l.
Proof.
rewrite ownptr_own. apply uPred.exist_proper=>l. iSplit.
(* FIXME: The goals here look rather confusing: One cannot tell that we are looking at
a statement in Iris; the top-level → could just as well be a Coq implication. *)
- iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
rewrite -uPred.sep_exist_l. iSplit; first done.
iNext. eauto with iFrame.
- iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
iExists vl. rewrite uninit_own vec_to_list_length.
eauto with iFrame.
Qed.
End util.
Section typing.
Context `{typeG Σ}.
......
......@@ -582,5 +582,19 @@ Section subtyping.
Qed.
End subtyping.
Section type_util.
Context `{typeG Σ}.
Lemma heap_mapsto_ty_own l ty tid :
l ↦∗: ty_own ty tid ⊣⊢ (vl : vec val ty.(ty_size)), l ↦∗ vl ty_own ty tid vl.
Proof.
iSplit.
- iIntros "H". iDestruct "H" as (vl) "[Hl Hown]".
iDestruct (ty_size_eq with "Hown") as %<-.
iExists (list_to_vec vl). rewrite vec_to_list_of_list. iFrame.
- iIntros "H". iDestruct "H" as (vl) "[Hl Hown]". eauto with iFrame.
Qed.
End type_util.
Hint Resolve subtype_refl eqtype_refl : lrust_typing.
Hint Opaque subtype eqtype : lrust_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