WIP iApply diverges

theories/typing/programs.v

@@ -11,7 +11,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, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+    (□ ∀ tid qE, heap_ctx -∗ 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.
@@ -35,7 +35,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) "#HEAP #LFT Htl HE HL HC HT".
     iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
     iApply ("H" with "HEAP LFT Htl HE HL [HC] HT").
@@ -49,33 +49,33 @@ Section typing.
 
   (** Instruction *)
   Definition typed_instruction (E : elctx) (L : llctx)
-             (T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
-    ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+             (T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
+    (□ ∀ tid qE, heap_ctx -∗ 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) }}.
-  Global Arguments typed_instruction _%EL _%LL _%TC _%E _.
+                         llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
+  Global Arguments typed_instruction _%EL _%LL _%TC _%E _%TC.
 
   (** Writing and Reading **)
-  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
-    ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
+  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
+    (□ ∀ 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 ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
-            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
      mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
      make work for some of the provers way harder, since they'd have to show
      that nobody could possibly have changed the vl (because only half the
      fraction was given). So we go with the definition that is easier to prove. *)
-  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
-    ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
+  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
+    (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
       lft_ctx -∗ na_own tid F -∗
       elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
               (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗
-                              llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+                              llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty :=
@@ -91,7 +91,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 tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (He) "!#". iIntros (tid qE) "#HEAP #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 "HEAP LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
@@ -106,7 +106,7 @@ 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) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
+    iIntros (Hc He He') "!#". iIntros (tid qE) "#HEAP #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]").
     { iApply (He with "HEAP LFT Htl HE HL HT1"). }
     iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
@@ -130,7 +130,7 @@ Section typing_rules.
     (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
     typed_body E L C T (Newlft ;; e).
   Proof.
-    iIntros (Hc He tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (Hc He) "!#". iIntros (tid qE) "#HEAP #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 "HEAP LFT Htl HE [HL Htk] HC HT").
@@ -144,7 +144,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 tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
+    iIntros (Hc Hub He) "!#". iIntros (tid qE) "#HEAP #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.
     iApply (wp_fupd_step with "Hend"); try done. wp_seq.
@@ -156,11 +156,11 @@ 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 tid qE) "#HEAP #LFT $ HE HL".
+    iIntros (Hwrt) "!#". iIntros (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.
+    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.
@@ -175,10 +175,10 @@ 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 tid qE) "#HEAP #LFT Htl HE HL Hp".
+    iIntros (Hsz Hread) "!#". iIntros (tid qE) "#HEAP #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
+    iMod (Hread with "* [] LFT Htl HE HL Hown") as
         (l vl q) "(% & Hl & Hown & Hclose)"; first done.
     subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
     { rewrite -Hsz. iApply ty_size_eq. done. }
@@ -190,19 +190,20 @@ Section typing_rules.
   Qed.
 
   Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' n p1 p2 :
-    ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
+    ty.(ty_size) = n →
+    typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
       (p1 <⋯ !{n}p2)
     {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
-    iIntros (Hsz Hwrt Hread Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
+    iIntros (Hsz) "#Hwrt #Hread !#". iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
     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 HE1 HL1 Hown1")
+    iMod ("Hwrt" with "* [] LFT HE1 HL1 Hown1")
       as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
-    iMod (Hread with "* LFT Htl HE2 HL2 Hown2")
+    iMod ("Hread" with "* [] LFT Htl HE2 HL2 Hown2")
       as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
     iAssert (▷⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%".
     { by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
@@ -218,8 +219,8 @@ Section typing_rules.
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
-    iIntros (Hsz Hwrt Hread tid qE) "#HEAP #LFT Htl HE HL HT".
-    iApply (type_memcpy_iris with "[$HEAP $LFT $Htl $HE $HL HT]"); try done.
+    iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
+    iApply (type_memcpy_iris with "* [] [] []"). [$HEAP $LFT $Htl $HE $HL HT]"). ; try done.
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.