changes for rustverify talk

theories/typing/lib/cell.v

@@ -8,10 +8,18 @@ Set Default Proof Using "Type".
 Section cell.
   Context `{!typeG Σ}.
 
-  Program Definition cell (ty : type) :=
-    {| ty_size := ty.(ty_size);
-       ty_own := ty.(ty_own);
-       ty_shr κ tid l := (&na{κ, tid, shrN.@l}(l ↦∗: ty.(ty_own) tid))%I |}.
+
+
+  Program Definition cell (ty : type) := {|
+    ty_size := ty.(ty_size);
+    ty_own := ty.(ty_own);
+    ty_shr κ tid l :=
+      &na{κ, tid, shrN.@l}
+         (∃ v, l ↦∗ v ∗ ty.(ty_own) tid v)
+  |}%I.
+
+
+
   Next Obligation. apply ty_size_eq. Qed.
   Next Obligation.
     iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
@@ -84,14 +92,18 @@ Section typing.
   (** The next couple functions essentially show owned-type equalities, as they
       are all different types for the identity function. *)
   (* Constructing a cell. *)
-  Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
 
-  Lemma cell_new_type ty `{!TyWf ty} : typed_val cell_new (fn(∅; ty) → cell ty).
+  Definition cell_new : val :=
+    funrec: <> ["x"] := return: ["x"].
+
+  Lemma cell_new_type ty `{!TyWf ty} :
+    typed_val cell_new (fn(∅; ty) → cell ty).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_jump; [solve_typing..|].
-    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    intros E L. iApply type_fn; [solve_typing..|].
+    iIntros "/= !#". iIntros (_ ϝ ret arg). inv_vec arg=>x.
+    simpl_subst. iApply type_jump; [solve_typing..|].
+    iIntros (???) "#LFT _ $ Hty".
+    rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   (* The other direction: getting ownership out of a cell. *)
@@ -181,49 +193,41 @@ Section typing.
       let: "c'" := !"c" in
       letalloc: "r" <-{ty.(ty_size)} !"c'" in
       "c'" <-{ty.(ty_size)} !"x";;
-      delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
+      delete [ #1; "c"] ;;
+      delete [ #ty.(ty_size); "x"] ;;
+      return: ["r"].
 
   Lemma cell_replace_type ty `{!TyWf ty} :
     typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α}(cell ty), ty) → ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
-    iApply type_deref; [solve_typing..|].
-    iIntros (c'); simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    (* Drop to Iris level. *)
-    iIntros (tid qmax) "#LFT #HE Htl HL HC".
+    (* Drop to Iris level. *) iIntros (tid qmax) "#LFT #HE Htl HL HC".
     rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iIntros "(Hr & Hc & #Hc' & Hx)".
     destruct c' as [[|c'|]|]; try done. destruct x as [[|x|]|]; try done.
     destruct r as [[|r|]|]; try done.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q') "(Htok & HL & Hclose1)"; [solve_typing..|].
     iMod (na_bor_acc with "LFT Hc' Htok Htl") as "(Hc'↦ & Htl & Hclose2)"; [solve_ndisj..|].
-    iDestruct "Hc'↦" as (vc') "[>Hc'↦ Hc'own]".
-    iDestruct (ty_size_eq with "Hc'own") as "#>%".
+    iDestruct "Hc'↦" as (vc') "[>Hc'↦ Hc'own]". iDestruct (ty_size_eq with "Hc'own") as "#>%".
     iDestruct "Hr" as "[Hr↦ Hr†]". iDestruct "Hr↦" as (vr) "[>Hr↦ Hrown]".
     iDestruct (ty_size_eq with "Hrown") as ">Heq". iDestruct "Heq" as %Heq.
-    (* FIXME: Changing the order of $Hr↦ $Hc'↦ breaks applying...?? *)
-    wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]").
-    { by rewrite Heq. }
-    { f_equal. done. }
-    iIntros "[Hr↦ Hc'↦]". wp_seq.
-    iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
-    iDestruct (ty_size_eq with "Hxown") as "#%".
-    wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]"); try by f_equal.
-    iIntros "[Hc'↦ Hx↦]". wp_seq.
+    wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]"). { by rewrite Heq. } { f_equal. done. }
+    iIntros "[Hr↦ Hc'↦]". wp_seq. iDestruct "Hx" as "[Hx↦ Hx†]".
+    iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]". iDestruct (ty_size_eq with "Hxown") as "#%".
+    wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]"); try by f_equal. iIntros "[Hc'↦ Hx↦]". wp_seq.
     iMod ("Hclose2" with "[Hc'↦ Hxown] Htl") as "[Htok Htl]"; first by auto with iFrame.
     iMod ("Hclose1" with "Htok HL") as "HL".
     (* Now go back to typing level. *)
-    iApply (type_type _ _ _
-           [c ◁ box (&shr{α}(cell ty)); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
+    iApply (type_type _ _ _ [c ◁ box (&shr{α}(cell ty)); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
     with "[] LFT HE Htl HL HC"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
       - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
       - iFrame. iExists _. iFrame. }
-    iApply type_delete; [solve_typing..|].
-    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|]. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.