From 5ca9b8b661e5a543e5d720b21a2d9f75dd7cb7a6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 21 Dec 2016 23:55:39 +0100
Subject: [PATCH] show typing of memcpy

---
 theories/lang/memcpy.v     |  2 +-
 theories/typing/programs.v | 22 +++++++++++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 7c427006..ca2fe83d 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -7,7 +7,7 @@ Definition memcpy : val :=
     if: "len" ≤ #0 then #()
     else "dst" <- !"src";;
          "memcpy" ["dst" +â‚— #1 ; "len" - #1 ; "src" +â‚— #1].
-Opaque memcpy.
+Global Opaque memcpy.
 
 Notation "e1 <-{ n } ! e2" := (App memcpy [e1%E ; Lit (LitInt n) ; e2%E])
   (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 25ba68e7..35d93b86 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation.
-From lrust.lang Require Import proofmode.
+From lrust.lang Require Import proofmode memcpy.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 
@@ -121,4 +121,24 @@ Section typing_rules.
     by iFrame.
   Qed.
 
+  Lemma type_memcpy E L ty1 ty1' ty2 ty2' ty n p1 p2 :
+    ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
+    typed_instruction E L [TCtx_hasty p1 ty1; TCtx_hasty p2 ty2] (p1 <-{n} !p2)
+                          (λ _, [TCtx_hasty p1 ty1'; TCtx_hasty p2 ty2']).
+  Proof.
+    iIntros (Hsz Hwrt Hread tid qE) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2]".
+    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 HE1 HL1 Hown1") as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
+    iMod (Hread with "* LFT Htl HE2 HL2 Hown2") as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
+    iAssert (▷⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%".
+    { by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
+    iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
+    iNext. iIntros "[Hl1 Hl2]". iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
+    { iExists _. iFrame. }
+    iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.
+  Qed.
+
 End typing_rules.
-- 
GitLab