typing/program.v

_CoqProject

@@ -15,6 +15,8 @@ theories/lifetime/lifetime.v
 theories/lifetime/at_borrow.v
 theories/lifetime/na_borrow.v
 theories/lifetime/frac_borrow.v
+theories/lang/notation.v
+theories/lang/memcpy.v
 theories/typing/base.v
 theories/typing/lft_contexts.v
 theories/typing/type.v
@@ -24,3 +26,4 @@ theories/typing/util.v
 theories/typing/product.v
 theories/typing/sum.v
 theories/typing/uninit.v
+theories/typing/programs.v

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-04-18.3.1e40dfb2") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-04-23.0.2e828a7c") | (= "dev") }
 ]

theories/lang/memcpy.v

+From lrust.lang Require Export notation.
+From gpfsl.lang Require Import proofmode.
+Set Default Proof Using "Type".
+
+Definition memcpy : val :=
+  rec: "memcpy" ["dst";"len";"src"] :=
+    if: "len" ≤ #0 then #☠
+    else "dst" <- !"src";;
+         "memcpy" ["dst" +ₗ #1 ; "len" - #1 ; "src" +ₗ #1].
+
+Notation "e1 <-{ n } ! e2" :=
+  (memcpy (@cons expr e1%E
+          (@cons expr (Lit n)
+          (@cons expr e2%E nil))))
+  (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
+
+Notation "e1 <-{ n ',Σ' i } ! e2" :=
+  (e1 <-{Σ i} () ;; e1 +ₗ #1 <-{n} !e2)%E
+  (at level 80, n, i at next level,
+   format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
+
+Lemma wp_memcpy `{noprolG Σ} E l1 l2 vl1 vl2 q (n : Z):
+  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
+  {{{ ⎡l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2⎤ }}}
+    #l1 <-{n} !#l2 @ E
+  {{{ RET #☠; ⎡l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2⎤ }}}.
+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]".
+    (* FIXME : change the operational semantics, we should allow
+       reading and writing poison. *)
+    destruct v2; [admit|admit|].
+    destruct v1; [admit|admit|].
+    Local Opaque Zminus.
+    wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
+    iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
+Admitted.

theories/lang/notation.v

+From gpfsl.lang Require Export notation.
+
+Notation Newlft := (Lit LitPoison) (only parsing).
+Notation Endlft := Skip (only parsing).
+
+Notation "'let:' x := e1 'in' e2" :=
+  ((Lam (@cons binder x%bind nil) e2%E) (@cons expr e1%E nil))
+  (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
+Notation "e1 ;; e2" := (let: <> := e1 in e2)%E
+  (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
+(* These are not actually values, but we want them to be pretty-printed. *)
+Notation "'let:' x := e1 'in' e2" :=
+  (LamV (@cons binder x%bind nil) e2%E (@cons expr e1%E nil))
+  (at level 102, x at level 1, e1, e2 at level 150) : val_scope.
+Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
+  (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
+
+Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
+  (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
+  (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'return:'" := "return" : expr_scope.
+
+Notation "'letcont:' k xl := e1 'in' e2" :=
+  ((Lam (@cons binder k%bind nil) e2%E) [Rec k%bind xl%bind e1%E])
+  (at level 102, k, xl at level 1, e1, e2 at level 150) : expr_scope.
+Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
+  ((Lam (@cons binder k1%bind nil) e1%E) [Rec k2%bind ((fun _ : eq k1%bind k2%bind => xl%bind) eq_refl) e2%E])
+  (only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
+
+Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"]) args))%E
+  (only parsing, at level 102, f, args, k at level 1) : expr_scope.
+Notation "'letcall:' x := f args 'in' e" :=
+  (letcont: "_k" [ x ] := e in call: f args → "_k")%E
+  (at level 102, x, f, args at level 1, e at level 150) : expr_scope.
+
+(* These notations unfortunately do not print.  Also, I don't think
+   we would even want them to print in general.
+   TODO: Introduce a Definition. *)
+Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
+  (only parsing, at level 80, format "e1  <-{Σ  i }  ()" ) : expr_scope.
+Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+ₗ#1 <- e2)%E
+  (at level 80, format "e1 <-{Σ  i }  e2") : expr_scope.

theories/typing/cont_context.v

@@ -8,8 +8,8 @@ Section cont_context_def.
   Definition cont_postcondition : tvProp Σ := True%I.
 
   Record cctx_elt : Type :=
-    CCtx_iscont { cctxe_k : base.val; cctxe_L : llctx;
-                  cctxe_n : nat; cctxe_T : vec base.val cctxe_n → tctx }.
+    CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
+                  cctxe_n : nat; cctxe_T : vec val cctxe_n → tctx }.
 End cont_context_def.
 Add Printing Constructor cctx_elt.
 
@@ -82,7 +82,7 @@ Section cont_context.
     iApply ("H" with "[%]"). by apply HC1C2.
   Qed.
 
-  Lemma cctx_incl_cons_match E k L n (T1 T2 : vec base.val n → tctx) C1 C2 :
+  Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
     cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
   Proof.
@@ -99,7 +99,7 @@ Section cont_context.
   Lemma cctx_incl_nil E C : cctx_incl E C [].
   Proof. apply incl_cctx_incl. by set_unfold. Qed.
 
-  Lemma cctx_incl_cons E k L n (T1 T2 : vec base.val n → tctx) C1 C2 :
+  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
     k ◁cont(L, T1) ∈ C1 →
     (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E C1 C2 →

theories/typing/programs.v

+From gpfsl.lang Require Import proofmode.
+From lrust.lang Require Import memcpy.
+From lrust.typing Require Export type lft_contexts type_context cont_context.
+Set Default Proof Using "Type".
+
+Section typing.
+  Context `{typeG Σ}.
+
+  (** Function Body *)
+  (* This is an iProp because it is also used by the function type. *)
+  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
+                        (e : expr) : tvPropI Σ :=
+    (∀ tid, ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡na_own tid ⊤⎤ -∗ ⎡llctx_interp L 1⎤ -∗
+               cctx_interp tid C -∗ ⎡tctx_interp tid T⎤ -∗
+               WP e {{ _, cont_postcondition }})%I.
+  Global Arguments typed_body _ _ _ _ _%E.
+
+  Global Instance typed_body_llctx_permut E :
+    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
+  Proof.
+    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body.
+    by setoid_rewrite HL.
+  Qed.
+
+  Global Instance typed_body_elctx_permut :
+    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> eq ==> (⊢)) typed_body.
+  Proof.
+    intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body.
+    by setoid_rewrite HE.
+  Qed.
+
+  Global Instance typed_body_mono E L:
+    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
+           (typed_body E L).
+  Proof.
+    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
+    iIntros (tid) "#LFT #HE Htl HL HC HT".
+    iMod (HT with "[LFT //] HE HL HT") as "(HL & HT)".
+    iApply ("H" with "LFT HE Htl HL [HC] HT").
+    iApply (HC with "LFT HE HC").
+  Qed.
+
+  Global Instance typed_body_mono_flip E L:
+    Proper (cctx_incl E ==> tctx_incl E L ==> eq ==> flip (⊢))
+           (typed_body E L).
+  Proof. intros ?????????. by eapply typed_body_mono. Qed.
+
+  (** Instruction *)
+  Definition typed_instruction (E : elctx) (L : llctx)
+             (T1 : tctx) (e : expr) (T2 : val → tctx) : tvPropI Σ :=
+    (∀ tid, ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡na_own tid ⊤⎤ -∗
+              ⎡llctx_interp L 1⎤ -∗ ⎡tctx_interp tid T1⎤ -∗
+              WP e {{ v, ⎡na_own tid ⊤⎤ ∗
+                         ⎡llctx_interp L 1⎤ ∗ ⎡tctx_interp tid (T2 v)⎤ }})%I.
+  Global Arguments typed_instruction _ _ _ _%E _.
+
+  (** Writing and Reading **)
+  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : tvPropI Σ :=
+    (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
+      ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡llctx_interp L qL⎤ -∗ ⎡ty1.(ty_own) tid [v]⎤ ={F}=∗
+        ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = VVal #l⌝ ∗ ⎡l ↦∗ vl⎤ ∗
+          (⎡▷ l ↦∗: ty.(ty_own) tid⎤ ={F}=∗
+            ⎡llctx_interp L qL⎤ ∗ ⎡ty2.(ty_own) tid [v]⎤))%I.
+  Global Arguments typed_write _ _ _%T _%T _%T.
+
+  (* Technically speaking, we could remvoe the vl quantifiaction here and use
+     mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
+     make work for some of the provers way harder, since they'd have to show
+     that nobody could possibly have changed the vl (because only half the
+     fraction was given). So we go with the definition that is easier to prove. *)
+  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : tvPropI Σ :=
+    (□ ∀ v tid F qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
+      ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡na_own tid F⎤ -∗
+      ⎡llctx_interp L qL⎤ -∗ ⎡ty1.(ty_own) tid [v]⎤ ={F}=∗
+        ∃ (l : loc) vl q, ⌜v = VVal #l⌝ ∗ ⎡l ↦∗{q} vl⎤ ∗ ⎡▷ ty.(ty_own) tid vl⎤ ∗
+              (⎡l ↦∗{q} vl⎤ ={F}=∗ ⎡na_own tid F⎤ ∗
+                              ⎡llctx_interp L qL⎤ ∗ ⎡ty2.(ty_own) tid [v]⎤))%I.
+  Global Arguments typed_read _ _ _%T _%T _%T.
+End typing.
+
+Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+    (e : expr) (ty : type) : tvPropI Σ :=
+  typed_instruction E L T e (λ v, [v ◁ ty]).
+Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
+
+Definition typed_val `{typeG Σ} (v : val) (ty : type) : Prop :=
+  ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
+Arguments typed_val _ _ _%V _%T.
+
+Section typing_rules.
+  Context `{typeG Σ}.
+
+  (* This lemma is helpful when switching from proving unsafe code in Iris
+     back to proving it in the type system. *)
+  Lemma type_type E L C T e :
+    typed_body E L C T e -∗ typed_body E L C T e.
+  Proof. done. Qed.
+
+  (* TODO: Proof a version of this that substitutes into a compatible context...
+     if we really want to do that. *)
+  Lemma type_equivalize_lft E L C T κ1 κ2 e :
+    typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e →
+    typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
+  Proof.
+    iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
+    iMod (lctx_equalize_lft with "[LFT //] Hκ") as "[Hκ1 Hκ2]".
+    iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
+    rewrite /elctx_interp /=. by iFrame.
+  Qed.
+
+  Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
+    Closed (xb :b: []) e' →
+    typed_instruction E L T1 e T2 -∗
+    (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) -∗
+    typed_body E L C (T1 ++ T) (let: xb := e in e').
+  Proof.
+    iIntros (Hc) "He He'". iIntros (tid) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
+    iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
+    { iApply ("He" with "LFT HE Htl HL HT1"). }
+    iIntros (v) "/= (Htl & HL & HT2)". wp_let.
+    iApply ("He'" with "LFT HE Htl HL HC [HT2 HT]").
+    rewrite tctx_interp_app. by iFrame.
+  Qed.
+
+  (* We do not make the [typed_instruction] hypothesis part of the
+     Iris hypotheses, because we want to preserve the order of the
+     hypotheses. The is important, since proving [typed_instruction]
+     will instantiate [T1] and [T2], and hence we know what to search
+     for the following hypothesis. *)
+  Lemma type_let E L T T' T1 T2 C xb e e' :
+    Closed (xb :b: []) e' →
+    typed_instruction E L T1 e T2 →
+    tctx_extract_ctx E L T1 T T' →
+    (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) -∗
+    typed_body E L C T (let: xb := e in e').
+  Proof.
+    unfold tctx_extract_ctx. iIntros (? He ->) "?". iApply type_let'; last done.
+    iApply He.
+  Qed.
+
+  Lemma type_seq E L T T' T1 T2 C e e' :
+    Closed [] e' →
+    typed_instruction E L T1 e (λ _, T2) →
+    tctx_extract_ctx E L T1 T T' →
+    typed_body E L C (T2 ++ T') e' -∗
+    typed_body E L C T (e ;; e').
+  Proof. iIntros. iApply (type_let E L T T' T1 (λ _, T2)); auto. Qed.
+
+  Lemma type_newlft {E L C T} κs e :
+    Closed [] e →
+    (∀ κ, typed_body E ((κ ⊑ₗ κs) :: L) C T e) -∗
+    typed_body E L C T (Newlft ;; e).
+  Proof.
+    iIntros (Hc) "He". iIntros (tid) "#LFT #HE Htl HL HC HT".
+    iMod (lft_create with "[LFT //]") as (Λ) "[Htk #Hinh]"; first done.
+    set (κ' := lft_intersect_list κs). wp_seq.
+    iApply ("He" $! (κ' ⊓ Λ) with "LFT HE Htl [HL Htk] HC HT").
+    rewrite /llctx_interp /=. iFrame "HL".
+    iExists Λ. iSplit; first done. iFrame. iModIntro. done.
+  Qed.
+
+  (* TODO: It should be possible to show this while taking only one step.
+     Right now, we could take two. *)
+  Lemma type_endlft E L C T1 T2 κ κs e :
+    Closed [] e → UnblockTctx κ T1 T2 →
+    typed_body E L C T2 e -∗ typed_body E ((κ ⊑ₗ κs) :: L) C T1 (Endlft ;; e).
+  Proof.
+    iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
+    iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
+    iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
+    iApply (wp_mask_mono (↑lftN)); first done.
+    iApply (wp_step_fupd _ ∅ with "[Hend]"); [done|set_solver| |].
+    { iMod "Hend". iModIntro. iNext. iMod "Hend". iModIntro. iApply "Hend". }
+    wp_seq. iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
+    iMod (Hub with "[] HT") as "$"; [|done]. simpl in *. subst κ.
+    rewrite -lft_dead_or. by iRight.
+  Qed.
+
+  Lemma type_path_instr {E L} p ty :
+    typed_instruction_ty E L [p ◁ ty] p ty.
+  Proof.
+    iIntros (?) "_ _ $$ [? _]".
+    iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
+    rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
+  Qed.
+
+  Lemma type_letpath {E L} ty C T T' x p e :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p ty T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ ty) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p in e).
+  Proof. iIntros. iApply type_let; [by apply type_path_instr|solve_typing|done]. Qed.
+
+  Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
+    typed_write E L ty1 ty ty1' →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']).
+  Proof.
+    iIntros (Hwrt tid) "#LFT #HE $ HL".
+    rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
+    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 HE HL Hown1") as (l vl [?[= ->]]) "(Hl & Hclose)"; first done.
+    iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
+    rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
+    rewrite own_loc_na_vec_singleton. iApply wp_fupd. wp_write.
+    rewrite -own_loc_na_vec_singleton.
+    iMod ("Hclose" with "[Hl Hown2]") as "($ & Hown)".
+    { iExists _. iFrame. }
+    rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_assign {E L} ty1 ty ty1' C T T' p1 p2 e:
+    Closed [] e →
+    tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
+    typed_write E L ty1 ty ty1' →
+    typed_body E L C ((p1 ◁ ty1') :: T') e -∗
+    typed_body E L C T (p1 <- p2 ;; e).
+  Proof. iIntros. by iApply type_seq; first apply type_assign_instr. Qed.
+
+  Lemma type_deref_instr {E L} ty ty1 ty1' p :
+    ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
+    typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]).
+  Proof.
+    iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
+    rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
+    iIntros (v) "% Hown".
+    iMod (Hread with "[] LFT HE Htl HL Hown") as
+        (l vl q [= ->]) "(Hl & Hown & Hclose)"; first done.
+    iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
+    destruct vl as [|v [|]]; try done.
+    rewrite own_loc_na_vec_singleton. iApply wp_fupd. admit. (*  wp_read. *)
+    (* iMod ("Hclose" with "Hl") as "($ & $ & Hown2)". *)
+    (* rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //. *)
+    (* by iFrame. *)
+  Admitted.
+
+  Lemma type_deref {E L} ty1 C T T' ty ty1' x p e:
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p ty1 T T' →
+    typed_read E L ty1 ty ty1' →
+    ty.(ty_size) = 1%nat →
+    (∀ (v : val), typed_body E L C ((p ◁ ty1') :: (v ◁ ty) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := !p in e).
+  Proof. iIntros. by iApply type_let; [apply type_deref_instr|solve_typing|]. Qed.
+
+  Lemma type_memcpy_iris E L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
+    {{{ ⎡lft_ctx⎤ ∗ ⎡elctx_interp E⎤ ∗ ⎡na_own tid ⊤⎤ ∗ ⎡llctx_interp L qL⎤ ∗
+        ⎡tctx_elt_interp tid (p1 ◁ ty1)⎤ ∗ ⎡tctx_elt_interp tid (p2 ◁ ty2)⎤ }}}
+      (p1 <-{n} !p2)
+    {{{ RET #☠; ⎡na_own tid ⊤⎤ ∗ ⎡llctx_interp L qL⎤ ∗
+                 ⎡tctx_elt_interp tid (p1 ◁ ty1')⎤ ∗ ⎡tctx_elt_interp tid (p2 ◁ ty2')⎤ }}}.
+  Proof.
+    iIntros (<-) "#Hwrt #Hread !#".
+    iIntros (Φ) "(#LFT & #HE & Htl & [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 HE HL1 Hown1")
+      as (l1 vl1 [?[= ->]]) "(Hl1 & Hcl1)"; first done.
+    iMod ("Hread" with "[] LFT HE Htl HL2 Hown2")
+      as (l2 vl2 q2 [= ->]) "(Hl2 & Hown2 & Hcl2)"; first done.
+    iDestruct (ty_size_eq with "Hown2") as "#>%". iApply wp_fupd.
+    iApply (wp_memcpy with "[$Hl1 $Hl2]"); try congruence; [].
+    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_instr {E L} ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
+    Z.of_nat (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']).
+  Proof.
+    iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
+    iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
+    { iApply Hwrt. }
+    { iApply Hread. }
+    { rewrite tctx_interp_cons tctx_interp_singleton. by iDestruct "HT" as "[$$]". }
+    rewrite tctx_interp_cons tctx_interp_singleton embed_sep. auto.
+  Qed.
+
+  Lemma type_memcpy {E L} ty ty1 ty2 (n : Z) C T T' ty1' ty2' p1 p2 e:
+    Closed [] e →
+    tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
+    typed_write E L ty1 ty ty1' →
+    typed_read E L ty2 ty ty2' →
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
+    typed_body E L C T (p1 <-{n} !p2;; e).
+  Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed.
+End typing_rules.
+
+Hint Opaque typed_read typed_write : lrust_typing.

theories/typing/sum.v

@@ -23,7 +23,7 @@ Section sum.
   Qed.
   Next Obligation. iIntros (κ κ' tid l) "#Hord []". Qed.
 
-  Definition is_pad i tyl (vl : list (@value.val base.val)) : vProp Σ :=
+  Definition is_pad i tyl (vl : list (@value.val val)) : vProp Σ :=
     ⌜((nth i tyl emp0).(ty_size) + length vl)%nat = (max_list_with ty_size tyl)⌝%I.
 
   Lemma split_sum_mt l tid q tyl :

theories/typing/type.v

@@ -113,7 +113,7 @@ Proof.
 Qed.
 
 Record simple_type `{typeG Σ} :=
-  { st_own : thread_id → list (@value.val base.val) → vProp Σ;
+  { st_own : thread_id → list (@value.val val) → vProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Existing Instance st_own_persistent.
@@ -166,7 +166,7 @@ Section ofe.
   Instance type_dist : Dist type := type_dist'.
 
   Let T := prodC
-    (prodC natC (thread_id -c> list (@value.val base.val) -c> vPropC Σ))
+    (prodC natC (thread_id -c> list (@value.val val) -c> vPropC Σ))
     (lft -c> thread_id -c> loc -c> vPropC Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧

theories/typing/type_context.v

@@ -22,7 +22,7 @@ Section type_context.
   Context `{typeG Σ}.
   Implicit Types T : tctx.
 
-  Fixpoint eval_path (p : path) : option base.val :=
+  Fixpoint eval_path (p : path) : option val :=
     match p with
     | BinOp OffsetOp e (Lit (LitInt n)) =>
       match eval_path e with
@@ -32,7 +32,7 @@ Section type_context.
     | e => base.to_val e
     end.
 
-  Lemma eval_path_of_val (v : base.val) :
+  Lemma eval_path_of_val (v : val) :
     eval_path v = Some v.
   Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
 
@@ -48,8 +48,7 @@ Section type_context.
     destruct v0; try discriminate; [].
     destruct l; try discriminate; [].
     intros [=<-]. wp_bind p1. iApply (wp_wand with "[]"); [by iApply IHp1|].
-    iIntros (v) "->". iApply wp_bin_op; [by constructor|done|].
-    iIntros (l' Hl') "!%". by inversion Hl'.
+    iIntros (v) "->". by wp_op.
   Qed.
 
   Lemma eval_path_closed p v :
@@ -74,7 +73,7 @@ Section type_context.
   (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
   Global Arguments tctx_elt_interp : simpl never.
 
-  Lemma tctx_hasty_val tid (v : base.val) ty :
+  Lemma tctx_hasty_val tid (v : val) ty :
     tctx_elt_interp tid (v ◁ ty) ⊣⊢ ty.(ty_own) tid [VVal v].
   Proof.
     rewrite /tctx_elt_interp eval_path_of_val. iSplit.
@@ -87,7 +86,7 @@ Section type_context.
     tctx_elt_interp tid (p1 ◁ ty) ≡ tctx_elt_interp tid (p2 ◁ ty).
   Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
 
-  Lemma tctx_hasty_val' tid p (v : base.val) ty :
+  Lemma tctx_hasty_val' tid p (v : val) ty :
     eval_path p = Some v →
     tctx_elt_interp tid (p ◁ ty) ⊣⊢ ty.(ty_own) tid [VVal v].
   Proof.