typed_instr and typed_body need the heap_ctx; prove assignment (based on typed_writing)

c8f39283 · Ralf Jung · cf158914 · c8f39283 · c8f39283 · c8f39283
Commit c8f39283 authored 8 years ago by Ralf Jung
--- 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 (He1 with "HEAP LFT HE HL HC HT").
-    - iApply (He2 with "LFT HE HL HC HT").
+    - iApply (He2 with "HEAP LFT HE HL HC HT").
  Qed.
 End typing.
--- 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.

--- 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".
+    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE #HL HC HT".
-    iApply ("Hf" with "* LFT [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.

--- 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".

--- 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↦".

--- 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 Σ :=
+             (T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
-    (∀ tid qE, □ (lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+    ∀ 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) }}))%I.
+                   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 →
+    ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
-      lft_ctx -∗ ty1.(ty_own) tid [v] ={E}=∗
+      lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
-        ∃ l vl, ⌜length vl = ty.(ty_size)⌝ ∗ l ↦∗ vl ∗
+        ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
-        ∀ vl', l ↦∗ vl' -∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ty2.(ty_own) tid [v].
+        ∀ 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.
--- 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) -∗