From 0f85e94ea146a3b2a0bc6c75dc8f11e308f954f0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 11 May 2018 12:44:41 +0200
Subject: [PATCH] Port single-threaded stuff in theories/typing/lib/ (except
 refcell).

---
 _CoqProject                            |   8 +
 opam                                   |   2 +-
 theories/lang/swap.v                   |  31 ++++
 theories/typing/lib/cell.v             | 217 +++++++++++++++++++++++++
 theories/typing/lib/diverging_static.v |  56 +++++++
 theories/typing/lib/fake_shared_box.v  |  36 ++++
 theories/typing/lib/option.v           |  95 +++++++++++
 theories/typing/lib/panic.v            |  25 +++
 theories/typing/lib/swap.v             |  48 ++++++
 theories/typing/lib/take_mut.v         |  68 ++++++++
 10 files changed, 585 insertions(+), 1 deletion(-)
 create mode 100644 theories/lang/swap.v
 create mode 100644 theories/typing/lib/cell.v
 create mode 100644 theories/typing/lib/diverging_static.v
 create mode 100644 theories/typing/lib/fake_shared_box.v
 create mode 100644 theories/typing/lib/option.v
 create mode 100644 theories/typing/lib/panic.v
 create mode 100644 theories/typing/lib/swap.v
 create mode 100644 theories/typing/lib/take_mut.v

diff --git a/_CoqProject b/_CoqProject
index e439a2af..733ff617 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -18,6 +18,7 @@ theories/lifetime/frac_borrow.v
 theories/lang/notation.v
 theories/lang/memcpy.v
 theories/lang/new_delete.v
+theories/lang/swap.v
 theories/typing/base.v
 theories/typing/lft_contexts.v
 theories/typing/type.v
@@ -41,3 +42,10 @@ theories/typing/cont.v
 theories/typing/function.v
 theories/typing/typing.v
 theories/typing/soundness.v
+theories/typing/lib/cell.v
+theories/typing/lib/diverging_static.v
+theories/typing/lib/fake_shared_box.v
+theories/typing/lib/option.v
+theories/typing/lib/panic.v
+theories/typing/lib/swap.v
+theories/typing/lib/take_mut.v
diff --git a/opam b/opam
index 35baa191..63606754 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-05-10.1.98c35138") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-05-11.0.57089764") | (= "dev") }
 ]
diff --git a/theories/lang/swap.v b/theories/lang/swap.v
new file mode 100644
index 00000000..2e8d497b
--- /dev/null
+++ b/theories/lang/swap.v
@@ -0,0 +1,31 @@
+From lrust.lang Require Export notation.
+From gpfsl.lang Require Import 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 `{noprolG Σ} tid 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] in tid @ 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; case_bool_decide; 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 || omega).
+    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !own_loc_na_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.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
new file mode 100644
index 00000000..f9451fee
--- /dev/null
+++ b/theories/typing/lib/cell.v
@@ -0,0 +1,217 @@
+From iris.proofmode Require Import tactics.
+From iris.bi Require Import big_op.
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+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.(tid_na_inv_pool), shrN.@l}(l ↦∗: ty.(ty_own) tid))%I |}.
+  Next Obligation. apply ty_size_eq. Qed.
+  Next Obligation.
+    iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
+  Qed.
+  Next Obligation.
+    iIntros (ty ?? tid l) "#H⊑ H". by iApply (na_bor_shorten with "H⊑").
+  Qed.
+
+  Global Instance cell_wf ty `{!TyWf ty} : TyWf (cell ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Global Instance cell_type_ne : TypeNonExpansive cell.
+  Proof. solve_type_proper. Qed.
+
+  Global Instance cell_ne : NonExpansive cell.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
+  Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
+  Proof.
+    move=>?? /eqtype_unfold EQ. iIntros (?) "HL".
+    iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE".
+    iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
+    iSplit; [done|iSplit; iIntros "!# * H"].
+    - iApply ("Hown" with "H").
+    - iApply na_bor_iff; last done. iIntros "!>!#"; iSplit; iIntros "H";
+      iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
+  Qed.
+  Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).
+  Proof. eapply cell_mono. Qed.
+  Global Instance cell_proper E L : Proper (eqtype E L ==> eqtype E L) cell.
+  Proof. by split; apply cell_mono. Qed.
+  Lemma cell_proper' E L ty1 ty2 : eqtype E L ty1 ty2 → eqtype E L (cell ty1) (cell ty2).
+  Proof. eapply cell_proper. Qed.
+
+  Global Instance cell_copy :
+    Copy ty → Copy (cell ty).
+  Proof.
+    intros ty Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
+    iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
+    (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
+    destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
+    { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
+      iDestruct "Hown" as (vl) "[H↦ #Hown]".
+      simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
+      iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
+      iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
+      { iExists vl. by iFrame. }
+      iModIntro. iSplitL "".
+      { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
+        by iApply own_loc_na_vec_nil. }
+      by iIntros "$ _". }
+    (* Now we are in the non-0 case. *)
+    iMod (na_bor_acc with "LFT Hshr Htok Htl") as "($ & Htl & Hclose)"; [solve_ndisj..|].
+    iDestruct (na_own_acc with "Htl") as "($ & Hclose')"; first by set_solver.
+    iIntros "!> Htl Hown". iPoseProof ("Hclose'" with "Htl") as "Htl".
+    by iMod ("Hclose" with "Hown Htl") as "[$ $]".
+  Qed.
+
+  Global Instance cell_send :
+    Send ty → Send (cell ty).
+  Proof. by unfold cell, Send. Qed.
+End cell.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  (* 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).
+  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.
+  Qed.
+
+  (* The other direction: getting ownership out of a cell. *)
+  Definition cell_into_inner : val := funrec: <> ["x"] := return: ["x"].
+
+  Lemma cell_into_inner_type ty `{!TyWf ty} :
+    typed_val cell_into_inner (fn(∅; cell ty) → 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.
+  Qed.
+
+  Definition cell_get_mut : val :=
+    funrec: <> ["x"] := return: ["x"].
+
+  Lemma cell_get_mut_type ty `{!TyWf ty} :
+    typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} (cell ty)) → &uniq{α} 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..|]. rewrite /tctx_incl /=.
+    iIntros (??) "_ _ $". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+    by iIntros "$".
+  Qed.
+
+  (* Reading from a cell *)
+  Definition cell_get ty : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      letalloc: "r" <-{ty.(ty_size)} !"x'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma cell_get_type ty `{!TyWf ty} `(!Copy ty) :
+    typed_val (cell_get ty) (fn(∀ α, ∅; &shr{α} (cell ty)) → ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
+    { apply (read_shr _ _ _ (cell ty)); solve_typing. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Writing to a cell *)
+  Definition cell_replace ty : val :=
+    funrec: <> ["c"; "x"] :=
+      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"].
+
+  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_new; [solve_typing..|]; iIntros (r); simpl_subst.
+    (* Drop to Iris level. *)
+    iIntros (tid) "#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 "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.
+    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]
+    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_jump; solve_typing.
+  Qed.
+
+  (* Create a shared cell from a mutable borrow.
+     Called alias::one in Rust. *)
+  Definition fake_shared_cell : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      letalloc: "r" <- "x'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma fake_shared_cell_type ty `{!TyWf ty} :
+    typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α}(cell ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iApply (type_type _ _ _ [ x ◁ box (&uniq{α}(cell ty)) ]
+            with "[] LFT HE Hna HL Hk [HT]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply (type_letalloc_1 (&shr{α}(cell ty))); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End typing.
+
+Hint Resolve cell_mono' cell_proper' : lrust_typing.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
new file mode 100644
index 00000000..b07fdb62
--- /dev/null
+++ b/theories/typing/lib/diverging_static.v
@@ -0,0 +1,56 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section diverging_static.
+  Context `{!typeG Σ}.
+
+  (* Show that we can convert any live borrow to 'static with an infinite
+     loop. *)
+  Definition diverging_static_loop (call_once : val) : val :=
+    funrec: <> ["x"; "f"] :=
+      let: "call_once" := call_once in
+      letcall: "ret" := "call_once" ["f"; "x"]%E in
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      "loop" [].
+
+  Lemma diverging_static_loop_type T F call_once
+        `{!TyWf T, !TyWf F} :
+    (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
+    typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
+    typed_val (diverging_static_loop call_once)
+              (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → ∅).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
+    (* Drop to Iris *)
+    iIntros (tid) "#LFT #HE Hna HL Hk (Hcall & Hx & Hf & _)".
+    (* We need a ϝ token to show that we can call F despite it being non-'static. *)
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & _)";
+      [solve_typing..|].
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & _ & _)";
+      [solve_typing..|].
+    iMod (lft_eternalize with "Hα") as "#Hα".
+    iAssert (type_incl (box (&shr{α} T)) (box (&shr{static} T))) as "#[_ [Hincl _]]".
+    { iApply box_type_incl. iNext. iApply shr_type_incl; first done.
+      iApply type_incl_refl. }
+    wp_let. rewrite tctx_hasty_val.
+    iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
+    - solve_typing.
+    - by rewrite /= (right_id static).
+    - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
+      iApply "Hincl". done.
+    - iClear "Hα Hincl". iIntros (r) "Htl Hϝ1 Hret". wp_rec.
+      (* Go back to the type system. *)
+      iApply (type_type _ [] _ [] with "[] LFT HE Htl [] Hk [-]"); last first.
+      { rewrite /tctx_interp /=. done. }
+      { rewrite /llctx_interp /=. done. }
+      iApply (type_cont [] [] (λ _, [])).
+      + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
+      + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
+  Qed.
+End diverging_static.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
new file mode 100644
index 00000000..038aeb51
--- /dev/null
+++ b/theories/typing/lib/fake_shared_box.v
@@ -0,0 +1,36 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section fake_shared_box.
+  Context `{typeG Σ}.
+
+  Definition fake_shared_box : val :=
+    funrec: <> ["x"] := Skip ;; return: ["x"].
+
+  Lemma fake_shared_box_type ty `{!TyWf ty} :
+    typed_val fake_shared_box
+      (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iAssert (▷ ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
+    { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
+      iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
+      iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
+      iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
+      { iApply frac_bor_iff; last done. iIntros "!>!# *".
+        rewrite own_loc_na_vec_singleton. iSplit; auto. }
+      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
+      by iApply ty_shr_mono. }
+    do 2 wp_seq.
+    iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
+            with "[] LFT [] Hna HL Hk [HT]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    { by rewrite /elctx_interp. }
+    iApply type_jump; solve_typing.
+  Qed.
+End fake_shared_box.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
new file mode 100644
index 00000000..8ac02855
--- /dev/null
+++ b/theories/typing/lib/option.v
@@ -0,0 +1,95 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing lib.panic.
+Set Default Proof Using "Type".
+
+Section option.
+  Context `{typeG Σ}.
+
+  Definition option (τ : type) := Σ[unit; τ]%T.
+
+  (* Variant indices. *)
+  Definition none := 0%nat.
+  Definition some := 1%nat.
+
+  Definition option_as_mut : val :=
+    funrec: <> ["o"] :=
+      let: "o'" := !"o" in
+      let: "r" := new [ #2 ] in
+    withcont: "k":
+      case: !"o'" of
+        [ "r" <-{Σ none} ();; "k" [];
+          "r" <-{Σ some} "o'" +ₗ #1;; "k" [] ]
+    cont: "k" [] :=
+      delete [ #1; "o"];; return: ["r"].
+
+  Lemma option_as_mut_type τ `{!TyWf τ} :
+    typed_val
+      option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
+      inv_vec p=>o. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [o ◁ _; r ◁ _])) ; [solve_typing..| |].
+    - iIntros (k). simpl_subst.
+      iApply type_case_uniq; [solve_typing..|].
+        constructor; last constructor; last constructor; left.
+      + iApply (type_sum_unit (option $ &uniq{α}τ)%T); [solve_typing..|].
+        iApply type_jump; solve_typing.
+      + iApply (type_sum_assign (option $ &uniq{α}τ)%T); [try solve_typing..|].
+        iApply type_jump; solve_typing.
+    - iIntros "/= !#". iIntros (k args). inv_vec args. simpl_subst.
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+
+  Definition option_unwrap_or τ : val :=
+    funrec: <> ["o"; "def"] :=
+      case: !"o" of
+      [ delete [ #(S τ.(ty_size)); "o"];;
+        return: ["def"];
+
+        letalloc: "r" <-{τ.(ty_size)} !("o" +ₗ #1) in
+        delete [ #(S τ.(ty_size)); "o"];; delete [ #τ.(ty_size); "def"];;
+        return: ["r"]].
+
+  Lemma option_unwrap_or_type τ `{!TyWf τ} :
+    typed_val (option_unwrap_or τ) (fn(∅; option τ, τ) → τ).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>o def. simpl_subst.
+    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+    + right. iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+    + left. iApply type_letalloc_n; [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+
+  Definition option_unwrap τ : val :=
+    funrec: <> ["o"] :=
+      case: !"o" of
+      [ let: "panic" := panic in
+        letcall: "emp" := "panic" [] in
+        case: !"emp" of [];
+
+        letalloc: "r" <-{τ.(ty_size)} !("o" +ₗ #1) in
+        delete [ #(S τ.(ty_size)); "o"];;
+        return: ["r"]].
+
+  Lemma option_unwrap_type τ `{!TyWf τ} :
+    typed_val (option_unwrap τ) (fn(∅; option τ) → τ).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>o. simpl_subst.
+    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+    + right. iApply type_let; [iApply panic_type|solve_typing|].
+        iIntros (panic). simpl_subst.
+      iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply type_case_own; solve_typing.
+    + left. iApply type_letalloc_n; [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+End option.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
new file mode 100644
index 00000000..5296c6c4
--- /dev/null
+++ b/theories/typing/lib/panic.v
@@ -0,0 +1,25 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+(* Minimal support for panic. Lambdarust does not support unwinding the
+   stack. Instead, we just end the current thread by not calling any
+   continuation.
+
+   This properly models "panic=abort", but fails to take into account the
+   trouble caused by unwinding. This is why we do not get into trouble with
+   [take_mut]. *)
+
+Section panic.
+  Context `{typeG Σ}.
+
+  Definition panic : val :=
+    funrec: <> [] := #☠.
+
+  Lemma panic_type : typed_val panic (fn(∅) → ∅).
+  Proof.
+    intros E L. iApply type_fn; [done|]. iIntros "!# *".
+    inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
+    by iApply wp_value.
+  Qed.
+End panic.
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
new file mode 100644
index 00000000..dc4886b8
--- /dev/null
+++ b/theories/typing/lib/swap.v
@@ -0,0 +1,48 @@
+From lrust.typing Require Import typing.
+From lrust.lang 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.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
new file mode 100644
index 00000000..2c1617eb
--- /dev/null
+++ b/theories/typing/lib/take_mut.v
@@ -0,0 +1,68 @@
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section code.
+  Context `{typeG Σ}.
+
+  Definition take ty (call_once : val) : val :=
+    funrec: <> ["x"; "f"] :=
+      let: "x'" := !"x" in
+      let: "call_once" := call_once in
+      letalloc: "t" <-{ty.(ty_size)} !"x'" in
+      letcall: "r" := "call_once" ["f"; "t"]%E in
+      "x'" <-{ty.(ty_size)} !"r";;
+      delete [ #1; "x"];;  delete [ #ty.(ty_size); "r"];;
+      let: "r" := new [ #0] in return: ["r"].
+
+  Lemma take_type ty fty call_once `{!TyWf ty, !TyWf fty} :
+    (* fty : FnOnce(ty) -> ty, as witnessed by the impl call_once *)
+    typed_val call_once (fn(∅; fty, ty) → ty) →
+    typed_val (take ty call_once) (fn(∀ α, ∅; &uniq{α} ty, fty) → unit).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+      inv_vec arg=>x env. simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (x'); simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]; iIntros (f'); simpl_subst.
+    iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
+    (* Switch to Iris. *)
+    iIntros (tid) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
+    rewrite !tctx_hasty_val [[x]]lock [[env]]lock [fn _]lock.
+    iDestruct (ownptr_uninit_own with "Ht") as (tl tvl) "(% & >Htl & Htl†)". subst t. simpl.
+    destruct x' as [[|lx'|]|]; try done. simpl.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & Hclose2)"; [solve_typing..|].
+    iMod (bor_acc with "LFT Hx' Hα") as "[Hx' Hclose3]"; first done.
+    iDestruct (heap_mapsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
+    wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
+    iIntros "[Htl Hx'↦]". wp_seq.
+    (* Call the function. *)
+    wp_let. unlock.
+    iApply (type_call_iris _ [ϝ] () [_; _]
+      with "LFT HE Hna [Hϝ] Hf' [Henv Htl Htl† Hx'vl]"); [solve_typing| | |].
+    { by rewrite /= (right_id static). }
+    { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. iExists _. iFrame. }
+    (* Prove the continuation of the function call. *)
+    iIntros (r) "Hna Hϝ Hr". simpl.
+    iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
+    wp_rec.
+    rewrite (right_id static).
+    wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using vec_to_list_length..|].
+    iIntros "[Hlx' Hlr]". wp_seq.
+    iMod ("Hclose3" with "[Hlx' Hrvl]") as "[Hlx' Hα]".
+    { iExists _. iFrame. }
+    iMod ("Hclose2" with "Hϝ HL") as "HL".
+    iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ x ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
+    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 code.
-- 
GitLab