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

experiment with removing sections

parent 01de0893
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/arc.v
+ 42
− 41
View file @ ff44d9c0
......@@ -13,6 +13,8 @@ Definition arc_invN := arcN .@ "inv".
Definition arc_shrN := arcN .@ "shr".
Definition arc_endN := arcN .@ "end".
Local Notation P2 l n := ((† l…(2 + n%nat%type%stdpp))%I%I ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n%nat⌝)%I.
Section arc.
Context `{!typeG Σ, !arcG Σ}.
......@@ -20,7 +22,6 @@ Section arc.
Let P1 ν q := (q.[ν])%I.
Instance P1_fractional ν : Fractional (P1 ν).
Proof. unfold P1. apply _. Qed.
Let P2 l n := († l…(2 + n) ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
Definition arc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
(is_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN γ l ∗
(* We use this disjunction, and not simply [ty_shr] here, *)
......@@ -322,9 +323,10 @@ Section arc.
repeat (apply send_change_tid || apply bi.exist_mono ||
(apply arc_persist_send; apply _) || f_equiv || intros ?).
Qed.
End arc.
(* Code : constructors *)
Definition arc_new ty : val :=
Definition arc_new `{!typeG Σ, !arcG Σ} ty : val :=
funrec: <> ["x"] :=
let: "arcbox" := new [ #(2 + ty.(ty_size))%nat ] in
let: "arc" := new [ #1 ] in
......@@ -334,7 +336,7 @@ Section arc.
"arc" <- "arcbox";;
delete [ #ty.(ty_size); "x"];; return: ["arc"].
Lemma arc_new_type ty `{!TyWf ty} :
Lemma arc_new_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val (arc_new ty) (fn(∅; ty) → arc ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -367,7 +369,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition weak_new ty : val :=
Definition weak_new `{!typeG Σ, !arcG Σ} ty : val :=
funrec: <> [] :=
let: "arcbox" := new [ #(2 + ty.(ty_size))%nat ] in
let: "w" := new [ #1 ] in
......@@ -376,7 +378,7 @@ Section arc.
"w" <- "arcbox";;
return: ["w"].
Lemma weak_new_type ty `{!TyWf ty} :
Lemma weak_new_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val (weak_new ty) (fn(∅) → weak ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -400,7 +402,7 @@ Section arc.
with "[] LFT HE Hna HL Hk [>-]"); last first.
{ rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
iMod (create_weak (λ q, q.[ν])%I (P2 lrcbox ty.(ty_size))
with "Hrcbox↦0 Hrcbox↦1 [-]") as (γ) "[Ha Htok]".
{ rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
by rewrite vec_to_list_length. }
......@@ -410,14 +412,14 @@ Section arc.
Qed.
(* Code : deref *)
Definition arc_deref : val :=
Definition arc_deref `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["arc"] :=
let: "x" := new [ #1 ] in
let: "arc'" := !"arc" in
"x" <- (!"arc'" +ₗ #2);;
delete [ #1; "arc" ];; return: ["x"].
Lemma arc_deref_type ty `{!TyWf ty} :
Lemma arc_deref_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val arc_deref (fn(∀ α, ∅; &shr{α}(arc ty)) → &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -453,7 +455,7 @@ Section arc.
Qed.
(* Code : getters *)
Definition arc_strong_count : val :=
Definition arc_strong_count `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
......@@ -461,7 +463,7 @@ Section arc.
"r" <- strong_count ["arc''"];;
delete [ #1; "arc" ];; return: ["r"].
Lemma arc_strong_count_type ty `{!TyWf ty} :
Lemma arc_strong_count_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val arc_strong_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -479,7 +481,7 @@ Section arc.
iApply wp_fupd. wp_read.
iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (strong_count_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
wp_apply (strong_count_spec (λ q, q.[ν])%I (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
......@@ -496,7 +498,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition arc_weak_count : val :=
Definition arc_weak_count `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
......@@ -504,7 +506,7 @@ Section arc.
"r" <- weak_count ["arc''"];;
delete [ #1; "arc" ];; return: ["r"].
Lemma arc_weak_count_type ty `{!TyWf ty} :
Lemma arc_weak_count_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val arc_weak_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -522,7 +524,7 @@ Section arc.
iApply wp_fupd. wp_read.
iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (weak_count_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
wp_apply (weak_count_spec (λ q, q.[ν])%I (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
......@@ -540,7 +542,7 @@ Section arc.
Qed.
(* Code : clone, [up/down]grade. *)
Definition arc_clone : val :=
Definition arc_clone `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
......@@ -549,7 +551,7 @@ Section arc.
"r" <- "arc''";;
delete [ #1; "arc" ];; return: ["r"].
Lemma arc_clone_type ty `{!TyWf ty} :
Lemma arc_clone_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val arc_clone (fn(∀ α, ∅; &shr{α}(arc ty)) → arc ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -567,7 +569,7 @@ Section arc.
iApply wp_fupd. wp_read.
iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (clone_arc_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
wp_apply (clone_arc_spec (λ q, q.[ν])%I (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
......@@ -584,7 +586,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition weak_clone : val :=
Definition weak_clone `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["w"] :=
let: "r" := new [ #1 ] in
let: "w'" := !"w" in
......@@ -593,7 +595,7 @@ Section arc.
"r" <- "w''";;
delete [ #1; "w" ];; return: ["r"].
Lemma weak_clone_type ty `{!TyWf ty} :
Lemma weak_clone_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -611,7 +613,7 @@ Section arc.
iApply wp_fupd. wp_read.
iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
iDestruct "Hproto" as (γ ν) "#[Hpersist Hrctokb]". iModIntro. wp_let.
wp_apply (clone_weak_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
wp_apply (clone_weak_spec (λ q, q.[ν])%I (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
......@@ -628,7 +630,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition downgrade : val :=
Definition downgrade `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
......@@ -637,7 +639,7 @@ Section arc.
"r" <- "arc''";;
delete [ #1; "arc" ];; return: ["r"].
Lemma downgrade_type ty `{!TyWf ty} :
Lemma downgrade_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val downgrade (fn(∀ α, ∅; &shr{α}(arc ty)) → weak ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -655,7 +657,7 @@ Section arc.
iApply wp_fupd. wp_read.
iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (downgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
wp_apply (downgrade_spec (λ q, q.[ν])%I (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
......@@ -672,7 +674,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition upgrade : val :=
Definition upgrade `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["w"] :=
let: "r" := new [ #2 ] in
let: "w'" := !"w" in
......@@ -684,7 +686,7 @@ Section arc.
"r" <-{Σ none} ();;
delete [ #1; "w" ];; return: ["r"].
Lemma upgrade_type ty `{!TyWf ty} :
Lemma upgrade_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (arc ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -702,7 +704,7 @@ Section arc.
iApply wp_fupd. wp_read.
iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
iDestruct "Hproto" as (γ ν) "#[Hpersist Hrctokb]". iModIntro. wp_let.
wp_apply (upgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
wp_apply (upgrade_spec (λ q, q.[ν])%I (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
......@@ -729,7 +731,7 @@ Section arc.
Qed.
(* Code : drop *)
Definition arc_drop ty : val :=
Definition arc_drop `{!typeG Σ, !arcG Σ} ty : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #(option ty).(ty_size) ] in
let: "arc'" := !"arc" in
......@@ -742,7 +744,7 @@ Section arc.
else #☠);;
delete [ #1; "arc"];; return: ["r"].
Lemma arc_drop_type ty `{!TyWf ty} :
Lemma arc_drop_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val (arc_drop ty) (fn(∅; arc ty) → option ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -755,8 +757,8 @@ Section arc.
iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
{ iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
wp_bind (drop_arc _). iApply (drop_arc_spec with "[] [$Htok Hν]");
[by iDestruct "Hpersist" as "[$?]"|done|].
wp_bind (drop_arc _). iApply (drop_arc_spec (λ q, (q).[ν])%I with "[] [$Htok $Hν]");
[by iDestruct "Hpersist" as "[$?]"|].
iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
{ destruct b; wp_if=>//. destruct r as [[]|]; try done.
......@@ -773,7 +775,7 @@ Section arc.
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
{ unfold P2. auto with iFrame. }
{ unfold P2. iFrame. iExists _. iFrame. auto. }
wp_apply (drop_weak_spec with "[//] Htok"). unlock. iIntros ([]); last first.
{ iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
......@@ -796,7 +798,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition weak_drop ty : val :=
Definition weak_drop `{!typeG Σ, !arcG Σ} ty : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #0] in
let: "arc'" := !"arc" in
......@@ -804,7 +806,7 @@ Section arc.
else #☠);;
delete [ #1; "arc"];; return: ["r"].
Lemma weak_drop_type ty `{!TyWf ty} :
Lemma weak_drop_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val (weak_drop ty) (fn(∅; weak ty) → unit).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -832,7 +834,7 @@ Section arc.
Qed.
(* Code : other primitives *)
Definition arc_try_unwrap ty : val :=
Definition arc_try_unwrap `{!typeG Σ, !arcG Σ} ty : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #(Σ[ ty; arc ty ]).(ty_size) ] in
let: "arc'" := !"arc" in
......@@ -847,7 +849,7 @@ Section arc.
"r" <-{Σ 1} "arc'";;
delete [ #1; "arc"];; return: ["r"].
Lemma arc_try_unwrap_type ty `{!TyWf ty} :
Lemma arc_try_unwrap_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val (arc_try_unwrap ty) (fn(∅; arc ty) → Σ[ ty; arc ty ]).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -860,7 +862,7 @@ Section arc.
iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
{ iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
wp_apply (try_unwrap_spec with "[] [Hν Htok]");
wp_apply (try_unwrap_spec (λ q, (q).[ν])%I with "[] [Hν Htok]");
[by iDestruct "Hpersist" as "[$?]"|iFrame|].
iIntros ([]) "H"; wp_if.
- iDestruct "H" as "[Hν Hend]". rewrite -(lock [r]). destruct r as [[|r|]|]=>//=.
......@@ -906,7 +908,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition arc_get_mut : val :=
Definition arc_get_mut `{!typeG Σ, !arcG Σ} : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #2 ] in
let: "arc'" := !"arc" in
......@@ -920,7 +922,7 @@ Section arc.
"r" <-{Σ none} ();;
delete [ #1; "arc"];; return: ["r"].
Lemma arc_get_mut_type ty `{!TyWf ty} :
Lemma arc_get_mut_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} :
typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α}(arc ty)) → option (&uniq{α}ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
......@@ -968,7 +970,7 @@ Section arc.
iApply type_jump; solve_typing.
Qed.
Definition arc_make_mut (ty : type) (clone : val) : val :=
Definition arc_make_mut `{!typeG Σ, !arcG Σ} (ty : type) (clone : val) : val :=
funrec: <> ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
......@@ -1006,7 +1008,7 @@ Section arc.
delete [ #1; "arc"];; return: ["r"]
]).
Lemma arc_make_mut_type ty `{!TyWf ty} clone :
Lemma arc_make_mut_type `{!typeG Σ, !arcG Σ} ty `{!TyWf ty} clone :
typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(arc ty)) → &uniq{α} ty).
Proof.
......@@ -1116,4 +1118,3 @@ Section arc.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
End arc.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment