array_copy.v 1.3 KB
Newer Older
1
From iris_c.vcgen Require Import proofmode.
Dan Frumin's avatar
Dan Frumin committed
2

3
Definition array_copy : val := λᶜ "arg",
4 5 6 7 8 9
  "p" mut c_ret (Fst "arg");
  "q" mut c_ret (Fst (Snd "arg"));
  "n" ←ᶜ c_ret (Snd (Snd "arg"));
  "pend" ←ᶜ ∗ᶜ (c_ret "p") +∗ᶜ (c_ret "n");
  while (∗ᶜ (c_ret "p") <∗ᶜ c_ret "pend") {
    (c_ret "p" += 1) = ∗ᶜ(c_ret "q" += 1)
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  }.
Dan Frumin's avatar
Dan Frumin committed
11

12
Lemma array_copy_spec `{cmonadG Σ} lxs lys xs ys n R :
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
  length xs = n  length ys = n 
  lxs C xs - lys C ys -
15
  CWP array_copy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs C ys  lys C ys }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Proof.
17 18
  iIntros (Hlen <-) "**". iApply cwp_fun; simpl. vcg. iIntros (p q) "**".
  iApply (cwp_wand _ (λ _,  p' q', p C p'  q C q' 
19
    lxs C ys  lys C ys)%I with "[-]"); last first.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  { iIntros (v). iDestruct 1 as (p' q') "[??]". vcg_continue; auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen);
22
    destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame.
23
  vcg; iIntros "!> !> !> **".
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25
  iSpecialize ("IH" $! (lxs + 1) (lys + 1) with "[//] [$] [$] [$] [$]").
  rewrite !cloc_plus_plus -(Nat2Z.inj_add 1).
26
  iApply (cwp_wand with "IH").
27
  iIntros (v). iDestruct 1 as (p' q') "[??]". vcg_continue; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Qed.