Commit 2985f8dd authored by Dan Frumin's avatar Dan Frumin

[flock2] Get rid of some admits

parent 8f5c5363
......@@ -161,10 +161,13 @@ Section flock.
iNext. iExists _,_,_. iFrame. iFrame "Hrest".
rewrite /all_props big_sepM_insert; last first.
+ apply (not_elem_of_dom _ i (D:=gset prop_id)).
revert Hs. rewrite dom_union_L not_elem_of_union. set_solver.
revert Hs. rewrite dom_union_L not_elem_of_union. set_solver.
+ iFrame "Hfp". iSplitR; last by eauto.
iPureIntro. admit. (* TODO: map disjoint *)
Admitted.
iPureIntro. apply map_disjoint_insert_l_2; eauto.
eapply (not_elem_of_dom (D:=gset prop_id)).
intros Hi; apply Hs. rewrite dom_union_L elem_of_union.
eauto.
Qed.
Lemma flock_res_single_dealloc γ lk i R E :
flockN E
......@@ -176,7 +179,7 @@ Section flock.
- iDestruct "Hrest" as ">[Hlocked Htokens]".
iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct (own_valid_2 with "Hauth HR")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
iAssert (fa !! i = None)%I with "[-]" as %Hbar.
{ remember (fa !! i) as fai. destruct fai as [[π [ρ'1 ρ'2]]|]; last done.
iExFalso.
......@@ -193,7 +196,8 @@ Section flock.
simplify_eq/=.
iDestruct (own_valid with "Htokens") as %Hbaz1%frac_valid'.
iDestruct (own_valid_2 with "Hρ2 Htokens") as %Hbaz2.
rewrite frac_op' in Hbaz2. exfalso. apply Hbaz2. admit. (* TODO: Qp *) }
rewrite frac_op' in Hbaz2. exfalso.
eapply Qp_not_plus_q_ge_1. apply Hbaz2. }
assert (fp !! i = Some (ρ1, ρ2)) as Hbaz.
{ apply lookup_union_Some in Hfoo; last done.
destruct Hfoo as [? | Hfoo]; first done.
......@@ -208,7 +212,8 @@ Section flock.
iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "Hfoo".
iMod ("Hcl" with "[-HR' Hfoo Hρ2]") as "_".
{ iNext. iExists Locked, (delete i fp),fa. iFrame.
iSplit. admit. (* TODO: map_disjoint *)
iSplit.
{ iPureIntro. by apply map_disjoint_delete_l. }
rewrite /to_props_map -fmap_delete.
rewrite delete_union (delete_notin (from_active fa)); first iFrame.
by rewrite /from_active lookup_fmap Hbar. }
......@@ -221,7 +226,7 @@ Section flock.
rewrite from_active_empty right_id.
iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct (own_valid_2 with "Hauth HR")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hauth HR") as "Hauth".
{ apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
......@@ -234,7 +239,7 @@ Section flock.
rewrite /to_props_map fmap_delete. iFrame "Hauth".
iPureIntro. apply map_disjoint_empty_r. }
iModIntro. iExists R'. iFrame.
Admitted.
Qed.
Lemma newlock_cancel_spec :
{{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
......@@ -258,6 +263,14 @@ Section flock.
rewrite /is_flock. by iFrame "Hlock".
Qed.
(* {{{ is_flock γ lk ∗ *)
(* ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}} *)
(* acquire lk *)
(* {{{ RET #(); *)
(* ▷ ▷ ([∗ list] (i, R, π) ∈ I, R) ∗ *)
(* (▷ ([∗ list] (i, R, π) ∈ I, R) *)
(* ={⊤}=∗ flocked γ ∅ ∗ ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}}. *)
Lemma acquire_cancel_spec γ π lk i R :
{{{ is_flock γ lk flock_res γ i R π }}}
acquire lk
......@@ -287,20 +300,20 @@ Section flock.
(* (i,ρ) ∈ fp *)
iDestruct (own_valid_2 with "Hauth HR")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
iDestruct "Hfp" as "[HR' Hfp]".
iDestruct "HR'" as (R') "[Hsaved HR']".
iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "#Hfoo".
(* move (i,ρ) to the set of active propositions *)
iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
{ apply (auth_update _ _ (Excl' {[ i := (π, (ρ1, ρ2)) ]})
(Excl' {[ i := (π, (ρ1, ρ2)) ]})).
apply option_local_update.
by apply exclusive_local_update. }
iMod ("Hcl" with "[-HΦ HR' Hfoo Haactive Hflkd HR]") as "_".
{ iNext. iExists Locked,(delete i fp),{[i := (π, (ρ1, ρ2))]}.
iFrame. iSplitR. admit. (* TODO: map_disjoint *)
......@@ -331,7 +344,7 @@ Section flock.
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
fold_leibniz. inversion Hfoo.
+ iDestruct "Hrest" as ">[Hlocked Htokens]".
iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
fold_leibniz. simplify_eq/=.
......@@ -345,7 +358,7 @@ Section flock.
{ apply (auth_update _ _ (Excl' )
(Excl' )).
apply option_local_update. by apply exclusive_local_update. }
iMod ("Hcl" with "[HR' Hlocked Hstate Hauth Hfactive Hfp]") as "_".
{ iNext. iExists Locked,(<[i := (ρ1,ρ2)]>fp),.
iSplitR.
......@@ -375,7 +388,7 @@ Section flock.
- iDestruct (own_valid_2 with "Hstate Hflkd")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
fold_leibniz. inversion Hfoo.
- iDestruct "Hrest" as ">[Hlocked Htokens]".
- iDestruct "Hrest" as ">[Hlocked Htokens]".
iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
fold_leibniz. simplify_eq/=.
......
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