Commit 1d0a5447 authored by Dan Frumin's avatar Dan Frumin

Get rid of admits

parent 05073110
......@@ -105,16 +105,16 @@ Section proofs.
iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
{ remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
iDestruct "Hls" as (v') "Hl'". admit.
(* iDestruct (mapsto_valid_2 with "[Hl] [Hl']") as "Hfoo". *) }
iDestruct "Hls" as (v') "Hl'".
by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
wp_apply (release_cancel_spec with "[$Hfl $Hlkd $HR Hσ Hls Hl HX]").
{ iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
- rewrite big_sepM_insert; eauto. iFrame. eauto.
- iPureIntro. admit. (* TODO: need a lemma for corrrect locks *)
- iPureIntro. by rewrite locked_locs_alloc_unlocked.
}
iIntros "Hunfl". wp_seq. iFrame. by iApply "HΦ".
Admitted.
Qed.
End proofs.
......@@ -115,8 +115,32 @@ Section properties.
right. intros ?. rewrite lookup_insert=>?. simplify_eq/=.
naive_solver.
- rewrite lookup_delete_ne; last done.
admit.
Admitted.
remember (σ !! j) as σj. symmetry in Heqσj. destruct σj as [[|]|].
+ transitivity (Some LLvl); [|symmetry]; apply map_filter_lookup_Some; try naive_solver.
rewrite lookup_insert_ne; naive_solver.
+ transitivity (@None level); [|symmetry]; apply map_filter_lookup_None; right; try naive_solver.
rewrite lookup_insert_ne; naive_solver.
+ transitivity (@None level); [|symmetry]; apply map_filter_lookup_None; right; try naive_solver.
rewrite lookup_insert_ne; naive_solver.
Qed.
Lemma locked_locs_alloc_unlocked σ l :
σ !! l = None
locked_locs (<[l := ULvl]>σ) = locked_locs σ.
Proof.
intros Hl. rewrite /locked_locs. f_equal.
apply map_eq => j.
destruct (decide (l = j)) as [->|?].
- transitivity (@None level); [|symmetry]; apply map_filter_lookup_None; [right|by left].
+ rewrite lookup_insert. naive_solver.
- remember (σ !! j) as σj. symmetry in Heqσj. destruct σj as [[|]|].
+ transitivity (Some LLvl); [|symmetry]; apply map_filter_lookup_Some; try naive_solver.
rewrite lookup_insert_ne; naive_solver.
+ transitivity (@None level); [|symmetry]; apply map_filter_lookup_None; right; try naive_solver.
rewrite lookup_insert_ne; naive_solver.
+ transitivity (@None level); [|symmetry]; apply map_filter_lookup_None; right; try naive_solver.
rewrite lookup_insert_ne; naive_solver.
Qed.
Lemma heap_singleton_included (σ : gmap loc level) l x :
{[l := Excl x]} (to_locking_heap σ) σ !! l = Some x.
......
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