From iris_c.vcgen Require Import proofmode.
Definition array_copy : val := λᶜ "arg",
"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)
}.
Lemma array_copy_spec `{cmonadG Σ} lxs lys xs ys n R :
length xs = n → length ys = n →
lxs ↦C∗ xs -∗ lys ↦C∗ ys -∗
CWP array_copy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs ↦C∗ ys ∗ lys ↦C∗ ys }}.
Proof.
iIntros (Hlen <-) "**". iApply cwp_fun; simpl. vcg. iIntros (p q) "**".
iApply (cwp_wand _ (λ _, ∃ p' q', p ↦C p' ∗ q ↦C q' ∗
lxs ↦C∗ ys ∗ lys ↦C∗ ys)%I with "[-]"); last first.
{ iIntros (v). iDestruct 1 as (p' q') "[??]". vcg_continue; auto. }
iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen);
destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame.
vcg; iIntros "!> !> !> **".
iSpecialize ("IH" $! (lxs +∗ 1) (lys +∗ 1) with "[//] [$] [$] [$] [$]").
rewrite !cloc_plus_plus -(Nat2Z.inj_add 1).
iApply (cwp_wand with "IH").
iIntros (v). iDestruct 1 as (p' q') "[??]". vcg_continue; eauto with iFrame.
Qed.