Cloning a ref.

Also : declared a canonical structure for lft as a leibniz ofe, and changed the statement of wp_memcpy, so that it unifys with any relevant goal.

_CoqProject

@@ -56,3 +56,4 @@ theories/typing/unsafe/refcell/refcell.v
 theories/typing/unsafe/refcell/ref.v
 theories/typing/unsafe/refcell/refmut.v
 theories/typing/unsafe/refcell/refcell_code.v
+theories/typing/unsafe/refcell/ref_code.v

theories/lang/memcpy.v

@@ -21,9 +21,9 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
+Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q (n : Z):
   ↑heapN ⊆ E →
-  length vl1 = n → length vl2 = n →
+  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
   {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
@@ -32,11 +32,10 @@ Proof.
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
   - iApply "HΦ". assert (n = O) by lia; subst.
     destruct vl1, vl2; try discriminate. by iFrame.
-  - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n]; try discriminate.
-    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons.
+  - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try discriminate.
+    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
     iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
-    wp_read; wp_write. replace (Z.pos (Pos.of_succ_nat n)) with (n+1) by lia.
-    do 3 wp_op. rewrite Z.add_simpl_r.
-    iApply ("IH" with "[%] [%] Hl1 Hl2"); try done.
+    Local Opaque Zminus.
+    wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
     iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
 Qed.

theories/lifetime/lifetime.v

@@ -14,6 +14,8 @@ Module Export lifetime : lifetime_sig.
   Include creation.
 End lifetime.
 
+Canonical lftC := leibnizC lft.
+
 Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.

theories/typing/type_sum.v

@@ -233,7 +233,7 @@ Section case.
     rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
     iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
     iDestruct (ty_size_eq with "Hty") as "#>%".
-    iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); try done.
+    iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); [done| |lia|].
     { rewrite take_length. lia. }
     iNext; iIntros "[H↦vl1 H↦2]".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.

theories/typing/unsafe/cell.v

@@ -161,7 +161,7 @@ Section typing.
       iDestruct ("Hown") as (vl) "[>H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as "#>%".
       iDestruct (ty_size_eq with "Hown'") as "#>%".
-      iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done..|].
+      iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done||lia..|].
       iNext. iIntros "[H↦ H↦']". rewrite {1}/elctx_interp big_opL_singleton /=.
       iMod ("Hclose" with "[H↦ Hown'] Htl") as "[$ $]".
       { iExists vl'. by iFrame. }

theories/typing/unsafe/refcell/ref_code.v

+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.refcell Require Import refcell ref.
+Set Default Proof Using "Type".
+
+Section ref_functions.
+  Context `{typeG Σ, refcellG Σ}.
+
+  Definition ref_clone : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "rc" := !("x'" +ₗ #1) in
+      let: "n" := !"rc" in
+      "rc" <- "n" + #1;;
+      letalloc: "r" <-{2} !"x'" in
+      delete [ #1; "x"];; "return" ["r"].
+
+  (* FIXME : using λ instead of fun triggers an anomaly.
+     See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
+  Lemma ref_clone_type ty :
+    typed_instruction_ty [] [] [] ref_clone
+      (fn (fun '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
+                                       (fun '(α, β) => ref β ty)%T).
+  Proof.
+    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iIntros "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']".
+    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
+    wp_op. rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
+    iDestruct "HE" as "[[Hα1 Hα2] Hβ]".
+    iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
+    iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+    iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
+    iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
+    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
+    iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_read. wp_let. wp_op. wp_write.
+    iAssert (∃ q' n, st ≡ Some (Cinr (to_agree ν, q', n)))%I with "[#]" as (q' n) "Hst".
+    { iDestruct (own_valid_2 with "H● H◯") as %[[[=]|
+         (? & st' & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
+      - iExists q, xH. iPureIntro. constructor. done.
+      - iClear "∗#".
+        revert Hle Hv=>/csum_included [ -> // | [[?[?[//]]] | [?[st''[Heq[-> Hle]]]]]].
+        revert Heq. intros [= <-]. destruct st'' as [[ag q'] n].
+        revert Hle=>/Some_included_2 /Some_pair_included
+               [/Some_pair_included_total_1 [/agree_included Heq _] _] [[Hag _] _].
+        iExists q', n. iPureIntro. repeat constructor. apply Cinlr_equiv.
+        do 2 constructor; last done. apply agree_op_inv. by rewrite comm -Heq. }
+    iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
+    destruct st' as [|[[]]|]; try by inversion Hst'. apply (inj Cinr), (inj2 pair) in Hst'.
+    destruct Hst' as [[Hst' <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv].
+    simpl. setoid_rewrite <-Hst'. clear Hst'.
+    iDestruct "INV" as (q'' ν') "(Hag & Hq'q'' & [Hν1 Hν2] & INV)".
+    iDestruct "Hag" as %<-%(inj to_agree)%leibniz_equiv.
+    iDestruct "Hq'q''" as %Hq'q''.
+    iMod (own_update with "H●") as "[H● ?]".
+    { apply auth_update_alloc,
+         (op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[[Hagv _]_].
+      split; [split|].
+      - by rewrite /= agree_idemp.
+      - change ((q''/2+q')%Qp ≤ 1%Qp)%Qc. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
+        apply Qcplus_le_mono_r, Qp_ge_0.
+      - done. }
+    wp_bind (new [ #2])%E. iApply wp_new; [done..|]. iNext. iIntros (lr ?) "(%&?&Hlr)".
+    iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
+    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
+    wp_let. wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hlr $H↦]"); [done..|].
+    iIntros "!>[Hlr H↦]". wp_seq.
+    iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
+    iMod ("Hcloseδ" with "[H↦lrc H● Hν1 INV] Hna") as "[Hδ Hna]".
+    { iExists _. rewrite Z.add_comm. iFrame. iExists _, _. iFrame. simpl.
+      rewrite agree_idemp (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+    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 _ _
+        [ x ◁ box (uninit 1); #lr ◁ box(ref β ty)]%TC with "HEAP LFT Hna HE HL Hk");
+      [solve_typing..| |]; 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_jump [ #_]); solve_typing.
+  Qed.
+End ref_functions.
\ No newline at end of file

theories/typing/unsafe/refcell/refcell.v

@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Definition refcell_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR (leibnizC lft)) fracR) posR)).
+  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) posR)).
 Class refcellG Σ :=
   RefCellG :> inG Σ (authR refcell_stR).
 
@@ -17,8 +17,8 @@ Definition Z_of_refcell_st (st : refcell_stR) : Z :=
   | Some _ => -1
   end.
 
-Definition reading_st (q : frac) (κ : lft) : refcell_stR :=
-  Some (Cinr (to_agree (κ : leibnizC lft), q, xH)).
+Definition reading_st (q : frac) (ν : lft) : refcell_stR :=
+  Some (Cinr (to_agree ν, q, xH)).
 Definition writing_st : refcell_stR := Some (Cinl (Excl ())).
 
 Definition refcellN := lrustN .@ "refcell".
@@ -108,8 +108,7 @@ Section refcell.
     clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
     - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
     - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
-      iMod (own_alloc
-         (● Some (Cinr (to_agree (ν : leibnizC _), (1/2)%Qp, n)))) as (γ) "Hst".
+      iMod (own_alloc (● Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
       iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
       { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }

theories/typing/unsafe/refcell/refcell_code.v

@@ -36,7 +36,7 @@ Section refcell_functions.
     iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
     rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦1 $Hx↦]"); [done..|].
+    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦1 $Hx↦]"); [done||lia..|].
     iIntros "!> [Hr↦1 Hx↦]". wp_seq.
     iApply (type_delete _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
         with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
@@ -70,7 +70,7 @@ Section refcell_functions.
     iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
     iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
     iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦ $Hx↦1]"); [done..|].
+    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $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 "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.