change semantics of typed_writing to make proofs simpler

theories/typing/bool.v

@@ -30,7 +30,7 @@ Section typing.
     (* FIXME why can't I merge these two iIntros? *)
     iIntros (He1 He2). iIntros (tid qE) "#LFT HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hp HT]".
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "% Hown".
+    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").

theories/typing/int.v

@@ -28,8 +28,8 @@ Section typing.
   Proof.
     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".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
     iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
     iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
     wp_op. rewrite tctx_interp_singleton. iExists _. iSplitR; first done.
@@ -41,8 +41,8 @@ Section typing.
   Proof.
     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".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
     iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
     iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
     wp_op. rewrite tctx_interp_singleton. iExists _. iSplitR; first done.
@@ -54,8 +54,8 @@ Section typing.
   Proof.
     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".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
     iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
     iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
     wp_op; intros _; rewrite tctx_interp_singleton; iExists _; (iSplitR; first done);

theories/typing/own.v

@@ -142,20 +142,16 @@ 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 ?) "_ Hp HΦ". iApply wp_fupd. iApply (wp_hasty with "Hp").
-    iIntros (v) "Hp Hown". iDestruct "Hp" as %Hp.
-    iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (Hsz p tid F ?) "_ 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 ">%".
-    iApply ("HΦ" with "* [%] [] H↦"); [congruence|done|].
-    iIntros (vl') "H↦ Hown' !>". iExists _. iSplit; first done.
+    iDestruct "Hown" as ">%". iModIntro. iExists _, _. iFrame "H↦".
+    iSplit; first by rewrite Hsz. iIntros (vl') "H↦ Hown' !>".
     iExists _. iSplit; first done. rewrite Hsz. iFrame "H†".
     iExists _. iFrame.
   Qed.
 
   (* Old Typing *)
-
   Lemma consumes_copy_own ty n:
     Copy ty → consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n ty)%P.
   Proof.

theories/typing/programs.v

@@ -46,13 +46,10 @@ Section typing.
 
   (** Writing and Reading **)
   Definition typed_writing (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
-    ∀ p tid Φ E, lftE ∪ (↑lrustN) ⊆ E →
-      lft_ctx -∗ tctx_elt_interp tid (TCtx_hasty p ty1) -∗
-      (∀ (l:loc) vl,
-         ⌜length vl = ty.(ty_size)⌝ -∗ ⌜eval_path p = Some #l⌝ -∗ l ↦∗ vl -∗
-           (∀ vl', l ↦∗ vl' -∗ ▷ (ty.(ty_own) tid vl') ={E}=∗
-                           tctx_elt_interp tid (TCtx_hasty p ty2)) -∗ Φ #l) -∗
-      WP p @ E {{ Φ }}.
+    ∀ 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].
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).

theories/typing/type_context.v

@@ -24,12 +24,29 @@ Section type_context.
     eval_path v = Some v.
   Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
 
+  Lemma wp_eval_path E p v :
+    eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
+  Proof.
+    revert v; induction p; intros v; cbn -[to_val];
+      try (intros ?; by iApply wp_value); [].
+    destruct op; try discriminate; [].
+    destruct p2; try (intros ?; by iApply wp_value); [].
+    destruct l; try (intros ?; by iApply wp_value); [].
+    destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
+    destruct v0; try discriminate; [].
+    destruct l; try discriminate; [].
+    intros [=<-]. iStartProof. wp_bind p1.
+    iApply (wp_wand with "[]").
+    { iApply IHp1. done. }
+    iIntros (v) "%". subst v. wp_op. done.
+  Qed.
+
+  (** Type context element *)
   (* TODO: Consider mking this a pair of a path and the rest. We could
      then e.g. formulate tctx_elt_hasty_path more generally. *)
   Inductive tctx_elt : Type :=
   | TCtx_hasty (p : path) (ty : type)
   | TCtx_blocked (p : path) (κ : lft) (ty : type).
-  Definition tctx := list tctx_elt.
 
   Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
     match x with
@@ -40,6 +57,34 @@ Section type_context.
   (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
   Global Arguments tctx_elt_interp : simpl never.
 
+  Lemma tctx_hasty_val tid (v : val) ty :
+    tctx_elt_interp tid (TCtx_hasty v ty) ⊣⊢ ty.(ty_own) tid [v].
+  Proof.
+    rewrite /tctx_elt_interp eval_path_of_val. iSplit.
+    - iIntros "H". iDestruct "H" as (?) "[EQ ?]".
+      iDestruct "EQ" as %[=->]. done.
+    - iIntros "?". iExists _. auto.
+  Qed.
+
+  Lemma tctx_elt_interp_hasty_path p1 p2 ty tid :
+    eval_path p1 = eval_path p2 →
+    tctx_elt_interp tid (TCtx_hasty p1 ty) ≡
+    tctx_elt_interp tid (TCtx_hasty p2 ty).
+  Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. 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) -∗
+    WP p @ E {{ Φ }}.
+  Proof.
+    iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
+    iApply (wp_wand with "[]"). { iApply wp_eval_path. done. }
+    iIntros (v') "%". subst v'. iApply ("HΦ" with "* [] Hown"). by auto.
+  Qed.
+
+  (** Type context *)
+  Definition tctx := list tctx_elt.
+
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
 
@@ -101,39 +146,6 @@ Section type_context.
       by iMod (H2 with "LFT HE HL H") as "($ & $ & $)".
   Qed.
 
-  Lemma tctx_elt_interp_hasty_path p1 p2 ty tid :
-    eval_path p1 = eval_path p2 →
-    tctx_elt_interp tid (TCtx_hasty p1 ty) ≡
-    tctx_elt_interp tid (TCtx_hasty p2 ty).
-  Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
-
-  Lemma wp_eval_path E p v :
-    eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
-  Proof.
-    revert v; induction p; intros v; cbn -[to_val];
-      try (intros ?; by iApply wp_value); [].
-    destruct op; try discriminate; [].
-    destruct p2; try (intros ?; by iApply wp_value); [].
-    destruct l; try (intros ?; by iApply wp_value); [].
-    destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
-    destruct v0; try discriminate; [].
-    destruct l; try discriminate; [].
-    intros [=<-]. iStartProof. wp_bind p1.
-    iApply (wp_wand with "[]").
-    { iApply IHp1. done. }
-    iIntros (v) "%". subst v. wp_op. 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) -∗
-    WP p @ E {{ Φ }}.
-  Proof.
-    iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
-    iApply (wp_wand with "[]"). { iApply wp_eval_path. done. }
-    iIntros (v') "%". subst v'. iApply ("HΦ" with "* [] Hown"). by auto.
-  Qed.
-
   Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
   Proof.
     rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_contains.