Commit 73f3ded1 authored by Ralf Jung's avatar Ralf Jung

update dependencies; seal typed_{read,write} to avoid unification slowness

parent 66509f23
Pipeline #25806 failed with stage
in 2 minutes and 1 second
......@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
"coq-iris" { (= "dev.2020-03-18.6.d157edcc") | (= "dev") }
"coq-iris" { (= "dev.2020-03-21.0.ed3b52f9") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -168,7 +168,9 @@ Section typing.
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
{ apply (read_shr _ _ _ (cell ty)); solve_typing. }
{ rewrite typed_read_eq.
have Hrd := (read_shr _ _ _ (cell ty)). rewrite typed_read_eq in Hrd.
apply Hrd; solve_typing. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
......
......@@ -221,7 +221,8 @@ Section typing.
Lemma write_own {E L} ty ty' n :
ty.(ty_size) = ty'.(ty_size) typed_write E L (own_ptr n ty') ty (own_ptr n ty).
Proof.
iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
rewrite typed_write_eq. iIntros (Hsz) "!#".
iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
Qed.
......@@ -229,7 +230,8 @@ Section typing.
Lemma read_own_copy E L ty n :
Copy ty typed_read E L (own_ptr n ty) ty (own_ptr n ty).
Proof.
iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
rewrite typed_read_eq. iIntros (Hsz) "!#".
iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
iExists _. auto.
......@@ -238,7 +240,8 @@ Section typing.
Lemma read_own_move E L ty n :
typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
Proof.
iAlways. iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
rewrite typed_read_eq. iAlways.
iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
......
......@@ -54,27 +54,41 @@ Section typing.
Global Arguments typed_instruction _ _ _ _%E _.
(** Writing and Reading **)
Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
( v tid F qL, lftE (lrustN) F
lft_ctx - elctx_interp E - llctx_interp L qL - ty1.(ty_own) tid [v] ={F}=
(l : loc) vl, length vl = ty.(ty_size) v = #l l ↦∗ vl
( l ↦∗: ty.(ty_own) tid ={F}=
llctx_interp L qL ty2.(ty_own) tid [v]))%I.
Definition typed_write_aux : seal (@typed_write_def). by eexists. Qed.
Definition typed_write := typed_write_aux.(unseal).
Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
Global Arguments typed_write _ _ _%T _%T _%T.
Global Instance typed_write_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
Persistent (typed_write E L ty1 ty ty2).
Proof. rewrite typed_write_eq. apply _. Qed.
(* Technically speaking, we could remvoe the vl quantifiaction here and use
mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
make work for some of the provers way harder, since they'd have to show
that nobody could possibly have changed the vl (because only half the
fraction was given). So we go with the definition that is easier to prove. *)
Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
Definition typed_read_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
( v tid F qL, lftE lrustN F
lft_ctx - elctx_interp E - na_own tid F -
llctx_interp L qL - ty1.(ty_own) tid [v] ={F}=
(l : loc) vl q, v = #l l ↦∗{q} vl ty.(ty_own) tid vl
(l ↦∗{q} vl ={F}= na_own tid F
llctx_interp L qL ty2.(ty_own) tid [v]))%I.
Definition typed_read_aux : seal (@typed_read_def). by eexists. Qed.
Definition typed_read := typed_read_aux.(unseal).
Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
Global Arguments typed_read _ _ _%T _%T _%T.
Global Instance typed_read_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
Persistent (typed_read E L ty1 ty ty2).
Proof. rewrite typed_read_eq. apply _. Qed.
End typing.
Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
......@@ -196,6 +210,7 @@ Section typing_rules.
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
rewrite typed_write_eq in Hwrt.
iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
......@@ -221,6 +236,7 @@ Section typing_rules.
iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
iIntros (v) "% Hown".
rewrite typed_read_eq in Hread.
iMod (Hread with "[] LFT HE Htl HL Hown") as
(l vl q) "(% & Hl & Hown & Hclose)"; first done.
subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
......@@ -253,6 +269,7 @@ Section typing_rules.
iIntros (Φ) "(#LFT & #HE & Htl & [HL1 HL2] & [Hp1 Hp2]) HΦ".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
rewrite typed_write_eq typed_read_eq.
iMod ("Hwrt" with "[] LFT HE HL1 Hown1")
as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
iMod ("Hread" with "[] LFT HE Htl HL2 Hown2")
......@@ -274,8 +291,6 @@ Section typing_rules.
Proof.
iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
{ iApply Hwrt. }
{ iApply Hread. }
{ by rewrite tctx_interp_cons tctx_interp_singleton. }
rewrite tctx_interp_cons tctx_interp_singleton. auto.
Qed.
......@@ -290,5 +305,3 @@ Section typing_rules.
typed_body E L C T (p1 <-{n} !p2;; e).
Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed.
End typing_rules.
Hint Opaque typed_read typed_write : lrust_typing.
......@@ -84,7 +84,7 @@ Section typing.
Lemma read_shr E L κ ty :
Copy ty lctx_lft_alive E L κ typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#".
rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)"; first solve_ndisj.
......
......@@ -153,6 +153,7 @@ Section case.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
rewrite typed_write_eq in Hw.
iMod (Hw with "[] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
......@@ -190,7 +191,8 @@ Section case.
Proof.
iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
rewrite typed_write_eq in Hw.
iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)"; first done.
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
......@@ -224,13 +226,15 @@ Section case.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
rewrite typed_write_eq in Hw.
iMod (Hw with "[] LFT HE HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
clear Hw. destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
rewrite typed_read_eq in Hr.
iMod (Hr with "[] LFT HE Htl HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
subst. assert (ty.(ty_size) length vl1).
clear Hr. subst. assert (ty.(ty_size) length vl1).
{ revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
- intros [= ->]. lia.
- specialize (IHtyl i). intuition lia. }
......
......@@ -131,7 +131,7 @@ Section typing.
Lemma read_uniq E L κ ty :
Copy ty lctx_lft_alive E L κ typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#".
rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first solve_ndisj.
......@@ -145,7 +145,7 @@ Section typing.
Lemma write_uniq E L κ ty :
lctx_lft_alive E L κ typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Halive) "!#".
rewrite typed_write_eq. iIntros (Halive) "!#".
iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']"; first solve_ndisj.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment