Commit 3216e98d authored by Dan Frumin's avatar Dan Frumin

[WIP] Better spec for alloc that does not expose `loc`

parent ca87e38f
......@@ -29,7 +29,7 @@ Section derived.
IntoVal e1 ev1
ValToNat ev1 n
IntoVal e2 ev2
( l: loc, (l,O) C replicate n ev2 - Φ (cloc_to_val (l,O))) -
( l: cloc, l C replicate n ev2 - Φ (cloc_to_val l)) -
awp (a_alloc (a_ret e1) (a_ret e2)) R Φ.
Proof.
iIntros (? ? ?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I).
......
......@@ -109,7 +109,7 @@ Section proofs.
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ v2, ( v1, Ψ1 v1 - n : nat,
v1 = #n
l, (l,O) C replicate n v2 - Φ (cloc_to_val (l,O))) }} -
l, l C replicate n v2 - Φ (cloc_to_val l)) }} -
AWP alloc(e1, e2) @ R {{ Φ }}.
Proof.
iIntros "H1 HΦ".
......@@ -123,7 +123,7 @@ Section proofs.
wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
iApply wp_fupd. wp_alloc l as "Hl".
iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply "HΦ"].
iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (l, 0%nat))].
iExists X, _. iFrame.
iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
exists cl; split; first done. by rewrite locked_locs_alloc_heap.
......
......@@ -113,19 +113,22 @@ Section in_place_reversal.
iIntros "Hlst". awp_lam.
iApply awp_bind; awp_alloc_ret i "[Hi _]".
iApply awp_bind; awp_alloc_ret j "[Hj _]".
compute[cloc_add]. rewrite !Nat.add_0_r.
assert ((i.1, i.2) = i) as -> by (destruct i; auto).
assert ((j.1, j.2) = j) as -> by (destruct j; auto).
iApply a_sequence_spec'. iNext.
iApply (a_while_inv_spec ( ls rs rhd hd, (i,O) C hd is_list hd ls
(j,O) C rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
iApply (a_while_inv_spec ( ls rs rhd hd, i C hd is_list hd ls
j C rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
- iExists xs, [], (InjLV #()), hd; eauto with iFrame.
- iModIntro; iIntros "H". clear hd.
iDestruct "H" as (ls rs rhd hd) "(Hi & Hls & Hj & Hrs & %)".
iApply a_un_op_spec. iApply (a_bin_op_spec _ _
(λ x, x = hd (i,O) C hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").
{ awp_load_ret (i,O). } { awp_ret_value. }
(λ x, x = hd i C hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").
{ awp_load_ret i. } { awp_ret_value. }
iNext. iIntros (? ?) "[-> Hi ] ->". destruct ls.
+ rewrite{1}/ is_list. iDestruct "Hls" as "->".
iExists #true; iSplit; first done. iExists #false; iSplit; first done.
iLeft; iSplit; first done. do 2 iModIntro. awp_load_ret (j,O).
iLeft; iSplit; first done. do 2 iModIntro. awp_load_ret j.
iIntros "_". simplify_eq /=. by rewrite app_nil_r reverse_involutive.
+ iDestruct "Hls" as (l lnxt) "(-> & Hl & Hls)". fold is_list.
iExists #false; iSplit; first done; iExists #true; iSplit; first done.
......@@ -133,15 +136,17 @@ Section in_place_reversal.
iNext. iApply (a_alloc_spec _ _ (λ v, v = #1) with "[] [-]")%I.
{ iApply awp_ret. by wp_value_head. }
iApply a_list_next_spec.
awp_load_ret (i,O). iIntros "Hi". iExists l, lnxt, v, ls.
awp_load_ret i. iIntros "Hi". iExists l, lnxt, v, ls.
iSplit; first done. iFrame. iIntros "Hl Hls".
iNext. iIntros (? ->). iExists 1%nat; iSplit; eauto.
iIntros (k) "[Hk _]". awp_let. iApply a_sequence_spec'; iNext.
compute[cloc_add]. rewrite !Nat.add_0_r.
assert ((k.1, k.2) = k) as -> by (destruct k; auto).
iApply (a_list_store_next_spec _ _
(λ z, z = (v, SOMEV (cloc_to_val l)) (i,O) C (SOMEV (cloc_to_val l)) )%I
(λ v, v = rhd (j,O) C rhd)%I with "[Hi Hl] [Hj]").
{ awp_load_ret (i,O). eauto 42 with iFrame. }
{ awp_load_ret (j,O). }
(λ z, z = (v, SOMEV (cloc_to_val l)) i C (SOMEV (cloc_to_val l)) )%I
(λ v, v = rhd j C rhd)%I with "[Hi Hl] [Hj]").
{ awp_load_ret i. eauto 42 with iFrame. }
{ awp_load_ret j. }
iIntros (a0 ? ?) "(% & Hi) (% & Hj)". simplify_eq/=.
(* TODO: this is annoying *)
assert (a0 = l) as ->. { by destruct l,a0; simplify_eq/=. }
......
......@@ -47,12 +47,13 @@ Section test.
awp (swap (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".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "[Hr _]".
compute[cloc_add]. rewrite Nat.add_0_r.
assert ((r.1, r.2) = r) as -> by (destruct r; auto).
iApply a_sequence_spec'.
iNext.
iApply (a_store_ret (r,0%nat) with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iDestruct "Hr" as "[Hr _]". compute[cloc_add]. simpl. iFrame.
iNext. iApply (a_store_ret r with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. iApply a_sequence_spec'.
iNext. iApply (a_store_ret with "[Hl1 Hl2 Hr]").
......@@ -60,7 +61,7 @@ Section test.
iIntros "Hl1". iModIntro. iApply awp_bind.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret (r,0%nat). iIntros "Hr". iExists v2. iFrame.
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
......
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