swap

_CoqProject

@@ -22,6 +22,7 @@ theories/lang/proofmode.v
 theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/lib/memcpy.v
+theories/lang/lib/swap.v
 theories/lang/lib/new_delete.v
 theories/lang/lib/spawn.v
 theories/lang/lib/lock.v
@@ -57,6 +58,7 @@ theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
 theories/typing/lib/arc.v
+theories/typing/lib/swap.v
 theories/typing/lib/mutex/mutex.v
 theories/typing/lib/mutex/mutexguard.v
 theories/typing/lib/refcell/refcell.v

theories/lang/lib/swap.v

+From iris.base_logic.lib Require Import namespaces.
+From lrust.lang Require Export notation.
+From lrust.lang Require Import heap proofmode.
+Set Default Proof Using "Type".
+
+Definition swap : val :=
+  rec: "swap" ["p1";"p2";"len"] :=
+    if: "len" ≤ #0 then #()
+    else let: "x" := !"p1" in
+         "p1" <- !"p2";;
+         "p2" <- "x";;
+         "swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
+
+Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
+  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
+  {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
+    swap [ #l1; #l2; #n] @ E
+  {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
+Proof.
+  iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
+  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. subst n.
+    iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
+    Local Opaque Zminus.
+    wp_read; wp_let; wp_read; do 2 wp_write. do 3 wp_op.
+    iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
+    iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
+Qed.

theories/typing/lib/swap.v

+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+From lrust.lang.lib Require Import swap.
+Set Default Proof Using "Type".
+
+Section swap.
+  Context `{typeG Σ}.
+
+  Definition swap ty : val :=
+    funrec: <> ["p1"; "p2"] :=
+      let: "p1'" := !"p1" in
+      let: "p2'" := !"p2" in
+      swap ["p1'"; "p2'"; #ty.(ty_size)];;
+      delete [ #1; "p1"];; delete [ #1; "p2"];;
+      let: "r" := new [ #0] in return: ["r"].
+
+  Lemma swap_type τ `{!TyWf τ} :
+    typed_val (swap τ) (fn(∀ α, ∅; &uniq{α} τ, &uniq{α} τ) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
+      inv_vec p=>p1 p2. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (p1'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (p2'). simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk (H2 & H2' & H1 & H1' & _)".
+    rewrite !tctx_hasty_val.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
+      [solve_typing..|].
+    iDestruct (uniq_is_ptr with "H1'") as (l1) "#H1eq". iDestruct "H1eq" as %[=->].
+    iMod (bor_acc with "LFT H1' Hα1") as "[H1' Hclose1]"=>//.
+    iDestruct "H1'" as (vl1) "[>H↦1 H1']".
+    iDestruct (τ.(ty_size_eq) with "H1'") as "#>%".
+    iDestruct (uniq_is_ptr with "H2'") as (l2) "#H2eq". iDestruct "H2eq" as %[=->].
+    iMod (bor_acc with "LFT H2' Hα2") as "[H2' Hclose2]"=>//.
+    iDestruct "H2'" as (vl2) "[>H↦2 H2']".
+    iDestruct (τ.(ty_size_eq) with "H2'") as "#>%".
+    wp_apply (wp_swap with "[$H↦1 $H↦2]"); try lia. iIntros "[H↦1 H↦2]". wp_seq.
+    iMod ("Hclose" with "[>-Hna HL H1 H2 Hk] HL") as "HL".
+    { iMod ("Hclose1" with "[H2' H↦1]") as "[_ $]"; first by iExists _; iFrame.
+      by iMod ("Hclose2" with "[H1' H↦2]") as "[_ $]"; first by iExists _; iFrame. }
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ p1 ◁ box (uninit 1); p2 ◁ box (uninit 1) ]
+      with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_new _); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+End swap.