Commit cef2551f authored by Robbert Krebbers's avatar Robbert Krebbers

Some notes.

parent 5fb2e503
......@@ -90,22 +90,19 @@ Section memcpy.
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. vcg_solver. iExists 1%nat; iSplit; first done.
iIntros (? ?) "Hp Hq". vcg_solver. awp_lam.
iApply awp_bind. vcg_solver. iExists 1%nat; iSplit; first done.
iIntros (pp) "[Hpp _]". vcg_continue. iIntros "Hpp". awp_let.
iApply awp_bind. vcg_solver. iIntros "Hpp". iExists 1%nat; iSplit; first done.
iIntros (qq) "[Hqq _]". vcg_continue. iIntros "Hpp Hqq". awp_let.
repeat awp_proj. awp_let.
set (e :=( while (∗ᶜ (a_ret (cloc_to_val (cloc_plus pp 0))) <∗ᶜ a_ret "pend") { (a_ret (cloc_to_val (cloc_plus pp 0)) +=
1) =
∗ᶜ (a_ret (cloc_to_val (cloc_plus qq 0)) +=
1) })%E).
Check awp_bind.
repeat awp_proj. awp_let. (* iApply awp_bind hangs without the set *)
set (e :=( while (_) { _ })%E).
iApply awp_bind. unfold e. apply _.
vcg_solver. iIntros "Hpp Hqq".
(* Ouch, this goal is ugly. We either need to embed naturals into the
reified syntax, or let the binop evaluator be total and generate
side-conditions (here 0 ≤ n) for the result to be well-formed. *)
vcg_solver.
iIntros "Hpp Hqq". cloc_to_val (c iExists 1%nat; iSplit; first done.
(*
awp_proj. iApply awp_ret; wp_value_head.
......
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