Bake a binder in the notation for the postcondition of wp and triples.

That way, we do not have useless type annotations of the form
"v : language.val heap_lang" cluttering about any goal.

Note, that we could decide to eta expand everywhere (as we do for ∀
and ∃), and use the notation "WP e {{ Q }}" for "wp e ⊤ (λ _, Q)".
parent d8f499d5
 ... ... @@ -16,7 +16,7 @@ Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) : Proof. by rewrite -wp_if_true -wp_value. Qed. Lemma wp_assert' {Σ} (Φ : val → iProp heap_lang Σ) e : WP e {{ λ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}. WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}. Proof. rewrite /Assert. wp_focus e; apply wp_mono=>v. apply uPred.const_elim_l=>->. apply wp_assert. ... ...
 ... ... @@ -17,7 +17,7 @@ Section client. Local Notation iProp := (iPropG heap_lang Σ). Definition y_inv (q : Qp) (l : loc) : iProp := (∃ f : val, l ↦{q} f ★ □ ∀ n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I. (∃ f : val, l ↦{q} f ★ □ ∀ n : Z, WP f #n {{ v, v = #(n + 42) }})%I. Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ★ y_inv (q/2) l). Proof. ... ... @@ -27,7 +27,7 @@ Section client. Lemma worker_safe q (n : Z) (b y : loc) : (heap_ctx heapN ★ recv heapN N b (y_inv q y)) ⊢ WP worker n (%b) (%y) {{ λ _, True }}. ⊢ WP worker n (%b) (%y) {{ _, True }}. Proof. iIntros "[#Hh Hrecv]". wp_lam. wp_let. wp_apply wait_spec; iFrame "Hrecv". ... ... @@ -36,7 +36,7 @@ Section client. iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"]. Qed. Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ λ _, True }}. Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ _, True }}. Proof. iIntros {?} "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let. wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done. ... ... @@ -61,7 +61,7 @@ Section ClosedProofs. Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ]. Notation iProp := (iPropG heap_lang Σ). Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}. Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}. Proof. iIntros "! Hσ". iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done. ... ...
 ... ... @@ -13,10 +13,10 @@ Local Notation iProp := (iPropG heap_lang Σ). Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → ∃ recv send : loc → iProp -n> iProp, (∀ P, heap_ctx heapN ⊢ {{ True }} newbarrier #() {{ λ v, (∀ P, heap_ctx heapN ⊢ {{ True }} newbarrier #() {{ v, ∃ l : loc, v = LocV l ★ recv l P ★ send l P }}) ∧ (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧ (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) {{ _, P }}) ∧ (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧ (∀ l P Q, (P -★ Q) ⊢ (recv l P -★ recv l Q)). Proof. ... ...
 ... ... @@ -13,11 +13,11 @@ Implicit Types ef : option (expr []). (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *) Lemma wp_bind {E e} K Φ : WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. Proof. exact: wp_ectx_bind. Qed. Lemma wp_bindi {E e} Ki Φ : WP e @ E {{ λ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢ WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢ WP fill_item Ki e @ E {{ Φ }}. Proof. exact: weakestpre.wp_bind. Qed. ... ... @@ -81,7 +81,7 @@ Qed. (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e Φ : (▷ Φ (LitV LitUnit) ★ ▷ WP e {{ λ _, True }}) ⊢ WP Fork e @ E {{ Φ }}. (▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }}) ⊢ WP Fork e @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=; last by intros; inv_head_step; eauto. ... ...
 ... ... @@ -2,6 +2,7 @@ From iris.heap_lang Require Export derived. Export heap_lang. Arguments wp {_ _} _ _%E _. Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ) (at level 20, e, Φ at level 200, format "'WP' e @ E {{ Φ } }") : uPred_scope. ... ... @@ -9,6 +10,13 @@ Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ) (at level 20, e, Φ at level 200, format "'WP' e {{ Φ } }") : uPred_scope. Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q)) (at level 20, e, Q at level 200, format "'WP' e @ E {{ v , Q } }") : uPred_scope. Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) (at level 20, e, Q at level 200, format "'WP' e {{ v , Q } }") : uPred_scope. Coercion LitInt : Z >-> base_lit. Coercion LitBool : bool >-> base_lit. Coercion App : expr >-> Funclass. ... ...
 ... ... @@ -84,7 +84,7 @@ Qed. Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ λ v', ■ φ v' }} → (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ v', ■ φ v' }} → rtc step ([e], σ1) (of_val v :: t2, σ2) → φ v. Proof. ... ... @@ -100,7 +100,7 @@ Qed. Lemma ht_adequacy_result E φ e v t2 σ1 m σ2 : ✓ m → {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■ φ v' }} → {{ ownP σ1 ★ ownG m }} e @ E {{ v', ■ φ v' }} → rtc step ([e], σ1) (of_val v :: t2, σ2) → φ v. Proof. ... ...
 ... ... @@ -14,7 +14,7 @@ Hint Resolve head_prim_reducible head_reducible_prim_step. Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I. Lemma wp_ectx_bind {E e} K Φ : WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. Proof. apply: weakestpre.wp_bind. Qed. Lemma wp_lift_head_step E1 E2 ... ...
 ... ... @@ -19,6 +19,19 @@ Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e Φ) (at level 20, P, e, Φ at level 200, format "{{ P } } e {{ Φ } }") : C_scope. Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q)) (at level 20, P, e, Q at level 200, format "{{ P } } e @ E {{ v , Q } }") : uPred_scope. Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e (λ v, Q)) (at level 20, P, e, Q at level 200, format "{{ P } } e {{ v , Q } }") : uPred_scope. Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e (λ v, Q)) (at level 20, P, e, Q at level 200, format "{{ P } } e @ E {{ v , Q } }") : C_scope. Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e (λ v, Q)) (at level 20, P, e, Q at level 200, format "{{ P } } e {{ v , Q } }") : C_scope. Section hoare. Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q : iProp Λ Σ. ... ... @@ -42,8 +55,7 @@ Proof. solve_proper. Qed. Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}. Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed. Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}. Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ v', v = v' }}. Proof. iIntros "! _". by iApply wp_value'. Qed. Lemma ht_vs E P P' Φ Φ' e : ... ... @@ -83,18 +95,18 @@ Proof. Qed. Lemma ht_frame_l E P Φ R e : {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ λ v, R ★ Φ v }}. {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ v, R ★ Φ v }}. Proof. iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp". Qed. Lemma ht_frame_r E P Φ R e : {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ λ v, Φ v ★ R }}. {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ v, Φ v ★ R }}. Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed. Lemma ht_frame_step_l E P R e Φ : to_val e = None → {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}. {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ v, R ★ Φ v }}. Proof. iIntros {?} "#Hwp ! [HR HP]". iApply wp_frame_step_l; try done. iFrame "HR". by iApply "Hwp". ... ... @@ -102,7 +114,7 @@ Qed. Lemma ht_frame_step_r E P Φ R e : to_val e = None → {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}. {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ v, Φ v ★ R }}. Proof. iIntros {?} "#Hwp ! [HP HR]". iApply wp_frame_step_r; try done. iFrame "HR". by iApply "Hwp". ... ... @@ -110,7 +122,7 @@ Qed. Lemma ht_inv N E P Φ R e : atomic e → nclose N ⊆ E → (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ λ v, ▷ R ★ Φ v }}) (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ v, ▷ R ★ Φ v }}) ⊢ {{ P }} e @ E {{ Φ }}. Proof. iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto. ... ...
 ... ... @@ -3,14 +3,14 @@ From iris.program_logic Require Export hoare lifting. From iris.program_logic Require Import ownership. From iris.proofmode Require Import tactics pviewshifts. Local Notation "{{ P } } ef ?@ E {{ Φ } }" := (default True%I ef (λ e, ht E P e Φ)) (at level 20, P, ef, Φ at level 200, format "{{ P } } ef ?@ E {{ Φ } }") : uPred_scope. Local Notation "{{ P } } ef ?@ E {{ Φ } }" := (True ⊢ default True ef (λ e, ht E P e Φ)) (at level 20, P, ef, Φ at level 200, format "{{ P } } ef ?@ E {{ Φ } }") : C_scope. Local Notation "{{ P } } ef ?@ E {{ v , Q } }" := (default True%I ef (λ e, ht E P e (λ v, Q))) (at level 20, P, ef, Q at level 200, format "{{ P } } ef ?@ E {{ v , Q } }") : uPred_scope. Local Notation "{{ P } } ef ?@ E {{ v , Q } }" := (True ⊢ default True ef (λ e, ht E P e (λ v, Q))) (at level 20, P, ef, Q at level 200, format "{{ P } } ef ?@ E {{ v , Q } }") : C_scope. Section lifting. Context {Λ : language} {Σ : iFunctor}. ... ... @@ -26,7 +26,7 @@ Lemma ht_lift_step E1 E2 ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧ (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧ (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})) (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})) ⊢ {{ P }} e1 @ E1 {{ Ψ }}. Proof. iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP". ... ... @@ -45,8 +45,8 @@ Lemma ht_lift_atomic_step atomic e1 → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ λ _, True }}) ⊢ {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}. (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ _, True }}) ⊢ {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}. Proof. iIntros {? Hsafe Hstep} "#Hef". set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef). ... ... @@ -68,7 +68,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) → ((∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧ (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})) (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ _, True }})) ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}. Proof. iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP". ... ... @@ -83,7 +83,7 @@ Lemma ht_lift_pure_det_step to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→ ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ λ _, True }}) ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }}) ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}. Proof. iIntros {? Hsafe Hdet} "[#He2 #Hef]". ... ...
 ... ... @@ -82,13 +82,13 @@ Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed. Lemma wp_inv E e N P Φ R : atomic e → nclose N ⊆ E → R ⊢ inv N P → R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) → R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ v, ▷ P ★ Φ v }}) → R ⊢ WP e @ E {{ Φ }}. Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed. Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R : atomic e → nclose N ⊆ E → R ⊢ inv N P → R ⊢ (P -★ WP e @ E ∖ nclose N {{ λ v, P ★ Φ v }}) → R ⊢ (P -★ WP e @ E ∖ nclose N {{ v, P ★ Φ v }}) → R ⊢ WP e @ E {{ Φ }}. Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed. ... ...
 ... ... @@ -64,6 +64,13 @@ Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ) (at level 20, e, Φ at level 200, format "'WP' e {{ Φ } }") : uPred_scope. Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q)) (at level 20, e, Q at level 200, format "'WP' e @ E {{ v , Q } }") : uPred_scope. Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q)) (at level 20, e, Q at level 200, format "'WP' e {{ v , Q } }") : uPred_scope. Section wp. Context {Λ : language} {Σ : iFunctor}. Implicit Types P : iProp Λ Σ. ... ... @@ -141,7 +148,7 @@ Proof. rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. eapply wp_step_inv with (S k) r'; eauto. Qed. Lemma wp_pvs E e Φ : WP e @ E {{ λ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}. Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}. Proof. rewrite wp_eq. split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ. ... ... @@ -155,7 +162,7 @@ Proof. Qed. Lemma wp_atomic E1 E2 e Φ : E2 ⊆ E1 → atomic e → (|={E1,E2}=> WP e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}. (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}. Proof. rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor. eauto using atomic_not_val. intros rf k Ef σ1 ???. ... ... @@ -172,7 +179,7 @@ Proof. - by rewrite -assoc. - constructor; apply pvs_intro; auto. Qed. Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ R) ⊢ WP e @ E {{ λ v, Φ v ★ R }}. Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ R) ⊢ WP e @ E {{ v, Φ v ★ R }}. Proof. rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp. ... ... @@ -190,7 +197,7 @@ Proof. - apply IH; eauto using uPred_weaken. Qed. Lemma wp_frame_step_r E e Φ R : to_val e = None → (WP e @ E {{ Φ }} ★ ▷ R) ⊢ WP e @ E {{ λ v, Φ v ★ R }}. to_val e = None → (WP e @ E {{ Φ }} ★ ▷ R) ⊢ WP e @ E {{ v, Φ v ★ R }}. Proof. rewrite wp_eq. intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). ... ... @@ -207,7 +214,7 @@ Proof. eapply uPred_weaken with n rR; eauto. Qed. Lemma wp_bind `{LanguageCtx Λ K} E e Φ : WP e @ E {{ λ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}. WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}. Proof. rewrite wp_eq. split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?. ... ... @@ -239,19 +246,19 @@ Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed. Lemma wp_value_pvs E Φ e v : to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}. Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed. Lemma wp_frame_l E e Φ R : (R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ★ Φ v }}. Lemma wp_frame_l E e Φ R : (R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ★ Φ v }}. Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed. Lemma wp_frame_step_l E e Φ R : to_val e = None → (▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ★ Φ v }}. to_val e = None → (▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ★ Φ v }}. Proof. rewrite (comm _ (▷ R)%I); setoid_rewrite (comm _ R). apply wp_frame_step_r. Qed. Lemma wp_always_l E e Φ R `{!PersistentP R} : (R ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ∧ Φ v }}. (R ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ∧ Φ v }}. Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed. Lemma wp_always_r E e Φ R `{!PersistentP R} : (WP e @ E {{ Φ }} ∧ R) ⊢ WP e @ E {{ λ v, Φ v ∧ R }}. (WP e @ E {{ Φ }} ∧ R) ⊢ WP e @ E {{ v, Φ v ∧ R }}. Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed. Lemma wp_wand_l E e Φ Ψ : ((∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Ψ }}. ... ...
 ... ... @@ -24,7 +24,7 @@ Section LiftingTests. Definition heap_e : expr [] := let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x". Lemma heap_e_spec E N : nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ λ v, v = #2 }}. nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}. Proof. iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done. wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load. ... ... @@ -58,7 +58,7 @@ Section LiftingTests. Qed. Lemma Pred_user E : (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}. (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ v, v = #40 }}. Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed. End LiftingTests. ... ... @@ -66,7 +66,7 @@ Section ClosedProofs. Definition Σ : gFunctors := #[ heapGF ]. Notation iProp := (iPropG heap_lang Σ). Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}. Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}. Proof. iProof. iIntros "! Hσ". iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot. ... ...
 ... ... @@ -19,8 +19,8 @@ Definition barrier_res γ (Φ : X → iProp) : iProp := (∃ x, one_shot_own γ x ★ Φ x)%I. Lemma worker_spec e γ l (Φ Ψ : X → iProp) : (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ λ _, Ψ x }}) ⊢ WP wait (%l) ;; e {{ λ _, barrier_res γ Ψ }}. (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ _, Ψ x }}) ⊢ WP wait (%l) ;; e {{ _, barrier_res γ Ψ }}. Proof. iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl". iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]". ... ... @@ -50,10 +50,10 @@ Qed. Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) : heapN ⊥ N → eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 → (heap_ctx heapN ★ P ★ {{ P }} eM {{ λ _, ∃ x, Φ x }} ★ (∀ x, {{ Φ1 x }} eW1 {{ λ _, Ψ1 x }}) ★ (∀ x, {{ Φ2 x }} eW2 {{ λ _, Ψ2 x }})) ⊢ WP client eM' eW1' eW2' {{ λ _, ∃ γ, barrier_res γ Ψ }}. ★ {{ P }} eM {{ _, ∃ x, Φ x }} ★ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) ★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})) ⊢ WP client eM' eW1' eW2' {{ _, ∃ γ, barrier_res γ Ψ }}. Proof. iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client. iPvs one_shot_alloc as {γ} "Hγ". ... ...
 ... ... @@ -37,8 +37,8 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp := Lemma wp_one_shot (Φ : val → iProp) : (heap_ctx heapN ★ ∀ f1 f2 : val, (∀ n : Z, □ WP f1 #n {{ λ w, w = #true ∨ w = #false }}) ★ □ WP f2 #() {{ λ g, □ WP g #() {{ λ _, True }} }} -★ Φ (f1,f2)%V) (∀ n : Z, □ WP f1 #n {{ w, w = #true ∨ w = #false }}) ★ □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -★ Φ (f1,f2)%V) ⊢ WP one_shot_example #() {{ Φ }}. Proof. iIntros "[#? Hf] /=". ... ... @@ -83,9 +83,9 @@ Qed. Lemma hoare_one_shot (Φ : val → iProp) : heap_ctx heapN ⊢ {{ True }} one_shot_example #() {{ λ ff, (∀ n : Z, {{ True }} Fst ff #n {{ λ w, w = #true ∨ w = #false }}) ★ {{ True }} Snd ff #() {{ λ g, {{ True }} g #() {{ λ _, True }} }} {{ ff, (∀ n : Z, {{ True }} Fst ff #n {{ w, w = #true ∨ w = #false }}) ★ {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }} }}. Proof. iIntros "#? ! _". iApply wp_one_shot. iSplit; first done. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!