Commit cab3db52 authored by Dan Frumin's avatar Dan Frumin

Merge branch 'bind'

parents 6678f0c8 772ff880
This diff is collapsed.
......@@ -56,22 +56,22 @@ Section factorial_spec.
AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext.
vcg_solver.
iIntros (r) "[Hr _]". vcg_continue. iIntros "Hr".
iIntros (c) "[Hc _]". vcg_continue. iIntros "Hr Hc".
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro.
awp_load_ret r.
- iIntros (?) "[Hc Hr]". vcg_continue. iModIntro. eauto.
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext. do 3 awp_lam.
vcg_solver.
iIntros (r) "[Hr _]". vcg_continue. iIntros "Hr".
iIntros (c) "[Hc _]". vcg_continue. iIntros "Hr Hc".
do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
......@@ -87,8 +87,9 @@ Section factorial_spec.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. do 2 iModIntro.
+ iLeft. iSplit; eauto. iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
awp_load_ret r.
vcg_continue. eauto.
Qed.
End factorial_spec.
......@@ -93,36 +93,15 @@ Section memcpy.
AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}.
Proof.
iIntros (? ?) "Hp Hq". vcg_solver. awp_lam.
iApply awp_bind. vcg_solver.
iIntros (pp) "[Hpp _]". vcg_continue. iIntros "Hpp". awp_let.
iApply awp_bind. vcg_solver. iIntros "Hpp".
iIntros (qq) "[Hqq _]". vcg_continue. iIntros "Hpp Hqq". awp_let.
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".
vcg_solver. iIntros (pp) "[Hpp _]".
vcg_continue. iIntros "Hpp". iIntros (qq) "[Hqq _]".
vcg_continue. iIntros "Hpp Hqq".
repeat awp_proj. awp_let. set (e :=( while (_) { _ })%E).
unfold e. 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. *)
Admitted.
(*
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_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.
{ iPureIntro. repeat (case_option_guard; last omega). simpl.
repeat f_equal. rewrite !Nat2Z.id //. }
awp_let. iApply (memcpy_body_spec with "Hp Hq Hpp Hqq"); auto.
Qed. *) Admitted.
End memcpy.
......@@ -42,7 +42,9 @@ Section tests_vcg.
AWP (swap_with_alloc (cloc_to_val l1)) (cloc_to_val l2) @ R {{ _, l1 C v2 l2 C v1 }}.
Proof.
iIntros "Hl1 Hl2".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "[Hr _]".
vcg_solver. iIntros "!> !> !> **". eauto with iFrame.
do 2 awp_lam.
vcg_solver.
iIntros "Hl2 Hl1". iIntros (l3) "[Hl3 _]". vcg_continue.
iIntros "!> !> !> **". eauto with iFrame.
Qed.
End tests_vcg.
......@@ -28,27 +28,29 @@ Section vcg_continue.
FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100.
Proof. done. Qed.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
MapstoListFromEnv Γs_in Γs_out Γls
E = penv_to_known_locs Γls
ListOfMapsto Γls E m
IntoDCExpr E e de
dcexpr_wf [] E de
denv_wf (penv_to_known_locs Γls) m
envs_entails (Envs Γp Γs_out c)
(vcg_wp E m de R (λ E m dv,
mapsto_wand_list E m (Φ (dval_interp E dv))))
mapsto_wand_list E m (Φ (dval_interp E dv))) 1024 (*TODO: Fix this*))
envs_entails (Envs Γp Γs_in c) (awp e R Φ).
Proof.
intros Hsplit ->.
rewrite /ListOfMapsto. intros Hpenv [-> Hwf] Hmwf Hgoal.
rewrite /ListOfMapsto. intros Hpenv -> Hwf Hmwf Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R); last done.
rewrite (vcg_wp_correct R); try done.
iIntros (->) "H1 H2".
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v). iDestruct 1 as (E' dv m' Hpre) "(% & % & % & Hm & Hwp)".
rewrite Hpre.
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm").
Qed.
Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v dv E_old E_new (Φ: known_locs denv dval iProp Σ):
......@@ -74,6 +76,7 @@ Section vcg_continue.
* by left.
* right. by apply Hsplit.
Qed.
End vcg_continue.
Arguments vcg_wp_continuation {_ _ _ _}.
......@@ -89,6 +92,7 @@ Ltac vcg_solver :=
| simpl; reflexivity (* Compute the known locations *)
| apply _ (* Compute the symbolic environment based on known locations *)
| apply _ (* Reify the expression *)
| vm_compute[reflexivity]; try done (* Prove that the reified expression is well-formed *)
| done (* Prove that the environment is well-formed *)
| simpl ].
......@@ -99,4 +103,4 @@ Ltac vcg_continue :=
| apply _ (* ListOfMapsto Γls (E_old ++ E_new) ps *)
| apply _ (* IntoDVal (E_old ++ E_new) v dv *)
| done (* ps is well-formed *)
| simpl ].
| simpl; simpl_subst ].
This diff is collapsed.
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