Commit 13900169 by Zhen Zhang

### Update according to dependencies

parent 1c4eac1d
 ... @@ -16,8 +16,8 @@ Section atomic. ... @@ -16,8 +16,8 @@ Section atomic. (Ei Eo: coPset) (* inside/outside masks *) (Ei Eo: coPset) (* inside/outside masks *) (e: expr _) : iProp Σ := (e: expr _) : iProp Σ := (∀ P Q, (P ={Eo, Ei}=> ∃ x:A, (∀ P Q, (P ={Eo, Ei}=> ∃ x:A, α x ★ α x ∗ ((α x ={Ei, Eo}=★ P) ∧ ((α x ={Ei, Eo}=∗ P) ∧ (∀ v, β x v ={Ei, Eo}=★ Q v)) (∀ v, β x v ={Ei, Eo}=∗ Q v)) ) -★ {{ P }} e @ ⊤ {{ Q }})%I. ) -∗ {{ P }} e @ ⊤ {{ Q }})%I. End atomic. End atomic.
 ... @@ -20,7 +20,7 @@ Section incr. ... @@ -20,7 +20,7 @@ Section incr. (* TODO: Can we have a more WP-style definition and avoid the equality? *) (* TODO: Can we have a more WP-style definition and avoid the equality? *) Definition incr_triple (l: loc) := Definition incr_triple (l: loc) := atomic_triple (fun (v: Z) => l ↦ #v)%I atomic_triple (fun (v: Z) => l ↦ #v)%I (fun v ret => ret = #v ★ l ↦ #(v + 1))%I (fun v ret => ret = #v ∗ l ↦ #(v + 1))%I (nclose heapN) (nclose heapN) ⊤ ⊤ (incr #l). (incr #l). ... @@ -61,7 +61,7 @@ Section user. ... @@ -61,7 +61,7 @@ Section user. Definition incr_2 : val := Definition incr_2 : val := λ: "x", λ: "x", let: "l" := ref "x" in let: "l" := ref "x" in incr "l" || incr "l";; incr "l" ||| incr "l";; !"l". !"l". (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *) (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *) ... @@ -74,8 +74,8 @@ Section user. ... @@ -74,8 +74,8 @@ Section user. wp_alloc l as "Hl". wp_alloc l as "Hl". iMod (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto. iMod (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto. wp_let. wp_let. wp_bind (_ || _)%E. wp_bind (_ ||| _)%E. iApply (wp_par (λ _, True%I) (λ _, True%I)). iApply (wp_par (λ _, True%I) (λ _, True%I) with "[]"). iFrame "Hh". iFrame "Hh". (* prove worker triple *) (* prove worker triple *) iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//. iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//. ... ...
 ... @@ -23,7 +23,7 @@ Section atomic_pair. ... @@ -23,7 +23,7 @@ Section atomic_pair. Definition ϕ (ls: val) (xs: val) : iProp Σ := Definition ϕ (ls: val) (xs: val) : iProp Σ := (∃ (l1 l2: loc) (x1 x2: val), (∃ (l1 l2: loc) (x1 x2: val), ls = (#l1, #l2)%V ★ xs = (x1, x2)%V ★ l1 ↦ x1 ★ l2 ↦ x2)%I. ls = (#l1, #l2)%V ∗ xs = (x1, x2)%V ∗ l1 ↦ x1 ∗ l2 ↦ x2)%I. Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ := Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ := (■ ∃ a b x1 x2 x1' x2': val, (■ ∃ a b x1 x2 x1' x2': val, ... @@ -69,8 +69,8 @@ Section atomic_pair. ... @@ -69,8 +69,8 @@ Section atomic_pair. Lemma pcas_atomic_spec (mk_syncer: val) (l1 l2: loc) (x1 x2: val) : Lemma pcas_atomic_spec (mk_syncer: val) (l1 l2: loc) (x1 x2: val) : heapN ⊥ N → mk_syncer_spec N mk_syncer → heapN ⊥ N → mk_syncer_spec N mk_syncer → heap_ctx ★ l1 ↦ x1 ★ l2 ↦ x2 heap_ctx ∗ l1 ↦ x1 ∗ l2 ↦ x2 ⊢ WP sync mk_syncer pcas_seq (LitV l1, LitV l2)%V {{ f, ∃ γ, gHalf γ (x1, x2)%V ★ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ }}. ⊢ WP sync mk_syncer pcas_seq (LitV l1, LitV l2)%V {{ f, ∃ γ, gHalf γ (x1, x2)%V ∗ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ }}. Proof. Proof. iIntros (HN Hmk_syncer) "(#Hh & Hl1 & Hl2)". iIntros (HN Hmk_syncer) "(#Hh & Hl1 & Hl2)". iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//. iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//. ... ...
 ... @@ -20,13 +20,13 @@ Section atomic_sync. ... @@ -20,13 +20,13 @@ Section atomic_sync. Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g). Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g). Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) := Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) := (∀ g, {{ ϕ g ★ α g }} f x {{ v, ∃ g', ϕ g' ★ β g g' v }})%I. (∀ g, {{ ϕ g ∗ α g }} f x {{ v, ∃ g', ϕ g' ∗ β g g' v }})%I. (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *) (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *) Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) := Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) := (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x → (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x → atomic_triple (fun g => gHalf γ g ★ □ α g)%I atomic_triple (fun g => gHalf γ g ∗ □ α g)%I (fun g v => ∃ g', gHalf γ g' ★ β g g' v)%I (fun g v => ∃ g', gHalf γ g' ∗ β g g' v)%I ∅ ⊤ (f' x))%I. ∅ ⊤ (f' x))%I. (* TODO: Use our usual style with a generic post-condition. *) (* TODO: Use our usual style with a generic post-condition. *) ... @@ -42,7 +42,7 @@ Section atomic_sync. ... @@ -42,7 +42,7 @@ Section atomic_sync. Definition atomic_syncer_spec (mk_syncer: val) := Definition atomic_syncer_spec (mk_syncer: val) := ∀ (g0: A) (ϕ: A → iProp Σ), ∀ (g0: A) (ϕ: A → iProp Σ), heapN ⊥ N → heapN ⊥ N → {{{ heap_ctx ★ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 ★ is_atomic_syncer ϕ γ s }}}. {{{ heap_ctx ∗ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 ∗ is_atomic_syncer ϕ γ s }}}. Lemma atomic_spec (mk_syncer: val): Lemma atomic_spec (mk_syncer: val): mk_syncer_spec N mk_syncer → atomic_syncer_spec mk_syncer. mk_syncer_spec N mk_syncer → atomic_syncer_spec mk_syncer. ... @@ -50,7 +50,7 @@ Section atomic_sync. ... @@ -50,7 +50,7 @@ Section atomic_sync. iIntros (Hsync g0 ϕ HN ret) "[#Hh Hϕ] Hret". iIntros (Hsync g0 ϕ HN ret) "[#Hh Hϕ] Hret". iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]". iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]". { by rewrite pair_op dec_agree_idemp. } { by rewrite pair_op dec_agree_idemp. } iApply (Hsync (∃ g: A, ϕ g ★ gHalf γ g)%I with "[\$Hh Hg1 Hϕ]")=>//. iApply (Hsync (∃ g: A, ϕ g ∗ gHalf γ g)%I with "[\$Hh Hg1 Hϕ]")=>//. { iExists g0. by iFrame. } { iExists g0. by iFrame. } iNext. iIntros (s) "#Hsyncer". iApply "Hret". iNext. iIntros (s) "#Hsyncer". iApply "Hret". iSplitL "Hg2"; first done. iIntros "!#". iSplitL "Hg2"; first done. iIntros "!#". ... ...
 ... @@ -69,7 +69,7 @@ Section evmapR. ... @@ -69,7 +69,7 @@ Section evmapR. (* Some other supporting lemmas *) (* Some other supporting lemmas *) Lemma map_agree_none' γm (m: evmapR K A unitR) hd x: Lemma map_agree_none' γm (m: evmapR K A unitR) hd x: m !! hd = None → m !! hd = None → own γm (● m) ★ ev γm hd x ⊢ False. own γm (● m) ∗ ev γm hd x ⊢ False. Proof. Proof. iIntros (?) "[Hom Hev]". iIntros (?) "[Hom Hev]". iCombine "Hom" "Hev" as "Hauth". iCombine "Hom" "Hev" as "Hauth". ... @@ -80,7 +80,7 @@ Section evmapR. ... @@ -80,7 +80,7 @@ Section evmapR. Lemma map_agree_eq' γm m hd x agy: Lemma map_agree_eq' γm m hd x agy: m !! hd = Some ((), agy) → m !! hd = Some ((), agy) → ev γm hd x ★ own γm (● m) ⊢ DecAgree x = agy. ev γm hd x ∗ own γm (● m) ⊢ DecAgree x = agy. Proof. Proof. iIntros (?) "[#Hev Hom]". iIntros (?) "[#Hev Hom]". iCombine "Hom" "Hev" as "Hauth". iCombine "Hom" "Hev" as "Hauth". ... @@ -99,7 +99,7 @@ Section evmapR. ... @@ -99,7 +99,7 @@ Section evmapR. (* Evidence is the witness of membership *) (* Evidence is the witness of membership *) Lemma ev_map_witness γm m hd x: Lemma ev_map_witness γm m hd x: ev γm hd x ★ own γm (● m) ⊢ m !! hd = Some (∅, DecAgree x). ev γm hd x ∗ own γm (● m) ⊢ m !! hd = Some (∅, DecAgree x). Proof. Proof. iIntros "[#Hev Hom]". iIntros "[#Hev Hom]". destruct (m !! hd) as [[[] agy]|] eqn:Heqn. destruct (m !! hd) as [[[] agy]|] eqn:Heqn. ... @@ -109,7 +109,7 @@ Section evmapR. ... @@ -109,7 +109,7 @@ Section evmapR. (* Two evidences coincides *) (* Two evidences coincides *) Lemma evmap_frag_agree_split γm p (a1 a2: A): Lemma evmap_frag_agree_split γm p (a1 a2: A): ev γm p a1 ★ ev γm p a2 ⊢ a1 = a2. ev γm p a1 ∗ ev γm p a2 ⊢ a1 = a2. Proof. Proof. iIntros "[Ho Ho']". iIntros "[Ho Ho']". destruct (decide (a1 = a2)) as [->|Hneq]. destruct (decide (a1 = a2)) as [->|Hneq]. ... ...
 ... @@ -71,55 +71,55 @@ Section proof. ... @@ -71,55 +71,55 @@ Section proof. Context `{!heapG Σ, !lockG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace). Context `{!heapG Σ, !lockG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace). Definition init_s (ts: toks) := Definition init_s (ts: toks) := let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ★ own γ3 (Excl ()))%I. let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ∗ own γ3 (Excl ()))%I. Definition installed_s R (ts: toks) (f x: val) := Definition installed_s R (ts: toks) (f x: val) := let '(γx, γ1, _, γ4, γq) := ts in let '(γx, γ1, _, γ4, γq) := ts in (∃ (P: val → iProp Σ) Q, (∃ (P: val → iProp Σ) Q, own γx ((1/2)%Qp, DecAgree x) ★ P x ★ ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) ★ own γx ((1/2)%Qp, DecAgree x) ∗ P x ∗ ({{ R ∗ P x }} f x {{ v, R ∗ Q x v }}) ∗ saved_prop_own γq (Q x) ★ own γ1 (Excl ()) ★ own γ4 (Excl ()))%I. saved_prop_own γq (Q x) ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I. Definition received_s (ts: toks) (x: val) γr := Definition received_s (ts: toks) (x: val) γr := let '(γx, _, _, γ4, _) := ts in let '(γx, _, _, γ4, _) := ts in (own γx ((1/2/2)%Qp, DecAgree x) ★ own γr (Excl ()) ★ own γ4 (Excl ()))%I. (own γx ((1/2/2)%Qp, DecAgree x) ∗ own γr (Excl ()) ∗ own γ4 (Excl ()))%I. Definition finished_s (ts: toks) (x y: val) := Definition finished_s (ts: toks) (x y: val) := let '(γx, γ1, _, γ4, γq) := ts in let '(γx, γ1, _, γ4, γq) := ts in (∃ Q: val → val → iProp Σ, (∃ Q: val → val → iProp Σ, own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq (Q x) ★ own γx ((1/2)%Qp, DecAgree x) ∗ saved_prop_own γq (Q x) ∗ Q x y ★ own γ1 (Excl ()) ★ own γ4 (Excl ()))%I. Q x y ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I. Definition evm := ev loc toks. Definition evm := ev loc toks. (* p slot invariant *) (* p slot invariant *) Definition p_inv R (γm γr: gname) (v: val) := Definition p_inv R (γm γr: gname) (v: val) := (∃ (ts: toks) (p : loc), (∃ (ts: toks) (p : loc), v = #p ★ evm γm p ts ★ v = #p ∗ evm γm p ts ∗ ((* INIT *) ((* INIT *) (∃ y: val, p ↦{1/2} InjRV y ★ init_s ts)∨ (∃ y: val, p ↦{1/2} InjRV y ∗ init_s ts)∨ (* INSTALLED *) (* INSTALLED *) (∃ f x: val, p ↦{1/2} InjLV (f, x) ★ installed_s R ts f x) ∨ (∃ f x: val, p ↦{1/2} InjLV (f, x) ∗ installed_s R ts f x) ∨ (* RECEIVED *) (* RECEIVED *) (∃ f x: val, p ↦{1/2} InjLV (f, x) ★ received_s ts x γr) ∨ (∃ f x: val, p ↦{1/2} InjLV (f, x) ∗ received_s ts x γr) ∨ (* FINISHED *) (* FINISHED *) (∃ x y: val, p ↦{1/2} InjRV y ★ finished_s ts x y)))%I. (∃ x y: val, p ↦{1/2} InjRV y ∗ finished_s ts x y)))%I. Definition srv_stack_inv R γs γm γr s := (∃ xs, is_stack' (p_inv R γm γr) γs xs s)%I. Definition srv_stack_inv R γs γm γr s := (∃ xs, is_stack' (p_inv R γm γr) γs xs s)%I. Definition srv_tokm_inv γm := (∃ m : tokmR, own γm (● m) ★ [★ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I. Definition srv_tokm_inv γm := (∃ m : tokmR, own γm (● m) ∗ [∗ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I. Lemma install_push_spec R Lemma install_push_spec R (p: loc) (γs γm γr: gname) (ts: toks) (p: loc) (γs γm γr: gname) (ts: toks) (s: loc) (f x: val) (Φ: val → iProp Σ) : (s: loc) (f x: val) (Φ: val → iProp Σ) : heapN ⊥ N → heapN ⊥ N → heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★ heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ evm γm p ts ★ installed_s R ts f x ★ evm γm p ts ∗ installed_s R ts f x ∗ p ↦{1/2} InjLV (f, x) ★ ((∃ hd, evs γs hd #p) -★ Φ #()) p ↦{1/2} InjLV (f, x) ∗ ((∃ hd, evs γs hd #p) -∗ Φ #()) ⊢ WP push #s #p {{ Φ }}. ⊢ WP push #s #p {{ Φ }}. Proof. Proof. iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)". iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)". rewrite /srv_stack_inv. rewrite /srv_stack_inv. iDestruct (push_spec N (p_inv R γm γr) (fun v => (∃ hd, evs γs hd #p) ★ v = #())%I iDestruct (push_spec N (p_inv R γm γr) (fun v => (∃ hd, evs γs hd #p) ∗ v = #())%I with "[-HΦ]") as "Hpush"=>//. with "[-HΦ]") as "Hpush"=>//. - iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto. - iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto. iExists ts. iExists p. iSplit=>//. iFrame "Hpm". iExists ts. iExists p. iSplit=>//. iFrame "Hpm". ... @@ -132,16 +132,16 @@ Section proof. ... @@ -132,16 +132,16 @@ Section proof. Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) := Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) := let '(γx, _, γ3, _, γq) := ts in let '(γx, _, γ3, _, γq) := ts in (own γ3 (Excl ()) ★ own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq Q)%I. (own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, DecAgree x) ∗ saved_prop_own γq Q)%I. Lemma install_spec Lemma install_spec R P Q R P Q (f x: val) (γs γm γr: gname) (s: loc) (f x: val) (γs γm γr: gname) (s: loc) (Φ: val → iProp Σ): (Φ: val → iProp Σ): heapN ⊥ N → heapN ⊥ N → heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★ heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ P ★ ({{ R ★ P }} f x {{ v, R ★ Q v }}) ★ P ∗ ({{ R ∗ P }} f x {{ v, R ∗ Q v }}) ∗ (∀ (p: loc) (ts: toks), installed_recp ts x Q -★ evm γm p ts -★(∃ hd, evs γs hd #p) -★ Φ #p) (∀ (p: loc) (ts: toks), installed_recp ts x Q -∗ evm γm p ts -∗(∃ hd, evs γs hd #p) -∗ Φ #p) ⊢ WP install f x #s {{ Φ }}. ⊢ WP install f x #s {{ Φ }}. Proof. Proof. iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)". iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)". ... @@ -181,14 +181,14 @@ Section proof. ... @@ -181,14 +181,14 @@ Section proof. Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ: Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ: heapN ⊥ N → heapN ⊥ N → heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★ own γr (Excl ()) ★ R ★ heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ own γr (Excl ()) ∗ R ∗ is_list' γs hd xs ★ (own γr (Excl ()) -★ R -★ Φ #()) is_list' γs hd xs ∗ (own γr (Excl ()) -∗ R -∗ Φ #()) ⊢ WP iter #hd doOp {{ Φ }}. ⊢ WP iter #hd doOp {{ Φ }}. Proof. Proof. iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)". iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)". iApply (iter_spec N (p_inv R γm γr) Φ iApply (iter_spec N (p_inv R γm γr) Φ (* (fun v => v = #() ★ own γr (Excl ()) ★ R)%I *) (* (fun v => v = #() ∗ own γr (Excl ()) ∗ R)%I *) γs s (own γr (Excl ()) ★ R)%I (srv_tokm_inv γm) xs hd doOp doOp γs s (own γr (Excl ()) ∗ R)%I (srv_tokm_inv γm) xs hd doOp doOp with "[-]")=>//. with "[-]")=>//. - rewrite /f_spec. - rewrite /f_spec. iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')". iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')". ... @@ -296,12 +296,12 @@ Section proof. ... @@ -296,12 +296,12 @@ Section proof. Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()). Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()). Definition finished_recp (ts: toks) (x y: val) := Definition finished_recp (ts: toks) (x y: val) := let '(γx, _, _, _, γq) := ts in let '(γx, _, _, _, γq) := ts in (∃ Q, own γx ((1 / 2)%Qp, DecAgree x) ★ saved_prop_own γq (Q x) ★ Q x y)%I. (∃ Q, own γx ((1 / 2)%Qp, DecAgree x) ∗ saved_prop_own γq (Q x) ∗ Q x y)%I. Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ : Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ : heapN ⊥ N → heapN ⊥ N → heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★ heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ is_lock N γlk lk (own γr (Excl ()) ★ R) ★ Φ #() is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #() ⊢ WP try_srv lk #s {{ Φ }}. ⊢ WP try_srv lk #s {{ Φ }}. Proof. Proof. iIntros (?) "(#? & #? & #? & HΦ)". iIntros (?) "(#? & #? & #? & HΦ)". ... @@ -319,20 +319,20 @@ Section proof. ... @@ -319,20 +319,20 @@ Section proof. iModIntro. wp_let. iModIntro. wp_let. wp_bind (iter _ _). wp_bind (iter _ _). iApply wp_wand_r. iSplitL "HR Ho2 Hxs2". iApply wp_wand_r. iSplitL "HR Ho2 Hxs2". { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ★ R ★ v = #()))%I=>//. { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ∗ R ∗ v = #()))%I=>//. iFrame "#". iFrame. iIntros "? ?". by iFrame. } iFrame "#". iFrame. iIntros "? ?". by iFrame. } iIntros (f') "[Ho [HR %]]". subst. iIntros (f') "[Ho [HR %]]". subst. wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#★". wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗". iNext. iIntros. done. iNext. iIntros. done. Qed. Qed. Lemma loop_spec R (p s: loc) (lk: val) Lemma loop_spec R (p s: loc) (lk: val) (γs γr γm γlk: gname) (ts: toks) Φ: (γs γr γm γlk: gname) (ts: toks) Φ: heapN ⊥ N → heapN ⊥ N → heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★ heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ is_lock N γlk lk (own γr (Excl ()) ★ R) ★ is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ own_γ3 ts ★ evm γm p ts ★ own_γ3 ts ∗ evm γm p ts ∗ (∃ hd, evs γs hd #p) ★ (∀ x y, finished_recp ts x y -★ Φ y) (∃ hd, evs γs hd #p) ∗ (∀ x y, finished_recp ts x y -∗ Φ y) ⊢ WP loop #p #s lk {{ Φ }}. ⊢ WP loop #p #s lk {{ Φ }}. Proof. Proof. iIntros (HN) "(#Hh & #? & #? & Ho3 & #Hev & Hhd & HΦ)". iIntros (HN) "(#Hh & #? & #? & Ho3 & #Hev & Hhd & HΦ)". ... @@ -398,7 +398,7 @@ Section proof. ... @@ -398,7 +398,7 @@ Section proof. iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto. iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto. { iExists ∅. iFrame. by rewrite big_sepM_empty. } { iExists ∅. iFrame. by rewrite big_sepM_empty. } wp_seq. wp_bind (newlock _). wp_seq. wp_bind (newlock _). iApply (newlock_spec _ (own γr (Excl ()) ★ R)%I with "[\$Hh \$Ho2 \$HR]")=>//. iApply (newlock_spec _ (own γr (Excl ()) ∗ R)%I with "[\$Hh \$Ho2 \$HR]")=>//. iNext. iIntros (lk γlk) "#Hlk". iNext. iIntros (lk γlk) "#Hlk". wp_let. wp_bind (new_stack _). wp_let. wp_bind (new_stack _). iApply (new_stack_spec' _ (p_inv _ γm γr))=>//. iApply (new_stack_spec' _ (p_inv _ γm γr))=>//. ... ...
 ... @@ -21,7 +21,7 @@ End lemmas. ... @@ -21,7 +21,7 @@ End lemmas. Section excl. Section excl. Context `{!inG Σ (exclR unitC)}. Context `{!inG Σ (exclR unitC)}. Lemma excl_falso γ Q': Lemma excl_falso γ Q': own γ (Excl ()) ★ own γ (Excl ()) ⊢ Q'. own γ (Excl ()) ∗ own γ (Excl ()) ⊢ Q'. Proof. Proof. iIntros "[Ho1 Ho2]". iCombine "Ho1" "Ho2" as "Ho". iIntros "[Ho1 Ho2]". iCombine "Ho1" "Ho2" as "Ho". iExFalso. by iDestruct (own_valid with "Ho") as "%". iExFalso. by iDestruct (own_valid with "Ho") as "%". ... @@ -33,7 +33,7 @@ Section heap_extra. ... @@ -33,7 +33,7 @@ Section heap_extra. Lemma bogus_heap p (q1 q2: Qp) a b: Lemma bogus_heap p (q1 q2: Qp) a b: ~((q1 + q2)%Qp ≤ 1%Qp)%Qc → ~((q1 + q2)%Qp ≤ 1%Qp)%Qc → heap_ctx ★ p ↦{q1} a ★ p ↦{q2} b ⊢ False. heap_ctx ∗ p ↦{q1} a ∗ p ↦{q2} b ⊢ False. Proof. Proof. iIntros (?) "(#Hh & Hp1 & Hp2)". iIntros (?) "(#Hh & Hp1 & Hp2)". iCombine "Hp1" "Hp2" as "Hp". iCombine "Hp1" "Hp2" as "Hp". ... @@ -52,12 +52,12 @@ Section big_op_later. ... @@ -52,12 +52,12 @@ Section big_op_later. Lemma big_sepM_delete_later Φ m i x : Lemma big_sepM_delete_later Φ m i x : m !! i = Some x → m !! i = Some x → ▷ ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ ▷ Φ i x ★ ▷ [★ map] k↦y ∈ delete i m, Φ k y. ▷ ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ ▷ Φ i x ∗ ▷ [∗ map] k↦y ∈ delete i m, Φ k y. Proof. intros ?. rewrite big_sepM_delete=>//. apply later_sep. Qed. Proof. intros ?. rewrite big_sepM_delete=>//. apply later_sep. Qed. Lemma big_sepM_insert_later Φ m i x : Lemma big_sepM_insert_later Φ m i x : m !! i = None → m !! i = None → ▷ ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ ▷ Φ i x ★ ▷ [★ map] k↦y ∈ m, Φ k y. ▷ ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ ▷ Φ i x ∗ ▷ [∗ map] k↦y ∈ m, Φ k y. Proof. intros ?. rewrite big_sepM_insert=>//. apply later_sep. Qed. Proof. intros ?. rewrite big_sepM_insert=>//. apply later_sep. Qed. End big_op_later. End big_op_later. ... @@ -65,7 +65,7 @@ Section pair. ... @@ -65,7 +65,7 @@ Section pair. Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}. Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}. Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A): Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A): own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2) ⊢ (a1 = a2). own γm (q1, DecAgree a1) ∗ own γm (q2, DecAgree a2) ⊢ (a1 = a2). Proof. Proof. iIntros "[Ho Ho']". iIntros "[Ho Ho']". destruct (decide (a1 = a2)) as [->|Hneq]=>//. destruct (decide (a1 = a2)) as [->|Hneq]=>//. ... @@ -76,8 +76,8 @@ Section pair. ... @@ -76,8 +76,8 @@ Section pair. Qed. Qed. Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A): Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A): own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2) own γm (q1, DecAgree a1) ∗ own γm (q2, DecAgree a2) ⊢ own γm ((q1 + q2)%Qp, DecAgree a1) ★ (a1 = a2). ⊢ own γm ((q1 + q2)%Qp, DecAgree a1) ∗ (a1 = a2). Proof. Proof. iIntros "[Ho Ho']". iIntros "[Ho Ho']". iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame. iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame. ... ...
 ... @@ -16,13 +16,13 @@ Section defs. ... @@ -16,13 +16,13 @@ Section defs. Fixpoint is_list' (γ: gname) (hd: loc) (xs: list val) : iProp Σ := Fixpoint is_list' (γ: gname) (hd: loc) (xs: list val) : iProp Σ := match xs with match xs with | [] => (∃ q, hd ↦{ q } NONEV)%I | [] => (∃ q, hd ↦{ q } NONEV)%I | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ★ evs γ hd x ★ is_list' γ hd' xs)%I | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ evs γ hd x ∗ is_list' γ hd' xs)%I end. end. Lemma in_list' γ x xs: Lemma in_list' γ x xs: ∀ hd, x ∈ xs → ∀ hd, x ∈ xs → is_list' γ hd xs is_list' γ hd xs ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ★ evs γ hd' x. ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ∗ evs γ hd' x. Proof. Proof. induction xs as [|x' xs' IHxs']. induction xs as [|x' xs' IHxs']. - intros ? Hin. inversion Hin. - intros ? Hin. inversion Hin. ... @@ -36,13 +36,13 @@ Section defs. ... @@ -36,13 +36,13 @@ Section defs. iApply IHxs'=>//. iApply IHxs'=>//. Qed. Qed. Definition perR' hd v v' := (v = ((∅: unitR), DecAgree v') ★ R v' ★ allocated hd)%I. Definition perR' hd v v' := (v = ((∅: unitR), DecAgree v') ∗ R v' ∗ allocated hd)%I. Definition perR hd v := (∃ v', perR' hd v v')%I. Definition perR hd v := (∃ v', perR' hd v v')%I. Definition allR γ := (∃ m : evmapR loc val unitR, own γ (● m) ★ [★ map] hd ↦ v ∈ m, perR hd v)%I. Definition allR γ := (∃ m : evmapR loc val unitR, own γ (● m) ∗ [∗ map] hd ↦ v ∈ m, perR hd v)%I. Definition is_stack' γ xs s := Definition is_stack' γ xs s := (∃ hd: loc, s ↦ #hd ★ is_list' γ hd xs ★ allR γ)%I. (∃ hd: loc, s ↦ #hd ∗ is_list' γ hd xs ∗ allR γ)%I. Global Instance is_list'_timeless γ hd xs: TimelessP (is_list' γ hd xs). Global Instance is_list'_timeless γ hd xs: TimelessP (is_list' γ hd xs). Proof. generalize hd. induction xs; apply _. Qed. Proof. generalize hd. induction xs; apply _. Qed. ... @@ -51,7 +51,7 @@ Section defs. ... @@ -51,7 +51,7 @@ Section defs. Proof. apply _. Qed. Proof. apply _. Qed. Lemma dup_is_list' γ : ∀ xs hd, Lemma dup_is_list' γ : ∀ xs hd, heap_ctx ★ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ★ is_list' γ hd xs. heap_ctx ∗ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list' γ hd xs. Proof. Proof. induction xs as [|y xs' IHxs']. induction xs as [|y xs' IHxs']. - iIntros (hd) "(#? & Hs)". - iIntros (hd) "(#? & Hs)". ... @@ -63,7 +63,7 @@ Section defs. ... @@ -63,7 +63,7 @@ Section defs. Qed. Qed. Lemma extract_is_list γ : ∀ xs hd, Lemma extract_is_list γ : ∀ xs hd, heap_ctx ★ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ★ is_list hd xs. heap_ctx ∗ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list hd xs. Proof. Proof. induction xs as [|y xs' IHxs']. induction xs as [|y xs' IHxs']. - iIntros (hd) "(#? & Hs)". - iIntros (hd) "(#? & Hs)". ... @@ -78,8 +78,8 @@ Section defs. ... @@ -78,8 +78,8 @@ Section defs. (* Rf, RI is some frame *) (* Rf, RI is some frame *) ∀ Φ (x: val), ∀ Φ (x: val), heapN ⊥ N → heapN ⊥ N → heap_ctx ★ inv N ((∃ xs, is_stack' γ xs s) ★ RI) ★ (∃ hd, evs γ hd x) ★ heap_ctx ∗ inv N ((∃ xs, is_stack' γ xs s) ∗ RI) ∗ (∃ hd, evs γ hd x) ∗ Rf ★ (Rf -★ Φ #()) Rf ∗ (Rf -∗ Φ #()) ⊢ WP f x {{ Φ }}. ⊢ WP f x {{ Φ }}. End defs. End defs. ... @@ -89,7 +89,7 @@ Section proofs. ... @@ -89,7 +89,7 @@ Section proofs. Lemma new_stack_spec' Φ RI: Lemma new_stack_spec' Φ RI: heapN ⊥ N → heapN ⊥ N → heap_ctx ★ RI ★ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ★ RI) -★ Φ #s) heap_ctx ∗ RI ∗ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) -∗ Φ #s) ⊢ WP new_stack #() {{ Φ }}. ⊢ WP new_stack #() {{ Φ }}. Proof. Proof. iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd. iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd. ... @@ -97,19 +97,19 @@ Lemma new_stack_spec' Φ RI: ... @@ -97,19 +97,19 @@ Lemma new_stack_spec' Φ RI: { apply auth_valid_discrete_2. done. } { apply auth_valid_discrete_2. done. } wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl". wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl". wp_alloc s as "Hs". wp_alloc s as "Hs". iAssert ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']" as "Hinv". iAssert ((∃ xs : list val, is_stack' R γ xs s) ∗ RI)%I with "[-HΦ Hm']" as "Hinv". { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl". { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl". - eauto. - eauto. - iExists ∅. iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). } - iExists ∅. iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). } iMod (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']") as "#?"; first eauto. iMod (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ∗ RI)%I with "[-HΦ Hm']") as "#?"; first eauto. by iApply "HΦ". by iApply "HΦ". Qed. Qed. Lemma iter_spec Φ γ s (Rf RI: iProp Σ): Lemma iter_spec Φ γ s (Rf RI: iProp Σ): ∀ xs hd (f: expr) (f': val),