experiment with writing rules as Hoare triples (for proofs about unsafe code)

theories/typing/fixpoint.v

@@ -8,9 +8,6 @@ Section fixpoint.
 
   Context (T : type → type) `{Contractive T}.
 
-  (* FIXME : Contrarily to the rule on paper, these rules are
-     coinductive: they let one assume [ty] is [Copy]/[Send]/[Sync] to
-     prove that [T ty] is [Copy]/[Send]/[Sync]. *)
   Global Instance fixpoint_copy :
     (∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
   Proof.

theories/typing/programs.v

@@ -157,13 +157,15 @@ Section typing_rules.
     by iFrame.
   Qed.
 
-  Lemma type_memcpy E L ty1 ty1' ty2 ty2' ty n p1 p2 :
+  Lemma type_memcpy_iris E qE L qL tid ty1 ty1' ty2 ty2' ty n p1 p2 :
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
-                      (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
+    {{{ 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 tid qE) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2]".
-    rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
+    iIntros (Hsz Hwrt Hread Φ) "(#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")
@@ -173,9 +175,20 @@ Section typing_rules.
     iAssert (▷⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%".
     { by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
     iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
-    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-    iNext. iIntros "[Hl1 Hl2]". iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
+    iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with ">"). rewrite !tctx_hasty_val' //.
+    iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
     { iExists _. iFrame. }
     iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.
   Qed.
+
+  Lemma type_memcpy E L ty1 ty1' ty2 ty2' ty n p1 p2 :
+    ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
+    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.
+    { by rewrite tctx_interp_cons tctx_interp_singleton. }
+    rewrite tctx_interp_cons tctx_interp_singleton. auto.
+  Qed.
 End typing_rules.