From c8f3928306269dccff2aa230179a982155da4007 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 21 Dec 2016 16:07:33 +0100
Subject: [PATCH] typed_instr and typed_body need the heap_ctx; prove
assignment (based on typed_writing)
---
theories/typing/bool.v | 8 +++---
theories/typing/cont.v | 8 +++---
theories/typing/function.v | 22 ++++++++--------
theories/typing/int.v | 8 +++---
theories/typing/own.v | 2 +-
theories/typing/programs.v | 48 +++++++++++++++++++++++++---------
theories/typing/type_context.v | 8 ++++++
7 files changed, 67 insertions(+), 37 deletions(-)
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 4230b62c..f8b6c3f1 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -19,7 +19,7 @@ Section typing.
Lemma type_bool (b : Datatypes.bool) E L :
typed_instruction_ty E L [] #b bool.
Proof.
- iIntros (tid qE) "!# _ $ $ _". wp_value. rewrite tctx_interp_singleton.
+ iIntros (tid qE) "_ _ $ $ _". wp_value. rewrite tctx_interp_singleton.
iExists _. iSplitR; first done. iExists _. done.
Qed.
@@ -28,12 +28,12 @@ Section typing.
typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
Proof.
(* FIXME why can't I merge these two iIntros? *)
- iIntros (He1 He2). iIntros (tid qE) "#LFT HE HL HC".
+ iIntros (He1 He2). iIntros (tid qE) "#HEAP #LFT HE HL HC".
rewrite tctx_interp_cons. iIntros "[Hp HT]".
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
destruct b; wp_if.
- - iApply (He1 with "LFT HE HL HC HT").
- - iApply (He2 with "LFT HE HL HC HT").
+ - iApply (He1 with "HEAP LFT HE HL HC HT").
+ - iApply (He2 with "HEAP LFT HE HL HC HT").
Qed.
End typing.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index be7f6344..4189b543 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -12,7 +12,7 @@ Section typing.
tctx_incl E L T (T' args) →
typed_body E L [CCtx_iscont k L n T'] T (k (of_val <$> (args : list _))).
Proof.
- iIntros (Hincl tid qE) "#LFT HE HL HC HT".
+ iIntros (Hincl tid qE) "#HEAP #LFT HE HL HC HT".
iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
iSpecialize ("HC" with "HE * []"); first by (iPureIntro; apply elem_of_list_singleton).
simpl. iApply ("HC" with "* HL HT").
@@ -25,16 +25,16 @@ Section typing.
(∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 n T' :: C) T (subst' kb k e2)) →
typed_body E (L1 ++ L2) C T (let: kb := e1 in e2).
Proof.
- iIntros (-> Hc1 Hc2 Hecont He2 tid qE) "#LFT HE HL HC HT". iApply wp_let'.
+ iIntros (-> Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
- iModIntro. iApply (He2 with "* LFT HE HL [HC] HT"). clear He2.
+ iModIntro. iApply (He2 with "* HEAP LFT HE HL [HC] HT"). clear He2.
iIntros "HE". iLöb as "IH". iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
iIntros (args) "HL HT". iApply wp_rec; try done.
{ apply Forall_of_val_is_val. }
{ rewrite -vec_to_list_map -subst_vec_eq. eauto. }
(* FIXME: iNext here unfolds things in the context. *)
- iNext. iApply (Hecont with "* LFT HE HL [HC] HT").
+ iNext. iApply (Hecont with "* HEAP LFT HE HL [HC] HT").
by iApply "IH".
Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 44f8af54..7255a4e5 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -32,9 +32,9 @@ Section typing.
Proof.
intros Htys Hty. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
- iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * _ HE HL HC HT".
+ iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE HL HC HT".
iDestruct (elctx_interp_persist with "HE") as "#HE'".
- iApply ("Hf" with "* LFT HE HL [HC] [HT]").
+ iApply ("Hf" with "* HEAP LFT HE HL [HC] [HT]").
- iIntros "HE". unfold cctx_interp. iIntros (e) "He".
iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "HL HT".
iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
@@ -75,9 +75,9 @@ Section typing.
Proof.
intros HEE'. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
- iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * _ HE #HL HC HT".
+ iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE #HL HC HT".
iMod (HEE' x with "[%] HE HL") as (qE') "[HE Hclose]". done.
- iApply ("Hf" with "* LFT HE HL [Hclose HC] HT"). iIntros "HE".
+ iApply ("Hf" with "* HEAP LFT HE HL [Hclose HC] HT"). iIntros "HE".
iApply fupd_cctx_interp. iApply ("HC" with ">").
by iMod ("Hclose" with "HE") as "[$ _]".
Qed.
@@ -88,8 +88,8 @@ Section typing.
Proof.
intros Hκκ'. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
- iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * _ HE #HL HC HT".
- iApply ("Hf" with "* LFT [HE] HL [HC] HT").
+ iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE #HL HC HT".
+ iApply ("Hf" with "* HEAP LFT [HE] HL [HC] HT").
{ rewrite /elctx_interp big_sepL_cons. iFrame. iApply (Hκκ' with "HE0 HL0"). }
rewrite /elctx_interp big_sepL_cons. iIntros "[_ HE]". by iApply "HC".
Qed.
@@ -100,7 +100,7 @@ Section typing.
typed_body E L [CCtx_iscont k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
(TCtx_hasty p (fn E' tys ty) :: T) (p (of_val k :: ps)).
Proof.
- iIntros (HTsat HEsat tid qE) "#LFT HE HL HC".
+ iIntros (HTsat HEsat tid qE) "#HEAP #LFT HE HL HC".
rewrite tctx_interp_cons. iIntros "[Hf HT]".
wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
@@ -126,7 +126,7 @@ Section typing.
iDestruct "Hf" as (f) "[EQ #Hf]". iDestruct "EQ" as %[=->].
iSpecialize ("Hf" $! x vl k).
iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done.
- iApply ("Hf" with "LFT HE' [] [HC Hclose HT']").
+ iApply ("Hf" with "HEAP LFT HE' [] [HC Hclose HT']").
+ by rewrite /llctx_interp big_sepL_nil.
+ iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
@@ -147,16 +147,16 @@ Section typing.
(subst' fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
typed_instruction_ty E L (zip_with TCtx_hasty cps ctyl) ef (fn E' tys ty).
Proof.
- iIntros (-> Hc Hbody tid qE) "!# #LFT $ $ #HT". iApply wp_value.
+ iIntros (-> Hc Hbody tid qE) "#HEAP #LFT $ $ #HT". iApply wp_value.
{ simpl. rewrite decide_left. done. }
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ simpl. rewrite decide_left. done. }
iExists _. iSplit; first done. iAlways. clear qE.
- iIntros (x args k). iIntros (tid' qE) "_ HE HL HC HT'".
+ iIntros (x args k). iIntros (tid' qE) "_ _ HE HL HC HT'".
iApply wp_rec; try done.
{ apply Forall_of_val_is_val. }
{ rewrite -!vec_to_list_cons -vec_to_list_map -subst_vec_eq. eauto. }
- iApply (Hbody with "* LFT HE HL HC").
+ iApply (Hbody with "* HEAP LFT HE HL HC").
rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
iApply tctx_send. by iNext.
Qed.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 835cfda1..eb59fd32 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -19,14 +19,14 @@ Section typing.
Lemma type_int (z : Z) E L :
typed_instruction_ty E L [] #z int.
Proof.
- iIntros (tid qE) "!# _ $ $ _". wp_value. rewrite tctx_interp_singleton.
+ iIntros (tid qE) "_ _ $ $ _". wp_value. rewrite tctx_interp_singleton.
iExists _. iSplitR; first done. iExists _. done.
Qed.
Lemma type_plus E L p1 p2 :
typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 + p2) int.
Proof.
- iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid qE) "_ _ $ $". 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".
@@ -39,7 +39,7 @@ Section typing.
Lemma type_minus E L p1 p2 :
typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 - p2) int.
Proof.
- iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid qE) "_ _ $ $". 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".
@@ -52,7 +52,7 @@ Section typing.
Lemma type_le E L p1 p2 :
typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 ≤ p2) bool.
Proof.
- iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid qE) "_ _ $ $". 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".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 9ca354dd..78138e0b 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -142,7 +142,7 @@ Section typing.
Lemma write_own E L ty ty' n :
ty.(ty_size) = ty'.(ty_size) → typed_writing E L (own n ty') ty (own n ty).
Proof.
- iIntros (Hsz p tid F ?) "_ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+ iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
rewrite ty'.(ty_size_eq). (* This turns out to be the fastest way to apply a lemma below â–· -- at least if we're fine throwing away the premise even though the result is persistent, which in this case, we are. *)
iDestruct "Hown" as ">%". iModIntro. iExists _, _. iFrame "H↦".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 0b5ae8ba..0479a702 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -8,9 +8,10 @@ Section typing.
Context `{typeG Σ}.
(** Function Body *)
+ (* 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 -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
+ (∀ tid qE, heap_ctx -∗ lft_ctx -∗ 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.
Global Arguments typed_body _ _ _ _ _%E.
@@ -31,25 +32,26 @@ 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".
- iIntros (tid qE) "#LFT HE HL HC HT".
+ iIntros (tid qE) "#HEAP #LFT HE HL HC HT".
iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
- iApply ("H" with "LFT HE HL [HC] HT").
+ iApply ("H" with "HEAP LFT HE HL [HC] HT").
iIntros "HE". by iApply (HC with "LFT HC").
Qed.
(** Instruction *)
Definition typed_instruction (E : elctx) (L : llctx)
- (T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
- (∀ tid qE, □ (lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
- WP e {{ v, elctx_interp E qE ∗ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}))%I.
+ (T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
+ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+ WP e {{ v, elctx_interp E qE ∗ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}.
Global Arguments typed_instruction _ _ _ _%E _.
(** Writing and Reading **)
Definition typed_writing (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
- ∀ v tid E, lftE ∪ (↑lrustN) ⊆ E →
- lft_ctx -∗ ty1.(ty_own) tid [v] ={E}=∗
- ∃ l vl, ⌜length vl = ty.(ty_size)⌠∗ l ↦∗ vl ∗
- ∀ vl', l ↦∗ vl' -∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ty2.(ty_own) tid [v].
+ ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
+ lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+ ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌠∗ l ↦∗ vl ∗
+ ∀ vl', l ↦∗ vl' -∗ (ty.(ty_own) tid vl') ={F}=∗
+ elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v].
End typing.
Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).
@@ -63,10 +65,30 @@ 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' tid qE) "#LFT HE HL HC HT". rewrite tctx_interp_app.
+ iIntros (Hc He He' tid qE) "#HEAP #LFT HE HL HC HT". rewrite tctx_interp_app.
iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1]").
- { iApply (He with "LFT HE HL HT1"). }
+ { iApply (He with "HEAP LFT HE HL HT1"). }
iIntros (v) "/= (HE & HL & HT2)". iApply wp_let; first wp_done. iModIntro.
- iApply (He' with "LFT HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
+ iApply (He' with "HEAP LFT HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
Qed.
+
+ Lemma type_assign E L ty1 ty ty1' p1 p2 :
+ typed_writing E L ty1 ty ty1' →
+ typed_instruction E L [TCtx_hasty p1 ty1; TCtx_hasty p2 ty] (p1 <- p2)
+ (λ _, [TCtx_hasty p1 ty1']).
+ Proof.
+ iIntros (Hwrt tid qE) "#HEAP #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".
+ iMod (Hwrt with "* LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
+ subst v1. iAssert (⌜1%nat = ty_size tyâŒ%I) with "[#]" as %Hsz.
+ { change (1%nat) with (length [v2]). by iApply ty_size_eq. }
+ rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
+ rewrite heap_mapsto_vec_singleton. wp_write.
+ rewrite -heap_mapsto_vec_singleton.
+ iMod ("Hclose" with "* Hl Hown2") as "($ & $ & Hown)".
+ rewrite tctx_interp_singleton tctx_hasty_val' //.
+ Qed.
+
End typing_rules.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 7fb79ab5..0bac33bd 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -72,6 +72,14 @@ Section type_context.
tctx_elt_interp tid (TCtx_hasty p2 ty).
Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
+ Lemma tctx_hasty_val' tid p (v : val) ty :
+ eval_path p = Some v →
+ tctx_elt_interp tid (TCtx_hasty p ty) ⊣⊢ ty.(ty_own) tid [v].
+ Proof.
+ intros ?. rewrite -tctx_hasty_val. apply tctx_elt_interp_hasty_path.
+ rewrite eval_path_of_val. done.
+ Qed.
+
Lemma wp_hasty E tid p ty Φ :
tctx_elt_interp tid (TCtx_hasty p ty) -∗
(∀ v, ⌜eval_path p = Some v⌠-∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
--
GitLab