Commit 30cb8e51 authored by Léon Gondelman's avatar Léon Gondelman

factoring a_load (a_ret _) and a_alloc (a_ret _)

parent 5b78fb97
......@@ -33,6 +33,27 @@ Section factorial_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma a_load_ret (l: loc) (w: val) R Φ:
l U w (l U w - Φ w) -
awp (a_load (a_ret (#l)%E)) R Φ.
Proof.
iIntros "H". iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists l, w. by iFrame.
Qed.
Lemma a_alloc_ret (w: val) R Φ:
( (l: loc), (l U w - Φ #l)) -
awp (a_alloc (a_ret w)) R Φ.
Proof.
iIntros "H". iApply a_alloc_spec.
iApply awp_ret. by wp_value_head.
Qed.
Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
Ltac awp_alloc_ret w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
Lemma incr_spec (l : loc) (n : Z) R Φ :
l U #n - (l L #(n+1) - Φ #(n+1)) -
awp (incr #l) R Φ.
......@@ -41,13 +62,11 @@ Section factorial_spec.
awp_lam.
iApply (a_store_spec _ _
(λ r, r = l)%I (λ v, v = #(n+1) l U #n)%I with "[] [Hl]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ awp_ret_value. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #n l U #n )%I (λ v, v = #1)%I with "[-]").
+ iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _,_; iFrame; eauto.
+ iApply awp_ret. by wp_value_head.
+ awp_load_ret l #n.
+ awp_ret_value.
+ iIntros (? ?) "(% & Hc) %"; subst. iExists #(n+1). by iFrame. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame.
......@@ -64,9 +83,8 @@ Section factorial_spec.
iApply a_if_spec.
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc]").
- iApply a_load_spec. iApply awp_ret. wp_value_head.
iExists _,_; iFrame. eauto.
- iApply awp_ret. by wp_value_head.
- awp_load_ret c #k.
- awp_ret_value.
- iIntros (v1 v2) "[% Hc] %"; subst.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
case_bool_decide.
......@@ -79,16 +97,12 @@ Section factorial_spec.
(λ v, v = #(fact (k+1))
c U #(k + 1)
r U #(fact k))%I with "[] [Hr Hc]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ awp_ret_value. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
* iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _, _; iFrame. eauto.
* iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _, _; iFrame. eauto.
* awp_load_ret r #(fact k).
* awp_load_ret c #(k + 1).
* iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
rewrite /bin_op_eval /=.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
......@@ -109,16 +123,13 @@ Section factorial_spec.
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iIntros (r) "Hr". awp_lam.
iApply awp_bind. iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iIntros (c) "Hc". awp_lam.
iApply awp_bind. awp_alloc_ret #1 r "Hr".
iApply awp_bind. awp_alloc_ret #0 c "Hc".
iApply a_sequence_spec.
iApply (awp_wand _ (λ _, c U #n r U #(fact n))%I with "[Hr Hc]").
- iApply (factorial_body_spec n 0 c r R). iFrame. iPureIntro. lia.
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
iApply a_load_spec. iApply awp_ret. iApply wp_value; eauto.
iExists _,_; iFrame. eauto.
awp_load_ret r #(fact n).
Qed.
End factorial_spec.
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