From f4e566ec50d966cd156c900defc7839be355be11 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 13 Feb 2017 15:38:46 +0100
Subject: [PATCH] refcell: split switching back to the type system and chekcing
 the first instruction into two steps

---
 theories/typing/examples/option_as_mut.v      |  4 +-
 theories/typing/type_sum.v                    | 12 +++---
 theories/typing/unsafe/refcell/ref_code.v     | 16 ++++----
 theories/typing/unsafe/refcell/refcell_code.v | 38 ++++++++++---------
 theories/typing/unsafe/refcell/refmut_code.v  | 26 ++++++-------
 5 files changed, 50 insertions(+), 46 deletions(-)

diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/examples/option_as_mut.v
index aef773a7..2ede4418 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -25,9 +25,9 @@ Section option_as_mut.
       eapply type_new; [solve_typing..|]. intros r. simpl_subst.
       eapply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
-      + eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
+      + eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
         eapply (type_jump [_]); solve_typing.
-      + eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
+      + eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
         eapply (type_jump [_]); solve_typing.
     - move=>/= k r. inv_vec r=>r. simpl_subst.
       eapply type_delete; [solve_typing..|].
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index a529af73..7fa40e16 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -142,11 +142,11 @@ Section case.
   Qed.
 
   Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
-    typed_write E L ty1 (sum tyl) ty2 →
     tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]%TC).
   Proof.
-    iIntros (Hw Hty) "!# * #LFT $ HE HL Hp".
+    iIntros (Hty Hw) "!# * #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.
@@ -171,8 +171,8 @@ Section case.
     Closed [] e →
     0 ≤ i →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
-    typed_write E L ty1 (sum tyl) ty1' →
     tyl !! (Z.to_nat i) = Some ty →
+    typed_write E L ty1 (sum tyl) ty1' →
     typed_body E L C ((p1 ◁ ty1') :: T') e →
     typed_body E L C T (p1 <-{Σ i} p2 ;; e).
   Proof.
@@ -199,8 +199,8 @@ Section case.
     Closed [] e →
     0 ≤ i →
     tctx_extract_hasty E L p ty1 T T' →
-    typed_write E L ty1 (sum tyl) ty1' →
     tyl !! (Z.to_nat i) = Some unit →
+    typed_write E L ty1 (sum tyl) ty1' →
     typed_body E L C ((p ◁ ty1') :: T') e →
     typed_body E L C T (p <-{Σ i} () ;; e).
   Proof.
@@ -249,14 +249,14 @@ Section case.
     Closed [] e →
     0 ≤ i →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
+    tyl !! (Z.to_nat i) = Some ty →
     typed_write E L ty1 (sum tyl) ty1' →
     typed_read E L ty2 ty ty2' →
     Z.of_nat (ty.(ty_size)) = n →
-    tyl !! (Z.to_nat i) = Some ty →
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
     typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
   Proof.
-    intros ???? Hr ???. subst. rewrite -(Z2Nat.id i) //.
+    intros ????? Hr ??. subst. rewrite -(Z2Nat.id i) //.
     by eapply type_seq; [done|eapply type_sum_memcpy_instr, Hr|done|done].
   Qed.
 End case.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 3c816d24..8eb9adc2 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -99,12 +99,13 @@ Section ref_functions.
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα1".
     iAssert (elctx_interp [☀ α; ☀ β] qE) with "[Hα1 Hα2 Hβ]" as "HE".
     { rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
-    iApply (type_delete _ _
+    iApply (type_type _ _ _
         [ x ◁ box (uninit 1); #lr ◁ box(ref β ty)]%TC with "LFT Hna HE HL Hk");
-      [solve_typing..| |]; first last.
+        first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
       iFrame "∗#". }
+    eapply type_delete; [solve_typing..|].
     eapply (type_jump [ #_]); solve_typing.
   Qed.
 
@@ -139,11 +140,11 @@ Section ref_functions.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα".
     iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα Hβ Hαβ]" as "HE".
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
-    iApply (type_letalloc_1 (&shr{α}ty) _
-        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "LFT Hna HE HL Hk");
-      [solve_typing..| |]; first last.
+    iApply (type_type _ _ _
+        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "LFT Hna HE HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "LFT [] Hshr"). by iApply lft_incl_glb. }
+    eapply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     intros r. simpl_subst. eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
@@ -200,10 +201,11 @@ Section ref_functions.
     iMod ("Hcloseα" with "Hβ") as "Hα".
     iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
     { by rewrite /elctx_interp big_sepL_singleton. }
-    iApply (type_delete _ _ [ #lx ◁ box (uninit 2)]%TC with "LFT Hna HE HL Hk");
-      [solve_typing..| |]; first last.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "LFT Hna HE HL Hk");
+      first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+    eapply type_delete; [solve_typing..|].
     eapply type_new; [solve_typing..|]=>r. simpl_subst.
     eapply (type_jump [_]); solve_typing.
   Qed.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index ce279bc1..1dc95b9c 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -73,12 +73,13 @@ Section refcell_functions.
     iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
     iIntros "!> [Hr↦ Hx↦1]". wp_seq.
-    iApply (type_delete _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
-        with "LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
+        with "LFT Hna HE HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
       - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
       - iExists vl. iFrame. }
+    eapply type_delete; [solve_typing..|].
     eapply (type_jump [ #_]); solve_typing.
   Qed.
 
@@ -108,12 +109,12 @@ Section refcell_functions.
         iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
     destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
-    iApply (type_assign _ _ _ _
+    iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
-            with "LFT Hna HE HL HC [-]");
-      [solve_typing..|by apply write_own| |]; last first.
+            with "LFT Hna HE HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
+    eapply type_assign; [solve_typing..|exact: write_own|].
     eapply (type_jump [ #_]); solve_typing.
   Qed.
 
@@ -162,11 +163,12 @@ Section refcell_functions.
         first by iExists st; iFrame.
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [ref α ty; unit] _ _ _ _
+      iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|done| |]; first last.
+              with "LFT Hna HE HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      eapply (type_sum_assign_unit [ref α ty; unit]);
+        [solve_typing..|by eapply write_own|]; first last.
       simpl. eapply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
@@ -209,16 +211,17 @@ Section refcell_functions.
       iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [ref α ty; unit] _ _ _ _ _ _ _ _
+      iApply (type_type  _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]%TC
               with "LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
         first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_glb_mono. done. iApply lft_incl_refl. }
+      eapply (type_sum_memcpy [ref α ty; unit]);
+        [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
       simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
   Qed.
 
@@ -280,26 +283,27 @@ Section refcell_functions.
         iApply "Hbh". rewrite -lft_dead_or. auto. }
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [refmut α ty; unit] _ _ _ _ _ _ _ _
+      iApply (type_type _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]%TC
-              with "LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
-        first last.
+              with "LFT Hna HE HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_glb_mono; first done. iApply lft_incl_refl. }
+      eapply (type_sum_memcpy [refmut α ty; unit]);
+        [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
       simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
     - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
         first by iExists st; iFrame.
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [refmut α ty; unit] _ _ _ _
+      iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|done| |]; first last.
+              with "LFT Hna HE HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      eapply (type_sum_assign_unit [refmut α ty; unit]);
+        [solve_typing..|by eapply write_own|].
       simpl. eapply (type_jump [_]); solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 88819e74..04e083f8 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -43,14 +43,13 @@ Section refmut_functions.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
-    iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα1 Hα2 Hβ Hαβ]" as "HE".
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
-    iApply (type_letalloc_1 (&shr{α}ty) _
-        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "LFT Hna HE HL Hk");
-      [solve_typing..| |]; first last.
+    iApply (type_type [☀ α; ☀ β; α ⊑ β]%EL _ _ [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC
+            with "LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "LFT [] Hshr'"). iApply lft_incl_glb; first done.
       iApply lft_incl_refl. }
+    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+    eapply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     intros r. simpl_subst. eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
@@ -99,14 +98,13 @@ Section refmut_functions.
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
-    iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα Hβ Hαβ]" as "HE".
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
-    iApply (type_letalloc_1 (&uniq{α}ty) _
-        [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC with "LFT Hna HE HL Hk");
-      [solve_typing..| |]; first last.
+    iApply (type_type [☀ α; ☀ β; α ⊑ β]%EL _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC
+            with "LFT Hna [Hα Hβ Hαβ] HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb").
       by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
+    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+    eapply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     intros r. simpl_subst. eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
@@ -149,12 +147,12 @@ Section refmut_functions.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
       apply cancel_local_update_empty, _. }
     iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
-    iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
-    { by rewrite /elctx_interp big_sepL_singleton. }
-    iApply (type_delete _ _ [ #lx ◁ box (uninit 2)]%TC with "LFT Hna HE HL Hk");
-      [solve_typing..| |]; first last.
+    iApply (type_type [☀ α]%EL _ _ [ #lx ◁ box (uninit 2)]%TC
+            with "LFT Hna [Hα] HL Hk"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+    { by rewrite /elctx_interp big_sepL_singleton. }
+    eapply type_delete; [solve_typing..|].
     eapply type_new; [solve_typing..|]=>r. simpl_subst.
     eapply (type_jump [_]); solve_typing.
   Qed.
-- 
GitLab