memcpy.v 1.54 KB
Newer Older
1
2
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
3
Set Default Proof Using "Type".
4

5
Definition memcpy : val :=
6
  rec: "memcpy" ["dst";"len";"src"] :=
Ralf Jung's avatar
Ralf Jung committed
7
    if: "len"  #0 then #
8
    else "dst" <- !"src";;
9
         "memcpy" ["dst" + #1 ; "len" - #1 ; "src" + #1].
10

11
Notation "e1 <-{ n } ! e2" :=
12
13
14
  (memcpy (@cons expr e1%E
          (@cons expr (Lit n)
          (@cons expr e2%E nil))))
15
  (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
16

17
18
Notation "e1 <-{ n ',Σ' i } ! e2" :=
  (e1 <-{Σ i} () ;; e1+#1 <-{n} !e2)%E
19
  (at level 80, n, i at next level,
20
   format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
21

Ralf Jung's avatar
Ralf Jung committed
22
Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
23
  Z.of_nat (length vl1) = n  Z.of_nat (length vl2) = n 
24
  {{{ l1 ↦∗ vl1  l2 ↦∗{q} vl2 }}}
25
    #l1 <-{n} !#l2 @ E
Ralf Jung's avatar
Ralf Jung committed
26
  {{{ RET #; l1 ↦∗ vl2  l2 ↦∗{q} vl2 }}}.
27
Proof.
28
  iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
29
  iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op; case_bool_decide; wp_if.
30
31
  - iApply "HΦ". assert (n = O) by lia; subst.
    destruct vl1, vl2; try discriminate. by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
33
    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
34
    iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
35
36
    Local Opaque Zminus.
    wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
37
    iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
38
Qed.