From 42f3528f4bfdad3ce17c7731a4a0b524ba9a98dc Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 18 Feb 2017 11:43:02 +0100
Subject: [PATCH] Map for Ref.
* Also, removed the box from the definition of typing judgments, so that we can frame resources around them.
---
theories/lang/new_delete.v | 4 +-
theories/typing/bool.v | 4 +-
theories/typing/borrow.v | 8 +-
theories/typing/cont.v | 31 +++++--
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 3 +-
theories/typing/examples/lazy_lft.v | 3 +-
theories/typing/examples/option_as_mut.v | 8 +-
theories/typing/examples/rebor.v | 3 +-
theories/typing/examples/unbox.v | 3 +-
theories/typing/examples/unwrap_or.v | 3 +-
theories/typing/function.v | 33 +++----
theories/typing/int.v | 8 +-
theories/typing/lft_contexts.v | 17 +++-
theories/typing/own.v | 4 +-
theories/typing/programs.v | 24 +++---
theories/typing/type_sum.v | 12 +--
theories/typing/unsafe/cell.v | 17 ++--
theories/typing/unsafe/refcell/ref_code.v | 86 +++++++++++++++++--
theories/typing/unsafe/refcell/refcell_code.v | 33 ++++---
theories/typing/unsafe/refcell/refmut_code.v | 15 ++--
theories/typing/unsafe/spawn.v | 13 +--
22 files changed, 233 insertions(+), 101 deletions(-)
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index b27b5d5f..c78267bc 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -43,7 +43,7 @@ End specs.
(* FIXME : why are these notations not pretty-printed? *)
Notation "'letalloc:' x <- e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
- (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+ (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V} !e1 ;; e2)) [new [ #n]])%E
- (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+ (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index eed4fec3..7cb39d57 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -26,7 +26,7 @@ Section typing.
Lemma type_bool_instr (b : Datatypes.bool) E L :
typed_instruction_ty E L [] #b bool.
Proof.
- iAlways. iIntros (tid qE) "_ $ $ $ _". wp_value.
+ iIntros (tid qE) "_ $ $ $ _". wp_value.
rewrite tctx_interp_singleton tctx_hasty_val. by destruct b.
Qed.
@@ -41,7 +41,7 @@ Section typing.
typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
typed_body E L C T (if: p then e1 else e2).
Proof.
- iIntros (Hp) "#He1 #He2 !#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hp) "He1 He2". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 2ad78a0c..5e87a0b0 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -47,7 +47,7 @@ Section borrow.
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◠&uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
Proof.
- iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
+ iIntros (Hκ tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
@@ -77,7 +77,7 @@ Section borrow.
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◠&shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
Proof.
- iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
+ iIntros (Hκ tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
@@ -103,7 +103,7 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◠&uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
Proof.
- iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
+ iIntros (Hκ Hincl tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
@@ -137,7 +137,7 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◠&shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
Proof.
- iIntros (Hκ Hincl) "!# * #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+ iIntros (Hκ Hincl tid qE) "#LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 7331c523..8bb2f484 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -13,7 +13,7 @@ Section typing.
tctx_incl E L T (T' (list_to_vec args)) →
typed_body E L C T (k (of_val <$> args)).
Proof.
- iIntros (HC Hincl) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (HC Hincl tid qE) "#LFT Htl HE HL HC HT".
iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
iSpecialize ("HC" with "HE []"); first done.
rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "Htl HL HT").
@@ -22,13 +22,14 @@ Section typing.
Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
(∀ k, typed_body E L2 (k â—cont(L1, T') :: C) T (subst' kb k e2)) -∗
- (∀ k (args : vec val (length argsb)),
- typed_body E L1 (k â—cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt)) -∗
+ □ (∀ k (args : vec val (length argsb)),
+ typed_body E L1 (k â—cont(L1, T') :: C) (T' args)
+ (subst_v (kb::argsb) (k:::args) econt)) -∗
typed_body E L2 C T (e2 cont: kb argsb := econt).
Proof.
- iIntros (Hc1 Hc2) "#He2 #Hecont !#". iIntros (tid qE) "#LFT Htl HE HL HC HT". iApply wp_let'.
- { simpl. rewrite decide_left. done. }
- iModIntro. iApply ("He2" with "LFT Htl HE HL [HC] HT"). iClear "He2".
+ iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iApply wp_let'; first by rewrite /= decide_left.
+ iModIntro. iApply ("He2" with "LFT Htl HE HL [HC] HT").
iIntros "HE". iLöb as "IH". iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
@@ -36,4 +37,22 @@ Section typing.
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
iNext. iApply ("Hecont" with "LFT Htl HE HL [HC] HT"). by iApply "IH".
Qed.
+
+ Lemma type_cont_norec argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
+ Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+ (∀ k, typed_body E L2 (k â—cont(L1, T') :: C) T (subst' kb k e2)) -∗
+ (∀ k (args : vec val (length argsb)),
+ typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
+ typed_body E L2 C T (e2 cont: kb argsb := econt).
+ Proof.
+ iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iApply wp_let'; first by rewrite /= decide_left.
+ iModIntro. iApply ("He2" with "LFT Htl HE HL [HC Hecont] HT").
+ iIntros "HE". iIntros (x) "H".
+ iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
+ iIntros (args) "Htl HL HT". iApply wp_rec; try done.
+ { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
+ { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
+ iNext. iApply ("Hecont" with "LFT Htl HE HL HC HT").
+ Qed.
End typing.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 186d39a5..db14c7eb 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -18,7 +18,7 @@ Section get_x.
and without using 'typed_instruction_ty'. I think that's related to
the list notation that we added to %TC. *)
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret p).
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
inv_vec p=>p. simpl_subst.
iApply type_deref; [solve_typing..|by apply read_own_move|done|].
iIntros (p'); simpl_subst.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 44c0c100..1d1eefc0 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -16,7 +16,8 @@ Section init_prod.
typed_instruction_ty [] [] [] init_prod
(fn([]; int, int) → Π[int;int]).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p=>x y. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+ inv_vec p=>x y. simpl_subst.
iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (x'). simpl_subst.
iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (y'). simpl_subst.
iApply (type_new_subtype (Î [uninit 1; uninit 1])); [solve_typing..|].
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 58acc6f5..96c2d0ee 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -21,7 +21,8 @@ Section lazy_lft.
typed_instruction_ty [] [] [] lazy_lft
(fn([]) → unit).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+ inv_vec p. simpl_subst.
iApply (type_newlft []). iIntros (α).
iApply (type_new_subtype (Î [uninit 1;uninit 1])); [solve_typing..|].
iIntros (t). simpl_subst.
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/examples/option_as_mut.v
index 8a004b01..652d93ea 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -19,10 +19,12 @@ Section option_as_mut.
typed_instruction_ty [] [] [] option_as_mut
(fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ]) → Σ[unit; &uniq{α}τ]).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret p). inv_vec p=>o. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
+ inv_vec p=>o. simpl_subst.
iApply (type_cont [_] [] (λ r, [o ◠_; r!!!0 ◠_])%TC) ; [solve_typing..| |].
- iIntros (k). simpl_subst.
- iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (o'). simpl_subst.
+ iApply type_deref; [solve_typing|apply read_own_move|done|].
+ iIntros (o'). simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_case_uniq; [solve_typing..|].
constructor; last constructor; last constructor; left.
@@ -30,7 +32,7 @@ Section option_as_mut.
iApply (type_jump [_]); solve_typing.
+ iApply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
iApply (type_jump [_]); solve_typing.
- - simpl. iIntros (k r). inv_vec r=>r. simpl_subst.
+ - iIntros "/= !#". iIntros (k r). inv_vec r=>r. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing.
Qed.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 1a4103b6..99254956 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -20,7 +20,8 @@ Section rebor.
typed_instruction_ty [] [] [] rebor
(fn([]; Π[int; int], Π[int; int]) → int).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p=>t1 t2. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+ inv_vec p=>t1 t2. simpl_subst.
iApply (type_newlft []). iIntros (α).
iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index cabf1070..0aeb0f71 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -15,7 +15,8 @@ Section unbox.
typed_instruction_ty [] [] [] unbox
(fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret b). inv_vec b=>b. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret b).
+ inv_vec b=>b. simpl_subst.
iApply type_deref; [solve_typing..|by apply read_own_move|done|].
iIntros (b'); simpl_subst.
iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
diff --git a/theories/typing/examples/unwrap_or.v b/theories/typing/examples/unwrap_or.v
index e4584e02..dcb45785 100644
--- a/theories/typing/examples/unwrap_or.v
+++ b/theories/typing/examples/unwrap_or.v
@@ -16,7 +16,8 @@ Section unwrap_or.
typed_instruction_ty [] [] [] (unwrap_or Ï„)
(fn([]; Σ[unit; τ], τ) → τ).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p=>o def. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+ inv_vec p=>o def. simpl_subst.
iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+ right. iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5c67b116..fefa3888 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -13,11 +13,11 @@ Section fn.
{| st_own tid vl := (∃ fb kb xb e H,
⌜vl = [@RecV fb (kb::xb) e H]⌠∗ ⌜length xb = n⌠∗
▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
- typed_body (E x) []
- [kâ—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
- (zip_with (TCtx_hasty ∘ of_val) xl
- ((λ ty, box ty) <$> (vec_to_list (tys x))))
- (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
+ â–¡ typed_body (E x) []
+ [kâ—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
+ (zip_with (TCtx_hasty ∘ of_val) xl
+ ((λ ty, box ty) <$> (vec_to_list (tys x))))
+ (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
Next Obligation.
iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
Qed.
@@ -191,7 +191,7 @@ Section typing.
T)
(call: p ps → k).
Proof.
- iIntros (HE) "!# * #LFT Htl HE HL HC".
+ iIntros (HE tid qE) "#LFT Htl HE HL HC".
rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = kâŒ):::
@@ -253,7 +253,8 @@ Section typing.
(∀ ret : val, typed_body E L C ((ret ◠box (ty x))::T') (subst' b ret e)) -∗
typed_body E L C T (letcall: b := p ps in e).
Proof.
- iIntros (?? Hpsc ???) "He". iApply (type_cont [_] _ (λ r, (r!!!0 ◠box (ty x)) :: T')%TC).
+ iIntros (?? Hpsc ???) "He".
+ iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◠box (ty x)) :: T')%TC).
- (* TODO : make [solve_closed] work here. *)
eapply is_closed_weaken; first done. set_solver+.
- (* TODO : make [solve_closed] work here. *)
@@ -282,15 +283,15 @@ Section typing.
ef = (funrec: fb argsb := e)%E →
n = length argsb →
Closed (fb :b: "return" :b: argsb +b+ []) e →
- (∀ x (f : val) k (args : vec val (length argsb)),
- typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
- ((f â— fn E' tys ty) ::
- zip_with (TCtx_hasty ∘ of_val) args
- ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
- (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
+ □ (∀ x (f : val) k (args : vec val (length argsb)),
+ typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
+ ((f â— fn E' tys ty) ::
+ zip_with (TCtx_hasty ∘ of_val) args
+ ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
+ (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn E' tys ty).
Proof.
- iIntros (-> -> Hc) "#Hbody !# * #LFT $ $ $ #HT". iApply wp_value.
+ iIntros (-> -> Hc) "#Hbody". iIntros (tid qE) " #LFT $ $ $ #HT". iApply wp_value.
{ simpl. rewrite ->(decide_left Hc). done. }
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ simpl. rewrite decide_left. done. }
@@ -307,14 +308,14 @@ Section typing.
ef = (funrec: <> argsb := e)%E →
n = length argsb →
Closed ("return" :b: argsb +b+ []) e →
- (∀ x k (args : vec val (length argsb)),
+ □ (∀ x k (args : vec val (length argsb)),
typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
(zip_with (TCtx_hasty ∘ of_val) args
((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
(subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn E' tys ty).
Proof.
- iIntros (???) "He". iApply type_rec; try done. iIntros.
+ iIntros (???) "#He". iApply type_rec; try done. iIntros "!# *".
(iApply typed_body_mono; last by iApply "He"); try done.
eapply contains_tctx_incl. by constructor.
Qed.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 2dd8f692..fd21063a 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -25,7 +25,7 @@ Section typing.
Lemma type_int_instr (z : Z) E L :
typed_instruction_ty E L [] #z int.
Proof.
- iAlways. iIntros (tid qE) "_ $ $ $ _". wp_value.
+ iIntros (tid qE) "_ $ $ $ _". wp_value.
by rewrite tctx_interp_singleton tctx_hasty_val.
Qed.
@@ -38,7 +38,7 @@ Section typing.
Lemma type_plus_instr E L p1 p2 :
typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 + p2) int.
Proof.
- iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
@@ -55,7 +55,7 @@ Section typing.
Lemma type_minus_instr E L p1 p2 :
typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 - p2) int.
Proof.
- iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
@@ -72,7 +72,7 @@ Section typing.
Lemma type_le_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◠int; p2 ◠int] (p1 ≤ p2) bool.
Proof.
- iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index c6d5452e..e7632f58 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -334,6 +334,21 @@ Section lft_contexts.
iExists q. rewrite {1 2 4 5}/elctx_interp big_sepL_cons /=.
iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
Qed.
+
+ Lemma elctx_sat_app E1 E2 :
+ elctx_sat E1 → elctx_sat E2 → elctx_sat (E1 ++ E2).
+ Proof.
+ iIntros (HE1 HE2 ????) "[HE1 HE2] [HL1 HL2]".
+ iMod (HE1 with "HE1 HL1") as (qE1) "[HE1 Hclose1]". done.
+ iMod (HE2 with "HE2 HL2") as (qE2) "[HE2 Hclose2]". done.
+ destruct (Qp_lower_bound qE1 qE2) as (q & qE1' & qE2' & -> & ->). iExists q.
+ rewrite !fractional (fractional_half_equiv qE) /elctx_interp big_sepL_app.
+ iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]". iIntros "!> [Hq1 Hq2]".
+ iMod ("Hclose1" with "[$HE1 $Hq1]") as "[$ $]". iApply "Hclose2". iFrame.
+ Qed.
+
+ Lemma elctx_sat_refl : elctx_sat E.
+ Proof. iIntros (????) "??". iExists _. eauto with iFrame. Qed.
End lft_contexts.
Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
@@ -457,7 +472,7 @@ Hint Resolve
lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
lctx_lft_incl_external'
lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
- elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl
+ elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
: lrust_typing.
Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index d86aca22..95f6ade8 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -195,7 +195,7 @@ Section typing.
let n' := Z.to_nat n in
typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
Proof.
- intros. iAlways. iIntros (tid q) "#LFT $ $ $ _".
+ iIntros (? tid q) "#LFT $ $ $ _".
iApply wp_new; first done. iModIntro.
iIntros (l vl) "(% & H†& Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
@@ -227,7 +227,7 @@ Section typing.
Z.of_nat (ty.(ty_size)) = n →
typed_instruction E L [p ◠box ty] (delete [ #n; p])%E (λ _, []).
Proof.
- iIntros (<-) "!#". iIntros (tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+ iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as "[H↦∗: >H†]". iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 544e960f..e610b8bf 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -10,7 +10,7 @@ Section typing.
(* This is an iProp because it is also used by the function type. *)
Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
- (□ ∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
+ (∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
elctx_interp E qE -∗ llctx_interp L 1 -∗
(elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
WP e {{ _, cont_postcondition }})%I.
@@ -34,7 +34,7 @@ Section typing.
Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
(typed_body E L).
Proof.
- intros C1 C2 HC T1 T2 HT e ? <-. iIntros "#H !#".
+ intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
iApply ("H" with "LFT Htl HE HL [HC] HT").
@@ -49,7 +49,7 @@ Section typing.
(** Instruction *)
Definition typed_instruction (E : elctx) (L : llctx)
(T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
- (□ ∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
+ (∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗
llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
@@ -98,7 +98,7 @@ Section typing_rules.
typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
Proof.
- iIntros (He) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (He tid qE) "#LFT Htl HE HL HC HT".
rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
iApply (He with "LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
@@ -113,8 +113,8 @@ Section typing_rules.
(∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) -∗
typed_body E L C (T1 ++ T) (let: xb := e in e').
Proof.
- iIntros (Hc) "#He #He' !#". iIntros (tid qE) "#LFT Htl HE HL HC HT". rewrite tctx_interp_app.
- iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
+ iIntros (Hc) "He He'". iIntros (tid qE) "#LFT Htl HE HL HC HT". rewrite tctx_interp_app.
+ iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HE HL HT1 Htl]").
{ iApply ("He" with "LFT Htl HE HL HT1"). }
iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
iModIntro. iApply ("He'" with "LFT Htl HE HL HC [HT2 HT]").
@@ -150,7 +150,7 @@ Section typing_rules.
(∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) -∗
typed_body E L C T (Newlft ;; e).
Proof.
- iIntros (Hc) "#He !#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hc) "He". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
set (κ' := foldr (∪) static κs). wp_seq.
iApply ("He" $! (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
@@ -164,7 +164,7 @@ Section typing_rules.
Closed [] e → UnblockTctx κ T1 T2 →
typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
Proof.
- iIntros (Hc Hub) "#He !#". iIntros (tid qE) "#LFT Htl HE".
+ iIntros (Hc Hub) "He". iIntros (tid qE) "#LFT Htl HE".
rewrite /llctx_interp big_sepL_cons. iIntros "[Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
@@ -176,7 +176,7 @@ Section typing_rules.
Lemma type_path_instr {E L} p ty :
typed_instruction_ty E L [p â— ty] p ty.
Proof.
- iIntros "!# * _ $$$ ?". rewrite tctx_interp_singleton.
+ iIntros (??) "_ $$$ ?". rewrite tctx_interp_singleton.
iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
Qed.
@@ -192,7 +192,7 @@ Section typing_rules.
typed_write E L ty1 ty ty1' →
typed_instruction E L [p1 ◠ty1; p2 ◠ty] (p1 <- p2) (λ _, [p1 ◠ty1']%TC).
Proof.
- iIntros (Hwrt) "!#". iIntros (tid qE) "#LFT $ HE HL".
+ iIntros (Hwrt tid qE) "#LFT $ HE HL".
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".
@@ -218,7 +218,7 @@ Section typing_rules.
ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
typed_instruction E L [p ◠ty1] (!p) (λ v, [p ◠ty1'; v ◠ty]%TC).
Proof.
- iIntros (Hsz Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL Hp".
+ iIntros (Hsz Hread tid qE) "#LFT Htl HE HL Hp".
rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
iIntros (v) "% Hown".
iMod (Hread with "[] LFT Htl HE HL Hown") as
@@ -271,7 +271,7 @@ Section typing_rules.
typed_instruction E L [p1 â— ty1; p2 â— ty2] (p1 <-{n} !p2)
(λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
- iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL HT".
+ iIntros (Hsz Hwrt Hread tid qE) "#LFT Htl HE HL HT".
iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
{ iApply Hwrt. }
{ iApply Hread. }
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index e59eee2d..7513bbd0 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -16,7 +16,7 @@ Section case.
typed_body E L C ((p ◠own_ptr n (sum tyl)) :: T) e) tyl el →
typed_body E L C ((p â— own_ptr n (sum tyl)) :: T) (case: !p of el).
Proof.
- iIntros (Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
+ iIntros (Hel tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
@@ -61,7 +61,7 @@ Section case.
typed_body E L C ((p ◠&uniq{κ}sum tyl) :: T) e) tyl el →
typed_body E L C ((p ◠&uniq{κ}sum tyl) :: T) (case: !p of el).
Proof.
- iIntros (Halive Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
+ iIntros (Halive Hel tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
@@ -114,7 +114,7 @@ Section case.
typed_body E L C ((p ◠&shr{κ}sum tyl) :: T) e) tyl el →
typed_body E L C ((p ◠&shr{κ}sum tyl) :: T) (case: !p of el).
Proof.
- iIntros (Halive Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
+ iIntros (Halive Hel tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
iDestruct "Hp" as (i) "[#Hb Hshr]".
@@ -146,7 +146,7 @@ Section case.
typed_write E L ty1 (sum tyl) ty2 →
typed_instruction E L [p1 ◠ty1; p2 ◠ty] (p1 <-{Σ i} p2) (λ _, [p1 ◠ty2]%TC).
Proof.
- iIntros (Hty Hw) "!# * #LFT $ HE HL Hp".
+ iIntros (Hty Hw tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
@@ -185,7 +185,7 @@ Section case.
typed_write E L ty1 (sum tyl) ty2 →
typed_instruction E L [p ◠ty1] (p <-{Σ i} ()) (λ _, [p ◠ty2]%TC).
Proof.
- iIntros (Hty Hw) "!# * #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+ iIntros (Hty Hw tid qE) "#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.
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
@@ -215,7 +215,7 @@ Section case.
typed_instruction E L [p1 â— ty1; p2 â— ty2]
(p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
- iIntros (Hty Hw Hr) "!# * #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+ iIntros (Hty Hw Hr tid qE) "#LFT Htl [HE1 HE2] [HL1 HL2] Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index ffce1f6b..ba9d6f96 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -85,7 +85,8 @@ Section typing.
typed_instruction_ty [] [] [] cell_new
(fn([]; ty) → cell ty).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply (type_jump [_]); first solve_typing.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
@@ -97,7 +98,8 @@ Section typing.
typed_instruction_ty [] [] [] cell_into_inner
(fn([]; cell ty) → ty).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply (type_jump [_]); first solve_typing.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
@@ -109,7 +111,8 @@ Section typing.
typed_instruction_ty [] [] [] cell_get_mut
(fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
by iIntros "$".
@@ -126,7 +129,8 @@ Section typing.
typed_instruction_ty [] [] [] (cell_get ty)
(fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
{ apply (read_shr _ _ _ (cell ty)); solve_typing. }
@@ -146,11 +150,12 @@ Section typing.
typed_instruction_ty [] [] [] (cell_replace ty)
(fn(∀ α, [☀α]; &shr{α} cell ty, ty) → ty).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>c x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>c x. simpl_subst.
iApply type_deref; [solve_typing|exact: read_own_move|done|]. iIntros (c'); simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r); simpl_subst.
(* Drop to Iris level. *)
- iAlways. iIntros (tid qE) "#LFT Htl HE HL HC".
+ iIntros (tid qE) "#LFT Htl HE HL HC".
rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iIntros "(Hr & Hc & #Hc' & Hx)".
rewrite {1}/elctx_interp big_opL_singleton /=.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index bb3cfaab..af736767 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op fractional.
-From lrust.lifetime Require Import na_borrow.
+From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.unsafe.refcell Require Import refcell ref.
Set Default Proof Using "Type".
@@ -59,9 +59,10 @@ Section ref_functions.
(fn (fun '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
(fun '(α, β) => ref β ty)%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
- iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
@@ -120,9 +121,10 @@ Section ref_functions.
(fun '(α, β) => [# &shr{α}(ref β ty)]%T)
(fun '(α, β) => &shr{α}ty)%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
- iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
@@ -156,8 +158,9 @@ Section ref_functions.
Lemma ref_drop_type ty :
typed_instruction_ty [] [] [] ref_drop (fn(∀ α, [☀α]; ref α ty) → unit).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
- iIntros "!# * #LFT Hna Hα HL Hk Hx".
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iIntros (tid qE) "#LFT Hna Hα HL Hk Hx".
rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
@@ -201,4 +204,73 @@ Section ref_functions.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply (type_jump [_]); solve_typing.
Qed.
+
+ (* Apply a function within the ref, typically for accessing a component. *)
+ Definition ref_map : val :=
+ funrec: <> ["ref"; "f"; "env"] :=
+ let: "x'" := !"ref" in
+ let: "f'" := !"f" in
+ letalloc: "x" <- "x'" in
+ letcall: "r" := "f'" ["env"; "x"]%E in
+ let: "r'" := !"r" in
+ "ref" <- "r'";;
+ delete [ #1; "f"];; "k" []
+ cont: "k" [] :=
+ "return" ["ref"].
+
+ Lemma ref_map_type ty1 ty2 envty E :
+ typed_instruction_ty [] [] [] ref_map
+ (fn(∀ β, [☀β] ++ E; ref β ty1, fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
+ → ref β ty2).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>ref f env. simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT".
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iDestruct "HT" as "(Href & Hf & Henv)".
+ destruct ref as [[|lref|]|]; try done. iDestruct "Href" as "[Href Href†]".
+ iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
+ try iDestruct "Href" as "[_ >[]]".
+ rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
+ iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
+ rewrite -(freeable_sz_split _ 1 1). iDestruct "Href†" as "[Href†1 Href†2]".
+ destruct (Qp_lower_bound qE qν) as (q & qE' & qν' & ? & ?). subst.
+ iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
+ remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
+ iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
+ iApply (type_type ((☀ (α ∪ ν)) :: E)%EL []
+ [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&shr{α ∪ ν}ty2)])]%CC
+ [ f ◠box (fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
+ #lref ◠own_ptr 2 (&shr{α ∪ ν}ty1); env ◠box envty ]%TC
+ with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
+ rewrite heap_mapsto_vec_singleton. by iFrame. }
+ { rewrite !cctx_interp_singleton /=. iIntros "HE". iIntros (args) "Hna HL HT".
+ inv_vec args. subst. simpl. wp_rec.
+ rewrite {3}/elctx_interp big_sepL_cons /= -lft_tok_sep.
+ iDestruct "HE" as "[[Hα Hν] HE]". iSpecialize ("Hk" with "[Hα HE $HE']").
+ { rewrite /elctx_interp big_sepL_cons. iFrame. }
+ iApply ("Hk" $! [# #lref] with "Hna HL").
+ rewrite !tctx_interp_singleton !tctx_hasty_val' //.
+ iDestruct "HT" as "[Href Ḥref†2]".
+ rewrite /= -(freeable_sz_split _ 1 1). iFrame.
+ iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
+ iExists [ #lv'; #lrc].
+ rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
+ iExists ν, (q+qν')%Qp. eauto 10 with iFrame. }
+ { rewrite /elctx_interp !big_sepL_cons /= -lft_tok_sep. iFrame. }
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+ iIntros (x'). simpl_subst.
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+ iIntros (f'). simpl_subst.
+ iApply type_letalloc_1; [solve_typing..|]. iIntros (x). simpl_subst.
+ iApply (type_letcall); [simpl; solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_deref; [solve_typing|by eapply read_own_move|done|].
+ iIntros (r'). simpl_subst.
+ iApply type_assign; [solve_typing|by eapply write_own|].
+ iApply type_delete; [solve_typing..|].
+ iApply (type_jump []); solve_typing.
+ Qed.
End ref_functions.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 9fe6fa40..5c7e4844 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -23,9 +23,10 @@ Section refcell_functions.
typed_instruction_ty [] [] [] (refcell_new ty)
(fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|].
- iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ 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.
@@ -60,9 +61,10 @@ Section refcell_functions.
typed_instruction_ty [] [] [] (refcell_into_inner ty)
(fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|].
- iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ 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.
@@ -94,9 +96,11 @@ Section refcell_functions.
typed_instruction_ty [] [] [] refcell_get_mut
(fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
- iApply type_deref; [solve_typing..|by eapply read_own_move|done|]. iIntros (x'). simpl_subst.
- iIntros "!# * #LFT Hna HE HL HC HT".
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by eapply read_own_move|done|].
+ iIntros (x'). simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL HC HT".
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ zâŒ) ∗
@@ -143,15 +147,16 @@ Section refcell_functions.
typed_instruction_ty [] [] [] refcell_try_borrow
(fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply (type_cont [_] [] (λ r, [x ◠box (&shr{α} refcell ty);
r!!!0 ◠box Σ[ref α ty; unit]])%TC);
- [iIntros (k)|simpl; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
+ [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
- iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
@@ -248,15 +253,17 @@ Section refcell_functions.
typed_instruction_ty [] [] [] refcell_try_borrow_mut
(fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply (type_cont [_] [] (λ r, [x ◠box (&shr{α} refcell ty);
r!!!0 ◠box Σ[refmut α ty; unit]])%TC);
- [iIntros (k)|simpl; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
+ [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
+ simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
- iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 8f9bd748..9342af7e 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -26,9 +26,10 @@ Section refmut_functions.
(fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
(fun '(α, β) => &shr{α}ty)%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
- iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
@@ -67,9 +68,10 @@ Section refmut_functions.
(fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
(fun '(α, β) => &uniq{α}ty)%T).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
- iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
@@ -119,8 +121,9 @@ Section refmut_functions.
Lemma refmut_drop_type ty :
typed_instruction_ty [] [] [] refmut_drop (fn(∀ α, [☀α]; refmut α ty) → unit).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
- iIntros "!# * #LFT Hna Hα HL Hk Hx".
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iIntros (tid qE) "#LFT Hna Hα HL Hk Hx".
rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index 9addc231..a0c782dc 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -65,13 +65,14 @@ Section spawn.
typed_instruction_ty [] [] [] spawn
(fn([]; fn([] ; envty) → retty, envty) → join_handle retty).
Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
- iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>f env. simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>f env. simpl_subst.
iApply type_deref; [solve_typing..|exact: read_own_move|done|].
iIntros (f'). simpl_subst.
iApply (type_let _ _ _ _ ([f' â— _; env â— _]%TC)
(λ j, [j ◠join_handle retty]%TC)); try solve_typing; [|].
{ (* The core of the proof: showing that spawn is safe. *)
- iAlways. iIntros (tid qE) "#LFT $ $ $".
+ iIntros (tid qE) "#LFT $ $ $".
rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv retty tid) with "[-]");
first solve_to_val; last first; last simpl_subst.
@@ -113,11 +114,13 @@ Section spawn.
typed_instruction_ty [] [] [] join
(fn([]; join_handle retty) → retty).
Proof.
- iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>c. simpl_subst.
- iApply type_deref; [solve_typing..|exact: read_own_move|done|]. iIntros (c'); simpl_subst.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>c. simpl_subst.
+ iApply type_deref; [solve_typing..|exact: read_own_move|done|].
+ iIntros (c'); simpl_subst.
iApply (type_let _ _ _ _ ([c' â— _]%TC)
(λ r, [r ◠box retty]%TC)); try solve_typing; [|].
- { iAlways. iIntros (tid qE) "#LFT $ $ $".
+ { iIntros (tid qE) "#LFT $ $ $".
rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
iApply (join_spec with "Hc'"). iIntros "!> * Hret".
--
GitLab