Commit 283947ec authored by Dan Frumin's avatar Dan Frumin

Add memcpy.v

parent 9f7fbaca
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Section memcpy.
Context `{amonadG Σ}.
Ltac etaprod l :=
rewrite ?Nat.add_0_r;
assert ((l.1, l.2) = l) as -> by (destruct l; auto).
Definition memcpy : val := λ: "arg",
"p" ←ᶜ a_alloc 1 (a_ret (Fst "arg"));;
let: "q" := Fst (Snd "arg") in
let: "n" := Snd (Snd "arg") in
"pend" ←ᶜ ∗ᶜ(a_ret "p") +∗ᶜ (a_ret "n");;
while (∗ᶜ(a_ret "p") <∗ᶜ (a_ret "pend"))
{ ((a_ret "p")+=ᶜ♯1) = ∗ᶜ((a_ret "q")+=ᶜ♯1) }.
Lemma memcpy_body_spec (i: nat) (pp p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
length ls2 = n
take i ls1 = take i ls2 -
p C ls1 -
q C ls2 -
pp C (#p.1, #(p.2+i)%nat) -
AWP while (∗ᶜ (a_ret (#pp.1, #pp.2)) <∗ᶜ a_ret (#p.1, #(p.2 + n)%nat))
{ (a_ret (#pp.1, #pp.2) += 1) = ∗ᶜ (a_ret (#q.1, #q.2) += 1) }
@ R {{ _, p C ls2 q C ls2 }}.
Proof.
iIntros (? ?) "Htake Hp Hq Hpp".
iLöb as "IH" forall (i). iDestruct "Htake" as %Htake.
iApply a_while_spec'.
iNext.
iApply (a_ptr_lt_spec _ _ (λ v, v = (#p.1, #(p.2+i)%nat)%V pp C (#p.1, #(p.2+i)%nat))%I with "[Hpp]").
{ vcg_solver. eauto. }
vcg_solver. iNext. iIntros (?) "[% Hpp]"; simplify_eq/=.
iExists (p.1,p.2+i)%nat,(p.1,p.2+length ls1)%nat; repeat iSplit; eauto.
destruct (decide (i < length ls1)).
- iLeft. iSplit.
{ iPureIntro. compute[cloc_lt]. f_equal. simpl.
rewrite !bool_decide_true; auto. omega. }
eapply tac_vcg_sound.
apply _. (* Separate the - ↦ - propositions out of the context*)
compute; reflexivity. (* Compute the known locations *)
apply _. (* Compute the symbolic environment based on known locations *)
apply _. (* Reify the expression *)
done. (* Prove that the environment is well-formed *)
simpl.
Admitted.
Lemma memcpy_spec (p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
length ls2 = n
p C ls1 -
q C ls2 -
AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}.
Proof.
iIntros (? ?) "Hp Hq".
iApply a_invoke_simpl.
vcg_solver. iModIntro.
awp_lam. iApply awp_bind.
iApply (a_alloc_spec _ _ (λ v, v = #1))%I; first by (iApply awp_ret; wp_value_head).
awp_proj. iApply awp_ret; wp_value_head.
iNext. iIntros (? ->). iExists 1%nat. iSplit; eauto.
iIntros (pp) "[Hpp _]". rewrite {3}/cloc_add. etaprod pp.
repeat awp_pure _. iApply awp_bind.
iApply (a_ptr_add_spec _ _ (λ v, v = #n))%I; first by (iApply awp_ret; wp_value_head).
vcg_solver. iIntros "Hpp".
iNext. iIntros (? ->). iExists p,n; repeat iSplit; eauto.
awp_let. iApply (memcpy_body_spec 0 with "[] Hp Hq [Hpp]"); eauto.
by rewrite Nat.add_0_r.
Qed.
End memcpy.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment