Commit f9234e4f authored by jihgfee's avatar jihgfee

Removed Experimental

parent b7e45fde
From iris.heap_lang Require Export notation.
Class ValEnc A := val_encode : A val.
Class ValDec A := val_decode : val option A.
Class ValEncDec A `{!ValEnc A, !ValDec A} := {
val_encode_decode v : val_decode (val_encode v) = Some v;
val_decode_encode v x : val_decode v = Some x val_encode x = v;
}.
Local Arguments val_encode _ _ !_ /.
Local Arguments val_decode _ _ !_ /.
Lemma val_encode_decode_iff `{ValEncDec A} v x :
val_encode x = v val_decode v = Some x.
Proof.
split; last apply val_decode_encode. intros <-. by rewrite -val_encode_decode.
Qed.
Instance val_encode_inj `{ValEncDec A} : Inj (=) (=) val_encode.
Proof.
intros x y Heq. apply (inj Some).
by rewrite -(val_encode_decode x) Heq val_encode_decode.
Qed.
(* Instances *)
Instance val_val_enc : ValEnc val := id.
Instance val_val_dec : ValDec val := id $ Some.
Instance val_val_enc_dec : ValEncDec val.
Proof. split. done. by intros ?? [= ->]. Qed.
Instance int_val_enc : ValEnc Z := λ n, #n.
Instance int_val_dec : ValDec Z := λ v,
match v with LitV (LitInt z) => Some z | _ => None end.
Instance int_val_enc_dec : ValEncDec Z.
Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
Instance bool_val_enc : ValEnc bool := λ b, #b.
Instance bool_val_dec : ValDec bool := λ v,
match v with LitV (LitBool b) => Some b | _ => None end.
Instance bool_val_enc_dec : ValEncDec bool.
Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
Instance loc_val_enc : ValEnc loc := λ l, #l.
Instance loc_val_dec : ValDec loc := λ v,
match v with LitV (LitLoc l) => Some l | _ => None end.
Instance loc_val_enc_dec : ValEncDec loc.
Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
Instance unit_val_enc : ValEnc unit := λ _, #().
Instance unit_val_dec : ValDec unit := λ v,
match v with LitV LitUnit => Some () | _ => None end.
Instance unit_val_enc_dec : ValEncDec unit.
Proof. split. by intros []. by intros [[]| | | |] ? [= <-]. Qed.
Instance pair_val_enc `{ValEnc A, ValEnc B} : ValEnc (A * B) := λ p,
(val_encode p.1, val_encode p.2)%V.
Arguments pair_val_enc {_ _ _ _} !_ /.
Instance pair_val_dec `{ValDec A, ValDec B} : ValDec (A * B) := λ v,
match v with
| PairV v1 v2 => x1 val_decode v1; x2 val_decode v2; Some (x1, x2)
| _ => None
end.
Arguments pair_val_dec {_ _ _ _} !_ /.
Instance pair_val_enc_dec `{ValEncDec A, ValEncDec B} : ValEncDec (A * B).
Proof.
split.
- intros []. by rewrite /= val_encode_decode /= val_encode_decode.
- intros [] ??; simplify_option_eq;
by repeat match goal with
| H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
end.
Qed.
Instance option_val_enc `{ValEnc A} : ValEnc (option A) := λ mx,
match mx with Some x => SOMEV (val_encode x) | None => NONEV end%V.
Arguments option_val_enc {_ _} !_ /.
Instance option_val_dec `{ValDec A} : ValDec (option A) := λ v,
match v with
| SOMEV v => x val_decode v; Some (Some x)
| NONEV => Some None
| _ => None
end.
Arguments option_val_dec {_ _} !_ /.
Instance option_val_enc_dec `{ValEncDec A} : ValEncDec (option A).
Proof.
split.
- intros []=> //. by rewrite /= val_encode_decode.
- intros [] ??; repeat (simplify_option_eq || case_match);
by repeat match goal with
| H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
end.
Qed.
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.
(** Immutable ML-style functional lists *)
Fixpoint flist (vs : list val) : val :=
match vs with
| [] => NONEV
| v :: vs => SOMEV (v,flist vs)
end%V.
Arguments flist : simpl never.
Definition fnil : val := λ: <>, NONEV.
Definition fcons : val := λ: "x" "l", SOME ("x", "l").
Definition fisnil : val := λ: "l",
match: "l" with
SOME "p" => #false
| NONE => #true
end.
Definition fhead : val := λ: "l",
match: "l" with
SOME "p" => Fst "p"
| NONE => assert: #false
end.
Definition ftail : val := λ: "l",
match: "l" with
SOME "p" => Snd "p"
| NONE => assert: #false
end.
Definition flookup : val :=
rec: "go" "n" "l" :=
if: "n" = #0 then fhead "l" else
let: "l" := ftail "l" in "go" ("n" - #1) "l".
Definition finsert : val :=
rec: "go" "n" "x" "l" :=
if: "n" = #0 then let: "l" := ftail "l" in fcons "x" "l" else
let: "k" := ftail "l" in
let: "k" := "go" ("n" - #1) "x" "k" in
fcons (fhead "l") "k".
Definition freplicate : val :=
rec: "go" "n" "x" :=
if: "n" = #0 then fnil #() else
let: "l" := "go" ("n" - #1) "x" in fcons "x" "l".
Definition flength : val :=
rec: "go" "l" :=
match: "l" with
NONE => #0
| SOME "p" => #1 + "go" (Snd "p")
end.
Definition fapp : val :=
rec: "go" "l" "k" :=
match: "l" with
NONE => "k"
| SOME "p" => fcons (Fst "p") ("go" (Snd "p") "k")
end.
Definition fsnoc : val := λ: "l" "x", fapp "l" (fcons "x" (fnil #())).
Definition ftake : val :=
rec: "go" "l" "n" :=
if: "n" #0 then NONEV else
match: "l" with
NONE => NONEV
| SOME "l" => fcons (Fst "l") ("go" (Snd "l") ("n"-#1))
end.
Definition fdrop : val :=
rec: "go" "l" "n" :=
if: "n" #0 then "l" else
match: "l" with
NONE => NONEV
| SOME "l" => "go" (Snd "l") ("n"-#1)
end.
Definition fsplit_at : val := λ: "l" "n", (ftake "l" "n", fdrop "l" "n").
Definition fsplit : val := λ: "l", fsplit_at "l" (flength "l" `quot` #2).
Section lists.
Context `{heapG Σ}.
Implicit Types i : nat.
Implicit Types v : val.
Implicit Types vs : list val.
Lemma fnil_spec :
{{{ True }}} fnil #() {{{ RET flist []; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma fcons_spec v vs :
{{{ True }}} fcons v (flist vs) {{{ RET flist (v :: vs); True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma fisnil_spec vs:
{{{ True }}}
fisnil (flist vs)
{{{ RET #(if vs is [] then true else false); True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. destruct vs; wp_pures; by iApply "HΦ". Qed.
Lemma fhead_spec v vs :
{{{ True }}} fhead (flist (v :: vs)) {{{ RET v; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ftail_spec v vs :
{{{ True }}} ftail (flist (v :: vs)) {{{ RET flist vs; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma flookup_spec i vs v :
vs !! i = Some v
{{{ True }}} flookup #i (flist vs) {{{ RET v; True }}}.
Proof.
iIntros (Hi Φ _) "HΦ".
iInduction vs as [|v' vs] "IH" forall (i Hi);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. by iApply (fhead_spec with "[//]"). }
wp_lam. wp_pures.
wp_apply (ftail_spec with "[//]"); iIntros (_). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
Lemma finsert_spec i vs v :
is_Some (vs !! i)
{{{ True }}} finsert #i v (flist vs) {{{ RET flist (<[i:=v]>vs); True }}}.
Proof.
iIntros ([w Hi] Φ _) "HΦ".
iInduction vs as [|v' vs] "IH" forall (i Hi Φ);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. wp_apply (ftail_spec with "[//]"); iIntros (_).
wp_let. by iApply (fcons_spec with "[//]"). }
wp_lam; wp_pures.
wp_apply (ftail_spec with "[//]"); iIntros (_). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//]"); iIntros (_).
wp_apply (fhead_spec with "[//]"); iIntros "_".
by wp_apply (fcons_spec with "[//]").
Qed.
Lemma freplicate_spec i v :
{{{ True }}} freplicate #i v {{{ RET flist (replicate i v); True }}}.
Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
{ wp_lam; wp_pures. iApply (fnil_spec with "[//]"); auto. }
wp_lam; wp_pures.
rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply "IH"; iIntros (_). wp_let. by iApply (fcons_spec with "[//]").
Qed.
Lemma flength_spec vs :
{{{ True }}} flength (flist vs) {{{ RET #(length vs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
iInduction vs as [|v' vs] "IH" forall (Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". }
wp_lam. wp_match. wp_proj.
wp_apply "IH"; iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
Lemma fapp_spec vs1 vs2 :
{{{ True }}} fapp (flist vs1) (flist vs2) {{{ RET (flist (vs1 ++ vs2)); True }}}.
Proof.
iIntros (Φ _) "HΦ".
iInduction vs1 as [|v1 vs1] "IH" forall (Φ); simpl.
{ wp_rec. wp_pures. by iApply "HΦ". }
wp_rec. wp_pures. wp_apply "IH". iIntros (_). by wp_apply fcons_spec.
Qed.
Lemma fsnoc_spec vs v :
{{{ True }}} fsnoc (flist vs) v {{{ RET (flist (vs ++ [v])); True }}}.
Proof.
iIntros (Φ _) "HΦ". wp_lam. wp_apply (fnil_spec with "[//]"); iIntros (_).
wp_apply (fcons_spec with "[//]"); iIntros (_).
wp_apply (fapp_spec with "[//]"); iIntros (_). by iApply "HΦ".
Qed.
Lemma ftake_spec vs (n : nat) :
{{{ True }}} ftake (flist vs) #n {{{ RET flist (take n vs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
iInduction vs as [|x' vs] "IH" forall (n Φ).
- wp_rec. wp_pures.
destruct (bool_decide (n 0)); wp_pures; rewrite take_nil; by iApply "HΦ".
- wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply "IH"; iIntros (_).
wp_apply (fcons_spec with "[//]"); iIntros (_). by iApply "HΦ".
Qed.
Lemma fdrop_spec vs (n : nat) :
{{{ True }}} fdrop (flist vs) #n {{{ RET flist (drop n vs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
iInduction vs as [|x' vs] "IH" forall (n Φ).
- wp_rec. wp_pures.
destruct (bool_decide (n 0)); wp_pures; rewrite drop_nil; by iApply "HΦ".
- wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply "IH"; iIntros (_). by iApply "HΦ".
Qed.
Lemma fsplit_at_spec vs (n : nat) :
{{{ True }}}
fsplit_at (flist vs) #n
{{{ RET (flist (take n vs), flist (drop n vs)); True }}}.
Proof.
iIntros (Φ _) "HΦ". wp_lam.
wp_apply (fdrop_spec with "[//]"); iIntros (_).
wp_apply (ftake_spec with "[//]"); iIntros (_).
wp_pures. by iApply "HΦ".
Qed.
Lemma fsplit_spec vs :
{{{ True }}}
fsplit (flist vs)
{{{ ws1 ws2, RET (flist ws1, flist ws2); vs = ws1 ++ ws2 }}}.
Proof.
iIntros (Φ _) "HΦ". wp_lam.
wp_apply (flength_spec with "[//]"); iIntros (_). wp_pures.
rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
wp_apply (fsplit_at_spec with "[//]"); iIntros (_).
iApply "HΦ". by rewrite take_drop.
Qed.
End lists.
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
From actris.utils Require Import list compare spin_lock.
Definition qenqueue : val := λ: "q" "v", #().
Definition qdequeue : val := λ: "q", #().
Definition enq := true.
Definition deq := false.
Definition cont := true.
Definition stop := false.
Definition some := true.
Definition none := false.
Definition pd_loop : val :=
rec: "go" "q" "pc" "cc" "c" :=
if: "cc" #0 then #() else
if: recv "c" then (* enq/deq *)
if: recv "c" then (* cont/stop *)
let: "x" := recv "x" in
"go" (qenqueue "q" "x") "pc" "cc" "c"
else "go" "q" ("pc"-#1) "cc" "c"
else
if: lisnil "q" then
if: "pc" #0 then
send "c" #stop;;
"go" "q" "pc" ("cc"-#1) "c"
else
send "c" #cont;; send "c" #none;;
"go" "q" "pc" "cc" "c"
else
send "c" #cont;; send "c" #some;;
let: "qv" := qdequeue "q" in
send "c" (Snd "qv");;
"go" (Fst "qv") "pc" "cc" "c".
Definition new_pd : val := λ: "pc" "cc",
let: "q" := lnil #() in
let: "c" := start_chan (λ: "c", pd_loop "q" "pc" "cc" "c") in
let: "l" := new_lock #() in
("c", "l").
Definition pd_send : val := λ: "cl" "x",
acquire (Snd "cl");;
send (Fst "cl") #enq;; send (Fst "cl") #cont;; send (Fst "cl") "x";;
release (Snd "cl").
Definition pd_stop : val := λ: "cl",
acquire (Fst "cl");;
send (Snd "cl") #enq;; send (Snd "cl") #stop;;
release (Fst "cl").
Definition pd_recv : val :=
rec: "go" "cl" :=
acquire (Fst "cl");;
send (Snd "cl") #deq;;
if: recv (Snd "cl") then (* cont/stop *)
if: recv (Snd "cl") then (* some/none *)
let: "v" := recv (Snd "cl") in
release (Fst "cl");; SOME "v"
else release (Fst "cl");; "go" "c" "l"
else release (Fst "cl");; NONE.
Section sort_elem.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Definition queue_prot : iProto Σ := (END)%proto.
Lemma dist_queue_spec c :
{{{ c queue_prot @ N }}}
dist_queue (qnew #()) #0 #0 c
{{{ RET #(); c END @ N }}}.
Proof. Admitted.
(* Need predicate for end of production? *)
Definition produce_spec σ P (produce : val) :=
vs,
{{{ σ vs }}}
produce #()
{{{ v, RET v; ( w, v = SOMEV w P w σ (w::vs)) (v = NONEV) }}}.
Definition consume_spec σ P Q (consume : val) :=
vs, v : val,
{{{ σ vs P v }}}
consume v
{{{ RET #(); σ (v::vs) Q v }}}.
Lemma produce_consume_spec produce consume pσ cσ P Q pc cc :
pc > 0 cc > 0
produce_spec pσ P produce
consume_spec cσ P Q consume
{{{ pσ [] cσ [] }}}
produce_consume produce consume #pc #cc
{{{ vs, RET #(); pσ vs cσ vs [ list] v vs, Q v }}}.
Proof. Admitted.
(* Example producer *)
Definition ints_to_n (l : val) (n:nat) : val:=
λ: <>, let: "v" := !l in
if: "v" < #n
then l <- "v" + #1;; SOME "v"
else NONE.
Lemma ints_to_n_spec l n :
produce_spec (λ vs, ( loc, loc = LitV $ LitLoc l l #(length vs))%I)
(λ v, ⌜∃ i, v = LitV $ LitInt i%I) (ints_to_n #l n).
Proof.
iIntros (vs Φ) "Hσ HΦ".
iDestruct "Hσ" as (loc ->) "Hσ".
wp_lam. wp_load. wp_pures.
case_bool_decide.
- wp_store. wp_pures. iApply "HΦ".
(* Does this not exist? *)
assert ( n : nat, (n + 1) = (S n)). intros m. lia. rewrite H0.
by eauto 10 with iFrame.
- wp_pures. iApply "HΦ". by iRight.
Qed.
Definition consume_to_list l : val:=
λ: "v",
let: "xs" := !l in
l <- lcons "v" "xs".
Lemma consume_to_list_spec l :
consume_spec (λ vs, ( loc, loc = LitV $ LitLoc l l val_encode vs)%I)
(λ v, True%I) (λ v, True%I) (consume_to_list #l).
Proof. Admitted.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl auth frac csum.
From iris.base_logic.lib Require Import cancelable_invariants.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
Definition new_lock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
Class lockG Σ := LockG {
lock_tokG :> inG Σ (authR (optionUR (exclR fracR)));
lock_cinvG :> cinvG Σ;
}.
Definition lockΣ : gFunctors := #[GFunctor (authR (optionUR (exclR fracR))); cinvΣ].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition lock_inv (γ γi : gname) (lk : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, lk #b
if b then ( p, own γ ( (Excl' p)) cinv_own γi (p/2))
else own γ ( None) R)%I.
Definition is_lock (lk : loc) (R : iProp Σ) : iProp Σ :=
( γ γi : gname, meta lk N (γ,γi) cinv N γi (lock_inv γ γi lk R))%I.
Definition unlocked (lk : loc) (q : Qp) : iProp Σ :=
( γ γi : gname, meta lk N (γ,γi) cinv_own γi q)%I.
Definition locked (lk : loc) (q : Qp) : iProp Σ :=
( γ γi : gname, meta lk N (γ,γi) cinv_own γi (q/2) own γ ( (Excl' q)))%I.
Global Instance unlocked_fractional lk : Fractional (unlocked lk).
Proof.
intros q1 q2. iSplit.
- iDestruct 1 as (γ γi) "[#Hm [Hq Hq']]". iSplitL "Hq"; iExists γ, γi; by iSplit.
- iIntros "[Hq1 Hq2]". iDestruct "Hq1" as (γ γi) "[#Hm Hq1]".
iDestruct "Hq2" as (γ' γi') "[#Hm' Hq2]".
iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
iExists γ, γi; iSplit; first done. by iSplitL "Hq1".
Qed.
Global Instance unlocked_as_fractional γ :
AsFractional (unlocked γ p) (unlocked γ) p.
Proof. split. done. apply _. Qed.
Global Instance lock_inv_ne γ γi lk : NonExpansive (lock_inv γ γi lk).
Proof. solve_proper. Qed.
Global Instance is_lock_ne lk : NonExpansive (is_lock lk).
Proof. solve_proper. Qed.
Global Instance is_lock_persistent lk R : Persistent (is_lock lk R).
Proof. apply _. Qed.
Global Instance locked_timeless lk q : Timeless (locked lk q).
Proof. apply _. Qed.
Global Instance unlocked_timeless lk q : Timeless (unlocked lk q).
Proof. apply _. Qed.
Lemma lock_cancel E lk R : N E is_lock lk R - unlocked lk 1 ={E}= R.
Proof.
intros. iDestruct 1 as (γ γi) "#[Hm Hinv]". iDestruct 1 as (γ' γi') "[Hm' Hq]".
iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
iMod (cinv_open_strong with "[$] [$]") as "(HR & Hq & Hclose)"; first done.
iDestruct "HR" as ([]) "[Hl HR]".
- iDestruct "HR" as (p) "[_ Hq']". iDestruct (cinv_own_1_l with "Hq Hq'") as ">[]".
- iDestruct "HR" as "[_ $]". iApply "Hclose"; auto.
Qed.
Lemma new_lock_spec :
{{{ True }}}
new_lock #()
{{{ lk, RET #lk; unlocked lk 1 ( R, R ={}= is_lock lk R) }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
wp_apply (wp_alloc with "[//]"); iIntros (l) "[Hl Hm]".
iDestruct (meta_token_difference _ (N) with "Hm") as "[Hm1 Hm2]"; first done.
iMod (own_alloc ( None)) as (γ) "Hγ"; first by apply auth_auth_valid.
iMod (cinv_alloc_strong (λ _, True))
as (γi _) "[Hγi H]"; first by apply pred_infinite_True.
iMod (meta_set _ _ (γ,γi) with "Hm1") as "#Hm1"; first done.
iApply "HΦ"; iSplitL "Hγi"; first by (iExists γ, γi; auto).
iIntros "!>" (R) "HR".
iMod ("H" $! (lock_inv γ γi l R) with "[HR Hl Hγ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
iModIntro. iExists γ, γi; auto.
Qed.
Lemma try_acquire_spec lk R q :
{{{ is_lock lk R unlocked lk q }}}
try_acquire #lk
{{{ b, RET #b; if b is true then locked lk q R else unlocked lk q }}}.
Proof.
iIntros (Φ) "[#Hl Hq] HΦ". iDestruct "Hl" as (γ γi) "#[Hm Hinv]".
iDestruct "Hq" as (γ' γi') "[Hm' Hq]".
iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
wp_rec. wp_bind (CmpXchg _ _ _).
iInv N as "[HR Hq]"; iDestruct "HR" as ([]) "[Hl HR]".
- wp_cmpxchg_fail. iModIntro. iSplitL "Hl HR"; first (iExists true; iFrame).
wp_pures. iApply ("HΦ" $! false). iExists γ, γi; auto.
- wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]". iDestruct "Hq" as "[Hq Hq']".
iMod (own_update with "Hγ") as "[Hγ Hγ']".
{ by apply auth_update_alloc, (alloc_option_local_update (Excl q)). }
iModIntro. iSplitL "Hl Hγ Hq"; first (iNext; iExists true; eauto with iFrame).
wp_pures. iApply ("HΦ" $! true with "[$HR Hγ' Hq']"). iExists γ, γi; by iFrame.
Qed.
Lemma acquire_spec lk R q :
{{{ is_lock lk R unlocked lk q }}} acquire #lk {{{ RET #(); locked lk q R }}}.
Proof.
iIntros (Φ) "[#Hlk Hq] HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "[$Hlk $Hq]"); iIntros ([]).
- iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
- iIntros "Hq". wp_if. iApply ("IH" with "[$]"); auto.
Qed.
Lemma release_spec lk R q :
{{{ is_lock lk R locked lk q R }}} release #lk {{{ RET #(); unlocked lk q }}}.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (γ γi) "#[Hm Hinv]".
iDestruct "Hlocked" as (γ' γi') "(#Hm' & Hq & Hγ')".
iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
wp_lam. iInv N as "[HR' Hq]"; iDestruct "HR'" as ([]) "[Hl HR']".
- iDestruct "HR'" as (p) ">[Hγ Hq']".
iDestruct (own_valid_2 with "Hγ Hγ'")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
iMod (own_update_2 with "Hγ Hγ'") as "Hγ".
{ eapply auth_update_dealloc, delete_option_local_update; apply _. }
wp_store. iIntros "!>". iSplitL "Hl Hγ HR"; first (iExists false); iFrame.
iApply "HΦ". iExists γ, γi. iSplit; first done. by iSplitL "Hq".
- iDestruct "HR'" as "[>Hγ _]".
by iDestruct (own_valid_2 with "Hγ Hγ'")
as %[[[] ?%leibniz_equiv] _]%auth_both_valid.
Qed.
End proof.
Typeclasses Opaque is_lock locked.
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