Commit d2649221 authored by Dan Frumin's avatar Dan Frumin

Fix the memcpy test

parent af4a0111
......@@ -21,6 +21,7 @@ theories/vcgen/tests/unknowns.v
theories/vcgen/tests/test.v
theories/vcgen/tests/swap.v
theories/vcgen/tests/fact.v
theories/vcgen/tests/memcpy.v
# theories/tests/test1.v
# theories/tests/test2.v
# theories/tests/gcd.v
......
......@@ -14,58 +14,110 @@ Section memcpy.
Definition memcpy : val := λ: "arg",
"p" ←ᶜ a_alloc 1 (a_ret (Fst "arg"));;
let: "q" := Fst (Snd "arg") in
"q" ←ᶜ a_alloc 1 (a_ret (Fst (Snd "arg")));;
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) }.
{ ((a_ret "p")+=ᶜ♯1) = (∗ᶜ((a_ret "q")+=ᶜ♯1)) }.
(* TODO: move somewhere *)
Lemma cloc_lt_Z_eq l1 (o1 : nat) l2 (o2 : nat) :
cloc_lt_Z l1 o1 l2 o2 = Some (cloc_lt (l1,o1) (l2,o2)).
Proof. Admitted.
Proof.
destruct o1,o2; simpl; compute[cloc_lt]; simpl; repeat case_bool_decide; eauto; try naive_solver.
- exfalso. apply H2. rewrite !SuccNat2Pos.id_succ in H1. done.
- exfalso. apply H1. rewrite !SuccNat2Pos.id_succ in H1. done.
Qed.
Lemma cloc_add_Z_eq l1 (o1 o2 : nat) :
cloc_add_Z l1 o1 o2 = Some (cloc_add (l1,o1) o2).
Proof. Admitted.
Proof.
destruct o1,o2; simpl; compute[cloc_add]; simpl;
repeat case_bool_decide; rewrite ?SuccNat2Pos.id_succ; eauto.
by rewrite Nat.add_0_r.
Qed.
Lemma memcpy_body_spec (i: nat) (pp p q : cloc) (n : nat) (ls1 ls2 : list val) R :
Lemma cloc_add_0 cl : cloc_add cl 0 = cl.
Proof. destruct cl; cbv[cloc_add]. simpl. by rewrite Nat.add_0_r. Qed.
(* END TODO *)
Lemma memcpy_body_spec (* (i: nat) *) (pp qq p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
length ls2 = n
take i ls1 = take i ls2 -
(* ⌜take i ls1 = take i ls2⌝ -∗ *)
p C ls1 -
q C ls2 -
pp C (#p.1, #(p.2+i)%nat) -
pp C (#p.1, #(p.2)%nat) -
qq C (#q.1, #q.2) -
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) }
{ (a_ret (#pp.1, #pp.2) += 1) = (∗ᶜ (a_ret (#qq.1, #qq.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. vcg_solver. simpl.
destruct (decide (i < length ls1)%nat).
- iExists (dValUnknown #true). iSplit.
{ iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
rewrite !bool_decide_true; auto. omega. }
vcg_continue. iLeft; iSplit; first done.
(* vcg_solver DF: doesnt do anything *)
admit.
- iExists (dValUnknown #false). iSplit.
iIntros (Hlen1 Hlen2) "Hp Hq Hpp Hqq".
simplify_eq/=.
iAssert (length ls2 = length ls1)%I as "Hlen"; first done.
clear Hlen2.
iInduction ls2 as [|w ls2] "IH" forall (ls1 p q); iDestruct "Hlen" as %Hlen.
(* iLöb as "IH" forall (i). *) (* iDestruct "Htake" as %Htake. *)
- assert (ls1 = []) as -> by (destruct ls1; naive_solver).
simplify_eq/=. rewrite Nat.add_0_r.
iApply a_while_spec'.
iNext. vcg_solver. iExists #false. iSplit.
{ iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
rewrite bool_decide_true // bool_decide_false //. omega. }
vcg_continue. iRight; iSplit; first done.
rewrite bool_decide_true // bool_decide_false //. omega. }
rewrite Qp_half_half. iIntros "? ?".
vcg_continue. iIntros "Hpp Hqq". iRight. iSplit; first done.
iApply a_seq_spec. iModIntro. simplify_eq/=.
assert (ls1 = ls2) as ->.
{ generalize dependent i. generalize dependent ls2. induction ls1; simpl; eauto.
- intros ls2 ->%nil_length_inv. done.
- simpl. intros ls2 Hlen i Htake Hi.
induction ls2; simpl; eauto. inversion Hlen.
apply Nat.nlt_succ_r in Hi. destruct i as [|i]; first inversion Hi.
simpl in Htake. simplify_eq/=. f_equal. eapply IHls1; eauto.
intros ?%Nat.nlt_succ_r. done. }
iFrame.
Admitted.
- simpl in Hlen.
destruct ls1 as [|y ls1]; first done.
iDestruct "Hp" as "[Hy Hp]".
iDestruct "Hq" as "[Hw Hq]".
rewrite {1}/(cloc_add p). etaprod p.
rewrite {1}/(cloc_add q). etaprod q.
iApply a_while_spec'.
iNext. vcg_solver. iExists #true. iSplit.
{ iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
rewrite !bool_decide_true; auto. omega. }
rewrite Qp_half_half. iIntros "? ? ? ?".
vcg_continue. iIntros "Hqq Hpp Hw Hy". iLeft; iSplit; first done.
(* DF: vcgen doesnt do anything here *)
(* vcg_solver. iIntros "Hy Hw Hpp". *)
iApply (a_store_spec _ _
(λ v, v = cloc_to_val p pp C[LLvl] cloc_to_val (cloc_add p 1))
(λ v, v = w q C w qq C[LLvl] cloc_to_val (cloc_add q 1)) with "[Hpp] [Hqq Hw]")%I.
+ vcg_solver. iExists (dValUnknown (cloc_to_val (cloc_add p 1))).
iSplit.
{ iPureIntro. replace 1%Z with (Z.of_nat 1%nat); last done.
rewrite cloc_add_Z_eq. simpl. done. }
iIntros "Hpp /=". vcg_continue. eauto.
+ vcg_solver. iExists (dValUnknown (cloc_to_val (cloc_add q 1))).
iSplit.
{ iPureIntro. replace 1%Z with (Z.of_nat 1%nat); last done.
rewrite cloc_add_Z_eq. simpl. done. }
iIntros "Hq Hpp /=". vcg_continue. eauto with iFrame.
+ iNext. iIntros (? ?) "[% Hpp] (% & Hw & Hqq)"; simplify_eq/=.
iExists p,y. iSplit; eauto. iFrame. iIntros "Hy".
iModIntro.
iSpecialize ("IH" $! ls1 (cloc_add p 1) (cloc_add q 1)
with "[Hp] [Hq] Hpp Hqq []"); auto.
{ iApply (big_sepL_impl with "Hp"). iAlways. iIntros (k ? ?) "Hp".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l. }
{ iApply (big_sepL_impl with "Hq"). iAlways. iIntros (k ? ?) "Hq".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l. }
simpl. rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
iApply (awp_wand with "IH").
iIntros (?) "[Hp Hq]". rewrite !cloc_add_0. iFrame.
iSplitL "Hp".
* iApply (big_sepL_impl with "Hp"). iAlways. iIntros (k ? ?) "Hp".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
* iApply (big_sepL_impl with "Hq"). iAlways. iIntros (k ? ?) "Hq".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
Qed.
Lemma memcpy_spec (p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
......@@ -83,17 +135,18 @@ Section memcpy.
iNext. iIntros (? ->). iExists 1%nat. iSplit; eauto.
iIntros (pp) "[Hpp _]". rewrite {3}/cloc_add. etaprod pp.
repeat awp_pure _. iApply awp_bind.
(* DF: TODO!! if we run vcg_solver here then we loose pp ↦ -
some problem with vcgen for pre_op?
*)
iApply (a_alloc_spec _ _ (λ v, v = #1))%I; first by (iApply awp_ret; wp_value_head).
do 2 awp_proj. iApply awp_ret; wp_value_head.
iNext. iIntros (? ->). iExists 1%nat. iSplit; eauto.
iIntros (qq) "[Hqq _]". rewrite {3}/cloc_add. etaprod qq.
repeat awp_pure _. iApply awp_bind.
iApply (a_bin_op_spec _ _ (λ v, v = cloc_to_val p pp C (#p.1, #p.2)) (λ v, v = #n) with "[Hpp]")%I.
- vcg_solver. eauto.
- by vcg_solver.
- iNext. iIntros (? ?) "[% Hpp] %". simplify_eq/=.
iExists (cloc_to_val (p.1,p.2+length ls1))%nat; repeat iSplit; eauto.
{ rewrite cloc_add_Z_eq. done. }
awp_let. iApply (memcpy_body_spec 0 with "[] Hp Hq [Hpp]"); eauto.
by rewrite Nat.add_0_r.
Qed.
awp_let. iApply (memcpy_body_spec with "Hp Hq Hpp Hqq"); auto.
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