From de9dac6ce67ae6fd87e6d167fe249bf6c6790421 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 11 Feb 2025 15:14:41 +0100 Subject: [PATCH] improve lazy rand module --- .../examples/lazy_rand/lazy_rand_impl.v | 174 ++++++++---------- .../examples/lazy_rand/lazy_rand_interface.v | 54 +++--- .../examples/lazy_rand/lazy_rand_race.v | 40 ++-- 3 files changed, 118 insertions(+), 150 deletions(-) diff --git a/theories/coneris/examples/lazy_rand/lazy_rand_impl.v b/theories/coneris/examples/lazy_rand/lazy_rand_impl.v index 98b1aaba..c8bcddc0 100644 --- a/theories/coneris/examples/lazy_rand/lazy_rand_impl.v +++ b/theories/coneris/examples/lazy_rand/lazy_rand_impl.v @@ -1,5 +1,5 @@ From iris.algebra Require Import gmap. -From clutch.coneris Require Import coneris abstract_tape hocap_rand_alt lock lazy_rand_interface. +From clutch.coneris Require Import coneris hocap_rand_alt lock lazy_rand_interface. Set Default Proof Using "Type*". @@ -39,7 +39,7 @@ Section impl. Hv: !ghost_mapG Σ () (option (nat*nat)), lo:lock, Hl: lockG Σ, (* Hv: !inG Σ (excl_authR (optionO (prodO natO natO))), *) - Ht: !abstract_tapesGS Σ, + (* Ht: !abstract_tapesGS Σ, *) Hr: !rand_spec' val_size }. @@ -72,14 +72,14 @@ Section impl. Definition rand_tape_frag α n γ := - (rand_tapes α (option_to_list n) γ.1 ∗ α ◯↪N ( val_size ; option_to_list n ) @ γ.2)%I. + (rand_tapes α (option_to_list n) γ )%I. - Definition rand_tape_auth m γ :=(([∗ set] α∈ dom m, rand_token α γ.1) ∗ - ● ((λ x, (val_size, option_to_list x))<$>m) @ γ.2)%I. + (* Definition rand_tape_auth m γ :=(([∗ set] α∈ dom m, rand_token α γ.1) ∗ *) + (* ● ((λ x, (val_size, option_to_list x))<$>m) @ γ.2)%I. *) Definition abstract_lazy_rand_inv N γ_tape:= - (inv (N.@"tape") (∃ m, rand_tape_auth m γ_tape) ∗ is_rand (N.@"rand") γ_tape.1)%I. + ( is_rand (N) γ_tape)%I. Definition option_to_gmap n : gmap () (option (nat*nat)):= @@ -116,47 +116,43 @@ Section impl. abstract_lazy_rand_inv N γ_tape ∗ is_lock (L:=Hl) γ_lock lk (∃ res, P res ∗ rand_auth res γ_view ∗ l↦(option_to_val res)))%I. - Lemma rand_tape_presample_impl N c P {HP:∀ n, Timeless (P n)} γ γ_view γ_lock E m α ε (ε2:fin (S val_size) -> R): - ↑(N.@"rand")⊆E -> + Lemma rand_tape_presample_impl N c P {HP:∀ n, Timeless (P n)} γ γ_view γ_lock E α ε (ε2:fin (S val_size) -> R): + ↑(N)⊆E -> (∀ x, (0 <= ε2 x)%R)-> (SeriesC (λ n : fin (S val_size), 1 / S val_size * ε2 n) <= ε)%R -> lazy_rand_inv N c P γ γ_view γ_lock -∗ - rand_tape_auth m γ -∗ rand_tape_frag α None γ -∗ ↯ ε -∗ + rand_tape_frag α None γ -∗ ↯ ε -∗ state_update E E (∃ n, ↯ (ε2 n) ∗ - rand_tape_auth (<[α:=Some (fin_to_nat n)]>m) γ ∗ rand_tape_frag α (Some (fin_to_nat n)) γ). Proof. - iIntros (???) "(%&%&->&#[? Hinv]&#?) [Htokens Htauth] [Htape Hfrag] Herr". - iDestruct (abstract_tapes_agree with "[$][$]") as "%H'". - rewrite lookup_fmap in H'. apply fmap_Some_1 in H'. - destruct H' as (?&Hsome&?). simplify_eq. + iIntros (???) "(%&%&->&# Hinv&#?) Htape Herr". + (* iDestruct (abstract_tapes_agree with "[$][$]") as "%H'". *) + (* rewrite lookup_fmap in H'. apply fmap_Some_1 in H'. *) + (* destruct H' as (?&Hsome&?). simplify_eq. *) iMod (rand_tapes_presample with "[$][$][$]") as "(%&Htape&?)"; try done. - iMod (abstract_tapes_presample with "[$][$]") as "[? H]". - iFrame. iModIntro. - iSplitL "Htokens". - - by rewrite dom_insert_lookup_L. - - by rewrite fmap_insert. + (* iMod (abstract_tapes_presample with "[$][$]") as "[? H]". *) + by iFrame. Qed. - Lemma lazy_rand_presample_impl N c P {HP: ∀ n, Timeless (P n)} γ γ_view γ_lock Q - E : - ↑(N.@"tape") ⊆ E -> - lazy_rand_inv N c P γ γ_view γ_lock -∗ - (∀ m, rand_tape_auth m γ -∗ - state_update (E∖↑(N.@"tape")) (E∖↑(N.@"tape")) - (∃ m', rand_tape_auth m' γ ∗ Q m m') - ) -∗ - state_update E E ( - ∃ m m', Q m m' - ). - Proof. - iIntros (?) "(%&%&->&#[Hinv ?]&#?) Hvs". - iInv "Hinv" as ">(%&?)" "Hclose". - iMod ("Hvs" with "[$]") as "(%&?&?)". - iMod ("Hclose" with "[$]") as "_". - by iFrame. - Qed. + (* Lemma lazy_rand_presample_impl N c P {HP: ∀ n, Timeless (P n)} γ γ_view γ_lock Q *) + (* E : *) + (* ↑(N.@"tape") ⊆ E -> *) + (* lazy_rand_inv N c P γ γ_view γ_lock -∗ *) + (* (∀ m, rand_tape_auth m γ -∗ *) + (* state_update (E∖↑(N.@"tape")) (E∖↑(N.@"tape")) *) + (* (∃ m', rand_tape_auth m' γ ∗ Q m m') *) + (* ) -∗ *) + (* state_update E E ( *) + (* ∃ m m', Q m m' *) + (* ). *) + (* Proof. *) + (* iIntros (?) "(%&%&->&#[Hinv ?]&#?) Hvs". *) + (* iInv "Hinv" as ">(%&?)" "Hclose". *) + (* iMod ("Hvs" with "[$]") as "(%&?&?)". *) + (* iMod ("Hclose" with "[$]") as "_". *) + (* by iFrame. *) + (* Qed. *) Lemma lazy_rand_init_impl N P {HP: ∀ n, Timeless (P n)} : {{{ P None }}} @@ -181,93 +177,78 @@ Section impl. iIntros (??) "#Hlock". wp_pures. iMod (rand_inv_create_spec) as "(%&#Hrand)"; last first. - - iMod (abstract_tapes_alloc ∅) as "(%&Hm&_)". - iMod (inv_alloc _ _ (∃ m, rand_tape_auth m (_,_)) with "[Hm]") as "#Hinv". - { iNext. iExists ∅. rewrite /rand_tape_auth. rewrite fmap_empty. - iFrame. by rewrite dom_empty_L. } + - (* iMod (abstract_tapes_alloc ∅) as "(%&Hm&_)". *) + (* iMod (inv_alloc _ _ (∃ m, rand_tape_auth m (_,_)) with "[Hm]") as "#Hinv". *) + (* { iNext. iExists ∅. rewrite /rand_tape_auth. rewrite fmap_empty. *) + (* iFrame. by rewrite dom_empty_L. } *) iApply "HΦ". iFrame "Hlock". - rewrite /abstract_lazy_rand_inv. iExists (_,_). - by iFrame "Hrand Hinv". + rewrite /abstract_lazy_rand_inv. iExists _. + by iFrame "Hrand". - done. Qed. - Lemma lazy_rand_alloc_tape_impl N c P {HP: ∀ n, Timeless (P n)} γ_tape γ_view γ_lock Q: - {{{ lazy_rand_inv N c P γ_tape γ_view γ_lock ∗ - (∀ (m:gmap val (option nat)) α, ⌜α∉dom m⌝ -∗ |={⊤∖↑N.@"tape"}=> Q α) + Lemma lazy_rand_alloc_tape_impl N c P {HP: ∀ n, Timeless (P n)} γ_tape γ_view γ_lock : + {{{ lazy_rand_inv N c P γ_tape γ_view γ_lock }}} allocate_tape_prog #() - {{{ (α: val), RET α; rand_tape_frag α None γ_tape ∗ Q α }}}. + {{{ (α: val), RET α; rand_tape_frag α None γ_tape }}}. Proof. - iIntros (Φ) "[(%&%&->&#[Hinv ?]&_) Hvs] HΦ". + iIntros (Φ) "(%&%&->&#Hinv &_) HΦ". rewrite /allocate_tape_prog. wp_pures. iApply pgl_wp_fupd. wp_apply (rand_allocate_tape_spec with "[//]") as (α) "[Htoken Hrand]"; first done. - iInv "Hinv" as ">(%m&Htokens&Hauth)" "Hclose". - iAssert (⌜α∉dom m⌝)%I as "%". - { iIntros "%H". - rewrite big_sepS_elem_of_acc; last done. - iDestruct "Htokens" as "[? ?]". - iApply (rand_token_exclusive with "[$][$]"). - } - iMod ("Hvs" with "[//]") as "HQ". - iMod (abstract_tapes_new with "[$]") as "[Hauth Htape]"; last first. - - iMod ("Hclose" with "[Hauth Htoken Htokens]"). - + iExists (<[_:=_]> _). rewrite /rand_tape_auth. rewrite fmap_insert. iFrame. - rewrite dom_insert_L big_sepS_insert; last done. - iFrame. - + iApply "HΦ". by iFrame. - - rewrite lookup_fmap. apply not_elem_of_dom_1 in H. by rewrite H. + iApply "HΦ". + by iFrame. Qed. Lemma lazy_rand_spec_impl N c P {HP: ∀ n, Timeless (P n)} γ_tape γ_view γ_lock Q1 Q2 α (tid:nat): {{{ lazy_rand_inv N c P γ_tape γ_view γ_lock ∗ - ( ∀ n m, P n -∗ rand_auth n γ_view -∗ rand_tape_auth m γ_tape -∗ state_update (⊤∖↑N.@"tape") (⊤∖↑N.@"tape") + ( ∀ n, P n -∗ rand_auth n γ_view -∗ state_update (⊤) (⊤) match n with - | Some (res, tid') => P n ∗ rand_auth n γ_view ∗ rand_tape_auth m γ_tape ∗ Q1 res tid' - | None => ∃ n', rand_tape_frag α (Some n') γ_tape ∗ rand_tape_auth (<[α:=Some n']> m) γ_tape ∗ + | Some (res, tid') => P n ∗ rand_auth n γ_view ∗ Q1 res tid' + | None => ∃ n', rand_tape_frag α (Some n') γ_tape ∗ (rand_tape_frag α None γ_tape - ={⊤∖↑N.@"tape"}=∗ P (Some (n', tid)) ∗ rand_auth (Some (n', tid)) γ_view ∗ Q2 n' tid) + ={⊤}=∗ P (Some (n', tid)) ∗ rand_auth (Some (n', tid)) γ_view ∗ Q2 n' tid) end ) }}} - lazy_read_rand_prog c α #tid + lazy_read_rand_prog c α #tid {{{ (res' tid':nat), RET (#res', #tid')%V; (Q1 res' tid' ∨ Q2 res' tid' ) }}}. Proof. - iIntros (Φ) "[(%&%&->&#[Hinv ?]&#Hlock) Hvs] HΦ". + iIntros (Φ) "[(%&%&->&#Hinv&#Hlock) Hvs] HΦ". rewrite /lazy_read_rand_prog. wp_pures. wp_apply (acquire_spec with "[$]") as "[Hl (%res&HP&(Hauth & Hfrag & %Hvalid)&Hloc)]". wp_pures. wp_load. iApply state_update_pgl_wp. - iInv ("Hinv") as ">(%&Htokens&Htauth)" "Hclose". - iMod ("Hvs" with "[$][$Hauth $Hfrag//][$]") as "Hcont". + (* iInv ("Hinv") as ">(%&Htokens&Htauth)" "Hclose". *) + iMod ("Hvs" with "[$][$Hauth $Hfrag//]") as "Hcont". destruct res as [[]|]. - - iDestruct "Hcont" as "(HP&Hauth &Htauth&HQ)". - iMod ("Hclose" with "[$Htauth]") as "_". + - iDestruct "Hcont" as "(HP&Hauth &HQ)". iModIntro. wp_pures. wp_apply (release_spec with "[$Hlock $Hl $HP $Hloc $Hauth]"). iIntros. wp_pures. iApply "HΦ". by iFrame. - - iDestruct "Hcont" as "(%&[Ht Htfrag] &[Htokens Htauth] & Hvs)". - iMod ("Hclose" with "[$Htauth $Htokens]") as "_". + - iDestruct "Hcont" as "(%&Ht & Hvs)". + (* iMod ("Hclose" with "[$Htauth $Htokens]") as "_". *) iModIntro. wp_pures. wp_apply (rand_tape_spec_some with "[$]") as "Htape"; first done. iApply fupd_pgl_wp. - iInv ("Hinv") as ">(%&Htokens&Htauth)" "Hclose". - iDestruct (abstract_tapes_agree with "[$][$]") as "%Hsome". - apply lookup_fmap_Some in Hsome. - destruct Hsome as ([x|]&?&Hsome); simplify_eq. - iMod (abstract_tapes_pop with "[$][$]") as "[Hauth Htape']". + (* iInv ("Hinv") as ">(%&Htokens&Htauth)" "Hclose". *) + (* iDestruct (abstract_tapes_agree with "[$][$]") as "%Hsome". *) + (* apply lookup_fmap_Some in Hsome. *) + (* destruct Hsome as ([x|]&?&Hsome); simplify_eq. *) + (* iMod (abstract_tapes_pop with "[$][$]") as "[Hauth Htape']". *) iMod ("Hvs" with "[$]") as "(HP&Hrand&HQ)". - iMod ("Hclose" with "[Hauth Htokens]") as "_". - { iExists (<[_:=None]>_). - rewrite /rand_tape_auth. rewrite fmap_insert. - rewrite dom_insert_lookup_L; last done. iFrame. - } + (* iMod ("Hclose" with "[Hauth Htokens]") as "_". *) + (* { iExists (<[_:=None]>_). *) + (* rewrite /rand_tape_auth. rewrite fmap_insert. *) + (* rewrite dom_insert_lookup_L; last done. iFrame. *) + (* } *) iModIntro. wp_pures. wp_store. @@ -282,12 +263,12 @@ Section impl. allocate_tape := allocate_tape_prog; lazy_read_rand := lazy_read_rand_prog; lazy_rand_interface.rand_tape_frag := rand_tape_frag; - lazy_rand_interface.rand_tape_auth := rand_tape_auth; + (* lazy_rand_interface.rand_tape_auth := rand_tape_auth; *) lazy_rand_interface.rand_auth := rand_auth; lazy_rand_interface.rand_frag := rand_frag; rand_inv:=lazy_rand_inv; rand_tape_presample:=rand_tape_presample_impl; - lazy_rand_presample:=lazy_rand_presample_impl; + (* lazy_rand_presample:=lazy_rand_presample_impl; *) lazy_rand_init:=lazy_rand_init_impl; lazy_rand_alloc_tape:=lazy_rand_alloc_tape_impl; lazy_rand_spec:=lazy_rand_spec_impl @@ -298,22 +279,22 @@ Section impl. Qed. Next Obligation. rewrite /rand_tape_frag/=. - iIntros (???) "[??]". + iIntros (???) "?". iDestruct (rand_tapes_valid with "[$]") as "%H". by rewrite Forall_singleton in H. Qed. Next Obligation. rewrite /rand_tape_frag. - iIntros (????) "[??][??]". + iIntros (????) "??". iApply (rand_tapes_exclusive with "[$][$]"). Qed. - Next Obligation. - rewrite /rand_tape_auth/rand_tape_frag. - iIntros (?? x ?) "[??][??]". - iDestruct (abstract_tapes_agree with "[$][$]") as "%Hsome". - apply lookup_fmap_Some in Hsome. - by destruct Hsome as ([[]|]&?&Hsome); destruct x; simplify_eq. - Qed. + (* Next Obligation. *) + (* rewrite /rand_tape_auth/rand_tape_frag. *) + (* iIntros (?? x ?) "[??][??]". *) + (* iDestruct (abstract_tapes_agree with "[$][$]") as "%Hsome". *) + (* apply lookup_fmap_Some in Hsome. *) + (* by destruct Hsome as ([[]|]&?&Hsome); destruct x; simplify_eq. *) + (* Qed. *) Next Obligation. rewrite /rand_auth. iIntros (???) "[??][??]". @@ -354,4 +335,5 @@ Section impl. iFrame. by iMod (ghost_map_elem_persist with "[$]") as "$". Qed. + End impl. diff --git a/theories/coneris/examples/lazy_rand/lazy_rand_interface.v b/theories/coneris/examples/lazy_rand/lazy_rand_interface.v index dac638e4..bff4e0af 100644 --- a/theories/coneris/examples/lazy_rand/lazy_rand_interface.v +++ b/theories/coneris/examples/lazy_rand/lazy_rand_interface.v @@ -17,15 +17,15 @@ Class lazy_rand `{!conerisGS Σ} (val_size:nat):= Lazy_Rand rand_inv (N:namespace) (c: val) (P: option (nat*nat) -> iProp Σ) {HP: ∀ n, Timeless (P n)} (γ:rand_tape_gname) (γ':rand_view_gname) (γ_lock:rand_lock_gname): iProp Σ; rand_tape_frag (α:val) (n:option nat) (γ:rand_tape_gname): iProp Σ; - rand_tape_auth (m:gmap val (option nat)) (γ:rand_tape_gname) :iProp Σ; + (* rand_tape_auth (m:gmap val (option nat)) (γ:rand_tape_gname) :iProp Σ; *) rand_auth (m:option (nat*nat)) (γ:rand_view_gname) : iProp Σ; rand_frag (res:nat) (tid:nat) (γ:rand_view_gname) : iProp Σ; (** * General properties of the predicates *) #[global] rand_tape_frag_timeless α ns γ:: Timeless (rand_tape_frag α ns γ); - #[global] rand_tape_auth_timeless m γ:: - Timeless (rand_tape_auth m γ); + (* #[global] rand_tape_auth_timeless m γ:: *) + (* Timeless (rand_tape_auth m γ); *) #[global] rand_auth_timeless n γ:: Timeless (rand_auth n γ); #[global] rand_frag_timeless n tid γ:: @@ -42,8 +42,8 @@ Class lazy_rand `{!conerisGS Σ} (val_size:nat):= Lazy_Rand rand_tape_frag α ns γ-∗ rand_tape_frag α ns' γ-∗ False; (* rand_tape_auth_exclusive m m' γ: *) (* rand_tape_auth m γ -∗ rand_tape_auth m' γ -∗ False; *) - rand_tape_auth_frag_agree m α ns γ: - rand_tape_auth m γ -∗ rand_tape_frag α ns γ -∗ ⌜m!!α=Some ns⌝; + (* rand_tape_auth_frag_agree m α ns γ: *) + (* rand_tape_auth m γ -∗ rand_tape_frag α ns γ -∗ ⌜m!!α=Some ns⌝; *) rand_auth_exclusive n n' γ: rand_auth n γ -∗ rand_auth n' γ -∗ False; @@ -63,15 +63,14 @@ Class lazy_rand `{!conerisGS Σ} (val_size:nat):= Lazy_Rand (* rand_tape_auth_alloc m α γ: *) (* m!!α=None -> rand_tape_auth m γ ==∗ rand_tape_auth (<[α:=[]]> m) γ ∗ rand_tape α [] γ; *) - rand_tape_presample N c P {HP:∀ n, Timeless (P n)} γ γ_view γ_lock E m α ε (ε2:fin (S val_size) -> R): - ↑(N.@"rand")⊆E -> + rand_tape_presample N c P {HP:∀ n, Timeless (P n)} γ γ_view γ_lock E α ε (ε2:fin (S val_size) -> R): + ↑(N)⊆E -> (∀ x, (0 <= ε2 x)%R)-> (SeriesC (λ n : fin (S val_size), 1 / S val_size * ε2 n) <= ε)%R -> rand_inv N c P γ γ_view γ_lock -∗ - rand_tape_auth m γ -∗ rand_tape_frag α None γ -∗ ↯ ε -∗ + rand_tape_frag α None γ -∗ ↯ ε -∗ state_update E E (∃ n, ↯ (ε2 n) ∗ - rand_tape_auth (<[α:=Some (fin_to_nat n)]>m) γ ∗ rand_tape_frag α (Some (fin_to_nat n)) γ); (* rand_auth_exclusive m m' γ: *) (* rand_auth m γ -∗ rand_auth m' γ -∗ False; *) @@ -83,17 +82,17 @@ Class lazy_rand `{!conerisGS Σ} (val_size:nat):= Lazy_Rand (* m!!k=None -> rand_auth m γ ==∗ (rand_auth (<[k:=v]> m) γ ∗ rand_frag k v γ); *) - lazy_rand_presample N c P {HP: ∀ n, Timeless (P n)} γ γ_view γ_lock Q - E : - ↑(N.@"tape") ⊆ E -> - rand_inv N c P γ γ_view γ_lock -∗ - (∀ m, rand_tape_auth m γ -∗ - state_update (E∖↑(N.@"tape")) (E∖↑(N.@"tape")) - (∃ m', rand_tape_auth m' γ ∗ Q m m') - ) -∗ - state_update E E ( - ∃ m m', Q m m' - ); + (* lazy_rand_presample N c P {HP: ∀ n, Timeless (P n)} γ γ_view γ_lock Q *) + (* E : *) + (* ↑(N.@"tape") ⊆ E -> *) + (* rand_inv N c P γ γ_view γ_lock -∗ *) + (* (∀ m, rand_tape_auth m γ -∗ *) + (* state_update (E∖↑(N.@"tape")) (E∖↑(N.@"tape")) *) + (* (∃ m', rand_tape_auth m' γ ∗ Q m m') *) + (* ) -∗ *) + (* state_update E E ( *) + (* ∃ m m', Q m m' *) + (* ); *) lazy_rand_init N P {HP: ∀ n, Timeless (P n)} : {{{ P None }}} @@ -102,21 +101,20 @@ Class lazy_rand `{!conerisGS Σ} (val_size:nat):= Lazy_Rand ∃ γ γ_view γ_lock, rand_inv N c P γ γ_view γ_lock }}}; - lazy_rand_alloc_tape N c P {HP: ∀ n, Timeless (P n)} γ_tape γ_view γ_lock Q: - {{{ rand_inv N c P γ_tape γ_view γ_lock ∗ - (∀ (m:gmap val (option nat)) α, ⌜α∉dom m⌝ -∗ |={⊤∖↑N.@"tape"}=> Q α) + lazy_rand_alloc_tape N c P {HP: ∀ n, Timeless (P n)} γ_tape γ_view γ_lock: + {{{ rand_inv N c P γ_tape γ_view γ_lock }}} allocate_tape #() - {{{ (α: val), RET α; rand_tape_frag α None γ_tape ∗ Q α }}}; + {{{ (α: val), RET α; rand_tape_frag α None γ_tape }}}; lazy_rand_spec N c P {HP: ∀ n, Timeless (P n)} γ_tape γ_view γ_lock Q1 Q2 α (tid:nat): {{{ rand_inv N c P γ_tape γ_view γ_lock ∗ - ( ∀ n m, P n -∗ rand_auth n γ_view -∗ rand_tape_auth m γ_tape -∗ state_update (⊤∖↑N.@"tape") (⊤∖↑N.@"tape") + ( ∀ n, P n -∗ rand_auth n γ_view -∗ state_update (⊤) (⊤) match n with - | Some (res, tid') => P n ∗ rand_auth n γ_view ∗ rand_tape_auth m γ_tape ∗ Q1 res tid' - | None => ∃ n', rand_tape_frag α (Some n') γ_tape ∗ rand_tape_auth (<[α:=Some n']> m) γ_tape ∗ + | Some (res, tid') => P n ∗ rand_auth n γ_view ∗ Q1 res tid' + | None => ∃ n', rand_tape_frag α (Some n') γ_tape ∗ ( rand_tape_frag α None γ_tape - ={⊤∖↑N.@"tape"}=∗ P (Some (n', tid)) ∗ rand_auth (Some (n', tid)) γ_view ∗ Q2 n' tid) + ={⊤}=∗ P (Some (n', tid)) ∗ rand_auth (Some (n', tid)) γ_view ∗ Q2 n' tid) end ) }}} diff --git a/theories/coneris/examples/lazy_rand/lazy_rand_race.v b/theories/coneris/examples/lazy_rand/lazy_rand_race.v index 4be530aa..2411472a 100644 --- a/theories/coneris/examples/lazy_rand/lazy_rand_race.v +++ b/theories/coneris/examples/lazy_rand/lazy_rand_race.v @@ -61,23 +61,17 @@ Section race. wp_pures. wp_apply (wp_par (λ res, ∃ (n:nat), ⌜(#n, #n)%V = res⌝ ∗ rand_frag n n _)%I (λ res, ∃ (n:nat), ⌜(#n, #n)%V = res⌝ ∗ rand_frag n n _)%I with "[][]"). - - wp_apply (lazy_rand_alloc_tape _ _ ). - { iSplit; last by iIntros. done. } - iIntros (α) "[Ht _]". + - wp_apply (lazy_rand_alloc_tape _ _ with "[//]"). + iIntros (α) "Ht". replace #0 with (# (Z.of_nat 0)) by done. wp_apply (lazy_rand_spec _ _ _ _ _ _ (λ x y, ⌜x=y⌝ ∗ rand_frag x x _)%I (λ x y, ⌜x=y⌝ ∗ rand_frag x x _)%I with "[-]"). + iSplit; first done. - simpl. iIntros (n m) "H1 Hauth Htauth". - iApply (state_update_inv_acc with "Hinv2"). - { apply subseteq_difference_r; last done. - by apply ndot_preserve_disjoint_r, ndot_ne_disjoint. - } + simpl. iIntros (n) "H1 Hauth". + iApply (state_update_inv_acc with "Hinv2"); first done. iIntros ">[[H2 Herr]|H2]"; iDestruct "H1" as "[(->&?)|(%&->&?)]"; iDestruct (ghost_var_agree with "[$][$]") as "%"; simplify_eq. - * iMod (rand_tape_presample _ _ _ _ _ _ _ _ _ _ (λ x, if bool_decide (fin_to_nat x = 0%nat) then 0 else 1) with "[$][$][$][$]") as "(%n&?&?&?)". - { apply subseteq_difference_r. - - by apply ndot_preserve_disjoint_l, ndot_ne_disjoint. - - apply subseteq_difference_r; last done. - by apply ndot_ne_disjoint. + * iMod (rand_tape_presample _ _ _ _ _ _ _ _ _ (λ x, if bool_decide (fin_to_nat x = 0%nat) then 0 else 1) with "[$][$][$]") as "(%n&?&?)". + { apply subseteq_difference_r; last done. + by apply ndot_ne_disjoint. } { intros. case_bool_decide; simpl; lra. } { rewrite SeriesC_finite_foldr/=. lra. } @@ -102,23 +96,17 @@ Section race. repeat iSplit; try done. iRight. iFrame. by iExists _. + by iIntros (??) "[(->&#$)|(->&#$)]". - - wp_apply (lazy_rand_alloc_tape _ _ ). - { iSplit; last by iIntros. done. } - iIntros (α) "[Ht _]". + - wp_apply (lazy_rand_alloc_tape _ _ ); first done. + iIntros (α) "Ht". replace #1 with (# (Z.of_nat 1)) by done. wp_apply (lazy_rand_spec _ _ _ _ _ _ (λ x y, ⌜x=y⌝ ∗ rand_frag x x _)%I (λ x y, ⌜x=y⌝ ∗ rand_frag x x _)%I with "[-]"). + iSplit; first done. - simpl. iIntros (n m) "H1 Hauth Htauth". - iApply (state_update_inv_acc with "Hinv2"). - { apply subseteq_difference_r; last done. - by apply ndot_preserve_disjoint_r, ndot_ne_disjoint. - } + simpl. iIntros (n) "H1 Hauth". + iApply (state_update_inv_acc with "Hinv2"); first done. iIntros ">[[H2 Herr]|H2]"; iDestruct "H1" as "[(->&?)|(%&->&?)]"; iDestruct (ghost_var_agree with "[$][$]") as "%"; simplify_eq. - * iMod (rand_tape_presample _ _ _ _ _ _ _ _ _ _ (λ x, if bool_decide (fin_to_nat x = 1%nat) then 0 else 1) with "[$][$][$][$]") as "(%n&?&?&?)". - { apply subseteq_difference_r. - - by apply ndot_preserve_disjoint_l, ndot_ne_disjoint. - - apply subseteq_difference_r; last done. - by apply ndot_ne_disjoint. + * iMod (rand_tape_presample _ _ _ _ _ _ _ _ _ (λ x, if bool_decide (fin_to_nat x = 1%nat) then 0 else 1) with "[$][$][$]") as "(%n&?&?)". + { apply subseteq_difference_r; last done. + by apply ndot_ne_disjoint. } { intros. case_bool_decide; simpl; lra. } { rewrite SeriesC_finite_foldr/=. lra. }